src/FOL/fologic.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/fologic.ML	Wed Dec 03 10:48:16 1997 +0100
@@ -0,0 +1,52 @@
+(*  Title:      FOL/fologic.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson
+
+Abstract syntax operations for FOL.
+*)
+
+signature FOLOGIC =
+sig
+  val oT: typ
+  val mk_Trueprop: term -> term
+  val dest_Trueprop: term -> term
+  val conj: term
+  val disj: term
+  val imp: term
+  val eq_const: typ -> term
+  val all_const: typ -> term
+  val exists_const: typ -> term
+  val mk_eq: term * term -> term
+  val mk_all: term * term -> term
+  val mk_exists: term * term -> term
+end;
+
+
+structure FOLogic: FOLOGIC =
+struct
+
+val oT = Type("o",[]);
+
+val Trueprop = Const("Trueprop", oT-->propT);
+
+fun mk_Trueprop P = Trueprop $ P;
+
+fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
+  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
+
+(** Logical constants **)
+
+val conj = Const("op &", [oT,oT]--->oT)
+and disj = Const("op |", [oT,oT]--->oT)
+and imp = Const("op -->", [oT,oT]--->oT);
+
+fun eq_const T = Const ("op =", [T, T] ---> oT);
+fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
+
+fun all_const T = Const ("All", [T --> oT] ---> oT);
+fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
+
+fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
+fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
+
+end;