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