added unit and prod stuff;
authorwenzelm
Wed Jan 14 10:30:44 1998 +0100 (1998-01-14)
changeset 45716b02fc8a97f6
parent 4570 c04027ccc86e
child 4572 a259399ac328
added unit and prod stuff;
src/HOL/hologic.ML
     1.1 --- a/src/HOL/hologic.ML	Wed Jan 14 10:30:01 1998 +0100
     1.2 +++ b/src/HOL/hologic.ML	Wed Jan 14 10:30:44 1998 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    val conj: term
     1.5    val disj: term
     1.6    val imp: term
     1.7 -  val dest_imp	       : term -> term*term
     1.8 +  val dest_imp: term -> term * term
     1.9    val eq_const: typ -> term
    1.10    val all_const: typ -> term
    1.11    val exists_const: typ -> term
    1.12 @@ -38,6 +38,15 @@
    1.13    val dest_Suc: term -> term
    1.14    val mk_nat: int -> term
    1.15    val dest_nat: term -> int
    1.16 +  val unitT: typ
    1.17 +  val unit: term
    1.18 +  val is_unit: term -> bool
    1.19 +  val mk_prodT: typ * typ -> typ
    1.20 +  val dest_prodT: typ -> typ * typ
    1.21 +  val mk_prod: term * term -> term
    1.22 +  val dest_prod: term -> term * term
    1.23 +  val mk_fst: term -> term
    1.24 +  val mk_snd: term -> term
    1.25  end;
    1.26  
    1.27  
    1.28 @@ -138,4 +147,40 @@
    1.29    | dest_nat t = raise TERM ("dest_nat", [t]);
    1.30  
    1.31  
    1.32 +(* unit *)
    1.33 +
    1.34 +val unitT = Type ("unit", []);
    1.35 +
    1.36 +val unit = Const ("()", unitT);
    1.37 +
    1.38 +fun is_unit (Const ("()", _)) = true
    1.39 +  | is_unit _ = false;
    1.40 +
    1.41 +
    1.42 +(* prod *)
    1.43 +
    1.44 +fun mk_prodT (T1, T2) = Type ("*", [T1, T2]);
    1.45 +
    1.46 +fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
    1.47 +  | dest_prodT T = raise TYPE ("dest_prodT", [T], []);
    1.48 +
    1.49 +fun mk_prod (t1, t2) =
    1.50 +  let val T1 = fastype_of t1 and T2 = fastype_of t2 in
    1.51 +    Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2)) $ t1 $ t2
    1.52 +  end;
    1.53 +
    1.54 +fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2)
    1.55 +  | dest_prod t = raise TERM ("dest_prod", [t]);
    1.56 +
    1.57 +fun mk_fst p =
    1.58 +  let val pT = fastype_of p in
    1.59 +    Const ("fst", pT --> fst (dest_prodT pT)) $ p
    1.60 +  end;
    1.61 +
    1.62 +fun mk_snd p =
    1.63 +  let val pT = fastype_of p in
    1.64 +    Const ("snd", pT --> snd (dest_prodT pT)) $ p
    1.65 +  end;
    1.66 +
    1.67 +
    1.68  end;