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