# HG changeset patch
# User blanchet
# Date 1393955837 -3600
# Node ID 8c6d49dd8ae1902b40cef20f491c51af2f16ecd0
# Parent  21aa30ea680644e240fdbd6c3621806c687a4688
renamed a pair of low-level theorems to have c/dtor in their names (like the others)

diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 04 13:38:02 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 04 18:57:17 2014 +0100
@@ -183,8 +183,6 @@
 fun co_induct_of (i :: _) = i;
 fun strong_co_induct_of [_, s] = s;
 
-(* TODO: register "sum" and "prod" as datatypes to enable N2M reduction for them *)
-
 fun register_fp_sugar key fp_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 04 13:38:02 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 04 18:57:17 2014 +0100
@@ -58,6 +58,7 @@
   val ctor_rec_o_mapN: string
   val ctor_rec_uniqueN: string
   val ctor_relN: string
+  val ctor_rel_inductN: string
   val ctor_set_inclN: string
   val ctor_set_set_inclN: string
   val disc_corecN: string
@@ -75,6 +76,7 @@
   val dtor_map_strong_coinductN: string
   val dtor_map_uniqueN: string
   val dtor_relN: string
+  val dtor_rel_coinductN: string
   val dtor_set_inclN: string
   val dtor_set_set_inclN: string
   val dtor_strong_coinductN: string
@@ -323,7 +325,9 @@
 val injectN = "inject"
 val rel_injectN = relN ^ "_" ^ injectN
 val rel_coinductN = relN ^ "_" ^ coinductN
+val dtor_rel_coinductN = dtorN ^ "_" ^ rel_coinductN
 val rel_inductN = relN ^ "_" ^ inductN
+val ctor_rel_inductN = ctorN ^ "_" ^ rel_inductN
 val selN = "sel"
 val sel_corecN = selN ^ "_" ^ corecN
 
diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Mar 04 13:38:02 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Mar 04 18:57:17 2014 +0100
@@ -2570,7 +2570,7 @@
 
       val common_notes =
         [(dtor_coinductN, [dtor_coinduct_thm]),
-        (rel_coinductN, [Jrel_coinduct_thm]),
+        (dtor_rel_coinductN, [Jrel_coinduct_thm]),
         (dtor_unfold_transferN, dtor_unfold_transfer_thms)]
         |> map (fn (thmN, thms) =>
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Tue Mar 04 13:38:02 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Tue Mar 04 18:57:17 2014 +0100
@@ -1083,7 +1083,7 @@
     (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
   end;
 
-fun mk_unfold_transfer_tac ctxt m rel_coinduct map_transfers unfolds =
+fun mk_unfold_transfer_tac ctxt m ctor_rel_coinduct map_transfers unfolds =
   let
     val n = length map_transfers;
   in
@@ -1091,7 +1091,7 @@
       @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
     unfold_thms_tac ctxt @{thms fun_rel_iff_geq_image2p} THEN
     HEADGOAL (EVERY'
-      [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_coinduct,
+      [REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_coinduct,
       EVERY' (map (fn map_transfer => EVERY'
         [REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
         SELECT_GOAL (unfold_thms_tac ctxt unfolds),
diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 04 13:38:02 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 04 18:57:17 2014 +0100
@@ -1825,8 +1825,8 @@
       val common_notes =
         [(ctor_inductN, [ctor_induct_thm]),
         (ctor_induct2N, [ctor_induct2_thm]),
-        (rel_inductN, [Irel_induct_thm]),
-        (ctor_fold_transferN, ctor_fold_transfer_thms)]
+        (ctor_fold_transferN, ctor_fold_transfer_thms),
+        (ctor_rel_inductN, [Irel_induct_thm])]
         |> map (fn (thmN, thms) =>
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
diff -r 21aa30ea6806 -r 8c6d49dd8ae1 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Mar 04 13:38:02 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Mar 04 18:57:17 2014 +0100
@@ -783,7 +783,7 @@
       IHs ctor_rels rel_mono_strongs)] 1
   end;
 
-fun mk_fold_transfer_tac ctxt m rel_induct map_transfers folds =
+fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds =
   let
     val n = length map_transfers;
   in
@@ -791,7 +791,7 @@
       @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
     unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
     HEADGOAL (EVERY'
-      [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_induct,
+      [REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_induct,
       EVERY' (map (fn map_transfer => EVERY'
         [REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}],
         SELECT_GOAL (unfold_thms_tac ctxt folds),