47295
|
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
|