src/HOL/hologic.ML

--- a/src/HOL/hologic.ML	Wed Jan 14 10:30:01 1998 +0100
+++ b/src/HOL/hologic.ML	Wed Jan 14 10:30:44 1998 +0100
@@ -18,7 +18,7 @@
   val conj: term
   val disj: term
   val imp: term
-  val dest_imp	       : term -> term*term
+  val dest_imp: term -> term * term
   val eq_const: typ -> term
   val all_const: typ -> term
   val exists_const: typ -> term
@@ -38,6 +38,15 @@
   val dest_Suc: term -> term
   val mk_nat: int -> term
   val dest_nat: term -> int
+  val unitT: typ
+  val unit: term
+  val is_unit: term -> bool
+  val mk_prodT: typ * typ -> typ
+  val dest_prodT: typ -> typ * typ
+  val mk_prod: term * term -> term
+  val dest_prod: term -> term * term
+  val mk_fst: term -> term
+  val mk_snd: term -> term
 end;
 
 
@@ -138,4 +147,40 @@
   | dest_nat t = raise TERM ("dest_nat", [t]);
 
 
+(* unit *)
+
+val unitT = Type ("unit", []);
+
+val unit = Const ("()", unitT);
+
+fun is_unit (Const ("()", _)) = true
+  | is_unit _ = false;
+
+
+(* prod *)
+
+fun mk_prodT (T1, T2) = Type ("*", [T1, T2]);
+
+fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
+  | dest_prodT T = raise TYPE ("dest_prodT", [T], []);
+
+fun mk_prod (t1, t2) =
+  let val T1 = fastype_of t1 and T2 = fastype_of t2 in
+    Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2)) $ t1 $ t2
+  end;
+
+fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2)
+  | dest_prod t = raise TERM ("dest_prod", [t]);
+
+fun mk_fst p =
+  let val pT = fastype_of p in
+    Const ("fst", pT --> fst (dest_prodT pT)) $ p
+  end;
+
+fun mk_snd p =
+  let val pT = fastype_of p in
+    Const ("snd", pT --> snd (dest_prodT pT)) $ p
+  end;
+
+
 end;