1(* Title: FOL/fologic.ML 2 Author: Lawrence C Paulson 3 4Abstract syntax operations for FOL. 5*) 6 7signature FOLOGIC = 8sig 9 val oT: typ 10 val mk_Trueprop: term -> term 11 val dest_Trueprop: term -> term 12 val not: term 13 val conj: term 14 val disj: term 15 val imp: term 16 val iff: term 17 val mk_conj: term * term -> term 18 val mk_disj: term * term -> term 19 val mk_imp: term * term -> term 20 val dest_imp: term -> term * term 21 val dest_conj: term -> term list 22 val mk_iff: term * term -> term 23 val dest_iff: term -> term * term 24 val all_const: typ -> term 25 val mk_all: term * term -> term 26 val exists_const: typ -> term 27 val mk_exists: term * term -> term 28 val eq_const: typ -> term 29 val mk_eq: term * term -> term 30 val dest_eq: term -> term * term 31 val mk_binop: string -> term * term -> term 32 val mk_binrel: string -> term * term -> term 33 val dest_bin: string -> typ -> term -> term * term 34end; 35 36 37structure FOLogic: FOLOGIC = 38struct 39 40val oT = Type(\<^type_name>\<open>o\<close>,[]); 41 42val Trueprop = Const(\<^const_name>\<open>Trueprop\<close>, oT-->propT); 43 44fun mk_Trueprop P = Trueprop $ P; 45 46fun dest_Trueprop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ P) = P 47 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); 48 49 50(* Logical constants *) 51 52val not = Const (\<^const_name>\<open>Not\<close>, oT --> oT); 53val conj = Const(\<^const_name>\<open>conj\<close>, [oT,oT]--->oT); 54val disj = Const(\<^const_name>\<open>disj\<close>, [oT,oT]--->oT); 55val imp = Const(\<^const_name>\<open>imp\<close>, [oT,oT]--->oT) 56val iff = Const(\<^const_name>\<open>iff\<close>, [oT,oT]--->oT); 57 58fun mk_conj (t1, t2) = conj $ t1 $ t2 59and mk_disj (t1, t2) = disj $ t1 $ t2 60and mk_imp (t1, t2) = imp $ t1 $ t2 61and mk_iff (t1, t2) = iff $ t1 $ t2; 62 63fun dest_imp (Const(\<^const_name>\<open>imp\<close>,_) $ A $ B) = (A, B) 64 | dest_imp t = raise TERM ("dest_imp", [t]); 65 66fun dest_conj (Const (\<^const_name>\<open>conj\<close>, _) $ t $ t') = t :: dest_conj t' 67 | dest_conj t = [t]; 68 69fun dest_iff (Const(\<^const_name>\<open>iff\<close>,_) $ A $ B) = (A, B) 70 | dest_iff t = raise TERM ("dest_iff", [t]); 71 72fun eq_const T = Const (\<^const_name>\<open>eq\<close>, [T, T] ---> oT); 73fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; 74 75fun dest_eq (Const (\<^const_name>\<open>eq\<close>, _) $ lhs $ rhs) = (lhs, rhs) 76 | dest_eq t = raise TERM ("dest_eq", [t]) 77 78fun all_const T = Const (\<^const_name>\<open>All\<close>, [T --> oT] ---> oT); 79fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P; 80 81fun exists_const T = Const (\<^const_name>\<open>Ex\<close>, [T --> oT] ---> oT); 82fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P; 83 84 85(* binary oprations and relations *) 86 87fun mk_binop c (t, u) = 88 let val T = fastype_of t in 89 Const (c, [T, T] ---> T) $ t $ u 90 end; 91 92fun mk_binrel c (t, u) = 93 let val T = fastype_of t in 94 Const (c, [T, T] ---> oT) $ t $ u 95 end; 96 97fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) = 98 if c = c' andalso T = T' then (t, u) 99 else raise TERM ("dest_bin " ^ c, [tm]) 100 | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]); 101 102end; 103