35 |
35 |
36 |
36 |
37 structure FOLogic: FOLOGIC = |
37 structure FOLogic: FOLOGIC = |
38 struct |
38 struct |
39 |
39 |
40 val oT = Type(\<^type_name>\<open>o\<close>,[]); |
40 val oT = \<^Type>\<open>o\<close>; |
41 |
41 |
42 val Trueprop = Const(\<^const_name>\<open>Trueprop\<close>, oT-->propT); |
42 val Trueprop = \<^Const>\<open>Trueprop\<close>; |
43 |
43 |
44 fun mk_Trueprop P = Trueprop $ P; |
44 fun mk_Trueprop P = Trueprop $ P; |
45 |
45 |
46 fun dest_Trueprop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ P) = P |
46 fun dest_Trueprop \<^Const_>\<open>Trueprop for P\<close> = P |
47 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
47 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
48 |
48 |
49 |
49 |
50 (* Logical constants *) |
50 (* Logical constants *) |
51 |
51 |
52 val not = Const (\<^const_name>\<open>Not\<close>, oT --> oT); |
52 val not = \<^Const>\<open>Not\<close>; |
53 val conj = Const(\<^const_name>\<open>conj\<close>, [oT,oT]--->oT); |
53 val conj = \<^Const>\<open>conj\<close>; |
54 val disj = Const(\<^const_name>\<open>disj\<close>, [oT,oT]--->oT); |
54 val disj = \<^Const>\<open>disj\<close>; |
55 val imp = Const(\<^const_name>\<open>imp\<close>, [oT,oT]--->oT) |
55 val imp = \<^Const>\<open>imp\<close>; |
56 val iff = Const(\<^const_name>\<open>iff\<close>, [oT,oT]--->oT); |
56 val iff = \<^Const>\<open>iff\<close>; |
57 |
57 |
58 fun mk_conj (t1, t2) = conj $ t1 $ t2 |
58 fun mk_conj (t1, t2) = conj $ t1 $ t2 |
59 and mk_disj (t1, t2) = disj $ t1 $ t2 |
59 and mk_disj (t1, t2) = disj $ t1 $ t2 |
60 and mk_imp (t1, t2) = imp $ t1 $ t2 |
60 and mk_imp (t1, t2) = imp $ t1 $ t2 |
61 and mk_iff (t1, t2) = iff $ t1 $ t2; |
61 and mk_iff (t1, t2) = iff $ t1 $ t2; |
62 |
62 |
63 fun dest_imp (Const(\<^const_name>\<open>imp\<close>,_) $ A $ B) = (A, B) |
63 fun dest_imp \<^Const_>\<open>imp for A B\<close> = (A, B) |
64 | dest_imp t = raise TERM ("dest_imp", [t]); |
64 | dest_imp t = raise TERM ("dest_imp", [t]); |
65 |
65 |
66 fun dest_conj (Const (\<^const_name>\<open>conj\<close>, _) $ t $ t') = t :: dest_conj t' |
66 fun dest_conj \<^Const_>\<open>conj for t t'\<close> = t :: dest_conj t' |
67 | dest_conj t = [t]; |
67 | dest_conj t = [t]; |
68 |
68 |
69 fun dest_iff (Const(\<^const_name>\<open>iff\<close>,_) $ A $ B) = (A, B) |
69 fun dest_iff \<^Const_>\<open>iff for A B\<close> = (A, B) |
70 | dest_iff t = raise TERM ("dest_iff", [t]); |
70 | dest_iff t = raise TERM ("dest_iff", [t]); |
71 |
71 |
72 fun eq_const T = Const (\<^const_name>\<open>eq\<close>, [T, T] ---> oT); |
72 fun eq_const T = \<^Const>\<open>eq T\<close>; |
73 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
73 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
74 |
74 |
75 fun dest_eq (Const (\<^const_name>\<open>eq\<close>, _) $ lhs $ rhs) = (lhs, rhs) |
75 fun dest_eq \<^Const_>\<open>eq _ for lhs rhs\<close> = (lhs, rhs) |
76 | dest_eq t = raise TERM ("dest_eq", [t]) |
76 | dest_eq t = raise TERM ("dest_eq", [t]) |
77 |
77 |
78 fun all_const T = Const (\<^const_name>\<open>All\<close>, [T --> oT] ---> oT); |
78 fun all_const T = \<^Const>\<open>All T\<close>; |
79 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; |
80 |
80 |
81 fun exists_const T = Const (\<^const_name>\<open>Ex\<close>, [T --> oT] ---> oT); |
81 fun exists_const T = \<^Const>\<open>Ex T\<close>; |
82 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; |
83 |
83 |
84 |
84 |
85 (* binary oprations and relations *) |
85 (* binary operations and relations *) |
86 |
86 |
87 fun mk_binop c (t, u) = |
87 fun mk_binop c (t, u) = |
88 let val T = fastype_of t in |
88 let val T = fastype_of t in |
89 Const (c, [T, T] ---> T) $ t $ u |
89 Const (c, [T, T] ---> T) $ t $ u |
90 end; |
90 end; |