38 THEN (atac 2) |
38 THEN (atac 2) |
39 THEN (etac sym 1)) |
39 THEN (etac sym 1)) |
40 |
40 |
41 in |
41 in |
42 |
42 |
43 val less_ssum1a = prove_goalw Ssum1.thy [less_ssum_def] |
43 val less_ssum1a = prove_goalw thy [less_ssum_def] |
44 "[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less_ssum s1 s2 = (x << y)" |
44 "[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less s1 s2 = (x << y)" |
45 (fn prems => |
45 (fn prems => |
46 [ |
46 [ |
47 (cut_facts_tac prems 1), |
47 (cut_facts_tac prems 1), |
48 (rtac select_equality 1), |
48 (rtac select_equality 1), |
49 (dtac conjunct1 2), |
49 (dtac conjunct1 2), |
79 (UU_right "v"), |
79 (UU_right "v"), |
80 (Simp_tac 1) |
80 (Simp_tac 1) |
81 ]); |
81 ]); |
82 |
82 |
83 |
83 |
84 val less_ssum1b = prove_goalw Ssum1.thy [less_ssum_def] |
84 val less_ssum1b = prove_goalw thy [less_ssum_def] |
85 "[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less_ssum s1 s2 = (x << y)" |
85 "[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less s1 s2 = (x << y)" |
86 (fn prems => |
86 (fn prems => |
87 [ |
87 [ |
88 (cut_facts_tac prems 1), |
88 (cut_facts_tac prems 1), |
89 (rtac select_equality 1), |
89 (rtac select_equality 1), |
90 (dtac conjunct2 2), |
90 (dtac conjunct2 2), |
121 (etac sym 1), |
121 (etac sym 1), |
122 (rtac refl_less 1) |
122 (rtac refl_less 1) |
123 ]); |
123 ]); |
124 |
124 |
125 |
125 |
126 val less_ssum1c = prove_goalw Ssum1.thy [less_ssum_def] |
126 val less_ssum1c = prove_goalw thy [less_ssum_def] |
127 "[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less_ssum s1 s2 = ((x::'a) = UU)" |
127 "[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less s1 s2 = ((x::'a) = UU)" |
128 (fn prems => |
128 (fn prems => |
129 [ |
129 [ |
130 (cut_facts_tac prems 1), |
130 (cut_facts_tac prems 1), |
131 (rtac select_equality 1), |
131 (rtac select_equality 1), |
132 (rtac conjI 1), |
132 (rtac conjI 1), |
163 (etac mp 1), |
163 (etac mp 1), |
164 (fast_tac HOL_cs 1) |
164 (fast_tac HOL_cs 1) |
165 ]); |
165 ]); |
166 |
166 |
167 |
167 |
168 val less_ssum1d = prove_goalw Ssum1.thy [less_ssum_def] |
168 val less_ssum1d = prove_goalw thy [less_ssum_def] |
169 "[|s1=Isinr(x); s2=Isinl(y)|] ==> less_ssum s1 s2 = (x = UU)" |
169 "[|s1=Isinr(x); s2=Isinl(y)|] ==> less s1 s2 = (x = UU)" |
170 (fn prems => |
170 (fn prems => |
171 [ |
171 [ |
172 (cut_facts_tac prems 1), |
172 (cut_facts_tac prems 1), |
173 (rtac select_equality 1), |
173 (rtac select_equality 1), |
174 (dtac conjunct2 2), |
174 (dtac conjunct2 2), |
210 |
210 |
211 (* ------------------------------------------------------------------------ *) |
211 (* ------------------------------------------------------------------------ *) |
212 (* optimize lemmas about less_ssum *) |
212 (* optimize lemmas about less_ssum *) |
213 (* ------------------------------------------------------------------------ *) |
213 (* ------------------------------------------------------------------------ *) |
214 |
214 |
215 qed_goal "less_ssum2a" Ssum1.thy |
215 qed_goal "less_ssum2a" thy |
216 "less_ssum (Isinl x) (Isinl y) = (x << y)" |
216 "less (Isinl x) (Isinl y) = (x << y)" |
217 (fn prems => |
217 (fn prems => |
218 [ |
218 [ |
219 (rtac less_ssum1a 1), |
219 (rtac less_ssum1a 1), |
220 (rtac refl 1), |
220 (rtac refl 1), |
221 (rtac refl 1) |
221 (rtac refl 1) |
222 ]); |
222 ]); |
223 |
223 |
224 qed_goal "less_ssum2b" Ssum1.thy |
224 qed_goal "less_ssum2b" thy |
225 "less_ssum (Isinr x) (Isinr y) = (x << y)" |
225 "less (Isinr x) (Isinr y) = (x << y)" |
226 (fn prems => |
226 (fn prems => |
227 [ |
227 [ |
228 (rtac less_ssum1b 1), |
228 (rtac less_ssum1b 1), |
229 (rtac refl 1), |
229 (rtac refl 1), |
230 (rtac refl 1) |
230 (rtac refl 1) |
231 ]); |
231 ]); |
232 |
232 |
233 qed_goal "less_ssum2c" Ssum1.thy |
233 qed_goal "less_ssum2c" thy |
234 "less_ssum (Isinl x) (Isinr y) = (x = UU)" |
234 "less (Isinl x) (Isinr y) = (x = UU)" |
235 (fn prems => |
235 (fn prems => |
236 [ |
236 [ |
237 (rtac less_ssum1c 1), |
237 (rtac less_ssum1c 1), |
238 (rtac refl 1), |
238 (rtac refl 1), |
239 (rtac refl 1) |
239 (rtac refl 1) |
240 ]); |
240 ]); |
241 |
241 |
242 qed_goal "less_ssum2d" Ssum1.thy |
242 qed_goal "less_ssum2d" thy |
243 "less_ssum (Isinr x) (Isinl y) = (x = UU)" |
243 "less (Isinr x) (Isinl y) = (x = UU)" |
244 (fn prems => |
244 (fn prems => |
245 [ |
245 [ |
246 (rtac less_ssum1d 1), |
246 (rtac less_ssum1d 1), |
247 (rtac refl 1), |
247 (rtac refl 1), |
248 (rtac refl 1) |
248 (rtac refl 1) |
251 |
251 |
252 (* ------------------------------------------------------------------------ *) |
252 (* ------------------------------------------------------------------------ *) |
253 (* less_ssum is a partial order on ++ *) |
253 (* less_ssum is a partial order on ++ *) |
254 (* ------------------------------------------------------------------------ *) |
254 (* ------------------------------------------------------------------------ *) |
255 |
255 |
256 qed_goal "refl_less_ssum" Ssum1.thy "less_ssum p p" |
256 qed_goal "refl_less_ssum" thy "less (p::'a++'b) p" |
257 (fn prems => |
257 (fn prems => |
258 [ |
258 [ |
259 (res_inst_tac [("p","p")] IssumE2 1), |
259 (res_inst_tac [("p","p")] IssumE2 1), |
260 (hyp_subst_tac 1), |
260 (hyp_subst_tac 1), |
261 (rtac (less_ssum2a RS iffD2) 1), |
261 (rtac (less_ssum2a RS iffD2) 1), |
263 (hyp_subst_tac 1), |
263 (hyp_subst_tac 1), |
264 (rtac (less_ssum2b RS iffD2) 1), |
264 (rtac (less_ssum2b RS iffD2) 1), |
265 (rtac refl_less 1) |
265 (rtac refl_less 1) |
266 ]); |
266 ]); |
267 |
267 |
268 qed_goal "antisym_less_ssum" Ssum1.thy |
268 qed_goal "antisym_less_ssum" thy |
269 "[|less_ssum p1 p2; less_ssum p2 p1|] ==> p1=p2" |
269 "[|less (p1::'a++'b) p2; less p2 p1|] ==> p1=p2" |
270 (fn prems => |
270 (fn prems => |
271 [ |
271 [ |
272 (cut_facts_tac prems 1), |
272 (cut_facts_tac prems 1), |
273 (res_inst_tac [("p","p1")] IssumE2 1), |
273 (res_inst_tac [("p","p1")] IssumE2 1), |
274 (hyp_subst_tac 1), |
274 (hyp_subst_tac 1), |
293 (rtac antisym_less 1), |
293 (rtac antisym_less 1), |
294 (etac (less_ssum2b RS iffD1) 1), |
294 (etac (less_ssum2b RS iffD1) 1), |
295 (etac (less_ssum2b RS iffD1) 1) |
295 (etac (less_ssum2b RS iffD1) 1) |
296 ]); |
296 ]); |
297 |
297 |
298 qed_goal "trans_less_ssum" Ssum1.thy |
298 qed_goal "trans_less_ssum" thy |
299 "[|less_ssum p1 p2; less_ssum p2 p3|] ==> less_ssum p1 p3" |
299 "[|less (p1::'a++'b) p2; less p2 p3|] ==> less p1 p3" |
300 (fn prems => |
300 (fn prems => |
301 [ |
301 [ |
302 (cut_facts_tac prems 1), |
302 (cut_facts_tac prems 1), |
303 (res_inst_tac [("p","p1")] IssumE2 1), |
303 (res_inst_tac [("p","p1")] IssumE2 1), |
304 (hyp_subst_tac 1), |
304 (hyp_subst_tac 1), |