Re: [isabelle] Equal on function objects
Now, given similar lemmas, it seems several lemmas with a False
consequence can be proven. For example, given:
Depends on your understanding of essentially. Syntactically, they are
inherently different. For reasoning, they also behave differently (lem4
cannot be used as an introduction rule for "False", for instance).
However, you can prove everything with either of them, so logically,
they are the same.
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?
Yes, if you tell Isabelle to do so. Try
> Or even, does it try to simplify every goal to False
No, Isabelle does no simplification by its own. However, whenever you
apply some method or tactic which invokes the simplifier (like simp,
simp_all, clarsimp, auto, fastsimp, bestsimp, force) then the simplifier
uses its set of rewrite rules to simplify to the goal. Methods and
tactics without simplifier (like rule, clarify, safe, blast, iprover,
best, fast) obviously don't do this.
For more information about the simplifier, read Sec. 3.1 in the Tutorial
first before moving on?
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