src/Provers/order_procedure.ML
changeset 74625 e6f0c9bf966c
parent 73526 a3cc9fa1295d
equal deleted inserted replaced
74624:c2bc0180151a 74625:e6f0c9bf966c
     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 
   285   rbt_lookup ((ord_preorder o preorder_order o order_linorder) A_)
   287   rbt_lookup ((ord_preorder o preorder_order o order_linorder) A_)
   286     (impl_of A_ x);
   288     (impl_of A_ x);
   287 
   289 
   288 fun member A_ [] y = false
   290 fun member A_ [] y = false
   289   | member A_ (x :: xs) y = eq A_ x y orelse member A_ xs y;
   291   | 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 
   292 
   296 fun remdups A_ [] = []
   293 fun remdups A_ [] = []
   297   | remdups A_ (x :: xs) =
   294   | remdups A_ (x :: xs) =
   298     (if member A_ xs x then remdups A_ xs else x :: remdups A_ xs);
   295     (if member A_ xs x then remdups A_ xs else x :: remdups A_ xs);
   299 
   296 
   318 fun dnf_fm (And (phi_1, phi_2)) = dnf_and_fm (dnf_fm phi_1) (dnf_fm phi_2)
   315 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)
   316   | dnf_fm (Or (phi_1, phi_2)) = Or (dnf_fm phi_1, dnf_fm phi_2)
   320   | dnf_fm (Atom v) = Atom v
   317   | dnf_fm (Atom v) = Atom v
   321   | dnf_fm (Neg v) = Neg v;
   318   | dnf_fm (Neg v) = Neg v;
   322 
   319 
       
   320 fun folda A_ f (Mapping t) a = fold A_ f t a;
       
   321 
   323 fun keysa A_ (Mapping t) = Set (keys A_ t);
   322 fun keysa A_ (Mapping t) = Set (keys A_ t);
   324 
   323 
   325 fun amap_fm h (Atom a) = h a
   324 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)
   325   | 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)
   326   | amap_fm h (Or (phi_1, phi_2)) = Or (amap_fm h phi_1, amap_fm h phi_2)
   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"
   395   | dnf_and_fm_prf (Neg v) (Neg va) = PThm "all_conv";
   384   | dnf_and_fm_prf (Neg v) (Neg va) = PThm "all_conv";
   396 
   385 
   397 fun dnf_fm_prf (And (phi_1, phi_2)) =
   386 fun dnf_fm_prf (And (phi_1, phi_2)) =
   398   foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
   387   foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
   399     [foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
   388     [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]),
   389        [AppP (PThm "arg_conv", 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)]
   390       dnf_and_fm_prf (dnf_fm phi_1) (dnf_fm phi_2)]
   403   | dnf_fm_prf (Or (phi_1, phi_2)) =
   391   | dnf_fm_prf (Or (phi_1, phi_2)) =
   404     foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
   392     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]),
   393       [AppP (PThm "arg_conv", 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"
   394   | dnf_fm_prf (Atom v) = PThm "all_conv"
   408   | dnf_fm_prf (Neg v) = PThm "all_conv";
   395   | dnf_fm_prf (Neg v) = PThm "all_conv";
   409 
   396 
   410 fun of_alist A_ xs = foldr (fn (a, b) => update A_ a b) xs (emptya A_);
   397 fun of_alist A_ xs = foldr (fn (a, b) => update A_ a b) xs (emptya A_);
   411 
   398 
   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