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:

typedecl T
types S = "T set"

consts
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
by auto

lemma (in loc3) lem5:
shows "False"
using ax21 ax11
by auto

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 moving on?

Thanks again
John

On Feb 22, 2010 4:24pm, Andreas Lochbihler <andreas.lochbihler at kit.edu> wrote:
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, 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.



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.