binary oprations and relations;
nat;

--- a/src/HOL/hologic.ML	Thu Jan 16 14:53:37 1997 +0100
+++ b/src/HOL/hologic.ML	Thu Jan 16 16:53:15 1997 +0100
@@ -27,20 +27,30 @@
   val mk_exists: string * typ * term -> term
   val mk_Collect: string * typ * term -> term
   val mk_mem: term * term -> term
+  val mk_binop: string -> term * term -> term
+  val mk_binrel: string -> term * term -> term
+  val dest_bin: string -> typ -> term -> term * term
+  val natT: typ
+  val zero: term
+  val is_zero: term -> bool
+  val mk_Suc: term -> term
+  val dest_Suc: term -> term
+  val mk_nat: int -> term
 end;
 
+
 structure HOLogic: HOLOGIC =
 struct
 
-(* classes *)
+(* basics *)
 
 val termC: class = "term";
 val termS: sort = [termC];
 
+val termTVar = TVar (("'a", 0), termS);
 
-(* types *)
 
-val termTVar = TVar (("'a", 0), termS);
+(* bool and set *)
 
 val boolT = Type ("bool", []);
 
@@ -50,8 +60,6 @@
   | dest_setT T = raise_type "dest_setT: set type expected" [T] [];
 
 
-(* terms *)
-
 val Trueprop = Const ("Trueprop", boolT --> propT);
 
 fun mk_Trueprop P = Trueprop $ P;
@@ -82,5 +90,38 @@
   end;
 
 
+(* binary oprations and relations *)
+
+fun mk_binop c (t, u) =
+  let val T = fastype_of t in
+    Const (c, [T, T] ---> T) $ t $ u
+  end;
+
+fun mk_binrel c (t, u) =
+  let val T = fastype_of t in
+    Const (c, [T, T] ---> boolT) $ t $ u
+  end;
+
+fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
+      if c = c' andalso T = T' then (t, u)
+      else raise_term ("dest_bin " ^ c) [tm]
+  | dest_bin c _ tm = raise_term ("dest_bin " ^ c) [tm];
+
+
+(* nat *)
+
+val natT = Type ("nat", []);
+
+val zero = Const ("0", natT);
+fun is_zero t = t = zero;
+
+fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
+
+fun dest_Suc (Const ("Suc", _) $ t) = t
+  | dest_Suc t = raise_term "dest_Suc" [t];
+
+fun mk_nat 0 = zero
+  | mk_nat n = mk_Suc (mk_nat (n - 1));
+
+
 end;
-