# HG changeset patch # User blanchet # Date 1348404773 -7200 # Node ID 32fb6e4c7f4be9cbf955746f759ed2ff7971c547 # Parent b1bdbb099f9909942e3a57fe212ad4b1b474d383 renamed "map_simps" to "{c,d}tor_maps" diff -r b1bdbb099f99 -r 32fb6e4c7f4b src/HOL/BNF/Tools/bnf_fp.ML --- a/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -31,6 +31,7 @@ val ctor_foldN: string val ctor_fold_uniqueN: string val ctor_foldsN: string + val ctor_mapN: string val ctor_recN: string val ctor_recsN: string val ctor_relN: string @@ -41,6 +42,7 @@ val disc_corecsN: string val dtorN: string val dtor_coinductN: string + val dtor_mapN: string val dtor_relN: string val dtor_corecN: string val dtor_corecsN: string @@ -61,7 +63,6 @@ val injectN: string val isNodeN: string val lsbisN: string - val map_simpsN: string val map_uniqueN: string val min_algN: string val morN: string @@ -180,7 +181,8 @@ val ctor_fold_uniqueN = ctor_foldN ^ uniqueN val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN val ctor_dtor_unfoldsN = ctorN ^ "_" ^ dtor_unfoldN ^ "s" -val map_simpsN = mapN ^ "_" ^ simpsN +val ctor_mapN = ctorN ^ "_" ^ mapN +val dtor_mapN = dtorN ^ "_" ^ mapN val map_uniqueN = mapN ^ uniqueN val min_algN = "min_alg" val morN = "mor" diff -r b1bdbb099f99 -r 32fb6e4c7f4b src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -2366,7 +2366,7 @@ val p2id_Fmaps = map (mk_Fmap HOLogic.id_const p2s prodTs) (mk_mapsXB prodTs I); val pid_Fmaps = map (mk_Fmap HOLogic.id_const ps prodTs) (mk_mapsXC prodTs I); - val (map_simp_thms, map_thms) = + val (dtor_map_thms, map_thms) = let fun mk_goal fs_map map dtor dtor' = fold_rev Logic.all fs (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_map), @@ -2482,7 +2482,7 @@ map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs => singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal) - (mk_col_natural_tac cts rec_0s rec_Sucs map_simp_thms set_natural'ss)) + (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_natural'ss)) |> Thm.close_derivation) goals ctss hset_rec_0ss' hset_rec_Sucss'; in @@ -2550,7 +2550,7 @@ val thm = singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal - (K (mk_mcong_tac m (rtac coinduct) map_comp's map_simp_thms map_congs set_natural'ss + (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_congs set_natural'ss set_hset_thmss set_hset_hset_thmsss))) |> Thm.close_derivation in @@ -2572,7 +2572,7 @@ (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s)); val map_eq_thms = map2 (fn simp => fn diff => box_equals OF [diff RS iffD2, simp, simp]) - map_simp_thms dtor_inject_thms; + dtor_map_thms dtor_inject_thms; val map_wpull_thms = map (fn thm => thm OF (replicate m asm_rl @ replicate n @{thm wpull_thePull})) map_wpulls; val pickWP_assms_tacs = @@ -2893,7 +2893,7 @@ val Jsrel_defs = map srel_def_of_bnf Jbnfs; val Jrel_defs = map rel_def_of_bnf Jbnfs; - val folded_map_simp_thms = map fold_maps map_simp_thms; + val folded_dtor_map_thms = map fold_maps dtor_map_thms; val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss; val folded_set_simp_thmss' = transpose folded_set_simp_thmss; @@ -2905,13 +2905,13 @@ val goals = map6 mk_goal Jzs Jz's dtors dtor's JsrelRs srelRs; in map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong => - fn map_simp => fn set_simps => fn dtor_inject => fn dtor_ctor => + fn dtor_map => fn set_simps => fn dtor_inject => fn dtor_ctor => fn set_naturals => fn set_incls => fn set_set_inclss => Skip_Proof.prove lthy [] [] goal - (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps + (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map set_simps dtor_inject dtor_ctor set_naturals set_incls set_set_inclss)) |> Thm.close_derivation) - ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss' + ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_set_simp_thmss' dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss end; @@ -2939,9 +2939,9 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val Jbnf_notes = - [(dtor_relN, map single dtor_Jrel_thms), + [(dtor_mapN, map single folded_dtor_map_thms), + (dtor_relN, map single dtor_Jrel_thms), (dtor_srelN, map single dtor_Jsrel_thms), - (map_simpsN, map single folded_map_simp_thms), (set_inclN, set_incl_thmss), (set_set_inclN, map flat set_set_incl_thmsss)] @ map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss diff -r b1bdbb099f99 -r 32fb6e4c7f4b src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 @@ -1220,7 +1220,7 @@ replicate n (@{thm o_id} RS fun_cong)))) maps map_comps map_congs)] 1; -fun mk_mcong_tac m coinduct_tac map_comp's map_simps map_congs set_naturalss set_hsetss +fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_congs set_naturalss set_hsetss set_hset_hsetsss = let val n = length map_comp's; @@ -1228,13 +1228,13 @@ in EVERY' ([rtac rev_mp, coinduct_tac] @ - maps (fn (((((map_comp'_trans, map_simps_trans), map_cong), set_naturals), set_hsets), + maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong), set_naturals), set_hsets), set_hset_hsetss) => [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI, - rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong, + rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong, REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm id_apply}), REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym, - rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong, + rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong, EVERY' (maps (fn set_hset => [rtac o_apply_trans_sym, rtac (@{thm id_apply} RS trans), etac CollectE, REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets), @@ -1247,7 +1247,7 @@ CONJ_WRAP' (fn set_hset_hset => EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets]) (drop m set_naturals ~~ set_hset_hsetss)]) - (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) map_simps ~~ + (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~ map_congs ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @ [rtac impI, CONJ_WRAP' (fn k => @@ -1260,23 +1260,23 @@ unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN ALLGOALS (etac sym); -fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss +fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_naturalss {context = ctxt, prems = _} = let - val n = length map_simps; + val n = length dtor_maps; in EVERY' [rtac (Drule.instantiate' [] cts nat_induct), REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s), CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s, REPEAT_DETERM o rtac allI, - CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY' + CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY' [SELECT_GOAL (unfold_thms_tac ctxt - (rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})), + (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})), rtac @{thm Un_cong}, rtac refl, CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong})) (fn i => EVERY' [rtac @{thm UN_cong[OF refl]}, REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)]) - (rec_Sucs ~~ (map_simps ~~ set_naturalss))] 1 + (rec_Sucs ~~ (dtor_maps ~~ set_naturalss))] 1 end; fun mk_set_natural_tac hset_def col_natural = @@ -1494,7 +1494,7 @@ ALLGOALS (TRY o FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]) -fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor +fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map set_simps dtor_inject dtor_ctor set_naturals set_incls set_set_inclss = let val m = length set_incls; @@ -1519,7 +1519,7 @@ EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), - rtac trans, rtac sym, rtac map_simp, rtac (dtor_inject RS iffD2), atac]) + rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac]) @{thms fst_conv snd_conv}]; val only_if_tac = EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], @@ -1540,7 +1540,7 @@ (rev (active_set_naturals ~~ in_Jsrels))]) (set_simps ~~ passive_set_naturals), rtac conjI, - REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac map_simp, + REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map, rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans, rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac, diff -r b1bdbb099f99 -r 32fb6e4c7f4b src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -1394,7 +1394,7 @@ val p1s_maps = map (mk_map XTs p1s Ts ctors (mk_passive_maps passiveXs passiveAs)) ks; val p2s_maps = map (mk_map XTs p2s Ts' ctor's (mk_passive_maps passiveXs passiveBs)) ks; - val map_simp_thms = + val ctor_map_thms = let fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor), @@ -1520,7 +1520,7 @@ (map4 (mk_set_natural f) fs_maps Izs sets sets'))) fs setss_by_range setss_by_range'; - fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_natural'ss map_simp_thms; + fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_natural'ss ctor_map_thms; val thms = map5 (fn goal => fn csets => fn set_simps => fn induct => fn i => singleton (Proof_Context.export names_lthy lthy) @@ -1581,7 +1581,7 @@ val thm = singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal - (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs map_simp_thms)) + (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs ctor_map_thms)) |> Thm.close_derivation; in split_conj_thm thm @@ -1650,7 +1650,7 @@ val thm = singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal - (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls map_simp_thms + (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls ctor_map_thms (transpose set_simp_thmss) Fset_set_thmsss ctor_inject_thms))) |> Thm.close_derivation; in @@ -1661,7 +1661,7 @@ val map_id_tacs = map (K o mk_map_id_tac map_ids) map_unique_thms; val map_comp_tacs = - map2 (K oo mk_map_comp_tac map_comp's map_simp_thms) map_unique_thms ks; + map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) map_unique_thms ks; val map_cong_tacs = map (mk_map_cong_tac m) map_cong_thms; val set_nat_tacss = map (map (K o mk_set_natural_tac)) (transpose set_natural_thmss); val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders)); @@ -1736,7 +1736,7 @@ val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss; val set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss; - val folded_map_simp_thms = map fold_maps map_simp_thms; + val folded_ctor_map_thms = map fold_maps ctor_map_thms; val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss; val folded_set_simp_thmss' = transpose folded_set_simp_thmss; @@ -1748,13 +1748,13 @@ val goals = map6 mk_goal xFs yFs ctors ctor's IsrelRs srelRs; in map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong => - fn map_simp => fn set_simps => fn ctor_inject => fn ctor_dtor => + fn ctor_map => fn set_simps => fn ctor_inject => fn ctor_dtor => fn set_naturals => fn set_incls => fn set_set_inclss => Skip_Proof.prove lthy [] [] goal - (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps + (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map set_simps ctor_inject ctor_dtor set_naturals set_incls set_set_inclss)) |> Thm.close_derivation) - ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss' + ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_set_simp_thmss' ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss end; @@ -1781,9 +1781,9 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val Ibnf_notes = - [(ctor_relN, map single ctor_Irel_thms), + [(ctor_mapN, map single folded_ctor_map_thms), + (ctor_relN, map single ctor_Irel_thms), (ctor_srelN, map single ctor_Isrel_thms), - (map_simpsN, map single folded_map_simp_thms), (set_inclN, set_incl_thmss), (set_set_inclN, map flat set_set_incl_thmsss)] @ map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss diff -r b1bdbb099f99 -r 32fb6e4c7f4b src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200 @@ -607,23 +607,23 @@ end; fun mk_set_nat_tac m induct_tac set_natural'ss - map_simps csets set_simps i {context = ctxt, prems = _} = + ctor_maps csets set_simps i {context = ctxt, prems = _} = let - val n = length map_simps; + val n = length ctor_maps; fun useIH set_nat = EVERY' [rtac trans, rtac @{thm image_UN}, rtac trans, rtac @{thm UN_cong}, rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm UN_cong}, rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}]; - fun mk_set_nat cset map_simp set_simp set_nats = + fun mk_set_nat cset ctor_map set_simp set_nats = EVERY' [rtac trans, rtac @{thm image_cong}, rtac set_simp, rtac refl, - rtac sym, rtac (trans OF [map_simp RS HOL_arg_cong cset, set_simp RS trans]), + rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, set_simp RS trans]), rtac sym, EVERY' (map rtac (trans :: @{thms image_Un Un_cong})), rtac sym, rtac (nth set_nats (i - 1)), REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms image_Un Un_cong})), EVERY' (map useIH (drop m set_nats))]; in - (induct_tac THEN' EVERY' (map4 mk_set_nat csets map_simps set_simps set_natural'ss)) 1 + (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps set_simps set_natural'ss)) 1 end; fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss set_simps i {context = ctxt, prems = _} = @@ -642,7 +642,7 @@ (induct_tac THEN' EVERY' (map2 mk_set_nat set_simps set_bdss)) 1 end; -fun mk_mcong_tac induct_tac set_setsss map_congs map_simps {context = ctxt, prems = _} = +fun mk_mcong_tac induct_tac set_setsss map_congs ctor_maps {context = ctxt, prems = _} = let fun use_asm thm = EVERY' [etac bspec, etac set_rev_mp, rtac thm]; @@ -650,14 +650,14 @@ CONJ_WRAP' (fn thm => EVERY' [rtac ballI, etac bspec, etac set_rev_mp, etac thm]) set_sets]; - fun mk_map_cong map_simp map_cong set_setss = + fun mk_map_cong ctor_map map_cong set_setss = EVERY' [rtac impI, REPEAT_DETERM o etac conjE, - rtac trans, rtac map_simp, rtac trans, rtac (map_cong RS arg_cong), + rtac trans, rtac ctor_map, rtac trans, rtac (map_cong RS arg_cong), EVERY' (map use_asm (map hd set_setss)), EVERY' (map useIH (transpose (map tl set_setss))), - rtac sym, rtac map_simp]; + rtac sym, rtac ctor_map]; in - (induct_tac THEN' EVERY' (map3 mk_map_cong map_simps map_congs set_setsss)) 1 + (induct_tac THEN' EVERY' (map3 mk_map_cong ctor_maps map_congs set_setsss)) 1 end; fun mk_incl_min_alg_tac induct_tac set_setsss alg_sets alg_min_alg {context = ctxt, prems = _} = @@ -676,7 +676,7 @@ (induct_tac THEN' EVERY' (map2 mk_incl alg_sets set_setsss)) 1 end; -fun mk_lfp_map_wpull_tac m induct_tac wpulls map_simps set_simpss set_setsss ctor_injects = +fun mk_lfp_map_wpull_tac m induct_tac wpulls ctor_maps set_simpss set_setsss ctor_injects = let val n = length wpulls; val ks = 1 upto n; @@ -701,7 +701,7 @@ EVERY' [rtac @{thm UN_least}, rtac CollectE, etac set_rev_mp, atac, REPEAT_DETERM o etac conjE, atac]]; - fun mk_wpull wpull map_simp set_simps set_setss ctor_inject = + fun mk_wpull wpull ctor_map set_simps set_setss ctor_inject = EVERY' [rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac rev_mp, rtac wpull, EVERY' (map (fn i => REPEAT_DETERM_N (i - 1) o etac thin_rl THEN' atac) ls), @@ -712,12 +712,12 @@ CONJ_WRAP' (K (rtac subset_refl)) ks, rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss), CONJ_WRAP' (K (rtac subset_refl)) ks, - rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac map_simp, - rtac trans, atac, rtac map_simp, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], - hyp_subst_tac, rtac bexI, rtac conjI, rtac map_simp, rtac map_simp, rtac CollectI, + rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac ctor_map, + rtac trans, atac, rtac ctor_map, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], + hyp_subst_tac, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI, CONJ_WRAP' mk_subset set_simps]; in - (induct_tac THEN' EVERY' (map5 mk_wpull wpulls map_simps set_simpss set_setsss ctor_injects)) 1 + (induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps set_simpss set_setsss ctor_injects)) 1 end; (* BNF tactics *) @@ -728,18 +728,18 @@ EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id}, rtac (thm RS sym RS arg_cong)]) map_ids)) 1; -fun mk_map_comp_tac map_comps map_simps unique iplus1 = +fun mk_map_comp_tac map_comps ctor_maps unique iplus1 = let val i = iplus1 - 1; val unique' = Thm.permute_prems 0 i unique; val map_comps' = drop i map_comps @ take i map_comps; - val map_simps' = drop i map_simps @ take i map_simps; + val ctor_maps' = drop i ctor_maps @ take i ctor_maps; fun mk_comp comp simp = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply, rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp, rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply]; in - (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comps' map_simps')) 1 + (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comps' ctor_maps')) 1 end; fun mk_set_natural_tac set_nat = @@ -770,7 +770,7 @@ EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp, REPEAT_DETERM_N n o etac UnE]))))] 1); -fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject +fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map set_simps ctor_inject ctor_dtor set_naturals set_incls set_set_inclss = let val m = length set_incls; @@ -800,7 +800,7 @@ EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), - rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac map_simp, + rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map, etac eq_arg_cong_ctor_dtor]) fst_snd_convs]; val only_if_tac = @@ -821,7 +821,7 @@ (rev (active_set_naturals ~~ in_Isrels))]) (set_simps ~~ passive_set_naturals), rtac conjI, - REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac map_simp, rtac (ctor_inject RS iffD2), + REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2), rtac trans, rtac map_comp, rtac trans, rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, EVERY' (map (fn in_Isrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,