[isabelle] Equal on function objects
I'm trying to show that two function objects are equal in the following:
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:
shows "func2 = (%s. func1 s * func3 s)"
Does anyone know why having lem1 as a fact is insufficient to complete
Any help will be appreciated.
This archive was generated by a fusion of
Pipermail (Mailman edition) and