# HG changeset patch
# User paulson
# Date 965636762 -7200
# Node ID ce61d1c1a509f3850ff7818f1419ce7d13fc1578
# Parent  fa19ffdbe1de1394b81ed17b8d512f74afb75565
new abstract syntax operations, used in ZF

diff -r fa19ffdbe1de -r ce61d1c1a509 src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Mon Aug 07 10:25:12 2000 +0200
+++ b/src/FOL/fologic.ML	Mon Aug 07 10:26:02 2000 +0200
@@ -14,10 +14,13 @@
   val conj		: term
   val disj		: term
   val imp		: term
+  val iff		: term
   val mk_conj		: term * term -> term
   val mk_disj		: term * term -> term
   val mk_imp		: term * term -> term
   val dest_imp	       	: term -> term*term
+  val mk_iff		: term * term -> term
+  val dest_iff	       	: term -> term*term
   val all_const		: typ -> term
   val mk_all		: term * term -> term
   val exists_const	: typ -> term
@@ -25,6 +28,9 @@
   val eq_const		: typ -> term
   val mk_eq		: term * term -> term
   val dest_eq 		: 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
 end;
 
 
@@ -46,15 +52,20 @@
 
 val conj = Const("op &", [oT,oT]--->oT)
 and disj = Const("op |", [oT,oT]--->oT)
-and imp = Const("op -->", [oT,oT]--->oT);
+and imp = Const("op -->", [oT,oT]--->oT)
+and iff = Const("op <->", [oT,oT]--->oT);
 
 fun mk_conj (t1, t2) = conj $ t1 $ t2
 and mk_disj (t1, t2) = disj $ t1 $ t2
-and mk_imp (t1, t2) = imp $ t1 $ t2;
+and mk_imp (t1, t2) = imp $ t1 $ t2
+and mk_iff (t1, t2) = iff $ t1 $ t2;
 
 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);
 
+fun dest_iff (Const("op <->",_) $ A $ B) = (A, B)
+  | dest_iff  t = raise TERM ("dest_iff", [t]);
+
 fun eq_const T = Const ("op =", [T, T] ---> oT);
 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
 
@@ -67,4 +78,22 @@
 fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
 
+(* 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] ---> oT) $ 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]);
+
+
 end;