# Theory Timed_Automata.Approx_Beta

```theory Approx_Beta
imports DBM_Zone_Semantics Regions_Beta Closure
begin

chapter ‹Correctness of ‹β›-approximation from ‹α›-regions›

text ‹Instantiating real›

begin

definition
neutral_real: "𝟭 = (0 :: real)"

instance by standard (auto simp: neutral_real)

end

text ‹Merging the locales for the two types of regions›

locale Regions =
fixes X and k :: "'c ⇒ nat" and v :: "'c ⇒ nat" and n :: nat and not_in_X
assumes finite: "finite X"
assumes clock_numbering: "clock_numbering' v n" "∀k≤n. k > 0 ⟶ (∃c ∈ X. v c = k)"
"∀ c ∈ X. v c ≤ n"
assumes not_in_X: "not_in_X ∉ X"
assumes non_empty: "X ≠ {}"
begin

definition ℛ_def:  "ℛ ≡ {Regions.region X I r | I r. Regions.valid_region X k I r}"
definition ℛ⇩β_def: "ℛ⇩β ≡ {Regions_Beta.region X I J r | I J r. Regions_Beta.valid_region X k I J r}"
definition V_def:  "V ≡ {v . ∀ x ∈ X. v x ≥ 0}"

sublocale alpha_interp: AlphaClosure X k ℛ V by (unfold_locales) (auto simp: finite ℛ_def V_def)

sublocale beta_interp: Beta_Regions' X k ℛ⇩β V v n not_in_X
using finite non_empty clock_numbering not_in_X by (unfold_locales) (auto simp: ℛ⇩β_def V_def)

abbreviation "Approx⇩β ≡ beta_interp.Approx⇩β"

section ‹Preparing Bouyer's Theorem›

lemma region_dbm:
assumes "R ∈ ℛ"
defines "v' ≡ λ i. THE c. c ∈ X ∧ v c = i"
obtains M
where"[M]⇘v,n⇙ = R"
and "∀ i ≤ n. ∀ j ≤ n. M i 0 = ∞ ∧ j > 0 ∧ i ≠ j⟶ M i j = ∞ ∧ M j i = ∞"
and "∀ i ≤ n. M i i = Le 0"
and "∀ i ≤ n. ∀ j ≤ n. i > 0 ∧ j > 0 ∧ M i 0 ≠ ∞ ∧ M j 0 ≠ ∞ ⟶ (∃ d :: int.
(- k (v' j) ≤ d ∧ d ≤ k (v' i) ∧ M i j = Le d ∧ M j i = Le (-d))
∨ (- k (v' j) ≤ d - 1 ∧ d ≤ k (v' i) ∧ M i j = Lt d ∧ M j i = Lt (-d + 1)))"
and "∀ i ≤ n. i > 0 ∧ M i 0 ≠ ∞ ⟶
(∃ d :: int. d ≤ k (v' i) ∧ d ≥ 0
∧ (M i 0 = Le d ∧ M 0 i = Le (-d) ∨ M i 0 = Lt d ∧ M 0 i = Lt (-d + 1)))"
and "∀ i ≤ n. i > 0 ⟶ (∃ d :: int. - k (v' i) ≤ d ∧ d ≤ 0 ∧ (M 0 i = Le d ∨ M 0 i = Lt d))"
and "∀ i. ∀ j. M i j ≠ ∞ ⟶ get_const (M i j) ∈ ℤ"
and "∀ i ≤ n. ∀ j ≤ n. M i j ≠ ∞ ∧ i > 0 ∧ j > 0 ⟶
(∃ d:: int. (M i j = Le d ∨ M i j = Lt d) ∧ (- k (v' j)) ≤ d ∧ d ≤ k (v' i))"
proof -
from assms obtain I r where R: "R = region X I r" "valid_region X k I r" unfolding ℛ_def by blast
let ?X⇩0 = "{x ∈ X. ∃d. I x = Regions.intv.Intv d}"
define f where "f x = (if isIntv (I x) then Lt (intv_const (I x) + 1)
else if isConst (I x) then Le (intv_const (I x))
else ∞)" for x
define g where "g x = (if isIntv (I x) then Lt (- intv_const (I x))
else if isConst (I x) then Le (- intv_const (I x))
else Lt (- k x))" for x
define h where "h x y = (if isIntv (I x) ∧ isIntv (I y) then
if (y, x) ∈ r ∧ (x, y) ∉ r then Lt (int (intv_const (I x)) - intv_const (I y) + 1)
else if (x, y) ∈ r ∧ (y, x) ∉ r then Lt (int (intv_const (I x)) - intv_const (I y))
else Le (int (intv_const (I x)) - intv_const (I y))
else if isConst (I x) ∧ isConst (I y) then Le (int (intv_const (I x)) - intv_const (I y))
else if isIntv (I x) ∧ isConst (I y) then Lt (int (intv_const (I x)) + 1 - intv_const (I y))
else if isConst (I x) ∧ isIntv (I y) then Lt (int (intv_const (I x)) - intv_const (I y))
else ∞)" for x y
let ?M = "λ i j. if i = 0 then if j = 0 then Le 0 else g (v' j)
else if j = 0 then f (v' i) else if i = j then Le 0 else h (v' i) (v' j)"
have "[?M]⇘v,n⇙ ⊆ R"
proof
fix u assume u: "u ∈ [?M]⇘v,n⇙"
show "u ∈ R" unfolding R
proof (standard, goal_cases)
case 1
show ?case
proof
fix c assume c: "c ∈ X"
with clock_numbering have c2: "v c ≤ n" "v c > 0" "v' (v c) = c" unfolding v'_def by auto
with u have "dbm_entry_val u None (Some c) (g c)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
then show "0 ≤ u c" by (cases "isIntv (I c)"; cases "isConst (I c)") (auto simp: g_def)
qed
next
case 2
show ?case
proof
fix c assume c: "c ∈ X"
with clock_numbering have c2: "v c ≤ n" "v c > 0" "v' (v c) = c" unfolding v'_def by auto
with u have *: "dbm_entry_val u None (Some c) (g c)" "dbm_entry_val u (Some c) None (f c)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
show "intv_elem c u (I c)"
proof (cases "I c")
case (Const d)
then have "¬ isIntv (I c)" "isConst (I c)" by auto
with * Const show ?thesis unfolding g_def f_def using Const by auto
next
case (Intv d)
then have "isIntv (I c)" "¬ isConst (I c)" by auto
with * Intv show ?thesis unfolding g_def f_def by auto
next
case (Greater d)
then have "¬ isIntv (I c)" "¬ isConst (I c)" by auto
with * Greater R(2) c show ?thesis unfolding g_def f_def by fastforce
qed
qed
next
show "?X⇩0 = ?X⇩0" ..
show "∀x ∈ ?X⇩0. ∀ y ∈ ?X⇩0. (x, y) ∈ r ⟷ frac (u x) ≤ frac (u y)"
proof (standard, standard)
fix x y assume A: "x ∈ ?X⇩0" "y ∈ ?X⇩0"
show "(x, y) ∈ r ⟷ frac (u x) ≤ frac (u y)"
proof (cases "x = y")
case True
have "refl_on ?X⇩0 r" using R(2) by auto
with A True show ?thesis unfolding refl_on_def by auto
next
case False
from A obtain d d' where AA:
"I x = Intv d" "I y = Intv d'" "isIntv (I x)" "isIntv (I y)" "¬ isConst (I x)" "¬ isConst (I y)"
by auto
from A False clock_numbering have B:
"v x ≤ n" "v x > 0" "v' (v x) = x" "v y ≤ n" "v y > 0" "v' (v y) = y" "v x ≠ v y"
unfolding v'_def by auto
with u have *:
"dbm_entry_val u (Some x) (Some y) (h x y)" "dbm_entry_val u (Some y) (Some x) (h y x)"
"dbm_entry_val u None (Some x) (g x)" "dbm_entry_val u (Some x) None (f x)"
"dbm_entry_val u None (Some y) (g y)" "dbm_entry_val u (Some y) None (f y)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by force+
show "(x, y) ∈ r ⟷ frac (u x) ≤ frac (u y)"
proof
assume C: "(x, y) ∈ r"
show "frac (u x) ≤ frac (u y)"
proof (cases "(y, x) ∈ r")
case False
with * AA C have **:
"u x - u y < int d - d'"
"d < u x" "u x < d + 1" "d' < u y" "u y < d' + 1"
unfolding f_def g_def h_def by auto
from nat_intv_frac_decomp[OF **(2,3)] nat_intv_frac_decomp[OF **(4,5)] **(1) show
"frac (u x) ≤ frac (u y)"
by simp
next
case True
with * AA C have **:
"u x - u y ≤ int d - d'"
"d < u x" "u x < d + 1" "d' < u y" "u y < d' + 1"
unfolding f_def g_def h_def by auto
from nat_intv_frac_decomp[OF **(2,3)] nat_intv_frac_decomp[OF **(4,5)] **(1) show
"frac (u x) ≤ frac (u y)"
by simp
qed
next
assume "frac (u x) ≤ frac (u y)"
show "(x, y) ∈ r"
proof (rule ccontr)
assume C: "(x,y) ∉ r"
moreover from R(2) have "total_on ?X⇩0 r" by auto
ultimately have "(y, x) ∈ r" using False A unfolding total_on_def by auto
with *(2-) AA C have **:
"u y - u x < int d' - d"
"d < u x" "u x < d + 1" "d' < u y" "u y < d' + 1"
unfolding f_def g_def h_def by auto
from nat_intv_frac_decomp[OF **(2,3)] nat_intv_frac_decomp[OF **(4,5)] **(1) have
"frac (u y) < frac (u x)"
by simp
with ‹frac _ ≤ _› show False by auto
qed
qed
qed
qed
qed
qed
moreover have "R ⊆ [?M]⇘v,n⇙"
proof
fix u assume u: "u ∈ R"
show "u ∈ [?M]⇘v,n⇙" unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (safe, goal_cases)
case 1 then show ?case by auto
next
case (2 c)
with clock_numbering have "c ∈ X" by metis
with clock_numbering have *: "c ∈ X" "v c > 0" "v' (v c) = c" unfolding v'_def by auto
with R u have "intv_elem c u (I c)" "valid_intv (k c) (I c)" by auto
then have "dbm_entry_val u None (Some c) (g c)" unfolding g_def by (cases "I c") auto
with * show ?case by auto
next
case (3 c)
with clock_numbering have "c ∈ X" by metis
with clock_numbering have *: "c ∈ X" "v c > 0" "v' (v c) = c" unfolding v'_def by auto
with R u have "intv_elem c u (I c)" "valid_intv (k c) (I c)" by auto
then have "dbm_entry_val u (Some c) None (f c)" unfolding f_def by (cases "I c") auto
with * show ?case by auto
next
case (4 c1 c2)
with clock_numbering have "c1 ∈ X" "c2 ∈ X" by metis+
with clock_numbering have *:
"c1 ∈ X" "v c1 > 0" "v' (v c1) = c1" "c2 ∈ X" "v c2 > 0" "v' (v c2) = c2"
unfolding v'_def by auto
with R u have
"intv_elem c1 u (I c1)" "valid_intv (k c1) (I c1)"
"intv_elem c2 u (I c2)" "valid_intv (k c2) (I c2)"
by auto
then have "dbm_entry_val u (Some c1) (Some c2) (h c1 c2)" unfolding h_def
proof(cases "I c1", cases "I c2", fastforce+, cases "I c2", fastforce, goal_cases)
case (1 d d')
then show ?case
proof (cases "(c2, c1) ∈ r", goal_cases)
case 1
show ?case
proof (cases "(c1, c2) ∈ r")
case True
with 1 *(1,4) R(1) u have "frac (u c1) = frac (u c2)" by auto
with 1 have "u c1 - u c2 = real d - d'" by (fastforce dest: nat_intv_frac_decomp)
with 1 show ?thesis by auto
next
case False with 1 show ?thesis by auto
qed
next
case 2
show ?case
proof (cases "c1 = c2")
case True then show ?thesis by auto
next
case False
with 2 R(2) *(1,4) have "(c1, c2) ∈ r" by (fastforce simp: total_on_def)
with 2 *(1,4) R(1) u have "frac (u c1) < frac (u c2)" by auto
with 2 have "u c1 - u c2 < real d - d'" by (fastforce dest: nat_intv_frac_decomp)
with 2 show ?thesis by auto
qed
qed
qed fastforce+
then show ?case
proof (cases "v c1 = v c2", goal_cases)
case True with * clock_numbering have "c1 = c2" by auto
then show ?thesis by auto
next
case 2 with * show ?case by auto
qed
qed
qed
ultimately have "[?M]⇘v,n⇙ = R" by blast
moreover have "∀ i ≤ n. ∀ j ≤ n. ?M i 0 = ∞ ∧ j > 0 ∧ i ≠ j ⟶ ?M i j = ∞ ∧ ?M j i = ∞"
unfolding f_def h_def by auto
moreover have "∀ i ≤ n. ?M i i = Le 0" by auto
moreover
{ fix i j assume A: "i ≤ n" "j ≤ n" "i > 0" "j > 0" "?M i 0 ≠ ∞" "?M j 0 ≠ ∞"
with clock_numbering(2) obtain c1 c2 where B: "v c1 = i" "v c2 = j" "c1 ∈ X" "c2 ∈ X" by meson
with clock_numbering(1) A have C: "v' i = c1" "v' j = c2" unfolding v'_def by force+
from R(2) B have valid: "valid_intv (k c1) (I c1)" "valid_intv (k c2) (I c2)" by auto
have "∃ d :: int. (- k (v' j) ≤ d ∧ d ≤ k (v' i) ∧ ?M i j = Le d ∧ ?M j i = Le (-d)
∨ (- k (v' j) ≤ d - 1 ∧ d ≤ k (v' i) ∧ ?M i j = Lt d ∧ ?M j i = Lt (-d + 1)))"
proof (cases "i = j")
case True
then show ?thesis by auto
next
case False
then show ?thesis
proof (cases "I c1", goal_cases)
case 1
then show ?case
proof (cases "I c2")
case Const
let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
from Const 1 have "isConst (I c1)" "isConst (I c2)" by auto
with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
next
case Intv
let ?d = "int(intv_const (I c1)) - int (intv_const (I c2))"
from Intv 1 have "isConst (I c1)" "isIntv (I c2)" by auto
with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
next
case Greater
then have "¬ isIntv (I c2)" "¬ isConst (I c2)" by auto
with A 1(1) C have False unfolding f_def by simp
then show ?thesis by fast
qed
next
case 2
then show ?case
proof (cases "I c2")
case Const
let ?d = "int (intv_const (I c1)) + 1 - int (intv_const (I c2))"
from Const 2 have "isIntv (I c1)" "isConst (I c2)" by auto
with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
next
case Intv
with 2 have *: "isIntv (I c1)" "isIntv (I c2)" by auto
from Intv A(1-4) C show ?thesis apply simp
proof (standard, goal_cases)
case 1
show ?case
proof (cases "(c2, c1) ∈ r")
case True
note T = this
show ?thesis
proof (cases "(c1, c2) ∈ r")
case True
let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
from True T * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
next
case False
let ?d = "int (intv_const (I c1)) - int (intv_const (I c2)) + 1"
from False T * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
qed
next
case False
let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
from False * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
qed
qed
next
case Greater
then have "¬ isIntv (I c2)" "¬ isConst (I c2)" by auto
with A 2(1) C have False unfolding f_def by simp
then show ?thesis by fast
qed
next
case 3
then have "¬ isIntv (I c1)" "¬ isConst (I c1)" by auto
with A 3(1) C have False unfolding f_def by simp
then show ?thesis by fast
qed
qed
}
moreover
{ fix i assume A: "i ≤ n" "i > 0" "?M i 0 ≠ ∞"
with clock_numbering(2) obtain c1 where B: "v c1 = i" "c1 ∈ X" by meson
with clock_numbering(1) A have C: "v' i = c1" unfolding v'_def by force+
from R(2) B have valid: "valid_intv (k c1) (I c1)" by auto
have "∃ d :: int. d ≤ k (v' i) ∧ d ≥ 0
∧ (?M i 0 = Le d ∧ ?M 0 i = Le (-d) ∨ ?M i 0 = Lt d ∧ ?M 0 i = Lt (-d + 1))"
proof (cases "i = 0")
case True
then show ?thesis by auto
next
case False
then show ?thesis
proof (cases "I c1", goal_cases)
case 1
let ?d = "int (intv_const (I c1))"
from 1 have "isConst (I c1)" "¬ isIntv (I c1)" by auto
with A C valid show ?thesis unfolding f_def g_def by (intro exI[where x = ?d]) auto
next
case 2
let ?d = "int (intv_const (I c1)) + 1"
from 2 have "isIntv(I c1)" "¬ isConst (I c1)" by auto
with A C valid show ?thesis unfolding f_def g_def by (intro exI[where x = ?d]) auto
next
case 3
then have "¬ isIntv (I c1)" "¬ isConst (I c1)" by auto
with A 3(1) C have False unfolding f_def by simp
then show ?thesis by fast
qed
qed
}
moreover
{ fix i assume A: "i ≤ n" "i > 0"
with clock_numbering(2) obtain c1 where B: "v c1 = i" "c1 ∈ X" by meson
with clock_numbering(1) A have C: "v' i = c1" unfolding v'_def by force+
from R(2) B have valid: "valid_intv (k c1) (I c1)" by auto
have "∃ d :: int. - k (v' i) ≤ d ∧ d ≤ 0 ∧ (?M 0 i = Le d ∨ ?M 0 i = Lt d)"
proof (cases "i = 0")
case True
then show ?thesis by auto
next
case False
then show ?thesis
proof (cases "I c1", goal_cases)
case 1
let ?d = "- int (intv_const (I c1))"
from 1 have "isConst (I c1)" "¬ isIntv (I c1)" by auto
with A C valid show ?thesis unfolding f_def g_def by (intro exI[where x = ?d]) auto
next
case 2
let ?d = "- int (intv_const (I c1))"
from 2 have "isIntv(I c1)" "¬ isConst (I c1)" by auto
with A C valid show ?thesis unfolding f_def g_def by (intro exI[where x = ?d]) auto
next
case 3
let ?d = "- (k c1)"
from 3 have "¬ isIntv (I c1)" "¬ isConst (I c1)" by auto
with A C show ?thesis unfolding g_def by (intro exI[where x = ?d]) auto
qed
qed
}
moreover have "∀ i. ∀ j. ?M i j ≠ ∞ ⟶ get_const (?M i j) ∈ ℤ" unfolding f_def g_def h_def by auto
moreover have "∀ i ≤ n. ∀ j ≤ n. i > 0 ∧ j > 0 ∧ ?M i j ≠ ∞
⟶ (∃ d:: int. (?M i j = Le d ∨ ?M i j = Lt d) ∧ (- k (v' j)) ≤ d ∧ d ≤ k (v' i))"
proof (auto, goal_cases)
case A: (1 i j)
with clock_numbering(2) obtain c1 c2 where B: "v c1 = i" "c1 ∈ X" "v c2 = j" "c2 ∈ X" by meson
with clock_numbering(1) A have C: "v' i = c1" "v' j = c2" unfolding v'_def by force+
from R(2) B have valid: "valid_intv (k c1) (I c1)" "valid_intv (k c2) (I c2)" by auto
with A B C show ?case
proof (simp, goal_cases)
case 1
show ?case
proof (cases "I c1", goal_cases)
case 1
then show ?case
proof (cases "I c2")
case Const
let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
from Const 1 have "isConst (I c1)" "isConst (I c2)" by auto
with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
next
case Intv
let ?d = "int(intv_const (I c1)) - int (intv_const (I c2))"
from Intv 1 have "isConst (I c1)" "isIntv (I c2)" by auto
with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
next
case Greater
then have "¬ isIntv (I c2)" "¬ isConst (I c2)" by auto
with A 1(1) C show ?thesis unfolding h_def by simp
qed
next
case 2
then show ?case
proof (cases "I c2")
case Const
let ?d = "int (intv_const (I c1)) + 1 - int (intv_const (I c2))"
from Const 2 have "isIntv (I c1)" "isConst (I c2)" by auto
with A(1-4) C valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
next
case Intv
with 2 have *: "isIntv (I c1)" "isIntv (I c2)" by auto
from Intv A(1-4) C show ?thesis
proof goal_cases
case 1
show ?case
proof (cases "(c2, c1) ∈ r")
case True
note T = this
show ?thesis
proof (cases "(c1, c2) ∈ r")
case True
let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
from True T * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
next
case False
let ?d = "int (intv_const (I c1)) - int (intv_const (I c2)) + 1"
from False T * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
qed
next
case False
let ?d = "int (intv_const (I c1)) - int (intv_const (I c2))"
from False * valid show ?thesis unfolding h_def by (intro exI[where x = ?d]) auto
qed
qed
next
case Greater
then have "¬ isIntv (I c2)" "¬ isConst (I c2)" by auto
with A 2(1) C show ?thesis unfolding h_def by simp
qed
next
case 3
then have "¬ isIntv (I c1)" "¬ isConst (I c1)" by auto
with A 3(1) C show ?thesis unfolding h_def by simp
qed
qed
qed
moreover show ?thesis
apply (rule that)
apply (rule calculation(1))
apply (rule calculation(2))
apply (rule calculation(3))
apply (blast intro: calculation)+
apply (rule calculation(7))
using calculation(8) apply blast
done
qed

lemma len_inf_elem:
"(a, b) ∈ set (arcs i j xs) ⟹ M a b = ∞ ⟹ len M i j xs = ∞"
apply (induction rule: arcs.induct)
apply (auto simp: mult)
apply (rename_tac a' b' x xs)
apply (case_tac "M a' x")
by auto

lemma dbm_add_strict_right_mono_neutral: "a < Le d ⟹ a + Le (-d) < Le 0"
unfolding less mult by (cases a) (auto elim!: dbm_lt.cases)

lemma dbm_lt_not_inf_less[intro]: "A ≠ ∞ ⟹ A ≺ ∞" by (cases A) auto

"a + ∞ = ∞" "∞ + a = ∞"
unfolding mult by (cases a) auto

lemma inf_lt[simp,dest!]:
"∞ < x ⟹ False"
by (cases x) (auto simp: less)

lemma zone_diag_lt:
assumes "a ≤ n" "b ≤ n" and C: "v c1 = a" "v c2 = b" and not0: "a > 0" "b > 0"
shows "[(λ i j. if i = a ∧ j = b then Lt d else ∞)]⇘v,n⇙ = {u. u c1 - u c2 < d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (standard, goal_cases)
case 1
then show ?case using ‹a ≤ n› ‹b ≤ n› C by fastforce
next
case 2
then show ?case
proof (safe, goal_cases)
case 1 from not0 show ?case unfolding dbm_le_def by auto
next
case 2 with not0 show ?case by auto
next
case 3 with not0 show ?case by auto
next
case (4 u' y z)
show ?case
proof (cases "v y = a ∧ v z = b")
case True
with 4 clock_numbering C ‹a ≤ n› ‹b ≤ n› have "u' y - u' z < d" by metis
with True show ?thesis by auto
next
case False then show ?thesis by auto
qed
qed
qed

lemma zone_diag_le:
assumes "a ≤ n" "b ≤ n" and C: "v c1 = a" "v c2 = b" and not0: "a > 0" "b > 0"
shows "[(λ i j. if i = a ∧ j = b then Le d else ∞)]⇘v,n⇙ = {u. u c1 - u c2 ≤ d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (rule, goal_cases)
case 1
then show ?case using ‹a ≤ n› ‹b ≤ n› C by fastforce
next
case 2
then show ?case
proof (safe, goal_cases)
case 1 from not0 show ?case unfolding dbm_le_def by auto
next
case 2 with not0 show ?case by auto
next
case 3 with not0 show ?case by auto
next
case (4 u' y z)
show ?case
proof (cases "v y = a ∧ v z = b")
case True
with 4 clock_numbering C ‹a ≤ n› ‹b ≤ n› have "u' y - u' z ≤ d" by metis
with True show ?thesis by auto
next
case False then show ?thesis by auto
qed
qed
qed

lemma zone_diag_lt_2:
assumes "a ≤ n" and C: "v c = a" and not0: "a > 0"
shows "[(λ i j. if i = a ∧ j = 0 then Lt d else ∞)]⇘v,n⇙ = {u. u c < d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (rule, goal_cases)
case 1
then show ?case using ‹a ≤ n› C by fastforce
next
case 2
then show ?case
proof (safe, goal_cases)
case 1 from not0 show ?case unfolding dbm_le_def by auto
next
case 2 with not0 show ?case by auto
next
case (3 u c)
show ?case
proof (cases "v c = a")
case False then show ?thesis by auto
next
case True
with 3 clock_numbering C ‹a ≤ n› have "u c < d" by metis
with C show ?thesis by auto
qed
next
case (4 u' y z)
from clock_numbering(1) have "0 < v z" by auto
then show ?case by auto
qed
qed

lemma zone_diag_le_2:
assumes "a ≤ n" and C: "v c = a" and not0: "a > 0"
shows "[(λ i j. if i = a ∧ j = 0 then Le d else ∞)]⇘v,n⇙ = {u. u c ≤ d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (rule, goal_cases)
case 1
then show ?case using ‹a ≤ n› C by fastforce
next
case 2
then show ?case
proof (safe, goal_cases)
case 1 from not0 show ?case unfolding dbm_le_def by auto
next
case 2 with not0 show ?case by auto
next
case (3 u c)
show ?case
proof (cases "v c = a")
case False then show ?thesis by auto
next
case True
with 3 clock_numbering C ‹a ≤ n› have "u c ≤ d" by metis
with C show ?thesis by auto
qed
next
case (4 u' y z)
from clock_numbering(1) have "0 < v z" by auto
then show ?case by auto
qed
qed

lemma zone_diag_lt_3:
assumes "a ≤ n" and C: "v c = a" and not0: "a > 0"
shows "[(λ i j. if i = 0 ∧ j = a then Lt d else ∞)]⇘v,n⇙ = {u. - u c < d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (rule, goal_cases)
case 1
then show ?case using ‹a ≤ n› C by fastforce
next
case 2
then show ?case
proof (safe, goal_cases)
case 1 from not0 show ?case unfolding dbm_le_def by auto
next
case (2 u c)
show ?case
proof (cases "v c = a", goal_cases)
case False then show ?thesis by auto
next
case True
with 2 clock_numbering C ‹a ≤ n› have "- u c < d" by metis
with C show ?thesis by auto
qed
next
case (3 u) with not0 show ?case by auto
next
case (4 u' y z)
from clock_numbering(1) have "0 < v y" by auto
then show ?case by auto
qed
qed

lemma len_int_closed:
"∀ i j. (M i j :: real) ∈ ℤ ⟹ len M i j xs ∈ ℤ"
by (induction xs arbitrary: i) auto

lemma get_const_distr:
"a ≠ ∞ ⟹ b ≠ ∞ ⟹ get_const (a + b) = get_const a + get_const b"
by (cases a) (cases b, auto simp: mult)+

lemma len_int_dbm_closed:
"∀ (i, j) ∈ set (arcs i j xs). (get_const (M i j) :: real) ∈ ℤ ∧ M i j ≠ ∞
⟹ get_const (len M i j xs) ∈ ℤ ∧ len M i j xs ≠ ∞"
by (induction xs arbitrary: i) (auto simp: get_const_distr, simp add: dbm_add_not_inf mult)

lemma zone_diag_le_3:
assumes "a ≤ n" and C: "v c = a" and not0: "a > 0"
shows "[(λ i j. if i = 0 ∧ j = a then Le d else ∞)]⇘v,n⇙ = {u. - u c ≤ d}"
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (rule, goal_cases)
case 1
then show ?case using ‹a ≤ n› C by fastforce
next
case 2
then show ?case
proof (safe, goal_cases)
case 1 from not0 show ?case unfolding dbm_le_def by auto
next
case (2 u c)
show ?case
proof (cases "v c = a")
case False then show ?thesis by auto
next
case True
with 2 clock_numbering C ‹a ≤ n› have "- u c ≤ d" by metis
with C show ?thesis by auto
qed
next
case (3 u) with not0 show ?case by auto
next
case (4 u' y z)
from clock_numbering(1) have "0 < v y" by auto
then show ?case by auto
qed
qed

lemma dbm_lt':
assumes "[M]⇘v,n⇙ ⊆ V" "M a b ≤ Lt d" "a ≤ n" "b ≤ n" "v c1 = a" "v c2 = b" "a > 0" "b > 0"
shows "[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 - u c2 < d}"
proof -
from assms have "[M]⇘v,n⇙ ⊆ [(λ i j. if i = a ∧ j = b then Lt d else ∞)]⇘v,n⇙"
apply safe
apply (rule DBM_le_subset)
unfolding less_eq dbm_le_def by auto
moreover from zone_diag_lt[OF ‹a ≤ n› ‹b ≤ n› assms(5-)]
have "[(λ i j. if i = a ∧ j = b then Lt d else ∞)]⇘v,n⇙ = {u. u c1 - u c2 < d}" by blast
moreover from assms have "[M]⇘v,n⇙ ⊆ V" by auto
ultimately show ?thesis by auto
qed

lemma dbm_lt'2:
assumes "[M]⇘v,n⇙ ⊆ V" "M a 0 ≤ Lt d" "a ≤ n" "v c1 = a" "a > 0"
shows "[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 < d}"
proof -
from assms(2) have "[M]⇘v,n⇙ ⊆ [(λ i j. if i = a ∧ j = 0 then Lt d else ∞)]⇘v,n⇙"
apply safe
apply (rule DBM_le_subset)
unfolding less_eq dbm_le_def by auto
moreover from zone_diag_lt_2[OF ‹a ≤ n› assms(4,5)]
have "[(λ i j. if i = a ∧ j = 0 then Lt d else ∞)]⇘v,n⇙ = {u. u c1 < d}" by blast
ultimately show ?thesis using assms(1) by auto
qed

lemma dbm_lt'3:
assumes "[M]⇘v,n⇙ ⊆ V" "M 0 a ≤ Lt d" "a ≤ n" "v c1 = a" "a > 0"
shows "[M]⇘v,n⇙ ⊆ {u ∈ V. - u c1 < d}"
proof -
from assms(2) have "[M]⇘v,n⇙ ⊆ [(λ i j. if i = 0 ∧ j = a then Lt d else ∞)]⇘v,n⇙"
apply safe
apply (rule DBM_le_subset)
unfolding less_eq dbm_le_def by auto
moreover from zone_diag_lt_3[OF ‹a ≤ n› assms(4,5)]
have "[(λ i j. if i = 0 ∧ j = a then Lt d else ∞)]⇘v,n⇙ = {u. - u c1 < d}" by blast
ultimately show ?thesis using assms(1) by auto
qed

lemma dbm_le':
assumes "[M]⇘v,n⇙ ⊆ V" "M a b ≤ Le d" "a ≤ n" "b ≤ n" "v c1 = a" "v c2 = b" "a > 0" "b > 0"
shows "[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 - u c2 ≤ d}"
proof -
from assms have "[M]⇘v,n⇙ ⊆ [(λ i j. if i = a ∧ j = b then Le d else ∞)]⇘v,n⇙"
apply safe
apply (rule DBM_le_subset)
unfolding less_eq dbm_le_def by auto
moreover from zone_diag_le[OF ‹a ≤ n› ‹b ≤ n› assms(5-)]
have "[(λ i j. if i = a ∧ j = b then Le d else ∞)]⇘v,n⇙ = {u. u c1 - u c2 ≤ d}" by blast
moreover from assms have "[M]⇘v,n⇙ ⊆ V" by auto
ultimately show ?thesis by auto
qed

lemma dbm_le'2:
assumes "[M]⇘v,n⇙ ⊆ V" "M a 0 ≤ Le d" "a ≤ n" "v c1 = a" "a > 0"
shows "[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 ≤ d}"
proof -
from assms(2) have "[M]⇘v,n⇙ ⊆ [(λ i j. if i = a ∧ j = 0 then Le d else ∞)]⇘v,n⇙"
apply safe
apply (rule DBM_le_subset)
unfolding less_eq dbm_le_def by auto
moreover from zone_diag_le_2[OF ‹a ≤ n› assms(4,5)]
have "[(λ i j. if i = a ∧ j = 0 then Le d else ∞)]⇘v,n⇙ = {u. u c1 ≤ d}" by blast
ultimately show ?thesis using assms(1) by auto
qed

lemma dbm_le'3:
assumes "[M]⇘v,n⇙ ⊆ V" "M 0 a ≤ Le d" "a ≤ n" "v c1 = a" "a > 0"
shows "[M]⇘v,n⇙ ⊆ {u ∈ V. - u c1 ≤ d}"
proof -
from assms(2) have "[M]⇘v,n⇙ ⊆ [(λ i j. if i = 0 ∧ j = a then Le d else ∞)]⇘v,n⇙"
apply safe
apply (rule DBM_le_subset)
unfolding less_eq dbm_le_def by auto
moreover from zone_diag_le_3[OF ‹a ≤ n› assms(4,5)]
have "[(λ i j. if i = 0 ∧ j = a then Le d else ∞)]⇘v,n⇙ = {u. - u c1 ≤ d}" by blast
ultimately show ?thesis using assms(1) by auto
qed

lemma int_zone_dbm:
assumes "∀ (_,d) ∈ collect_clock_pairs cc. d ∈ ℤ" "∀ c ∈ collect_clks cc. v c ≤ n"
obtains M where "{u. u ⊢ cc} = [M]⇘v,n⇙" and "dbm_int M n"
using int_zone_dbm[OF _ assms] clock_numbering(1) by auto

lemma non_empty_dbm_diag_set':
assumes "clock_numbering' v n" "∀i≤n. ∀j≤n. M i j ≠ ∞ ⟶ get_const (M i j) ∈ ℤ"
"[M]⇘v,n⇙ ≠ {}"
obtains M' where "[M]⇘v,n⇙ = [M']⇘v,n⇙ ∧ (∀i≤n. ∀j≤n. M' i j ≠ ∞ ⟶ get_const (M' i j) ∈ ℤ)
∧ (∀ i ≤ n. M' i i = 𝟭)"
proof -
let ?M = "λi j. if i = j then 𝟭 else M i j"
from non_empty_dbm_diag_set[OF assms(1,3)] have "[M]⇘v,n⇙ = [?M]⇘v,n⇙" by auto
moreover from assms(2) have "∀i≤n. ∀j≤n. ?M i j ≠ ∞ ⟶ get_const (?M i j) ∈ ℤ"
unfolding neutral by auto
moreover have "∀ i ≤ n. ?M i i = 𝟭" by auto
ultimately show ?thesis by (auto intro: that)
qed

lemma dbm_entry_int:
"x ≠ ∞ ⟹ get_const x ∈ ℤ ⟹ ∃ d :: int. x = Le d ∨ x = Lt d"
apply (cases x) using Ints_cases by auto

abbreviation "vabstr ≡ beta_interp.vabstr"

section ‹Bouyer's Main Theorem›

theorem region_zone_intersect_empty_approx_correct:
assumes "R ∈ ℛ" "Z ⊆ V" "R ∩ Z = {}" "vabstr Z M"
shows "R ∩ Approx⇩β Z = {}"
proof -
define v' where "v' i = (THE c. c ∈ X ∧ v c = i)" for i
from region_dbm[OF assms(1)] obtain M⇩R where M⇩R:
"[M⇩R]⇘v,n⇙ = R" "∀i≤n. ∀j≤n. M⇩R i 0 = ∞ ∧ 0 < j ∧ i ≠ j ⟶ M⇩R i j = ∞ ∧ M⇩R j i = ∞"
"∀i≤n. M⇩R i i = Le 0"
"∀i≤n. ∀j≤n. 0 < i ∧ 0 < j ∧ M⇩R i 0 ≠ ∞ ∧ M⇩R j 0 ≠ ∞ ⟶
(∃d. - int (k (THE c. c ∈ X ∧ v c = j)) ≤ d ∧ d ≤ int (k (THE c. c ∈ X ∧ v c = i))
∧ M⇩R i j = Le d ∧ M⇩R j i = Le (real_of_int (- d))
∨ - int (k (THE c. c ∈ X ∧ v c = j)) ≤ d - 1 ∧ d ≤ int (k (THE c. c ∈ X ∧ v c = i))
∧ M⇩R i j = Lt d ∧ M⇩R j i = Lt (real_of_int (- d + 1)))"
"∀i≤n. 0 < i ∧ M⇩R i 0 ≠ ∞ ⟶ (∃d≤int (k (THE c. c ∈ X ∧ v c = i)). d ≥ 0 ∧
(M⇩R i 0 = Le d ∧ M⇩R 0 i = Le (real_of_int (- d)) ∨ M⇩R i 0 = Lt d ∧ M⇩R 0 i = Lt (real_of_int (- d + 1))))"
"∀i≤n. 0 < i ⟶ (∃d≥- int (k (THE c. c ∈ X ∧ v c = i)). d ≤ 0 ∧ (M⇩R 0 i = Le d ∨ M⇩R 0 i = Lt d))"
"∀i j. M⇩R i j ≠ ∞ ⟶ get_const (M⇩R i j) ∈ ℤ"
"∀i≤n. ∀j≤n. M⇩R i j ≠ ∞ ∧ 0 < i ∧ 0 < j ⟶ (∃d. (M⇩R i j = Le d ∨ M⇩R i j = Lt d)
∧ - int (k (THE c. c ∈ X ∧ v c = j)) ≤ d ∧ d ≤ int (k (THE c. c ∈ X ∧ v c = i)))"
.
show ?thesis
proof (cases "R = {}")
case True then show ?thesis by auto
next
case False
from clock_numbering(2) have cn_weak: "∀k≤n. 0 < k ⟶ (∃ c. v c = k)" by auto

show ?thesis
proof (cases "Z = {}")
case True
then show ?thesis using beta_interp.apx_empty by blast
next
case False
from assms(4) have
"Z = [M]⇘v,n⇙" "∀ i≤n. ∀ j≤n. M i j ≠ ∞ ⟶ get_const (M i j) ∈ ℤ"
by auto
from this(1) non_empty_dbm_diag_set'[OF clock_numbering(1) this(2)] ‹Z ≠ {}› obtain M where M:
"Z = [M]⇘v,n⇙ ∧ (∀i≤n. ∀j≤n. M i j ≠ ∞ ⟶ get_const (M i j) ∈ ℤ) ∧ (∀i≤n. M i i = 𝟭)"
by auto
with not_empty_cyc_free[OF cn_weak] False have "cyc_free M n" by auto
then have "cycle_free M n" using cycle_free_diag_equiv by auto
from M have "Z = [FW M n]⇘v,n⇙" unfolding neutral by (auto intro!: FW_zone_equiv[OF cn_weak])
moreover from fw_canonical[OF ‹cycle_free M _›] M have "canonical (FW M n) n" unfolding neutral by auto
moreover from FW_int_preservation M have
"∀i≤n. ∀j≤n. FW M n i j ≠ ∞ ⟶ get_const (FW M n i j) ∈ ℤ"
by auto
ultimately obtain M where M:
"[M]⇘v,n⇙ = Z" "canonical M n" "∀i≤n. ∀j≤n. M i j ≠ ∞ ⟶ get_const (M i j) ∈ ℤ"
by blast
let ?M = "λ i j. min (M i j) (M⇩R i j)"
from M(1) M⇩R(1) assms have "[M]⇘v,n⇙ ∩ [M⇩R]⇘v,n⇙ = {}" by auto
moreover from DBM_le_subset[folded less_eq, of n ?M M] have "[?M]⇘v,n⇙ ⊆ [M]⇘v,n⇙" by auto
moreover from DBM_le_subset[folded less_eq, of n ?M M⇩R] have "[?M]⇘v,n⇙ ⊆ [M⇩R]⇘v,n⇙" by auto
ultimately have "[?M]⇘v,n⇙ = {}" by blast
then have "¬ cyc_free ?M n" using cyc_free_not_empty[of n ?M v] clock_numbering(1) by auto
then obtain i xs where xs: "i ≤ n" "set xs ⊆ {0..n}" "len ?M i i xs < 𝟭" by auto
from this(1,2) canonical_shorten_rotate_neg_cycle[OF M(2) this(2,1,3)] obtain i ys where ys:
"len ?M i i ys < 𝟭"
"set ys ⊆ {0..n}" "successive (λ(a, b). ?M a b = M a b) (arcs i i ys)" "i ≤ n"
and distinct: "distinct ys" "i ∉ set ys"
and cycle_closes: "ys ≠ [] ⟶ ?M i (hd ys) ≠ M i (hd ys) ∨ ?M (last ys) i ≠ M (last ys) i"
by fastforce

have one_M_aux:
"len ?M i j ys = len M⇩R i j ys" if "∀ (a,b) ∈ set (arcs i j ys). M a b ≥ M⇩R a b" for j
using that by (induction ys arbitrary: i) (auto simp: min_def)
have one_M: "∃ (a,b) ∈ set (arcs i i ys). M a b < M⇩R a b"
proof (rule ccontr, goal_cases)
case 1
then have "∀(a, b)∈set (arcs i i ys). M⇩R a b ≤ M a b" by auto
from one_M_aux[OF this] have "len ?M i i ys = len M⇩R i i ys" .
with Nil ys(1) xs(3) have "len M⇩R i i ys < 𝟭" by simp
from DBM_val_bounded_neg_cycle[OF _ ‹i ≤ n› ‹set ys ⊆ _› this cn_weak]
have "[M⇩R]⇘v,n⇙ = {}" unfolding DBM_zone_repr_def by auto
with ‹R ≠ {}› M⇩R(1) show False by auto
qed
have one_M_R_aux:
"len ?M i j ys = len M i j ys" if "∀ (a,b) ∈ set (arcs i j ys). M a b ≤ M⇩R a b" for j
using that by (induction ys arbitrary: i) (auto simp: min_def)
have one_M_R: "∃ (a,b) ∈ set (arcs i i ys). M a b > M⇩R a b"
proof (rule ccontr, goal_cases)
case 1
then have "∀(a, b)∈set (arcs i i ys). M⇩R a b ≥ M a b" by auto
from one_M_R_aux[OF this] have "len ?M i i ys = len M i i ys" .
with Nil ys(1) xs(3) have "len M i i ys < 𝟭" by simp
from DBM_val_bounded_neg_cycle[OF _ ‹i ≤ n› ‹set ys ⊆ _› this cn_weak]
have "[M]⇘v,n⇙ = {}" unfolding DBM_zone_repr_def by auto
with ‹Z ≠ {}› M(1) show False by auto
qed

have 0: "(0,0) ∉ set (arcs i i ys)"
proof (cases "ys = []")
case False with distinct show ?thesis using arcs_distinct1 by blast
next
case True with ys(1) have "?M i i < 𝟭" by auto
then have "M i i < 𝟭 ∨ M⇩R i i < 𝟭" by (simp add: min_less_iff_disj)
from one_M one_M_R True show ?thesis by auto
qed

{ fix a b assume A: "(a,b) ∈ set (arcs i i ys)"
assume not0: "a > 0"
from aux1[OF ys(4,4,2) A] have C2: "a ≤ n" by auto
then obtain c1 where C: "v c1 = a" "c1 ∈ X"
using clock_numbering(2) not0 unfolding v'_def by meson
then have "v' a = c1" using clock_numbering C2 not0 unfolding v'_def by fastforce
with C C2 have "∃ c ∈ X. v c = a ∧ v' a = c" "a ≤ n" by auto
} note clock_dest_1 = this
{ fix a b assume A: "(a,b) ∈ set (arcs i i ys)"
assume not0: "b > 0"
from aux1[OF ys(4,4,2) A] have C2: "b ≤ n" by auto
then obtain c2 where C: "v c2 = b" "c2 ∈ X"
using clock_numbering(2) not0 unfolding v'_def by meson
then have "v' b = c2" using clock_numbering C2 not0 unfolding v'_def by fastforce
with C C2 have "∃ c ∈ X. v c = b ∧ v' b = c" "b ≤ n" by auto
} note clock_dest_2 = this
have clock_dest:
"⋀ a b. (a,b) ∈ set (arcs i i ys) ⟹ a > 0 ⟹ b > 0 ⟹
∃ c1 ∈ X. ∃ c2 ∈ X. v c1 = a ∧ v c2 = b ∧ v' a = c1 ∧ v' b = c2 &&& a ≤ n &&& b ≤ n"
using clock_dest_1 clock_dest_2 by (auto) presburger

{ fix a assume A: "(a,0) ∈ set (arcs i i ys)"
assume not0: "a > 0"
assume bounded: "M⇩R a 0 ≠ ∞"
assume lt: "M a 0 < M⇩R a 0"
from clock_dest_1[OF A not0] obtain c1 where C:
"v c1 = a" "c1 ∈ X" "v' a = c1" and C2: "a ≤ n"
by blast
from C2 not0 bounded M⇩R(5) obtain d :: int where *:
"d ≤ int (k (v' a))"
"M⇩R a 0 = Le d ∧ M⇩R 0 a = Le (- d) ∨ M⇩R a 0 = Lt d ∧ M⇩R 0 a = Lt (- d + 1)"
unfolding v'_def by auto
with C have **: "d ≤ int (k c1)" by auto
from *(2) have ?thesis
proof (standard, goal_cases)
case 1
with lt have "M a 0 < Le d" by auto
then have "M a 0 ≤ Lt d" unfolding less less_eq dbm_le_def by (fastforce elim!: dbm_lt.cases)
from dbm_lt'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 < d}"
by auto
from beta_interp.β_boundedness_lt'[OF ** C(2) this] have
"Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. u c1 < d}"
.
moreover
{ fix u assume u: "u ∈ [M⇩R]⇘v,n⇙"
with C C2 have
"dbm_entry_val u (Some c1) None (M⇩R a 0)" "dbm_entry_val u None (Some c1) (M⇩R 0 a)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
then have "u c1 = d" using 1 by auto
then have "u ∉ {u ∈ V. u c1 < d}" by auto
}
ultimately show ?thesis using M⇩R(1) M(1) by auto
next
case 2
from 2 lt have "M a 0 ≠ ∞" by auto
with dbm_entry_int[OF this] M(3) ‹a ≤ n›
obtain d' :: int where d': "M a 0 = Le d' ∨ M a 0 = Lt d'" by auto
then have "M a 0 ≤ Le (d - 1)" using lt 2
apply (auto simp: less_eq dbm_le_def less)
apply (cases rule: dbm_lt.cases)
apply auto
apply rule
apply (cases rule: dbm_lt.cases)
by auto
with lt have "M a 0 ≤ Le (d - 1)" by auto
from dbm_le'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 ≤ d - 1}"
by auto
from beta_interp.β_boundedness_le'[OF _ C(2) this] ** have
"Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. u c1 ≤ d - 1}"
by auto
moreover
{ fix u assume u: "u ∈ [M⇩R]⇘v,n⇙"
with C C2 have
"dbm_entry_val u None (Some c1) (M⇩R 0 a)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
then have "u c1 > d - 1" using 2 by auto
then have "u ∉ {u ∈ V. u c1 ≤ d - 1}" by auto
}
ultimately show ?thesis using M⇩R(1) M(1) by auto
qed
} note bounded_zero_1 = this

{ fix a assume A: "(0,a) ∈ set (arcs i i ys)"
assume not0: "a > 0"
assume bounded: "M⇩R a 0 ≠ ∞"
assume lt: "M 0 a < M⇩R 0 a"
from clock_dest_2[OF A not0] obtain c1 where C:
"v c1 = a" "c1 ∈ X" "v' a = c1" and C2: "a ≤ n"
by blast
from C2 not0 bounded M⇩R(5) obtain d :: int where *:
"d ≤ int (k (v' a))"
"M⇩R a 0 = Le d ∧ M⇩R 0 a = Le (- d) ∨ M⇩R a 0 = Lt d ∧ M⇩R 0 a = Lt (- d + 1)"
unfolding v'_def by auto
with C have **: "- int (k c1) ≤ - d" by auto
from *(2) have ?thesis
proof (standard, goal_cases)
case 1
with lt have "M 0 a < Le (-d)" by auto
then have "M 0 a ≤ Lt (-d)" unfolding less less_eq dbm_le_def by (fastforce elim!: dbm_lt.cases)
from dbm_lt'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. d < u c1}"
by auto
from beta_interp.β_boundedness_gt'[OF _ C(2) this] ** have
"Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. - u c1 < -d}"
by auto
moreover
{ fix u assume u: "u ∈ [M⇩R]⇘v,n⇙"
with C C2 have
"dbm_entry_val u (Some c1) None (M⇩R a 0)" "dbm_entry_val u None (Some c1) (M⇩R 0 a)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with 1 have "u ∉ {u ∈ V. - u c1 < -d}" by auto
}
ultimately show ?thesis using M⇩R(1) M(1) by auto
next
case 2
from 2 lt have "M 0 a ≠ ∞" by auto
with dbm_entry_int[OF this] M(3) ‹a ≤ n›
obtain d' :: int where d': "M 0 a = Le d' ∨ M 0 a = Lt d'" by auto
then have "M 0 a ≤ Le (-d)" using lt 2
apply (auto simp: less_eq dbm_le_def less)
apply (cases rule: dbm_lt.cases)
apply auto
apply rule
apply (metis get_const.simps(2) 2 of_int_less_iff of_int_minus zless_add1_eq)
apply (cases rule: dbm_lt.cases)
apply auto
apply (rule dbm_lt.intros(5))
from dbm_le'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. d ≤ u c1}"
by auto
from beta_interp.β_boundedness_ge'[OF _ C(2) this] ** have
"Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. - u c1 ≤ -d}"
by auto
moreover
{ fix u assume u: "u ∈ [M⇩R]⇘v,n⇙"
with C C2 have
"dbm_entry_val u (Some c1) None (M⇩R a 0)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with 2 have "u ∉ {u ∈ V. - u c1 ≤ -d}" by auto
}
ultimately show ?thesis using M⇩R(1) M(1) by auto
qed
} note bounded_zero_2 = this

{ fix a b c c1 c2 assume A: "(a,b) ∈ set (arcs i i ys)"
assume not0: "a > 0" "b > 0"
assume lt: "M a b = Lt c"
assume neg: "M a b + M⇩R b a < 𝟭"
assume C: "v c1 = a" "v c2 = b" "c1 ∈ X" "c2 ∈ X" and C2: "a ≤ n" "b ≤ n"
assume valid: "-k c2 ≤ -get_const (M⇩R b a)" "-get_const (M⇩R b a) ≤ k c1"
from neg have "M⇩R b a ≠ ∞" by auto
then obtain d where *: "M⇩R b a = Le d ∨ M⇩R b a = Lt d" by (cases "M⇩R b a", auto)+
with M⇩R(7) ‹_ _ _ ≠ ∞› have "d ∈ ℤ" by fastforce
with * obtain d :: int where *: "M⇩R b a = Le d ∨ M⇩R b a = Lt d" using Ints_cases by auto
with valid have valid: "- k c2 ≤ -d" "-d ≤ k c1" by auto
from * neg lt have "M a b ≤ Lt (-d)" unfolding less_eq dbm_le_def mult neutral less
by (auto elim!: dbm_lt.cases)
from dbm_lt'[OF assms(2)[folded M(1)] this C2 C(1,2) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 - u c2 < - d}"
.
from beta_interp.β_boundedness_diag_lt'[OF valid C(3,4) this] have
"Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. u c1 - u c2 < -d}"
.
moreover
{ fix u assume u: "u ∈ [M⇩R]⇘v,n⇙"
with C C2 have
"dbm_entry_val u (Some c2) (Some c1) (M⇩R b a)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with * have "u ∉ {u ∈ V. u c1 - u c2 < -d}" by auto
}
ultimately have ?thesis using M⇩R(1) M(1) by auto
} note neg_sum_lt = this

{ fix a b assume A: "(a,b) ∈ set (arcs i i ys)"
assume not0: "a > 0" "b > 0"
assume neg: "M a b + M⇩R b a < 𝟭"
from clock_dest[OF A not0] obtain c1 c2 where
C: "v c1 = a" "v c2 = b" "c1 ∈ X" "c2 ∈ X" and C2: "a ≤ n" "b ≤ n"
by blast
then have C3: "v' a = c1" "v' b = c2" unfolding v'_def using clock_numbering(1) by auto
from neg have inf: "M a b ≠ ∞" "M⇩R b a ≠ ∞" by auto
from M⇩R(8) inf not0 C(3,4) C2 C3 obtain d :: int where d:
"M⇩R b a = Le d ∨ M⇩R b a = Lt d" "- int (k c1) ≤ d" "d ≤ int (k c2)"
unfolding v'_def by auto
from inf obtain c where c: "M a b = Le c ∨ M a b = Lt c" by (cases "M a b") auto
{ assume **: "M a b ≤ Lt (-d)"
from dbm_lt'[OF assms(2)[folded M(1)] this C2 C(1,2) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 - u c2 < (- d)}"
.
from beta_interp.β_boundedness_diag_lt'[OF _ _ C(3,4) this] d have
"Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. u c1 - u c2 < -d}"
by auto
moreover
{ fix u assume u: "u ∈ [M⇩R]⇘v,n⇙"
with C C2 have
"dbm_entry_val u (Some c2) (Some c1) (M⇩R b a)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with d have "u ∉ {u ∈ V. u c1 - u c2 < -d}" by auto
}
ultimately have ?thesis using M⇩R(1) M(1) by auto
} note aux = this
from c have ?thesis
proof (standard, goal_cases)
case 2
with neg d have "M a b ≤ Lt (-d)" unfolding less_eq dbm_le_def mult neutral less
by (auto elim!: dbm_lt.cases)
with aux show ?thesis .
next
case 1
note A = this
from d(1) show ?thesis
proof (standard, goal_cases)
case 1
with A neg d have "M a b ≤ Lt (-d)" unfolding less_eq dbm_le_def mult neutral less
by (auto elim!: dbm_lt.cases)
with aux show ?thesis .
next
case 2
with A neg d have "M a b ≤ Le (-d)" unfolding less_eq dbm_le_def mult neutral less
by (auto elim!: dbm_lt.cases)
from dbm_le'[OF assms(2)[folded M(1)] this C2 C(1,2) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 - u c2 ≤ - d}"
.
from beta_interp.β_boundedness_diag_le'[OF _ _ C(3,4) this] d have
"Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. u c1 - u c2 ≤ -d}"
by auto
moreover
{ fix u assume u: "u ∈ [M⇩R]⇘v,n⇙"
with C C2 have
"dbm_entry_val u (Some c2) (Some c1) (M⇩R b a)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with A 2 have "u ∉ {u ∈ V. u c1 - u c2 ≤ -d}" by auto
}
ultimately show ?thesis using M⇩R(1) M(1) by auto
qed
qed
} note neg_sum_1 = this

{ fix a b assume A: "(a,0) ∈ set (arcs i i ys)"
assume not0: "a > 0"
assume neg: "M a 0 + M⇩R 0 a < 𝟭"
from clock_dest_1[OF A not0] obtain c1 where C: "v c1 = a" "c1 ∈ X" and C2: "a ≤ n" by blast
with clock_numbering(1) have C3: "v' a = c1" unfolding v'_def by auto
from neg have inf: "M a 0 ≠ ∞" "M⇩R 0 a ≠ ∞" by auto
from M⇩R(6) not0 C2 C3 obtain d :: int where d:
"M⇩R</```