172 CONJ_WRAP' (K (EVERY' [rtac ballI, rtac trans, rtac @{thm fst_convol'}, rtac o_apply])) ks) 1; |
172 CONJ_WRAP' (K (EVERY' [rtac ballI, rtac trans, rtac @{thm fst_convol'}, rtac o_apply])) ks) 1; |
173 |
173 |
174 fun mk_mor_UNIV_tac m morEs mor_def = |
174 fun mk_mor_UNIV_tac m morEs mor_def = |
175 let |
175 let |
176 val n = length morEs; |
176 val n = length morEs; |
177 fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE, |
177 fun mor_tac morE = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, etac morE, |
178 rtac CollectI, CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto m + n), |
178 rtac CollectI, CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto m + n), |
179 rtac sym, rtac o_apply]; |
179 rtac sym, rtac o_apply]; |
180 in |
180 in |
181 EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs, |
181 EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs, |
182 stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs, |
182 stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs, |
505 in |
505 in |
506 CONJ_WRAP' mk_unique type_defs 1 |
506 CONJ_WRAP' mk_unique type_defs 1 |
507 end; |
507 end; |
508 |
508 |
509 fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds = |
509 fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds = |
510 EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, |
510 EVERY' [stac dtor_def, rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac foldx, |
511 rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L, |
511 rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L, |
512 EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) |
512 EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) |
513 ctor_o_folds), |
513 ctor_o_folds), |
514 rtac sym, rtac id_apply] 1; |
514 rtac sym, rtac id_apply] 1; |
515 |
515 |
566 REPEAT_DETERM o eresolve_tac [conjE, allE], |
566 REPEAT_DETERM o eresolve_tac [conjE, allE], |
567 CONJ_WRAP' (K atac) ks] 1 |
567 CONJ_WRAP' (K atac) ks] 1 |
568 end; |
568 end; |
569 |
569 |
570 fun mk_map_tac m n foldx map_comp_id map_cong0 = |
570 fun mk_map_tac m n foldx map_comp_id map_cong0 = |
571 EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans, rtac o_apply, |
571 EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans, |
|
572 rtac o_apply, |
572 rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong0 RS arg_cong), |
573 rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong0 RS arg_cong), |
573 REPEAT_DETERM_N m o rtac refl, |
574 REPEAT_DETERM_N m o rtac refl, |
574 REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])), |
575 REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])), |
575 rtac sym, rtac o_apply] 1; |
576 rtac sym, rtac o_apply] 1; |
576 |
577 |
577 fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps = |
578 fun mk_ctor_map_unique_tac ctxt fold_unique sym_map_comps = |
578 rtac fold_unique 1 THEN |
579 rtac fold_unique 1 THEN |
579 unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN |
580 unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN |
580 ALLGOALS atac; |
581 ALLGOALS atac; |
581 |
582 |
582 fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply, |
583 fun mk_set_tac foldx = EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, |
583 rtac trans, rtac foldx, rtac sym, rtac o_apply] 1; |
584 rtac trans, rtac foldx, rtac sym, rtac o_apply] 1; |
584 |
585 |
585 fun mk_ctor_set_tac set set_map set_maps = |
586 fun mk_ctor_set_tac set set_map set_maps = |
586 let |
587 let |
587 val n = length set_maps; |
588 val n = length set_maps; |
672 val i = iplus1 - 1; |
673 val i = iplus1 - 1; |
673 val unique' = Thm.permute_prems 0 i unique; |
674 val unique' = Thm.permute_prems 0 i unique; |
674 val map_comp0s' = drop i map_comp0s @ take i map_comp0s; |
675 val map_comp0s' = drop i map_comp0s @ take i map_comp0s; |
675 val ctor_maps' = drop i ctor_maps @ take i ctor_maps; |
676 val ctor_maps' = drop i ctor_maps @ take i ctor_maps; |
676 fun mk_comp comp simp = |
677 fun mk_comp comp simp = |
677 EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply, |
678 EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac o_apply, |
678 rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp, |
679 rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp, |
679 rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply]; |
680 rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply]; |
680 in |
681 in |
681 (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1 |
682 (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1 |
682 end; |
683 end; |
683 |
684 |
684 fun mk_set_map0_tac set_nat = |
685 fun mk_set_map0_tac set_nat = |
685 EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1; |
686 EVERY' (map rtac [@{thm ext}, trans, o_apply, sym, trans, o_apply, set_nat]) 1; |
686 |
687 |
687 fun mk_bd_card_order_tac bd_card_orders = |
688 fun mk_bd_card_order_tac bd_card_orders = |
688 CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders 1; |
689 CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders 1; |
689 |
690 |
690 fun mk_wit_tac ctxt n ctor_set wit = |
691 fun mk_wit_tac ctxt n ctor_set wit = |