10 |
10 |
11 val simp_G = simplify (simpset() addsimps [Group_def]) (thm "Group_G"); |
11 val simp_G = simplify (simpset() addsimps [Group_def]) (thm "Group_G"); |
12 Addsimps [simp_G, thm "Group_G"]; |
12 Addsimps [simp_G, thm "Group_G"]; |
13 |
13 |
14 |
14 |
15 goal LocaleGroup.thy "e : carrier G"; |
15 Goal "e : carrier G"; |
16 by (afs [thm "e_def"] 1); |
16 by (simp_tac (simpset() addsimps [thm "e_def"]) 1); |
17 val e_closed = result(); |
17 qed "e_closed"; |
18 |
18 |
19 (* Mit dieser Def ist es halt schwierig *) |
19 (* Mit dieser Def ist es halt schwierig *) |
20 goal LocaleGroup.thy "op # : carrier G -> carrier G -> carrier G"; |
20 Goal "op # : carrier G -> carrier G -> carrier G"; |
21 by (res_inst_tac [("t","op #")] ssubst 1); |
21 by (res_inst_tac [("t","op #")] ssubst 1); |
22 by (rtac ext 1); |
22 by (rtac ext 1); |
23 by (rtac ext 1); |
23 by (rtac ext 1); |
24 by (rtac meta_eq_to_obj_eq 1); |
24 by (rtac meta_eq_to_obj_eq 1); |
25 by (rtac (thm "binop_def") 1); |
25 by (rtac (thm "binop_def") 1); |
26 by (Asm_full_simp_tac 1); |
26 by (Asm_full_simp_tac 1); |
27 val binop_funcset = result(); |
27 qed "binop_funcset"; |
28 |
28 |
29 goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G |] ==> x # y : carrier G"; |
29 Goal "[| x: carrier G; y: carrier G |] ==> x # y : carrier G"; |
30 by (afs [binop_funcset RS funcset2E1] 1); |
30 by (asm_simp_tac |
31 val binop_closed = result(); |
31 (simpset() addsimps [binop_funcset RS funcset_mem RS funcset_mem]) 1); |
|
32 qed "binop_closed"; |
32 |
33 |
33 goal LocaleGroup.thy "inv : carrier G -> carrier G"; |
34 Addsimps [binop_closed, e_closed]; |
34 by (res_inst_tac [("t","inv")] ssubst 1); |
|
35 by (rtac ext 1); |
|
36 by (rtac meta_eq_to_obj_eq 1); |
|
37 by (rtac (thm "inv_def") 1); |
|
38 by (Asm_full_simp_tac 1); |
|
39 val inv_funcset = result(); |
|
40 |
35 |
41 goal LocaleGroup.thy "!! x . x: carrier G ==> x -| : carrier G"; |
36 Goal "INV : carrier G -> carrier G"; |
42 by (afs [inv_funcset RS funcsetE1] 1); |
37 by (asm_simp_tac (simpset() addsimps [thm "inv_def"]) 1); |
43 val inv_closed = result(); |
38 qed "inv_funcset"; |
44 |
39 |
|
40 Goal "x: carrier G ==> x -| : carrier G"; |
|
41 by (asm_simp_tac (simpset() addsimps [inv_funcset RS funcset_mem]) 1); |
|
42 qed "inv_closed"; |
45 |
43 |
46 goal LocaleGroup.thy "!! x . x: carrier G ==> e # x = x"; |
44 Goal "x: carrier G ==> e # x = x"; |
47 by (afs [thm "e_def", thm "binop_def"] 1); |
45 by (asm_simp_tac (simpset() addsimps [thm "e_def", thm "binop_def"]) 1); |
48 val e_ax1 = result(); |
46 qed "e_ax1"; |
49 |
47 |
50 goal LocaleGroup.thy "!! x. x: carrier G ==> (x -|) # x = e"; |
48 Goal "x: carrier G ==> (x -|) # x = e"; |
51 by (afs [thm "binop_def", thm "inv_def", thm "e_def"] 1); |
49 by (asm_simp_tac |
52 val inv_ax2 = result(); |
50 (simpset() addsimps [thm "binop_def", thm "inv_def", thm "e_def"]) 1); |
|
51 qed "inv_ax2"; |
53 |
52 |
54 goal LocaleGroup.thy "!! x y z. [| x: carrier G; y: carrier G; z: carrier G |]\ |
53 Addsimps [inv_closed, e_ax1, inv_ax2]; |
|
54 |
|
55 Goal "[| x: carrier G; y: carrier G; z: carrier G |]\ |
55 \ ==> (x # y) # z = x # (y # z)"; |
56 \ ==> (x # y) # z = x # (y # z)"; |
56 by (afs [thm "binop_def"] 1); |
57 by (asm_simp_tac (simpset() addsimps [thm "binop_def"]) 1); |
57 val binop_assoc = result(); |
58 qed "binop_assoc"; |
58 |
59 |
59 goal LocaleGroup.thy "!! G f i e1. [|f : G -> G -> G; i: G -> G; e1: G;\ |
60 Goal "[|f : A -> A -> A; i: A -> A; e1: A;\ |
60 \ ! x: G. (f (i x) x = e1); ! x: G. (f e1 x = x);\ |
61 \ ! x: A. (f (i x) x = e1); ! x: A. (f e1 x = x);\ |
61 \ ! x: G. ! y: G. ! z: G.(f (f x y) z = f (x) (f y z)) |] \ |
62 \ ! x: A. ! y: A. ! z: A.(f (f x y) z = f (x) (f y z)) |] \ |
62 \ ==> (| carrier = G, bin_op = f, inverse = i, unit = e1 |) : Group"; |
63 \ ==> (| carrier = A, bin_op = f, inverse = i, unit = e1 |) : Group"; |
63 by (afs [Group_def] 1); |
64 by (asm_simp_tac (simpset() addsimps [Group_def]) 1); |
64 val GroupI = result(); |
65 qed "GroupI"; |
65 |
66 |
66 (*****) |
67 (*****) |
67 (* Now the real derivations *) |
68 (* Now the real derivations *) |
68 |
69 |
69 goal LocaleGroup.thy "!! x y z. [| x : carrier G ; y : carrier G; z : carrier G;\ |
70 Goal "[| x # y = x # z; \ |
70 \ x # y = x # z |] ==> y = z"; |
71 \ x : carrier G ; y : carrier G; z : carrier G |] ==> y = z"; |
71 (* remarkable: In the following step the use of e_ax1 instead of unit_ax1 |
|
72 is better! It doesn't produce G: Group as subgoal and the nice syntax stays *) |
|
73 by (res_inst_tac [("P","%r. r = z")] (e_ax1 RS subst) 1); |
72 by (res_inst_tac [("P","%r. r = z")] (e_ax1 RS subst) 1); |
74 by (assume_tac 1); |
73 by (assume_tac 1); |
75 (* great: we can use the nice syntax even in res_inst_tac *) |
74 (* great: we can use the nice syntax even in res_inst_tac *) |
76 by (res_inst_tac [("P","%r. r # y = z")] subst 1); |
75 by (res_inst_tac [("P","%r. r # y = z")] (inv_ax2 RS subst) 1); |
77 by (res_inst_tac [("x","x")] inv_ax2 1); |
|
78 by (assume_tac 1); |
76 by (assume_tac 1); |
79 by (stac binop_assoc 1); |
77 by (asm_simp_tac (simpset() delsimps [inv_ax2] addsimps [binop_assoc]) 1); |
80 by (rtac inv_closed 1); |
78 by (asm_simp_tac (simpset() addsimps [binop_assoc RS sym]) 1); |
81 by (assume_tac 1); |
79 qed "left_cancellation"; |
82 by (assume_tac 1); |
|
83 by (assume_tac 1); |
|
84 by (etac ssubst 1); |
|
85 by (rtac (binop_assoc RS subst) 1); |
|
86 by (rtac inv_closed 1); |
|
87 by (assume_tac 1); |
|
88 by (assume_tac 1); |
|
89 by (assume_tac 1); |
|
90 by (stac inv_ax2 1); |
|
91 by (assume_tac 1); |
|
92 by (stac e_ax1 1); |
|
93 by (assume_tac 1); |
|
94 by (rtac refl 1); |
|
95 val left_cancellation = result(); |
|
96 |
80 |
97 |
81 |
98 (* here are the other directions of basic lemmas, they needed a cancellation (left) *) |
82 (* Here are the other directions of basic lemmas. |
99 (* to be able to show the other directions of inverse and unity axiom we need:*) |
83 They needed a cancellation (left) to be able to show the other |
100 goal LocaleGroup.thy "!! x. x: carrier G ==> x # e = x"; |
84 directions of inverse and unity axiom.*) |
101 (* here is a problem with res_inst_tac: in Fun there is a |
85 Goal "x: carrier G ==> x # e = x"; |
102 constant inv, and that gets addressed when we type in -|. |
86 by (rtac left_cancellation 1); |
103 We have to use the defining term and then fold the def of inv *) |
87 by (etac inv_closed 2); |
104 by (res_inst_tac [("x","inverse G x")] left_cancellation 1); |
88 by (auto_tac (claset(), simpset() addsimps [binop_assoc RS sym])); |
105 by (fold_goals_tac [thm "inv_def"]); |
89 qed "e_ax2"; |
106 by (fast_tac (claset() addSEs [inv_closed]) 1); |
|
107 by (afs [binop_closed, e_closed] 1); |
|
108 by (assume_tac 1); |
|
109 by (rtac (binop_assoc RS subst) 1); |
|
110 by (fast_tac (claset() addSEs [inv_closed]) 1); |
|
111 by (assume_tac 1); |
|
112 by (rtac (e_closed) 1); |
|
113 by (stac inv_ax2 1); |
|
114 by (assume_tac 1); |
|
115 by (stac e_ax1 1); |
|
116 by (rtac e_closed 1); |
|
117 by (rtac refl 1); |
|
118 val e_ax2 = result(); |
|
119 |
90 |
120 goal LocaleGroup.thy "!! x. [| x: carrier G; x # x = x |] ==> x = e"; |
91 Addsimps [e_ax2]; |
121 by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS forw_subst) 1); |
92 |
122 by (assume_tac 1); |
93 Goal "[| x: carrier G; x # x = x |] ==> x = e"; |
|
94 by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS ssubst) 1); |
|
95 by (etac left_cancellation 2); |
|
96 by Auto_tac; |
|
97 qed "idempotent_e"; |
|
98 |
|
99 Goal "x: carrier G ==> x # (x -|) = e"; |
|
100 by (rtac idempotent_e 1); |
|
101 by (Asm_simp_tac 1); |
|
102 by (subgoal_tac "(x # x -|) # x # x -| = x # (x -| # x) # x -|" 1); |
|
103 by (asm_simp_tac (simpset() delsimps [inv_ax2] |
|
104 addsimps [binop_assoc]) 2); |
|
105 by Auto_tac; |
|
106 qed "inv_ax1"; |
|
107 |
|
108 Addsimps [inv_ax1]; |
|
109 |
|
110 Goal "[| x # y = e; x: carrier G; y: carrier G |] ==> y = x -|"; |
123 by (res_inst_tac [("x","x")] left_cancellation 1); |
111 by (res_inst_tac [("x","x")] left_cancellation 1); |
124 by (assume_tac 1); |
112 by Auto_tac; |
125 by (assume_tac 1); |
113 qed "inv_unique"; |
126 by (rtac e_closed 1); |
|
127 by (assume_tac 1); |
|
128 val idempotent_e = result(); |
|
129 |
114 |
130 goal LocaleGroup.thy "!! x. x: carrier G ==> x # (x -|) = e"; |
115 Goal "x : carrier G ==> x -| -| = x"; |
131 by (rtac idempotent_e 1); |
116 by (res_inst_tac [("x","x -|")] left_cancellation 1); |
132 by (afs [binop_closed,inv_closed] 1); |
117 by Auto_tac; |
133 by (stac binop_assoc 1); |
118 qed "inv_inv"; |
134 by (assume_tac 1); |
119 |
135 by (afs [inv_closed] 1); |
120 Addsimps [inv_inv]; |
136 by (afs [binop_closed,inv_closed] 1); |
121 |
137 by (res_inst_tac [("t","x -| # x # x -|")] subst 1); |
122 Goal "[| x : carrier G; y : carrier G |] ==> (x # y) -| = y -| # x -|"; |
138 by (rtac binop_assoc 1); |
123 by (rtac (inv_unique RS sym) 1); |
139 by (afs [inv_closed] 1); |
124 by (subgoal_tac "(x # y) # y -| # x -| = x # (y # y -|) # x -|" 1); |
140 by (assume_tac 1); |
125 by (asm_simp_tac (simpset() delsimps [inv_ax1, inv_ax2] |
141 by (afs [inv_closed] 1); |
126 addsimps [binop_assoc]) 2); |
142 by (stac inv_ax2 1); |
127 by Auto_tac; |
143 by (assume_tac 1); |
128 qed "inv_prod"; |
144 by (stac e_ax1 1); |
|
145 by (afs [inv_closed] 1); |
|
146 by (rtac refl 1); |
|
147 val inv_ax1 = result(); |
|
148 |
129 |
149 |
130 |
150 goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G; \ |
131 Goal "[| y # x = z # x; x : carrier G; y : carrier G; \ |
151 \ x # y = e |] ==> y = x -|"; |
132 \ z : carrier G |] ==> y = z"; |
152 by (res_inst_tac [("x","x")] left_cancellation 1); |
|
153 by (assume_tac 1); |
|
154 by (assume_tac 1); |
|
155 by (afs [inv_closed] 1); |
|
156 by (stac inv_ax1 1); |
|
157 by (assume_tac 1); |
|
158 by (assume_tac 1); |
|
159 val inv_unique = result(); |
|
160 |
|
161 goal LocaleGroup.thy "!! x. x : carrier G ==> x -| -| = x"; |
|
162 by (res_inst_tac [("x","inverse G x")] left_cancellation 1); |
|
163 by (fold_goals_tac [thm "inv_def"]); |
|
164 by (afs [inv_closed] 1); |
|
165 by (afs [inv_closed] 1); |
|
166 by (assume_tac 1); |
|
167 by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1); |
|
168 val inv_inv = result(); |
|
169 |
|
170 goal LocaleGroup.thy "!! x y. [| x : carrier G; y : carrier G |]\ |
|
171 \ ==> (x # y) -| = y -| # x -|"; |
|
172 by (rtac sym 1); |
|
173 by (rtac inv_unique 1); |
|
174 by (afs [binop_closed] 1); |
|
175 by (afs [inv_closed,binop_closed] 1); |
|
176 by (afs [binop_assoc,inv_closed,binop_closed] 1); |
|
177 by (res_inst_tac [("x1","y")] (binop_assoc RS subst) 1); |
|
178 by (assume_tac 1); |
|
179 by (afs [inv_closed] 1); |
|
180 by (afs [inv_closed] 1); |
|
181 by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1); |
|
182 val inv_prod = result(); |
|
183 |
|
184 |
|
185 goal LocaleGroup.thy "!! x y z. [| x : carrier G; y : carrier G;\ |
|
186 \ z : carrier G; y # x = z # x|] ==> y = z"; |
|
187 by (res_inst_tac [("P","%r. r = z")] (e_ax2 RS subst) 1); |
133 by (res_inst_tac [("P","%r. r = z")] (e_ax2 RS subst) 1); |
188 by (assume_tac 1); |
134 by (assume_tac 1); |
189 by (res_inst_tac [("P","%r. y # r = z")] subst 1); |
135 by (res_inst_tac [("P","%r. y # r = z")] (inv_ax1 RS subst) 1); |
190 by (rtac inv_ax1 1); |
|
191 by (assume_tac 1); |
136 by (assume_tac 1); |
192 by (rtac (binop_assoc RS subst) 1); |
137 by (asm_simp_tac (simpset() delsimps [inv_ax1] |
193 by (assume_tac 1); |
138 addsimps [binop_assoc RS sym]) 1); |
194 by (assume_tac 1); |
139 by (asm_simp_tac (simpset() addsimps [binop_assoc]) 1); |
195 by (afs [inv_closed] 1); |
140 qed "right_cancellation"; |
196 by (etac ssubst 1); |
141 |
197 by (afs [binop_assoc,inv_closed,inv_ax1,e_ax2] 1); |
142 Close_locale(); |
198 val right_cancellation = result(); |
|
199 |
143 |
200 (* example what happens if export *) |
144 (* example what happens if export *) |
201 val Left_cancellation = export left_cancellation; |
145 val Left_cancellation = export left_cancellation; |