[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.