|
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: "\<And>x y z. (x ** y) ** z = x ** (y ** z)" |
|
18 and left_one: "\<And>x. one ** x = x" |
|
19 and left_inverse: "\<And>x. 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: "e ** x = x \<Longrightarrow> one = e" |
|
59 proof - |
|
60 fix e x |
|
61 assume eq: "e ** x = x" |
|
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: "x' ** x = one \<Longrightarrow> inverse x = x'" |
|
76 proof - |
|
77 fix x x' |
|
78 assume eq: "x' ** x = one" |
|
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 |