1 (* Title: FOL/fologic.ML
2 Author: Lawrence C Paulson
4 Abstract syntax operations for FOL.
10 val mk_Trueprop: term -> term
11 val dest_Trueprop: term -> 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
37 structure FOLogic: FOLOGIC =
40 val oT = Type(@{type_name o},[]);
42 val Trueprop = Const(@{const_name Trueprop}, oT-->propT);
44 fun mk_Trueprop P = Trueprop $ P;
46 fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P
47 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
50 (* Logical constants *)
52 val not = Const (@{const_name Not}, oT --> oT);
53 val conj = Const(@{const_name conj}, [oT,oT]--->oT);
54 val disj = Const(@{const_name disj}, [oT,oT]--->oT);
55 val imp = Const(@{const_name imp}, [oT,oT]--->oT)
56 val iff = Const(@{const_name iff}, [oT,oT]--->oT);
58 fun mk_conj (t1, t2) = conj $ t1 $ t2
59 and mk_disj (t1, t2) = disj $ t1 $ t2
60 and mk_imp (t1, t2) = imp $ t1 $ t2
61 and mk_iff (t1, t2) = iff $ t1 $ t2;
63 fun dest_imp (Const(@{const_name imp},_) $ A $ B) = (A, B)
64 | dest_imp t = raise TERM ("dest_imp", [t]);
66 fun dest_conj (Const (@{const_name conj}, _) $ t $ t') = t :: dest_conj t'
69 fun dest_iff (Const(@{const_name iff},_) $ A $ B) = (A, B)
70 | dest_iff t = raise TERM ("dest_iff", [t]);
72 fun eq_const T = Const (@{const_name eq}, [T, T] ---> oT);
73 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
75 fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs)
76 | dest_eq t = raise TERM ("dest_eq", [t])
78 fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
79 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
81 fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
82 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
85 (* binary oprations and relations *)
87 fun mk_binop c (t, u) =
88 let val T = fastype_of t in
89 Const (c, [T, T] ---> T) $ t $ u
92 fun mk_binrel c (t, u) =
93 let val T = fastype_of t in
94 Const (c, [T, T] ---> oT) $ t $ u
97 fun 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]);