src/HOL/Isar_Examples/Group_Context.thy
 author hoelzl Tue Mar 26 12:20:58 2013 +0100 (2013-03-26) changeset 51526 155263089e7b parent 47872 1f6f519cdb32 child 55656 eb07b0acbebc permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
```     1 (*  Title:      HOL/Isar_Examples/Group_Context.thy
```
```     2     Author:     Makarius
```
```     3 *)
```
```     4
```
```     5 header {* Some algebraic identities derived from group axioms -- theory context version *}
```
```     6
```
```     7 theory Group_Context
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 text {* hypothetical group axiomatization *}
```
```    12
```
```    13 context
```
```    14   fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
```
```    15     and one :: "'a"
```
```    16     and inverse :: "'a => 'a"
```
```    17   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
```
```    18     and left_one: "one ** x = x"
```
```    19     and left_inverse: "inverse x ** x = one"
```
```    20 begin
```
```    21
```
```    22 text {* some consequences *}
```
```    23
```
```    24 lemma right_inverse: "x ** inverse x = one"
```
```    25 proof -
```
```    26   have "x ** inverse x = one ** (x ** inverse x)"
```
```    27     by (simp only: left_one)
```
```    28   also have "\<dots> = one ** x ** inverse x"
```
```    29     by (simp only: assoc)
```
```    30   also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"
```
```    31     by (simp only: left_inverse)
```
```    32   also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"
```
```    33     by (simp only: assoc)
```
```    34   also have "\<dots> = inverse (inverse x) ** one ** inverse x"
```
```    35     by (simp only: left_inverse)
```
```    36   also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"
```
```    37     by (simp only: assoc)
```
```    38   also have "\<dots> = inverse (inverse x) ** inverse x"
```
```    39     by (simp only: left_one)
```
```    40   also have "\<dots> = one"
```
```    41     by (simp only: left_inverse)
```
```    42   finally show "x ** inverse x = one" .
```
```    43 qed
```
```    44
```
```    45 lemma right_one: "x ** one = x"
```
```    46 proof -
```
```    47   have "x ** one = x ** (inverse x ** x)"
```
```    48     by (simp only: left_inverse)
```
```    49   also have "\<dots> = x ** inverse x ** x"
```
```    50     by (simp only: assoc)
```
```    51   also have "\<dots> = one ** x"
```
```    52     by (simp only: right_inverse)
```
```    53   also have "\<dots> = x"
```
```    54     by (simp only: left_one)
```
```    55   finally show "x ** one = x" .
```
```    56 qed
```
```    57
```
```    58 lemma one_equality:
```
```    59   assumes eq: "e ** x = x"
```
```    60   shows "one = e"
```
```    61 proof -
```
```    62   have "one = x ** inverse x"
```
```    63     by (simp only: right_inverse)
```
```    64   also have "\<dots> = (e ** x) ** inverse x"
```
```    65     by (simp only: eq)
```
```    66   also have "\<dots> = e ** (x ** inverse x)"
```
```    67     by (simp only: assoc)
```
```    68   also have "\<dots> = e ** one"
```
```    69     by (simp only: right_inverse)
```
```    70   also have "\<dots> = e"
```
```    71     by (simp only: right_one)
```
```    72   finally show "one = e" .
```
```    73 qed
```
```    74
```
```    75 lemma inverse_equality:
```
```    76   assumes eq: "x' ** x = one"
```
```    77   shows "inverse x = x'"
```
```    78 proof -
```
```    79   have "inverse x = one ** inverse x"
```
```    80     by (simp only: left_one)
```
```    81   also have "\<dots> = (x' ** x) ** inverse x"
```
```    82     by (simp only: eq)
```
```    83   also have "\<dots> = x' ** (x ** inverse x)"
```
```    84     by (simp only: assoc)
```
```    85   also have "\<dots> = x' ** one"
```
```    86     by (simp only: right_inverse)
```
```    87   also have "\<dots> = x'"
```
```    88     by (simp only: right_one)
```
```    89   finally show "inverse x = x'" .
```
```    90 qed
```
```    91
```
```    92 end
```
```    93
```
```    94 end
```