--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 04 17:23:08 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 04 18:14:58 2012 +0200
@@ -85,6 +85,8 @@
val mk_Inl: term -> typ -> term
val mk_Inr: term -> typ -> term
val mk_InN: typ list -> term -> int -> term
+ val mk_sum_case: term -> term -> term
+ val mk_sum_caseN: term list -> term
val mk_Field: term -> term
val mk_union: term * term -> term
@@ -201,6 +203,18 @@
| mk_InN (LT :: Ts) t m = mk_Inr (mk_InN Ts t (m - 1)) LT
| mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t]));
+fun mk_sum_case f g =
+ let
+ val fT = fastype_of f;
+ val gT = fastype_of g;
+ in
+ Const (@{const_name sum_case},
+ fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g
+ end;
+
+fun mk_sum_caseN [f] = f
+ | mk_sum_caseN (f :: fs) = mk_sum_case f (mk_sum_caseN fs);
+
fun mk_Field r =
let val T = fst (dest_relT (fastype_of r));
in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;