*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Wed, 02 May 2012 13:45:27 +0900*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201205020409.q42497Ou014411@poisson.math.northwestern.edu>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:12.0) Gecko/20120424 Thunderbird/12.0

Dear Bill, On 05/02/2012 01:09 PM, Bill Richter wrote:

Thanks, Chris, that's very helpful. I'll look for the red wavy error lines in jedit. I'll look at /src/HOL/ex/. I've looked at tutorial.pdf, but I'll look again, and isar-overview.pdf sounds good. Thanks for explaining simp, blast etc, although I don't really know what you mean. Is there somewhere an FOL example, with a long (perhaps indigestible) single step "rule" method proof, which is shortened with simp, and then shortened even more with blast& auto?

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 Which just uses the existing lemmas impI: (?P ==> ?Q) ==> ?P --> ?Q excluded_middle: ~ ?P | ?P disjE: ?P | ?Q ==> (?P ==> ?R) ==> (?Q ==> ?R) ==> ?R notE: ~ ?P ==> ?P ==> ?R mp: ?P --> ?Q ==> ?P ==> ?Q

lemma Pierce2: "((P --> Q) --> P) --> P" by blast

(In courses it is often done that students are only allowed to use certain rules in order to proof a statement, since the automatic tools would outright solve many typical examples.) Wow! Can you point me to any of these courses? That sounds like what I need to know. As I posted earlier, I'm mostly trying to cite some good code for my geometry paper above (which I'll then submit). I don't have to write the code myself, although I did http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar Examples of real classroom situations where students hand in Isabelle proofs would be fantastic! Dunno about Europe, but US public schools are really gungho about computer applications.

There is the Isabelle Community Wiki https://isabelle.in.tum.de/community

https://isabelle.in.tum.de/community/Course_Material This could be interesting for you. hope this helps chris

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

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

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

**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

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Date: [isabelle] Browsing Main?
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- 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