Re: [isabelle] Equal on function objects
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).
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"?
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 !
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))"
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
Adenauerring 20a, Gebäude 50.41, Raum 023
Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
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