# 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.
`
Andreas
--
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.edu
http://pp.info.uni-karlsruhe.de

`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.*