# HG changeset patch
# User blanchet
# Date 1376664526 -7200
# Node ID d4d47d08e16a193c6574c10a79ad91619c0959e5
# Parent  953534445ab6067e3999cb32b3704d916b2d83f2
added useful library function

diff -r 953534445ab6 -r d4d47d08e16a src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 15:49:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 16:48:46 2013 +0200
@@ -34,6 +34,7 @@
   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 dest_ctr: 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
@@ -288,6 +289,11 @@
         | _ => build_simple TU);
   in build end;
 
+fun fo_match ctxt t pat =
+  let val thy = Proof_Context.theory_of ctxt in
+    Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
+  end;
+
 val dummy_var_name = "?f"
 
 fun mk_map_pattern ctxt s =
@@ -303,13 +309,24 @@
 
 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);
+    val (_, tenv) = fo_match ctxt call pat;
   in
     (map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv [])
   end;
 
+fun dest_ctr ctxt s t =
+  let
+    val (f, args) = Term.strip_comb t;
+  in
+    (case fp_sugar_of ctxt s of
+      SOME fp_sugar =>
+      (case find_first (can (fo_match ctxt f)) (#ctrs (of_fp_sugar #ctr_sugars fp_sugar)) of
+        SOME f' => (f', args)
+      | NONE => raise Fail "dest_ctr")
+    | NONE => raise Fail "dest_ctr")
+  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