Re: [isabelle] locales and proofs

Chris, your code (below) runs fine, but I don't understood your
proof.  Please explain so I can understand the Isabelle proofs.

Isn't Pierce's law the rule 
(?P =⇒ ?Q) =⇒ ?P −→ ?Q     (impI)
What do you mean by proof (rule impI)?  

I would have proved Pierce's law like this.  Either P or ~P, as you
say.  Two cases:
if P, we're done, because the result is **** --> T, which is T.
If ~P, the result is 
((F --> Q) --> F) --> F 
= (T --> F) --> F  
= F ---> F = T 
((F --> Q) --> F) --> F 
= (T --> F) --> F  
= F ---> F = T 

I don't really see how to justify it easily using the Isar rules like 
( ¬ ?Q =⇒ ?P) =⇒ ?P ∨ ?Q (disjCI)
which seem primitive.  I'm impressed you wrote such a short proof!

The dox give explain the terms you use, with, show, by etc, but I
couldn't figure out what they meant.  Please explain in your example!


lemma Pierce1: "((P --> Q) --> P) --> P"
proof (rule impI)
   assume 1: "(P --> Q) --> P"
   have "(~ P) | P" by (rule excluded_middle)
   thus P
   proof (rule disjE)
     assume "P" thus "P" by assumption
     assume 2: "~ P"
     have "P --> Q"
     proof (rule impI)
       assume "P"
       with 2 show "Q" by (rule notE)
     with 1 show "P" by (rule mp)

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