Re: [isabelle] Equal on function objects
Thanks for the input -- that's very useful.
Now, given similar lemmas, it seems several lemmas with a False consequence
can be proven. For example, given:
types S = "T set"
func1 :: "T ⇒ real"
func2 :: "T ⇒ real"
func3 :: "T ⇒ real"
locale loc1 =
assumes ax11: "func1 p = func2 p / func3 p"
and ax12: "func3 p > 0"
locale loc2 =
fixes G :: S
assumes ax21: "EX g : G. func1 g ≠ func2 g / func3 g"
locale loc3 = loc1 + loc2
lemma (in loc3) lem4:
shows "EX g. func1 g ≠ func 1 g"
using ax21 ax11
lemma (in loc3) lem5:
using ax21 ax11
Are lem4 and lem5 essentially the same? Does Isabelle simplify lem4's goal
to False? Or even, does it try to simplify every goal to False first before
On Feb 22, 2010 4:24pm, Andreas Lochbihler <andreas.lochbihler at kit.edu>
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, ie:
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. fx = gx) == (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