|
1 structure Order_Procedure : sig |
|
2 datatype int = Int_of_integer of IntInf.int |
|
3 val integer_of_int : int -> IntInf.int |
|
4 datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm | |
|
5 Neg of 'a fm |
|
6 datatype trm = Const of string | App of trm * trm | Var of int |
|
7 datatype prf_trm = PThm of string | Appt of prf_trm * trm | |
|
8 AppP of prf_trm * prf_trm | AbsP of trm * prf_trm | Bound of trm | |
|
9 Conv of trm * prf_trm * prf_trm |
|
10 datatype o_atom = EQ of int * int | LEQ of int * int | LESS of int * int |
|
11 val lo_contr_prf : (bool * o_atom) fm -> prf_trm option |
|
12 val po_contr_prf : (bool * o_atom) fm -> prf_trm option |
|
13 end = struct |
|
14 |
|
15 datatype int = Int_of_integer of IntInf.int; |
|
16 |
|
17 fun integer_of_int (Int_of_integer k) = k; |
|
18 |
|
19 fun equal_inta k l = (((integer_of_int k) : IntInf.int) = (integer_of_int l)); |
|
20 |
|
21 type 'a equal = {equal : 'a -> 'a -> bool}; |
|
22 val equal = #equal : 'a equal -> 'a -> 'a -> bool; |
|
23 |
|
24 val equal_int = {equal = equal_inta} : int equal; |
|
25 |
|
26 fun less_eq_int k l = IntInf.<= (integer_of_int k, integer_of_int l); |
|
27 |
|
28 type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool}; |
|
29 val less_eq = #less_eq : 'a ord -> 'a -> 'a -> bool; |
|
30 val less = #less : 'a ord -> 'a -> 'a -> bool; |
|
31 |
|
32 fun less_int k l = IntInf.< (integer_of_int k, integer_of_int l); |
|
33 |
|
34 val ord_int = {less_eq = less_eq_int, less = less_int} : int ord; |
|
35 |
|
36 type 'a preorder = {ord_preorder : 'a ord}; |
|
37 val ord_preorder = #ord_preorder : 'a preorder -> 'a ord; |
|
38 |
|
39 type 'a order = {preorder_order : 'a preorder}; |
|
40 val preorder_order = #preorder_order : 'a order -> 'a preorder; |
|
41 |
|
42 val preorder_int = {ord_preorder = ord_int} : int preorder; |
|
43 |
|
44 val order_int = {preorder_order = preorder_int} : int order; |
|
45 |
|
46 type 'a linorder = {order_linorder : 'a order}; |
|
47 val order_linorder = #order_linorder : 'a linorder -> 'a order; |
|
48 |
|
49 val linorder_int = {order_linorder = order_int} : int linorder; |
|
50 |
|
51 fun eq A_ a b = equal A_ a b; |
|
52 |
|
53 fun equal_proda A_ B_ (x1, x2) (y1, y2) = eq A_ x1 y1 andalso eq B_ x2 y2; |
|
54 |
|
55 fun equal_prod A_ B_ = {equal = equal_proda A_ B_} : ('a * 'b) equal; |
|
56 |
|
57 fun less_eq_prod A_ B_ (x1, y1) (x2, y2) = |
|
58 less A_ x1 x2 orelse less_eq A_ x1 x2 andalso less_eq B_ y1 y2; |
|
59 |
|
60 fun less_prod A_ B_ (x1, y1) (x2, y2) = |
|
61 less A_ x1 x2 orelse less_eq A_ x1 x2 andalso less B_ y1 y2; |
|
62 |
|
63 fun ord_prod A_ B_ = {less_eq = less_eq_prod A_ B_, less = less_prod A_ B_} : |
|
64 ('a * 'b) ord; |
|
65 |
|
66 fun preorder_prod A_ B_ = |
|
67 {ord_preorder = ord_prod (ord_preorder A_) (ord_preorder B_)} : |
|
68 ('a * 'b) preorder; |
|
69 |
|
70 fun order_prod A_ B_ = |
|
71 {preorder_order = preorder_prod (preorder_order A_) (preorder_order B_)} : |
|
72 ('a * 'b) order; |
|
73 |
|
74 fun linorder_prod A_ B_ = |
|
75 {order_linorder = order_prod (order_linorder A_) (order_linorder B_)} : |
|
76 ('a * 'b) linorder; |
|
77 |
|
78 datatype nat = Zero_nat | Suc of nat; |
|
79 |
|
80 datatype color = R | B; |
|
81 |
|
82 datatype ('a, 'b) rbta = Empty | |
|
83 Branch of color * ('a, 'b) rbta * 'a * 'b * ('a, 'b) rbta; |
|
84 |
|
85 datatype ('b, 'a) rbt = RBT of ('b, 'a) rbta; |
|
86 |
|
87 datatype 'a set = Set of 'a list | Coset of 'a list; |
|
88 |
|
89 datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm | |
|
90 Neg of 'a fm; |
|
91 |
|
92 datatype trm = Const of string | App of trm * trm | Var of int; |
|
93 |
|
94 datatype prf_trm = PThm of string | Appt of prf_trm * trm | |
|
95 AppP of prf_trm * prf_trm | AbsP of trm * prf_trm | Bound of trm | |
|
96 Conv of trm * prf_trm * prf_trm; |
|
97 |
|
98 datatype ('a, 'b) mapping = Mapping of ('a, 'b) rbt; |
|
99 |
|
100 datatype o_atom = EQ of int * int | LEQ of int * int | LESS of int * int; |
|
101 |
|
102 fun id x = (fn xa => xa) x; |
|
103 |
|
104 fun impl_of B_ (RBT x) = x; |
|
105 |
|
106 fun folda f (Branch (c, lt, k, v, rt)) x = folda f rt (f k v (folda f lt x)) |
|
107 | folda f Empty x = x; |
|
108 |
|
109 fun fold A_ x xc = folda x (impl_of A_ xc); |
|
110 |
|
111 fun gen_keys kts (Branch (c, l, k, v, r)) = gen_keys ((k, r) :: kts) l |
|
112 | gen_keys ((k, t) :: kts) Empty = k :: gen_keys kts t |
|
113 | gen_keys [] Empty = []; |
|
114 |
|
115 fun keysb x = gen_keys [] x; |
|
116 |
|
117 fun keys A_ x = keysb (impl_of A_ x); |
|
118 |
|
119 fun maps f [] = [] |
|
120 | maps f (x :: xs) = f x @ maps f xs; |
|
121 |
|
122 fun empty A_ = RBT Empty; |
|
123 |
|
124 fun foldl f a [] = a |
|
125 | foldl f a (x :: xs) = foldl f (f a x) xs; |
|
126 |
|
127 fun foldr f [] = id |
|
128 | foldr f (x :: xs) = f x o foldr f xs; |
|
129 |
|
130 fun balance (Branch (R, a, w, x, b)) s t (Branch (R, c, y, z, d)) = |
|
131 Branch (R, Branch (B, a, w, x, b), s, t, Branch (B, c, y, z, d)) |
|
132 | balance (Branch (R, Branch (R, a, w, x, b), s, t, c)) y z Empty = |
|
133 Branch (R, Branch (B, a, w, x, b), s, t, Branch (B, c, y, z, Empty)) |
|
134 | balance (Branch (R, Branch (R, a, w, x, b), s, t, c)) y z |
|
135 (Branch (B, va, vb, vc, vd)) = |
|
136 Branch |
|
137 (R, Branch (B, a, w, x, b), s, t, |
|
138 Branch (B, c, y, z, Branch (B, va, vb, vc, vd))) |
|
139 | balance (Branch (R, Empty, w, x, Branch (R, b, s, t, c))) y z Empty = |
|
140 Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, Empty)) |
|
141 | balance |
|
142 (Branch (R, Branch (B, va, vb, vc, vd), w, x, Branch (R, b, s, t, c))) y z |
|
143 Empty = |
|
144 Branch |
|
145 (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t, |
|
146 Branch (B, c, y, z, Empty)) |
|
147 | balance (Branch (R, Empty, w, x, Branch (R, b, s, t, c))) y z |
|
148 (Branch (B, va, vb, vc, vd)) = |
|
149 Branch |
|
150 (R, Branch (B, Empty, w, x, b), s, t, |
|
151 Branch (B, c, y, z, Branch (B, va, vb, vc, vd))) |
|
152 | balance |
|
153 (Branch (R, Branch (B, ve, vf, vg, vh), w, x, Branch (R, b, s, t, c))) y z |
|
154 (Branch (B, va, vb, vc, vd)) = |
|
155 Branch |
|
156 (R, Branch (B, Branch (B, ve, vf, vg, vh), w, x, b), s, t, |
|
157 Branch (B, c, y, z, Branch (B, va, vb, vc, vd))) |
|
158 | balance Empty w x (Branch (R, b, s, t, Branch (R, c, y, z, d))) = |
|
159 Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, d)) |
|
160 | balance (Branch (B, va, vb, vc, vd)) w x |
|
161 (Branch (R, b, s, t, Branch (R, c, y, z, d))) = |
|
162 Branch |
|
163 (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t, |
|
164 Branch (B, c, y, z, d)) |
|
165 | balance Empty w x (Branch (R, Branch (R, b, s, t, c), y, z, Empty)) = |
|
166 Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, Empty)) |
|
167 | balance Empty w x |
|
168 (Branch (R, Branch (R, b, s, t, c), y, z, Branch (B, va, vb, vc, vd))) = |
|
169 Branch |
|
170 (R, Branch (B, Empty, w, x, b), s, t, |
|
171 Branch (B, c, y, z, Branch (B, va, vb, vc, vd))) |
|
172 | balance (Branch (B, va, vb, vc, vd)) w x |
|
173 (Branch (R, Branch (R, b, s, t, c), y, z, Empty)) = |
|
174 Branch |
|
175 (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t, |
|
176 Branch (B, c, y, z, Empty)) |
|
177 | balance (Branch (B, va, vb, vc, vd)) w x |
|
178 (Branch (R, Branch (R, b, s, t, c), y, z, Branch (B, ve, vf, vg, vh))) = |
|
179 Branch |
|
180 (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t, |
|
181 Branch (B, c, y, z, Branch (B, ve, vf, vg, vh))) |
|
182 | balance Empty s t Empty = Branch (B, Empty, s, t, Empty) |
|
183 | balance Empty s t (Branch (B, va, vb, vc, vd)) = |
|
184 Branch (B, Empty, s, t, Branch (B, va, vb, vc, vd)) |
|
185 | balance Empty s t (Branch (v, Empty, vb, vc, Empty)) = |
|
186 Branch (B, Empty, s, t, Branch (v, Empty, vb, vc, Empty)) |
|
187 | balance Empty s t (Branch (v, Branch (B, ve, vf, vg, vh), vb, vc, Empty)) = |
|
188 Branch |
|
189 (B, Empty, s, t, Branch (v, Branch (B, ve, vf, vg, vh), vb, vc, Empty)) |
|
190 | balance Empty s t (Branch (v, Empty, vb, vc, Branch (B, vf, vg, vh, vi))) = |
|
191 Branch |
|
192 (B, Empty, s, t, Branch (v, Empty, vb, vc, Branch (B, vf, vg, vh, vi))) |
|
193 | balance Empty s t |
|
194 (Branch (v, Branch (B, ve, vj, vk, vl), vb, vc, Branch (B, vf, vg, vh, vi))) |
|
195 = Branch |
|
196 (B, Empty, s, t, |
|
197 Branch |
|
198 (v, Branch (B, ve, vj, vk, vl), vb, vc, Branch (B, vf, vg, vh, vi))) |
|
199 | balance (Branch (B, va, vb, vc, vd)) s t Empty = |
|
200 Branch (B, Branch (B, va, vb, vc, vd), s, t, Empty) |
|
201 | balance (Branch (B, va, vb, vc, vd)) s t (Branch (B, ve, vf, vg, vh)) = |
|
202 Branch (B, Branch (B, va, vb, vc, vd), s, t, Branch (B, ve, vf, vg, vh)) |
|
203 | balance (Branch (B, va, vb, vc, vd)) s t (Branch (v, Empty, vf, vg, Empty)) |
|
204 = Branch |
|
205 (B, Branch (B, va, vb, vc, vd), s, t, Branch (v, Empty, vf, vg, Empty)) |
|
206 | balance (Branch (B, va, vb, vc, vd)) s t |
|
207 (Branch (v, Branch (B, vi, vj, vk, vl), vf, vg, Empty)) = |
|
208 Branch |
|
209 (B, Branch (B, va, vb, vc, vd), s, t, |
|
210 Branch (v, Branch (B, vi, vj, vk, vl), vf, vg, Empty)) |
|
211 | balance (Branch (B, va, vb, vc, vd)) s t |
|
212 (Branch (v, Empty, vf, vg, Branch (B, vj, vk, vl, vm))) = |
|
213 Branch |
|
214 (B, Branch (B, va, vb, vc, vd), s, t, |
|
215 Branch (v, Empty, vf, vg, Branch (B, vj, vk, vl, vm))) |
|
216 | balance (Branch (B, va, vb, vc, vd)) s t |
|
217 (Branch (v, Branch (B, vi, vn, vo, vp), vf, vg, Branch (B, vj, vk, vl, vm))) |
|
218 = Branch |
|
219 (B, Branch (B, va, vb, vc, vd), s, t, |
|
220 Branch |
|
221 (v, Branch (B, vi, vn, vo, vp), vf, vg, Branch (B, vj, vk, vl, vm))) |
|
222 | balance (Branch (v, Empty, vb, vc, Empty)) s t Empty = |
|
223 Branch (B, Branch (v, Empty, vb, vc, Empty), s, t, Empty) |
|
224 | balance (Branch (v, Empty, vb, vc, Branch (B, ve, vf, vg, vh))) s t Empty = |
|
225 Branch |
|
226 (B, Branch (v, Empty, vb, vc, Branch (B, ve, vf, vg, vh)), s, t, Empty) |
|
227 | balance (Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Empty)) s t Empty = |
|
228 Branch |
|
229 (B, Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Empty), s, t, Empty) |
|
230 | balance |
|
231 (Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Branch (B, ve, vj, vk, vl))) |
|
232 s t Empty = |
|
233 Branch |
|
234 (B, Branch |
|
235 (v, Branch (B, vf, vg, vh, vi), vb, vc, Branch (B, ve, vj, vk, vl)), |
|
236 s, t, Empty) |
|
237 | balance (Branch (v, Empty, vf, vg, Empty)) s t (Branch (B, va, vb, vc, vd)) |
|
238 = Branch |
|
239 (B, Branch (v, Empty, vf, vg, Empty), s, t, Branch (B, va, vb, vc, vd)) |
|
240 | balance (Branch (v, Empty, vf, vg, Branch (B, vi, vj, vk, vl))) s t |
|
241 (Branch (B, va, vb, vc, vd)) = |
|
242 Branch |
|
243 (B, Branch (v, Empty, vf, vg, Branch (B, vi, vj, vk, vl)), s, t, |
|
244 Branch (B, va, vb, vc, vd)) |
|
245 | balance (Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Empty)) s t |
|
246 (Branch (B, va, vb, vc, vd)) = |
|
247 Branch |
|
248 (B, Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Empty), s, t, |
|
249 Branch (B, va, vb, vc, vd)) |
|
250 | balance |
|
251 (Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Branch (B, vi, vn, vo, vp))) |
|
252 s t (Branch (B, va, vb, vc, vd)) = |
|
253 Branch |
|
254 (B, Branch |
|
255 (v, Branch (B, vj, vk, vl, vm), vf, vg, Branch (B, vi, vn, vo, vp)), |
|
256 s, t, Branch (B, va, vb, vc, vd)); |
|
257 |
|
258 fun rbt_ins A_ f k v Empty = Branch (R, Empty, k, v, Empty) |
|
259 | rbt_ins A_ f k v (Branch (B, l, x, y, r)) = |
|
260 (if less A_ k x then balance (rbt_ins A_ f k v l) x y r |
|
261 else (if less A_ x k then balance l x y (rbt_ins A_ f k v r) |
|
262 else Branch (B, l, x, f k y v, r))) |
|
263 | rbt_ins A_ f k v (Branch (R, l, x, y, r)) = |
|
264 (if less A_ k x then Branch (R, rbt_ins A_ f k v l, x, y, r) |
|
265 else (if less A_ x k then Branch (R, l, x, y, rbt_ins A_ f k v r) |
|
266 else Branch (R, l, x, f k y v, r))); |
|
267 |
|
268 fun paint c Empty = Empty |
|
269 | paint c (Branch (uu, l, k, v, r)) = Branch (c, l, k, v, r); |
|
270 |
|
271 fun rbt_insert_with_key A_ f k v t = paint B (rbt_ins A_ f k v t); |
|
272 |
|
273 fun rbt_insert A_ = rbt_insert_with_key A_ (fn _ => fn _ => fn nv => nv); |
|
274 |
|
275 fun insert A_ xc xd xe = |
|
276 RBT (rbt_insert ((ord_preorder o preorder_order o order_linorder) A_) xc xd |
|
277 (impl_of A_ xe)); |
|
278 |
|
279 fun rbt_lookup A_ Empty k = NONE |
|
280 | rbt_lookup A_ (Branch (uu, l, x, y, r)) k = |
|
281 (if less A_ k x then rbt_lookup A_ l k |
|
282 else (if less A_ x k then rbt_lookup A_ r k else SOME y)); |
|
283 |
|
284 fun lookup A_ x = |
|
285 rbt_lookup ((ord_preorder o preorder_order o order_linorder) A_) |
|
286 (impl_of A_ x); |
|
287 |
|
288 fun member A_ [] y = false |
|
289 | member A_ (x :: xs) y = eq A_ x y orelse member A_ xs y; |
|
290 |
|
291 fun hd (x21 :: x22) = x21; |
|
292 |
|
293 fun tl [] = [] |
|
294 | tl (x21 :: x22) = x22; |
|
295 |
|
296 fun remdups A_ [] = [] |
|
297 | remdups A_ (x :: xs) = |
|
298 (if member A_ xs x then remdups A_ xs else x :: remdups A_ xs); |
|
299 |
|
300 fun dnf_and_fm (Or (phi_1, phi_2)) psi = |
|
301 Or (dnf_and_fm phi_1 psi, dnf_and_fm phi_2 psi) |
|
302 | dnf_and_fm (Atom v) (Or (phi_1, phi_2)) = |
|
303 Or (dnf_and_fm (Atom v) phi_1, dnf_and_fm (Atom v) phi_2) |
|
304 | dnf_and_fm (And (v, va)) (Or (phi_1, phi_2)) = |
|
305 Or (dnf_and_fm (And (v, va)) phi_1, dnf_and_fm (And (v, va)) phi_2) |
|
306 | dnf_and_fm (Neg v) (Or (phi_1, phi_2)) = |
|
307 Or (dnf_and_fm (Neg v) phi_1, dnf_and_fm (Neg v) phi_2) |
|
308 | dnf_and_fm (Atom v) (Atom va) = And (Atom v, Atom va) |
|
309 | dnf_and_fm (Atom v) (And (va, vb)) = And (Atom v, And (va, vb)) |
|
310 | dnf_and_fm (Atom v) (Neg va) = And (Atom v, Neg va) |
|
311 | dnf_and_fm (And (v, va)) (Atom vb) = And (And (v, va), Atom vb) |
|
312 | dnf_and_fm (And (v, va)) (And (vb, vc)) = And (And (v, va), And (vb, vc)) |
|
313 | dnf_and_fm (And (v, va)) (Neg vb) = And (And (v, va), Neg vb) |
|
314 | dnf_and_fm (Neg v) (Atom va) = And (Neg v, Atom va) |
|
315 | dnf_and_fm (Neg v) (And (va, vb)) = And (Neg v, And (va, vb)) |
|
316 | dnf_and_fm (Neg v) (Neg va) = And (Neg v, Neg va); |
|
317 |
|
318 fun dnf_fm (And (phi_1, phi_2)) = dnf_and_fm (dnf_fm phi_1) (dnf_fm phi_2) |
|
319 | dnf_fm (Or (phi_1, phi_2)) = Or (dnf_fm phi_1, dnf_fm phi_2) |
|
320 | dnf_fm (Atom v) = Atom v |
|
321 | dnf_fm (Neg v) = Neg v; |
|
322 |
|
323 fun keysa A_ (Mapping t) = Set (keys A_ t); |
|
324 |
|
325 fun amap_fm h (Atom a) = h a |
|
326 | amap_fm h (And (phi_1, phi_2)) = And (amap_fm h phi_1, amap_fm h phi_2) |
|
327 | amap_fm h (Or (phi_1, phi_2)) = Or (amap_fm h phi_1, amap_fm h phi_2) |
|
328 | amap_fm h (Neg phi) = Neg (amap_fm h phi); |
|
329 |
|
330 fun emptya A_ = Mapping (empty A_); |
|
331 |
|
332 fun lookupa A_ (Mapping t) = lookup A_ t; |
|
333 |
|
334 fun update A_ k v (Mapping t) = Mapping (insert A_ k v t); |
|
335 |
|
336 fun gen_length n (x :: xs) = gen_length (Suc n) xs |
|
337 | gen_length n [] = n; |
|
338 |
|
339 fun size_list x = gen_length Zero_nat x; |
|
340 |
|
341 fun card A_ (Set xs) = size_list (remdups A_ xs); |
|
342 |
|
343 fun conj_list (And (phi_1, phi_2)) = conj_list phi_1 @ conj_list phi_2 |
|
344 | conj_list (Atom a) = [a]; |
|
345 |
|
346 fun trm_of_fm f (Atom a) = f a |
|
347 | trm_of_fm f (And (phi_1, phi_2)) = |
|
348 App (App (Const "conj", trm_of_fm f phi_1), trm_of_fm f phi_2) |
|
349 | trm_of_fm f (Or (phi_1, phi_2)) = |
|
350 App (App (Const "disj", trm_of_fm f phi_1), trm_of_fm f phi_2) |
|
351 | trm_of_fm f (Neg phi) = App (Const "Not", trm_of_fm f phi); |
|
352 |
|
353 fun dnf_and_fm_prf (Or (phi_1, phi_2)) psi = |
|
354 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
|
355 [PThm "conj_disj_distribR_conv", |
|
356 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
|
357 [AppP (PThm "arg_conv", |
|
358 hd [dnf_and_fm_prf phi_1 psi, dnf_and_fm_prf phi_2 psi]), |
|
359 hd (tl [dnf_and_fm_prf phi_1 psi, dnf_and_fm_prf phi_2 psi])]] |
|
360 | dnf_and_fm_prf (Atom v) (Or (phi_1, phi_2)) = |
|
361 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
|
362 [PThm "conj_disj_distribL_conv", |
|
363 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
|
364 [AppP (PThm "arg_conv", |
|
365 hd [dnf_and_fm_prf (Atom v) phi_1, |
|
366 dnf_and_fm_prf (Atom v) phi_2]), |
|
367 hd (tl [dnf_and_fm_prf (Atom v) phi_1, |
|
368 dnf_and_fm_prf (Atom v) phi_2])]] |
|
369 | dnf_and_fm_prf (And (v, va)) (Or (phi_1, phi_2)) = |
|
370 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
|
371 [PThm "conj_disj_distribL_conv", |
|
372 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
|
373 [AppP (PThm "arg_conv", |
|
374 hd [dnf_and_fm_prf (And (v, va)) phi_1, |
|
375 dnf_and_fm_prf (And (v, va)) phi_2]), |
|
376 hd (tl [dnf_and_fm_prf (And (v, va)) phi_1, |
|
377 dnf_and_fm_prf (And (v, va)) phi_2])]] |
|
378 | dnf_and_fm_prf (Neg v) (Or (phi_1, phi_2)) = |
|
379 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
|
380 [PThm "conj_disj_distribL_conv", |
|
381 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
|
382 [AppP (PThm "arg_conv", |
|
383 hd [dnf_and_fm_prf (Neg v) phi_1, |
|
384 dnf_and_fm_prf (Neg v) phi_2]), |
|
385 hd (tl [dnf_and_fm_prf (Neg v) phi_1, |
|
386 dnf_and_fm_prf (Neg v) phi_2])]] |
|
387 | dnf_and_fm_prf (Atom v) (Atom va) = PThm "all_conv" |
|
388 | dnf_and_fm_prf (Atom v) (And (va, vb)) = PThm "all_conv" |
|
389 | dnf_and_fm_prf (Atom v) (Neg va) = PThm "all_conv" |
|
390 | dnf_and_fm_prf (And (v, va)) (Atom vb) = PThm "all_conv" |
|
391 | dnf_and_fm_prf (And (v, va)) (And (vb, vc)) = PThm "all_conv" |
|
392 | dnf_and_fm_prf (And (v, va)) (Neg vb) = PThm "all_conv" |
|
393 | dnf_and_fm_prf (Neg v) (Atom va) = PThm "all_conv" |
|
394 | dnf_and_fm_prf (Neg v) (And (va, vb)) = PThm "all_conv" |
|
395 | dnf_and_fm_prf (Neg v) (Neg va) = PThm "all_conv"; |
|
396 |
|
397 fun dnf_fm_prf (And (phi_1, phi_2)) = |
|
398 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
|
399 [foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
|
400 [AppP (PThm "arg_conv", hd [dnf_fm_prf phi_1, dnf_fm_prf phi_2]), |
|
401 hd (tl [dnf_fm_prf phi_1, dnf_fm_prf phi_2])], |
|
402 dnf_and_fm_prf (dnf_fm phi_1) (dnf_fm phi_2)] |
|
403 | dnf_fm_prf (Or (phi_1, phi_2)) = |
|
404 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
|
405 [AppP (PThm "arg_conv", hd [dnf_fm_prf phi_1, dnf_fm_prf phi_2]), |
|
406 hd (tl [dnf_fm_prf phi_1, dnf_fm_prf phi_2])] |
|
407 | dnf_fm_prf (Atom v) = PThm "all_conv" |
|
408 | dnf_fm_prf (Neg v) = PThm "all_conv"; |
|
409 |
|
410 fun of_alist A_ xs = foldr (fn (a, b) => update A_ a b) xs (emptya A_); |
|
411 |
|
412 fun deneg (true, LESS (x, y)) = |
|
413 And (Atom (true, LEQ (x, y)), Atom (false, EQ (x, y))) |
|
414 | deneg (false, LESS (x, y)) = Atom (true, LEQ (y, x)) |
|
415 | deneg (false, LEQ (x, y)) = |
|
416 And (Atom (true, LEQ (y, x)), Atom (false, EQ (y, x))) |
|
417 | deneg (false, EQ (v, vb)) = Atom (false, EQ (v, vb)) |
|
418 | deneg (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc)) |
|
419 | deneg (true, LEQ (vb, vc)) = Atom (true, LEQ (vb, vc)); |
|
420 |
|
421 fun from_conj_prf trm_of_atom p (And (a, b)) = |
|
422 foldl (fn aa => fn ba => AppP (aa, ba)) (PThm "conjE") |
|
423 [Bound (trm_of_fm trm_of_atom (And (a, b))), |
|
424 AbsP (trm_of_fm trm_of_atom a, |
|
425 AbsP (trm_of_fm trm_of_atom b, |
|
426 from_conj_prf trm_of_atom (from_conj_prf trm_of_atom p b) |
|
427 a))] |
|
428 | from_conj_prf trm_of_atom p (Atom a) = p; |
|
429 |
|
430 fun contr_fm_prf trm_of_atom contr_atom_prf (Or (c, d)) = |
|
431 (case (contr_fm_prf trm_of_atom contr_atom_prf c, |
|
432 contr_fm_prf trm_of_atom contr_atom_prf d) |
|
433 of (NONE, _) => NONE | (SOME _, NONE) => NONE |
|
434 | (SOME p1, SOME p2) => |
|
435 SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "disjE") |
|
436 [Bound (trm_of_fm trm_of_atom (Or (c, d))), |
|
437 AbsP (trm_of_fm trm_of_atom c, p1), |
|
438 AbsP (trm_of_fm trm_of_atom d, p2)])) |
|
439 | contr_fm_prf trm_of_atom contr_atom_prf (And (a, b)) = |
|
440 (case contr_atom_prf (conj_list (And (a, b))) of NONE => NONE |
|
441 | SOME p => SOME (from_conj_prf trm_of_atom p (And (a, b)))) |
|
442 | contr_fm_prf trm_of_atom contr_atom_prf (Atom a) = contr_atom_prf [a]; |
|
443 |
|
444 fun deless (true, LESS (x, y)) = |
|
445 And (Atom (true, LEQ (x, y)), Atom (false, EQ (x, y))) |
|
446 | deless (false, LESS (x, y)) = |
|
447 Or (Atom (false, LEQ (x, y)), Atom (true, EQ (x, y))) |
|
448 | deless (false, EQ (v, vb)) = Atom (false, EQ (v, vb)) |
|
449 | deless (false, LEQ (v, vb)) = Atom (false, LEQ (v, vb)) |
|
450 | deless (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc)) |
|
451 | deless (v, LEQ (vb, vc)) = Atom (v, LEQ (vb, vc)); |
|
452 |
|
453 fun deneg_prf (true, LESS (x, y)) = PThm "less_le" |
|
454 | deneg_prf (false, LESS (x, y)) = PThm "nless_le" |
|
455 | deneg_prf (false, LEQ (x, y)) = PThm "nle_le" |
|
456 | deneg_prf (false, EQ (v, vb)) = PThm "all_conv" |
|
457 | deneg_prf (v, EQ (vb, vc)) = PThm "all_conv" |
|
458 | deneg_prf (true, LEQ (vb, vc)) = PThm "all_conv"; |
|
459 |
|
460 val one_nat : nat = Suc Zero_nat; |
|
461 |
|
462 fun map_option f NONE = NONE |
|
463 | map_option f (SOME x2) = SOME (f x2); |
|
464 |
|
465 fun deless_prf (true, LESS (x, y)) = PThm "less_le" |
|
466 | deless_prf (false, LESS (x, y)) = PThm "nless_le" |
|
467 | deless_prf (false, EQ (v, vb)) = PThm "all_conv" |
|
468 | deless_prf (false, LEQ (v, vb)) = PThm "all_conv" |
|
469 | deless_prf (v, EQ (vb, vc)) = PThm "all_conv" |
|
470 | deless_prf (v, LEQ (vb, vc)) = PThm "all_conv"; |
|
471 |
|
472 fun trm_of_oatom (EQ (x, y)) = App (App (Const "eq", Var x), Var y) |
|
473 | trm_of_oatom (LEQ (x, y)) = App (App (Const "le", Var x), Var y) |
|
474 | trm_of_oatom (LESS (x, y)) = App (App (Const "lt", Var x), Var y); |
|
475 |
|
476 fun minus_nat (Suc m) (Suc n) = minus_nat m n |
|
477 | minus_nat Zero_nat n = Zero_nat |
|
478 | minus_nat m Zero_nat = m; |
|
479 |
|
480 fun mapping_fold A_ f (Mapping t) a = fold A_ f t a; |
|
481 |
|
482 fun relcomp1_mapping A_ (B1_, B2_) x y1 pxy pm pma = |
|
483 mapping_fold (linorder_prod B2_ B2_) |
|
484 (fn (y2, z) => fn pyz => fn pmb => |
|
485 (if eq B1_ y1 y2 andalso not (eq B1_ y2 z) |
|
486 then update (linorder_prod A_ B2_) (x, z) |
|
487 (foldl (fn a => fn b => AppP (a, b)) (PThm "trans") [pxy, pyz]) |
|
488 pmb |
|
489 else pmb)) |
|
490 pm pma; |
|
491 |
|
492 fun relcomp_mapping (A1_, A2_) pm1 pm2 pma = |
|
493 mapping_fold (linorder_prod A2_ A2_) |
|
494 (fn (x, y) => fn pxy => fn pm => |
|
495 (if eq A1_ x y then pm |
|
496 else relcomp1_mapping A2_ (A1_, A2_) x y pxy pm2 pm)) |
|
497 pm1 pma; |
|
498 |
|
499 fun ntrancl_mapping (A1_, A2_) Zero_nat m = m |
|
500 | ntrancl_mapping (A1_, A2_) (Suc k) m = |
|
501 let |
|
502 val trclm = ntrancl_mapping (A1_, A2_) k m; |
|
503 in |
|
504 relcomp_mapping (A1_, A2_) trclm m trclm |
|
505 end; |
|
506 |
|
507 fun trancl_mapping (A1_, A2_) m = |
|
508 ntrancl_mapping (A1_, A2_) |
|
509 (minus_nat (card (equal_prod A1_ A1_) (keysa (linorder_prod A2_ A2_) m)) |
|
510 one_nat) |
|
511 m; |
|
512 |
|
513 fun is_in_leq leqm l = |
|
514 let |
|
515 val (x, y) = l; |
|
516 in |
|
517 (if equal_inta x y then SOME (Appt (PThm "refl", Var x)) |
|
518 else lookupa (linorder_prod linorder_int linorder_int) leqm l) |
|
519 end; |
|
520 |
|
521 fun is_in_eq leqm l = |
|
522 let |
|
523 val (x, y) = l; |
|
524 in |
|
525 (case (is_in_leq leqm (x, y), is_in_leq leqm (y, x)) of (NONE, _) => NONE |
|
526 | (SOME _, NONE) => NONE |
|
527 | (SOME p1, SOME p2) => |
|
528 SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "antisym") [p1, p2])) |
|
529 end; |
|
530 |
|
531 fun trm_of_oliteral (true, a) = trm_of_oatom a |
|
532 | trm_of_oliteral (false, a) = App (Const "Not", trm_of_oatom a); |
|
533 |
|
534 fun contr1_list leqm (false, LEQ (x, y)) = |
|
535 map_option |
|
536 (fn a => |
|
537 AppP (AppP (PThm "contr", Bound (trm_of_oliteral (false, LEQ (x, y)))), |
|
538 a)) |
|
539 (is_in_leq leqm (x, y)) |
|
540 | contr1_list leqm (false, EQ (x, y)) = |
|
541 map_option |
|
542 (fn a => |
|
543 AppP (AppP (PThm "contr", Bound (trm_of_oliteral (false, EQ (x, y)))), |
|
544 a)) |
|
545 (is_in_eq leqm (x, y)) |
|
546 | contr1_list uu (true, va) = NONE |
|
547 | contr1_list uu (v, LESS (vb, vc)) = NONE; |
|
548 |
|
549 fun contr_list_aux leqm [] = NONE |
|
550 | contr_list_aux leqm (l :: ls) = |
|
551 (case contr1_list leqm l of NONE => contr_list_aux leqm ls |
|
552 | SOME a => SOME a); |
|
553 |
|
554 fun leq1_member_list (true, LEQ (x, y)) = |
|
555 [((x, y), Bound (trm_of_oliteral (true, LEQ (x, y))))] |
|
556 | leq1_member_list (true, EQ (x, y)) = |
|
557 [((x, y), AppP (PThm "eqD1", Bound (trm_of_oliteral (true, EQ (x, y))))), |
|
558 ((y, x), AppP (PThm "eqD2", Bound (trm_of_oliteral (true, EQ (x, y)))))] |
|
559 | leq1_member_list (false, va) = [] |
|
560 | leq1_member_list (v, LESS (vb, vc)) = []; |
|
561 |
|
562 fun leq1_list a = maps leq1_member_list a; |
|
563 |
|
564 fun leq1_mapping a = |
|
565 of_alist (linorder_prod linorder_int linorder_int) (leq1_list a); |
|
566 |
|
567 fun contr_list a = |
|
568 contr_list_aux (trancl_mapping (equal_int, linorder_int) (leq1_mapping a)) a; |
|
569 |
|
570 fun contr_prf atom_conv phi = |
|
571 contr_fm_prf trm_of_oliteral contr_list (dnf_fm (amap_fm atom_conv phi)); |
|
572 |
|
573 fun amap_f_m_prf ap (Atom a) = AppP (PThm "atom_conv", ap a) |
|
574 | amap_f_m_prf ap (And (phi_1, phi_2)) = |
|
575 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
|
576 [AppP (PThm "arg_conv", |
|
577 hd [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2]), |
|
578 hd (tl [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2])] |
|
579 | amap_f_m_prf ap (Or (phi_1, phi_2)) = |
|
580 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
|
581 [AppP (PThm "arg_conv", |
|
582 hd [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2]), |
|
583 hd (tl [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2])] |
|
584 | amap_f_m_prf ap (Neg phi) = AppP (PThm "arg_conv", amap_f_m_prf ap phi); |
|
585 |
|
586 fun lo_contr_prf phi = |
|
587 map_option |
|
588 ((fn a => |
|
589 Conv (trm_of_fm trm_of_oliteral phi, amap_f_m_prf deneg_prf phi, a)) o |
|
590 (fn a => |
|
591 Conv (trm_of_fm trm_of_oliteral (amap_fm deneg phi), |
|
592 dnf_fm_prf (amap_fm deneg phi), a))) |
|
593 (contr_prf deneg phi); |
|
594 |
|
595 fun po_contr_prf phi = |
|
596 map_option |
|
597 ((fn a => |
|
598 Conv (trm_of_fm trm_of_oliteral phi, amap_f_m_prf deless_prf phi, a)) o |
|
599 (fn a => |
|
600 Conv (trm_of_fm trm_of_oliteral (amap_fm deless phi), |
|
601 dnf_fm_prf (amap_fm deless phi), a))) |
|
602 (contr_prf deless phi); |
|
603 |
|
604 end; (*struct Order_Procedure*) |