268 EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
268 EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
269 rtac CollectI, |
269 rtac CollectI, |
270 CONJ_WRAP' (fn (i, thm) => |
270 CONJ_WRAP' (fn (i, thm) => |
271 if i <= m |
271 if i <= m |
272 then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans, |
272 then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans, |
273 etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm diagI}] |
273 etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm Id_onI}] |
274 else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm, |
274 else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm, |
275 rtac trans_fun_cong_image_id_id_apply, atac]) |
275 rtac trans_fun_cong_image_id_id_apply, atac]) |
276 (1 upto (m + n) ~~ set_naturals), |
276 (1 upto (m + n) ~~ set_naturals), |
277 rtac trans, rtac trans, rtac map_comp, rtac map_cong, REPEAT_DETERM_N m o rtac thm, |
277 rtac trans, rtac trans, rtac map_comp, rtac map_cong, REPEAT_DETERM_N m o rtac thm, |
278 REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac]) |
278 REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac]) |
293 REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), |
293 REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), |
294 etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong, |
294 etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong, |
295 REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong), |
295 REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong), |
296 REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), |
296 REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), |
297 rtac trans, rtac map_cong, |
297 rtac trans, rtac map_cong, |
298 REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac set_mp, atac], |
298 REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac], |
299 REPEAT_DETERM_N n o rtac refl, |
299 REPEAT_DETERM_N n o rtac refl, |
300 etac sym, rtac CollectI, |
300 etac sym, rtac CollectI, |
301 CONJ_WRAP' (fn (i, thm) => |
301 CONJ_WRAP' (fn (i, thm) => |
302 if i <= m |
302 if i <= m |
303 then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI}, |
303 then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI}, |
304 rtac @{thm diag_fst}, etac set_mp, atac] |
304 rtac @{thm Id_on_fst}, etac set_mp, atac] |
305 else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm, |
305 else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm, |
306 rtac trans_fun_cong_image_id_id_apply, atac]) |
306 rtac trans_fun_cong_image_id_id_apply, atac]) |
307 (1 upto (m + n) ~~ set_naturals)]; |
307 (1 upto (m + n) ~~ set_naturals)]; |
308 in |
308 in |
309 EVERY' [rtac (bis_def RS trans), |
309 EVERY' [rtac (bis_def RS trans), |
317 CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans, |
317 CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans, |
318 rtac equalityD2, rtac @{thm converse_Times}])) srel_congs, |
318 rtac equalityD2, rtac @{thm converse_Times}])) srel_congs, |
319 CONJ_WRAP' (fn (srel_cong, srel_converse) => |
319 CONJ_WRAP' (fn (srel_cong, srel_converse) => |
320 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]}, |
320 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]}, |
321 rtac (srel_cong RS trans), |
321 rtac (srel_cong RS trans), |
322 REPEAT_DETERM_N m o rtac @{thm diag_converse}, |
322 REPEAT_DETERM_N m o rtac (@{thm converse_Id_on} RS sym), |
323 REPEAT_DETERM_N (length srel_congs) o rtac refl, |
323 REPEAT_DETERM_N (length srel_congs) o rtac refl, |
324 rtac srel_converse, |
324 rtac srel_converse, |
325 REPEAT_DETERM o etac allE, |
325 REPEAT_DETERM o etac allE, |
326 rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1; |
326 rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1; |
327 |
327 |
330 REPEAT_DETERM o etac conjE, rtac conjI, |
330 REPEAT_DETERM o etac conjE, rtac conjI, |
331 CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs, |
331 CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs, |
332 CONJ_WRAP' (fn (srel_cong, srel_O) => |
332 CONJ_WRAP' (fn (srel_cong, srel_O) => |
333 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]}, |
333 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]}, |
334 rtac (srel_cong RS trans), |
334 rtac (srel_cong RS trans), |
335 REPEAT_DETERM_N m o rtac @{thm diag_Comp}, |
335 REPEAT_DETERM_N m o rtac @{thm Id_on_Comp}, |
336 REPEAT_DETERM_N (length srel_congs) o rtac refl, |
336 REPEAT_DETERM_N (length srel_congs) o rtac refl, |
337 rtac srel_O, |
337 rtac srel_O, |
338 etac @{thm relcompE}, |
338 etac @{thm relcompE}, |
339 REPEAT_DETERM o dtac Pair_eqD, |
339 REPEAT_DETERM o dtac Pair_eqD, |
340 etac conjE, hyp_subst_tac, |
340 etac conjE, hyp_subst_tac, |
341 REPEAT_DETERM o etac allE, rtac @{thm relcompI}, |
341 REPEAT_DETERM o etac allE, rtac @{thm relcompI}, |
342 etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1; |
342 etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1; |
343 |
343 |
344 fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins |
344 fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins |
345 {context = ctxt, prems = _} = |
345 {context = ctxt, prems = _} = |
346 unfold_thms_tac ctxt (bis_srel :: @{thm diag_Gr} :: srel_Grs) THEN |
346 unfold_thms_tac ctxt (bis_srel :: @{thm Id_on_Gr} :: srel_Grs) THEN |
347 EVERY' [rtac conjI, |
347 EVERY' [rtac conjI, |
348 CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images, |
348 CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images, |
349 CONJ_WRAP' (fn (coalg_in, morE) => |
349 CONJ_WRAP' (fn (coalg_in, morE) => |
350 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrI}, etac coalg_in, |
350 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrI}, etac coalg_in, |
351 etac @{thm GrD1}, etac (morE RS trans), etac @{thm GrD1}, |
351 etac @{thm GrD1}, etac (morE RS trans), etac @{thm GrD1}, |
381 fun mk_incl_lsbis_tac n i lsbis_def = |
381 fun mk_incl_lsbis_tac n i lsbis_def = |
382 EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI, |
382 EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI, |
383 REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2, |
383 REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2, |
384 rtac (mk_nth_conv n i)] 1; |
384 rtac (mk_nth_conv n i)] 1; |
385 |
385 |
386 fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O = |
386 fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O = |
387 EVERY' [rtac (@{thm equiv_def} RS iffD2), |
387 EVERY' [rtac (@{thm equiv_def} RS iffD2), |
388 |
388 |
389 rtac conjI, rtac (@{thm refl_on_def} RS iffD2), |
389 rtac conjI, rtac (@{thm refl_on_def} RS iffD2), |
390 rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp, |
390 rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp, |
391 rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI}, |
391 rtac incl_lsbis, rtac bis_Id_on, atac, etac @{thm Id_onI}, |
392 |
392 |
393 rtac conjI, rtac (@{thm sym_def} RS iffD2), |
393 rtac conjI, rtac (@{thm sym_def} RS iffD2), |
394 rtac allI, rtac allI, rtac impI, rtac set_mp, |
394 rtac allI, rtac allI, rtac impI, rtac set_mp, |
395 rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI}, |
395 rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI}, |
396 |
396 |
1088 rtac @{thm relInvImage_mono}, rtac subset_trans, etac incl_lsbis, |
1088 rtac @{thm relInvImage_mono}, rtac subset_trans, etac incl_lsbis, |
1089 rtac ord_eq_le_trans, rtac @{thm sym[OF relImage_relInvImage]}, |
1089 rtac ord_eq_le_trans, rtac @{thm sym[OF relImage_relInvImage]}, |
1090 rtac @{thm xt1(3)}, rtac @{thm Sigma_cong}, |
1090 rtac @{thm xt1(3)}, rtac @{thm Sigma_cong}, |
1091 rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl, |
1091 rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl, |
1092 rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac, |
1092 rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac, |
1093 rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_diag}, |
1093 rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_Id_on}, |
1094 rtac Rep_inject]) |
1094 rtac Rep_inject]) |
1095 (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1 |
1095 (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1 |
1096 end; |
1096 end; |
1097 |
1097 |
1098 fun mk_unique_mor_tac raw_coinds bis = |
1098 fun mk_unique_mor_tac raw_coinds bis = |
1161 CONJ_WRAP' (fn i => EVERY' [rtac impI, dtac (mk_conjunctN n i), |
1161 CONJ_WRAP' (fn i => EVERY' [rtac impI, dtac (mk_conjunctN n i), |
1162 rtac @{thm subst[OF pair_in_Id_conv]}, etac set_mp, |
1162 rtac @{thm subst[OF pair_in_Id_conv]}, etac set_mp, |
1163 rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1 |
1163 rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1 |
1164 end; |
1164 end; |
1165 |
1165 |
1166 fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_diag = |
1166 fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_Id_on = |
1167 EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct), |
1167 EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct), |
1168 EVERY' (map (fn i => |
1168 EVERY' (map (fn i => |
1169 EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac meta_mp, |
1169 EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac meta_mp, |
1170 atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag, |
1170 atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_Id_on, |
1171 rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE, |
1171 rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE, |
1172 etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE], |
1172 etac impE, etac @{thm Id_on_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE], |
1173 rtac exI, rtac conjI, etac conjI, atac, |
1173 rtac exI, rtac conjI, etac conjI, atac, |
1174 CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], |
1174 CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], |
1175 rtac disjI2, rtac @{thm diagE}, etac set_mp, atac])) ks]) |
1175 rtac disjI2, rtac @{thm Id_onD}, etac set_mp, atac])) ks]) |
1176 ks), |
1176 ks), |
1177 rtac impI, REPEAT_DETERM o etac conjE, |
1177 rtac impI, REPEAT_DETERM o etac conjE, |
1178 CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1; |
1178 CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1; |
1179 |
1179 |
1180 fun mk_map_tac m n cT unfold map_comp' map_cong = |
1180 fun mk_map_tac m n cT unfold map_comp' map_cong = |