# HG changeset patch # User traytel # Date 1394724505 -3600 # Node ID bc7335979247596f012c6a555f2509b01a566fd3 # Parent e3b8f8319d7349d2b227cec93ad86e2c4e65bf1f tuned tactics diff -r e3b8f8319d73 -r bc7335979247 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Mar 13 11:15:04 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Mar 13 16:28:25 2014 +0100 @@ -348,7 +348,7 @@ (HOLogic.mk_Trueprop (mk_tcoalg activeAs ss)) in Goal.prove_sorry lthy [] [] goal - (K (stac coalg_def 1 THEN CONJ_WRAP + (K (rtac (coalg_def RS iffD2) 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac CollectI, CONJ_WRAP' (K (EVERY' [rtac @{thm subset_UNIV}])) allAs] 1)) ss)) |> Thm.close_derivation diff -r e3b8f8319d73 -r bc7335979247 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Mar 13 11:15:04 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Mar 13 16:28:25 2014 +0100 @@ -117,27 +117,29 @@ REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1; fun mk_mor_elim_tac mor_def = - (dtac (subst OF [mor_def]) THEN' + (dtac (mor_def RS iffD1) THEN' REPEAT o etac conjE THEN' TRY o rtac @{thm image_subsetI} THEN' etac bspec THEN' atac) 1; fun mk_mor_incl_tac mor_def map_ids = - (stac mor_def THEN' + (rtac (mor_def RS iffD2) THEN' rtac conjI THEN' - CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_ids THEN' + CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, etac (id_apply RS @{thm ssubst_mem})])) + map_ids THEN' CONJ_WRAP' (fn thm => - (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_ids) 1; + (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_ids) 1; fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids = let - fun fbetw_tac image = EVERY' [rtac ballI, stac o_apply, etac image, etac image, atac]; + fun fbetw_tac image = EVERY' [rtac ballI, rtac (o_apply RS @{thm ssubst_mem}), etac image, + etac image, atac]; fun mor_tac ((mor_image, morE), map_comp_id) = EVERY' [rtac ballI, stac o_apply, rtac trans, rtac (map_comp_id RS sym), rtac trans, etac (morE RS arg_cong), atac, etac morE, etac mor_image, atac]; in - (stac mor_def THEN' rtac conjI THEN' + (rtac (mor_def RS iffD2) THEN' rtac conjI THEN' CONJ_WRAP' fbetw_tac mor_images THEN' CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1 end; @@ -149,16 +151,16 @@ rtac UNIV_I, rtac sym, rtac o_apply]; in EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs, - stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs, + rtac (mor_def RS iffD2), rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs, CONJ_WRAP' (fn i => EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm comp_eq_dest}]) (1 upto n)] 1 end; fun mk_mor_str_tac ks mor_UNIV = - (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac refl)) ks) 1; + (rtac (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac refl)) ks) 1; fun mk_mor_case_sum_tac ks mor_UNIV = - (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm case_sum_o_inj(1)[symmetric]})) ks) 1; + (rtac (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac @{thm case_sum_o_inj(1)[symmetric]})) ks) 1; fun mk_set_incl_hset_tac rec_Suc = EVERY' (map rtac [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym, @@ -262,7 +264,7 @@ end; fun mk_bis_converse_tac m bis_rel rel_congs rel_converseps = - EVERY' [stac bis_rel, dtac (bis_rel RS iffD1), + EVERY' [rtac (bis_rel RS iffD2), dtac (bis_rel RS iffD1), REPEAT_DETERM o etac conjE, rtac conjI, CONJ_WRAP' (K (EVERY' [rtac converse_shift, etac subset_trans, rtac equalityD2, rtac @{thm converse_Times}])) rel_congs, @@ -276,7 +278,7 @@ rtac @{thm conversepI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1; fun mk_bis_O_tac ctxt m bis_rel rel_congs rel_OOs = - EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1), + EVERY' [rtac (bis_rel RS iffD2), REPEAT_DETERM o dtac (bis_rel RS iffD1), REPEAT_DETERM o etac conjE, rtac conjI, CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs, CONJ_WRAP' (fn (rel_cong, rel_OO) => @@ -294,7 +296,7 @@ fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins = unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN EVERY' [rtac conjI, - CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images, + CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS iffD2) THEN' etac thm) mor_images, CONJ_WRAP' (fn (coalg_in, morE) => EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrpI}, etac (morE RS trans), etac @{thm GrD1}, etac (@{thm GrD2} RS arg_cong), etac coalg_in, etac @{thm GrD1}]) @@ -560,7 +562,7 @@ (set_Levs, set_image_Levs))))) => EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], - rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst), + rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS iffD2), rtac exI, rtac conjI, if n = 1 then rtac refl else etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i), @@ -578,7 +580,7 @@ (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~ (set_Levss ~~ set_image_Levss))))), (*root isNode*) - rtac (isNode_def RS ssubst), rtac exI, rtac conjI, + rtac (isNode_def RS iffD2), rtac exI, rtac conjI, CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), if n = 1 then rtac refl else rtac (mk_sum_caseN n i), @@ -622,7 +624,7 @@ rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]}, rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac, - rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI, + rtac trans, rtac @{thm shift_def}, rtac iffD2, rtac @{thm fun_eq_iff}, rtac allI, CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt), if n = 1 then K all_tac @@ -632,7 +634,7 @@ in (rtac mor_cong THEN' EVERY' (map (fn thm => rtac (thm RS @{thm ext})) beh_defs) THEN' - stac mor_def THEN' rtac conjI THEN' + rtac (mor_def RS iffD2) THEN' rtac conjI THEN' CONJ_WRAP' fbetw_tac (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~ (rv_lastss ~~ (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))) THEN' @@ -653,22 +655,22 @@ etac (sym RS arg_cong RS trans), rtac map_comp_id] 1; fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_map0ss coalgT_setss = - EVERY' [stac coalg_def, + EVERY' [rtac (coalg_def RS iffD2), CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) => EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final, rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI, REPEAT_DETERM_N m o EVERY' [rtac conjI, rtac subset_UNIV], CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) => EVERY' [rtac (set_map0 RS ord_eq_le_trans), - rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff}, + rtac @{thm image_subsetI}, rtac iffD2, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set]) (equiv_LSBISs ~~ (drop m set_map0s ~~ coalgT_sets))]) ((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1; fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs = - EVERY' [stac mor_def, rtac conjI, + EVERY' [rtac (mor_def RS iffD2), rtac conjI, CONJ_WRAP' (fn equiv_LSBIS => - EVERY' [rtac ballI, rtac ssubst, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, atac]) + EVERY' [rtac ballI, rtac iffD2, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, atac]) equiv_LSBISs, CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) => EVERY' [rtac ballI, rtac sym, rtac trans, rtac @{thm univ_commute}, rtac equiv_LSBIS, @@ -754,7 +756,7 @@ etac unfold_unique_mor 1; fun mk_dtor_coinduct_tac m raw_coind bis_rel rel_congs = - EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_rel, rtac conjI, + EVERY' [rtac rev_mp, rtac raw_coind, rtac iffD2, rtac bis_rel, rtac conjI, CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) rel_congs, CONJ_WRAP' (fn rel_cong => EVERY' [rtac allI, rtac allI, rtac impI, diff -r e3b8f8319d73 -r bc7335979247 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Mar 13 11:15:04 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Mar 13 16:28:25 2014 +0100 @@ -296,7 +296,7 @@ (HOLogic.mk_Trueprop (mk_talg activeAs ss)) in Goal.prove_sorry lthy [] [] goal - (K (stac alg_def 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss)) + (K (rtac (alg_def RS iffD2) 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss)) |> Thm.close_derivation end; @@ -985,7 +985,7 @@ lthy |> fold_map3 (fn b => fn mx => fn car_init => typedef (Binding.conceal b, params, mx) car_init NONE - (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms, + (EVERY' [rtac iffD2, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms, rtac alg_init_thm] 1)) bs mixfixes car_inits |>> apsnd split_list o split_list; @@ -1005,7 +1005,7 @@ fun mk_inver_thm mk_tac rep abs X thm = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_inver rep abs X)) - (K (EVERY' [rtac ssubst, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1)) + (K (EVERY' [rtac iffD2, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1)) |> Thm.close_derivation; val inver_Reps = map4 (mk_inver_thm rtac) Abs_Ts Rep_Ts (map HOLogic.mk_UNIV Ts) Rep_inverses; diff -r e3b8f8319d73 -r bc7335979247 src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Mar 13 11:15:04 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Mar 13 16:28:25 2014 +0100 @@ -86,7 +86,8 @@ val subset_trans = @{thm subset_trans}; val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]}; val rev_bspec = Drule.rotate_prems 1 bspec; -val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \"]} +val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \"]}; +val relChainD = @{thm iffD2[OF meta_eq_to_obj_eq[OF relChain_def]]}; fun mk_alg_set_tac alg_def = EVERY' [dtac (alg_def RS iffD1), REPEAT_DETERM o etac conjE, etac bspec, rtac CollectI, @@ -102,24 +103,26 @@ etac @{thm emptyE}) 1; fun mk_mor_elim_tac mor_def = - (dtac (subst OF [mor_def]) THEN' + (dtac (mor_def RS iffD1) THEN' REPEAT o etac conjE THEN' TRY o rtac @{thm image_subsetI} THEN' etac bspec THEN' atac) 1; fun mk_mor_incl_tac mor_def map_ids = - (stac mor_def THEN' + (rtac (mor_def RS iffD2) THEN' rtac conjI THEN' - CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_ids THEN' + CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, etac (id_apply RS @{thm ssubst_mem})])) + map_ids THEN' CONJ_WRAP' (fn thm => - (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_ids) 1; + (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_ids) 1; fun mk_mor_comp_tac mor_def set_maps map_comp_ids = let - val fbetw_tac = EVERY' [rtac ballI, stac o_apply, etac bspec, etac bspec, atac]; + val fbetw_tac = + EVERY' [rtac ballI, rtac (o_apply RS @{thm ssubst_mem}), etac bspec, etac bspec, atac]; fun mor_tac (set_map, map_comp_id) = - EVERY' [rtac ballI, stac o_apply, rtac trans, + EVERY' [rtac ballI, rtac (o_apply RS trans), rtac trans, rtac trans, dtac rev_bspec, atac, etac arg_cong, REPEAT o eresolve_tac [CollectE, conjE], etac bspec, rtac CollectI] THEN' CONJ_WRAP' (fn thm => @@ -128,7 +131,7 @@ etac bspec, etac set_mp, atac])]) set_map THEN' rtac (map_comp_id RS arg_cong); in - (dtac (mor_def RS subst) THEN' dtac (mor_def RS subst) THEN' stac mor_def THEN' + (dtac (mor_def RS iffD1) THEN' dtac (mor_def RS iffD1) THEN' rtac (mor_def RS iffD2) THEN' REPEAT o etac conjE THEN' rtac conjI THEN' CONJ_WRAP' (K fbetw_tac) set_maps THEN' @@ -150,9 +153,9 @@ rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map, rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_cong0L RS arg_cong), REPEAT_DETERM_N (length morEs) o - (EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])]; + (EVERY' [rtac iffD1, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])]; in - (stac mor_def THEN' + (rtac (mor_def RS iffD2) THEN' dtac (alg_def RS iffD1) THEN' dtac (alg_def RS iffD1) THEN' REPEAT o etac conjE THEN' @@ -162,12 +165,12 @@ end; fun mk_mor_str_tac ks mor_def = - (stac mor_def THEN' rtac conjI THEN' + (rtac (mor_def RS iffD2) THEN' rtac conjI THEN' CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN' CONJ_WRAP' (K (EVERY' [rtac ballI, rtac refl])) ks) 1; fun mk_mor_convol_tac ks mor_def = - (stac mor_def THEN' rtac conjI THEN' + (rtac (mor_def RS iffD2) THEN' rtac conjI THEN' CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN' CONJ_WRAP' (K (EVERY' [rtac ballI, rtac trans, rtac @{thm fst_convol'}, rtac o_apply])) ks) 1; @@ -179,17 +182,17 @@ rtac sym, rtac o_apply]; in EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs, - stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs, - REPEAT_DETERM o etac conjE, REPEAT_DETERM_N n o dtac (@{thm fun_eq_iff} RS subst), + rtac (mor_def RS iffD2), rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs, + REPEAT_DETERM o etac conjE, REPEAT_DETERM_N n o dtac (@{thm fun_eq_iff} RS iffD1), CONJ_WRAP' (K (EVERY' [rtac ballI, REPEAT_DETERM o etac allE, rtac trans, - etac (o_apply RS subst), rtac o_apply])) morEs] 1 + etac (o_apply RS sym RS trans), rtac o_apply])) morEs] 1 end; fun mk_iso_alt_tac mor_images mor_inv = let val n = length mor_images; fun if_wrap_tac thm = - EVERY' [rtac ssubst, rtac @{thm bij_betw_iff_ex}, rtac exI, rtac conjI, + EVERY' [rtac iffD2, rtac @{thm bij_betw_iff_ex}, rtac exI, rtac conjI, rtac @{thm inver_surj}, etac thm, etac thm, atac, etac conjI, atac] val if_tac = EVERY' [etac thin_rl, etac thin_rl, REPEAT o eresolve_tac [conjE, exE], @@ -222,7 +225,7 @@ (set_maps ~~ alg_sets); in (rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN' - stac alg_def THEN' copy_str_tac) 1 + rtac (alg_def RS iffD2) THEN' copy_str_tac) 1 end; fun mk_copy_alg_tac ctxt set_maps alg_sets mor_def iso_alt copy_str = @@ -240,7 +243,7 @@ (set_maps ~~ alg_sets); in (rtac (iso_alt RS iffD2) THEN' etac copy_str THEN' REPEAT_DETERM o atac THEN' - rtac conjI THEN' stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' + rtac conjI THEN' rtac (mor_def RS iffD2) THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' CONJ_WRAP' (K atac) alg_sets) 1 end; @@ -270,16 +273,16 @@ EVERY' [rtac Un_cong, minG_tac, rtac @{thm image_cong}, rtac thm, REPEAT_DETERM_N (length in_congs) o minG_tac, rtac refl]; in - (rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ssubst THEN' + (rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac iffD2 THEN' rtac meta_eq_to_obj_eq THEN' rtac (worel RS @{thm wo_rel.adm_wo_def}) THEN' REPEAT_DETERM_N 3 o rtac allI THEN' rtac impI THEN' CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1 end; -fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI, - rtac impI, rtac @{thm case_split}, rtac @{thm xt1(3)}, rtac min_algs, etac @{thm FieldI2}, - rtac subsetI, rtac UnI1, rtac @{thm UN_I}, etac @{thm underS_I}, atac, atac, - rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac ctxt, rtac refl] 1; +fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac relChainD, rtac allI, rtac allI, rtac impI, + rtac @{thm case_split}, rtac @{thm xt1(3)}, rtac min_algs, etac @{thm FieldI2}, rtac subsetI, + rtac UnI1, rtac @{thm UN_I}, etac @{thm underS_I}, atac, atac, rtac equalityD1, + dtac @{thm notnotD}, hyp_subst_tac ctxt, rtac refl] 1; fun mk_min_algs_card_of_tac cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite = @@ -370,13 +373,14 @@ end; fun mk_card_of_min_alg_tac min_alg_def card_of suc_Card_order suc_Asuc Asuc_Cinfinite = - EVERY' [stac min_alg_def, rtac @{thm UNION_Cinfinite_bound}, - rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_Field_ordIso}, rtac suc_Card_order, - rtac @{thm ordLess_imp_ordLeq}, rtac suc_Asuc, rtac ballI, dtac rev_mp, rtac card_of, - REPEAT_DETERM o etac conjE, atac, rtac Asuc_Cinfinite] 1; + EVERY' [rtac @{thm ordIso_ordLeq_trans}, rtac (min_alg_def RS @{thm card_of_ordIso_subst}), + rtac @{thm UNION_Cinfinite_bound}, rtac @{thm ordIso_ordLeq_trans}, + rtac @{thm card_of_Field_ordIso}, rtac suc_Card_order, rtac @{thm ordLess_imp_ordLeq}, + rtac suc_Asuc, rtac ballI, dtac rev_mp, rtac card_of, REPEAT_DETERM o etac conjE, atac, + rtac Asuc_Cinfinite] 1; fun mk_least_min_alg_tac min_alg_def least = - EVERY' [stac min_alg_def, rtac @{thm UN_least}, dtac least, dtac mp, atac, + EVERY' [rtac (min_alg_def RS ord_eq_le_trans), rtac @{thm UN_least}, dtac least, dtac mp, atac, REPEAT_DETERM o etac conjE, atac] 1; fun mk_alg_select_tac ctxt Abs_inverse = @@ -393,24 +397,25 @@ CONJ_WRAP' (fn thm => EVERY' [rtac ballI, rtac thm]) str_init_defs; fun alg_epi_tac ((alg_set, str_init_def), set_map) = EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, - rtac ballI, ftac (alg_select RS bspec), stac str_init_def, etac alg_set, - REPEAT_DETERM o EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, rtac subset_trans, - etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]]; + rtac ballI, ftac (alg_select RS bspec), rtac (str_init_def RS @{thm ssubst_mem}), + etac alg_set, REPEAT_DETERM o EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, + rtac subset_trans, etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, + atac]]; in - (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm comp_id}) THEN' - rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN' - stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' rtac mor_incl_min_alg THEN' - stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)) 1 + EVERY' [rtac mor_cong, REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm comp_id}), + rtac (Thm.permute_prems 0 1 mor_comp), etac (Thm.permute_prems 0 1 mor_comp), + rtac (mor_def RS iffD2), rtac conjI, fbetw_tac, mor_tac, rtac mor_incl_min_alg, + rtac (alg_def RS iffD2), CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)] 1 end; fun mk_init_ex_mor_tac ctxt Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs mor_comp mor_select mor_incl_min_alg = let val n = length card_of_min_algs; - val card_of_ordIso_tac = EVERY' [rtac ssubst, rtac @{thm card_of_ordIso}, + val card_of_ordIso_tac = EVERY' [rtac iffD2, rtac @{thm card_of_ordIso}, rtac @{thm ordIso_symmetric}, rtac conjunct1, rtac conjunct2, atac]; - fun internalize_tac card_of = EVERY' [rtac subst, rtac @{thm internalize_card_of_ordLeq2}, - rtac @{thm ordLeq_ordIso_trans}, rtac card_of, rtac subst, + fun internalize_tac card_of = EVERY' [rtac iffD1, rtac @{thm internalize_card_of_ordLeq2}, + rtac @{thm ordLeq_ordIso_trans}, rtac card_of, rtac iffD1, rtac @{thm Card_order_iff_ordIso_card_of}, rtac @{thm Card_order_cexp}]; in (rtac rev_mp THEN' @@ -451,7 +456,7 @@ fun mk_unique_tac (k, least_min_alg) = select_prem_tac n (etac @{thm prop_restrict}) k THEN' rtac least_min_alg THEN' - stac alg_def THEN' + rtac (alg_def RS iffD2) THEN' CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s))); in CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1 @@ -471,7 +476,7 @@ fun mk_induct_tac least_min_alg = rtac ballI THEN' etac @{thm prop_restrict} THEN' rtac least_min_alg THEN' - stac alg_def THEN' + rtac (alg_def RS iffD2) THEN' CONJ_WRAP' mk_alg_tac alg_sets; in CONJ_WRAP' mk_induct_tac least_min_algs 1 @@ -507,8 +512,8 @@ end; fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds = - EVERY' [stac dtor_def, rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac foldx, - rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L, + EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac (dtor_def RS fun_cong RS trans), + rtac trans, rtac foldx, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L, EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) ctor_o_folds), rtac sym, rtac id_apply] 1; @@ -530,18 +535,18 @@ val ks = 1 upto n; fun mk_IH_tac Rep_inv Abs_inv set_map = - DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS subst), etac bspec, + DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS iffD1), etac bspec, dtac set_rev_mp, rtac equalityD1, rtac set_map, etac imageE, - hyp_subst_tac ctxt, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac]; + hyp_subst_tac ctxt, rtac (Abs_inv RS @{thm ssubst_mem}), etac set_mp, atac, atac]; fun mk_closed_tac (k, (morE, set_maps)) = EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI, - rtac (mor_Abs RS morE RS arg_cong RS ssubst), atac, + rtac (mor_Abs RS morE RS arg_cong RS iffD2), atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec}, EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac]; fun mk_induct_tac (Rep, Rep_inv) = - EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RSN (2, bspec))]; + EVERY' [rtac (Rep_inv RS arg_cong RS iffD1), etac (Rep RSN (2, bspec))]; in (rtac mp THEN' rtac impI THEN' DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN'