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