1 structure Order_Procedure : sig |
1 structure Order_Procedure : sig |
2 datatype int = Int_of_integer of IntInf.int |
2 datatype inta = Int_of_integer of int |
3 val integer_of_int : int -> IntInf.int |
3 val integer_of_int : inta -> int |
4 datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm | |
4 datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm | |
5 Neg of 'a fm |
5 Neg of 'a fm |
6 datatype trm = Const of string | App of trm * trm | Var of int |
6 datatype trm = Const of string | App of trm * trm | Var of inta |
7 datatype prf_trm = PThm of string | Appt of prf_trm * trm | |
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 | |
8 AppP of prf_trm * prf_trm | AbsP of trm * prf_trm | Bound of trm | |
9 Conv of trm * prf_trm * prf_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 |
10 datatype order_atom = EQ of inta * inta | LEQ of inta * inta | |
11 val lo_contr_prf : (bool * o_atom) fm -> prf_trm option |
11 LESS of inta * inta |
12 val po_contr_prf : (bool * o_atom) fm -> prf_trm option |
12 val lo_contr_prf : (bool * order_atom) fm -> prf_trm option |
|
13 val po_contr_prf : (bool * order_atom) fm -> prf_trm option |
13 end = struct |
14 end = struct |
14 |
15 |
15 datatype int = Int_of_integer of IntInf.int; |
16 datatype inta = Int_of_integer of int; |
16 |
17 |
17 fun integer_of_int (Int_of_integer k) = k; |
18 fun integer_of_int (Int_of_integer k) = k; |
18 |
19 |
19 fun equal_inta k l = (((integer_of_int k) : IntInf.int) = (integer_of_int l)); |
20 fun equal_inta k l = integer_of_int k = integer_of_int l; |
20 |
21 |
21 type 'a equal = {equal : 'a -> 'a -> bool}; |
22 type 'a equal = {equal : 'a -> 'a -> bool}; |
22 val equal = #equal : 'a equal -> 'a -> 'a -> bool; |
23 val equal = #equal : 'a equal -> 'a -> 'a -> bool; |
23 |
24 |
24 val equal_int = {equal = equal_inta} : int equal; |
25 val equal_int = {equal = equal_inta} : inta equal; |
25 |
26 |
26 fun less_eq_int k l = IntInf.<= (integer_of_int k, integer_of_int l); |
27 fun less_eq_int k l = integer_of_int k <= integer_of_int l; |
27 |
28 |
28 type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool}; |
29 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_eq = #less_eq : 'a ord -> 'a -> 'a -> bool; |
30 val less = #less : 'a ord -> 'a -> 'a -> bool; |
31 val less = #less : 'a ord -> 'a -> 'a -> bool; |
31 |
32 |
32 fun less_int k l = IntInf.< (integer_of_int k, integer_of_int l); |
33 fun less_int k l = integer_of_int k < integer_of_int l; |
33 |
34 |
34 val ord_int = {less_eq = less_eq_int, less = less_int} : int ord; |
35 val ord_int = {less_eq = less_eq_int, less = less_int} : inta ord; |
35 |
36 |
36 type 'a preorder = {ord_preorder : 'a ord}; |
37 type 'a preorder = {ord_preorder : 'a ord}; |
37 val ord_preorder = #ord_preorder : 'a preorder -> 'a ord; |
38 val ord_preorder = #ord_preorder : 'a preorder -> 'a ord; |
38 |
39 |
39 type 'a order = {preorder_order : 'a preorder}; |
40 type 'a order = {preorder_order : 'a preorder}; |
40 val preorder_order = #preorder_order : 'a order -> 'a preorder; |
41 val preorder_order = #preorder_order : 'a order -> 'a preorder; |
41 |
42 |
42 val preorder_int = {ord_preorder = ord_int} : int preorder; |
43 val preorder_int = {ord_preorder = ord_int} : inta preorder; |
43 |
44 |
44 val order_int = {preorder_order = preorder_int} : int order; |
45 val order_int = {preorder_order = preorder_int} : inta order; |
45 |
46 |
46 type 'a linorder = {order_linorder : 'a order}; |
47 type 'a linorder = {order_linorder : 'a order}; |
47 val order_linorder = #order_linorder : 'a linorder -> 'a order; |
48 val order_linorder = #order_linorder : 'a linorder -> 'a order; |
48 |
49 |
49 val linorder_int = {order_linorder = order_int} : int linorder; |
50 val linorder_int = {order_linorder = order_int} : inta linorder; |
50 |
51 |
51 fun eq A_ a b = equal A_ a b; |
52 fun eq A_ a b = equal A_ a b; |
52 |
53 |
53 fun equal_proda A_ B_ (x1, x2) (y1, y2) = eq A_ x1 y1 andalso eq B_ x2 y2; |
54 fun equal_proda A_ B_ (x1, x2) (y1, y2) = eq A_ x1 y1 andalso eq B_ x2 y2; |
54 |
55 |
87 datatype 'a set = Set of 'a list | Coset of 'a list; |
88 datatype 'a set = Set of 'a list | Coset of 'a list; |
88 |
89 |
89 datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm | |
90 datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm | |
90 Neg of 'a fm; |
91 Neg of 'a fm; |
91 |
92 |
92 datatype trm = Const of string | App of trm * trm | Var of int; |
93 datatype trm = Const of string | App of trm * trm | Var of inta; |
93 |
94 |
94 datatype prf_trm = PThm of string | Appt of prf_trm * trm | |
95 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 AppP of prf_trm * prf_trm | AbsP of trm * prf_trm | Bound of trm | |
96 Conv of trm * prf_trm * prf_trm; |
97 Conv of trm * prf_trm * prf_trm; |
97 |
98 |
98 datatype ('a, 'b) mapping = Mapping of ('a, 'b) rbt; |
99 datatype ('a, 'b) mapping = Mapping of ('a, 'b) rbt; |
99 |
100 |
100 datatype o_atom = EQ of int * int | LEQ of int * int | LESS of int * int; |
101 datatype order_atom = EQ of inta * inta | LEQ of inta * inta | |
|
102 LESS of inta * inta; |
101 |
103 |
102 fun id x = (fn xa => xa) x; |
104 fun id x = (fn xa => xa) x; |
103 |
105 |
104 fun impl_of B_ (RBT x) = x; |
106 fun impl_of B_ (RBT x) = x; |
105 |
107 |
106 fun folda f (Branch (c, lt, k, v, rt)) x = folda f rt (f k v (folda f lt x)) |
108 fun foldb f (Branch (c, lt, k, v, rt)) x = foldb f rt (f k v (foldb f lt x)) |
107 | folda f Empty x = x; |
109 | foldb f Empty x = x; |
108 |
110 |
109 fun fold A_ x xc = folda x (impl_of A_ xc); |
111 fun fold A_ x xc = foldb x (impl_of A_ xc); |
110 |
112 |
111 fun gen_keys kts (Branch (c, l, k, v, r)) = gen_keys ((k, r) :: kts) l |
113 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 |
114 | gen_keys ((k, t) :: kts) Empty = k :: gen_keys kts t |
113 | gen_keys [] Empty = []; |
115 | gen_keys [] Empty = []; |
114 |
116 |
352 |
351 |
353 fun dnf_and_fm_prf (Or (phi_1, phi_2)) psi = |
352 fun dnf_and_fm_prf (Or (phi_1, phi_2)) psi = |
354 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
353 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
355 [PThm "conj_disj_distribR_conv", |
354 [PThm "conj_disj_distribR_conv", |
356 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
355 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
357 [AppP (PThm "arg_conv", |
356 [AppP (PThm "arg_conv", dnf_and_fm_prf phi_1 psi), |
358 hd [dnf_and_fm_prf phi_1 psi, dnf_and_fm_prf phi_2 psi]), |
357 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)) = |
358 | dnf_and_fm_prf (Atom v) (Or (phi_1, phi_2)) = |
361 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
359 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
362 [PThm "conj_disj_distribL_conv", |
360 [PThm "conj_disj_distribL_conv", |
363 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
361 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
364 [AppP (PThm "arg_conv", |
362 [AppP (PThm "arg_conv", dnf_and_fm_prf (Atom v) phi_1), |
365 hd [dnf_and_fm_prf (Atom v) phi_1, |
363 dnf_and_fm_prf (Atom v) phi_2]] |
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)) = |
364 | dnf_and_fm_prf (And (v, va)) (Or (phi_1, phi_2)) = |
370 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
365 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
371 [PThm "conj_disj_distribL_conv", |
366 [PThm "conj_disj_distribL_conv", |
372 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
367 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
373 [AppP (PThm "arg_conv", |
368 [AppP (PThm "arg_conv", dnf_and_fm_prf (And (v, va)) phi_1), |
374 hd [dnf_and_fm_prf (And (v, va)) phi_1, |
369 dnf_and_fm_prf (And (v, va)) phi_2]] |
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)) = |
370 | dnf_and_fm_prf (Neg v) (Or (phi_1, phi_2)) = |
379 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
371 foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") |
380 [PThm "conj_disj_distribL_conv", |
372 [PThm "conj_disj_distribL_conv", |
381 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
373 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
382 [AppP (PThm "arg_conv", |
374 [AppP (PThm "arg_conv", dnf_and_fm_prf (Neg v) phi_1), |
383 hd [dnf_and_fm_prf (Neg v) phi_1, |
375 dnf_and_fm_prf (Neg v) phi_2]] |
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" |
376 | dnf_and_fm_prf (Atom v) (Atom va) = PThm "all_conv" |
388 | dnf_and_fm_prf (Atom v) (And (va, vb)) = PThm "all_conv" |
377 | dnf_and_fm_prf (Atom v) (And (va, vb)) = PThm "all_conv" |
389 | dnf_and_fm_prf (Atom v) (Neg va) = PThm "all_conv" |
378 | dnf_and_fm_prf (Atom v) (Neg va) = PThm "all_conv" |
390 | dnf_and_fm_prf (And (v, va)) (Atom vb) = PThm "all_conv" |
379 | 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" |
380 | dnf_and_fm_prf (And (v, va)) (And (vb, vc)) = PThm "all_conv" |
416 And (Atom (true, LEQ (y, x)), Atom (false, EQ (y, x))) |
403 And (Atom (true, LEQ (y, x)), Atom (false, EQ (y, x))) |
417 | deneg (false, EQ (v, vb)) = Atom (false, EQ (v, vb)) |
404 | deneg (false, EQ (v, vb)) = Atom (false, EQ (v, vb)) |
418 | deneg (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc)) |
405 | deneg (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc)) |
419 | deneg (true, LEQ (vb, vc)) = Atom (true, LEQ (vb, vc)); |
406 | deneg (true, LEQ (vb, vc)) = Atom (true, LEQ (vb, vc)); |
420 |
407 |
|
408 fun map_option f NONE = NONE |
|
409 | map_option f (SOME x2) = SOME (f x2); |
|
410 |
421 fun from_conj_prf trm_of_atom p (And (a, b)) = |
411 fun from_conj_prf trm_of_atom p (And (a, b)) = |
422 foldl (fn aa => fn ba => AppP (aa, ba)) (PThm "conjE") |
412 foldl (fn aa => fn ba => AppP (aa, ba)) (PThm "conjE") |
423 [Bound (trm_of_fm trm_of_atom (And (a, b))), |
413 [Bound (trm_of_fm trm_of_atom (And (a, b))), |
424 AbsP (trm_of_fm trm_of_atom a, |
414 AbsP (trm_of_fm trm_of_atom a, |
425 AbsP (trm_of_fm trm_of_atom b, |
415 AbsP (trm_of_fm trm_of_atom b, |
426 from_conj_prf trm_of_atom (from_conj_prf trm_of_atom p b) |
416 from_conj_prf trm_of_atom (from_conj_prf trm_of_atom p b) |
427 a))] |
417 a))] |
428 | from_conj_prf trm_of_atom p (Atom a) = p; |
418 | from_conj_prf trm_of_atom p (Atom a) = p; |
429 |
419 |
430 fun contr_fm_prf trm_of_atom contr_atom_prf (Or (c, d)) = |
420 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, |
421 (case contr_fm_prf trm_of_atom contr_atom_prf c of NONE => NONE |
432 contr_fm_prf trm_of_atom contr_atom_prf d) |
422 | SOME p1 => |
433 of (NONE, _) => NONE | (SOME _, NONE) => NONE |
423 map_option |
434 | (SOME p1, SOME p2) => |
424 (fn p2 => |
435 SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "disjE") |
425 foldl (fn a => fn b => AppP (a, b)) (PThm "disjE") |
436 [Bound (trm_of_fm trm_of_atom (Or (c, d))), |
426 [Bound (trm_of_fm trm_of_atom (Or (c, d))), |
437 AbsP (trm_of_fm trm_of_atom c, p1), |
427 AbsP (trm_of_fm trm_of_atom c, p1), |
438 AbsP (trm_of_fm trm_of_atom d, p2)])) |
428 AbsP (trm_of_fm trm_of_atom d, p2)]) |
|
429 (contr_fm_prf trm_of_atom contr_atom_prf d)) |
439 | contr_fm_prf trm_of_atom contr_atom_prf (And (a, b)) = |
430 | 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 |
431 (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)))) |
432 | 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]; |
433 | contr_fm_prf trm_of_atom contr_atom_prf (Atom a) = contr_atom_prf [a]; |
443 |
434 |
448 | deless (false, EQ (v, vb)) = Atom (false, EQ (v, vb)) |
439 | deless (false, EQ (v, vb)) = Atom (false, EQ (v, vb)) |
449 | deless (false, LEQ (v, vb)) = Atom (false, LEQ (v, vb)) |
440 | deless (false, LEQ (v, vb)) = Atom (false, LEQ (v, vb)) |
450 | deless (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc)) |
441 | deless (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc)) |
451 | deless (v, LEQ (vb, vc)) = Atom (v, LEQ (vb, vc)); |
442 | deless (v, LEQ (vb, vc)) = Atom (v, LEQ (vb, vc)); |
452 |
443 |
|
444 fun fst (x1, x2) = x1; |
|
445 |
|
446 fun snd (x1, x2) = x2; |
|
447 |
453 fun deneg_prf (true, LESS (x, y)) = PThm "less_le" |
448 fun deneg_prf (true, LESS (x, y)) = PThm "less_le" |
454 | deneg_prf (false, LESS (x, y)) = PThm "nless_le" |
449 | deneg_prf (false, LESS (x, y)) = PThm "nless_le" |
455 | deneg_prf (false, LEQ (x, y)) = PThm "nle_le" |
450 | deneg_prf (false, LEQ (x, y)) = PThm "nle_le" |
456 | deneg_prf (false, EQ (v, vb)) = PThm "all_conv" |
451 | deneg_prf (false, EQ (v, vb)) = PThm "all_conv" |
457 | deneg_prf (v, EQ (vb, vc)) = PThm "all_conv" |
452 | deneg_prf (v, EQ (vb, vc)) = PThm "all_conv" |
458 | deneg_prf (true, LEQ (vb, vc)) = PThm "all_conv"; |
453 | deneg_prf (true, LEQ (vb, vc)) = PThm "all_conv"; |
459 |
454 |
460 val one_nat : nat = Suc Zero_nat; |
455 val one_nat : nat = Suc Zero_nat; |
461 |
456 |
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" |
457 fun deless_prf (true, LESS (x, y)) = PThm "less_le" |
466 | deless_prf (false, LESS (x, y)) = PThm "nless_le" |
458 | deless_prf (false, LESS (x, y)) = PThm "nless_le" |
467 | deless_prf (false, EQ (v, vb)) = PThm "all_conv" |
459 | deless_prf (false, EQ (v, vb)) = PThm "all_conv" |
468 | deless_prf (false, LEQ (v, vb)) = PThm "all_conv" |
460 | deless_prf (false, LEQ (v, vb)) = PThm "all_conv" |
469 | deless_prf (v, EQ (vb, vc)) = PThm "all_conv" |
461 | deless_prf (v, EQ (vb, vc)) = PThm "all_conv" |
470 | deless_prf (v, LEQ (vb, vc)) = PThm "all_conv"; |
462 | deless_prf (v, LEQ (vb, vc)) = PThm "all_conv"; |
471 |
463 |
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 |
464 fun minus_nat (Suc m) (Suc n) = minus_nat m n |
477 | minus_nat Zero_nat n = Zero_nat |
465 | minus_nat Zero_nat n = Zero_nat |
478 | minus_nat m Zero_nat = m; |
466 | minus_nat m Zero_nat = m; |
479 |
467 |
480 fun mapping_fold A_ f (Mapping t) a = fold A_ f t a; |
468 fun relcomp1_mapping B_ (C1_, C2_) combine x y1 pxy pm pma = |
481 |
469 folda (linorder_prod C2_ C2_) |
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 => |
470 (fn (y2, z) => fn pyz => fn pmb => |
485 (if eq B1_ y1 y2 andalso not (eq B1_ y2 z) |
471 (if eq C1_ y1 y2 andalso not (eq C1_ y2 z) |
486 then update (linorder_prod A_ B2_) (x, z) |
472 then update (linorder_prod B_ C2_) (x, z) (combine pxy pyz) pmb |
487 (foldl (fn a => fn b => AppP (a, b)) (PThm "trans") [pxy, pyz]) |
|
488 pmb |
|
489 else pmb)) |
473 else pmb)) |
490 pm pma; |
474 pm pma; |
491 |
475 |
492 fun relcomp_mapping (A1_, A2_) pm1 pm2 pma = |
476 fun relcomp_mapping (B1_, B2_) combine pm1 pm2 pma = |
493 mapping_fold (linorder_prod A2_ A2_) |
477 folda (linorder_prod B2_ B2_) |
494 (fn (x, y) => fn pxy => fn pm => |
478 (fn (x, y) => fn pxy => fn pm => |
495 (if eq A1_ x y then pm |
479 (if eq B1_ x y then pm |
496 else relcomp1_mapping A2_ (A1_, A2_) x y pxy pm2 pm)) |
480 else relcomp1_mapping B2_ (B1_, B2_) combine x y pxy pm2 pm)) |
497 pm1 pma; |
481 pm1 pma; |
498 |
482 |
499 fun ntrancl_mapping (A1_, A2_) Zero_nat m = m |
483 fun ntrancl_mapping (B1_, B2_) combine Zero_nat m = m |
500 | ntrancl_mapping (A1_, A2_) (Suc k) m = |
484 | ntrancl_mapping (B1_, B2_) combine (Suc k) m = |
501 let |
485 let |
502 val trclm = ntrancl_mapping (A1_, A2_) k m; |
486 val trclm = ntrancl_mapping (B1_, B2_) combine k m; |
503 in |
487 in |
504 relcomp_mapping (A1_, A2_) trclm m trclm |
488 relcomp_mapping (B1_, B2_) combine trclm m trclm |
505 end; |
489 end; |
506 |
490 |
507 fun trancl_mapping (A1_, A2_) m = |
491 fun trancl_mapping (B1_, B2_) combine m = |
508 ntrancl_mapping (A1_, A2_) |
492 ntrancl_mapping (B1_, B2_) combine |
509 (minus_nat (card (equal_prod A1_ A1_) (keysa (linorder_prod A2_ A2_) m)) |
493 (minus_nat (card (equal_prod B1_ B1_) (keysa (linorder_prod B2_ B2_) m)) |
510 one_nat) |
494 one_nat) |
511 m; |
495 m; |
512 |
496 |
|
497 fun trm_of_order_atom (EQ (x, y)) = App (App (Const "eq", Var x), Var y) |
|
498 | trm_of_order_atom (LEQ (x, y)) = App (App (Const "le", Var x), Var y) |
|
499 | trm_of_order_atom (LESS (x, y)) = App (App (Const "lt", Var x), Var y); |
|
500 |
|
501 fun trm_of_order_literal (true, a) = trm_of_order_atom a |
|
502 | trm_of_order_literal (false, a) = App (Const "Not", trm_of_order_atom a); |
|
503 |
513 fun is_in_leq leqm l = |
504 fun is_in_leq leqm l = |
514 let |
505 (if equal_inta (fst l) (snd l) then SOME (Appt (PThm "refl", Var (fst l))) |
515 val (x, y) = l; |
506 else lookupa (linorder_prod linorder_int linorder_int) leqm 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 |
507 |
521 fun is_in_eq leqm l = |
508 fun is_in_eq leqm l = |
522 let |
509 (case (is_in_leq leqm l, is_in_leq leqm (snd l, fst l)) of (NONE, _) => NONE |
523 val (x, y) = l; |
510 | (SOME _, NONE) => NONE |
524 in |
511 | (SOME p1, SOME p2) => |
525 (case (is_in_leq leqm (x, y), is_in_leq leqm (y, x)) of (NONE, _) => NONE |
512 SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "antisym") [p1, p2])); |
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 |
513 |
534 fun contr1_list leqm (false, LEQ (x, y)) = |
514 fun contr1_list leqm (false, LEQ (x, y)) = |
535 map_option |
515 map_option |
536 (fn a => |
516 (fn a => |
537 AppP (AppP (PThm "contr", Bound (trm_of_oliteral (false, LEQ (x, y)))), |
517 AppP (AppP (PThm "contr", |
|
518 Bound (trm_of_order_literal (false, LEQ (x, y)))), |
538 a)) |
519 a)) |
539 (is_in_leq leqm (x, y)) |
520 (is_in_leq leqm (x, y)) |
540 | contr1_list leqm (false, EQ (x, y)) = |
521 | contr1_list leqm (false, EQ (x, y)) = |
541 map_option |
522 map_option |
542 (fn a => |
523 (fn a => |
543 AppP (AppP (PThm "contr", Bound (trm_of_oliteral (false, EQ (x, y)))), |
524 AppP (AppP (PThm "contr", |
|
525 Bound (trm_of_order_literal (false, EQ (x, y)))), |
544 a)) |
526 a)) |
545 (is_in_eq leqm (x, y)) |
527 (is_in_eq leqm (x, y)) |
546 | contr1_list uu (true, va) = NONE |
528 | contr1_list uu (true, va) = NONE |
547 | contr1_list uu (v, LESS (vb, vc)) = NONE; |
529 | contr1_list uu (v, LESS (vb, vc)) = NONE; |
548 |
530 |
550 | contr_list_aux leqm (l :: ls) = |
532 | contr_list_aux leqm (l :: ls) = |
551 (case contr1_list leqm l of NONE => contr_list_aux leqm ls |
533 (case contr1_list leqm l of NONE => contr_list_aux leqm ls |
552 | SOME a => SOME a); |
534 | SOME a => SOME a); |
553 |
535 |
554 fun leq1_member_list (true, LEQ (x, y)) = |
536 fun leq1_member_list (true, LEQ (x, y)) = |
555 [((x, y), Bound (trm_of_oliteral (true, LEQ (x, y))))] |
537 [((x, y), Bound (trm_of_order_literal (true, LEQ (x, y))))] |
556 | leq1_member_list (true, EQ (x, y)) = |
538 | leq1_member_list (true, EQ (x, y)) = |
557 [((x, y), AppP (PThm "eqD1", Bound (trm_of_oliteral (true, EQ (x, y))))), |
539 [((x, y), |
558 ((y, x), AppP (PThm "eqD2", Bound (trm_of_oliteral (true, EQ (x, y)))))] |
540 AppP (PThm "eqD1", Bound (trm_of_order_literal (true, EQ (x, y))))), |
|
541 ((y, x), |
|
542 AppP (PThm "eqD2", Bound (trm_of_order_literal (true, EQ (x, y)))))] |
559 | leq1_member_list (false, va) = [] |
543 | leq1_member_list (false, va) = [] |
560 | leq1_member_list (v, LESS (vb, vc)) = []; |
544 | leq1_member_list (v, LESS (vb, vc)) = []; |
561 |
545 |
562 fun leq1_list a = maps leq1_member_list a; |
546 fun leq1_list a = maps leq1_member_list a; |
563 |
547 |
564 fun leq1_mapping a = |
548 fun leq1_mapping a = |
565 of_alist (linorder_prod linorder_int linorder_int) (leq1_list a); |
549 of_alist (linorder_prod linorder_int linorder_int) (leq1_list a); |
566 |
550 |
567 fun contr_list a = |
551 fun contr_list a = |
568 contr_list_aux (trancl_mapping (equal_int, linorder_int) (leq1_mapping a)) a; |
552 contr_list_aux |
|
553 (trancl_mapping (equal_int, linorder_int) |
|
554 (fn p1 => fn p2 => |
|
555 foldl (fn aa => fn b => AppP (aa, b)) (PThm "trans") [p1, p2]) |
|
556 (leq1_mapping a)) |
|
557 a; |
569 |
558 |
570 fun contr_prf atom_conv phi = |
559 fun contr_prf atom_conv phi = |
571 contr_fm_prf trm_of_oliteral contr_list (dnf_fm (amap_fm atom_conv phi)); |
560 contr_fm_prf trm_of_order_literal contr_list (dnf_fm (amap_fm atom_conv phi)); |
572 |
561 |
573 fun amap_f_m_prf ap (Atom a) = AppP (PThm "atom_conv", ap a) |
562 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)) = |
563 | amap_f_m_prf ap (And (phi_1, phi_2)) = |
575 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
564 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
576 [AppP (PThm "arg_conv", |
565 [AppP (PThm "arg_conv", amap_f_m_prf ap phi_1), amap_f_m_prf ap phi_2] |
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)) = |
566 | amap_f_m_prf ap (Or (phi_1, phi_2)) = |
580 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
567 foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") |
581 [AppP (PThm "arg_conv", |
568 [AppP (PThm "arg_conv", amap_f_m_prf ap phi_1), amap_f_m_prf ap phi_2] |
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); |
569 | amap_f_m_prf ap (Neg phi) = AppP (PThm "arg_conv", amap_f_m_prf ap phi); |
585 |
570 |
586 fun lo_contr_prf phi = |
571 fun lo_contr_prf phi = |
587 map_option |
572 map_option |
588 ((fn a => |
573 ((fn a => |
589 Conv (trm_of_fm trm_of_oliteral phi, amap_f_m_prf deneg_prf phi, a)) o |
574 Conv (trm_of_fm trm_of_order_literal phi, amap_f_m_prf deneg_prf phi, |
|
575 a)) o |
590 (fn a => |
576 (fn a => |
591 Conv (trm_of_fm trm_of_oliteral (amap_fm deneg phi), |
577 Conv (trm_of_fm trm_of_order_literal (amap_fm deneg phi), |
592 dnf_fm_prf (amap_fm deneg phi), a))) |
578 dnf_fm_prf (amap_fm deneg phi), a))) |
593 (contr_prf deneg phi); |
579 (contr_prf deneg phi); |
594 |
580 |
595 fun po_contr_prf phi = |
581 fun po_contr_prf phi = |
596 map_option |
582 map_option |
597 ((fn a => |
583 ((fn a => |
598 Conv (trm_of_fm trm_of_oliteral phi, amap_f_m_prf deless_prf phi, a)) o |
584 Conv (trm_of_fm trm_of_order_literal phi, amap_f_m_prf deless_prf phi, |
|
585 a)) o |
599 (fn a => |
586 (fn a => |
600 Conv (trm_of_fm trm_of_oliteral (amap_fm deless phi), |
587 Conv (trm_of_fm trm_of_order_literal (amap_fm deless phi), |
601 dnf_fm_prf (amap_fm deless phi), a))) |
588 dnf_fm_prf (amap_fm deless phi), a))) |
602 (contr_prf deless phi); |
589 (contr_prf deless phi); |
603 |
590 |
604 end; (*struct Order_Procedure*) |
591 end; (*struct Order_Procedure*) |
|
592 |