*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] locales and proofs*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Fri, 4 May 2012 22:48:11 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAMXsiaNt7gi9NPRAEAVvO4r8Mmor28YJprMrpkBBzUt9TUL=w@mail.gmail.com> (message from Brian Huffman on Fri, 4 May 2012 08:06:48 +0200)*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.7030904@jaist.ac.jp> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.4060302@jaist.ac.jp> <201205040401.q4441PxX003215@poisson.math.northwestern.edu> <CAAMXsiaNt7gi9NPRAEAVvO4r8Mmor28YJprMrpkBBzUt9TUL=w@mail.gmail.com>

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! -- Best, Bill 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 next assume 2: "~ P" have "P --> Q" proof (rule impI) assume "P" with 2 show "Q" by (rule notE) qed with 1 show "P" by (rule mp) qed qed

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**[isabelle] locales, including documentation & possible programming bugs***From:*Bill Richter

**Re: [isabelle] locales, including documentation & possible programming bugs***From:*Brian Huffman

- Previous by Date: Re: [isabelle] locales and proofs programming bugs
- Next by Date: Re: [isabelle] Isabelle2012-RC1 available for testing
- Previous by Thread: Re: [isabelle] locales and proofs programming bugs
- Next by Thread: Re: [isabelle] locales, including documentation & possible programming bugs
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list