|
|
|
|
Quellcode-Bibliothek Simplex.thy
Sprache: Isabelle
|
|
(* Authors: F. Maric, M. Spasic, R. Thiemann *)
section ‹The Simplex Algorithm›
theory Simplex
imports
Linear_Poly_Maps
QDelta
Rel_Chain
Simplex_Algebra
"HOL-Library.Multiset"
"HOL-Library.RBT_Mapping"
"HOL-Library.Code_Target_Numeral"
begin
text‹Linear constraints are of the form ‹p ⋈ c›, where ‹p› is
homogenenous linear polynomial, ‹c› is a rational constant and ‹⋈ ∈
<, >, ≤, ≥, =}›. Their abstract syntax is given by the ‹constraint› type, and semantics is given by the relation ‹⊨c›, defined straightforwardly by primitive recursion over the
‹constraint› type. A set of constraints is satisfied,
by ‹⊨cs›, if all constraints are. There is also an indexed
‹⊨ics› which takes an explicit set of indices and then only
that these constraints are satisfied.›
datatype constraint = LT linear_poly rat
| GT linear_poly rat
| LEQ linear_poly rat
| GEQ linear_poly rat
| EQ linear_poly rat
text ‹Indexed constraints are just pairs of indices and constraints. Indices will be used
to identify constraints, e.g., to easily specify an unsatisfiable core by a list of indices.›
type_synonym 'i i_constraint = "'i × constraint"
abbreviation (input) restrict_to :: "'i set ==> ('i × 'a) set ==> 'a set" where
"restrict_to I xs ≡ snd ` (xs ∩ (I × UNIV))"
text ‹The operation @{const restrict_to} is used to select constraints for a given index set.›
abbreviation (input) flat :: "('i × 'a) set ==> 'a set" where
"flat xs ≡ snd ` xs"
text ‹The operation @{const flat} is used to drop indices from a set of indexed constraints.›
abbreviation (input) flat_list :: "('i × 'a) list ==> 'a list" where
"flat_list xs ≡ map snd xs"
primrec
satisfies_constraint :: "'a :: lrv valuation ==> constraint ==> bool" (infixl ‹⊨c› 100) where
"v ⊨c (LT l r) ⟷ (l{v}) < r *R 1"
| "v ⊨c GT l r ⟷ (l{v}) > r *R 1"
| "v ⊨c LEQ l r ⟷ (l{v}) ≤ r *R 1"
| "v ⊨c GEQ l r ⟷ (l{v}) ≥ r *R 1"
| "v ⊨c EQ l r ⟷ (l{v}) = r *R 1"
abbreviation satisfies_constraints :: "rat valuation ==> constraint set ==> bool" (infixl ‹⊨cs› 100) where
"v ⊨cs cs ≡ ∀ c ∈ cs. v ⊨c c"
lemma unsat_mono: assumes "¬ (∃ v. v ⊨cs cs)"
and "cs ⊆ ds"
shows "¬ (∃ v. v ⊨cs ds)"
using assms by auto
fun i_satisfies_cs (infixl ‹⊨ics› 100) where
"(I,v) ⊨ics cs ⟷ v ⊨cs restrict_to I cs"
definition distinct_indices :: "('i × 'c) list ==> bool" where
"distinct_indices as = (distinct (map fst as))"
lemma distinct_indicesD: "distinct_indices as ==> (i,x) ∈ set as ==> (i,y) ∈ set as ==> x = y"
unfolding distinct_indices_def by (rule eq_key_imp_eq_value)
text ‹For the unsat-core predicate we only demand minimality in case that the indices are distinct.
Otherwise, minimality does in general not hold. For instance, consider the input
constraints $c_1: x < 0$, $c_2: x > 2$ and $c_2: x < 1$ where the index $c_2$ occurs twice.
If the simplex-method first encounters constraint $c_1$, then it will detect that there is a conflict
between $c_1$ and the first $c_2$-constraint. Consequently, the index-set $\{c_1,c_2\}$ will be returned,
but this set is not minimal since $\{c_2\}$ is already unsatisfiable.›
definition minimal_unsat_core :: "'i set ==> 'i i_constraint list ==> bool" where
"minimal_unsat_core I ics = ((I ⊆ fst ` set ics) ∧ (¬ (∃ v. (I,v) ⊨ics set ics))
∧ (distinct_indices ics ⟶ (∀ J. J ⊂ I ⟶ (∃ v. (J,v) ⊨ics set ics))))"
subsection ‹Procedure Specification›
abbreviation (input) Unsat where "Unsat ≡ Inl"
abbreviation (input) Sat where "Sat ≡ Inr"
text‹The specification for the satisfiability check procedure is given by:›
locale Solve =
― ‹Decide if the given list of constraints is satisfiable. Return either
an unsat core, or a satisfying valuation.›
fixes solve :: "'i i_constraint list ==> 'i list + rat valuation"
― ‹If the status @{const Sat} is returned, then returned valuation
satisfies all constraints.›
assumes simplex_sat: "solve cs = Sat v ==> v ⊨cs flat (set cs)"
― ‹If the status @{const Unsat} is returned, then constraints are
unsatisfiable, i.e., an unsatisfiable core is returned.›
assumes simplex_unsat: "solve cs = Unsat I ==> minimal_unsat_core (set I) cs"
abbreviation (input) look where "look ≡ Mapping.lookup"
abbreviation (input) upd where "upd ≡ Mapping.update"
lemma look_upd: "look (upd k v m) = (look m)(k ↦ v)"
by (transfer, auto)
lemmas look_upd_simps[simp] = look_upd Mapping.lookup_empty
definition map2fun:: "(var, 'a :: zero) mapping ==> var ==> 'a" where
"map2fun v ≡ λx. case look v x of None ==> 0 | Some y ==> y"
syntax
"_map2fun" :: "(var, 'a) mapping ==> var ==> 'a" (‹⟨_⟩›)
syntax_consts
"_map2fun" == map2fun
translations
"⟨v⟩" == "CONST map2fun v"
lemma map2fun_def':
"⟨v⟩ x ≡ case Mapping.lookup v x of None ==> 0 | Some y ==> y"
by (auto simp add: map2fun_def)
text‹Note that the above specification requires returning a
(defined as a HOL function), which is not efficiently
. In order to enable more efficient data structures for
valuations, a refinement of this specification is needed
the function ‹solve› is replaced by the function ‹solve_exec› returning optional ‹(var, rat) mapping› instead
‹var ==> rat› function. This way, efficient data structures
representing mappings can be easily plugged-in during code
cite‹"florian-refinement"›. A conversion from the ‹mapping› datatype to HOL function is denoted by ‹⟨_⟩› and
by: @{thm map2fun_def'[no_vars]}.›
locale SolveExec =
fixes solve_exec :: "'i i_constraint list ==> 'i list + (var, rat) mapping"
assumes simplex_sat0: "solve_exec cs = Sat v ==> ⟨v⟩ ⊨cs flat (set cs)"
assumes simplex_unsat0: "solve_exec cs = Unsat I ==> minimal_unsat_core (set I) cs"
begin
definition solve where
"solve cs ≡ case solve_exec cs of Sat v ==> Sat ⟨v⟩ | Unsat c ==> Unsat c"
end
sublocale SolveExec < Solve solve
by (unfold_locales, insert simplex_sat0 simplex_unsat0,
auto simp: solve_def split: sum.splits)
subsection ‹Handling Strict Inequalities›
text‹The first step of the procedure is removing all equalities and
inequalities. Equalities can be easily rewritten to non-strict
. Removing strict inequalities can be done by replacing
list of constraints by a new one, formulated over an extension
‹ℚ'› of the space of rationals ‹ℚ›. ‹ℚ'› must
a structure of a linearly ordered vector space over ‹ℚ›
represented by the type class ‹lrv›) and must guarantee that
some non-strict constraints are satisfied in ‹ℚ'›, then
is a satisfying valuation for the original constraints in ‹ℚ›. Our final implementation uses the ‹ℚ\δ› space, defined in
cite‹"simplex-rad"› (basic idea is to replace ‹p < c› by ‹p ≤ c - δ› and ‹p > c› by ‹p ≥ c + δ› for a symbolic
‹δ›). So, all constraints are reduced to the form
‹p ⋈ b›, where ‹p› is a linear polynomial (still over
‹ℚ›), ‹b› is constant from ‹ℚ'› and ‹⋈
∈ {≤, ≥}›. The non-strict constraints are represented by the type
‹'a ns_constraint›, and their semantics is denoted by ‹⊨ns› and ‹⊨nss›. The indexed variant is ‹⊨inss›.›
datatype 'a ns_constraint = LEQ_ns linear_poly 'a | GEQ_ns linear_poly 'a
type_synonym ('i,'a) i_ns_constraint = "'i × 'a ns_constraint"
primrec satisfiable_ns_constraint :: "'a::lrv valuation ==> 'a ns_constraint ==> bool" (infixl ‹⊨ns› 100) where
"v ⊨ns LEQ_ns l r ⟷ l{v} ≤ r"
| "v ⊨ns GEQ_ns l r ⟷ l{v} ≥ r"
abbreviation satisfies_ns_constraints :: "'a::lrv valuation ==> 'a ns_constraint set ==> bool" (infixl ‹⊨nss › 100) where
"v ⊨nss cs ≡ ∀ c ∈ cs. v ⊨ns c"
fun i_satisfies_ns_constraints :: "'i set × 'a::lrv valuation ==> ('i,'a) i_ns_constraint set ==> bool" (infixl ‹⊨inss › 100) where
"(I,v) ⊨inss cs ⟷ v ⊨nss restrict_to I cs"
lemma i_satisfies_ns_constraints_mono:
"(I,v) ⊨inss cs ==> J ⊆ I ==> (J,v) ⊨inss cs"
by auto
primrec poly :: "'a ns_constraint ==> linear_poly" where
"poly (LEQ_ns p a) = p"
| "poly (GEQ_ns p a) = p"
primrec ns_constraint_const :: "'a ns_constraint ==> 'a" where
"ns_constraint_const (LEQ_ns p a) = a"
| "ns_constraint_const (GEQ_ns p a) = a"
definition distinct_indices_ns :: "('i,'a :: lrv) i_ns_constraint set ==> bool" where
"distinct_indices_ns ns = ((∀ n1 n2 i. (i,n1) ∈ ns ⟶ (i,n2) ∈ ns ⟶
poly n1 = poly n2 ∧ ns_constraint_const n1 = ns_constraint_const n2))"
definition minimal_unsat_core_ns :: "'i set ==> ('i,'a :: lrv) i_ns_constraint set ==> bool" where
"minimal_unsat_core_ns I cs = ((I ⊆ fst ` cs) ∧ (¬ (∃ v. (I,v) ⊨inss cs))
∧ (distinct_indices_ns cs ⟶ (∀ J ⊂ I. ∃ v. (J,v) ⊨inss cs)))"
text‹Specification of reduction of constraints to non-strict form is given by:›
locale To_ns =
― ‹Convert a constraint to an equisatisfiable non-strict constraint list.
The conversion must work for arbitrary subsets of constraints -- selected by some index set I --
in order to carry over unsat-cores and in order to support incremental simplex solving.›
fixes to_ns :: "'i i_constraint list ==> ('i,'a::lrv) i_ns_constraint list"
― ‹Convert the valuation that satisfies all non-strict constraints to the valuation that
satisfies all initial constraints.›
fixes from_ns :: "(var, 'a) mapping ==> 'a ns_constraint list ==> (var, rat) mapping"
assumes to_ns_unsat: "minimal_unsat_core_ns I (set (to_ns cs)) ==> minimal_unsat_core I cs"
assumes i_to_ns_sat: "(I,⟨v'⟩) ⊨inss set (to_ns cs) ==> (I,⟨from_ns v' (flat_list (to_ns cs))⟩) ⊨ics set cs"
assumes to_ns_indices: "fst ` set (to_ns cs) = fst ` set cs"
assumes distinct_cond: "distinct_indices cs ==> distinct_indices_ns (set (to_ns cs))"
begin
lemma to_ns_sat: "⟨v'⟩ ⊨nss flat (set (to_ns cs)) ==> ⟨from_ns v' (flat_list (to_ns cs))⟩ ⊨cs flat (set cs)"
using i_to_ns_sat[of UNIV v' cs] by auto
end
locale Solve_exec_ns =
fixes solve_exec_ns :: "('i,'a::lrv) i_ns_constraint list ==> 'i list + (var, 'a) mapping"
assumes simplex_ns_sat: "solve_exec_ns cs = Sat v ==> ⟨v⟩ ⊨nss flat (set cs)"
assumes simplex_ns_unsat: "solve_exec_ns cs = Unsat I ==> minimal_unsat_core_ns (set I) (set cs)"
text‹After the transformation, the procedure is reduced to solving
the non-strict constraints, implemented in the ‹solve_exec_ns› function having an analogous specification to the
‹solve› function. If ‹to_ns›, ‹from_ns› and
‹solve_exec_ns› are available, the ‹solve_exec›
can be easily defined and it can be easily shown that this
satisfies its specification (also analogous to ‹solve›).
›
locale SolveExec' = To_ns to_ns from_ns + Solve_exec_ns solve_exec_ns for
to_ns:: "'i i_constraint list ==> ('i,'a::lrv) i_ns_constraint list" and
from_ns :: "(var, 'a) mapping ==> 'a ns_constraint list ==> (var, rat) mapping" and
solve_exec_ns :: "('i,'a) i_ns_constraint list ==> 'i list + (var, 'a) mapping"
begin
definition solve_exec where
"solve_exec cs ≡ let cs' = to_ns cs in case solve_exec_ns cs'
of Sat v ==> Sat (from_ns v (flat_list cs'))
| Unsat is ==> Unsat is"
end
sublocale SolveExec' < SolveExec solve_exec
by (unfold_locales, insert simplex_ns_sat simplex_ns_unsat to_ns_sat to_ns_unsat,
(force simp: solve_exec_def Let_def split: sum.splits)+)
subsection ‹Preprocessing›
text‹The next step in the procedure rewrites a list of non-strict
into an equisatisfiable form consisting of a list of
equations (called the \emph{tableau}) and of a list of
emph{atoms} of the form ‹xi ⋈ bi› where ‹xi› is a
and ‹bi› is a constant (from the extension field). The
is straightforward and introduces auxiliary variables
linear polynomials occurring in the initial formula. For example,
‹[x1 + x2 ≤ b1, x1 + x2 ≥ b2, x2 ≥ b3]› can be transformed to
tableau ‹[x3 = x1 + x2]› and atoms ‹[x3 ≤ b1, x3 ≥
2, x2 ≥ b3]›.›
type_synonym eq = "var × linear_poly"
primrec lhs :: "eq ==> var" where "lhs (l, r) = l"
primrec rhs :: "eq ==> linear_poly" where "rhs (l, r) = r"
abbreviation rvars_eq :: "eq ==> var set" where
"rvars_eq eq ≡ vars (rhs eq)"
definition satisfies_eq :: "'a::rational_vector valuation ==> eq ==> bool" (infixl ‹⊨e› 100) where
"v ⊨e eq ≡ v (lhs eq) = (rhs eq){v}"
lemma satisfies_eq_iff: "v ⊨e (x, p) ≡ v x = p{v}"
by (simp add: satisfies_eq_def)
type_synonym tableau ="eq list"
definition satisfies_tableau ::"'a::rational_vector valuation ==> tableau ==> bool" (infixl ‹⊨t› 100) where
"v ⊨t t ≡ ∀ e ∈ set t. v ⊨e e"
definition lvars :: "tableau ==> var set" where
"lvars t = set (map lhs t)"
definition rvars :: "tableau ==> var set" where
"rvars t = ∪ (set (map rvars_eq t))"
abbreviation tvars where "tvars t ≡ lvars t ∪ rvars t"
text ‹The condition that the rhss are non-zero is required to obtain minimal unsatisfiable cores.
observe the problem with 0 as rhs, consider the tableau $x = 0$ in combination
atom $(A: x \leq 0)$ where then $(B: x \geq 1)$ is asserted.
this case, the unsat core would be computed as $\{A,B\}$, although already $\{B\}$ is unsatisfiable.›
definition normalized_tableau :: "tableau ==> bool" (‹△›) where
"normalized_tableau t ≡ distinct (map lhs t) ∧ lvars t ∩ rvars t = {} ∧ 0 ∉ rhs ` set t"
text‹Equations are of the form ‹x = p›, where ‹x› is
variable and ‹p› is a polynomial, and are represented by the
‹eq = var × linear_poly›. Semantics of equations is given
@{thm satisfies_eq_iff[no_vars]}. Tableau is represented as a list
equations, by the type ‹tableau = eq list›. Semantics for a
is given by @{thm satisfies_tableau_def[no_vars]}. Functions
‹lvars› and ‹rvars› return sets of variables appearing on
left hand side (lhs) and the right hand side (rhs) of a
. Lhs variables are called \emph{basic} while rhs variables are
\emph{non-basic} variables. A tableau ‹t› is
emph{normalized} (denoted by @{term "△ t"}) iff no variable occurs on
lhs of two equations in a tableau and if sets of lhs and rhs
are distinct.›
lemma normalized_tableau_unique_eq_for_lvar:
assumes "△ t"
shows "∀ x ∈ lvars t. ∃! p. (x, p) ∈ set t"
proof (safe)
fix x
assume "x ∈ lvars t"
then show "∃p. (x, p) ∈ set t"
unfolding lvars_def
by auto
next
fix x p1 p2
assume *: "(x, p1) ∈ set t" "(x, p2) ∈ set t"
then show "p1 = p2"
using ‹△ t›
unfolding normalized_tableau_def
by (force simp add: distinct_map inj_on_def)
qed
lemma recalc_tableau_lvars:
assumes "△ t"
shows "∀ v. ∃ v'. (∀ x ∈ rvars t. v x = v' x) ∧ v' ⊨t t"
proof
fix v
let ?v' = "λ x. if x ∈ lvars t then (THE p. (x, p) ∈ set t) { v } else v x"
show "∃ v'. (∀ x ∈ rvars t. v x = v' x) ∧ v' ⊨t t"
proof (rule_tac x="?v'" in exI, rule conjI)
show "∀x∈rvars t. v x = ?v' x"
using ‹△ t›
unfolding normalized_tableau_def
by auto
show "?v' ⊨t t"
unfolding satisfies_tableau_def satisfies_eq_def
proof
fix e
assume "e ∈ set t"
obtain l r where e: "e = (l,r)" by force
show "?v' (lhs e) = rhs e { ?v' }"
proof-
have "(lhs e, rhs e) ∈ set t"
using ‹e ∈ set t› e by auto
have "∃!p. (lhs e, p) ∈ set t"
using ‹△ t› normalized_tableau_unique_eq_for_lvar[of t]
using ‹e ∈ set t›
unfolding lvars_def
by auto
let ?p = "THE p. (lhs e, p) ∈ set t"
have "(lhs e, ?p) ∈ set t"
apply (rule theI')
using ‹∃!p. (lhs e, p) ∈ set t›
by auto
then have "?p = rhs e"
using ‹(lhs e, rhs e) ∈ set t›
using ‹∃!p. (lhs e, p) ∈ set t›
by auto
moreover
have "?v' (lhs e) = ?p { v }"
using ‹e ∈ set t›
unfolding lvars_def
by simp
moreover
have "rhs e { ?v' } = rhs e { v }"
apply (rule valuate_depend)
using ‹△ t› ‹e ∈ set t›
unfolding normalized_tableau_def
by (auto simp add: lvars_def rvars_def)
ultimately
show ?thesis
by auto
qed
qed
qed
qed
lemma tableau_perm:
assumes "lvars t1 = lvars t2" "rvars t1 = rvars t2"
"△ t1" "△ t2" "∧ v::'a::lrv valuation. v ⊨t t1 ⟷ v ⊨t t2"
shows "mset t1 = mset t2"
proof-
{
fix t1 t2
assume "lvars t1 = lvars t2" "rvars t1 = rvars t2"
"△ t1" "∧ v::'a::lrv valuation. v ⊨t t1 ⟷ v ⊨t t2"
have "set t1 ⊆ set t2"
proof (safe)
fix a b
assume "(a, b) ∈ set t1"
then have "a ∈ lvars t1"
unfolding lvars_def
by force
then have "a ∈ lvars t2"
using ‹lvars t1 = lvars t2›
by simp
then obtain b' where "(a, b') ∈ set t2"
unfolding lvars_def
by force
have "∀v::'a valuation. ∃v'. (∀x∈vars (b - b'). v' x = v x) ∧ (b - b') { v' } = 0"
proof
fix v::"'a valuation"
obtain v' where "v' ⊨t t1" "∀ x ∈ rvars t1. v x = v' x"
using recalc_tableau_lvars[of t1] ‹△ t1›
by auto
have "v' ⊨t t2"
using ‹v' ⊨t t1› ‹∧ v. v ⊨t t1 ⟷ v ⊨t t2›
by simp
have "b {v'} = b' {v'}"
using ‹(a, b) ∈ set t1› ‹v' ⊨t t1›
using ‹(a, b') ∈ set t2› ‹v' ⊨t t2›
unfolding satisfies_tableau_def satisfies_eq_def
by force
then have "(b - b') {v'} = 0"
using valuate_minus[of b b' v']
by auto
moreover
have "vars b ⊆ rvars t1" "vars b' ⊆ rvars t1"
using ‹(a, b) ∈ set t1› ‹(a, b') ∈ set t2› ‹rvars t1 = rvars t2›
unfolding rvars_def
by force+
then have "vars (b - b') ⊆ rvars t1"
using vars_minus[of b b']
by blast
then have "∀x∈vars (b - b'). v' x = v x"
using ‹∀ x ∈ rvars t1. v x = v' x›
by auto
ultimately
show "∃v'. (∀x∈vars (b - b'). v' x = v x) ∧ (b - b') { v' } = 0"
by auto
qed
then have "b = b'"
using all_val[of "b - b'"]
by simp
then show "(a, b) ∈ set t2"
using ‹(a, b') ∈ set t2›
by simp
qed
}
note * = this
have "set t1 = set t2"
using *[of t1 t2] *[of t2 t1]
using assms
by auto
moreover
have "distinct t1" "distinct t2"
using ‹△ t1› ‹△ t2›
unfolding normalized_tableau_def
by (auto simp add: distinct_map)
ultimately
show ?thesis
by (auto simp add: set_eq_iff_mset_eq_distinct)
qed
text‹Elementary atoms are represented by the type ‹'a atom›
semantics for atoms and sets of atoms is denoted by ‹⊨a› and
‹⊨as› and given by:
›
datatype 'a atom = Leq var 'a | Geq var 'a
primrec atom_var::"'a atom ==> var" where
"atom_var (Leq var a) = var"
| "atom_var (Geq var a) = var"
primrec atom_const::"'a atom ==> 'a" where
"atom_const (Leq var a) = a"
| "atom_const (Geq var a) = a"
primrec satisfies_atom :: "'a::linorder valuation ==> 'a atom ==> bool" (infixl ‹⊨a› 100) where
"v ⊨a Leq x c ⟷ v x ≤ c" | "v ⊨a Geq x c ⟷ v x ≥ c"
definition satisfies_atom_set :: "'a::linorder valuation ==> 'a atom set ==> bool" (infixl ‹⊨as› 100) where
"v ⊨as as ≡ ∀ a ∈ as. v ⊨a a"
definition satisfies_atom' :: "'a::linorder valuation ==> 'a atom ==> bool" (infixl ‹⊨ae› 100) where
"v ⊨ae a ⟷ v (atom_var a) = atom_const a"
lemma satisfies_atom'_stronger: "v ⊨ae a ==> v ⊨a a" by (cases a, auto simp: satisfies_atom'_def)
abbreviation satisfies_atom_set' :: "'a::linorder valuation ==> 'a atom set ==> bool" (infixl ‹⊨aes› 100) where
"v ⊨aes as ≡ ∀ a ∈ as. v ⊨ae a"
lemma satisfies_atom_set'_stronger: "v ⊨aes as ==> v ⊨as as"
using satisfies_atom'_stronger unfolding satisfies_atom_set_def by auto
text ‹There is also the indexed variant of an atom›
type_synonym ('i,'a) i_atom = "'i × 'a atom"
fun i_satisfies_atom_set :: "'i set × 'a::linorder valuation ==> ('i,'a) i_atom set ==> bool" (infixl ‹⊨ias› 100) where
"(I,v) ⊨ias as ⟷ v ⊨as restrict_to I as"
fun i_satisfies_atom_set' :: "'i set × 'a::linorder valuation ==> ('i,'a) i_atom set ==> bool" (infixl ‹⊨iaes› 100) where
"(I,v) ⊨iaes as ⟷ v ⊨aes restrict_to I as"
lemma i_satisfies_atom_set'_stronger: "Iv ⊨iaes as ==> Iv ⊨ias as"
using satisfies_atom_set'_stronger[of _ "snd Iv"] by (cases Iv, auto)
lemma satisifies_atom_restrict_to_Cons: "v ⊨as restrict_to I (set as) ==> (i ∈ I ==> v ⊨a a)
==> v ⊨as restrict_to I (set ((i,a) # as))"
unfolding satisfies_atom_set_def by auto
lemma satisfies_tableau_Cons: "v ⊨t t ==> v ⊨e e ==> v ⊨t (e # t)"
unfolding satisfies_tableau_def by auto
definition distinct_indices_atoms :: "('i,'a) i_atom set ==> bool" where
"distinct_indices_atoms as = (∀ i a b. (i,a) ∈ as ⟶ (i,b) ∈ as ⟶ atom_var a = atom_var b ∧ atom_const a = atom_const b)"
text‹
specification of the preprocessing function is given by:›
locale Preprocess = fixes preprocess::"('i,'a::lrv) i_ns_constraint list ==> tableau× ('i,'a) i_atom list
× ((var,'a) mapping ==> (var,'a) mapping) × 'i list"
assumes
― ‹The returned tableau is always normalized.›
preprocess_tableau_normalized: "preprocess cs = (t,as,trans_v,U) ==> △ t" and
― ‹Tableau and atoms are equisatisfiable with starting non-strict constraints.›
i_preprocess_sat: "∧ v. preprocess cs = (t,as,trans_v,U) ==> I ∩ set U = {} ==> (I,⟨v⟩) ⊨ias set as ==> ⟨v⟩ ⊨t t ==> (I,⟨trans_v v⟩) ⊨inss set cs" and
preprocess_unsat: "preprocess cs = (t, as,trans_v,U) ==> (I,v) ⊨inss set cs ==> ∃ v'. (I,v') ⊨ias set as ∧ v' ⊨t t" and
― ‹distinct indices on ns-constraints ensures distinct indices in atoms›
preprocess_distinct: "preprocess cs = (t, as,trans_v, U) ==> distinct_indices_ns (set cs) ==> distinct_indices_atoms (set as)" and
― ‹unsat indices›
preprocess_unsat_indices: "preprocess cs = (t, as,trans_v, U) ==> i ∈ set U ==> ¬ (∃ v. ({i},v) ⊨inss set cs)" and
― ‹preprocessing cannot introduce new indices›
preprocess_index: "preprocess cs = (t,as,trans_v, U) ==> fst ` set as ∪ set U ⊆ fst ` set cs"
begin
lemma preprocess_sat: "preprocess cs = (t,as,trans_v,U) ==> U = [] ==> ⟨v⟩ ⊨as flat (set as) ==> ⟨v⟩ ⊨t t ==> ⟨trans_v v⟩ ⊨nss flat (set cs)"
using i_preprocess_sat[of cs t as trans_v U UNIV v] by auto
end
definition minimal_unsat_core_tabl_atoms :: "'i set ==> tableau ==> ('i,'a::lrv) i_atom set ==> bool" where
"minimal_unsat_core_tabl_atoms I t as = ( I ⊆ fst ` as ∧ (¬ (∃ v. v ⊨t t ∧ (I,v) ⊨ias as)) ∧
(distinct_indices_atoms as ⟶ (∀ J ⊂ I. ∃ v. v ⊨t t ∧ (J,v) ⊨iaes as)))"
lemma minimal_unsat_core_tabl_atomsD: assumes "minimal_unsat_core_tabl_atoms I t as"
shows "I ⊆ fst ` as"
"¬ (∃ v. v ⊨t t ∧ (I,v) ⊨ias as)"
"distinct_indices_atoms as ==> J ⊂ I ==> ∃ v. v ⊨t t ∧ (J,v) ⊨iaes as"
using assms unfolding minimal_unsat_core_tabl_atoms_def by auto
locale AssertAll =
fixes assert_all :: "tableau ==> ('i,'a::lrv) i_atom list ==> 'i list + (var, 'a)mapping"
assumes assert_all_sat: "△ t ==> assert_all t as = Sat v ==> ⟨v⟩ ⊨t t ∧ ⟨v⟩ ⊨as flat (set as)"
assumes assert_all_unsat: "△ t ==> assert_all t as = Unsat I ==> minimal_unsat_core_tabl_atoms (set I) t (set as)"
text‹Once the preprocessing is done and tableau and atoms are
, their satisfiability is checked by the
‹assert_all› function. Its precondition is that the starting
is normalized, and its specification is analogue to the one for the
‹solve› function. If ‹preprocess› and ‹assert_all›
available, the ‹solve_exec_ns› can be defined, and it
easily be shown that this definition satisfies the specification.›
locale Solve_exec_ns' = Preprocess preprocess + AssertAll assert_all for
preprocess:: "('i,'a::lrv) i_ns_constraint list ==> tableau × ('i,'a) i_atom list × ((var,'a)mapping ==> (var,'a)mapping) × 'i list" and
assert_all :: "tableau ==> ('i,'a::lrv) i_atom list ==> 'i list + (var, 'a) mapping"
begin
definition solve_exec_ns where
"solve_exec_ns s ≡
case preprocess s of (t,as,trans_v,ui) ==>
(case ui of i # _ ==> Inl [i] | _ ==>
(case assert_all t as of Inl I ==> Inl I | Inr v ==> Inr (trans_v v))) "
end
context Preprocess
begin
lemma preprocess_unsat_index: assumes prep: "preprocess cs = (t,as,trans_v,ui)"
and i: "i ∈ set ui"
shows "minimal_unsat_core_ns {i} (set cs)"
proof -
from preprocess_index[OF prep] have "set ui ⊆ fst ` set cs" by auto
with i have i': "i ∈ fst ` set cs" by auto
from preprocess_unsat_indices[OF prep i]
show ?thesis unfolding minimal_unsat_core_ns_def using i' by auto
qed
lemma preprocess_minimal_unsat_core: assumes prep: "preprocess cs = (t,as,trans_v,ui)"
and unsat: "minimal_unsat_core_tabl_atoms I t (set as)"
and inter: "I ∩ set ui = {}"
shows "minimal_unsat_core_ns I (set cs)"
proof -
from preprocess_tableau_normalized[OF prep]
have t: "△ t" .
from preprocess_index[OF prep] have index: "fst ` set as ∪ set ui ⊆ fst ` set cs" by auto
from minimal_unsat_core_tabl_atomsD(1,2)[OF unsat] preprocess_unsat[OF prep, of I]
have 1: "I ⊆ fst ` set as" "¬ (∃ v. (I, v) ⊨inss set cs)" by force+
show "minimal_unsat_core_ns I (set cs)" unfolding minimal_unsat_core_ns_def
proof (intro conjI impI allI 1(2))
show "I ⊆ fst ` set cs" using 1 index by auto
fix J
assume "distinct_indices_ns (set cs)" "J ⊂ I"
with preprocess_distinct[OF prep]
have "distinct_indices_atoms (set as)" "J ⊂ I" by auto
from minimal_unsat_core_tabl_atomsD(3)[OF unsat this]
obtain v where model: "v ⊨t t" "(J, v) ⊨iaes set as" by auto
from i_satisfies_atom_set'_stronger[OF model(2)]
have model': "(J, v) ⊨ias set as" .
define w where "w = Mapping.Mapping (λ x. Some (v x))"
have "v = ⟨w⟩" unfolding w_def map2fun_def
by (intro ext, transfer, auto)
with model model' have "⟨w⟩ ⊨t t" "(J, ⟨w⟩) ⊨ias set as" by auto
from i_preprocess_sat[OF prep _ this(2,1)] ‹J ⊂ I› inter
have "(J, ⟨trans_v w⟩) ⊨inss set cs" by auto
then show "∃ w. (J, w) ⊨inss set cs" by auto
qed
qed
end
sublocale Solve_exec_ns' < Solve_exec_ns solve_exec_ns
proof
fix cs
obtain t as trans_v ui where prep: "preprocess cs = (t,as,trans_v,ui)" by (cases "preprocess cs")
from preprocess_tableau_normalized[OF prep]
have t: "△ t" .
from preprocess_index[OF prep] have index: "fst ` set as ∪ set ui ⊆ fst ` set cs" by auto
note solve = solve_exec_ns_def[of cs, unfolded prep split]
{
fix v
assume "solve_exec_ns cs = Sat v"
from this[unfolded solve] t assert_all_sat[OF t] preprocess_sat[OF prep]
show " ⟨v⟩ ⊨nss flat (set cs)" by (auto split: sum.splits list.splits)
}
{
fix I
assume res: "solve_exec_ns cs = Unsat I"
show "minimal_unsat_core_ns (set I) (set cs)"
proof (cases ui)
case (Cons i uis)
hence I: "I = [i]" using res[unfolded solve] by auto
from preprocess_unsat_index[OF prep, of i] I Cons index show ?thesis by auto
next
case Nil
from res[unfolded solve Nil] have assert: "assert_all t as = Unsat I"
by (auto split: sum.splits)
from assert_all_unsat[OF t assert]
have "minimal_unsat_core_tabl_atoms (set I) t (set as)" .
from preprocess_minimal_unsat_core[OF prep this] Nil
show "minimal_unsat_core_ns (set I) (set cs)" by simp
qed
}
qed
subsection‹Incrementally Asserting Atoms›
text‹The function @{term assert_all} can be implemented by
asserting one by one atom from the given list of atoms.
›
type_synonym 'a bounds = "var ⇀ 'a"
text‹Asserted atoms will be stored in a form of \emph{bounds} for a
variable. Bounds are of the form ‹li ≤ xi ≤ ui›, where
‹li› and ‹ui› and are either scalars or $\pm
infty$. Each time a new atom is asserted, a bound for the
variable is updated (checking for conflict with the
bounds). Since bounds for a variable can be either finite or
\pm \infty$, they are represented by (partial) maps from variables to
(‹'a bounds = var ⇀ 'a›). Upper and lower bounds are
separately. Infinite bounds map to @{term None} and this
reflected in the semantics:
begin{small}
‹c ≥ub b ⟷ case b of None ==> False | Some b' ==> c ≥ b'›
‹c ≤ub b ⟷ case b of None ==> True | Some b' ==> c ≤ b'›
end{small}
noindent Strict comparisons, and comparisons with lower bounds are performed similarly.
›
abbreviation (input) le where
"le lt x y ≡ lt x y ∨ x = y"
definition geub (‹⊵ub›) where
"⊵ub lt c b ≡ case b of None ==> False | Some b' ==> le lt b' c"
definition gtub (‹⊳ub›) where
"⊳ub lt c b ≡ case b of None ==> False | Some b' ==> lt b' c"
definition leub (‹⊴ub›) where
"⊴ub lt c b ≡ case b of None ==> True | Some b' ==> le lt c b'"
definition ltub (‹⊲ub›) where
"⊲ub lt c b ≡ case b of None ==> True | Some b' ==> lt c b'"
definition lelb (‹⊴lb›) where
"⊴lb lt c b ≡ case b of None ==> False | Some b' ==> le lt c b'"
definition ltlb (‹⊲lb›) where
"⊲lb lt c b ≡ case b of None ==> False | Some b' ==> lt c b'"
definition gelb (‹⊵lb›) where
"⊵lb lt c b ≡ case b of None ==> True | Some b' ==> le lt b' c"
definition gtlb (‹⊳lb›) where
"⊳lb lt c b ≡ case b of None ==> True | Some b' ==> lt b' c"
definition ge_ubound :: "'a::linorder ==> 'a option ==> bool" (infixl ‹≥ub› 100) where
"c ≥ub b = ⊵ub (<) c b"
definition gt_ubound :: "'a::linorder ==> 'a option ==> bool" (infixl ‹>ub› 100) where
"c >ub b = ⊳ub (<) c b"
definition le_ubound :: "'a::linorder ==> 'a option ==> bool" (infixl ‹≤ub› 100) where
"c ≤ub b = ⊴ub (<) c b"
definition lt_ubound :: "'a::linorder ==> 'a option ==> bool" (infixl ‹<\<^sub>ub› 100) where
"c <ub b = ⊲ub (<) c b"
definition le_lbound :: "'a::linorder ==> 'a option ==> bool" (infixl ‹≤lb› 100) where
"c ≤lb b = ⊴lb (<) c b"
definition lt_lbound :: "'a::linorder ==> 'a option ==> bool" (infixl ‹<\<^sub>lb› 100) where
"c <lb b = ⊲lb (<) c b"
definition ge_lbound :: "'a::linorder ==> 'a option ==> bool" (infixl ‹≥lb› 100) where
"c ≥lb b = ⊵lb (<) c b"
definition gt_lbound :: "'a::linorder ==> 'a option ==> bool" (infixl ‹>lb› 100) where
"c >lb b = ⊳lb (<) c b"
lemmas bound_compare'_defs =
geub_def gtub_def leub_def ltub_def
gelb_def gtlb_def lelb_def ltlb_def
lemmas bound_compare''_defs =
ge_ubound_def gt_ubound_def le_ubound_def lt_ubound_def
le_lbound_def lt_lbound_def ge_lbound_def gt_lbound_def
lemmas bound_compare_defs = bound_compare'_defs bound_compare''_defs
lemma opposite_dir [simp]:
"⊴lb (>) a b = ⊵ub (<) a b"
"⊴ub (>) a b = ⊵lb (<) a b"
"⊵lb (>) a b = ⊴ub (<) a b"
"⊵ub (>) a b = ⊴lb (<) a b"
"⊲lb (>) a b = ⊳ub (<) a b"
"⊲ub (>) a b = ⊳lb (<) a b"
"⊳lb (>) a b = ⊲ub (<) a b"
"⊳ub (>) a b = ⊲lb (<) a b"
by (case_tac[!] b) (auto simp add: bound_compare'_defs)
(* Auxiliary lemmas about bound comparison *)
lemma [simp]: "¬ c ≥ub None " "¬ c ≤lb None"
by (auto simp add: bound_compare_defs)
lemma neg_bounds_compare:
"(¬ (c ≥ub b)) ==> c <ub b" "(¬ (c ≤ub b)) ==> c >ub b"
"(¬ (c >ub b)) ==> c ≤ub b" "(¬ (c <ub b)) ==> c ≥ub b"
"(¬ (c ≤lb b)) ==> c >lb b" "(¬ (c ≥lb b)) ==> c <lb b"
"(¬ (c <lb b)) ==> c ≥lb b" "(¬ (c >lb b)) ==> c ≤lb b"
by (case_tac[!] b) (auto simp add: bound_compare_defs)
lemma bounds_compare_contradictory [simp]:
"[c ≥ub b; c <ub b] ==> False" "[c ≤ub b; c >ub b] ==> False"
"[c >ub b; c ≤ub b] ==> False" "[c <ub b; c ≥ub b] ==> False"
"[c ≤lb b; c >lb b] ==> False" "[c ≥lb b; c <lb b] ==> False"
"[c <lb b; c ≥lb b] ==> False" "[c >lb b; c ≤lb b] ==> False"
by (case_tac[!] b) (auto simp add: bound_compare_defs)
lemma compare_strict_nonstrict:
"x <ub b ==> x ≤ub b"
"x >ub b ==> x ≥ub b"
"x <lb b ==> x ≤lb b"
"x >lb b ==> x ≥lb b"
by (case_tac[!] b) (auto simp add: bound_compare_defs)
lemma [simp]:
"[ x ≤ c; c <ub b ] ==> x <ub b"
"[ x < c; c ≤ub b ] ==> x <ub b"
"[ x ≤ c; c ≤ub b ] ==> x ≤ub b"
"[ x ≥ c; c >lb b ] ==> x >lb b"
"[ x > c; c ≥lb b ] ==> x >lb b"
"[ x ≥ c; c ≥lb b ] ==> x ≥lb b"
by (case_tac[!] b) (auto simp add: bound_compare_defs)
lemma bounds_lg [simp]:
"[ c >ub b; x ≤ub b] ==> x < c"
"[ c ≥ub b; x <ub b] ==> x < c"
"[ c ≥ub b; x ≤ub b] ==> x ≤ c"
"[ c <lb b; x ≥lb b] ==> x > c"
"[ c ≤lb b; x >lb b] ==> x > c"
"[ c ≤lb b; x ≥lb b] ==> x ≥ c"
by (case_tac[!] b) (auto simp add: bound_compare_defs)
lemma bounds_compare_Some [simp]:
"x ≤ub Some c ⟷ x ≤ c" "x ≥ub Some c ⟷ x ≥ c"
"x <ub Some c ⟷ x < c" "x >ub Some c ⟷ x > c"
"x ≥lb Some c ⟷ x ≥ c" "x ≤lb Some c ⟷ x ≤ c"
"x >lb Some c ⟷ x > c" "x <lb Some c ⟷ x < c"
by (auto simp add: bound_compare_defs)
fun in_bounds where
"in_bounds x v (lb, ub) = (v x ≥lb lb x ∧ v x ≤ub ub x)"
fun satisfies_bounds :: "'a::linorder valuation ==> 'a bounds × 'a bounds ==> bool" (infixl ‹⊨b› 100) where
"v ⊨b b ⟷ (∀ x. in_bounds x v b)"
declare satisfies_bounds.simps [simp del]
lemma satisfies_bounds_iff:
"v ⊨b (lb, ub) ⟷ (∀ x. v x ≥lb lb x ∧ v x ≤ub ub x)"
by (auto simp add: satisfies_bounds.simps)
lemma not_in_bounds:
"¬ (in_bounds x v (lb, ub)) = (v x <lb lb x ∨ v x >ub ub x)"
using bounds_compare_contradictory(7)
using bounds_compare_contradictory(2)
using neg_bounds_compare(7)[of "v x" "lb x"]
using neg_bounds_compare(2)[of "v x" "ub x"]
by auto
fun atoms_equiv_bounds :: "'a::linorder atom set ==> 'a bounds × 'a bounds ==> bool" (infixl ‹≐› 100) where
"as ≐ (lb, ub) ⟷ (∀ v. v ⊨as as ⟷ v ⊨b (lb, ub))"
declare atoms_equiv_bounds.simps [simp del]
lemma atoms_equiv_bounds_simps:
"as ≐ (lb, ub) ≡ ∀ v. v ⊨as as ⟷ v ⊨b (lb, ub)"
by (simp add: atoms_equiv_bounds.simps)
text‹A valuation satisfies bounds iff the value of each variable
both its lower and upper bound, i.e, @{thm
[no_vars]}. Asserted atoms are precisely encoded
the current bounds in a state (denoted by ‹≐›) if every
satisfies them iff it satisfies the bounds, i.e.,
{thm atoms_equiv_bounds_simps[no_vars, iff]}.›
text‹The procedure also keeps track of a valuation that is a
solution. Whenever a new atom is asserted, it is checked
the valuation is still satisfying. If not, the procedure tries
fix that by changing it and changing the tableau if necessary (but
that it remains equivalent to the initial tableau).›
text‹Therefore, the state of the procedure stores the tableau
denoted by ‹T›), lower and upper bounds (denoted by ‹Bl› and ‹Bu›, and ordered pair of lower and upper bounds
by ‹B›), candidate solution (denoted by ‹V›)
a flag (denoted by ‹U›) indicating if unsatisfiability has
detected so far:›
text‹Since we also need to now about the indices of atoms, actually,
the bounds are also indexed, and in addition to the flag for unsatisfiability,
we also store an optional unsat core.›
type_synonym 'i bound_index = "var ==> 'i"
type_synonym ('i,'a) bounds_index = "(var, ('i × 'a))mapping"
datatype ('i,'a) state = State
(T: "tableau")
(Bil: "('i,'a) bounds_index")
(Biu: "('i,'a) bounds_index")
(V: "(var, 'a) mapping")
(U: bool)
(Uc: "'i list option")
definition indexl :: "('i,'a) state ==> 'i bound_index" (‹Il›) where
"Il s = (fst o the) o look (Bil s)"
definition boundsl :: "('i,'a) state ==> 'a bounds" (‹Bl›) where
"Bl s = map_option snd o look (Bil s)"
definition indexu :: "('i,'a) state ==> 'i bound_index" (‹Iu›) where
"Iu s = (fst o the) o look (Biu s)"
definition boundsu :: "('i,'a) state ==> 'a bounds" (‹Bu›) where
"Bu s = map_option snd o look (Biu s)"
abbreviation BoundsIndicesMap (‹Bi›) where "Bi s ≡ (Bil s, Biu s)"
abbreviation Bounds :: "('i,'a) state ==> 'a bounds × 'a bounds" (‹B›) where "B s ≡ (Bl s, Bu s)"
abbreviation Indices :: "('i,'a) state ==> 'i bound_index × 'i bound_index" (‹I›) where "I s ≡ (Il s, Iu s)"
abbreviation BoundsIndices :: "('i,'a) state ==> ('a bounds × 'a bounds) × ('i bound_index × 'i bound_index)" (‹BI›)
where "BI s ≡ (B s, I s)"
fun satisfies_bounds_index :: "'i set × 'a::lrv valuation ==> ('a bounds × 'a bounds) ×
('i bound_index × 'i bound_index) ==> bool" (infixl ‹⊨ib› 100) where
"(I,v) ⊨ib ((BL,BU),(IL,IU)) ⟷ (
(∀ x c. BL x = Some c ⟶ IL x ∈ I ⟶ v x ≥ c)
∧ (∀ x c. BU x = Some c ⟶ IU x ∈ I ⟶ v x ≤ c))"
declare satisfies_bounds_index.simps[simp del]
fun satisfies_bounds_index' :: "'i set × 'a::lrv valuation ==> ('a bounds × 'a bounds) ×
('i bound_index × 'i bound_index) ==> bool" (infixl ‹⊨ibe› 100) where
"(I,v) ⊨ibe ((BL,BU),(IL,IU)) ⟷ (
(∀ x c. BL x = Some c ⟶ IL x ∈ I ⟶ v x = c)
∧ (∀ x c. BU x = Some c ⟶ IU x ∈ I ⟶ v x = c))"
declare satisfies_bounds_index'.simps[simp del]
fun atoms_imply_bounds_index :: "('i,'a::lrv) i_atom set ==> ('a bounds × 'a bounds) × ('i bound_index × 'i bound_index)
==> bool" (infixl ‹⊨i› 100) where
"as ⊨i bi ⟷ (∀ I v. (I,v) ⊨ias as ⟶ (I,v) ⊨ib bi)"
declare atoms_imply_bounds_index.simps[simp del]
lemma i_satisfies_atom_set_mono: "as ⊆ as' ==> v ⊨ias as' ==> v ⊨ias as"
by (cases v, auto simp: satisfies_atom_set_def)
lemma atoms_imply_bounds_index_mono: "as ⊆ as' ==> as ⊨i bi ==> as' ⊨i bi"
unfolding atoms_imply_bounds_index.simps using i_satisfies_atom_set_mono by blast
definition satisfies_state :: "'a::lrv valuation ==> ('i,'a) state ==> bool" (infixl ‹⊨s› 100) where
"v ⊨s s ≡ v ⊨b B s ∧ v ⊨t T s"
definition curr_val_satisfies_state :: "('i,'a::lrv) state ==> bool" (‹⊨›) where
"⊨ s ≡ ⟨V s⟩ ⊨s s"
fun satisfies_state_index :: "'i set × 'a::lrv valuation ==> ('i,'a) state ==> bool" (infixl ‹⊨is› 100) where
"(I,v) ⊨is s ⟷ (v ⊨t T s ∧ (I,v) ⊨ib BI s)"
declare satisfies_state_index.simps[simp del]
fun satisfies_state_index' :: "'i set × 'a::lrv valuation ==> ('i,'a) state ==> bool" (infixl ‹⊨ise› 100) where
"(I,v) ⊨ise s ⟷ (v ⊨t T s ∧ (I,v) ⊨ibe BI s)"
declare satisfies_state_index'.simps[simp del]
definition indices_state :: "('i,'a)state ==> 'i set" where
"indices_state s = { i. ∃ x b. look (Bil s) x = Some (i,b) ∨ look (Biu s) x = Some (i,b)}"
text ‹distinctness requires that for each index $i$, there is at most one variable $x$ and bound
$b$ such that $x \leq b$ or $x \geq b$ or both are enforced.›
definition distinct_indices_state :: "('i,'a)state ==> bool" where
"distinct_indices_state s = (∀ i x b x' b'.
((look (Bil s) x = Some (i,b) ∨ look (Biu s) x = Some (i,b)) ⟶
(look (Bil s) x' = Some (i,b') ∨ look (Biu s) x' = Some (i,b')) ⟶
(x = x' ∧ b = b')))"
lemma distinct_indices_stateD: assumes "distinct_indices_state s"
shows "look (Bil s) x = Some (i,b) ∨ look (Biu s) x = Some (i,b) ==> look (Bil s) x' = Some (i,b') ∨ look (Biu s) x' = Some (i,b')
==> x = x' ∧ b = b'"
using assms unfolding distinct_indices_state_def by blast+
definition unsat_state_core :: "('i,'a::lrv) state ==> bool" where
"unsat_state_core s = (set (the (Uc s)) ⊆ indices_state s ∧ (¬ (∃ v. (set (the (Uc s)),v) ⊨is s)))"
definition subsets_sat_core :: "('i,'a::lrv) state ==> bool" where
"subsets_sat_core s = ((∀ I. I ⊂ set (the (Uc s)) ⟶ (∃ v. (I,v) ⊨ise s)))"
definition minimal_unsat_state_core :: "('i,'a::lrv) state ==> bool" where
"minimal_unsat_state_core s = (unsat_state_core s ∧ (distinct_indices_state s ⟶ subsets_sat_core s))"
lemma minimal_unsat_core_tabl_atoms_mono: assumes sub: "as ⊆ bs"
and unsat: "minimal_unsat_core_tabl_atoms I t as"
shows "minimal_unsat_core_tabl_atoms I t bs"
unfolding minimal_unsat_core_tabl_atoms_def
proof (intro conjI impI allI)
note min = unsat[unfolded minimal_unsat_core_tabl_atoms_def]
from min have I: "I ⊆ fst ` as" by blast
with sub show "I ⊆ fst ` bs" by blast
from min have "(∄v. v ⊨t t ∧ (I, v) ⊨ias as)" by blast
with i_satisfies_atom_set_mono[OF sub]
show "(∄v. v ⊨t t ∧ (I, v) ⊨ias bs)" by blast
fix J
assume J: "J ⊂ I" and dist_bs: "distinct_indices_atoms bs"
hence dist: "distinct_indices_atoms as"
using sub unfolding distinct_indices_atoms_def by blast
from min dist J obtain v where v: "v ⊨t t" "(J, v) ⊨iaes as" by blast
have "(J, v) ⊨iaes bs"
unfolding i_satisfies_atom_set'.simps
proof (intro ballI)
fix a
assume "a ∈ snd ` (bs ∩ J × UNIV)"
then obtain i where ia: "(i,a) ∈ bs" and i: "i ∈ J"
by force
with J have "i ∈ I" by auto
with I obtain b where ib: "(i,b) ∈ as" by force
with sub have ib': "(i,b) ∈ bs" by auto
from dist_bs[unfolded distinct_indices_atoms_def, rule_format, OF ia ib']
have id: "atom_var a = atom_var b" "atom_const a = atom_const b" by auto
from v(2)[unfolded i_satisfies_atom_set'.simps] i ib
have "v ⊨ae b" by force
thus "v ⊨ae a" using id unfolding satisfies_atom'_def by auto
qed
with v show "∃v. v ⊨t t ∧ (J, v) ⊨iaes bs" by blast
qed
lemma state_satisfies_index: assumes "v ⊨s s"
shows "(I,v) ⊨is s"
unfolding satisfies_state_index.simps satisfies_bounds_index.simps
proof (intro conjI impI allI)
fix x c
from assms[unfolded satisfies_state_def satisfies_bounds.simps, simplified]
have "v ⊨t T s" and bnd: "v x ≥lb Bl s x" "v x ≤ub Bu s x" by auto
show "v ⊨t T s" by fact
show "Bl s x = Some c ==> Il s x ∈ I ==> c ≤ v x"
using bnd(1) by auto
show "Bu s x = Some c ==> Iu s x ∈ I ==> v x ≤ c"
using bnd(2) by auto
qed
lemma unsat_state_core_unsat: "unsat_state_core s ==> ¬ (∃ v. v ⊨s s)"
unfolding unsat_state_core_def using state_satisfies_index by blast
definition tableau_valuated (‹∇›) where
"∇ s ≡ ∀ x ∈ tvars (T s). Mapping.lookup (V s) x ≠ None"
definition index_valid where
"index_valid as (s :: ('i,'a) state) = (∀ x b i.
(look (Bil s) x = Some (i,b) ⟶ ((i, Geq x b) ∈ as))
∧ (look (Biu s) x = Some (i,b) ⟶ ((i, Leq x b) ∈ as)))"
lemma index_valid_indices_state: "index_valid as s ==> indices_state s ⊆ fst ` as"
unfolding index_valid_def indices_state_def by force
lemma index_valid_mono: "as ⊆ bs ==> index_valid as s ==> index_valid bs s"
unfolding index_valid_def by blast
lemma index_valid_distinct_indices: assumes "index_valid as s"
and "distinct_indices_atoms as"
shows "distinct_indices_state s"
unfolding distinct_indices_state_def
proof (intro allI impI, goal_cases)
case (1 i x b y c)
note valid = assms(1)[unfolded index_valid_def, rule_format]
from 1(1) valid[of x i b] have "(i, Geq x b) ∈ as ∨ (i, Leq x b) ∈ as" by auto
then obtain a where a: "(i,a) ∈ as" "atom_var a = x" "atom_const a = b" by auto
from 1(2) valid[of y i c] have y: "(i, Geq y c) ∈ as ∨ (i, Leq y c) ∈ as" by auto
then obtain a' where a': "(i,a') ∈ as" "atom_var a' = y" "atom_const a' = c" by auto
from assms(2)[unfolded distinct_indices_atoms_def, rule_format, OF a(1) a'(1)]
show ?case using a a' by auto
qed
text‹To be a solution of the initial problem, a valuation should
the initial tableau and list of atoms. Since tableau is
only by equivalency preserving transformations and asserted
are encoded in the bounds, a valuation is a solution if it
both the tableau and the bounds in the final state (when all
have been asserted). So, a valuation ‹v› satisfies a state
‹s› (denoted by ‹⊨s›) if it satisfies the tableau and
bounds, i.e., @{thm satisfies_state_def [no_vars]}. Since ‹V› should be a candidate solution, it should satisfy the state
unless the ‹U› flag is raised). This is denoted by ‹⊨ s›
defined by @{thm curr_val_satisfies_state_def[no_vars]}. ‹∇
› will denote that all variables of ‹T s› are explicitly
in ‹V s›.›
definition updateBI where
[simp]: "updateBI field_update i x c s = field_update (upd x (i,c)) s"
fun Biu_update where
"Biu_update up (State T BIL BIU V U UC) = State T BIL (up BIU) V U UC"
fun Bil_update where
"Bil_update up (State T BIL BIU V U UC) = State T (up BIL) BIU V U UC"
fun V_update where
"V_update V (State T BIL BIU V_old U UC) = State T BIL BIU V U UC"
fun T_update where
"T_update T (State T_old BIL BIU V U UC) = State T BIL BIU V U UC"
lemma update_simps[simp]:
"Biu (Biu_update up s) = up (Biu s)"
"Bil (Biu_update up s) = Bil s"
"T (Biu_update up s) = T s"
"V (Biu_update up s) = V s"
"U (Biu_update up s) = U s"
"Uc (Biu_update up s) = Uc s"
"Bil (Bil_update up s) = up (Bil s)"
"Biu (Bil_update up s) = Biu s"
"T (Bil_update up s) = T s"
"V (Bil_update up s) = V s"
"U (Bil_update up s) = U s"
"Uc (Bil_update up s) = Uc s"
"V (V_update V s) = V"
"Bil (V_update V s) = Bil s"
"Biu (V_update V s) = Biu s"
"T (V_update V s) = T s"
"U (V_update V s) = U s"
"Uc (V_update V s) = Uc s"
"T (T_update T s) = T"
"Bil (T_update T s) = Bil s"
"Biu (T_update T s) = Biu s"
"V (T_update T s) = V s"
"U (T_update T s) = U s"
"Uc (T_update T s) = Uc s"
by (atomize(full), cases s, auto)
declare
Biu_update.simps[simp del]
Bil_update.simps[simp del]
fun set_unsat :: "'i list ==> ('i,'a) state ==> ('i,'a) state" where
"set_unsat I (State T BIL BIU V U UC) = State T BIL BIU V True (Some (remdups I))"
lemma set_unsat_simps[simp]: "Bil (set_unsat I s) = Bil s"
"Biu (set_unsat I s) = Biu s"
"T (set_unsat I s) = T s"
"V (set_unsat I s) = V s"
"U (set_unsat I s) = True"
"Uc (set_unsat I s) = Some (remdups I)"
by (atomize(full), cases s, auto)
datatype ('i,'a) Direction = Direction
(lt: "'a::linorder ==> 'a ==> bool")
(LBI: "('i,'a) state ==> ('i,'a) bounds_index")
(UBI: "('i,'a) state ==> ('i,'a) bounds_index")
(LB: "('i,'a) state ==> 'a bounds")
(UB: "('i,'a) state ==> 'a bounds")
(LI: "('i,'a) state ==> 'i bound_index")
(UI: "('i,'a) state ==> 'i bound_index")
(UBI_upd: "(('i,'a) bounds_index ==> ('i,'a) bounds_index) ==> ('i,'a) state ==> ('i,'a) state")
(LE: "var ==> 'a ==> 'a atom")
(GE: "var ==> 'a ==> 'a atom")
(le_rat: "rat ==> rat ==> bool")
definition Positive where
[simp]: "Positive ≡ Direction (<) Bil Biu Bl Bu Il Iu Biu_update Leq Geq (≤)"
definition Negative where
[simp]: "Negative ≡ Direction (>) Biu Bil Bu Bl Iu Il Bil_update Geq Leq (≥)"
text‹Assuming that the ‹U› flag and the current valuation
‹V› in the final state determine the solution of a problem, the
‹assert_all› function can be reduced to the ‹assert_all_state›
that operates on the states:
{text[display] "assert_all t as ≡ let s = assert_all_state t as in
if (U s) then (False, None) else (True, Some (V s))" }
›
text‹Specification for the ‹assert_all_state› can be directly
from the specification of ‹assert_all›, and it describes
connection between the valuation in the final state and the
tableau and atoms. However, we will make an additional
step and give stronger assumptions about the ‹assert_all_state› function that describes the connection between
initial tableau and atoms with the tableau and bounds in the final
.›
locale AssertAllState = fixes assert_all_state::"tableau ==> ('i,'a::lrv) i_atom list ==> ('i,'a) state"
assumes
― ‹The final and the initial tableau are equivalent.›
assert_all_state_tableau_equiv: "△ t ==> assert_all_state t as = s' ==> (v::'a valuation) ⊨t t ⟷ v ⊨t T s'" and
― ‹If @{term U} is not raised, then the valuation in the
state satisfies its tableau and its bounds (that are, in this
, equivalent to the set of all asserted bounds).›
assert_all_state_sat: "△ t ==> assert_all_state t as = s' ==> ¬ U s' ==> ⊨ s'" and
assert_all_state_sat_atoms_equiv_bounds: "△ t ==> assert_all_state t as = s' ==> ¬ U s' ==> flat (set as) ≐ B s'" and
― ‹If @{term U} is raised, then there is no valuation
satisfying the tableau and the bounds in the final state (that are,
in this case, equivalent to a subset of asserted atoms).›
assert_all_state_unsat: "△ t ==> assert_all_state t as = s' ==> U s' ==> minimal_unsat_state_core s'" and
assert_all_state_unsat_atoms_equiv_bounds: "△ t ==> assert_all_state t as = s' ==> U s' ==> set as ⊨i BI s'" and
― ‹The set of indices is taken from the constraints›
assert_all_state_indices: "△ t ==> assert_all_state t as = s ==> indices_state s ⊆ fst ` set as" and
assert_all_index_valid: "△ t ==> assert_all_state t as = s ==> index_valid (set as) s"
begin
definition assert_all where
"assert_all t as ≡ let s = assert_all_state t as in
if (U s) then Unsat (the (Uc s)) else Sat (V s)"
end
text‹The ‹assert_all_state› function can be implemented by first
the ‹init› function that creates an initial state based
the starting tableau, and then by iteratively applying the ‹assert› function for each atom in the starting atoms list.›
text‹
begin{small}
‹assert_loop as s ≡ foldl (λ s' a. if (U s') then s' else assert a s') s as›
‹assert_all_state t as ≡ assert_loop ats (init t)›
end{small}
›
locale Init' =
fixes init :: "tableau ==> ('i,'a::lrv) state"
assumes init'_tableau_normalized: "△ t ==> △ (T (init t))"
assumes init'_tableau_equiv: "△ t ==> (v::'a valuation) ⊨t t = v ⊨t T (init t)"
assumes init'_sat: "△ t ==> ¬ U (init t) ⟶ ⊨ (init t)"
assumes init'_unsat: "△ t ==> U (init t) ⟶ minimal_unsat_state_core (init t)"
assumes init'_atoms_equiv_bounds: "△ t ==> {} ≐ B (init t)"
assumes init'_atoms_imply_bounds_index: "△ t ==> {} ⊨i BI (init t)"
text‹Specification for ‹init› can be obtained from the
of ‹asser_all_state› since all its assumptions
also hold for ‹init› (when the list of atoms is
). Also, since ‹init› is the first step in the ‹assert_all_state› implementation, the precondition for ‹init›
same as for the ‹assert_all_state›. However,
is never going to be detected during initialization
@{term U} flag is never going to be raised. Also, the tableau in
initial state can just be initialized with the starting
. The condition @{term "{} ≐ B (init t)"} is equivalent to
that initial bounds are empty. Therefore, specification for
‹init› can be refined to:›
locale Init = fixes init::"tableau ==> ('i,'a::lrv) state"
assumes
― ‹Tableau in the initial state for @{text t} is @{text t}:› init_tableau_id: "T (init t) = t" and
― ‹Since unsatisfiability is not detected, @{text U}
flag must not be set:› init_unsat_flag: "¬ U (init t)" and
― ‹The current valuation must satisfy the tableau:› init_satisfies_tableau: "⟨V (init t)⟩ ⊨t t" and
― ‹In an inital state no atoms are yet asserted so the bounds
must be empty:›
init_bounds: "Bil (init t) = Mapping.empty" "Biu (init t) = Mapping.empty" and
― ‹All tableau vars are valuated:› init_tableau_valuated: "∇ (init t)"
begin
lemma init_satisfies_bounds:
"⟨V (init t)⟩ ⊨b B (init t)"
using init_bounds
unfolding satisfies_bounds.simps in_bounds.simps bound_compare_defs
by (auto simp: boundsl_def boundsu_def)
lemma init_satisfies:
"⊨ (init t)"
using init_satisfies_tableau init_satisfies_bounds init_tableau_id
unfolding curr_val_satisfies_state_def satisfies_state_def
by simp
lemma init_atoms_equiv_bounds:
"{} ≐ B (init t)"
using init_bounds
unfolding atoms_equiv_bounds.simps satisfies_bounds.simps in_bounds.simps satisfies_atom_set_def
unfolding bound_compare_defs
by (auto simp: indexl_def indexu_def boundsl_def boundsu_def)
lemma init_atoms_imply_bounds_index:
"{} ⊨i BI (init t)"
using init_bounds
unfolding atoms_imply_bounds_index.simps satisfies_bounds_index.simps in_bounds.simps
i_satisfies_atom_set.simps satisfies_atom_set_def
unfolding bound_compare_defs
by (auto simp: indexl_def indexu_def boundsl_def boundsu_def)
lemma init_tableau_normalized:
"△ t ==> △ (T (init t))"
using init_tableau_id
by simp
lemma init_index_valid: "index_valid as (init t)"
using init_bounds unfolding index_valid_def by auto
lemma init_indices: "indices_state (init t) = {}"
unfolding indices_state_def init_bounds by auto
end
sublocale Init < Init' init
using init_tableau_id init_satisfies init_unsat_flag init_atoms_equiv_bounds init_atoms_imply_bounds_index
by unfold_locales auto
abbreviation vars_list where
"vars_list t ≡ remdups (map lhs t @ (concat (map (Abstract_Linear_Poly.vars_list ∘ rhs) t)))"
lemma "tvars t = set (vars_list t)"
by (auto simp add: set_vars_list lvars_def rvars_def)
text‹\smallskip The ‹assert› function asserts a single
. Since the ‹init› function does not raise the ‹U›
, from the definition of ‹assert_loop›, it is clear that the
is not raised when the ‹assert› function is
. Moreover, the assumptions about the ‹assert_all_state›
that the loop invariant must be that if the ‹U› flag is
raised, then the current valuation must satisfy the state (i.e.,
‹⊨ s›). The ‹assert› function will be more easily
if it is always applied to a state with a normalized and
tableau, so we make this another loop invariant. Therefore,
precondition for the ‹assert a s› function call is that
‹¬ U s›, ‹⊨ s›, ‹△ (T s)› and ‹∇ s›
. The specification for ‹assert› directly follows from the
of ‹assert_all_state› (except that it is
required that bounds reflect asserted atoms also when
is detected, and that it is required that ‹assert› keeps the tableau normalized and valuated).›
locale Assert = fixes assert::"('i,'a::lrv) i_atom ==> ('i,'a) state ==> ('i,'a) state"
assumes
― ‹Tableau remains equivalent to the previous one and normalized and valuated.›
assert_tableau: "[¬ U s; ⊨ s; △ (T s); ∇ s] ==> let s' = assert a s in
((v::'a valuation) ⊨t T s ⟷ v ⊨t T s') ∧ △ (T s') ∧ ∇ s'" and
― ‹If the @{term U} flag is not raised, then the current
valuation is updated so that it satisfies the current tableau and
the current bounds.›
assert_sat: "[¬ U s; ⊨ s; △ (T s); ∇ s] ==> ¬ U (assert a s) ==> ⊨ (assert a s)" and
― ‹The set of asserted atoms remains equivalent to the bounds
in the state.›
assert_atoms_equiv_bounds: "[¬ U s; ⊨ s; △ (T s); ∇ s] ==> flat ats ≐ B s ==> flat (ats ∪ {a}) ≐ B (assert a s)" and
― ‹There is a subset of asserted atoms which remains index-equivalent to the bounds
in the state.›
assert_atoms_imply_bounds_index: "[¬ U s; ⊨ s; △ (T s); ∇ s] ==> ats ⊨i BI s ==>
insert a ats ⊨i BI (assert a s)" and
― ‹If the @{term U} flag is raised, then there is no valuation
that satisfies both the current tableau and the current bounds.›
assert_unsat: "[¬ U s; ⊨ s; △ (T s); ∇ s; index_valid ats s] ==> U (assert a s) ==> minimal_unsat_state_core (assert a s)" and
assert_index_valid: "[¬ U s; ⊨ s; △ (T s); ∇ s] ==> index_valid ats s ==> index_valid (insert a ats) (assert a s)"
begin
lemma assert_tableau_equiv: "[¬ U s; ⊨ s; △ (T s); ∇ s] ==> (v::'a valuation) ⊨t T s ⟷ v ⊨t T (assert a s)"
using assert_tableau
by (simp add: Let_def)
lemma assert_tableau_normalized: "[¬ U s; ⊨ s; △ (T s); ∇ s] ==> △ (T (assert a s))"
using assert_tableau
by (simp add: Let_def)
lemma assert_tableau_valuated: "[¬ U s; ⊨ s; △ (T s); ∇ s] ==> ∇ (assert a s)"
using assert_tableau
by (simp add: Let_def)
end
locale AssertAllState' = Init init + Assert assert for
init :: "tableau \<Rightarrow> ('i,'a::lrv) state" and assert :: "('i,'a) i_atom \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state"
begin
definition assert_loop where
"assert_loop as s \<equiv> foldl (\<lambda> s' a. if (\<U> s') then s' else assert a s') s as"
definition assert_all_state where [simp]:
"assert_all_state t as \<equiv> assert_loop as (init t)"
lemma AssertAllState'_precond:
"\<triangle> t \<Longrightarrow> \<triangle> (\<T> (assert_all_state t as))
\<and> (\<nabla> (assert_all_state t as))
\<and> (\<not> \<U> (assert_all_state t as) \<longrightarrow> \<Turnstile> (assert_all_state t as))"
unfolding assert_all_state_def assert_loop_def
using init_satisfies init_tableau_normalized init_index_valid
using assert_sat assert_tableau_normalized init_tableau_valuated assert_tableau_valuated
by (induct as rule: rev_induct) auto
lemma AssertAllState'Induct:
assumes
"\<triangle> t"
"P {} (init t)"
"\<And> as bs t. as \<subseteq> bs \<Longrightarrow> P as t \<Longrightarrow> P bs t"
"\<And> s a as. \<lbrakk>\<not> \<U> s; \<Turnstile> s; \<triangle> (\<T> s); \<nabla> s; P as s; index_valid as s\<rbrakk> \<Longrightarrow> P (insert a as) (assert a s)"
shows "P (set as) (assert_all_state t as)"
proof -
have "P (set as) (assert_all_state t as) \<and> index_valid (set as) (assert_all_state t as)"
proof (induct as rule: rev_induct)
case Nil
then show ?case
unfolding assert_all_state_def assert_loop_def
using assms(2) init_index_valid by auto
next
case (snoc a as')
let ?f = "\<lambda>s' a. if \<U> s' then s' else assert a s'"
let ?s = "foldl ?f (init t) as'"
show ?case
proof (cases "\<U> ?s")
case True
from snoc index_valid_mono[of _ "set (a # as')" "(assert_all_state t as')"]
have index: "index_valid (set (a # as')) (assert_all_state t as')"
by auto
from snoc assms(3)[of "set as'" "set (a # as')"]
have P: "P (set (a # as')) (assert_all_state t as')" by auto
show ?thesis
using True P index
unfolding assert_all_state_def assert_loop_def
by simp
next
case False
then show ?thesis
using snoc
using assms(1) assms(4)
using AssertAllState'_precond assert_index_valid
unfolding assert_all_state_def assert_loop_def
by auto
qed
qed
then show ?thesis ..
qed
lemma AssertAllState_index_valid: "\<triangle> t \<Longrightarrow> index_valid (set as) (assert_all_state t as)"
by (rule AssertAllState'Induct, auto intro: assert_index_valid init_index_valid index_valid_mono)
lemma AssertAllState'_sat_atoms_equiv_bounds:
"\<triangle> t \<Longrightarrow> \<not> \<U> (assert_all_state t as) \<Longrightarrow> flat (set as) \<doteq> \<B> (assert_all_state t as)"
using AssertAllState'_precond
using init_atoms_equiv_bounds assert_atoms_equiv_bounds
unfolding assert_all_state_def assert_loop_def
by (induct as rule: rev_induct) auto
lemma AssertAllState'_unsat_atoms_implies_bounds:
assumes "\<triangle> t"
shows "set as \<Turnstile>\<^sub>i \<B>\<I> (assert_all_state t as)"
proof (induct as rule: rev_induct)
case Nil
then show ?case
using assms init_atoms_imply_bounds_index
unfolding assert_all_state_def assert_loop_def
by simp
next
case (snoc a as')
let ?s = "assert_all_state t as'"
show ?case
proof (cases "\<U> ?s")
case True
then show ?thesis
using snoc atoms_imply_bounds_index_mono[of "set as'" "set (as' @ [a])"]
unfolding assert_all_state_def assert_loop_def
by auto
next
case False
then have id: "assert_all_state t (as' @ [a]) = assert a ?s"
unfolding assert_all_state_def assert_loop_def by simp
from snoc have as': "set as' \<Turnstile>\<^sub>i \<B>\<I> ?s" by auto
from AssertAllState'_precond[of t as'] assms False
have "\<Turnstile> ?s" "\<triangle> (\<T> ?s)" "\<nabla> ?s" by auto
from assert_atoms_imply_bounds_index[OF False this as', of a]
show ?thesis unfolding id by auto
qed
qed
end
text\<open>Under these assumptions, it can easily be shown (mainly by
induction) that the previously shown implementation of \<open>assert_all_state\<close> satisfies its specification.\<close>
sublocale AssertAllState' < AssertAllState assert_all_state
proof
fix v::"'a valuation" and t as s'
assume *: "\<triangle> t" and id: "assert_all_state t as = s'"
note idsym = id[symmetric]
show "v \<Turnstile>\<^sub>t t = v \<Turnstile>\<^sub>t \<T> s'" unfolding idsym
using init_tableau_id[of t] assert_tableau_equiv[of _ v]
by (induct rule: AssertAllState'Induct) (auto simp add: * )
show "\<not> \<U> s' \<Longrightarrow> \<Turnstile> s'" unfolding idsym
using AssertAllState'_precond by (simp add: * )
show "\<not> \<U> s' \<Longrightarrow> flat (set as) \<doteq> \<B> s'"
unfolding idsym
using *
by (rule AssertAllState'_sat_atoms_equiv_bounds)
show "\<U> s' \<Longrightarrow> set as \<Turnstile>\<^sub>i \<B>\<I> s'"
using * unfolding idsym
by (rule AssertAllState'_unsat_atoms_implies_bounds)
show "\<U> s' \<Longrightarrow> minimal_unsat_state_core s'"
using init_unsat_flag assert_unsat assert_index_valid unfolding idsym
by (induct rule: AssertAllState'Induct) (auto simp add: * )
show "indices_state s' \<subseteq> fst ` set as" unfolding idsym using *
by (intro index_valid_indices_state, induct rule: AssertAllState'Induct,
auto simp: init_index_valid index_valid_mono assert_index_valid)
show "index_valid (set as) s'" using "*" AssertAllState_index_valid idsym by blast
qed
subsection\<open>Asserting Single Atoms\<close>
text\<open>The @{term assert} function is split in two phases. First,
@{term assert_bound} updates the bounds and checks only for conflicts
cheap to detect. Next, \<open>check\<close> performs the full simplex
algorithm. The \<open>assert\<close> function can be implemented as \<open>assert a s = check (assert_bound a s)\<close>. Note that it is also
possible to do the first phase for several asserted atoms, and only
then to let the expensive second phase work.
\medskip Asserting an atom \<open>x \<bowtie> b\<close> begins with the function
\<open>assert_bound\<close>. If the atom is subsumed by the current bounds,
then no changes are performed. Otherwise, bounds for \<open>x\<close> are
changed to incorporate the atom. If the atom is inconsistent with the
previous bounds for \<open>x\<close>, the @{term \<U>} flag is raised. If
\<open>x\<close> is not a lhs variable in the current tableau and if the
value for \<open>x\<close> in the current valuation violates the new bound
\<open>b\<close>, the value for \<open>x\<close> can be updated and set to
\<open>b\<close>, meanwhile updating the values for lhs variables of
the tableau so that it remains satisfied. Otherwise, no changes to the
current valuation are performed.\<close>
fun satisfies_bounds_set :: "'a::linorder valuation \<Rightarrow> 'a bounds \<times> 'a bounds \<Rightarrow> var set \<Rightarrow> bool" where
"satisfies_bounds_set v (lb, ub) S \<longleftrightarrow> (\<forall> x \<in> S. in_bounds x v (lb, ub))"
declare satisfies_bounds_set.simps [simp del]
syntax
"_satisfies_bounds_set" :: "(var \<Rightarrow> 'a::linorder) \<Rightarrow> 'a bounds \<times> 'a bounds \<Rightarrow> var set \<Rightarrow> bool" (\<open>_ \<Turnstile>\<^sub>b _ \<parallel>/ _\<close>)
syntax_consts
"_satisfies_bounds_set" == satisfies_bounds_set
translations
"v \<Turnstile>\<^sub>b b \<parallel> S" == "CONST satisfies_bounds_set v b S"
lemma satisfies_bounds_set_iff:
"v \<Turnstile>\<^sub>b (lb, ub) \<parallel> S \<equiv> (\<forall> x \<in> S. v x \<ge>\<^sub>l\<^sub>b lb x \<and> v x \<le>\<^sub>u\<^sub>b ub x)"
by (simp add: satisfies_bounds_set.simps)
definition curr_val_satisfies_no_lhs (\<open>\<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s\<close>) where
"\<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s \<equiv> \<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t (\<T> s) \<and> (\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>b (\<B> s) \<parallel> (- lvars (\<T> s)))"
lemma satisfies_satisfies_no_lhs:
"\<Turnstile> s \<Longrightarrow> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s"
by (simp add: curr_val_satisfies_state_def satisfies_state_def curr_val_satisfies_no_lhs_def satisfies_bounds.simps satisfies_bounds_set.simps)
definition bounds_consistent :: "('i,'a::linorder) state \<Rightarrow> bool" (\<open>\<diamond>\<close>) where
"\<diamond> s \<equiv>
\<forall> x. if \<B>\<^sub>l s x = None \<or> \<B>\<^sub>u s x = None then True else the (\<B>\<^sub>l s x) \<le> the (\<B>\<^sub>u s x)"
text\<open>So, the \<open>assert_bound\<close> function must ensure that the
given atom is included in the bounds, that the tableau remains
satisfied by the valuation and that all variables except the lhs variables
in the tableau are within their
bounds. To formalize this, we introduce the notation \<open>v
\<Turnstile>\<^sub>b (lb, ub) \<parallel> S\<close>, and define @{thm
satisfies_bounds_set_iff[no_vars]}, and @{thm
curr_val_satisfies_no_lhs_def[no_vars]}. The \<open>assert_bound\<close>
function raises the \<open>\<U>\<close> flag if and only if lower and upper
bounds overlap. This is formalized as @{thm
bounds_consistent_def[no_vars]}.\<close>
lemma satisfies_bounds_consistent:
"(v::'a::linorder valuation) \<Turnstile>\<^sub>b \<B> s \<longrightarrow> \<diamond> s"
unfolding satisfies_bounds.simps in_bounds.simps bounds_consistent_def bound_compare_defs
by (auto split: option.split) force
lemma satisfies_consistent:
"\<Turnstile> s \<longrightarrow> \<diamond> s"
by (auto simp add: curr_val_satisfies_state_def satisfies_state_def satisfies_bounds_consistent)
lemma bounds_consistent_geq_lb:
"\<lbrakk>\<diamond> s; \<B>\<^sub>u s x\<^sub>i = Some c\<rbrakk>
\<Longrightarrow> c \<ge>\<^sub>l\<^sub>b \<B>\<^sub>l s x\<^sub>i"
unfolding bounds_consistent_def
by (cases "\<B>\<^sub>l s x\<^sub>i", auto simp add: bound_compare_defs split: if_splits)
(erule_tac x="x\<^sub>i" in allE, auto)
lemma bounds_consistent_leq_ub:
"\<lbrakk>\<diamond> s; \<B>\<^sub>l s x\<^sub>i = Some c\<rbrakk>
\<Longrightarrow> c \<le>\<^sub>u\<^sub>b \<B>\<^sub>u s x\<^sub>i"
unfolding bounds_consistent_def
by (cases "\<B>\<^sub>u s x\<^sub>i", auto simp add: bound_compare_defs split: if_splits)
(erule_tac x="x\<^sub>i" in allE, auto)
lemma bounds_consistent_gt_ub:
"\<lbrakk>\<diamond> s; c <\<^sub>l\<^sub>b \<B>\<^sub>l s x \<rbrakk> \<Longrightarrow> \<not> c >\<^sub>u\<^sub>b \<B>\<^sub>u s x"
unfolding bounds_consistent_def
by (case_tac[!] "\<B>\<^sub>l s x", case_tac[!] "\<B>\<^sub>u s x")
(auto simp add: bound_compare_defs, erule_tac x="x" in allE, simp)
lemma bounds_consistent_lt_lb:
"\<lbrakk>\<diamond> s; c >\<^sub>u\<^sub>b \<B>\<^sub>u s x \<rbrakk> \<Longrightarrow> \<not> c <\<^sub>l\<^sub>b \<B>\<^sub>l s x"
unfolding bounds_consistent_def
by (case_tac[!] "\<B>\<^sub>l s x", case_tac[!] "\<B>\<^sub>u s x")
(auto simp add: bound_compare_defs, erule_tac x="x" in allE, simp)
text\<open>Since the \<open>assert_bound\<close> is the first step in the \<open>assert\<close> function implementation, the preconditions for \<open>assert_bound\<close> are the same as preconditions for the \<open>assert\<close>
function. The specifiction for the \<open>assert_bound\<close> is:\<close>
locale AssertBound = fixes assert_bound::"('i,'a::lrv) i_atom \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state"
assumes
\<comment> \<open>The tableau remains unchanged and valuated.\<close>
assert_bound_tableau: "\<lbrakk>\<not> \<U> s; \<Turnstile> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> assert_bound a s = s' \<Longrightarrow> \<T> s' = \<T> s \<and> \<nabla> s'" and
\<comment> \<open>If the @{term \<U>} flag is not set, all but the
lhs variables in the tableau remain within their bounds,
the new valuation satisfies the tableau, and bounds do not overlap.\<close>
assert_bound_sat: "\<lbrakk>\<not> \<U> s; \<Turnstile> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> assert_bound a s = s' \<Longrightarrow> \<not> \<U> s' \<Longrightarrow> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s' \<and> \<diamond> s'" and
\<comment> \<open>The set of asserted atoms remains equivalent to the bounds in the state.\<close>
assert_bound_atoms_equiv_bounds: "\<lbrakk>\<not> \<U> s; \<Turnstile> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow>
flat ats \<doteq> \<B> s \<Longrightarrow> flat (ats \<union> {a}) \<doteq> \<B> (assert_bound a s)" and
assert_bound_atoms_imply_bounds_index: "\<lbrakk>\<not> \<U> s; \<Turnstile> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow>
ats \<Turnstile>\<^sub>i \<B>\<I> s \<Longrightarrow> insert a ats \<Turnstile>\<^sub>i \<B>\<I> (assert_bound a s)" and
\<comment> \<open>@{term \<U>} flag is raised, only if the bounds became inconsistent:\<close>
assert_bound_unsat: "\<lbrakk>\<not> \<U> s; \<Turnstile> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> index_valid as s \<Longrightarrow> assert_bound a s = s' \<Longrightarrow> \<U> s' \<Longrightarrow> minimal_unsat_state_core s'" and
assert_bound_index_valid: "\<lbrakk>\<not> \<U> s; \<Turnstile> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> index_valid as s \<Longrightarrow> index_valid (insert a as) (assert_bound a s)"
begin
lemma assert_bound_tableau_id: "\<lbrakk>\<not> \<U> s; \<Turnstile> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<T> (assert_bound a s) = \<T> s"
using assert_bound_tableau by blast
lemma assert_bound_tableau_valuated: "\<lbrakk>\<not> \<U> s; \<Turnstile> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<nabla> (assert_bound a s)"
using assert_bound_tableau by blast
end
locale AssertBoundNoLhs =
fixes assert_bound :: "('i,'a::lrv) i_atom \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state"
assumes assert_bound_nolhs_tableau_id: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<triangle> (\<T> s); \<nabla> s; \<diamond> s\<rbrakk> \<Longrightarrow> \<T> (assert_bound a s) = \<T> s"
assumes assert_bound_nolhs_sat: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<triangle> (\<T> s); \<nabla> s; \<diamond> s\<rbrakk> \<Longrightarrow>
\<not> \<U> (assert_bound a s) \<Longrightarrow> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s (assert_bound a s) \<and> \<diamond> (assert_bound a s)"
assumes assert_bound_nolhs_atoms_equiv_bounds: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<triangle> (\<T> s); \<nabla> s; \<diamond> s\<rbrakk> \<Longrightarrow>
flat ats \<doteq> \<B> s \<Longrightarrow> flat (ats \<union> {a}) \<doteq> \<B> (assert_bound a s)"
assumes assert_bound_nolhs_atoms_imply_bounds_index: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<triangle> (\<T> s); \<nabla> s; \<diamond> s\<rbrakk> \<Longrightarrow>
ats \<Turnstile>\<^sub>i \<B>\<I> s \<Longrightarrow> insert a ats \<Turnstile>\<^sub>i \<B>\<I> (assert_bound a s)"
assumes assert_bound_nolhs_unsat: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<triangle> (\<T> s); \<nabla> s; \<diamond> s\<rbrakk> \<Longrightarrow>
index_valid as s \<Longrightarrow> \<U> (assert_bound a s) \<Longrightarrow> minimal_unsat_state_core (assert_bound a s)"
assumes assert_bound_nolhs_tableau_valuated: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<triangle> (\<T> s); \<nabla> s; \<diamond> s\<rbrakk> \<Longrightarrow>
\<nabla> (assert_bound a s)"
assumes assert_bound_nolhs_index_valid: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<triangle> (\<T> s); \<nabla> s; \<diamond> s\<rbrakk> \<Longrightarrow>
index_valid as s \<Longrightarrow> index_valid (insert a as) (assert_bound a s)"
sublocale AssertBoundNoLhs < AssertBound
by unfold_locales
((metis satisfies_satisfies_no_lhs satisfies_consistent
assert_bound_nolhs_tableau_id assert_bound_nolhs_sat assert_bound_nolhs_atoms_equiv_bounds
assert_bound_nolhs_index_valid assert_bound_nolhs_atoms_imply_bounds_index
assert_bound_nolhs_unsat assert_bound_nolhs_tableau_valuated)+)
text\<open>The second phase of \<open>assert\<close>, the \<open>check\<close> function,
is the heart of the Simplex algorithm. It is always called after
\<open>assert_bound\<close>, but in two different situations. In the first
case \<open>assert_bound\<close> raised the \<open>\<U>\<close> flag and then
\<open>check\<close> should retain the flag and should not perform any changes.
In the second case \<open>assert_bound\<close> did not raise the
\<open>\<U>\<close> flag, so \<open>\<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s\<close>, \<open>\<diamond> s\<close>, \<open>\<triangle> (\<T>
s)\<close>, and \<open>\<nabla> s\<close> hold.\<close>
locale Check = fixes check::"('i,'a::lrv) state \<Rightarrow> ('i,'a) state"
assumes
\<comment> \<open>If @{text check} is called from an inconsistent state, the state is unchanged.\<close>
check_unsat_id: "\<U> s \<Longrightarrow> check s = s" and
\<comment> \<open>The tableau remains equivalent to the previous one, normalized and valuated, the state stays consistent.\<close>
check_tableau: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow>
let s' = check s in ((v::'a valuation) \<Turnstile>\<^sub>t \<T> s \<longleftrightarrow> v \<Turnstile>\<^sub>t \<T> s') \<and> \<triangle> (\<T> s') \<and> \<nabla> s' \<and> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s' \<and> \<diamond> s'" and
\<comment> \<open>The bounds remain unchanged.\<close>
check_bounds_id: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<B>\<^sub>i (check s) = \<B>\<^sub>i s" and
\<comment> \<open>If @{term \<U>} flag is not raised, the current valuation
@{text "\<V>"} satisfies both the tableau and the bounds and if it is
raised, there is no valuation that satisfies them.\<close>
check_sat: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<not> \<U> (check s) \<Longrightarrow> \<Turnstile> (check s)" and
check_unsat: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<U> (check s) \<Longrightarrow> minimal_unsat_state_core (check s)"
begin
lemma check_tableau_equiv: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow>
(v::'a valuation) \<Turnstile>\<^sub>t \<T> s \<longleftrightarrow> v \<Turnstile>\<^sub>t \<T> (check s)"
using check_tableau
by (simp add: Let_def)
lemma check_tableau_index_valid: assumes "\<not> \<U> s" " \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s" "\<diamond> s" "\<triangle> (\<T> s)" "\<nabla> s"
shows "index_valid as (check s) = index_valid as s"
unfolding index_valid_def using check_bounds_id[OF assms]
by (auto simp: indexl_def indexu_def boundsl_def boundsu_def)
lemma check_tableau_normalized: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<triangle> (\<T> (check s))"
using check_tableau
by (simp add: Let_def)
lemma check_bounds_consistent: assumes "\<not> \<U> s" "\<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s" "\<diamond> s" "\<triangle> (\<T> s)" "\<nabla> s"
shows "\<diamond> (check s)"
using check_bounds_id[OF assms] assms(3)
unfolding Let_def bounds_consistent_def boundsl_def boundsu_def
by (metis Pair_inject)
lemma check_tableau_valuated: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<nabla> (check s)"
using check_tableau
by (simp add: Let_def)
lemma check_indices_state: assumes "\<not> \<U> s \<Longrightarrow> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s" "\<not> \<U> s \<Longrightarrow> \<diamond> s" "\<not> \<U> s \<Longrightarrow> \<triangle> (\<T> s)" "\<not> \<U> s \<Longrightarrow> \<nabla> s"
shows "indices_state (check s) = indices_state s"
using check_bounds_id[OF _ assms] check_unsat_id[of s]
unfolding indices_state_def by (cases "\<U> s", auto)
lemma check_distinct_indices_state: assumes "\<not> \<U> s \<Longrightarrow> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s" "\<not> \<U> s \<Longrightarrow> \<diamond> s" "\<not> \<U> s \<Longrightarrow> \<triangle> (\<T> s)" "\<not> \<U> s \<Longrightarrow> \<nabla> s"
shows "distinct_indices_state (check s) = distinct_indices_state s"
using check_bounds_id[OF _ assms] check_unsat_id[of s]
unfolding distinct_indices_state_def by (cases "\<U> s", auto)
end
locale Assert' = AssertBound assert_bound + Check check for
assert_bound :: "('i,'a::lrv) i_atom \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state" and
check :: "('i,'a::lrv) state \<Rightarrow> ('i,'a) state"
begin
definition assert :: "('i,'a) i_atom \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state" where
"assert a s \<equiv> check (assert_bound a s)"
lemma Assert'Precond:
assumes "\<not> \<U> s" "\<Turnstile> s" "\<triangle> (\<T> s)" "\<nabla> s"
shows
"\<triangle> (\<T> (assert_bound a s))"
"\<not> \<U> (assert_bound a s) \<Longrightarrow> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s (assert_bound a s) \<and> \<diamond> (assert_bound a s)"
"\<nabla> (assert_bound a s)"
using assms
using assert_bound_tableau_id assert_bound_sat assert_bound_tableau_valuated
by (auto simp add: satisfies_bounds_consistent Let_def)
end
sublocale Assert' < Assert assert
proof
fix s::"('i,'a) state" and v::"'a valuation" and a::"('i,'a) i_atom"
assume *: "\<not> \<U> s" "\<Turnstile> s" "\<triangle> (\<T> s)" "\<nabla> s"
have "\<triangle> (\<T> (assert a s))"
using check_tableau_normalized[of "assert_bound a s"] check_unsat_id[of "assert_bound a s"] *
using assert_bound_sat[of s a] Assert'Precond[of s a]
by (force simp add: assert_def)
moreover
have "v \<Turnstile>\<^sub>t \<T> s = v \<Turnstile>\<^sub>t \<T> (assert a s)"
using check_tableau_equiv[of "assert_bound a s" v] *
using check_unsat_id[of "assert_bound a s"]
by (force simp add: assert_def Assert'Precond assert_bound_sat assert_bound_tableau_id)
moreover
have "\<nabla> (assert a s)"
using assert_bound_tableau_valuated[of s a] *
using check_tableau_valuated[of "assert_bound a s"]
using check_unsat_id[of "assert_bound a s"]
by (cases "\<U> (assert_bound a s)") (auto simp add: Assert'Precond assert_def)
ultimately
show "let s' = assert a s in (v \<Turnstile>\<^sub>t \<T> s = v \<Turnstile>\<^sub>t \<T> s') \<and> \<triangle> (\<T> s') \<and> \<nabla> s'"
by (simp add: Let_def)
next
fix s::"('i,'a) state" and a::"('i,'a) i_atom"
assume "\<not> \<U> s" "\<Turnstile> s" "\<triangle> (\<T> s)" "\<nabla> s"
then show "\<not> \<U> (assert a s) \<Longrightarrow> \<Turnstile> (assert a s)"
unfolding assert_def
using check_unsat_id[of "assert_bound a s"]
using check_sat[of "assert_bound a s"]
by (force simp add: Assert'Precond)
next
fix s::"('i,'a) state" and a::"('i,'a) i_atom" and ats::"('i,'a) i_atom set"
assume "\<not> \<U> s" "\<Turnstile> s" "\<triangle> (\<T> s)" "\<nabla> s"
then show "flat ats \<doteq> \<B> s \<Longrightarrow> flat (ats \<union> {a}) \<doteq> \<B> (assert a s)"
using assert_bound_atoms_equiv_bounds
using check_unsat_id[of "assert_bound a s"] check_bounds_id
by (cases "\<U> (assert_bound a s)") (auto simp add: Assert'Precond assert_def
simp: indexl_def indexu_def boundsl_def boundsu_def)
next
fix s::"('i,'a) state" and a::"('i,'a) i_atom" and ats
assume *: "\<not> \<U> s" "\<Turnstile> s" "\<triangle> (\<T> s)" "\<nabla> s" "\<U> (assert a s)" "index_valid ats s"
show "minimal_unsat_state_core (assert a s)"
proof (cases "\<U> (assert_bound a s)")
case True
then show ?thesis
unfolding assert_def
using * assert_bound_unsat check_tableau_equiv[of "assert_bound a s"] check_bounds_id
using check_unsat_id[of "assert_bound a s"]
by (auto simp add: Assert'Precond satisfies_state_def Let_def)
next
case False
then show ?thesis
unfolding assert_def
using * assert_bound_sat[of s a] check_unsat Assert'Precond
by (metis assert_def)
qed
next
fix ats
fix s::"('i,'a) state" and a::"('i,'a) i_atom"
assume *: "index_valid ats s"
and **: "\<not> \<U> s" "\<Turnstile> s" "\<triangle> (\<T> s)" "\<nabla> s"
have *: "index_valid (insert a ats) (assert_bound a s)"
using assert_bound_index_valid[OF ** *] .
show "index_valid (insert a ats) (assert a s)"
proof (cases "\<U> (assert_bound a s)")
case True
show ?thesis unfolding assert_def check_unsat_id[OF True] using * .
next
case False
show ?thesis unfolding assert_def using Assert'Precond[OF **, of a] False *
by (subst check_tableau_index_valid[OF False], auto)
qed
next
fix s ats a
let ?s = "assert_bound a s"
assume *: "\<not> \<U> s" "\<Turnstile> s" "\<triangle> (\<T> s)" "\<nabla> s" "ats \<Turnstile>\<^sub>i \<B>\<I> s"
from assert_bound_atoms_imply_bounds_index[OF this, of a]
have as: "insert a ats \<Turnstile>\<^sub>i \<B>\<I> (assert_bound a s)" by auto
show "insert a ats \<Turnstile>\<^sub>i \<B>\<I> (assert a s)"
proof (cases "\<U> ?s")
case True
from check_unsat_id[OF True] as show ?thesis unfolding assert_def by auto
next
case False
from assert_bound_tableau_id[OF *(1-4)] *
have t: "\<triangle> (\<T> ?s)" by simp
from assert_bound_tableau_valuated[OF *(1-4)]
have v: "\<nabla> ?s" .
from assert_bound_sat[OF *(1-4) refl False]
have "\<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s ?s" "\<diamond> ?s" by auto
from check_bounds_id[OF False this t v] as
show ?thesis unfolding assert_def
by (auto simp: indexl_def indexu_def boundsl_def boundsu_def)
qed
qed
text\<open>Under these assumptions for \<open>assert_bound\<close> and \<open>check\<close>, it can be easily shown that the implementation of \<open>assert\<close> (previously given) satisfies its specification.\<close>
locale AssertAllState'' = Init init + AssertBoundNoLhs assert_bound + Check check for
init :: "tableau \<Rightarrow> ('i,'a::lrv) state" and
assert_bound :: "('i,'a::lrv) i_atom \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state" and
check :: "('i,'a::lrv) state \<Rightarrow> ('i,'a) state"
begin
definition assert_bound_loop where
"assert_bound_loop ats s \<equiv> foldl (\<lambda> s' a. if (\<U> s') then s' else assert_bound a s') s ats"
definition assert_all_state where [simp]:
"assert_all_state t ats \<equiv> check (assert_bound_loop ats (init t))"
text\<open>However, for efficiency reasons, we want to allow
implementations that delay the \<open>check\<close> function call and call it
after several \<open>assert_bound\<close> calls. For example:
\smallskip
\begin{small}
@{thm assert_bound_loop_def[no_vars]}
@{thm assert_all_state_def[no_vars]}
\end{small}
\smallskip
Then, the loop consists only of \<open>assert_bound\<close> calls, so \<open>assert_bound\<close> postcondition must imply its precondition. This is not
the case, since variables on the lhs may be out of their
bounds. Therefore, we make a refinement and specify weaker
preconditions (replace \<open>\<Turnstile> s\<close>, by \<open>\<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s\<close> and \<open>\<diamond> s\<close>) for \<open>assert_bound\<close>, and show that these
preconditions are still good enough to prove the correctnes of this
alternative \<open>assert_all_state\<close> definition.\<close>
lemma AssertAllState''_precond':
assumes "\<triangle> (\<T> s)" "\<nabla> s" "\<not> \<U> s \<longrightarrow> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s \<and> \<diamond> s"
shows "let s' = assert_bound_loop ats s in
\<triangle> (\<T> s') \<and> \<nabla> s' \<and> (\<not> \<U> s' \<longrightarrow> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s' \<and> \<diamond> s')"
using assms
using assert_bound_nolhs_tableau_id assert_bound_nolhs_sat assert_bound_nolhs_tableau_valuated
by (induct ats rule: rev_induct) (auto simp add: assert_bound_loop_def Let_def)
lemma AssertAllState''_precond:
assumes "\<triangle> t"
shows "let s' = assert_bound_loop ats (init t) in
\<triangle> (\<T> s') \<and> \<nabla> s' \<and> (\<not> \<U> s' \<longrightarrow> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s' \<and> \<diamond> s')"
using assms
using AssertAllState''_precond'[of "init t" ats]
by (simp add: Let_def init_tableau_id init_unsat_flag init_satisfies satisfies_consistent
satisfies_satisfies_no_lhs init_tableau_valuated)
lemma AssertAllState''Induct:
assumes
"\<triangle> t"
"P {} (init t)"
"\<And> as bs t. as \<subseteq> bs \<Longrightarrow> P as t \<Longrightarrow> P bs t"
"\<And> s a ats. \<lbrakk>\<not> \<U> s; \<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<triangle> (\<T> s); \<nabla> s; \<diamond> s; P (set ats) s; index_valid (set ats) s\<rbrakk>
\<Longrightarrow> P (insert a (set ats)) (assert_bound a s)"
shows "P (set ats) (assert_bound_loop ats (init t))"
proof -
have "P (set ats) (assert_bound_loop ats (init t)) \<and> index_valid (set ats) (assert_bound_loop ats (init t))"
proof (induct ats rule: rev_induct)
case Nil
then show ?case
unfolding assert_bound_loop_def
using assms(2) init_index_valid
by simp
next
case (snoc a as')
let ?s = "assert_bound_loop as' (init t)"
from snoc index_valid_mono[of _ "set (a # as')" "assert_bound_loop as' (init t)"]
have index: "index_valid (set (a # as')) (assert_bound_loop as' (init t))"
by auto
from snoc assms(3)[of "set as'" "set (a # as')"]
have P: "P (set (a # as')) (assert_bound_loop as' (init t))" by auto
show ?case
proof (cases "\<U> ?s")
case True
then show ?thesis
using P index
unfolding assert_bound_loop_def
by simp
next
case False
have id': "set (as' @ [a]) = insert a (set as')" by simp
have id: "assert_bound_loop (as' @ [a]) (init t) =
assert_bound a (assert_bound_loop as' (init t))"
using False unfolding assert_bound_loop_def by auto
from snoc have index: "index_valid (set as') ?s" by simp
show ?thesis unfolding id unfolding id' using False snoc AssertAllState''_precond[OF assms(1)]
by (intro conjI assert_bound_nolhs_index_valid index assms(4); (force simp: Let_def curr_val_satisfies_no_lhs_def)?)
qed
qed
then show ?thesis ..
qed
lemma AssertAllState''_tableau_id:
"\<triangle> t \<Longrightarrow> \<T> (assert_bound_loop ats (init t)) = \<T> (init t)"
by (rule AssertAllState''Induct) (auto simp add: init_tableau_id assert_bound_nolhs_tableau_id)
lemma AssertAllState''_sat:
"\<triangle> t \<Longrightarrow>
\<not> \<U> (assert_bound_loop ats (init t)) \<longrightarrow> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s (assert_bound_loop ats (init t)) \<and> \<diamond> (assert_bound_loop ats (init t))"
by (rule AssertAllState''Induct) (auto simp add: init_unsat_flag init_satisfies satisfies_consistent satisfies_satisfies_no_lhs assert_bound_nolhs_sat)
lemma AssertAllState''_unsat:
"\<triangle> t \<Longrightarrow> \<U> (assert_bound_loop ats (init t)) \<longrightarrow> minimal_unsat_state_core (assert_bound_loop ats (init t))"
by (rule AssertAllState''Induct)
(auto simp add: init_tableau_id assert_bound_nolhs_unsat init_unsat_flag)
lemma AssertAllState''_sat_atoms_equiv_bounds:
"\<triangle> t \<Longrightarrow> \<not> \<U> (assert_bound_loop ats (init t)) \<longrightarrow> flat (set ats) \<doteq> \<B> (assert_bound_loop ats (init t))"
using AssertAllState''_precond
using assert_bound_nolhs_atoms_equiv_bounds init_atoms_equiv_bounds
by (induct ats rule: rev_induct) (auto simp add: Let_def assert_bound_loop_def)
lemma AssertAllState''_atoms_imply_bounds_index:
assumes "\<triangle> t"
shows "set ats \<Turnstile>\<^sub>i \<B>\<I> (assert_bound_loop ats (init t))"
proof (induct ats rule: rev_induct)
case Nil
then show ?case
unfolding assert_bound_loop_def
using init_atoms_imply_bounds_index assms
by simp
next
case (snoc a ats')
let ?s = "assert_bound_loop ats' (init t)"
show ?case
proof (cases "\<U> ?s")
case True
then show ?thesis
using snoc atoms_imply_bounds_index_mono[of "set ats'" "set (ats' @ [a])"]
unfolding assert_bound_loop_def
by auto
next
case False
then have id: "assert_bound_loop (ats' @ [a]) (init t) = assert_bound a ?s"
unfolding assert_bound_loop_def by auto
from snoc have ats: "set ats' \<Turnstile>\<^sub>i \<B>\<I> ?s" by auto
from AssertAllState''_precond[of t ats', OF assms, unfolded Let_def] False
have *: "\<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s ?s" "\<triangle> (\<T> ?s)" "\<nabla> ?s" "\<diamond> ?s" by auto
show ?thesis unfolding id using assert_bound_nolhs_atoms_imply_bounds_index[OF False * ats, of a] by auto
qed
qed
lemma AssertAllState''_index_valid:
"\<triangle> t \<Longrightarrow> index_valid (set ats) (assert_bound_loop ats (init t))"
by (rule AssertAllState''Induct, auto simp: init_index_valid index_valid_mono assert_bound_nolhs_index_valid)
end
sublocale AssertAllState'' < AssertAllState assert_all_state
proof
fix v::"'a valuation" and t ats s'
assume *: "\<triangle> t" and "assert_all_state t ats = s'"
then have s': "s' = assert_all_state t ats" by simp
let ?s' = "assert_bound_loop ats (init t)"
show "v \<Turnstile>\<^sub>t t = v \<Turnstile>\<^sub>t \<T> s'"
unfolding assert_all_state_def s'
using * check_tableau_equiv[of ?s' v] AssertAllState''_tableau_id[of t ats] init_tableau_id[of t]
using AssertAllState''_sat[of t ats] check_unsat_id[of ?s']
using AssertAllState''_precond[of t ats]
by force
show "\<not> \<U> s' \<Longrightarrow> \<Turnstile> s'"
unfolding assert_all_state_def s'
using * AssertAllState''_precond[of t ats]
using check_sat check_unsat_id
by (force simp add: Let_def)
show "\<U> s' \<Longrightarrow> minimal_unsat_state_core s'"
using * check_unsat check_unsat_id[of ?s'] check_bounds_id
using AssertAllState''_unsat[of t ats] AssertAllState''_precond[of t ats] s'
by (force simp add: Let_def satisfies_state_def)
show "\<not> \<U> s' \<Longrightarrow> flat (set ats) \<doteq> \<B> s'"
unfolding assert_all_state_def s'
using * AssertAllState''_precond[of t ats]
using check_bounds_id[of ?s'] check_unsat_id[of ?s']
using AssertAllState''_sat_atoms_equiv_bounds[of t ats]
by (force simp add: Let_def simp: indexl_def indexu_def boundsl_def boundsu_def)
show "\<U> s' \<Longrightarrow> set ats \<Turnstile>\<^sub>i \<B>\<I> s'"
unfolding assert_all_state_def s'
using * AssertAllState''_precond[of t ats]
unfolding Let_def
using check_bounds_id[of ?s']
using AssertAllState''_atoms_imply_bounds_index[of t ats]
using check_unsat_id[of ?s']
by (cases "\<U> ?s'") (auto simp add: Let_def simp: indexl_def indexu_def boundsl_def boundsu_def)
show "index_valid (set ats) s'"
unfolding assert_all_state_def s'
using * AssertAllState''_precond[of t ats] AssertAllState''_index_valid[OF *, of ats]
unfolding Let_def
using check_tableau_index_valid[of ?s']
using check_unsat_id[of ?s']
by (cases "\<U> ?s'", auto)
show "indices_state s' \<subseteq> fst ` set ats"
by (intro index_valid_indices_state, fact)
qed
subsection\<open>Update and Pivot\<close>
text\<open>Both \<open>assert_bound\<close> and \<open>check\<close> need to update
the valuation so that the tableau remains satisfied. If the value for
a variable not on the lhs of the tableau is changed, this
can be done rather easily (once the value of that variable is changed,
one should recalculate and change the values for all lhs
variables of the tableau). The \<open>update\<close> function does this, and
it is specified by:\<close>
locale Update = fixes update::"var \<Rightarrow> 'a::lrv \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state"
assumes
\<comment> \<open>Tableau, bounds, and the unsatisfiability flag are preserved.\<close>
update_id: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x \<notin> lvars (\<T> s)\<rbrakk> \<Longrightarrow>
let s' = update x c s in \<T> s' = \<T> s \<and> \<B>\<^sub>i s' = \<B>\<^sub>i s \<and> \<U> s' = \<U> s \<and> \<U>\<^sub>c s' = \<U>\<^sub>c s" and
\<comment> \<open>Tableau remains valuated.\<close>
update_tableau_valuated: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x \<notin> lvars (\<T> s)\<rbrakk> \<Longrightarrow> \<nabla> (update x v s)" and
\<comment> \<open>The given variable @{text "x"} in the updated valuation is
set to the given value @{text "v"} while all other variables
(except those on the lhs of the tableau) are
unchanged.\<close>
update_valuation_nonlhs: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x \<notin> lvars (\<T> s)\<rbrakk> \<Longrightarrow> x' \<notin> lvars (\<T> s) \<longrightarrow>
look (\<V> (update x v s)) x' = (if x = x' then Some v else look (\<V> s) x')" and
\<comment> \<open>Updated valuation continues to satisfy the tableau.\<close>
update_satisfies_tableau: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x \<notin> lvars (\<T> s)\<rbrakk> \<Longrightarrow> \<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s \<longrightarrow> \<langle>\<V> (update x c s)\<rangle> \<Turnstile>\<^sub>t \<T> s"
begin
lemma update_bounds_id:
assumes "\<triangle> (\<T> s)" "\<nabla> s" "x \<notin> lvars (\<T> s)"
shows "\<B>\<^sub>i (update x c s) = \<B>\<^sub>i s"
"\<B>\<I> (update x c s) = \<B>\<I> s"
"\<B>\<^sub>l (update x c s) = \<B>\<^sub>l s"
"\<B>\<^sub>u (update x c s) = \<B>\<^sub>u s"
using update_id assms
by (auto simp add: Let_def simp: indexl_def indexu_def boundsl_def boundsu_def)
lemma update_indices_state_id:
assumes "\<triangle> (\<T> s)" "\<nabla> s" "x \<notin> lvars (\<T> s)"
shows "indices_state (update x c s) = indices_state s"
using update_bounds_id[OF assms] unfolding indices_state_def by auto
lemma update_tableau_id: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x \<notin> lvars (\<T> s)\<rbrakk> \<Longrightarrow> \<T> (update x c s) = \<T> s"
using update_id
by (auto simp add: Let_def)
lemma update_unsat_id: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x \<notin> lvars (\<T> s)\<rbrakk> \<Longrightarrow> \<U> (update x c s) = \<U> s"
using update_id
by (auto simp add: Let_def)
lemma update_unsat_core_id: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x \<notin> lvars (\<T> s)\<rbrakk> \<Longrightarrow> \<U>\<^sub>c (update x c s) = \<U>\<^sub>c s"
using update_id
by (auto simp add: Let_def)
definition assert_bound' where
[simp]: "assert_bound' dir i x c s \<equiv>
(if (\<unrhd>\<^sub>u\<^sub>b (lt dir)) c (UB dir s x) then s
else let s' = update\<B>\<I> (UBI_upd dir) i x c s in
if (\<lhd>\<^sub>l\<^sub>b (lt dir)) c ((LB dir) s x) then
set_unsat [i, ((LI dir) s x)] s'
else if x \<notin> lvars (\<T> s') \<and> (lt dir) c (\<langle>\<V> s\<rangle> x) then
update x c s'
else
s')"
fun assert_bound :: "('i,'a::lrv) i_atom \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state" where
"assert_bound (i,Leq x c) s = assert_bound' Positive i x c s"
| "assert_bound (i,Geq x c) s = assert_bound' Negative i x c s"
lemma assert_bound'_cases:
assumes "\<lbrakk>\<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)\<rbrakk> \<Longrightarrow> P s"
assumes "\<lbrakk>\<not> (\<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)); \<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x)\<rbrakk> \<Longrightarrow>
P (set_unsat [i, ((LI dir) s x)] (update\<B>\<I> (UBI_upd dir) i x c s))"
assumes "\<lbrakk>x \<notin> lvars (\<T> s); (lt dir) c (\<langle>\<V> s\<rangle> x); \<not> (\<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)); \<not> (\<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x))\<rbrakk> \<Longrightarrow>
P (update x c (update\<B>\<I> (UBI_upd dir) i x c s))"
assumes "\<lbrakk>\<not> (\<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)); \<not> (\<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x)); x \<in> lvars (\<T> s)\<rbrakk> \<Longrightarrow>
P (update\<B>\<I> (UBI_upd dir) i x c s)"
assumes "\<lbrakk>\<not> (\<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)); \<not> (\<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x)); \<not> ((lt dir) c (\<langle>\<V> s\<rangle> x))\<rbrakk> \<Longrightarrow>
P (update\<B>\<I> (UBI_upd dir) i x c s)"
assumes "dir = Positive \<or> dir = Negative"
shows "P (assert_bound' dir i x c s)"
proof (cases "\<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)")
case True
then show ?thesis
using assms(1)
by simp
next
case False
show ?thesis
proof (cases "\<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x)")
case True
then show ?thesis
using \<open>\<not> \<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)\<close>
using assms(2)
by simp
next
case False
let ?s = "update\<B>\<I> (UBI_upd dir) i x c s"
show ?thesis
proof (cases "x \<notin> lvars (\<T> ?s) \<and> (lt dir) c (\<langle>\<V> s\<rangle> x)")
case True
then show ?thesis
using \<open>\<not> \<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)\<close> \<open>\<not> \<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x)\<close>
using assms(3) assms(6)
by auto
next
case False
then have "x \<in> lvars (\<T> ?s) \<or> \<not> ((lt dir) c (\<langle>\<V> s\<rangle> x))"
by simp
then show ?thesis
proof
assume "x \<in> lvars (\<T> ?s)"
then show ?thesis
using \<open>\<not> \<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)\<close> \<open>\<not> \<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x)\<close>
using assms(4) assms(6)
by auto
next
assume "\<not> (lt dir) c (\<langle>\<V> s\<rangle> x)"
then show ?thesis
using \<open>\<not> \<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)\<close> \<open>\<not> \<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x)\<close>
using assms(5) assms(6)
by simp
qed
qed
qed
qed
lemma assert_bound_cases:
assumes "\<And> c x dir.
\<lbrakk> dir = Positive \<or> dir = Negative;
a = LE dir x c;
\<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)
\<rbrakk> \<Longrightarrow>
P' (lt dir) (UBI dir) (LBI dir) (UB dir) (LB dir) (UBI_upd dir) (UI dir) (LI dir) (LE dir) (GE dir) s"
assumes "\<And> c x dir.
\<lbrakk>dir = Positive \<or> dir = Negative;
a = LE dir x c;
\<not> \<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x); \<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x)
\<rbrakk> \<Longrightarrow>
P' (lt dir) (UBI dir) (LBI dir) (UB dir) (LB dir) (UBI_upd dir) (UI dir) (LI dir) (LE dir) (GE dir)
(set_unsat [i, ((LI dir) s x)] (update\<B>\<I> (UBI_upd dir) i x c s))"
assumes "\<And> c x dir.
\<lbrakk> dir = Positive \<or> dir = Negative;
a = LE dir x c;
x \<notin> lvars (\<T> s); (lt dir) c (\<langle>\<V> s\<rangle> x);
\<not> (\<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)); \<not> (\<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x))
\<rbrakk> \<Longrightarrow>
P' (lt dir) (UBI dir) (LBI dir) (UB dir) (LB dir) (UBI_upd dir) (UI dir) (LI dir) (LE dir) (GE dir)
(update x c ((update\<B>\<I> (UBI_upd dir) i x c s)))"
assumes "\<And> c x dir.
\<lbrakk> dir = Positive \<or> dir = Negative;
a = LE dir x c;
x \<in> lvars (\<T> s); \<not> (\<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x));
\<not> (\<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x))
\<rbrakk> \<Longrightarrow>
P' (lt dir) (UBI dir) (LBI dir) (UB dir) (LB dir) (UBI_upd dir) (UI dir) (LI dir) (LE dir) (GE dir)
((update\<B>\<I> (UBI_upd dir) i x c s))"
assumes "\<And> c x dir.
\<lbrakk> dir = Positive \<or> dir = Negative;
a = LE dir x c;
\<not> (\<unrhd>\<^sub>u\<^sub>b (lt dir) c ((UB dir) s x)); \<not> (\<lhd>\<^sub>l\<^sub>b (lt dir) c ((LB dir) s x));
\<not> ((lt dir) c (\<langle>\<V> s\<rangle> x))
\<rbrakk> \<Longrightarrow>
P' (lt dir) (UBI dir) (LBI dir) (UB dir) (LB dir) (UBI_upd dir) (UI dir) (LI dir) (LE dir) (GE dir)
((update\<B>\<I> (UBI_upd dir) i x c s))"
assumes "\<And> s. P s = P' (>) \<B>\<^sub>i\<^sub>l \<B>\<^sub>i\<^sub>u \<B>\<^sub>l \<B>\<^sub>u \<B>\<^sub>i\<^sub>l_update \<I>\<^sub>l \<I>\<^sub>u Geq Leq s"
assumes "\<And> s. P s = P' (<) \<B>\<^sub>i\<^sub>u \<B>\<^sub>i\<^sub>l \<B>\<^sub>u \<B>\<^sub>l \<B>\<^sub>i\<^sub>u_update \<I>\<^sub>u \<I>\<^sub>l Leq Geq s"
shows "P (assert_bound (i,a) s)"
proof (cases a)
case (Leq x c)
then show ?thesis
apply (simp del: assert_bound'_def)
apply (rule assert_bound'_cases, simp_all)
using assms(1)[of Positive x c]
using assms(2)[of Positive x c]
using assms(3)[of Positive x c]
using assms(4)[of Positive x c]
using assms(5)[of Positive x c]
using assms(7)
by auto
next
case (Geq x c)
then show ?thesis
apply (simp del: assert_bound'_def)
apply (rule assert_bound'_cases)
using assms(1)[of Negative x c]
using assms(2)[of Negative x c]
using assms(3)[of Negative x c]
using assms(4)[of Negative x c]
using assms(5)[of Negative x c]
using assms(6)
by auto
qed
end
lemma set_unsat_bounds_id: "\<B> (set_unsat I s) = \<B> s"
unfolding boundsl_def boundsu_def by auto
lemma decrease_ub_satisfied_inverse:
assumes lt: "\<lhd>\<^sub>u\<^sub>b (lt dir) c (UB dir s x)" and dir: "dir = Positive \<or> dir = Negative"
assumes v: "v \<Turnstile>\<^sub>b \<B> (update\<B>\<I> (UBI_upd dir) i x c s)"
shows "v \<Turnstile>\<^sub>b \<B> s"
unfolding satisfies_bounds.simps
proof
fix x'
show "in_bounds x' v (\<B> s)"
proof (cases "x = x'")
case False
then show ?thesis
using v dir
unfolding satisfies_bounds.simps
by (auto split: if_splits simp: boundsl_def boundsu_def)
next
case True
then show ?thesis
using v dir
unfolding satisfies_bounds.simps
using lt
by (erule_tac x="x'" in allE)
(auto simp add: lt_ubound_def[THEN sym] gt_lbound_def[THEN sym] compare_strict_nonstrict
boundsl_def boundsu_def)
qed
qed
lemma atoms_equiv_bounds_extend:
fixes x c dir
assumes "dir = Positive \<or> dir = Negative" "\<not> \<unrhd>\<^sub>u\<^sub>b (lt dir) c (UB dir s x)" "ats \<doteq> \<B> s"
shows "(ats \<union> {LE dir x c}) \<doteq> \<B> (update\<B>\<I> (UBI_upd dir) i x c s)"
unfolding atoms_equiv_bounds.simps
proof
fix v
let ?s = "update\<B>\<I> (UBI_upd dir) i x c s"
show "v \<Turnstile>\<^sub>a\<^sub>s (ats \<union> {LE dir x c}) = v \<Turnstile>\<^sub>b \<B> ?s"
proof
assume "v \<Turnstile>\<^sub>a\<^sub>s (ats \<union> {LE dir x c})"
then have "v \<Turnstile>\<^sub>a\<^sub>s ats" "le (lt dir) (v x) c"
using \<open>dir = Positive \<or> dir = Negative\<close>
unfolding satisfies_atom_set_def
by auto
show "v \<Turnstile>\<^sub>b \<B> ?s"
unfolding satisfies_bounds.simps
proof
fix x'
show "in_bounds x' v (\<B> ?s)"
using \<open>v \<Turnstile>\<^sub>a\<^sub>s ats\<close> \<open>le (lt dir) (v x) c\<close> \<open>ats \<doteq> \<B> s\<close>
using \<open>dir = Positive \<or> dir = Negative\<close>
unfolding atoms_equiv_bounds.simps satisfies_bounds.simps
by (cases "x = x'") (auto simp: boundsl_def boundsu_def)
qed
next
assume "v \<Turnstile>\<^sub>b \<B> ?s"
then have "v \<Turnstile>\<^sub>b \<B> s"
using \<open>\<not> \<unrhd>\<^sub>u\<^sub>b (lt dir) c (UB dir s x)\<close>
using \<open>dir = Positive \<or> dir = Negative\<close>
using decrease_ub_satisfied_inverse[of dir c s x v]
using neg_bounds_compare(1)[of c "\<B>\<^sub>u s x"]
using neg_bounds_compare(5)[of c "\<B>\<^sub>l s x"]
by (auto simp add: lt_ubound_def[THEN sym] ge_ubound_def[THEN sym] le_lbound_def[THEN sym] gt_lbound_def[THEN sym])
show "v \<Turnstile>\<^sub>a\<^sub>s (ats \<union> {LE dir x c})"
unfolding satisfies_atom_set_def
proof
fix a
assume "a \<in> ats \<union> {LE dir x c}"
then show "v \<Turnstile>\<^sub>a a"
proof
assume "a \<in> {LE dir x c}"
then show ?thesis
using \<open>v \<Turnstile>\<^sub>b \<B> ?s\<close>
using \<open>dir = Positive \<or> dir = Negative\<close>
unfolding satisfies_bounds.simps
by (auto split: if_splits simp: boundsl_def boundsu_def)
next
assume "a \<in> ats"
then show ?thesis
using \<open>ats \<doteq> \<B> s\<close>
using \<open>v \<Turnstile>\<^sub>b \<B> s\<close>
unfolding atoms_equiv_bounds.simps satisfies_atom_set_def
by auto
qed
qed
qed
qed
lemma bounds_updates: "\<B>\<^sub>l (\<B>\<^sub>i\<^sub>u_update u s) = \<B>\<^sub>l s"
"\<B>\<^sub>u (\<B>\<^sub>i\<^sub>l_update u s) = \<B>\<^sub>u s"
"\<B>\<^sub>u (\<B>\<^sub>i\<^sub>u_update (upd x (i,c)) s) = (\<B>\<^sub>u s) (x \<mapsto> c)"
"\<B>\<^sub>l (\<B>\<^sub>i\<^sub>l_update (upd x (i,c)) s) = (\<B>\<^sub>l s) (x \<mapsto> c)"
by (auto simp: boundsl_def boundsu_def)
locale EqForLVar =
fixes eq_idx_for_lvar :: "tableau \<Rightarrow> var \<Rightarrow> nat"
assumes eq_idx_for_lvar:
"\<lbrakk>x \<in> lvars t\<rbrakk> \<Longrightarrow> eq_idx_for_lvar t x < length t \<and> lhs (t ! eq_idx_for_lvar t x) = x"
begin
definition eq_for_lvar :: "tableau \<Rightarrow> var \<Rightarrow> eq" where
"eq_for_lvar t v \<equiv> t ! (eq_idx_for_lvar t v)"
lemma eq_for_lvar:
"\<lbrakk>x \<in> lvars t\<rbrakk> \<Longrightarrow> eq_for_lvar t x \<in> set t \<and> lhs (eq_for_lvar t x) = x"
unfolding eq_for_lvar_def
using eq_idx_for_lvar
by auto
abbreviation rvars_of_lvar where
"rvars_of_lvar t x \<equiv> rvars_eq (eq_for_lvar t x)"
lemma rvars_of_lvar_rvars:
assumes "x \<in> lvars t"
shows "rvars_of_lvar t x \<subseteq> rvars t"
using assms eq_for_lvar[of x t]
unfolding rvars_def
by auto
end
text \<open>Updating changes the value of \<open>x\<close> and then updates
values of all lhs variables so that the tableau remains
satisfied. This can be based on a function that recalculates rhs
polynomial values in the changed valuation:\<close>
locale RhsEqVal = fixes rhs_eq_val::"(var, 'a::lrv) mapping \<Rightarrow> var \<Rightarrow> 'a \<Rightarrow> eq \<Rightarrow> 'a"
\<comment> \<open>@{text rhs_eq_val} computes the value of the rhs of @{text e} in @{text "\<langle>v\<rangle>(x := c)"}.\<close>
assumes rhs_eq_val: "\<langle>v\<rangle> \<Turnstile>\<^sub>e e \<Longrightarrow> rhs_eq_val v x c e = rhs e \<lbrace> \<langle>v\<rangle> (x := c) \<rbrace>"
begin
text\<open>\noindent Then, the next implementation of \<open>update\<close>
satisfies its specification:\<close>
abbreviation update_eq where
"update_eq v x c v' e \<equiv> upd (lhs e) (rhs_eq_val v x c e) v'"
definition update :: "var \<Rightarrow> 'a \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state" where
"update x c s \<equiv> \<V>_update (upd x c (foldl (update_eq (\<V> s) x c) (\<V> s) (\<T> s))) s"
lemma update_no_set_none:
shows "look (\<V> s) y \<noteq> None \<Longrightarrow>
look (foldl (update_eq (\<V> s) x v) (\<V> s) t) y \<noteq> None"
by (induct t rule: rev_induct, auto simp: lookup_update')
lemma update_no_left:
assumes "y \<notin> lvars t"
shows "look (\<V> s) y = look (foldl (update_eq (\<V> s) x v) (\<V> s) t) y"
using assms
by (induct t rule: rev_induct) (auto simp add: lvars_def lookup_update')
lemma update_left:
assumes "y \<in> lvars t"
shows "\<exists> eq \<in> set t. lhs eq = y \<and>
look (foldl (update_eq (\<V> s) x v) (\<V> s) t) y = Some (rhs_eq_val (\<V> s) x v eq)"
using assms
by (induct t rule: rev_induct) (auto simp add: lvars_def lookup_update')
lemma update_valuate_rhs:
assumes "e \<in> set (\<T> s)" "\<triangle> (\<T> s)"
shows "rhs e \<lbrace> \<langle>\<V> (update x c s)\<rangle> \<rbrace> = rhs e \<lbrace> \<langle>\<V> s\<rangle> (x := c) \<rbrace>"
proof (rule valuate_depend, safe)
fix y
assume "y \<in> rvars_eq e"
then have "y \<notin> lvars (\<T> s)"
using \<open>\<triangle> (\<T> s)\<close> \<open>e \<in> set (\<T> s)\<close>
by (auto simp add: normalized_tableau_def rvars_def)
then show "\<langle>\<V> (update x c s)\<rangle> y = (\<langle>\<V> s\<rangle>(x := c)) y"
using update_no_left[of y "\<T> s" s x c]
by (auto simp add: update_def map2fun_def lookup_update')
qed
end
sublocale RhsEqVal < Update update
proof
fix s::"('i,'a) state" and x c
show "let s' = update x c s in \<T> s' = \<T> s \<and> \<B>\<^sub>i s' = \<B>\<^sub>i s \<and> \<U> s' = \<U> s \<and> \<U>\<^sub>c s' = \<U>\<^sub>c s"
by (simp add: Let_def update_def add: boundsl_def boundsu_def indexl_def indexu_def)
next
fix s::"('i,'a) state" and x c
assume "\<triangle> (\<T> s)" "\<nabla> s" "x \<notin> lvars (\<T> s)"
then show "\<nabla> (update x c s)"
using update_no_set_none[of s]
by (simp add: Let_def update_def tableau_valuated_def lookup_update')
next
fix s::"('i,'a) state" and x x' c
assume "\<triangle> (\<T> s)" "\<nabla> s" "x \<notin> lvars (\<T> s)"
show "x' \<notin> lvars (\<T> s) \<longrightarrow>
look (\<V> (update x c s)) x' =
(if x = x' then Some c else look (\<V> s) x')"
using update_no_left[of x' "\<T> s" s x c]
unfolding update_def lvars_def Let_def
by (auto simp: lookup_update')
next
fix s::"('i,'a) state" and x c
assume "\<triangle> (\<T> s)" "\<nabla> s" "x \<notin> lvars (\<T> s)"
have "\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s \<Longrightarrow> \<forall>e \<in> set (\<T> s). \<langle>\<V> (update x c s)\<rangle> \<Turnstile>\<^sub>e e"
proof
fix e
assume "e \<in> set (\<T> s)" "\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s"
then have "\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>e e"
by (simp add: satisfies_tableau_def)
have "x \<noteq> lhs e"
using \<open>x \<notin> lvars (\<T> s)\<close> \<open>e \<in> set (\<T> s)\<close>
by (auto simp add: lvars_def)
then have "\<langle>\<V> (update x c s)\<rangle> (lhs e) = rhs_eq_val (\<V> s) x c e"
using update_left[of "lhs e" "\<T> s" s x c] \<open>e \<in> set (\<T> s)\<close> \<open>\<triangle> (\<T> s)\<close>
by (auto simp add: lvars_def lookup_update' update_def Let_def map2fun_def normalized_tableau_def distinct_map inj_on_def)
then show "\<langle>\<V> (update x c s)\<rangle> \<Turnstile>\<^sub>e e"
using \<open>\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>e e\<close> \<open>e \<in> set (\<T> s)\<close> \<open>x \<notin> lvars (\<T> s)\<close> \<open>\<triangle> (\<T> s)\<close>
using rhs_eq_val
by (simp add: satisfies_eq_def update_valuate_rhs)
qed
then show "\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s \<longrightarrow> \<langle>\<V> (update x c s)\<rangle> \<Turnstile>\<^sub>t \<T> s"
by(simp add: satisfies_tableau_def update_def)
qed
text\<open>To update the valuation for a variable that is on the lhs of
the tableau it should first be swapped with some rhs variable of its
equation, in an operation called \emph{pivoting}. Pivoting has the
precondition that the tableau is normalized and that it is always
called for a lhs variable of the tableau, and a rhs variable in the
equation with that lhs variable. The set of rhs variables for the
given lhs variable is found using the \<open>rvars_of_lvar\<close> function
(specified in a very simple locale \<open>EqForLVar\<close>, that we do not
print).\<close>
locale Pivot = EqForLVar + fixes pivot::"var \<Rightarrow> var \<Rightarrow> ('i,'a::lrv) state \<Rightarrow> ('i,'a) state"
assumes
\<comment> \<open>Valuation, bounds, and the unsatisfiability flag are not changed.\<close>
pivot_id: "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
let s' = pivot x\<^sub>i x\<^sub>j s in \<V> s' = \<V> s \<and> \<B>\<^sub>i s' = \<B>\<^sub>i s \<and> \<U> s' = \<U> s \<and> \<U>\<^sub>c s' = \<U>\<^sub>c s" and
\<comment> \<open>The tableau remains equivalent to the previous one and normalized.\<close>
pivot_tableau: "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
let s' = pivot x\<^sub>i x\<^sub>j s in ((v::'a valuation) \<Turnstile>\<^sub>t \<T> s \<longleftrightarrow> v \<Turnstile>\<^sub>t \<T> s') \<and> \<triangle> (\<T> s') " and
\<comment> \<open>@{text "x\<^sub>i"} and @{text "x\<^sub>j"} are swapped, while the other variables do not change sides.\<close>
pivot_vars': "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow> let s' = pivot x\<^sub>i x\<^sub>j s in
rvars(\<T> s') = rvars(\<T> s)-{x\<^sub>j}\<union>{x\<^sub>i} \<and> lvars(\<T> s') = lvars(\<T> s)-{x\<^sub>i}\<union>{x\<^sub>j}"
begin
lemma pivot_bounds_id: "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
\<B>\<^sub>i (pivot x\<^sub>i x\<^sub>j s) = \<B>\<^sub>i s"
using pivot_id
by (simp add: Let_def)
lemma pivot_bounds_id': assumes "\<triangle> (\<T> s)" "x\<^sub>i \<in> lvars (\<T> s)" "x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i"
shows "\<B>\<I> (pivot x\<^sub>i x\<^sub>j s) = \<B>\<I> s" "\<B> (pivot x\<^sub>i x\<^sub>j s) = \<B> s" "\<I> (pivot x\<^sub>i x\<^sub>j s) = \<I> s"
using pivot_bounds_id[OF assms]
by (auto simp: indexl_def indexu_def boundsl_def boundsu_def)
lemma pivot_valuation_id: "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow> \<V> (pivot x\<^sub>i x\<^sub>j s) = \<V> s"
using pivot_id
by (simp add: Let_def)
lemma pivot_unsat_id: "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow> \<U> (pivot x\<^sub>i x\<^sub>j s) = \<U> s"
using pivot_id
by (simp add: Let_def)
lemma pivot_unsat_core_id: "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow> \<U>\<^sub>c (pivot x\<^sub>i x\<^sub>j s) = \<U>\<^sub>c s"
using pivot_id
by (simp add: Let_def)
lemma pivot_tableau_equiv: "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
(v::'a valuation) \<Turnstile>\<^sub>t \<T> s = v \<Turnstile>\<^sub>t \<T> (pivot x\<^sub>i x\<^sub>j s)"
using pivot_tableau
by (simp add: Let_def)
lemma pivot_tableau_normalized: "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow> \<triangle> (\<T> (pivot x\<^sub>i x\<^sub>j s))"
using pivot_tableau
by (simp add: Let_def)
lemma pivot_rvars: "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow> rvars (\<T> (pivot x\<^sub>i x\<^sub>j s)) = rvars (\<T> s) - {x\<^sub>j} \<union> {x\<^sub>i}"
using pivot_vars'
by (simp add: Let_def)
lemma pivot_lvars: "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow> lvars (\<T> (pivot x\<^sub>i x\<^sub>j s)) = lvars (\<T> s) - {x\<^sub>i} \<union> {x\<^sub>j}"
using pivot_vars'
by (simp add: Let_def)
lemma pivot_vars:
"\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow> tvars (\<T> (pivot x\<^sub>i x\<^sub>j s)) = tvars (\<T> s) "
using pivot_lvars[of s x\<^sub>i x\<^sub>j] pivot_rvars[of s x\<^sub>i x\<^sub>j]
using rvars_of_lvar_rvars[of x\<^sub>i "\<T> s"]
by auto
lemma
pivot_tableau_valuated: "\<lbrakk>\<triangle> (\<T> s); x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i; \<nabla> s\<rbrakk> \<Longrightarrow> \<nabla> (pivot x\<^sub>i x\<^sub>j s)"
using pivot_valuation_id pivot_vars
by (auto simp add: tableau_valuated_def)
end
text\<open>Functions \<open>pivot\<close> and \<open>update\<close> can be used to
implement the \<open>check\<close> function. In its context, \<open>pivot\<close>
and \<open>update\<close> functions are always called together, so the
following definition can be used: @{prop "pivot_and_update x\<^sub>i x\<^sub>j c s =
update x\<^sub>i c (pivot x\<^sub>i x\<^sub>j s)"}. It is possible to make a more efficient
implementation of \<open>pivot_and_update\<close> that does not use separate
implementations of \<open>pivot\<close> and \<open>update\<close>. To allow this, a
separate specification for \<open>pivot_and_update\<close> can be given. It can be
easily shown that the \<open>pivot_and_update\<close> definition above
satisfies this specification.\<close>
locale PivotAndUpdate = EqForLVar +
fixes pivot_and_update :: "var \<Rightarrow> var \<Rightarrow> 'a::lrv \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state"
assumes pivotandupdate_unsat_id: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
\<U> (pivot_and_update x\<^sub>i x\<^sub>j c s) = \<U> s"
assumes pivotandupdate_unsat_core_id: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
\<U>\<^sub>c (pivot_and_update x\<^sub>i x\<^sub>j c s) = \<U>\<^sub>c s"
assumes pivotandupdate_bounds_id: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
\<B>\<^sub>i (pivot_and_update x\<^sub>i x\<^sub>j c s) = \<B>\<^sub>i s"
assumes pivotandupdate_tableau_normalized: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
\<triangle> (\<T> (pivot_and_update x\<^sub>i x\<^sub>j c s))"
assumes pivotandupdate_tableau_equiv: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
(v::'a valuation) \<Turnstile>\<^sub>t \<T> s \<longleftrightarrow> v \<Turnstile>\<^sub>t \<T> (pivot_and_update x\<^sub>i x\<^sub>j c s)"
assumes pivotandupdate_satisfies_tableau: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s \<longrightarrow> \<langle>\<V> (pivot_and_update x\<^sub>i x\<^sub>j c s)\<rangle> \<Turnstile>\<^sub>t \<T> s"
assumes pivotandupdate_rvars: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
rvars (\<T> (pivot_and_update x\<^sub>i x\<^sub>j c s)) = rvars (\<T> s) - {x\<^sub>j} \<union> {x\<^sub>i}"
assumes pivotandupdate_lvars: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
lvars (\<T> (pivot_and_update x\<^sub>i x\<^sub>j c s)) = lvars (\<T> s) - {x\<^sub>i} \<union> {x\<^sub>j}"
assumes pivotandupdate_valuation_nonlhs: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
x \<notin> lvars (\<T> s) - {x\<^sub>i} \<union> {x\<^sub>j} \<longrightarrow> look (\<V> (pivot_and_update x\<^sub>i x\<^sub>j c s)) x = (if x = x\<^sub>i then Some c else look (\<V> s) x)"
assumes pivotandupdate_tableau_valuated: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow>
\<nabla> (pivot_and_update x\<^sub>i x\<^sub>j c s)"
begin
lemma pivotandupdate_bounds_id': assumes "\<triangle> (\<T> s)" "\<nabla> s" "x\<^sub>i \<in> lvars (\<T> s)" "x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i"
shows "\<B>\<I> (pivot_and_update x\<^sub>i x\<^sub>j c s) = \<B>\<I> s"
"\<B> (pivot_and_update x\<^sub>i x\<^sub>j c s) = \<B> s"
"\<I> (pivot_and_update x\<^sub>i x\<^sub>j c s) = \<I> s"
using pivotandupdate_bounds_id[OF assms]
by (auto simp: indexl_def indexu_def boundsl_def boundsu_def)
lemma pivotandupdate_valuation_xi: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i\<rbrakk> \<Longrightarrow> look (\<V> (pivot_and_update x\<^sub>i x\<^sub>j c s)) x\<^sub>i = Some c"
using pivotandupdate_valuation_nonlhs[of s x\<^sub>i x\<^sub>j x\<^sub>i c]
using rvars_of_lvar_rvars
by (auto simp add: normalized_tableau_def)
lemma pivotandupdate_valuation_other_nolhs: "\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i; x \<notin> lvars (\<T> s); x \<noteq> x\<^sub>j\<rbrakk> \<Longrightarrow> look (\<V> (pivot_and_update x\<^sub>i x\<^sub>j c s)) x = look (\<V> s) x"
using pivotandupdate_valuation_nonlhs[of s x\<^sub>i x\<^sub>j x c]
by auto
lemma pivotandupdate_nolhs:
"\<lbrakk> \<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i;
\<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<B>\<^sub>l s x\<^sub>i = Some c \<or> \<B>\<^sub>u s x\<^sub>i = Some c\<rbrakk> \<Longrightarrow>
\<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s (pivot_and_update x\<^sub>i x\<^sub>j c s)"
using pivotandupdate_satisfies_tableau[of s x\<^sub>i x\<^sub>j c]
using pivotandupdate_tableau_equiv[of s x\<^sub>i x\<^sub>j _ c]
using pivotandupdate_valuation_xi[of s x\<^sub>i x\<^sub>j c]
using pivotandupdate_valuation_other_nolhs[of s x\<^sub>i x\<^sub>j _ c]
using pivotandupdate_lvars[of s x\<^sub>i x\<^sub>j c]
by (auto simp add: curr_val_satisfies_no_lhs_def satisfies_bounds.simps satisfies_bounds_set.simps
bounds_consistent_geq_lb bounds_consistent_leq_ub map2fun_def pivotandupdate_bounds_id')
lemma pivotandupdate_bounds_consistent:
assumes "\<triangle> (\<T> s)" "\<nabla> s" "x\<^sub>i \<in> lvars (\<T> s)" "x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i"
shows "\<diamond> (pivot_and_update x\<^sub>i x\<^sub>j c s) = \<diamond> s"
using assms pivotandupdate_bounds_id'[of s x\<^sub>i x\<^sub>j c]
by (simp add: bounds_consistent_def)
end
locale PivotUpdate = Pivot eq_idx_for_lvar pivot + Update update for
eq_idx_for_lvar :: "tableau \<Rightarrow> var \<Rightarrow> nat" and
pivot :: "var \<Rightarrow> var \<Rightarrow> ('i,'a::lrv) state \<Rightarrow> ('i,'a) state" and
update :: "var \<Rightarrow> 'a \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state"
begin
definition pivot_and_update :: "var \<Rightarrow> var \<Rightarrow> 'a \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state" where [simp]:
"pivot_and_update x\<^sub>i x\<^sub>j c s \<equiv> update x\<^sub>i c (pivot x\<^sub>i x\<^sub>j s)"
lemma pivot_update_precond:
assumes "\<triangle> (\<T> s)" "x\<^sub>i \<in> lvars (\<T> s)" "x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i"
shows "\<triangle> (\<T> (pivot x\<^sub>i x\<^sub>j s))" "x\<^sub>i \<notin> lvars (\<T> (pivot x\<^sub>i x\<^sub>j s))"
proof-
from assms have "x\<^sub>i \<noteq> x\<^sub>j"
using rvars_of_lvar_rvars[of x\<^sub>i "\<T> s"]
by (auto simp add: normalized_tableau_def)
then show "\<triangle> (\<T> (pivot x\<^sub>i x\<^sub>j s))" "x\<^sub>i \<notin> lvars (\<T> (pivot x\<^sub>i x\<^sub>j s))"
using assms
using pivot_tableau_normalized[of s x\<^sub>i x\<^sub>j]
using pivot_lvars[of s x\<^sub>i x\<^sub>j]
by auto
qed
end
sublocale PivotUpdate < PivotAndUpdate eq_idx_for_lvar pivot_and_update
using pivot_update_precond
using update_unsat_id pivot_unsat_id pivot_unsat_core_id update_bounds_id pivot_bounds_id
update_tableau_id pivot_tableau_normalized pivot_tableau_equiv update_satisfies_tableau
pivot_valuation_id pivot_lvars pivot_rvars update_valuation_nonlhs update_valuation_nonlhs
pivot_tableau_valuated update_tableau_valuated update_unsat_core_id
by (unfold_locales, auto)
text\<open>Given the @{term update} function, \<open>assert_bound\<close> can be
implemented as follows.
\vspace{-2mm}
@{text[display]
"assert_bound (Leq x c) s \<equiv>
if c \<ge>\<^sub>u\<^sub>b \<B>\<^sub>u s x then s
else let s' = s \<lparr> \<B>\<^sub>u := (\<B>\<^sub>u s) (x := Some c) \<rparr>
in if c <\<^sub>l\<^sub>b \<B>\<^sub>l s x then s' \<lparr> \<U> := True \<rparr>
else if x \<notin> lvars (\<T> s') \<and> c < \<langle>\<V> s\<rangle> x then update x c s' else s'"
}
\vspace{-2mm}
\noindent The case of \<open>Geq x c\<close> atoms is analogous (a systematic way to
avoid symmetries is discussed in Section \ref{sec:symmetries}). This
implementation satisfies both its specifications.
\<close>
lemma indices_state_set_unsat: "indices_state (set_unsat I s) = indices_state s"
by (cases s, auto simp: indices_state_def)
lemma \<B>\<I>_set_unsat: "\<B>\<I> (set_unsat I s) = \<B>\<I> s"
by (cases s, auto simp: boundsl_def boundsu_def indexl_def indexu_def)
lemma satisfies_tableau_cong: assumes "\<And> x. x \<in> tvars t \<Longrightarrow> v x = w x"
shows "(v \<Turnstile>\<^sub>t t) = (w \<Turnstile>\<^sub>t t)"
unfolding satisfies_tableau_def satisfies_eq_def
by (intro ball_cong[OF refl] arg_cong2[of _ _ _ _ "(=)"] valuate_depend,
insert assms, auto simp: lvars_def rvars_def)
lemma satisfying_state_valuation_to_atom_tabl: assumes J: "J \<subseteq> indices_state s"
and model: "(J, v) \<Turnstile>\<^sub>i\<^sub>s\<^sub>e s"
and ivalid: "index_valid as s"
and dist: "distinct_indices_atoms as"
shows "(J, v) \<Turnstile>\<^sub>i\<^sub>a\<^sub>e\<^sub>s as" "v \<Turnstile>\<^sub>t \<T> s"
unfolding i_satisfies_atom_set'.simps
proof (intro ballI)
from model[unfolded satisfies_state_index'.simps]
have model: "v \<Turnstile>\<^sub>t \<T> s" "(J, v) \<Turnstile>\<^sub>i\<^sub>b\<^sub>e \<B>\<I> s" by auto
show "v \<Turnstile>\<^sub>t \<T> s" by fact
fix a
assume "a \<in> restrict_to J as"
then obtain i where iJ: "i \<in> J" and mem: "(i,a) \<in> as" by auto
with J have "i \<in> indices_state s" by auto
from this[unfolded indices_state_def] obtain x c where
look: "look (\<B>\<^sub>i\<^sub>l s) x = Some (i, c) \<or> look (\<B>\<^sub>i\<^sub>u s) x = Some (i, c)" by auto
with ivalid[unfolded index_valid_def]
obtain b where "(i,b) \<in> as" "atom_var b = x" "atom_const b = c" by force
with dist[unfolded distinct_indices_atoms_def, rule_format, OF this(1) mem]
have a: "atom_var a = x" "atom_const a = c" by auto
from model(2)[unfolded satisfies_bounds_index'.simps] look iJ have "v x = c"
by (auto simp: boundsu_def boundsl_def indexu_def indexl_def)
thus "v \<Turnstile>\<^sub>a\<^sub>e a" unfolding satisfies_atom'_def a .
qed
text \<open>Note that in order to ensure minimality of the unsat cores, pivoting is required.\<close>
sublocale AssertAllState < AssertAll assert_all
proof
fix t as v I
assume D: "\<triangle> t"
from D show "assert_all t as = Sat v \<Longrightarrow> \<langle>v\<rangle> \<Turnstile>\<^sub>t t \<and> \<langle>v\<rangle> \<Turnstile>\<^sub>a\<^sub>s flat (set as)"
unfolding Let_def assert_all_def
using assert_all_state_tableau_equiv[OF D refl]
using assert_all_state_sat[OF D refl]
using assert_all_state_sat_atoms_equiv_bounds[OF D refl, of as]
unfolding atoms_equiv_bounds.simps curr_val_satisfies_state_def satisfies_state_def satisfies_atom_set_def
by (auto simp: Let_def split: if_splits)
let ?s = "assert_all_state t as"
assume "assert_all t as = Unsat I"
then have i: "I = the (\<U>\<^sub>c ?s)" and U: "\<U> ?s"
unfolding assert_all_def Let_def by (auto split: if_splits)
from assert_all_index_valid[OF D refl, of as] have ivalid: "index_valid (set as) ?s" .
note unsat = assert_all_state_unsat[OF D refl U, unfolded minimal_unsat_state_core_def unsat_state_core_def i[symmetric]]
from unsat have "set I \<subseteq> indices_state ?s" by auto
also have "\<dots> \<subseteq> fst ` set as" using assert_all_state_indices[OF D refl] .
finally have indices: "set I \<subseteq> fst ` set as" .
show "minimal_unsat_core_tabl_atoms (set I) t (set as)"
unfolding minimal_unsat_core_tabl_atoms_def
proof (intro conjI impI allI indices, clarify)
fix v
assume model: "v \<Turnstile>\<^sub>t t" "(set I, v) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as"
from unsat have no_model: "\<not> ((set I, v) \<Turnstile>\<^sub>i\<^sub>s ?s)" by auto
from assert_all_state_unsat_atoms_equiv_bounds[OF D refl U]
have equiv: "set as \<Turnstile>\<^sub>i \<B>\<I> ?s" by auto
from assert_all_state_tableau_equiv[OF D refl, of v] model
have model_t: "v \<Turnstile>\<^sub>t \<T> ?s" by auto
have model_as': "(set I, v) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as"
using model(2) by (auto simp: satisfies_atom_set_def)
with equiv model_t have "(set I, v) \<Turnstile>\<^sub>i\<^sub>s ?s"
unfolding satisfies_state_index.simps atoms_imply_bounds_index.simps by simp
with no_model show False by simp
next
fix J
assume dist: "distinct_indices_atoms (set as)" and J: "J \<subset> set I"
from J unsat[unfolded subsets_sat_core_def, folded i]
have J': "J \<subseteq> indices_state ?s" by auto
from index_valid_distinct_indices[OF ivalid dist] J unsat[unfolded subsets_sat_core_def, folded i]
obtain v where model: "(J, v) \<Turnstile>\<^sub>i\<^sub>s\<^sub>e ?s" by blast
have "(J, v) \<Turnstile>\<^sub>i\<^sub>a\<^sub>e\<^sub>s set as" "v \<Turnstile>\<^sub>t t"
using satisfying_state_valuation_to_atom_tabl[OF J' model ivalid dist]
assert_all_state_tableau_equiv[OF D refl] by auto
then show "\<exists> v. v \<Turnstile>\<^sub>t t \<and> (J, v) \<Turnstile>\<^sub>i\<^sub>a\<^sub>e\<^sub>s set as" by blast
qed
qed
lemma (in Update) update_to_assert_bound_no_lhs: assumes pivot: "Pivot eqlvar (pivot :: var \<Rightarrow> var \<Rightarrow> ('i,'a) state \<Rightarrow> ('i,'a) state)"
shows "AssertBoundNoLhs assert_bound"
proof
fix s::"('i,'a) state" and a
assume "\<not> \<U> s" "\<triangle> (\<T> s)" "\<nabla> s"
then show "\<T> (assert_bound a s) = \<T> s"
by (cases a, cases "snd a") (auto simp add: Let_def update_tableau_id tableau_valuated_def)
next
fix s::"('i,'a) state" and ia and as
assume *: "\<not> \<U> s" "\<triangle> (\<T> s)" "\<nabla> s" and **: "\<U> (assert_bound ia s)"
and index: "index_valid as s"
and consistent: "\<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s" "\<diamond> s"
obtain i a where ia: "ia = (i,a)" by force
let ?modelU = "\<lambda> lt UB UI s v x c i. UB s x = Some c \<longrightarrow> UI s x = i \<longrightarrow> i \<in> set (the (\<U>\<^sub>c s)) \<longrightarrow> (lt (v x) c \<or> v x = c)"
let ?modelL = "\<lambda> lt LB LI s v x c i. LB s x = Some c \<longrightarrow> LI s x = i \<longrightarrow> i \<in> set (the (\<U>\<^sub>c s)) \<longrightarrow> (lt c (v x) \<or> c = v x)"
let ?modelIU = "\<lambda> I lt UB UI s v x c i. UB s x = Some c \<longrightarrow> UI s x = i \<longrightarrow> i \<in> I \<longrightarrow> (v x = c)"
let ?modelIL = "\<lambda> I lt LB LI s v x c i. LB s x = Some c \<longrightarrow> LI s x = i \<longrightarrow> i \<in> I \<longrightarrow> (v x = c)"
let ?P' = "\<lambda> lt UBI LBI UB LB UBI_upd UI LI LE GE s.
\<U> s \<longrightarrow> (set (the (\<U>\<^sub>c s)) \<subseteq> indices_state s \<and> \<not> (\<exists>v. (v \<Turnstile>\<^sub>t \<T> s
\<and> (\<forall> x c i. ?modelU lt UB UI s v x c i)
\<and> (\<forall> x c i. ?modelL lt LB LI s v x c i))))
\<and> (distinct_indices_state s \<longrightarrow> (\<forall> I. I \<subset> set (the (\<U>\<^sub>c s)) \<longrightarrow> (\<exists> v. v \<Turnstile>\<^sub>t \<T> s \<and>
(\<forall> x c i. ?modelIU I lt UB UI s v x c i) \<and> (\<forall> x c i. ?modelIL I lt LB LI s v x c i))))"
have "\<U> (assert_bound ia s) \<longrightarrow> (unsat_state_core (assert_bound ia s) \<and>
(distinct_indices_state (assert_bound ia s) \<longrightarrow> subsets_sat_core (assert_bound ia s)))" (is "?P (assert_bound ia s)") unfolding ia
proof (rule assert_bound_cases[of _ _ ?P'])
fix s' :: "('i,'a) state"
have id: "((x :: 'a) < y \<or> x = y) \<longleftrightarrow> x \<le> y" "((x :: 'a) > y \<or> x = y) \<longleftrightarrow> x \<ge> y" for x y by auto
have id': "?P' (>) \<B>\<^sub>i\<^sub>l \<B>\<^sub>i\<^sub>u \<B>\<^sub>l \<B>\<^sub>u undefined \<I>\<^sub>l \<I>\<^sub>u Geq Leq s' = ?P' (<) \<B>\<^sub>i\<^sub>u \<B>\<^sub>i\<^sub>l \<B>\<^sub>u \<B>\<^sub>l undefined \<I>\<^sub>u \<I>\<^sub>l Leq Geq s'"
by (intro arg_cong[of _ _ "\<lambda> y. _ \<longrightarrow> y"] arg_cong[of _ _ "\<lambda> x. _ \<and> x"],
intro arg_cong2[of _ _ _ _ "(\<and>)"] arg_cong[of _ _ "\<lambda> y. _ \<longrightarrow> y"] arg_cong[of _ _ "\<lambda> y. \<forall> x \<subset> set (the (\<U>\<^sub>c s')). y x"] ext arg_cong[of _ _ Not],
unfold id, auto)
show "?P s' = ?P' (>) \<B>\<^sub>i\<^sub>l \<B>\<^sub>i\<^sub>u \<B>\<^sub>l \<B>\<^sub>u undefined \<I>\<^sub>l \<I>\<^sub>u Geq Leq s'"
unfolding satisfies_state_def satisfies_bounds_index.simps satisfies_bounds.simps
in_bounds.simps unsat_state_core_def satisfies_state_index.simps subsets_sat_core_def
satisfies_state_index'.simps satisfies_bounds_index'.simps
unfolding bound_compare''_defs id
by ((intro arg_cong[of _ _ "\<lambda> x. _ \<longrightarrow> x"] arg_cong[of _ _ "\<lambda> x. _ \<and> x"],
intro arg_cong2[of _ _ _ _ "(\<and>)"] refl arg_cong[of _ _ "\<lambda> x. _ \<longrightarrow> x"] arg_cong[of _ _ Not]
arg_cong[of _ _ "\<lambda> y. \<forall> x \<subset> set (the (\<U>\<^sub>c s')). y x"] ext; intro arg_cong[of _ _ Ex] ext), auto)
then show "?P s' = ?P' (<) \<B>\<^sub>i\<^sub>u \<B>\<^sub>i\<^sub>l \<B>\<^sub>u \<B>\<^sub>l undefined \<I>\<^sub>u \<I>\<^sub>l Leq Geq s'" unfolding id' .
next
fix c::'a and x::nat and dir
assume "\<lhd>\<^sub>l\<^sub>b (lt dir) c (LB dir s x)" and dir: "dir = Positive \<or> dir = Negative"
then obtain d where some: "LB dir s x = Some d" and lt: "lt dir c d"
by (auto simp: bound_compare'_defs split: option.splits)
from index[unfolded index_valid_def, rule_format, of x _ d]
some dir obtain j where ind: "LI dir s x = j" "look (LBI dir s) x = Some (j,d)" and ge: "(j, GE dir x d) \<in> as"
by (auto simp: indexl_def indexu_def boundsl_def boundsu_def)
let ?s = "set_unsat [i, ((LI dir) s x)] (update\<B>\<I> (UBI_upd dir) i x c s)"
let ?ss = "update\<B>\<I> (UBI_upd dir) i x c s"
show "?P' (lt dir) (UBI dir) (LBI dir) (UB dir) (LB dir) (UBI_upd dir) (UI dir) (LI dir) (LE dir) (GE dir) ?s"
proof (intro conjI impI allI, goal_cases)
case 1
thus ?case using dir ind ge lt some by (force simp: indices_state_def split: if_splits)
next
case 2
{
fix v
assume vU: "\<forall> x c i. ?modelU (lt dir) (UB dir) (UI dir) ?s v x c i"
assume vL: "\<forall> x c i. ?modelL (lt dir) (LB dir) (LI dir) ?s v x c i"
from dir have "UB dir ?s x = Some c" "UI dir ?s x = i" by (auto simp: boundsl_def boundsu_def indexl_def indexu_def)
from vU[rule_format, OF this] have vx_le_c: "lt dir (v x) c \<or> v x = c" by auto
from dir ind some have *: "LB dir ?s x = Some d" "LI dir ?s x = j" by (auto simp: boundsl_def boundsu_def indexl_def indexu_def) | | |