renamed "map_simps" to "{c,d}tor_maps"
authorblanchet
Sun Sep 23 14:52:53 2012 +0200 (2012-09-23)
changeset 4954132fb6e4c7f4b
parent 49540 b1bdbb099f99
child 49542 b39354db8629
renamed "map_simps" to "{c,d}tor_maps"
src/HOL/BNF/Tools/bnf_fp.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_gfp_tactics.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_lfp_tactics.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp.ML	Sun Sep 23 14:52:53 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp.ML	Sun Sep 23 14:52:53 2012 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    val ctor_foldN: string
     1.5    val ctor_fold_uniqueN: string
     1.6    val ctor_foldsN: string
     1.7 +  val ctor_mapN: string
     1.8    val ctor_recN: string
     1.9    val ctor_recsN: string
    1.10    val ctor_relN: string
    1.11 @@ -41,6 +42,7 @@
    1.12    val disc_corecsN: string
    1.13    val dtorN: string
    1.14    val dtor_coinductN: string
    1.15 +  val dtor_mapN: string
    1.16    val dtor_relN: string
    1.17    val dtor_corecN: string
    1.18    val dtor_corecsN: string
    1.19 @@ -61,7 +63,6 @@
    1.20    val injectN: string
    1.21    val isNodeN: string
    1.22    val lsbisN: string
    1.23 -  val map_simpsN: string
    1.24    val map_uniqueN: string
    1.25    val min_algN: string
    1.26    val morN: string
    1.27 @@ -180,7 +181,8 @@
    1.28  val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
    1.29  val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
    1.30  val ctor_dtor_unfoldsN = ctorN ^ "_" ^ dtor_unfoldN ^ "s"
    1.31 -val map_simpsN = mapN ^ "_" ^ simpsN
    1.32 +val ctor_mapN = ctorN ^ "_" ^ mapN
    1.33 +val dtor_mapN = dtorN ^ "_" ^ mapN
    1.34  val map_uniqueN = mapN ^ uniqueN
    1.35  val min_algN = "min_alg"
    1.36  val morN = "mor"
     2.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 14:52:53 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 14:52:53 2012 +0200
     2.3 @@ -2366,7 +2366,7 @@
     2.4          val p2id_Fmaps = map (mk_Fmap HOLogic.id_const p2s prodTs) (mk_mapsXB prodTs I);
     2.5          val pid_Fmaps = map (mk_Fmap HOLogic.id_const ps prodTs) (mk_mapsXC prodTs I);
     2.6  
     2.7 -        val (map_simp_thms, map_thms) =
     2.8 +        val (dtor_map_thms, map_thms) =
     2.9            let
    2.10              fun mk_goal fs_map map dtor dtor' = fold_rev Logic.all fs
    2.11                (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_map),
    2.12 @@ -2482,7 +2482,7 @@
    2.13                map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
    2.14                  singleton (Proof_Context.export names_lthy lthy)
    2.15                    (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
    2.16 -                    (mk_col_natural_tac cts rec_0s rec_Sucs map_simp_thms set_natural'ss))
    2.17 +                    (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_natural'ss))
    2.18                  |> Thm.close_derivation)
    2.19                goals ctss hset_rec_0ss' hset_rec_Sucss';
    2.20            in
    2.21 @@ -2550,7 +2550,7 @@
    2.22  
    2.23              val thm = singleton (Proof_Context.export names_lthy lthy)
    2.24                (Skip_Proof.prove lthy [] [] goal
    2.25 -              (K (mk_mcong_tac m (rtac coinduct) map_comp's map_simp_thms map_congs set_natural'ss
    2.26 +              (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_congs set_natural'ss
    2.27                set_hset_thmss set_hset_hset_thmsss)))
    2.28                |> Thm.close_derivation
    2.29            in
    2.30 @@ -2572,7 +2572,7 @@
    2.31            (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s));
    2.32  
    2.33          val map_eq_thms = map2 (fn simp => fn diff => box_equals OF [diff RS iffD2, simp, simp])
    2.34 -          map_simp_thms dtor_inject_thms;
    2.35 +          dtor_map_thms dtor_inject_thms;
    2.36          val map_wpull_thms = map (fn thm => thm OF
    2.37            (replicate m asm_rl @ replicate n @{thm wpull_thePull})) map_wpulls;
    2.38          val pickWP_assms_tacs =
    2.39 @@ -2893,7 +2893,7 @@
    2.40          val Jsrel_defs = map srel_def_of_bnf Jbnfs;
    2.41          val Jrel_defs = map rel_def_of_bnf Jbnfs;
    2.42  
    2.43 -        val folded_map_simp_thms = map fold_maps map_simp_thms;
    2.44 +        val folded_dtor_map_thms = map fold_maps dtor_map_thms;
    2.45          val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
    2.46          val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
    2.47  
    2.48 @@ -2905,13 +2905,13 @@
    2.49              val goals = map6 mk_goal Jzs Jz's dtors dtor's JsrelRs srelRs;
    2.50            in
    2.51              map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
    2.52 -              fn map_simp => fn set_simps => fn dtor_inject => fn dtor_ctor =>
    2.53 +              fn dtor_map => fn set_simps => fn dtor_inject => fn dtor_ctor =>
    2.54                fn set_naturals => fn set_incls => fn set_set_inclss =>
    2.55                Skip_Proof.prove lthy [] [] goal
    2.56 -                (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps
    2.57 +                (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map set_simps
    2.58                    dtor_inject dtor_ctor set_naturals set_incls set_set_inclss))
    2.59                |> Thm.close_derivation)
    2.60 -            ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
    2.61 +            ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_set_simp_thmss'
    2.62                dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
    2.63            end;
    2.64  
    2.65 @@ -2939,9 +2939,9 @@
    2.66              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    2.67  
    2.68          val Jbnf_notes =
    2.69 -          [(dtor_relN, map single dtor_Jrel_thms),
    2.70 +          [(dtor_mapN, map single folded_dtor_map_thms),
    2.71 +          (dtor_relN, map single dtor_Jrel_thms),
    2.72            (dtor_srelN, map single dtor_Jsrel_thms),
    2.73 -          (map_simpsN, map single folded_map_simp_thms),
    2.74            (set_inclN, set_incl_thmss),
    2.75            (set_set_inclN, map flat set_set_incl_thmsss)] @
    2.76            map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     3.3 @@ -1220,7 +1220,7 @@
     3.4          replicate n (@{thm o_id} RS fun_cong))))
     3.5      maps map_comps map_congs)] 1;
     3.6  
     3.7 -fun mk_mcong_tac m coinduct_tac map_comp's map_simps map_congs set_naturalss set_hsetss
     3.8 +fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_congs set_naturalss set_hsetss
     3.9    set_hset_hsetsss =
    3.10    let
    3.11      val n = length map_comp's;
    3.12 @@ -1228,13 +1228,13 @@
    3.13    in
    3.14      EVERY' ([rtac rev_mp,
    3.15        coinduct_tac] @
    3.16 -      maps (fn (((((map_comp'_trans, map_simps_trans), map_cong), set_naturals), set_hsets),
    3.17 +      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong), set_naturals), set_hsets),
    3.18          set_hset_hsetss) =>
    3.19          [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
    3.20 -         rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong,
    3.21 +         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
    3.22           REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm id_apply}),
    3.23           REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
    3.24 -         rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong,
    3.25 +         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
    3.26           EVERY' (maps (fn set_hset =>
    3.27             [rtac o_apply_trans_sym, rtac (@{thm id_apply} RS trans), etac CollectE,
    3.28             REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
    3.29 @@ -1247,7 +1247,7 @@
    3.30               CONJ_WRAP' (fn set_hset_hset =>
    3.31                 EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
    3.32             (drop m set_naturals ~~ set_hset_hsetss)])
    3.33 -        (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) map_simps ~~
    3.34 +        (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~
    3.35            map_congs ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
    3.36        [rtac impI,
    3.37         CONJ_WRAP' (fn k =>
    3.38 @@ -1260,23 +1260,23 @@
    3.39    unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
    3.40    ALLGOALS (etac sym);
    3.41  
    3.42 -fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss
    3.43 +fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_naturalss
    3.44    {context = ctxt, prems = _} =
    3.45    let
    3.46 -    val n = length map_simps;
    3.47 +    val n = length dtor_maps;
    3.48    in
    3.49      EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
    3.50        REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
    3.51        CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
    3.52        REPEAT_DETERM o rtac allI,
    3.53 -      CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY'
    3.54 +      CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY'
    3.55          [SELECT_GOAL (unfold_thms_tac ctxt
    3.56 -          (rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
    3.57 +          (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
    3.58          rtac @{thm Un_cong}, rtac refl,
    3.59          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
    3.60            (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
    3.61              REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
    3.62 -      (rec_Sucs ~~ (map_simps ~~ set_naturalss))] 1
    3.63 +      (rec_Sucs ~~ (dtor_maps ~~ set_naturalss))] 1
    3.64    end;
    3.65  
    3.66  fun mk_set_natural_tac hset_def col_natural =
    3.67 @@ -1494,7 +1494,7 @@
    3.68    ALLGOALS (TRY o
    3.69      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
    3.70  
    3.71 -fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
    3.72 +fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map set_simps dtor_inject dtor_ctor
    3.73    set_naturals set_incls set_set_inclss =
    3.74    let
    3.75      val m = length set_incls;
    3.76 @@ -1519,7 +1519,7 @@
    3.77            EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
    3.78            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
    3.79            REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
    3.80 -          rtac trans, rtac sym, rtac map_simp, rtac (dtor_inject RS iffD2), atac])
    3.81 +          rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
    3.82          @{thms fst_conv snd_conv}];
    3.83      val only_if_tac =
    3.84        EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
    3.85 @@ -1540,7 +1540,7 @@
    3.86              (rev (active_set_naturals ~~ in_Jsrels))])
    3.87          (set_simps ~~ passive_set_naturals),
    3.88          rtac conjI,
    3.89 -        REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac map_simp,
    3.90 +        REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
    3.91            rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
    3.92            rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
    3.93            EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
     4.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 23 14:52:53 2012 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 23 14:52:53 2012 +0200
     4.3 @@ -1394,7 +1394,7 @@
     4.4          val p1s_maps = map (mk_map XTs p1s Ts ctors (mk_passive_maps passiveXs passiveAs)) ks;
     4.5          val p2s_maps = map (mk_map XTs p2s Ts' ctor's (mk_passive_maps passiveXs passiveBs)) ks;
     4.6  
     4.7 -        val map_simp_thms =
     4.8 +        val ctor_map_thms =
     4.9            let
    4.10              fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs
    4.11                (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
    4.12 @@ -1520,7 +1520,7 @@
    4.13                    (map4 (mk_set_natural f) fs_maps Izs sets sets')))
    4.14                    fs setss_by_range setss_by_range';
    4.15  
    4.16 -            fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_natural'ss map_simp_thms;
    4.17 +            fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_natural'ss ctor_map_thms;
    4.18              val thms =
    4.19                map5 (fn goal => fn csets => fn set_simps => fn induct => fn i =>
    4.20                  singleton (Proof_Context.export names_lthy lthy)
    4.21 @@ -1581,7 +1581,7 @@
    4.22  
    4.23              val thm = singleton (Proof_Context.export names_lthy lthy)
    4.24                (Skip_Proof.prove lthy [] [] goal
    4.25 -              (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs map_simp_thms))
    4.26 +              (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs ctor_map_thms))
    4.27                |> Thm.close_derivation;
    4.28            in
    4.29              split_conj_thm thm
    4.30 @@ -1650,7 +1650,7 @@
    4.31  
    4.32              val thm = singleton (Proof_Context.export names_lthy lthy)
    4.33                (Skip_Proof.prove lthy [] [] goal
    4.34 -              (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls map_simp_thms
    4.35 +              (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls ctor_map_thms
    4.36                  (transpose set_simp_thmss) Fset_set_thmsss ctor_inject_thms)))
    4.37                |> Thm.close_derivation;
    4.38            in
    4.39 @@ -1661,7 +1661,7 @@
    4.40  
    4.41          val map_id_tacs = map (K o mk_map_id_tac map_ids) map_unique_thms;
    4.42          val map_comp_tacs =
    4.43 -          map2 (K oo mk_map_comp_tac map_comp's map_simp_thms) map_unique_thms ks;
    4.44 +          map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) map_unique_thms ks;
    4.45          val map_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
    4.46          val set_nat_tacss = map (map (K o mk_set_natural_tac)) (transpose set_natural_thmss);
    4.47          val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
    4.48 @@ -1736,7 +1736,7 @@
    4.49  
    4.50          val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
    4.51          val set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
    4.52 -        val folded_map_simp_thms = map fold_maps map_simp_thms;
    4.53 +        val folded_ctor_map_thms = map fold_maps ctor_map_thms;
    4.54          val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
    4.55          val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
    4.56  
    4.57 @@ -1748,13 +1748,13 @@
    4.58              val goals = map6 mk_goal xFs yFs ctors ctor's IsrelRs srelRs;
    4.59            in
    4.60              map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
    4.61 -              fn map_simp => fn set_simps => fn ctor_inject => fn ctor_dtor =>
    4.62 +              fn ctor_map => fn set_simps => fn ctor_inject => fn ctor_dtor =>
    4.63                fn set_naturals => fn set_incls => fn set_set_inclss =>
    4.64                Skip_Proof.prove lthy [] [] goal
    4.65 -               (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps
    4.66 +               (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map set_simps
    4.67                   ctor_inject ctor_dtor set_naturals set_incls set_set_inclss))
    4.68                |> Thm.close_derivation)
    4.69 -            ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
    4.70 +            ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_set_simp_thmss'
    4.71                ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
    4.72            end;
    4.73  
    4.74 @@ -1781,9 +1781,9 @@
    4.75              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    4.76  
    4.77          val Ibnf_notes =
    4.78 -          [(ctor_relN, map single ctor_Irel_thms),
    4.79 +          [(ctor_mapN, map single folded_ctor_map_thms),
    4.80 +          (ctor_relN, map single ctor_Irel_thms),
    4.81            (ctor_srelN, map single ctor_Isrel_thms),
    4.82 -          (map_simpsN, map single folded_map_simp_thms),
    4.83            (set_inclN, set_incl_thmss),
    4.84            (set_set_inclN, map flat set_set_incl_thmsss)] @
    4.85            map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
     5.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     5.3 @@ -607,23 +607,23 @@
     5.4    end;
     5.5  
     5.6  fun mk_set_nat_tac m induct_tac set_natural'ss
     5.7 -    map_simps csets set_simps i {context = ctxt, prems = _} =
     5.8 +    ctor_maps csets set_simps i {context = ctxt, prems = _} =
     5.9    let
    5.10 -    val n = length map_simps;
    5.11 +    val n = length ctor_maps;
    5.12  
    5.13      fun useIH set_nat = EVERY' [rtac trans, rtac @{thm image_UN}, rtac trans, rtac @{thm UN_cong},
    5.14        rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm UN_cong},
    5.15        rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}];
    5.16  
    5.17 -    fun mk_set_nat cset map_simp set_simp set_nats =
    5.18 +    fun mk_set_nat cset ctor_map set_simp set_nats =
    5.19        EVERY' [rtac trans, rtac @{thm image_cong}, rtac set_simp, rtac refl,
    5.20 -        rtac sym, rtac (trans OF [map_simp RS HOL_arg_cong cset, set_simp RS trans]),
    5.21 +        rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, set_simp RS trans]),
    5.22          rtac sym, EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
    5.23          rtac sym, rtac (nth set_nats (i - 1)),
    5.24          REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
    5.25          EVERY' (map useIH (drop m set_nats))];
    5.26    in
    5.27 -    (induct_tac THEN' EVERY' (map4 mk_set_nat csets map_simps set_simps set_natural'ss)) 1
    5.28 +    (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps set_simps set_natural'ss)) 1
    5.29    end;
    5.30  
    5.31  fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss set_simps i {context = ctxt, prems = _} =
    5.32 @@ -642,7 +642,7 @@
    5.33      (induct_tac THEN' EVERY' (map2 mk_set_nat set_simps set_bdss)) 1
    5.34    end;
    5.35  
    5.36 -fun mk_mcong_tac induct_tac set_setsss map_congs map_simps {context = ctxt, prems = _} =
    5.37 +fun mk_mcong_tac induct_tac set_setsss map_congs ctor_maps {context = ctxt, prems = _} =
    5.38    let
    5.39      fun use_asm thm = EVERY' [etac bspec, etac set_rev_mp, rtac thm];
    5.40  
    5.41 @@ -650,14 +650,14 @@
    5.42        CONJ_WRAP' (fn thm =>
    5.43          EVERY' [rtac ballI, etac bspec, etac set_rev_mp, etac thm]) set_sets];
    5.44  
    5.45 -    fun mk_map_cong map_simp map_cong set_setss =
    5.46 +    fun mk_map_cong ctor_map map_cong set_setss =
    5.47        EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
    5.48 -        rtac trans, rtac map_simp, rtac trans, rtac (map_cong RS arg_cong),
    5.49 +        rtac trans, rtac ctor_map, rtac trans, rtac (map_cong RS arg_cong),
    5.50          EVERY' (map use_asm (map hd set_setss)),
    5.51          EVERY' (map useIH (transpose (map tl set_setss))),
    5.52 -        rtac sym, rtac map_simp];
    5.53 +        rtac sym, rtac ctor_map];
    5.54    in
    5.55 -    (induct_tac THEN' EVERY' (map3 mk_map_cong map_simps map_congs set_setsss)) 1
    5.56 +    (induct_tac THEN' EVERY' (map3 mk_map_cong ctor_maps map_congs set_setsss)) 1
    5.57    end;
    5.58  
    5.59  fun mk_incl_min_alg_tac induct_tac set_setsss alg_sets alg_min_alg {context = ctxt, prems = _} =
    5.60 @@ -676,7 +676,7 @@
    5.61      (induct_tac THEN' EVERY' (map2 mk_incl alg_sets set_setsss)) 1
    5.62    end;
    5.63  
    5.64 -fun mk_lfp_map_wpull_tac m induct_tac wpulls map_simps set_simpss set_setsss ctor_injects =
    5.65 +fun mk_lfp_map_wpull_tac m induct_tac wpulls ctor_maps set_simpss set_setsss ctor_injects =
    5.66    let
    5.67      val n = length wpulls;
    5.68      val ks = 1 upto n;
    5.69 @@ -701,7 +701,7 @@
    5.70          EVERY' [rtac @{thm UN_least}, rtac CollectE, etac set_rev_mp, atac,
    5.71            REPEAT_DETERM o etac conjE, atac]];
    5.72  
    5.73 -    fun mk_wpull wpull map_simp set_simps set_setss ctor_inject =
    5.74 +    fun mk_wpull wpull ctor_map set_simps set_setss ctor_inject =
    5.75        EVERY' [rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
    5.76          rtac rev_mp, rtac wpull,
    5.77          EVERY' (map (fn i => REPEAT_DETERM_N (i - 1) o etac thin_rl THEN' atac) ls),
    5.78 @@ -712,12 +712,12 @@
    5.79            CONJ_WRAP' (K (rtac subset_refl)) ks,
    5.80          rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss),
    5.81            CONJ_WRAP' (K (rtac subset_refl)) ks,
    5.82 -        rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac map_simp,
    5.83 -        rtac trans, atac, rtac map_simp, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE],
    5.84 -        hyp_subst_tac, rtac bexI, rtac conjI, rtac map_simp, rtac map_simp, rtac CollectI,
    5.85 +        rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac ctor_map,
    5.86 +        rtac trans, atac, rtac ctor_map, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE],
    5.87 +        hyp_subst_tac, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI,
    5.88          CONJ_WRAP' mk_subset set_simps];
    5.89    in
    5.90 -    (induct_tac THEN' EVERY' (map5 mk_wpull wpulls map_simps set_simpss set_setsss ctor_injects)) 1
    5.91 +    (induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps set_simpss set_setsss ctor_injects)) 1
    5.92    end;
    5.93  
    5.94  (* BNF tactics *)
    5.95 @@ -728,18 +728,18 @@
    5.96      EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id},
    5.97        rtac (thm RS sym RS arg_cong)]) map_ids)) 1;
    5.98  
    5.99 -fun mk_map_comp_tac map_comps map_simps unique iplus1 =
   5.100 +fun mk_map_comp_tac map_comps ctor_maps unique iplus1 =
   5.101    let
   5.102      val i = iplus1 - 1;
   5.103      val unique' = Thm.permute_prems 0 i unique;
   5.104      val map_comps' = drop i map_comps @ take i map_comps;
   5.105 -    val map_simps' = drop i map_simps @ take i map_simps;
   5.106 +    val ctor_maps' = drop i ctor_maps @ take i ctor_maps;
   5.107      fun mk_comp comp simp =
   5.108        EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
   5.109          rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp,
   5.110          rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply];
   5.111    in
   5.112 -    (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comps' map_simps')) 1
   5.113 +    (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comps' ctor_maps')) 1
   5.114    end;
   5.115  
   5.116  fun mk_set_natural_tac set_nat =
   5.117 @@ -770,7 +770,7 @@
   5.118            EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
   5.119              REPEAT_DETERM_N n o etac UnE]))))] 1);
   5.120  
   5.121 -fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject
   5.122 +fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map set_simps ctor_inject
   5.123    ctor_dtor set_naturals set_incls set_set_inclss =
   5.124    let
   5.125      val m = length set_incls;
   5.126 @@ -800,7 +800,7 @@
   5.127            EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
   5.128            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   5.129            REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
   5.130 -          rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac map_simp,
   5.131 +          rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map,
   5.132            etac eq_arg_cong_ctor_dtor])
   5.133          fst_snd_convs];
   5.134      val only_if_tac =
   5.135 @@ -821,7 +821,7 @@
   5.136              (rev (active_set_naturals ~~ in_Isrels))])
   5.137          (set_simps ~~ passive_set_naturals),
   5.138          rtac conjI,
   5.139 -        REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac map_simp, rtac (ctor_inject RS iffD2),
   5.140 +        REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
   5.141            rtac trans, rtac map_comp, rtac trans, rtac map_cong,
   5.142            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   5.143            EVERY' (map (fn in_Isrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,