# HG changeset patch
# User blanchet
# Date 1367936121 -7200
# Node ID 126f8d11f87354caae64dfdb2226525585a44327
# Parent  1ab4214a08f993dc040875dcdc90df63a503c301
move function to library

diff -r 1ab4214a08f9 -r 126f8d11f873 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 15:40:00 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 16:15:21 2013 +0200
@@ -27,6 +27,16 @@
   val exists_subtype_in: typ list -> typ -> bool
   val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c
   val mk_fp_iter: bool -> typ list -> typ list -> term list -> term list * typ list
+  val mk_un_fold_co_rec_prelims: bool -> typ list -> typ list -> typ list -> int list ->
+    int list list -> term list -> term list -> Proof.context ->
+    (term list * term list * ((term list list * typ list list * term list list list)
+       * (term list list * typ list list * term 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))
+        * ((term list list * term list list list list * term list list list list)
+           * (typ list * typ list list list * typ list list))) option)
+    * Proof.context
   val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
 
   val mk_iter_fun_arg_types_pairsss: typ list -> int list -> int list list -> term ->
@@ -156,11 +166,6 @@
 val simp_attrs = @{attributes [simp]};
 val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
 
-fun split_list4 [] = ([], [], [], [])
-  | split_list4 ((x1, x2, x3, x4) :: xs) =
-    let val (xs1, xs2, xs3, xs4) = split_list4 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
-
 val exists_subtype_in = Term.exists_subtype o member (op =);
 
 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
@@ -334,6 +339,22 @@
     ((cs, cpss, (unfold_args, unfold_types), (corec_args, corec_types)), lthy)
   end;
 
+fun mk_un_fold_co_rec_prelims lfp fpTs As Cs ns mss fp_folds0 fp_recs0 lthy =
+  let
+    val (fp_folds, fp_fold_fun_Ts) = mk_fp_iter lfp As Cs fp_folds0;
+    val (fp_recs, fp_rec_fun_Ts) = mk_fp_iter lfp As Cs fp_recs0;
+
+    val ((fold_rec_args_types, unfold_corec_args_types), lthy') =
+      if lfp then
+        mk_fold_rec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
+        |>> (rpair NONE o SOME)
+      else
+        mk_unfold_corec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
+        |>> (pair NONE o SOME)
+  in
+    ((fp_folds, fp_recs, fold_rec_args_types, unfold_corec_args_types), lthy')
+  end;
+
 fun mk_map live Ts Us t =
   let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
     Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
@@ -1130,16 +1151,8 @@
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
-    val (fp_folds, fp_fold_fun_Ts) = mk_fp_iter lfp As Cs fp_folds0;
-    val (fp_recs, fp_rec_fun_Ts) = mk_fp_iter lfp As Cs fp_recs0;
-
-    val ((fold_rec_arg_types, unfold_corec_args_types), _) =
-      if lfp then
-        mk_fold_rec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
-        |>> rpair ([], [], (([], [], []), ([], [], [])), (([], [], []), ([], [], [])))
-      else
-        mk_unfold_corec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
-        |>> pair (([], [], []), ([], [], []));
+    val ((fp_folds, fp_recs, fold_rec_args_types, unfold_corec_args_types), lthy) =
+      mk_un_fold_co_rec_prelims lfp fpTs As Cs ns mss fp_folds0 fp_recs0 lthy;
 
     fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
             fp_fold), fp_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
@@ -1331,8 +1344,8 @@
       in
         (wrap_ctrs
          #> derive_maps_sets_rels
-         ##>> (if lfp then define_fold_rec fold_rec_arg_types
-           else define_unfold_corec unfold_corec_args_types)
+         ##>> (if lfp then define_fold_rec (the fold_rec_args_types)
+           else define_unfold_corec (the unfold_corec_args_types))
              mk_binding fpTs As Cs fp_fold fp_rec
          #> massage_res, lthy')
       end;
diff -r 1ab4214a08f9 -r 126f8d11f873 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Tue May 07 15:40:00 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Tue May 07 16:15:21 2013 +0200
@@ -46,6 +46,7 @@
   val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
     'i list -> 'j -> 'k list * 'j
+  val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
   val splice: 'a list -> 'a list -> 'a list
   val transpose: 'a list list -> 'a list list
   val unsort: ('a * 'b -> bool) -> 'b list -> 'c list -> 'a list -> 'c list
@@ -306,6 +307,11 @@
     in (x :: xs, acc'') end
   | fold_map9 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
+fun split_list4 [] = ([], [], [], [])
+  | split_list4 ((x1, x2, x3, x4) :: xs) =
+    let val (xs1, xs2, xs3, xs4) = split_list4 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
+
 (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);