*To*: tjm1983 at gmail.com, makarius at sketis.net*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Tue, 1 May 2012 21:07:31 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> (message from Makarius on Mon, 30 Apr 2012 11:30:27 +0200 (CEST))*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de>

Tim and Makarius, I can't follow the Isabelle dox, and I need something like ``Isabelle for Dummies.'' I just want to know how to write my FOL proofs in Isabelle, how to compile them, with examples. Now I feel strongly that Isabelle (like Mizar) ought to be able to check FOL proofs without specifying any proof strategies like Tim's `simp add' or `blast'. Mizar makes lots of proof shortcuts that I wouldn't have expected, and I'd be happier if Isabelle did few proof shortcuts. I want the students to have to write up most of the proof. I think in strict FOL, you have to insert so many needless steps that the proofs become unreadable. I guess we need a good compromise. I untarred Isabelle2011-1_bundle_x86-linux.tar.gz and went to the directory Isabelle2011-1. I ran the executable ./Isabelle and up popped jedit. I pasted in Isabelle code from Tim's master's thesis into Scratch.thy. There's extensive jedit help on the Help menu, but I couldn't figure out how to compile my buffer. So then I tried bin/isabelle emacs po.thy & and up popped a Proof General Emacs frame displaying my short file po.thy based on the first example in the Isabelle2011-1/doc/locales.pdf. ------ po.thy ---- theory PO imports Main begin locale partial_order = fixes le :: " 'a ⇒ 'a ⇒ bool " (infixl "\<sqsubseteq>" 50) assumes refl [intro, simp]: "x \<sqsubseteq> x" and anti_sym [intro]: "[[ x \<sqsubseteq> y; y \<sqsubseteq> x ]] =⇒ x = y" and trans [trans]: "[[ x \<sqsubseteq> y; y \<sqsubseteq> z ]] =⇒ x \<sqsubseteq> z" ------ end po.thy ---- Now I can see how to compile my file! I click on menu item Isabelle -> Start Isabelle I think that's the much the same thing as clicking the down-arrow button which says ``process whole buffer''. I get an error message: * Inner lexical error at: ⇒ 'a ⇒ bool (line 6 of "/home/richter/Isabelle/Isabelle2011-1/po.thy") *** Failed to parse type *** At command "locale" (line 5 of "/home/richter/Isabelle/Isabelle2011-1/po.thy") I have no idea what this means. Posibly I'm using the wrong quote. I'm writing 'a, but locales.pdf actually shows ’a. So I changed to this quote, and I got a new error message: *** Inner lexical error at: ’a ⇒ ’a ⇒ bool (line 6 of "/home/richter/Isabelle/Isabelle2011-1/po.thy") *** Failed to parse type *** At command "locale" (line 5 of "/home/richter/Isabelle/Isabelle2011-1/po.thy") Maybe that's progress, because Proof General is now noticing my first quote a, and not just the second one. I'm actually trying to understand Tim's Tarski geometry axiom code. So I tried compiling a simple version of it below. Proof General gives me an error message similar to the above one: *** Outer syntax error (line 5 of "/home/richter/Isabelle/Isabelle2011-1/Scratch.thy"): command expected, *** but symbolic identifier - (line 5 of "/home/richter/Isabelle/Isabelle2011-1/Scratch.thy") was found But it's the code I'm more interested in now. Tim's axioms make perfect sense, except for the (- - ≡ - - [99,99,99,99] 50) on the line defining C. I'm concerned about lemma A1, which just restates the axiom A1. I do something like that in my Mizar code, and I was really hoping it wouldn't be necessary in Isabelle. Maybe I don't know what lemma A1 is for. But there's plenty of stuff I don't understand in Tim's proof, like by (simp add: A1) with A2 show ?thesis by blast On p 123 of isar-ref.pdf, this is somewhat explained: Typically, the soundness proof is relatively straight-forward, often just by canonical automated tools such as “by simp ” or “by blast ”. I'm guessing that simp and blast are like what HOL Light calls tactics, search strategies for Isabelle to concoct a proof. One of the nice things about Mizar is that you don't ever have to specify any proof strategies, although clearly Mizar is using a strategy. Tim's ?thesis I bet can understand, from p 6: ?thesis — the main conclusion of the innermost pending claim Tim's show ?thesis seems to be explained on p 126: Typical idioms for concluding calculational proofs are “finally show ?thesis .” ---- simple version of Tim's Tarski code ---- theory Tarski imports Main begin locale tarski-first7 = fixes C :: "'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool " (- - ≡ - - [99,99,99,99] 50) fixes B :: 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool assumes A1: \<forall> a b. a b \<equiv> b a and A2: \<forall> a b p q r s. a b \<equiv> p q \<and> a b \<equiv> r s −\<rightarrow> p q \<equiv> r s and A3: \<forall> a b c. a b \<equiv> c c −\<rightarrow> a = b and A4: \<forall> q a b c. \<exists> x. B q a x \<and> a x \<equiv> b c and A5: \<forall> a b c d a b c d . a = b \<and> B a b c \<and> B a b c \<and>ab \<equiv> a b \<and>bc \<equiv> b c \<and>ad \<equiv> a d \<and> bd \<equiv> b d −\<rightarrow> c d \<equiv> c d and A6: \<forall> a b. B a b a −\<rightarrow> a = b and A7: \<forall> a b c p q. B a p c \<and> B b q c −\<rightarrow> (\<exists> x. B p x b \<and> B q x a) context tarski-first7 begin lemma A1 : a b \<equiv> b a by (simp add: A1) lemma A2 : [[a b \<equiv> p q; a b \<equiv> r s]] =\<Rightarrow> p q \<equiv> r s proof − assume a b \<equiv> p q and a b \<equiv> r s with A2 show ?thesis by blast qed lemma A3 : a b \<equiv> c c =\<Rightarrow> a = b by (simp add: A3) theorem th2-1: a b \<equiv> a b proof − from A2 [of b a a b a b] and A1 [of b a] show ?thesis by simp qed theorem th2-2: a b \<equiv> c d =\<Rightarrow> c d \<equiv> a b proof − assume a b \<equiv> c d with A2 [of a b c d a b] and th2-1 [of a b] show ?thesis by simp qed theorem th2-3: [[a b \<equiv> c d; c d \<equiv> e f ]] =\<Rightarrow> a b \<equiv> e f proof − assume a b \<equiv> c d with th2-2 [of a b c d] have c d \<equiv> a b by simp assume c d \<equiv> e f with A2 [of c d a b e f ] and c d \<equiv> a b show ?thesis by simp qed theorem th2-4: a b \<equiv> c d =\<Rightarrow> b a \<equiv> c d proof − assume a b \<equiv> c d with th2-3 [of b a a b c d] and A1 [of b a] show ?thesis by simp qed theorem th2-5: a b \<equiv> c d =\<Rightarrow> a b \<equiv> d c proof − assume a b \<equiv> c d with th2-3 [of a b c d d c] and A1 [of c d] show ?thesis by simp qed -- Best, Bill

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

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