# HG changeset patch # User Lukas Stevens # Date 1635512986 -7200 # Node ID e6f0c9bf966c1807795a2bb83c8ef78f76ce4130 # Parent c2bc0180151abc39f184eea49389962f04039a01 order_tac: prevent potential bug, improve perf and tracing - We need to be careful when the order operators contain schematic variables, e.g. <= = ccw' ?p. diff -r c2bc0180151a -r e6f0c9bf966c src/Provers/order_procedure.ML --- a/src/Provers/order_procedure.ML Fri Oct 29 13:23:41 2021 +0200 +++ b/src/Provers/order_procedure.ML Fri Oct 29 15:09:46 2021 +0200 @@ -1,37 +1,38 @@ 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; @@ -39,14 +40,14 @@ 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; @@ -89,7 +90,7 @@ 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 | @@ -97,16 +98,17 @@ 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 @@ -288,11 +290,6 @@ 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); @@ -320,6 +317,8 @@ | 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 @@ -354,36 +353,26 @@ 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" @@ -397,13 +386,11 @@ 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"; @@ -418,6 +405,9 @@ | 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))), @@ -428,14 +418,15 @@ | 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)))) @@ -450,6 +441,10 @@ | 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" @@ -459,9 +454,6 @@ 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" @@ -469,78 +461,68 @@ | 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 @@ -552,10 +534,12 @@ | 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)) = []; @@ -565,40 +549,44 @@ 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 -r c2bc0180151a -r e6f0c9bf966c src/Provers/order_tac.ML --- a/src/Provers/order_tac.ML Fri Oct 29 13:23:41 2021 +0200 +++ b/src/Provers/order_tac.ML Fri Oct 29 15:09:46 2021 +0200 @@ -8,18 +8,18 @@ structure Reifytab: REIFY_TABLE = struct - type table = (int * int Termtab.table * term Inttab.table) + type table = (int * (term * int) list) - val empty = (0, Termtab.empty, Inttab.empty) + val empty = (0, []) - 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)) + 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 = @@ -54,7 +54,7 @@ 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, @@ -78,68 +78,10 @@ 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) @@ -204,7 +146,7 @@ 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 @@ -253,125 +195,162 @@ 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