# [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
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.