renamed "dtor_coinduct" etc. to "dtor_map_coinduct"

--- a/src/HOL/BNF/Tools/bnf_fp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -44,13 +44,14 @@
   val disc_corec_iffN: string
   val disc_corecsN: string
   val dtorN: string
-  val dtor_coinductN: string
   val dtor_corecN: string
   val dtor_corecsN: string
   val dtor_ctorN: string
   val dtor_exhaustN: string
   val dtor_injectN: string
   val dtor_mapN: string
+  val dtor_map_coinductN: string
+  val dtor_map_strong_coinductN: string
   val dtor_map_uniqueN: string
   val dtor_relN: string
   val dtor_rel_coinductN: string
@@ -60,7 +61,6 @@
   val dtor_srelN: string
   val dtor_srel_coinductN: string
   val dtor_srel_strong_coinductN: string
-  val dtor_strong_coinductN: string
   val dtor_unfoldN: string
   val dtor_unfold_uniqueN: string
   val dtor_unfoldsN: string
@@ -243,11 +243,11 @@
 val coinductN = coN ^ inductN
 val ctor_inductN = ctorN ^ "_" ^ inductN
 val ctor_induct2N = ctor_inductN ^ "2"
-val dtor_coinductN = dtorN ^ "_" ^ coinductN
+val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
 val dtor_rel_coinductN = dtor_relN ^ "_" ^ coinductN
 val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN
 val strongN = "strong_"
-val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN
+val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strongN ^ coinductN
 val dtor_rel_strong_coinductN = dtor_relN ^ "_" ^ strongN ^ coinductN
 val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strongN ^ coinductN
 val hsetN = "Hset"

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -2180,8 +2180,9 @@
 
     val timer = time (timer "corec definitions & thms");
 
-    val (dtor_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_rel_coinduct_thm,
-         dtor_strong_coinduct_thm, dtor_srel_strong_coinduct_thm, dtor_rel_strong_coinduct_thm) =
+    val (dtor_map_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_rel_coinduct_thm,
+         dtor_map_strong_coinduct_thm, dtor_srel_strong_coinduct_thm,
+         dtor_rel_strong_coinduct_thm) =
       let
         val zs = Jzs1 @ Jzs2;
         val frees = phis @ zs;
@@ -2251,9 +2252,9 @@
         val dtor_prems = mk_dtor_prems false;
         val dtor_upto_prems = mk_dtor_prems true;
 
-        val dtor_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (dtor_prems, concl));
-        val dtor_coinduct = Skip_Proof.prove lthy [] [] dtor_coinduct_goal
-          (K (mk_dtor_coinduct_tac m ks raw_coind_thm bis_def))
+        val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (dtor_prems, concl));
+        val dtor_map_coinduct = Skip_Proof.prove lthy [] [] dtor_map_coinduct_goal
+          (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def))
           |> Thm.close_derivation;
 
         val cTs = map (SOME o certifyT lthy o TFree) coinduct_params;
@@ -2265,10 +2266,10 @@
             (K (mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids)))
           |> Thm.close_derivation;
 
-        val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
+        val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] []
             (fold_rev Logic.all zs (Logic.list_implies (dtor_upto_prems, concl)))
-            (K (mk_dtor_strong_coinduct_tac ks cTs cts dtor_coinduct bis_def
+            (K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def
               (tcoalg_thm RS bis_diag_thm))))
           |> Thm.close_derivation;
 
@@ -2278,8 +2279,8 @@
         val dtor_rel_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_coinduct;
         val dtor_rel_strong_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_strong_coinduct;
       in
-        (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), dtor_srel_coinduct,
-         dtor_rel_coinduct, dtor_strong_coinduct, dtor_srel_strong_coinduct,
+        (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_srel_coinduct,
+         dtor_rel_coinduct, dtor_map_strong_coinduct, dtor_srel_strong_coinduct,
          dtor_rel_strong_coinduct)
       end;
 
@@ -2546,7 +2547,7 @@
             val cphis =
               map9 mk_cphi setss_by_bnf Jzs' Jzs fs_maps fs_copy_maps Jys' Jys Jys'_copy Jys_copy;
 
-            val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
+            val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_map_coinduct_thm;
 
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -2965,8 +2966,8 @@
         [(dtor_rel_coinductN, [dtor_rel_coinduct_thm]),
         (dtor_rel_strong_coinductN, [dtor_rel_strong_coinduct_thm])] @
         (if note_all then
-           [(dtor_coinductN, [dtor_coinduct_thm]),
-           (dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
+           [(dtor_map_coinductN, [dtor_map_coinduct_thm]),
+           (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),
            (dtor_srel_coinductN, [dtor_srel_coinduct_thm]),
            (dtor_srel_strong_coinductN, [dtor_srel_strong_coinduct_thm])]
          else
@@ -2992,7 +2993,7 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((dtors, ctors, Jrels, unfolds, corecs, dtor_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
+    ((dtors, ctors, Jrels, unfolds, corecs, dtor_map_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
       ctor_inject_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;

--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -37,14 +37,14 @@
   val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic
   val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
-  val mk_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic
+  val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
+  val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
+    thm -> thm -> tactic
   val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
   val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
     thm list -> thm list -> tactic
   val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
     thm list -> thm list -> thm list list -> tactic
-  val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
-    thm -> thm -> tactic
   val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
@@ -1144,7 +1144,7 @@
     rtac impI, REPEAT_DETERM o etac conjE,
     CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) srel_Ids] 1;
 
-fun mk_dtor_coinduct_tac m ks raw_coind bis_def =
+fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def =
   let
     val n = length ks;
   in
@@ -1165,8 +1165,8 @@
         rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
   end;
 
-fun mk_dtor_strong_coinduct_tac ks cTs cts dtor_coinduct bis_def bis_diag =
-  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_coinduct),
+fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_diag =
+  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct),
     EVERY' (map (fn i =>
       EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp},
         atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,