[isabelle] Elim resolution



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
--
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.