# HG changeset patch
# User blanchet
# Date 1376660147 -7200
# Node ID 83cbe188855acfe8b1928de78709c05d29ab87c0
# Parent  1b18e3ce776fd2e817fd4fbc86a2d6e50f02c25f
moved useful library functions upstream

diff -r 1b18e3ce776f -r 83cbe188855a src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Fri Aug 16 15:33:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Fri Aug 16 15:35:47 2013 +0200
@@ -83,6 +83,8 @@
 
   val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
 
+  val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list
+
   datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
   datatype fact_policy = Dont_Note | Note_Some | Note_All
 
@@ -321,6 +323,15 @@
 val nwits_of_bnf = #nwits o rep_bnf;
 val wits_of_bnf = #wits o rep_bnf;
 
+fun flatten_type_args_of_bnf bnf dead_x xs =
+  let
+    val Type (_, Ts) = T_of_bnf bnf;
+    val lives = lives_of_bnf bnf;
+    val deads = deads_of_bnf bnf;
+  in
+    sort_like (op =) (deads @ lives) (replicate (length deads) dead_x @ xs) Ts
+  end;
+
 (*terms*)
 val map_of_bnf = #map o rep_bnf;
 val sets_of_bnf = #sets o rep_bnf;
diff -r 1b18e3ce776f -r 83cbe188855a src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 15:33:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 15:35:47 2013 +0200
@@ -33,6 +33,7 @@
   val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
   val mk_map: int -> typ list -> typ list -> term -> term
   val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
+  val dest_map: Proof.context -> string -> term -> term * term list
   val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
     int list list -> term list list -> Proof.context ->
     (term list list
@@ -287,6 +288,28 @@
         | _ => build_simple TU);
   in build end;
 
+val dummy_var_name = "?f"
+
+fun mk_map_pattern ctxt s =
+  let
+    val bnf = the (bnf_of ctxt s);
+    val mapx = map_of_bnf bnf;
+    val live = live_of_bnf bnf;
+    val (f_Ts, _) = strip_typeN live (fastype_of mapx);
+    val fs = map_index (fn (i, T) => Var ((dummy_var_name, i), T)) f_Ts;
+  in
+    (mapx, betapplys (mapx, fs))
+  end;
+
+fun dest_map ctxt s call =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val (map0, pat) = mk_map_pattern ctxt s;
+    val (_, tenv) = Pattern.first_order_match thy (pat, call) (Vartab.empty, Vartab.empty);
+  in
+    (map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv [])
+  end;
+
 fun liveness_of_fp_bnf n bnf =
   (case T_of_bnf bnf of
     Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts