renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name

--- 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
@@ -90,11 +90,13 @@
   val unfoldsN: string
   val uniqueN: string
 
+  val mk_ctor_setsN: int -> string
+  val mk_dtor_set_inductN: int -> string
+  val mk_dtor_setsN: int -> string
   val mk_exhaustN: string -> string
   val mk_injectN: string -> string
   val mk_nchotomyN: string -> string
-  val mk_set_simpsN: int -> string
-  val mk_set_minimalN: int -> string
+  val mk_setsN: int -> string
   val mk_set_inductN: int -> string
 
   val mk_common_name: string list -> string
@@ -196,9 +198,11 @@
 val LevN = "Lev"
 val rvN = "recover"
 val behN = "beh"
-fun mk_set_simpsN i = mk_setN i ^ "_" ^ simpsN
-fun mk_set_minimalN i = mk_setN i ^ "_minimal"
+fun mk_setsN i = mk_setN i ^ "s"
+val mk_ctor_setsN = prefix (ctorN ^ "_") o mk_setsN
+val mk_dtor_setsN = prefix (dtorN ^ "_") o mk_setsN
 fun mk_set_inductN i = mk_setN i ^ "_induct"
+val mk_dtor_set_inductN = prefix (dtorN ^ "_") o mk_set_inductN
 
 val str_initN = "str_init"
 val recN = "rec"

--- a/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -70,6 +70,8 @@
   unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN
   unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
 
+(* TODO: Try "map_pair_simp" instead of "map_pair_def" everywhere. *)
+
 val rec_like_unfold_thms =
   @{thms comp_def convol_def id_apply map_pair_def prod_case_Pair_iden sum.simps(5,6) sum_map.simps
       split_conv unit_case_Unity};
@@ -79,7 +81,7 @@
     rec_like_unfold_thms) THEN unfold_thms_tac ctxt @{thms id_def} THEN rtac refl 1;
 
 val corec_like_ss = ss_only @{thms if_True if_False};
-val corec_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
+val corec_like_unfold_thms = @{thms id_apply map_pair_def prod.cases sum_map.simps};
 
 fun mk_corec_like_tac corec_like_defs map_ids ctor_dtor_corec_like pre_map_def ctr_def ctxt =
   unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN

--- 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
@@ -2302,7 +2302,7 @@
         val YTs = mk_Ts passiveYs;
 
         val ((((((((((((((((((((fs, fs'), fs_copy), gs), us),
-          (Jys, Jys')), (Jys_copy, Jys'_copy)), set_induct_phiss), JRs), Jphis),
+          (Jys, Jys')), (Jys_copy, Jys'_copy)), dtor_set_induct_phiss), JRs), Jphis),
           B1s), B2s), AXs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)),
           names_lthy) = names_lthy
           |> mk_Frees' "f" fTs
@@ -2677,7 +2677,7 @@
         val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
 
-        val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, hset_induct_thms) =
+        val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
           let
             fun tinst_of dtor =
               map (SOME o certify lthy) (dtor :: remove (op =) dtor dtors);
@@ -2713,7 +2713,7 @@
                 SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
                   HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
               phis jsets Jzs Jzs';
-            val set_induct_thms =
+            val dtor_set_induct_thms =
               map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
                 ((set_minimal
                   |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y')
@@ -2722,9 +2722,9 @@
                     maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
                 |> singleton (Proof_Context.export names_lthy lthy)
                 |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl)))
-              set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' set_induct_phiss
+              set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' dtor_set_induct_phiss
           in
-            (set_incl_thmss, set_set_incl_thmsss, set_induct_thms)
+            (set_incl_thmss, set_set_incl_thmsss, dtor_set_induct_thms)
           end;
 
         fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit);
@@ -2833,7 +2833,7 @@
               Skip_Proof.prove lthy [] [] goal
                 (mk_coind_wit_tac induct dtor_unfold_thms (flat set_natural'ss) wit_thms)
               |> Thm.close_derivation)
-            goals hset_induct_thms
+            goals dtor_hset_induct_thms
             |> map split_conj_thm
             |> transpose
             |> map (map_filter (try (fn thm => thm RS bspec RS mp)))
@@ -2876,7 +2876,7 @@
 
         val set_incl_thmss = map (map fold_sets) hset_dtor_incl_thmss;
         val set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss;
-        val set_induct_thms = map fold_sets hset_induct_thms;
+        val dtor_set_induct_thms = map fold_sets dtor_hset_induct_thms;
 
         val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
         val Jsrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Jbnfs;
@@ -2905,10 +2905,10 @@
             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 dtor_map => fn set_simps => fn dtor_inject => fn dtor_ctor =>
+              fn dtor_map => fn dtor_sets => 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 dtor_map set_simps
+                (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets
                   dtor_inject dtor_ctor set_naturals set_incls set_set_inclss))
               |> Thm.close_derivation)
             ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_set_simp_thmss'
@@ -2934,7 +2934,7 @@
 
         val Jbnf_common_notes =
           [(map_uniqueN, [fold_maps map_unique_thm])] @
-          map2 (fn i => fn thm => (mk_set_inductN i, [thm])) ls' set_induct_thms
+          map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_set_induct_thms
           |> map (fn (thmN, thms) =>
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
@@ -2944,7 +2944,7 @@
           (dtor_srelN, map single dtor_Jsrel_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
+          map2 (fn i => fn thms => (mk_dtor_setsN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))

--- 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
@@ -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 dtor_map set_simps dtor_inject dtor_ctor
+fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets dtor_inject dtor_ctor
   set_naturals set_incls set_set_inclss =
   let
     val m = length set_incls;
@@ -1538,7 +1538,7 @@
                 dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
                 hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
             (rev (active_set_naturals ~~ in_Jsrels))])
-        (set_simps ~~ passive_set_naturals),
+        (dtor_sets ~~ passive_set_naturals),
         rtac conjI,
         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,

--- 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
@@ -1475,13 +1475,13 @@
                   FTs_setss ctors xFs sets)
                 ls setss_by_range;
 
-            val set_simpss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
+            val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
                 Skip_Proof.prove lthy [] [] goal
                   (K (mk_set_simp_tac set (nth set_nats (i - 1)) (drop m set_nats)))
                 |> Thm.close_derivation)
               set_natural'ss) ls simp_goalss setss;
           in
-            set_simpss
+            ctor_setss
           end;
 
         fun mk_set_thms set_simp = (@{thm xt1(3)} OF [set_simp, @{thm Un_upper1}]) ::
@@ -1522,9 +1522,9 @@
 
             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 =>
+              map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
                 singleton (Proof_Context.export names_lthy lthy)
-                  (Skip_Proof.prove lthy [] [] goal (mk_tac induct csets set_simps i))
+                  (Skip_Proof.prove lthy [] [] goal (mk_tac induct csets ctor_sets i))
                 |> Thm.close_derivation)
               goals csetss set_simp_thmss inducts ls;
           in
@@ -1549,9 +1549,9 @@
 
             fun mk_tac induct = mk_set_bd_tac m (rtac induct) bd_Cinfinite set_bd_cpowss;
             val thms =
-              map4 (fn goal => fn set_simps => fn induct => fn i =>
+              map4 (fn goal => fn ctor_sets => fn induct => fn i =>
                 singleton (Proof_Context.export names_lthy lthy)
-                  (Skip_Proof.prove lthy [] [] goal (mk_tac induct set_simps i))
+                  (Skip_Proof.prove lthy [] [] goal (mk_tac induct ctor_sets i))
                 |> Thm.close_derivation)
               goals set_simp_thmss inducts ls;
           in
@@ -1748,10 +1748,10 @@
             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 ctor_map => fn set_simps => fn ctor_inject => fn ctor_dtor =>
+              fn ctor_map => fn ctor_sets => 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 ctor_map set_simps
+               (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets
                  ctor_inject ctor_dtor set_naturals set_incls set_set_inclss))
               |> Thm.close_derivation)
             ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_set_simp_thmss'
@@ -1786,7 +1786,7 @@
           (ctor_srelN, map single ctor_Isrel_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
+          map2 (fn i => fn thms => (mk_ctor_setsN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))

--- 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,7 +607,7 @@
   end;
 
 fun mk_set_nat_tac m induct_tac set_natural'ss
-    ctor_maps csets set_simps i {context = ctxt, prems = _} =
+    ctor_maps csets ctor_sets i {context = ctxt, prems = _} =
   let
     val n = length ctor_maps;
 
@@ -623,12 +623,12 @@
         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 ctor_maps set_simps set_natural'ss)) 1
+    (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_natural'ss)) 1
   end;
 
-fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss set_simps i {context = ctxt, prems = _} =
+fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i {context = ctxt, prems = _} =
   let
-    val n = length set_simps;
+    val n = length ctor_sets;
 
     fun useIH set_bd = EVERY' [rtac @{thm UNION_Cinfinite_bound}, rtac set_bd, rtac ballI,
       Goal.assume_rule_tac ctxt, rtac bd_Cinfinite];
@@ -639,7 +639,7 @@
         REPEAT_DETERM_N (n - 1) o rtac (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
         EVERY' (map useIH (drop m set_bds))];
   in
-    (induct_tac THEN' EVERY' (map2 mk_set_nat set_simps set_bdss)) 1
+    (induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1
   end;
 
 fun mk_mcong_tac induct_tac set_setsss map_congs ctor_maps {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 ctor_maps set_simpss set_setsss ctor_injects =
+fun mk_lfp_map_wpull_tac m induct_tac wpulls ctor_maps ctor_setss 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 ctor_map set_simps set_setss ctor_inject =
+    fun mk_wpull wpull ctor_map ctor_sets 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),
@@ -715,9 +715,9 @@
         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];
+        CONJ_WRAP' mk_subset ctor_sets];
   in
-    (induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps set_simpss set_setsss ctor_injects)) 1
+    (induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps ctor_setss set_setsss ctor_injects)) 1
   end;
 
 (* BNF tactics *)
@@ -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 ctor_map set_simps ctor_inject
+fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets ctor_inject
   ctor_dtor set_naturals set_incls set_set_inclss =
   let
     val m = length set_incls;
@@ -819,7 +819,7 @@
                 dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
                 hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
             (rev (active_set_naturals ~~ in_Isrels))])
-        (set_simps ~~ passive_set_naturals),
+        (ctor_sets ~~ passive_set_naturals),
         rtac conjI,
         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,