*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] locales, including documentation & possible programming bugs*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Sat, 5 May 2012 18:01:21 -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>

Brian, I read ref.pdf p 30--32 on misfixes, but I could not figure out how to write (in my code below) C a b c d as a b \<equiv> c d. I seem to have a priority problem. I'm using the priority stuff ps = [99,99,99,99] and p = 70, and I've tried lots of others. My "\<forall> a b . a b \<equiv> b a" gets me the error, a do-not-enter on locale, and when I click on locale, I see in the output window Ambiguous input. 2 types are correct: (\<forall> (a b) . (a b \<equiv> b a)) ((\<forall> (a b) . (a b)) \<equiv> (b a)) If I change that to "a b \<equiv> b a", and then I get no error, but the output window reads Ambiguous input produces 2 parse trees: [which seem to be] (C a b b a) (C a b) (C b a) Fortunately, only one is correct, but you may still want to disambiguate your grammar or input. There's more of the same for every \<equiv> expression in my axioms. II tried to write a simple proof following p 40--42 of isar-ref.pdf, but it didn't work. I get do-not-enter signs on every line of the proof. The following commented proof is no better. ----- Tarski2.thy Tarski2 theory Tarski2 imports Complex_Main begin locale tarskifirst7 = fixes C :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("_ _ \<equiv> _ _" [99,99,99,99] 70) fixes B :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (* assumes A1: "\<forall> a b . a b \<equiv> b a" *) assumes A1: "a b \<equiv> b a" and A2: "a b \<equiv> p q \<and> a b \<equiv> r s --> p q \<equiv> r s" and A3: "a b \<equiv> c c ==> a = b" and A4: "\<exists> x. B q a x \<and> a x \<equiv> b c" and A5: "a \<noteq> b \<and> B a b x \<and> B a' b' x' \<and> b x \<equiv> b' x' \<and> a b \<equiv> a' b' \<and> a c \<equiv> a' c' \<and> b c \<equiv> b' c' --> c x \<equiv> c' x'" and A6: "B a b a ==> a = b" and A7: "B a p c \<and> B b q c ==> (\<exists> x. B p x b \<and> B q x a)" context tarskifirst7 begin theorem EquivReflexive: "a b \<equiv> a b" proof - have "b a \<equiv> a b" by (rule A1) have "b a \<equiv> a b" by (rule A1) thus "a b \<equiv> a b" by (rule A2) qed end (* proof - have "b a \<equiv> a b" by (rule A1 [symmetric]) have "b a \<equiv> a b" by (rule A1 [symmetric]) also have "a b \<equiv> a b" by (rule A2 [symmetric]) finally show "a b \<equiv> a b" qed end *) (* end *) (* lemma A1: "C a b b a" by (simp add: A1) lemma A2: "C a b p q \<and> C a b r s ==> C p q r s" by (simp add: A2) 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 definition is-segment :: 'p set \<Rightarrow> bool where is-segment X \<exists> x y. X = {x, y} definition segments :: p set set where segments = {X. is-segment X} definition SC :: p set \<Rightarrow> p set \<Rightarrow> bool where SC X Y \<exists> w x y z. X = {w, x} \<and> Y = {y, z} \<and> w x \<equiv> y z *)

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

**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] Isabelle2012-RC1 available for testing
- Next by Date: Re: [isabelle] locales, including documentation & possible programming bugs
- Previous by Thread: Re: [isabelle] locales and proofs
- 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