src/HOL/Codatatype/Tools/bnf_fp_util.ML
changeset 49255 2ecc533d6697
parent 49240 f7e75b802ef2
child 49264 9059e0dbdbc1
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 10 17:32:39 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 10 17:35:53 2012 +0200
     1.3 @@ -81,15 +81,18 @@
     1.4    val split_conj_thm: thm -> thm list
     1.5    val split_conj_prems: int -> thm -> thm
     1.6  
     1.7 +  val mk_sumTN: typ list -> typ
     1.8 +
     1.9    val Inl_const: typ -> typ -> term
    1.10    val Inr_const: typ -> typ -> term
    1.11  
    1.12 -  val mk_Inl: term -> typ -> term
    1.13 -  val mk_Inr: term -> typ -> term
    1.14 +  val mk_Inl: typ -> term -> term
    1.15 +  val mk_Inr: typ -> term -> term
    1.16    val mk_InN: typ list -> term -> int -> term
    1.17 -  val mk_sum_case: term -> term -> term
    1.18 +  val mk_sum_case: term * term -> term
    1.19    val mk_sum_caseN: term list -> term
    1.20  
    1.21 +  val dest_sumT: typ -> typ * typ
    1.22    val dest_sumTN: int -> typ -> typ list
    1.23    val dest_tupleT: int -> typ -> typ list
    1.24  
    1.25 @@ -197,18 +200,20 @@
    1.26  val set_inclN = "set_incl"
    1.27  val set_set_inclN = "set_set_incl"
    1.28  
    1.29 +fun mk_sumTN Ts = Library.foldr1 mk_sumT Ts;
    1.30 +
    1.31  fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
    1.32 -fun mk_Inl t RT = Inl_const (fastype_of t) RT $ t;
    1.33 +fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
    1.34  
    1.35  fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
    1.36 -fun mk_Inr t LT = Inr_const LT (fastype_of t) $ t;
    1.37 +fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
    1.38  
    1.39  fun mk_InN [_] t 1 = t
    1.40 -  | mk_InN (_ :: Ts) t 1 = mk_Inl t (mk_sumTN Ts)
    1.41 -  | mk_InN (LT :: Ts) t m = mk_Inr (mk_InN Ts t (m - 1)) LT
    1.42 +  | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t
    1.43 +  | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1))
    1.44    | mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t]));
    1.45  
    1.46 -fun mk_sum_case f g =
    1.47 +fun mk_sum_case (f, g) =
    1.48    let
    1.49      val fT = fastype_of f;
    1.50      val gT = fastype_of g;
    1.51 @@ -218,7 +223,9 @@
    1.52    end;
    1.53  
    1.54  fun mk_sum_caseN [f] = f
    1.55 -  | mk_sum_caseN (f :: fs) = mk_sum_case f (mk_sum_caseN fs);
    1.56 +  | mk_sum_caseN (f :: fs) = mk_sum_case (f, mk_sum_caseN fs);
    1.57 +
    1.58 +fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
    1.59  
    1.60  fun dest_sumTN 1 T = [T]
    1.61    | dest_sumTN n (Type (@{type_name sum}, [T, T'])) = T :: dest_sumTN (n - 1) T';
    1.62 @@ -247,7 +254,7 @@
    1.63        if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
    1.64    in split limit 1 th end;
    1.65  
    1.66 -fun mk_sumEN 1 = @{thm obj_sum_base}
    1.67 +fun mk_sumEN 1 = @{thm one_pointE}
    1.68    | mk_sumEN 2 = @{thm sumE}
    1.69    | mk_sumEN n =
    1.70      (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF