# Theory Simplex_Auxiliary

(* Authors: F. Maric, M. Spasic *)
section ‹Auxiliary Results›
theory Simplex_Auxiliary
imports
"HOL-Library.Mapping"
begin

(* -------------------------------------------------------------------------- *)
(* MoreList *)
(* -------------------------------------------------------------------------- *)
lemma map_reindex:
assumes "∀ i < length l. g (l ! i) = f i"
shows "map f [0..<length l] = map g l"
using assms
by (induct l rule: rev_induct) (auto simp add: nth_append split: if_splits)

lemma map_parametrize_idx:
"map f l = map (λi. f (l ! i)) [0..<length l]"
by (induct l rule: rev_induct) (auto simp add: nth_append)

lemma last_tl:
assumes "length l > 1"
shows "last (tl l) = last l"
using assms
by (induct l) auto

lemma hd_tl:
assumes "length l > 1"
shows "hd (tl l) = l ! 1"
using assms
by (induct l) (auto simp add: hd_conv_nth)

lemma butlast_empty_conv_length:
shows "(butlast l = []) = (length l ≤ 1)"
by (induct l) (auto split: if_splits)

lemma butlast_nth:
assumes "n + 1 < length l"
shows "butlast l ! n = l ! n"
using assms
by (induct l rule: rev_induct) (auto simp add: nth_append)

lemma last_take_conv_nth:
assumes "0 < n" "n ≤ length l"
shows "last (take n l) = l ! (n - 1)"
using assms
by (cases "l = []") (auto simp add: last_conv_nth min_def)

lemma tl_nth:
assumes "l ≠ []"
shows "tl l ! n = l ! (n + 1)"
using assms
by (induct l) auto

lemma interval_3split:
assumes "i < n"
shows "[0..<n] = [0..<i] @ [i] @ [i+1..<n]"
proof-
have "[0..<n] = [0..<i + 1] @ [i + 1..<n]"
using upt_add_eq_append[of 0 "i + 1" "n - i - 1"]
using ‹i < n›
by (auto simp del: upt_Suc)
then show ?thesis
by simp
qed

abbreviation "list_min l ≡ foldl min (hd l) (tl l)"
lemma list_min_Min[simp]: "l ≠ [] ⟹ list_min l = Min (set l)"
proof (induct l rule: rev_induct)
case (snoc a l')
then show ?case
by (cases "l' = []") (auto simp add: ac_simps)
qed simp

(* Minimal element of a list satisfying the given property *)

definition min_satisfying :: "(('a::linorder) ⇒ bool) ⇒ 'a list ⇒ 'a option" where
"min_satisfying P l ≡
let xs = filter P l in
if xs = [] then None else Some (list_min xs)"

lemma min_satisfying_None:
"min_satisfying P l = None ⟶
(∀ x ∈ set l. ¬ P x)"
unfolding min_satisfying_def Let_def

lemma min_satisfying_Some:
"min_satisfying P l = Some x ⟶
x ∈ set l ∧ P x ∧ (∀ x' ∈ set l. x' < x ⟶ ¬ P x')"
proof (safe)
let ?xs = "filter P l"
assume "min_satisfying P l = Some x"
then have "set ?xs ≠ {}" "x = Min (set ?xs)"
unfolding min_satisfying_def Let_def
by (auto split: if_splits simp add: filter_empty_conv)
then show "x ∈ set l" "P x"
using Min_in[of "set ?xs"]
by simp_all
fix x'
assume "x' ∈ set l" "P x'" "x' < x"
have "x' ∉ set ?xs"
proof (rule ccontr)
assume "¬ ?thesis"
then have "x' ≥ x"
using ‹x = Min (set ?xs)›
by simp
then show False
using ‹x' < x›
by simp
qed
then show "False"
using ‹x' ∈ set l› ‹P x'›
by simp
qed

(* -------------------------------------------------------------------------- *)
(* MoreNat *)
(* -------------------------------------------------------------------------- *)

lemma min_element:
fixes k :: nat
assumes "∃ (m::nat). P m"
shows "∃ mm. P mm ∧ (∀ m'. m' < mm ⟶ ¬ P m')"
proof-
from assms obtain m where "P m"
by auto
show ?thesis
proof (cases "∀m'<m. ¬ P m'")
case True
then show ?thesis
using ‹P m›
by auto
next
case False
then show ?thesis
proof (induct m)
case 0
then show ?case
by auto
next
case (Suc m')
then show ?case
by (cases "¬ (∀m'a<m'. ¬ P m'a)") auto
qed
qed
qed

(* -------------------------------------------------------------------------- *)
(* MoreFun *)
(* -------------------------------------------------------------------------- *)

lemma finite_fun_args:
assumes "finite A" "∀ a ∈ A. finite (B a)"
shows "finite {f. (∀ a. if a ∈ A then f a ∈ B a else f a = f0 a)}" (is "finite (?F A)")
using assms
proof (induct)
case empty
have "?F {} = {λ x. f0 x}"
by auto
then show ?case
by auto
next
case (insert a A')
then have "finite (?F A')"
by auto
let ?f = "λ f. {f'. (∀ a'. if a = a' then f' a ∈ B a else f' a' = f a')}"
have "∀ f ∈ ?F A'. finite (?f f)"
proof
fix f
assume "f ∈ ?F A'"
then have "?f f = (λ b. f (a := b))  B a"
by (force split: if_splits)
then show "finite (?f f)"
using ‹∀a∈insert a A'. finite (B a)›
by auto
qed
then have "finite (⋃ (?f  (?F A')))"
using ‹finite (?F A')›
by auto
moreover
have "?F (insert a A') = ⋃ (?f  (?F A'))"
proof
show "?F (insert a A') ⊆ ⋃ (?f  (?F A'))"
proof
fix f
assume "f ∈ ?F (insert a A')"
then have "f ∈ ?f (f (a := f0 a))" "f (a := f0 a) ∈ ?F A'"
using ‹a ∉ A'›
by auto
then show "f ∈ ⋃ (?f  (?F A'))"
by blast
qed
next
show "⋃ (?f  (?F A')) ⊆ ?F (insert a A')"
proof
fix f
assume "f ∈ ⋃ (?f  (?F A'))"
then obtain f0 where "f0 ∈ ?F A'" "f ∈ ?f f0"
by auto
then show "f ∈ ?F (insert a A')"
using ‹a ∉ A'›
by (force split: if_splits)
qed
qed
ultimately
show ?case
by simp
qed

(* -------------------------------------------------------------------------- *)
(* MoreMapping *)
(* -------------------------------------------------------------------------- *)

lemma foldl_mapping_update:
assumes "X ∈ set l" "distinct (map f l)"
shows "Mapping.lookup (foldl (λm a. Mapping.update (f a) (g a) m) i l) (f X) = Some (g X)"
using assms
proof(induct l rule:rev_induct)
case Nil
then show ?case
by simp
next
case (snoc h t)
show ?case
proof (cases "f h = f X")
case True
then show ?thesis using snoc by (auto simp: lookup_update)
next
case False
show ?thesis by (simp add: lookup_update' False, rule snoc, insert False snoc, auto)
qed
qed

end


# Theory Rel_Chain

(* Authors: F. Maric, M. Spasic *)
theory Rel_Chain
imports
Simplex_Auxiliary
begin

definition
rel_chain :: "'a list ⇒ ('a × 'a) set ⇒ bool"
where
"rel_chain l r = (∀ k < length l - 1. (l ! k, l ! (k + 1)) ∈ r)"

lemma
rel_chain_Nil: "rel_chain [] r" and
rel_chain_Cons: "rel_chain (x # xs) r = (if xs = [] then True else ((x, hd xs) ∈ r) ∧ rel_chain xs r)"
by (auto simp add: rel_chain_def hd_conv_nth nth_Cons split: nat.split_asm nat.split)

lemma rel_chain_drop:
"rel_chain l R ==> rel_chain (drop n l) R"
unfolding rel_chain_def
by simp

lemma rel_chain_take:
"rel_chain l R ==> rel_chain (take n l) R"
unfolding rel_chain_def
by simp

lemma rel_chain_butlast:
"rel_chain l R ==> rel_chain (butlast l) R"
unfolding rel_chain_def

lemma rel_chain_tl:
"rel_chain l R ==> rel_chain (tl l) R"
unfolding rel_chain_def
by (cases "l = []") (auto simp add: tl_nth)

lemma rel_chain_append:
assumes "rel_chain l R" "rel_chain l' R" "(last l, hd l') ∈ R"
shows "rel_chain (l @ l') R"
using assms
by (induct l) (auto simp add: rel_chain_Cons split: if_splits)

lemma rel_chain_appendD:
assumes "rel_chain (l @ l') R"
shows "rel_chain l R" "rel_chain l' R" "l ≠ [] ∧ l' ≠ [] ⟶ (last l, hd l') ∈ R"
using assms
by (induct l) (auto simp add: rel_chain_Cons rel_chain_Nil split: if_splits)

lemma rtrancl_rel_chain:
"(x, y) ∈ R⇧* ⟷ (∃ l. l ≠ [] ∧ hd l = x ∧ last l = y ∧ rel_chain l R)"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
by (induct rule: converse_rtrancl_induct) (auto simp add: rel_chain_Cons)
next
assume ?rhs
then obtain l where "l ≠ []" "hd l = x" "last l = y" "rel_chain l R"
by auto
then show ?lhs
by (induct l arbitrary: x) (auto simp add: rel_chain_Cons, force)
qed

lemma trancl_rel_chain:
"(x, y) ∈ R⇧+ ⟷ (∃ l. l ≠ [] ∧ length l > 1 ∧ hd l = x ∧ last l = y ∧ rel_chain l R)" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
then obtain z where "(x, z) ∈ R" "(z, y) ∈ R⇧*"
by (auto dest: tranclD)
then obtain l where  "l ≠ [] ∧ hd l = z ∧ last l = y ∧ rel_chain l R"
then show ?rhs
using ‹(x, z) ∈ R›
by (rule_tac x="x # l" in exI) (auto simp add: rel_chain_Cons)
next
assume ?rhs
then obtain l where "1 < length l" "l ≠ []" "hd l = x" "last l = y" "rel_chain l R"
by auto
then obtain l' where
"l' ≠ []" "l = x # l'" "(x, hd l') ∈ R" "rel_chain l' R"
using ‹1 < length l›
by (cases l) (auto simp add: rel_chain_Cons)
then have "(x, hd l') ∈ R" "(hd l', y) ∈ R⇧*"
using ‹last l = y›
then show ?lhs
by auto
qed

lemma rel_chain_elems_rtrancl:
assumes "rel_chain l R" "i ≤ j" "j < length l"
shows "(l ! i, l ! j) ∈ R⇧*"
proof (cases "i = j")
case True
then show ?thesis
by simp
next
case False
then have "i < j"
using ‹i ≤ j›
by simp
then have "l ≠ []"
using ‹j < length l›
by auto

let ?l = "drop i (take (j + 1) l)"

have "?l ≠ []"
using ‹i < j› ‹j < length l›
by simp
moreover
have "hd ?l = l ! i"
using ‹?l ≠ []› ‹i < j›
moreover
have "last ?l = l ! j"
using ‹?l ≠ []› ‹l ≠ []› ‹i < j› ‹j < length l›
by (cases "length l = j + 1") (auto simp add: last_conv_nth min_def)
moreover
have "rel_chain ?l R"
using ‹rel_chain l R›
by (auto intro: rel_chain_drop rel_chain_take)
ultimately
show ?thesis
by (subst rtrancl_rel_chain) blast
qed

lemma reorder_cyclic_list:
assumes  "hd l = s" "last l = s" "length l > 2" "sl + 1 < length l"
"rel_chain l r"
obtains l' :: "'a list"
where "hd l' = l ! (sl + 1)" "last l' = l ! sl" "rel_chain l' r" "length l' = length l - 1"
"∀ i. i + 1 < length l' ⟶
(∃ j. j + 1 < length l ∧ l' ! i = l ! j ∧ l' ! (i + 1) = l ! (j + 1))"
proof-
have "l ≠ []"
using ‹length l > 2›
by auto

have  "length (tl l) > 1" "tl l ≠ []"
using ‹length l > 2›
by (auto simp add: length_0_conv[THEN sym])

let ?l' = "if sl = 0 then
tl l
else
drop (sl + 1) l @ tl (take (sl + 1) l)"

have "hd ?l' = l ! (sl + 1)"
proof (cases "sl > 0", simp_all)
show "hd (tl l) = l ! (Suc 0)"
using ‹tl l ≠ []› ‹l ≠ []›
next
assume "0 < sl"
show "hd (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! (Suc sl)"
using ‹sl + 1 < length l› ‹l ≠ []›
by (auto simp add: hd_append hd_drop_conv_nth)
qed

moreover

have "last ?l' = l ! sl"
proof (cases "sl > 0", simp_all)
show "last (tl l) = l ! 0"
using ‹l ≠ []› ‹last l = s› ‹hd l = s› ‹length l > 2›
next
assume "sl > 0"
then show "last (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! sl"
using ‹l ≠ []› ‹tl l ≠ []› ‹sl + 1 < length l›
by (auto simp add: last_append drop_Suc tl_take last_take_conv_nth tl_nth)
qed

moreover

have "rel_chain ?l' r"
proof (cases "sl = 0", simp_all)
case True
show "rel_chain (tl l) r"
using ‹rel_chain l r›
by (auto intro: rel_chain_tl)
next
assume "sl > 0"
show  "rel_chain (drop (Suc sl) l @ tl (take (Suc sl) l)) r"
proof (rule rel_chain_append)
show "rel_chain (drop (Suc sl) l) r"
using ‹rel_chain l r›
by (auto intro: rel_chain_drop)
next
show "rel_chain (tl (take (Suc sl) l)) r"
using ‹rel_chain l r›
by (auto intro: rel_chain_tl rel_chain_take)
next
have "last (drop (sl + 1) l) = l ! 0"
using ‹sl + 1 < length l› ‹last l = s› ‹hd l = s› ‹l ≠ []›
moreover
have "sl > 0 ⟶ tl (take (sl + 1) l) ≠ []"
using ‹sl + 1 < length l› ‹l ≠ []› ‹tl l ≠ []›
then have "sl > 0 ⟶ hd (tl (take (sl + 1) l)) = l ! 1"
using ‹l ≠ []›
by (auto simp add: hd_conv_nth take_Suc tl_nth)
ultimately
show "(last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) ∈ r"
using ‹rel_chain l r› ‹length l > 2› ‹sl > 0›
unfolding rel_chain_def
by simp
qed
qed

moreover

have "length ?l' = length l - 1"
by auto

ultimately

obtain l' where *: "l' = ?l'" "hd l' = l ! (sl + 1)" "last l' = l ! sl" "rel_chain l' r" "length l' = length l - 1"
by auto

have l'_l: "∀ i. i + 1 < length l' ⟶
(∃ j. j + 1 < length l ∧ l' ! i = l ! j ∧ l' ! (i + 1) = l ! (j + 1))"
proof (safe)
fix i
assume "i + 1 < length l'"
show "∃ j. j + 1 < length l ∧ l' ! i = l ! j ∧ l' ! (i + 1) = l ! (j + 1)"
proof (cases "sl = 0")
case True
then show ?thesis
using ‹i + 1 < length l'›
using ‹l' = ?l'› ‹l ≠ []›
next
case False
then have "length l' = length l - 1"
using ‹l' = ?l'› ‹sl + 1 < length l›
then have "i + 2 < length l"
using ‹i + 1 < length l'›
by simp

show ?thesis
proof (cases "i + 1 < length (drop (sl + 1) l)")
case True
then show ?thesis
using ‹sl ≠ 0› ‹l' = ?l'›
next
case False
show ?thesis
proof (cases "i + 1 > length (drop (sl + 1) l)")
case True
then have "i + 1 > length l - (sl + 1)"
by auto
have
"l' ! i = l ! Suc (i - (length l - Suc sl))"
"l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))"
using ‹i + 2 < length l› ‹sl + 1 < length l›
using ‹i + 1 > length l - (sl + 1)›
using ‹sl ≠ 0› ‹l' = ?l'› ‹l ≠ []›
using tl_nth[of "take (sl + 1) l" "i - (length l - Suc sl)"]
using tl_nth[of "take (sl + 1) l" "Suc i - (length l - Suc sl)"]

have "Suc (i - (length l - Suc sl)) = i + sl + 1 - length l + 1"
"Suc (Suc i - (length l - Suc sl)) = (i + sl + 1 - length l + 1) + 1"
"i + sl + 1 - length l + 1 + 1 < length l"
using ‹sl + 1 < length l›
using ‹i + 1 > length l - (sl + 1)›
using ‹i + 2 < length l›
by auto

have "l' ! i = l ! (i + sl + 1 - length l + 1)"
using ‹l' ! i = l ! Suc (i - (length l - Suc sl))›
by (subst ‹Suc (i - (length l - Suc sl)) = i + sl + 1 - length l + 1›[THEN sym])
moreover
have "l' ! (i + 1) = l ! ((i + sl + 1 - length l + 1) + 1)"
using ‹l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))›
by (subst ‹Suc (Suc i - (length l - Suc sl)) = (i + sl + 1 - length l + 1) + 1›[THEN sym])
ultimately
show ?thesis
using ‹i + sl + 1 - length l + 1 + 1 < length l›
by force
next
case False
then have "i + 1 = length l - sl - 1"
using ‹¬ i + 1 < length (drop (sl + 1) l)›
by simp
then have "length l - 1 = sl + i + 1"
by auto
then have "l ! Suc (sl + i) = last l"
using last_conv_nth[of l, THEN sym] ‹l ≠ []›
by simp
then show ?thesis
using ‹i + 1 = length l - sl - 1›
using ‹l' = ?l'› ‹sl ≠ 0› ‹l ≠ []›
using tl_nth[of "take (sl + 1) l" 0]
using ‹hd l = s› ‹last l = s›
by (force simp add: nth_append hd_conv_nth)
qed
qed
qed
qed

then show thesis
using * l'_l
apply -
..
qed

end


# Theory Simplex_Algebra

(* Authors: F. Maric, M. Spasic *)
section ‹Linearly Ordered Rational Vectors›
theory Simplex_Algebra
imports
HOL.Rat
HOL.Real_Vector_Spaces
begin

class scaleRat =
fixes scaleRat :: "rat ⇒ 'a ⇒ 'a" (infixr "*R" 75)
begin

abbreviation
divideRat :: "'a ⇒ rat ⇒ 'a" (infixl "'/R" 70)
where
"x /R r == scaleRat (inverse r) x"
end

class rational_vector = scaleRat + ab_group_add +
assumes scaleRat_right_distrib: "scaleRat a (x + y) = scaleRat a x + scaleRat a y"
and scaleRat_left_distrib: "scaleRat (a + b) x = scaleRat a x + scaleRat b x"
and scaleRat_scaleRat: "scaleRat a (scaleRat b x) = scaleRat (a * b) x"
and scaleRat_one: "scaleRat 1 x = x"

interpretation rational_vector:
vector_space "scaleRat :: rat ⇒ 'a ⇒ 'a::rational_vector"
by (unfold_locales) (simp_all add: scaleRat_right_distrib  scaleRat_left_distrib scaleRat_scaleRat scaleRat_one)

class ordered_rational_vector = rational_vector + order

class linordered_rational_vector = ordered_rational_vector + linorder +
assumes plus_less: "(a::'a) < b ⟹ a + c < b + c" and
scaleRat_less1: "⟦(a::'a) < b; k > 0⟧ ⟹ (k *R a) < (k *R b)" and
scaleRat_less2: "⟦(a::'a) < b; k < 0⟧ ⟹ (k *R a) > (k *R b)"
begin

lemma scaleRat_leq1: "⟦ a ≤ b; k > 0⟧ ⟹ k *R a ≤ k *R b"
unfolding le_less
using scaleRat_less1[of a b k]
by auto

lemma scaleRat_leq2: "⟦ a ≤ b; k < 0⟧ ⟹ k *R a ≥ k *R b"
unfolding le_less
using scaleRat_less2[of a b k]
by auto

lemma zero_scaleRat
[simp]: "0 *R v = zero"
using scaleRat_left_distrib[of 0 0 v]
by auto

lemma scaleRat_zero
[simp]: "a *R (0::'a) = 0"
using scaleRat_right_distrib[of a 0 0]
by auto

lemma scaleRat_uminus [simp]:
"-1 *R x = - (x :: 'a)"
proof-
have "0  = -1 *R x + x"
using scaleRat_left_distrib[of "-1" 1 x]
have "-x = 0 - x"
by simp
then have "-x = -1 *R x + x - x"
using ‹0  = -1 *R x + x›
by simp
then show ?thesis
qed

lemma minus_lt: "(a::'a) < b ⟷ a - b < 0"
using plus_less[of a b "-b"]
using plus_less[of "a - b" 0 b]

lemma minus_gt: "(a::'a) < b ⟷ 0 < b - a"
using plus_less[of a b "-a"]
using plus_less[of 0 "b-a" a]

lemma minus_leq:
"(a::'a) ≤ b ⟷ a - b ≤ 0"
proof-
have *: "a ≤ b ⟹ a - b ≤ (0 :: 'a)"
using minus_gt[of a b]
using scaleRat_less2[of 0 "b-a" "-1"]
have **: "a - b ≤ 0 ⟹ a ≤ b"
proof-
assume "a - b ≤ 0"
show ?thesis
proof(cases "a - b < 0")
case True
then show ?thesis
using plus_less[of "a - b" 0 b]
next
case False
then show ?thesis
using ‹a - b ≤ 0›
qed
qed
show ?thesis
using * **
by auto
qed

lemma minus_geq: "(a::'a) ≤ b ⟷ 0 ≤ b - a"
proof-
have *: "a ≤ b ⟹ 0 ≤ b - a"
using minus_gt[of a b]
have **: "0 ≤ b - a ⟹ a ≤ b"
proof-
assume "0 ≤ b - a"
show ?thesis
proof(cases "0 < b - a")
case True
then show ?thesis
using plus_less[of 0 "b - a" a]
next
case False
then show ?thesis
using ‹0 ≤ b - a›
using order.eq_iff[of "b - a" 0]
by auto
qed
qed
show ?thesis
using * **
by auto
qed

lemma divide_lt:
"⟦c *R (a::'a) < b; (c::rat) > 0 ⟧ ⟹ a < (1/c) *R b"
using scaleRat_less1[of "c *R a" b "1/c"]

lemma divide_gt:
"⟦c *R (a::'a) > b;(c::rat) > 0⟧ ⟹ a > (1/c) *R b"
using scaleRat_less1[of b "c *R a" "1/c"]

lemma divide_leq:
"⟦c *R (a::'a) ≤  b; (c::rat) > 0⟧ ⟹ a ≤ (1/c) *R b"
proof(cases "c *R a < b")
assume "c > 0"
case True
then show ?thesis
using divide_lt[of c a b]
using ‹c > 0›
by simp
next
assume "c *R a ≤  b" "c > 0"
case False
then have *: "c *R a = b"
using ‹c *R a ≤ b›
by simp
then show ?thesis
using ‹c > 0›
by (auto simp add: scaleRat_one scaleRat_scaleRat)
qed

lemma divide_geq:
"⟦c *R (a::'a) ≥ b; (c::rat) > 0⟧ ⟹ a ≥ (1/c) *R b"
proof(cases "c *R a > b")
assume "c > 0"
case True
then show ?thesis
using divide_gt[of b c a]
using ‹c > 0›
by simp
next
assume "c *R a ≥ b" "c > 0"
case False
then have *: "c *R a = b"
using ‹c *R a ≥ b›
by simp
then show ?thesis
using ‹c > 0›
by (auto simp add: scaleRat_one scaleRat_scaleRat)
qed

lemma divide_lt1:
"⟦c *R (a::'a) < b; (c::rat) < 0⟧ ⟹ a > (1/c) *R b"
using scaleRat_less2[of "c *R a" b "1/c"]

lemma divide_gt1:
"⟦c *R (a::'a) > b; (c::rat) < 0 ⟧ ⟹  a < (1/c) *R b"
using scaleRat_less2[of b "c *R a" "1/c"]

lemma divide_leq1:
"⟦c *R (a::'a) ≤  b; (c::rat) < 0⟧ ⟹ a ≥ (1/c) *R b"
proof(cases "c *R a < b")
assume "c < 0"
case True
then show ?thesis
using divide_lt1[of c a b]
using ‹c < 0›
by simp
next
assume "c *R a ≤  b" "c < 0"
case False
then have *: "c *R a = b"
using ‹c *R a ≤ b›
by simp
then show ?thesis
using ‹c < 0›
by (auto simp add: scaleRat_one scaleRat_scaleRat)
qed

lemma divide_geq1:
"⟦c *R (a::'a) ≥ b; (c::rat) < 0⟧ ⟹ a ≤ (1/c) *R b"
proof(cases "c *R a > b")
assume "c < 0"
case True
then show ?thesis
using divide_gt1[of b c a]
using ‹c < 0›
by simp
next
assume "c *R a ≥ b" "c < 0"
case False
then have *: "c *R a = b"
using ‹c *R a ≥ b›
by simp
then show ?thesis
using ‹c < 0›
by (auto simp add: scaleRat_one scaleRat_scaleRat)
qed

end

class lrv = linordered_rational_vector + one +
assumes zero_neq_one: "0 ≠ 1"

proof
fix a b c
assume "a ≤ b"
then show "c + a ≤ c + b"
using plus_less[of a b c]
qed

instantiation rat :: rational_vector
begin
definition scaleRat_rat :: "rat ⇒ rat ⇒ rat" where
[simp]: "x *R y = x * y"
instance by standard (auto simp add: field_simps)
end

instantiation rat :: ordered_rational_vector
begin
instance ..
end

instantiation rat :: linordered_rational_vector
begin
instance by standard (auto simp add: field_simps)
end

instantiation rat :: lrv
begin
instance by standard (auto simp add: field_simps)
end

lemma uminus_less_lrv[simp]: fixes a b :: "'a :: lrv"
shows "- a < - b ⟷ b < a"
proof -
have "(- a < - b) = (-1 *R a < -1 *R b)" by simp
also have "… ⟷ (b < a)"
using scaleRat_less2[of _ _ "-1"] scaleRat_less2[of "-1 *R a" "-1 *R b" "-1"] by auto
finally show ?thesis .
qed

end


# Theory Abstract_Linear_Poly

(* Authors: F. Maric, M. Spasic, R. Thiemann *)
section ‹Linear Polynomials and Constraints›

theory Abstract_Linear_Poly
imports
Simplex_Algebra
begin

type_synonym var = nat

text‹(Infinite) linear polynomials as functions from vars to coeffs›

definition fun_zero :: "var ⇒ 'a::zero" where
[simp]: "fun_zero == λ v. 0"
definition fun_plus :: "(var ⇒ 'a) ⇒ (var ⇒ 'a) ⇒ var ⇒ 'a::plus" where
[simp]: "fun_plus f1 f2 == λ v. f1 v + f2 v"
definition fun_scale :: "'a ⇒ (var ⇒ 'a) ⇒ (var ⇒ 'a::ring)" where
[simp]: "fun_scale c f == λ v. c*(f v)"
definition fun_coeff :: "(var ⇒ 'a) ⇒ var ⇒ 'a" where
[simp]: "fun_coeff f var = f var"
definition fun_vars :: "(var ⇒ 'a::zero) ⇒ var set" where
[simp]: "fun_vars f = {v. f v ≠ 0}"
definition fun_vars_list :: "(var ⇒ 'a::zero) ⇒ var list" where
[simp]: "fun_vars_list f = sorted_list_of_set {v. f v ≠ 0}"
definition fun_var :: "var ⇒ (var ⇒ 'a::{zero,one})" where
[simp]: "fun_var x = (λ x'. if x' = x then 1 else 0)"
type_synonym 'a valuation = "var ⇒ 'a"
definition fun_valuate :: "(var ⇒ rat) ⇒ 'a valuation ⇒ ('a::rational_vector)" where
[simp]: "fun_valuate lp val = (∑x∈{v. lp v ≠ 0}. lp x *R val x)"

text‹Invariant -- only finitely many variables›
definition inv where
[simp]: "inv c == finite {v. c v ≠ 0}"

lemma inv_fun_zero [simp]:
"inv fun_zero" by simp

lemma inv_fun_plus [simp]:
"⟦inv (f1 :: nat ⇒ 'a::monoid_add); inv f2⟧ ⟹ inv (fun_plus f1 f2)"
proof-
have *: "{v. f1 v + f2 v ≠ (0 :: 'a)} ⊆ {v. f1 v ≠ (0 :: 'a)} ∪ {v. f2 v ≠ (0 :: 'a)}"
by auto
assume "inv f1" "inv f2"
then show ?thesis
using *
qed

lemma inv_fun_scale [simp]:
"inv (f :: nat ⇒ 'a::ring) ⟹ inv (fun_scale r f)"
proof-
have *: "{v. r * (f v) ≠ 0} ⊆ {v. f v ≠ 0}"
by auto
assume "inv f"
then show ?thesis
using *
qed

text‹linear-poly type -- rat coeffs›
(* TODO: change rat to arbitrary ring *)

typedef  linear_poly = "{c :: var ⇒ rat. inv c}"
by (rule_tac x="λ v. 0" in exI) auto

text‹Linear polynomials are of the form $a_1 \cdot x_1 + ... + a_n \cdot x_n$. Their formalization follows the data-refinement approach
of Isabelle/HOL \cite{florian-refinement}. Abstract representation of
polynomials are functions mapping variables to their coefficients,
where only finitely many variables have non-zero
coefficients. Operations on polynomials are defined as operations on
functions. For example, the sum of @{term "p⇩1"} and ‹p⇩2› is
defined by @{term "λ v. p⇩1 v + p⇩2 v"} and the value of a polynomial
@{term "p"} for a valuation @{term "v"} (denoted by ‹p⦃v⦄›),
is defined by @{term "∑x∈{x. p x ≠ 0}. p x * v x"}. Executable
representation of polynomials uses RBT mappings instead of functions.
›

setup_lifting type_definition_linear_poly

text‹Vector space operations on polynomials›
instantiation linear_poly :: rational_vector
begin

lift_definition zero_linear_poly :: "linear_poly" is fun_zero by (rule inv_fun_zero)

lift_definition plus_linear_poly :: "linear_poly ⇒ linear_poly ⇒ linear_poly" is fun_plus
by (rule inv_fun_plus)

lift_definition scaleRat_linear_poly :: "rat ⇒ linear_poly ⇒ linear_poly" is fun_scale
by (rule inv_fun_scale)

definition uminus_linear_poly :: "linear_poly ⇒ linear_poly" where
"uminus_linear_poly lp = -1 *R lp"

definition minus_linear_poly :: "linear_poly ⇒ linear_poly ⇒ linear_poly" where
"minus_linear_poly lp1 lp2 = lp1 + (- lp2)"

instance
proof
fix a b c::linear_poly
show "a + b + c = a + (b + c)" by (transfer, auto)
show "a + b = b + a" by (transfer, auto)
show "0 + a = a" by (transfer, auto)
show "-a + a = 0" unfolding uminus_linear_poly_def by (transfer, auto)
show "a - b = a + (- b)" unfolding minus_linear_poly_def ..
next
fix a :: rat and x y :: linear_poly
show "a *R (x + y) = a *R x + a *R y" by (transfer, auto simp: field_simps)
next
fix a b::rat and x::linear_poly
show "(a + b) *R x = a *R x + b *R x" by (transfer, auto simp: field_simps)
show "a *R b *R x = (a * b) *R x" by (transfer, auto simp: field_simps)
next
fix x::linear_poly
show "1 *R x = x" by (transfer, auto)
qed

end

text‹Coefficient›
lift_definition coeff :: "linear_poly ⇒ var ⇒ rat" is fun_coeff .

lemma coeff_plus [simp] : "coeff (lp1 + lp2) var = coeff lp1 var + coeff lp2 var"
by transfer auto

lemma coeff_scaleRat [simp]: "coeff (k *R lp1) var = k * coeff lp1 var"
by transfer auto

lemma coeff_uminus [simp]: "coeff (-lp) var = - coeff lp var"
unfolding uminus_linear_poly_def
by transfer auto

lemma coeff_minus [simp]: "coeff (lp1 - lp2) var = coeff lp1 var - coeff lp2 var"
unfolding minus_linear_poly_def uminus_linear_poly_def
by transfer auto

text‹Set of variables›

lift_definition vars :: "linear_poly ⇒ var set" is fun_vars .

lemma coeff_zero: "coeff p x ≠ 0 ⟷ x ∈ vars p"
by transfer auto

lemma finite_vars: "finite (vars p)"
by transfer auto

text‹List of variables›
lift_definition vars_list :: "linear_poly ⇒ var list" is fun_vars_list .

lemma set_vars_list: "set (vars_list lp) = vars lp"
by transfer auto

text‹Construct single variable polynomial›
lift_definition Var :: "var ⇒ linear_poly" is fun_var by auto

text‹Value of a polynomial in a given valuation›
lift_definition valuate :: "linear_poly ⇒ 'a valuation ⇒ ('a::rational_vector)" is fun_valuate .

syntax
"_valuate" :: "linear_poly ⇒ 'a valuation ⇒ 'a"    ("_ ⦃ _ ⦄")
translations
"p⦃v⦄ " == "CONST valuate p v"

lemma valuate_zero: "(0 ⦃v⦄) = 0"
by transfer auto

lemma
valuate_diff: "(p ⦃v1⦄) - (p ⦃v2⦄) = (p ⦃ λ x. v1 x - v2 x ⦄)"
by (transfer, simp add: sum_subtractf[THEN sym], auto simp: rational_vector.scale_right_diff_distrib)

lemma valuate_opposite_val:
shows "p ⦃ λ x. - v x ⦄ = - (p ⦃ v ⦄)"
using valuate_diff[of p "λ x. 0" v]

lemma valuate_nonneg:
fixes v :: "'a::linordered_rational_vector valuation"
assumes "∀ x ∈ vars p. (coeff p x > 0 ⟶ v x ≥ 0) ∧ (coeff p x < 0 ⟶ v x ≤ 0)"
shows "p ⦃ v ⦄ ≥ 0"
using assms
proof (transfer, unfold fun_valuate_def, goal_cases)
case (1 p v)
from 1 have fin: "finite {v. p v ≠ 0}" by auto
then show "0 ≤ (∑x∈{v. p v ≠ 0}. p x *R v x)"
proof (induct rule: finite_induct)
case empty show ?case by auto
next
case (insert x F)
show ?case unfolding sum.insert[OF insert(1-2)]
proof (rule order.trans[OF _ add_mono[OF _ insert(3)]])
show "0 ≤ p x *R v x" using scaleRat_leq1[of 0 "v x" "p x"]
using scaleRat_leq2[of "v x" 0 "p x"] 1(2)
by (cases "p x > 0"; cases "p x < 0"; auto)
qed auto
qed
qed

lemma valuate_nonpos:
fixes v :: "'a::linordered_rational_vector valuation"
assumes "∀ x ∈ vars p. (coeff p x > 0 ⟶ v x ≤ 0) ∧ (coeff p x < 0 ⟶ v x ≥ 0)"
shows "p ⦃ v ⦄ ≤ 0"
using assms
using valuate_opposite_val[of p v]
using valuate_nonneg[of p "λ x. - v x"]
using scaleRat_leq2[of "0::'a" _ "-1"]
using scaleRat_leq2[of _ "0::'a" "-1"]
by force

lemma valuate_uminus: "(-p) ⦃v⦄ = - (p ⦃v⦄)"
unfolding uminus_linear_poly_def
by (transfer, auto simp: sum_negf)

fixes v :: "'a ⇒ 'b::rational_vector"
assumes "finite {v. f1 v ≠ 0}" "finite {v. f2 v ≠ 0}"
shows
"(∑x∈{v. f1 v + f2 v ≠ 0}. (f1 x + f2 x) *R v x) =
(∑x∈{v. f1 v ≠ 0}. f1 x *R v x) +  (∑x∈{v. f2 v ≠ 0}. f2 x *R v x)"
proof-
let ?A = "{v. f1 v + f2 v ≠ 0} ∪ {v. f1 v + f2 v = 0 ∧ (f1 v ≠ 0 ∨ f2 v ≠ 0)}"
have "?A = {v. f1 v ≠ 0 ∨ f2 v ≠ 0}"
by auto
then have
"finite ?A"
using assms
by (subgoal_tac "{v. f1 v ≠ 0 ∨ f2 v ≠ 0} = {v. f1 v ≠ 0} ∪ {v. f2 v ≠ 0}") auto

then have "(∑x∈{v. f1 v + f2 v ≠ 0}. (f1 x + f2 x) *R v x) =
(∑x∈{v. f1 v + f2 v ≠ 0} ∪ {v. f1 v + f2 v = 0 ∧ (f1 v ≠ 0 ∨ f2 v ≠ 0)}. (f1 x + f2 x) *R v x)"
by (rule sum.mono_neutral_left) auto
also have "... = (∑x ∈ {v. f1 v ≠ 0 ∨ f2 v ≠ 0}. (f1 x + f2 x) *R v x)"
by (rule sum.cong) auto
also have "... = (∑x ∈ {v. f1 v ≠ 0 ∨ f2 v ≠ 0}. f1 x *R v x) +
(∑x ∈ {v. f1 v ≠ 0 ∨ f2 v ≠ 0}. f2 x *R v x)"
also have "... = (∑x∈{v. f1 v ≠ 0}. f1 x *R v x) +  (∑x∈{v. f2 v ≠ 0}. f2 x *R v x)"
proof-
{
fix f1 f2::"'a ⇒ rat"
assume "finite {v. f1 v ≠ 0}" "finite {v. f2 v ≠ 0}"
then have "finite {v. f1 v ≠ 0 ∨ f2 v ≠ 0 ∧ f1 v = 0}"
by (subgoal_tac "{v. f1 v ≠ 0 ∨ f2 v ≠ 0} = {v. f1 v ≠ 0} ∪ {v. f2 v ≠ 0}") auto
have "(∑x∈{v. f1 v ≠ 0 ∨ f2 v ≠ 0}. f1 x *R v x) =
(∑x∈{v. f1 v ≠ 0 ∨ (f2 v ≠ 0 ∧ f1 v = 0)}. f1 x *R v x)"
by auto
also have "... = (∑x∈{v. f1 v ≠ 0}. f1 x *R v x)"
using ‹finite {v. f1 v ≠ 0 ∨ f2 v ≠ 0 ∧ f1 v = 0}›
by (rule sum.mono_neutral_left[THEN sym]) auto
ultimately have "(∑x∈{v. f1 v ≠ 0 ∨ f2 v ≠ 0}. f1 x *R v x) =
(∑x∈{v. f1 v ≠ 0}. f1 x *R v x)"
by simp
}
note * = this
show ?thesis
using assms
using *[of f1 f2]
using *[of f2 f1]
by (subgoal_tac "{v. f2 v ≠ 0 ∨ f1 v ≠ 0} = {v. f1 v ≠ 0 ∨ f2 v ≠ 0}") auto
qed
ultimately
show ?thesis by simp
qed

lemma valuate_add:  "(p1 + p2) ⦃v⦄ = (p1 ⦃v⦄) + (p2 ⦃v⦄)"

lemma valuate_minus: "(p1 - p2) ⦃v⦄ = (p1 ⦃v⦄) - (p2 ⦃v⦄)"

lemma valuate_scaleRat:
"(c *R lp) ⦃ v ⦄ = c *R ( lp⦃v⦄ )"
proof (cases "c=0")
case True
then show ?thesis
by (auto simp add: valuate_def zero_linear_poly_def Abs_linear_poly_inverse)
next
case False
then have "⋀ v. Rep_linear_poly (c *R lp) v = c * (Rep_linear_poly lp v)"
unfolding scaleRat_linear_poly_def
using Abs_linear_poly_inverse[of "λv. c * Rep_linear_poly lp v"]
using Rep_linear_poly
by auto
then show ?thesis
unfolding valuate_def
using ‹c ≠ 0›
by auto (subst rational_vector.scale_sum_right, auto)
qed

lemma valuate_Var: "(Var x) ⦃v⦄ = v x"
by transfer auto

lemma valuate_sum: "((∑x∈A. f x) ⦃ v ⦄) = (∑x∈A. ((f x) ⦃ v ⦄))"
by (induct A rule: infinite_finite_induct, auto simp: valuate_zero valuate_add)

lemma distinct_vars_list:
"distinct (vars_list p)"
by transfer (use distinct_sorted_list_of_set in auto)

lemma zero_coeff_zero: "p = 0 ⟷ (∀ v. coeff p v = 0)"
by transfer auto

lemma all_val:
assumes "∀ (v::var ⇒ 'a::lrv). ∃ v'. (∀ x ∈ vars p. v' x = v x) ∧ (p ⦃v'⦄ = 0)"
shows "p = 0"
proof (subst zero_coeff_zero, rule allI)
fix x
show "coeff p x = 0"
proof (cases "x ∈ vars p")
case False
then show ?thesis
using coeff_zero[of p x]
by simp
next
case True
have "(0::'a::lrv) ≠ (1::'a)"
using zero_neq_one
by auto

let ?v = "λ x'. if x = x' then 1 else 0::'a"
obtain v' where "∀ x ∈ vars p. v' x = ?v x" "p ⦃v'⦄ = 0"
using assms
by (erule_tac x="?v" in allE) auto
then have "∀ x' ∈ vars p. v' x' = (if x = x' then 1 else 0)" "p ⦃v'⦄ = 0"
by auto

let ?fp = "Rep_linear_poly p"
have "{x. ?fp x ≠ 0 ∧ v' x ≠ (0 :: 'a)} = {x}"
using ‹x ∈ vars p› unfolding vars_def
proof (safe, simp_all)
fix x'
assume "v' x' ≠ 0" "Rep_linear_poly p x' ≠ 0"
then show "x' = x"
using ‹∀ x' ∈ vars p. v' x' = (if x = x' then 1 else 0)›
unfolding vars_def
by (erule_tac x="x'" in ballE) (simp_all split: if_splits)
next
assume "v' x = 0" "Rep_linear_poly p x ≠ 0"
then show False
using ‹∀ x' ∈ vars p. v' x' = (if x = x' then 1 else 0)›
using ‹0 ≠ 1›
unfolding vars_def
by simp
qed

have "p ⦃v'⦄ = (∑x∈{v. ?fp v ≠ 0}. ?fp x *R v' x)"
unfolding valuate_def
by auto
also have "... = (∑x∈{v. ?fp v ≠ 0 ∧ v' v ≠ 0}. ?fp x *R v' x)"
apply (rule sum.mono_neutral_left[THEN sym])
using Rep_linear_poly[of p]
by auto
also have "... = ?fp x *R v' x"
using ‹{x. ?fp x ≠ 0 ∧ v' x ≠ (0 :: 'a)} = {x}›
by simp
also have "... = ?fp x *R 1"
using ‹x ∈ vars p›
using ‹∀ x' ∈ vars p. v' x' = (if x = x' then 1 else 0)›
by simp
ultimately
have "p ⦃v'⦄ = ?fp x *R 1"
by simp
then have "coeff p x *R (1::'a)= 0"
using ‹p ⦃v'⦄ = 0›
unfolding coeff_def
by simp
then show ?thesis
using rational_vector.scale_eq_0_iff
using ‹0 ≠ 1›
by simp
qed
qed

lift_definition lp_monom :: "rat ⇒ var ⇒ linear_poly" is
"λ c x y. if x = y then c else 0" by auto

lemma valuate_lp_monom: "((lp_monom c x) ⦃v⦄) = c * (v x)"
proof (transfer, simp, goal_cases)
case (1 c x v)
have id: "{v. x = v ∧ (x = v ⟶ c ≠ 0)} = (if c = 0 then {} else {x})" by auto
show ?case unfolding id
by (cases "c = 0", auto)
qed

lemma valuate_lp_monom_1[simp]: "((lp_monom 1 x) ⦃v⦄) = v x"
by transfer simp

lemma coeff_lp_monom [simp]:
shows "coeff (lp_monom c v) v' = (if v = v' then c else 0)"
by (transfer, auto)

lemma vars_uminus [simp]: "vars (-p) = vars p"
unfolding uminus_linear_poly_def
by transfer auto

lemma vars_plus [simp]: "vars (p1 + p2) ⊆ vars p1 ∪ vars p2"
by transfer auto

lemma vars_minus [simp]: "vars (p1 - p2) ⊆ vars p1 ∪ vars p2"
unfolding minus_linear_poly_def
using vars_plus[of p1 "-p2"] vars_uminus[of p2]
by simp

lemma vars_lp_monom: "vars (lp_monom r x) = (if r = 0 then {} else {x})"
by (transfer, auto)

lemma vars_scaleRat1: "vars (c *R p) ⊆ vars p"
by transfer auto

lemma vars_scaleRat: "c ≠ 0 ⟹ vars(c *R p) = vars p"
by transfer auto

lemma vars_Var [simp]: "vars (Var x) = {x}"
by transfer auto

lemma coeff_Var1 [simp]: "coeff (Var x) x = 1"
by transfer auto

lemma coeff_Var2: "x ≠ y ⟹ coeff (Var x) y = 0"
by transfer auto

lemma valuate_depend:
assumes "∀ x ∈ vars p. v x = v' x"
shows "(p ⦃v⦄) = (p ⦃v'⦄)"
using assms
by transfer auto

lemma valuate_update_x_lemma:
fixes v1 v2 :: "'a::rational_vector valuation"
assumes
"∀y. f y ≠ 0 ⟶ y ≠ x ⟶ v1 y = v2 y"
"finite {v. f v ≠ 0}"
shows
"(∑x∈{v. f v ≠ 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (∑x∈{v. f v ≠ 0}. f x *R v2 x)"
proof (cases "f x = 0")
case True
then have "∀y. f y ≠ 0 ⟶ v1 y = v2 y"
using assms(1) by auto
then show ?thesis using ‹f x = 0› by auto
next
case False
let ?A = "{v. f v ≠ 0}" and ?Ax = "{v. v ≠ x ∧ f v ≠ 0}"
have "?A = ?Ax ∪ {x}"
using ‹f x ≠ 0› by auto
then have "(∑x∈?A. f x *R v1 x) = f x *R v1 x + (∑x∈?Ax. f x *R v1 x)"
"(∑x∈?A. f x *R v2 x) = f x *R v2 x + (∑x∈?Ax. f x *R v2 x)"
using assms(2) by auto
moreover
have "∀ y ∈ ?Ax. v1 y = v2 y"
using assms by auto
moreover
have "f x *R v1 x + f x *R (v2 x - v1 x) = f x *R v2 x"
by (subst rational_vector.scale_right_diff_distrib) auto
ultimately
show ?thesis by simp
qed

lemma valuate_update_x:
fixes v1 v2 :: "'a::rational_vector valuation"
assumes "∀y ∈ vars lp. y≠x ⟶ v1 y = v2 y"
shows "lp ⦃v1⦄  + coeff lp x *R (v2 x - v1 x) = (lp ⦃v2⦄)"
using assms
unfolding valuate_def vars_def coeff_def
using valuate_update_x_lemma[of "Rep_linear_poly lp" x v1 v2] Rep_linear_poly
by auto

lemma vars_zero: "vars 0 = {}"
using zero_coeff_zero coeff_zero by auto

lemma vars_empty_zero: "vars lp = {} ⟷ lp = 0"
using zero_coeff_zero coeff_zero by auto

definition max_var:: "linear_poly ⇒ var" where
"max_var lp ≡ if lp = 0 then 0 else Max (vars lp)"

lemma max_var_max:
assumes "a ∈ vars lp"
shows "max_var lp ≥ a"
using assms
by (auto simp add: finite_vars max_var_def vars_zero)

lemma max_var_code[code]:
"max_var lp = (let vl = vars_list lp
in if vl = [] then 0 else foldl max (hd vl) (tl vl))"
proof (cases "lp = (0::linear_poly)")
case True
then show ?thesis
using set_vars_list[of lp]
by (auto simp add: max_var_def vars_zero)
next
case False
then show ?thesis
using set_vars_list[of lp, THEN sym]
using vars_empty_zero[of lp]
unfolding max_var_def Let_def
using Max.set_eq_fold[of "hd (vars_list lp)" "tl (vars_list lp)"]
by (cases "vars_list lp", auto simp: foldl_conv_fold intro!: fold_cong)
qed

definition monom_var:: "linear_poly ⇒ var" where
"monom_var l = max_var l"

definition monom_coeff:: "linear_poly ⇒ rat" where
"monom_coeff l = coeff l (monom_var l)"

definition is_monom :: "linear_poly ⇒ bool" where
"is_monom l ⟷ length (vars_list l) = 1"

lemma is_monom_vars_not_empty:
"is_monom l ⟹ vars l ≠ {}"

lemma monom_var_in_vars:
"is_monom l ⟹ monom_var l ∈ vars l"
using vars_zero
by (auto simp add: monom_var_def max_var_def is_monom_vars_not_empty finite_vars is_monom_def)

lemma zero_is_no_monom[simp]: "¬ is_monom 0"
using is_monom_vars_not_empty vars_zero by blast

lemma is_monom_monom_coeff_not_zero:
"is_monom l ⟹ monom_coeff l ≠ 0"
by (simp add: coeff_zero monom_var_in_vars monom_coeff_def)

lemma list_two_elements:
"⟦y ∈ set l; x ∈ set l; length l = Suc 0; y ≠ x⟧ ⟹ False"
by (induct l) auto

lemma is_monom_vars_monom_var:
assumes "is_monom l"
shows "vars l = {monom_var l}"
proof-
have "⋀x. ⟦is_monom l; x ∈ vars l⟧ ⟹ monom_var l = x"
proof-
fix x
assume "is_monom l" "x ∈ vars l"
then have "x ∈ set (vars_list l)"
using finite_vars
by (auto simp add: vars_list_def vars_def)
show "monom_var l = x"
proof(rule ccontr)
assume "monom_var l ≠ x"
then have "∃y. monom_var l = y ∧ y ≠ x"
by simp
then obtain y where "monom_var l = y" "y ≠ x"
by auto
then have "Rep_linear_poly l y ≠ 0"
using monom_var_in_vars ‹is_monom l›
then have "y ∈ set (vars_list l)"
using finite_vars
by (auto simp add: vars_def vars_list_def)
then show False
using ‹x ∈ set (vars_list l)› ‹is_monom l› ‹y ≠ x›
using list_two_elements
qed
qed
then show "vars l = {monom_var l}"
using assms
qed

lemma monom_valuate:
assumes "is_monom m"
shows "m⦃v⦄ = (monom_coeff m) *R v (monom_var m)"
using assms
using is_monom_vars_monom_var
by (simp add: vars_def coeff_def monom_coeff_def valuate_def)

lemma coeff_zero_simp [simp]:
"coeff 0 v = 0"
using zero_coeff_zero by blast

lemma poly_eq_iff: "p = q ⟷ (∀ v. coeff p v = coeff q v)"
by transfer auto

lemma poly_eqI:
assumes "⋀v. coeff p v = coeff q v"
shows "p = q"
using assms poly_eq_iff by simp

lemma coeff_sum_list:
assumes "distinct xs"
shows "coeff (∑x←xs. f x *R lp_monom 1 x) v = (if v ∈ set xs then f v else 0)"
using assms by (induction xs) auto

lemma linear_poly_sum:
"p ⦃ v ⦄ = (∑x∈vars p. coeff p x *R v x)"
by transfer simp

lemma all_valuate_zero: assumes "⋀(v::'a::lrv valuation). p ⦃v⦄ = 0"
shows "p = 0"
using all_val assms by blast

lemma linear_poly_eqI: assumes "⋀(v::'a::lrv valuation). (p ⦃v⦄) = (q ⦃v⦄)"
shows "p = q"
using assms
proof -
have "(p - q) ⦃ v ⦄ = 0" for v::"'a::lrv valuation"
using assms by (subst valuate_minus) auto
then have "p - q = 0"
by (intro all_valuate_zero) auto
then show ?thesis
by simp
qed

lemma monom_poly_assemble:
assumes "is_monom p"
shows "monom_coeff p *R lp_monom 1 (monom_var p) = p"
by (simp add: assms linear_poly_eqI monom_valuate valuate_scaleRat)

lemma coeff_sum: "coeff (sum (f :: _ ⇒ linear_poly) is) x = sum (λ i. coeff (f i) x) is"
by (induct "is" rule: infinite_finite_induct, auto)

end


# Theory Linear_Poly_Maps

(* Authors: F. Maric, M. Spasic, R. Thiemann *)
theory Linear_Poly_Maps
imports Abstract_Linear_Poly
"HOL-Library.Finite_Map"
begin

(* ************************************************************************** *)
(* Executable implementation                                                  *)
(* ************************************************************************** *)
definition get_var_coeff :: "(var, rat) fmap ⇒ var ⇒ rat" where
"get_var_coeff lp v == case fmlookup lp v of None ⇒ 0 | Some c ⇒ c"

definition set_var_coeff :: "var ⇒ rat ⇒ (var, rat) fmap ⇒ (var, rat) fmap" where
"set_var_coeff v c lp ==
if c = 0 then fmdrop v lp else fmupd v c lp"

lift_definition LinearPoly :: "(var, rat) fmap ⇒ linear_poly" is get_var_coeff
proof -
fix fmap
show "inv (get_var_coeff fmap)" unfolding inv_def
by (rule finite_subset[OF _ dom_fmlookup_finite[of fmap]],
auto intro: fmdom'I simp: get_var_coeff_def split: option.splits)
qed

definition ordered_keys :: "('a :: linorder, 'b)fmap ⇒ 'a list" where
"ordered_keys m = sorted_list_of_set (fset (fmdom m))"

context includes fmap.lifting lifting_syntax
begin

lemma [transfer_rule]: "(((=) ===> (=)) ===> pcr_linear_poly ===> (=)) (=) pcr_linear_poly"
by(standard,auto simp: pcr_linear_poly_def cr_linear_poly_def rel_fun_def OO_def)

lemma [transfer_rule]: "(pcr_fmap (=) (=) ===> pcr_linear_poly) (λ f x. case f x of None ⇒ 0 | Some x ⇒ x) LinearPoly"
by (standard, transfer, auto simp:get_var_coeff_def fmap.pcr_cr_eq cr_fmap_def)

lift_definition linear_poly_map :: "linear_poly ⇒ (var, rat) fmap" is
"λ lp x. if lp x = 0 then None else Some (lp x)" by (auto simp: dom_def)

lemma certificate[code abstype]:
"LinearPoly (linear_poly_map lp) = lp"
by (transfer, auto)

text‹Zero›
definition zero :: "(var, rat)fmap" where "zero = fmempty"

lemma [code abstract]:
"linear_poly_map 0 = zero" unfolding zero_def
by (transfer, auto)

definition add_monom :: "rat ⇒ var ⇒ (var, rat) fmap ⇒ (var, rat) fmap" where
"add_monom c v lp == set_var_coeff v (c + get_var_coeff lp v) lp"

definition add :: "(var, rat) fmap ⇒ (var, rat) fmap ⇒ (var, rat) fmap" where
"add lp1 lp2 = foldl (λ lp v. add_monom (get_var_coeff lp1 v) v lp) lp2 (ordered_keys lp1)"

"get_var_coeff lp v + c ≠ 0 ⟹
fmlookup (add_monom c v lp) v = Some (get_var_coeff lp v + c)"
"get_var_coeff lp v + c = 0 ⟹
fmlookup (add_monom c v lp) v = None"
"x ≠ v ⟹ fmlookup (add_monom c v lp) x = fmlookup lp x"
by auto

lemma fmlookup_fold_not_mem: "x ∉ set k1 ⟹
fmlookup (foldl (λlp v. add_monom (get_var_coeff P1 v) v lp) P2 k1) x
= fmlookup P2 x"
by (induct k1 arbitrary: P2, auto simp: lookup_add_monom)

lemma [code abstract]:
"linear_poly_map (p1 + p2) = add (linear_poly_map p1) (linear_poly_map p2)"
proof (rule fmap_ext)
fix x :: nat (* index *)
let ?p1 = "fmlookup (linear_poly_map p1) x"
let ?p2 = "fmlookup (linear_poly_map p2) x"
define P1 where "P1 = linear_poly_map p1"
define P2 where "P2 = linear_poly_map p2"
define k1 where "k1 = ordered_keys P1"
have k1: "distinct k1 ∧ fset (fmdom P1) = set k1" unfolding k1_def P1_def ordered_keys_def
by auto
have id: "fmlookup (linear_poly_map (p1 + p2)) x = (case ?p1 of None ⇒ ?p2 | Some y1 ⇒
(case ?p2 of None ⇒ Some y1 | Some y2 ⇒ if y1 + y2 = 0 then None else Some (y1 + y2)))"
by (transfer, auto)
show "fmlookup (linear_poly_map (p1 + p2)) x = fmlookup (add (linear_poly_map p1) (linear_poly_map p2)) x"
proof (cases "fmlookup P1 x")
case None
from fmdom_notI[OF None] have "x ∉ fset (fmdom P1)" by (meson notin_fset)
with k1 have x: "x ∉ set k1" by auto
show ?thesis unfolding id P1_def[symmetric] P2_def[symmetric] None
unfolding add_def k1_def[symmetric] fmlookup_fold_not_mem[OF x] by auto
next
case (Some y1)
from fmdomI[OF this] have "x ∈ fset (fmdom P1)" by (meson notin_fset)
with k1 have "x ∈ set k1" by auto
from split_list[OF this] obtain bef aft where k1_id: "k1 = bef @ x # aft" by auto
with k1 have x: "x ∉ set bef" "x ∉ set aft" by auto
have xy1: "get_var_coeff P1 x = y1" using Some unfolding get_var_coeff_def by auto
let ?P = "foldl (λlp v. add_monom (get_var_coeff P1 v) v lp) P2 bef"
show ?thesis unfolding id P1_def[symmetric] P2_def[symmetric] Some option.simps
unfolding add_def k1_def[symmetric] k1_id foldl_append foldl_Cons
unfolding fmlookup_fold_not_mem[OF x(2)] xy1
proof -
show "(case fmlookup P2 x of None ⇒ Some y1 | Some y2 ⇒ if y1 + y2 = 0 then None else Some (y1 + y2))
= fmlookup (add_monom y1 x ?P) x"
proof (cases "get_var_coeff ?P x + y1 = 0")
case True
from Some[unfolded P1_def] have y1: "y1 ≠ 0"
by (transfer, auto split: if_splits)
then show ?thesis unfolding lookup_add_monom(2)[OF True] using True
unfolding get_var_coeff_def[of _ x] fmlookup_fold_not_mem[OF x(1)]
by (auto split: option.splits)
next
case False
show ?thesis unfolding lookup_add_monom(1)[OF False] using False
unfolding get_var_coeff_def[of _ x] fmlookup_fold_not_mem[OF x(1)]
by (auto split: option.splits)
qed
qed
qed
qed

text‹Scaling›
definition scale :: "rat ⇒ (var, rat) fmap ⇒ (var, rat) fmap" where
"scale r lp = (if r = 0 then fmempty else (fmmap ((*) r) lp))"

lemma [code abstract]:
"linear_poly_map (r *R p) = scale r (linear_poly_map p)"
proof (cases "r = 0")
case True
then have *: "(r = 0) = True" by simp
show ?thesis unfolding scale_def * if_True using True
by (transfer, auto)
next
case False
then have *: "(r = 0) = False" by simp
show ?thesis unfolding scale_def * if_False using False
by (transfer, auto)
qed

(* Coeff *)
lemma coeff_code [code]:
"coeff lp = get_var_coeff (linear_poly_map lp)"
by (rule ext, unfold get_var_coeff_def, transfer, auto)

(* Var *)
lemma Var_code[code abstract]:
"linear_poly_map (Var x) = set_var_coeff x 1 fmempty"
unfolding set_var_coeff_def
by (transfer, auto split: if_splits simp: fun_eq_iff map_upd_def)

(* vars *)
lemma vars_code[code]: "vars lp = fset (fmdom (linear_poly_map lp))"
by (transfer, auto simp: Transfer.Rel_def rel_fun_def pcr_fset_def cr_fset_def)

(* vars_list *)
lemma vars_list_code[code]: "vars_list lp = ordered_keys (linear_poly_map lp)"
unfolding ordered_keys_def vars_code[symmetric]
by (transfer, auto)

(* valuate *)
lemma valuate_code[code]:  "valuate lp val = (
let lpm = linear_poly_map lp
in sum_list (map (λ x. (the (fmlookup lpm x)) *R (val x)) (vars_list lp)))"
unfolding Let_def
proof (subst sum_list_distinct_conv_sum_set)
show "distinct (vars_list lp)"
by (transfer, auto)
next
show "lp ⦃ val ⦄ =
(∑x∈set (vars_list lp). the (fmlookup (linear_poly_map lp) x) *R val x)"
unfolding set_vars_list
by (transfer, auto)
qed

end

lemma lp_monom_code[code]: "linear_poly_map (lp_monom c x) = (if c = 0 then fmempty else fmupd x c fmempty)"
proof (rule fmap_ext, goal_cases)
case (1 y)
include fmap.lifting
show ?case by (cases "c = 0", (transfer, auto)+)
qed

instantiation linear_poly :: equal
begin

definition "equal_linear_poly x y = (linear_poly_map x = linear_poly_map y)"

instance
proof (standard, unfold equal_linear_poly_def, standard)
fix x y
assume "linear_poly_map x = linear_poly_map y"
from arg_cong[OF this, of LinearPoly, unfolded certificate]
show "x = y" .
qed auto
end

end

# Theory QDelta

(* Authors: F. Maric, M. Spasic, R. Thiemann *)
section ‹Rational Numbers Extended with Infinitesimal Element›
theory QDelta
imports
Abstract_Linear_Poly
Simplex_Algebra
begin

datatype QDelta = QDelta rat rat

primrec qdfst :: "QDelta ⇒ rat" where
"qdfst (QDelta a b) = a"

primrec qdsnd :: "QDelta ⇒ rat" where
"qdsnd (QDelta a b) = b"

lemma [simp]: "QDelta (qdfst qd) (qdsnd qd) = qd"
by (cases qd) auto

lemma [simp]: "⟦QDelta.qdsnd x = QDelta.qdsnd y; QDelta.qdfst y = QDelta.qdfst x⟧ ⟹ x = y"
by (cases x) auto

instantiation QDelta :: rational_vector
begin

definition zero_QDelta :: "QDelta"
where
"0 = QDelta 0 0"

definition plus_QDelta :: "QDelta ⇒ QDelta ⇒ QDelta"
where
"qd1 + qd2 = QDelta (qdfst qd1 + qdfst qd2) (qdsnd qd1 + qdsnd qd2)"

definition minus_QDelta :: "QDelta ⇒ QDelta ⇒ QDelta"
where
"qd1 - qd2 = QDelta (qdfst qd1 - qdfst qd2) (qdsnd qd1 - qdsnd qd2)"

definition uminus_QDelta :: "QDelta ⇒ QDelta"
where
"- qd = QDelta (- (qdfst qd)) (- (qdsnd qd))"

definition scaleRat_QDelta :: "rat ⇒ QDelta ⇒ QDelta"
where
"r *R qd = QDelta (r*(qdfst qd)) (r*(qdsnd qd))"

instance
proof
qed (auto simp add: plus_QDelta_def zero_QDelta_def uminus_QDelta_def minus_QDelta_def scaleRat_QDelta_def field_simps)
end

instantiation QDelta :: linorder
begin
definition less_eq_QDelta :: "QDelta ⇒ QDelta ⇒ bool"
where
"qd1 ≤ qd2 ⟷ (qdfst qd1 < qdfst qd2) ∨ (qdfst qd1 = qdfst qd2 ∧ qdsnd qd1 ≤ qdsnd qd2)"

definition less_QDelta :: "QDelta ⇒ QDelta ⇒ bool"
where
"qd1 < qd2 ⟷ (qdfst qd1 < qdfst qd2) ∨ (qdfst qd1 = qdfst qd2 ∧ qdsnd qd1 < qdsnd qd2)"

instance proof qed (auto simp add: less_QDelta_def less_eq_QDelta_def)
end

instantiation QDelta:: linordered_rational_vector
begin
instance proof qed (auto simp add: plus_QDelta_def less_QDelta_def scaleRat_QDelta_def mult_strict_left_mono mult_strict_left_mono_neg)
end

instantiation QDelta :: lrv
begin
definition one_QDelta where
"one_QDelta = QDelta 1 0"
instance proof qed (auto simp add: one_QDelta_def zero_QDelta_def)
end

definition δ0 :: "QDelta ⇒ QDelta ⇒ rat"
where
"δ0 qd1 qd2 ==
let c1 = qdfst qd1; c2 = qdfst qd2; k1 = qdsnd qd1; k2 = qdsnd qd2 in
(if (c1 < c2 ∧ k1 > k2) then
(c2 - c1) / (k1 - k2)
else
1
)
"

definition val :: "QDelta ⇒ rat ⇒ rat"
where "val qd δ = (qdfst qd) + δ * (qdsnd qd)"

lemma val_plus:
"val (qd1 + qd2) δ = val qd1 δ + val qd2 δ"
by (simp add: field_simps val_def plus_QDelta_def)

lemma val_scaleRat:
"val (c *R qd) δ = c * val qd δ"
by (simp add: field_simps val_def scaleRat_QDelta_def)

lemma qdfst_setsum:
"finite A ⟹ qdfst (∑x∈A. f x) = (∑x∈A. qdfst (f x))"
by (induct A rule: finite_induct) (auto simp add: zero_QDelta_def plus_QDelta_def)

lemma qdsnd_setsum:
"finite A ⟹ qdsnd (∑x∈A. f x) = (∑x∈A. qdsnd (f x))"
by (induct A rule: finite_induct) (auto simp add: zero_QDelta_def plus_QDelta_def)

lemma valuate_valuate_rat:
"lp ⦃(λv. (QDelta (vl v) 0))⦄ = QDelta (lp⦃vl⦄) 0"
using Rep_linear_poly
by (simp add: valuate_def scaleRat_QDelta_def qdsnd_setsum qdfst_setsum)

lemma valuate_rat_valuate:
"lp⦃(λv. val (vl v) δ)⦄ = val (lp⦃vl⦄) δ"
unfolding valuate_def val_def
using rational_vector.scale_sum_right[of δ "λx. Rep_linear_poly lp x * qdsnd (vl x)" "{v :: nat. Rep_linear_poly lp v ≠ (0 :: rat)}"]
using Rep_linear_poly
by (auto simp add: field_simps sum.distrib qdfst_setsum qdsnd_setsum) (auto simp add: scaleRat_QDelta_def)

lemma delta0:
assumes "qd1 ≤ qd2"
shows "∀ ε. ε > 0 ∧ ε ≤ (δ0 qd1 qd2) ⟶ val qd1 ε ≤ val qd2 ε"
proof-
have "⋀ e c1 c2 k1 k2 :: rat. ⟦e ≥ 0; c1 < c2; k1 ≤ k2⟧ ⟹ c1 + e*k1 ≤ c2 + e*k2"
proof-
fix e c1 c2 k1 k2 :: rat
show "⟦e ≥ 0; c1 < c2; k1 ≤ k2⟧ ⟹ c1 + e*k1 ≤ c2 + e*k2"
using mult_left_mono[of "k1" "k2" "e"]
using add_less_le_mono[of "c1" "c2" "e*k1" "e*k2"]
by simp
qed
then show ?thesis
using assms
by (auto simp add: δ0_def val_def less_eq_QDelta_def Let_def field_simps mult_left_mono)
qed

primrec
δ_min ::"(QDelta × QDelta) list ⇒ rat" where
"δ_min [] = 1" |
"δ_min (h # t) = min (δ_min t) (δ0 (fst h) (snd h))"

lemma delta_gt_zero:
"δ_min l > 0"
by (induct l) (auto simp add: Let_def field_simps δ0_def)

lemma delta_le_one:
"δ_min l ≤ 1"
by (induct l, auto)

lemma delta_min_append:
"δ_min (as @ bs) = min (δ_min as) (δ_min bs)"
by (induct as, insert delta_le_one[of bs], auto)

lemma delta_min_mono: "set as ⊆ set bs ⟹ δ_min bs ≤ δ_min as"
proof (induct as)
case Nil
then show ?case using delta_le_one by simp
next
case (Cons a as)
from Cons(2) have "a ∈ set bs" by auto
from split_list[OF this]
obtain bs1 bs2 where bs: "bs = bs1 @ [a] @ bs2" by auto
have bs: "δ_min bs = δ_min ([a] @ bs)" unfolding bs delta_min_append by auto
show ?case unfolding bs using Cons(1-2) by auto
qed

lemma delta_min:
assumes "∀ qd1 qd2. (qd1, qd2) ∈ set qd ⟶ qd1 ≤ qd2"
shows "∀ ε. ε > 0 ∧ ε ≤ δ_min qd ⟶ (∀ qd1 qd2. (qd1, qd2) ∈ set qd ⟶ val qd1 ε ≤ val qd2 ε)"
using assms
using delta0
by (induct qd, auto)

lemma QDelta_0_0: "QDelta 0 0 = 0" by code_simp
lemma qdsnd_0: "qdsnd 0 = 0" by code_simp
lemma qdfst_0: "qdfst 0 = 0" by code_simp

end


# Theory Simplex

(* 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› or ‹p⇩1 ⨝ p⇩2›, where ‹p›, ‹p⇩1›, and ‹p⇩2›, are
linear polynomials, ‹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,
denoted by ‹⊨⇩c⇩s›, if all constraints are. There is also an indexed
version ‹⊨⇩i⇩c⇩s› which takes an explicit set of indices and then only
demands 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
| LTPP linear_poly linear_poly
| GTPP linear_poly linear_poly
| LEQPP linear_poly linear_poly
| GEQPP linear_poly linear_poly
| EQPP linear_poly linear_poly

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"
| "v ⊨⇩c LTPP l1 l2 ⟷ (l1⦃v⦄) < (l2⦃v⦄)"
| "v ⊨⇩c GTPP l1 l2 ⟷ (l1⦃v⦄) > (l2⦃v⦄)"
| "v ⊨⇩c LEQPP l1 l2 ⟷ (l1⦃v⦄) ≤ (l2⦃v⦄)"
| "v ⊨⇩c GEQPP l1 l2 ⟷ (l1⦃v⦄) ≥ (l2⦃v⦄)"
| "v ⊨⇩c EQPP l1 l2 ⟷ (l1⦃v⦄) = (l2⦃v⦄)"

abbreviation satisfies_constraints :: "rat valuation ⇒ constraint set ⇒ bool" (infixl "⊨⇩c⇩s" 100) where
"v ⊨⇩c⇩s cs ≡ ∀ c ∈ cs. v ⊨⇩c c"

lemma unsat_mono: assumes "¬ (∃ v. v ⊨⇩c⇩s cs)"
and "cs ⊆ ds"
shows "¬ (∃ v. v ⊨⇩c⇩s ds)"
using assms by auto

fun i_satisfies_cs (infixl "⊨⇩i⇩c⇩s" 100) where
"(I,v) ⊨⇩i⇩c⇩s cs ⟷ v ⊨⇩c⇩s 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) ⊨⇩i⇩c⇩s set ics))
∧ (distinct_indices ics ⟶ (∀ J. J ⊂ I ⟶ (∃ v. (J,v) ⊨⇩i⇩c⇩s 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 ⊨⇩c⇩s 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"  ("⟨_⟩")
translations
"⟨v⟩" == "CONST map2fun v"

lemma map2fun_def':
"⟨v⟩ x ≡ case Mapping.lookup v x of None ⇒ 0 | Some y ⇒ y"

text‹Note that the above specification requires returning a
valuation (defined as a HOL function), which is not efficiently
executable. In order to enable more efficient data structures for
representing valuations, a refinement of this specification is needed
and the function ‹solve› is replaced by the function ‹solve_exec› returning optional ‹(var, rat) mapping› instead
of ‹var ⇒ rat› function. This way, efficient data structures
for representing mappings can be easily plugged-in during code
generation \cite{florian-refinement}. A conversion from the ‹mapping› datatype to HOL function is denoted by ‹⟨_⟩› and
given 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⟩ ⊨⇩c⇩s 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
strict inequalities. Equalities can be easily rewritten to non-strict
inequalities. Removing strict inequalities can be done by replacing
the list of constraints by a new one, formulated over an extension
‹ℚ'› of the space of rationals ‹ℚ›. ‹ℚ'› must
have a structure of a linearly ordered vector space over ‹ℚ›
(represented by the type class ‹lrv›) and must guarantee that
if some non-strict constraints are satisfied in ‹ℚ'›, then
there 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
parameter ‹δ›). 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 ‹⊨⇩n⇩s› and ‹⊨⇩n⇩s⇩s›. The indexed variant is ‹⊨⇩i⇩n⇩s⇩s›.›
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 "⊨⇩n⇩s" 100) where
"v ⊨⇩n⇩s LEQ_ns l r ⟷ l⦃v⦄ ≤ r"
| "v ⊨⇩n⇩s GEQ_ns l r ⟷ l⦃v⦄ ≥ r"

abbreviation satisfies_ns_constraints :: "'a::lrv valuation ⇒ 'a ns_constraint set ⇒ bool" (infixl "⊨⇩n⇩s⇩s " 100) where
"v ⊨⇩n⇩s⇩s cs ≡ ∀ c ∈ cs. v ⊨⇩n⇩s c"

fun i_satisfies_ns_constraints :: "'i set × 'a::lrv valuation ⇒ ('i,'a) i_ns_constraint set ⇒ bool" (infixl "⊨⇩i⇩n⇩s⇩s " 100) where
"(I,v) ⊨⇩i⇩n⇩s⇩s cs ⟷ v ⊨⇩n⇩s⇩s restrict_to I cs"

lemma i_satisfies_ns_constraints_mono:
"(I,v) ⊨⇩i⇩n⇩s⇩s cs ⟹ J ⊆ I ⟹ (J,v) ⊨⇩i⇩n⇩s⇩s 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) ⊨⇩i⇩n⇩s⇩s cs))
∧ (distinct_indices_ns cs ⟶ (∀ J ⊂ I. ∃ v. (J,v) ⊨⇩i⇩n⇩s⇩s 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'⟩) ⊨⇩i⇩n⇩s⇩s set (to_ns cs) ⟹ (I,⟨from_ns v' (flat_list (to_ns cs))⟩) ⊨⇩i⇩c⇩s 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'⟩  ⊨⇩n⇩s⇩s flat (set (to_ns cs)) ⟹ ⟨from_ns v' (flat_list (to_ns cs))⟩ ⊨⇩c⇩s 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⟩ ⊨⇩n⇩s⇩s 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
only 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›
function can be easily defined and it can be easily shown that this
definition 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
constraints into an equisatisfiable form consisting of a list of
linear equations (called the \emph{tableau}) and of a list of
\emph{atoms} of the form ‹x⇩i ⨝ b⇩i› where ‹x⇩i› is a
variable and ‹b⇩i› is a constant (from the extension field). The
transformation is straightforward and introduces auxiliary variables
for linear polynomials occurring in the initial formula. For example,
‹[x⇩1 + x⇩2 ≤ b⇩1, x⇩1 + x⇩2 ≥ b⇩2, x⇩2 ≥ b⇩3]› can be transformed to
the tableau ‹[x⇩3 = x⇩1 + x⇩2]› and atoms ‹[x⇩3 ≤ b⇩1, x⇩3 ≥
b⇩2, x⇩2 ≥ b⇩3]›.›

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⦄"

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.
To observe the problem with 0 as rhs, consider the tableau $x = 0$ in combination
with atom $(A: x \leq 0)$ where then $(B: x \geq 1)$ is asserted.
In 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
a variable and ‹p› is a polynomial, and are represented by the
type ‹eq = var × linear_poly›. Semantics of equations is given
by @{thm satisfies_eq_iff[no_vars]}. Tableau is represented as a list
of equations, by the type ‹tableau = eq list›. Semantics for a
tableau is given by @{thm satisfies_tableau_def[no_vars]}. Functions
‹lvars› and ‹rvars› return sets of variables appearing on
the left hand side (lhs) and the right hand side (rhs) of a
tableau. Lhs variables are called \emph{basic} while rhs variables are
called \emph{non-basic} variables. A tableau ‹t› is
\emph{normalized} (denoted by @{term "△ t"}) iff no variable occurs on
the lhs of two equations in a tableau and if sets of lhs and rhs
variables 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
ultimately
show ?thesis
qed

text‹Elementary atoms are represented by the type ‹'a atom›
and semantics for atoms and sets of atoms is denoted by ‹⊨⇩a› and
‹⊨⇩a⇩s› 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 "⊨⇩a⇩s" 100) where
"v ⊨⇩a⇩s as ≡ ∀ a ∈ as. v ⊨⇩a a"

definition satisfies_atom' :: "'a::linorder valuation ⇒ 'a atom ⇒ bool" (infixl "⊨⇩a⇩e" 100) where
"v ⊨⇩a⇩e a ⟷ v (atom_var a) = atom_const a"

lemma satisfies_atom'_stronger: "v ⊨⇩a⇩e a ⟹ v ⊨⇩a a" by (cases a, auto simp: satisfies_atom'_def)

abbreviation satisfies_atom_set' :: "'a::linorder valuation ⇒ 'a atom set ⇒ bool" (infixl "⊨⇩a⇩e⇩s" 100) where
"v ⊨⇩a⇩e⇩s as ≡ ∀ a ∈ as. v ⊨⇩a⇩e a"

lemma satisfies_atom_set'_stronger: "v ⊨⇩a⇩e⇩s as ⟹ v ⊨⇩a⇩s 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 "⊨⇩i⇩a⇩s" 100) where
"(I,v) ⊨⇩i⇩a⇩s as ⟷ v ⊨⇩a⇩s restrict_to I as"

fun i_satisfies_atom_set' :: "'i set × 'a::linorder valuation ⇒ ('i,'a) i_atom set ⇒ bool" (infixl "⊨⇩i⇩a⇩e⇩s" 100) where
"(I,v) ⊨⇩i⇩a⇩e⇩s as ⟷ v ⊨⇩a⇩e⇩s restrict_to I as"

lemma i_satisfies_atom_set'_stronger: "Iv ⊨⇩i⇩a⇩e⇩s as ⟹ Iv ⊨⇩i⇩a⇩s as"
using satisfies_atom_set'_stronger[of _ "snd Iv"] by (cases Iv, auto)

lemma satisifies_atom_restrict_to_Cons: "v ⊨⇩a⇩s restrict_to I (set as) ⟹ (i ∈ I ⟹ v ⊨⇩a a)
⟹ v ⊨⇩a⇩s 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‹
The 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⟩) ⊨⇩i⇩a⇩s set as ⟹ ⟨v⟩ ⊨⇩t t ⟹ (I,⟨trans_v v⟩) ⊨⇩i⇩n⇩s⇩s set cs" and

preprocess_unsat: "preprocess cs = (t, as,trans_v,U) ⟹ (I,v) ⊨⇩i⇩n⇩s⇩s set cs ⟹ ∃ v'. (I,v') ⊨⇩i⇩a⇩s 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) ⊨⇩i⇩n⇩s⇩s 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⟩ ⊨⇩a⇩s flat (set as) ⟹ ⟨v⟩ ⊨⇩t t ⟹ ⟨trans_v v⟩ ⊨⇩n⇩s⇩s 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) ⊨⇩i⇩a⇩s as)) ∧
(distinct_indices_atoms as ⟶ (∀ J ⊂ I. ∃ v. v ⊨⇩t t ∧ (J,v) ⊨⇩i⇩a⇩e⇩s 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) ⊨⇩i⇩a⇩s as)"
"distinct_indices_atoms as ⟹ J ⊂ I ⟹ ∃ v. v ⊨⇩t t ∧ (J,v) ⊨⇩i⇩a⇩e⇩s 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⟩ ⊨⇩a⇩s 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
obtained, their satisfiability is checked by the
‹assert_all› function. Its precondition is that the starting
tableau is normalized, and its specification is analogue to the one for the
‹solve› function. If ‹preprocess› and ‹assert_all›
are available, the  ‹solve_exec_ns› can be defined, and it
can 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) ⊨⇩i⇩n⇩s⇩s 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) ⊨⇩i⇩a⇩e⇩s set as" by auto
from i_satisfies_atom_set'_stronger[OF model(2)]
have model': "(J, v) ⊨⇩i⇩a⇩s 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⟩) ⊨⇩i⇩a⇩s set as" by auto
from i_preprocess_sat[OF prep _ this(2,1)] ‹J ⊂ I› inter
have "(J, ⟨trans_v w⟩) ⊨⇩i⇩n⇩s⇩s set cs" by auto
then show "∃ w. (J, w) ⊨⇩i⇩n⇩s⇩s 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⟩ ⊨⇩n⇩s⇩s 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
iteratively 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
given variable. Bounds are of the form ‹l⇩i ≤ x⇩i ≤ u⇩i›, where
‹l⇩i› and ‹u⇩i› and are either scalars or $\pm \infty$. Each time a new atom is asserted, a bound for the
corresponding variable is updated (checking for conflict with the
previous bounds). Since bounds for a variable can be either finite or
$\pm \infty$, they are represented by (partial) maps from variables to
values (‹'a bounds = var ⇀ 'a›). Upper and lower bounds are
represented separately. Infinite bounds map to @{term None} and this
is reflected in the semantics:

\begin{small}
‹c ≥⇩u⇩b b ⟷ case b of None ⇒ False | Some b' ⇒ c ≥ b'›

‹c ≤⇩u⇩b 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 ("⊵⇩u⇩b") where
"⊵⇩u⇩b lt c b ≡ case b of None ⇒ False | Some b' ⇒ le lt b' c"
definition gtub ("⊳⇩u⇩b") where
"⊳⇩u⇩b lt c b ≡ case b of None ⇒ False | Some b' ⇒ lt b' c"
definition leub ("⊴⇩u⇩b") where
"⊴⇩u⇩b lt c b ≡ case b of None ⇒ True | Some b' ⇒ le lt c b'"
definition ltub ("⊲⇩u⇩b") where
"⊲⇩u⇩b lt c b ≡ case b of None ⇒ True | Some b' ⇒ lt c b'"
definition lelb ("⊴⇩l⇩b") where
"⊴⇩l⇩b lt c b ≡ case b of None ⇒ False | Some b' ⇒ le lt c b'"
definition ltlb ("⊲⇩l⇩b") where
"⊲⇩l⇩b lt c b ≡ case b of None ⇒ False | Some b' ⇒ lt c b'"
definition gelb ("⊵⇩l⇩b") where
"⊵⇩l⇩b lt c b ≡ case b of None ⇒ True | Some b' ⇒ le lt b' c"
definition gtlb ("⊳⇩l⇩b") where
"⊳⇩l⇩b lt c b ≡ case b of None ⇒ True | Some b' ⇒ lt b' c"

definition ge_ubound :: "'a::linorder ⇒ 'a option ⇒ bool" (infixl "≥⇩u⇩b" 100) where
"c ≥⇩u⇩b b = ⊵⇩u⇩b (<) c b"
definition gt_ubound :: "'a::linorder ⇒ 'a option ⇒ bool" (infixl ">⇩u⇩b" 100) where
"c >⇩u⇩b b = ⊳⇩u⇩b (<) c b"
definition le_ubound :: "'a::linorder ⇒ 'a option ⇒ bool" (infixl "≤⇩u⇩b" 100) where
"c ≤⇩u⇩b b = ⊴⇩u⇩b (<) c b"
definition lt_ubound :: "'a::linorder ⇒ 'a option ⇒ bool" (infixl "<⇩u⇩b" 100) where
"c <⇩u⇩b b = ⊲⇩u⇩b (<) c b"
definition le_lbound :: "'a::linorder ⇒ 'a option ⇒ bool" (infixl "≤⇩l⇩b" 100) where
"c ≤⇩l⇩b b = ⊴⇩l⇩b (<) c b"
definition lt_lbound :: "'a::linorder ⇒ 'a option ⇒ bool" (infixl "<⇩l⇩b" 100) where
"c <⇩l⇩b b = ⊲⇩l⇩b (<) c b"
definition ge_lbound :: "'a::linorder ⇒ 'a option ⇒ bool" (infixl "≥⇩l⇩b" 100) where
"c ≥⇩l⇩b b = ⊵⇩l⇩b (<) c b"
definition gt_lbound :: "'a::linorder ⇒ 'a option ⇒ bool" (infixl ">⇩l⇩b" 100) where
"c >⇩l⇩b b = ⊳⇩l⇩b (<) 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]:
"⊴⇩l⇩b (>) a b = ⊵⇩u⇩b (<) a b"
"⊴⇩u⇩b (>) a b = ⊵⇩l⇩b (<) a b"
"⊵⇩l⇩b (>) a b = ⊴⇩u⇩b (<) a b"
"⊵⇩u⇩b (>) a b = ⊴⇩l⇩b (<) a b"
"⊲⇩l⇩b (>) a b = ⊳⇩u⇩b (<) a b"
"⊲⇩u⇩b (>) a b = ⊳⇩l⇩b (<) a b"
"⊳⇩l⇩b (>) a b = ⊲⇩u⇩b (<) a b"
"⊳⇩u⇩b (>) a b = ⊲⇩l⇩b (<) a b"
by (case_tac[!] b) (auto simp add: bound_compare'_defs)

(* Auxiliary lemmas about bound comparison *)

lemma [simp]: "¬ c ≥⇩u⇩b None " "¬ c ≤⇩l⇩b None"

lemma neg_bounds_compare:
"(¬ (c ≥⇩u⇩b b)) ⟹ c <⇩u⇩b b" "(¬ (c ≤⇩u⇩b b)) ⟹ c >⇩u⇩b b"
"(¬ (c >⇩u⇩b b)) ⟹ c ≤⇩u⇩b b" "(¬ (c <⇩u⇩b b)) ⟹ c ≥⇩u⇩b b"
"(¬ (c ≤⇩l⇩b b)) ⟹ c >⇩l⇩b b" "(¬ (c ≥⇩l⇩b b)) ⟹ c <⇩l⇩b b"
"(¬ (c <⇩l⇩b b)) ⟹ c ≥⇩l⇩b b" "(¬ (c >⇩l⇩b b)) ⟹ c ≤⇩l⇩b b"
by (case_tac[!] b) (auto simp add: bound_compare_defs)

"⟦c ≥⇩u⇩b b; c <⇩u⇩b b⟧ ⟹ False" "⟦c ≤⇩u⇩b b; c >⇩u⇩b b⟧ ⟹ False"
"⟦c >⇩u⇩b b; c ≤⇩u⇩b b⟧ ⟹ False" "⟦c <⇩u⇩b b; c ≥⇩u⇩b b⟧ ⟹ False"
"⟦c ≤⇩l⇩b b; c >⇩l⇩b b⟧ ⟹ False" "⟦c ≥⇩l⇩b b; c <⇩l⇩b b⟧ ⟹ False"
"⟦c <⇩l⇩b b; c ≥⇩l⇩b b⟧ ⟹ False" "⟦c >⇩l⇩b b; c ≤⇩l⇩b b⟧ ⟹ False"
by (case_tac[!] b) (auto simp add: bound_compare_defs)

lemma compare_strict_nonstrict:
"x <⇩u⇩b b ⟹ x ≤⇩u⇩b b"
"x >⇩u⇩b b ⟹ x ≥⇩u⇩b b"
"x <⇩l⇩b b ⟹ x ≤⇩l⇩b b"
"x >⇩l⇩b b ⟹ x ≥⇩l⇩b b"
by (case_tac[!] b) (auto simp add: bound_compare_defs)

lemma [simp]:
"⟦ x ≤ c; c <⇩u⇩b b ⟧ ⟹ x <⇩u⇩b b"
"⟦ x < c; c ≤⇩u⇩b b ⟧ ⟹ x <⇩u⇩b b"
"⟦ x ≤ c; c ≤⇩u⇩b b ⟧ ⟹ x ≤⇩u⇩b b"
"⟦ x ≥ c; c >⇩l⇩b b ⟧ ⟹ x >⇩l⇩b b"
"⟦ x > c; c ≥⇩l⇩b b ⟧ ⟹ x >⇩l⇩b b"
"⟦ x ≥ c; c ≥⇩l⇩b b ⟧ ⟹ x ≥⇩l⇩b b"
by (case_tac[!] b) (auto simp add: bound_compare_defs)

lemma bounds_lg [simp]:
"⟦ c >⇩u⇩b b; x ≤⇩u⇩b b⟧ ⟹ x < c"
"⟦ c ≥⇩u⇩b b; x <⇩u⇩b b⟧ ⟹ x < c"
"⟦ c ≥⇩u⇩b b; x ≤⇩u⇩b b⟧ ⟹ x ≤ c"
"⟦ c <⇩l⇩b b; x ≥⇩l⇩b b⟧ ⟹ x > c"
"⟦ c ≤⇩l⇩b b; x >⇩l⇩b b⟧ ⟹ x > c"
"⟦ c ≤⇩l⇩b b; x ≥⇩l⇩b b⟧ ⟹ x ≥ c"
by (case_tac[!] b) (auto simp add: bound_compare_defs)

lemma bounds_compare_Some [simp]:
"x ≤⇩u⇩b Some c ⟷ x ≤ c" "x ≥⇩u⇩b Some c ⟷ x ≥ c"
"x <⇩u⇩b Some c ⟷ x < c" "x >⇩u⇩b Some c ⟷ x > c"
"x ≥⇩l⇩b Some c ⟷ x ≥ c" "x ≤⇩l⇩b Some c ⟷ x ≤ c"
"x >⇩l⇩b Some c ⟷ x > c" "x <⇩l⇩b Some c ⟷ x < c"

fun in_bounds where
"in_bounds x v (lb, ub) = (v x ≥⇩l⇩b lb x ∧ v x ≤⇩u⇩b 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 ≥⇩l⇩b lb x ∧ v x ≤⇩u⇩b ub x)"

lemma not_in_bounds:
"¬ (in_bounds x v (lb, ub)) = (v x <⇩l⇩b lb x ∨ v x >⇩u⇩b ub x)"
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 ⊨⇩a⇩s as ⟷ v ⊨⇩b (lb, ub))"
declare atoms_equiv_bounds.simps [simp del]

lemma atoms_equiv_bounds_simps:
"as ≐ (lb, ub) ≡ ∀ v. v ⊨⇩a⇩s as ⟷ v ⊨⇩b (lb, ub)"

text‹A valuation satisfies bounds iff the value of each variable
respects both its lower and upper bound, i.e, @{thm
satisfies_bounds_iff[no_vars]}. Asserted atoms are precisely encoded
by the current bounds in a state (denoted by ‹≐›) if every
valuation 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
candidate solution. Whenever a new atom is asserted, it is checked
whether the valuation is still satisfying. If not, the procedure tries
to fix that by changing it and changing the tableau if necessary (but
so that it remains equivalent to the initial tableau).›

text‹Therefore, the state of the procedure stores the tableau
(denoted by ‹𝒯›), lower and upper bounds (denoted by ‹ℬ⇩l› and ‹ℬ⇩u›, and ordered pair of lower and upper bounds
denoted by ‹ℬ›), candidate solution (denoted by ‹𝒱›)
and a flag (denoted by ‹𝒰›) indicating if unsatisfiability has
been 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
(𝒯: "tableau")
(ℬ⇩i⇩l: "('i,'a) bounds_index")
(ℬ⇩i⇩u: "('i,'a) bounds_index")
(𝒱: "(var, 'a) mapping")
(𝒰: bool)
(𝒰⇩c: "'i list option")

definition indexl :: "('i,'a) state ⇒ 'i bound_index" ("ℐ⇩l") where
"ℐ⇩l s = (fst o the) o look (ℬ⇩i⇩l s)"

definition boundsl :: "('i,'a) state ⇒ 'a bounds" ("ℬ⇩l") where
"ℬ⇩l s = map_option snd o look (ℬ⇩i⇩l s)"

definition indexu :: "('i,'a) state ⇒ 'i bound_index" ("ℐ⇩u") where
"ℐ⇩u s = (fst o the) o look (ℬ⇩i⇩u s)"

definition boundsu :: "('i,'a) state ⇒ 'a bounds" ("ℬ⇩u") where
"ℬ⇩u s = map_option snd o look (ℬ⇩i⇩u s)"

abbreviation BoundsIndicesMap ("ℬ⇩i") where  "ℬ⇩i s ≡ (ℬ⇩i⇩l s, ℬ⇩i⇩u s)"
abbreviation Bounds :: "('i,'a) state ⇒ 'a bounds × 'a bounds" ("ℬ") where  "ℬ s ≡ (ℬ⇩l s, ℬ⇩u s)"
abbreviation Indices :: "('i,'a) state ⇒ 'i bound_index × 'i bound_index" ("ℐ") where  "ℐ s ≡ (ℐ⇩l s, ℐ⇩u s)"
abbreviation BoundsIndices :: "('i,'a) state ⇒ ('a bounds × 'a bounds) × ('i bound_index × 'i bound_index)" ("ℬℐ")
where  "ℬℐ s ≡ (ℬ s, ℐ s)"

fun satisfies_bounds_index :: "'i set × 'a::lrv valuation ⇒ ('a bounds × 'a bounds) ×
('i bound_index × 'i bound_index) ⇒ bool" (infixl "⊨⇩i⇩b" 100) where
"(I,v) ⊨⇩i⇩b ((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 "⊨⇩i⇩b⇩e" 100) where
"(I,v) ⊨⇩i⇩b⇩e ((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) ⊨⇩i⇩a⇩s as ⟶ (I,v) ⊨⇩i⇩b bi)"
declare atoms_imply_bounds_index.simps[simp del]

lemma i_satisfies_atom_set_mono: "as ⊆ as' ⟹ v ⊨⇩i⇩a⇩s as' ⟹ v ⊨⇩i⇩a⇩s 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 ℬ s ∧ v ⊨⇩t 𝒯 s"

definition curr_val_satisfies_state :: "('i,'a::lrv) state ⇒ bool" ("⊨") where
"⊨ s ≡ ⟨𝒱 s⟩ ⊨⇩s s"

fun satisfies_state_index :: "'i set × 'a::lrv valuation ⇒ ('i,'a) state ⇒ bool" (infixl "⊨⇩i⇩s" 100) where
"(I,v) ⊨⇩i⇩s s ⟷ (v ⊨⇩t 𝒯 s ∧ (I,v) ⊨⇩i⇩b ℬℐ s)"
declare satisfies_state_index.simps[simp del]

fun satisfies_state_index' :: "'i set × 'a::lrv valuation ⇒ ('i,'a) state ⇒ bool" (infixl "⊨⇩i⇩s⇩e" 100) where
"(I,v) ⊨⇩i⇩s⇩e s ⟷ (v ⊨⇩t 𝒯 s ∧ (I,v) ⊨⇩i⇩b⇩e ℬℐ s)"
declare satisfies_state_index'.simps[simp del]

definition indices_state :: "('i,'a)state ⇒ 'i set" where
"indices_state s = { i. ∃ x b. look (ℬ⇩i⇩l s) x = Some (i,b) ∨ look (ℬ⇩i⇩u 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 (ℬ⇩i⇩l s) x = Some (i,b) ∨ look (ℬ⇩i⇩u s) x = Some (i,b)) ⟶
(look (ℬ⇩i⇩l s) x' = Some (i,b') ∨ look (ℬ⇩i⇩u s) x' = Some (i,b')) ⟶
(x = x' ∧ b = b')))"

lemma distinct_indices_stateD: assumes "distinct_indices_state s"
shows "look (ℬ⇩i⇩l s) x = Some (i,b) ∨ look (ℬ⇩i⇩u s) x = Some (i,b) ⟹ look (ℬ⇩i⇩l s) x' = Some (i,b') ∨ look (ℬ⇩i⇩u 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 (𝒰⇩c s)) ⊆ indices_state s ∧ (¬ (∃ v. (set (the (𝒰⇩c s)),v) ⊨⇩i⇩s s)))"

definition subsets_sat_core :: "('i,'a::lrv) state ⇒ bool" where
"subsets_sat_core s = ((∀ I. I ⊂ set (the (𝒰⇩c s)) ⟶ (∃ v. (I,v) ⊨⇩i⇩s⇩e 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) ⊨⇩i⇩a⇩s as)" by blast
with i_satisfies_atom_set_mono[OF sub]
show "(∄v. v ⊨⇩t t ∧ (I, v) ⊨⇩i⇩a⇩s 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) ⊨⇩i⇩a⇩e⇩s as" by blast
have "(J, v) ⊨⇩i⇩a⇩e⇩s 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 ⊨⇩a⇩e b" by force
thus "v ⊨⇩a⇩e a" using id unfolding satisfies_atom'_def by auto
qed
with v show "∃v. v ⊨⇩t t ∧ (J, v) ⊨⇩i⇩a⇩e⇩s bs" by blast
qed

lemma state_satisfies_index: assumes "v ⊨⇩s s"
shows "(I,v) ⊨⇩i⇩s 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 𝒯 s" and bnd: "v x ≥⇩l⇩b ℬ⇩l s x" "v x ≤⇩u⇩b ℬ⇩u s x" by auto
show "v ⊨⇩t 𝒯 s" by fact
show "ℬ⇩l s x = Some c ⟹ ℐ⇩l s x ∈ I ⟹ c ≤ v x"
using bnd(1) by auto
show "ℬ⇩u s x = Some c ⟹ ℐ⇩u 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 (𝒯 s). Mapping.lookup (𝒱 s) x ≠ None"

definition index_valid where
"index_valid as (s :: ('i,'a) state) = (∀ x b i.
(look (ℬ⇩i⇩l s) x = Some (i,b) ⟶ ((i, Geq x b) ∈ as))
∧ (look (ℬ⇩i⇩u 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
satisfy the initial tableau and list of atoms. Since tableau is
changed only by equivalency preserving transformations and asserted
atoms are encoded in the bounds, a valuation is a solution if it
satisfies both the tableau and the bounds in the final state (when all
atoms have been asserted). So, a valuation ‹v› satisfies a state
‹s› (denoted by ‹⊨⇩s›) if it satisfies the tableau and
the bounds, i.e., @{thm satisfies_state_def [no_vars]}. Since ‹𝒱› should be a candidate solution, it should satisfy the state
(unless the ‹𝒰› flag is raised). This is denoted by ‹⊨ s›
and defined by @{thm curr_val_satisfies_state_def[no_vars]}. ‹∇
s› will denote that all variables of ‹𝒯 s› are explicitly
valuated in ‹𝒱 s›.›

definition updateℬℐ where
[simp]: "updateℬℐ field_update i x c s = field_update (upd x (i,c)) s"

fun ℬ⇩i⇩u_update where
"ℬ⇩i⇩u_update up (State T BIL BIU V U UC) = State T BIL (up BIU) V U UC"

fun ℬ⇩i⇩l_update where
"ℬ⇩i⇩l_update up (State T BIL BIU V U UC) = State T (up BIL) BIU V U UC"

fun 𝒱_update where
"𝒱_update V (State T BIL BIU V_old U UC) = State T BIL BIU V U UC"

fun 𝒯_update where
"𝒯_update T (State T_old BIL BIU V U UC) = State T BIL BIU V U UC"

lemma update_simps[simp]:
"ℬ⇩i⇩u (ℬ⇩i⇩u_update up s) = up (ℬ⇩i⇩u s)"
"ℬ⇩i⇩l (ℬ⇩i⇩u_update up s) = ℬ⇩i⇩l s"
"𝒯 (ℬ⇩i⇩u_update up s) = 𝒯 s"
"𝒱 (ℬ⇩i⇩u_update up s) = 𝒱 s"
"𝒰 (ℬ⇩i⇩u_update up s) = 𝒰 s"
"𝒰⇩c (ℬ⇩i⇩u_update up s) = 𝒰⇩c s"
"ℬ⇩i⇩l (ℬ⇩i⇩l_update up s) = up (ℬ⇩i⇩l s)"
"ℬ⇩i⇩u (ℬ⇩i⇩l_update up s) = ℬ⇩i⇩u s"
"𝒯 (ℬ⇩i⇩l_update up s) = 𝒯 s"
"𝒱 (ℬ⇩i⇩l_update up s) = 𝒱 s"
"𝒰 (ℬ⇩i⇩l_update up s) = 𝒰 s"
"𝒰⇩c (ℬ⇩i⇩l_update up s) = 𝒰⇩c s"
"𝒱 (𝒱_update V s) = V"
"ℬ⇩i⇩l (𝒱_update V s) = ℬ⇩i⇩l s"
"ℬ⇩i⇩u (𝒱_update V s) = ℬ⇩i⇩u s"
"𝒯 (𝒱_update V s) = 𝒯 s"
"𝒰 (𝒱_update V s) = 𝒰 s"
"𝒰⇩c (𝒱_update V s) = 𝒰⇩c s"
"𝒯 (𝒯_update T s) = T"
"ℬ⇩i⇩l (𝒯_update T s) = ℬ⇩i⇩l s"
"ℬ⇩i⇩u (𝒯_update T s) = ℬ⇩i⇩u s"
"𝒱 (𝒯_update T s) = 𝒱 s"
"𝒰 (𝒯_update T s) = 𝒰 s"
"𝒰⇩c (𝒯_update T s) = 𝒰⇩c s"
by (atomize(full), cases s, auto)

declare
ℬ⇩i⇩u_update.simps[simp del]
ℬ⇩i⇩l_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]: "ℬ⇩i⇩l (set_unsat I s) = ℬ⇩i⇩l s"
"ℬ⇩i⇩u (set_unsat I s) = ℬ⇩i⇩u s"
"𝒯 (set_unsat I s) = 𝒯 s"
"𝒱 (set_unsat I s) = 𝒱 s"
"𝒰 (set_unsat I s) = True"
"𝒰⇩c (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 (<) ℬ⇩i⇩l ℬ⇩i⇩u ℬ⇩l ℬ⇩u ℐ⇩l ℐ⇩u ℬ⇩i⇩u_update Leq Geq (≤)"

definition Negative where
[simp]: "Negative ≡ Direction (>) ℬ⇩i⇩u ℬ⇩i⇩l ℬ⇩u ℬ⇩l ℐ⇩u ℐ⇩l ℬ⇩i⇩l_update Geq Leq (≥)"

text‹Assuming that the ‹𝒰› flag and the current valuation
‹𝒱› in the final state determine the solution of a problem, the
‹assert_all› function can be reduced to the ‹assert_all_state›
function that operates on the states:
@{text[display] "assert_all t as ≡ let s = assert_all_state t as in
if (𝒰 s) then (False, None) else (True, Some (𝒱 s))" }
›
text‹Specification for the ‹assert_all_state› can be directly
obtained from the specification of ‹assert_all›, and it describes
the connection between the valuation in the final state and the
initial tableau and atoms. However, we will make an additional
refinement step and give stronger assumptions about the ‹assert_all_state› function that describes the connection between
the initial tableau and atoms with the tableau and bounds in the final
state.›

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 𝒯 s'" and

― ‹If @{term 𝒰} is not raised, then the valuation in the
final state satisfies its tableau and its bounds (that are, in this
case, equivalent to the set of all asserted bounds).›
assert_all_state_sat: "△ t ⟹ assert_all_state t as = s' ⟹ ¬ 𝒰 s' ⟹ ⊨ s'" and

assert_all_state_sat_atoms_equiv_bounds: "△ t ⟹ assert_all_state t as = s' ⟹ ¬ 𝒰 s' ⟹ flat (set as) ≐ ℬ s'" and

― ‹If @{term 𝒰} 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' ⟹ 𝒰 s' ⟹ minimal_unsat_state_core s'"  and

assert_all_state_unsat_atoms_equiv_bounds: "△ t ⟹ assert_all_state t as = s' ⟹ 𝒰 s' ⟹ set as ⊨⇩i ℬℐ 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 (𝒰 s) then Unsat (the (𝒰⇩c s)) else Sat (𝒱 s)"
end

text‹The ‹assert_all_state› function can be implemented by first
applying the ‹init› function that creates an initial state based
on 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 (𝒰 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 ⟹ △ (𝒯 (init t))"
assumes init'_tableau_equiv: "△ t ⟹ (v::'a valuation) ⊨⇩t t = v ⊨⇩t 𝒯 (init t)"
assumes init'_sat: "△ t ⟹ ¬ 𝒰 (init t) ⟶ ⊨ (init t)"
assumes init'_unsat: "△ t ⟹ 𝒰 (init t) ⟶ minimal_unsat_state_core (init t)"
assumes init'_atoms_equiv_bounds: "△ t ⟹ {} ≐ ℬ (init t)"
assumes init'_atoms_imply_bounds_index: "△ t ⟹ {} ⊨⇩i ℬℐ (init t)"

text‹Specification for ‹init› can be obtained from the
specification of ‹asser_all_state› since all its assumptions
must also hold for ‹init› (when the list of atoms is
empty). Also, since ‹init› is the first step in the ‹assert_all_state› implementation, the precondition for ‹init›
the same as for the ‹assert_all_state›. However,
unsatisfiability is never going to be detected during initialization
and @{term 𝒰} flag is never going to be raised. Also, the tableau in
the initial state can just be initialized with the starting
tableau. The condition @{term "{} ≐ ℬ (init t)"} is equivalent to
asking 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: "𝒯 (init t) = t" and

― ‹Since unsatisfiability is not detected, @{text 𝒰}
flag must not be set:› init_unsat_flag: "¬ 𝒰 (init t)" and

― ‹The current valuation must satisfy the tableau:› init_satisfies_tableau: "⟨𝒱 (init t)⟩ ⊨⇩t t" and

― ‹In an inital state no atoms are yet asserted so the bounds
must be empty:›
init_bounds: "ℬ⇩i⇩l (init t) = Mapping.empty"   "ℬ⇩i⇩u (init t) = Mapping.empty"  and

― ‹All tableau vars are valuated:› init_tableau_valuated: "∇ (init t)"

begin

lemma init_satisfies_bounds:
"⟨𝒱 (init t)⟩ ⊨⇩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:
"{} ≐ ℬ (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 ℬℐ (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 ⟹ △ (𝒯 (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
atom. Since the ‹init› function does not raise the ‹𝒰›
flag, from the definition of ‹assert_loop›, it is clear that the
flag is not raised when the ‹assert› function is
called. Moreover, the assumptions about the ‹assert_all_state›
imply that the loop invariant must be that if the ‹𝒰› flag is
not raised, then the current valuation must satisfy the state (i.e.,
‹⊨ s›). The ‹assert› function will be more easily
implemented if it is always applied to a state with a normalized and
valuated tableau, so we make this another loop invariant. Therefore,
the precondition for the ‹assert a s› function call is that
‹¬ 𝒰 s›, ‹⊨ s›, ‹△ (𝒯 s)› and ‹∇ s›
hold. The specification for ‹assert› directly follows from the
specification of ‹assert_all_state› (except that it is
additionally required that bounds reflect asserted atoms also when
unsatisfiability 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: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ let s' = assert a s in
((v::'a valuation) ⊨⇩t 𝒯 s ⟷ v ⊨⇩t 𝒯 s') ∧ △ (𝒯 s') ∧ ∇ s'" and

― ‹If the @{term 𝒰} flag is not raised, then the current
valuation is updated so that it satisfies the current tableau and
the current bounds.›
assert_sat: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ ¬ 𝒰 (assert a s) ⟹ ⊨ (assert a s)" and

― ‹The set of asserted atoms remains equivalent to the bounds
in the state.›
assert_atoms_equiv_bounds: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ flat ats ≐ ℬ s ⟹ flat (ats ∪ {a}) ≐ ℬ (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: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ ats ⊨⇩i ℬℐ s ⟹
insert a ats ⊨⇩i ℬℐ (assert a s)" and

― ‹If the @{term 𝒰} flag is raised, then there is no valuation
that satisfies both the current tableau and the current bounds.›
assert_unsat: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s; index_valid ats s⟧ ⟹ 𝒰 (assert a s) ⟹  minimal_unsat_state_core (assert a s)" and

assert_index_valid: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ index_valid ats s ⟹ index_valid (insert a ats) (assert a s)"

begin
lemma assert_tableau_equiv: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ (v::'a valuation) ⊨⇩t 𝒯 s ⟷ v ⊨⇩t 𝒯 (assert a s)"
using assert_tableau

lemma assert_tableau_normalized: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ △ (𝒯 (assert a s))"
using assert_tableau

lemma assert_tableau_valuated: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ ∇ (assert a s)"
using assert_tableau
end

locale AssertAllState' = Init init + Assert assert for
init :: "tableau ⇒ ('i,'a::lrv) state" and assert :: "('i,'a) i_atom ⇒ ('i,'a) state ⇒ ('i,'a) state"
begin

definition assert_loop where
"assert_loop as s ≡ foldl (λ s' a. if (𝒰 s') then s' else assert a s') s as"

definition assert_all_state where [simp]:
"assert_all_state t as ≡ assert_loop as (init t)"

lemma AssertAllState'_precond:
"△ t ⟹ △ (𝒯 (assert_all_state t as))
∧ (∇ (assert_all_state t as))
∧ (¬ 𝒰 (assert_all_state t as) ⟶ ⊨ (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
"△ t"
"P {} (init t)"
"⋀ as bs t. as ⊆ bs ⟹ P as t ⟹ P bs t"
"⋀ s a as. ⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s; P as s; index_valid as s⟧ ⟹ 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) ∧ 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 = "λs' a. if 𝒰 s' then s' else assert a s'"
let ?s = "foldl ?f (init t) as'"
show ?case
proof (cases "𝒰 ?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: "△ t ⟹ 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:
"△ t ⟹ ¬ 𝒰 (assert_all_state t as) ⟹ flat (set as) ≐ ℬ (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 "△ t"
shows "set as ⊨⇩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 "𝒰 ?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' ⊨⇩i ℬℐ ?s" by auto
from AssertAllState'_precond[of t as'] assms False
have "⊨ ?s" "△ (𝒯 ?s)" "∇ ?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‹Under these assumptions, it can easily be shown (mainly by
induction) that the previously shown implementation of ‹assert_all_state› satisfies its specification.›

sublocale AssertAllState' < AssertAllState assert_all_state
proof
fix v::"'a valuation" and t as s'
assume *: "△ t" and id: "assert_all_state t as = s'"
note idsym = id[symmetric]

show "v ⊨⇩t t = v ⊨⇩t 𝒯 s'" unfolding idsym
using  init_tableau_id[of t] assert_tableau_equiv[of _ v]
by (induct rule: AssertAllState'Induct) (auto simp add: * )

show "¬ 𝒰 s' ⟹ ⊨ s'" unfolding idsym
using AssertAllState'_precond by (simp add: * )

show "¬ 𝒰 s' ⟹ flat (set as) ≐ ℬ s'"
unfolding idsym
using *
by (rule AssertAllState'_sat_atoms_equiv_bounds)

show "𝒰 s' ⟹ set as ⊨⇩i ℬℐ s'"
using * unfolding idsym
by (rule AssertAllState'_unsat_atoms_implies_bounds)

show "𝒰 s' ⟹ 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' ⊆ 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‹Asserting Single Atoms›

text‹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, ‹check› performs the full simplex
algorithm. The ‹assert› function can be implemented as ‹assert a s = check (assert_bound a s)›. 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 ‹x ⨝ b› begins with the function
‹assert_bound›.  If the atom is subsumed by the current bounds,
then no changes are performed. Otherwise, bounds for ‹x› are
changed to incorporate the atom. If the atom is inconsistent with the
previous bounds for ‹x›, the @{term 𝒰} flag is raised. If
‹x› is not a lhs variable in the current tableau and if the
value for ‹x› in the current valuation violates the new bound
‹b›, the value for ‹x› can be updated and set to
‹b›, meanwhile updating the values for lhs variables of
the tableau so that it remains satisfied. Otherwise, no changes to the
current valuation are performed.›

fun satisfies_bounds_set  :: "'a::linorder valuation ⇒ 'a bounds × 'a bounds ⇒ var set ⇒ bool" where
"satisfies_bounds_set v (lb, ub) S ⟷ (∀ x ∈ S. in_bounds x v (lb, ub))"
declare satisfies_bounds_set.simps [simp del]
syntax
"_satisfies_bounds_set" :: "(var ⇒ 'a::linorder) ⇒ 'a bounds × 'a bounds ⇒ var set ⇒ bool"    ("_ ⊨⇩b _ ∥/ _")
translations
"v ⊨⇩b b ∥ S" == "CONST satisfies_bounds_set v b S"
lemma satisfies_bounds_set_iff:
"v ⊨⇩b (lb, ub) ∥ S ≡ (∀ x ∈ S. v x ≥⇩l⇩b lb x ∧ v x ≤⇩u⇩b ub x)"

definition curr_val_satisfies_no_lhs ("⊨⇩n⇩o⇩l⇩h⇩s") where
"⊨⇩n⇩o⇩l⇩h⇩s s ≡ ⟨𝒱 s⟩ ⊨⇩t (𝒯 s) ∧ (⟨𝒱 s⟩ ⊨⇩b (ℬ s) ∥ (- lvars (𝒯 s)))"
lemma satisfies_satisfies_no_lhs:
"⊨ s ⟹ ⊨⇩n⇩o⇩l⇩h⇩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 ⇒ bool" ("◇") where
"◇ s ≡
∀ x. if ℬ⇩l s x = None ∨ ℬ⇩u s x = None then True else the (ℬ⇩l s x) ≤ the (ℬ⇩u s x)"

text‹So, the ‹assert_bound› 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 ‹v
⊨⇩b (lb, ub) ∥ S›, and define @{thm
satisfies_bounds_set_iff[no_vars]}, and @{thm
curr_val_satisfies_no_lhs_def[no_vars]}. The ‹assert_bound›
function raises the ‹𝒰› flag if and only if lower and upper
bounds overlap. This is formalized as @{thm
bounds_consistent_def[no_vars]}.›

lemma satisfies_bounds_consistent:
"(v::'a::linorder valuation) ⊨⇩b ℬ s ⟶ ◇ s"
unfolding satisfies_bounds.simps in_bounds.simps bounds_consistent_def bound_compare_defs
by (auto split: option.split) force

lemma satisfies_consistent:
"⊨ s ⟶ ◇ s"
by (auto simp add: curr_val_satisfies_state_def satisfies_state_def satisfies_bounds_consistent)

lemma bounds_consistent_geq_lb:
"⟦◇ s; ℬ⇩u s x⇩i = Some c⟧
⟹ c ≥⇩l⇩b ℬ⇩l s x⇩i"
unfolding bounds_consistent_def
by (cases "ℬ⇩l s x⇩i", auto simp add: bound_compare_defs split: if_splits)
(erule_tac x="x⇩i" in allE, auto)

lemma bounds_consistent_leq_ub:
"⟦◇ s; ℬ⇩l s x⇩i = Some c⟧
⟹ c ≤⇩u⇩b ℬ⇩u s x⇩i"
unfolding bounds_consistent_def
by (cases "ℬ⇩u s x⇩i", auto simp add: bound_compare_defs split: if_splits)
(erule_tac x="x⇩i" in allE, auto)

lemma bounds_consistent_gt_ub:
"⟦◇ s; c <⇩l⇩b ℬ⇩l s x ⟧ ⟹ ¬ c >⇩u⇩b ℬ⇩u s x"
unfolding bounds_consistent_def
by (case_tac[!] "ℬ⇩l s x", case_tac[!] "ℬ⇩u s x")
(auto simp add: bound_compare_defs, erule_tac x="x" in allE, simp)

lemma bounds_consistent_lt_lb:
"⟦◇ s; c >⇩u⇩b ℬ⇩u s x ⟧ ⟹ ¬ c <⇩l⇩b ℬ⇩l s x"
unfolding bounds_consistent_def
by (case_tac[!] "ℬ⇩l s x", case_tac[!] "ℬ⇩u s x")
(auto simp add: bound_compare_defs, erule_tac x="x" in allE, simp)

text‹Since the ‹assert_bound› is the first step in the ‹assert› function implementation, the preconditions for ‹assert_bound› are the same as preconditions for the ‹assert›
function. The specifiction for the ‹assert_bound› is:›

locale AssertBound = fixes assert_bound::"('i,'a::lrv) i_atom ⇒ ('i,'a) state ⇒ ('i,'a) state"
assumes
― ‹The tableau remains unchanged and valuated.›

assert_bound_tableau: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ assert_bound a s = s' ⟹ 𝒯 s' = 𝒯 s ∧ ∇ s'" and

― ‹If the @{term 𝒰} 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.›
assert_bound_sat: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ assert_bound a s = s' ⟹ ¬ 𝒰 s' ⟹ ⊨⇩n⇩o⇩l⇩h⇩s s' ∧ ◇ s'" and

― ‹The set of asserted atoms remains equivalent to the bounds in the state.›

assert_bound_atoms_equiv_bounds: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹
flat ats ≐ ℬ s ⟹ flat (ats ∪ {a}) ≐ ℬ (assert_bound a s)" and

assert_bound_atoms_imply_bounds_index: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹
ats ⊨⇩i ℬℐ s ⟹ insert a ats ⊨⇩i ℬℐ (assert_bound a s)" and

― ‹@{term 𝒰} flag is raised, only if the bounds became inconsistent:›

assert_bound_unsat: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ index_valid as s ⟹ assert_bound a s = s' ⟹ 𝒰 s' ⟹ minimal_unsat_state_core s'" and

assert_bound_index_valid: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ index_valid as s ⟹ index_valid (insert a as) (assert_bound a s)"

begin
lemma assert_bound_tableau_id: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ 𝒯 (assert_bound a s) = 𝒯 s"
using assert_bound_tableau by blast

lemma assert_bound_tableau_valuated: "⟦¬ 𝒰 s; ⊨ s; △ (𝒯 s); ∇ s⟧ ⟹ ∇ (assert_bound a s)"
using assert_bound_tableau by blast

end

locale AssertBoundNoLhs =
fixes assert_bound :: "('i,'a::lrv) i_atom ⇒ ('i,'a) state ⇒ ('i,'a) state"
assumes assert_bound_nolhs_tableau_id: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; △ (𝒯 s); ∇ s; ◇ s⟧ ⟹ 𝒯 (assert_bound a s) = 𝒯 s"
assumes assert_bound_nolhs_sat: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; △ (𝒯 s); ∇ s; ◇ s⟧ ⟹
¬ 𝒰 (assert_bound a s) ⟹ ⊨⇩n⇩o⇩l⇩h⇩s (assert_bound a s) ∧ ◇ (assert_bound a s)"
assumes assert_bound_nolhs_atoms_equiv_bounds: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; △ (𝒯 s); ∇ s; ◇ s⟧ ⟹
flat ats ≐ ℬ s ⟹ flat (ats ∪ {a}) ≐ ℬ (assert_bound a s)"
assumes assert_bound_nolhs_atoms_imply_bounds_index: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; △ (𝒯 s); ∇ s; ◇ s⟧ ⟹
ats ⊨⇩i ℬℐ s ⟹ insert a ats ⊨⇩i ℬℐ (assert_bound a s)"
assumes assert_bound_nolhs_unsat: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; △ (𝒯 s); ∇ s; ◇ s⟧ ⟹
index_valid as s ⟹ 𝒰 (assert_bound a s) ⟹ minimal_unsat_state_core (assert_bound a s)"
assumes assert_bound_nolhs_tableau_valuated: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; △ (𝒯 s); ∇ s; ◇ s⟧ ⟹
∇ (assert_bound a s)"
assumes assert_bound_nolhs_index_valid: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; △ (𝒯 s); ∇ s; ◇ s⟧ ⟹
index_valid as s ⟹ 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‹The second phase of ‹assert›, the ‹check› function,
is the heart of the Simplex algorithm. It is always called after
‹assert_bound›, but in two different situations. In the first
case ‹assert_bound› raised the ‹𝒰› flag and then
‹check› should retain the flag and should not perform any changes.
In the second case ‹assert_bound› did not raise the
‹𝒰› flag, so ‹⊨⇩n⇩o⇩l⇩h⇩s s›, ‹◇ s›, ‹△ (𝒯
s)›, and ‹∇ s› hold.›

locale Check = fixes check::"('i,'a::lrv) state ⇒ ('i,'a) state"
assumes
― ‹If @{text check} is called from an inconsistent state, the state is unchanged.›

check_unsat_id: "𝒰 s ⟹ check s = s"  and

― ‹The tableau remains equivalent to the previous one, normalized and valuated.›

check_tableau:  "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; ◇ s; △ (𝒯 s); ∇ s⟧ ⟹
let s' = check s in ((v::'a valuation) ⊨⇩t 𝒯 s ⟷ v ⊨⇩t 𝒯 s') ∧ △ (𝒯 s') ∧ ∇ s'" and

― ‹The bounds remain unchanged.›

check_bounds_id:  "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; ◇ s; △ (𝒯 s); ∇ s⟧ ⟹ ℬ⇩i (check s) = ℬ⇩i s"  and

― ‹If @{term 𝒰} flag is not raised, the current valuation
@{text "𝒱"} satisfies both the tableau and the bounds and if it is
raised, there is no valuation that satisfies them.›

check_sat: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; ◇ s; △ (𝒯 s); ∇ s⟧ ⟹ ¬ 𝒰 (check s) ⟹ ⊨ (check s)"  and

check_unsat: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; ◇ s; △ (𝒯 s); ∇ s⟧ ⟹ 𝒰 (check s) ⟹ minimal_unsat_state_core (check s)"

begin

lemma check_tableau_equiv: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; ◇ s; △ (𝒯 s); ∇ s⟧ ⟹
(v::'a valuation) ⊨⇩t 𝒯 s ⟷ v ⊨⇩t 𝒯 (check s)"
using check_tableau

lemma check_tableau_index_valid: assumes "¬ 𝒰 s" " ⊨⇩n⇩o⇩l⇩h⇩s s" "◇ s" "△ (𝒯 s)" "∇ 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: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; ◇ s; △ (𝒯 s); ∇ s⟧ ⟹ △ (𝒯 (check s))"
using check_tableau

lemma check_tableau_valuated: "⟦¬ 𝒰 s; ⊨⇩n⇩o⇩l⇩h⇩s s; ◇ s; △ (𝒯 s); ∇ s⟧ ⟹ ∇ (check s)"
using check_tableau

lemma check_indices_state: assumes "¬ 𝒰 s ⟹ ⊨⇩n⇩o⇩l⇩h⇩s s" "¬ 𝒰 s ⟹ ◇ s" "¬ 𝒰 s ⟹ △ (𝒯 s)" "¬ 𝒰 s ⟹ ∇ 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 "𝒰 s", auto)

lemma check_distinct_indices_state: assumes "¬ 𝒰 s ⟹ ⊨⇩n⇩o⇩l⇩h⇩s s" "¬ 𝒰 s ⟹ ◇ s" "¬ 𝒰 s ⟹ △ (𝒯 s)" "¬ 𝒰 s ⟹ ∇ 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 "𝒰 s", auto)

end

locale Assert' = AssertBound assert_bound + Check check for
assert_bound :: "('i,'a::lrv) i_atom ⇒ ('i,'a) state ⇒ ('i,'a) state" and
check :: "('i,'a::lrv) state ⇒ ('i,'a) state"
begin
definition assert :: "('i,'a) i_atom ⇒ ('i,'a) state ⇒ ('i,'a) state" where
"assert a s ≡ check (assert_bound a s)"

lemma Assert'Precond:
assumes "¬ 𝒰 s" "⊨ s" "△ (𝒯 s)" "∇ s"
shows
"△ (𝒯 (assert_bound a s))"
"¬ 𝒰 (assert_bound a s) ⟹  ⊨⇩n⇩o⇩l⇩h⇩s (assert_bound a s) ∧ ◇ (assert_bound a s)"
"∇ (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 *: "¬ 𝒰 s" "⊨ s" "△ (𝒯 s)" "∇ s"
have "△ (𝒯 (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]
moreover
have "v ⊨⇩t 𝒯 s = v ⊨⇩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 "∇ (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 "𝒰 (assert_bound a s)") (auto simp add: Assert'Precond assert_def)
ultimately
show "let s' = assert a s in (v ⊨⇩t 𝒯 s = v ⊨⇩t 𝒯 s') ∧ △ (𝒯 s') ∧ ∇ s'"
next
fix s::"('i,'a) state" and a::"('i,'a) i_atom"
assume "¬ 𝒰 s" "⊨ s" "△ (𝒯 s)" "∇ s"
then show "¬ 𝒰 (assert a s) ⟹ ⊨ (assert a s)"
unfolding assert_def
using check_unsat_id[of "assert_bound a s"]
using check_sat[of "assert_bound a s"]
next
fix s::"('i,'a) state" and a::"('i,'a) i_atom" and ats::"('i,'a) i_atom set"
assume "¬ 𝒰 s" "⊨ s" "△ (𝒯 s)" "∇ s"
then show "flat ats ≐ ℬ s ⟹ flat (ats ∪ {a}) ≐ ℬ (assert a s)"
using assert_bound_atoms_equiv_bounds
using check_unsat_id[of "assert_bound a s"] check_bounds_id
by (cases "𝒰 (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 *: "¬ 𝒰 s" "⊨ s" "△ (𝒯 s)" "∇ s" "𝒰 (assert a s)" "index_valid ats s"
show "minimal_unsat_state_core (assert a s)"
proof (cases "𝒰 (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 **: "¬ 𝒰 s" "⊨ s" "△ (𝒯 s)" "∇ 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 "𝒰 (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 *: "¬ 𝒰 s" "⊨ s" "△ (𝒯 s)" "∇ s" "ats ⊨⇩i ℬℐ s"
from assert_bound_atoms_imply_bounds_index[OF this, of a]
have as: "insert a ats ⊨⇩i ℬℐ (assert_bound a s)" by auto
show "insert a ats ⊨⇩i ℬℐ (assert a s)"
proof (cases "𝒰 ?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: "△ (𝒯 ?s)" by simp
from assert_bound_tableau_valuated[OF *(1-4)]
have v: "∇ ?s" .
from assert_bound_sat[OF *(1-4) refl False]
have "⊨⇩n⇩o⇩l⇩h⇩s ?s" "◇ ?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‹Under these assumptions for ‹assert_bound› and ‹check›, it can be easily shown that the implementation of ‹assert› (previously given) satisfies its specification.›

locale AssertAllState'' = Init init + AssertBoundNoLhs assert_bound + Check check for
init :: "tableau ⇒ ('i,'a::lrv) state" and
assert_bound :: "('i,'a::lrv) i_atom ⇒ ('i,'a) state ⇒ ('i,'a) state" and
check :: "('i,'a::lrv) state ⇒ ('i,'a) state"
begin
definition assert_bound_loop where
"assert_bound_loop ats s ≡ foldl (λ s' a. if (𝒰 s') then s' else assert_bound a s') s ats"
definition assert_all_state where [simp]:
"assert_all_state t ats ≡ check (assert_bound_loop ats (init t))"

text‹However, for efficiency reasons, we want to allow
implementations that delay the ‹check› function call and call it
after several ‹assert_bound› 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 ‹assert_bound› calls, so ‹assert_bound› 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 ‹⊨ s›, by ‹⊨⇩n⇩o⇩l⇩h⇩s s› and ‹◇ s›) for ‹assert_bound›, and show that these
preconditions are still good enough to prove the correctnes of this
alternative ‹assert_all_state› definition.›

lemma AssertAllState''_precond':
assumes "△ (𝒯 s)" "∇ s" "¬ 𝒰 s ⟶ ⊨⇩n⇩o⇩l⇩h⇩s s ∧ ◇ s"
shows "let s' = assert_bound_loop ats s in
△ (𝒯 s') ∧ ∇ s' ∧ (¬ 𝒰 s' ⟶ ⊨⇩n⇩o⇩l⇩h⇩s s' ∧ ◇ 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 "△ t"
shows "let s' = assert_bound_loop ats (init t) in
△ (𝒯 s') ∧ ∇ s' ∧ (¬ 𝒰 s' ⟶ ⊨⇩n⇩o⇩l⇩h⇩s s' ∧ ◇ 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
"△ t"
"P {} (init t)"
"⋀ as bs t. as ⊆ bs ⟹ P as t ⟹ P bs t"
"⋀ s a ats. ⟦¬ 𝒰 s;  ⟨𝒱 s⟩ ⊨⇩t 𝒯 s; ⊨⇩n⇩o⇩l⇩h⇩s s; △ (𝒯 s); ∇ s; ◇ s; P (set ats) s; index_valid (set ats) s⟧
⟹ 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)) ∧ 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