wenzelm@47295 ` 1` ```(* Title: HOL/Isar_Examples/Group_Notepad.thy ``` wenzelm@47295 ` 2` ``` Author: Makarius ``` wenzelm@47295 ` 3` ```*) ``` wenzelm@47295 ` 4` wenzelm@47295 ` 5` ```header {* Some algebraic identities derived from group axioms -- proof notepad version *} ``` wenzelm@47295 ` 6` wenzelm@47295 ` 7` ```theory Group_Notepad ``` wenzelm@47295 ` 8` ```imports Main ``` wenzelm@47295 ` 9` ```begin ``` wenzelm@47295 ` 10` wenzelm@47295 ` 11` ```notepad ``` wenzelm@47295 ` 12` ```begin ``` wenzelm@47295 ` 13` ``` txt {* hypothetical group axiomatization *} ``` wenzelm@47295 ` 14` wenzelm@47295 ` 15` ``` fix prod :: "'a \ 'a \ 'a" (infixl "**" 70) ``` wenzelm@47295 ` 16` ``` and one :: "'a" ``` wenzelm@55656 ` 17` ``` and inverse :: "'a \ 'a" ``` wenzelm@47295 ` 18` ``` assume assoc: "\x y z. (x ** y) ** z = x ** (y ** z)" ``` wenzelm@47295 ` 19` ``` and left_one: "\x. one ** x = x" ``` wenzelm@47295 ` 20` ``` and left_inverse: "\x. inverse x ** x = one" ``` wenzelm@47295 ` 21` wenzelm@47295 ` 22` ``` txt {* some consequences *} ``` wenzelm@47295 ` 23` wenzelm@47295 ` 24` ``` have right_inverse: "\x. x ** inverse x = one" ``` wenzelm@47295 ` 25` ``` proof - ``` wenzelm@47295 ` 26` ``` fix x ``` wenzelm@47295 ` 27` ``` have "x ** inverse x = one ** (x ** inverse x)" ``` wenzelm@47295 ` 28` ``` by (simp only: left_one) ``` wenzelm@47295 ` 29` ``` also have "\ = one ** x ** inverse x" ``` wenzelm@47295 ` 30` ``` by (simp only: assoc) ``` wenzelm@47295 ` 31` ``` also have "\ = inverse (inverse x) ** inverse x ** x ** inverse x" ``` wenzelm@47295 ` 32` ``` by (simp only: left_inverse) ``` wenzelm@47295 ` 33` ``` also have "\ = inverse (inverse x) ** (inverse x ** x) ** inverse x" ``` wenzelm@47295 ` 34` ``` by (simp only: assoc) ``` wenzelm@47295 ` 35` ``` also have "\ = inverse (inverse x) ** one ** inverse x" ``` wenzelm@47295 ` 36` ``` by (simp only: left_inverse) ``` wenzelm@47295 ` 37` ``` also have "\ = inverse (inverse x) ** (one ** inverse x)" ``` wenzelm@47295 ` 38` ``` by (simp only: assoc) ``` wenzelm@47295 ` 39` ``` also have "\ = inverse (inverse x) ** inverse x" ``` wenzelm@47295 ` 40` ``` by (simp only: left_one) ``` wenzelm@47295 ` 41` ``` also have "\ = one" ``` wenzelm@47295 ` 42` ``` by (simp only: left_inverse) ``` wenzelm@47295 ` 43` ``` finally show "x ** inverse x = one" . ``` wenzelm@47295 ` 44` ``` qed ``` wenzelm@47295 ` 45` wenzelm@47295 ` 46` ``` have right_one: "\x. x ** one = x" ``` wenzelm@47295 ` 47` ``` proof - ``` wenzelm@47295 ` 48` ``` fix x ``` wenzelm@47295 ` 49` ``` have "x ** one = x ** (inverse x ** x)" ``` wenzelm@47295 ` 50` ``` by (simp only: left_inverse) ``` wenzelm@47295 ` 51` ``` also have "\ = x ** inverse x ** x" ``` wenzelm@47295 ` 52` ``` by (simp only: assoc) ``` wenzelm@47295 ` 53` ``` also have "\ = one ** x" ``` wenzelm@47295 ` 54` ``` by (simp only: right_inverse) ``` wenzelm@47295 ` 55` ``` also have "\ = x" ``` wenzelm@47295 ` 56` ``` by (simp only: left_one) ``` wenzelm@47295 ` 57` ``` finally show "x ** one = x" . ``` wenzelm@47295 ` 58` ``` qed ``` wenzelm@47295 ` 59` wenzelm@47295 ` 60` ``` have one_equality: "\e x. e ** x = x \ one = e" ``` wenzelm@47295 ` 61` ``` proof - ``` wenzelm@47295 ` 62` ``` fix e x ``` wenzelm@47295 ` 63` ``` assume eq: "e ** x = x" ``` wenzelm@47295 ` 64` ``` have "one = x ** inverse x" ``` wenzelm@47295 ` 65` ``` by (simp only: right_inverse) ``` wenzelm@47295 ` 66` ``` also have "\ = (e ** x) ** inverse x" ``` wenzelm@47295 ` 67` ``` by (simp only: eq) ``` wenzelm@47295 ` 68` ``` also have "\ = e ** (x ** inverse x)" ``` wenzelm@47295 ` 69` ``` by (simp only: assoc) ``` wenzelm@47295 ` 70` ``` also have "\ = e ** one" ``` wenzelm@47295 ` 71` ``` by (simp only: right_inverse) ``` wenzelm@47295 ` 72` ``` also have "\ = e" ``` wenzelm@47295 ` 73` ``` by (simp only: right_one) ``` wenzelm@47295 ` 74` ``` finally show "one = e" . ``` wenzelm@47295 ` 75` ``` qed ``` wenzelm@47295 ` 76` wenzelm@47295 ` 77` ``` have inverse_equality: "\x x'. x' ** x = one \ inverse x = x'" ``` wenzelm@47295 ` 78` ``` proof - ``` wenzelm@47295 ` 79` ``` fix x x' ``` wenzelm@47295 ` 80` ``` assume eq: "x' ** x = one" ``` wenzelm@47295 ` 81` ``` have "inverse x = one ** inverse x" ``` wenzelm@47295 ` 82` ``` by (simp only: left_one) ``` wenzelm@47295 ` 83` ``` also have "\ = (x' ** x) ** inverse x" ``` wenzelm@47295 ` 84` ``` by (simp only: eq) ``` wenzelm@47295 ` 85` ``` also have "\ = x' ** (x ** inverse x)" ``` wenzelm@47295 ` 86` ``` by (simp only: assoc) ``` wenzelm@47295 ` 87` ``` also have "\ = x' ** one" ``` wenzelm@47295 ` 88` ``` by (simp only: right_inverse) ``` wenzelm@47295 ` 89` ``` also have "\ = x'" ``` wenzelm@47295 ` 90` ``` by (simp only: right_one) ``` wenzelm@47295 ` 91` ``` finally show "inverse x = x'" . ``` wenzelm@47295 ` 92` ``` qed ``` wenzelm@47295 ` 93` wenzelm@47295 ` 94` ```end ``` wenzelm@47295 ` 95` wenzelm@47295 ` 96` ```end ```