Theory DBM_Constraint_Systems

chapter ‹DBMs as Constraint Systems›
theory DBM_Constraint_Systems
  imports
    DBM_Operations
    DBM_Normalization
begin

section ‹Misc›

lemma Max_le_MinI:
  assumes "finite S" "finite T" "S ≠ {}" "T ≠ {}" "⋀x y. x ∈ S ⟹ y ∈ T ⟹ x ≤ y"
  shows "Max S ≤ Min T" by (simp add: assms)

lemma Min_insert_cases:
  assumes "x = Min (insert a S)" "finite S"
  obtains (default) "x = a" | (elem) "x ∈ S"
  by (metis Min_in assms finite.insertI insertE insert_not_empty)

lemma cval_add_simp[simp]:
  "(u ⊕ d) x = u x + d"
  unfolding cval_add_def by simp

lemmas [simp] = any_le_inf

lemma Le_in_between:
  assumes "a < b"
  obtains d where "a ≤ Le d" "Le d ≤ b"
  using assms by atomize_elim (cases a; cases b; auto)

lemma DBMEntry_le_to_sum:
  fixes e e' :: "'t :: time DBMEntry"
  assumes "e' ≠ ∞" "e ≤ e'"
  shows "- e' + e ≤ 0"
  using assms by (cases e; cases e') (auto simp: DBM.neutral DBM.add uminus)

lemma DBMEntry_le_add:
  fixes a b c :: "'t :: time DBMEntry"
  assumes "a ≤ b + c" "c ≠ ∞"
  shows "-c + a ≤ b"
  using assms
  by (cases a; cases b; cases c) (auto simp: DBM.neutral DBM.add uminus algebra_simps)

lemma DBM_triv_emptyI:
  assumes "M 0 0 < 0"
  shows "[M]⇘v,n⇙ = {}"
  using assms
  unfolding DBM_zone_repr_def DBM_val_bounded_def DBM.less_eq[symmetric] DBM.neutral by auto



section ‹Definition and Semantics of Constraint Systems›
datatype ('x, 'v) constr =
  Lower 'x "'v DBMEntry" | Upper 'x "'v DBMEntry" | Diff 'x 'x "'v DBMEntry"

type_synonym ('x, 'v) cs = "('x, 'v) constr set"

inductive entry_sem ("_ ⊨⇩e _" [62, 62] 62) where
  "v ⊨⇩e Lt x" if "v < x" |
  "v ⊨⇩e Le x" if "v ≤ x" |
  "v ⊨⇩e ∞"

inductive constr_sem ("_ ⊨⇩c _" [62, 62] 62) where
  "u ⊨⇩c Lower x e" if "- u x ⊨⇩e e" |
  "u ⊨⇩c Upper x e" if   "u x ⊨⇩e e" |
  "u ⊨⇩c Diff x y e" if "u x - u y ⊨⇩e e"

definition cs_sem ("_ ⊨⇩c⇩s _" [62, 62] 62) where
  "u ⊨⇩c⇩s cs ⟷ (∀c ∈ cs. u ⊨⇩c c)"

definition cs_models ("_ ⊨ _" [62, 62] 62) where
  "cs ⊨ c ≡ ∀u. u ⊨⇩c⇩s cs ⟶ u ⊨⇩c c"

definition cs_equiv ("_ ≡⇩c⇩s _" [62, 62] 62) where
  "cs ≡⇩c⇩s cs' ≡ ∀u. u ⊨⇩c⇩s cs ⟷ u ⊨⇩c⇩s cs'"

definition
  "closure cs ≡ {c. cs ⊨ c}"

definition
  "bot_cs = {Lower undefined (Lt 0), Upper undefined (Lt 0)}"

lemma constr_sem_less_eq_iff:
  "u ⊨⇩c Lower x e ⟷ Le (-u x) ≤ e"
  "u ⊨⇩c Upper x e ⟷ Le (u x) ≤ e"
  "u ⊨⇩c Diff x y e ⟷ Le (u x - u y) ≤ e"
  by (cases e; auto simp: constr_sem.simps entry_sem.simps)+

lemma constr_sem_mono:
  assumes "e ≤ e'"
  shows
    "u ⊨⇩c Lower x e  ⟹ u ⊨⇩c Lower x e'"
    "u ⊨⇩c Upper x e  ⟹ u ⊨⇩c Upper x e'"
    "u ⊨⇩c Diff x y e ⟹ u ⊨⇩c Diff x y e'"
  using assms unfolding constr_sem_less_eq_iff by simp+

lemma constr_sem_triv[simp,intro]:
  "u ⊨⇩c Upper x ∞" "u ⊨⇩c Lower y ∞" "u ⊨⇩c Diff x y ∞"
  unfolding constr_sem.simps entry_sem.simps by auto

lemma cs_sem_antimono:
  assumes "cs ⊆ cs'" "u ⊨⇩c⇩s cs'"
  shows "u ⊨⇩c⇩s cs"
  using assms unfolding cs_sem_def by auto

lemma cs_equivD[intro, dest]:
  assumes "u ⊨⇩c⇩s cs" "cs ≡⇩c⇩s cs'"
  shows "u ⊨⇩c⇩s cs'"
  using assms unfolding cs_equiv_def by auto

lemma cs_equiv_sym:
  "cs ≡⇩c⇩s cs'" if "cs' ≡⇩c⇩s cs"
  using that unfolding cs_equiv_def by fast

lemma cs_equiv_union:
  "cs ≡⇩c⇩s cs ∪ cs'" if "cs ≡⇩c⇩s cs'"
  using that unfolding cs_equiv_def cs_sem_def by blast

lemma cs_equiv_alt_def:
  "cs ≡⇩c⇩s cs' ⟷ (∀c. cs ⊨ c ⟷ cs' ⊨ c)"
  unfolding cs_equiv_def cs_models_def cs_sem_def by auto

lemma closure_equiv:
  "closure cs ≡⇩c⇩s cs"
  unfolding cs_equiv_alt_def closure_def cs_models_def cs_sem_def by auto

lemma closure_superset:
  "cs ⊆ closure cs"
  unfolding closure_def cs_models_def cs_sem_def by auto

lemma bot_cs_empty:
  "¬ (u :: ('c ⇒ 't :: linordered_ab_group_add)) ⊨⇩c⇩s bot_cs"
  unfolding bot_cs_def cs_sem_def by (auto elim!: constr_sem.cases entry_sem.cases)

lemma finite_bot_cs:
  "finite bot_cs"
  unfolding bot_cs_def by auto

definition cs_vars where
  "cs_vars cs = ⋃ (set1_constr ` cs)"

definition map_cs_vars where
  "map_cs_vars v cs = map_constr v id ` cs"

lemma constr_sem_rename_vars:
  assumes "inj_on v S" "set1_constr c ⊆ S"
  shows "(u o inv_into S v) ⊨⇩c map_constr v id c ⟷ u ⊨⇩c c"
  using assms
  by (cases c) (auto intro!: constr_sem.intros elim!: constr_sem.cases simp: DBMEntry.map_id)

lemma cs_sem_rename_vars:
  assumes "inj_on v (cs_vars cs)"
  shows "(u o inv_into (cs_vars cs) v) ⊨⇩c⇩s map_cs_vars v cs ⟷ u ⊨⇩c⇩s cs"
  using assms constr_sem_rename_vars unfolding map_cs_vars_def cs_sem_def cs_vars_def by blast


section ‹Conversion of DBMs to Constraint Systems and Back›

definition dbm_to_cs :: "nat ⇒ ('x ⇒ nat) ⇒ ('v :: {linorder,zero}) DBM ⇒ ('x, 'v) cs" where
  "dbm_to_cs n v M ≡ if M 0 0 < 0 then bot_cs else
    {Lower x (M 0 (v x)) | x. v x ≤ n} ∪
    {Upper x (M (v x) 0) | x. v x ≤ n} ∪
    {Diff x y (M (v x) (v y)) | x y. v x ≤ n ∧ v y ≤ n}"

lemma dbm_entry_val_Lower_iff:
  "dbm_entry_val u None (Some x) e ⟷ u ⊨⇩c Lower x e"
  by (cases e) (auto simp: constr_sem_less_eq_iff)

lemma dbm_entry_val_Upper_iff:
  "dbm_entry_val u (Some x) None e ⟷ u ⊨⇩c Upper x e"
  by (cases e) (auto simp: constr_sem_less_eq_iff)

lemma dbm_entry_val_Diff_iff:
  "dbm_entry_val u (Some x) (Some y) e ⟷ u ⊨⇩c Diff x y e"
  by (cases e) (auto simp: constr_sem_less_eq_iff)

lemmas dbm_entry_val_constr_sem_iff =
  dbm_entry_val_Lower_iff
  dbm_entry_val_Upper_iff
  dbm_entry_val_Diff_iff

theorem dbm_to_cs_correct:
  "u ⊢⇘v,n⇙ M ⟷ u ⊨⇩c⇩s dbm_to_cs n v M"
  apply (rule iffI)
  unfolding DBM_val_bounded_def dbm_entry_val_constr_sem_iff dbm_to_cs_def
  subgoal
    by (auto simp: DBM.neutral DBM.less_eq[symmetric] cs_sem_def)
  using bot_cs_empty by (cases "M 0 0 < 0", auto simp: DBM.neutral DBM.less_eq[symmetric] cs_sem_def)

definition
  "cs_to_dbm v cs ≡ if (∀u. ¬u ⊨⇩c⇩s cs) then (λ_ _. Lt 0) else (
    λi j.
      if i = 0 then
        if j = 0 then
          Le 0
        else
          Min (insert ∞ {e. ∃x. Lower x e ∈ cs ∧ v x = j})
      else
        if j = 0 then
          Min (insert ∞ {e. ∃x. Upper x e ∈ cs ∧ v x = i})
        else
          Min (insert ∞ {e. ∃x y. Diff x y e ∈ cs ∧ v x = i ∧ v y = j})
  )"

lemma finite_dbm_to_cs:
  assumes "finite {x. v x ≤ n}"
  shows "finite (dbm_to_cs n v M)"
  using [[simproc add: finite_Collect]] unfolding dbm_to_cs_def
  by (auto intro: assms simp: finite_bot_cs)

lemma empty_dbm_empty:
  "u ⊢⇘v,n⇙ (λ_ _. Lt 0) ⟷ False"
  unfolding DBM_val_bounded_def by (auto simp: DBM.less_eq[symmetric])

fun expr_of_constr where
  "expr_of_constr (Lower _ e) = e" |
  "expr_of_constr (Upper _ e) = e" |
  "expr_of_constr (Diff _ _ e) = e"

lemma cs_to_dbm1:
  assumes "∀x ∈ cs_vars cs. v x > 0 ∧ v x ≤ n" "finite cs"
  assumes "u ⊢⇘v,n⇙ cs_to_dbm v cs"
  shows "u ⊨⇩c⇩s cs"
proof (cases "∀u. ¬u ⊨⇩c⇩s cs")
  case True
  with assms(3) show ?thesis
    unfolding cs_to_dbm_def by (simp add: empty_dbm_empty)
next
  case False
  show "u ⊨⇩c⇩s cs"
    unfolding cs_sem_def
  proof (rule ballI)
    fix c
    assume "c ∈ cs"
    show "u ⊨⇩c c"
    proof (cases c)
      case (Lower x e)
      with assms(1) ‹c ∈ cs› have *: "0 < v x" "v x ≤ n"
        by (auto simp: cs_vars_def)
      let ?S = "{e. ∃x'. Lower x' e ∈ cs ∧ v x' = v x}"
      let ?e = "Min (insert ∞ ?S)"
      have "?S ⊆ expr_of_constr ` cs"
        by force
      with ‹finite cs› ‹c ∈ cs› ‹c = _› have "?e ≤ e"
        using finite_subset finite_imageI by (blast intro: Min_le)
      moreover from * assms(3) False have "dbm_entry_val u None (Some x) ?e"
        unfolding DBM_val_bounded_def cs_to_dbm_def by (auto 4 4)
      ultimately have "dbm_entry_val u None (Some x) (e)"
        by - (rule dbm_entry_val_mono[folded DBM.less_eq])
      then show ?thesis
        unfolding dbm_entry_val_constr_sem_iff[symmetric] ‹c = _› .
    next
      case (Upper x e)
      with assms(1) ‹c ∈ cs› have *: "0 < v x" "v x ≤ n"
        by (auto simp: cs_vars_def)
      let ?S = "{e. ∃x'. Upper x' e ∈ cs ∧ v x' = v x}"
      let ?e = "Min (insert ∞ ?S)"
      have "?S ⊆ expr_of_constr ` cs"
        by force
      with ‹finite cs› ‹c ∈ cs› ‹c = _› have "?e ≤ e"
        using finite_subset finite_imageI by (blast intro: Min_le)
      moreover from * assms(3) False have "dbm_entry_val u (Some x) None ?e"
        unfolding DBM_val_bounded_def cs_to_dbm_def by (auto 4 4)
      ultimately have "dbm_entry_val u (Some x) None e"
        by - (rule dbm_entry_val_mono[folded DBM.less_eq])
      then show ?thesis
        unfolding dbm_entry_val_constr_sem_iff ‹c = _› .
    next
      case (Diff x y e)
      with assms(1) ‹c ∈ cs› have *: "0 < v x" "v x ≤ n" "0 < v y" "v y ≤ n"
        by (auto simp: cs_vars_def)
      let ?S = "{e. ∃x' y'. Diff x' y' e ∈ cs ∧ v x' = v x ∧ v y' = v y}"
      let ?e = "Min (insert ∞ ?S)"
      have "?S ⊆ expr_of_constr ` cs"
        by force
      with ‹finite cs› ‹c ∈ cs› ‹c = _› have "?e ≤ e"
        using finite_subset finite_imageI by (blast intro: Min_le)
      moreover from * assms(3) False have "dbm_entry_val u (Some x) (Some y) ?e"
        unfolding DBM_val_bounded_def cs_to_dbm_def by (auto 4 4)
      ultimately have "dbm_entry_val u (Some x) (Some y) e"
        by - (rule dbm_entry_val_mono[folded DBM.less_eq])
      then show ?thesis
        unfolding dbm_entry_val_constr_sem_iff ‹c = _› .
    qed
  qed
qed

lemma cs_to_dbm2:
  assumes "∀x. v x ≤ n ⟶ v x > 0" "∀x y. v x ≤ n ∧ v y ≤ n ∧ v x = v y ⟶ x = y"
  assumes "finite cs"
  assumes "u ⊨⇩c⇩s cs"
  shows "u ⊢⇘v,n⇙ cs_to_dbm v cs"
proof (cases "∀u. ¬u ⊨⇩c⇩s cs")
  case True
  with assms show ?thesis
    unfolding cs_to_dbm_def by (simp add: empty_dbm_empty)
next
  case False
  let ?M = "cs_to_dbm v cs"
  show "u ⊢⇘v,n⇙ cs_to_dbm v cs"
    unfolding DBM_val_bounded_def DBM.less_eq[symmetric]
  proof (safe)
    show "Le 0 ≤ cs_to_dbm v cs 0 0"
      using False unfolding cs_to_dbm_def by auto
  next
    fix x :: 'a
    assume "v x ≤ n"
    let ?S = "{e. ∃x'. Lower x' e ∈ cs ∧ v x' = v x}"
    from ‹v x ≤ n› assms have "v x > 0"
      by simp
    with False have "?M 0 (v x) = Min (insert ∞ ?S)"
      unfolding cs_to_dbm_def by auto
    moreover have "finite ?S"
    proof -
      have "?S ⊆ expr_of_constr ` cs"
        by force
      also have "finite …"
        using ‹finite cs› by (rule finite_imageI)
      finally show ?thesis .
    qed
    ultimately show "dbm_entry_val u None (Some x) (?M 0 (v x))"
      using assms(2-) ‹v x ≤ n›
      apply (cases rule: Min_insert_cases)
       apply auto[]
      apply (simp add: dbm_entry_val_constr_sem_iff cs_sem_def, metis)
      done
  next
    fix x :: 'a
    assume "v x ≤ n"
    let ?S = "{e. ∃x'. Upper x' e ∈ cs ∧ v x' = v x}"
    from ‹v x ≤ n› assms have "v x > 0"
      by simp
    with False have "?M (v x) 0 = Min (insert ∞ ?S)"
      unfolding cs_to_dbm_def by auto
    moreover have "finite ?S"
    proof -
      have "?S ⊆ expr_of_constr ` cs"
        by force
      also have "finite …"
        using ‹finite cs› by (rule finite_imageI)
      finally show ?thesis .
    qed
    ultimately show "dbm_entry_val u (Some x) None (cs_to_dbm v cs (v x) 0)"
      using ‹v x ≤ n› assms(2-)
      apply (cases rule: Min_insert_cases)
       apply auto[]
      apply (simp add: dbm_entry_val_constr_sem_iff cs_sem_def, metis)
      done
  next
    fix x y :: 'a
    assume "v x ≤ n" "v y ≤ n"
    let ?S = "{e. ∃x' y'. Diff x' y' e ∈ cs ∧ v x' = v x ∧ v y' = v y}"
    from ‹v x ≤ n› ‹v y ≤ n› assms have "v x > 0" "v y > 0"
      by auto
    with False have "?M (v x) (v y) = Min (insert ∞ ?S)"
      unfolding cs_to_dbm_def by auto
    moreover have "finite ?S"
    proof -
      have "?S ⊆ expr_of_constr ` cs"
        by force
      also have "finite …"
        using ‹finite cs› by (rule finite_imageI)
      finally show ?thesis .
    qed
    ultimately show "dbm_entry_val u (Some x) (Some y) (cs_to_dbm v cs (v x) (v y))"
      using ‹v x ≤ n› ‹v y ≤ n› assms(2-)
      apply (cases rule: Min_insert_cases)
       apply auto[]
      apply (simp add: dbm_entry_val_constr_sem_iff cs_sem_def, metis)
      done
  qed
qed

theorem cs_to_dbm_correct:
  assumes "∀x ∈ cs_vars cs. v x ≤ n" "∀x. v x ≤ n ⟶ v x > 0"
    "∀x y. v x ≤ n ∧ v y ≤ n ∧ v x = v y ⟶ x = y"
    "finite cs"
  shows "u ⊢⇘v,n⇙ cs_to_dbm v cs ⟷ u ⊨⇩c⇩s cs"
  using assms by (blast intro: cs_to_dbm1 cs_to_dbm2)

corollary cs_to_dbm_correct':
  assumes
    "bij_betw v (cs_vars cs) {1..n}" "∀x. v x ≤ n ⟶ v x > 0" "∀x. x ∉ cs_vars cs ⟶ v x > n"
    "finite cs"
  shows "u ⊢⇘v,n⇙ cs_to_dbm v cs ⟷ u ⊨⇩c⇩s cs"
proof (rule cs_to_dbm_correct , safe)
  fix x assume "x ∈ cs_vars cs"
  then show "v x ≤ n"
    using assms(1) unfolding bij_betw_def by auto
next
  fix x assume "v x ≤ n"
  then show "0 < v x"
    using assms(2) by blast
next
  fix x y :: 'a
  assume A: "v x ≤ n" "v y ≤ n" "v x = v y"
  with A assms show "x = y"
    unfolding bij_betw_def by (auto dest!: inj_onD)
next
  show "finite cs"
    by (rule assms)
qed


section ‹Application: Relaxation On Constraint Systems›
text ‹The following is a sample application of viewing DBMs as constraint systems.
We show define an equivalent of the @{term up} operation on DBMs, prove it correct,
and then derive an alternative correctness proof for @{term up}.
›
definition
  "up_cs cs = {c. c ∈ cs ∧ (case c of Upper _ _ ⇒ False | _ ⇒ True)}"

lemma Lower_shiftI:
  "u ⊕ d ⊨⇩c Lower x e" if "u ⊨⇩c Lower x e" "(d :: 't :: linordered_ab_group_add) ≥ 0"
  using that diff_mono less_trans not_less_iff_gr_or_eq
  by (cases e;fastforce simp: constr_sem_less_eq_iff)

lemma Upper_shiftI:
  "u ⊕ d ⊨⇩c Upper x e" if "u ⊨⇩c Upper x e" "(d :: 't :: linordered_ab_group_add) ≤ 0"
  using that add_less_le_mono
  by (cases e) (fastforce simp: constr_sem_less_eq_iff add.commute add_decreasing)+

lemma Diff_shift:
  "u ⊕ d ⊨⇩c Diff x y e ⟷ u ⊨⇩c Diff x y e" for d :: "'t :: linordered_ab_group_add"
  by (cases e) (auto simp: constr_sem_less_eq_iff)

lemma up_cs_complete:
  "u ⊕ d ⊨⇩c⇩s up_cs cs" if "u ⊨⇩c⇩s cs" "d ≥ 0" for d :: "'t :: linordered_ab_group_add"
  using that unfolding up_cs_def cs_sem_def
  apply clarsimp
  subgoal for x
    by (cases x) (auto simp: Diff_shift intro: Lower_shiftI)
  done


definition
  "lower_upper_closed cs ≡ ∀x y e e'.
    Lower x e ∈ cs ∧ Upper y e' ∈ cs ⟶ (∃ e''. Diff y x e'' ∈ cs ∧ e'' ≤ e + e')"

lemma up_cs_sound:
  assumes "u ⊨⇩c⇩s up_cs cs" "lower_upper_closed cs" "finite cs"
  obtains u' and d :: "'t :: time" where "d ≥ 0" "u' ⊨⇩c⇩s cs" "u = u' ⊕ d"
proof -
  define U and L and LT where
    "U ≡ {e  + Le (-u x) | x e. Upper x e ∈ cs ∧ e ≠ ∞}"
    and "L ≡ {-e + Le (-u x) | x e. Lower x e ∈ cs ∧ e ≠ ∞}"
    and "LT ≡ {Le (-d - u x) | x d. Lower x (Lt d) ∈ cs}"
  note defs = U_def L_def LT_def
  let ?l = "Max L" and ?u = "Min U"
  have "LT ⊆ L"
    by (force simp: DBM_arith_defs defs)
  have Diff_semD: "u ⊨⇩c Diff y x (e + e')" if "Lower x e ∈ cs" "Upper y e' ∈ cs" for x y e e'
  proof -
    from assms that obtain e'' where "Diff y x e'' ∈ cs" "e'' ≤ e + e'"
      unfolding lower_upper_closed_def cs_equiv_def by blast
    with assms(1) show ?thesis
      unfolding cs_sem_def up_cs_def by (auto intro: constr_sem_mono)
  qed
  have Lower_semD: "u ⊨⇩c Lower x e" if "Lower x e ∈ cs" for x e
    using that assms unfolding cs_sem_def up_cs_def by auto
  have Lower_boundI: "-e + Le (-u x) ≤ 0" if "Lower x e ∈ cs" "e ≠ ∞" for x e
    using Lower_semD[OF that(1)] that(2) unfolding constr_sem_less_eq_iff
    by (intro DBMEntry_le_to_sum)
  from ‹finite cs› have "finite L"
    unfolding defs
    by (force intro: finite_subset[where B = "(λc. case c of Lower x e ⇒ - e + Le (- u x)) ` cs"])
  from ‹finite cs› have "finite U"
    unfolding defs
    by (force intro: finite_subset[where B = "(λc. case c of Upper x e ⇒ e + Le (- u x)) ` cs"])
  note L_ge = Max_ge[OF ‹finite L›] and U_le = Min_le[OF ‹finite U›]
  have L_0: "Max L ≤ 0" if "L ≠ {}"
    by (intro Max.boundedI ‹finite L› that) (auto intro: Lower_boundI simp: defs)
  have L_U: "Max L ≤ Min U" if "L ≠ {}" "U ≠ {}"
    apply (intro Max_le_MinI ‹finite L› ‹finite U› that)
    apply (clarsimp simp: defs)
    apply (drule (1) Diff_semD)
    subgoal for x y e e'
      unfolding constr_sem_less_eq_iff
      by (cases e; cases e'; simp add: DBM_arith_defs; simp add: algebra_simps)
    done
  consider
    (L_empty) "L = {}" | (Lt_empty) "LT = {}" | (L_gt_Lt) "Max L > Max LT" |
    (Lt_Max) x d where "Lower x (Lt d) ∈ cs" "Le (-d - u x) ∈ LT" "Max L = Le (-d - u x)"
    by (smt finite_subset Max_in Max_mono ‹finite L› ‹LT ⊆ L› less_le mem_Collect_eq defs)
  note L_Lt_cases = this
  have Lt_Max_rule: "- c - u x < 0"
    if "Lower x (Lt c) ∈ cs" "Max L = Le (- c - u x)" "L ≠ {}" for c x
    using that
    by (metis DBMEntry.distinct(1) L_0 Le_le_LeD Le_less_Lt Lower_semD
          add.inverse_inverse constr_sem_less_eq_iff(1) eq_iff_diff_eq_0 less_le neutral)
  have LT_0_boundI: "∃d ≤ 0. (∀l ∈ L. l ≤ Le d) ∧ (∀l ∈ LT. l < Le d)" if ‹L ≠ {}›
  proof -
    obtain d where d: "?l ≤ Le d" "d ≤ 0"
      by (metis L_0 ‹L ≠ {}› neutral order_refl)
    show ?thesis
    proof (cases rule: L_Lt_cases)
      case L_empty
      with ‹L ≠ {}› show ?thesis
        by simp
    next
      case Lt_empty
      then show ?thesis
        by (smt L_ge d(1,2) empty_iff leD leI less_le_trans)
    next
      case L_gt_Lt
      then show ?thesis
        by (smt finite_subset Max_ge ‹finite L› ‹LT ⊆ L› d(1,2) leD leI less_le_trans)
    next
      case (Lt_Max x c)
      define d where "d ≡ - c - u x"
      from Lt_Max(1,3) ‹L ≠ {}› have "d < 0"
        unfolding d_def by (rule Lt_Max_rule)
      then obtain d' where d': "d < d'" "d' < 0"
        using dense by auto
      have "∀l ∈ L. l < Le d'"
      proof safe
        fix l
        assume "l ∈ L"
        then have "l ≤ Le d"
          unfolding d_def ‹Max L = _›[symmetric] by (rule L_ge)
        also from d' have "… < Le d'"
          by auto
        finally show "l < Le d'" .
      qed
      with Lt_Max(1,3) d' ‹finite L› ‹L ≠ {}› ‹LT ⊆ L› show ?thesis
        by (intro exI[of _ d']) auto
    qed
  qed
  consider
      (none)   "L = {}" "U = {}"
    | (upper)  "L = {}" "U ≠ {}"
    | (lower)  "L ≠ {}" "U = {}"
    | (proper) "L ≠ {}" "U ≠ {}"
    by force
  text ‹The main statement of of the proof. Note that most of the lengthiness of the proof is
  owed to the third conjunct. Our initial hope was that this conjunct would not be needed.›
  then obtain d where d: "d ≤ 0" "∀l ∈ L. l ≤ Le d" "∀l ∈ LT. l < Le d" "∀u ∈ U. Le d ≤ u"
  proof cases
    case none
    then show ?thesis
      by (intro that[of 0]) (auto simp: defs)
  next
    case upper
    obtain d where "Le d ≤ Min U" "d ≤ 0"
      by (smt DBMEntry.distinct(3) add_inf(2) any_le_inf neg_le_0_iff_le DBM.neutral
            order.not_eq_order_implies_strict sum_gt_neutral_dest')
    then show ?thesis
      using upper ‹finite U› by (intro that[of d]) (auto simp: defs)
  next
    case lower
    obtain d where d: "Max L ≤ Le d" "d ≤ 0"
      by (smt L_0 lower(1) neutral order_refl)
    show ?thesis
    proof (cases rule: L_Lt_cases)
      case L_empty
      with lower(1) show ?thesis
        by simp
    next
      case Lt_empty
      then show ?thesis
        by (metis (lifting) L_ge d(1,2) empty_iff leD leI less_le_trans lower(2) that)
    next
      case L_gt_Lt
      then show ?thesis
        using LT_0_boundI lower(1,2) that by blast
    next
      case (Lt_Max x c)
      define d where "d ≡ - c - u x"
      from Lt_Max(1,3) lower(1) have "d < 0"
        unfolding d_def by (rule Lt_Max_rule)
      then obtain d' where d': "d < d'" "d' < 0"
        using dense by auto
      have "∀l ∈ L. l < Le d'"
      proof safe
        fix l
        assume "l ∈ L"
        then have "l ≤ Le d"
          unfolding d_def ‹Max L = _›[symmetric] by (rule L_ge)
        also from d' have "… < Le d'"
          by auto
        finally show "l < Le d'" .
      qed
      with Lt_Max(1,3) d' ‹finite L› lower ‹LT ⊆ L› show ?thesis
        by (intro that[of d']) auto
    qed
  next
    case proper
    with L_U L_0 have "Max L ≤ Min U" "Max L ≤ 0"
      by auto
    from ‹finite U› ‹U ≠ {}› have "?u ∈ U"
      unfolding U_def by (rule Min_in)
    have main:
      "∃d'. -d - u x < d' ∧ Le d' < ?u"
      if "Lower x (Lt d) ∈ cs" "Le (-d - u x) ∈ LT" "?l = Le (-d - u x)" for d x
    proof (cases ?u)
      case (Le d')
      with ‹?u ∈ U› obtain e y where *: "Le d' = e + Le (- u y)" "Upper y e ∈ cs"
        unfolding U_def by auto
      then obtain d1 where "e = Le d1"
        by (cases e) (auto simp: DBM_arith_defs)
      with * have "d' = d1 - u y"
        by (auto simp: DBM_arith_defs)
      from Diff_semD[OF ‹Lower x (Lt d) ∈ cs› ‹Upper y e ∈ _›] have "u y - u x < d + d1"
        unfolding constr_sem_less_eq_iff ‹e = _› by (simp add: DBM_arith_defs)
      then have "- d - u x < d'"
        unfolding ‹d' = _› by (simp add: algebra_simps)
      then obtain d1 where "-d - u x < d1" "d1 < d'"
        using dense by auto
      with ‹?u = _› show ?thesis
        by (intro exI[where x = d1]) auto
    next
      case (Lt d')
      with ‹?u ∈ U› obtain e y where *: "Lt d' = e + Le (- u y)" "Upper y e ∈ cs"
        unfolding U_def by auto
      then obtain d1 where "e = Lt d1"
        by (cases e) (auto simp: DBM_arith_defs)
      with * have "d' = d1 - u y"
        by (auto simp: DBM_arith_defs)
      from Diff_semD[OF ‹Lower x (Lt d) ∈ cs› ‹Upper y e ∈ _›] have "u y - u x < d + d1"
        unfolding constr_sem_less_eq_iff ‹e = _› by (simp add: DBM_arith_defs)
      then have "- d - u x < d'"
        unfolding ‹d' = _› by (simp add: algebra_simps)
      then obtain d1 where "-d - u x < d1" "d1 < d'"
        using dense by auto
      with ‹?u = _› show ?thesis
        by (intro exI[where x = d1]) auto
    next
      case INF
      with ‹?u ∈ U› show ?thesis
        using Lt_Max_rule proper(1) that(1,3) by fastforce
    qed
    consider (eq) "Max L = Min U" | (0) "Min U ≥ 0" | (gt) "Max L < Min U" "Min U < 0"
      using ‹Max L ≤ Min U› by fastforce
    then show ?thesis
    proof cases
      case eq
      from proper ‹finite L› ‹finite U› have "?l ∈ L" "?u ∈ U"
        by - (rule Max_in Min_in; assumption)+
      then obtain x y e e' where *:
        "?l = - e + Le (- u x)" "Lower x e ∈ cs" "e ≠ ∞"
        "?u = e' + Le (- u y)" "Upper y e' ∈ cs" "e' ≠ ∞"
        unfolding defs by auto
      with ‹?l = ?u› obtain d where d: "?l = Le d"
        apply (cases e; cases e'; simp add: DBM_arith_defs)
        subgoal for a b
        proof -
          assume prems: "- a - u x = b - u y" "e = Le a" "e' = Lt b"
          from * have "u ⊨⇩c Diff y x (e + e')"
            by (intro Diff_semD)
          with prems have False
            by (simp add: DBM_arith_defs constr_sem_less_eq_iff algebra_simps)
          then show ?thesis ..
        qed
        done
      from ‹?l ≤ 0› have **: "d ≤ 0" "∀l ∈ L. l ≤ Le d" "∀u ∈ U. Le d ≤ u"
          apply (simp add: DBM.neutral d)
         apply (auto simp: d[symmetric] intro: L_ge)[]
        apply (auto simp: d[symmetric] eq intro: U_le L_ge)[]
        done
      show ?thesis
      proof (cases rule: L_Lt_cases)
        case L_empty
        with ‹L ≠ {}› show ?thesis
          by simp
      next
        case Lt_empty
        with ** show ?thesis
          by (intro that[of d]) auto
      next
        case L_gt_Lt
        with ** show ?thesis
          by (intro that[of d]; simp)
             (metis finite_subset Max_ge ‹LT ⊆ L› ‹finite L› d le_less_trans)
      next
        case (Lt_Max y d1)
        from main[OF this] obtain d' where "d' > - d1 - u y" "Le d' < Min U"
          by auto
        with ** Lt_Max(3)[symmetric] d eq show ?thesis
          by (intro that[of d']; simp)
      qed
    next
      case 0
      from LT_0_boundI[OF ‹L ≠ {}›] obtain d where "d ≤ 0" "∀l∈L. l ≤ Le d" "∀l∈LT. l < Le d"
        by safe
      with ‹Max L ≤ 0› ‹finite L› ‹finite U› proper 0 show ?thesis
        by (intro that[of d]) (auto simp: DBM.neutral intro: order_trans)
    next
      case gt
      then obtain d where d: "Max L ≤ Le d" "Le d ≤ Min U"
        by (elim Le_in_between)
      with ‹_ < 0› have "Le d < 0"
        by auto
      then have "d ≤ 0"
        by (simp add: neutral)
      show ?thesis
      proof (cases rule: L_Lt_cases)
        case L_empty
        with ‹L ≠ {}› show ?thesis
          by simp
      next
        case Lt_empty
        with d ‹d ≤ 0› show ?thesis
          using proper ‹finite L› ‹finite U› by (intro that[of d]) (auto intro: L_ge U_le)
      next
        case L_gt_Lt
        with d ‹d ≤ 0› proper ‹finite L› ‹finite U› show ?thesis
          apply (intro that[of d])
             apply (auto intro: L_ge U_le)[2]
           apply (meson finite_subset Max_ge ‹LT ⊆ L› le_less_trans less_le_trans)
          apply simp
          done
      next
        case (Lt_Max y d1)
        from main[OF this] obtain d' where d': "d' > - d1 - u y" "Le d' < Min U"
          by auto
        with d have d_bounds: "?l < Le d'" "Le d' ≤ ?u"
          unfolding ‹?l = _› by auto
        from ‹?l < Le d'› have "∀l ∈ L. l < Le d'"
          using Max_less_iff ‹finite L› by blast
        moreover from ‹Le d' ≤ ?u› ‹?u < 0› have "d' ≤ 0"
          by (metis Le_le_LeD le_less_trans neutral order.strict_iff_order)
        with d Lt_Max(3)[symmetric] d_bounds d' ‹LT ⊆ L› show ?thesis
          using proper ‹finite L› ‹finite U›
          by (intro that[of d']; auto)
      qed
    qed
  qed
  have "u ⊕ d ⊨⇩c⇩s cs"
    unfolding cs_sem_def
  proof safe
    fix c :: "('a, 't) constr"
    assume "c ∈ cs"
    show "u ⊕ d ⊨⇩c c"
    proof (cases c)
      case (Lower x e)
      show ?thesis
      proof (cases "e = ∞")
        case True
        with ‹c = _› show ?thesis
          by (auto simp: constr_sem_less_eq_iff)
      next
        case False
        with ‹c = _› ‹c ∈ _› have "-e + Le (-u x) ∈ L"
          unfolding defs by auto
        with d have "-e + Le (-u x) ≤ Le d"
          by auto
        then show ?thesis
          using d(3) ‹c ∈ _› unfolding ‹c = _› constr_sem_less_eq_iff
          apply (cases e; simp add: defs DBM_arith_defs)
           apply (metis diff_le_eq minus_add_distrib minus_le_iff uminus_add_conv_diff)
          apply (metis ab_group_add_class.ab_diff_conv_add_uminus leD le_less less_diff_eq
                minus_diff_eq neg_less_iff_less)
          done
      qed
    next
      case (Upper x e)
      show ?thesis
      proof (cases "e = ∞")
        case True
        with ‹c = _› show ?thesis
          by (auto simp: constr_sem_less_eq_iff)
      next
        case False
        with ‹c = _› ‹c ∈ _› have "e + Le (-u x) ∈ U"
          by (auto simp: defs)
        with d show ?thesis
          by (cases e) (auto simp: ‹c = _› constr_sem_less_eq_iff DBM_arith_defs algebra_simps)
      qed
    next
      case (Diff x y e)
      with assms ‹c ∈ cs› show ?thesis
        by (auto simp: Diff_shift cs_sem_def up_cs_def)
    qed
  qed
  with ‹d ≤ 0› show ?thesis
    by (intro that[of "-d" "u ⊕ d"]; simp add: cval_add_def)
qed
text ‹Note that if we compare this proof to @{thm DBM_up_sound'}, we can see that we have
not gained much. Settling on DBM entry arithmetic as done above was not the optimal choice for this
proof, while it can drastically simply some other proofs.
Also, note that the final theorem we obtain below (‹DBM_up_correct›)
is slightly stronger than what we would get with @{thm DBM_up_sound'}.
Finally, note that a more elegant definition of @{term lower_upper_closed} would probably be:
\<^text>‹
definition
  "lower_upper_closed cs ≡ ∀x y e e'.
    cs ⊨ Lower x e ∧ cs ⊨ Upper y e' ⟶ (∃ e''. cs ⊨ Diff y x e'' ∧ e'' ≤ e + e')"›
This would mean that in the proof we would have to replace minimum and maximum by
supremum and infimum. The advantage would be that the finiteness assumption could be removed. 
However, as our DBM entries do not come with ‹-∞›, they do not form a complete lattice.
Thus we would either have to make this extension or directly refer to the embedded values
directly, which would again have to form a complete lattice.
Both variants come with some technical inconvenience.
›

lemma up_cs_sem:
  fixes cs :: "('x, 'v :: time) cs"
  assumes "lower_upper_closed cs" "finite cs"
  shows "{u. u ⊨⇩c⇩s up_cs cs} = {u ⊕ d | u d. u ⊨⇩c⇩s cs ∧ d ≥ 0}"
  by safe (metis up_cs_sound up_cs_complete assms)+

definition
  close_lu :: "('t::linordered_cancel_ab_semigroup_add) DBM ⇒ 't DBM"
where
  "close_lu M ≡ λi j. if i > 0 then min (dbm_add (M i 0) (M 0 j)) (M i j) else M i j"

definition
  up' :: "('t::linordered_cancel_ab_semigroup_add) DBM ⇒ 't DBM"
where
  "up' M ≡ λi j. if i > 0 ∧ j = 0 then ∞ else M i j"

lemma up_alt_def:
  "up M = up' (close_lu M)"
  by (intro ext) (simp add: up_def up'_def close_lu_def)

lemma close_lu_equiv:
  fixes M :: "'t ::time DBM"
  shows "dbm_to_cs n v M ≡⇩c⇩s dbm_to_cs n v (close_lu M)"
  unfolding cs_equiv_def dbm_to_cs_correct[symmetric]
    DBM_val_bounded_def close_lu_def dbm_entry_val_constr_sem_iff
  unfolding min_def DBM.add[symmetric]
  unfolding constr_sem_less_eq_iff
  unfolding DBM.less_eq[symmetric] DBM.neutral[symmetric]
  apply (auto simp:)[]
            apply (force simp add: add_increasing2)
           apply (metis (full_types) le0)+
  subgoal premises prems for u c1 c2
  proof -
    have "Le (u c1 - u c2) = Le (u c1) + Le (- u c2)"
      by (simp add: DBM_arith_defs)
    also from prems have "… ≤ M (v c1) 0 + M 0 (v c2)"
      by (intro add_mono) auto
    finally show ?thesis .
  qed
  by (smt leI le_zero_eq order_trans | metis le0)+

lemma close_lu_closed:
  "lower_upper_closed (dbm_to_cs n v (close_lu M))" if "M 0 0 ≥ 0"
  using that unfolding lower_upper_closed_def dbm_to_cs_def close_lu_def
  apply (clarsimp; safe)
  subgoal
    by auto
  subgoal for x y
    by (auto simp: DBM.add[symmetric])
       (metis add.commute add.right_neutral add_left_mono min.absorb2 min.cobounded1)
  by (simp add: add_increasing2)

lemma close_lu_closed': ― ‹Unused›
  "lower_upper_closed (dbm_to_cs n v (close_lu M) ∪ dbm_to_cs n v M)" if "M 0 0 ≥ 0"
  using that unfolding lower_upper_closed_def dbm_to_cs_def close_lu_def
  apply (clarsimp; safe)
  subgoal
    by auto
  subgoal for x y
    by (metis DBM.add add.commute add.right_neutral add_left_mono min.absorb2 min.cobounded1)
  subgoal for x y
    by (metis DBM.add add.commute min.cobounded1)
  by (simp add: add_increasing2)

lemma up_cs_up'_equiv:
  fixes M :: "'t ::time DBM"
  assumes "M 0 0 ≥ 0" "clock_numbering v"
  shows "up_cs (dbm_to_cs n v M) ≡⇩c⇩s dbm_to_cs n v (up' M)"
  using assms
  unfolding up'_def up_cs_def cs_equiv_def dbm_to_cs_correct[symmetric]
    DBM_val_bounded_def close_lu_def dbm_entry_val_constr_sem_iff
  by (auto split: if_split_asm
      simp: dbm_to_cs_def cs_sem_def DBM.add[symmetric] DBM.less_eq[symmetric] DBM.neutral)

lemma up_equiv_cong: ― ‹Unused›
  fixes cs cs' :: "('x, 'v :: time) cs"
  assumes "cs ≡⇩c⇩s cs'" "finite cs" "finite cs'" "lower_upper_closed cs" "lower_upper_closed cs'"
  shows "up_cs cs ≡⇩c⇩s up_cs cs'"
  using assms unfolding cs_equiv_def by (metis up_cs_complete up_cs_sound)

lemma DBM_up_correct:
  fixes M :: "'t ::time DBM"
  assumes "clock_numbering v" "finite {x. v x ≤ n}"
  shows "u ∈ ([M]⇘v,n⇙)⇧↑ ⟷ u ∈ [up M]⇘v,n⇙"
proof (cases "M 0 0 ≥ 0")
  case True
  have "u ∈ ([M]⇘v,n⇙)⇧↑ ⟷ (∃d u'. u' ⊢⇘v,n⇙ M ∧ d ≥ 0 ∧ u = u' ⊕ d)"
    unfolding DBM_zone_repr_def zone_delay_def by auto
  also have "… ⟷ (∃d u'. u' ⊨⇩c⇩s dbm_to_cs n v M ∧ d ≥ 0 ∧ u = u' ⊕ d)"
    unfolding dbm_to_cs_correct ..
  also have "… ⟷ (∃d u'. u' ⊨⇩c⇩s dbm_to_cs n v (close_lu M) ∧ d ≥ 0 ∧ u = u' ⊕ d)"
    using cs_equivD close_lu_equiv cs_equiv_sym by metis
  also have "… ⟷ u ⊨⇩c⇩s up_cs (dbm_to_cs n v (close_lu M))"
  proof -
    let ?cs = "dbm_to_cs n v (close_lu M)"
    have "lower_upper_closed ?cs"
      by (intro close_lu_closed True)
    moreover have "finite ?cs"
      by (intro finite_dbm_to_cs assms)
    ultimately have "{u. u ⊨⇩c⇩s up_cs ?cs} = {u ⊕ d |u d. u ⊨⇩c⇩s ?cs ∧ 0 ≤ d}"
      by (rule up_cs_sem)
    then show ?thesis
      by (auto 4 3)
  qed
  also have "… ⟷ u ⊨⇩c⇩s dbm_to_cs n v (up' (close_lu M))"
  proof -
    from ‹M 0 0 ≥ 0› have "up_cs (dbm_to_cs n v (close_lu M)) ≡⇩c⇩s dbm_to_cs n v (up' (close_lu M))"
      by (intro up_cs_up'_equiv[OF _ ‹clock_numbering v›], simp add: close_lu_def)
    then show ?thesis
      using cs_equivD cs_equiv_sym by metis
  qed
  also have "… ⟷ u ⊨⇩c⇩s dbm_to_cs n v (up M)"
    unfolding up_alt_def ..
  also have "… ⟷ u ⊢⇘v,n⇙ up M"
    unfolding dbm_to_cs_correct ..
  also have "… ⟷ u ∈ [up M]⇘v,n⇙"
    unfolding DBM_zone_repr_def by blast
  finally show ?thesis .
next
  case False
  then have "M 0 0 < 0"
    by auto
  then have "up M 0 0 < 0"
    unfolding up_def by auto
  with ‹M 0 0 < 0› have "[M]⇘v,n⇙ = {}" "[up M]⇘v,n⇙ = {}"
    by (auto intro!: DBM_triv_emptyI)
  then show ?thesis
    unfolding zone_delay_def by blast
qed

end