src/HOL/Isar_examples/Group.thy
 author wenzelm Fri Jun 04 16:16:31 1999 +0200 (1999-06-04) changeset 6763 df12aef00932 child 6784 687ddcad8581 permissions -rw-r--r--
Some bits of group theory. Demonstrate calculational proofs.
 wenzelm@6763 ` 1` ```(* Title: HOL/Isar_examples/Group.thy ``` wenzelm@6763 ` 2` ``` ID: \$Id\$ ``` wenzelm@6763 ` 3` ``` Author: Markus Wenzel, TU Muenchen ``` wenzelm@6763 ` 4` wenzelm@6763 ` 5` ```Some bits of group theory. Demonstrate calculational proofs. ``` wenzelm@6763 ` 6` ```*) ``` wenzelm@6763 ` 7` wenzelm@6763 ` 8` ```theory Group = Main:; ``` wenzelm@6763 ` 9` wenzelm@6763 ` 10` wenzelm@6763 ` 11` ```subsection {* axiomatic type class of groups over signature (*, inv, one) *}; ``` wenzelm@6763 ` 12` wenzelm@6763 ` 13` ```consts ``` wenzelm@6763 ` 14` ``` inv :: "'a => 'a" ``` wenzelm@6763 ` 15` ``` one :: "'a"; ``` wenzelm@6763 ` 16` wenzelm@6763 ` 17` ```axclass ``` wenzelm@6763 ` 18` ``` group < times ``` wenzelm@6763 ` 19` ``` assoc: "(x * y) * z = x * (y * z)" ``` wenzelm@6763 ` 20` ``` left_unit: "one * x = x" ``` wenzelm@6763 ` 21` ``` left_inverse: "inverse x * x = one"; ``` wenzelm@6763 ` 22` wenzelm@6763 ` 23` wenzelm@6763 ` 24` ```subsection {* some basic theorems of group theory *}; ``` wenzelm@6763 ` 25` wenzelm@6763 ` 26` ```text {* We simulate *}; ``` wenzelm@6763 ` 27` wenzelm@6763 ` 28` ```theorem right_inverse: "x * inverse x = (one::'a::group)"; ``` wenzelm@6763 ` 29` ```proof same; ``` wenzelm@6763 ` 30` ``` have "x * inverse x = one * (x * inverse x)"; ``` wenzelm@6763 ` 31` ``` by (simp add: left_unit); ``` wenzelm@6763 ` 32` wenzelm@6763 ` 33` ``` note calculation = facts; ``` wenzelm@6763 ` 34` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 35` wenzelm@6763 ` 36` ``` have "... = (one * x) * inverse x"; ``` wenzelm@6763 ` 37` ``` by (simp add: assoc); ``` wenzelm@6763 ` 38` wenzelm@6763 ` 39` ``` note calculation = trans[APP calculation facts]; ``` wenzelm@6763 ` 40` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 41` wenzelm@6763 ` 42` ``` have "... = inverse (inverse x) * inverse x * x * inverse x"; ``` wenzelm@6763 ` 43` ``` by (simp add: left_inverse); ``` wenzelm@6763 ` 44` wenzelm@6763 ` 45` ``` note calculation = trans[APP calculation facts]; ``` wenzelm@6763 ` 46` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 47` wenzelm@6763 ` 48` ``` have "... = inverse (inverse x) * (inverse x * x) * inverse x"; ``` wenzelm@6763 ` 49` ``` by (simp add: assoc); ``` wenzelm@6763 ` 50` wenzelm@6763 ` 51` ``` note calculation = trans[APP calculation facts]; ``` wenzelm@6763 ` 52` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 53` wenzelm@6763 ` 54` ``` have "... = inverse (inverse x) * one * inverse x"; ``` wenzelm@6763 ` 55` ``` by (simp add: left_inverse); ``` wenzelm@6763 ` 56` wenzelm@6763 ` 57` ``` note calculation = trans[APP calculation facts]; ``` wenzelm@6763 ` 58` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 59` wenzelm@6763 ` 60` ``` have "... = inverse (inverse x) * (one * inverse x)"; ``` wenzelm@6763 ` 61` ``` by (simp add: assoc); ``` wenzelm@6763 ` 62` wenzelm@6763 ` 63` ``` note calculation = trans[APP calculation facts]; ``` wenzelm@6763 ` 64` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 65` wenzelm@6763 ` 66` ``` have "... = inverse (inverse x) * inverse x"; ``` wenzelm@6763 ` 67` ``` by (simp add: left_unit); ``` wenzelm@6763 ` 68` wenzelm@6763 ` 69` ``` note calculation = trans[APP calculation facts]; ``` wenzelm@6763 ` 70` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 71` wenzelm@6763 ` 72` ``` have "... = one"; ``` wenzelm@6763 ` 73` ``` by (simp add: left_inverse); ``` wenzelm@6763 ` 74` wenzelm@6763 ` 75` ``` note calculation = trans[APP calculation facts]; ``` wenzelm@6763 ` 76` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 77` ``` from calculation; ``` wenzelm@6763 ` 78` wenzelm@6763 ` 79` ``` show ??thesis; .; ``` wenzelm@6763 ` 80` ```qed; ``` wenzelm@6763 ` 81` wenzelm@6763 ` 82` wenzelm@6763 ` 83` ```theorem right_inverse: "x * one = (x::'a::group)"; ``` wenzelm@6763 ` 84` ```proof same; ``` wenzelm@6763 ` 85` wenzelm@6763 ` 86` ``` have "x * one = x * (inverse x * x)"; ``` wenzelm@6763 ` 87` ``` by (simp add: left_inverse); ``` wenzelm@6763 ` 88` wenzelm@6763 ` 89` ``` note calculation = facts; ``` wenzelm@6763 ` 90` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 91` wenzelm@6763 ` 92` ``` have "... = x * inverse x * x"; ``` wenzelm@6763 ` 93` ``` by (simp add: assoc); ``` wenzelm@6763 ` 94` wenzelm@6763 ` 95` ``` note calculation = trans[APP calculation facts]; ``` wenzelm@6763 ` 96` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 97` wenzelm@6763 ` 98` ``` have "... = one * x"; ``` wenzelm@6763 ` 99` ``` by (simp add: right_inverse); ``` wenzelm@6763 ` 100` wenzelm@6763 ` 101` ``` note calculation = trans[APP calculation facts]; ``` wenzelm@6763 ` 102` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 103` wenzelm@6763 ` 104` ``` have "... = x"; ``` wenzelm@6763 ` 105` ``` by (simp add: left_unit); ``` wenzelm@6763 ` 106` wenzelm@6763 ` 107` ``` note calculation = trans[APP calculation facts]; ``` wenzelm@6763 ` 108` ``` let "_ = ..." = ??facts; ``` wenzelm@6763 ` 109` ``` from calculation; ``` wenzelm@6763 ` 110` wenzelm@6763 ` 111` ``` show ??thesis; .; ``` wenzelm@6763 ` 112` ```qed; ``` wenzelm@6763 ` 113` wenzelm@6763 ` 114` wenzelm@6763 ` 115` ```end; ```