--- 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