for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants

--- a/src/HOL/Codatatype/Examples/HFset.thy	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/HFset.thy	Sat Sep 08 21:30:31 2012 +0200
@@ -50,11 +50,11 @@
 
 lemma hfset_fld_rec:
 "hfset_fld_rec R (Fold hs) = R (map_fset <id, hfset_fld_rec R> hs)"
-using hfset.fld_rec unfolding Fold_def .
+using hfset.fld_recs unfolding Fold_def .
 
 (* The iterator has a simpler form: *)
 lemma hfset_fld_iter:
 "hfset_fld_iter R (Fold hs) = R (map_fset (hfset_fld_iter R) hs)"
-using hfset.fld_iter unfolding Fold_def .
+using hfset.fld_iters unfolding Fold_def .
 
 end

--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy	Sat Sep 08 21:30:31 2012 +0200
@@ -177,7 +177,7 @@
 theorem TTree_coit:
 "root (TTree_coit rt ct b) = rt b"
 "ccont (TTree_coit rt ct b) = map_fset (id \<oplus> TTree_coit rt ct) (ct b)"
-using Tree.unf_coiter[of "<rt,ct>" b] unfolding Tree_coit_coit fst_convol snd_convol
+using Tree.unf_coiters[of "<rt,ct>" b] unfolding Tree_coit_coit fst_convol snd_convol
 unfolding pre_Tree_map' fst_convol' snd_convol'
 unfolding Tree_unf_root_ccont by simp_all
 
@@ -194,7 +194,7 @@
 theorem TTree_corec:
 "root (TTree_corec rt ct b) = rt b"
 "ccont (TTree_corec rt ct b) = map_fset (id \<oplus> ([[id, TTree_corec rt ct]]) ) (ct b)"
-using Tree.unf_corec[of "<rt,ct>" b] unfolding Tree_unf_corec_corec fst_convol snd_convol
+using Tree.unf_corecs[of "<rt,ct>" b] unfolding Tree_unf_corec_corec fst_convol snd_convol
 unfolding pre_Tree_map' fst_convol' snd_convol'
 unfolding Tree_unf_root_ccont by simp_all
 

--- a/src/HOL/Codatatype/Examples/Lambda_Term.thy	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy	Sat Sep 08 21:30:31 2012 +0200
@@ -141,21 +141,21 @@
 
 lemma trmrec_Var[simp]:
 "trmrec var app lam lt (Var x) = var x"
-unfolding trmrec_def Var_def trm.fld_rec pre_trm_map(1) by simp
+unfolding trmrec_def Var_def trm.fld_recs pre_trm_map(1) by simp
 
 lemma trmrec_App[simp]:
 "trmrec var app lam lt (App t1 t2) =
  app t1 (trmrec var app lam lt t1) t2 (trmrec var app lam lt t2)"
-unfolding trmrec_def App_def trm.fld_rec pre_trm_map(2) convol_def by simp
+unfolding trmrec_def App_def trm.fld_recs pre_trm_map(2) convol_def by simp
 
 lemma trmrec_Lam[simp]:
 "trmrec var app lam lt (Lam x t) = lam x t (trmrec var app lam lt t)"
-unfolding trmrec_def Lam_def trm.fld_rec pre_trm_map(3) convol_def by simp
+unfolding trmrec_def Lam_def trm.fld_recs pre_trm_map(3) convol_def by simp
 
 lemma trmrec_Lt[simp]:
 "trmrec var app lam lt (Lt xts t) =
  lt (map_fset (\<lambda> (x,t). (x,t,trmrec var app lam lt t)) xts) t (trmrec var app lam lt t)"
-unfolding trmrec_def Lt_def trm.fld_rec pre_trm_map(4) convol_def by simp
+unfolding trmrec_def Lt_def trm.fld_recs pre_trm_map(4) convol_def by simp
 
 definition
 "sumJoinI4 f1 f2 f3 f4 \<equiv>
@@ -178,21 +178,21 @@
 
 lemma trmiter_Var[simp]:
 "trmiter var app lam lt (Var x) = var x"
-unfolding trmiter_def Var_def trm.fld_iter pre_trm_map(1) by simp
+unfolding trmiter_def Var_def trm.fld_iters pre_trm_map(1) by simp
 
 lemma trmiter_App[simp]:
 "trmiter var app lam lt (App t1 t2) =
  app (trmiter var app lam lt t1) (trmiter var app lam lt t2)"
-unfolding trmiter_def App_def trm.fld_iter pre_trm_map(2) by simp
+unfolding trmiter_def App_def trm.fld_iters pre_trm_map(2) by simp
 
 lemma trmiter_Lam[simp]:
 "trmiter var app lam lt (Lam x t) = lam x (trmiter var app lam lt t)"
-unfolding trmiter_def Lam_def trm.fld_iter pre_trm_map(3) by simp
+unfolding trmiter_def Lam_def trm.fld_iters pre_trm_map(3) by simp
 
 lemma trmiter_Lt[simp]:
 "trmiter var app lam lt (Lt xts t) =
  lt (map_fset (\<lambda> (x,t). (x,trmiter var app lam lt t)) xts) (trmiter var app lam lt t)"
-unfolding trmiter_def Lt_def trm.fld_iter pre_trm_map(4) by simp
+unfolding trmiter_def Lt_def trm.fld_iters pre_trm_map(4) by simp
 
 
 subsection{* Example: The set of all variables varsOf and free variables fvarsOf of a term: *}

--- a/src/HOL/Codatatype/Examples/ListF.thy	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/ListF.thy	Sat Sep 08 21:30:31 2012 +0200
@@ -18,27 +18,27 @@
 definition "Conss a as \<equiv> listF_fld (Inr (a, as))"
 
 lemma listF_map_NilF[simp]: "listF_map f NilF = NilF"
-unfolding listF_map_def pre_listF_map_def NilF_def listF.fld_iter by simp
+unfolding listF_map_def pre_listF_map_def NilF_def listF.fld_iters by simp
 
 lemma listF_map_Conss[simp]:
   "listF_map f (Conss x xs) = Conss (f x) (listF_map f xs)"
-unfolding listF_map_def pre_listF_map_def Conss_def listF.fld_iter by simp
+unfolding listF_map_def pre_listF_map_def Conss_def listF.fld_iters by simp
 
 lemma listF_set_NilF[simp]: "listF_set NilF = {}"
-unfolding listF_set_def NilF_def listF.fld_iter pre_listF_set1_def pre_listF_set2_def
+unfolding listF_set_def NilF_def listF.fld_iters pre_listF_set1_def pre_listF_set2_def
   sum_set_defs pre_listF_map_def collect_def[abs_def] by simp
 
 lemma listF_set_Conss[simp]: "listF_set (Conss x xs) = {x} \<union> listF_set xs"
-unfolding listF_set_def Conss_def listF.fld_iter pre_listF_set1_def pre_listF_set2_def
+unfolding listF_set_def Conss_def listF.fld_iters pre_listF_set1_def pre_listF_set2_def
   sum_set_defs prod_set_defs pre_listF_map_def collect_def[abs_def] by simp
 
 lemma iter_sum_case_NilF: "listF_fld_iter (sum_case f g) NilF = f ()"
-unfolding NilF_def listF.fld_iter pre_listF_map_def by simp
+unfolding NilF_def listF.fld_iters pre_listF_map_def by simp
 
 
 lemma iter_sum_case_Conss:
   "listF_fld_iter (sum_case f g) (Conss y ys) = g (y, listF_fld_iter (sum_case f g) ys)"
-unfolding Conss_def listF.fld_iter pre_listF_map_def by simp
+unfolding Conss_def listF.fld_iters pre_listF_map_def by simp
 
 (* familiar induction principle *)
 lemma listF_induct:

--- a/src/HOL/Codatatype/Examples/Process.thy	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Process.thy	Sat Sep 08 21:30:31 2012 +0200
@@ -326,7 +326,7 @@
   let ?f = "pcoiter isA pr co isC c1 c2"  let ?s = "join22 isA pr co isC c1 c2"
   assume isA: "isA P"
   have unf: "process_unf (process_unf_coiter ?s P) = Inl (pr P, ?f (co P))"
-  using process.unf_coiter[of ?s P]
+  using process.unf_coiters[of ?s P]
   unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA]
             pre_process_map id_apply pcoiter_def .
   thus "?f P = Action (pr P) (?f (co P))"
@@ -336,7 +336,7 @@
   let ?f = "pcoiter isA pr co isC c1 c2"  let ?s = "join22 isA pr co isC c1 c2"
   assume isA: "\<not> isA P" and isC: "isC P"
   have unf: "process_unf (process_unf_coiter ?s P) = Inr (?f (c1 P), ?f (c2 P))"
-  using process.unf_coiter[of ?s P]
+  using process.unf_coiters[of ?s P]
   unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC]
             pre_process_map id_apply pcoiter_def .
   thus "?f P = Choice (?f (c1 P)) (?f (c2 P))"
@@ -367,14 +367,14 @@
   proof(cases "co P")
     case (Inl p)
     have "process_unf (process_unf_corec ?s P) = Inl (pr P, p)"
-    using process.unf_corec[of ?s P]
+    using process.unf_corecs[of ?s P]
     unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA]
               pre_process_map id_apply pcorec_def Inl by simp
     thus ?thesis unfolding Inl pcorec_def Action_def using process.fld_unf by (simp, metis)
   next
     case (Inr Q)
     have "process_unf (process_unf_corec ?s P) = Inl (pr P, ?f Q)"
-    using process.unf_corec[of ?s P]
+    using process.unf_corecs[of ?s P]
     unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA]
               pre_process_map id_apply pcorec_def Inr by simp
     thus ?thesis unfolding Inr pcorec_def Action_def using process.fld_unf by (simp, metis)
@@ -405,14 +405,14 @@
     proof(cases "c2 P")
       case (Inl p2)  note c2 = Inl
       have "process_unf (process_unf_corec ?s P) = Inr (p1, p2)"
-      using process.unf_corec[of ?s P]
+      using process.unf_corecs[of ?s P]
       unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC]
                 pre_process_map id_apply pcorec_def c1 c2 by simp
       thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis)
     next
       case (Inr Q2)  note c2 = Inr
       have "process_unf (process_unf_corec ?s P) = Inr (p1, ?f Q2)"
-      using process.unf_corec[of ?s P]
+      using process.unf_corecs[of ?s P]
       unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC]
                 pre_process_map id_apply pcorec_def c1 c2 by simp
       thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis)
@@ -423,14 +423,14 @@
     proof(cases "c2 P")
       case (Inl p2)  note c2 = Inl
       have "process_unf (process_unf_corec ?s P) = Inr (?f Q1, p2)"
-      using process.unf_corec[of ?s P]
+      using process.unf_corecs[of ?s P]
       unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC]
                 pre_process_map id_apply pcorec_def c1 c2 by simp
       thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis)
     next
       case (Inr Q2)  note c2 = Inr
       have "process_unf (process_unf_corec ?s P) = Inr (?f Q1, ?f Q2)"
-      using process.unf_corec[of ?s P]
+      using process.unf_corecs[of ?s P]
       unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC]
                 pre_process_map id_apply pcorec_def c1 c2 by simp
       thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis)

--- a/src/HOL/Codatatype/Examples/Stream.thy	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Stream.thy	Sat Sep 08 21:30:31 2012 +0200
@@ -19,11 +19,11 @@
 definition "tll as \<equiv> snd (stream_unf as)"
 
 lemma coiter_pair_fun_hdd[simp]: "hdd (stream_unf_coiter (f \<odot> g) t) = f t"
-unfolding hdd_def pair_fun_def stream.unf_coiter by simp
+unfolding hdd_def pair_fun_def stream.unf_coiters by simp
 
 lemma coiter_pair_fun_tll[simp]: "tll (stream_unf_coiter (f \<odot> g) t) =
  stream_unf_coiter (f \<odot> g) (g t)"
-unfolding tll_def pair_fun_def stream.unf_coiter by simp
+unfolding tll_def pair_fun_def stream.unf_coiters by simp
 
 (* infinite trees: *)
 coinductive infiniteTr where

--- a/src/HOL/Codatatype/Examples/TreeFI.thy	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFI.thy	Sat Sep 08 21:30:31 2012 +0200
@@ -31,10 +31,10 @@
   "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
 
 lemma coiter_pair_fun_lab: "lab (treeFI_unf_coiter (f \<odot> g) t) = f t"
-unfolding lab_def pair_fun_def treeFI.unf_coiter pre_treeFI_map_def by simp
+unfolding lab_def pair_fun_def treeFI.unf_coiters pre_treeFI_map_def by simp
 
 lemma coiter_pair_fun_sub: "sub (treeFI_unf_coiter (f \<odot> g) t) = listF_map (treeFI_unf_coiter (f \<odot> g)) (g t)"
-unfolding sub_def pair_fun_def treeFI.unf_coiter pre_treeFI_map_def by simp
+unfolding sub_def pair_fun_def treeFI.unf_coiters pre_treeFI_map_def by simp
 
 (* Tree reverse:*)
 definition "trev \<equiv> treeFI_unf_coiter (lab \<odot> lrev o sub)"

--- a/src/HOL/Codatatype/Examples/TreeFsetI.thy	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy	Sat Sep 08 21:30:31 2012 +0200
@@ -27,10 +27,10 @@
 unfolding lab_def sub_def by simp
 
 lemma coiter_pair_fun_lab: "lab (treeFsetI_unf_coiter (f \<odot> g) t) = f t"
-unfolding lab_def pair_fun_def treeFsetI.unf_coiter pre_treeFsetI_map_def by simp
+unfolding lab_def pair_fun_def treeFsetI.unf_coiters pre_treeFsetI_map_def by simp
 
 lemma coiter_pair_fun_sub: "sub (treeFsetI_unf_coiter (f \<odot> g) t) = map_fset (treeFsetI_unf_coiter (f \<odot> g)) (g t)"
-unfolding sub_def pair_fun_def treeFsetI.unf_coiter pre_treeFsetI_map_def by simp
+unfolding sub_def pair_fun_def treeFsetI.unf_coiters pre_treeFsetI_map_def by simp
 
 (* tree map (contrived example): *)
 definition "tmap f \<equiv> treeFsetI_unf_coiter (f o lab \<odot> sub)"

--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:30:31 2012 +0200
@@ -28,7 +28,9 @@
   val fld_inductN: string
   val fld_injectN: string
   val fld_iterN: string
+  val fld_itersN: string
   val fld_recN: string
+  val fld_recsN: string
   val fld_unfN: string
   val hsetN: string
   val hset_recN: string
@@ -59,7 +61,9 @@
   val unf_coinductN: string
   val unf_coinduct_uptoN: string
   val unf_coiterN: string
+  val unf_coitersN: string
   val unf_corecN: string
+  val unf_corecsN: string
   val unf_exhaustN: string
   val unf_fldN: string
   val unf_injectN: string
@@ -146,7 +150,9 @@
 val fldN = "fld"
 val unfN = "unf"
 val fld_iterN = fldN ^ "_" ^ iterN
+val fld_itersN = fld_iterN ^ "s"
 val unf_coiterN = unfN ^ "_" ^ coiterN
+val unf_coitersN = unf_coiterN ^ "s"
 val fld_iter_uniqueN = fld_iterN ^ uniqueN
 val unf_coiter_uniqueN = unf_coiterN ^ uniqueN
 val fld_unf_coiterN = fldN ^ "_" ^ unf_coiterN
@@ -172,7 +178,9 @@
 val recN = "rec"
 val corecN = coN ^ recN
 val fld_recN = fldN ^ "_" ^ recN
+val fld_recsN = fld_recN ^ "s"
 val unf_corecN = unfN ^ "_" ^ corecN
+val unf_corecsN = unf_corecN ^ "s"
 
 val fld_unfN = fldN ^ "_" ^ unfN
 val unf_fldN = unfN ^ "_" ^ fldN

--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:30:31 2012 +0200
@@ -2984,9 +2984,9 @@
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
       val notes =
-        [(unf_coiterN, coiter_thms),
+        [(unf_coitersN, coiter_thms),
         (unf_coiter_uniqueN, coiter_unique_thms),
-        (unf_corecN, corec_thms),
+        (unf_corecsN, corec_thms),
         (unf_fldN, unf_fld_thms),
         (fld_unfN, fld_unf_thms),
         (unf_injectN, unf_inject_thms),

--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sat Sep 08 21:30:31 2012 +0200
@@ -1808,9 +1808,9 @@
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
       val notes =
-        [(fld_iterN, iter_thms),
+        [(fld_itersN, iter_thms),
         (fld_iter_uniqueN, iter_unique_thms),
-        (fld_recN, rec_thms),
+        (fld_recsN, rec_thms),
         (unf_fldN, unf_fld_thms),
         (fld_unfN, fld_unf_thms),
         (unf_injectN, unf_inject_thms),