--- 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*)
+
--- 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