Theory Simplex_Incremental
section ‹The Incremental Simplex Algorithm›
text ‹In this theory we specify operations which permit to incrementally
add constraints. To this end, first an indexed list of potential constraints is used
to construct the initial state, and then one can activate indices, extract solutions or unsat cores,
do backtracking, etc.›
theory Simplex_Incremental
imports Simplex
begin
subsection ‹Lowest Layer: Fixed Tableau and Incremental Atoms›
text ‹Interface›
locale Incremental_Atom_Ops = fixes
init_s :: "tableau ⇒ 's" and
assert_s :: "('i,'a :: lrv) i_atom ⇒ 's ⇒ 'i list + 's" and
check_s :: "'s ⇒ 's × ('i list option)" and
solution_s :: "'s ⇒ (var, 'a) mapping" and
checkpoint_s :: "'s ⇒ 'c" and
backtrack_s :: "'c ⇒ 's ⇒ 's" and
precond_s :: "tableau ⇒ bool" and
weak_invariant_s :: "tableau ⇒ ('i,'a) i_atom set ⇒ 's ⇒ bool" and
invariant_s :: "tableau ⇒ ('i,'a) i_atom set ⇒ 's ⇒ bool" and
checked_s :: "tableau ⇒ ('i,'a) i_atom set ⇒ 's ⇒ bool"
assumes
assert_s_ok: "invariant_s t as s ⟹ assert_s a s = Inr s' ⟹
invariant_s t (insert a as) s'" and
assert_s_unsat: "invariant_s t as s ⟹ assert_s a s = Unsat I ⟹
minimal_unsat_core_tabl_atoms (set I) t (insert a as)" and
check_s_ok: "invariant_s t as s ⟹ check_s s = (s', None) ⟹
checked_s t as s'" and
check_s_unsat: "invariant_s t as s ⟹ check_s s = (s',Some I) ⟹
weak_invariant_s t as s' ∧ minimal_unsat_core_tabl_atoms (set I) t as" and
init_s: "precond_s t ⟹ checked_s t {} (init_s t)" and
solution_s: "checked_s t as s ⟹ solution_s s = v ⟹ ⟨v⟩ ⊨⇩t t ∧ ⟨v⟩ ⊨⇩a⇩s Simplex.flat as" and
backtrack_s: "checked_s t as s ⟹ checkpoint_s s = c
⟹ weak_invariant_s t bs s' ⟹ backtrack_s c s' = s'' ⟹ as ⊆ bs ⟹ invariant_s t as s''" and
weak_invariant_s: "invariant_s t as s ⟹ weak_invariant_s t as s" and
checked_invariant_s: "checked_s t as s ⟹ invariant_s t as s"
begin
fun assert_all_s :: "('i,'a) i_atom list ⇒ 's ⇒ 'i list + 's" where
"assert_all_s [] s = Inr s"
| "assert_all_s (a # as) s = (case assert_s a s of Unsat I ⇒ Unsat I
| Inr s' ⇒ assert_all_s as s')"
lemma assert_all_s_ok: "invariant_s t as s ⟹ assert_all_s bs s = Inr s' ⟹
invariant_s t (set bs ∪ as) s'"
proof (induct bs arbitrary: s as)
case (Cons b bs s as)
from Cons(3) obtain s'' where ass: "assert_s b s = Inr s''" and rec: "assert_all_s bs s'' = Inr s'"
by (auto split: sum.splits)
from Cons(1)[OF assert_s_ok[OF Cons(2) ass] rec]
show ?case by auto
qed auto
lemma assert_all_s_unsat: "invariant_s t as s ⟹ assert_all_s bs s = Unsat I ⟹
minimal_unsat_core_tabl_atoms (set I) t (as ∪ set bs)"
proof (induct bs arbitrary: s as)
case (Cons b bs s as)
show ?case
proof (cases "assert_s b s")
case unsat: (Inl J)
with Cons have J: "J = I" by auto
from assert_s_unsat[OF Cons(2) unsat] J
have min: "minimal_unsat_core_tabl_atoms (set I) t (insert b as)" by auto
show ?thesis
by (rule minimal_unsat_core_tabl_atoms_mono[OF _ min], auto)
next
case (Inr s')
from Cons(1)[OF assert_s_ok[OF Cons(2) Inr]] Cons(3) Inr show ?thesis by auto
qed
qed simp
end
text ‹Implementation of the interface via the Simplex operations init, check, and assert-bound.›
locale Incremental_State_Ops_Simplex = AssertBoundNoLhs assert_bound + Init init + Check check
for assert_bound :: "('i,'a::lrv) i_atom ⇒ ('i,'a) state ⇒ ('i,'a) state" and
init :: "tableau ⇒ ('i,'a) state" and
check :: "('i,'a) state ⇒ ('i,'a) state"
begin
definition weak_invariant_s where
"weak_invariant_s t (as :: ('i,'a)i_atom set) s =
(⊨⇩n⇩o⇩l⇩h⇩s s ∧
△ (𝒯 s) ∧
∇ s ∧
◇ s ∧
(∀ v :: (var ⇒ 'a). v ⊨⇩t 𝒯 s ⟷ v ⊨⇩t t) ∧
index_valid as s ∧
Simplex.flat as ≐ ℬ s ∧
as ⊨⇩i ℬℐ s)"
definition invariant_s where
"invariant_s t (as :: ('i,'a)i_atom set) s =
(weak_invariant_s t as s ∧ ¬ 𝒰 s)"
definition checked_s where
"checked_s t as s = (invariant_s t as s ∧ ⊨ s)"
definition assert_s where "assert_s a s = (let s' = assert_bound a s in
if 𝒰 s' then Inl (the (𝒰⇩c s')) else Inr s')"
definition check_s where "check_s s = (let s' = check s in
if 𝒰 s' then (s', Some (the (𝒰⇩c s'))) else (s', None))"
definition checkpoint_s where "checkpoint_s s = ℬ⇩i s"
fun backtrack_s :: "_ ⇒ ('i, 'a) state ⇒ ('i, 'a) state"
where "backtrack_s (bl, bu) (State t bl_old bu_old v u uc) = State t bl bu v False None"
lemmas invariant_defs = weak_invariant_s_def invariant_s_def checked_s_def
lemma invariant_sD: assumes "invariant_s t as s"
shows "¬ 𝒰 s" "⊨⇩n⇩o⇩l⇩h⇩s s" "△ (𝒯 s)" "∇ s" "◇ s"
"Simplex.flat as ≐ ℬ s" "as ⊨⇩i ℬℐ s" "index_valid as s"
"(∀ v :: (var ⇒ 'a). v ⊨⇩t 𝒯 s ⟷ v ⊨⇩t t)"
using assms unfolding invariant_defs by auto
lemma weak_invariant_sD: assumes "weak_invariant_s t as s"
shows "⊨⇩n⇩o⇩l⇩h⇩s s" "△ (𝒯 s)" "∇ s" "◇ s"
"Simplex.flat as ≐ ℬ s" "as ⊨⇩i ℬℐ s" "index_valid as s"
"(∀ v :: (var ⇒ 'a). v ⊨⇩t 𝒯 s ⟷ v ⊨⇩t t)"
using assms unfolding invariant_defs by auto
lemma minimal_unsat_state_core_translation: assumes
unsat: "minimal_unsat_state_core (s :: ('i,'a::lrv)state)" and
tabl: "∀(v :: 'a valuation). v ⊨⇩t 𝒯 s = v ⊨⇩t t" and
index: "index_valid as s" and
imp: "as ⊨⇩i ℬℐ s" and
I: "I = the (𝒰⇩c s)"
shows "minimal_unsat_core_tabl_atoms (set I) t as"
unfolding minimal_unsat_core_tabl_atoms_def
proof (intro conjI impI notI allI; (elim exE conjE)?)
from unsat[unfolded minimal_unsat_state_core_def]
have unsat: "unsat_state_core s"
and minimal: "distinct_indices_state s ⟹ subsets_sat_core s"
by auto
from unsat[unfolded unsat_state_core_def I[symmetric]]
have Is: "set I ⊆ indices_state s" and unsat: "(∄v. (set I, v) ⊨⇩i⇩s s)" by auto
from Is index show "set I ⊆ fst ` as"
using index_valid_indices_state by blast
{
fix v
assume t: "v ⊨⇩t t" and as: "(set I, v) ⊨⇩i⇩a⇩s as"
from t tabl have t: "v ⊨⇩t 𝒯 s" by auto
then have "(set I, v) ⊨⇩i⇩s s" using as imp
using atoms_imply_bounds_index.simps satisfies_state_index.simps by blast
with unsat show False by blast
}
{
fix J
assume dist: "distinct_indices_atoms as"
and J: "J ⊂ set I"
from J Is have J': "J ⊆ indices_state s" by auto
from dist index have "distinct_indices_state s" by (metis index_valid_distinct_indices)
with minimal have "subsets_sat_core s" .
from this[unfolded subsets_sat_core_def I[symmetric], rule_format, OF J]
obtain v where "(J, v) ⊨⇩i⇩s⇩e s" by blast
from satisfying_state_valuation_to_atom_tabl[OF J' this index dist] tabl
show "∃v. v ⊨⇩t t ∧ (J, v) ⊨⇩i⇩a⇩e⇩s as" by blast
}
qed
sublocale Incremental_Atom_Ops
init assert_s check_s 𝒱 checkpoint_s backtrack_s △ weak_invariant_s invariant_s checked_s
proof (unfold_locales, goal_cases)
case (1 t as s a s')
from 1(2)[unfolded assert_s_def Let_def]
have U: "¬ 𝒰 (assert_bound a s)" and s': "s' = assert_bound a s" by (auto split: if_splits)
note * = invariant_sD[OF 1(1)]
from assert_bound_nolhs_tableau_id[OF *(1-5)]
have T: "𝒯 s' = 𝒯 s" unfolding s' by auto
from *(3,9)
have "△ (𝒯 s')" "∀ v :: var ⇒ 'a. v ⊨⇩t 𝒯 s' = v ⊨⇩t t" unfolding T by blast+
moreover from assert_bound_nolhs_sat[OF *(1-5) U]
have " ⊨⇩n⇩o⇩l⇩h⇩s s'" "◇ s'" unfolding s' by auto
moreover from assert_bound_nolhs_atoms_equiv_bounds[OF *(1-6), of a]
have "Simplex.flat (insert a as) ≐ ℬ s'" unfolding s' by auto
moreover from assert_bound_nolhs_atoms_imply_bounds_index[OF *(1-5,7)]
have "insert a as ⊨⇩i ℬℐ s'" unfolding s' .
moreover from assert_bound_nolhs_tableau_valuated[OF *(1-5)]
have "∇ s'" unfolding s' .
moreover from assert_bound_nolhs_index_valid[OF *(1-5,8)]
have "index_valid (insert a as) s'" unfolding s' by auto
moreover from U s'
have "¬ 𝒰 s'" by auto
ultimately show ?case unfolding invariant_defs by auto
next
case (2 t as s a I)
from 2(2)[unfolded assert_s_def Let_def]
obtain s' where s': "s' = assert_bound a s" and U: "𝒰 (assert_bound a s)"
and I: "I = the (𝒰⇩c s')"
by (auto split: if_splits)
note * = invariant_sD[OF 2(1)]
from assert_bound_nolhs_tableau_id[OF *(1-5)]
have T: "𝒯 s' = 𝒯 s" unfolding s' by auto
from *(3,9)
have tabl: "∀ v :: var ⇒ 'a. v ⊨⇩t 𝒯 s' = v ⊨⇩t t" unfolding T by blast+
from assert_bound_nolhs_unsat[OF *(1-5,8) U] s'
have unsat: "minimal_unsat_state_core s'" by auto
from assert_bound_nolhs_index_valid[OF *(1-5,8)]
have index: "index_valid (insert a as) s'" unfolding s' by auto
from assert_bound_nolhs_atoms_imply_bounds_index[OF *(1-5,7)]
have imp: "insert a as ⊨⇩i ℬℐ s'" unfolding s' .
from minimal_unsat_state_core_translation[OF unsat tabl index imp I]
show ?case .
next
case (3 t as s s')
from 3(2)[unfolded check_s_def Let_def]
have U: "¬ 𝒰 (check s)" and s': "s' = check s" by (auto split: if_splits)
note * = invariant_sD[OF 3(1)]
note ** = *(1,2,5,3,4)
from check_tableau_equiv[OF **] *(9)
have "∀v :: _ ⇒ 'a. v ⊨⇩t 𝒯 s' = v ⊨⇩t t" unfolding s' by auto
moreover from check_tableau_index_valid[OF **] *(8)
have "index_valid as s'" unfolding s' by auto
moreover from check_tableau_normalized[OF **]
have "△ (𝒯 s')" unfolding s' .
moreover from check_tableau_valuated[OF **]
have "∇ s'" unfolding s' .
moreover from check_sat[OF ** U]
have "⊨ s'" unfolding s'.
moreover from satisfies_satisfies_no_lhs[OF this] satisfies_consistent[of s'] this
have " ⊨⇩n⇩o⇩l⇩h⇩s s'" "◇ s'" by blast+
moreover from check_bounds_id[OF **] *(6)
have "Simplex.flat as ≐ ℬ s'" unfolding s' by (auto simp: boundsu_def boundsl_def)
moreover from check_bounds_id[OF **] *(7)
have "as ⊨⇩i ℬℐ s'" unfolding s' by (auto simp: boundsu_def boundsl_def indexu_def indexl_def)
moreover from U
have "¬ 𝒰 s'" unfolding s' .
ultimately show ?case unfolding invariant_defs by auto
next
case (4 t as s s' I)
from 4(2)[unfolded check_s_def Let_def]
have s': "s' = check s" and U: "𝒰 (check s)"
and I: "I = the (𝒰⇩c s')"
by (auto split: if_splits)
note * = invariant_sD[OF 4(1)]
note ** = *(1,2,5,3,4)
from check_unsat[OF ** U]
have unsat: "minimal_unsat_state_core s'" unfolding s' by auto
from check_tableau_equiv[OF **] *(9)
have tabl: "∀v :: _ ⇒ 'a. v ⊨⇩t 𝒯 s' = v ⊨⇩t t" unfolding s' by auto
from check_tableau_index_valid[OF **] *(8)
have index: "index_valid as s'" unfolding s' by auto
from check_bounds_id[OF **] *(7)
have imp: "as ⊨⇩i ℬℐ s'" unfolding s' by (auto simp: boundsu_def boundsl_def indexu_def indexl_def)
from check_bounds_id[OF **] *(6)
have bequiv: "Simplex.flat as ≐ ℬ s'" unfolding s' by (auto simp: boundsu_def boundsl_def)
have "weak_invariant_s t as s'" unfolding invariant_defs
using
check_tableau_normalized[OF **]
check_tableau_valuated[OF **]
check_tableau[OF **]
unfolding s'[symmetric]
by (intro conjI index imp tabl bequiv, auto)
with minimal_unsat_state_core_translation[OF unsat tabl index imp I]
show ?case by auto
next
case *: (5 t)
show ?case unfolding invariant_defs
using
init_tableau_normalized[OF *]
init_index_valid[of _ t]
init_atoms_imply_bounds_index[of t]
init_satisfies[of t]
init_atoms_equiv_bounds[of t]
init_tableau_id[of t]
init_unsat_flag[of t]
init_tableau_valuated[of t]
satisfies_consistent[of "init t"] satisfies_satisfies_no_lhs[of "init t"]
by auto
next
case (6 t as s v)
then show ?case unfolding invariant_defs
by (meson atoms_equiv_bounds.simps curr_val_satisfies_state_def satisfies_state_def)
next
case (7 t as s c bs s' s'')
from 7(1)[unfolded checked_s_def]
have inv_s: "invariant_s t as s" and s: "⊨ s" by auto
from 7(2) have c: "c = ℬ⇩i s" unfolding checkpoint_s_def by auto
have s'': "𝒯 s'' = 𝒯 s'" "𝒱 s'' = 𝒱 s'" "ℬ⇩i s'' = ℬ⇩i s" "𝒰 s'' = False" "𝒰⇩c s'' = None"
unfolding 7(4)[symmetric] c
by (atomize(full), cases s', auto)
then have BI: "ℬ s'' = ℬ s" "ℐ s'' = ℐ s" by (auto simp: boundsu_def boundsl_def indexu_def indexl_def)
note * = invariant_sD[OF inv_s]
note ** = weak_invariant_sD[OF 7(3)]
have "¬ 𝒰 s''" unfolding s'' by auto
moreover from **(2)
have "△ (𝒯 s'')" unfolding s'' .
moreover from **(3)
have "∇ s''" unfolding tableau_valuated_def s'' .
moreover from **(8)
have "∀v :: _ ⇒ 'a. v ⊨⇩t 𝒯 s'' = v ⊨⇩t t" unfolding s'' .
moreover from *(6)
have "Simplex.flat as ≐ ℬ s''" unfolding BI .
moreover from *(7)
have "as ⊨⇩i ℬℐ s''" unfolding BI .
moreover from *(8)
have "index_valid as s''" unfolding index_valid_def using s'' by auto
moreover from **(3)
have "∇ s''" unfolding tableau_valuated_def s'' .
moreover from satisfies_consistent[of s] s
have "◇ s''" unfolding bounds_consistent_def using BI by auto
moreover
from 7(5) *(6) **(5)
have vB: "v ⊨⇩b ℬ s' ⟹ v ⊨⇩b ℬ s''" for v
unfolding atoms_equiv_bounds.simps satisfies_atom_set_def BI
by force
from **(1)
have t: "⟨𝒱 s'⟩ ⊨⇩t 𝒯 s'" and b: "⟨𝒱 s'⟩ ⊨⇩b ℬ s' ∥ - lvars (𝒯 s')"
unfolding curr_val_satisfies_no_lhs_def by auto
let ?v = "λ x. if x ∈ lvars (𝒯 s') then case ℬ⇩l s' x of None ⇒ the (ℬ⇩u s' x) | Some b ⇒ b else ⟨𝒱 s'⟩ x"
have "?v ⊨⇩b ℬ s'" unfolding satisfies_bounds.simps
proof (intro allI)
fix x :: var
show "in_bounds x ?v (ℬ s')"
proof (cases "x ∈ lvars (𝒯 s')")
case True
with **(4)[unfolded bounds_consistent_def, rule_format, of x]
show ?thesis by (cases "ℬ⇩l s' x"; cases "ℬ⇩u s' x", auto simp: bound_compare_defs)
next
case False
with b
show ?thesis unfolding satisfies_bounds_set.simps by auto
qed
qed
from vB[OF this] have v: "?v ⊨⇩b ℬ s''" .
have "⟨𝒱 s'⟩ ⊨⇩b ℬ s'' ∥ - lvars (𝒯 s')" unfolding satisfies_bounds_set.simps
proof clarify
fix x
assume "x ∉ lvars (𝒯 s')"
with v[unfolded satisfies_bounds.simps, rule_format, of x]
show "in_bounds x ⟨𝒱 s'⟩ (ℬ s'')" by auto
qed
with t have "⊨⇩n⇩o⇩l⇩h⇩s s''" unfolding curr_val_satisfies_no_lhs_def s''
by auto
ultimately show ?case unfolding invariant_defs by blast
qed (auto simp: invariant_defs)
end
subsection ‹Intermediate Layer: Incremental Non-Strict Constraints›
text ‹Interface›
locale Incremental_NS_Constraint_Ops = fixes
init_nsc :: "('i,'a :: lrv) i_ns_constraint list ⇒ 's" and
assert_nsc :: "'i ⇒ 's ⇒ 'i list + 's" and
check_nsc :: "'s ⇒ 's × ('i list option)" and
solution_nsc :: "'s ⇒ (var, 'a) mapping" and
checkpoint_nsc :: "'s ⇒ 'c" and
backtrack_nsc :: "'c ⇒ 's ⇒ 's" and
weak_invariant_nsc :: "('i,'a) i_ns_constraint list ⇒ 'i set ⇒ 's ⇒ bool" and
invariant_nsc :: "('i,'a) i_ns_constraint list ⇒ 'i set ⇒ 's ⇒ bool" and
checked_nsc :: "('i,'a) i_ns_constraint list ⇒ 'i set ⇒ 's ⇒ bool"
assumes
assert_nsc_ok: "invariant_nsc nsc J s ⟹ assert_nsc j s = Inr s' ⟹
invariant_nsc nsc (insert j J) s'" and
assert_nsc_unsat: "invariant_nsc nsc J s ⟹ assert_nsc j s = Unsat I ⟹
set I ⊆ insert j J ∧ minimal_unsat_core_ns (set I) (set nsc)" and
check_nsc_ok: "invariant_nsc nsc J s ⟹ check_nsc s = (s', None) ⟹
checked_nsc nsc J s'" and
check_nsc_unsat: "invariant_nsc nsc J s ⟹ check_nsc s = (s',Some I) ⟹
set I ⊆ J ∧ weak_invariant_nsc nsc J s' ∧ minimal_unsat_core_ns (set I) (set nsc)" and
init_nsc: "checked_nsc nsc {} (init_nsc nsc)" and
solution_nsc: "checked_nsc nsc J s ⟹ solution_nsc s = v ⟹ (J, ⟨v⟩) ⊨⇩i⇩n⇩s⇩s set nsc" and
backtrack_nsc: "checked_nsc nsc J s ⟹ checkpoint_nsc s = c
⟹ weak_invariant_nsc nsc K s' ⟹ backtrack_nsc c s' = s'' ⟹ J ⊆ K ⟹ invariant_nsc nsc J s''" and
weak_invariant_nsc: "invariant_nsc nsc J s ⟹ weak_invariant_nsc nsc J s" and
checked_invariant_nsc: "checked_nsc nsc J s ⟹ invariant_nsc nsc J s"
text ‹Implementation via the Simplex operation preprocess and the incremental operations for atoms.›
fun create_map :: "('i × 'a)list ⇒ ('i, ('i × 'a) list)mapping" where
"create_map [] = Mapping.empty"
| "create_map ((i,a) # xs) = (let m = create_map xs in
case Mapping.lookup m i of
None ⇒ Mapping.update i [(i,a)] m
| Some ias ⇒ Mapping.update i ((i,a) # ias) m)"
definition list_map_to_fun :: "('i, ('i × 'a) list)mapping ⇒ 'i ⇒ ('i × 'a) list" where
"list_map_to_fun m i = (case Mapping.lookup m i of None ⇒ [] | Some ias ⇒ ias)"
lemma list_map_to_fun_create_map: "set (list_map_to_fun (create_map ias) i) = set ias ∩ {i} × UNIV"
proof (induct ias)
case Nil
show ?case unfolding list_map_to_fun_def by auto
next
case (Cons ja ias)
obtain j a where ja: "ja = (j,a)" by force
show ?case
proof (cases "j = i")
case False
then have id: "list_map_to_fun (create_map (ja # ias)) i = list_map_to_fun (create_map ias) i"
unfolding ja list_map_to_fun_def
by (auto simp: Let_def split: option.splits)
show ?thesis unfolding id Cons unfolding ja using False by auto
next
case True
with ja have ja: "ja = (i,a)" by auto
have id: "list_map_to_fun (create_map (ja # ias)) i = ja # list_map_to_fun (create_map ias) i"
unfolding ja list_map_to_fun_def
by (auto simp: Let_def split: option.splits)
show ?thesis unfolding id using Cons unfolding ja by auto
qed
qed
fun prod_wrap :: "('c ⇒ 's ⇒ 's × ('i list option))
⇒ 'c × 's ⇒ ('c × 's) × ('i list option)" where
"prod_wrap f (asi,s) = (case f asi s of (s', info) ⇒ ((asi,s'), info))"
lemma prod_wrap_def': "prod_wrap f (asi,s) = map_prod (Pair asi) id (f asi s)"
unfolding prod_wrap.simps by (auto split: prod.splits)
locale Incremental_Atom_Ops_For_NS_Constraint_Ops =
Incremental_Atom_Ops init_s assert_s check_s solution_s checkpoint_s backtrack_s △
weak_invariant_s invariant_s checked_s
+ Preprocess preprocess
for
init_s :: "tableau ⇒ 's" and
assert_s :: "('i :: linorder,'a :: lrv) i_atom ⇒ 's ⇒ 'i list + 's" and
check_s :: "'s ⇒ 's × 'i list option" and
solution_s :: "'s ⇒ (var, 'a) mapping" and
checkpoint_s :: "'s ⇒ 'c" and
backtrack_s :: "'c ⇒ 's ⇒ 's" and
weak_invariant_s :: "tableau ⇒ ('i,'a) i_atom set ⇒ 's ⇒ bool" and
invariant_s :: "tableau ⇒ ('i,'a) i_atom set ⇒ 's ⇒ bool" and
checked_s :: "tableau ⇒ ('i,'a) i_atom set ⇒ 's ⇒ bool" and
preprocess :: "('i,'a) i_ns_constraint list ⇒ tableau × ('i,'a) i_atom list × ((var,'a)mapping ⇒ (var,'a)mapping) × 'i list"
begin
definition check_nsc where "check_nsc = prod_wrap (λ asitv. check_s)"
definition assert_nsc where "assert_nsc i = (λ ((asi,tv,ui),s).
if i ∈ set ui then Unsat [i] else
case assert_all_s (list_map_to_fun asi i) s of Unsat I ⇒ Unsat I | Inr s' ⇒ Inr ((asi,tv,ui),s'))"
fun checkpoint_nsc where "checkpoint_nsc (asi_tv_ui,s) = checkpoint_s s"
fun backtrack_nsc where "backtrack_nsc c (asi_tv_ui,s) = (asi_tv_ui, backtrack_s c s)"
fun solution_nsc where "solution_nsc ((asi,tv,ui),s) = tv (solution_s s)"
definition "init_nsc nsc = (case preprocess nsc of (t,as,trans_v,ui) ⇒
((create_map as, trans_v, remdups ui), init_s t))"
fun invariant_as_asi where "invariant_as_asi as asi tc tc' ui ui' = (tc = tc' ∧ set ui = set ui' ∧
(∀ i. set (list_map_to_fun asi i) = (as ∩ ({i} × UNIV))))"
fun weak_invariant_nsc where
"weak_invariant_nsc nsc J ((asi,tv,ui),s) = (case preprocess nsc of (t,as,tv',ui') ⇒ invariant_as_asi (set as) asi tv tv' ui ui' ∧
weak_invariant_s t (set as ∩ (J × UNIV)) s ∧ J ∩ set ui = {})"
fun invariant_nsc where
"invariant_nsc nsc J ((asi,tv,ui),s) = (case preprocess nsc of (t,as,tv',ui') ⇒ invariant_as_asi (set as) asi tv tv' ui ui' ∧
invariant_s t (set as ∩ (J × UNIV)) s ∧ J ∩ set ui = {})"
fun checked_nsc where
"checked_nsc nsc J ((asi,tv,ui),s) = (case preprocess nsc of (t,as,tv',ui') ⇒ invariant_as_asi (set as) asi tv tv' ui ui' ∧
checked_s t (set as ∩ (J × UNIV)) s ∧ J ∩ set ui = {})"
lemma i_satisfies_atom_set_inter_right: "((I, v) ⊨⇩i⇩a⇩s (ats ∩ (J × UNIV))) ⟷ ((I ∩ J, v) ⊨⇩i⇩a⇩s ats)"
unfolding i_satisfies_atom_set.simps
by (rule arg_cong[of _ _ "λ x. v ⊨⇩a⇩s x"], auto)
lemma ns_constraints_ops: "Incremental_NS_Constraint_Ops init_nsc assert_nsc
check_nsc solution_nsc checkpoint_nsc backtrack_nsc
weak_invariant_nsc invariant_nsc checked_nsc"
proof (unfold_locales, goal_cases)
case (1 nsc J S j S')
obtain asi tv s ui where S: "S = ((asi,tv,ui),s)" by (cases S, auto)
obtain t as tv' ui' where prep[simp]: "preprocess nsc = (t, as, tv', ui')" by (cases "preprocess nsc")
note pre = 1[unfolded S assert_nsc_def]
from pre(2) obtain s' where
ok: "assert_all_s (list_map_to_fun asi j) s = Inr s'" and S': "S' = ((asi,tv,ui),s')" and j: "j ∉ set ui"
by (auto split: sum.splits if_splits)
from pre(1)[simplified]
have inv: "invariant_s t (set as ∩ J × UNIV) s"
and asi: "set (list_map_to_fun asi j) = set as ∩ {j} × UNIV" "invariant_as_asi (set as) asi tv tv' ui ui'" "J ∩ set ui = {}" by auto
from assert_all_s_ok[OF inv ok, unfolded asi] asi(2-) j
show ?case unfolding invariant_nsc.simps S' prep split
by (metis Int_insert_left Sigma_Un_distrib1 inf_sup_distrib1 insert_is_Un)
next
case (2 nsc J S j I)
obtain asi s tv ui where S: "S = ((asi,tv,ui),s)" by (cases S, auto)
obtain t as tv' ui' where prep[simp]: "preprocess nsc = (t, as, tv', ui')" by (cases "preprocess nsc")
note pre = 2[unfolded S assert_nsc_def split]
show ?case
proof (cases "j ∈ set ui")
case False
with pre(2) have unsat: "assert_all_s (list_map_to_fun asi j) s = Unsat I"
by (auto split: sum.splits)
from pre(1)
have inv: "invariant_s t (set as ∩ J × UNIV) s"
and asi: "set (list_map_to_fun asi j) = set as ∩ {j} × UNIV" by auto
from assert_all_s_unsat[OF inv unsat, unfolded asi]
have "minimal_unsat_core_tabl_atoms (set I) t (set as ∩ J × UNIV ∪ set as ∩ {j} × UNIV)" .
also have "set as ∩ J × UNIV ∪ set as ∩ {j} × UNIV = set as ∩ insert j J × UNIV" by blast
finally have unsat: "minimal_unsat_core_tabl_atoms (set I) t (set as ∩ insert j J × UNIV)" .
hence I: "set I ⊆ insert j J" unfolding minimal_unsat_core_tabl_atoms_def by force
with False pre have empty: "set I ∩ set ui' = {}" by auto
have "minimal_unsat_core_tabl_atoms (set I) t (set as)"
by (rule minimal_unsat_core_tabl_atoms_mono[OF _ unsat], auto)
from preprocess_minimal_unsat_core[OF prep this empty]
have "minimal_unsat_core_ns (set I) (set nsc)" .
then show ?thesis using I by blast
next
case True
with pre(2) have I: "I = [j]" by auto
from pre(1)[unfolded invariant_nsc.simps prep split invariant_as_asi.simps]
have "set ui = set ui'" by simp
with True have j: "j ∈ set ui'" by auto
from preprocess_unsat_index[OF prep j]
show ?thesis unfolding I by auto
qed
next
case (3 nsc J S S')
then show ?case using check_s_ok unfolding check_nsc_def
by (cases S, auto split: prod.splits, blast)
next
case (4 nsc J S S' I)
obtain asi s tv ui where S: "S = ((asi,tv,ui),s)" by (cases S, auto)
obtain t as tv' ui' where prep[simp]: "preprocess nsc = (t, as, tv', ui')" by (cases "preprocess nsc")
from 4(2)[unfolded S check_nsc_def, simplified]
obtain s' where unsat: "check_s s = (s', Some I)" and S': "S' = ((asi, tv, ui), s')"
by (cases "check_s s", auto)
note pre = 4[unfolded S check_nsc_def unsat, simplified]
from pre have
inv: "invariant_s t (set as ∩ J × UNIV) s"
by auto
from check_s_unsat[OF inv unsat]
have weak: "weak_invariant_s t (set as ∩ J × UNIV) s'"
and unsat: "minimal_unsat_core_tabl_atoms (set I) t (set as ∩ J × UNIV)" by auto
hence I: "set I ⊆ J" unfolding minimal_unsat_core_tabl_atoms_def by force
with pre have empty: "set I ∩ set ui' = {}" by auto
have "minimal_unsat_core_tabl_atoms (set I) t (set as)"
by (rule minimal_unsat_core_tabl_atoms_mono[OF _ unsat], auto)
from preprocess_minimal_unsat_core[OF prep this empty]
have "minimal_unsat_core_ns (set I) (set nsc)" .
then show ?case using I weak unfolding S' using pre by auto
next
case (5 nsc)
obtain t as tv' ui' where prep[simp]: "preprocess nsc = (t, as, tv', ui')" by (cases "preprocess nsc")
show ?case unfolding init_nsc_def
using init_s preprocess_tableau_normalized[OF prep]
by (auto simp: list_map_to_fun_create_map)
next
case (6 nsc J S v)
obtain asi s tv ui where S: "S = ((asi,tv,ui),s)" by (cases S, auto)
obtain t as tv' ui' where prep[simp]: "preprocess nsc = (t, as, tv', ui')" by (cases "preprocess nsc")
have "(J,⟨solution_s s⟩) ⊨⇩i⇩a⇩s set as" "⟨solution_s s⟩ ⊨⇩t t"
using 6 S solution_s[of t _ s] by auto
from i_preprocess_sat[OF prep _ this]
show ?case using 6 S by auto
next
case (7 nsc J S c K S' S'')
obtain t as tvp uip where prep[simp]: "preprocess nsc = (t, as, tvp, uip)" by (cases "preprocess nsc")
obtain asi s tv ui where S: "S = ((asi,tv,ui),s)" by (cases S, auto)
obtain asi' s' tv' ui' where S': "S' = ((asi',tv',ui'),s')" by (cases S', auto)
obtain asi'' s'' tv'' ui'' where S'': "S'' = ((asi'',tv'',ui''),s'')" by (cases S'', auto)
from backtrack_s[of t _ s c _ s' s'']
show ?case using 7 S S' S'' by auto
next
case (8 nsc J S)
then show ?case using weak_invariant_s by (cases S, auto)
next
case (9 nsc J S)
then show ?case using checked_invariant_s by (cases S, auto)
qed
end
subsection ‹Highest Layer: Incremental Constraints›
text ‹Interface›
locale Incremental_Simplex_Ops = fixes
init_cs :: "'i i_constraint list ⇒ 's" and
assert_cs :: "'i ⇒ 's ⇒ 'i list + 's" and
check_cs :: "'s ⇒ 's × 'i list option" and
solution_cs :: "'s ⇒ rat valuation" and
checkpoint_cs :: "'s ⇒ 'c" and
backtrack_cs :: "'c ⇒ 's ⇒ 's" and
weak_invariant_cs :: "'i i_constraint list ⇒ 'i set ⇒ 's ⇒ bool" and
invariant_cs :: "'i i_constraint list ⇒ 'i set ⇒ 's ⇒ bool" and
checked_cs :: "'i i_constraint list ⇒ 'i set ⇒ 's ⇒ bool"
assumes
assert_cs_ok: "invariant_cs cs J s ⟹ assert_cs j s = Inr s' ⟹
invariant_cs cs (insert j J) s'" and
assert_cs_unsat: "invariant_cs cs J s ⟹ assert_cs j s = Unsat I ⟹
set I ⊆ insert j J ∧ minimal_unsat_core (set I) cs" and
check_cs_ok: "invariant_cs cs J s ⟹ check_cs s = (s', None) ⟹
checked_cs cs J s'" and
check_cs_unsat: "invariant_cs cs J s ⟹ check_cs s = (s',Some I) ⟹
weak_invariant_cs cs J s' ∧ set I ⊆ J ∧ minimal_unsat_core (set I) cs" and
init_cs: "checked_cs cs {} (init_cs cs)" and
solution_cs: "checked_cs cs J s ⟹ solution_cs s = v ⟹ (J, v) ⊨⇩i⇩c⇩s set cs" and
backtrack_cs: "checked_cs cs J s ⟹ checkpoint_cs s = c
⟹ weak_invariant_cs cs K s' ⟹ backtrack_cs c s' = s'' ⟹ J ⊆ K ⟹ invariant_cs cs J s''" and
weak_invariant_cs: "invariant_cs cs J s ⟹ weak_invariant_cs cs J s" and
checked_invariant_cs: "checked_cs cs J s ⟹ invariant_cs cs J s"
text ‹Implementation via the Simplex-operation To-Ns and the Incremental Operations for Non-Strict Constraints›
locale Incremental_NS_Constraint_Ops_To_Ns_For_Incremental_Simplex =
Incremental_NS_Constraint_Ops init_nsc assert_nsc check_nsc solution_nsc checkpoint_nsc backtrack_nsc
weak_invariant_nsc invariant_nsc checked_nsc + To_ns to_ns from_ns
for
init_nsc :: "('i,'a :: lrv) i_ns_constraint list ⇒ 's" and
assert_nsc :: "'i ⇒ 's ⇒ 'i list + 's" and
check_nsc :: "'s ⇒ 's × 'i list option" and
solution_nsc :: "'s ⇒ (var, 'a) mapping" and
checkpoint_nsc :: "'s ⇒ 'c" and
backtrack_nsc :: "'c ⇒ 's ⇒ 's" and
weak_invariant_nsc :: "('i,'a) i_ns_constraint list ⇒ 'i set ⇒ 's ⇒ bool" and
invariant_nsc :: "('i,'a) i_ns_constraint list ⇒ 'i set ⇒ 's ⇒ bool" and
checked_nsc :: "('i,'a) i_ns_constraint list ⇒ 'i set ⇒ 's ⇒ bool" and
to_ns :: "'i i_constraint list ⇒ ('i,'a) i_ns_constraint list" and
from_ns :: "(var, 'a) mapping ⇒ 'a ns_constraint list ⇒ (var, rat) mapping"
begin
fun assert_cs where "assert_cs i (cs,s) = (case assert_nsc i s of
Unsat I ⇒ Unsat I
| Inr s' ⇒ Inr (cs, s'))"
definition "init_cs cs = (let tons_cs = to_ns cs in (map snd (tons_cs), init_nsc tons_cs))"
definition "check_cs s = prod_wrap (λ cs. check_nsc) s"
fun checkpoint_cs where "checkpoint_cs (cs,s) = (checkpoint_nsc s)"
fun backtrack_cs where "backtrack_cs c (cs,s) = (cs, backtrack_nsc c s)"
fun solution_cs where "solution_cs (cs,s) = (⟨from_ns (solution_nsc s) cs⟩)"
fun weak_invariant_cs where
"weak_invariant_cs cs J (ds,s) = (ds = map snd (to_ns cs) ∧ weak_invariant_nsc (to_ns cs) J s)"
fun invariant_cs where
"invariant_cs cs J (ds,s) = (ds = map snd (to_ns cs) ∧ invariant_nsc (to_ns cs) J s)"
fun checked_cs where
"checked_cs cs J (ds,s) = (ds = map snd (to_ns cs) ∧ checked_nsc (to_ns cs) J s)"
sublocale Incremental_Simplex_Ops
init_cs
assert_cs
check_cs
solution_cs
checkpoint_cs
backtrack_cs
weak_invariant_cs
invariant_cs
checked_cs
proof (unfold_locales, goal_cases)
case (1 cs J S j S')
then obtain s where S: "S = (map snd (to_ns cs),s)" by (cases S, auto)
note pre = 1[unfolded S assert_cs.simps]
from pre(2) obtain s' where
ok: "assert_nsc j s = Inr s'" and S': "S' = (map snd (to_ns cs),s')"
by (auto split: sum.splits)
from pre(1)
have inv: "invariant_nsc (to_ns cs) J s" by simp
from assert_nsc_ok[OF inv ok]
show ?case unfolding invariant_cs.simps S' split by auto
next
case (2 cs J S j I)
then obtain s where S: "S = (map snd (to_ns cs), s)" by (cases S, auto)
note pre = 2[unfolded S assert_cs.simps]
from pre(2) have unsat: "assert_nsc j s = Unsat I"
by (auto split: sum.splits)
from pre(1) have inv: "invariant_nsc (to_ns cs) J s" by auto
from assert_nsc_unsat[OF inv unsat]
have "set I ⊆ insert j J" "minimal_unsat_core_ns (set I) (set (to_ns cs))"
by auto
from to_ns_unsat[OF this(2)] this(1)
show ?case by blast
next
case (3 cs J S S')
then show ?case using check_nsc_ok unfolding check_cs_def
by (cases S, auto split: prod.splits)
next
case (4 cs J S S' I)
then obtain s where S: "S = (map snd (to_ns cs),s)" by (cases S, auto)
note pre = 4[unfolded S check_cs_def]
from pre(2) obtain s' where unsat: "check_nsc s = (s',Some I)"
and S': "S' = (map snd (to_ns cs),s')"
by (auto split: prod.splits)
from pre(1) have inv: "invariant_nsc (to_ns cs) J s" by auto
from check_nsc_unsat[OF inv unsat]
have "set I ⊆ J" "weak_invariant_nsc (to_ns cs) J s'"
"minimal_unsat_core_ns (set I) (set (to_ns cs))"
unfolding minimal_unsat_core_ns_def by auto
from to_ns_unsat[OF this(3)] this(1,2)
show ?case unfolding S' using S by auto
next
case (5 cs)
show ?case unfolding init_cs_def Let_def using init_nsc by auto
next
case (6 cs J S v)
then obtain s where S: "S = (map snd (to_ns cs),s)" by (cases S, auto)
obtain w where w: "solution_nsc s = w" by auto
note pre = 6[unfolded S solution_cs.simps w Let_def]
from pre have
inv: "checked_nsc (to_ns cs) J s" and
v: "v = ⟨from_ns w (map snd (to_ns cs))⟩" by auto
from solution_nsc[OF inv w] have w: "(J, ⟨w⟩) ⊨⇩i⇩n⇩s⇩s set (to_ns cs)" .
from i_to_ns_sat[OF w]
show ?case unfolding v .
next
case (7 cs J S c K S' S'')
then show ?case using backtrack_nsc[of "to_ns cs" J]
by (cases S, cases S', cases S'', auto)
next
case (8 cs J S)
then show ?case using weak_invariant_nsc by (cases S, auto)
next
case (9 cs J S)
then show ?case using checked_invariant_nsc by (cases S, auto)
qed
end
subsection ‹Concrete Implementation›
subsubsection ‹Connecting all the locales›
global_interpretation Incremental_State_Ops_Simplex_Default:
Incremental_State_Ops_Simplex assert_bound_code init_state check_code
defines assert_s = Incremental_State_Ops_Simplex_Default.assert_s and
check_s = Incremental_State_Ops_Simplex_Default.check_s and
backtrack_s = Incremental_State_Ops_Simplex_Default.backtrack_s and
checkpoint_s = Incremental_State_Ops_Simplex_Default.checkpoint_s and
weak_invariant_s = Incremental_State_Ops_Simplex_Default.weak_invariant_s and
invariant_s = Incremental_State_Ops_Simplex_Default.invariant_s and
checked_s = Incremental_State_Ops_Simplex_Default.checked_s and
assert_all_s = Incremental_State_Ops_Simplex_Default.assert_all_s
..
lemma Incremental_State_Ops_Simplex_Default_assert_all_s[simp]:
"Incremental_State_Ops_Simplex_Default.assert_all_s = assert_all_s"
by (metis assert_all_s_def assert_s_def)
lemmas assert_all_s_code = Incremental_State_Ops_Simplex_Default.assert_all_s.simps[unfolded
Incremental_State_Ops_Simplex_Default_assert_all_s]
declare assert_all_s_code[code]