# 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.
`
Regards,
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.*