Email Gateway (Aug 18 2022 at 12:49): Email Gateway (Aug 18 2022 at 12:49):From: Chris Capel <pdf23ds@gmail.com>
I'm reading "Introduction to Isabelle", which has a very nice few
chapters on the low-level user-visible parts of Isabelle. I'm
surprised it's not linked from the Documentation page on the main
site, even if it does have a long section on shell interaction. None
of the other documents come close to the level of detail as to how
Isabelle really works, and none leave me feeling as if I really
understand what I'm doing when I'm executing a proof. It's nice that
even though I'm not a mathematician (by any means), I was able to read
a few Wikipedia articles for background and understand almost all of
it.
Anyway, I'm a bit slow with all of this, being new to formal math, and
I'm having trouble understanding how part of elim resolution is
justified logically. Take the example from ITI 5.3 and 6.1:
[| P | P ==> P |] ==> P | P --> P
To prove this, we'd like to apply elim resolution (erule) to the only
subgoal with disjE, which reads
[| Q | R; Q ==> S; R ==> S |] ==> S
First disjE needs to be lifted:
[| P | P ==> ?Q | ?R; [| P | P; ?Q |] ==> ?S; [| P | P; ?R |] ==> ?S
|] ==> (P | P ==> ?S)
I follow up to this point. Here the book skips right to [| P ==> P; P
==> P |] ==> P | P --> P. I understand how it was unified, and I
understand how the first subgoal, "P | P ==> ?Q | ?R" before
unification, was discharged automatically as part of elim resolution,
but I don't understand how the first assumption "P | P" from the two
remaining subgoals can be eliminated. How is that justified?
To restate, the book says that elim resolution replaces subgoal phi_i
of the proof with lifted assumptions psi'_2 ... psi'_m from the
resolution rule, except with the assumption of psi'_1 deleted
(assuming psi'_1 was solved by assumption). How is that last part
justified? Unless I'm missing something, the book skips that detail.
Chris Capel
Email Gateway (Aug 18 2022 at 12:50):From: Lawrence Paulson <lp15@cam.ac.uk>
The removal of an assumption indeed sounds like we are getting
something for nothing. However, remember that we use backward proof;
removal of an assumption actually means you have to prove the subgoal
With fewer facts than you were entitled to use. The reason it is
beneficial to remove this assumption is simply that it will be
redundant.
Larry Paulson
Email Gateway (Aug 18 2022 at 12:50):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Hello Chris
Can you give me a link to this? "Introduction to Isabelle" is a very
unfortunate search term for web search ...
smime.p7s
Email Gateway (Aug 18 2022 at 12:50):From: Lawrence Paulson <lp15@cam.ac.uk>
Historical Isabelle documentation is available, along with other old
papers, at this webpage:
http://www.cl.cam.ac.uk/~lp15/papers/techreports.html
Various other Isabelle related papers of mine can be downloaded from
another webpage:
http://www.cl.cam.ac.uk/~lp15/papers/isabelle.html
There are indeed a lot of insights to be gained from these old papers,
but please bear in mind that they refer to earlier versions of
Isabelle and many of the examples in them may no longer work.
Larry Paulson
Email Gateway (Aug 18 2022 at 12:50):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Christian Doczkal wrote:
This document was in the Isabelle distribution up to, so far as I can
see, Isabelle2003 (Isabelle2003/doc/intro.{dvi,ps}). Somehow it seems
to have got lost since then.
Anyhow, let me encourage you to try to understand the system if you're
planning to use it. I've seen people not do so, and eventually give up.
Jeremy
Last updated: May 03 2024 at 01:09 UTC