*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] locales, including documentation & possible programming bugs*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Thu, 3 May 2012 23:01:25 -0500*In-reply-to*: <4FA0BBE7.4060302@jaist.ac.jp> (message from Christian Sternagel on Wed, 02 May 2012 13:45:27 +0900)*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>

My axiomatic geometry quest is now entirely about locales, and I have a documentation bug. The syntax looks incorrect in both locales.pdf and p 40 of the Isabelle/Isar Reference Manual, which has a nice group theory example, from which I learned something about proofs. So I created the file Group1.thy below and had a lot of fun playing with it in jedit. First notice all the "s and 's I inserted. There are none of p 40, or in locales.pdf, and wouldn't that be great if we didn't need them. I figured that out the `"'s & `''s easily by trial and error, but It took me a long time to realize I had to put the final period after the `"'. I didn't know how to make the -1 exponent in jedit, so I changed x^{-1} to sqrt x. Can someone tell me how? And here's another newbie question: If you have a 4-ary relation C, how do you tell Isabelle you want to write it as a b <\equiv> c d? That's what Tim does, but where is that explained? I partly understand the clever group theory proof. Call x' = x^{-1}. We'll substitute in the equations x'' x' = 1 and x' x = 1 at some points, and use assoc, left ident & left inverses: x x' = 1(x x') = (1 x) x' = ((x'' x') x) x' = ((x'' (x' x)) x' = ((x'' 1) x' = x'' (1 x') = x'' x' = 1 Using `...' for the previous right hand side, Isabelle more or less proved four separate statements S1: x x' = 1(x x') = (1 x) x' S2: (1 x) = (x'' x') x S3: (x'' (x' x)) x' = x'' (1 x') S4: x'' (1 x') = 1 and said finally we're done! Well, why are we done? Isabelle must have used the transitive property of = on S3 & S4 to get S5: (x'' (x' x)) x' = 1. Some such transitivity was used to produce S1--4, but at least there we had ... to lead the way. Isabelle then multiplied S2 on the right by x' to get (1 x) x' = ((x'' x') x) x' used transitivity with S5 to get (1 x) x' = 1 Transitivity with S1 gives x x' = 1. Am I getting this right? I don't how readable I think proof is. *) -------- Group1.thy ---- theory Group1 imports Main begin locale group = fixes prod :: "'i \<Rightarrow> 'i \<Rightarrow> 'i" (infix "◦" 70) fixes inv :: "'i \<Rightarrow> 'i" ( "\<surd>") fixes unit :: "'i" ("1") assumes assoc: "(x ◦ y ) ◦ z = x ◦ (y ◦ z )" and left_inv: "\<surd>x ◦ x = 1" and left_unit : "1 ◦ x = x" begin theorem right_inv: "x ◦ \<surd>x = 1" proof - have "x ◦ \<surd>x = 1 ◦ (x ◦ \<surd>x )" by (rule left_unit [symmetric]) also have "... = (1 ◦ x ) ◦ \<surd>x" by (rule assoc [symmetric]) also have "1 = \<surd>(\<surd>x) ◦ \<surd>x" by (rule left_inv [symmetric]) also have "... ◦ x = \<surd> (\<surd> x ) ◦ (\<surd> x ◦ x )" by (rule assoc) also have "\<surd>x ◦ x = 1" by (rule left_inv ) also have "(\<surd>(\<surd>x ) ◦ ...) ◦ \<surd>x = \<surd> (\<surd>x) ◦ (1 ◦ \<surd>x )" by (rule assoc) also have "1 ◦ \<surd> x = \<surd> x" by (rule left_unit ) also have "\<surd>(\<surd>x ) ◦ ... = 1" by (rule left_inv ) finally show "x ◦ \<surd>x = 1". qed end

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

- Previous by Date: Re: [isabelle] Using system jEdit with bundle
- Next by Date: Re: [isabelle] locales, including documentation & possible programming bugs
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- 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