author | traytel |
Fri, 05 Apr 2013 22:08:42 +0200 | |
changeset 51678 | 1e33b81c328a |
parent 47872 | 1f6f519cdb32 |
child 55656 | eb07b0acbebc |
permissions | -rw-r--r-- |
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" |
|
47311
1addbe2a7458
close context elements via Expression.cert/read_declaration;
wenzelm
parents:
47295
diff
changeset
|
17 |
assumes assoc: "(x ** y) ** z = x ** (y ** z)" |
1addbe2a7458
close context elements via Expression.cert/read_declaration;
wenzelm
parents:
47295
diff
changeset
|
18 |
and left_one: "one ** x = x" |
1addbe2a7458
close context elements via Expression.cert/read_declaration;
wenzelm
parents:
47295
diff
changeset
|
19 |
and left_inverse: "inverse x ** x = one" |
47295 | 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 |
||
47872 | 58 |
lemma one_equality: |
59 |
assumes eq: "e ** x = x" |
|
60 |
shows "one = e" |
|
47295 | 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 |
||
47872 | 75 |
lemma inverse_equality: |
76 |
assumes eq: "x' ** x = one" |
|
77 |
shows "inverse x = x'" |
|
47295 | 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 |