# HG changeset patch
# User desharna
# Date 1411735406 -7200
# Node ID 75ee8d49c724ae26e0a0d51a2d2b30898ea520c5
# Parent  a88eb33058f753094cdb673ff20985a96b0d8295
refactor fp_sugar move theorems

diff -r a88eb33058f7 -r 75ee8d49c724 src/HOL/Library/bnf_lfp_countable.ML
--- a/src/HOL/Library/bnf_lfp_countable.ML	Fri Sep 26 14:41:54 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Fri Sep 26 14:43:26 2014 +0200
@@ -150,13 +150,14 @@
           HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0),
             HOLogic.eq_const fpT $ x $ Bound 0));
 
-      val fp_sugars as {fp_nesting_bnfs, common_co_inducts = induct :: _, ...} :: _ =
+      val fp_sugars as
+          {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ =
         map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
       val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
 
       val ctrss0 = map #ctrs ctr_sugars;
       val ns = map length ctrss0;
-      val recs0 = map #co_rec fp_sugars;
+      val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
       val nchotomys = map #nchotomy ctr_sugars;
       val injectss = map #injects ctr_sugars;
       val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
diff -r a88eb33058f7 -r 75ee8d49c724 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 26 14:41:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 26 14:43:26 2014 +0200
@@ -18,7 +18,10 @@
      rel_distincts: thm list}
 
   type fp_co_induct_sugar =
-    {co_inducts: thm list,
+    {co_rec: term,
+     common_co_inducts: thm list,
+     co_inducts: thm list,
+     co_rec_def: thm,
      co_rec_thms: thm list,
      co_rec_discs: thm list,
      co_rec_selss: thm list list}
@@ -34,10 +37,7 @@
      absT_info: BNF_Comp.absT_info,
      fp_nesting_bnfs: BNF_Def.bnf list,
      live_nesting_bnfs: BNF_Def.bnf list,
-     co_rec: term,
-     co_rec_def: thm,
      maps: thm list,
-     common_co_inducts: thm list,
      fp_ctr_sugar: fp_ctr_sugar,
      fp_bnf_sugar: fp_bnf_sugar,
      fp_co_induct_sugar: fp_co_induct_sugar};
@@ -170,7 +170,10 @@
    rel_distincts: thm list}
 
 type fp_co_induct_sugar =
-  {co_inducts: thm list,
+  {co_rec: term,
+   common_co_inducts: thm list,
+   co_inducts: thm list,
+   co_rec_def: thm,
    co_rec_thms: thm list,
    co_rec_discs: thm list,
    co_rec_selss: thm list list}
@@ -186,10 +189,7 @@
    absT_info: absT_info,
    fp_nesting_bnfs: bnf list,
    live_nesting_bnfs: bnf list,
-   co_rec: term,
-   co_rec_def: thm,
    maps: thm list,
-   common_co_inducts: thm list,
    fp_ctr_sugar: fp_ctr_sugar,
    fp_bnf_sugar: fp_bnf_sugar,
    fp_co_induct_sugar: fp_co_induct_sugar};
@@ -198,9 +198,12 @@
   {rel_injects = map (Morphism.thm phi) rel_injects,
    rel_distincts = map (Morphism.thm phi) rel_distincts}
 
-fun morph_fp_co_induct_sugar phi ({co_inducts, co_rec_thms, co_rec_discs,
-    co_rec_selss} : fp_co_induct_sugar) =
-  {co_inducts = map (Morphism.thm phi) co_inducts,
+fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms,
+    co_rec_discs, co_rec_selss} : fp_co_induct_sugar) =
+  {co_rec = Morphism.term phi co_rec,
+   common_co_inducts = map (Morphism.thm phi) common_co_inducts,
+   co_inducts = map (Morphism.thm phi) co_inducts,
+   co_rec_def = Morphism.thm phi co_rec_def,
    co_rec_thms = map (Morphism.thm phi) co_rec_thms,
    co_rec_discs = map (Morphism.thm phi) co_rec_discs,
    co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss}
@@ -211,7 +214,7 @@
    ctr_sugar = morph_ctr_sugar phi ctr_sugar}
 
 fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
-    live_nesting_bnfs, co_rec, co_rec_def, maps, common_co_inducts, fp_ctr_sugar, fp_bnf_sugar,
+    live_nesting_bnfs, maps, fp_ctr_sugar, fp_bnf_sugar,
     fp_co_induct_sugar} : fp_sugar) =
   {T = Morphism.typ phi T,
    BT = Morphism.typ phi BT,
@@ -223,10 +226,7 @@
    absT_info = morph_absT_info phi absT_info,
    fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs,
    live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
-   co_rec = Morphism.term phi co_rec,
-   co_rec_def = Morphism.thm phi co_rec_def,
    maps = map (Morphism.thm phi) maps,
-   common_co_inducts = map (Morphism.thm phi) common_co_inducts,
    fp_ctr_sugar = morph_fp_ctr_sugar phi fp_ctr_sugar,
    fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar,
    fp_co_induct_sugar = morph_fp_co_induct_sugar phi fp_co_induct_sugar};
@@ -288,8 +288,7 @@
         {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
          pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk,
          fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
-         co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk, maps = nth mapss kk,
-         common_co_inducts = common_co_inducts,
+         maps = nth mapss kk,
          fp_ctr_sugar =
            {ctrXs_Tss = nth ctrXs_Tsss kk,
             ctr_defs = nth ctr_defss kk,
@@ -298,7 +297,10 @@
            {rel_injects = nth rel_injectss kk,
             rel_distincts = nth rel_distinctss kk},
          fp_co_induct_sugar =
-           {co_inducts = nth co_inductss kk,
+           {co_rec = nth co_recs kk,
+            common_co_inducts = common_co_inducts,
+            co_inducts = nth co_inductss kk,
+            co_rec_def = nth co_rec_defs kk,
             co_rec_thms = nth co_rec_thmss kk,
             co_rec_discs = nth co_rec_discss kk,
             co_rec_selss = nth co_rec_selsss kk}}
diff -r a88eb33058f7 -r 75ee8d49c724 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Sep 26 14:41:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Sep 26 14:43:26 2014 +0200
@@ -296,8 +296,7 @@
             ({fp_bnf_sugar = {rel_injects, rel_distincts, ...}, ...} : fp_sugar) =
           {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
            pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs,
-           live_nesting_bnfs = live_nesting_bnfs, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
-           common_co_inducts = common_co_inducts,
+           live_nesting_bnfs = live_nesting_bnfs, maps = maps,
            fp_ctr_sugar =
              {ctrXs_Tss = ctrXs_Tss,
               ctr_defs = ctr_defs,
@@ -306,7 +305,10 @@
              {rel_injects = rel_injects,
               rel_distincts = rel_distincts},
            fp_co_induct_sugar =
-             {co_inducts = co_inducts,
+             {co_rec = co_rec,
+              common_co_inducts = common_co_inducts,
+              co_inducts = co_inducts,
+              co_rec_def = co_rec_def, 
               co_rec_thms = co_rec_thms,
               co_rec_discs = co_rec_disc_thms,
               co_rec_selss = co_rec_sel_thmss}}
diff -r a88eb33058f7 -r 75ee8d49c724 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 26 14:41:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 26 14:43:26 2014 +0200
@@ -408,7 +408,8 @@
     val thy = Proof_Context.theory_of lthy0;
 
     val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
-          common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
+          fp_co_induct_sugar = {common_co_inducts = common_coinduct_thms, ...}, ...} :: _,
+          (_, gfp_sugar_thms)), lthy) =
       nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0;
 
     val coinduct_attrs_pair =
@@ -430,7 +431,8 @@
 
     val perm_Ts = map #T perm_fp_sugars;
     val perm_Xs = map #X perm_fp_sugars;
-    val perm_Cs = map (domain_type o body_fun_type o fastype_of o #co_rec) perm_fp_sugars;
+    val perm_Cs =
+      map (domain_type o body_fun_type o fastype_of o #co_rec o #fp_co_induct_sugar) perm_fp_sugars;
     val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
 
     fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
@@ -496,8 +498,8 @@
           distinct_discsss collapses corec_thms corec_discs corec_selss
       end;
 
-    fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...}, co_rec = corec,
-        fp_co_induct_sugar = {co_rec_thms = corec_thms, co_rec_discs = corec_discs,
+    fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...},
+        fp_co_induct_sugar = {co_rec = corec, co_rec_thms = corec_thms, co_rec_discs = corec_discs,
         co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
       {corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, exhaust_discs = exhaust_discs,
        sel_defs = sel_defs,
diff -r a88eb33058f7 -r 75ee8d49c724 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Fri Sep 26 14:41:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Fri Sep 26 14:43:26 2014 +0200
@@ -76,10 +76,7 @@
      absT_info = trivial_absT_info_of fpT,
      fp_nesting_bnfs = [],
      live_nesting_bnfs = [],
-     co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
-     co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]},
      maps = @{thms map_sum.simps},
-     common_co_inducts = @{thms sum.induct},
      fp_ctr_sugar =
        {ctrXs_Tss = ctr_Tss,
         ctr_defs = @{thms Inl_def_alt Inr_def_alt},
@@ -88,7 +85,10 @@
        {rel_injects = @{thms rel_sum_simps(1,4)},
         rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}},
      fp_co_induct_sugar =
-       {co_inducts = @{thms sum.induct},
+       {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
+        common_co_inducts = @{thms sum.induct},
+        co_inducts = @{thms sum.induct},
+        co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]},
         co_rec_thms = @{thms sum.case},
         co_rec_discs = [],
         co_rec_selss = []}}
@@ -120,10 +120,7 @@
      absT_info = trivial_absT_info_of fpT,
      fp_nesting_bnfs = [],
      live_nesting_bnfs = [],
-     co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
-     co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
      maps = @{thms map_prod_simp},
-     common_co_inducts = @{thms prod.induct},
      fp_ctr_sugar =
        {ctrXs_Tss = [ctr_Ts],
         ctr_defs = @{thms Pair_def_alt},
@@ -132,7 +129,10 @@
        {rel_injects = @{thms rel_prod_apply},
         rel_distincts = []},
      fp_co_induct_sugar =
-       {co_inducts = @{thms prod.induct},
+       {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
+        common_co_inducts = @{thms prod.induct},
+        co_inducts = @{thms prod.induct},
+        co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
         co_rec_thms = @{thms prod.case},
         co_rec_discs = [],
         co_rec_selss = []}}
diff -r a88eb33058f7 -r 75ee8d49c724 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Sep 26 14:41:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Sep 26 14:43:26 2014 +0200
@@ -297,9 +297,9 @@
     val Xs' = map #X fp_sugars';
     val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss o #fp_ctr_sugar) fp_sugars';
     val ctrss' = map2 mk_ctr_of fp_sugars' fpTs';
-    val {common_co_inducts = induct :: _, ...} :: _ = fp_sugars';
+    val {fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ = fp_sugars';
     val inducts = map (hd o #co_inducts o #fp_co_induct_sugar) fp_sugars';
-    val recs = map #co_rec fp_sugars';
+    val recs = map (#co_rec o #fp_co_induct_sugar) fp_sugars';
     val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars';
 
     fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) Xs' (body_type T)
diff -r a88eb33058f7 -r 75ee8d49c724 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 26 14:41:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 26 14:43:26 2014 +0200
@@ -24,8 +24,8 @@
   | is_new_datatype ctxt s =
     (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
 
-fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...}, co_rec = recx,
-    fp_co_induct_sugar = {co_rec_thms = rec_thms, ...}, ...} : fp_sugar) =
+fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...},
+    fp_co_induct_sugar = {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) =
   {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
    recx = recx, rec_thms = rec_thms};
 
@@ -34,7 +34,7 @@
   | basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 =
     let
       val ((missing_arg_Ts, perm0_kks,
-            fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
+            fp_sugars as {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _,
             (lfp_sugar_thms, _)), lthy) =
         nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0;
 
@@ -42,7 +42,7 @@
 
       val Ts = map #T fp_sugars;
       val Xs = map #X fp_sugars;
-      val Cs = map (body_type o fastype_of o #co_rec) fp_sugars;
+      val Cs = map (body_type o fastype_of o #co_rec o #fp_co_induct_sugar) fp_sugars;
       val Xs_TCs = Xs ~~ (Ts ~~ Cs);
 
       fun zip_XrecT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_XrecT) Us)]
diff -r a88eb33058f7 -r 75ee8d49c724 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Sep 26 14:41:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Sep 26 14:43:26 2014 +0200
@@ -93,7 +93,7 @@
 
       val B_ify = Term.typ_subst_atomic (As ~~ Bs);
 
-      val recs = map #co_rec fp_sugars;
+      val recs = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
       val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
       val rec_Ts as rec_T1 :: _ = map fastype_of recs;
       val rec_arg_Ts = binder_fun_types rec_T1;
@@ -283,7 +283,7 @@
             val pre_map_defs = map map_def_of_bnf pre_bnfs;
             val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
             val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
-            val rec_defs = map #co_rec_def fp_sugars;
+            val rec_defs = map (#co_rec_def o #fp_co_induct_sugar) fp_sugars;
 
             val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;