1 (* Title: HOL/AxClasses/Tutorial/Group.thy |
1 (* Title: HOL/AxClasses/Tutorial/Group.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 theory Group = Main:; |
6 theory Group = Main: |
7 |
7 |
8 subsection {* Monoids and Groups *}; |
8 subsection {* Monoids and Groups *} |
9 |
9 |
10 consts |
10 consts |
11 times :: "'a => 'a => 'a" (infixl "[*]" 70) |
11 times :: "'a => 'a => 'a" (infixl "[*]" 70) |
12 inverse :: "'a => 'a" |
12 inverse :: "'a => 'a" |
13 one :: 'a; |
13 one :: 'a |
14 |
14 |
15 |
15 |
16 axclass |
16 axclass |
17 monoid < "term" |
17 monoid < "term" |
18 assoc: "(x [*] y) [*] z = x [*] (y [*] z)" |
18 assoc: "(x [*] y) [*] z = x [*] (y [*] z)" |
19 left_unit: "one [*] x = x" |
19 left_unit: "one [*] x = x" |
20 right_unit: "x [*] one = x"; |
20 right_unit: "x [*] one = x" |
21 |
21 |
22 |
22 |
23 axclass |
23 axclass |
24 semigroup < "term" |
24 semigroup < "term" |
25 assoc: "(x [*] y) [*] z = x [*] (y [*] z)"; |
25 assoc: "(x [*] y) [*] z = x [*] (y [*] z)" |
26 |
26 |
27 axclass |
27 axclass |
28 group < semigroup |
28 group < semigroup |
29 left_unit: "one [*] x = x" |
29 left_unit: "one [*] x = x" |
30 left_inverse: "inverse x [*] x = one"; |
30 left_inverse: "inverse x [*] x = one" |
31 |
31 |
32 axclass |
32 axclass |
33 agroup < group |
33 agroup < group |
34 commute: "x [*] y = y [*] x"; |
34 commute: "x [*] y = y [*] x" |
35 |
35 |
36 |
36 |
37 subsection {* Abstract reasoning *}; |
37 subsection {* Abstract reasoning *} |
38 |
38 |
39 theorem group_right_inverse: "x [*] inverse x = (one::'a::group)"; |
39 theorem group_right_inverse: "x [*] inverse x = (one::'a::group)" |
40 proof -; |
40 proof - |
41 have "x [*] inverse x = one [*] (x [*] inverse x)"; |
41 have "x [*] inverse x = one [*] (x [*] inverse x)" |
42 by (simp only: group.left_unit); |
42 by (simp only: group.left_unit) |
43 also; have "... = one [*] x [*] inverse x"; |
43 also have "... = one [*] x [*] inverse x" |
44 by (simp only: semigroup.assoc); |
44 by (simp only: semigroup.assoc) |
45 also; have "... = inverse (inverse x) [*] inverse x [*] x [*] inverse x"; |
45 also have "... = inverse (inverse x) [*] inverse x [*] x [*] inverse x" |
46 by (simp only: group.left_inverse); |
46 by (simp only: group.left_inverse) |
47 also; have "... = inverse (inverse x) [*] (inverse x [*] x) [*] inverse x"; |
47 also have "... = inverse (inverse x) [*] (inverse x [*] x) [*] inverse x" |
48 by (simp only: semigroup.assoc); |
48 by (simp only: semigroup.assoc) |
49 also; have "... = inverse (inverse x) [*] one [*] inverse x"; |
49 also have "... = inverse (inverse x) [*] one [*] inverse x" |
50 by (simp only: group.left_inverse); |
50 by (simp only: group.left_inverse) |
51 also; have "... = inverse (inverse x) [*] (one [*] inverse x)"; |
51 also have "... = inverse (inverse x) [*] (one [*] inverse x)" |
52 by (simp only: semigroup.assoc); |
52 by (simp only: semigroup.assoc) |
53 also; have "... = inverse (inverse x) [*] inverse x"; |
53 also have "... = inverse (inverse x) [*] inverse x" |
54 by (simp only: group.left_unit); |
54 by (simp only: group.left_unit) |
55 also; have "... = one"; |
55 also have "... = one" |
56 by (simp only: group.left_inverse); |
56 by (simp only: group.left_inverse) |
57 finally; show ?thesis; .; |
57 finally show ?thesis . |
58 qed; |
58 qed |
59 |
59 |
60 theorem group_right_unit: "x [*] one = (x::'a::group)"; |
60 theorem group_right_unit: "x [*] one = (x::'a::group)" |
61 proof -; |
61 proof - |
62 have "x [*] one = x [*] (inverse x [*] x)"; |
62 have "x [*] one = x [*] (inverse x [*] x)" |
63 by (simp only: group.left_inverse); |
63 by (simp only: group.left_inverse) |
64 also; have "... = x [*] inverse x [*] x"; |
64 also have "... = x [*] inverse x [*] x" |
65 by (simp only: semigroup.assoc); |
65 by (simp only: semigroup.assoc) |
66 also; have "... = one [*] x"; |
66 also have "... = one [*] x" |
67 by (simp only: group_right_inverse); |
67 by (simp only: group_right_inverse) |
68 also; have "... = x"; |
68 also have "... = x" |
69 by (simp only: group.left_unit); |
69 by (simp only: group.left_unit) |
70 finally; show ?thesis; .; |
70 finally show ?thesis . |
71 qed; |
71 qed |
72 |
72 |
73 |
73 |
74 subsection {* Abstract instantiation *}; |
74 subsection {* Abstract instantiation *} |
75 |
75 |
76 instance monoid < semigroup; |
76 instance monoid < semigroup |
77 proof intro_classes; |
77 proof intro_classes |
78 fix x y z :: "'a::monoid"; |
78 fix x y z :: "'a::monoid" |
79 show "x [*] y [*] z = x [*] (y [*] z)"; |
79 show "x [*] y [*] z = x [*] (y [*] z)" |
80 by (rule monoid.assoc); |
80 by (rule monoid.assoc) |
81 qed; |
81 qed |
82 |
82 |
83 instance group < monoid; |
83 instance group < monoid |
84 proof intro_classes; |
84 proof intro_classes |
85 fix x y z :: "'a::group"; |
85 fix x y z :: "'a::group" |
86 show "x [*] y [*] z = x [*] (y [*] z)"; |
86 show "x [*] y [*] z = x [*] (y [*] z)" |
87 by (rule semigroup.assoc); |
87 by (rule semigroup.assoc) |
88 show "one [*] x = x"; |
88 show "one [*] x = x" |
89 by (rule group.left_unit); |
89 by (rule group.left_unit) |
90 show "x [*] one = x"; |
90 show "x [*] one = x" |
91 by (rule group_right_unit); |
91 by (rule group_right_unit) |
92 qed; |
92 qed |
93 |
93 |
94 |
94 |
95 subsection {* Concrete instantiation *}; |
95 subsection {* Concrete instantiation *} |
96 |
96 |
97 defs (overloaded) |
97 defs (overloaded) |
98 times_bool_def: "x [*] y == x ~= (y::bool)" |
98 times_bool_def: "x [*] y == x ~= (y::bool)" |
99 inverse_bool_def: "inverse x == x::bool" |
99 inverse_bool_def: "inverse x == x::bool" |
100 unit_bool_def: "one == False"; |
100 unit_bool_def: "one == False" |
101 |
101 |
102 instance bool :: agroup; |
102 instance bool :: agroup |
103 proof (intro_classes, |
103 proof (intro_classes, |
104 unfold times_bool_def inverse_bool_def unit_bool_def); |
104 unfold times_bool_def inverse_bool_def unit_bool_def) |
105 fix x y z; |
105 fix x y z |
106 show "((x ~= y) ~= z) = (x ~= (y ~= z))"; by blast; |
106 show "((x ~= y) ~= z) = (x ~= (y ~= z))" by blast |
107 show "(False ~= x) = x"; by blast; |
107 show "(False ~= x) = x" by blast |
108 show "(x ~= x) = False"; by blast; |
108 show "(x ~= x) = False" by blast |
109 show "(x ~= y) = (y ~= x)"; by blast; |
109 show "(x ~= y) = (y ~= x)" by blast |
110 qed; |
110 qed |
111 |
111 |
112 |
112 |
113 subsection {* Lifting and Functors *}; |
113 subsection {* Lifting and Functors *} |
114 |
114 |
115 defs (overloaded) |
115 defs (overloaded) |
116 times_prod_def: "p [*] q == (fst p [*] fst q, snd p [*] snd q)"; |
116 times_prod_def: "p [*] q == (fst p [*] fst q, snd p [*] snd q)" |
117 |
117 |
118 instance * :: (semigroup, semigroup) semigroup; |
118 instance * :: (semigroup, semigroup) semigroup |
119 proof (intro_classes, unfold times_prod_def); |
119 proof (intro_classes, unfold times_prod_def) |
120 fix p q r :: "'a::semigroup * 'b::semigroup"; |
120 fix p q r :: "'a::semigroup * 'b::semigroup" |
121 show |
121 show |
122 "(fst (fst p [*] fst q, snd p [*] snd q) [*] fst r, |
122 "(fst (fst p [*] fst q, snd p [*] snd q) [*] fst r, |
123 snd (fst p [*] fst q, snd p [*] snd q) [*] snd r) = |
123 snd (fst p [*] fst q, snd p [*] snd q) [*] snd r) = |
124 (fst p [*] fst (fst q [*] fst r, snd q [*] snd r), |
124 (fst p [*] fst (fst q [*] fst r, snd q [*] snd r), |
125 snd p [*] snd (fst q [*] fst r, snd q [*] snd r))"; |
125 snd p [*] snd (fst q [*] fst r, snd q [*] snd r))" |
126 by (simp add: semigroup.assoc); |
126 by (simp add: semigroup.assoc) |
127 qed; |
127 qed |
128 |
128 |
129 end; |
129 end |