Re: [isabelle] Equal on function objects

Hi John,

Now, given similar lemmas, it seems several lemmas with a False consequence can be proven. For example, given:

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?
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.

Does Isabelle simplify lem4's goal to False?
Yes, if you tell Isabelle to do so. Try

thm lem4
thm lem4[simplified]

> Or even, does it try to simplify every goal to False
first before moving on?
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 on Isabelle/HOL.


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