# HG changeset patch # User wenzelm # Date 928611782 -7200 # Node ID 88aba7f486cb67a57f65d2c308935d65d85135dd # Parent c68035d06cce6d03133aa56fbe0b15bc1935cf92 groups as monoids; tuned; diff -r c68035d06cce -r 88aba7f486cb src/HOL/Isar_examples/Group.thy --- a/src/HOL/Isar_examples/Group.thy Sat Jun 05 21:38:30 1999 +0200 +++ b/src/HOL/Isar_examples/Group.thy Sat Jun 05 21:43:02 1999 +0200 @@ -5,12 +5,12 @@ theory Group = Main:; -title {* Basic group theory -- demonstrating calculational proofs *}; +title {* Basic group theory *}; section {* Groups *}; text {* - We define an axiomatic type class of general groupes over signature + We define an axiomatic type class of general groups over signature (op *, one, inv). *}; @@ -20,95 +20,92 @@ axclass group < times - assoc: "(x * y) * z = x * (y * z)" - left_unit: "one * x = x" - left_inverse: "inv x * x = one"; + group_assoc: "(x * y) * z = x * (y * z)" + group_left_unit: "one * x = x" + group_left_inverse: "inv x * x = one"; text {* - The group axioms only state the properties of left unit and inverse, the - right versions are derivable as follows. The calculational proof style below - closely follows a typical presentation given in any basic course on - algebra. + The group axioms only state the properties of left unit and inverse, + the right versions are derivable as follows. The calculational proof + style below closely follows typical presentations given in any basic + course on algebra. *}; -theorem right_inverse: "x * inv x = (one::'a::group)"; +theorem group_right_inverse: "x * inv x = (one::'a::group)"; proof same; have "x * inv x = one * (x * inv x)"; - by (simp add: left_unit); + by (simp add: group_left_unit); also; have "... = (one * x) * inv x"; - by (simp add: assoc); + by (simp add: group_assoc); also; have "... = inv (inv x) * inv x * x * inv x"; - by (simp add: left_inverse); + by (simp add: group_left_inverse); also; have "... = inv (inv x) * (inv x * x) * inv x"; - by (simp add: assoc); + by (simp add: group_assoc); also; have "... = inv (inv x) * one * inv x"; - by (simp add: left_inverse); + by (simp add: group_left_inverse); also; have "... = inv (inv x) * (one * inv x)"; - by (simp add: assoc); + by (simp add: group_assoc); also; have "... = inv (inv x) * inv x"; - by (simp add: left_unit); + by (simp add: group_left_unit); also; have "... = one"; - by (simp add: left_inverse); + by (simp add: group_left_inverse); finally; show ??thesis; .; qed; text {* - With right_inverse already at our disposel, right_unit is now - obtained much simpler. + With group_right_inverse already at our disposal, group_right_unit is + now obtained much easier as follows. *}; -theorem right_unit: "x * one = (x::'a::group)"; +theorem group_right_unit: "x * one = (x::'a::group)"; proof same; have "x * one = x * (inv x * x)"; - by (simp add: left_inverse); + by (simp add: group_left_inverse); also; have "... = x * inv x * x"; - by (simp add: assoc); + by (simp add: group_assoc); also; have "... = one * x"; - by (simp add: right_inverse); + by (simp add: group_right_inverse); also; have "... = x"; - by (simp add: left_unit); + by (simp add: group_left_unit); finally; show ??thesis; .; qed; text {* - There are only two language elements 'also' (for initial or - intermediate calculational steps), and 'finally' (for picking up the - result of a calculation). These constructs are not hardwired into - Isabelle/Isar, but defined on top of the basic Isar/VM interpreter. + There are only two Isar language elements for calculational proofs: + 'also' for initial or intermediate calculational steps, and 'finally' + for building the result of a calculation. These constructs are not + hardwired into Isabelle/Isar, but defined on top of the basic Isar/VM + interpreter. Expanding the 'also' or 'finally' derived language + elements, calculations may be simulated as demonstrated below. - Without referring to 'also' or 'finally', calculations may be - simulated as follows. This can be also understood as an expansion of these - two derived language elements. - - Also note that "..." is just a special term binding that happens to - be bound automatically to the argument of the last fact established by - assume or any local goal. Unlike ??thesis, "..." is bound after the - proof is finished. + Note that "..." is just a special term binding that happens to be + bound automatically to the argument of the last fact established by + assume or any local goal. In contrast to ??thesis, "..." is bound + after the proof is finished. *}; -theorem right_unit': "x * one = (x::'a::group)"; +theorem "x * one = (x::'a::group)"; proof same; - have "x * one = x * (inv x * x)"; - by (simp add: left_inverse); + by (simp add: group_left_inverse); note calculation = facts - -- {* first calculational step: init register *}; + -- {* first calculational step: init calculation register *}; have "... = x * inv x * x"; - by (simp add: assoc); + by (simp add: group_assoc); note calculation = trans[APP calculation facts] -- {* general calculational step: compose with transitivity rule *}; have "... = one * x"; - by (simp add: right_inverse); + by (simp add: group_right_inverse); note calculation = trans[APP calculation facts] -- {* general calculational step: compose with transitivity rule *}; have "... = x"; - by (simp add: left_unit); + by (simp add: group_left_unit); note calculation = trans[APP calculation facts] -- {* final calculational step: compose with transitivity rule ... *}; @@ -116,8 +113,34 @@ -- {* ... and pick up final result *}; show ??thesis; .; - qed; +section {* Groups and monoids *}; + +text {* + Monoids are usually defined like this. +*}; + +axclass monoid < times + monoid_assoc: "(x * y) * z = x * (y * z)" + monoid_left_unit: "one * x = x" + monoid_right_unit: "x * one = x"; + +text {* + Groups are *not* yet monoids directly from the definition . For + monoids, right_unit had to be included as an axiom, but for groups + both right_unit and right_inverse are derivable from the other + axioms. With group_right_unit derived as a theorem of group theory + (see above), we may still instantiate group < monoid properly as + follows. +*}; + +instance group < monoid; + by (expand_classes, + rule group_assoc, + rule group_left_unit, + rule group_right_unit); + + end;