203 map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc, UnI2, |
203 map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc, UnI2, |
204 mk_UnIN n i] @ |
204 mk_UnIN n i] @ |
205 [etac @{thm UN_I}, atac]) 1; |
205 [etac @{thm UN_I}, atac]) 1; |
206 |
206 |
207 fun mk_set_incl_hin_tac incls = |
207 fun mk_set_incl_hin_tac incls = |
208 if null incls then rtac @{thm subset_UNIV} 1 |
208 if null incls then rtac subset_UNIV 1 |
209 else EVERY' [rtac subsetI, rtac CollectI, |
209 else EVERY' [rtac subsetI, rtac CollectI, |
210 CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1; |
210 CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1; |
211 |
211 |
212 fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} = |
212 fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} = |
213 EVERY' [rtac (Drule.instantiate' [] cts nat_induct), |
213 EVERY' [rtac (Drule.instantiate' [] cts nat_induct), |
532 CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY' |
532 CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY' |
533 [rtac (mk_UnIN n i), dtac (def RS iffD1), |
533 [rtac (mk_UnIN n i), dtac (def RS iffD1), |
534 REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI, |
534 REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI, |
535 REPEAT_DETERM_N m o (rtac conjI THEN' atac), |
535 REPEAT_DETERM_N m o (rtac conjI THEN' atac), |
536 CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans, |
536 CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans, |
537 rtac @{thm subset_UNIV}, rtac equalityD2, rtac @{thm Field_card_order}, |
537 rtac subset_UNIV, rtac equalityD2, rtac @{thm Field_card_order}, |
538 rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs), |
538 rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs), |
539 atac] 1 |
539 atac] 1 |
540 end; |
540 end; |
541 |
541 |
542 fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}= |
542 fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}= |
1152 CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks, |
1152 CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks, |
1153 CONJ_WRAP' (fn i => EVERY' [select_prem_tac n (dtac asm_rl) i, REPEAT_DETERM o rtac allI, |
1153 CONJ_WRAP' (fn i => EVERY' [select_prem_tac n (dtac asm_rl) i, REPEAT_DETERM o rtac allI, |
1154 rtac impI, REPEAT_DETERM o dtac @{thm meta_spec}, etac CollectE, etac @{thm meta_impE}, |
1154 rtac impI, REPEAT_DETERM o dtac @{thm meta_spec}, etac CollectE, etac @{thm meta_impE}, |
1155 atac, etac exE, etac conjE, etac conjE, rtac bexI, rtac conjI, |
1155 atac, etac exE, etac conjE, etac conjE, rtac bexI, rtac conjI, |
1156 etac @{thm fst_conv[THEN subst]}, etac @{thm snd_conv[THEN subst]}, |
1156 etac @{thm fst_conv[THEN subst]}, etac @{thm snd_conv[THEN subst]}, |
1157 rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}), |
1157 rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV), |
1158 CONJ_WRAP' (fn i' => EVERY' [rtac subsetI, rtac CollectI, dtac (mk_conjunctN n i'), |
1158 CONJ_WRAP' (fn i' => EVERY' [rtac subsetI, rtac CollectI, dtac (mk_conjunctN n i'), |
1159 REPEAT_DETERM o etac allE, etac mp, rtac @{thm ssubst_mem[OF pair_collapse]}, atac]) |
1159 REPEAT_DETERM o etac allE, etac mp, rtac @{thm ssubst_mem[OF pair_collapse]}, atac]) |
1160 ks]) |
1160 ks]) |
1161 ks, |
1161 ks, |
1162 rtac impI, |
1162 rtac impI, |
1375 EVERY' (map (etac o mk_conjunctN m) (1 upto m)), |
1375 EVERY' (map (etac o mk_conjunctN m) (1 upto m)), |
1376 pickWP_assms_tac, |
1376 pickWP_assms_tac, |
1377 SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}), rtac impI, |
1377 SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}), rtac impI, |
1378 REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
1378 REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
1379 rtac CollectI, |
1379 rtac CollectI, |
1380 REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}), |
1380 REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV), |
1381 CONJ_WRAP' (fn set_natural => |
1381 CONJ_WRAP' (fn set_natural => |
1382 EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_natural, |
1382 EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_natural, |
1383 rtac trans_fun_cong_image_id_id_apply, atac]) |
1383 rtac trans_fun_cong_image_id_id_apply, atac]) |
1384 (drop m set_naturals)]) |
1384 (drop m set_naturals)]) |
1385 (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1; |
1385 (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1; |