# HG changeset patch
# User wenzelm
# Date 928505791 -7200
# Node ID df12aef00932433ee6a6c3bbdd1f6f9ec3b5ea0c
# Parent  a9a515a43ae040a09a904d65053296ab9ddbe45a
Some bits of group theory.  Demonstrate calculational proofs.

diff -r a9a515a43ae0 -r df12aef00932 src/HOL/Isar_examples/Group.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Group.thy	Fri Jun 04 16:16:31 1999 +0200
@@ -0,0 +1,115 @@
+(*  Title:      HOL/Isar_examples/Group.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Some bits of group theory.  Demonstrate calculational proofs.
+*)
+
+theory Group = Main:;
+
+
+subsection {* axiomatic type class of groups over signature (*, inv, one) *};
+
+consts
+  inv :: "'a => 'a"
+  one :: "'a";
+
+axclass
+  group < times
+  assoc:         "(x * y) * z = x * (y * z)"
+  left_unit:     "one * x = x"
+  left_inverse:  "inverse x * x = one";
+
+
+subsection {* some basic theorems of group theory *};
+
+text {* We simulate *};
+
+theorem right_inverse: "x * inverse x = (one::'a::group)";
+proof same;
+  have "x * inverse x = one * (x * inverse x)";
+    by (simp add: left_unit);
+
+  note calculation = facts;
+  let "_ = ..." = ??facts;
+
+  have "... = (one * x) * inverse x";
+    by (simp add: assoc);
+
+  note calculation = trans[APP calculation facts];
+  let "_ = ..." = ??facts;
+
+  have "... = inverse (inverse x) * inverse x * x * inverse x";
+    by (simp add: left_inverse);
+
+  note calculation = trans[APP calculation facts];
+  let "_ = ..." = ??facts;
+
+  have "... = inverse (inverse x) * (inverse x * x) * inverse x";
+    by (simp add: assoc);
+
+  note calculation = trans[APP calculation facts];
+  let "_ = ..." = ??facts;
+
+  have "... = inverse (inverse x) * one * inverse x";
+    by (simp add: left_inverse);
+
+  note calculation = trans[APP calculation facts];
+  let "_ = ..." = ??facts;
+
+  have "... = inverse (inverse x) * (one * inverse x)";
+    by (simp add: assoc);
+
+  note calculation = trans[APP calculation facts];
+  let "_ = ..." = ??facts;
+
+  have "... = inverse (inverse x) * inverse x";
+    by (simp add: left_unit);
+
+  note calculation = trans[APP calculation facts];
+  let "_ = ..." = ??facts;
+
+  have "... = one";
+    by (simp add: left_inverse);
+
+  note calculation = trans[APP calculation facts];
+  let "_ = ..." = ??facts;
+  from calculation;
+
+  show ??thesis; .;
+qed;
+
+
+theorem right_inverse: "x * one = (x::'a::group)";
+proof same;
+
+  have "x * one = x * (inverse x * x)";
+    by (simp add: left_inverse);
+
+  note calculation = facts;
+  let "_ = ..." = ??facts;
+
+  have "... = x * inverse x * x";
+    by (simp add: assoc);
+
+  note calculation = trans[APP calculation facts];
+  let "_ = ..." = ??facts;
+
+  have "... = one * x";
+    by (simp add: right_inverse);
+
+  note calculation = trans[APP calculation facts];
+  let "_ = ..." = ??facts;
+
+  have "... = x";
+    by (simp add: left_unit);
+
+  note calculation = trans[APP calculation facts];
+  let "_ = ..." = ??facts;
+  from calculation;
+
+  show ??thesis; .;
+qed;
+
+
+end;