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