# HG changeset patch
# User blanchet
# Date 1367488698 -7200
# Node ID 7a08fe1e19b159616e8ee29314d428fdbfdc9a35
# Parent  17e7f00563fbc70930c5dc4dd1471132426387a9
added and moved library functions (used in primrec code)

diff -r 17e7f00563fb -r 7a08fe1e19b1 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 11:19:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 11:58:18 2013 +0200
@@ -141,12 +141,6 @@
     let val (xs1, xs2, xs3, xs4) = split_list4 xs;
     in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
 
-fun add_components_of_typ (Type (s, Ts)) =
-    fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
-  | add_components_of_typ _ = I;
-
-fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
-
 fun exists_subtype_in Ts = exists_subtype (member (op =) Ts);
 
 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
@@ -157,13 +151,6 @@
     | SOME T' => T')
   | typ_subst_nonatomic inst T = the_default T (AList.lookup (op =) inst T);
 
-fun variant_types ss Ss ctxt =
-  let
-    val (tfrees, _) =
-      fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
-    val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
-  in (tfrees, ctxt') end;
-
 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
 
 fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
@@ -848,8 +835,7 @@
       |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
       |> mk_TFrees (length unsorted_As)
       ||>> mk_TFrees nn
-      ||>> apfst (map TFree) o
-        variant_types (map (prefix "'") fp_b_names) (replicate nn HOLogic.typeS);
+      ||>> variant_tfrees fp_b_names;
 
     (* TODO: cleaner handling of fake contexts, without "background_theory" *)
     (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
diff -r 17e7f00563fb -r 7a08fe1e19b1 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 11:19:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 11:58:18 2013 +0200
@@ -120,8 +120,13 @@
   val mk_dtor_set_inductN: int -> string
   val mk_set_inductN: int -> string
 
+  val base_name_of_typ: typ -> string
   val mk_common_name: string list -> string
 
+  val variant_types: string list -> sort list -> Proof.context ->
+    (string * sort) list * Proof.context
+  val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
+
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
@@ -156,6 +161,7 @@
   val mk_sum_casesN: int -> int -> thm
   val mk_sum_casesN_balanced: int -> int -> thm
 
+  val find_minimum: ('b * 'b -> order) -> ('a -> 'b) -> 'a list -> 'a
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
   val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list ->
@@ -315,6 +321,12 @@
 val sel_unfoldN = selN ^ "_" ^ unfoldN
 val sel_corecN = selN ^ "_" ^ corecN
 
+fun add_components_of_typ (Type (s, Ts)) =
+    fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
+  | add_components_of_typ _ = I;
+
+fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
+
 val mk_common_name = space_implode "_";
 
 fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
@@ -381,9 +393,33 @@
 
 val mk_union = HOLogic.mk_binop @{const_name sup};
 
+fun find_minimum _ _ [] = raise Empty
+  | find_minimum _ _ [x] = x
+  | find_minimum ord f xs =
+    let
+      fun find [x] = (f x, x)
+        | find (x :: xs) =
+          let
+            val y = f x;
+            val p' as (y', _) = find xs;
+          in
+            if ord (y', y) = LESS then p' else (y, x)
+          end;
+    in snd (find xs) end;
+
 (*dangerous; use with monotonic, converging functions only!*)
 fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X);
 
+fun variant_types ss Ss ctxt =
+  let
+    val (tfrees, _) =
+      fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
+    val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
+  in (tfrees, ctxt') end;
+
+fun variant_tfrees ss =
+  apfst (map TFree) o variant_types (map (prefix "'") ss) (replicate (length ss) HOLogic.typeS);
+
 (* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *)
 fun split_conj_thm th =
   ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];