src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Jun 06 11:47:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Jun 06 12:16:35 2013 +0200
@@ -32,11 +32,10 @@
   val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
   val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
   val mk_un_fold_co_rec_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
-    int list list -> term list -> term list -> Proof.context ->
-    (term list * term list
-       * ((typ list list * typ list list list list * term list list * term list list list list)
-          * (typ list list * typ list list list list * term list list
-             * term list list list list)) option
+    int list list -> term list list -> Proof.context ->
+    (term list list
+     * (typ list list * typ list list list list * term list list
+        * term list list list list) list option
      * (term list * term list list
         * ((term list list * term list list list list * term list list list list)
            * (typ list * typ list list list * typ list list))
@@ -49,8 +48,7 @@
   val mk_iter_fun_arg_typessss: typ list -> int list -> int list list -> term ->
     typ list list list list
   val define_fold_rec:
-    (typ list list * typ list list list list * term list list * term list list list list)
-     * (typ list list * typ list list list list * term list list * term list list list list) ->
+    (typ list list * typ list list list list * term list list * term list list list list) list ->
     (string -> binding) -> typ list -> typ list -> term -> term -> Proof.context ->
     (term * term * thm * thm) * Proof.context
   val define_unfold_corec: term list * term list list
@@ -60,10 +58,11 @@
          * (typ list * typ list list list * typ list list)) ->
     (string -> binding) -> typ list -> typ list -> term -> term -> Proof.context ->
     (term * term * thm * thm) * Proof.context
-  val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list list -> thm ->
-    thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list ->
-    typ list list list -> term list list -> thm list list -> term list list -> thm list list ->
-    local_theory ->
+  val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list list ->
+    (typ list list * typ list list list list * term list list * term list list list list) list ->
+    thm -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->
+    typ list -> typ list list list -> term list list -> thm list list -> term list list ->
+    thm list list -> local_theory ->
     (thm * thm list * Args.src list) * (thm list list * Args.src list)
     * (thm list list * Args.src list)
   val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list -> term list -> term list ->
@@ -275,7 +274,7 @@
   #> map3 mk_fun_arg_typess ns mss
   #> map (map (map (unzip_recT Cs)));
 
-fun mk_fold_rec_args_types Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy =
+fun mk_fold_rec_args_types Cs ns mss [ctor_fold_fun_Ts, ctor_rec_fun_Ts] lthy =
   let
     val Css = map2 replicate ns Cs;
     val y_Tsss = map3 mk_fun_arg_typess ns mss ctor_fold_fun_Ts;
@@ -303,10 +302,10 @@
       |> mk_Freessss "y" (map (map (map tl)) z_Tssss);
     val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl;
   in
-    (((g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)), lthy)
+    ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
   end;
 
-fun mk_unfold_corec_args_types Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy =
+fun mk_unfold_corec_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy =
   let
     (*avoid "'a itself" arguments in coiterators and corecursors*)
     fun repair_arity [0] = [1]
@@ -361,7 +360,7 @@
     ((cs, cpss, (unfold_args, unfold_types), (corec_args, corec_types)), lthy)
   end;
 
-fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_un_folds0 xtor_co_recs0 lthy =
+fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss [xtor_un_folds0, xtor_co_recs0] lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
@@ -372,13 +371,13 @@
 
     val ((fold_rec_args_types, unfold_corec_args_types), lthy') =
       if fp = Least_FP then
-        mk_fold_rec_args_types Cs ns mss xtor_un_fold_fun_Ts xtor_co_rec_fun_Ts lthy
+        mk_fold_rec_args_types Cs ns mss [xtor_un_fold_fun_Ts, xtor_co_rec_fun_Ts] lthy
         |>> (rpair NONE o SOME)
       else
-        mk_unfold_corec_args_types Cs ns mss xtor_un_fold_fun_Ts xtor_co_rec_fun_Ts lthy
+        mk_unfold_corec_args_types Cs ns mss [xtor_un_fold_fun_Ts, xtor_co_rec_fun_Ts] lthy
         |>> (pair NONE o SOME)
   in
-    ((xtor_un_folds, xtor_co_recs, fold_rec_args_types, unfold_corec_args_types), lthy')
+    (([xtor_un_folds, xtor_co_recs], fold_rec_args_types, unfold_corec_args_types), lthy')
   end;
 
 fun mk_map live Ts Us t =
@@ -477,7 +476,7 @@
     Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss)
   end;
 
-fun define_fold_rec (fold_only, rec_only) mk_binding fpTs Cs ctor_fold ctor_rec lthy0 =
+fun define_fold_rec [fold_args_types, rec_args_types] mk_binding fpTs Cs ctor_fold ctor_rec lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
@@ -495,7 +494,7 @@
       in (b, spec) end;
 
     val binding_specs =
-      map generate_iter [(foldN, ctor_fold, fold_only), (recN, ctor_rec, rec_only)];
+      map generate_iter [(foldN, ctor_fold, fold_args_types), (recN, ctor_rec, rec_args_types)];
 
     val ((csts, defs), (lthy', lthy)) = lthy0
       |> apfst split_list o fold_map (fn (b, spec) =>
@@ -513,8 +512,8 @@
   end;
 
 (* TODO: merge with above function? *)
-fun define_unfold_corec (cs, cpss, unfold_only, corec_only) mk_binding fpTs Cs dtor_unfold
-    dtor_corec lthy0 =
+fun define_unfold_corec (cs, cpss, unfold_args_types, corec_args_types) mk_binding fpTs Cs
+    dtor_unfold dtor_corec lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
@@ -533,7 +532,8 @@
       in (b, spec) end;
 
     val binding_specs =
-      map generate_coiter [(unfoldN, dtor_unfold, unfold_only), (corecN, dtor_corec, corec_only)];
+      map generate_coiter [(unfoldN, dtor_unfold, unfold_args_types),
+        (corecN, dtor_corec, corec_args_types)];
 
     val ((csts, defs), (lthy', lthy)) = lthy0
       |> apfst split_list o fold_map (fn (b, spec) =>
@@ -550,9 +550,9 @@
     ((unfold, corec, unfold_def, corec_def), lthy')
   end ;
 
-fun derive_induct_fold_rec_thms_for_types pre_bnfs [ctor_folds, ctor_recs] ctor_induct
-    [ctor_fold_thms, ctor_rec_thms] nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
-    [folds, recs] [fold_defs, rec_defs] lthy =
+fun derive_induct_fold_rec_thms_for_types pre_bnfs [ctor_folds, ctor_recs]
+    [fold_args_types, rec_args_types] ctor_induct [ctor_fold_thms, ctor_rec_thms] nesting_bnfs
+    nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss [folds, recs] [fold_defs, rec_defs] lthy =
   let
     val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
 
@@ -571,11 +571,8 @@
     val ctor_fold_fun_Ts = mk_fp_iter_fun_types (hd ctor_folds);
     val ctor_rec_fun_Ts = mk_fp_iter_fun_types (hd ctor_recs);
 
-    val ((fold_only, rec_only), names_lthy0) =
-      mk_fold_rec_args_types Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy;
-
     val ((((ps, ps'), xsss), us'), names_lthy) =
-      names_lthy0
+      lthy
       |> mk_Frees' "P" (map mk_pred1T fpTs)
       ||>> mk_Freesss "x" ctr_Tsss
       ||>> Variable.variant_fixes fp_b_names;
@@ -700,8 +697,8 @@
         map2 (map2 prove) goalss tacss
       end;
 
-    val fold_thmss = mk_iter_thmss fold_only folds fold_defs ctor_fold_thms;
-    val rec_thmss = mk_iter_thmss rec_only recs rec_defs ctor_rec_thms;
+    val fold_thmss = mk_iter_thmss fold_args_types folds fold_defs ctor_fold_thms;
+    val rec_thmss = mk_iter_thmss rec_args_types recs rec_defs ctor_rec_thms;
   in
     ((induct_thm, induct_thms, [induct_case_names_attr]),
      (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
@@ -735,7 +732,7 @@
     val sel_thmsss = map #sel_thmss ctr_sugars;
 
     val ((cs, cpss, ((pgss, crssss, cgssss), _), ((phss, csssss, chssss), _)), names_lthy0) =
-      mk_unfold_corec_args_types Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy;
+      mk_unfold_corec_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy;
 
     val (((rs, us'), vs'), names_lthy) =
       names_lthy0
@@ -1128,8 +1125,8 @@
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
-    val ((xtor_un_folds, xtor_co_recs, fold_rec_args_types, unfold_corec_args_types), lthy) =
-      mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_un_folds0 xtor_co_recs0 lthy;
+    val (([xtor_un_folds, xtor_co_recs], fold_rec_args_types, unfold_corec_args_types), lthy) =
+      mk_un_fold_co_rec_prelims fp fpTs Cs ns mss [xtor_un_folds0, xtor_co_recs0] lthy;
 
     fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
               xtor_un_fold), xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def),
@@ -1347,8 +1344,9 @@
         val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs),
              (rec_thmss, rec_attrs)) =
           derive_induct_fold_rec_thms_for_types pre_bnfs [xtor_un_folds, xtor_co_recs]
-            xtor_co_induct [xtor_un_fold_thms, xtor_co_rec_thms] nesting_bnfs nested_bnfs fpTs Cs Xs
-            ctrXs_Tsss ctrss ctr_defss [folds, recs] [fold_defs, rec_defs] lthy;
+            (the fold_rec_args_types) xtor_co_induct [xtor_un_fold_thms, xtor_co_rec_thms]
+            nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss [folds, recs]
+            [fold_defs, rec_defs] lthy;
 
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;