Re: [isabelle] Equal on function objects

John Munroe wrote:

I'm trying to show that two function objects are equal in the following:

theory T1
imports Real

typedecl T

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?

Try rule 'ext', specifically by (auto intro: ext)
by (blast intro: ext) also solves it

Isabelle doesn't apply ext within auto by default, possibly as it can lead to explosions with recursive functions.


Rafal Kolanski.

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