[isabelle] locales, including documentation & possible programming bugs



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.