# [isabelle] Equal on function objects

Hi,
I'm trying to show that two function objects are equal in the following:
theory T1
imports Real
begin
typedecl T
consts
func1 :: "T => real"
func2 :: "T => real"
func3 :: "T => real"
locale loc =
assumes ax1: "func1 p = func2 p / func3 p"
and ax2: "func3 p > 0"
lemma (in loc) lem1: "ALL p. func2 p = func1 p * func3 p"
using ax1 ax2
by (metis divide_le_eq divide_less_eq order_eq_refl order_less_irrefl xt1(11))
lemma (in loc) lem2:
assumes "loc"
shows "func2 = (%s. func1 s * func3 s)"
using lem1
by auto
Does anyone know why having lem1 as a fact is insufficient to complete
the proof?
Any help will be appreciated.
Thanks,
John

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*