Session Simplex

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
  by (simp add: filter_empty_conv)

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 ainsert 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
  by (auto simp add: butlast_nth)

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"
    by (auto simp add: rtrancl_rel_chain)
  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
    by (auto simp add: rtrancl_rel_chain)
  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
    by (auto simp add: hd_conv_nth)
  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  []
      by (simp add: hd_conv_nth tl_nth)
  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
      by (simp add: hd_conv_nth last_tl)
  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  []
        by (auto simp add: hd_conv_nth)
      moreover
      have "sl > 0  tl (take (sl + 1) l)  []"
        using sl + 1 < length l l  [] ‹tl l  []
        by (auto simp add: take_Suc)
      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  []
        by (force simp add: tl_nth)
    next
      case False
      then have "length l' = length l - 1"
        using l' = ?l' sl + 1 < length l
        by (simp add: min_def)
      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'
          by (force simp add: nth_append)
      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)"]
            by (auto simp add: nth_append)

          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]
    by (simp add: scaleRat_one)
  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
    by (simp add: add_assoc)
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]
  by (auto simp add: add_assoc)

lemma minus_gt: "(a::'a) < b  0 < b - a"
  using plus_less[of a b "-a"]
  using plus_less[of 0 "b-a" a]
  by (auto simp add: add_assoc)

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"]
    by (auto simp add: not_less_iff_gr_or_eq)
  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]
        by (simp add: add_assoc )
    next
      case False
      then show ?thesis
        using a - b  0
        by (simp add:antisym_conv1)
    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]
    by (auto simp add: not_less_iff_gr_or_eq)
  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]
        by (simp add: add_assoc)
    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"]
  by (simp add: scaleRat_one scaleRat_scaleRat)

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"]
  by (simp add: scaleRat_one scaleRat_scaleRat)

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"]
  by (simp add: scaleRat_scaleRat scaleRat_one)

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"]
  by (simp add: scaleRat_scaleRat scaleRat_one)

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"

subclass (in linordered_rational_vector) ordered_ab_semigroup_add
proof
  fix a b c
  assume "a  b"
  then show "c + a  c + b"
    using plus_less[of a b c]
    by (auto simp add: add_ac le_less)
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 *
    by (auto simp add: finite_subset)
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 *
    by (auto simp add: finite_subset)
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 "p1"} and p2 is
defined by @{term "λ v. p1 v + p2 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
  "pv " == "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]
  by (auto simp add: valuate_def)

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)

lemma valuate_add_lemma:
  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)"
    by (simp add: scaleRat_left_distrib sum.distrib)
  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)"
  by (transfer, simp add: valuate_add_lemma)

lemma valuate_minus: "(p1 - p2) v = (p1 v) - (p2 v)"
  unfolding minus_linear_poly_def valuate_add 
  by (simp add: valuate_uminus)


lemma valuate_scaleRat:
  "(c *R lp)  v  = c *R ( lpv )"
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: "((xA. f x)  v ) = (xA. ((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. yx  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  {}"
  by (auto simp add: is_monom_def vars_list_def) (auto simp add: vars_def)

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
        by (auto simp add: vars_def)
      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
        by (simp add: is_monom_def)
    qed
  qed
  then show "vars l = {monom_var l}"
    using assms
    by (auto simp add: monom_var_in_vars)
qed

lemma monom_valuate:
  assumes "is_monom m"
  shows "mv = (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 (xxs. 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  = (xvars 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"
    "HOL-Library.Monad_Syntax"
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)

text‹Addition›

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

lemma lookup_add_monom:
  "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"
  unfolding add_monom_def get_var_coeff_def set_var_coeff_def
  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  =
        (xset (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 (xA. f x) = (xA. qdfst (f x))"
  by (induct A rule: finite_induct) (auto simp add: zero_QDelta_def plus_QDelta_def)

lemma qdsnd_setsum:
  "finite A  qdsnd (xA. f x) = (xA. 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 (lpvl) 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 (lpvl) δ"
  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 p1 ⨝ p2, where p›, p1, and p2, 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 cs, if all constraints are. There is also an indexed
version ics 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)  (lv) < r *R 1"
| "v c GT l r  (lv) > r *R 1"
| "v c LEQ l r  (lv)  r *R 1"
| "v c GEQ l r  (lv)   r *R 1"
| "v c EQ l r  (lv) = r *R 1"
| "v c LTPP l1 l2  (l1v) < (l2v)"
| "v c GTPP l1 l2  (l1v) > (l2v)"
| "v c LEQPP l1 l2  (l1v)  (l2v)"
| "v c GEQPP l1 l2  (l1v)  (l2v)"
| "v c EQPP l1 l2  (l1v) = (l2v)"


abbreviation satisfies_constraints :: "rat valuation  constraint set  bool" (infixl "cs" 100) where
  "v cs cs   c  cs. v c c"

lemma unsat_mono: assumes "¬ ( v. v cs cs)"
  and "cs  ds"
shows "¬ ( v. v cs ds)"
  using assms by auto

fun i_satisfies_cs (infixl "ics" 100) where
  "(I,v) ics cs  v cs restrict_to I cs"

definition distinct_indices :: "('i × 'c) list  bool" where
  "distinct_indices as = (distinct (map fst as))"

lemma distinct_indicesD: "distinct_indices as  (i,x)  set as  (i,y)  set as  x = y"
  unfolding distinct_indices_def by (rule eq_key_imp_eq_value)

text ‹For the unsat-core predicate we only demand minimality in case that the indices are distinct.
  Otherwise, minimality does in general not hold. For instance, consider the input
  constraints $c_1: x < 0$, $c_2: x > 2$ and $c_2: x < 1$ where the index $c_2$ occurs twice.
  If the simplex-method first encounters constraint $c_1$, then it will detect that there is a conflict
  between $c_1$ and the first $c_2$-constraint. Consequently, the index-set $\{c_1,c_2\}$ will be returned,
  but this set is not minimal since $\{c_2\}$ is already unsatisfiable.›
definition minimal_unsat_core :: "'i set  'i i_constraint list  bool" where
  "minimal_unsat_core I ics  = ((I  fst ` set ics)  (¬ ( v. (I,v) ics set ics))
      (distinct_indices ics  ( J. J  I  ( v. (J,v) ics set ics))))"

subsection ‹Procedure Specification›

abbreviation (input) Unsat where "Unsat  Inl"
abbreviation (input) Sat where "Sat  Inr"


text‹The specification for the satisfiability check procedure is given by:›
locale Solve =
  ― ‹Decide if the given list of constraints is satisfiable. Return either
     an unsat core, or a satisfying valuation.›
  fixes solve :: "'i i_constraint list  'i list + rat valuation"
    ― ‹If the status @{const Sat} is returned, then returned valuation
      satisfies all constraints.›
  assumes  simplex_sat:  "solve cs = Sat v  v cs flat (set cs)"
    ― ‹If the status @{const Unsat} is returned, then constraints are
     unsatisfiable, i.e., an unsatisfiable core is returned.›
  assumes  simplex_unsat:  "solve cs = Unsat I  minimal_unsat_core (set I) cs"

abbreviation (input) look where "look  Mapping.lookup"
abbreviation (input) upd where "upd  Mapping.update"

lemma look_upd: "look (upd k v m) = (look m)(k  v)"
  by (transfer, auto)

lemmas look_upd_simps[simp] = look_upd Mapping.lookup_empty

definition map2fun:: "(var, 'a :: zero) mapping  var  'a" where
  "map2fun v  λx. case look v x of None  0 | Some y  y"
syntax
  "_map2fun" :: "(var, 'a) mapping  var  'a"  ("_")
translations
  "v" == "CONST map2fun v"

lemma map2fun_def':
  "v x  case Mapping.lookup v x of None  0 | Some y  y"
  by (auto simp add: map2fun_def)


text‹Note that the above specification requires returning a
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 cs flat (set cs)"
  assumes  simplex_unsat0:  "solve_exec cs = Unsat I  minimal_unsat_core (set I) cs"
begin
definition solve where
  "solve cs  case solve_exec cs of Sat v  Sat v | Unsat c  Unsat c"
end

sublocale SolveExec < Solve solve
  by (unfold_locales, insert simplex_sat0 simplex_unsat0,
      auto simp: solve_def split: sum.splits)


subsection ‹Handling Strict Inequalities›

text‹The first step of the procedure is removing all equalities and
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 ns and nss. The indexed variant is inss.›
datatype 'a ns_constraint = LEQ_ns linear_poly 'a    |    GEQ_ns linear_poly 'a

type_synonym ('i,'a) i_ns_constraint = "'i × 'a ns_constraint"

primrec satisfiable_ns_constraint :: "'a::lrv valuation  'a ns_constraint  bool" (infixl "ns" 100) where
  "v ns LEQ_ns l r  lv  r"
| "v ns GEQ_ns l r  lv  r"

abbreviation satisfies_ns_constraints :: "'a::lrv valuation  'a ns_constraint set  bool" (infixl "nss " 100) where
  "v nss cs   c  cs. v ns c"

fun i_satisfies_ns_constraints :: "'i set × 'a::lrv valuation  ('i,'a) i_ns_constraint set  bool" (infixl "inss " 100) where
  "(I,v) inss cs  v nss restrict_to I cs"

lemma i_satisfies_ns_constraints_mono:
  "(I,v) inss cs  J  I  (J,v) inss cs"
  by auto

primrec poly :: "'a ns_constraint  linear_poly" where
  "poly (LEQ_ns p a) = p"
| "poly (GEQ_ns p a) = p"

primrec ns_constraint_const :: "'a ns_constraint  'a" where
  "ns_constraint_const (LEQ_ns p a) = a" 
| "ns_constraint_const (GEQ_ns p a) = a" 

definition distinct_indices_ns :: "('i,'a :: lrv) i_ns_constraint set  bool" where 
  "distinct_indices_ns ns = (( n1 n2 i. (i,n1)  ns  (i,n2)  ns  
     poly n1 = poly n2  ns_constraint_const n1 = ns_constraint_const n2))" 

definition minimal_unsat_core_ns :: "'i set  ('i,'a :: lrv) i_ns_constraint set  bool" where
  "minimal_unsat_core_ns I cs = ((I  fst ` cs)  (¬ ( v. (I,v) inss cs))
      (distinct_indices_ns cs  ( J  I.  v. (J,v) inss cs)))"


text‹Specification of reduction of constraints to non-strict form is given by:›
locale To_ns =
  ― ‹Convert a constraint to an equisatisfiable non-strict constraint list.
      The conversion must work for arbitrary subsets of constraints -- selected by some index set I --
      in order to carry over unsat-cores and in order to support incremental simplex solving.›
  fixes to_ns :: "'i i_constraint list  ('i,'a::lrv) i_ns_constraint list"
    ― ‹Convert the valuation that satisfies all non-strict constraints to the valuation that
   satisfies all initial constraints.›
  fixes from_ns :: "(var, 'a) mapping  'a ns_constraint list  (var, rat) mapping"
  assumes  to_ns_unsat:  "minimal_unsat_core_ns I (set (to_ns cs))  minimal_unsat_core I cs"
  assumes  i_to_ns_sat:  "(I,v') inss set (to_ns cs)  (I,from_ns v' (flat_list (to_ns cs))) ics set cs"
  assumes to_ns_indices: "fst ` set (to_ns cs) = fst ` set cs"
  assumes distinct_cond: "distinct_indices cs  distinct_indices_ns (set (to_ns cs))" 
begin
lemma to_ns_sat: "v'  nss flat (set (to_ns cs))  from_ns v' (flat_list (to_ns cs)) cs flat (set cs)"
  using i_to_ns_sat[of UNIV v' cs] by auto
end


locale Solve_exec_ns =
  fixes solve_exec_ns :: "('i,'a::lrv) i_ns_constraint list  'i list + (var, 'a) mapping"
  assumes simplex_ns_sat:  "solve_exec_ns cs = Sat v  v nss flat (set cs)"
  assumes simplex_ns_unsat:  "solve_exec_ns cs = Unsat I  minimal_unsat_core_ns (set I) (set cs)"


text‹After the transformation, the procedure is reduced to solving
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 xi ⨝ bi where xi is a
variable and bi 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,
[x1 + x2 ≤ b1, x1 + x2 ≥ b2, x2 ≥ b3]› can be transformed to
the tableau [x3 = x1 + x2]› and atoms [x3 ≤ b1, x3 ≥
b2, x2 ≥ b3]›.›


type_synonym eq = "var × linear_poly"
primrec lhs :: "eq  var" where "lhs (l, r) = l"
primrec rhs :: "eq  linear_poly" where "rhs (l, r) = r"
abbreviation rvars_eq :: "eq  var set" where
  "rvars_eq eq  vars (rhs eq)"


definition satisfies_eq :: "'a::rational_vector valuation  eq  bool" (infixl "e" 100) where
  "v e eq  v (lhs eq) = (rhs eq)v"

lemma satisfies_eq_iff: "v e (x, p)  v x = pv"
  by (simp add: satisfies_eq_def)



type_synonym tableau ="eq list"


definition satisfies_tableau ::"'a::rational_vector valuation  tableau  bool" (infixl "t" 100) where
  "v t t   e  set t. v e e"


definition lvars :: "tableau  var set" where
  "lvars t = set (map lhs t)"
definition rvars :: "tableau  var set" where
  "rvars t =  (set (map rvars_eq t))"
abbreviation tvars where "tvars t  lvars t  rvars t"

text ‹The condition that the rhss are non-zero is required to obtain minimal unsatisfiable cores.
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 "xrvars 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'. (xvars (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 "xvars (b - b'). v' x = v x"
          using  x  rvars t1. v x = v' x
          by auto
        ultimately
        show "v'. (xvars (b - b'). v' x = v x)  (b - b')  v'  = 0"
          by auto
      qed
      then have "b = b'"
        using all_val[of "b - b'"]
        by simp
      then show "(a, b)  set t2"
        using (a, b')  set t2
        by simp
    qed
  }
  note * = this
  have "set t1 = set t2"
    using *[of t1 t2] *[of t2 t1]
    using assms
    by auto
  moreover
  have "distinct t1" "distinct t2"
    using  t1  t2
    unfolding normalized_tableau_def
    by (auto simp add: distinct_map)
  ultimately
  show ?thesis
    by (auto simp add: set_eq_iff_mset_eq_distinct)
qed


text‹Elementary atoms are represented by the type 'a atom›
and semantics for atoms and sets of atoms is denoted by a and
as and given by:
›

datatype 'a atom  = Leq var 'a    |    Geq var 'a

primrec atom_var::"'a atom  var" where
  "atom_var (Leq var a) = var"
| "atom_var (Geq var a) = var"

primrec atom_const::"'a atom  'a" where
  "atom_const (Leq var a) = a"
| "atom_const (Geq var a) = a"

primrec satisfies_atom :: "'a::linorder valuation  'a atom  bool" (infixl "a" 100) where
  "v a Leq x c  v x  c"    |    "v a Geq x c  v x  c"

definition satisfies_atom_set :: "'a::linorder valuation  'a atom set  bool" (infixl "as" 100) where
  "v as as   a  as. v a a"

definition satisfies_atom' :: "'a::linorder valuation  'a atom  bool" (infixl "ae" 100) where
  "v ae a  v (atom_var a) = atom_const a"

lemma satisfies_atom'_stronger: "v ae a  v a a" by (cases a, auto simp: satisfies_atom'_def)

abbreviation satisfies_atom_set' :: "'a::linorder valuation  'a atom set  bool" (infixl "aes" 100) where
  "v aes as   a  as. v ae a"

lemma satisfies_atom_set'_stronger: "v aes as  v as as" 
  using satisfies_atom'_stronger unfolding satisfies_atom_set_def by auto

text ‹There is also the indexed variant of an atom›

type_synonym ('i,'a) i_atom = "'i × 'a atom"

fun i_satisfies_atom_set :: "'i set × 'a::linorder valuation  ('i,'a) i_atom set  bool" (infixl "ias" 100) where
  "(I,v) ias as  v as restrict_to I as"

fun i_satisfies_atom_set' :: "'i set × 'a::linorder valuation  ('i,'a) i_atom set  bool" (infixl "iaes" 100) where
  "(I,v) iaes as  v aes restrict_to I as"

lemma i_satisfies_atom_set'_stronger: "Iv iaes as  Iv ias as" 
  using satisfies_atom_set'_stronger[of _ "snd Iv"] by (cases Iv, auto)

lemma satisifies_atom_restrict_to_Cons: "v as restrict_to I (set as)  (i  I  v a a)
   v as restrict_to I (set ((i,a) # as))"
  unfolding satisfies_atom_set_def by auto

lemma satisfies_tableau_Cons: "v t t  v e e  v t (e # t)"
  unfolding satisfies_tableau_def by auto

definition distinct_indices_atoms :: "('i,'a) i_atom set  bool" where
  "distinct_indices_atoms as = ( i a b. (i,a)  as  (i,b)  as  atom_var a = atom_var b  atom_const a = atom_const b)" 

text‹
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) ias set as  v t t  (I,trans_v v) inss set cs" and

preprocess_unsat: "preprocess cs = (t, as,trans_v,U)  (I,v) inss set cs   v'. (I,v') ias set as  v' t t" and

― ‹distinct indices on ns-constraints ensures distinct indices in atoms›
preprocess_distinct: "preprocess cs = (t, as,trans_v, U)  distinct_indices_ns (set cs)  distinct_indices_atoms (set as)" and

― ‹unsat indices›
preprocess_unsat_indices: "preprocess cs = (t, as,trans_v, U)  i  set U  ¬ ( v. ({i},v) inss set cs)" and

― ‹preprocessing cannot introduce new indices›
preprocess_index: "preprocess cs = (t,as,trans_v, U)  fst ` set as  set U  fst ` set cs"
begin
lemma preprocess_sat: "preprocess cs = (t,as,trans_v,U)  U = []  v as flat (set as)  v t t  trans_v v nss flat (set cs)"
  using i_preprocess_sat[of cs t as trans_v U UNIV v] by auto

end

definition minimal_unsat_core_tabl_atoms :: "'i set  tableau  ('i,'a::lrv) i_atom set  bool" where
  "minimal_unsat_core_tabl_atoms I t as = ( I  fst ` as  (¬ ( v. v t t  (I,v) ias as)) 
       (distinct_indices_atoms as  ( J  I.  v. v t t  (J,v) iaes as)))" 

lemma minimal_unsat_core_tabl_atomsD: assumes "minimal_unsat_core_tabl_atoms I t as"
  shows "I  fst ` as" 
    "¬ ( v. v t t  (I,v) ias as)" 
    "distinct_indices_atoms as  J  I   v. v t t  (J,v) iaes as" 
  using assms unfolding minimal_unsat_core_tabl_atoms_def by auto

locale AssertAll =
  fixes assert_all :: "tableau  ('i,'a::lrv) i_atom list  'i list + (var, 'a)mapping"
  assumes assert_all_sat:  " t  assert_all t as = Sat v  v t t  v as flat (set as)"
  assumes assert_all_unsat:  " t  assert_all t as = Unsat I  minimal_unsat_core_tabl_atoms (set I) t (set as)"


text‹Once the preprocessing is done and tableau and atoms are
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) inss set cs)" by force+
  show "minimal_unsat_core_ns I (set cs)" unfolding minimal_unsat_core_ns_def
  proof (intro conjI impI allI 1(2))
    show "I  fst ` set cs" using 1 index by auto
    fix J
    assume "distinct_indices_ns (set cs)" "J  I" 
    with preprocess_distinct[OF prep]
    have "distinct_indices_atoms (set as)" "J  I" by auto
    from minimal_unsat_core_tabl_atomsD(3)[OF unsat this]
    obtain v where model: "v t t" "(J, v) iaes set as" by auto
    from i_satisfies_atom_set'_stronger[OF model(2)] 
    have model': "(J, v) ias set as" . 
    define w where "w = Mapping.Mapping (λ x. Some (v x))"
    have "v = w" unfolding w_def map2fun_def
      by (intro ext, transfer, auto)
    with model model' have "w t t" "(J, w) ias set as" by auto
    from i_preprocess_sat[OF prep _ this(2,1)] J  I inter
    have "(J, trans_v w) inss set cs" by auto
    then show " w. (J, w) inss set cs" by auto
  qed
qed
end

sublocale Solve_exec_ns' < Solve_exec_ns solve_exec_ns
proof
  fix cs
  obtain t as trans_v ui where prep: "preprocess cs = (t,as,trans_v,ui)" by (cases "preprocess cs")
  from preprocess_tableau_normalized[OF prep]
  have t: " t" .
  from preprocess_index[OF prep] have index: "fst ` set as  set ui  fst ` set cs" by auto
  note solve = solve_exec_ns_def[of cs, unfolded prep split]
  {
    fix v
    assume "solve_exec_ns cs = Sat v"
    from this[unfolded solve] t assert_all_sat[OF t] preprocess_sat[OF prep]
    show " v nss flat (set cs)" by (auto split: sum.splits list.splits)
  }
  {
    fix I
    assume res: "solve_exec_ns cs = Unsat I"
    show "minimal_unsat_core_ns (set I) (set cs)" 
    proof (cases ui)
      case (Cons i uis)
      hence I: "I = [i]" using res[unfolded solve] by auto
      from preprocess_unsat_index[OF prep, of i] I Cons index show ?thesis by auto
    next
      case Nil
      from res[unfolded solve Nil] have assert: "assert_all t as = Unsat I"
        by (auto split: sum.splits)
      from assert_all_unsat[OF t assert]
      have "minimal_unsat_core_tabl_atoms (set I) t (set as)" .
      from preprocess_minimal_unsat_core[OF prep this] Nil
      show "minimal_unsat_core_ns (set I) (set cs)" by simp
    qed
  }
qed

subsection‹Incrementally Asserting Atoms›

text‹The function @{term assert_all} can be implemented by
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 li ≤ xi ≤ ui, where
li and ui and are either scalars or $\pm
\infty$. Each time a new atom is asserted, a bound for the
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 ≥ub b ⟷ case b of None ⇒ False | Some b' ⇒ c ≥ b'›

c ≤ub b ⟷ case b of None ⇒ True | Some b' ⇒ c ≤ b'›
\end{small}

\noindent Strict comparisons, and comparisons with lower bounds are performed similarly.
›

abbreviation (input) le where
  "le lt x y  lt x y  x = y"
definition geub ("ub") where
  "ub lt c b  case b of None  False | Some b'  le lt b' c"
definition gtub ("ub") where
  "ub lt c b  case b of None  False | Some b'  lt b' c"
definition leub ("ub") where
  "ub lt c b  case b of None  True | Some b'  le lt c b'"
definition ltub ("ub") where
  "ub lt c b  case b of None  True | Some b'  lt c b'"
definition lelb ("lb") where
  "lb lt c b  case b of None  False | Some b'  le lt c b'"
definition ltlb ("lb") where
  "lb lt c b  case b of None  False | Some b'  lt c b'"
definition gelb ("lb") where
  "lb lt c b  case b of None  True | Some b'  le lt b' c"
definition gtlb ("lb") where
  "lb lt c b  case b of None  True | Some b'  lt b' c"


definition ge_ubound :: "'a::linorder  'a option  bool" (infixl "ub" 100) where
  "c ub b = ub (<) c b"
definition gt_ubound :: "'a::linorder  'a option  bool" (infixl ">ub" 100) where
  "c >ub b = ub (<) c b"
definition le_ubound :: "'a::linorder  'a option  bool" (infixl "ub" 100) where
  "c ub b = ub (<) c b"
definition lt_ubound :: "'a::linorder  'a option  bool" (infixl "<ub" 100) where
  "c <ub b = ub (<) c b"
definition le_lbound :: "'a::linorder  'a option  bool" (infixl "lb" 100) where
  "c lb b = lb (<) c b"
definition lt_lbound :: "'a::linorder  'a option  bool" (infixl "<lb" 100) where
  "c <lb b = lb (<) c b"
definition ge_lbound :: "'a::linorder  'a option  bool" (infixl "lb" 100) where
  "c lb b = lb (<) c b"
definition gt_lbound :: "'a::linorder  'a option  bool" (infixl ">lb" 100) where
  "c >lb b = lb (<) c b"


lemmas bound_compare'_defs =
  geub_def gtub_def leub_def ltub_def
  gelb_def gtlb_def lelb_def ltlb_def

lemmas bound_compare''_defs =
  ge_ubound_def gt_ubound_def le_ubound_def lt_ubound_def
  le_lbound_def lt_lbound_def ge_lbound_def gt_lbound_def

lemmas bound_compare_defs = bound_compare'_defs bound_compare''_defs


lemma opposite_dir [simp]:
  "lb (>) a b = ub (<) a b"
  "ub (>) a b = lb (<) a b"
  "lb (>) a b = ub (<) a b"
  "ub (>) a b = lb (<) a b"
  "lb (>) a b = ub (<) a b"
  "ub (>) a b = lb (<) a b"
  "lb (>) a b = ub (<) a b"
  "ub (>) a b = lb (<) a b"
  by (case_tac[!] b) (auto simp add: bound_compare'_defs)


(* Auxiliary lemmas about bound comparison *)

lemma [simp]: "¬ c ub None " "¬ c lb None"
  by (auto simp add: bound_compare_defs)

lemma neg_bounds_compare:
  "(¬ (c ub b))  c <ub b" "(¬ (c ub b))  c >ub b"
  "(¬ (c >ub b))  c ub b" "(¬ (c <ub b))  c ub b"
  "(¬ (c lb b))  c >lb b" "(¬ (c lb b))  c <lb b"
  "(¬ (c <lb b))  c lb b" "(¬ (c >lb b))  c lb b"
  by (case_tac[!] b) (auto simp add: bound_compare_defs)

lemma bounds_compare_contradictory [simp]:
  "c ub b; c <ub b  False" "c ub b; c >ub b  False"
  "c >ub b; c ub b  False" "c <ub b; c ub b  False"
  "c lb b; c >lb b  False" "c lb b; c <lb b  False"
  "c <lb b; c lb b  False" "c >lb b; c lb b  False"
  by (case_tac[!] b) (auto simp add: bound_compare_defs)

lemma compare_strict_nonstrict:
  "x <ub b  x ub b"
  "x >ub b  x ub b"
  "x <lb b  x lb b"
  "x >lb b  x lb b"
  by (case_tac[!] b) (auto simp add: bound_compare_defs)

lemma [simp]:
  " x  c; c <ub b   x <ub b"
  " x < c; c ub b   x <ub b"
  " x  c; c ub b   x ub b"
  " x  c; c >lb b   x >lb b"
  " x > c; c lb b   x >lb b"
  " x  c; c lb b   x lb b"
  by (case_tac[!] b) (auto simp add: bound_compare_defs)

lemma bounds_lg [simp]:
  " c >ub b; x ub b  x < c"
  " c ub b; x <ub b  x < c"
  " c ub b; x ub b  x  c"
  " c <lb b; x lb b  x > c"
  " c lb b; x >lb b  x > c"
  " c lb b; x lb b  x  c"
  by (case_tac[!] b) (auto simp add: bound_compare_defs)

lemma bounds_compare_Some [simp]:
  "x ub Some c  x  c" "x ub Some c  x  c"
  "x <ub Some c  x < c" "x >ub Some c  x > c"
  "x lb Some c  x  c" "x lb Some c  x  c"
  "x >lb Some c  x > c" "x <lb Some c  x < c"
  by (auto simp add: bound_compare_defs)

fun in_bounds where
  "in_bounds x v (lb, ub) = (v x lb lb x  v x ub ub x)"

fun satisfies_bounds :: "'a::linorder valuation  'a bounds × 'a bounds  bool" (infixl "b" 100) where
  "v b b  ( x. in_bounds x v b)"
declare satisfies_bounds.simps [simp del]


lemma satisfies_bounds_iff:
  "v b (lb, ub)  ( x. v x lb lb x  v x ub ub x)"
  by (auto simp add: satisfies_bounds.simps)

lemma not_in_bounds:
  "¬ (in_bounds x v (lb, ub)) = (v x <lb lb x  v x >ub ub x)"
  using bounds_compare_contradictory(7)
  using bounds_compare_contradictory(2)
  using neg_bounds_compare(7)[of "v x" "lb x"]
  using neg_bounds_compare(2)[of "v x" "ub x"]
  by auto

fun atoms_equiv_bounds :: "'a::linorder atom set  'a bounds × 'a bounds  bool" (infixl "" 100) where
  "as  (lb, ub)  ( v. v as as  v b (lb, ub))"
declare atoms_equiv_bounds.simps [simp del]

lemma atoms_equiv_bounds_simps:
  "as  (lb, ub)   v. v as as  v b (lb, ub)"
  by (simp add: atoms_equiv_bounds.simps)

text‹A valuation satisfies bounds iff the value of each variable
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")
  (il: "('i,'a) bounds_index")
  (iu: "('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 (il s)"

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

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

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

abbreviation BoundsIndicesMap ("i") where  "i s  (il s,iu 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 "ib" 100) where
  "(I,v) ib ((BL,BU),(IL,IU))  (
     ( x c. BL x = Some c  IL x  I  v x  c)
    ( x c. BU x = Some c  IU x  I  v x  c))"
declare satisfies_bounds_index.simps[simp del]

fun satisfies_bounds_index' :: "'i set × 'a::lrv valuation  ('a bounds × 'a bounds) ×
  ('i bound_index × 'i bound_index)  bool" (infixl "ibe" 100) where
  "(I,v) ibe ((BL,BU),(IL,IU))  (
     ( x c. BL x = Some c  IL x  I  v x = c)
    ( x c. BU x = Some c  IU x  I  v x = c))"
declare satisfies_bounds_index'.simps[simp del]

fun atoms_imply_bounds_index :: "('i,'a::lrv) i_atom set  ('a bounds × 'a bounds) × ('i bound_index × 'i bound_index)
   bool" (infixl "i" 100) where
  "as i bi  ( I v. (I,v) ias as  (I,v) ib bi)"
declare atoms_imply_bounds_index.simps[simp del]

lemma i_satisfies_atom_set_mono: "as  as'  v ias as'  v ias as"
  by (cases v, auto simp: satisfies_atom_set_def)

lemma atoms_imply_bounds_index_mono: "as  as'  as i bi  as' i bi"
  unfolding atoms_imply_bounds_index.simps using i_satisfies_atom_set_mono by blast

definition satisfies_state :: "'a::lrv valuation  ('i,'a) state  bool" (infixl "s" 100) where
  "v s s  v b  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 "is" 100) where
  "(I,v) is s  (v t 𝒯 s  (I,v) ib ℬℐ s)"
declare satisfies_state_index.simps[simp del]

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

definition indices_state :: "('i,'a)state  'i set" where
  "indices_state s = { i.  x b. look (il s) x = Some (i,b)  look (iu 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 (il s) x = Some (i,b)  look (iu s) x = Some (i,b)) 
    (look (il s) x' = Some (i,b')  look (iu s) x' = Some (i,b')) 
    (x = x'  b = b')))" 

lemma distinct_indices_stateD: assumes "distinct_indices_state s"
  shows "look (il s) x = Some (i,b)  look (iu s) x = Some (i,b)  look (il s) x' = Some (i,b')  look (iu 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) is s)))"

definition subsets_sat_core :: "('i,'a::lrv) state  bool" where
  "subsets_sat_core s = (( I. I  set (the (𝒰c s))  ( v. (I,v) ise s)))" 

definition minimal_unsat_state_core :: "('i,'a::lrv) state  bool" where
  "minimal_unsat_state_core s = (unsat_state_core s  (distinct_indices_state s  subsets_sat_core s))" 

lemma minimal_unsat_core_tabl_atoms_mono: assumes sub: "as  bs" 
  and unsat: "minimal_unsat_core_tabl_atoms I t as" 
shows "minimal_unsat_core_tabl_atoms I t bs" 
  unfolding minimal_unsat_core_tabl_atoms_def
proof (intro conjI impI allI)
  note min = unsat[unfolded minimal_unsat_core_tabl_atoms_def]
  from min have I: "I  fst ` as" by blast
  with sub show "I  fst ` bs" by blast
  from min have "(v. v t t  (I, v) ias as)" by blast
  with i_satisfies_atom_set_mono[OF sub]
  show "(v. v t t  (I, v) ias bs)" by blast
  fix J
  assume J: "J  I" and dist_bs: "distinct_indices_atoms bs" 
  hence dist: "distinct_indices_atoms as" 
    using sub unfolding distinct_indices_atoms_def by blast
  from min dist J obtain v where v: "v t t" "(J, v) iaes as" by blast
  have "(J, v) iaes bs"
    unfolding i_satisfies_atom_set'.simps
  proof (intro ballI)
    fix a
    assume "a  snd ` (bs  J × UNIV)" 
    then obtain i where ia: "(i,a)  bs" and i: "i  J" 
      by force
    with J have "i  I" by auto 
    with I obtain b where ib: "(i,b)  as" by force
    with sub have ib': "(i,b)  bs" by auto
    from dist_bs[unfolded distinct_indices_atoms_def, rule_format, OF ia ib']
    have id: "atom_var a = atom_var b" "atom_const a = atom_const b" by auto
    from v(2)[unfolded i_satisfies_atom_set'.simps] i ib 
    have "v ae b" by force
    thus "v ae a" using id unfolding satisfies_atom'_def by auto
  qed
  with v show "v. v t t  (J, v) iaes bs" by blast
qed

lemma state_satisfies_index: assumes "v s s"
  shows "(I,v) is s"
  unfolding satisfies_state_index.simps satisfies_bounds_index.simps
proof (intro conjI impI allI)
  fix x c
  from assms[unfolded satisfies_state_def satisfies_bounds.simps, simplified]
  have "v t 𝒯 s" and bnd: "v x lb l s x" "v x ub 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 (il s) x = Some (i,b)  ((i, Geq x b)  as))
     (look (iu 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 iu_update where
  "iu_update up (State T BIL BIU V U UC) = State T BIL (up BIU) V U UC"

fun il_update where
  "il_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]:
  "ℬiu (iu_update up s) = up (iu s)"
  "ℬil (iu_update up s) =il s"
  "𝒯 (iu_update up s) = 𝒯 s"
  "𝒱 (iu_update up s) = 𝒱 s"
  "𝒰 (iu_update up s) = 𝒰 s"
  "𝒰c (iu_update up s) = 𝒰c s"
  "ℬil (il_update up s) = up (il s)"
  "ℬiu (il_update up s) =iu s"
  "𝒯 (il_update up s) = 𝒯 s"
  "𝒱 (il_update up s) = 𝒱 s"
  "𝒰 (il_update up s) = 𝒰 s"
  "𝒰c (il_update up s) = 𝒰c s"
  "𝒱 (𝒱_update V s) = V"
  "ℬil (𝒱_update V s) =il s"
  "ℬiu (𝒱_update V s) =iu s"
  "𝒯 (𝒱_update V s) = 𝒯 s"
  "𝒰 (𝒱_update V s) = 𝒰 s"
  "𝒰c (𝒱_update V s) = 𝒰c s"
  "𝒯 (𝒯_update T s) = T"
  "ℬil (𝒯_update T s) =il s"
  "ℬiu (𝒯_update T s) =iu s"
  "𝒱 (𝒯_update T s) = 𝒱 s"
  "𝒰 (𝒯_update T s) = 𝒰 s"
  "𝒰c (𝒯_update T s) = 𝒰c s"
  by (atomize(full), cases s, auto)

declareiu_update.simps[simp del]il_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]: "ℬil (set_unsat I s) =il s"
  "ℬiu (set_unsat I s) =iu 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 (<)iliu l u l uiu_update Leq Geq (≤)"

definition Negative where
  [simp]: "Negative  Direction (>)iuil u l u lil_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: "ℬil (init t) = Mapping.empty"   "ℬiu (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
  by (simp add: Let_def)

lemma assert_tableau_normalized: "¬ 𝒰 s;  s;  (𝒯 s);  s   (𝒯 (assert a s))"
  using assert_tableau
  by (simp add: Let_def)

lemma assert_tableau_valuated: "¬ 𝒰 s;  s;  (𝒯 s);  s   (assert a s)"
  using assert_tableau
  by (simp add: Let_def)
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 lb lb x  v x ub ub x)"
  by (simp add: satisfies_bounds_set.simps)


definition curr_val_satisfies_no_lhs ("nolhs") where
  "nolhs s  𝒱 s t (𝒯 s)  (𝒱 s b ( s)  (- lvars (𝒯 s)))"
lemma satisfies_satisfies_no_lhs:
  " s  nolhs 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 xi = Some c
     c lb l s xi"
  unfolding bounds_consistent_def
  by (cases "l s xi", auto simp add: bound_compare_defs split: if_splits)
    (erule_tac x="xi" in allE, auto)

lemma bounds_consistent_leq_ub:
  " s; l s xi = Some c
     c ub u s xi"
  unfolding bounds_consistent_def
  by (cases "u s xi", auto simp add: bound_compare_defs split: if_splits)
    (erule_tac x="xi" in allE, auto)

lemma bounds_consistent_gt_ub:
  " s; c <lb l s x   ¬ c >ub 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 >ub u s x   ¬ c <lb 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'  nolhs 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; nolhs s;  (𝒯 s);  s;  s  𝒯 (assert_bound a s) = 𝒯 s"
  assumes assert_bound_nolhs_sat: "¬ 𝒰 s; nolhs s;  (𝒯 s);  s;  s 
    ¬ 𝒰 (assert_bound a s)  nolhs (assert_bound a s)   (assert_bound a s)"
  assumes assert_bound_nolhs_atoms_equiv_bounds: "¬ 𝒰 s; nolhs s;  (𝒯 s);  s;  s 
    flat ats   s  flat (ats  {a})   (assert_bound a s)"
  assumes assert_bound_nolhs_atoms_imply_bounds_index: "¬ 𝒰 s; nolhs s;  (𝒯 s);  s;  s 
    ats i ℬℐ s  insert a ats i ℬℐ (assert_bound a s)"
  assumes assert_bound_nolhs_unsat: "¬ 𝒰 s; nolhs 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; nolhs s;  (𝒯 s);  s;  s 
    (assert_bound a s)"
  assumes assert_bound_nolhs_index_valid: "¬ 𝒰 s; nolhs 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 nolhs 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; nolhs 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; nolhs 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; nolhs s;  s;  (𝒯 s);  s  ¬ 𝒰 (check s)   (check s)"  and


check_unsat: "¬ 𝒰 s; nolhs s;  s;  (𝒯 s);  s  𝒰 (check s)  minimal_unsat_state_core (check s)"

begin

lemma check_tableau_equiv: "¬ 𝒰 s; nolhs s;  s;  (𝒯 s);  s 
                      (v::'a valuation) t 𝒯 s  v t 𝒯 (check s)"
  using check_tableau
  by (simp add: Let_def)

lemma check_tableau_index_valid: assumes "¬ 𝒰 s" " nolhs 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; nolhs s;  s;  (𝒯 s);  s   (𝒯 (check s))"
  using check_tableau
  by (simp add: Let_def)

lemma check_tableau_valuated: "¬ 𝒰 s; nolhs s;  s;  (𝒯 s);  s   (check s)"
  using check_tableau
  by (simp add: Let_def)

lemma check_indices_state: assumes "¬ 𝒰 s  nolhs 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  nolhs 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)   nolhs (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]
    by (force simp add: assert_def)
  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'"
    by (simp add: Let_def)
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"]
    by (force simp add: Assert'Precond)
next
  fix s::"('i,'a) state" and a::"('i,'a) i_atom" and ats::"('i,'a) i_atom set"
  assume "¬ 𝒰 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 "nolhs ?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 nolhs 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  nolhs s   s"
  shows "let s' = assert_bound_loop ats s in
          (𝒯 s')   s'  (¬ 𝒰 s'  nolhs 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'  nolhs 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; nolhs 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