diff --git a/src/Provers/order_procedure.ML b/src/Provers/order_procedure.ML --- a/src/Provers/order_procedure.ML +++ b/src/Provers/order_procedure.ML @@ -1,604 +1,592 @@ structure Order_Procedure : sig - datatype int = Int_of_integer of IntInf.int - val integer_of_int : int -> IntInf.int + datatype inta = Int_of_integer of int + val integer_of_int : inta -> int datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm | Neg of 'a fm - datatype trm = Const of string | App of trm * trm | Var of int + datatype trm = Const of string | App of trm * trm | Var of inta datatype prf_trm = PThm of string | Appt of prf_trm * trm | AppP of prf_trm * prf_trm | AbsP of trm * prf_trm | Bound of trm | Conv of trm * prf_trm * prf_trm - datatype o_atom = EQ of int * int | LEQ of int * int | LESS of int * int - val lo_contr_prf : (bool * o_atom) fm -> prf_trm option - val po_contr_prf : (bool * o_atom) fm -> prf_trm option + datatype order_atom = EQ of inta * inta | LEQ of inta * inta | + LESS of inta * inta + val lo_contr_prf : (bool * order_atom) fm -> prf_trm option + val po_contr_prf : (bool * order_atom) fm -> prf_trm option end = struct -datatype int = Int_of_integer of IntInf.int; +datatype inta = Int_of_integer of int; fun integer_of_int (Int_of_integer k) = k; -fun equal_inta k l = (((integer_of_int k) : IntInf.int) = (integer_of_int l)); +fun equal_inta k l = integer_of_int k = integer_of_int l; type 'a equal = {equal : 'a -> 'a -> bool}; val equal = #equal : 'a equal -> 'a -> 'a -> bool; -val equal_int = {equal = equal_inta} : int equal; +val equal_int = {equal = equal_inta} : inta equal; -fun less_eq_int k l = IntInf.<= (integer_of_int k, integer_of_int l); +fun less_eq_int k l = integer_of_int k <= integer_of_int l; type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool}; val less_eq = #less_eq : 'a ord -> 'a -> 'a -> bool; val less = #less : 'a ord -> 'a -> 'a -> bool; -fun less_int k l = IntInf.< (integer_of_int k, integer_of_int l); +fun less_int k l = integer_of_int k < integer_of_int l; -val ord_int = {less_eq = less_eq_int, less = less_int} : int ord; +val ord_int = {less_eq = less_eq_int, less = less_int} : inta ord; type 'a preorder = {ord_preorder : 'a ord}; val ord_preorder = #ord_preorder : 'a preorder -> 'a ord; type 'a order = {preorder_order : 'a preorder}; val preorder_order = #preorder_order : 'a order -> 'a preorder; -val preorder_int = {ord_preorder = ord_int} : int preorder; +val preorder_int = {ord_preorder = ord_int} : inta preorder; -val order_int = {preorder_order = preorder_int} : int order; +val order_int = {preorder_order = preorder_int} : inta order; type 'a linorder = {order_linorder : 'a order}; val order_linorder = #order_linorder : 'a linorder -> 'a order; -val linorder_int = {order_linorder = order_int} : int linorder; +val linorder_int = {order_linorder = order_int} : inta linorder; fun eq A_ a b = equal A_ a b; fun equal_proda A_ B_ (x1, x2) (y1, y2) = eq A_ x1 y1 andalso eq B_ x2 y2; fun equal_prod A_ B_ = {equal = equal_proda A_ B_} : ('a * 'b) equal; fun less_eq_prod A_ B_ (x1, y1) (x2, y2) = less A_ x1 x2 orelse less_eq A_ x1 x2 andalso less_eq B_ y1 y2; fun less_prod A_ B_ (x1, y1) (x2, y2) = less A_ x1 x2 orelse less_eq A_ x1 x2 andalso less B_ y1 y2; fun ord_prod A_ B_ = {less_eq = less_eq_prod A_ B_, less = less_prod A_ B_} : ('a * 'b) ord; fun preorder_prod A_ B_ = {ord_preorder = ord_prod (ord_preorder A_) (ord_preorder B_)} : ('a * 'b) preorder; fun order_prod A_ B_ = {preorder_order = preorder_prod (preorder_order A_) (preorder_order B_)} : ('a * 'b) order; fun linorder_prod A_ B_ = {order_linorder = order_prod (order_linorder A_) (order_linorder B_)} : ('a * 'b) linorder; datatype nat = Zero_nat | Suc of nat; datatype color = R | B; datatype ('a, 'b) rbta = Empty | Branch of color * ('a, 'b) rbta * 'a * 'b * ('a, 'b) rbta; datatype ('b, 'a) rbt = RBT of ('b, 'a) rbta; datatype 'a set = Set of 'a list | Coset of 'a list; datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm | Neg of 'a fm; -datatype trm = Const of string | App of trm * trm | Var of int; +datatype trm = Const of string | App of trm * trm | Var of inta; datatype prf_trm = PThm of string | Appt of prf_trm * trm | AppP of prf_trm * prf_trm | AbsP of trm * prf_trm | Bound of trm | Conv of trm * prf_trm * prf_trm; datatype ('a, 'b) mapping = Mapping of ('a, 'b) rbt; -datatype o_atom = EQ of int * int | LEQ of int * int | LESS of int * int; +datatype order_atom = EQ of inta * inta | LEQ of inta * inta | + LESS of inta * inta; fun id x = (fn xa => xa) x; fun impl_of B_ (RBT x) = x; -fun folda f (Branch (c, lt, k, v, rt)) x = folda f rt (f k v (folda f lt x)) - | folda f Empty x = x; +fun foldb f (Branch (c, lt, k, v, rt)) x = foldb f rt (f k v (foldb f lt x)) + | foldb f Empty x = x; -fun fold A_ x xc = folda x (impl_of A_ xc); +fun fold A_ x xc = foldb x (impl_of A_ xc); fun gen_keys kts (Branch (c, l, k, v, r)) = gen_keys ((k, r) :: kts) l | gen_keys ((k, t) :: kts) Empty = k :: gen_keys kts t | gen_keys [] Empty = []; fun keysb x = gen_keys [] x; fun keys A_ x = keysb (impl_of A_ x); fun maps f [] = [] | maps f (x :: xs) = f x @ maps f xs; fun empty A_ = RBT Empty; fun foldl f a [] = a | foldl f a (x :: xs) = foldl f (f a x) xs; fun foldr f [] = id | foldr f (x :: xs) = f x o foldr f xs; fun balance (Branch (R, a, w, x, b)) s t (Branch (R, c, y, z, d)) = Branch (R, Branch (B, a, w, x, b), s, t, Branch (B, c, y, z, d)) | balance (Branch (R, Branch (R, a, w, x, b), s, t, c)) y z Empty = Branch (R, Branch (B, a, w, x, b), s, t, Branch (B, c, y, z, Empty)) | balance (Branch (R, Branch (R, a, w, x, b), s, t, c)) y z (Branch (B, va, vb, vc, vd)) = Branch (R, Branch (B, a, w, x, b), s, t, Branch (B, c, y, z, Branch (B, va, vb, vc, vd))) | balance (Branch (R, Empty, w, x, Branch (R, b, s, t, c))) y z Empty = Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, Empty)) | balance (Branch (R, Branch (B, va, vb, vc, vd), w, x, Branch (R, b, s, t, c))) y z Empty = Branch (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t, Branch (B, c, y, z, Empty)) | balance (Branch (R, Empty, w, x, Branch (R, b, s, t, c))) y z (Branch (B, va, vb, vc, vd)) = Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, Branch (B, va, vb, vc, vd))) | balance (Branch (R, Branch (B, ve, vf, vg, vh), w, x, Branch (R, b, s, t, c))) y z (Branch (B, va, vb, vc, vd)) = Branch (R, Branch (B, Branch (B, ve, vf, vg, vh), w, x, b), s, t, Branch (B, c, y, z, Branch (B, va, vb, vc, vd))) | balance Empty w x (Branch (R, b, s, t, Branch (R, c, y, z, d))) = Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, d)) | balance (Branch (B, va, vb, vc, vd)) w x (Branch (R, b, s, t, Branch (R, c, y, z, d))) = Branch (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t, Branch (B, c, y, z, d)) | balance Empty w x (Branch (R, Branch (R, b, s, t, c), y, z, Empty)) = Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, Empty)) | balance Empty w x (Branch (R, Branch (R, b, s, t, c), y, z, Branch (B, va, vb, vc, vd))) = Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, Branch (B, va, vb, vc, vd))) | balance (Branch (B, va, vb, vc, vd)) w x (Branch (R, Branch (R, b, s, t, c), y, z, Empty)) = Branch (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t, Branch (B, c, y, z, Empty)) | balance (Branch (B, va, vb, vc, vd)) w x (Branch (R, Branch (R, b, s, t, c), y, z, Branch (B, ve, vf, vg, vh))) = Branch (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t, Branch (B, c, y, z, Branch (B, ve, vf, vg, vh))) | balance Empty s t Empty = Branch (B, Empty, s, t, Empty) | balance Empty s t (Branch (B, va, vb, vc, vd)) = Branch (B, Empty, s, t, Branch (B, va, vb, vc, vd)) | balance Empty s t (Branch (v, Empty, vb, vc, Empty)) = Branch (B, Empty, s, t, Branch (v, Empty, vb, vc, Empty)) | balance Empty s t (Branch (v, Branch (B, ve, vf, vg, vh), vb, vc, Empty)) = Branch (B, Empty, s, t, Branch (v, Branch (B, ve, vf, vg, vh), vb, vc, Empty)) | balance Empty s t (Branch (v, Empty, vb, vc, Branch (B, vf, vg, vh, vi))) = Branch (B, Empty, s, t, Branch (v, Empty, vb, vc, Branch (B, vf, vg, vh, vi))) | balance Empty s t (Branch (v, Branch (B, ve, vj, vk, vl), vb, vc, Branch (B, vf, vg, vh, vi))) = Branch (B, Empty, s, t, Branch (v, Branch (B, ve, vj, vk, vl), vb, vc, Branch (B, vf, vg, vh, vi))) | balance (Branch (B, va, vb, vc, vd)) s t Empty = Branch (B, Branch (B, va, vb, vc, vd), s, t, Empty) | balance (Branch (B, va, vb, vc, vd)) s t (Branch (B, ve, vf, vg, vh)) = Branch (B, Branch (B, va, vb, vc, vd), s, t, Branch (B, ve, vf, vg, vh)) | balance (Branch (B, va, vb, vc, vd)) s t (Branch (v, Empty, vf, vg, Empty)) = Branch (B, Branch (B, va, vb, vc, vd), s, t, Branch (v, Empty, vf, vg, Empty)) | balance (Branch (B, va, vb, vc, vd)) s t (Branch (v, Branch (B, vi, vj, vk, vl), vf, vg, Empty)) = Branch (B, Branch (B, va, vb, vc, vd), s, t, Branch (v, Branch (B, vi, vj, vk, vl), vf, vg, Empty)) | balance (Branch (B, va, vb, vc, vd)) s t (Branch (v, Empty, vf, vg, Branch (B, vj, vk, vl, vm))) = Branch (B, Branch (B, va, vb, vc, vd), s, t, Branch (v, Empty, vf, vg, Branch (B, vj, vk, vl, vm))) | balance (Branch (B, va, vb, vc, vd)) s t (Branch (v, Branch (B, vi, vn, vo, vp), vf, vg, Branch (B, vj, vk, vl, vm))) = Branch (B, Branch (B, va, vb, vc, vd), s, t, Branch (v, Branch (B, vi, vn, vo, vp), vf, vg, Branch (B, vj, vk, vl, vm))) | balance (Branch (v, Empty, vb, vc, Empty)) s t Empty = Branch (B, Branch (v, Empty, vb, vc, Empty), s, t, Empty) | balance (Branch (v, Empty, vb, vc, Branch (B, ve, vf, vg, vh))) s t Empty = Branch (B, Branch (v, Empty, vb, vc, Branch (B, ve, vf, vg, vh)), s, t, Empty) | balance (Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Empty)) s t Empty = Branch (B, Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Empty), s, t, Empty) | balance (Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Branch (B, ve, vj, vk, vl))) s t Empty = Branch (B, Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Branch (B, ve, vj, vk, vl)), s, t, Empty) | balance (Branch (v, Empty, vf, vg, Empty)) s t (Branch (B, va, vb, vc, vd)) = Branch (B, Branch (v, Empty, vf, vg, Empty), s, t, Branch (B, va, vb, vc, vd)) | balance (Branch (v, Empty, vf, vg, Branch (B, vi, vj, vk, vl))) s t (Branch (B, va, vb, vc, vd)) = Branch (B, Branch (v, Empty, vf, vg, Branch (B, vi, vj, vk, vl)), s, t, Branch (B, va, vb, vc, vd)) | balance (Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Empty)) s t (Branch (B, va, vb, vc, vd)) = Branch (B, Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Empty), s, t, Branch (B, va, vb, vc, vd)) | balance (Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Branch (B, vi, vn, vo, vp))) s t (Branch (B, va, vb, vc, vd)) = Branch (B, Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Branch (B, vi, vn, vo, vp)), s, t, Branch (B, va, vb, vc, vd)); fun rbt_ins A_ f k v Empty = Branch (R, Empty, k, v, Empty) | rbt_ins A_ f k v (Branch (B, l, x, y, r)) = (if less A_ k x then balance (rbt_ins A_ f k v l) x y r else (if less A_ x k then balance l x y (rbt_ins A_ f k v r) else Branch (B, l, x, f k y v, r))) | rbt_ins A_ f k v (Branch (R, l, x, y, r)) = (if less A_ k x then Branch (R, rbt_ins A_ f k v l, x, y, r) else (if less A_ x k then Branch (R, l, x, y, rbt_ins A_ f k v r) else Branch (R, l, x, f k y v, r))); fun paint c Empty = Empty | paint c (Branch (uu, l, k, v, r)) = Branch (c, l, k, v, r); fun rbt_insert_with_key A_ f k v t = paint B (rbt_ins A_ f k v t); fun rbt_insert A_ = rbt_insert_with_key A_ (fn _ => fn _ => fn nv => nv); fun insert A_ xc xd xe = RBT (rbt_insert ((ord_preorder o preorder_order o order_linorder) A_) xc xd (impl_of A_ xe)); fun rbt_lookup A_ Empty k = NONE | rbt_lookup A_ (Branch (uu, l, x, y, r)) k = (if less A_ k x then rbt_lookup A_ l k else (if less A_ x k then rbt_lookup A_ r k else SOME y)); fun lookup A_ x = rbt_lookup ((ord_preorder o preorder_order o order_linorder) A_) (impl_of A_ x); fun member A_ [] y = false | member A_ (x :: xs) y = eq A_ x y orelse member A_ xs y; -fun hd (x21 :: x22) = x21; - -fun tl [] = [] - | tl (x21 :: x22) = x22; - fun remdups A_ [] = [] | remdups A_ (x :: xs) = (if member A_ xs x then remdups A_ xs else x :: remdups A_ xs); fun dnf_and_fm (Or (phi_1, phi_2)) psi = Or (dnf_and_fm phi_1 psi, dnf_and_fm phi_2 psi) | dnf_and_fm (Atom v) (Or (phi_1, phi_2)) = Or (dnf_and_fm (Atom v) phi_1, dnf_and_fm (Atom v) phi_2) | dnf_and_fm (And (v, va)) (Or (phi_1, phi_2)) = Or (dnf_and_fm (And (v, va)) phi_1, dnf_and_fm (And (v, va)) phi_2) | dnf_and_fm (Neg v) (Or (phi_1, phi_2)) = Or (dnf_and_fm (Neg v) phi_1, dnf_and_fm (Neg v) phi_2) | dnf_and_fm (Atom v) (Atom va) = And (Atom v, Atom va) | dnf_and_fm (Atom v) (And (va, vb)) = And (Atom v, And (va, vb)) | dnf_and_fm (Atom v) (Neg va) = And (Atom v, Neg va) | dnf_and_fm (And (v, va)) (Atom vb) = And (And (v, va), Atom vb) | dnf_and_fm (And (v, va)) (And (vb, vc)) = And (And (v, va), And (vb, vc)) | dnf_and_fm (And (v, va)) (Neg vb) = And (And (v, va), Neg vb) | dnf_and_fm (Neg v) (Atom va) = And (Neg v, Atom va) | dnf_and_fm (Neg v) (And (va, vb)) = And (Neg v, And (va, vb)) | dnf_and_fm (Neg v) (Neg va) = And (Neg v, Neg va); fun dnf_fm (And (phi_1, phi_2)) = dnf_and_fm (dnf_fm phi_1) (dnf_fm phi_2) | dnf_fm (Or (phi_1, phi_2)) = Or (dnf_fm phi_1, dnf_fm phi_2) | dnf_fm (Atom v) = Atom v | dnf_fm (Neg v) = Neg v; +fun folda A_ f (Mapping t) a = fold A_ f t a; + fun keysa A_ (Mapping t) = Set (keys A_ t); fun amap_fm h (Atom a) = h a | amap_fm h (And (phi_1, phi_2)) = And (amap_fm h phi_1, amap_fm h phi_2) | amap_fm h (Or (phi_1, phi_2)) = Or (amap_fm h phi_1, amap_fm h phi_2) | amap_fm h (Neg phi) = Neg (amap_fm h phi); fun emptya A_ = Mapping (empty A_); fun lookupa A_ (Mapping t) = lookup A_ t; fun update A_ k v (Mapping t) = Mapping (insert A_ k v t); fun gen_length n (x :: xs) = gen_length (Suc n) xs | gen_length n [] = n; fun size_list x = gen_length Zero_nat x; fun card A_ (Set xs) = size_list (remdups A_ xs); fun conj_list (And (phi_1, phi_2)) = conj_list phi_1 @ conj_list phi_2 | conj_list (Atom a) = [a]; fun trm_of_fm f (Atom a) = f a | trm_of_fm f (And (phi_1, phi_2)) = App (App (Const "conj", trm_of_fm f phi_1), trm_of_fm f phi_2) | trm_of_fm f (Or (phi_1, phi_2)) = App (App (Const "disj", trm_of_fm f phi_1), trm_of_fm f phi_2) | trm_of_fm f (Neg phi) = App (Const "Not", trm_of_fm f phi); fun dnf_and_fm_prf (Or (phi_1, phi_2)) psi = foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") [PThm "conj_disj_distribR_conv", foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") - [AppP (PThm "arg_conv", - hd [dnf_and_fm_prf phi_1 psi, dnf_and_fm_prf phi_2 psi]), - hd (tl [dnf_and_fm_prf phi_1 psi, dnf_and_fm_prf phi_2 psi])]] + [AppP (PThm "arg_conv", dnf_and_fm_prf phi_1 psi), + dnf_and_fm_prf phi_2 psi]] | dnf_and_fm_prf (Atom v) (Or (phi_1, phi_2)) = foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") [PThm "conj_disj_distribL_conv", foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") - [AppP (PThm "arg_conv", - hd [dnf_and_fm_prf (Atom v) phi_1, - dnf_and_fm_prf (Atom v) phi_2]), - hd (tl [dnf_and_fm_prf (Atom v) phi_1, - dnf_and_fm_prf (Atom v) phi_2])]] + [AppP (PThm "arg_conv", dnf_and_fm_prf (Atom v) phi_1), + dnf_and_fm_prf (Atom v) phi_2]] | dnf_and_fm_prf (And (v, va)) (Or (phi_1, phi_2)) = foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") [PThm "conj_disj_distribL_conv", foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") - [AppP (PThm "arg_conv", - hd [dnf_and_fm_prf (And (v, va)) phi_1, - dnf_and_fm_prf (And (v, va)) phi_2]), - hd (tl [dnf_and_fm_prf (And (v, va)) phi_1, - dnf_and_fm_prf (And (v, va)) phi_2])]] + [AppP (PThm "arg_conv", dnf_and_fm_prf (And (v, va)) phi_1), + dnf_and_fm_prf (And (v, va)) phi_2]] | dnf_and_fm_prf (Neg v) (Or (phi_1, phi_2)) = foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") [PThm "conj_disj_distribL_conv", foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") - [AppP (PThm "arg_conv", - hd [dnf_and_fm_prf (Neg v) phi_1, - dnf_and_fm_prf (Neg v) phi_2]), - hd (tl [dnf_and_fm_prf (Neg v) phi_1, - dnf_and_fm_prf (Neg v) phi_2])]] + [AppP (PThm "arg_conv", dnf_and_fm_prf (Neg v) phi_1), + dnf_and_fm_prf (Neg v) phi_2]] | dnf_and_fm_prf (Atom v) (Atom va) = PThm "all_conv" | dnf_and_fm_prf (Atom v) (And (va, vb)) = PThm "all_conv" | dnf_and_fm_prf (Atom v) (Neg va) = PThm "all_conv" | dnf_and_fm_prf (And (v, va)) (Atom vb) = PThm "all_conv" | dnf_and_fm_prf (And (v, va)) (And (vb, vc)) = PThm "all_conv" | dnf_and_fm_prf (And (v, va)) (Neg vb) = PThm "all_conv" | dnf_and_fm_prf (Neg v) (Atom va) = PThm "all_conv" | dnf_and_fm_prf (Neg v) (And (va, vb)) = PThm "all_conv" | dnf_and_fm_prf (Neg v) (Neg va) = PThm "all_conv"; fun dnf_fm_prf (And (phi_1, phi_2)) = foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv") [foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") - [AppP (PThm "arg_conv", hd [dnf_fm_prf phi_1, dnf_fm_prf phi_2]), - hd (tl [dnf_fm_prf phi_1, dnf_fm_prf phi_2])], + [AppP (PThm "arg_conv", dnf_fm_prf phi_1), dnf_fm_prf phi_2], dnf_and_fm_prf (dnf_fm phi_1) (dnf_fm phi_2)] | dnf_fm_prf (Or (phi_1, phi_2)) = foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") - [AppP (PThm "arg_conv", hd [dnf_fm_prf phi_1, dnf_fm_prf phi_2]), - hd (tl [dnf_fm_prf phi_1, dnf_fm_prf phi_2])] + [AppP (PThm "arg_conv", dnf_fm_prf phi_1), dnf_fm_prf phi_2] | dnf_fm_prf (Atom v) = PThm "all_conv" | dnf_fm_prf (Neg v) = PThm "all_conv"; fun of_alist A_ xs = foldr (fn (a, b) => update A_ a b) xs (emptya A_); fun deneg (true, LESS (x, y)) = And (Atom (true, LEQ (x, y)), Atom (false, EQ (x, y))) | deneg (false, LESS (x, y)) = Atom (true, LEQ (y, x)) | deneg (false, LEQ (x, y)) = And (Atom (true, LEQ (y, x)), Atom (false, EQ (y, x))) | deneg (false, EQ (v, vb)) = Atom (false, EQ (v, vb)) | deneg (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc)) | deneg (true, LEQ (vb, vc)) = Atom (true, LEQ (vb, vc)); +fun map_option f NONE = NONE + | map_option f (SOME x2) = SOME (f x2); + fun from_conj_prf trm_of_atom p (And (a, b)) = foldl (fn aa => fn ba => AppP (aa, ba)) (PThm "conjE") [Bound (trm_of_fm trm_of_atom (And (a, b))), AbsP (trm_of_fm trm_of_atom a, AbsP (trm_of_fm trm_of_atom b, from_conj_prf trm_of_atom (from_conj_prf trm_of_atom p b) a))] | from_conj_prf trm_of_atom p (Atom a) = p; fun contr_fm_prf trm_of_atom contr_atom_prf (Or (c, d)) = - (case (contr_fm_prf trm_of_atom contr_atom_prf c, - contr_fm_prf trm_of_atom contr_atom_prf d) - of (NONE, _) => NONE | (SOME _, NONE) => NONE - | (SOME p1, SOME p2) => - SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "disjE") - [Bound (trm_of_fm trm_of_atom (Or (c, d))), - AbsP (trm_of_fm trm_of_atom c, p1), - AbsP (trm_of_fm trm_of_atom d, p2)])) + (case contr_fm_prf trm_of_atom contr_atom_prf c of NONE => NONE + | SOME p1 => + map_option + (fn p2 => + foldl (fn a => fn b => AppP (a, b)) (PThm "disjE") + [Bound (trm_of_fm trm_of_atom (Or (c, d))), + AbsP (trm_of_fm trm_of_atom c, p1), + AbsP (trm_of_fm trm_of_atom d, p2)]) + (contr_fm_prf trm_of_atom contr_atom_prf d)) | contr_fm_prf trm_of_atom contr_atom_prf (And (a, b)) = (case contr_atom_prf (conj_list (And (a, b))) of NONE => NONE | SOME p => SOME (from_conj_prf trm_of_atom p (And (a, b)))) | contr_fm_prf trm_of_atom contr_atom_prf (Atom a) = contr_atom_prf [a]; fun deless (true, LESS (x, y)) = And (Atom (true, LEQ (x, y)), Atom (false, EQ (x, y))) | deless (false, LESS (x, y)) = Or (Atom (false, LEQ (x, y)), Atom (true, EQ (x, y))) | deless (false, EQ (v, vb)) = Atom (false, EQ (v, vb)) | deless (false, LEQ (v, vb)) = Atom (false, LEQ (v, vb)) | deless (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc)) | deless (v, LEQ (vb, vc)) = Atom (v, LEQ (vb, vc)); +fun fst (x1, x2) = x1; + +fun snd (x1, x2) = x2; + fun deneg_prf (true, LESS (x, y)) = PThm "less_le" | deneg_prf (false, LESS (x, y)) = PThm "nless_le" | deneg_prf (false, LEQ (x, y)) = PThm "nle_le" | deneg_prf (false, EQ (v, vb)) = PThm "all_conv" | deneg_prf (v, EQ (vb, vc)) = PThm "all_conv" | deneg_prf (true, LEQ (vb, vc)) = PThm "all_conv"; val one_nat : nat = Suc Zero_nat; -fun map_option f NONE = NONE - | map_option f (SOME x2) = SOME (f x2); - fun deless_prf (true, LESS (x, y)) = PThm "less_le" | deless_prf (false, LESS (x, y)) = PThm "nless_le" | deless_prf (false, EQ (v, vb)) = PThm "all_conv" | deless_prf (false, LEQ (v, vb)) = PThm "all_conv" | deless_prf (v, EQ (vb, vc)) = PThm "all_conv" | deless_prf (v, LEQ (vb, vc)) = PThm "all_conv"; -fun trm_of_oatom (EQ (x, y)) = App (App (Const "eq", Var x), Var y) - | trm_of_oatom (LEQ (x, y)) = App (App (Const "le", Var x), Var y) - | trm_of_oatom (LESS (x, y)) = App (App (Const "lt", Var x), Var y); - fun minus_nat (Suc m) (Suc n) = minus_nat m n | minus_nat Zero_nat n = Zero_nat | minus_nat m Zero_nat = m; -fun mapping_fold A_ f (Mapping t) a = fold A_ f t a; - -fun relcomp1_mapping A_ (B1_, B2_) x y1 pxy pm pma = - mapping_fold (linorder_prod B2_ B2_) +fun relcomp1_mapping B_ (C1_, C2_) combine x y1 pxy pm pma = + folda (linorder_prod C2_ C2_) (fn (y2, z) => fn pyz => fn pmb => - (if eq B1_ y1 y2 andalso not (eq B1_ y2 z) - then update (linorder_prod A_ B2_) (x, z) - (foldl (fn a => fn b => AppP (a, b)) (PThm "trans") [pxy, pyz]) - pmb + (if eq C1_ y1 y2 andalso not (eq C1_ y2 z) + then update (linorder_prod B_ C2_) (x, z) (combine pxy pyz) pmb else pmb)) pm pma; -fun relcomp_mapping (A1_, A2_) pm1 pm2 pma = - mapping_fold (linorder_prod A2_ A2_) +fun relcomp_mapping (B1_, B2_) combine pm1 pm2 pma = + folda (linorder_prod B2_ B2_) (fn (x, y) => fn pxy => fn pm => - (if eq A1_ x y then pm - else relcomp1_mapping A2_ (A1_, A2_) x y pxy pm2 pm)) + (if eq B1_ x y then pm + else relcomp1_mapping B2_ (B1_, B2_) combine x y pxy pm2 pm)) pm1 pma; -fun ntrancl_mapping (A1_, A2_) Zero_nat m = m - | ntrancl_mapping (A1_, A2_) (Suc k) m = +fun ntrancl_mapping (B1_, B2_) combine Zero_nat m = m + | ntrancl_mapping (B1_, B2_) combine (Suc k) m = let - val trclm = ntrancl_mapping (A1_, A2_) k m; + val trclm = ntrancl_mapping (B1_, B2_) combine k m; in - relcomp_mapping (A1_, A2_) trclm m trclm + relcomp_mapping (B1_, B2_) combine trclm m trclm end; -fun trancl_mapping (A1_, A2_) m = - ntrancl_mapping (A1_, A2_) - (minus_nat (card (equal_prod A1_ A1_) (keysa (linorder_prod A2_ A2_) m)) +fun trancl_mapping (B1_, B2_) combine m = + ntrancl_mapping (B1_, B2_) combine + (minus_nat (card (equal_prod B1_ B1_) (keysa (linorder_prod B2_ B2_) m)) one_nat) m; +fun trm_of_order_atom (EQ (x, y)) = App (App (Const "eq", Var x), Var y) + | trm_of_order_atom (LEQ (x, y)) = App (App (Const "le", Var x), Var y) + | trm_of_order_atom (LESS (x, y)) = App (App (Const "lt", Var x), Var y); + +fun trm_of_order_literal (true, a) = trm_of_order_atom a + | trm_of_order_literal (false, a) = App (Const "Not", trm_of_order_atom a); + fun is_in_leq leqm l = - let - val (x, y) = l; - in - (if equal_inta x y then SOME (Appt (PThm "refl", Var x)) - else lookupa (linorder_prod linorder_int linorder_int) leqm l) - end; + (if equal_inta (fst l) (snd l) then SOME (Appt (PThm "refl", Var (fst l))) + else lookupa (linorder_prod linorder_int linorder_int) leqm l); fun is_in_eq leqm l = - let - val (x, y) = l; - in - (case (is_in_leq leqm (x, y), is_in_leq leqm (y, x)) of (NONE, _) => NONE - | (SOME _, NONE) => NONE - | (SOME p1, SOME p2) => - SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "antisym") [p1, p2])) - end; - -fun trm_of_oliteral (true, a) = trm_of_oatom a - | trm_of_oliteral (false, a) = App (Const "Not", trm_of_oatom a); + (case (is_in_leq leqm l, is_in_leq leqm (snd l, fst l)) of (NONE, _) => NONE + | (SOME _, NONE) => NONE + | (SOME p1, SOME p2) => + SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "antisym") [p1, p2])); fun contr1_list leqm (false, LEQ (x, y)) = map_option (fn a => - AppP (AppP (PThm "contr", Bound (trm_of_oliteral (false, LEQ (x, y)))), + AppP (AppP (PThm "contr", + Bound (trm_of_order_literal (false, LEQ (x, y)))), a)) (is_in_leq leqm (x, y)) | contr1_list leqm (false, EQ (x, y)) = map_option (fn a => - AppP (AppP (PThm "contr", Bound (trm_of_oliteral (false, EQ (x, y)))), + AppP (AppP (PThm "contr", + Bound (trm_of_order_literal (false, EQ (x, y)))), a)) (is_in_eq leqm (x, y)) | contr1_list uu (true, va) = NONE | contr1_list uu (v, LESS (vb, vc)) = NONE; fun contr_list_aux leqm [] = NONE | contr_list_aux leqm (l :: ls) = (case contr1_list leqm l of NONE => contr_list_aux leqm ls | SOME a => SOME a); fun leq1_member_list (true, LEQ (x, y)) = - [((x, y), Bound (trm_of_oliteral (true, LEQ (x, y))))] + [((x, y), Bound (trm_of_order_literal (true, LEQ (x, y))))] | leq1_member_list (true, EQ (x, y)) = - [((x, y), AppP (PThm "eqD1", Bound (trm_of_oliteral (true, EQ (x, y))))), - ((y, x), AppP (PThm "eqD2", Bound (trm_of_oliteral (true, EQ (x, y)))))] + [((x, y), + AppP (PThm "eqD1", Bound (trm_of_order_literal (true, EQ (x, y))))), + ((y, x), + AppP (PThm "eqD2", Bound (trm_of_order_literal (true, EQ (x, y)))))] | leq1_member_list (false, va) = [] | leq1_member_list (v, LESS (vb, vc)) = []; fun leq1_list a = maps leq1_member_list a; fun leq1_mapping a = of_alist (linorder_prod linorder_int linorder_int) (leq1_list a); fun contr_list a = - contr_list_aux (trancl_mapping (equal_int, linorder_int) (leq1_mapping a)) a; + contr_list_aux + (trancl_mapping (equal_int, linorder_int) + (fn p1 => fn p2 => + foldl (fn aa => fn b => AppP (aa, b)) (PThm "trans") [p1, p2]) + (leq1_mapping a)) + a; fun contr_prf atom_conv phi = - contr_fm_prf trm_of_oliteral contr_list (dnf_fm (amap_fm atom_conv phi)); + contr_fm_prf trm_of_order_literal contr_list (dnf_fm (amap_fm atom_conv phi)); fun amap_f_m_prf ap (Atom a) = AppP (PThm "atom_conv", ap a) | amap_f_m_prf ap (And (phi_1, phi_2)) = foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") - [AppP (PThm "arg_conv", - hd [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2]), - hd (tl [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2])] + [AppP (PThm "arg_conv", amap_f_m_prf ap phi_1), amap_f_m_prf ap phi_2] | amap_f_m_prf ap (Or (phi_1, phi_2)) = foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv") - [AppP (PThm "arg_conv", - hd [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2]), - hd (tl [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2])] + [AppP (PThm "arg_conv", amap_f_m_prf ap phi_1), amap_f_m_prf ap phi_2] | amap_f_m_prf ap (Neg phi) = AppP (PThm "arg_conv", amap_f_m_prf ap phi); fun lo_contr_prf phi = map_option ((fn a => - Conv (trm_of_fm trm_of_oliteral phi, amap_f_m_prf deneg_prf phi, a)) o + Conv (trm_of_fm trm_of_order_literal phi, amap_f_m_prf deneg_prf phi, + a)) o (fn a => - Conv (trm_of_fm trm_of_oliteral (amap_fm deneg phi), + Conv (trm_of_fm trm_of_order_literal (amap_fm deneg phi), dnf_fm_prf (amap_fm deneg phi), a))) (contr_prf deneg phi); fun po_contr_prf phi = map_option ((fn a => - Conv (trm_of_fm trm_of_oliteral phi, amap_f_m_prf deless_prf phi, a)) o + Conv (trm_of_fm trm_of_order_literal phi, amap_f_m_prf deless_prf phi, + a)) o (fn a => - Conv (trm_of_fm trm_of_oliteral (amap_fm deless phi), + Conv (trm_of_fm trm_of_order_literal (amap_fm deless phi), dnf_fm_prf (amap_fm deless phi), a))) (contr_prf deless phi); end; (*struct Order_Procedure*) + diff --git a/src/Provers/order_tac.ML b/src/Provers/order_tac.ML --- a/src/Provers/order_tac.ML +++ b/src/Provers/order_tac.ML @@ -1,455 +1,434 @@ signature REIFY_TABLE = sig type table val empty : table val get_var : term -> table -> (int * table) val get_term : int -> table -> term option end structure Reifytab: REIFY_TABLE = struct - type table = (int * int Termtab.table * term Inttab.table) - - val empty = (0, Termtab.empty, Inttab.empty) + type table = (int * (term * int) list) - fun get_var t (tab as (max_var, termtab, inttab)) = - (case Termtab.lookup termtab t of - SOME v => (v, tab) - | NONE => (max_var, - (max_var + 1, Termtab.update (t, max_var) termtab, Inttab.update (max_var, t) inttab)) + val empty = (0, []) + + fun get_var t (max_var, tis) = + (case AList.lookup Envir.aeconv tis t of + SOME v => (v, (max_var, tis)) + | NONE => (max_var, (max_var + 1, (t, max_var) :: tis)) ) - fun get_term v (_, _, inttab) = Inttab.lookup inttab v + fun get_term v (_, tis) = Library.find_first (fn (_, v2) => v = v2) tis + |> Option.map fst end signature LOGIC_SIGNATURE = sig val mk_Trueprop : term -> term val dest_Trueprop : term -> term val Trueprop_conv : conv -> conv val Not : term val conj : term val disj : term val notI : thm (* (P \ False) \ \ P *) val ccontr : thm (* (\ P \ False) \ P *) val conjI : thm (* P \ Q \ P \ Q *) val conjE : thm (* P \ Q \ (P \ Q \ R) \ R *) val disjE : thm (* P \ Q \ (P \ R) \ (Q \ R) \ R *) val not_not_conv : conv (* \ (\ P) \ P *) val de_Morgan_conj_conv : conv (* \ (P \ Q) \ \ P \ \ Q *) val de_Morgan_disj_conv : conv (* \ (P \ Q) \ \ P \ \ Q *) val conj_disj_distribL_conv : conv (* P \ (Q \ R) \ (P \ Q) \ (P \ R) *) val conj_disj_distribR_conv : conv (* (Q \ R) \ P \ (Q \ P) \ (R \ P) *) end (* Control tracing output of the solver. *) val order_trace_cfg = Attrib.setup_config_bool @{binding "order_trace"} (K false) (* In partial orders, literals of the form \ x < y will force the order solver to perform case distinctions, which leads to an exponential blowup of the runtime. The split limit controls the number of literals of this form that are passed to the solver. *) val order_split_limit_cfg = Attrib.setup_config_int @{binding "order_split_limit"} (K 8) datatype order_kind = Order | Linorder -type order_literal = (bool * Order_Procedure.o_atom) +type order_literal = (bool * Order_Procedure.order_atom) type order_context = { kind : order_kind, ops : term list, thms : (string * thm) list, conv_thms : (string * thm) list } signature BASE_ORDER_TAC = sig val tac : (order_literal Order_Procedure.fm -> Order_Procedure.prf_trm option) -> order_context -> thm list -> Proof.context -> int -> tactic end functor Base_Order_Tac( structure Logic_Sig : LOGIC_SIGNATURE; val excluded_types : typ list) : BASE_ORDER_TAC = struct open Order_Procedure fun expect _ (SOME x) = x | expect f NONE = f () - fun matches_skeleton t s = t = Term.dummy orelse - (case (t, s) of - (t0 $ t1, s0 $ s1) => matches_skeleton t0 s0 andalso matches_skeleton t1 s1 - | _ => t aconv s) - - fun dest_binop t = - let - val binop_skel = Term.dummy $ Term.dummy $ Term.dummy - val not_binop_skel = Logic_Sig.Not $ binop_skel - in - if matches_skeleton not_binop_skel t - then (case t of (_ $ (t1 $ t2 $ t3)) => (false, (t1, t2, t3))) - else if matches_skeleton binop_skel t - then (case t of (t1 $ t2 $ t3) => (true, (t1, t2, t3))) - else raise TERM ("Not a binop literal", [t]) - end - - fun find_term t = Library.find_first (fn (t', _) => t' aconv t) - - fun reify_order_atom (eq, le, lt) t reifytab = - let - val (b, (t0, t1, t2)) = - (dest_binop t) handle TERM (_, _) => raise TERM ("Can't reify order literal", [t]) - val binops = [(eq, EQ), (le, LEQ), (lt, LESS)] - in - case find_term t0 binops of - SOME (_, reified_bop) => - reifytab - |> Reifytab.get_var t1 ||> Reifytab.get_var t2 - |> (fn (v1, (v2, vartab')) => - ((b, reified_bop (Int_of_integer v1, Int_of_integer v2)), vartab')) - |>> Atom - | NONE => raise TERM ("Can't reify order literal", [t]) - end - - fun reify consts reify_atom t reifytab = - let - fun reify' (t1 $ t2) reifytab = - let - val (t0, ts) = strip_comb (t1 $ t2) - val consts_of_arity = filter (fn (_, (_, ar)) => length ts = ar) consts - in - (case find_term t0 consts_of_arity of - SOME (_, (reified_op, _)) => fold_map reify' ts reifytab |>> reified_op - | NONE => reify_atom (t1 $ t2) reifytab) - end - | reify' t reifytab = reify_atom t reifytab - in - reify' t reifytab - end - fun list_curry0 f = (fn [] => f, 0) fun list_curry1 f = (fn [x] => f x, 1) fun list_curry2 f = (fn [x, y] => f x y, 2) - fun reify_order_conj ord_ops = - let - val consts = map (apsnd (list_curry2 o curry)) [(Logic_Sig.conj, And), (Logic_Sig.disj, Or)] - in - reify consts (reify_order_atom ord_ops) - end - fun dereify_term consts reifytab t = let fun dereify_term' (App (t1, t2)) = (dereify_term' t1) $ (dereify_term' t2) | dereify_term' (Const s) = AList.lookup (op =) consts s |> expect (fn () => raise TERM ("Const " ^ s ^ " not in", map snd consts)) | dereify_term' (Var v) = Reifytab.get_term (integer_of_int v) reifytab |> the in dereify_term' t end fun dereify_order_fm (eq, le, lt) reifytab t = let val consts = [ ("eq", eq), ("le", le), ("lt", lt), ("Not", Logic_Sig.Not), ("disj", Logic_Sig.disj), ("conj", Logic_Sig.conj) ] in dereify_term consts reifytab t end fun strip_AppP t = let fun strip (AppP (f, s), ss) = strip (f, s::ss) | strip x = x in strip (t, []) end fun replay_conv convs cvp = let val convs = convs @ [("all_conv", list_curry0 Conv.all_conv)] @ map (apsnd list_curry1) [ ("atom_conv", I), ("neg_atom_conv", I), ("arg_conv", Conv.arg_conv)] @ map (apsnd list_curry2) [ ("combination_conv", Conv.combination_conv), ("then_conv", curry (op then_conv))] fun lookup_conv convs c = AList.lookup (op =) convs c |> expect (fn () => error ("Can't replay conversion: " ^ c)) fun rp_conv t = (case strip_AppP t ||> map rp_conv of (PThm c, cvs) => let val (conv, arity) = lookup_conv convs c in if arity = length cvs then conv cvs else error ("Expected " ^ Int.toString arity ^ " arguments for conversion " ^ c ^ " but got " ^ (length cvs |> Int.toString) ^ " arguments") end | _ => error "Unexpected constructor in conversion proof") in rp_conv cvp end fun replay_prf_trm replay_conv dereify ctxt thmtab assmtab p = let fun replay_prf_trm' _ (PThm s) = AList.lookup (op =) thmtab s |> expect (fn () => error ("Cannot replay theorem: " ^ s)) | replay_prf_trm' assmtab (Appt (p, t)) = replay_prf_trm' assmtab p |> Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt (dereify t))] | replay_prf_trm' assmtab (AppP (p1, p2)) = - apply2 (replay_prf_trm' assmtab) (p2, p1) |> (op COMP) + apply2 (replay_prf_trm' assmtab) (p2, p1) |> op COMP | replay_prf_trm' assmtab (AbsP (reified_t, p)) = let val t = dereify reified_t val t_thm = Logic_Sig.mk_Trueprop t |> Thm.cterm_of ctxt |> Assumption.assume ctxt val rp = replay_prf_trm' (Termtab.update (Thm.prop_of t_thm, t_thm) assmtab) p in Thm.implies_intr (Thm.cprop_of t_thm) rp end | replay_prf_trm' assmtab (Bound reified_t) = let val t = dereify reified_t |> Logic_Sig.mk_Trueprop in Termtab.lookup assmtab t |> expect (fn () => raise TERM ("Assumption not found:", t::Termtab.keys assmtab)) end | replay_prf_trm' assmtab (Conv (t, cp, p)) = let val thm = replay_prf_trm' assmtab (Bound t) val conv = Logic_Sig.Trueprop_conv (replay_conv cp) val conv_thm = Conv.fconv_rule conv thm val conv_term = Thm.prop_of conv_thm in replay_prf_trm' (Termtab.update (conv_term, conv_thm) assmtab) p end in replay_prf_trm' assmtab p end fun replay_order_prf_trm ord_ops {thms = thms, conv_thms = conv_thms, ...} ctxt reifytab assmtab = let val thmtab = thms @ [ ("conjE", Logic_Sig.conjE), ("conjI", Logic_Sig.conjI), ("disjE", Logic_Sig.disjE) ] val convs = map (apsnd list_curry0) ( map (apsnd Conv.rewr_conv) conv_thms @ [ ("not_not_conv", Logic_Sig.not_not_conv), ("de_Morgan_conj_conv", Logic_Sig.de_Morgan_conj_conv), ("de_Morgan_disj_conv", Logic_Sig.de_Morgan_disj_conv), ("conj_disj_distribR_conv", Logic_Sig.conj_disj_distribR_conv), ("conj_disj_distribL_conv", Logic_Sig.conj_disj_distribL_conv) ]) val dereify = dereify_order_fm ord_ops reifytab in replay_prf_trm (replay_conv convs) dereify ctxt thmtab assmtab end - fun is_binop_term t = - let - fun is_included t = forall (curry (op <>) (t |> fastype_of |> domain_type)) excluded_types - in - (case dest_binop (Logic_Sig.dest_Trueprop t) of - (_, (binop, t1, t2)) => - is_included binop andalso - (* Exclude terms with schematic variables since the solver can't deal with them. - More specifically, the solver uses Assumption.assume which does not allow schematic - variables in the assumed cterm. - *) - Term.add_var_names (binop $ t1 $ t2) [] = [] - ) handle TERM (_, _) => false - end + fun strip_Not (nt $ t) = if nt = Logic_Sig.Not then t else nt $ t + | strip_Not t = t - fun partition_matches ctxt term_of pats ys = - let - val thy = Proof_Context.theory_of ctxt - - fun find_match t env = - Library.get_first (try (fn pat => Pattern.match thy (pat, t) env)) pats - - fun filter_matches xs = fold (fn x => fn (mxs, nmxs, env) => - case find_match (term_of x) env of - SOME env' => (x::mxs, nmxs, env') - | NONE => (mxs, x::nmxs, env)) xs ([], [], (Vartab.empty, Vartab.empty)) - - fun partition xs = - case filter_matches xs of - ([], _, _) => [] - | (mxs, nmxs, env) => (env, mxs) :: partition nmxs - in - partition ys - end - - fun limit_not_less [_, _, lt] ctxt prems = + fun limit_not_less [_, _, lt] ctxt decomp_prems = let val thy = Proof_Context.theory_of ctxt val trace = Config.get ctxt order_trace_cfg val limit = Config.get ctxt order_split_limit_cfg fun is_not_less_term t = - (case dest_binop (Logic_Sig.dest_Trueprop t) of - (false, (t0, _, _)) => Pattern.matches thy (lt, t0) - | _ => false) - handle TERM _ => false + case try (strip_Not o Logic_Sig.dest_Trueprop) t of + SOME (binop $ _ $ _) => Pattern.matches thy (lt, binop) + | NONE => false - val not_less_prems = filter (is_not_less_term o Thm.prop_of) prems + val not_less_prems = filter (is_not_less_term o Thm.prop_of o fst) decomp_prems val _ = if trace andalso length not_less_prems > limit then tracing "order split limit exceeded" else () in - filter_out (is_not_less_term o Thm.prop_of) prems @ + filter_out (is_not_less_term o Thm.prop_of o fst) decomp_prems @ take limit not_less_prems end + + fun decomp [eq, le, lt] ctxt t = + let + fun is_excluded t = exists (fn ty => ty = fastype_of t) excluded_types + + fun decomp'' (binop $ t1 $ t2) = + let + open Order_Procedure + val thy = Proof_Context.theory_of ctxt + fun try_match pat = try (Pattern.match thy (pat, binop)) (Vartab.empty, Vartab.empty) + in if is_excluded t1 then NONE + else case (try_match eq, try_match le, try_match lt) of + (SOME env, _, _) => SOME (true, EQ, (t1, t2), env) + | (_, SOME env, _) => SOME (true, LEQ, (t1, t2), env) + | (_, _, SOME env) => SOME (true, LESS, (t1, t2), env) + | _ => NONE + end + | decomp'' _ = NONE + + fun decomp' (nt $ t) = + if nt = Logic_Sig.Not + then decomp'' t |> Option.map (fn (b, c, p, e) => (not b, c, p, e)) + else decomp'' (nt $ t) + | decomp' t = decomp'' t + + in + try Logic_Sig.dest_Trueprop t |> Option.mapPartial decomp' + end + + fun maximal_envs envs = + let + fun test_opt p (SOME x) = p x + | test_opt _ NONE = false + + fun leq_env (tyenv1, tenv1) (tyenv2, tenv2) = + Vartab.forall (fn (v, ty) => + Vartab.lookup tyenv2 v |> test_opt (fn ty2 => ty2 = ty)) tyenv1 + andalso + Vartab.forall (fn (v, (ty, t)) => + Vartab.lookup tenv2 v |> test_opt (fn (ty2, t2) => ty2 = ty andalso t2 aconv t)) tenv1 + + fun fold_env (i, env) es = fold_index (fn (i2, env2) => fn es => + if i = i2 then es else if leq_env env env2 then (i, i2) :: es else es) envs es + + val env_order = fold_index fold_env envs [] + + val graph = fold_index (fn (i, env) => fn g => Int_Graph.new_node (i, env) g) + envs Int_Graph.empty + val graph = fold Int_Graph.add_edge env_order graph + + val strong_conns = Int_Graph.strong_conn graph + val maximals = + filter (fn comp => length comp = length (Int_Graph.all_succs graph comp)) strong_conns + in + map (Int_Graph.all_preds graph) maximals + end fun order_tac raw_order_proc octxt simp_prems = Subgoal.FOCUS (fn {prems=prems, context=ctxt, ...} => let val trace = Config.get ctxt order_trace_cfg - val binop_prems = filter (is_binop_term o Thm.prop_of) (prems @ simp_prems) - val strip_binop = (fn (x, _, _) => x) o snd o dest_binop - val binop_of = strip_binop o Logic_Sig.dest_Trueprop o Thm.prop_of + fun these' _ [] = [] + | these' f (x :: xs) = case f x of NONE => these' f xs | SOME y => (x, y) :: these' f xs - (* Due to local_setup, the operators of the order may contain schematic term and type - variables. We partition the premises according to distinct instances of those operators. - *) - val part_prems = partition_matches ctxt binop_of (#ops octxt) binop_prems - |> (case #kind octxt of - Order => map (fn (env, prems) => - (env, limit_not_less (#ops octxt) ctxt prems)) - | _ => I) - + val prems = simp_prems @ prems + |> filter (fn p => null (Term.add_vars (Thm.prop_of p) [])) + |> map (Conv.fconv_rule Thm.eta_conversion) + val decomp_prems = these' (decomp (#ops octxt) ctxt o Thm.prop_of) prems + + fun env_of (_, (_, _, _, env)) = env + val env_groups = maximal_envs (map env_of decomp_prems) + fun order_tac' (_, []) = no_tac - | order_tac' (env, prems) = + | order_tac' (env, decomp_prems) = let - val [eq, le, lt] = #ops octxt - val subst_contract = Envir.eta_contract o Envir.subst_term env - val ord_ops = (subst_contract eq, - subst_contract le, - subst_contract lt) - - val _ = if trace then @{print} (ord_ops, prems) else (ord_ops, prems) - - val prems_conj_thm = foldl1 (fn (x, a) => Logic_Sig.conjI OF [x, a]) prems - |> Conv.fconv_rule Thm.eta_conversion + val [eq, le, lt] = #ops octxt |> map (Envir.eta_contract o Envir.subst_term env) + + val decomp_prems = case #kind octxt of + Order => limit_not_less (#ops octxt) ctxt decomp_prems + | _ => decomp_prems + + fun reify_prem (_, (b, ctor, (x, y), _)) (ps, reifytab) = + (Reifytab.get_var x ##>> Reifytab.get_var y) reifytab + |>> (fn vp => (b, ctor (apply2 Int_of_integer vp)) :: ps) + val (reified_prems, reifytab) = fold_rev reify_prem decomp_prems ([], Reifytab.empty) + + val reified_prems_conj = foldl1 (fn (x, a) => And (x, a)) (map Atom reified_prems) + val prems_conj_thm = map fst decomp_prems + |> foldl1 (fn (x, a) => Logic_Sig.conjI OF [x, a]) + |> Conv.fconv_rule Thm.eta_conversion val prems_conj = prems_conj_thm |> Thm.prop_of - val (reified_prems_conj, reifytab) = - reify_order_conj ord_ops (Logic_Sig.dest_Trueprop prems_conj) Reifytab.empty - + val proof = raw_order_proc reified_prems_conj - + + val pretty_term_list = + Pretty.list "" "" o map (Syntax.pretty_term (Config.put show_types true ctxt)) + val pretty_thm_list = Pretty.list "" "" o map (Thm.pretty_thm ctxt) + fun pretty_type_of t = Pretty.block [ Pretty.str "::", Pretty.brk 1, + Pretty.quote (Syntax.pretty_typ ctxt (Term.fastype_of t)) ] + fun pretty_trace () = + [ ("order kind:", Pretty.str (@{make_string} (#kind octxt))) + , ("order operators:", Pretty.block [ pretty_term_list [eq, le, lt], Pretty.brk 1 + , pretty_type_of le ]) + , ("premises:", pretty_thm_list prems) + , ("selected premises:", pretty_thm_list (map fst decomp_prems)) + , ("reified premises:", Pretty.str (@{make_string} reified_prems)) + , ("contradiction:", Pretty.str (@{make_string} (Option.isSome proof))) + ] |> map (fn (t, pp) => Pretty.block [Pretty.str t, Pretty.brk 1, pp]) + |> Pretty.big_list "order solver called with the parameters" + val _ = if trace then tracing (Pretty.string_of (pretty_trace ())) else () + val assmtab = Termtab.make [(prems_conj, prems_conj_thm)] - val replay = replay_order_prf_trm ord_ops octxt ctxt reifytab assmtab + val replay = replay_order_prf_trm (eq, le, lt) octxt ctxt reifytab assmtab in case proof of NONE => no_tac | SOME p => SOLVED' (resolve_tac ctxt [replay p]) 1 end in - FIRST (map order_tac' part_prems) + map (fn is => ` (env_of o hd) (map (nth decomp_prems) is) |> order_tac') env_groups + |> FIRST end) val ad_absurdum_tac = SUBGOAL (fn (A, i) => - case try (Logic_Sig.dest_Trueprop o Logic.strip_assums_concl) A of - SOME (nt $ _) => - if nt = Logic_Sig.Not - then resolve0_tac [Logic_Sig.notI] i - else resolve0_tac [Logic_Sig.ccontr] i - | SOME _ => resolve0_tac [Logic_Sig.ccontr] i - | NONE => resolve0_tac [Logic_Sig.ccontr] i) + case try (Logic_Sig.dest_Trueprop o Logic.strip_assums_concl) A of + SOME (nt $ _) => + if nt = Logic_Sig.Not + then resolve0_tac [Logic_Sig.notI] i + else resolve0_tac [Logic_Sig.ccontr] i + | _ => resolve0_tac [Logic_Sig.ccontr] i) fun tac raw_order_proc octxt simp_prems ctxt = - EVERY' [ - ad_absurdum_tac, - CONVERSION Thm.eta_conversion, - order_tac raw_order_proc octxt simp_prems ctxt - ] + ad_absurdum_tac THEN' order_tac raw_order_proc octxt simp_prems ctxt end functor Order_Tac(structure Base_Tac : BASE_ORDER_TAC) = struct fun order_context_eq ({kind = kind1, ops = ops1, ...}, {kind = kind2, ops = ops2, ...}) = kind1 = kind2 andalso eq_list (op aconv) (ops1, ops2) fun order_data_eq (x, y) = order_context_eq (fst x, fst y) structure Data = Generic_Data( type T = (order_context * (order_context -> thm list -> Proof.context -> int -> tactic)) list val empty = [] fun merge data = Library.merge order_data_eq data ) fun declare (octxt as {kind = kind, raw_proc = raw_proc, ...}) lthy = lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context => let val ops = map (Morphism.term phi) (#ops octxt) val thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#thms octxt) val conv_thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#conv_thms octxt) val octxt' = {kind = kind, ops = ops, thms = thms, conv_thms = conv_thms} in context |> Data.map (Library.insert order_data_eq (octxt', raw_proc)) end) fun declare_order { ops = {eq = eq, le = le, lt = lt}, thms = { trans = trans, (* x \ y \ y \ z \ x \ z *) refl = refl, (* x \ x *) eqD1 = eqD1, (* x = y \ x \ y *) eqD2 = eqD2, (* x = y \ y \ x *) antisym = antisym, (* x \ y \ y \ x \ x = y *) contr = contr (* \ P \ P \ R *) }, conv_thms = { less_le = less_le, (* x < y \ x \ y \ x \ y *) nless_le = nless_le (* \ a < b \ \ a \ b \ a = b *) } } = declare { kind = Order, ops = [eq, le, lt], thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2), ("antisym", antisym), ("contr", contr)], conv_thms = [("less_le", less_le), ("nless_le", nless_le)], raw_proc = Base_Tac.tac Order_Procedure.po_contr_prf } fun declare_linorder { ops = {eq = eq, le = le, lt = lt}, thms = { trans = trans, (* x \ y \ y \ z \ x \ z *) refl = refl, (* x \ x *) eqD1 = eqD1, (* x = y \ x \ y *) eqD2 = eqD2, (* x = y \ y \ x *) antisym = antisym, (* x \ y \ y \ x \ x = y *) contr = contr (* \ P \ P \ R *) }, conv_thms = { less_le = less_le, (* x < y \ x \ y \ x \ y *) nless_le = nless_le, (* \ x < y \ y \ x *) nle_le = nle_le (* \ a \ b \ b \ a \ b \ a *) } } = declare { kind = Linorder, ops = [eq, le, lt], thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2), ("antisym", antisym), ("contr", contr)], conv_thms = [("less_le", less_le), ("nless_le", nless_le), ("nle_le", nle_le)], raw_proc = Base_Tac.tac Order_Procedure.lo_contr_prf } (* Try to solve the goal by calling the order solver with each of the declared orders. *) fun tac simp_prems ctxt = let fun app_tac (octxt, tac0) = CHANGED o tac0 octxt simp_prems ctxt in FIRST' (map app_tac (Data.get (Context.Proof ctxt))) end end