author wenzelm Tue, 03 Oct 2000 18:56:44 +0200 changeset 10141 964d9dc47041 parent 10140 ba9297b71897 child 10142 d1d61d13e461
tuned names; added more theorems of group theory (from old AxClasses/Group/Group.ML);
--- a/src/HOL/Isar_examples/Group.thy	Tue Oct 03 18:55:23 2000 +0200
+++ b/src/HOL/Isar_examples/Group.thy	Tue Oct 03 18:56:44 2000 +0200
@@ -11,42 +11,42 @@

text {*
Groups over signature $({\times} :: \alpha \To \alpha \To \alpha, - \idt{one} :: \alpha, \idt{inv} :: \alpha \To \alpha)$ are defined as
- an axiomatic type class as follows.  Note that the parent class
+ \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$are defined + as an axiomatic type class as follows. Note that the parent class$\idt{times}$is provided by the basic HOL theory. *} consts one :: "'a" - inv :: "'a => 'a" + inverse :: "'a => 'a" axclass group < times group_assoc: "(x * y) * z = x * (y * z)" - group_left_unit: "one * x = x" - group_left_inverse: "inv x * x = one" + group_left_one: "one * x = x" + group_left_inverse: "inverse x * x = one" text {* - The group axioms only state the properties of left unit and inverse, + The group axioms only state the properties of left one and inverse, the right versions may be derived as follows. *} -theorem group_right_inverse: "x * inv x = (one::'a::group)" +theorem group_right_inverse: "x * inverse x = (one::'a::group)" proof - - have "x * inv x = one * (x * inv x)" - by (simp only: group_left_unit) - also have "... = one * x * inv x" + have "x * inverse x = one * (x * inverse x)" + by (simp only: group_left_one) + also have "... = one * x * inverse x" by (simp only: group_assoc) - also have "... = inv (inv x) * inv x * x * inv x" + also have "... = inverse (inverse x) * inverse x * x * inverse x" by (simp only: group_left_inverse) - also have "... = inv (inv x) * (inv x * x) * inv x" + also have "... = inverse (inverse x) * (inverse x * x) * inverse x" by (simp only: group_assoc) - also have "... = inv (inv x) * one * inv x" + also have "... = inverse (inverse x) * one * inverse x" by (simp only: group_left_inverse) - also have "... = inv (inv x) * (one * inv x)" + also have "... = inverse (inverse x) * (one * inverse x)" by (simp only: group_assoc) - also have "... = inv (inv x) * inv x" - by (simp only: group_left_unit) + also have "... = inverse (inverse x) * inverse x" + by (simp only: group_left_one) also have "... = one" by (simp only: group_left_inverse) finally show ?thesis . @@ -54,20 +54,20 @@ text {* With \name{group-right-inverse} already available, - \name{group-right-unit}\label{thm:group-right-unit} is now - established much easier. + \name{group-right-one}\label{thm:group-right-one} is now established + much easier. *} -theorem group_right_unit: "x * one = (x::'a::group)" +theorem group_right_one: "x * one = (x::'a::group)" proof - - have "x * one = x * (inv x * x)" + have "x * one = x * (inverse x * x)" by (simp only: group_left_inverse) - also have "... = x * inv x * x" + also have "... = x * inverse x * x" by (simp only: group_assoc) also have "... = one * x" by (simp only: group_right_inverse) also have "... = x" - by (simp only: group_left_unit) + by (simp only: group_left_one) finally show ?thesis . qed @@ -97,13 +97,13 @@ theorem "x * one = (x::'a::group)" proof - - have "x * one = x * (inv x * x)" + have "x * one = x * (inverse x * x)" by (simp only: group_left_inverse) note calculation = this -- {* first calculational step: init calculation register *} - have "... = x * inv x * x" + have "... = x * inverse x * x" by (simp only: group_assoc) note calculation = trans [OF calculation this] @@ -116,7 +116,7 @@ -- {* general calculational step: compose with transitivity rule *} have "... = x" - by (simp only: group_left_unit) + by (simp only: group_left_one) note calculation = trans [OF calculation this] -- {* final calculational step: compose with transitivity rule ... *} @@ -145,24 +145,24 @@ axclass monoid < times monoid_assoc: "(x * y) * z = x * (y * z)" - monoid_left_unit: "one * x = x" - monoid_right_unit: "x * one = x" + monoid_left_one: "one * x = x" + monoid_right_one: "x * one = x" text {* Groups are \emph{not} yet monoids directly from the definition. For - monoids, \name{right-unit} had to be included as an axiom, but for - groups both \name{right-unit} and \name{right-inverse} are derivable - from the other axioms. With \name{group-right-unit} derived as a - theorem of group theory (see page~\pageref{thm:group-right-unit}), we - may still instantiate$\idt{group} \subset \idt{monoid}$properly as - follows. + monoids, \name{right-one} had to be included as an axiom, but for + groups both \name{right-one} and \name{right-inverse} are derivable + from the other axioms. With \name{group-right-one} derived as a + theorem of group theory (see page~\pageref{thm:group-right-one}), we + may still instantiate$\idt{group} \subseteq \idt{monoid}\$ properly
+ as follows.
*}

instance group < monoid
by (intro_classes,
rule group_assoc,
-       rule group_left_unit,
-       rule group_right_unit)
+       rule group_left_one,
+       rule group_right_one)

text {*
The \isacommand{instance} command actually is a version of
@@ -173,4 +173,94 @@
type signature extension behind the scenes.
*}

-end
+subsection {* More theorems of group theory *}
+
+text {*
+ The one element is already uniquely determined by preserving an
+ \emph{arbitrary} group element.
+*}
+
+theorem group_one_equality: "e * x = x ==> one = (e::'a::group)"
+proof -
+  assume eq: "e * x = x"
+  have "one = x * inverse x"
+    by (simp only: group_right_inverse)
+  also have "... = (e * x) * inverse x"
+    by (simp only: eq)
+  also have "... = e * (x * inverse x)"
+    by (simp only: group_assoc)
+  also have "... = e * one"
+    by (simp only: group_right_inverse)
+  also have "... = e"
+    by (simp only: group_right_one)
+  finally show ?thesis .
+qed
+
+text {*
+ Likewise, the inverse is already determined by the cancel property.
+*}
+
+theorem group_inverse_equality:
+  "x' * x = one ==> inverse x = (x'::'a::group)"
+proof -
+  assume eq: "x' * x = one"
+  have "inverse x = one * inverse x"
+    by (simp only: group_left_one)
+  also have "... = (x' * x) * inverse x"
+    by (simp only: eq)
+  also have "... = x' * (x * inverse x)"
+    by (simp only: group_assoc)
+  also have "... = x' * one"
+    by (simp only: group_right_inverse)
+  also have "... = x'"
+    by (simp only: group_right_one)
+  finally show ?thesis .
+qed
+
+text {*
+ The inverse operation has some further characteristic properties.
+*}
+
+theorem group_inverse_times:
+  "inverse (x * y) = inverse y * inverse (x::'a::group)"
+proof (rule group_inverse_equality)
+  show "(inverse y * inverse x) * (x * y) = one"
+  proof -
+    have "(inverse y * inverse x) * (x * y) =
+        (inverse y * (inverse x * x)) * y"
+      by (simp only: group_assoc)
+    also have "... = (inverse y * one) * y"
+      by (simp only: group_left_inverse)
+    also have "... = inverse y * y"
+      by (simp only: group_right_one)
+    also have "... = one"
+      by (simp only: group_left_inverse)
+    finally show ?thesis .
+  qed
+qed
+
+theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)"
+proof (rule group_inverse_equality)
+  show "x * inverse x = one"
+    by (simp only: group_right_inverse)
+qed
+
+theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)"
+proof -
+  assume eq: "inverse x = inverse y"
+  have "x = x * one"
+    by (simp only: group_right_one)
+  also have "... = x * (inverse y * y)"
+    by (simp only: group_left_inverse)
+  also have "... = x * (inverse x * y)"
+    by (simp only: eq)
+  also have "... = (x * inverse x) * y"
+    by (simp only: group_assoc)
+  also have "... = one * y"
+    by (simp only: group_right_inverse)
+  also have "... = y"
+    by (simp only: group_left_one)
+  finally show ?thesis .
+qed
+
+end
\ No newline at end of file