*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Wed, 02 May 2012 14:00:27 +0900*In-reply-to*: <4FA0BBE7.4060302@jaist.ac.jp>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:12.0) Gecko/20120424 Thunderbird/12.0

On 05/02/2012 01:45 PM, Christian Sternagel wrote:

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?Well, not really indigestible, but consider the following Isabelle/HOL proof of Pierce's Law: 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 where the question marks indicate that variables can be instantiated arbitrarily (i.e., they are so called "schematic variables"). In this proof every step (w.r.t. some given set of rules) is done explicitly. If we use "blast" (or "auto" for that matter) it reduces to. lemma Pierce2: "((P --> Q) --> P) --> P" by blast But note that both proofs are equally rigorous, since blast just applies existing lemmas that are setup as introduction and elimination rules for logical symbols (besides others). (The whole idea of proof assistants like Isabelle, is that internally everything is reducible to the initial axioms, whether this is done by hand or left to the system is to some extend the users choice [sometimes the automatic methods are just not powerful enough to solve a goal and the user has to divide it in smaller pieces manually].)(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 (which has not yet really come to life). It contains pointers to some courses that use or are about Isabelle https://isabelle.in.tum.de/community/Course_Material This could be interesting for you. hope this helps chris

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

- Previous by Date: Re: [isabelle] Linear Ordering for nat list
- Next by Date: Re: [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