# HG changeset patch
# User blanchet
# Date 1393847300 -3600
# Node ID 516ab2906e7e421a245737b6bd255f13d8a4b515
# Parent  fa3a1ec69a1bc55be24362f362d70154d23987f0
rationalized internals

diff -r fa3a1ec69a1b -r 516ab2906e7e src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -72,21 +72,21 @@
   val define_iter:
     (typ list list * typ list list list list * term list list * term list list list list) option ->
     (string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context ->
-    (term list * thm list) * Proof.context
+    (term * thm) * Proof.context
   val define_coiter: 'a * term list * term list list
       * ((term list list * term list list list) * typ list) -> (string -> binding) -> 'b list ->
-    typ list -> term list -> term -> Proof.context -> (term list * thm list) * local_theory
+    typ list -> term list -> term -> Proof.context -> (term * thm) * local_theory
   val derive_induct_iters_thms_for_types: BNF_Def.bnf list ->
      ('a * typ list list list list * term list list * 'b) option -> thm -> thm list list ->
      BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list ->
      typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list ->
-     term list list -> thm list list -> Proof.context -> lfp_sugar_thms
+     term list -> thm list -> Proof.context -> lfp_sugar_thms
   val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list ->
     string * term list * term list list * ((term list list * term list list list) * typ list) ->
     thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list ->
     typ list -> typ list list list -> int list list -> int list list -> int list -> thm list ->
-    thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list list ->
-    thm list list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
+    thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list ->
+    thm list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
 
   type co_datatype_spec =
     ((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
@@ -359,9 +359,6 @@
       |> mk_Freess "f" g_Tss
       ||>> mk_Freesss "x" y_Tsss;
 
-    val y_Tssss = map (map (map single)) y_Tsss;
-    val yssss = map (map (map single)) ysss;
-
     val z_Tssss =
       map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_iter_fun_Ts =>
           map2 (map2 unzip_recT)
@@ -481,65 +478,54 @@
     Term.lambda c (mk_IfN absT cps ts)
   end;
 
-fun define_co_iters fp fpT Cs binding_specs lthy0 =
+fun define_co_iter fp fpT Cs b rhs lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
     val maybe_conceal_def_binding = Thm.def_binding
       #> Config.get lthy0 bnf_note_all = false ? Binding.conceal;
 
-    val ((csts, defs), (lthy', lthy)) = lthy0
-      |> apfst split_list o fold_map (fn (b, rhs) =>
-        Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
-        #>> apsnd snd) binding_specs
+    val ((cst, (_, def)), (lthy', lthy)) = lthy0
+      |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
       ||> `Local_Theory.restore;
 
     val phi = Proof_Context.export_morphism lthy lthy';
 
-    val csts' = map (mk_co_iter thy fp fpT Cs o Morphism.term phi) csts;
-    val defs' = map (Morphism.thm phi) defs;
+    val cst' = mk_co_iter thy fp fpT Cs (Morphism.term phi cst);
+    val def' = Morphism.thm phi def;
   in
-    ((csts', defs'), lthy')
+    ((cst', def'), lthy')
   end;
 
-fun define_iter NONE _ _ _ _ _ lthy = (([], []), lthy)
-  | define_iter (SOME (_, _, fss, xssss)) mk_binding fpTs Cs reps ctor_iter lthy =
+fun define_iter NONE _ _ _ _ _ = pair (Term.dummy, refl)
+  | define_iter (SOME (_, _, fss, xssss)) mk_binding fpTs Cs reps ctor_iter =
     let
       val nn = length fpTs;
       val (ctor_iter_absTs, fpT) = strip_typeN nn (fastype_of ctor_iter)
         |>> map domain_type ||> domain_type;
-
-      val binding_spec =
-        (mk_binding recN,
-         fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_iter,
+    in
+      define_co_iter Least_FP fpT Cs (mk_binding recN)
+        (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_iter,
            map4 (fn ctor_iter_absT => fn rep => fn fs => fn xsss =>
                mk_case_absumprod ctor_iter_absT rep fs
                  (map (HOLogic.mk_tuple o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
-             ctor_iter_absTs reps fss xssss)));
-    in
-      define_co_iters Least_FP fpT Cs [binding_spec] lthy
+             ctor_iter_absTs reps fss xssss)))
     end;
 
-fun define_coiter (_, cs, cpss, ((pfss, cqfsss), f_absTs)) mk_binding fpTs Cs abss dtor_coiter lthy =
+fun define_coiter (_, cs, cpss, ((pfss, cqfsss), f_absTs)) mk_binding fpTs Cs abss dtor_coiter =
   let
     val nn = length fpTs;
     val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_coiter)));
-
-    fun generate_coiter dtor_coiter =
-      (mk_binding corecN,
-       fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_coiter,
-         map5 mk_preds_getterss_join cs cpss f_absTs abss cqfsss)));
   in
-    define_co_iters Greatest_FP fpT Cs [generate_coiter dtor_coiter] lthy
+    define_co_iter Greatest_FP fpT Cs (mk_binding corecN)
+      (fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_coiter,
+         map5 mk_preds_getterss_join cs cpss f_absTs abss cqfsss)))
   end;
 
 fun derive_induct_iters_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_iter_thmss
     nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses
-    ctrss ctr_defss iterss iter_defss lthy =
+    ctrss ctr_defss recs rec_defs lthy =
   let
-    val iterss' = transpose iterss;
-    val iter_defss' = transpose iter_defss;
-
     val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
 
     val nn = length pre_bnfs;
@@ -688,8 +674,7 @@
     val rec_thmss =
       (case rec_args_typess of
         SOME types =>
-        mk_iter_thmss types (the_single iterss') (the_single iter_defss')
-          (map co_rec_of ctor_iter_thmss)
+        mk_iter_thmss types recs rec_defs (map co_rec_of ctor_iter_thmss)
       | NONE => replicate nn []);
   in
     ((induct_thms, induct_thm, [induct_case_names_attr]),
@@ -700,7 +685,7 @@
       coiters_args_types as ((phss, cshsss), _))
     dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
     mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
-    coiterss coiter_defss export_args lthy =
+    corecs corec_defs export_args lthy =
   let
     fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter =
       iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
@@ -708,11 +693,6 @@
     val ctor_dtor_coiter_thmss =
       map3 (map oo mk_ctor_dtor_coiter_thm) dtor_injects dtor_ctors dtor_coiter_thmss;
 
-    val coiterss' = transpose coiterss;
-    val coiter_defss' = transpose coiter_defss;
-
-    val [corec_defs] = coiter_defss';
-
     val nn = length pre_bnfs;
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
@@ -826,7 +806,7 @@
     fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
 
     val fcoiterss' as [hcorecs] =
-      map2 (fn (pfss, _) => map (lists_bmoc pfss)) [fst coiters_args_types] coiterss';
+      map2 (fn (pfss, _) => map (lists_bmoc pfss)) [fst coiters_args_types] [corecs];
 
     val corec_thmss =
       let
@@ -1355,18 +1335,18 @@
 
     fun derive_note_induct_iters_thms_for_types
         ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
-          (iterss, iter_defss)), lthy) =
+          (recs, rec_defs)), lthy) =
       let
         val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, iter_attrs)) =
           derive_induct_iters_thms_for_types pre_bnfs iters_args_types xtor_co_induct
             xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses
-            type_definitions abs_inverses ctrss ctr_defss iterss iter_defss lthy;
+            type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
 
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;
 
-        val (recs, rec_thmss') =
-          if iterss = [[]] then (map #casex ctr_sugars, map #case_thms ctr_sugars)
-          else (map the_single iterss, rec_thmss);
+        val (recs', rec_thmss') =
+          if is_some iters_args_types then (recs, rec_thmss)
+          else (map #casex ctr_sugars, map #case_thms ctr_sugars);
 
         val simp_thmss =
           map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injects rel_distincts setss;
@@ -1383,18 +1363,18 @@
       in
         lthy
         |> (if is_some iters_args_types then
-              Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss)
+              Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
             else
               I)
         |> Local_Theory.notes (common_notes @ notes) |> snd
         |> register_fp_sugars Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
-          ctrXs_Tsss ctr_defss ctr_sugars recs mapss [induct_thm] (map single induct_thms)
+          ctrXs_Tsss ctr_defss ctr_sugars recs' mapss [induct_thm] (map single induct_thms)
           rec_thmss' (replicate nn []) (replicate nn [])
       end;
 
     fun derive_note_coinduct_coiters_thms_for_types
         ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
-          (coiterss, coiter_defss)), lthy) =
+          (coiters, corec_defs)), lthy) =
       let
         val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
               coinduct_attrs),
@@ -1404,7 +1384,7 @@
              (sel_corec_thmsss, sel_coiter_attrs)) =
           derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
-            abs_inverses abs_inverses I ctr_defss ctr_sugars coiterss coiter_defss
+            abs_inverses abs_inverses I ctr_defss ctr_sugars coiters corec_defs
             (Proof_Context.export lthy' no_defs_lthy) lthy;
 
         val sel_corec_thmss = map flat sel_corec_thmsss;
@@ -1436,19 +1416,16 @@
            (simpsN, simp_thmss, K []),
            (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)]
           |> massage_multi_notes;
-
-        (* TODO: code theorems *)
-        fun add_spec_rules coiter_of sel_thmss ctr_thmss =
-          fold (curry (Spec_Rules.add Spec_Rules.Equational) (map coiter_of coiterss))
-            [flat sel_thmss, flat ctr_thmss]
       in
         lthy
-        |> add_spec_rules co_rec_of sel_corec_thmss corec_thmss
+        (* TODO: code theorems *)
+        |> fold (curry (Spec_Rules.add Spec_Rules.Equational) coiters)
+          [flat sel_corec_thmss, flat corec_thmss]
         |> Local_Theory.notes (common_notes @ notes) |> snd
         |> register_fp_sugars Xs Greatest_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
-          ctrXs_Tsss ctr_defss ctr_sugars (map the_single coiterss) mapss
-          [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms])
-          corec_thmss disc_corec_thmss sel_corec_thmsss
+          ctrXs_Tsss ctr_defss ctr_sugars coiters mapss [coinduct_thm, strong_coinduct_thm]
+          (transpose [coinduct_thms, strong_coinduct_thms]) corec_thmss disc_corec_thmss
+          sel_corec_thmsss
       end;
 
     val lthy'' = lthy'
diff -r fa3a1ec69a1b -r 516ab2906e7e src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -245,7 +245,7 @@
 
         fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
 
-        val ((co_iterss, co_iter_defss), lthy) =
+        val ((co_recs, co_rec_defs), lthy) =
           fold_map2 (fn b =>
             if fp = Least_FP then define_iter iters_args_types (mk_binding b) fpTs Cs reps
             else define_coiter (the coiters_args_types) (mk_binding b) fpTs Cs abss)
@@ -257,7 +257,7 @@
           if fp = Least_FP then
             derive_induct_iters_thms_for_types pre_bnfs iters_args_types xtor_co_induct
               xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
-              fp_type_definitions abs_inverses ctrss ctr_defss co_iterss co_iter_defss lthy
+              fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs lthy
             |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
               ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
             ||> (fn info => (SOME info, NONE))
@@ -265,7 +265,7 @@
             derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
               dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
               ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
-              ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
+              ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
             |> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _,
                      (sel_corec_thmsss, _)) =>
               (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
@@ -286,8 +286,7 @@
 
         val target_fp_sugars =
           map14 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
-            (map the_single co_iterss) mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss
-            sel_corec_thmsss;
+            co_recs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss sel_corec_thmsss;
 
         val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
       in