src/HOL/Isar_Examples/Group_Context.thy
 author wenzelm Tue Sep 26 20:54:40 2017 +0200 (23 months ago) changeset 66695 91500c024c7f parent 63585 f4a308fdf664 permissions -rw-r--r--
tuned;
 wenzelm@47295 ` 1` ```(* Title: HOL/Isar_Examples/Group_Context.thy ``` wenzelm@47295 ` 2` ``` Author: Makarius ``` wenzelm@47295 ` 3` ```*) ``` wenzelm@47295 ` 4` wenzelm@58882 ` 5` ```section \Some algebraic identities derived from group axioms -- theory context version\ ``` wenzelm@47295 ` 6` wenzelm@47295 ` 7` ```theory Group_Context ``` wenzelm@63585 ` 8` ``` imports Main ``` wenzelm@47295 ` 9` ```begin ``` wenzelm@47295 ` 10` wenzelm@58614 ` 11` ```text \hypothetical group axiomatization\ ``` wenzelm@47295 ` 12` wenzelm@47295 ` 13` ```context ``` wenzelm@61797 ` 14` ``` fixes prod :: "'a \ 'a \ 'a" (infixl "\" 70) ``` wenzelm@47295 ` 15` ``` and one :: "'a" ``` wenzelm@55656 ` 16` ``` and inverse :: "'a \ 'a" ``` wenzelm@61797 ` 17` ``` assumes assoc: "(x \ y) \ z = x \ (y \ z)" ``` wenzelm@61797 ` 18` ``` and left_one: "one \ x = x" ``` wenzelm@61797 ` 19` ``` and left_inverse: "inverse x \ x = one" ``` wenzelm@47295 ` 20` ```begin ``` wenzelm@47295 ` 21` wenzelm@58614 ` 22` ```text \some consequences\ ``` wenzelm@47295 ` 23` wenzelm@61797 ` 24` ```lemma right_inverse: "x \ inverse x = one" ``` wenzelm@47295 ` 25` ```proof - ``` wenzelm@61797 ` 26` ``` have "x \ inverse x = one \ (x \ inverse x)" ``` wenzelm@47295 ` 27` ``` by (simp only: left_one) ``` wenzelm@61797 ` 28` ``` also have "\ = one \ x \ inverse x" ``` wenzelm@47295 ` 29` ``` by (simp only: assoc) ``` wenzelm@61797 ` 30` ``` also have "\ = inverse (inverse x) \ inverse x \ x \ inverse x" ``` wenzelm@47295 ` 31` ``` by (simp only: left_inverse) ``` wenzelm@61797 ` 32` ``` also have "\ = inverse (inverse x) \ (inverse x \ x) \ inverse x" ``` wenzelm@47295 ` 33` ``` by (simp only: assoc) ``` wenzelm@61797 ` 34` ``` also have "\ = inverse (inverse x) \ one \ inverse x" ``` wenzelm@47295 ` 35` ``` by (simp only: left_inverse) ``` wenzelm@61797 ` 36` ``` also have "\ = inverse (inverse x) \ (one \ inverse x)" ``` wenzelm@47295 ` 37` ``` by (simp only: assoc) ``` wenzelm@61797 ` 38` ``` also have "\ = inverse (inverse x) \ inverse x" ``` wenzelm@47295 ` 39` ``` by (simp only: left_one) ``` wenzelm@47295 ` 40` ``` also have "\ = one" ``` wenzelm@47295 ` 41` ``` by (simp only: left_inverse) ``` wenzelm@61797 ` 42` ``` finally show ?thesis . ``` wenzelm@47295 ` 43` ```qed ``` wenzelm@47295 ` 44` wenzelm@61797 ` 45` ```lemma right_one: "x \ one = x" ``` wenzelm@47295 ` 46` ```proof - ``` wenzelm@61797 ` 47` ``` have "x \ one = x \ (inverse x \ x)" ``` wenzelm@47295 ` 48` ``` by (simp only: left_inverse) ``` wenzelm@61797 ` 49` ``` also have "\ = x \ inverse x \ x" ``` wenzelm@47295 ` 50` ``` by (simp only: assoc) ``` wenzelm@61797 ` 51` ``` also have "\ = one \ x" ``` wenzelm@47295 ` 52` ``` by (simp only: right_inverse) ``` wenzelm@47295 ` 53` ``` also have "\ = x" ``` wenzelm@47295 ` 54` ``` by (simp only: left_one) ``` wenzelm@61797 ` 55` ``` finally show ?thesis . ``` wenzelm@47295 ` 56` ```qed ``` wenzelm@47295 ` 57` wenzelm@47872 ` 58` ```lemma one_equality: ``` wenzelm@61797 ` 59` ``` assumes eq: "e \ x = x" ``` wenzelm@47872 ` 60` ``` shows "one = e" ``` wenzelm@47295 ` 61` ```proof - ``` wenzelm@61797 ` 62` ``` have "one = x \ inverse x" ``` wenzelm@47295 ` 63` ``` by (simp only: right_inverse) ``` wenzelm@61797 ` 64` ``` also have "\ = (e \ x) \ inverse x" ``` wenzelm@47295 ` 65` ``` by (simp only: eq) ``` wenzelm@61797 ` 66` ``` also have "\ = e \ (x \ inverse x)" ``` wenzelm@47295 ` 67` ``` by (simp only: assoc) ``` wenzelm@61797 ` 68` ``` also have "\ = e \ one" ``` wenzelm@47295 ` 69` ``` by (simp only: right_inverse) ``` wenzelm@47295 ` 70` ``` also have "\ = e" ``` wenzelm@47295 ` 71` ``` by (simp only: right_one) ``` wenzelm@61797 ` 72` ``` finally show ?thesis . ``` wenzelm@47295 ` 73` ```qed ``` wenzelm@47295 ` 74` wenzelm@47872 ` 75` ```lemma inverse_equality: ``` wenzelm@61797 ` 76` ``` assumes eq: "x' \ x = one" ``` wenzelm@47872 ` 77` ``` shows "inverse x = x'" ``` wenzelm@47295 ` 78` ```proof - ``` wenzelm@61797 ` 79` ``` have "inverse x = one \ inverse x" ``` wenzelm@47295 ` 80` ``` by (simp only: left_one) ``` wenzelm@61797 ` 81` ``` also have "\ = (x' \ x) \ inverse x" ``` wenzelm@47295 ` 82` ``` by (simp only: eq) ``` wenzelm@61797 ` 83` ``` also have "\ = x' \ (x \ inverse x)" ``` wenzelm@47295 ` 84` ``` by (simp only: assoc) ``` wenzelm@61797 ` 85` ``` also have "\ = x' \ one" ``` wenzelm@47295 ` 86` ``` by (simp only: right_inverse) ``` wenzelm@47295 ` 87` ``` also have "\ = x'" ``` wenzelm@47295 ` 88` ``` by (simp only: right_one) ``` wenzelm@61797 ` 89` ``` finally show ?thesis . ``` wenzelm@47295 ` 90` ```qed ``` wenzelm@47295 ` 91` wenzelm@47295 ` 92` ```end ``` wenzelm@47295 ` 93` wenzelm@47295 ` 94` ```end ```