4 Abstract syntax operations for FOL. |
4 Abstract syntax operations for FOL. |
5 *) |
5 *) |
6 |
6 |
7 signature FOLOGIC = |
7 signature FOLOGIC = |
8 sig |
8 sig |
9 val oT : typ |
9 val oT: typ |
10 val mk_Trueprop : term -> term |
10 val mk_Trueprop: term -> term |
11 val dest_Trueprop : term -> term |
11 val dest_Trueprop: term -> term |
12 val not : term |
12 val not: term |
13 val conj : term |
13 val conj: term |
14 val disj : term |
14 val disj: term |
15 val imp : term |
15 val imp: term |
16 val iff : term |
16 val iff: term |
17 val mk_conj : term * term -> term |
17 val mk_conj: term * term -> term |
18 val mk_disj : term * term -> term |
18 val mk_disj: term * term -> term |
19 val mk_imp : term * term -> term |
19 val mk_imp: term * term -> term |
20 val dest_imp : term -> term*term |
20 val dest_imp: term -> term * term |
21 val dest_conj : term -> term list |
21 val dest_conj: term -> term list |
22 val mk_iff : term * term -> term |
22 val mk_iff: term * term -> term |
23 val dest_iff : term -> term*term |
23 val dest_iff: term -> term * term |
24 val all_const : typ -> term |
24 val all_const: typ -> term |
25 val mk_all : term * term -> term |
25 val mk_all: term * term -> term |
26 val exists_const : typ -> term |
26 val exists_const: typ -> term |
27 val mk_exists : term * term -> term |
27 val mk_exists: term * term -> term |
28 val eq_const : typ -> term |
28 val eq_const: typ -> term |
29 val mk_eq : term * term -> term |
29 val mk_eq: term * term -> term |
30 val dest_eq : term -> term*term |
30 val dest_eq: term -> term * term |
31 val mk_binop: string -> term * term -> term |
31 val mk_binop: string -> term * term -> term |
32 val mk_binrel: string -> term * term -> term |
32 val mk_binrel: string -> term * term -> term |
33 val dest_bin: string -> typ -> term -> term * term |
33 val dest_bin: string -> typ -> term -> term * term |
34 end; |
34 end; |
35 |
35 |
44 fun mk_Trueprop P = Trueprop $ P; |
44 fun mk_Trueprop P = Trueprop $ P; |
45 |
45 |
46 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P |
46 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P |
47 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
47 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
48 |
48 |
49 (** Logical constants **) |
49 |
|
50 (* Logical constants *) |
50 |
51 |
51 val not = Const ("Not", oT --> oT); |
52 val not = Const ("Not", oT --> oT); |
52 val conj = Const("op &", [oT,oT]--->oT); |
53 val conj = Const("op &", [oT,oT]--->oT); |
53 val disj = Const("op |", [oT,oT]--->oT); |
54 val disj = Const("op |", [oT,oT]--->oT); |
54 val imp = Const("op -->", [oT,oT]--->oT) |
55 val imp = Const("op -->", [oT,oT]--->oT) |
78 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P)); |
79 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P)); |
79 |
80 |
80 fun exists_const T = Const ("Ex", [T --> oT] ---> oT); |
81 fun exists_const T = Const ("Ex", [T --> oT] ---> oT); |
81 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P)); |
82 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P)); |
82 |
83 |
|
84 |
83 (* binary oprations and relations *) |
85 (* binary oprations and relations *) |
84 |
86 |
85 fun mk_binop c (t, u) = |
87 fun mk_binop c (t, u) = |
86 let val T = fastype_of t in |
88 let val T = fastype_of t in |
87 Const (c, [T, T] ---> T) $ t $ u |
89 Const (c, [T, T] ---> T) $ t $ u |
95 fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) = |
97 fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) = |
96 if c = c' andalso T = T' then (t, u) |
98 if c = c' andalso T = T' then (t, u) |
97 else raise TERM ("dest_bin " ^ c, [tm]) |
99 else raise TERM ("dest_bin " ^ c, [tm]) |
98 | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]); |
100 | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]); |
99 |
101 |
100 |
|
101 end; |
102 end; |