src/HOL/Isar_Examples/Group_Context.thy
 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_Context.thy
2     Author:     Makarius
3 *)
5 header {* Some algebraic identities derived from group axioms -- theory context version *}
7 theory Group_Context
8 imports Main
9 begin
11 text {* hypothetical group axiomatization *}
13 context
14   fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
15     and one :: "'a"
16     and inverse :: "'a \<Rightarrow> '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
22 text {* some consequences *}
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
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
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
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
92 end
94 end