theory Branch_and_Bound
imports
Linear_Inequalities.Mixed_Integer_Solutions
Simplex.Simplex_Incremental
Farkas.Matrix_Farkas
"List-Index.List_Index"
"Certification_Monads.Check_Monad"
begin
hide_const (open) Farkas.rel_of
hide_const (open) Missing_Lemmas.max_list
abbreviation Var where "Var ≡ Abstract_Linear_Poly.Var"
abbreviation max_var where "max_var ≡ Abstract_Linear_Poly.max_var"
abbreviation vars_list where "vars_list ≡ Abstract_Linear_Poly.vars_list"
fun satisfies_mixed_constraints (infixl "⊨⇩m⇩c⇩s" 100) where
"v ⊨⇩m⇩c⇩s (cs, I) = (v ⊨⇩c⇩s cs ∧ (∀ i ∈ I. v i ∈ ℤ))"
text ‹We define the following measure on the arguments of the branch-and-bound
algorithm to prove its termination.
The idea is that at each recursive call ("branch operation"), if the branch
is performed on the variable x, then the quantity ub x - lb x strictly
decreases while the other ones are left unchanged.
Finally, if the sum of the ub x - lb x is nonpositive, then the problem
has an unique solution with integral values for the elements of Is, or is
infeasible.›
fun bb_measure where
"bb_measure (Is, lb, ub) = nat (sum_list (map (λ x. ub x - lb x) Is))"
definition bounds_to_constraints where
"bounds_to_constraints Is lb ub =
map (λ x. GEQ (Var x) (of_int (lb x))) Is @
map (λ x. LEQ (Var x) (of_int (ub x))) Is"
lemma bounds_to_constraints_sat:
"v ⊨⇩c⇩s set (bounds_to_constraints Is lb ub) ⟷
(∀ i ∈ set Is. of_int (lb i) ≤ v i ∧ v i ≤ of_int (ub i))"
proof -
{
fix i
assume v: "v ⊨⇩c⇩s set (bounds_to_constraints Is lb ub)"
assume "i ∈ set Is"
hence "GEQ (Var i) (of_int (lb i)) ∈ set (bounds_to_constraints Is lb ub)"
and "LEQ (Var i) (of_int (ub i)) ∈ set (bounds_to_constraints Is lb ub)"
unfolding bounds_to_constraints_def by auto
hence "v ⊨⇩c GEQ (Var i) (of_int (lb i)) ∧
v ⊨⇩c LEQ (Var i) (of_int (ub i))" using v by blast
hence "of_int (lb i) ≤ v i ∧ v i ≤ of_int (ub i)"
using valuate_Var[of i v] by auto
}
moreover
{
fix c
assume bnd: "(∀ i ∈ set Is. of_int (lb i) ≤ v i ∧ v i ≤ of_int (ub i))"
assume "c ∈ set (bounds_to_constraints Is lb ub)"
then obtain i where i: "i ∈ set Is"
and "c = GEQ (Var i) (of_int (lb i)) ∨
c = LEQ (Var i) (of_int (ub i))"
unfolding bounds_to_constraints_def by auto
hence "v ⊨⇩c c" using i bnd valuate_Var[of i v] by fastforce
}
ultimately show ?thesis by blast
qed
lemma bounds_to_constraints_cong:
assumes "⋀x. x ∈ set Is ⟹ lb x = lb' x" "⋀x. x ∈ set Is ⟹ ub x = ub' x"
shows "bounds_to_constraints Is lb ub = bounds_to_constraints Is lb' ub'"
unfolding bounds_to_constraints_def
using assms by auto
lemma sat_impl_sum_diff_bounds_nonneg:
assumes sat: "simplex (cs @ bounds_to_constraints Is lb ub) = Sat v"
and J: "set J ⊆ set Is"
shows "(∑x←J. ub x - lb x) ≥ 0"
proof (rule sum_list_nonneg)
fix y assume "y ∈ set (map (λx. ub x - lb x) J)"
then obtain x where x: "x ∈ set J" and y: "y = ub x - lb x" by auto
from sat have "⟨v⟩ ⊨⇩c⇩s set (bounds_to_constraints Is lb ub)"
using simplex(3) by fastforce
hence "⟨v⟩ ⊨⇩c⇩s set (bounds_to_constraints J lb ub)"
unfolding bounds_to_constraints_def using J by auto
hence "of_int (lb x) ≤ ⟨v⟩ x ∧ ⟨v⟩ x ≤ of_int (ub x)"
using bounds_to_constraints_sat x by blast
hence "ub x - lb x ≥ 0" by linarith
thus "y ≥ 0" using y by blast
qed
lemma find_Some_set:
assumes "find P xs = Some x"
shows "x ∈ set xs ∧ P x"
proof -
from assms obtain i where "x = xs ! i" and "i < length xs" and "P (xs ! i)"
using find_Some_iff[of P xs x] by blast
thus ?thesis by auto
qed
lemma int_le_floor_iff:
assumes "x ∈ ℤ"
shows "x ≤ y ⟷ x ≤ of_int ⌊y⌋"
proof
assume "x ≤ y"
thus "x ≤ of_int ⌊y⌋"
using le_floor_iff[of "⌊x⌋" "y"] floor_of_int_eq[OF assms] by auto
next
assume "x ≤ of_int ⌊y⌋"
thus "x ≤ y"
using le_floor_iff[of "⌊x⌋" "of_int ⌊y⌋"] floor_of_int_eq[OF assms]
by linarith
qed
lemma int_ge_ceiling_iff:
assumes "x ∈ ℤ"
shows "x ≥ y ⟷ x ≥ of_int ⌈y⌉"
unfolding ceiling_def
using int_le_floor_iff[of "-x" "-y"] assms by fastforce
lemma nonnint_sat_pos_measure:
assumes sat: "simplex (cs @ bounds_to_constraints Is lb ub) = Sat v"
assumes find: "find (λy. ⟨v⟩ y ∉ ℤ) Is = Some x"
shows "0 < (∑x←Is. ub x - lb x)"
proof -
have x: "x ∈ set Is" and "⟨v⟩ x ∉ ℤ" using find_Some_set[OF find] by auto
from sat simplex(3) have "⟨v⟩ ⊨⇩c⇩s set (bounds_to_constraints Is lb ub)"
by auto
hence "of_int (lb x) ≤ ⟨v⟩ x ∧ ⟨v⟩ x ≤ of_int (ub x)"
using bounds_to_constraints_sat x by blast
hence "rat_of_int (lb x) ≥ rat_of_int (ub x) ⟹ rat_of_int (lb x) = ⟨v⟩ x"
by linarith
hence "¬ (rat_of_int (lb x) ≥ rat_of_int (ub x))"
using `⟨v⟩ x ∉ ℤ` Ints_of_int by metis
hence "0 < ub x - lb x" by linarith
moreover have "0 ≤ (∑i←remove1 x Is. ub i - lb i)"
using set_remove1_subset
by (rule sat_impl_sum_diff_bounds_nonneg[OF sat])
ultimately have "0 < (ub x - lb x) + (∑i←remove1 x Is. ub i - lb i)"
by linarith
also have "… = (∑i←Is. ub i - lb i)"
using sum_list_map_remove1[OF x, of "λ i. ub i - lb i"] by auto
finally show ?thesis by blast
qed
text ‹The core of a branch-and-bound solver for mixed-integer linear problems.
It takes as arguments a constraint list, the list of integral variables, and
functions mapping integral variables to lower and upper-bounds›
definition atom_to_qdnsconstr :: "rat atom ⇒ QDelta ns_constraint" where
"atom_to_qdnsconstr atm =
(case atm of
(Leq x qdcnst) ⇒ (LEQ_ns (Var x) (QDelta qdcnst 0))
| (Geq x qdcnst) ⇒ (GEQ_ns (Var x) (QDelta qdcnst 0)))"
definition atom_to_qdatom where
"atom_to_qdatom atm = (case atm of
(Leq vr c) ⇒ (Leq vr (QDelta c 0)) |
(Geq vr c) ⇒ (Geq vr (QDelta c 0)))"
definition update_iatom_in_state' ::
"nat simplex_state ⇒ (nat, rat) i_atom ⇒ nat simplex_state" where
"update_iatom_in_state' s iatm =
(case s of Simplex_State (cs, (asi, tv, ui), l3s) ⇒
let cs' = cs[(fst iatm) := atom_to_qdnsconstr (snd iatm)];
asi' = Mapping.update (fst iatm) [(fst iatm, atom_to_qdatom (snd iatm))] asi in
Simplex_State (cs', (asi', tv, ui), l3s))"
definition i_bounds_to_constraints where
"i_bounds_to_constraints Is lb ub =
map (λ x. (fst (lb x), GEQ (Var x) (of_int (snd (lb x))))) Is @
map (λ x. (fst (ub x), LEQ (Var x) (of_int (snd (ub x))))) Is"
fun enumerated where
"enumerated n [] = True" |
"enumerated n ((i, x)#xs) = (n = i ∧ enumerated (Suc n) xs)"
lemma enumerated_enumerate:
"enumerated n xs = (xs = List.enumerate n (map snd xs))"
by (induction n xs rule: enumerated.induct) (auto)
lemma enumerated_distinct: "enumerated n xs ⟹ distinct (map fst xs)"
unfolding enumerated_enumerate enumerate_eq_zip by (induction n xs rule: enumerated.induct) (auto)
lemma enumerated_sorted: "enumerated n xs ⟹ sorted (map fst xs)"
unfolding enumerated_enumerate using sorted_enumerate by metis
lemma enumerated: "map fst xs = [n..<n +length xs] ⟷ enumerated n xs"
unfolding enumerated_enumerate by (metis enumerate_eq_zip length_map map_fst_enumerate zip_map_fst_snd)
lemma enumeratedE[elim]:
assumes a: "enumerated n xs" and
b: "distinct (map fst xs) ⟹ sorted (map fst xs) ⟹ P"
shows "P"
using assms enumerated_distinct enumerated_sorted by blast
lemma sorted_map_distinct_set_unique:
assumes "sorted (map f xs)" "distinct (map f xs)" "sorted (map f ys)" "distinct (map f ys)"
"set xs = set ys" "length xs = length ys"
shows "xs = ys"
using assms proof (induction rule: list_induct2[OF `length xs = length ys`])
case 1
then show ?case by (simp)
next
case (2 x xs y ys)
then have 1: "x = y"
by (clarsimp) (metis eq_iff image_iff insert_iff)
moreover have "y ∉ set ys"
using 2 by fastforce
ultimately have "set xs = set ys"
using 2 by fastforce
then show ?case
using 1 2 by auto
qed
lemma enumerated_set_unique:
assumes "enumerated n xs" "enumerated n ys" "set xs = set ys" "length xs = length ys"
shows "xs = ys"
using assms by (auto intro: sorted_map_distinct_set_unique)
lemma enumerated_update:
assumes "xs' = xs[i := (i + n, y)]" "enumerated n xs"
shows "enumerated n xs'"
proof (cases "i < length xs")
case True
then show ?thesis
using assms
unfolding enumerated_enumerate enumerate_eq_zip
proof (induction xs' arbitrary: xs i n y)
case Nil
then show ?case by auto
next
case (Cons a xs')
have "fst (xs ! i) = i + n"
by (metis Cons.prems(1) Cons.prems(3) add.commute add_diff_cancel_left' length_map length_upt less_diff_conv map_fst_zip nth_map nth_upt)
then show ?case
using Cons apply(auto)
using add_diff_cancel_left' fst_conv length_map length_upt list_update_id map_fst_zip map_update update_zip
by smt
qed
next
case False
then show ?thesis
using assms by auto
qed
lemma enumerated_Cons: "enumerated n (x # xs) ⟹ enumerated (Suc n) xs"
by (cases x) auto
lemma enumerated_append: "enumerated n (xs @ ys) ⟹ enumerated n xs"
by (induction n xs rule: enumerated.induct) (auto)
lemma enumerated_nth: "enumerated n xs ⟹ (n + i, y) ∈ set xs ⟹ xs ! i = (n + i, y)"
apply(induction n xs arbitrary: i y rule: enumerated.induct )
apply(auto)
apply(case_tac i)
apply(auto)
apply (metis One_nat_def Suc_less_eq Suc_pred enumerated_enumerate in_set_enumerate_eq le_imp_less_Suc nth_Cons_pos prod.sel(1))
by (metis One_nat_def Suc_pred add.right_neutral add_Suc_right enumerated_enumerate in_set_enumerate_eq lessI linorder_not_less neq0_conv nth_Cons' prod.sel(1))
lemma enumerated_nth': "enumerated n xs ⟹ i < length xs ⟹ xs ! i = (n + i, snd (xs ! i))"
apply(induction n xs arbitrary: i rule: enumerated.induct )
apply(auto)
apply(case_tac i)
apply(auto)
apply (metis length_nth_simps(4) not0_implies_Suc not_less_eq nth_Cons_0 snd_conv)
using less_Suc_eq_0_disj by auto
definition state_invariant where
"state_invariant cs Is lb ub s =
(let bs = i_bounds_to_constraints Is lb ub @ cs in
enumerated 0 bs ∧
invariant_simplex bs (fst ` set bs) s)"
definition checked_bnc where
"checked_bnc cs Is lb ub s =
(let bs = i_bounds_to_constraints Is lb ub @ cs in
enumerated 0 bs ∧
checked_simplex bs (fst ` set bs) s)"
lemma checked_invariant_bnc: "checked_bnc cs Is lb ub s ⟹ state_invariant cs Is lb ub s"
unfolding checked_bnc_def state_invariant_def using checked_invariant_simplex by (auto simp add: Let_def)
lemma state_invariant_simplex:
assumes inv: "state_invariant cs Is lb ub s"
and sat: "check_simplex s = Sat s'"
and "solution_simplex s' = v"
shows "v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb ub @ cs))"
proof -
let ?bs = "i_bounds_to_constraints Is lb ub @ cs"
have "checked_simplex ?bs (fst ` set ?bs) s'" using sat inv check_simplex_ok
unfolding state_invariant_def by (auto simp add: Let_def)
then have "((fst ` set ?bs), v) ⊨⇩i⇩c⇩s set ?bs" using solution_simplex assms(3) by blast
then have "v ⊨⇩c⇩s set (map snd ?bs)" by force
then show ?thesis unfolding i_bounds_to_constraints_def bounds_to_constraints_def by simp
qed
lemma state_invariant_simplex_Unsat:
assumes inv: "state_invariant cs Is lb ub s"
and sat: "check_simplex s = Unsat I"
shows "∄v. v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb ub @ cs))"
proof -
let ?bs = "i_bounds_to_constraints Is lb ub @ cs"
have "set I ⊆ set (map fst ?bs) ∧ minimal_unsat_core (set I) ?bs"
using assms unfolding state_invariant_def
by (intro check_simplex_unsat) (auto simp add: image_Un Let_def)
then show ?thesis
unfolding minimal_unsat_core_def by force
qed
lemma sat_impl_sum_diff_bounds_nonneg':
assumes sat: "v ⊨⇩c⇩s set (bounds_to_constraints Is lb ub)"
and J: "set J ⊆ set Is"
shows "(∑x←J. ub x - lb x) ≥ 0"
proof (rule sum_list_nonneg)
fix y assume "y ∈ set (map (λx. ub x - lb x) J)"
then obtain x where x: "x ∈ set J" and y: "y = ub x - lb x" by auto
have "of_int (lb x) ≤ v x ∧ v x ≤ of_int (ub x)"
using assms bounds_to_constraints_sat x by blast
hence "ub x - lb x ≥ 0" by linarith
thus "y ≥ 0" using y by blast
qed
lemma nonnint_sat_pos_measure':
assumes sat: "v ⊨⇩c⇩s set (bounds_to_constraints Is lb ub)"
assumes find: "find (λy. v y ∉ ℤ) Is = Some x"
shows "0 < (∑x←Is. ub x - lb x)"
proof -
have x: "x ∈ set Is" and "v x ∉ ℤ" using find_Some_set[OF find] by auto
then have "of_int (lb x) ≤ v x ∧ v x ≤ of_int (ub x)"
using assms bounds_to_constraints_sat x by blast
then have "rat_of_int (lb x) ≥ rat_of_int (ub x) ⟹ rat_of_int (lb x) = v x"
by linarith
then have "¬ (rat_of_int (lb x) ≥ rat_of_int (ub x))"
using `v x ∉ ℤ` Ints_of_int by metis
then have "0 < ub x - lb x" by linarith
moreover have "0 ≤ (∑i←remove1 x Is. ub i - lb i)"
using set_remove1_subset sat_impl_sum_diff_bounds_nonneg'[OF sat] by metis
ultimately have "0 < (ub x - lb x) + (∑i←remove1 x Is. ub i - lb i)"
by linarith
also have "… = (∑i←Is. ub i - lb i)"
using sum_list_map_remove1[OF x, of "λ i. ub i - lb i"] by auto
finally show ?thesis by blast
qed
definition del_atom_from_state'' :: "nat simplex_state ⇒ (nat, rat) i_atom ⇒ nat simplex_state"
where
"del_atom_from_state'' s iatm = (case s of
Simplex_State (l1, l2, State t bl bu v c uc) ⇒
(let bu' = Mapping.delete (atom_var (snd iatm)) bu;
bl' = Mapping.delete (atom_var (snd iatm)) bl in
Simplex_State (l1, l2, State t bl' bu' v c uc)))"
fun sum_to_option where
"sum_to_option (Inr x) = Some x" |
"sum_to_option (Inl _) = None"
definition bnb_update_state'' ::
"(nat × constraint) list ⇒ var list ⇒ (var ⇒ (nat × int)) ⇒ (var ⇒ (nat × int))
⇒ nat simplex_state ⇒ (nat, rat) i_atom ⇒ nat simplex_state option" where
"bnb_update_state'' cs Is lb ub s iatm =
(let idx_list = (map fst (i_bounds_to_constraints Is lb ub @ cs)) in
(case (assert_all_simplex (remove1 (fst iatm) idx_list) (del_atom_from_state'' s iatm)) of
Sat s' ⇒ sum_to_option (assert_simplex (fst iatm) (update_iatom_in_state' s' iatm)) |
Unsat uc ⇒ None))"
definition suitable_upd_atom where
"suitable_upd_atom iatm ics =
(let tons = to_ns ics;
i = (find_index (λx. fst x = fst iatm ∧ poly (snd x) = Var (atom_var (snd iatm))) tons) in
(if i ≥ length tons then False else True))"
lemma mapping_del[simp]:
"Mapping.lookup (Mapping.delete v m1) x = (if x = v then None else Mapping.lookup m1 x)"
by (transfer, auto)
lemma mapping_del2[simp]:
"Mapping.lookup m1 x = None ⟹ Mapping.lookup (Mapping.delete v m1) x = None"
by (transfer, auto)
lemma normalize_ns_constraint_vars_eq:
"vars (poly (normalize_ns_constraint nc)) = vars (poly nc)"
by (smt inverse_inverse_eq inverse_zero normalize_ns_constraint.elims poly.simps(1) poly.simps(2)
vars_scaleRat ns_constraint.split)
lemma firstfresh_ge_start:
"Poly_Mapping (preprocess' t v) p = Some vr ⟹ vr ≥ v"
by (induct t) (auto simp: Let_def fresh_var_monoinc split: option.splits if_splits)
lemma single_var_poly_is_monom:
"vars p = {vr} ⟹ is_monom p"
proof -
assume "vars p = {vr}"
then have "vars_list p = [vr]"
by (metis all_not_in_conv distinct.simps(2) insert_eq_iff list.set_intros(1) list.simps(15)
list_encode.cases set_empty2 singletonD distinct_vars_list set_vars_list)
then show ?thesis using is_monom_def by simp
qed
lemma preprocess'_iatom_from_insconstr:
assumes "as = Atoms (preprocess' ntons start)"
shows "∀a. a ∈ set as ⟶
(∃vr nc. (snd a) = qdelta_constraint_to_atom nc vr ∧ (fst a, nc) ∈ set ntons)"
and "∀a. (a ∈ set as ∧ atom_var (snd a) < start) ⟶
(∃vr nc. vars (poly nc) = {atom_var (snd a)} ∧ (snd a) = qdelta_constraint_to_atom nc vr
∧ (fst a, nc) ∈ set ntons)"
proof -
show "∀a. a ∈ set as ⟶
(∃vr nc. (snd a) = qdelta_constraint_to_atom nc vr ∧ (fst a, nc) ∈ set ntons)"
unfolding assms
proof (induct ntons start rule: preprocess'.induct)
case (2 i h t v)
then show ?case
proof (intro allI impI, goal_cases)
case (1 a)
then show ?case
proof (cases "a ∈ set (Atoms (preprocess' t v))")
case True
then show ?thesis using 1 by fastforce
next
case new: False
then have "fst a = i" using 1(2) by(auto simp: Let_def split: if_splits option.splits)
then show ?thesis
proof (cases "is_monom (poly h)")
case True
then show ?thesis using new 1(2) by (auto simp: Let_def)
next
case False
then show ?thesis using new 1(2) by (auto simp: Let_def split: option.splits if_splits)
qed
qed
qed
qed auto
show "∀a. (a ∈ set as ∧ atom_var (snd a) < start) ⟶
(∃vr nc. vars (poly nc) = {atom_var (snd a)} ∧ (snd a) = qdelta_constraint_to_atom nc vr
∧ (fst a, nc) ∈ set ntons)"
unfolding assms
proof (induct ntons start rule: preprocess'.induct)
case (2 i h t v)
then show ?case
proof (intro allI impI, goal_cases)
case (1 a)
show ?case
proof (cases "a ∈ set (Atoms (preprocess' t v))")
case True
then show ?thesis using 1 by fastforce
next
case a_nin_prepr_t: False
then have a_is_hd: "a = hd (Atoms (preprocess' ((i, h) # t) v))"
using 1 by (auto simp: Let_def split: option.splits if_splits)
have hnz: "poly h ≠ 0"
using a_nin_prepr_t 1 by (auto simp: Let_def split: option.splits if_splits)
define ff where "ff = (FirstFreshVariable (preprocess' t v))"
have ff_gt_iatm: "ff > atom_var (snd a)"
by (metis 1(2) ff_def fresh_var_monoinc less_trans linorder_neqE_nat not_le)
show ?thesis
proof(cases "is_monom (poly h)")
case h_monom: True
then have a: "a = (i, qdelta_constraint_to_atom h ff)"
using 1 ff_def a_nin_prepr_t
by (auto simp: Let_def split: option.splits if_splits)
then have snd_a: "snd a = qdelta_constraint_to_atom h ff" by simp
show ?thesis
proof(cases "vars (poly (snd (i,h))) = {atom_var (snd a)}")
case h_eq_iatm: True
have "∀vr'. atom_var (qdelta_constraint_to_atom h vr') = monom_var (poly h)"
by (metis qdelta_constraint_to_atom.simps poly.simps monom_to_atom.simps
atom_var.simps lec_of_nsc.cases h_monom)
then have "vars (poly h) = {atom_var (snd a)}"
using 1 is_monom_vars_monom_var h_monom h_eq_iatm by auto
then show ?thesis using 1 single_var_poly_is_monom a_nin_prepr_t
by (auto simp: Let_def split: option.splits if_splits)
next
case h_monom_neq_iatm: False
obtain ov where "vars (poly h) = {ov}" and ov: "ov ≠ atom_var (snd a)"
using h_monom_neq_iatm is_monom_vars_monom_var h_monom by simp
then have "monom_var (poly h) = ov" using h_monom monom_var_in_vars by blast
then have "atom_var (snd a) = ov"
by (cases "poly h", metis h_monom atom_var.simps lec_of_nsc.cases snd_a
monom_to_atom.simps poly.simps qdelta_constraint_to_atom.simps)
then have False using 1 ov by simp
then show ?thesis by simp
qed
next
case h_not_monom: False
then show ?thesis
proof (cases "Poly_Mapping (preprocess' t v) (poly h) = None")
case True
have "atom_var (qdelta_constraint_to_atom h ff) = ff" using h_not_monom ff_def
by (metis atom_var.simps qdelta_constraint_to_atom.simps lec_of_nsc.cases poly.simps)
then have "snd a ≠ qdelta_constraint_to_atom h ff" using ff_gt_iatm 1(2) by fastforce
then have "a ≠ hd (Atoms (preprocess' ((i, h) # t) v))" using hnz h_not_monom ff_def
by (auto simp: Let_def True split: option.splits if_splits)
then have False using a_is_hd by blast
then show ?thesis by simp
next
case False
then obtain vr where vr: "Poly_Mapping (preprocess' t v) (poly h) = Some vr" by auto
then have "vr ≥ v" using firstfresh_ge_start by auto
then have vrav: "vr > atom_var (snd a)" using 1 by linarith
have "atom_var (qdelta_constraint_to_atom h vr) = vr" using h_not_monom
by (metis atom_var.simps qdelta_constraint_to_atom.simps lec_of_nsc.cases poly.simps)
then have "snd a ≠ (qdelta_constraint_to_atom h vr)" using vrav 1(2) by fastforce
then have "a ≠ hd (Atoms (preprocess' ((i, h) # t) v))" using hnz h_not_monom vr
by (auto simp: Let_def split: option.splits if_splits)
then have False using a_is_hd by blast
then show ?thesis by simp
qed
qed
qed
qed
qed auto
qed
lemma bnb_update_del:
assumes "state_invariant cs Is lb ub s"
"cs' = i_bounds_to_constraints Is lb ub @ cs"
"suitable_upd_atom iatm cs'"
"s' = del_atom_from_state'' s iatm"
shows "∃ J. set J ⊆ (set (remove1 (fst iatm) (map fst cs')))
∧ invariant_simplex cs' (set J) s'"
proof -
define tons where "tons = to_ns cs'"
define idxs where "idxs = set (map fst tons)"
let ?eq_iatm_poly = "(λx. vars (poly (snd x)) = {atom_var (snd iatm)})"
have polyvar: "poly (snd x) = Var (atom_var (snd iatm)) ⟹ ?eq_iatm_poly x "
for x :: "nat × QDelta ns_constraint" by simp
have idxs: "idxs = set (map fst (to_ns cs'))" using tons_def idxs_def by simp
define del_idxs where
"del_idxs = set (map fst (filter ?eq_iatm_poly tons))"
define J where "J = filter (λi. i ∉ del_idxs) (map fst tons)"
have seteq: "set (map fst cs') = set (map fst tons)"
using tons_def by (metis SolveExec'Default.to_ns_indices set_map)
have "fst iatm ∈ del_idxs"
using tons_def del_idxs_def assms(3) polyvar nth_find_index suitable_upd_atom_def
by (smt image_eqI mem_Collect_eq not_less nth_mem set_filter set_map)
then have J: "set J ⊆ (set (remove1 (fst iatm) (map fst cs')))"
using seteq J_def filter_is_subset filter_remove1 remove1_filter_not filter_set by metis
obtain ncs asitv l3s where 1: "s = Simplex_State (ncs, asitv, l3s)"
using check_simplex.cases by blast
obtain ncs' asitv' l3s' where 2: "s' = Simplex_State (ncs', asitv', l3s')"
using check_simplex.cases by blast
have "ncs' = ncs" and "asitv = asitv'" using assms(4) 1 2
unfolding del_atom_from_state''_def by (auto split: atom.splits state.splits)
moreover obtain asi tv ui where asitv: "asitv = (asi, tv, ui)"
using Product_Type.prod_cases3 by blast
ultimately have s'id: "s' = Simplex_State (ncs, (asi, tv, ui), l3s')" using 2 by simp
have inv_nsc: "invariant_nsc tons idxs ((asi,tv,ui),l3s)"
by (metis assms(1) state_invariant_def seteq assms(2) invariant_simplex.simps tons_def idxs_def
1 Incremental_Simplex.invariant_cs.simps asitv image_set)
obtain tt as tv' ui' where prepr: "preprocess tons = (tt,as,tv',ui')"
using Product_Type.prod_cases4 by blast
define as_s where "as_s = set as ∩ (idxs × UNIV)"
define as_s' where "as_s' = set as ∩ (set J × UNIV)"
have Jidx: "set J = idxs - del_idxs" using del_idxs_def idxs_def J_def by auto
have Jidx2: "del_idxs = idxs - (set J)" using del_idxs_def idxs_def J_def by auto
have tons_idx: "i < length tons ⟹ poly (snd (tons ! i)) = x
⟹ (∀j < length tons. fst (tons ! j) = fst (tons ! i) ⟶ poly (snd (tons ! j)) = x)" for x i
proof -
assume x: "poly (snd (tons ! i)) = x"
assume "i < length tons"
then obtain cs_i where tonsi: "tons ! i ∈ set ((map i_constraint_to_qdelta_constraint cs') ! cs_i)"
and cs_i_len: "cs_i < length cs'"
using tons_def to_ns_def nth_concat_split nth_mem by (metis length_map)
have cs'k: "(i_constraint_to_qdelta_constraint (cs' ! k))
= map (Pair (fst (cs' ! k))) (constraint_to_qdelta_constraint (snd (cs' ! k)))" for k
by (metis i_constraint_to_qdelta_constraint.simps prod.collapse)
have fel: "∀el ∈ set (i_constraint_to_qdelta_constraint (cs' ! k)).
fst el = fst (cs' ! k)" for k
using find_index_in_set i_constraint_to_qdelta_constraint_def cs'k by simp
have fel2: "el ∈ set (i_constraint_to_qdelta_constraint (cs' ! k)) ⟹
(∀el2 ∈ set (i_constraint_to_qdelta_constraint (cs' ! k)). poly (snd el) = poly (snd el2))" for el k
proof -
assume el: "el ∈ set (i_constraint_to_qdelta_constraint (cs' ! k))"
then have sndel: "snd el ∈ set (constraint_to_qdelta_constraint (snd (cs' ! k)))"
using cs'k by auto
{
fix el2
assume "el2 ∈ set (i_constraint_to_qdelta_constraint (cs' ! k))"
then have "snd el2 ∈ set (constraint_to_qdelta_constraint (snd (cs' ! k)))" using cs'k by auto
moreover have "∀el1 el2.
{el1, el2} ⊆ set (constraint_to_qdelta_constraint nc) ⟶ poly el1 = poly el2" for nc
by (cases nc, auto)
ultimately have "poly (snd el2) = poly (snd el)" using sndel by blast
}
then show ?thesis by simp
qed
{
fix j
assume "j < length tons" moreover
assume "fst (tons ! j) = fst (tons ! i)" moreover
obtain cs_j where tonsj: "tons ! j ∈ set ((map i_constraint_to_qdelta_constraint cs') ! cs_j)"
and cs_j_len: "cs_j < length cs'"
using tons_def to_ns_def nth_concat_split nth_mem calculation by (metis length_map)
then have "fst (tons ! j) = fst (cs' ! cs_i)" using fel calculation cs_i_len tonsi by auto
moreover have "distinct (map fst cs')"
using assms(1,2) unfolding state_invariant_def by (meson enumerated_distinct)
ultimately have "poly (snd (tons ! j)) = poly (snd (tons ! i))"
using fel2 tonsi tonsj cs_j_len cs_i_len
by (metis (no_types, lifting) distinct_conv_nth fel length_map map_nth_eq_conv)
}
then show ?thesis using x by blast
qed
have tons_del: "∀i < length tons. (fst (tons ! i) ∈ del_idxs ⟶ ?eq_iatm_poly (tons ! i))"
proof -
{
fix i
assume ilen: "i < length tons"
assume "fst (tons ! i) ∈ del_idxs"
then obtain c where "c ∈ set (filter ?eq_iatm_poly tons)"
and "fst c = fst (tons ! i)" using del_idxs_def by auto
then have "?eq_iatm_poly (tons ! i)" using tons_idx ilen
by (metis (mono_tags) in_set_conv_nth mem_Collect_eq set_filter)
then have "(fst (tons ! i) ∈ del_idxs ⟶ ?eq_iatm_poly (tons ! i))"
by simp
}
then show ?thesis by auto
qed
define ntons where "ntons = (map (map_prod id normalize_ns_constraint) tons)"
define prstart where "prstart = start_fresh_variable ntons"
have avstart: "atom_var (snd iatm) < prstart"
proof -
obtain i where "fst (tons ! i) ∈ del_idxs" and ilen: "i < length tons"
by (metis DiffE Jidx2 ‹fst iatm ∈ del_idxs› idxs_def imageE in_set_conv_nth set_map)
then have "vars (poly (snd (ntons ! i))) = {atom_var (snd iatm)}" using ntons_def tons_del
by (simp add: ilen normalize_ns_constraint_vars_eq)
then have "atom_var (snd iatm) ∈ vars_constraints (Simplex.flat_list ntons)"
using ilen nth_mem ntons_def by auto
then show ?thesis unfolding prstart_def using start_fresh_variable_fresh by auto
qed
have "preprocess tons = (case preprocess_part_1 (map (map_prod id normalize_ns_constraint) tons) of
(t,as,ui) ⇒ case preprocess_part_2 as t of (t,tv) ⇒ (t,as,tv,ui))" using preprocess_def by auto
moreover obtain tp asp uip where
"preprocess_part_1 (map (map_prod id normalize_ns_constraint) tons) = (tp, asp, uip)"
using prod_cases3 by blast
moreover then obtain tpp and tvpp :: "(nat, QDelta) mapping ⇒ (nat, QDelta) mapping" where
"preprocess_part_2 asp tp = (tpp , tvpp)" by fastforce
ultimately moreover have "asp = as" using prepr by auto
ultimately have asat: "as = Atoms (preprocess' ntons prstart)" using ntons_def prstart_def
by (metis (no_types, lifting) Pair_inject preprocess_part_1_def)
have as_s': "∀a ∈ set as. atom_var (snd a) = atom_var (snd iatm) ⟷ fst a ∈ del_idxs"
proof -
{
fix a
assume a: "a ∈ set as"
{
assume "atom_var (snd a) = atom_var (snd iatm)"
then obtain nc where p1: "vars (poly nc) = {atom_var (snd iatm)}"
and "(fst a, nc) ∈ set ntons"
by (metis preprocess'_iatom_from_insconstr[OF asat] a avstart)
then obtain inc where "(fst a, nc) = (map_prod id normalize_ns_constraint) inc" and
"inc ∈ set tons" using ntons_def by auto
moreover then have "fst inc ∈ del_idxs"
using del_idxs_def snd_conv snd_map_prod p1 normalize_ns_constraint_vars_eq
by (smt image_eqI mem_Collect_eq set_filter set_map)
ultimately have "fst a ∈ del_idxs"
by (metis fst_conv id_apply map_prod_simp prod.collapse)
} moreover
{
assume fsta: "fst a ∈ del_idxs"
then obtain vr nc where "(fst a, nc) ∈ set ntons"
and anc: "snd a = qdelta_constraint_to_atom nc vr"
using preprocess'_iatom_from_insconstr[OF asat] a by blast
then obtain inc where ncinc: "(fst a, nc) = (map_prod id normalize_ns_constraint) inc" and
incs: "inc ∈ set tons" using ntons_def by auto
then have ncinc2: "nc = normalize_ns_constraint (snd inc)" by (metis snd_conv snd_map_prod)
have "fst inc ∈ del_idxs" by (metis fsta ncinc fst_conv fst_map_prod id_apply)
then have iatm: "?eq_iatm_poly inc" using tons_del in_set_conv_nth incs by metis
have ism: "is_monom (poly nc)" using ncinc2 iatm single_var_poly_is_monom
by (metis single_var_poly_is_monom normalize_ns_constraint_vars_eq)
then have "monom_var (poly nc) = atom_var (snd iatm)" using iatm
using monom_var_in_vars ncinc2 normalize_ns_constraint_vars_eq by auto
then have "atom_var (snd a) = atom_var (snd iatm)"
by (cases "poly nc", metis anc ism atom_var.simps lec_of_nsc.cases monom_to_atom.simps
poly.simps qdelta_constraint_to_atom.simps)
}
ultimately have "atom_var (snd a) = atom_var (snd iatm) ⟷ fst a ∈ del_idxs" by auto
}
then show ?thesis by auto
qed
then have as_s'': "∀a ∈ set as. atom_var (snd a) = atom_var (snd iatm) ⟷ a ∈ as_s - as_s'"
using Jidx2 as_s_def as_s'_def Diff_Int_distrib Int_iff Sigma_Diff_distrib1 vimage_eq vimage_fst
by auto
have l3s_inv_s: "invariant_s tt as_s l3s" using inv_nsc prepr as_s_def by simp
obtain t iub ilb v c uc where l3s_descrip: "l3s = (State t ilb iub v c uc)"
using Simplex.state.exhaust by blast
obtain t' iub' ilb' v' c' uc' where "l3s' = (State t' ilb' iub' v' c' uc')"
using Simplex.state.exhaust by blast
then have l3s'_descrip: "l3s' = (State t ilb' iub' v c uc)" using l3s_descrip assms(4) 1 2
unfolding del_atom_from_state''_def by auto
then have ilb': "ilb' = Mapping.delete (atom_var (snd iatm)) ilb"
using assms(4) l3s_descrip 1 2 unfolding del_atom_from_state''_def by auto
have iub': "iub' = Mapping.delete (atom_var (snd iatm)) iub" using assms(4) l3s_descrip
l3s'_descrip 1 2 unfolding del_atom_from_state''_def by auto
have bnds_eq_l: "ℬ⇩l l3s' x ≠ None ⟹ ℬ⇩l l3s' x = ℬ⇩l l3s x" for x
by (metis l3s'_descrip ilb' boundsl_def comp_apply mapping_del option.simps(8) state.sel(2)
l3s_descrip)
have bnds_eq_u: "ℬ⇩u l3s' x ≠ None ⟹ ℬ⇩u l3s' x = ℬ⇩u l3s x" for x
by (metis l3s'_descrip iub' boundsu_def comp_apply mapping_del option.simps(8) state.sel(3)
l3s_descrip)
have l3s'_inv_s: "invariant_s tt as_s' l3s'"
proof -
have "¬ 𝒰 l3s'" using l3s'_descrip l3s_descrip l3s_inv_s unfolding invariant_s_def
using Incremental_State_Ops_Simplex_Default.invariant_sD(1) l3s_inv_s state.sel(5) by blast
moreover have "△ (𝒯 l3s')"
using l3s_descrip l3s'_descrip l3s_inv_s Incremental_State_Ops_Simplex_Default.invariant_sD(3)
by fastforce
moreover have "∇ l3s'"
proof -
have "∇ l3s" using l3s_inv_s Incremental_State_Ops_Simplex_Default.invariant_sD(4) by blast
then show ?thesis using l3s_descrip l3s'_descrip by (simp add: tableau_valuated_def)
qed
moreover have "◇ l3s'"
using l3s_inv_s Incremental_State_Ops_Simplex_Default.invariant_sD(5) bnds_eq_l bnds_eq_u
by (metis bounds_consistent_def)
moreover have "(∀ v :: (nat ⇒ QDelta). v ⊨⇩t 𝒯 l3s' ⟷ v ⊨⇩t tt)"
using l3s_descrip l3s'_descrip
Incremental_State_Ops_Simplex_Default.invariant_sD(9)[OF l3s_inv_s] by simp
moreover have "⊨⇩n⇩o⇩l⇩h⇩s l3s'"
proof -
have "(∀ x ∈ (- lvars t). ⟨v⟩ x ≥⇩l⇩b ℬ⇩l l3s x ∧ ⟨v⟩ x ≤⇩u⇩b ℬ⇩u l3s x)"
using curr_val_satisfies_no_lhs_def satisfies_bounds_set_iff l3s_descrip l3s_inv_s
Incremental_State_Ops_Simplex_Default.invariant_sD(2)
by (metis state.sel(1) state.sel(4))
then have "(∀ x ∈ (- lvars t). ⟨v⟩ x ≥⇩l⇩b ℬ⇩l l3s' x ∧ ⟨v⟩ x ≤⇩u⇩b ℬ⇩u l3s' x)"
using bnds_eq_l bnds_eq_u option.case_eq_if l3s_descrip l3s'_descrip ilb'
unfolding ge_lbound_def gelb_def le_ubound_def leub_def by (metis (no_types, lifting))
then show ?thesis
using l3s'_descrip l3s_descrip l3s_inv_s Incremental_State_Ops_Simplex_Default.invariant_sD(2)
by (metis curr_val_satisfies_no_lhs_def satisfies_bounds_set_iff state.sel(1) state.sel(4))
qed
moreover have indval': "index_valid as_s' l3s'"
proof -
have ind_val: "index_valid as_s l3s" using inv_nsc l3s_inv_s unfolding as_s_def
using Incremental_State_Ops_Simplex_Default.invariant_sD(8) by blast
{
fix x b j
assume lkp: "Mapping.lookup ilb' x = Some (j,b)"
then have xneq: "x ≠ atom_var (snd iatm)" using ilb' by auto
then have "Mapping.lookup ilb x = Some (j,b)" using l3s_descrip l3s'_descrip ilb' lkp by simp
then have "(j, Geq x b) ∈ as_s" using ind_val by (simp add: index_valid_def l3s_descrip)
moreover have "(j, Geq x b) ∈ set as"
using index_valid_def l3s_descrip ind_val as_s_def calculation by blast
ultimately have "(j, Geq x b) ∈ as_s'" using as_s'' xneq by auto
}
moreover
{
fix x b j
assume lkp: "Mapping.lookup iub' x = Some (j,b)"
then have xneq: "x ≠ atom_var (snd iatm)" using iub' by auto
then have "Mapping.lookup iub x = Some (j,b)" using l3s_descrip l3s'_descrip iub' lkp by simp
then have "(j, Leq x b) ∈ as_s" using ind_val by (simp add: index_valid_def l3s_descrip)
moreover have "(j, Leq x b) ∈ set as"
using index_valid_def l3s_descrip ind_val as_s_def calculation by blast
ultimately have "(j, Leq x b) ∈ as_s'" using as_s'' xneq by auto
}
ultimately show ?thesis using l3s'_descrip unfolding index_valid_def by simp
qed
moreover have "Simplex.flat as_s' ≐ ℬ l3s'"
proof -
have doteq: "Simplex.flat as_s ≐ ℬ l3s"
using l3s_descrip l3s_inv_s Incremental_State_Ops_Simplex_Default.invariant_sD(6) by auto
let ?upd = "(if ℬ⇩l l3s (atom_var (snd iatm)) = None then
(if ℬ⇩u l3s (atom_var (snd iatm)) = None then 0 else the (ℬ⇩u l3s (atom_var (snd iatm))))
else the (ℬ⇩l l3s (atom_var (snd iatm))))"
have "∀v'. v' ⊨⇩a⇩s (Simplex.flat as_s') ⟶ v' ⊨⇩b ℬ l3s'"
proof (rule ccontr)
assume "¬ (∀v'. v' ⊨⇩a⇩s (Simplex.flat as_s') ⟶ v' ⊨⇩b ℬ l3s')"
from this obtain v'
where v'as: "v' ⊨⇩a⇩s (Simplex.flat as_s')" and nv'B: "¬ (v' ⊨⇩b ℬ l3s')" by auto
then have "∃x. (v' x <⇩l⇩b (ℬ⇩l l3s') x ∨ v' x >⇩u⇩b (ℬ⇩u l3s') x)"
using neg_bounds_compare(3) neg_bounds_compare(7) satisfies_bounds_iff by blast
from this obtain x where "(v' x <⇩l⇩b (ℬ⇩l l3s') x ∨ v' x >⇩u⇩b (ℬ⇩u l3s') x)" by auto
moreover {
assume "v' x <⇩l⇩b (ℬ⇩l l3s') x"
moreover then have "(ℬ⇩l l3s') x ≠ None"
by (smt bound_compare_defs(15) bound_compare_defs(5) bounds_compare_contradictory(7)
option.case_eq_if)
then obtain i b where "Mapping.lookup (ℬ⇩i⇩l l3s') x = Some (i, b)" using boundsl_def
by (metis None_eq_map_option_iff comp_apply old.prod.exhaust option.exhaust)
moreover then have "(ℬ⇩l l3s') x = Some b" by (simp add: boundsl_def)
moreover have "v' x < b" using calculation by (simp add: boundsl_def)
have "¬ (v' ⊨⇩a (Geq x b))" using calculation by simp
ultimately moreover have "(i, Geq x b) ∈ as_s'" using indval' by (simp add: index_valid_def)
then have "Geq x b ∈ Simplex.flat as_s'" by force
ultimately have "¬ (v' ⊨⇩a⇩s Simplex.flat as_s')" by (meson satisfies_atom_set_def)
} moreover
{
assume "v' x >⇩u⇩b (ℬ⇩u l3s') x"
moreover then have "(ℬ⇩u l3s') x ≠ None"
using bound_compare_defs(10) bound_compare_defs(2) option.case_eq_if by metis
then obtain i b where "Mapping.lookup (ℬ⇩i⇩u l3s') x = Some (i, b)" using boundsu_def
by (metis None_eq_map_option_iff comp_apply old.prod.exhaust option.exhaust)
moreover then have "(ℬ⇩u l3s') x = Some b" by (simp add: boundsu_def)
moreover then have "v' x > b" using calculation by simp
have "¬ (v' ⊨⇩a (Leq x b))" using calculation by simp
ultimately moreover have "(i, Leq x b) ∈ as_s'" using indval' by (simp add: index_valid_def)
then have "Leq x b ∈ Simplex.flat as_s'" by force
ultimately have "¬ (v' ⊨⇩a⇩s Simplex.flat as_s')" by (meson satisfies_atom_set_def)
}
ultimately show False using v'as by auto
qed
moreover
{
fix v'
define v where "v = v' ((atom_var (snd iatm)) := ?upd)"
assume v'b: "v' ⊨⇩b ℬ l3s'"
then have "v ⊨⇩b ℬ l3s"
proof -
{
fix x
have "v x ≥⇩l⇩b (ℬ⇩l l3s) x ∧ v x ≤⇩u⇩b (ℬ⇩u l3s) x"
proof (cases "x = (atom_var (snd iatm))")
case True
then show ?thesis using bound_compare_defs option.case_eq_if
by (smt Incremental_State_Ops_Simplex_Default.invariant_sD(5)
bounds_consistent_leq_ub fun_upd_same l3s_inv_s option.expand option.sel
option.simps(3) v_def)
next
case False
then have "v x ≥⇩l⇩b (ℬ⇩l l3s') x ∧ v x ≤⇩u⇩b (ℬ⇩u l3s') x"
using v'b ilb' iub' l3s'_descrip l3s_descrip satisfies_bounds_iff
by (metis (no_types, lifting) fun_upd_other v_def)
then show ?thesis using False
by (simp add: boundsl_def boundsu_def ilb' iub' l3s'_descrip l3s_descrip)
qed
}
then show ?thesis using satisfies_bounds_iff by blast
qed
then have "v ⊨⇩a⇩s (Simplex.flat as_s)" using doteq atoms_equiv_bounds.simps by blast
then have vas: "v ⊨⇩a⇩s (Simplex.flat as_s')" using as_s'_def
by (simp add: Jidx Sigma_Diff_distrib1 as_s_def satisfies_atom_set_def)
then have "v' ⊨⇩a⇩s (Simplex.flat as_s')"
proof -
have xneq: "∀x. x ≠ atom_var (snd iatm) ⟶ v' x = v x" using v_def by simp
have "∀a ∈ Simplex.flat as_s'. atom_var a ≠ atom_var (snd iatm)" using as_s'' as_s'_def by blast
then have "∀a ∈ Simplex.flat as_s'. v' ⊨⇩a a ⟷ v ⊨⇩a a" using xneq
by (metis (full_types) atom_var.simps nsc_of_atom.cases satisfies_atom.simps
satisfies_atom_set_def vas)
then show ?thesis using vas by (simp add: satisfies_atom_set_def)
qed
}
ultimately have "(∀ v. v ⊨⇩a⇩s Simplex.flat as_s' ⟷ v ⊨⇩b ℬ l3s')" by auto
then show ?thesis by (simp add: atoms_equiv_bounds_simps)
qed
moreover have "as_s' ⊨⇩i ℬℐ l3s'"
proof -
have BIl: "(ℬ⇩l l3s') x ≠ None ⟹ (ℐ⇩l l3s') x ∉ del_idxs" for x
proof -
assume "(ℬ⇩l l3s') x ≠ None"
then obtain i b where "Mapping.lookup (ℬ⇩i⇩l l3s') x = Some (i, b)" using boundsl_def
by (metis None_eq_map_option_iff comp_apply old.prod.exhaust option.exhaust)
moreover then have "(ℐ⇩l l3s') x = i" by (simp add: indexl_def)
moreover have "(i, Geq x b) ∈ as_s'" using indval' calculation by (simp add: index_valid_def)
ultimately have "(ℐ⇩l l3s') x ∉ del_idxs" using as_s'' IntE as_s' as_s'_def by auto
then show ?thesis by simp
qed
have BIu: "(ℬ⇩u l3s') x ≠ None ⟹ (ℐ⇩u l3s') x ∉ del_idxs" for x
proof -
assume "(ℬ⇩u l3s') x ≠ None"
then obtain i b where "Mapping.lookup (ℬ⇩i⇩u l3s') x = Some (i, b)" using boundsu_def
by (metis None_eq_map_option_iff comp_apply old.prod.exhaust option.exhaust)
moreover then have "(ℐ⇩u l3s') x = i" by (simp add: indexu_def)
moreover have "(i, Leq x b) ∈ as_s'" using indval' calculation by (simp add: index_valid_def)
ultimately have "(ℐ⇩u l3s') x ∉ del_idxs" using as_s'' IntE as_s' as_s'_def by auto
then show ?thesis by simp
qed
{
fix I v
assume "(I,v) ⊨⇩i⇩a⇩s as_s'"
then have "(I - del_idxs, v) ⊨⇩i⇩a⇩s as_s" using Jidx as_s'_def as_s_def
by (metis Int_Diff Diff_Int2 Diff_Int_distrib2
Incremental_Atom_Ops_For_NS_Constraint_Ops_Default.i_satisfies_atom_set_inter_right)
then have "(I - del_idxs, v) ⊨⇩i⇩b ℬℐ l3s" by (meson atoms_imply_bounds_index.elims(2)
Incremental_State_Ops_Simplex_Default.invariant_sD(7) l3s_inv_s)
then have Idib: "(I - del_idxs, v) ⊨⇩i⇩b ℬℐ l3s'" using l3s'_descrip l3s_descrip ilb' iub'
by (simp add: boundsl_def boundsu_def indexl_def indexu_def satisfies_bounds_index.simps)
have "(I, v) ⊨⇩i⇩b ℬℐ l3s'"
proof -
{
fix x c
have "((ℬ⇩l l3s') x = Some c ⟶ (ℐ⇩l l3s') x ∈ I ⟶ v x ≥ c) ∧
((ℬ⇩u l3s') x = Some c ⟶ (ℐ⇩u l3s') x ∈ I ⟶ v x ≤ c)"
using BIl BIu Idib satisfies_bounds_index.simps by (simp add: satisfies_bounds_index.simps)
}
then show ?thesis by (simp add: satisfies_bounds_index.simps)
qed
}
then show ?thesis using atoms_imply_bounds_index.simps by blast
qed
ultimately show ?thesis unfolding Incremental_State_Ops_Simplex_Default.invariant_s_def
by (metis (no_types, lifting))
qed
have "invariant_nsc tons (set J) ((asi, tv, ui), l3s')"
proof -
have "Incremental_Atom_Ops_For_NS_Constraint_Ops.invariant_as_asi (set as) asi tv tv' ui ui'"
using inv_nsc prepr s'id by simp
moreover have "invariant_s tt (set as ∩ ((set J) × UNIV)) l3s' ∧ (set J) ∩ set ui' = {}"
using l3s'_inv_s as_s'_def prepr inv_nsc Jidx by auto
ultimately show ?thesis using prepr by simp
qed
then have "invariant_simplex cs' (set J) s'" using tons_def
by (metis "1" Incremental_Simplex.invariant_cs.simps assms(1) assms(2) invariant_simplex.simps
state_invariant_def s'id)
then show ?thesis using J by blast
qed
lemma bnb_update_assertall:
assumes "state_invariant cs Is lb ub s"
"cs' = i_bounds_to_constraints Is lb ub @ cs"
"suitable_upd_atom iatm cs'"
"atom_var (snd iatm) ∈ set Is"
"assert_all_simplex (remove1 (fst iatm) (map fst cs')) (del_atom_from_state'' s iatm) = Sat s'"
shows "invariant_simplex cs' (set (remove1 (fst iatm) (map fst cs'))) s'"
proof -
define Ai where "Ai = (remove1 (fst iatm) (map fst cs'))"
let ?s' = "del_atom_from_state'' s iatm"
obtain J where "set J ⊆ (set Ai)" and "invariant_simplex cs' (set J) ?s'"
using assms bnb_update_del unfolding Ai_def by blast
then show ?thesis using Ai_def assert_all_simplex_ok assms(4) le_iff_sup assms by metis
qed
lemma bnb_update1:
assumes
"checked_bnc cs Is lb ub s"
"cs' = i_bounds_to_constraints Is lb ub @ cs"
"suitable_upd_atom iatm cs'"
"idx_list = map fst cs'"
shows "∃s'. assert_all_simplex (remove1 (fst iatm) idx_list) (del_atom_from_state'' s iatm) = Sat s'
∧ invariant_simplex cs' (set (remove1 (fst iatm) idx_list)) s'"
proof -
define d where "d = del_atom_from_state'' s iatm"
have "state_invariant cs Is lb ub s"
using assms checked_invariant_bnc by auto
then obtain js where js: "set js ⊆ set (remove1 (fst iatm) (map fst cs'))" "invariant_simplex cs' (set js) d"
using assms bnb_update_del unfolding d_def by blast
have "set (remove1 (fst iatm) (map fst cs')) = fst ` set cs' - {fst iatm}"
apply(subst set_remove1_eq)
using assms enumerated_distinct[of 0 cs'] enumerated_sorted unfolding checked_bnc_def by (auto simp add: Let_def)
have "∃s'. assert_all_simplex (remove1 (fst iatm) idx_list) d = Sat s'"
proof (rule ccontr)
assume "∄s'. assert_all_simplex (remove1 (fst iatm) idx_list) d = Inr s'"
then have "∃ix. assert_all_simplex (remove1 (fst iatm) idx_list) d = Unsat ix"
by (meson sumE)
then obtain ix where ix: "assert_all_simplex (remove1 (fst iatm) idx_list) d = Unsat ix"
by blast
have "minimal_unsat_core (set ix) cs'"
using assert_all_simplex_unsat js ix by blast
moreover have "(fst `set cs', solution_simplex s) ⊨⇩i⇩c⇩s set cs'"
by (intro solution_simplex) (use assms in ‹auto simp add: checked_bnc_def Let_def›)
ultimately show False
unfolding minimal_unsat_core_def by force
qed
then obtain s' where s': "assert_all_simplex (remove1 (fst iatm) idx_list) d = Sat s'"
by blast
then have "invariant_simplex cs' (set js ∪ set (remove1 (fst iatm) idx_list)) s'"
using js by (auto intro: assert_all_simplex_ok)
also have "set js ∪ set (remove1 (fst iatm) idx_list) = set (remove1 (fst iatm) idx_list)"
using js assms by blast
finally show ?thesis
using s' by (auto simp add: d_def)
qed
lemma NAME_ME1: "x ∈ set xs ⟹ insert x (set (remove1 x xs)) = set xs"
by (induction xs) (auto)
lemma Var_eqI: "Var x = Var y ⟹ x = y"
using coeff_Var2 by force
lemma concat_map_list_update: "(∀x ∈ set cs ∪ {x}. f x = [hd (f x)]) ⟹
concat (map f (cs[i := x])) = (concat (map f cs))[i := hd (f x)]"
proof (induction cs arbitrary: i)
case (Cons c cs)
show ?case
proof (cases "i = 0")
case False
have "concat (map f ((c # cs)[i := x])) = f c @ concat (map f (cs[i - 1 := x]))"
using False by (auto split: nat.splits)
also have "concat (map f (cs[i - 1 := x])) = (concat (map f cs))[i - 1 := hd (f x)]"
using Cons by simp
also have "f c @ … = hd (f c) # (concat (map f cs))[i - 1 := hd (f x)]"
using Cons by auto
also have "… = (hd (f c) # (concat (map f cs)))[i := hd (f x)]"
using False by (auto split: nat.splits)
also have "hd (f c) # (concat (map f cs)) = (f c) @ (concat (map f cs))"
using Cons by simp
finally show ?thesis
using Cons False by (auto split: nat.splits)
next
case True
have "(f c @ concat (map f cs)) = hd (f c) # concat (map f cs)"
using Cons by auto
then show ?thesis
using Cons True by (auto) (metis append_Cons list_update_code(2))
qed
qed (auto)
lemma concat_map: "(∀x ∈ set cs. f x = [hd (f x)]) ⟹
concat (map f cs) = (map (hd ∘ f) cs)"
by (induction cs) (auto)
lemma max_var_Var: "max_var (Var x) = x"
proof -
have "Var x ≠ 0"
by (metis empty_iff insertI1 vars_Var vars_zero)
then show ?thesis
unfolding Abstract_Linear_Poly.max_var_def by (simp)
qed
lemma start_fresh_variable_append: "start_fresh_variable (xs @ ys) =
max (start_fresh_variable xs) (start_fresh_variable ys)"
by (induction xs) auto
lemma start_fresh_variable_Max:
shows "start_fresh_variable xs =
(if xs = [] then 0 else Max (set (map (Branch_and_Bound.max_var ∘ poly ∘ snd) xs)) + 1)"
by (induction xs) (auto)
locale preprocess'L
begin
fun p_mapping where
"p_mapping [] x = (Map.empty, x)" |
"p_mapping ((i,nc)#ncs) x = (let (m', x') = p_mapping ncs x; p = poly nc
in
if (is_monom p) then (m', x')
else if p = 0 then (m', x')
else (case m' p of Some v ⇒ (m', x')
| None ⇒ (m' (p ↦ x'), x' + 1)))"
lemma p_mapping: "S = preprocess' ncs x ⟹ p_mapping ncs x = (m, x') ⟹
(Poly_Mapping S = m ∧ FirstFreshVariable S = x')"
proof (induction ncs x arbitrary: m x' S rule: p_mapping.induct)
case (2 i nc ncs x)
define p where "p = poly nc"
obtain m' x'' where mx': "p_mapping ncs x = (m',x'')"
using prod_cases by fastforce
have m': "m' = Poly_Mapping (preprocess' ncs x)"
using 2 mx' by blast
have x'': "x'' = FirstFreshVariable (preprocess' ncs x)"
using 2 mx' by blast
consider (a) "is_monom p ∨ p = 0 ∨ (∃v. m' p = Some v)" | (b) "¬ is_monom p ∧ p ≠ 0 ∧ m' p = None"
by fastforce
then show ?case
proof (cases)
case a
show ?thesis
using 2 m' p_def x'' mx' a by (auto simp add: Let_def)
next
case b
show ?thesis
using 2 m' p_def x'' mx' b by (fastforce simp add: Let_def)
qed
qed (auto)
lemma preprocess'_mapping_Some:
"S = preprocess' ncs x ⟹ m = Poly_Mapping S ⟹ (i, nc) ∈ set ncs ⟹
¬ is_monom (Simplex.poly nc) ⟹ Simplex.poly nc ≠ 0 ⟹
(∃v. m (poly nc) = Some v)"
by(induction ncs x arbitrary: m S rule: preprocess'.induct)
(auto simp add: Let_def split: if_splits option.splits)
fun
atoms where
"atoms m [] = []"
| "atoms m ((i,nc) # ncs) = (let p = poly nc; as' = atoms m ncs in
if (is_monom p) then ((i, qdelta_constraint_to_atom nc 0) # as')
else if p = 0 then as'
else (case m p of Some v ⇒ ((i,qdelta_constraint_to_atom nc v) # as') |
None ⇒ as'))"
lemma atoms:
assumes S: "S = preprocess' ncs x" and m: "m = Poly_Mapping S" and
"⋀nc i. (i, nc) ∈ set ncs ⟹ m' (poly nc) = m (poly nc)"
shows "Atoms S = atoms m' ncs"
using assms proof (induction ncs x arbitrary: m' m S rule: preprocess'.induct)
case (1 v)
then show ?case by (auto)
next
case (2 i nc ncs x)
define p where "p = poly nc"
define m'' where "m'' = Poly_Mapping (preprocess' ncs x)"
define x'' where "x'' = FirstFreshVariable (preprocess' ncs x)"
consider (a) "is_monom p" | (b) "¬ is_monom p ∧ p = 0" | (c) "¬ is_monom p ∧ p ≠ 0 ∧ m'' p = None"
| (d) "¬ is_monom p ∧ p ≠ 0 ∧ (∃v. m'' p = Some v)"
by fastforce
then show ?case
proof (cases)
case a
then show ?thesis
using 2 p_def by (cases nc) (fastforce split: atom.split simp add: Let_def)+
next
case b
then show ?thesis
using 2 p_def by (fastforce simp add: Let_def)
next
case c
then have mp: "Some x''= m p"
using 2 p_def m''_def x''_def by (auto simp add: Let_def)
also have "m p = m' p"
unfolding p_def using 2 by fastforce
finally have mp: "m' p = Some x''"
by simp
then have "Atoms S = (i, qdelta_constraint_to_atom nc x'') # Atoms (preprocess' ncs x)"
using c 2 p_def m''_def x''_def by (auto simp add: Let_def map_update split: option.split if_splits)
also have "Atoms (preprocess' ncs x) = atoms m' ncs"
proof -
have "m'' (poly nc') = m (poly nc')" if "(i', nc') ∈ set ncs" for i' nc'
using option.simps(3) preprocess'_mapping_Some 2 that m''_def c
apply (auto split: option.splits if_splits prod.splits simp add: Let_def)
by (metis option.distinct(1) preprocess'L.preprocess'_mapping_Some)
also have "m (poly nc') = m' (poly nc')" if "(i', nc') ∈ set ncs" for i' nc'
using 2 that by fastforce
finally show ?thesis
using m''_def 2 by (intro 2(1)[of _ m'']) (auto)
qed
also have "(i, qdelta_constraint_to_atom nc x'') # … = atoms m' ((i, nc) # ncs)"
using c p_def mp by (auto simp add: Let_def map_update split: option.split if_splits)
finally show ?thesis
by simp
next
case d
then obtain v where v_def: "m'' p = Some v"
by blast
have mp: "m'' p = m p"
using 2 d p_def m''_def by (auto simp add: Let_def)
also have "m p = m' p"
unfolding p_def using 2 by fastforce
finally have mp: "m' p = Some v"
using v_def by simp
then have "Atoms S = (i, qdelta_constraint_to_atom nc v) # Atoms (preprocess' ncs x)"
using d 2 p_def m''_def v_def x''_def by (auto simp add: Let_def map_update split: option.split if_splits)
also have "Atoms (preprocess' ncs x) = atoms m' ncs"
proof -
have "m'' (poly nc') = m (poly nc')" if "(i', nc') ∈ set ncs" for i' nc'
using option.simps(3) preprocess'_mapping_Some 2 that m''_def d
apply (auto split: option.splits if_splits prod.splits simp add: Let_def)
by (metis option.distinct(1) preprocess'L.preprocess'_mapping_Some)
also have "m (poly nc') = m' (poly nc')" if "(i', nc') ∈ set ncs" for i' nc'
using 2 that by fastforce
finally show ?thesis
using m''_def 2 by (intro 2(1)[of _ m'']) (auto)
qed
also have "(i, qdelta_constraint_to_atom nc v) # … = atoms m' ((i, nc) # ncs)"
using d p_def mp by (auto simp add: Let_def map_update split: option.split if_splits)
finally show ?thesis
by simp
qed
qed
lemma atoms_append: "atoms m (ncs @ mcs) = atoms m ncs @ atoms m mcs"
by (induction m ncs rule: atoms.induct) (auto simp add: Let_def split: option.splits)
lemma atoms_map:
assumes "⋀i nc. (i, nc) ∈ set ncs ⟹ is_monom (Simplex.poly nc)"
shows "atoms m ncs = map (λ(i, nc). (i, qdelta_constraint_to_atom nc 0)) ncs"
using assms
by (induction m ncs rule: atoms.induct) (fastforce simp add: Let_def split: option.split)+
lemma atoms_index:
assumes "i ∈ set (map fst (atoms m ncs))"
shows "i ∈ set (map fst ncs)"
using assms
by (induction m ncs rule: atoms.induct) (auto simp add: Let_def split: if_splits option.splits)
fun
alt where
"alt [] s = s"
| "alt ((i,h) # t) s = (let s' = alt t s; p = poly h; is_monom_h = is_monom p;
v' = FirstFreshVariable s';
t' = Tableau s';
a' = Atoms s';
m' = Poly_Mapping s';
u' = UnsatIndices s' in
if is_monom_h then IState v' t'
((i,qdelta_constraint_to_atom h v') # a') m' u'
else if p = 0 then
if zero_satisfies h then s' else
IState v' t' a' m' (i # u')
else (case m' p of Some v ⇒
IState v' t' ((i,qdelta_constraint_to_atom h v) # a') m' u'
| None ⇒ IState (v' + 1) (linear_poly_to_eq p v' # t')
((i,qdelta_constraint_to_atom h v') # a') (m' (p ↦ v')) u'))"
lemma alt:
assumes "s = IState x [] [] Map.empty []"
shows "preprocess' ncs x = alt ncs s"
using assms by (induction ncs x rule: preprocess'.induct) auto
lemma alt_append:
assumes "s⇩1 = alt ncs' s⇩0" "s⇩2 = alt ncs s⇩1"
shows "s⇩2 = alt (ncs @ ncs') s⇩0"
using assms by (induction ncs s⇩0 arbitrary: s⇩1 s⇩2 rule: alt.induct) auto
lemma UnsatIndices:
assumes "ncs⇩f = filter (λ(i, nc). Simplex.poly nc = 0) ncs"
shows "UnsatIndices (preprocess' ncs x) = UnsatIndices (preprocess' ncs⇩f x)"
using assms
by (induction ncs x arbitrary: ncs⇩f rule: preprocess'.induct) (auto simp add: Let_def split: option.split)
lemma Tableau':
assumes "ncs⇩f = filter (λ(i, nc). ¬ is_monom (poly nc) ∧ Simplex.poly nc ≠ 0) ncs"
shows "Tableau (preprocess' ncs x) = Tableau (preprocess' ncs⇩f x) ∧ FirstFreshVariable (preprocess' ncs x) = FirstFreshVariable (preprocess' ncs⇩f x)
∧ Poly_Mapping (preprocess' ncs x) = Poly_Mapping (preprocess' ncs⇩f x)"
using assms
by (induction ncs x arbitrary: ncs⇩f rule: preprocess'.induct) (auto simp add: Let_def split: option.split)
lemma Atoms':
assumes "ncs⇩f = filter (λ(i, nc). Simplex.poly nc ≠ 0) ncs"
shows "Atoms (preprocess' ncs x) = Atoms (preprocess' ncs⇩f x) ∧ FirstFreshVariable (preprocess' ncs x) = FirstFreshVariable (preprocess' ncs⇩f x)
∧ Poly_Mapping (preprocess' ncs x) = Poly_Mapping (preprocess' ncs⇩f x)"
using assms
by (induction ncs x arbitrary: ncs⇩f rule: preprocess'.induct) (auto simp add: Let_def split: option.split)
lemma Tableau:
assumes "ncs⇩f = filter (λ(i, nc). ¬ is_monom (poly nc) ∧ Simplex.poly nc ≠ 0) ncs"
shows "Tableau (preprocess' ncs x) = Tableau (preprocess' ncs⇩f x)"
using assms Tableau' by (auto)
lemma Poly_Mapping:
assumes "ncs⇩f = filter (λ(i, nc). ¬ is_monom (poly nc) ∧ Simplex.poly nc ≠ 0) ncs"
shows "Poly_Mapping (preprocess' ncs x) = Poly_Mapping (preprocess' ncs⇩f x)"
using assms Tableau' by (auto)
end
global_interpretation preprocess': preprocess'L .
lemma enumerated_diff:
"enumerated n xs ⟹ i < length xs ⟹ set xs - {xs ! i} = set xs - {n + i} × UNIV"
apply(induction xs arbitrary: i n)
apply(auto simp del: enumerated.simps)
apply (metis enumerated_nth list.set_intros(1))
apply (metis enumerated_nth insert_iff list.simps(15))
apply (metis enumerated_enumerate length_enumerate length_nth_simps(2) nth_enumerate_eq prod.inject)
by (metis Pair_inject enumerated_enumerate length_Cons length_enumerate nth_enumerate_eq)
lemma filter_list_update:
"¬ P x ⟹ ¬ P (xs ! i) ⟹ filter P xs = filter P (xs[i := x])"
apply(induction xs) apply(auto split: nat.splits)
by (smt filter.simps(2) filter_append list_update_beyond list_update_id not_le_imp_less upd_conv_take_nth_drop)
lemma is_monom_Var: "is_monom (Var x)"
unfolding is_monom_def by (transfer) simp
lemma Var_uneq_0: "(Var x) ≠ 0"
by (transfer) (metis class_field.zero_not_one fun_var_def fun_zero_def)
lemma monom_coeff_Var: "monom_coeff (Var x) = 1"
unfolding monom_coeff_def monom_var_def using coeff_Var1 max_var_Var by auto
lemma monom_var_Var: "monom_var (Var x) = x"
unfolding monom_coeff_def monom_var_def using coeff_Var1 max_var_Var by auto
lemma distinct_map_not_inj: "f x = f y ⟹ x ≠ y ⟹ x ∈ set xs ⟹ y ∈ set xs ⟹ ¬ distinct (map f xs)"
by (induction xs) (auto simp add: rev_image_eqI)
lemma
assumes "checked_bnc acs Is lb ub s"
"x ∈ set Is"
"new = (if t then (fst (lb x), Geq x (rat_of_int y)) else (fst (ub x), Leq x (rat_of_int y)))"
"lb' = (if t then lb(x := (fst (lb x), y)) else lb)"
"ub' = (if t then ub else ub(x := (fst (ub x), y)))"
shows
bnb_update_state_invariant: "bnb_update_state'' acs Is lb' ub' s new = Some s' ⟹
state_invariant acs Is lb' ub' s'" and
bnb_update_state_Unsat: "bnb_update_state'' acs Is lb' ub' s new = None ⟹
∄v. v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb' ub' @ acs))"
proof -
define cs⇩u where "cs⇩u = map (λ x. (fst (ub x), LEQ (Var x) (of_int (snd (ub x))))) Is"
define cs⇩l where "cs⇩l = map (λ x. (fst (lb x), GEQ (Var x) (of_int (snd (lb x))))) Is"
define cs where "cs = i_bounds_to_constraints Is lb ub @ acs"
have cs_app: "cs = (cs⇩l @ cs⇩u) @ acs"
unfolding cs_def cs⇩u_def cs⇩l_def by (auto simp add: i_bounds_to_constraints_def)
define cs' where "cs' = i_bounds_to_constraints Is lb' ub' @ acs"
define ls where "ls = map fst cs"
define i where "i = (if t then fst (lb x) else fst (ub x))"
define ls⇩2 where "ls⇩2 = remove1 (fst new) ls"
define c where "c = (if t then GEQ (Var x) (rat_of_int y) else LEQ (Var x) (rat_of_int y))"
have enumerated_cs: "enumerated 0 cs"
by (metis assms(1) checked_bnc_def cs_def)
have fst_ub': "fst (ub' y) = fst (ub y)" for y
unfolding assms by auto
have fst_lb': "fst (lb' y) = fst (lb y)" for y
unfolding assms by auto
have enumerated_cs': "enumerated 0 cs'"
using enumerated_cs unfolding enumerated[symmetric]
unfolding cs'_def cs_def i_bounds_to_constraints_def fst_ub' fst_lb' by (auto simp add: comp_def)
have length_cs': "length cs' = length cs"
unfolding cs_def cs'_def i_bounds_to_constraints_def by auto
have ls_cs': "ls = map fst cs'"
using enumerated_cs enumerated_cs' length_cs' unfolding enumerated[symmetric] ls_def by simp
have distinct_ls: "distinct ls"
by (metis assms(1) checked_bnc_def cs_def enumerated_distinct ls_def)
have ub_lb1: "fst (ub x) ≠ fst (ub y)" if "x ≠ y" "x ∈ set Is" "y ∈ set Is" for x y
using that cs_def distinct_ls unfolding ls_def i_bounds_to_constraints_def
by (auto simp add: distinct_map_not_inj)
have ub_lb2: "fst (lb x) ≠ fst (lb y)" if "x ≠ y" "x ∈ set Is" "y ∈ set Is" for x y
using that cs_def distinct_ls unfolding ls_def i_bounds_to_constraints_def
by (auto simp add: distinct_map_not_inj)
have ub_lb': "fst (ub x) ≠ fst (lb y)" if "x ∈ set Is" "y ∈ set Is" for x y
using that cs_def distinct_ls unfolding ls_def i_bounds_to_constraints_def by (auto)
have i_acs: "i ∉ fst ` set acs"
using cs_def distinct_ls unfolding ls_def i_bounds_to_constraints_def i_def
using assms disjoint_iff_not_equal image_eqI by auto
have i_ls: "i ∈ set ls"
using cs_def unfolding ls_def i_bounds_to_constraints_def i_def
using assms by auto
have i_length_cs: "i < length cs"
using i_ls enumerated_cs unfolding ls_def enumerated[symmetric] by simp
have set_cs': "set cs' = set (cs[i := (i, c)])"
proof -
have 1: "set cs - {cs ! i} = set cs - {i} × UNIV"
using i_length_cs enumerated_cs by (subst enumerated_diff[of 0]) auto
show ?thesis
unfolding c_def
apply(subst set_update_distinct)
defer defer
apply(subst 1) apply(simp add: assms(5) cs'_def cs_def)
apply(auto simp add: i_def i_bounds_to_constraints_def assms)
apply (metis assms(2) ub_lb2)
apply (simp add: assms(2) ub_lb2)
using assms(2) ub_lb' apply fastforce
using i_acs i_def image_iff apply fastforce
using assms(2) ub_lb' apply blast
apply (metis assms(2) ub_lb1)
apply (simp add: assms(2) ub_lb1)
using i_acs i_def image_iff apply fastforce
using distinct_map enumerated_cs apply blast
using i_def i_length_cs by auto[2]
qed
have cs': "cs' = cs[i := (i, c)]"
using enumerated_cs' enumerated_cs set_cs' length_cs'
by (intro enumerated_set_unique[of 0]) (auto intro: enumerated_update)
have enumerated_cs⇩l⇩u: "enumerated 0 (cs⇩l @ cs⇩u)"
using enumerated_cs enumerated_append unfolding cs_def cs⇩u_def cs⇩l_def i_bounds_to_constraints_def
by blast
have i_length_Is: "i < length Is + length Is"
proof -
have "i ∈ set (map fst (i_bounds_to_constraints Is lb ub))"
unfolding i_def i_bounds_to_constraints_def using assms by simp
moreover have "enumerated 0 (i_bounds_to_constraints Is lb ub)"
using enumerated_cs enumerated_append unfolding cs_def by auto
ultimately have "i < length (map fst (i_bounds_to_constraints Is lb ub))"
unfolding enumerated[symmetric] by auto
then show ?thesis
unfolding i_bounds_to_constraints_def by simp
qed
have cs'': "cs' = (cs⇩l @ cs⇩u)[i := (i, c)] @ acs"
unfolding cs' cs_app cs⇩l_def cs⇩u_def using i_length_Is by (subst list_update_append1) auto
have "to_ns cs' = to_ns ((cs⇩l @ cs⇩u)[i := (i, c)]) @ to_ns acs"
unfolding cs'' to_ns_def by (simp)
also have "… = map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)[i := (i, c)]) @ to_ns acs"
proof -
have "to_ns ((cs⇩l @ cs⇩u)[i := (i, c)]) =
map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)[i := (i, c)])"
proof -
have "∀d ∈ insert (i,c) (set (cs⇩l @ cs⇩u)).
i_constraint_to_qdelta_constraint d = [hd (i_constraint_to_qdelta_constraint d)]"
unfolding cs⇩l_def cs⇩u_def c_def by (auto)
then show ?thesis
using set_update_subset_insert unfolding to_ns_def by (subst concat_map) fast+
qed
then show ?thesis
using assms by (auto simp add: map_update c_def atom_to_qdnsconstr_def)
qed
finally have to_ns_cs':
"to_ns cs' = map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)[i := (i, c)]) @ to_ns acs"
by simp
also have "(map (map_prod id normalize_ns_constraint) …) =
(map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)[i := (i, c)])) @
map (map_prod id normalize_ns_constraint) (to_ns acs)"
proof -
have "(a, b) ∈ insert (i,c) (set (cs⇩l @ cs⇩u)) ⟹
map_prod id normalize_ns_constraint (hd (map (Pair a) (constraint_to_qdelta_constraint b))) =
hd (map (Pair a) (constraint_to_qdelta_constraint b))" for a b
unfolding cs⇩l_def cs⇩u_def c_def by (auto simp add: max_var_Var coeff_Var1 normalize_ns_constraint.simps)
then show ?thesis
using set_update_subset_insert by (fastforce)
qed
finally have mmn_to_ns_cs':
"map (map_prod id normalize_ns_constraint) (to_ns cs') =
map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)[i := (i, c)]) @
map (map_prod id normalize_ns_constraint) (to_ns acs)"
by blast
have to_ns_cs: "to_ns cs = map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)) @ to_ns acs"
unfolding to_ns_def cs_app unfolding cs⇩l_def cs⇩u_def by (auto simp add: concat_map)
have ls⇩2: "ls⇩2 = remove1 i ls"
unfolding ls⇩2_def i_def using assms by auto
note inv_simps =
Incremental_Simplex.invariant_cs.simps invariant_simplex.simps
Incremental_Atom_Ops_For_NS_Constraint_Ops_Default.invariant_nsc.simps
Incremental_Atom_Ops_For_NS_Constraint_Ops_Default.invariant_as_asi.simps
have "∃y ∈ set (to_ns cs). fst y = i ∧ Simplex.poly (snd y) = Var x"
unfolding cs_app cs⇩l_def cs⇩u_def apply(auto simp add: to_ns_def i_constraint_to_qdelta_constraint_def)
apply(rule bexI[of _ "(i, (if t then GEQ_ns (Var x) (QDelta (rat_of_int (snd (lb x))) 0) else
LEQ_ns (Var x) (QDelta (rat_of_int (snd (ub x))) 0)))"])
using assms by (auto simp add: i_def)
then have "suitable_upd_atom new cs"
unfolding find_index_less_size_conv[symmetric]
unfolding suitable_upd_atom_def by (auto simp add: assms i_def)
then obtain s⇩2 where s⇩2:
"assert_all_simplex ls⇩2 (del_atom_from_state'' s new) = Inr s⇩2"
"invariant_simplex cs (set ls⇩2) s⇩2"
using bnb_update1[OF assms(1) cs_def _ ls_def] unfolding ls⇩2_def by blast
obtain ncs⇩2 as⇩2 tv⇩2 ui⇩2 l3s⇩2 where s⇩2_def: "s⇩2 = Simplex_State (ncs⇩2, (as⇩2, tv⇩2, ui⇩2), l3s⇩2)"
using solution_simplex.cases by blast
obtain t⇩3⇩1 as⇩3⇩1 tv⇩3⇩1 ui⇩3⇩1 where preprocess: "preprocess (to_ns cs') = (t⇩3⇩1, as⇩3⇩1, tv⇩3⇩1, ui⇩3⇩1)"
using prod_cases4 by blast
obtain t⇩2⇩1 as⇩2⇩1 tv⇩2⇩1 ui⇩2⇩1 where preprocess_cs: "preprocess (to_ns cs) = (t⇩2⇩1, as⇩2⇩1, tv⇩2⇩1, ui⇩2⇩1)"
using prod_cases4 by blast
define s⇩3 where "s⇩3 = update_iatom_in_state' s⇩2 new"
obtain ncs⇩3 as⇩3 tv⇩3 ui⇩3 l3s⇩3 where s⇩3: "s⇩3 = Simplex_State (ncs⇩3, (as⇩3, tv⇩3, ui⇩3), l3s⇩3)"
using solution_simplex.cases by blast
define qda where "qda = atom_to_qdatom (snd new)"
have as⇩3: "as⇩3 = Mapping.update i [(i, qda)] as⇩2"
using s⇩3 unfolding s⇩2_def s⇩3_def update_iatom_in_state'_def assms i_def qda_def by (auto)
have cs'_to_ns: "to_ns cs' = (to_ns cs)[i := (i, atom_to_qdnsconstr (snd new))]"
using assms i_length_Is unfolding to_ns_cs to_ns_cs' by (subst (2) list_update_append1)
(auto simp add: list_update_append1 map_update c_def atom_to_qdnsconstr_def cs⇩l_def cs⇩u_def)
define ncs where "ncs = (map (map_prod id normalize_ns_constraint) (to_ns cs))"
have ncs: "ncs = (map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u))) @
map (map_prod id normalize_ns_constraint) (to_ns acs)"
unfolding ncs_def to_ns_cs using max_var_Var
by (auto simp add: cs⇩u_def cs⇩l_def normalize_ns_constraint.simps)
define ncs' where "ncs' = ncs[i := (i, (if t then GEQ_ns (Var x) (QDelta (rat_of_int y) 0)
else LEQ_ns (Var x) (QDelta (rat_of_int y) 0)))]"
define sv where "sv = start_fresh_variable ncs"
define sv' where "sv' = start_fresh_variable ncs'"
have ncs': "(map (map_prod id normalize_ns_constraint) (to_ns cs')) = ncs'"
unfolding ncs'_def i_def ncs_def cs'_to_ns by (subst map_update)
(auto simp add: assms atom_to_qdnsconstr_def normalize_ns_constraint.simps max_var_Var)
then have ncs'': "ncs' = map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)[i := (i, c)]) @
map (map_prod id normalize_ns_constraint) (to_ns acs)"
unfolding mmn_to_ns_cs' by auto
have cs⇩l⇩u_x: "(cs⇩l @ cs⇩u) ! i = (i, (if t then GEQ (Var x) (of_int (snd (lb x))) else LEQ (Var x) (of_int (snd (ub x)))))"
apply(subst enumerated_nth[of 0])
apply (simp add: enumerated_cs⇩l⇩u)
defer apply(simp)
unfolding i_def cs⇩l_def cs⇩u_def using assms by auto
have i_length_cs⇩l⇩u: "i < length (cs⇩l @ cs⇩u)"
unfolding cs⇩l_def cs⇩u_def using i_length_Is by auto
have sv_sv': "sv = sv'"
proof -
have 1: "(map (Branch_and_Bound.max_var ∘ Simplex.poly ∘ snd ∘ hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u)) ! i = x"
apply(subst nth_map)
subgoal using i_length_cs⇩l⇩u by auto
using max_var_Var by (subst cs⇩l⇩u_x) (auto simp add: cs⇩l_def cs⇩u_def cs⇩l⇩u_x)
then have "(map (Branch_and_Bound.max_var ∘ Simplex.poly ∘ snd ∘ hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u))
= (map (Branch_and_Bound.max_var ∘ Simplex.poly ∘ snd ∘ hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)[i := (i, c)]))"
apply(subst map_update)
apply(subst upd_conv_take_nth_drop) subgoal using i_length_cs⇩l⇩u by auto
apply(subst id_take_nth_drop[of i ])
subgoal using i_length_cs⇩l⇩u by auto
using max_var_Var by (auto simp add: c_def cs⇩l_def cs⇩u_def)
then have "start_fresh_variable (map (hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u))
= start_fresh_variable (map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)[i := (i, c)]))"
by (auto simp add: start_fresh_variable_Max comp_def)
then show ?thesis
unfolding sv_def sv'_def ncs'' ncs by (simp add: start_fresh_variable_append)
qed
define s⇩3⇩1⇩1 where "s⇩3⇩1⇩1 = preprocess' ncs' sv'"
define s⇩2⇩1⇩1 where "s⇩2⇩1⇩1 = preprocess' ncs sv"
define oa where "oa = snd (map (hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u) ! i)"
have i_oa: "(map (hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u) ! i) = (i, oa)"
proof -
have 1: "map fst (cs⇩l @ cs⇩u) = map (λx. fst (hd (i_constraint_to_qdelta_constraint x))) (cs⇩l @ cs⇩u)"
by (auto simp add: cs⇩l_def cs⇩u_def)
have "enumerated 0 (map (hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u))"
using enumerated_cs⇩l⇩u unfolding enumerated[symmetric] 1 by (auto simp add: comp_def)
then show ?thesis
using i_length_Is unfolding oa_def by (subst enumerated_nth') (auto simp add: cs⇩l_def cs⇩u_def)
qed
then have ncs_i_oa: "ncs ! i = (i, oa)"
using i_length_Is unfolding ncs by (subst nth_append) (auto simp add: cs⇩u_def cs⇩l_def)
have oa: "is_monom (poly oa)" "poly oa ≠ 0"
proof -
have "(i, oa) ∈ set (map (hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u))"
using i_length_Is unfolding i_oa[symmetric] by (intro nth_mem) (auto simp add: cs⇩l_def cs⇩u_def)
moreover have "is_monom (poly p)" if "(j,p) ∈ set (map (hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u))" for j p
using that is_monom_Var unfolding cs⇩l_def cs⇩u_def by auto
moreover have "poly p ≠ 0" if "(j,p) ∈ set (map (hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u))" for j p
using that Var_uneq_0 unfolding cs⇩l_def cs⇩u_def by (auto)
ultimately show "is_monom (poly oa)" "poly oa ≠ 0"
by blast+
qed
have u_s⇩3⇩1⇩1: "UnsatIndices s⇩3⇩1⇩1 = UnsatIndices s⇩2⇩1⇩1"
proof -
have "UnsatIndices s⇩2⇩1⇩1 = UnsatIndices (preprocess' (filter (λ(i, nc). Simplex.poly nc = 0) ncs) sv)"
unfolding s⇩2⇩1⇩1_def apply(subst preprocess'.UnsatIndices) by auto
also have "(filter (λ(i, nc). Simplex.poly nc = 0) ncs) = (filter (λ(i, nc). Simplex.poly nc = 0) ncs')"
using is_monom_Var oa Var_uneq_0 unfolding ncs'_def
by (intro filter_list_update) (auto simp add: ncs_i_oa)
also have "sv = sv'"
using sv_sv' by simp
also have "UnsatIndices (preprocess' (filter (λ(i, nc). Simplex.poly nc = 0) ncs') sv')
= UnsatIndices s⇩3⇩1⇩1"
unfolding s⇩3⇩1⇩1_def apply(subst preprocess'.UnsatIndices[symmetric]) by auto
finally show ?thesis
by simp
qed have t_s⇩3⇩1⇩1: "Tableau s⇩3⇩1⇩1 = Tableau s⇩2⇩1⇩1"
proof -
have "Tableau s⇩2⇩1⇩1 = Tableau (preprocess' (filter (λ(i, nc). ¬ is_monom (Simplex.poly nc) ∧ Simplex.poly nc ≠ 0) ncs) sv)"
unfolding s⇩2⇩1⇩1_def apply(subst preprocess'.Tableau) by auto
also have "filter (λ(i, nc). ¬ is_monom (Simplex.poly nc) ∧ Simplex.poly nc ≠ 0) ncs
= filter (λ(i, nc). ¬ is_monom (Simplex.poly nc) ∧ Simplex.poly nc ≠ 0) ncs'"
using is_monom_Var oa Var_uneq_0 unfolding ncs'_def
by (intro filter_list_update) (auto simp add: ncs_i_oa)
also have "sv = sv'"
using sv_sv' by simp
also have "Tableau (preprocess' (filter (λa. case a of (i, nc) ⇒ ¬ is_monom (Simplex.poly nc) ∧ Simplex.poly nc ≠ 0) ncs') sv')
= Tableau s⇩3⇩1⇩1"
unfolding s⇩3⇩1⇩1_def apply(subst preprocess'.Tableau[symmetric]) by auto
finally show ?thesis
by simp
qed
obtain t⇩3⇩1⇩1 and tv⇩3⇩1⇩1 :: "(nat, QDelta) mapping ⇒ (nat, QDelta) mapping"
where "preprocess_part_2 (Atoms s⇩3⇩1⇩1) (Tableau s⇩3⇩1⇩1) = (t⇩3⇩1⇩1, tv⇩3⇩1⇩1)"
using prod_cases by fastforce
define m where "m = Poly_Mapping (preprocess' ncs sv)"
define f where
"f = (λ(i::nat, nc). (i, qdelta_constraint_to_atom nc 0)) ∘ (hd ∘ i_constraint_to_qdelta_constraint)"
have enumerated_f_cs⇩l⇩u: "enumerated 0 (map f cs⇩l @ map f cs⇩u)"
proof -
have m: "map fst (cs⇩l @ cs⇩u) = map (fst ∘ f) (cs⇩l @ cs⇩u)"
by (rule map_cong) (auto simp add: f_def cs⇩l_def cs⇩u_def)
then show ?thesis
using enumerated_cs⇩l⇩u unfolding m enumerated[symmetric] by auto
qed
define tail where
"tail = preprocess'.atoms m (map (map_prod id normalize_ns_constraint) (to_ns acs))"
have m: "m = Poly_Mapping (preprocess' ncs' sv')"
proof -
have "m = Poly_Mapping (preprocess' (filter (λ(i, nc). ¬ is_monom (Simplex.poly nc) ∧ Simplex.poly nc ≠ 0) ncs) sv)"
unfolding m_def apply(subst preprocess'.Poly_Mapping) by auto
also have "filter (λ(i, nc). ¬ is_monom (Simplex.poly nc) ∧ Simplex.poly nc ≠ 0) ncs
= filter (λ(i, nc). ¬ is_monom (Simplex.poly nc) ∧ Simplex.poly nc ≠ 0) ncs'"
using is_monom_Var oa Var_uneq_0 unfolding ncs'_def
by (intro filter_list_update) (auto simp add: ncs_i_oa)
also have "sv = sv'"
using sv_sv' by simp
also have "Poly_Mapping (preprocess' (filter (λa. case a of (i, nc) ⇒ ¬ is_monom (Simplex.poly nc) ∧ Simplex.poly nc ≠ 0) ncs') sv')
= Poly_Mapping (preprocess' ncs' sv')"
unfolding s⇩3⇩1⇩1_def apply(subst preprocess'.Poly_Mapping[symmetric]) by auto
finally show ?thesis
by simp
qed
have "Atoms s⇩2⇩1⇩1 = preprocess'.atoms m ncs"
using m_def unfolding s⇩2⇩1⇩1_def by (subst preprocess'.atoms) (auto)
also note ncs
also have "preprocess'.atoms m (map (hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u) @
map (map_prod id normalize_ns_constraint) (to_ns acs)) =
preprocess'.atoms m (map (hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u)) @ tail"
unfolding tail_def by (subst preprocess'.atoms_append) auto
also have "preprocess'.atoms m (map (hd ∘ i_constraint_to_qdelta_constraint) (cs⇩l @ cs⇩u))
= map f (cs⇩l @ cs⇩u)"
unfolding f_def using is_monom_Var
by (subst preprocess'.atoms_map) (auto simp add: comp_def cs⇩u_def cs⇩l_def)
finally have Atoms_s⇩2⇩1⇩1: "Atoms s⇩2⇩1⇩1 = map f (cs⇩l @ cs⇩u) @ tail"
unfolding tail_def f_def by blast
have "Atoms s⇩3⇩1⇩1 = preprocess'.atoms m ncs'"
using m unfolding s⇩3⇩1⇩1_def by (subst preprocess'.atoms) (auto)
also note ncs''
also have "preprocess'.atoms m (map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)[i := (i, c)])
@ map (map_prod id normalize_ns_constraint) (to_ns acs))
= preprocess'.atoms m (map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)[i := (i, c)]))
@ tail"
unfolding tail_def using preprocess'.atoms_append by auto
also have "preprocess'.atoms m (map (hd ∘ i_constraint_to_qdelta_constraint) ((cs⇩l @ cs⇩u)[i := (i, c)]))
= map f ((cs⇩l @ cs⇩u)[i := (i, c)])"
apply(subst preprocess'.atoms_map)
using set_update_subset_insert[of "(cs⇩l @ cs⇩u)" i "(i,c)"] is_monom_Var
by (auto split: if_splits simp add: f_def comp_def cs⇩l_def cs⇩u_def c_def)
finally have Atoms_s⇩3⇩1⇩1: "Atoms s⇩3⇩1⇩1 = map f ((cs⇩l @ cs⇩u)[i := (i, c)]) @ tail"
unfolding f_def by (simp add: map_update comp_def id_def)
also have 1: "set … = insert (f (i, c)) (set (map f cs⇩l @ map f cs⇩u) - {i} × UNIV ∪ set tail)"
unfolding map_update apply(simp)
apply(subst set_update_distinct)
subgoal using enumerated_f_cs⇩l⇩u by (simp add: enumerated_enumerate)
subgoal unfolding cs⇩l_def cs⇩u_def using i_length_Is by simp
apply(subst enumerated_diff[of 0])
subgoal using enumerated_f_cs⇩l⇩u by simp
subgoal unfolding cs⇩l_def cs⇩u_def using i_length_Is by simp
apply(subst Un_insert_left)
unfolding c_def by (simp)
also have "set (map f cs⇩l @ map f cs⇩u) - {i} × UNIV ∪ set tail =
(set (map f cs⇩l @ map f cs⇩u) ∪ set tail) - {i} × UNIV"
proof -
have "False" if "(i, b) ∈ set tail" for b
proof -
have "i ∈ set (map fst (map (map_prod id normalize_ns_constraint) (to_ns acs)))"
using that unfolding tail_def
by (intro preprocess'.atoms_index[of _ m]) (auto simp add: rev_image_eqI)
then have "i ∈ set (map fst acs)"
apply(auto simp add: to_ns_def)
subgoal for ba x
apply(cases ba)
by (auto simp add: rev_image_eqI)
done
then show False
using i_acs by simp
qed
then have t: "set tail = set tail - {i} × UNIV"
by (auto)
show ?thesis
by (subst t) blast
qed
also have "… = set (Atoms s⇩2⇩1⇩1) - {i} × UNIV"
unfolding Atoms_s⇩2⇩1⇩1 by auto
also have "(f (i, c)) = (i, qda)"
unfolding f_def c_def qda_def using assms is_monom_Var monom_coeff_Var max_var_Var
by (auto simp add: monom_var_def atom_to_qdatom_def)
finally have s⇩3⇩1⇩1_Atoms: "set (Atoms s⇩3⇩1⇩1) = insert ((i, qda)) (set (Atoms s⇩2⇩1⇩1) - ({i} × UNIV))"
by blast
have pp2: "preprocess_part_2 (Atoms s⇩3⇩1⇩1) (Tableau s⇩3⇩1⇩1) = preprocess_part_2 (Atoms s⇩2⇩1⇩1) (Tableau s⇩2⇩1⇩1)"
proof -
have "atom_var y = x" if "(i, y) ∈ set (Atoms s⇩2⇩1⇩1)" for y
proof -
have tail: False if "(i, y) ∈ set tail"
proof -
have "i ∈ set (map fst (preprocess'.atoms m (map (map_prod id normalize_ns_constraint) (to_ns acs))))"
using that unfolding tail_def by force
then have "i ∈ set (map fst (map (map_prod id normalize_ns_constraint) (to_ns acs)))"
by (rule preprocess'.atoms_index)
then have "i ∈ set (map fst acs)"
unfolding to_ns_def apply(auto) subgoal for ba x'
by (cases ba) (force)+
done
then show False
using i_acs by auto
qed
moreover have "atom_var y = x" if "(i, y) ∈ set (map f (cs⇩l @ cs⇩u))"
proof -
have "enumerated 0 (map f (cs⇩l @ cs⇩u))"
using enumerated_cs⇩l⇩u unfolding enumerated[symmetric] f_def
by (auto simp add: cs⇩l_def cs⇩u_def comp_def i_constraint_to_qdelta_constraint_def split: prod.splits)
then have "(i, y) = (map f (cs⇩l @ cs⇩u)) ! i"
apply(subst enumerated_nth[of 0])
using that unfolding Atoms_s⇩2⇩1⇩1 using tail by auto
also have "… = f ((cs⇩l @ cs⇩u) ! i)"
using i_length_cs⇩l⇩u by (subst nth_map) auto
also have "atom_var (snd …) = x"
unfolding cs⇩l⇩u_x f_def using monom_coeff_Var is_monom_Var monom_var_Var by(auto)
finally show ?thesis
by auto
qed
ultimately show ?thesis
using that unfolding Atoms_s⇩2⇩1⇩1 by (auto)
qed
moreover have "x ∈ atom_var ` snd ` set (Atoms s⇩2⇩1⇩1)"
unfolding Atoms_s⇩2⇩1⇩1 f_def using is_monom_Var monom_coeff_Var monom_var_Var apply(auto simp add: cs⇩l_def)
using assms(2)
by (smt UnCI atom_var.simps(2) image_iff snd_conv)
ultimately have "atom_var ` snd ` set (Atoms s⇩3⇩1⇩1) = atom_var ` snd ` set (Atoms s⇩2⇩1⇩1)"
unfolding s⇩3⇩1⇩1_Atoms qda_def
by (auto simp add: atom_to_qdatom_def assms) (metis DiffI SigmaE2 image_eqI singletonD snd_conv)
then show ?thesis
unfolding preprocess_part_2_def t_s⇩3⇩1⇩1 by simp
qed
have as⇩3⇩1: "as⇩3⇩1 = Atoms s⇩3⇩1⇩1"
using preprocess s⇩2(2) unfolding s⇩2_def inv_simps ncs'
preprocess_def unfolding ncs_def[symmetric] preprocess_part_1_def
sv_def[symmetric] sv'_def[symmetric]
Let_def s⇩2⇩1⇩1_def[symmetric] s⇩3⇩1⇩1_def[symmetric] apply(auto)
unfolding pp2[symmetric] by (auto split: prod.splits)
have "ncs⇩3 = map snd (to_ns cs')"
proof -
note cs'_to_ns
also have "map snd ((to_ns cs)[i := (i, atom_to_qdnsconstr (snd new))]) =
(map snd (to_ns cs))[fst new := atom_to_qdnsconstr (snd new)]"
apply(subst map_update) by (auto simp add: i_def assms)
also have "map snd (to_ns cs) = ncs⇩2"
using s⇩2 unfolding s⇩2_def invariant_simplex.simps inv_simps by simp
also have "ncs⇩2[fst new := atom_to_qdnsconstr (snd new)] = ncs⇩3"
using s⇩3_def unfolding s⇩3 update_iatom_in_state'_def s⇩2_def by simp
finally show ?thesis
by simp
qed
moreover have "tv⇩3 = tv⇩3⇩1"
proof -
have "tv⇩3 = tv⇩2"
using s⇩3 unfolding s⇩3_def s⇩2_def by (auto simp add: update_iatom_in_state'_def)
also have "tv⇩2 = tv⇩2⇩1"
using s⇩2 unfolding s⇩2_def inv_simps preprocess_cs by (auto)
also have "… = tv⇩3⇩1"
using preprocess_cs unfolding preprocess_def preprocess_part_1_def
unfolding ncs_def[symmetric] sv_def[symmetric]
using preprocess unfolding preprocess_def preprocess_part_1_def unfolding ncs' sv'_def[symmetric]
apply(simp) unfolding s⇩2⇩1⇩1_def[symmetric] s⇩3⇩1⇩1_def[symmetric]
apply(simp) unfolding pp2[symmetric] ‹preprocess_part_2 (Atoms s⇩3⇩1⇩1) (Tableau s⇩3⇩1⇩1) = (t⇩3⇩1⇩1, tv⇩3⇩1⇩1)›
by simp
finally show ?thesis
by simp
qed
moreover have "set ui⇩3 = set ui⇩3⇩1"
proof -
have "ui⇩3 = ui⇩2"
using s⇩3_def unfolding s⇩3 update_iatom_in_state'_def s⇩2_def by (auto)
also have "set ui⇩2 = set ui⇩2⇩1"
using s⇩2(2) unfolding s⇩2_def unfolding inv_simps preprocess_cs by (simp)
also have "ui⇩2⇩1 = UnsatIndices s⇩2⇩1⇩1"
using preprocess_cs unfolding preprocess_def ncs_def[symmetric] preprocess_part_1_def
sv_def[symmetric] Let_def s⇩2⇩1⇩1_def[symmetric] by (auto split: prod.splits)
also have "… = UnsatIndices s⇩3⇩1⇩1"
by (simp add: u_s⇩3⇩1⇩1)
also have "… = ui⇩3⇩1"
using preprocess unfolding preprocess_def ncs' preprocess_part_1_def Let_def sv'_def[symmetric]
s⇩3⇩1⇩1_def[symmetric] by (auto split: prod.splits)
finally show ?thesis
by simp
qed
moreover have "(∀i. set (list_map_to_fun as⇩3 i) = set as⇩3⇩1 ∩ {i} × UNIV)"
proof -
have "(∀i. set (list_map_to_fun as⇩2 i) = set (Atoms s⇩2⇩1⇩1) ∩ {i} × UNIV)"
using s⇩2(2) unfolding s⇩2_def inv_simps ncs'
preprocess_def unfolding ncs_def[symmetric] preprocess_part_1_def
sv_def[symmetric] sv'_def[symmetric]
Let_def s⇩2⇩1⇩1_def[symmetric] s⇩3⇩1⇩1_def[symmetric] by (auto split: prod.splits)
then show ?thesis
unfolding as⇩3 as⇩3⇩1 s⇩3⇩1⇩1_Atoms by (auto simp add: list_map_to_fun_def)
qed
moreover have "invariant_s t⇩3⇩1 (set as⇩3⇩1 ∩ set ls⇩2 × UNIV) l3s⇩3"
proof -
have "invariant_s t⇩3⇩1 (set (Atoms s⇩2⇩1⇩1) ∩ set ls⇩2 × UNIV) l3s⇩2"
using preprocess s⇩2(2) unfolding s⇩2_def inv_simps ncs'
preprocess_def unfolding ncs_def[symmetric] preprocess_part_1_def
sv_def[symmetric] sv'_def[symmetric]
Let_def s⇩2⇩1⇩1_def[symmetric] s⇩3⇩1⇩1_def[symmetric] apply(auto)
unfolding pp2[symmetric] by (auto split: prod.splits)
also have "set (Atoms s⇩2⇩1⇩1) ∩ set ls⇩2 × UNIV = set (Atoms s⇩3⇩1⇩1) ∩ set ls⇩2 × UNIV"
unfolding s⇩3⇩1⇩1_Atoms using distinct_ls by (auto simp add: ls⇩2)
also have "Atoms s⇩3⇩1⇩1 = as⇩3⇩1"
using as⇩3⇩1 by simp
also have "l3s⇩2 = l3s⇩3"
using s⇩3_def unfolding s⇩2_def s⇩3 update_iatom_in_state'_def by simp
finally show ?thesis
by simp
qed
moreover have "set ls⇩2 ∩ set ui⇩3 = {}"
proof -
have "set ui⇩3 = set ui⇩2"
using s⇩3_def unfolding s⇩3 s⇩2_def update_iatom_in_state'_def by (auto)
also have "set ls⇩2 ∩ set ui⇩2 = {}"
using s⇩2 unfolding s⇩2_def inv_simps by auto
finally show ?thesis
by simp
qed
ultimately have inv: "invariant_simplex cs' (set ls⇩2) s⇩3"
unfolding s⇩3 unfolding update_iatom_in_state'_def unfolding inv_simps preprocess by (auto)
show "state_invariant acs Is lb' ub' s'" if "bnb_update_state'' acs Is lb' ub' s new = Some s'"
proof -
have "assert_simplex (fst new) (update_iatom_in_state' s⇩2 new) = Sat s'"
using s⇩2 assms ls_cs' that unfolding bnb_update_state''_def ls⇩2_def
by (auto simp add: Let_def cs'_def elim: sum_to_option.elims)
moreover have "insert (fst new) (set ls⇩2) = set ls"
proof -
have i: "i ∈ set ls"
unfolding ls_def i_def cs_def i_bounds_to_constraints_def using assms by (auto)
have "fst new = i"
using assms unfolding i_def by auto
also have "insert i (set ls⇩2) = set ls"
unfolding ls⇩2 using i distinct_ls by (auto)
finally show ?thesis
by auto
qed
ultimately have "invariant_simplex cs' (set ls) s'"
using inv assert_simplex_ok unfolding s⇩3_def by metis
then show ?thesis
using enumerated_cs' unfolding state_invariant_def cs'_def ls_cs' by (fastforce simp add: Let_def image_Un)
qed
show "∄v. v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb' ub' @ acs))"
if "bnb_update_state'' acs Is lb' ub' s new = None"
proof -
have "∃ds. assert_simplex (fst new) (update_iatom_in_state' s⇩2 new) = Inl ds"
using s⇩2 assms that unfolding bnb_update_state''_def ls⇩2_def cs'_def ls_cs'
by (auto simp add: Let_def cs'_def elim: sum_to_option.elims)
then obtain ds where "assert_simplex (fst new) (update_iatom_in_state' s⇩2 new) = Inl ds"
by blast
moreover have "insert (fst new) (set ls⇩2) = set ls"
proof -
have i: "i ∈ set ls"
unfolding ls_def i_def cs_def i_bounds_to_constraints_def using assms by (auto)
have "fst new = i"
using assms unfolding i_def by auto
also have "insert i (set ls⇩2) = set ls"
unfolding ls⇩2 using i distinct_ls by (auto)
finally show ?thesis
by auto
qed
ultimately have "set ds ⊆ insert (fst new) (set ls⇩2) ∧ minimal_unsat_core (set ds) cs'"
using assert_simplex_unsat inv unfolding s⇩3_def by blast
then show ?thesis
unfolding minimal_unsat_core_def cs'_def by force
qed
qed
lemma i_bounds_to_constraints:
"map snd (i_bounds_to_constraints Is lb ub) = bounds_to_constraints Is (snd ∘ lb) (snd ∘ ub)"
unfolding i_bounds_to_constraints_def bounds_to_constraints_def by auto
function bnb_state_core where
"bnb_state_core cs Is lb ub s =
(if state_invariant cs Is lb ub s then
(case check_simplex s of
Unsat _ ⇒ None
| Sat s' ⇒ (let v = solution_simplex s' in
case find (λ x. v x ∉ ℤ) Is of
None ⇒ Some v
| Some x ⇒
let new_leq = (fst (ub x), Leq x (rat_of_int ⌊v x⌋));
new_geq = (fst (lb x), Geq x (rat_of_int ⌈v x⌉));
ub' = ub(x := (fst (ub x), ⌊v x⌋));
lb' = lb(x := (fst (lb x), ⌈v x⌉));
left_b = (bnb_update_state'' cs Is lb ub' s' new_leq ⤜ bnb_state_core cs Is lb ub')
in case left_b of
None ⇒ (bnb_update_state'' cs Is lb' ub s' new_geq ⤜ bnb_state_core cs Is lb' ub) |
Some v ⇒ Some v))
else None)"
by pat_completeness auto
termination
proof (relation "measure (λ(_,Is,lb,ub,_). bb_measure (Is,snd ∘ lb, snd ∘ ub))", force, goal_cases)
case (1 cs Is lb ub s s' v x new_leq new_geq ub' lb' s'')
let ?ubs = "snd ∘ ub"
let ?ubs' = "snd ∘ ub'"
let ?lbs = "snd ∘ lb"
have v: "v ⊨⇩c⇩s set (bounds_to_constraints Is ?lbs ?ubs)"
using state_invariant_simplex 1 by (auto simp add: i_bounds_to_constraints)
have x: "x ∈ set Is" and "v x ∉ ℤ"
using find_Some_set 1 by metis+
then have "v x ≤ of_int (?ubs x)"
using bounds_to_constraints_sat v by auto
then have ub'x: "⌊v x⌋ < (?ubs x)"
using floor_less[OF ‹v x ∉ ℤ›] by linarith
have "(∑i←Is. ?ubs' i - ?lbs i) = ?ubs' x - ?lbs x + (∑i←remove1 x Is. ?ubs' i - ?lbs i)"
using sum_list_map_remove1[OF x] by blast
moreover have "?ubs' x - ?lbs x < ?ubs x - ?lbs x"
unfolding `ub' = ub(x := (fst (ub x), ⌊v x⌋))` using ub'x by auto
moreover have "(∑i←remove1 x Is. ?ubs' i - ?lbs i) ≤ (∑i←remove1 x Is. ?ubs i - ?lbs i)"
by (intro sum_list_mono) (use ub'x 1 in auto)
moreover have "(∑i←Is. ?ubs i - ?lbs i) = ?ubs x - ?lbs x + (∑i←remove1 x Is. ?ubs i - ?lbs i)"
using sum_list_map_remove1[OF x] by blast
ultimately have "(∑i←Is. ?ubs' i - ?lbs i) < (∑i←Is. ?ubs i - ?lbs i)"
by linarith
thus ?case
using nonnint_sat_pos_measure'[OF v] 1 by auto
next
case (2 cs Is lb ub s s' v x new_leq new_geq ub' lb' s'')
let ?ubs = "snd ∘ ub"
let ?lbs = "snd ∘ lb"
let ?lbs' = "snd ∘ lb'"
have v: "v ⊨⇩c⇩s set (bounds_to_constraints Is ?lbs ?ubs)"
using state_invariant_simplex 2 by (auto simp add: i_bounds_to_constraints)
have x: "x ∈ set Is" and vx_Int: "v x ∉ ℤ"
using find_Some_set 2 by metis+
then have "of_int (?lbs x) ≤ v x"
using bounds_to_constraints_sat v by auto
then have lb'x: "?lbs x < ⌈v x⌉"
by (subst less_ceiling_iff) (use vx_Int Ints_of_int less_eq_rat_def in metis)
have "(∑i←Is. ?ubs i - ?lbs' i) = ?ubs x - ?lbs' x + (∑i←remove1 x Is. ?ubs i - ?lbs' i)"
using sum_list_map_remove1[OF x] by blast
moreover have "?ubs x - ?lbs' x < ?ubs x - ?lbs x"
unfolding `lb' = lb(x := (fst (lb x), ⌈v x⌉))` using lb'x by auto
moreover have "(∑i←remove1 x Is. ?ubs i - ?lbs' i) ≤ (∑i←remove1 x Is. ?ubs i - ?lbs i)"
by (intro sum_list_mono) (use lb'x 2 in auto)
moreover have "(∑i←Is. ?ubs i - ?lbs i) = ?ubs x - ?lbs x + (∑i←remove1 x Is. ?ubs i - ?lbs i)"
using sum_list_map_remove1[OF x] by blast
ultimately have "(∑i←Is. ?ubs i - ?lbs' i) < (∑i←Is. ?ubs i - ?lbs i)"
by linarith
thus ?case
using nonnint_sat_pos_measure'[OF v] 2 by auto
qed
declare bnb_state_core.simps[simp del]
lemma bnb_state_core_sat:
assumes "state_invariant cs Is lb ub s" "bnb_state_core cs Is lb ub s = Some v"
shows "v ⊨⇩m⇩c⇩s (snd ` (set cs), set Is)"
using assms proof (induction arbitrary: v rule: bnb_state_core.induct )
case (1 cs Is lb ub s)
note [simp] = bnb_state_core.simps[of cs Is lb ub s]
show ?case
proof (cases "check_simplex s")
case (Inr s')
note ni = `state_invariant cs Is lb ub s`
note s' = Inr
define r where "r = solution_simplex s'"
then have r: "r ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb ub @ cs))"
using Inr 1(3,4) by (intro state_invariant_simplex) (auto intro!: state_invariant_simplex)
have ni_s': "checked_bnc cs Is lb ub s'"
using ni s' check_simplex_ok
by (auto simp add: checked_bnc_def state_invariant_def Let_def intro!: checked_invariant_simplex)
show ?thesis
proof (cases "find (λ x. r x ∉ ℤ) Is")
case None
then have "∀x ∈ set Is. r x ∈ ℤ"
using find_None_iff by metis
then have r: "r ⊨⇩m⇩c⇩s (snd ` (set cs), set Is)"
using r by auto
also have "r = v"
using 1(3,4) Inr None unfolding r_def by (auto)
finally show ?thesis
by simp
next
case (Some x)
have x_Is: "x ∈ set Is"
by (meson Some find_Some_set)
note x = Some
define ub' where "ub' = ub(x := (fst (ub x), ⌊r x⌋))"
define new_leq where "new_leq = (fst (ub x), Leq x (rat_of_int ⌊r x⌋))"
define lb' where "lb' = lb(x := (fst (lb x), ⌈r x⌉))"
define new_geq where "new_geq = (fst (lb x), Geq x (rat_of_int ⌈r x⌉))"
note lets = ub'_def new_leq_def lb'_def new_geq_def
show ?thesis
proof (cases "bnb_update_state'' cs Is lb ub' s' new_leq")
case (Some s'')
note s'' = Some
then show ?thesis
proof (cases "bnb_state_core cs Is lb ub' s''")
case (Some v')
have "x ∈ set Is"
using x by (meson find_Some_set)
then have ni': "state_invariant cs Is lb ub' s''"
apply(intro bnb_update_state_invariant)
using Inr 1(3) ni_s' ub'_def new_leq_def s'' by (auto)
have "v' ⊨⇩m⇩c⇩s (snd ` set cs, set Is)"
apply(rule 1(1))
using 1 apply(blast)
using s' apply(blast)
using r_def apply(blast)
using x apply(blast)
prefer 5 using s'' apply(blast)
using new_leq_def apply(simp)
apply(simp)
using ub'_def apply(simp)
apply(simp)
defer
using Some ni' by (auto)
also have "v' = v"
using 1(3,4) s' x r_def s'' ub'_def new_leq_def Some by (auto)
finally show ?thesis
by simp
next
case None
note None' = None
then show ?thesis
proof (cases "bnb_update_state'' cs Is lb' ub s' new_geq")
case (None)
then show ?thesis
using 1(3,4) s' x r_def lets s'' None' by (auto)
next
case (Some s''')
note Some' = Some
then show ?thesis
proof (cases "bnb_state_core cs Is lb' ub s'''")
case (Some v')
have ni': "state_invariant cs Is lb' ub s'''"
apply(rule bnb_update_state_invariant) using Some' 1(3) ni_s' lets x_Is by (auto)
have "v' ⊨⇩m⇩c⇩s (snd ` set cs, set Is)"
apply(rule 1(2))
using 1 apply(blast)
using s' apply(blast)
using r_def apply(blast)
using x apply(blast)
prefer 7 using Some' apply(blast)
using lets apply(simp)
using lets apply(simp)
using lets apply(simp)
using lets apply(simp)
apply(simp)
using s'' lets None apply(simp)
using ni' Some ni by (auto)
also have "v' = v"
using 1(3,4) s' s'' x r_def Inr lets Some' Some None by (auto)
finally show ?thesis
by simp
next
case (None)
show ?thesis
using `bnb_state_core cs Is lb ub' s'' = None`
1(3,4) s' s'' x r_def Inr lets Some None by (auto)
qed
qed
qed
next
case (None)
note None' = None
then show ?thesis
proof (cases "bnb_update_state'' cs Is lb' ub s' new_geq")
case (None)
then show ?thesis
using 1(3,4) s' x r_def lets None' by (auto)
next
case (Some s''')
note Some' = Some
then show ?thesis
proof (cases "bnb_state_core cs Is lb' ub s'''")
case (Some v')
have ni': "state_invariant cs Is lb' ub s'''"
apply(rule bnb_update_state_invariant) using Some Some' 1(3) ni_s' lets x_Is by (auto)
have "v' ⊨⇩m⇩c⇩s (snd ` set cs, set Is)"
apply(rule 1(2))
using 1 apply(blast)
using s' apply(blast)
using r_def apply(blast)
using x apply(blast)
prefer 7 using Some' apply(blast)
using lets apply(simp)
using lets apply(simp)
using lets apply(simp)
using lets apply(simp)
apply(simp)
using None' lets apply(simp)
using ni' Some ni by (auto)
also have "v' = v"
using 1(3,4) s' None' x r_def Inr lets Some' Some by (auto)
finally show ?thesis
by simp
next
case None
show ?thesis
using None' 1(3,4) s' x r_def Inr lets Some None by (auto)
qed
qed
qed
qed
next
case (Inl ds)
then show ?thesis
using 1(3,4) by (auto)
qed
qed
lemma bnb_state_core_unsat:
assumes "state_invariant cs Is lb ub s" "bnb_state_core cs Is lb ub s = None"
"v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb ub))"
shows "¬ v ⊨⇩m⇩c⇩s (snd ` (set cs), set Is)"
using assms proof (induction rule: bnb_state_core.induct)
case (1 cs Is lb ub s)
note ni = `state_invariant cs Is lb ub s`
note bnb = `bnb_state_core cs Is lb ub s = None`
note [simp] = bnb_state_core.simps[of cs Is lb ub s]
show ?case
proof (cases "check_simplex s")
case (Inr s')
note s' = Inr
define r where "r = solution_simplex s'"
then have r: "r ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb ub @ cs))"
by (intro state_invariant_simplex) (use Inr 1(3,4) in auto)
note 1
have ni_s': "checked_bnc cs Is lb ub s'"
using ni s' check_simplex_ok
by (auto simp add: checked_bnc_def state_invariant_def Let_def intro!: checked_invariant_simplex)
show ?thesis
proof (cases "find (λ x. r x ∉ ℤ) Is")
case None
then show ?thesis
using ni s' bnb r_def by (auto)
next
case (Some x)
define ub' where "ub' = ub(x := (fst (ub x), ⌊r x⌋))"
define new_leq where "new_leq = (fst (ub x), Leq x (rat_of_int ⌊r x⌋))"
define lb' where "lb' = lb(x := (fst (lb x), ⌈r x⌉))"
define new_geq where "new_geq = (fst (lb x), Geq x (rat_of_int ⌈r x⌉))"
define bus where "bus = bnb_update_state'' cs Is lb ub' s' new_leq"
define left_b where "left_b = (bus ⤜ bnb_state_core cs Is lb ub')"
note lets = ub'_def new_leq_def lb'_def new_geq_def
have x_Is: "x ∈ set Is" and rx: "r x ∉ ℤ"
using Some find_Some_set by metis+
note x = Some
show ?thesis
proof (cases left_b)
case None
have v_ub': "¬ v ⊨⇩m⇩c⇩s (snd ` set cs, set Is)" if "v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb ub'))"
proof (cases bus)
case (None)
then have "∄v. v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb ub' @ cs))"
using ni_s' x_Is ub'_def bus_def new_leq_def by (intro bnb_update_state_Unsat) (auto)
then show ?thesis
using that by auto
next
case (Some s'')
then have "state_invariant cs Is lb ub' s''"
using ni_s' x_Is bus_def ub'_def new_leq_def
by (intro bnb_update_state_invariant) (auto)
moreover have "bnb_state_core cs Is lb ub' s'' = None"
using None Some unfolding left_b_def by (auto)
ultimately show ?thesis
apply(intro 1(1))
using that Some ni s' x r_def ub'_def bus_def new_leq_def by (auto simp add: fun_upd_def)
qed
have v_lb': "¬ v ⊨⇩m⇩c⇩s (snd ` set cs, set Is)" if "v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb' ub))"
proof (cases "bnb_update_state'' cs Is lb' ub s' new_geq")
case (None)
then have "∄v. v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb' ub @ cs))"
using ni_s' x_Is lb'_def bus_def new_geq_def by (intro bnb_update_state_Unsat) (auto)
then show ?thesis
using that by auto
next
case (Some s'')
then have "state_invariant cs Is lb' ub s''"
using ni_s' x_Is bus_def lb'_def new_geq_def
by (intro bnb_update_state_invariant) (auto)
moreover have "bnb_state_core cs Is lb' ub s'' = None"
using bnb ni s' x r_def None Some unfolding left_b_def bus_def lets
by (auto simp add: Let_def)
ultimately show ?thesis
apply(intro 1(2))
using that Some ni s' x r_def lb'_def bus_def new_geq_def None
unfolding left_b_def bus_def lets fun_upd_def by (auto)
qed
show ?thesis
proof rule
assume v: "v ⊨⇩m⇩c⇩s (snd ` set cs, set Is)"
then have vx: "v x ∈ ℤ"
using x_Is by auto
show False
proof (cases "v x ≤ r x")
case True
then have "v x ≤ rat_of_int ⌊r x⌋"
using vx int_le_floor_iff by blast
then have "∀i∈set Is. of_int (snd (lb i)) ≤ v i ∧ v i ≤ of_int (snd (ub' i))"
using 1(5) unfolding ub'_def unfolding i_bounds_to_constraints
bounds_to_constraints_sat by auto
then have "v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb ub'))"
unfolding i_bounds_to_constraints bounds_to_constraints_sat by simp
then show ?thesis
using v_ub' v by blast
next
case False
then have "rat_of_int ⌈r x⌉ ≤ v x"
using vx int_ge_ceiling_iff by fastforce
then have "∀i∈set Is. of_int (snd (lb' i)) ≤ v i ∧ v i ≤ of_int (snd (ub i))"
using 1(5) unfolding lb'_def unfolding i_bounds_to_constraints
bounds_to_constraints_sat by auto
then have "v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb' ub))"
unfolding i_bounds_to_constraints bounds_to_constraints_sat by simp
then show ?thesis
using v_lb' v by blast
qed
qed
next
case (Some a)
then show ?thesis
using bnb ni s' bnb r_def x
apply (auto simp add: left_b_def bus_def Let_def)
unfolding lets by auto
qed
qed
next
case (Inl a)
then have "∄v. v ⊨⇩c⇩s set (map snd (i_bounds_to_constraints Is lb ub @ cs))"
using ni by (intro state_invariant_simplex_Unsat) (auto)
then have "¬ v ⊨⇩c⇩s set (map snd cs)"
using 1 by auto
then show ?thesis
by simp
qed
qed
partial_function (option) bnb_state_core_p where
[code]: "bnb_state_core_p cs Is lb ub s =
(case check_simplex s of
Unsat _ ⇒ Some None
| Sat s' ⇒ (let v = solution_simplex s' in
case find (λ x. v x ∉ ℤ) Is of
None ⇒ Some (Some v)
| Some x ⇒
let new_leq = (fst (the (Mapping.lookup ub x)), Leq x (rat_of_int ⌊v x⌋));
new_geq = (fst (the (Mapping.lookup lb x)), Geq x (rat_of_int ⌈v x⌉));
ub' = Mapping.update x (fst (the (Mapping.lookup ub x)), ⌊v x⌋) ub;
lb' = Mapping.update x (fst (the (Mapping.lookup lb x)), ⌈v x⌉) lb in
(case bnb_update_state'' cs Is (the ∘ (Mapping.lookup lb)) (the ∘ (Mapping.lookup ub')) s' new_leq of
Some s'' ⇒ bnb_state_core_p cs Is lb ub' s'' |
None ⇒ Some None) ⤜
(λt. case t of
None ⇒ case bnb_update_state'' cs Is (the ∘ (Mapping.lookup lb')) (the ∘ (Mapping.lookup ub)) s' new_geq of
Some s'' ⇒ bnb_state_core_p cs Is lb' ub s'' |
None ⇒ Some None |
Some v ⇒ Some (Some v))))"
lemma bnb_state_core_p:
assumes "lb = (the ∘ (Mapping.lookup lb⇩m))" "ub = (the ∘ (Mapping.lookup ub⇩m))"
"state_invariant cs Is lb ub s"
shows "bnb_state_core_p cs Is lb⇩m ub⇩m s = Some (bnb_state_core cs Is lb ub s)"
using assms proof (induction cs Is lb ub s arbitrary: lb⇩m ub⇩m rule: bnb_state_core.induct)
case (1 cs Is lb ub s)
show ?case
proof (cases "check_simplex s")
case (Inl a)
then show ?thesis by (simp add: bnb_state_core_p.simps bnb_state_core.simps)
next
case (Inr s')
note Inr1 = Inr
define i_b where "i_b = i_bounds_to_constraints Is lb ub @ cs"
have "checked_simplex i_b (fst ` set i_b) s'"
apply(rule check_simplex_ok[of _ _ s])
using Inr1 1(5) unfolding state_invariant_def i_b_def by (metis)+
then have c_bnc: "checked_bnc cs Is lb ub s'"
using 1(5) unfolding state_invariant_def i_b_def checked_bnc_def by metis
define v where "v = solution_simplex s'"
show ?thesis
proof (cases "find (λ x. v x ∉ ℤ) Is")
case None
then show ?thesis using 1 by (simp add: v_def Inr bnb_state_core_p.simps bnb_state_core.simps)
next
case (Some x)
note Some1 = Some
have x_Is: "x ∈ set Is"
by (meson Some1 find_Some_set)
define new_leq where "new_leq = (fst (ub x), Leq x (rat_of_int ⌊v x⌋))"
define new_geq where "new_geq = (fst (lb x), Geq x (rat_of_int ⌈v x⌉))"
define ub' where "ub' = ub(x := (fst (ub x), ⌊v x⌋))"
define lb' where "lb' = lb(x := (fst (lb x), ⌈v x⌉))"
define new_leq where "new_leq = (fst (ub x), Leq x (rat_of_int ⌊v x⌋))"
define ub'⇩m where "ub'⇩m = Mapping.update x (fst (the (Mapping.lookup ub⇩m x)), ⌊v x⌋) ub⇩m"
define lb'⇩m where "lb'⇩m = Mapping.update x (fst (the (Mapping.lookup lb⇩m x)), ⌈v x⌉) lb⇩m"
define bus⇩u where "bus⇩u = bnb_update_state'' cs Is lb ub' s' new_leq"
define bus⇩l where "bus⇩l = bnb_update_state'' cs Is lb' ub s' new_geq"
define t⇩p⇩u where "t⇩p⇩u = (case bus⇩u of Some s'' ⇒ bnb_state_core_p cs Is lb⇩m ub'⇩m s'' |
None ⇒ Some None)"
define t⇩u where "t⇩u = (case bus⇩u of Some s'' ⇒ bnb_state_core cs Is lb ub' s'' |
None ⇒ None)"
have t⇩u: "t⇩p⇩u = Some t⇩u"
proof (cases bus⇩u)
case None
then show ?thesis unfolding t⇩p⇩u_def t⇩u_def by simp
next
case (Some s'')
have "state_invariant cs Is lb ub' s''"
apply(rule bnb_update_state_invariant[of _ _ _ _ _ x, where t=False])
apply(rule c_bnc)
apply (meson Some1 find_Some_set)
using new_leq_def[unfolded v_def] apply(blast)
using ub'_def v_def apply(simp)
using ub'_def v_def apply(simp)
using Some unfolding bus⇩u_def ub'_def new_leq_def 1 comp_def v_def by auto
then have "bnb_state_core_p cs Is lb⇩m ub'⇩m s'' = Some (bnb_state_core cs Is lb ub' s'')"
apply(intro 1(1))
using 1 Inr1 Some1 apply(auto simp add: v_def ub'_def)[8]
subgoal
using Some unfolding bus⇩u_def ub'_def new_leq_def 1 comp_def v_def by blast
using 1 apply(blast)
using ub'_def ub'⇩m_def 1 apply(auto)[1]
by blast
then show ?thesis using Some unfolding t⇩p⇩u_def t⇩u_def by simp
qed
have "bnb_state_core_p cs Is lb⇩m ub⇩m s =
t⇩p⇩u ⤜
(λt. case t of
None ⇒ case bus⇩l of
Some s'' ⇒ bnb_state_core_p cs Is lb'⇩m ub⇩m s'' |
None ⇒ Some None |
Some v ⇒ Some (Some v))"
using Inr1 Some1
unfolding 1 t⇩p⇩u_def bus⇩u_def bus⇩l_def ub'_def lb'_def v_def new_leq_def new_geq_def ub'⇩m_def lb'⇩m_def
by (subst bnb_state_core_p.simps) (auto simp add: 1 Let_def fun_upd_comp v_def)
then have bp: "bnb_state_core_p cs Is lb⇩m ub⇩m s = (case t⇩u of
None ⇒ case bus⇩l of
Some s'' ⇒ bnb_state_core_p cs Is lb'⇩m ub⇩m s'' |
None ⇒ Some None |
Some v ⇒ Some (Some v))"
unfolding t⇩u by simp
have b: "bnb_state_core cs Is lb ub s =
(case t⇩u of
None ⇒ case bus⇩l of
Some s'' ⇒ bnb_state_core cs Is lb' ub s'' |
None ⇒ None |
Some v ⇒ (Some v))"
using Inr1 Some1
unfolding 1 comp_def t⇩u_def bus⇩u_def bus⇩l_def ub'_def lb'_def v_def new_leq_def new_geq_def ub'⇩m_def lb'⇩m_def
using 1(5)
by (subst bnb_state_core.simps) (auto simp add: 1 Let_def v_def split: Option.bind_splits option.splits)
then show ?thesis
proof (cases t⇩u)
case None
note None' = None
then show ?thesis
proof (cases bus⇩l)
case None
then show ?thesis using None' unfolding bp b by (simp)
next
case (Some s'')
have "state_invariant cs Is lb' ub s''"
apply(rule bnb_update_state_invariant[where new = new_geq and t = True])
apply(rule c_bnc)
using x_Is apply(simp)
using new_geq_def apply(simp)
subgoal unfolding lb'_def lb'⇩m_def 1 by auto[1]
using Some unfolding bus⇩l_def lb'_def new_geq_def v_def 1 comp_def by auto
then show ?thesis using None' Some unfolding bp b apply (simp)
apply(rule 1(2)[of _ _ _ _ _ _ _ t⇩u])
using 1 Inr1 Some1 apply(auto simp add: v_def lb'_def)[8]
subgoal
unfolding t⇩u_def bus⇩u_def ub'_def new_leq_def 1 comp_def v_def by (auto split: option.splits)
apply(auto)[1]
subgoal
unfolding bus⇩l_def lb'_def new_geq_def v_def 1 comp_def by blast
subgoal unfolding lb'_def lb'⇩m_def 1 by auto[1]
subgoal unfolding 1 by simp
by simp
qed
next
case (Some a)
then show ?thesis unfolding bp b by (simp)
qed
qed
qed
qed
definition bnb_state_init where
"bnb_state_init cs Is lb ub =
(let
lb' = zip Is [0 ..<length Is];
ub' = zip Is [length Is ..<length Is + length Is];
lb' = map (λ(x,y). (x, y, lb x)) lb';
ub' = map (λ(x,y). (x, y, ub x)) ub';
lb_m = Mapping.of_alist lb';
ub_m = Mapping.of_alist ub';
cs' = zip [length Is + length Is ..< length Is + length Is + length cs] cs;
bs = i_bounds_to_constraints Is (the ∘ (Mapping.lookup lb_m)) (the ∘ (Mapping.lookup ub_m)) @ cs';
s = (assert_all_simplex (map fst bs) (init_simplex bs))
in (cs', lb_m, ub_m, s))
"
lemma bnb_state_init:
assumes "distinct Is" "bnb_state_init cs Is lb ub = (cs', lb_m, ub_m, s')" "s' = Inr s"
shows "state_invariant cs' Is (the ∘ Mapping.lookup lb_m) (the ∘ Mapping.lookup ub_m) s"
proof -
define bs where "bs = i_bounds_to_constraints Is (the ∘ Mapping.lookup lb_m) (the ∘ Mapping.lookup ub_m) @ cs'"
have ub_m: "ub_m = Mapping.of_alist (map2 (λx y. (x, y, ub x)) Is [length Is..<length Is + length Is])"
using assms unfolding bnb_state_init_def by (simp add: Let_def)
have lb_m: "lb_m = Mapping.of_alist (map2 (λx y. (x, y, lb x)) Is [0..<length Is])"
using assms unfolding bnb_state_init_def by (simp add: Let_def)
have 1: "map (λx. fst (the (map_of (map2 (λx y. (x, y, f x)) xs ys) x))) xs = ys"
if "length ys = length xs" "distinct xs" for ys::"'c list" and xs and f::"'a ⇒ 'b"
using that proof (induction xs arbitrary: ys)
case Nil
then show ?case by (simp)
next
case (Cons x xs)
then have "∃y ys'. ys = y # ys'"
by (metis length_nth_simps(2) list.exhaust list.map(1) list.map(2) list.simps(3) list.size(3) nth_Cons_0 nth_Cons_Suc zip_Nil)
then obtain y ys' where "ys = y # ys'"
by blast
then show ?case
apply(auto)
using Cons apply(auto)
by (smt map_eq_conv)
qed
have "map (λx. fst (the (Mapping.lookup (Mapping.of_alist (map2 (λx y. (x, y, lb x)) Is [0..<length Is])) x))) Is
= [0..<length Is]"
using 1[of " [0..<length Is]" "Is" lb] assms
unfolding lb_m by (simp add: lookup_of_alist)
moreover have "map (λx. fst (the (Mapping.lookup ub_m x))) Is
= [length Is..<length Is + length Is]"
using 1[of " [length Is..<length Is + length Is]" "Is" ub] assms
unfolding ub_m lookup_of_alist by simp
ultimately have "enumerated 0 bs"
unfolding bs_def enumerated[symmetric] apply(auto simp add: i_bounds_to_constraints_def lb_m comp_def)
using assms unfolding bnb_state_init_def apply(auto simp add: Let_def)
by (smt add.commute add.left_commute append_assoc upt_add_eq_append zero_le)
moreover have "invariant_simplex bs ({} ∪ set (map fst bs)) s"
apply(rule assert_all_simplex_ok)
apply(rule checked_invariant_simplex)
apply(rule init_simplex)
using assms unfolding bnb_state_init_def by (auto simp add: bs_def Let_def)
ultimately show ?thesis
unfolding state_invariant_def unfolding bs_def by (simp add: Let_def image_Un)
qed
lemma bnb_state_init':
assumes "distinct Is" "bnb_state_init cs Is lb ub = (cs', lb_m, ub_m, s')" "s' = Inl I"
shows "∄v. v ⊨⇩c⇩s set ((bounds_to_constraints Is lb ub) @ cs)"
proof -
define bs where "bs = i_bounds_to_constraints Is (the ∘ Mapping.lookup lb_m) (the ∘ Mapping.lookup ub_m) @ cs'"
have ub_m: "ub_m = Mapping.of_alist (map2 (λx y. (x, y, ub x)) Is [length Is..<length Is + length Is])"
using assms unfolding bnb_state_init_def by (simp add: Let_def)
have lb_m: "lb_m = Mapping.of_alist (map2 (λx y. (x, y, lb x)) Is [0..<length Is])"
using assms unfolding bnb_state_init_def by (simp add: Let_def)
have "map (λx. snd (the (map_of (map2 (λx y. (x, y, f x)) xs ys) x))) xs = map f xs"
if "length ys = length xs" "distinct xs" for ys::"'c list" and xs and f::"'a ⇒ 'b"
using that proof (induction xs arbitrary: ys)
case Nil
then show ?case by (simp)
next
case (Cons x xs)
then have "∃y ys'. ys = y # ys'"
by (metis length_nth_simps(2) list.exhaust list.map(1) list.map(2) list.simps(3) list.size(3) nth_Cons_0 nth_Cons_Suc zip_Nil)
then obtain y ys' where "ys = y # ys'"
by blast
then show ?case
using Cons by (auto)
qed
then have 1: "(snd (the (map_of (map2 (λx y. (x, y, f x)) xs ys) x))) = f x"
if "length ys = length xs" "distinct xs" "x ∈ set xs"for ys::"'c list" and x xs and f::"'a ⇒ 'b"
using map_eq_conv that by auto
have "set I ⊆ set (map fst bs) ∪ {} ∧ minimal_unsat_core (set I) bs"
apply(rule assert_all_simplex_unsat[of _ _ "init_simplex bs"])
apply(rule checked_invariant_simplex)
apply(rule init_simplex)
using assms bs_def by (auto simp add: Let_def bnb_state_init_def)
then have "∄v. v ⊨⇩c⇩s set (map snd bs)"
unfolding minimal_unsat_core_def by auto
also have "map snd bs = bounds_to_constraints Is (snd ∘ (the ∘ Mapping.lookup lb_m))
(snd ∘ (the ∘ Mapping.lookup ub_m)) @ map snd cs'"
unfolding bs_def by (simp add: i_bounds_to_constraints)
also have "bounds_to_constraints Is (snd ∘ (the ∘ Mapping.lookup lb_m)) (snd ∘ (the ∘ Mapping.lookup ub_m))
= bounds_to_constraints Is lb ub"
proof -
have "snd (the (Mapping.lookup lb_m x)) = lb x" if "x ∈ set Is" for x
using that `distinct Is` unfolding lb_m lookup_of_alist by (auto simp add: 1)
moreover have "snd (the (Mapping.lookup ub_m x)) = ub x" if "x ∈ set Is" for x
using that `distinct Is` unfolding ub_m lookup_of_alist by (auto simp add: 1)
ultimately show ?thesis
unfolding bounds_to_constraints_def by simp
qed
also have "map snd cs' = cs"
using assms unfolding bnb_state_init_def by (auto simp add: Let_def)
finally show ?thesis
by simp
qed
function branch_and_bound_core ::
"constraint list ⇒ var list ⇒ (var ⇒ int) ⇒ (var ⇒ int) ⇒ rat valuation option" where
"branch_and_bound_core cs Is lb ub =
(case simplex (cs @ bounds_to_constraints Is lb ub) of
Unsat _ ⇒ None
| Sat r ⇒ (let v = ⟨r⟩ in
case find (λ x. v x ∉ ℤ) Is of
None ⇒ Some v
| Some x ⇒ (let lb' = lb(x := ⌈v x⌉) in
let ub' = ub(x := ⌊v x⌋) in
let sol = branch_and_bound_core cs Is lb ub' in
if sol ≠ None then sol else branch_and_bound_core cs Is lb' ub)))"
by pat_completeness auto
termination
proof (relation "measure (λ(_,Is,lb,ub). bb_measure (Is,lb,ub))", force, goal_cases)
case (1 cs Is lb ub v vv x lb' ub')
hence sat: "simplex (cs @ bounds_to_constraints Is lb ub) = Sat v"
and x: "find (λi. ⟨v⟩ i ∉ ℤ) Is = Some x" by auto
let ?ub' = "λ i. (if i = x then ⌊⟨v⟩ x⌋ else ub i)"
from find_Some_set[OF x] have x: "x ∈ set Is" and "⟨v⟩ x ∉ ℤ" by auto
from sat simplex(3) have "⟨v⟩ ⊨⇩c⇩s set (bounds_to_constraints Is lb ub)"
by auto
hence "⟨v⟩ x ≤ of_int (ub x)" using bounds_to_constraints_sat x by blast
hence ub'x: "⌊⟨v⟩ x⌋ < ub x" using floor_less[OF ‹⟨v⟩ x ∉ ℤ›] by linarith
have "(∑i←Is. ?ub' i - lb i) = ?ub' x - lb x +
(∑i←remove1 x Is. ?ub' i - lb i)"
using sum_list_map_remove1[OF x] by blast
moreover have "?ub' x - lb x < ub x - lb x" using ub'x by auto
moreover have "(∑i←remove1 x Is. ?ub' i - lb i) ≤
(∑i←remove1 x Is. ub i - lb i)"
by(rule sum_list_mono, insert ub'x, simp)
moreover have "(∑i←Is. ub i - lb i) =
ub x - lb x + (∑i←remove1 x Is. ub i - lb i)"
using sum_list_map_remove1[OF x] by blast
ultimately have "(∑i←Is. ?ub' i - lb i) < (∑i←Is. ub i - lb i)"
by linarith
thus ?case using nonnint_sat_pos_measure 1 by auto
next
case (2 cs Is lb ub v vv x lb' ub' sol)
hence sat: "simplex (cs @ bounds_to_constraints Is lb ub) = Sat v"
and x: "find (λi. ⟨v⟩ i ∉ ℤ) Is = Some x" by auto
let ?lb' = "λ i. if i = x then ⌈⟨v⟩ x⌉ else lb i"
from find_Some_set[OF x] have x: "x ∈ set Is" and "⟨v⟩ x ∉ ℤ" by auto
from sat simplex(3) have "⟨v⟩ ⊨⇩c⇩s set (bounds_to_constraints Is lb ub)"
by auto
hence "of_int (lb x) ≤ ⟨v⟩ x" using bounds_to_constraints_sat x by blast
hence lb'x: "lb x < ⌈⟨v⟩ x⌉" using less_ceiling_iff[of "lb x" "⟨v⟩ x"]
by (metis Ints_of_int ‹⟨v⟩ x ∉ ℤ› order.not_eq_order_implies_strict)
have "(∑i←Is. ub i - ?lb' i) = ub x - ?lb' x +
(∑i←remove1 x Is. ub i - ?lb' i)"
using sum_list_map_remove1[OF x] by blast
moreover have "ub x - ?lb' x < ub x - lb x" using lb'x by auto
moreover have "(∑i←remove1 x Is. ub i - ?lb' i) ≤
(∑i←remove1 x Is. ub i - lb i)"
by(rule sum_list_mono, insert lb'x, simp)
moreover have "(∑i←Is. ub i - lb i) =
ub x - lb x + (∑i←remove1 x Is. ub i - lb i)"
using sum_list_map_remove1[OF x] by blast
ultimately have "(∑i←Is. ub i - ?lb' i) < (∑i←Is. ub i - lb i)"
by linarith
thus ?case using nonnint_sat_pos_measure 2 by auto
qed
declare branch_and_bound_core.simps[simp del]
lemma branch_and_bound_core_sat:
"branch_and_bound_core cs Is lb ub = Some v ⟹ v ⊨⇩m⇩c⇩s (set cs, set Is)"
proof (induction rule: branch_and_bound_core.induct)
case (1 cs Is lb ub)
note [simp] = branch_and_bound_core.simps[of cs Is lb ub]
show ?case
proof (cases "simplex (cs @ bounds_to_constraints Is lb ub)")
case (Inr r)
hence r: "⟨r⟩ ⊨⇩c⇩s set (cs @ bounds_to_constraints Is lb ub)"
using simplex(3) by blast
show ?thesis
proof (cases "find (λ x. ⟨r⟩ x ∉ ℤ) Is")
case None
hence "∀ i ∈ set Is. ⟨r⟩ i ∈ ℤ"
using find_None_iff[of _ Is] by simp
hence r: "⟨r⟩ ⊨⇩m⇩c⇩s (set cs, set Is)" using r by auto
have "branch_and_bound_core cs Is lb ub = Some ⟨r⟩"
by (simp add: Inr None)
hence "⟨r⟩ = v" using Inr 1(3) by auto
thus ?thesis using r by blast
next
case (Some x)
define lb' where "lb' = lb(x := ⌈⟨r⟩ x⌉)"
define ub' where "ub' = ub(x := ⌊⟨r⟩ x⌋)"
define sol where "sol = branch_and_bound_core cs Is lb ub'"
show ?thesis
proof (cases)
assume sol: "sol = None"
hence "branch_and_bound_core cs Is lb ub =
branch_and_bound_core cs Is lb' ub"
using Inr Some lb'_def ub'_def sol_def by (auto simp add: fun_upd_def)
hence "branch_and_bound_core cs Is lb' ub = Some v"
using 1(3) by presburger
thus ?thesis using sol 1(2)[OF Inr _ Some lb'_def ub'_def sol_def]
by fast
next
assume sol: "sol ≠ None"
hence "branch_and_bound_core cs Is lb ub = sol"
using Inr Some unfolding sol_def ub'_def by force
hence "sol = Some v" using 1(3) by blast
thus ?thesis
using 1(1)[OF Inr _ Some lb'_def ub'_def]
unfolding sol_def by blast
qed
qed
qed (insert 1, auto)
qed
lemma branch_and_bound_core_unsat:
"branch_and_bound_core c Is lb ub = None ⟹
∀ i ∈ set Is. of_int (lb i) ≤ v i ∧ v i ≤ of_int (ub i) ⟹
¬ (v ⊨⇩m⇩c⇩s (set c, set Is))"
proof (induction rule: branch_and_bound_core.induct)
case (1 cs Is lb ub)
note [simp] = branch_and_bound_core.simps[of cs Is lb ub]
show ?case
proof (cases "simplex (cs @ bounds_to_constraints Is lb ub)")
case Inl
from bounds_to_constraints_sat[of Is lb ub v] 1(4)
have "v ⊨⇩c⇩s set (bounds_to_constraints Is lb ub)" by blast
hence "¬ (v ⊨⇩c⇩s set cs)" using simplex(1)[OF Inl] by auto
thus ?thesis by auto
next
case (Inr r)
hence r: "⟨r⟩ ⊨⇩c⇩s set (cs @ bounds_to_constraints Is lb ub)"
using simplex(3) by blast
show ?thesis
proof (cases "find (λ x. ⟨r⟩ x ∉ ℤ) Is")
case None
have "branch_and_bound_core cs Is lb ub = Some ⟨r⟩"
by (simp add: Inr None)
thus ?thesis using 1(3) by auto
next
case (Some x)
hence x: "x ∈ set Is" and rx: "⟨r⟩ x ∉ ℤ"
using find_Some_set[of _ Is x] by (blast, blast)
define lb' where "lb' = lb (x := ⌈⟨r⟩ x⌉)"
define ub' where "ub' = ub (x := ⌊⟨r⟩ x⌋)"
define sol where "sol = branch_and_bound_core cs Is lb ub'"
show ?thesis
proof (cases, standard)
assume v: "v ⊨⇩m⇩c⇩s (set cs, set Is)"
assume sol: "sol = None"
from v have "v x ∈ ℤ" using x by simp
show False
proof cases
assume "v x ≤ ⟨r⟩ x"
hence "v x ≤ of_int ⌊⟨r⟩ x⌋"
using int_le_floor_iff[OF ‹v x ∈ ℤ›] by blast
hence "∀i∈set Is. of_int (lb i) ≤ v i ∧ v i ≤ of_int (ub' i)"
using 1(4) unfolding ub'_def by auto
thus False
using 1(1)[OF Inr _ Some lb'_def ub'_def sol[unfolded sol_def]] v
by blast
next
assume "~ (v x ≤ ⟨r⟩ x)"
hence "v x ≥ ⟨r⟩ x" by linarith
hence "v x ≥ of_int ⌈⟨r⟩ x⌉"
using int_ge_ceiling_iff[OF ‹v x ∈ ℤ›] by blast
hence bnds: "∀i∈set Is. of_int (lb' i) ≤ v i ∧ v i ≤ of_int (ub i)"
using 1(4) unfolding lb'_def by auto
from sol have "branch_and_bound_core cs Is lb ub =
branch_and_bound_core cs Is lb' ub"
using Inr Some lb'_def ub'_def sol_def by simp
hence sol_lb': "branch_and_bound_core cs Is lb' ub = None"
using 1(3) by argo
thus False
using 1(2)[OF Inr _ Some lb'_def ub'_def sol_def _ sol_lb' bnds]
sol v by blast
qed
next
assume sol: "sol ≠ None"
hence "branch_and_bound_core cs Is lb ub = sol"
using Inr Some unfolding sol_def ub'_def by force
thus ?thesis using 1(3) sol by fast
qed
qed
qed
qed
abbreviation (input) "Ltc ≡ Le_Constraint Lt_Rel"
primrec constraint_to_le_constraint where
"constraint_to_le_constraint (LEQ l x) = [Leqc l x]"
| "constraint_to_le_constraint (GEQ l x) = [Leqc (-l) (-x)]"
| "constraint_to_le_constraint (LT l x) = [Ltc l x]"
| "constraint_to_le_constraint (GT l x) = [Ltc (-l) (-x)]"
| "constraint_to_le_constraint (EQ l x) = [Leqc l x, Leqc (-l) (-x)]"
| "constraint_to_le_constraint (LEQPP l0 l1) = [Leqc (l0 - l1) 0]"
| "constraint_to_le_constraint (GEQPP l0 l1) = [Leqc (l1 - l0) 0]"
| "constraint_to_le_constraint (LTPP l0 l1) = [Ltc (l0 - l1) 0]"
| "constraint_to_le_constraint (GTPP l0 l1) = [Ltc (l1 - l0) 0]"
| "constraint_to_le_constraint (EQPP l0 l1) = [Leqc (l0 - l1) 0, Leqc (l1 - l0) 0]"
lemma constraint_to_le_constraint:
assumes "constraint_to_le_constraint c = cs"
shows "v ⊨⇩c c ⟷ (∀ c' ∈ set cs. v ⊨⇩l⇩e c')"
by (insert assms, cases c, auto simp: valuate_minus valuate_uminus)
definition var_list :: "constraint list ⇒ var list" where
"var_list cs = (let lecs = concat (map constraint_to_le_constraint cs);
polys = map lec_poly lecs in
remdups (concat (map vars_list polys)))"
lemma varlist_distinct:
shows "distinct (var_list cs)"
unfolding var_list_def by simp
definition normalize where
"normalize cs = concat (map constraint_to_le_constraint cs)"
lemma normalize_satisfies: "v ⊨⇩c⇩s set cs ⟷ (∀ c ∈ set (normalize cs). v ⊨⇩l⇩e c)"
unfolding normalize_def using constraint_to_le_constraint by auto
lemma constrtoleconstr_preserves_vars:
assumes "lec ∈ set (normalize cs)"
shows "vars (lec_poly lec) ⊆ set (var_list cs)"
using assms normalize_def set_vars_list var_list_def by auto
definition integral_linear_poly where "integral_linear_poly l = (∀ x. coeff l x ∈ ℤ)"
abbreviation "integral_constraint c ≡
(integral_linear_poly (lec_poly c) ∧ lec_const c ∈ ℤ)"
definition integral_constraints where
"integral_constraints cs = (∀ c ∈ set cs. integral_constraint c)"
primrec max_coeff :: "rat le_constraint ⇒ rat" where
"max_coeff (Le_Constraint _ l c) = Max ({¦c¦} ∪ {¦coeff l x¦ | x. x ∈ vars l})"
lemma max_coeff_const: "max_coeff (Le_Constraint r l c) ≥ ¦c¦"
using finite_vars by auto
lemma max_coeff: "max_coeff (Le_Constraint r l c) ≥ ¦coeff l x¦"
proof cases
assume "x ∈ vars l"
hence "¦coeff l x¦ ∈ {¦c¦} ∪ {¦coeff l x¦ | x. x ∈ vars l}" by blast
thus ?thesis using finite_vars by simp
next
assume "x ∉ vars l"
hence "¦coeff l x ¦ = 0" using coeff_zero by auto
also have "0 ≤ max_coeff (Le_Constraint r l c)"
using max_coeff_const[of c r l] by linarith
finally show ?thesis by blast
qed
lemma integral_max_coeff:
assumes "integral_constraint c"
shows "max_coeff c ∈ ℤ"
proof -
obtain r l x where c: "c = Le_Constraint r l x"
using le_constraint.collapse[of c] by metis
have "max_coeff c ∈ {¦x¦} ∪ {¦coeff l i¦ | i. i ∈ vars l}"
unfolding c max_coeff.simps
by (rule Max_in, insert finite_vars, simp_all)
moreover have "{¦x¦} ⊆ ℤ" using assms unfolding c by auto
moreover have "{¦coeff l i¦ | i. i ∈ vars l} ⊆ ℤ"
using assms unfolding c integral_linear_poly_def by auto
ultimately show ?thesis by blast
qed
definition max_coeff_constraints where
"max_coeff_constraints cs = Max (set (0 # map max_coeff cs))"
lemma max_coeff_constraints:
assumes "c ∈ set cs"
shows "¦lec_const c¦ ≤ max_coeff_constraints cs" (is ?thes1)
and "¦coeff (lec_poly c) x¦ ≤ max_coeff_constraints cs" (is ?thes2)
proof -
have "¦lec_const c¦ ≤ max_coeff c"
using max_coeff_const le_constraint.collapse by metis
moreover have "max_coeff c ≤ max_coeff_constraints cs"
unfolding max_coeff_constraints_def using assms by auto
ultimately show ?thes1 by linarith
have "¦coeff (lec_poly c) x¦ ≤ max_coeff c"
using max_coeff le_constraint.collapse by metis
moreover have "max_coeff c ≤ max_coeff_constraints cs"
unfolding max_coeff_constraints_def using assms by auto
ultimately show ?thes2 by linarith
qed
lemma max_coeff_constraints_0: "0 ≤ max_coeff_constraints cs"
unfolding max_coeff_constraints_def by auto
primrec lec_coeffs :: "rat le_constraint ⇒ rat set" where
"lec_coeffs (Le_Constraint _ l c) = {c} ∪ {coeff l x | x. x ∈ vars l}"
lemma lecconst_in_leccoeffs:
shows "lec_const lec ∈ lec_coeffs lec"
unfolding lec_coeffs_def lec_const_def
by (smt Set.insert_def insertI1 le_constraint.exhaust le_constraint.rec
le_constraint.sel(3) lec_const_def singleton_conv)
lemma equal_leccoeffs_impl_equal_maxcoeff:
assumes "lec_coeffs lec1 = lec_coeffs lec2"
shows "max_coeff lec1 = max_coeff lec2" and
"max_coeff_constraints [lec1] = max_coeff_constraints [lec2]"
proof -
let ?fct = "rec_le_constraint (λ_ l c. {¦c¦} ∪ {¦coeff l x¦ |x. x ∈ vars l})"
have "⋀lec. rec_le_constraint (λ_ l c. {¦c¦}) lec = {¦lec_const lec¦}"
by (metis le_constraint.exhaust_sel le_constraint.rec)
moreover have "⋀lec. rec_le_constraint (λ_ l c. {¦coeff l x¦ |x. x ∈ vars l}) lec =
{¦ coeff (lec_poly lec) x ¦ |x. x ∈ vars (lec_poly lec)}"
proof -
fix lec :: "'a le_constraint"
obtain ll :: "'a le_constraint ⇒ le_rel" and lla :: "'a le_constraint ⇒ linear_poly"
and aa :: "'a le_constraint ⇒ 'a" where
f1: "⋀l. Le_Constraint (ll l) (lla l) (aa l) = l"
by (metis (no_types) le_constraint.exhaust)
then have f2: "⋀l. lec_poly l = lla l" by (metis le_constraint.sel(2))
have "⋀f l. f (ll l) (lla l) (aa l) = (rec_le_constraint f l::rat set)"
using f1 by (metis le_constraint.rec)
then show
"rec_le_constraint (λl la a. {¦Abstract_Linear_Poly.coeff la n¦ |n. n ∈ vars la}) lec
= {¦Abstract_Linear_Poly.coeff (lec_poly lec) n¦ |n. n ∈ vars (lec_poly lec)}"
using f2 by presburger
qed
ultimately have "⋀lec. ?fct lec = {¦lec_const lec¦} ∪
{¦ coeff (lec_poly lec) x ¦ |x. x ∈ vars (lec_poly lec)}"
by (smt insertE le_constraint.collapse le_constraint.rec mem_Collect_eq)
moreover have "⋀lec. abs ` ({lec_const lec } ∪
{ coeff (lec_poly lec) x |x. x ∈ vars (lec_poly lec)}) = {¦lec_const lec¦} ∪
{¦ coeff (lec_poly lec) x ¦ |x. x ∈ vars (lec_poly lec)}" by auto
moreover have "{lec_const lec1 } ∪ { coeff (lec_poly lec1) x |x. x ∈ vars (lec_poly lec1)}
= {lec_const lec2 } ∪ { coeff (lec_poly lec2) x |x. x ∈ vars (lec_poly lec2)}"
proof -
have "∃l la. lec_coeffs (Le_Constraint la (lec_poly lec1) (lec_const lec1)) =
lec_coeffs (Le_Constraint l (lec_poly lec2) (lec_const lec2))"
by (metis assms le_constraint.exhaust le_constraint.sel(2) le_constraint.sel(3))
then show ?thesis by simp
qed
ultimately have "?fct lec1 = ?fct lec2" by metis
hence 1: "rec_le_constraint (λ_ l c. Max({¦c¦} ∪
{¦Abstract_Linear_Poly.coeff l x¦ |x. x ∈ vars l})) lec1 =
rec_le_constraint (λ_ l c. Max({¦c¦} ∪
{¦Abstract_Linear_Poly.coeff l x¦ |x. x ∈ vars l})) lec2"
by (metis (no_types, lifting) le_constraint.collapse le_constraint.rec)
thus "max_coeff_constraints [lec1] = max_coeff_constraints [lec2]"
unfolding max_coeff_constraints_def max_coeff_def by simp
thus "max_coeff lec1 = max_coeff lec2" unfolding max_coeff_def using 1 by simp
qed
lemma equal_mapleccoeffs_impl_equal_maxcoeff:
assumes "map lec_coeffs lecs1 = map lec_coeffs lecs2"
shows "map max_coeff lecs1 = map max_coeff lecs2" and
"max_coeff_constraints lecs1 = max_coeff_constraints lecs2"
proof -
have "⋀i. max_coeff (lecs1 ! i) = max_coeff (lecs2 ! i)"
proof(goal_cases)
case (1 i)
then show ?case using assms equal_leccoeffs_impl_equal_maxcoeff
length_map map_nth_conv by (metis (no_types, lifting) undef_vec)
qed
hence "⋀i. (map max_coeff lecs1) ! i = (map max_coeff lecs2) ! i"
by (metis assms length_map nth_map undef_vec)
thus "map max_coeff lecs1 = map max_coeff lecs2"
by (metis assms length_map nth_equalityI)
thus "max_coeff_constraints lecs1 = max_coeff_constraints lecs2"
unfolding max_coeff_constraints_def by simp
qed
definition constraints_to_pairs ::
"rat le_constraint list ⇒ (linear_poly × rat) list × (linear_poly × rat) list"
where "constraints_to_pairs cs =
(let leq_cs = filter (λ c. lec_rel c = Leq_Rel) cs in
let lt_cs = filter (λ c. lec_rel c = Lt_Rel) cs in
(map (λ c. (lec_poly c, lec_const c)) leq_cs,
map (λ c. (lec_poly c, lec_const c)) lt_cs))"
lemma constraints_to_pairs:
assumes "constraints_to_pairs cs = (leq_pairs, lt_pairs)"
shows "(∀ c ∈ set cs. v ⊨⇩l⇩e c) ⟷ ((∀ (l, x) ∈ set leq_pairs. (l ⦃ v ⦄) ≤ x) ∧
(∀ (l, x) ∈ set lt_pairs. (l ⦃ v ⦄) < x))"
(is "?L ⟷ ?R")
and "integral_constraints cs ⟹
(l, x) ∈ set leq_pairs ∪ set lt_pairs ⟹ integral_linear_poly l ∧ x ∈ ℤ"
(is "?INT0 ⟹ ?LX ⟹ ?INT1")
and "(l, x) ∈ set leq_pairs ∪ set lt_pairs ⟹
¦coeff l i¦ ≤ max_coeff_constraints cs ∧ ¦x¦ ≤ max_coeff_constraints cs"
(is "?LX' ⟹ ?BND")
proof -
define leq_cs where "leq_cs = filter (λ c. lec_rel c = Leq_Rel) cs"
define lt_cs where "lt_cs = filter (λ c. lec_rel c = Lt_Rel) cs"
have "constraints_to_pairs cs = (map (λ c. (lec_poly c, lec_const c)) leq_cs,
map (λ c. (lec_poly c, lec_const c)) lt_cs)"
unfolding constraints_to_pairs_def leq_cs_def lt_cs_def
by metis
hence leq_pairs: "leq_pairs = map (λ c. (lec_poly c, lec_const c)) leq_cs"
and lt_pairs: "lt_pairs = map (λ c. (lec_poly c, lec_const c)) lt_cs"
using assms by auto
have constructor: "⋀ c. c = Leq_Rel ∨ c = Lt_Rel"
proof -
fix c show "c = Leq_Rel ∨ c = Lt_Rel" by (cases c, simp_all)
qed
have "∀ c ∈ set leq_cs. lec_rel c = Leq_Rel" unfolding leq_cs_def by fastforce
hence leq_decomp: "∀ c ∈ set leq_cs. c = Le_Constraint Leq_Rel (lec_poly c) (lec_const c)"
using leq_cs_def le_constraint.collapse by metis
have "∀ c ∈ set lt_cs. lec_rel c = Lt_Rel" unfolding lt_cs_def by fastforce
hence lt_decomp: "∀ c ∈ set lt_cs. c = Le_Constraint Lt_Rel (lec_poly c) (lec_const c)"
using leq_cs_def le_constraint.collapse by metis
have sets: "set cs = set leq_cs ∪ set lt_cs"
unfolding leq_cs_def lt_cs_def using constructor by auto
have "(∀ c ∈ set cs. v ⊨⇩l⇩e c) ⟷
(∀ c ∈ set leq_cs. v ⊨⇩l⇩e c) ∧ (∀ c ∈ set lt_cs. v ⊨⇩l⇩e c)"
unfolding leq_cs_def lt_cs_def using constructor by auto
also have "(∀ c ∈ set leq_cs. v ⊨⇩l⇩e c) ⟷
(∀ c ∈ set leq_cs. ((lec_poly c) ⦃ v ⦄) ≤ (lec_const c))"
using leq_decomp satisfiable_le_constraint.simps[of v] rel_of.simps(1) by metis
also have "(∀ c ∈ set lt_cs. v ⊨⇩l⇩e c) ⟷
(∀ c ∈ set lt_cs. ((lec_poly c) ⦃ v ⦄) < (lec_const c))"
using lt_decomp satisfiable_le_constraint.simps[of v] rel_of.simps(2) by metis
finally show "?L ⟷ ?R" unfolding leq_pairs lt_pairs by auto
show "?INT0 ⟹ ?LX ⟹ ?INT1"
unfolding integral_constraints_def leq_pairs lt_pairs sets
by auto
assume "?LX'"
then obtain c where c: "c ∈ set cs"
and l: "l = lec_poly c" and x: "x = lec_const c"
unfolding leq_pairs lt_pairs sets by auto
show ?BND
unfolding l x using max_coeff_constraints[OF c]
by blast
qed
lift_definition vec_of_poly :: "linear_poly ⇒ nat ⇒ rat vec" is
"λ l n. vec n l"
.
lemma vec_of_poly_dim[simp]: "vec_of_poly v n ∈ carrier_vec n"
by (transfer, auto)
lemma inverse_vec_of_poly:
assumes "n > max_var l"
shows "poly_of_vec (vec_of_poly l n) = l"
proof -
have "∀ i ≥ n. i ∉ vars l" using assms max_var_max by fastforce
thus ?thesis by (transfer, force)
qed
lemma dot_vec_of_poly:
assumes v: "v ∈ carrier_vec n"
assumes l: "n > Abstract_Linear_Poly.max_var l"
shows "(vec_of_poly l n) ∙ v = (l ⦃ val_of_vec v ⦄)"
using valuate_poly_of_vec[OF v, of "vec_of_poly l n"]
inverse_vec_of_poly[OF l] by simp
lemma integral_vec_of_poly:
"integral_linear_poly l ⟹ vec_of_poly l n ∈ ℤ⇩v"
unfolding integral_linear_poly_def
by (transfer, auto simp: Ints_vec_def)
lemma vec_of_poly_bound:
"∀ x. ¦coeff l x¦ ≤ Bnd ⟹ vec_of_poly l n ∈ Bounded_vec Bnd"
by (transfer, auto simp: Bounded_vec_def)
abbreviation "lec_max_var ≡ max_var ∘ lec_poly"
definition constraints_max_var :: "rat le_constraint list ⇒ nat" where
"constraints_max_var cs = Max (set (0 # map lec_max_var cs))"
lemma constraints_max_var_to_pairs:
assumes "constraints_to_pairs cs = (leq_pairs, lt_pairs)"
assumes "(l, x) ∈ set leq_pairs ∪ set lt_pairs"
shows "max_var l ≤ constraints_max_var cs"
proof -
define leq_cs where "leq_cs = filter (λ c. lec_rel c = Leq_Rel) cs"
define lt_cs where "lt_cs = filter (λ c. lec_rel c = Lt_Rel) cs"
have "constraints_to_pairs cs = (map (λ c. (lec_poly c, lec_const c)) leq_cs,
map (λ c. (lec_poly c, lec_const c)) lt_cs)"
unfolding constraints_to_pairs_def leq_cs_def lt_cs_def
by metis
hence leq_pairs: "leq_pairs = map (λ c. (lec_poly c, lec_const c)) leq_cs"
and lt_pairs: "lt_pairs = map (λ c. (lec_poly c, lec_const c)) lt_cs"
using assms(1) by auto
then obtain c where "c ∈ set cs" and "l = lec_poly c"
using assms(2) unfolding leq_pairs lt_pairs leq_cs_def lt_cs_def by force
moreover have "constraints_max_var cs = Max (set (0 # map lec_max_var cs))"
unfolding constraints_max_var_def by presburger
ultimately show ?thesis by simp
qed
definition mats_vecs_of_constraints ::
"rat le_constraint list ⇒ rat mat × rat vec × rat mat × rat vec" where
"mats_vecs_of_constraints cs = (
let n = 1 + constraints_max_var cs in
let (leq_pairs, lt_pairs) = constraints_to_pairs cs in
let leq_polys = map fst leq_pairs in
let leq_rows = map (λ l. vec_of_poly l n) leq_polys in
let leq_bounds = map snd leq_pairs in
let lt_polys = map fst lt_pairs in
let lt_rows = map (λ l. vec_of_poly l n) lt_polys in
let lt_bounds = map snd lt_pairs in
(mat_of_rows n leq_rows, vec_of_list leq_bounds,
mat_of_rows n lt_rows, vec_of_list lt_bounds))"
lemma satisfies_le_constraint_depend:
assumes "n > lec_max_var c"
and "∀ x < n. v0 x = v1 x"
shows "v0 ⊨⇩l⇩e c ⟷ v1 ⊨⇩l⇩e c"
proof -
from assms have "∀ x ∈ vars (lec_poly c). v0 x = v1 x"
using max_var_max[of _ "lec_poly c"] by force
hence "((lec_poly c) ⦃ v0 ⦄) = ((lec_poly c) ⦃ v1 ⦄)"
using valuate_depend by blast
thus ?thesis
using satisfiable_le_constraint.simps le_constraint.collapse by metis
qed
lemma satisfies_constraints_depend:
assumes "n > constraints_max_var cs"
and "∀ x < n. v0 x = v1 x"
shows "(∀ c ∈ set cs. v0 ⊨⇩l⇩e c) ⟷ (∀ c ∈ set cs. v1 ⊨⇩l⇩e c)"
proof -
have "constraints_max_var cs = Max (set (0 # map lec_max_var cs))"
unfolding constraints_max_var_def by presburger
hence "⋀ c. c ∈ set cs ⟹ lec_max_var c < n" using assms(1) by fastforce
thus ?thesis using satisfies_le_constraint_depend[OF _ assms(2)] by blast
qed
lemma mats_vecs_of_constraints:
assumes "mats_vecs_of_constraints cs = (A, b, A', b')"
and n: "n = 1 + constraints_max_var cs"
shows "∃ nr nr'. A ∈ carrier_mat nr n ∧
b ∈ carrier_vec nr ∧
A' ∈ carrier_mat nr' n ∧
b' ∈ carrier_vec nr'" (is ?DIM)
and "(∀ c ∈ set cs. v ⊨⇩l⇩e c) ⟷ (A *⇩v (vec n v) ≤ b ∧ A' *⇩v (vec n v) <⇩v b')"
(is "?L ⟷ ?R")
and "integral_constraints cs ⟹ A ∈ ℤ⇩m ∧ b ∈ ℤ⇩v ∧ A' ∈ ℤ⇩m ∧ b' ∈ ℤ⇩v"
(is "?INT0 ⟹ ?INT1")
and "A ∈ Bounded_mat (max_coeff_constraints cs) ∧
b ∈ Bounded_vec (max_coeff_constraints cs) ∧
A' ∈ Bounded_mat (max_coeff_constraints cs) ∧
b' ∈ Bounded_vec (max_coeff_constraints cs)" (is ?BNDS)
proof -
obtain leq_pairs lt_pairs leq_polys lt_polys
leq_rows leq_bounds lt_rows lt_bounds
where
pairs: "constraints_to_pairs cs = (leq_pairs, lt_pairs)" and
leq_polys: "leq_polys = map fst leq_pairs" and
leq_rows: "leq_rows = map (λ l. vec_of_poly l n) leq_polys" and
leq_bounds: "leq_bounds = map snd leq_pairs" and
lt_polys: "lt_polys = map fst lt_pairs" and
lt_rows: "lt_rows = map (λ l. vec_of_poly l n) lt_polys" and
lt_bounds: "lt_bounds = map snd lt_pairs" and
res: "mats_vecs_of_constraints cs = (mat_of_rows n leq_rows,
vec_of_list leq_bounds,
mat_of_rows n lt_rows,
vec_of_list lt_bounds)"
unfolding mats_vecs_of_constraints_def
apply(cases "constraints_to_pairs cs")
apply(simp add: n del: vec_of_list_map)
done
from res assms(1) have A: "A = mat_of_rows n leq_rows" and
b: "b = vec_of_list leq_bounds" and
A': "A' = mat_of_rows n lt_rows" and
b': "b' = vec_of_list lt_bounds" by auto
have A_carrier: "A ∈ carrier_mat (length leq_pairs) n" and
b_carrier: "b ∈ carrier_vec (length leq_pairs)"
using A b leq_rows leq_polys leq_bounds by (fastforce, fastforce)
have A'_carrier: "A' ∈ carrier_mat (length lt_pairs) n" and
b'_carrier: "b' ∈ carrier_vec (length lt_pairs)"
using A' b' lt_rows lt_polys lt_bounds by (fastforce, fastforce)
show ?DIM using A_carrier b_carrier A'_carrier b'_carrier by blast
show "?L ⟷ ?R" proof(standard)
assume v: ?L
have "A *⇩v (vec n v) ≤ b"
proof (rule lesseq_vecI[OF _ b_carrier], insert A_carrier, simp)
fix i
assume i: "i < length leq_pairs"
hence i': "i < dim_row A" using A leq_rows leq_polys by fastforce
have pairs_i: "(leq_polys ! i, leq_bounds ! i) ∈ set leq_pairs"
using i leq_polys leq_bounds by fastforce
have max_var: "max_var (leq_polys ! i) < n" using n leq_polys
using constraints_max_var_to_pairs[OF pairs, of "leq_polys ! i" "leq_bounds ! i"]
pairs_i by force
from v have "(∀ (l, x) ∈ set leq_pairs. (l ⦃ v ⦄) ≤ x)"
using constraints_to_pairs(1)[OF pairs] by blast
hence "(leq_polys ! i) ⦃ v ⦄ ≤ leq_bounds ! i"
using i leq_polys leq_bounds by auto
also have "valuate (leq_polys ! i) v =
valuate (leq_polys ! i) (val_of_vec (vec n v))"
unfolding val_of_vec_def
apply(rule valuate_depend)
apply(insert max_var max_var_max, force)
done
also have "… = vec_of_poly (leq_polys ! i) n ∙ (vec n v)"
using dot_vec_of_poly[of "vec n v" n, OF _ max_var] by fastforce
also have "vec_of_poly (leq_polys ! i) n = row A i"
unfolding A leq_rows leq_polys
using i length_map[of fst leq_pairs] by fastforce
also have "row A i ∙ vec n v = (A *⇩v (vec n v)) $ i"
using index_mult_mat_vec[OF i'] by presburger
also have "leq_bounds ! i = b $ i" unfolding b using i leq_bounds by fastforce
finally show "(A *⇩v (vec n v)) $ i ≤ b $ i" by blast
qed
moreover
have "A' *⇩v (vec n v) <⇩v b'"
proof (rule less_vecI[OF _ b'_carrier], insert A'_carrier, simp)
fix i
assume i: "i < length lt_pairs"
hence i': "i < dim_row A'" using A' lt_rows lt_polys by force
have pairs_i: "(lt_polys ! i, lt_bounds ! i) ∈ set lt_pairs"
using i lt_polys lt_bounds by fastforce
have max_var: "max_var (lt_polys ! i) < n" using n leq_polys
using constraints_max_var_to_pairs[OF pairs] pairs_i by fastforce
from v have "(∀ (l, x) ∈ set lt_pairs. (l ⦃ v ⦄) < x)"
using constraints_to_pairs(1)[OF pairs] by algebra
hence "(lt_polys ! i) ⦃ v ⦄ < lt_bounds ! i"
using i lt_polys lt_bounds by auto
also have "valuate (lt_polys ! i) v =
valuate (lt_polys ! i) (val_of_vec (vec n v))"
unfolding val_of_vec_def
apply(rule valuate_depend)
apply(insert max_var max_var_max, force)
done
also have "… = vec_of_poly (lt_polys ! i) n ∙ (vec n v)"
using dot_vec_of_poly[of "vec n v" n, OF _ max_var] by fastforce
also have "vec_of_poly (lt_polys ! i) n = row A' i"
unfolding A' lt_rows lt_polys
using i length_map[of fst lt_pairs] by fastforce
also have "row A' i ∙ vec n v = (A' *⇩v (vec n v)) $ i"
using index_mult_mat_vec[OF i'] by presburger
also have "lt_bounds ! i = b' $ i" unfolding b' using i lt_bounds by fastforce
finally show "(A' *⇩v (vec n v)) $ i < b' $ i" by blast
qed
ultimately show ?R by fastforce
next
assume R: ?R
define x where "x = vec n v"
have xn: "x ∈ carrier_vec n" and x0: "A *⇩v x ≤ b" and x1: "A' *⇩v x <⇩v b'"
using R unfolding x_def by auto
{
fix l t
assume lt0: "(l, t) ∈ set leq_pairs"
then obtain i where i: "i < length leq_pairs" and lt: "(l, t) = leq_pairs ! i"
by (metis in_set_conv_nth)
have max_var: "max_var l < n"
using constraints_max_var_to_pairs[OF pairs, of l t] n lt0 by fastforce
have "(A *⇩v x) $ i ≤ b $ i" by (rule lesseq_vecD[OF b_carrier x0 i])
also have "(A *⇩v x) $ i = row A i ∙ x"
by (rule index_mult_mat_vec, simp add: i A leq_rows leq_polys)
also have "row A i = vec_of_poly l n"
unfolding A leq_rows leq_polys
using i length_map[of fst leq_pairs] lt fst_conv[of l t] by simp
also have "vec_of_poly l n ∙ x = (l ⦃ val_of_vec x ⦄)"
by (rule dot_vec_of_poly[OF xn max_var])
also have "b $ i = t" unfolding b leq_bounds using i lt
using snd_conv[of l t] vec_of_list_index by simp
finally have "(l ⦃ val_of_vec x ⦄) ≤ t" by blast
} moreover {
fix l t
assume lt0: "(l, t) ∈ set lt_pairs"
then obtain i where i: "i < length lt_pairs" and lt: "(l, t) = lt_pairs ! i"
by (metis in_set_conv_nth)
have max_var: "max_var l < n"
using constraints_max_var_to_pairs[OF pairs, of l t] n lt0 by fastforce
have "(A' *⇩v x) $ i < b' $ i"
by (rule less_vecD[OF x1 b'_carrier i])
also have "(A' *⇩v x) $ i = row A' i ∙ x"
by (rule index_mult_mat_vec, simp add: i A' lt_rows lt_polys)
also have "row A' i = vec_of_poly l n"
unfolding A' lt_rows lt_polys
using i length_map[of fst lt_pairs] lt fst_conv[of l t] by simp
also have "vec_of_poly l n ∙ x = (l ⦃ val_of_vec x ⦄)"
by (rule dot_vec_of_poly[OF xn max_var])
also have "b' $ i = t" unfolding b' lt_bounds using i lt
using snd_conv[of l t] vec_of_list_index by simp
finally have "(l ⦃ val_of_vec x ⦄) < t" by blast
}
ultimately have
"(∀(l, t)∈set leq_pairs. (l ⦃ val_of_vec x ⦄) ≤ t) ∧
(∀(l, t)∈set lt_pairs. (l ⦃ val_of_vec x ⦄) < t)" by blast
hence "∀ c ∈ set cs. val_of_vec x ⊨⇩l⇩e c"
using constraints_to_pairs(1)[OF pairs] by presburger
thus ?L using satisfies_constraints_depend[of cs n v "val_of_vec x"] n
unfolding x_def val_of_vec_def by fastforce
qed
have leq_rows_carrier: "set leq_rows ⊆ carrier_vec n" unfolding leq_rows by auto
have lt_rows_carrier: "set lt_rows ⊆ carrier_vec n" unfolding lt_rows by auto
let ?Bnd = "max_coeff_constraints cs"
from constraints_to_pairs(3)[OF pairs]
have polys: "∀ l ∈ set leq_polys ∪ set lt_polys. ∀ i. ¦coeff l i¦ ≤ ?Bnd"
and bounds: "∀ c ∈ set leq_bounds ∪ set lt_bounds. ¦c¦ ≤ ?Bnd"
unfolding leq_polys lt_polys leq_bounds lt_bounds by (force, force)
from polys have "set leq_rows ∪ set lt_rows ⊆ Bounded_vec ?Bnd"
unfolding leq_rows lt_rows
using vec_of_poly_bound[of _ _ n] by auto
hence "A ∈ Bounded_mat ?Bnd ∧ A' ∈ Bounded_mat ?Bnd"
using Bounded_vec_rows_Bounded_mat[of _ ?Bnd]
rows_mat_of_rows[OF leq_rows_carrier]
rows_mat_of_rows[OF lt_rows_carrier]
unfolding A A' by fastforce
moreover have "b ∈ Bounded_vec ?Bnd ∧ b' ∈ Bounded_vec ?Bnd"
by(auto simp: b b' Bounded_vec_def bounds)
ultimately show ?BNDS by blast
assume int0: ?INT0
from constraints_to_pairs(2)[OF pairs int0]
have polys: "∀ l ∈ set leq_polys ∪ set lt_polys. integral_linear_poly l"
and bounds: "set leq_bounds ∪ set lt_bounds ⊆ ℤ"
unfolding leq_polys lt_polys leq_bounds lt_bounds
by (force, force)
from polys have "set leq_rows ∪ set lt_rows ⊆ ℤ⇩v"
unfolding leq_rows lt_rows using integral_vec_of_poly[of _ n] by auto
hence "A ∈ ℤ⇩m ∧ A' ∈ ℤ⇩m" unfolding A A'
using Ints_vec_rows_Ints_mat rows_mat_of_rows[OF leq_rows_carrier]
rows_mat_of_rows[OF lt_rows_carrier] by fastforce
moreover have "b ∈ ℤ⇩v ∧ b' ∈ ℤ⇩v" unfolding b b' Ints_vec_def
using bounds by fastforce
ultimately show ?INT1 by blast
qed
primrec mul_constraint where
"mul_constraint x (Le_Constraint r l c) = Le_Constraint r (x *R l) (x * c)"
lemma mul_constraint:
assumes "x > 0"
shows "v ⊨⇩l⇩e c ⟷ v ⊨⇩l⇩e mul_constraint x c"
proof -
from le_constraint.collapse[of c] obtain r l y where
decomp: "c = Le_Constraint r l y"
by metis
have "(l ⦃ v ⦄) < y ⟷ ((x *R l) ⦃ v ⦄) < x * y"
using mult_less_cancel_left_pos[OF assms] valuate_scaleRat[of x l v]
by force
moreover have "(l ⦃ v ⦄) ≤ y ⟷ ((x *R l) ⦃ v ⦄) ≤ x * y"
using mult_le_cancel_left_pos[OF assms] valuate_scaleRat[of x l v]
by force
ultimately show ?thesis unfolding decomp
by (cases r, simp_all)
qed
primrec common_denominator where
"common_denominator (Le_Constraint _ l c) =
(let coeffs_list = map (coeff l) (vars_list l) in
let denominators = map (snd ∘ quotient_of) (c # coeffs_list) in
lcm_list denominators)"
lemma mult_denom_int:
assumes "quotient_of x = (n, d)"
and "d dvd d'"
shows "of_int d' * x ∈ ℤ"
proof -
from assms(2) obtain k where d': "d' = k * d" unfolding dvd_def by fastforce
have "d ≠ 0" using assms quotient_of_nonzero(2)[of x] by auto
hence "of_int n = of_int d * x" using quotient_of_div[OF assms(1)] by simp
hence "of_int d * x ∈ ℤ" using Ints_of_int by metis
hence "of_int k * (of_int d * x) ∈ ℤ" by simp
hence "(of_int k * of_int d) * x ∈ ℤ" using mult.assoc by metis
thus ?thesis unfolding d' by simp
qed
lemma common_denominator:
shows "common_denominator c > 0" (is ?pos)
and "of_int (common_denominator c) * lec_const c ∈ ℤ" (is ?const)
and "of_int (common_denominator c) * (coeff (lec_poly c) i) ∈ ℤ"
(is ?coeff)
proof -
from le_constraint.collapse[of c] obtain r l x where
decomp: "c = Le_Constraint r l x"
by metis
define coeffs_list where "coeffs_list = map (coeff l) (vars_list l)"
define denominators where "denominators = map (snd ∘ quotient_of) (x # coeffs_list)"
have res: "common_denominator c = lcm_list denominators"
unfolding decomp denominators_def coeffs_list_def common_denominator.simps
by presburger
have "0 ∉ set denominators"
unfolding denominators_def using quotient_of_nonzero(2) by fastforce
thus ?pos using res list_lcm_pos(3) by presburger
have "snd (quotient_of x) dvd common_denominator c"
using list_lcm unfolding res denominators_def by auto
thus ?const
using mult_denom_int[OF surjective_pairing]
unfolding decomp le_constraint.sel(3) by blast
show ?coeff
proof cases
assume "i ∈ vars l"
hence "coeff l i ∈ set coeffs_list"
unfolding coeffs_list_def using set_vars_list by auto
hence "snd (quotient_of (coeff l i)) dvd common_denominator c"
using list_lcm unfolding res denominators_def by auto
thus ?coeff
using mult_denom_int[OF surjective_pairing]
unfolding decomp le_constraint.sel(2) by blast
next
assume "i ∉ vars l"
hence "coeff l i = 0" using coeff_zero by fast
thus ?coeff unfolding decomp le_constraint.sel(2) by auto
qed
qed
definition
"constraint_to_ints c = mul_constraint (rat_of_int (common_denominator c)) c"
lemma constraint_to_ints: fixes c :: "rat le_constraint"
shows "v ⊨⇩l⇩e c ⟷ v ⊨⇩l⇩e constraint_to_ints c" (is ?R0)
and "integral_constraint (constraint_to_ints c)" (is ?R1)
proof -
show ?R0
using common_denominator(1) mul_constraint
unfolding constraint_to_ints_def by presburger
let ?x = "of_int (common_denominator c)"
have "c = Le_Constraint (lec_rel c) (lec_poly c) (lec_const c)"
using le_constraint.collapse by auto
hence "mul_constraint ?x c =
Le_Constraint (lec_rel c) (?x *R lec_poly c) (?x * lec_const c)"
using mul_constraint.simps by metis
hence "lec_poly (mul_constraint ?x c) = ?x *R lec_poly c"
and "lec_const (mul_constraint ?x c) = ?x * lec_const c" by auto
thus ?R1 using common_denominator(2-3) unfolding integral_linear_poly_def
unfolding constraint_to_ints_def
by simp
qed
lemma equal_leccoeffs_impl_equal_leccoeffsconstrainttoints:
assumes "lec_coeffs lec1 = lec_coeffs lec2"
shows "lec_coeffs (constraint_to_ints lec1) = lec_coeffs (constraint_to_ints lec2)"
proof -
have "⋀lec. set ((lec_const lec)
# (map (coeff (lec_poly lec)) (vars_list (lec_poly lec)))) = lec_coeffs lec"
using lec_coeffs.simps
by (metis Set.insert_def list.set(2) set_map singleton_conv Setcompr_eq_image
le_constraint.collapse set_vars_list)
hence cd_eq: "common_denominator lec1 = common_denominator lec2"
unfolding common_denominator_def using assms
by (metis (mono_tags, lifting) le_constraint.collapse le_constraint.rec set_map)
have "⋀x c. lec_coeffs (mul_constraint x c) = (λy. x * y) ` (lec_coeffs c)"
proof (goal_cases)
case (1 x c)
then show ?case
proof (cases "x = 0")
case True
then show ?thesis unfolding lec_coeffs_def mul_constraint_def
by (smt Collect_empty_eq Setcompr_eq_image Un_insert_left bot_set_def empty_iff
image_cong image_constant_conv insert_not_empty le_constraint.exhaust
le_constraint.rec mul_constraint.simps mult_zero_left
rational_vector.scale_zero_left set_zero sup_bot.left_neutral vars_zero)
next
case False
then show ?thesis
proof -
define r l cst where "r = lec_rel c" and "l = x *R lec_poly c"
and "cst = x * (lec_const c)"
have "lec_coeffs (Le_Constraint r l cst) = (λy. x * y) ` (lec_coeffs c)"
unfolding lec_coeffs_def r_def l_def cst_def
by (smt Collect_cong Set.insert_def Setcompr_eq_image coeff_scaleRat
image_insert le_constraint.collapse le_constraint.rec mem_Collect_eq
singleton_conv vars_scaleRat False)
thus ?thesis
unfolding mul_constraint_def r_def l_def cst_def
by (metis (no_types, lifting) le_constraint.collapse le_constraint.rec)
qed
qed
qed
thus ?thesis using cd_eq assms by (simp add: constraint_to_ints_def)
qed
lemma map_equal_leccoeffs_impl_equal_leccoeffsconstrainttoints:
assumes "map lec_coeffs lecs1 = map lec_coeffs lecs2"
shows "map lec_coeffs (map constraint_to_ints lecs1) =
map lec_coeffs (map constraint_to_ints lecs2)"
proof -
have "⋀i. lec_coeffs (constraint_to_ints (lecs1 ! i)) =
lec_coeffs (constraint_to_ints (lecs2 ! i))"
using equal_leccoeffs_impl_equal_leccoeffsconstrainttoints assms length_map nth_map undef_vec
by metis
thus ?thesis
by (metis (mono_tags, lifting) assms length_map nth_equalityI nth_map)
qed
lemma consttoints_preserves_vars:
shows "vars (lec_poly (constraint_to_ints lec)) ⊆ vars (lec_poly lec)"
unfolding constraint_to_ints_def mul_constraint_def
by (metis (no_types, lifting) le_constraint.collapse le_constraint.inject
le_constraint.rec vars_scaleRat1)
definition renvar_valuation :: "('a :: lrv valuation) ⇒ nat list ⇒ ('a :: lrv valuation)" where
"renvar_valuation vl vrs = (λi. if i < length vrs then vl (vrs ! i) else 0)"
definition renvar_index :: "nat ⇒ nat list ⇒ nat" where
"renvar_index i vrs = (if i∈ set vrs then (index vrs i) else length vrs)"
definition renvar_index_set :: "nat set ⇒ nat list ⇒ nat set" where
"renvar_index_set I vrs = (λi. renvar_index i vrs) ` I"
lemma renvar_valuation_int:
assumes "distinct vrs"
shows "v i ∈ ℤ ⟹ renvar_valuation v vrs (renvar_index i vrs) ∈ ℤ"
unfolding renvar_valuation_def renvar_index_def by simp
lift_definition renvar_linearpoly :: "linear_poly ⇒ (nat list) ⇒ linear_poly" is
"(λp vrs. (λi. if i < length vrs then p (vrs ! i) else 0))"
by auto
lemma renvar_linearpoly_minus:
shows "- renvar_linearpoly p vrs = renvar_linearpoly (-p) vrs"
proof -
{
fix v :: "var"
define minp where "minp = -p"
have "coeff (- renvar_linearpoly p vrs) v = - coeff (renvar_linearpoly p vrs) v"
by simp
also have "… = -(if v < length vrs then (coeff p (vrs ! v)) else 0)" by transfer auto
also have "… = (if v < length vrs then (coeff minp (vrs ! v)) else 0)"
unfolding minp_def by simp
also have "… = coeff (renvar_linearpoly minp vrs) v" by transfer auto
also have "… = coeff (renvar_linearpoly (-p) vrs) v" unfolding minp_def by simp
finally have "coeff (- renvar_linearpoly p vrs) v = coeff (renvar_linearpoly (-p) vrs) v"
by simp
}
thus ?thesis using poly_eqI by simp
qed
lemma renvar_linearpoly_diff:
shows "renvar_linearpoly p1 vrs - renvar_linearpoly p2 vrs =
renvar_linearpoly (p1 - p2) vrs"
proof -
{
fix v :: "var"
define p1p2 where "p1p2 = p1 - p2"
have "coeff (renvar_linearpoly p1 vrs - renvar_linearpoly p2 vrs) v
= coeff (renvar_linearpoly p1 vrs) v - coeff (renvar_linearpoly p2 vrs) v"
by simp
also have "coeff (renvar_linearpoly p1 vrs) v =
(if v < length vrs then (coeff p1 (vrs ! v)) else 0)" by transfer auto
also have "coeff (renvar_linearpoly p2 vrs) v =
(if v < length vrs then (coeff p2 (vrs ! v)) else 0)" by transfer auto
also have "(if v < length vrs then (coeff p1 (vrs ! v)) else 0) -
(if v < length vrs then (coeff p2 (vrs ! v)) else 0) =
(if v < length vrs then (coeff p1p2 (vrs ! v)) else 0)"
unfolding p1p2_def by simp
also have "… = coeff (renvar_linearpoly p1p2 vrs) v" by (transfer, auto)
finally have "coeff (renvar_linearpoly p1 vrs - renvar_linearpoly p2 vrs) v =
coeff (renvar_linearpoly (p1-p2) vrs) v" unfolding p1p2_def by simp
} note coeffid = this
thus ?thesis using poly_eq_iff coeffid by simp
qed
lemma varlist_renvar_linearpoly:
assumes "vars p ⊆ set vrs" and "distinct vrs"
shows "Max ({0} ∪ vars (renvar_linearpoly p vrs)) ≤ length vrs"
by (transfer,auto)
lemma renvar_linearpoly_var_range:
shows "vars (renvar_linearpoly lp vrs) ⊆ {0..(length vrs -1)}"
by (transfer, auto)
lemma renvar_linearpoly_sat:
assumes "vars p ⊆ set vrs" and "distinct vrs"
shows "(renvar_linearpoly p vrs)⦃renvar_valuation v vrs⦄ = p⦃v⦄"
unfolding renvar_valuation_def
using assms
proof (transfer, simp, goal_cases)
case (1 p vrs vl)
show ?case
proof -
have seq: "{v. (v < length vrs ⟶ p (vrs ! v) ≠ 0) ∧ v < length vrs} =
{v. v < length vrs ∧ p(vrs ! v) ≠ 0}" by blast
let ?A = "{v. v < length vrs ∧ p(vrs ! v) ≠ 0}"
let ?fct = "(λx. vrs ! x)"
have injo: "inj_on ?fct ?A" using 1 inj_on_nth by fastforce
have seq2: "?fct ` ?A = {v. p v ≠ 0}"
proof
{
fix x
assume pxz: "x ∈ {v. p v ≠ 0}"
hence "∃i < length vrs. x = vrs ! i" by (metis 1(2) in_set_conv_nth subsetD)
then obtain i where "x = vrs ! i" and "i < length vrs" by auto
hence "x ∈ ?fct ` ?A" using pxz by simp
}
thus "{v. p v ≠ 0} ⊆ (!) vrs ` {v. v < length vrs ∧ p (vrs ! v) ≠ 0}" by blast
qed auto
show ?thesis
by (metis (mono_tags, lifting) injo sum.reindex_cong seq2 seq)
qed
qed
lemma renvar_linearpoly_coeff:
assumes "vars p ⊆ set vrs" and "distinct vrs" and "i < length vrs"
shows "coeff (renvar_linearpoly p vrs) i = coeff p (vrs ! i)"
using assms
by (transfer, simp)
fun renvar_leconstraint :: "rat le_constraint ⇒ nat list ⇒ rat le_constraint" where
"renvar_leconstraint (Leqc l c) vrs = (Leqc (renvar_linearpoly l vrs) c)"
| "renvar_leconstraint (Ltc l c) vrs = (Ltc (renvar_linearpoly l vrs) c)"
lemma renvar_leconstraint_var_range:
assumes "vars (lec_poly c) ⊆ set vrs" and "distinct vrs"
shows "Max ({0} ∪ vars (lec_poly (renvar_leconstraint c vrs))) ≤ length vrs"
by (smt le_constraint.collapse le_constraint.sel(2)
le_rel.exhaust renvar_leconstraint.simps assms varlist_renvar_linearpoly)
lemma renvar_leconstraint_sat:
assumes "vars (lec_poly c) ⊆ set vrs" and "distinct vrs"
shows "(v :: rat valuation) ⊨⇩l⇩e c ⟷
(renvar_valuation v vrs) ⊨⇩l⇩e (renvar_leconstraint c vrs)"
using renvar_linearpoly_sat[OF assms(1) assms(2)]
by (metis (full_types) le_constraint.collapse le_rel.exhaust
renvar_leconstraint.simps(1) renvar_leconstraint.simps(2)
satisfiable_le_constraint.simps)
lemma lecpoly_renvar_commute:
shows "lec_poly (renvar_leconstraint c vrs) = renvar_linearpoly (lec_poly c) vrs"
by (metis (full_types) le_constraint.collapse le_constraint.sel(2) le_rel.exhaust
renvar_leconstraint.simps)
lemma lecconst_renvar_commute:
shows "lec_const lec = lec_const (renvar_leconstraint lec vrs)"
by (metis le_constraint.sel(3) renvar_leconstraint.elims)
lemma leccoeffs_renvar_invariant:
assumes "distinct vrs" and "vars (lec_poly lec) ⊆ set vrs"
shows "lec_coeffs lec = lec_coeffs (renvar_leconstraint lec vrs)"
proof
define renlec where "renlec = renvar_leconstraint lec vrs"
{
fix coef
assume coef: "coef ∈ lec_coeffs lec"
have "coef ∈ lec_coeffs (renvar_leconstraint lec vrs)"
proof (cases "coef = lec_const lec")
case True
then show ?thesis using lecconst_renvar_commute[of lec vrs] lecconst_in_leccoeffs by simp
next
case False
then show ?thesis
proof -
obtain vr where vr: "vr ∈ vars (lec_poly lec)" and
cf: "coef = coeff (lec_poly lec) vr"
by (smt False Un_insert_left coef insert_iff le_constraint.collapse
lec_coeffs.simps mem_Collect_eq sup_bot.left_neutral)
hence "coef = coeff (lec_poly renlec) (index vrs vr)"
unfolding renlec_def using renvar_linearpoly_coeff[OF assms(2) assms(1)]
lecpoly_renvar_commute assms(2) by auto
thus ?thesis unfolding lec_coeffs_def renlec_def
by (metis (mono_tags, lifting) UnI2 cf coeff_zero le_constraint.collapse
le_constraint.rec mem_Collect_eq renlec_def vr)
qed
qed
}
thus "lec_coeffs lec ⊆ lec_coeffs (renvar_leconstraint lec vrs)" by auto
{
fix coef
assume coef: "coef ∈ lec_coeffs renlec"
have "coef ∈ lec_coeffs lec"
proof (cases "coef = lec_const renlec")
case True
then show ?thesis using lecconst_renvar_commute[of lec vrs, symmetric]
lecconst_in_leccoeffs unfolding renlec_def by simp
next
case False
then show ?thesis
proof -
obtain vr where vr: "vr ∈ vars (lec_poly renlec)" and
cf: "coef = coeff (lec_poly renlec) vr"
by (smt False Un_insert_left coef insert_iff
le_constraint.collapse lec_coeffs.simps mem_Collect_eq sup_bot.left_neutral)
have "vrs ≠ []" using vr
by (metis assms(2) coeff_zero diff_self in_set_simps(3) lecpoly_renvar_commute
renvar_linearpoly_diff renlec_def subsetI subset_antisym zero_coeff_zero)
hence "vr < length vrs"
using One_nat_def atLeastAtMost_iff diff_Suc_less length_greater_0_conv
lecpoly_renvar_commute renvar_linearpoly_var_range less_le_trans not_less
by (metis (no_types, lifting) in_mono renlec_def vr)
hence "coef = coeff (lec_poly lec) (vrs ! vr)"
using cf unfolding renlec_def
by (simp add: assms lecpoly_renvar_commute renvar_linearpoly_coeff)
thus ?thesis unfolding lec_coeffs_def
by (metis (mono_tags, lifting) UnI2 cf coeff_zero le_constraint.collapse
le_constraint.rec mem_Collect_eq vr)
qed
qed
}
thus "lec_coeffs (renvar_leconstraint lec vrs) ⊆ lec_coeffs lec" unfolding renlec_def
by auto
qed
primrec renvar_constraint :: "constraint ⇒ nat list ⇒ constraint" where
"renvar_constraint (LEQ l x) vrs = (LEQ (renvar_linearpoly l vrs) x)"
| "renvar_constraint (GEQ l x) vrs = (GEQ (renvar_linearpoly l vrs) x)"
| "renvar_constraint (LT l x) vrs = (LT (renvar_linearpoly l vrs) x)"
| "renvar_constraint (GT l x) vrs = (GT (renvar_linearpoly l vrs) x)"
| "renvar_constraint (EQ l x) vrs = (EQ (renvar_linearpoly l vrs) x)"
| "renvar_constraint (LEQPP l0 l1) vrs = (LEQPP (renvar_linearpoly l0 vrs) (renvar_linearpoly l1 vrs))"
| "renvar_constraint (GEQPP l0 l1) vrs = (GEQPP (renvar_linearpoly l0 vrs) (renvar_linearpoly l1 vrs))"
| "renvar_constraint (LTPP l0 l1) vrs = (LTPP (renvar_linearpoly l0 vrs) (renvar_linearpoly l1 vrs))"
| "renvar_constraint (GTPP l0 l1) vrs = (GTPP (renvar_linearpoly l0 vrs) (renvar_linearpoly l1 vrs))"
| "renvar_constraint (EQPP l0 l1) vrs = (EQPP (renvar_linearpoly l0 vrs) (renvar_linearpoly l1 vrs))"
lemma constrtoleconstr_renvar_commute:
shows "set (constraint_to_le_constraint (renvar_constraint c vrs)) =
(λx. renvar_leconstraint x vrs) ` set (constraint_to_le_constraint c)"
by (cases c, auto simp: renvar_linearpoly_diff renvar_linearpoly_minus)
lemma constrtoleconstr_renvar_commute_list:
shows
"constraint_to_le_constraint (renvar_constraint c vrs) =
map (λx. renvar_leconstraint x vrs) (constraint_to_le_constraint c)"
by (cases c, auto simp: renvar_linearpoly_diff renvar_linearpoly_minus)
lemma renvar_constraint_var_range:
assumes "set (var_list [c]) ⊆ set vrs" and "distinct vrs"
shows "Max ({0} ∪ set (var_list [renvar_constraint c vrs])) ≤ length vrs"
using var_list_def constrtoleconstr_renvar_commute set_vars_list assms
renvar_leconstraint_var_range finite_vars by fastforce
lemma renvar_constraint_sat:
assumes "set (var_list [c]) ⊆ set vrs" and "distinct vrs"
shows "(v :: rat valuation) ⊨⇩c c ⟷
(renvar_valuation v vrs) ⊨⇩c renvar_constraint c vrs"
proof -
have "∀p ∈ set (map lec_poly (constraint_to_le_constraint c)). vars p ⊆ set vrs"
using assms set_vars_list unfolding var_list_def by auto
thus ?thesis using constraint_to_le_constraint renvar_leconstraint_sat assms
constraint_to_le_constraint constrtoleconstr_renvar_commute by fastforce
qed
definition renvar_constraintlist where
"renvar_constraintlist cs vrs = map (λx. renvar_constraint x vrs) cs"
lemma renvar_constraintlist_var_range:
assumes "set (var_list cs) ⊆ set vrs" and "distinct vrs"
shows "Max ({0} ∪ set (var_list (renvar_constraintlist cs vrs))) ≤ length vrs"
using var_list_def renvar_constraintlist_def renvar_constraint_def assms
renvar_constraint_var_range Max_ge by fastforce
lemma renvar_constraintlist_sat:
assumes "set (var_list cs) ⊆ set vrs" and "distinct vrs"
shows "v ⊨⇩c⇩s set cs ⟷
(renvar_valuation v vrs) ⊨⇩c⇩s set (renvar_constraintlist cs vrs)"
proof -
have "⋀c. c ∈ set cs ⟹
v ⊨⇩c c ⟷ (renvar_valuation v vrs) ⊨⇩c renvar_constraint c vrs"
using var_list_def assms renvar_constraint_sat by fastforce
thus ?thesis by (simp add: renvar_constraintlist_def)
qed
lemma renvar_constraintlist_sat':
shows "v ⊨⇩c⇩s set cs ⟷ (renvar_valuation v (var_list cs)) ⊨⇩c⇩s
set (renvar_constraintlist cs (var_list cs))"
using renvar_constraintlist_sat unfolding var_list_def by simp
lemma leccoeffs_normalize_renvar_invariant:
assumes "set (var_list cs) ⊆ set vrs" and "distinct vrs"
shows "(map lec_coeffs (normalize cs)) =
(map lec_coeffs (normalize (renvar_constraintlist cs vrs)))"
proof -
have "normalize (renvar_constraintlist cs vrs) =
(map (λx. renvar_leconstraint x vrs) (normalize cs))"
unfolding normalize_def renvar_constraintlist_def
by (smt length_map map_nth_eq_conv renvar_constraintlist_def map_concat
constrtoleconstr_renvar_commute_list)
thus ?thesis
using leccoeffs_renvar_invariant[OF assms(2)] assms(1) constrtoleconstr_preserves_vars
by fastforce
qed
lemma maxcoeffconstraints_renvar_invariant:
shows "(let le_cs = normalize cs;
le_cs' = map constraint_to_ints le_cs in max_coeff_constraints le_cs') =
(let le_cs = normalize (renvar_constraintlist cs (var_list cs));
le_cs' = map constraint_to_ints le_cs in max_coeff_constraints le_cs')" (is "?A = ?B")
using map_equal_leccoeffs_impl_equal_leccoeffsconstrainttoints varlist_distinct
leccoeffs_normalize_renvar_invariant equal_mapleccoeffs_impl_equal_maxcoeff(2)
by (meson order_refl)
definition truncate_val where
"truncate_val v maxvr = (λi. if i < maxvr then v i else 0)"
lemma truncated_valuation_linearpoly:
assumes "vars p ⊆ set vrs" and "distinct vrs"
shows "(renvar_linearpoly p vrs)⦃v⦄ =
(renvar_linearpoly p vrs)⦃truncate_val v (length vrs)⦄"
unfolding truncate_val_def
by(transfer, auto)
lemma truncated_valuation_leconstraint:
assumes "vars (lec_poly c) ⊆ set vrs" and "distinct vrs"
shows "v ⊨⇩l⇩e (renvar_leconstraint c vrs) ⟷
(truncate_val v (length vrs)) ⊨⇩l⇩e (renvar_leconstraint c vrs)"
by (metis le_constraint.sel(2) renvar_leconstraint.elims le_constraint.collapse
satisfiable_le_constraint.simps truncated_valuation_linearpoly assms)
lemma truncated_valuation_constraint:
assumes "set (var_list [c]) ⊆ set vrs" and "distinct vrs"
shows "(v :: rat valuation) ⊨⇩c (renvar_constraint c vrs) ⟷
(truncate_val v (length vrs)) ⊨⇩c (renvar_constraint c vrs)"
using constrtoleconstr_renvar_commute constraint_to_le_constraint set_vars_list
truncated_valuation_leconstraint assms var_list_def by fastforce
lemma renvar_valuation_indexset_sat:
assumes "distinct vrs" and "set (var_list cs) ⊆ set vrs"
and "v ⊨⇩m⇩c⇩s (set (renvar_constraintlist cs vrs), (renvar_index_set I vrs))
∧ (∀i∈ (renvar_index_set I vrs). ¦v i¦ ≤ bnd)"
shows "∃v'. v' ⊨⇩m⇩c⇩s (set cs, I) ∧ (∀i∈ I. ¦v' i¦ ≤ bnd)"
proof -
define rencs where "rencs = renvar_constraintlist cs vrs"
define trv where "trv = truncate_val v (length vrs)"
have mod: "trv ⊨⇩m⇩c⇩s (set (renvar_constraintlist cs vrs), (renvar_index_set I vrs))"
proof -
{
fix rc
assume c: "rc ∈ set (rencs)"
from this obtain c where c: "c ∈ set cs" and "rc = renvar_constraint c vrs"
and "set (var_list [c]) ⊆ set vrs"
using assms(2) unfolding rencs_def renvar_constraintlist_def var_list_def
by auto
hence "trv ⊨⇩c rc ⟷ v ⊨⇩c rc" unfolding trv_def
using truncated_valuation_constraint assms(1) by blast
}
thus ?thesis using assms(3) rencs_def satisfies_mixed_constraints.simps
unfolding trv_def renvar_index_set_def truncate_val_def by simp
qed
define v' where "v' = (λvr. if vr ∈ set vrs then v (index vrs vr) else 0)"
have rv: "trv = renvar_valuation v' vrs"
unfolding trv_def v'_def renvar_valuation_def truncate_val_def
using assms(1) index_nth_id nth_mem by metis
hence "v' ⊨⇩c⇩s set cs" using assms(1,2) mod
using renvar_constraintlist_sat satisfies_mixed_constraints.simps by blast
moreover have "∀ i ∈ I. v' i ∈ ℤ" using assms(3)
by (simp add: renvar_index_def renvar_index_set_def v'_def)
ultimately have md: "v' ⊨⇩m⇩c⇩s (set cs, I)" by simp
have "⋀i. i ∈ (set vrs) ⟹
v' i = v (renvar_index i vrs)" unfolding v'_def renvar_index_def by simp
hence "∀i∈ I. ¦v' i¦ ≤ bnd" using rv
using assms(3) renvar_index_set_def v'_def by auto
thus ?thesis using md by blast
qed
definition compute_bound_num_of_vars :: "constraint list ⇒ int" where
"compute_bound_num_of_vars cs =
(let le_cs = normalize cs in
let le_cs' = map constraint_to_ints le_cs in
let max_coeff = max_coeff_constraints le_cs' in
let n = 1 + length (var_list cs) in
fact (n + 1) * ⌊max_coeff⌋ ^ n)"
definition compute_bound :: "constraint list ⇒ int" where
"compute_bound cs =
(let le_cs = normalize cs in
let le_cs' = map constraint_to_ints le_cs in
let max_coeff = max_coeff_constraints le_cs' in
let n = 1 + constraints_max_var le_cs' in
fact (n + 1) * ⌊max_coeff⌋ ^ n)"
lemma power_increasing_int:
"1 ≤ n ⟹ n ≤ N ⟹ 0 ≤ (a :: int) ⟹ a ^ n ≤ a ^ N"
by (cases "a = 0", insert power_increasing[of n N a], auto simp: power_0_left)
lemma computebound_leq_computeboundnumofvars:
shows "compute_bound (renvar_constraintlist cs (var_list cs)) ≤ compute_bound_num_of_vars cs"
proof -
define rencs where "rencs = renvar_constraintlist cs (var_list cs)"
define le_cs where "le_cs = normalize rencs"
define le_cs' where "le_cs' = map constraint_to_ints le_cs"
define max_cf where "max_cf = max_coeff_constraints le_cs'"
define n where "n = 1 + constraints_max_var le_cs'"
let ?fact = "fact :: nat ⇒ int"
define Bnd where "Bnd = ?fact (n + 1) * ⌊max_cf⌋ ^ n"
have id: "compute_bound (renvar_constraintlist cs (var_list cs)) = Bnd"
unfolding compute_bound_def Bnd_def n_def max_cf_def le_cs'_def le_cs_def rencs_def
by metis
define nn where "nn = 1 + length (var_list cs)"
define max_coeff where "max_coeff = (let le_cs = normalize cs;
le_cs' = map constraint_to_ints le_cs in max_coeff_constraints le_cs')"
have ineq0: "n ≤ nn"
proof -
have fav: "∀v ∈ ⋃ (vars ` (set (map lec_poly le_cs'))). v ≤ length (var_list cs)"
using rencs_def renvar_constraintlist_var_range varlist_distinct
consttoints_preserves_vars constrtoleconstr_preserves_vars le_cs_def
unfolding le_cs'_def by fastforce
have "constraints_max_var le_cs' ∈ {0} ∪ ⋃ (vars ` (set (map lec_poly le_cs')))"
proof (cases le_cs')
case Nil
then show ?thesis unfolding constraints_max_var_def by simp
next
case (Cons a list)
then show ?thesis
proof -
obtain lec where "lec ∈ set le_cs'" and
"Max (lec_max_var ` set (le_cs')) = lec_max_var lec"
using Gram_Schmidt_2.ex_MAXIMUM Cons List.finite_set set_empty2
by (metis Collect_mem_eq empty_Collect_eq list.set_intros(1))
thus ?thesis unfolding max_var_def constraints_max_var_def
using Cons finite_vars vars_empty_zero by fastforce
qed
qed
hence "constraints_max_var le_cs' ≤ length (var_list cs)" using fav by auto
thus ?thesis unfolding n_def nn_def by simp
qed
have id': "max_cf = max_coeff"
unfolding max_cf_def le_cs'_def le_cs_def rencs_def max_coeff_def
using maxcoeffconstraints_renvar_invariant by simp
have id'': "compute_bound_num_of_vars cs = ?fact (nn + 1) * ⌊max_coeff⌋ ^ nn"
unfolding compute_bound_num_of_vars_def max_coeff_def nn_def by metis
have mc0: "floor max_coeff ≥ 0" unfolding id'[symmetric] max_cf_def max_coeff_constraints_def
by simp
have n0: "n > 0" unfolding n_def by auto
show ?thesis unfolding id id'' Bnd_def id' using mc0 ineq0 n0
by (intro mult_mono power_increasing_int, auto intro!: mult_mono fact_mono)
qed
lemma compute_bound:
assumes "vl ⊨⇩m⇩c⇩s (set cs_list, Is)"
shows "∃ v. v ⊨⇩m⇩c⇩s (set cs_list, Is) ∧
(∀ i ∈ Is. ¦v i¦ ≤ of_int (compute_bound_num_of_vars cs_list))"
proof -
define cs where "cs = renvar_constraintlist cs_list (var_list cs_list)"
have dist: "distinct (var_list cs_list)" unfolding var_list_def by simp
define v where "v = renvar_valuation vl (var_list cs_list)"
define I where "I = renvar_index_set Is (var_list cs_list)"
have v_models: "v ⊨⇩m⇩c⇩s (set cs, I)"
using assms renvar_constraintlist_sat' renvar_valuation_int
unfolding cs_def v_def I_def
by (simp, smt distinct_remdups imageE renvar_index_set_def
renvar_valuation_int var_list_def)
define le_cs where "le_cs = normalize cs"
define le_cs' where "le_cs' = map constraint_to_ints le_cs"
define max_cf where "max_cf = max_coeff_constraints le_cs'"
define n where "n = 1 + constraints_max_var le_cs'"
define Bnd where "Bnd = fact (n + 1) * (⌊max_cf⌋) ^ n"
have "compute_bound cs = Bnd"
unfolding compute_bound_def le_cs_def le_cs'_def
max_cf_def n_def Bnd_def by metis
hence ineq: "Bnd ≤ compute_bound_num_of_vars cs_list"
unfolding cs_def using computebound_leq_computeboundnumofvars by auto
interpret gram_schmidt_floor n .
have int: "integral_constraints le_cs'"
unfolding le_cs'_def integral_constraints_def
using constraint_to_ints(2) by auto
hence "max_cf ∈ ℤ"
unfolding max_cf_def integral_constraints_def
max_coeff_constraints_def
using integral_max_coeff Max_in[of "set (0 # map max_coeff le_cs')"]
by fastforce
hence "of_int ⌊max_cf⌋ = max_cf" using floor_of_int_eq by blast
hence Bnd_rat: "of_int Bnd = fact (n + 1) * max_cf ^ n"
unfolding Bnd_def by auto
have max_cf0: "max_cf ≥ 0" unfolding max_cf_def
using max_coeff_constraints_0 .
have "rat_of_int Bnd ≥ 0" unfolding Bnd_def using max_cf0 by auto
obtain A b A' b' where matsvecs: "mats_vecs_of_constraints le_cs' = (A, b, A', b')"
by (rule prod_cases4)
obtain nr nr' where
A_dim: "A ∈ carrier_mat nr n" and b_dim: "b ∈ carrier_vec nr" and
A'_dim: "A' ∈ carrier_mat nr' n" and b'_dim: "b' ∈ carrier_vec nr'"
using mats_vecs_of_constraints(1)[OF matsvecs n_def] by blast
from mats_vecs_of_constraints(3-4)[OF matsvecs n_def] int
have A: "A ∈ ℤ⇩m ∩ Bounded_mat max_cf"
and A': "A' ∈ ℤ⇩m ∩ Bounded_mat max_cf"
and b: "b ∈ ℤ⇩v ∩ Bounded_vec max_cf"
and b': "b' ∈ ℤ⇩v ∩ Bounded_vec max_cf"
unfolding max_cf_def by auto
{
fix v
have "v ⊨⇩c⇩s set cs ⟷ (∀ c ∈ set le_cs. v ⊨⇩l⇩e c)"
unfolding le_cs_def by (rule normalize_satisfies)
also have "… ⟷ (∀ c ∈ set le_cs'. v ⊨⇩l⇩e c)"
unfolding le_cs'_def using constraint_to_ints(1) by auto
also have "… ⟷ (A *⇩v vec n v ≤ b ∧ A' *⇩v vec n v <⇩v b')"
by (rule mats_vecs_of_constraints(2)[OF matsvecs n_def])
finally have "v ⊨⇩c⇩s set cs ⟷ (A *⇩v vec n v ≤ b ∧ A' *⇩v vec n v <⇩v b')"
by blast
} note sat_cs = this
hence Avb: "A *⇩v vec n v ≤ b" and A'vb': "A' *⇩v vec n v <⇩v b'" using v_models by auto
from v_models have "vec n v ∈ indexed_Ints_vec I"
unfolding indexed_Ints_vec_def by auto
then obtain x where xn: "x ∈ carrier_vec n" and xI: "x ∈ indexed_Ints_vec I"
and Axb: "A *⇩v x ≤ b" and A'xb': "A' *⇩v x <⇩v b'"
and xBnd: "x ∈ Bounded_vec (of_int Bnd)"
using small_mixed_integer_solution[OF A_dim A'_dim b_dim b'_dim
A b A' b' _ _ Avb A'vb'] max_cf0
unfolding Bnd_rat by auto
define v' where "v' = (λ i. if i < n then x $ i else 0)"
have "vec n v' = x" unfolding v'_def using xn by fastforce
hence "v' ⊨⇩c⇩s set cs"
using sat_cs Axb A'xb' by presburger
moreover have "∀ i ∈ I. v' i ∈ ℤ"
using xI xn unfolding v'_def indexed_Ints_vec_def by fastforce
moreover have "∀ i. ¦v' i¦ ≤ of_int Bnd"
proof (rule allI, cases)
fix i assume "i < n"
thus "¦v' i¦ ≤ of_int Bnd"
using xBnd xn unfolding v'_def Bounded_vec_def by fastforce
next
fix i assume "¬ (i < n)"
thus "¦v' i¦ ≤ of_int Bnd" unfolding v'_def using `of_int Bnd ≥ 0` by fastforce
qed
ultimately have
"∃v. v ⊨⇩m⇩c⇩s (set cs, I) ∧ (∀i∈I. ¦v i¦ ≤ rat_of_int (compute_bound_num_of_vars cs_list))"
using ineq
by (meson dual_order.trans of_int_le_iff satisfies_mixed_constraints.simps)
from this obtain tmpv where
"tmpv ⊨⇩m⇩c⇩s (set cs, I) ∧ (∀i∈I. ¦tmpv i¦ ≤ rat_of_int (compute_bound_num_of_vars cs_list))" by auto
thus ?thesis
using renvar_valuation_indexset_sat[OF varlist_distinct[of cs_list],
of cs_list tmpv Is "rat_of_int (compute_bound_num_of_vars cs_list)"]
unfolding cs_def I_def by simp
qed
definition branch_and_bound :: "constraint list ⇒ var list ⇒ rat valuation option"
where "branch_and_bound cs Is = (
let Bnd = compute_bound_num_of_vars cs in
branch_and_bound_core cs Is (λ _. -Bnd) (λ _. Bnd))"
lemma branch_and_bound_sat:
"branch_and_bound cs Is = Some v ⟹ v ⊨⇩m⇩c⇩s (set cs, set Is)"
unfolding branch_and_bound_def using branch_and_bound_core_sat by metis
lemma branch_and_bound_unsat:
assumes "branch_and_bound cs Is = None"
shows "¬ v ⊨⇩m⇩c⇩s (set cs, set Is)"
proof
define Bnd where "Bnd = compute_bound_num_of_vars cs"
assume "v ⊨⇩m⇩c⇩s (set cs, set Is)"
then obtain v where v: "v ⊨⇩m⇩c⇩s (set cs, set Is)"
and vBnd: "(∀ i ∈ set Is. ¦v i¦ ≤ of_int Bnd)"
using compute_bound unfolding Bnd_def by blast
from assms have "branch_and_bound_core cs Is (λ _. -Bnd) (λ _. Bnd) = None"
unfolding branch_and_bound_def Bnd_def by metis
moreover from vBnd have "(∀ i ∈ set Is. of_int (-Bnd) ≤ v i ∧ v i ≤ of_int Bnd)"
by fastforce
ultimately show False
using branch_and_bound_core_unsat v by presburger
qed
definition vars_of_constraints :: "constraint list ⇒ var list" where
"vars_of_constraints cs = remdups (concat (map (vars_list o lec_poly) (normalize cs)))"
lemma vars_of_constraints_cong: assumes "⋀ x. x ∈ set (vars_of_constraints cs) ⟹ v x = w x"
shows "(v ⊨⇩c⇩s set cs) = (w ⊨⇩c⇩s set cs)"
unfolding normalize_satisfies vars_of_constraints_def
proof (intro ball_cong[OF refl], goal_cases)
case (1 c)
with assms have "∀ x ∈ vars (lec_poly c). v x = w x"
unfolding vars_of_constraints_def o_def by (auto simp: set_vars_list)
from valuate_depend[OF this] show ?case by (cases c, auto)
qed
definition branch_and_bound_int :: "constraint list ⇒ int valuation option" where
"branch_and_bound_int cs = (
let vs = vars_of_constraints cs
in case branch_and_bound cs vs of
None ⇒ None
| Some v ⇒ Some (λ x. if x ∈ set vs then int_of_rat (v x) else 0))"
lemma branch_and_bound_int_sat: assumes "branch_and_bound_int cs = Some v"
shows "(rat_of_int o v) ⊨⇩c⇩s set cs"
proof -
let ?vs = "vars_of_constraints cs"
from assms obtain w where
some: "branch_and_bound cs ?vs = Some w" and
v: "v = (λ x. if x ∈ set ?vs then int_of_rat (w x) else 0)"
by (cases "branch_and_bound cs ?vs", auto simp: branch_and_bound_int_def)
from branch_and_bound_sat[OF some]
have w: "w ⊨⇩c⇩s set cs" and int: "∀i∈set (vars_of_constraints cs). w i ∈ ℤ"
by auto
moreover have "(w ⊨⇩c⇩s set cs) = ((rat_of_int o v) ⊨⇩c⇩s set cs)"
by (rule vars_of_constraints_cong, unfold v, insert int, auto)
ultimately show ?thesis by auto
qed
lemma branch_and_bound_int_unsat: assumes "branch_and_bound_int cs = None"
shows "¬ (rat_of_int o v) ⊨⇩c⇩s set cs"
proof -
let ?vs = "vars_of_constraints cs"
from assms have
none: "branch_and_bound cs ?vs = None"
by (cases "branch_and_bound cs ?vs", auto simp: branch_and_bound_int_def)
from branch_and_bound_unsat[OF none, of "rat_of_int o v"]
show ?thesis by auto
qed
section ‹Wrapper Lemmas for branch_and_bound using incremental simplex›
definition bnb_incr
where "bnb_incr cs Is = (
let Bnd = compute_bound_num_of_vars cs in
let (cs', lb_m, ub_m, s) = bnb_state_init cs Is (λ _. -Bnd) (λ _. Bnd) in
case s of Inr s' ⇒ the (bnb_state_core_p cs' Is lb_m ub_m s')
| Inl _ ⇒ None)"
lemma bnb_incr_unsat:
assumes "bnb_incr cs Is = None" "distinct Is"
shows "¬ v ⊨⇩m⇩c⇩s (set cs, set Is)"
proof -
define Bnd where "Bnd = compute_bound_num_of_vars cs"
obtain cs' lb_m ub_m s where a: "(cs', lb_m, ub_m, s) = bnb_state_init cs Is (λ _. -Bnd) (λ _. Bnd)"
using prod_cases4 by metis
have aa: "map snd cs' = cs"
using a unfolding bnb_state_init_def by (auto simp add: Let_def)
show ?thesis
proof (cases s)
case (Inl a)
have b: "∄v. v ⊨⇩c⇩s set (bounds_to_constraints Is (λ _. -Bnd) (λ _. Bnd) @ cs)"
using assms a Inl by (intro bnb_state_init'[of _ _ _ _ cs' lb_m ub_m s]) (auto)
have False if c: "v ⊨⇩m⇩c⇩s (set cs, set Is)" for v
proof -
obtain v where v: "v ⊨⇩m⇩c⇩s (set cs, set Is)" and vBnd: "(∀ i ∈ set Is. ¦v i¦ ≤ of_int Bnd)"
using c compute_bound unfolding Bnd_def by blast
have "v ⊨⇩c⇩s set (bounds_to_constraints Is (λ_. - Bnd) (λ_. Bnd))"
using vBnd v by (subst bounds_to_constraints_sat) auto
then have "v ⊨⇩c⇩s set (bounds_to_constraints Is (λ_. - Bnd) (λ_. Bnd) @ cs)"
using v by auto
then show False
using b by blast
qed
then show ?thesis
by blast
next
case (Inr s')
define lb where "lb = the ∘ Mapping.lookup lb_m"
define ub where "ub = the ∘ Mapping.lookup ub_m"
have "bnb_state_core_p cs' Is lb_m ub_m s' = Some (bnb_state_core cs' Is lb ub s')"
unfolding lb_def ub_def apply(rule bnb_state_core_p)
apply(simp) apply(simp)
apply(rule bnb_state_init[of _ cs "(λ _. -Bnd)" "(λ _. Bnd)" _ _ _ s])
using assms Inr a by (auto)
then have b1: "bnb_state_core cs' Is lb ub s' = None"
using assms unfolding bnb_incr_def using a Inr unfolding Bnd_def
by (auto simp add: Let_def split: sum.splits prod.splits)
have "map (λx. snd (the (map_of (map2 (λx y. (x, y, f x)) xs ys) x))) xs = map f xs"
if "length ys = length xs" "distinct xs" for ys::"'c list" and xs and f::"'a ⇒ 'b"
using that proof (induction xs arbitrary: ys)
case Nil
then show ?case by (simp)
next
case (Cons x xs)
then have "∃y ys'. ys = y # ys'"
by (metis length_nth_simps(2) list.exhaust list.map(1) list.map(2) list.simps(3) list.size(3) nth_Cons_0 nth_Cons_Suc zip_Nil)
then obtain y ys' where "ys = y # ys'"
by blast
then show ?case
using Cons by (auto)
qed
then have 1: "(snd (the (map_of (map2 (λx y. (x, y, f x)) xs ys) x))) = f x"
if "length ys = length xs" "distinct xs" "x ∈ set xs"for ys::"'c list" and x xs and f::"'a ⇒ 'b"
using map_eq_conv that by auto
have False if c: "v ⊨⇩m⇩c⇩s (set cs, set Is)"
proof -
have ca: "x ∈ set Is ⟹ - Bnd = (snd ∘ (the ∘ Mapping.lookup lb_m)) x" for x
using a 1 assms unfolding bnb_state_init_def by (auto simp add: Let_def 1 lookup_of_alist)
have cb: "x ∈ set Is ⟹ Bnd = (snd ∘ (the ∘ Mapping.lookup ub_m)) x" for x
using a 1 assms unfolding bnb_state_init_def by (auto simp add: Let_def 1 lookup_of_alist)
obtain v where v: "v ⊨⇩m⇩c⇩s (set cs, set Is)" and vBnd: "(∀ i ∈ set Is. ¦v i¦ ≤ of_int Bnd)"
using c compute_bound unfolding Bnd_def by blast
have "v ⊨⇩c⇩s set (bounds_to_constraints Is (λ_. - Bnd) (λ_. Bnd))"
using vBnd v by (subst bounds_to_constraints_sat) auto
then have "¬ v ⊨⇩m⇩c⇩s (snd ` set cs', set Is)"
apply(intro bnb_state_core_unsat)
unfolding i_bounds_to_constraints
apply(rule bnb_state_init[of _ cs "(λ _. -Bnd)" "(λ _. Bnd)" _ _ _ s])
using assms Inr a b1 apply(auto simp add: lb_def ub_def)
apply(subst (asm) bounds_to_constraints_cong[of _ _ "snd ∘ (the ∘ Mapping.lookup lb_m)"
_ "snd ∘ (the ∘ Mapping.lookup ub_m)"])
using ca cb by (auto)
then show ?thesis
using v aa by fastforce
qed
then show ?thesis
by blast
qed
qed
lemma bnb_incr_sat:
assumes "bnb_incr cs Is = Some v" "distinct Is"
shows "v ⊨⇩m⇩c⇩s (set cs, set Is)"
proof -
define Bnd where "Bnd = compute_bound_num_of_vars cs"
obtain cs' lb_m ub_m s where a: "(cs', lb_m, ub_m, s) = bnb_state_init cs Is (λ _. -Bnd) (λ _. Bnd)"
using prod_cases4 by metis
have aa: "map snd cs' = cs"
using a unfolding bnb_state_init_def by (auto simp add: Let_def)
show ?thesis
proof (cases s)
case (Inl a)
then show ?thesis
using assms a unfolding bnb_incr_def Bnd_def
by (auto simp add: Let_def split: prod.splits sum.splits)
next
case (Inr s')
define lb where "lb = the ∘ Mapping.lookup lb_m"
define ub where "ub = the ∘ Mapping.lookup ub_m"
have "bnb_state_core_p cs' Is lb_m ub_m s' = Some (bnb_state_core cs' Is lb ub s')"
unfolding lb_def ub_def apply(rule bnb_state_core_p)
apply(simp) apply(simp)
apply(rule bnb_state_init[of _ cs "(λ _. -Bnd)" "(λ _. Bnd)" _ _ _ s])
using assms Inr a by auto
then have b1: "bnb_state_core cs' Is lb ub s' = Some v"
using assms unfolding bnb_incr_def using a Inr unfolding Bnd_def
by (auto simp add: Let_def split: sum.splits prod.splits)
then have "v ⊨⇩m⇩c⇩s (snd ` (set cs'), set Is)"
apply(intro bnb_state_core_sat)
apply(rule bnb_state_init[OF _ a[symmetric]])
using assms Inr a unfolding lb_def ub_def by auto
then show ?thesis
using aa by auto
qed
qed
definition bnb_incr_int :: "constraint list ⇒ int valuation option" where
"bnb_incr_int cs = (
let vs = vars_of_constraints cs
in case bnb_incr cs vs of
None ⇒ None
| Some v ⇒ Some (λ x. if x ∈ set vs then int_of_rat (v x) else 0))"
lemma vars_of_constraints_distinct: "distinct (vars_of_constraints cs)"
unfolding vars_of_constraints_def by simp
lemma bnb_incr_int_sat: assumes "bnb_incr_int cs = Some v"
shows "(rat_of_int o v) ⊨⇩c⇩s set cs"
proof -
let ?vs = "vars_of_constraints cs"
from assms obtain w where
some: "bnb_incr cs ?vs = Some w" and
v: "v = (λ x. if x ∈ set ?vs then int_of_rat (w x) else 0)"
by (cases "bnb_incr cs ?vs", auto simp: bnb_incr_int_def)
from bnb_incr_sat[OF some]
have w: "w ⊨⇩c⇩s set cs" and int: "∀i∈set (vars_of_constraints cs). w i ∈ ℤ"
using vars_of_constraints_distinct by auto
moreover have "(w ⊨⇩c⇩s set cs) = ((rat_of_int o v) ⊨⇩c⇩s set cs)"
by (rule vars_of_constraints_cong, unfold v, insert int, auto)
ultimately show ?thesis by auto
qed
lemma bnb_incr_int_unsat: assumes "bnb_incr_int cs = None"
shows "¬ (rat_of_int ∘ v) ⊨⇩c⇩s set cs"
proof -
let ?vs = "vars_of_constraints cs"
from assms have
none: "bnb_incr cs ?vs = None"
by (cases "bnb_incr cs ?vs", auto simp: bnb_incr_int_def)
from bnb_incr_unsat[OF none, of "rat_of_int o v"] vars_of_constraints_distinct
show ?thesis by auto
qed
hide_const (open) Var
hide_const (open) max_var
hide_const (open) vars_list
end