Re: [isabelle] Equal on function objects

Hi John,

Thanks for the help. Just curious, what if loc.ax1 is changed to:

"EX p. func1 p ~= func2 p / func3 p"

Can auto/blast intro: ext still be used to show that

"func1 ~= func2 / func3"?
What should func2 / func3 be? There is no division operator for functions in HOL by default. I guess you mean "%p. func2 p / func3 p". No, you cannot use ext for that: The inequality is first turned into equality in the assumptions by the rule notI, which leaves you to show False. Since ext is typically used as an introduction rule, it cannot be applied to False. In this case, expand the function equality in the assumptions with expand_fun_eq: by(auto simp: expand_fun_eq).

In fact, why isn't ext defined with iff instead, i.e.:

lemma ext: "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) <==> (%x. f(x))=(%x. g(x))"
Since "%x. f(x)" is eta-equal to f and similarly for g, the backward direction of your rule is build into the simplifier, so it is hardly useful. Your lemma is almost expand_fun_eq[symmetric], except for the meta-quantifier !! being replaced the HOL quantifier !
If you like, you could also prove this lemma:

lemma "(!!x. f x = g x) == (Trueprop (f = g))"
by(rule equal_intr_rule)(auto intro: ext)

Note that there is no meta-biimplication in Isabelle, so I used meta-equality instead. Trueprop converts boolean terms to propositions and is added to most lemmas implicitly. Since meta-quantifiers are mixed with meta-equality here, it must be explicitly written out.


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft

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