Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Bill R. <ri...@ma...>]

Makarius, here's a miz3 version of an Isabelle proof you asked me to
look at, from the Group theory examples in the Isabelle/Isar Reference
Manual, p 18--19 isabelle.in.tum.de/doc/isar-ref.pdf which gives a
nice proof that left units/identity implies right units.  I find the
Isabelle proof very hard to read, and I prefer the miz3 proof below.
Can you tell me what I'm missing?  Can you write this Mizar-style
proof in Isabelle?  Maybe it would be nice to be able to mix Isabelle
locales and fancy symbols with the miz3 style proofs.

(* Paste in these 2 commands:
   hol_light> ocaml
   #use "hol.ml";;  
   then paste in the following file*)


parse_as_infix("***",(20,"right"));;

#load "unix.cma";;
loadt "miz3/miz3.ml";;

horizon := 0;; 

let right_inv = thm `;
  let g be A->bool;
  let (**) be A->A->A;
  let i be A->A;
  let e be A;
  assume (e IN g) /\ (!x. x IN g ==> i(x) IN g) /\
    (!x y. x IN g /\ y IN g ==> x ** y IN g) [1];
  assume !x y z. x IN g /\ y IN g /\ z IN g
                 ==> x ** (y ** z) = (x ** y) ** z [Assoc];
  assume !x. x IN g ==> e ** x = x [Left_Unit];
  assume !x. x IN g ==> i(x) ** x = e [Left_Inv];
  thus ! x. x IN g ==> x ** i(x) = e

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

  proof
  let x be A;
  assume x IN g [xing];
  x ** i(x) = e ** (x ** i(x)) by 1, xing, Left_Unit;
  x ** i(x) = (e ** x) ** i(x) by 1, xing, -, Assoc;
  x ** i(x) = ((i(i(x)) ** i(x)) ** x) ** i(x) by 1, xing, -, Left_Inv;
  x ** i(x) = (i(i(x)) ** (i(x) ** x)) ** i(x) by 1, xing, -, Assoc;
  x ** i(x) = (i(i(x)) ** e) ** i(x) by 1, xing, -, Left_Inv;
  x ** i(x) = i(i(x)) ** (e ** i(x)) by 1, xing, -, Assoc;
  x ** i(x) = i(i(x)) ** i(x) by 1, xing, -, Left_Unit;
  qed by 1, xing, -, Left_Inv`;;


(*
It works!  The output is 

  |- !g (**) i e.
         e IN g /\
         (!x. x IN g ==> i x IN g) /\
         (!x y. x IN g /\ y IN g ==> x ** y IN g)
         ==> (!x y z.
                  x IN g /\ y IN g /\ z IN g ==> x ** y ** z = (x ** y) ** z)
         ==> (!x. x IN g ==> e ** x = x)
         ==> (!x. x IN g ==> i x ** x = e)
         ==> (!x. x IN g ==> x ** i x = e)


Some discussion: 

There's no question that the Isabelle proof is easier on the eyes.  I
checked that I can replace `**' by `*', but you \circ is nicer, and
your x^{-1} exponent is a lot more readable than i(x).  More
substantively, it hurts readability to state all the left group theory
axioms in the statement of the theorem.  But most substantively, the
miz3 proof is easier for me to read. 

 A modification of Freek's lagrange1.ml is

let group = new_definition
  `group(g,(**),i,(e:A)) <=>
    (e IN g) /\ (!x. x IN g ==> i(x) IN g) /\
    (!x y. x IN g /\ y IN g ==> x**y IN g) /\
    (!x y z. x IN g /\ y IN g /\ z IN g ==> x**(y**z) = (x**y)**z) /\
    (!x. x IN g ==> e**x = x) /\
    (!x. x IN g ==> x**i(x) = e )`;;

That's something like an Isabelle locale, but I don't know how to put
labels on the axioms, and Freek did not do so.  

The clever Isabelle proof uses the facts x'' x' = 1 and x' x = 1 at
some points, and uses 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

I can't see how Isabelle justified this proof. I know `...' means the
previous right hand side.  But Isabelle is doing other things too. 
Isabelle 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 combined S3 & S4 to get 
 (x'' (x' x)) x' = 1
and then multiplied S2 on the right by x' to get 
(1 x) x' = ((x'' x') x) x' 
combined the last two statements to 
(1 x) x' = 1
and combined this with S1 to get 
x x' = 1.  
I don't see the Isabelle mechanism yet, and I think my proof above is
a more readable.
*)