|
1 (* Title: FOL/fologic.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson |
|
4 |
|
5 Abstract syntax operations for FOL. |
|
6 *) |
|
7 |
|
8 signature FOLOGIC = |
|
9 sig |
|
10 val oT: typ |
|
11 val mk_Trueprop: term -> term |
|
12 val dest_Trueprop: term -> term |
|
13 val conj: term |
|
14 val disj: term |
|
15 val imp: term |
|
16 val eq_const: typ -> term |
|
17 val all_const: typ -> term |
|
18 val exists_const: typ -> term |
|
19 val mk_eq: term * term -> term |
|
20 val mk_all: term * term -> term |
|
21 val mk_exists: term * term -> term |
|
22 end; |
|
23 |
|
24 |
|
25 structure FOLogic: FOLOGIC = |
|
26 struct |
|
27 |
|
28 val oT = Type("o",[]); |
|
29 |
|
30 val Trueprop = Const("Trueprop", oT-->propT); |
|
31 |
|
32 fun mk_Trueprop P = Trueprop $ P; |
|
33 |
|
34 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P |
|
35 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
|
36 |
|
37 (** Logical constants **) |
|
38 |
|
39 val conj = Const("op &", [oT,oT]--->oT) |
|
40 and disj = Const("op |", [oT,oT]--->oT) |
|
41 and imp = Const("op -->", [oT,oT]--->oT); |
|
42 |
|
43 fun eq_const T = Const ("op =", [T, T] ---> oT); |
|
44 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
|
45 |
|
46 fun all_const T = Const ("All", [T --> oT] ---> oT); |
|
47 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P)); |
|
48 |
|
49 fun exists_const T = Const ("Ex", [T --> oT] ---> oT); |
|
50 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P)); |
|
51 |
|
52 end; |