Theory Approx_Beta
theory Approx_Beta
imports DBM_Zone_Semantics Regions_Beta Closure
begin
no_notation infinity (‹∞›)
chapter ‹Correctness of ‹β›-approximation from ‹α›-regions›
text ‹Merging the locales for the two types of regions›
locale Regions_defs =
Alpha_defs X for X :: "'c set"+
fixes v :: "'c ⇒ nat" and n :: nat
begin
abbreviation vabstr :: "('c, t) zone ⇒ _ ⇒ _" where
"vabstr S M ≡ S = [M]⇘v,n⇙ ∧ (∀ i≤n. ∀ j≤n. M i j ≠ ∞ ⟶ get_const (M i j) ∈ ℤ)"
definition "V' ≡ {Z. Z ⊆ V ∧ (∃ M. vabstr Z M)}"
end
locale Regions_global =
Regions_defs X v n for X :: "'c set" and v n +
fixes k :: "'c ⇒ 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}"
sublocale alpha_interp:
AlphaClosure_global X k ℛ by (unfold_locales) (auto simp: finite ℛ_def V_def)
sublocale beta_interp: Beta_Regions' X k v n not_in_X
rewrites "beta_interp.V = V"
using finite non_empty clock_numbering not_in_X unfolding V_def
by - ((subst Beta_Regions.V_def)?, unfold_locales; (assumption | rule HOL.refl))+
abbreviation ℛ⇩β where "ℛ⇩β ≡ beta_interp.ℛ"
lemmas ℛ⇩β_def = beta_interp.ℛ_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 (real (intv_const (I x) + 1))
else if isConst (I x) then Le (real (intv_const (I x)))
else ∞"
define g where "g ≡
λ x. if isIntv (I x) then Lt (- real (intv_const (I x)))
else if isConst (I x) then Le (- real (intv_const (I x)))
else Lt (- real (k x))"
define h where "h ≡
λ x y. if isIntv (I x) ∧ isIntv (I y) then
if (y, x) ∈ r ∧ (x, y) ∉ r then Lt (real_of_int (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 ∞"
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: add)
apply (rename_tac a' b' x xs)
apply (case_tac "M a' x")
by auto
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: add)+
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 add)
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 = 0)"
proof -
let ?M = "λi j. if i = j then 0 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 = 0" by auto
ultimately show ?thesis by (auto intro: that)
qed
lemma dbm_entry_int:
"(x :: t DBMEntry) ≠ ∞ ⟹ get_const x ∈ ℤ ⟹ ∃ d :: int. x = Le d ∨ x = Lt d"
apply (cases x) using Ints_cases by auto
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"
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 = 0)"
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 ‹cyc_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 < 0" 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 < 0"
"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 < 0" 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 < 0" 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 < 0" by auto
then have "M i i < 0 ∨ M⇩R i i < 0" 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, unfolded ℛ⇩β_def] 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))
by (simp add: int_lt_Suc_le)
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 < 0"
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 add 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 < 0"
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 add 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 add 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 add 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 < 0"
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 0 a = Le d ∨ M⇩R 0 a = Lt d" "- int (k c1) ≤ d" "d ≤ 0"
unfolding v'_def by auto
from inf obtain c where c: "M a 0 = Le c ∨ M a 0 = Lt c" by (cases "M a 0") auto
{ assume "M a 0 ≤ Lt (-d)"
from dbm_lt'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 < - d}"
.
from beta_interp.β_boundedness_lt'[OF _ C(2) this] d 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 None (Some c1) (M⇩R 0 a)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with d have "u ∉ {u ∈ V. u c1 < -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 0 ≤ Lt (-d)" unfolding less_eq dbm_le_def add 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 0 ≤ Lt (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
with aux show ?thesis .
next
case 2
with A neg d have "M a 0 ≤ Le (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
from dbm_le'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 ≤ - d}"
.
from beta_interp.β_boundedness_le'[OF _ C(2) this] d 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 None (Some c1) (M⇩R 0 a)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with A 2 have "u ∉ {u ∈ V. u c1 ≤ -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: "(0,b) ∈ set (arcs i i ys)"
assume not0: "b > 0"
assume neg: "M 0 b + M⇩R b 0 < 0"
from clock_dest_2[OF A not0] obtain c2 where
C: "v c2 = b" "c2 ∈ X" and C2: "b ≤ n"
by blast
with clock_numbering(1) have C3: "v' b = c2" unfolding v'_def by auto
from neg have "M 0 b ≠ ∞" "M⇩R b 0 ≠ ∞" by auto
with M⇩R(5) not0 C2 C3 obtain d :: int where d:
"M⇩R b 0 = Le d ∨ M⇩R b 0 = Lt d" "d ≤ k c2"
unfolding v'_def by fastforce
from ‹M 0 b ≠ ∞› obtain c where c: "M 0 b = Le c ∨ M 0 b = Lt c" by (cases "M 0 b") auto
{ assume "M 0 b ≤ Lt (-d)"
from dbm_lt'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c2 > d}"
by simp
from beta_interp.β_boundedness_gt'[OF _ C(2) this] d have
"Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. - 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) None (M⇩R b 0)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with d have "u ∉ {u ∈ V. - 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 0 b ≤ Lt (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
with aux show ?thesis .
next
case A: 1
from d(1) show ?thesis
proof (standard, goal_cases)
case 1
with A neg have "M 0 b ≤ Lt (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
with aux show ?thesis .
next
case 2
with A neg c have "M 0 b ≤ Le (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
from dbm_le'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c2 ≥ d}"
by simp
from beta_interp.β_boundedness_ge'[OF _ C(2) this] d(2) have
"Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. - 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) None (M⇩R b 0)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with A 2 have "u ∉ {u ∈ V. - 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,b) ∈ set (arcs i i ys)"
assume not0: "b > 0" "a > 0"
assume neg: "M⇩R a b + M b a < 0"
from clock_dest[OF A not0(2,1)] 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 b a ≠ ∞" "M⇩R a b ≠ ∞" by auto
with M⇩R(8) not0 C(3,4) C2 C3 obtain d :: int where d:
"M⇩R a b = Le d ∨ M⇩R a b = Lt d" "d ≥ -int (k c2)" "d ≤ int (k c1)"
unfolding v'_def by blast
from inf obtain c where c: "M b a = Le c ∨ M b a = Lt c" by (cases "M b a") auto
{ assume "M b a ≤ Lt (-d)"
from dbm_lt'[OF assms(2)[folded M(1)] this C2(2,1) C(2,1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c2 - u c1 < - d}"
.
from beta_interp.β_boundedness_diag_lt'[OF _ _ C(4,3) this] d
have "Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. u c2 - 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) (Some c2) (M⇩R a b)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with d have "u ∉ {u ∈ V. u c2 - u c1 < -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 b a ≤ Lt (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
with aux show ?thesis .
next
case A: 1
from d(1) show ?thesis
proof (standard, goal_cases)
case 1
with A neg d have "M b a ≤ Lt (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
with aux show ?thesis .
next
case 2
with A neg d have "M b a ≤ Le (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
from dbm_le'[OF assms(2)[folded M(1)] this C2(2,1) C(2,1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c2 - u c1 ≤ - d}"
.
from beta_interp.β_boundedness_diag_le'[OF _ _ C(4,3) this] d
have "Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. u c2 - 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) (Some c2) (M⇩R a b)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with A 2 have "u ∉ {u ∈ V. u c2 - u c1 ≤ -d}" by auto
}
ultimately show ?thesis using M⇩R(1) M(1) by auto
qed
qed
} note neg_sum_2 = this
{ fix a b assume A: "(a,0) ∈ set (arcs i i ys)"
assume not0: "a > 0"
assume neg: "M⇩R a 0 + M 0 a < 0"
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 0 a ≠ ∞" "M⇩R a 0 ≠ ∞" by auto
with M⇩R(5) not0 C2 C3 obtain d :: int where d:
"M⇩R a 0 = Le d ∨ M⇩R a 0 = Lt d" "d ≤ int (k c1)" "d ≥ 0"
unfolding v'_def by auto
from inf obtain c where c: "M 0 a = Le c ∨ M 0 a = Lt c" by (cases "M 0 a") auto
{ assume "M 0 a ≤ Lt (-d)"
from dbm_lt'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 > d}"
by simp
from beta_interp.β_boundedness_gt'[OF _ C(2) this] d 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 d have "u ∉ {u ∈ V. u c1 > 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 0 a ≤ Lt (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
with aux show ?thesis .
next
case A: 1
from d(1) show ?thesis
proof (standard, goal_cases)
case 1
with A neg d have "M 0 a ≤ Lt (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
with aux show ?thesis .
next
case 2
with A neg d have "M 0 a ≤ Le (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
from dbm_le'3[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c1 ≥ d}"
by simp
from beta_interp.β_boundedness_ge'[OF _ C(2) this] d 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 A 2 have "u ∉ {u ∈ V. u c1 ≥ d}" by auto
}
ultimately show ?thesis using M⇩R(1) M(1) by auto
qed
qed
} note neg_sum_2' = this
{ fix a b assume A: "(0,b) ∈ set (arcs i i ys)"
assume not0: "b > 0"
assume neg: "M⇩R 0 b + M b 0 < 0"
from clock_dest_2[OF A not0] obtain c2 where
C: "v c2 = b" "c2 ∈ X" and C2: "b ≤ n"
by blast
with clock_numbering(1) have C3: "v' b = c2" unfolding v'_def by auto
from neg have "M b 0 ≠ ∞" "M⇩R 0 b ≠ ∞" by auto
with M⇩R(6) not0 C2 C3 obtain d :: int where d:
"M⇩R 0 b = Le d ∨ M⇩R 0 b = Lt d" "-d ≤ k c2"
unfolding v'_def by fastforce
from ‹M b 0 ≠ ∞› obtain c where c: "M b 0 = Le c ∨ M b 0 = Lt c" by (cases "M b 0") auto
{ assume "M b 0 ≤ Lt (-d)"
from dbm_lt'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c2 < - d}"
by simp
from beta_interp.β_boundedness_lt'[OF _ C(2) this] d have
"Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. u c2 < -d}"
by auto
moreover
{ fix u assume u: "u ∈ [M⇩R]⇘v,n⇙"
with C C2 have
"dbm_entry_val u None (Some c2) (M⇩R 0 b)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with d have "u ∉ {u ∈ V. 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 b 0 ≤ Lt (-d)" unfolding less_eq dbm_le_def add 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 have "M b 0 ≤ Lt (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
with aux show ?thesis .
next
case 2
with A neg c have "M b 0 ≤ Le (-d)" unfolding less_eq dbm_le_def add neutral less
by (auto elim!: dbm_lt.cases)
from dbm_le'2[OF assms(2)[folded M(1)] this C2 C(1) not0] have
"[M]⇘v,n⇙ ⊆ {u ∈ V. u c2 ≤ - d}"
by simp
from beta_interp.β_boundedness_le'[OF _ C(2) this] d(2) have
"Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. u c2 ≤ -d}"
by auto
moreover
{ fix u assume u: "u ∈ [M⇩R]⇘v,n⇙"
with C C2 have
"dbm_entry_val u None (Some c2) (M⇩R 0 b)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with A 2 have "u ∉ {u ∈ V. u c2 ≤ -d}" by auto
}
ultimately show ?thesis using M⇩R(1) M(1) by auto
qed
qed
} note neg_sum_2'' = this
{ fix a b assume A: "(a,b) ∈ set (arcs i i ys)"
assume not0: "a > 0" "b > 0"
assume bounded: "M⇩R a 0 ≠ ∞" "M⇩R b 0 ≠ ∞"
assume lt: "M a b < M⇩R a b"
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
from C C2 clock_numbering(1,3) have C3: "v' b = c2" "v' a = c1" unfolding v'_def by blast+
with C C2 not0 bounded M⇩R(4) obtain d :: int where *:
"- int (k c2) ≤ d ∧ d ≤ int (k c1) ∧ M⇩R a b = Le d ∧ M⇩R b a = Le (- d)
∨ - int (k c2) ≤ d - 1 ∧ d ≤ int (k c1) ∧ M⇩R a b = Lt d ∧ M⇩R b a = Lt (- d + 1)"
unfolding v'_def by force
from * have ?thesis
proof (standard, goal_cases)
case 1
with lt have "M a b < Le d" by auto
then have "M a b ≤ Lt d" unfolding less less_eq dbm_le_def by (fastforce 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 _ _ C(3,4) this] 1
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 c1) (Some c2) (M⇩R a b)" "dbm_entry_val u (Some c2) (Some c1) (M⇩R b a)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with 1 have "u ∉ {u ∈ V. u c1 - u c2 < d}" by auto
}
ultimately show ?thesis using M⇩R(1) M(1) by auto
next
case 2
with lt have "M a b ≠ ∞" by auto
with dbm_entry_int[OF this] M(3) ‹a ≤ n› ‹b ≤ n›
obtain d' :: int where d': "M a b = Le d' ∨ M a b = Lt d'" by auto
then have "M a b ≤ 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 dbm_lt.intros)
apply (cases rule: dbm_lt.cases)
by auto
with lt have "M a b ≤ Le (d - 1)" by auto
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 - 1}"
.
from beta_interp.β_boundedness_diag_le'[OF _ _ C(3,4) this] 2
have "Approx⇩β ([M]⇘v,n⇙) ⊆ {u ∈ V. u c1 - u c2 ≤ d - 1}" 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 2 have "u ∉ {u ∈ V. u c1 - u c2 ≤ d - 1}" by auto
}
ultimately show ?thesis using M⇩R(1) M(1) by auto
qed
} note bounded = this
{ assume not_bounded: "∀ (a,b) ∈ set (arcs i i ys). M a b < M⇩R a b ⟶ M⇩R a 0 = ∞ ∨ M⇩R b 0 = ∞"
have "∃ y z zs. set zs ∪ {0, y, z} = set (i # ys) ∧ len ?M 0 0 (y # z # zs) < Le 0 ∧
(∀ (a,b) ∈ set (arcs 0 0 (y # z # zs)). M a b < M⇩R a b ⟶ a = y ∧ b = z)
∧ M y z < M⇩R y z ∧ distinct (0 # y # z # zs) ∨ ?thesis"
proof (cases ys)
case Nil
show ?thesis
proof (cases "M i i < M⇩R i i")
case True
then have "?M i i = M i i" by simp
with Nil ys(1) xs(3) have *: "M i i < 0" by simp
with neg_cycle_empty[OF cn_weak _ ‹i ≤ n›, of "[]" M] have "[M]⇘v,n⇙ = {}" by auto
with ‹Z ≠ {}› M(1) show ?thesis by auto
next
case False
then have "?M i i = M⇩R i i" by (simp add: min_absorb2)
with Nil ys(1) xs(3) have "M⇩R i i < 0" by simp
with neg_cycle_empty[OF cn_weak _ ‹i ≤ n›, of "[]" M⇩R] have "[M⇩R]⇘v,n⇙ = {}" by auto
with ‹R ≠ {}› M⇩R(1) show ?thesis by auto
qed
next
case (Cons w ws)
note ws = this
show ?thesis
proof (cases ws)
case Nil
with ws ys xs(3) have *:
"?M i w + ?M w i < 0" "?M w i = M w i ⟶ ?M i w ≠ M i w" "(i, w) ∈ set (arcs i i ys)"
by auto
have "R ∩ Approx⇩β Z = {}"
proof (cases "?M w i = M w i")
case True
with *(2) have "?M i w = M⇩R i w" unfolding min_def by auto
with *(1) True have neg: "M⇩R i w + M w i < 0" by auto
show ?thesis
proof (cases "i = 0")
case True
show ?thesis
proof (cases "w = 0")
case True with 0 ‹i = 0› *(3) show ?thesis by auto
next
case False with ‹i = 0› neg_sum_2'' *(3) neg show ?thesis by blast
qed
next
case False
show ?thesis
proof (cases "w = 0")
case True with ‹i ≠ 0› neg_sum_2' *(3) neg show ?thesis by blast
next
case False with ‹i ≠ 0› neg_sum_2 *(3) neg show ?thesis by blast
qed
qed
next
case False
have "M⇩R w i < M w i"
proof (rule ccontr, goal_cases)
case 1
then have "M⇩R w i ≥ M w i" by auto
with False show False unfolding min_def by auto
qed
with one_M ws Nil have "M i w < M⇩R i w" by auto
then have "?M i w = M i w" unfolding min_def by auto
moreover from False *(2) have "?M w i = M⇩R w i" unfolding min_def by auto
ultimately have neg: "M i w + M⇩R w i < 0" using *(1) by auto
show ?thesis
proof (cases "i = 0")
case True
show ?thesis
proof (cases "w = 0")
case True with 0 ‹i = 0› *(3) show ?thesis by auto
next
case False with ‹i = 0› neg_sum_1'' *(3) neg show ?thesis by blast
qed
next
case False
show ?thesis
proof (cases "w = 0")
case True with ‹i ≠ 0› neg_sum_1' *(3) neg show ?thesis by blast
next
case False with ‹i ≠ 0› neg_sum_1 *(3) neg show ?thesis by blast
qed
qed
qed
then show ?thesis by simp
next
case zs: (Cons z zs)
from one_M obtain a b where *:
"(a,b) ∈ set (arcs i i ys)" "M a b < M⇩R a b"
by fastforce
from cycle_rotate_3'[OF _ *(1) ys(3)] ws cycle_closes obtain ws' where ws':
"len ?M i i ys = len ?M a a (b # ws')" "set (a # b # ws') = set (i # ys)"
"1 + length ws' = length ys" "set (arcs i i ys) = set (arcs a a (b # ws'))"
and successive: "successive (λ(a, b). ?M a b = M a b) (arcs a a (b # ws') @ [(a, b)])"
by blast
from successive have successive_arcs:
"successive (λ(a, b). ?M a b = M a b) (arcs a b (b # ws' @ [a]))"
using arcs_decomp_tail by auto
from ws'(4) one_M_R *(2) obtain c d where **:
"(c,d) ∈ set (arcs a a (b # ws'))" "M c d > M⇩R c d" "(a,b) ≠ (c,d)"
by fastforce
from card_distinct[of "a # b # ws'"] distinct_card[of "i # ys"] ws'(2,3) distinct
have distinct: "distinct (a # b # ws')" by simp
from ws zs ws'(3) have "ws' ≠ []" by auto
then obtain z zs where z: "ws' = zs @ [z]" by (metis append_butlast_last_id)
then have "b # ws' = (b # zs) @ [z]" by simp
with len_decomp[OF this, of ?M a a] arcs_decomp_tail have rotated:
"len ?M a a (b # ws') = len ?M z z (a # b # zs)"
"set (arcs a a (b # ws')) = set (arcs z z (a # b # zs))"
by (auto simp add: comm)
from ys(1) xs(3) ws'(1) have "len ?M a a (b # ws') < 0" by auto
from ws'(2) ys(2) ‹i ≤ n› z have n_bounds: "a ≤ n" "b ≤ n" "set ws' ⊆ {0..n}" "z ≤ n" by auto
from * have a_b: "?M a b = M a b" by simp
from successive successive_split[of _ "arcs a z (b # zs)" "[(z,a), (a,b)]"]
have first: "successive (λ(a, b). ?M a b = M a b) (arcs a z (b # zs))" and
last_two: "successive (λ(a, b). ?M a b = M a b) [(z, a), (a, b)]"
using arcs_decomp_tail z by auto
from * not_bounded have not_bounded': "M⇩R a 0 = ∞ ∨ M⇩R b 0 = ∞" by auto
from this(1) have "z = 0"
proof
assume inf: "M⇩R b 0 = ∞"
from a_b successive obtain z where z: "(b,z) ∈ set (arcs b a ws')" "?M b z ≠ M b z"
by (cases ws') auto
then have "?M b z = M⇩R b z" by (meson min_def)
from arcs_distinct2[OF _ _ _ _ z(1)] distinct have "b ≠ z" by auto
from z n_bounds have "z ≤ n"
apply (induction ws' arbitrary: b)
apply auto[]
apply (rename_tac ws' b)
apply (case_tac ws')
apply auto
done
have "M⇩R b z = ∞"
proof (cases "z = 0")
case True
with inf show ?thesis by auto
next
case False
with inf M⇩R(2) ‹b ≠ z› ‹z ≤ n› ‹b ≤ n› show ?thesis by blast
qed
with ‹?M b z = M⇩R b z› have "len ?M b a ws' = ∞" by (auto intro: len_inf_elem[OF z(1)])
then have "∞ = len ?M a a (b # ws')" by simp
with ‹len ?M a a _ < 0› show ?thesis by auto
next
assume inf: "M⇩R a 0 = ∞"
show "z = 0"
proof (rule ccontr)
assume "z ≠ 0"
with last_two a_b have "?M z a = M⇩R z a" by (auto simp: min_def)
from distinct z have "a ≠ z" by auto
with ‹z ≠ 0› ‹a ≤ n› ‹z ≤ n› M⇩R(2) inf have "M⇩R z a = ∞" by blast
with ‹?M z a = M⇩R z a› have "len ?M z z (a # b # zs) = ∞" by (auto intro: len_inf_elem)
with ‹len ?M a a _ < 0› rotated show False by auto
qed
qed
{ fix c d assume A: "(c, d) ∈ set (arcs 0 0 (a # b # zs))" "M c d < M⇩R c d"
then have *: "?M c d = M c d" by simp
from rotated(2) A ‹z = 0› not_bounded ws'(4) have **: "M⇩R c 0 = ∞ ∨ M⇩R d 0 = ∞" by auto
{ assume inf: "M⇩R c 0 = ∞"
fix x assume x: "(x, c) ∈ set (arcs a 0 (b # zs))" "?M x c ≠ M x c"
from x(2) have "?M x c = M⇩R x c" unfolding min_def by auto
from arcs_elem[OF x(1)] z ‹z = 0› have
"x ∈ set (a # b # ws')" "c ∈ set (a # b # ws')"
by auto
with n_bounds have "x ≤ n" "c ≤ n" by auto
have "x = 0"
proof (rule ccontr)
assume "x ≠ 0"
from distinct z arcs_distinct1[OF _ _ _ _ x(1)] ‹z = 0›have "x ≠ c" by auto
with ‹x ≠ 0› ‹c ≤ n› ‹x ≤ n› M⇩R(2) inf have "M⇩R x c = ∞" by blast
with ‹?M x c = M⇩R x c› have
"len ?M a 0 (b # zs) = ∞"
by (fastforce intro: len_inf_elem[OF x(1)])
with ‹z = 0› have "len ?M z z (a # b # zs) = ∞" by auto
with ‹len ?M a a _ < 0› rotated show False by auto
qed
with arcs_distinct_dest1[OF _ x(1), of z] z distinct x ‹z = 0› have False by auto
} note c_0_inf = this
have "a = c ∧ b = d"
proof (cases "(c, d) = (0, a)")
case True
with last_two ‹z = 0› * a_b have False by auto
then show ?thesis by simp
next
case False
show ?thesis
proof (rule ccontr, goal_cases)
case 1
with False A(1) have ***: "(c, d) ∈ set (arcs b 0 zs)" by auto
from successive z ‹z = 0› have
"successive (λ(a, b). ?M a b = M a b) ([(a, b)] @ arcs b 0 zs @ [(0, a), (a, b)])"
by (simp add: arcs_decomp)
then have ****: "successive (λ(a, b). ?M a b = M a b) (arcs b 0 zs)"
using successive_split[of _ "[(a, b)]" "arcs b 0 zs @ [(0, a), (a, b)]"]
successive_split[of _ "arcs b 0 zs" "[(0, a), (a, b)]"]
by auto
from successive_predecessor[OF *** _ this] successive z
obtain x where x: "(x, c) ∈ set (arcs a 0 (b # zs))" "?M x c ≠ M x c"
proof (cases "c = b")
case False
then have "zs ≠ []" using *** by auto
from successive_predecessor[OF *** False **** _ this] * obtain x where x:
"(zs = [c] ∧ x = b ∨ (∃ys. zs = c # d # ys ∧ x = b)
∨ (∃ys. zs = ys @ [x, c] ∧ d = 0) ∨ (∃ys ws. zs = ys @ x # c # d # ws))"
"?M x c ≠ M x c"
by blast+
from this(1) have "(x, c) ∈ set (arcs a 0 (b # zs))" using arcs_decomp by auto
with x(2) show ?thesis by (auto intro: that)
next
case True
have ****: "successive (λ(a, b). ?M a b = M a b) (arcs a 0 (b # zs))"
using first ‹z = 0› arcs_decomp successive_arcs z by auto
show ?thesis
proof (cases zs)
case Nil
with **** True *** * show ?thesis by (auto intro: that)
next
case (Cons u us)
with *** True distinct z ‹z = 0› have "distinct (b # u # us @ [0])" by auto
from arcs_distinct_fix[OF this] *** True Cons have "d = u" by auto
with **** * Cons True show ?thesis by (auto intro: that)
qed
qed
show False
proof (cases "d = 0")
case True
from ** show False
proof
assume "M⇩R c 0 = ∞" from c_0_inf[OF this x] show False .
next
assume "M⇩R d 0 = ∞" with ‹d = 0› M⇩R(3) show False by auto
qed
next
case False with *** have "zs ≠ []" by auto
from successive_successor[OF ‹(c,d) ∈ set (arcs b 0 zs)› False **** _ this] *
obtain e where
"(zs = [d] ∧ e = 0 ∨ (∃ys. zs = d # e # ys) ∨ (∃ys. zs = ys @ [c, d] ∧ e = 0)
∨ (∃ys ws. zs = ys @ c # d # e # ws))" "?M d e ≠ M d e"
by blast
then have e: "(d, e) ∈ set (arcs b 0 zs)" "?M d e ≠ M d e" using arcs_decomp by auto
from ** show False
proof
assume inf: "M⇩R d 0 = ∞"
from e have "?M d e = M⇩R d e" by (meson min_def)
from arcs_distinct2[OF _ _ _ _ e(1)] z ‹z = 0› distinct have "d ≠ e" by auto
from z n_bounds have "set zs ⊆ {0..n}" by auto
with e have "e ≤ n"
apply (induction zs arbitrary: d)
apply auto
apply (case_tac zs)
apply auto
done
from n_bounds z arcs_elem(2)[OF A(1)] have "d ≤ n" by auto
have "M⇩R d e = ∞"
proof (cases "e = 0")
case True
with inf show ?thesis by auto
next
case False
with inf M⇩R(2) ‹d ≠ e› ‹e ≤ n› ‹d ≤ n› show ?thesis by blast
qed
with ‹?M d e = M⇩R d e› have "len ?M b 0 zs = ∞" by (auto intro: len_inf_elem[OF e(1)])
with ‹z = 0› rotated have "∞ = len ?M a a (b # ws')" by simp
with ‹len ?M a a _ < 0› show ?thesis by auto
next
assume "M⇩R c 0 = ∞" from c_0_inf[OF this x] show False .
qed
qed
qed
qed
}
then have "∀(c, d)∈set (arcs 0 0 (a # b # zs)). M c d < M⇩R c d ⟶ c = a ∧ d = b"
by blast
moreover from ys(1) xs(3) have "len ?M i i ys < Le 0" unfolding neutral by auto
moreover with rotated ws'(1) have "len ?M z z (a # b # zs) < Le 0" by auto
moreover from ‹z = 0› z ws'(2) have "set zs ∪ {0, a, b} = set (i # ys)" by auto
moreover from ‹z = 0› distinct z have "distinct (0 # a # b # zs)" by auto
ultimately show ?thesis using ‹z = 0› ‹M a b < M⇩R a b› by blast
qed
qed note * = this
{ assume "¬ ?thesis"
with * obtain y z zs where *:
"set zs ∪ {0, y, z} = set (i # ys)" "len ?M 0 0 (y # z # zs) < Le 0"
"∀(a, b)∈set (arcs 0 0 (y # z # zs)). M a b < M⇩R a b ⟶ a = y ∧ b = z" "M y z < M⇩R y z"
and distinct': "distinct (0 # y # z # zs)"
by blast
then have "y ≠ 0" "z ≠ 0" by auto
let ?r = "len M⇩R z 0 zs"
have "∀(a, b)∈set (arcs z 0 zs). ?M a b = M⇩R a b"
proof (safe, goal_cases)
case A: (1 a b)
have "M⇩R a b ≤ M a b"
proof (rule ccontr, goal_cases)
case 1
with *(3) A have "a = y" "b = z" by auto
with A distinct' arcs_distinct3[OF _ A, of y] show False by auto
qed
then show ?case by (simp add: min_def)
qed
then have r: "len ?M z 0 zs = ?r" by (induction zs arbitrary: z) auto
with *(2) have **: "?M 0 y + (?M y z + ?r) < Le 0" by simp
from M⇩R(1) ‹R ≠ {}› obtain u where u: "DBM_val_bounded v u M⇩R n"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
from *(1) ‹i ≤ n› ‹set ys ⊆ _› have "y ≤ n" "z ≤ n" by fastforce+
from *(1) ys(2,4) have "set zs ⊆ {0 ..n}" by auto
from ‹y ≤ n› ‹z ≤ n› clock_numbering(2) ‹y ≠ 0› ‹z ≠ 0› obtain c1 c2 where C:
"c1 ∈ X" "c2 ∈ X" "v c1 = y" "v c2 = z"
by blast+
with clock_numbering(1,3) have C2: "v' y = c1" "v' z = c2" unfolding v'_def by auto
with C have "v (v' z) = z" by auto
with DBM_val_bounded_len'1[OF u, of zs "v' z"] have "dbm_entry_val u (Some (v' z)) None ?r"
using ‹z ≤ n› clock_numbering(2) ‹set zs ⊆ _› distinct' by force
from len_inf_elem ** have tl_not_inf: "∀(a, b)∈set (arcs z 0 zs). M⇩R a b ≠ ∞" by fastforce
with M⇩R(7) len_int_dbm_closed have "get_const ?r ∈ ℤ ∧ ?r ≠ ∞" by blast
then obtain r :: int where r': "?r = Le r ∨ ?r = Lt r" using Ints_cases by (cases ?r) auto
from r' ‹dbm_entry_val _ _ _ _› C C2 have le: "u (v' z) ≤ r" by fastforce
from arcs_ex_head obtain z' where "(z, z') ∈ set (arcs z 0 zs)" by blast
then have z':
"(z, z') ∈ set (arcs 0 0 (y # z # zs))" "(z, z') ∈ set (arcs z 0 zs)"
by auto
have "M⇩R z 0 ≠ ∞"
proof (rule ccontr, goal_cases)
case 1
then have inf: "M⇩R z 0 = ∞" by auto
have "M⇩R z z' = ∞"
proof (cases "z' = 0")
case True
with 1 show ?thesis by auto
next
case False
from arcs_elem[OF z'(1)] *(1) ‹i ≤ n› ‹set ys ⊆ _› have "z' ≤ n" by fastforce
moreover from distinct' *(1) arcs_distinct1[OF _ _ _ _ z'(1)] have "z ≠ z'" by auto
ultimately show ?thesis using M⇩R(2) ‹z ≤ n› False inf by blast
qed
with tl_not_inf z'(2) show False by auto
qed
with M⇩R(5) ‹z ≠ 0› ‹z ≤ n› obtain d :: int where d:
"M⇩R z 0 = Le d ∧ M⇩R 0 z = Le (-d) ∨ M⇩R z 0 = Lt d ∧ M⇩R 0 z = Lt (-d + 1)"
"d ≤ k (v' z)" "0 ≤ d"
unfolding v'_def by auto
text ‹Needs property that len of integral dbm entries is integral and definition of ‹M_R››
from this (1) have rr: "?r ≥ M⇩R z 0"
proof (standard, goal_cases)
case A: 1
with u ‹z ≤ n› C C2 have *: "- u (v' z) ≤ -d" unfolding DBM_val_bounded_def by fastforce
from r' show ?case
proof (standard, goal_cases)
case 1
with le * A show ?case unfolding less_eq dbm_le_def by fastforce
next
case 2
with ‹dbm_entry_val _ _ _ _› C C2 have "u (v' z) < r" by fastforce
with * have "r > d" by auto
with A 2 show ?case unfolding less_eq dbm_le_def by fastforce
qed
next
case A: 2
with u ‹z ≤ n› C C2 have *: "- u (v' z) < -d + 1" unfolding DBM_val_bounded_def by fastforce
from r' show ?case
proof (standard, goal_cases)
case 1
with le * A show ?case unfolding less_eq dbm_le_def by fastforce
next
case 2
with ‹dbm_entry_val _ _ _ _› C C2 have "u (v' z) ≤ r" by fastforce
with * have "r ≥ d" by auto
with A 2 show ?case unfolding less_eq dbm_le_def by fastforce
qed
qed
with *(3) ‹y ≠ 0› have "M 0 y ≥ M⇩R 0 y" by fastforce
then have "?M 0 y = M⇩R 0 y" by (simp add: min.absorb2)
moreover from *(4) have "?M y z = M y z" unfolding min_def by auto
ultimately have **: "M⇩R 0 y + (M y z + M⇩R z 0) < Le 0"
using ** add_mono_right[OF add_mono_right[OF rr], of "M⇩R 0 y" "M y z"] by simp
from ** have not_inf: "M⇩R 0 y ≠ ∞" "M y z ≠ ∞" "M⇩R z 0 ≠ ∞" by auto
from M⇩R(6) ‹y ≠ 0› ‹y ≤ n› obtain c :: int where c:
"M⇩R 0 y = Le c ∨ M⇩R 0 y = Lt c" "- k (v' y) ≤ c" "c ≤ 0"
unfolding v'_def by auto
have ?thesis
proof (cases "M⇩R 0 y + M⇩R z 0 = Lt (c + d)")
case True
from ** have "(M⇩R 0 y + M⇩R z 0) + M y z < Le 0" using comm add.assoc by metis
with True have **: "Lt (c + d) + M y z < Le 0" by simp
then have "M y z ≤ Le (- (c + d))" unfolding less less_eq dbm_le_def add
by (cases "M y z") (fastforce elim!: dbm_lt.cases)+
from dbm_le'[OF assms(2)[folded M(1)] this ‹y ≤ n› ‹z ≤ n› C(3,4)] ‹y ≠ 0› ‹z ≠ 0› M
have subs: "Z ⊆ {u ∈ V. u c1 - u c2 ≤ - (c + d)}" by blast
with c d have "- k (v' z) ≤ - (c + d)" "- (c + d) ≤ k (v' y)" by auto
with beta_interp.β_boundedness_diag_le'[OF _ _ C(1,2) subs] C2 have
"Approx⇩β Z ⊆ {u ∈ V. u c1 - u c2 ≤ - (c + d)}"
by auto
moreover
{ fix u assume u: "u ∈ R"
with C ‹y ≤ n› ‹z ≤ n› M⇩R(1) have
"dbm_entry_val u (Some c2) None (M⇩R z 0)" "dbm_entry_val u None (Some c1) (M⇩R 0 y)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with True c d(1) have "u ∉ {u ∈ V. u c1 - u c2 ≤ - (c + d)}" unfolding add by auto
}
ultimately show ?thesis by blast
next
case False
with c d have "M⇩R 0 y + M⇩R z 0 = Le (c + d)" unfolding add by fastforce
moreover from ** have "(M⇩R 0 y + M⇩R z 0) + M y z < Le 0" using comm add.assoc by metis
ultimately have **: "Le (c + d) + M y z < Le 0" by simp
then have "M y z ≤ Lt (- (c + d))" unfolding less less_eq dbm_le_def add
by (cases "M y z") (fastforce elim!: dbm_lt.cases)+
from dbm_lt'[OF assms(2)[folded M(1)] this ‹y ≤ n› ‹z ≤ n› C(3,4)] ‹y ≠ 0› ‹z ≠ 0› M
have subs: "Z ⊆ {u ∈ V. u c1 - u c2 < - (c + d)}" by auto
from c d(2-) C2 have "- k c2 ≤ - (c + d)" "- (c + d) ≤ k c1" by auto
from beta_interp.β_boundedness_diag_lt'[OF this C(1,2) subs] have
"Approx⇩β Z ⊆ {u ∈ V. u c1 - u c2 < - (c + d)}"
.
moreover
{ fix u assume u: "u ∈ R"
with C ‹y ≤ n› ‹z ≤ n› M⇩R(1) have
"dbm_entry_val u (Some c2) None (M⇩R z 0)" "dbm_entry_val u None (Some c1) (M⇩R 0 y)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with c d(1) have "u ∉ {u ∈ V. u c1 - u c2 < - (c + d)}" by auto
}
ultimately show ?thesis by auto
qed
} then have ?thesis by auto
}
with bounded 0 bounded_zero_1 bounded_zero_2 show ?thesis by blast
qed
qed
qed
section ‹Nice Corollaries of Bouyer's Theorem›
lemma ℛ_V: "⋃ ℛ = V" unfolding V_def ℛ_def using region_cover[of X _ k] by auto
lemma regions_beta_V: "R ∈ ℛ⇩β ⟹ R ⊆ V" unfolding V_def ℛ⇩β_def by auto
lemma apx_V: "Z ⊆ V ⟹ Approx⇩β Z ⊆ V"
proof (goal_cases)
case 1
from beta_interp.apx_in[OF 1] obtain U where "Approx⇩β Z = ⋃U" "U ⊆ ℛ⇩β" by auto
with regions_beta_V show ?thesis by auto
qed
corollary approx_β_closure_α:
assumes "Z ⊆ V" "vabstr Z M"
shows "Approx⇩β Z ⊆ Closure⇩α Z"
proof -
note T = region_zone_intersect_empty_approx_correct[OF _ assms(1) _ assms(2-)]
have "- ⋃{R ∈ ℛ. R ∩ Z ≠ {}} = ⋃{R ∈ ℛ. R ∩ Z = {}} ∪ - V"
proof (safe, goal_cases)
case 1 with ℛ_V show False by fast
next
case 2 then show ?case using alpha_interp.valid_regions_distinct_spec by fastforce
next
case 3 then show ?case using ℛ_V unfolding V_def by blast
qed
with T apx_V[OF assms(1)] have "Approx⇩β Z ∩ - ⋃{R ∈ ℛ. R ∩ Z ≠ {}} = {}" by auto
then show ?thesis unfolding alpha_interp.cla_def by blast
qed
corollary approx_β_closure_α': "Z ∈ V' ⟹ Approx⇩β Z ⊆ Closure⇩α Z"
using approx_β_closure_α unfolding V'_def by auto
text ‹We could prove this more directly too (without using ‹Closure⇩α Z›), obviously›
lemma apx_empty_iff:
assumes "Z ⊆ V" "vabstr Z M"
shows "Z = {} ⟷ Approx⇩β Z = {}"
using alpha_interp.cla_empty_iff[OF assms(1)] approx_β_closure_α[OF assms] beta_interp.apx_subset
by auto
lemma apx_empty_iff':
assumes "Z ∈ V'" shows "Z = {} ⟷ Approx⇩β Z = {}"
using apx_empty_iff assms unfolding V'_def by force
lemma apx_V':
assumes "Z ⊆ V" shows "Approx⇩β Z ∈ V'"
proof (cases "Z = {}")
case True
with beta_interp.apx_empty beta_interp.empty_zone_dbm show ?thesis unfolding V'_def neutral by auto
next
case False
then have non_empty: "Approx⇩β Z ≠ {}" using beta_interp.apx_subset by blast
from beta_interp.apx_in[OF assms] obtain U M where *:
"Approx⇩β Z = ⋃U" "U ⊆ ℛ⇩β" "Z ⊆ Approx⇩β Z" "vabstr (Approx⇩β Z) M"
by blast
moreover from * beta_interp.ℛ_union have "⋃ U ⊆ V" by blast
ultimately show ?thesis using *(1,4) unfolding V'_def by auto
qed
end
lemma valid_abstraction_pairsD:
"∀(x, m)∈Timed_Automata.clkp_set A. x ∈ X ∧ m ∈ ℕ" if "valid_abstraction A X k"
using that
apply cases
unfolding clkp_set_def Timed_Automata.clkp_set_def
unfolding collect_clki_def Timed_Automata.collect_clki_def
unfolding collect_clkt_def Timed_Automata.collect_clkt_def
by blast
section ‹A New Zone Semantics Abstracting with ‹Approx⇩β››
locale Regions =
Regions_defs X v n for X and v :: "'c ⇒ nat" and n :: nat +
fixes k :: "'s ⇒ 'c ⇒ 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: "ℛ l ≡ {Regions.region X I r | I r. Regions.valid_region X (k l) I r}"
definition ℛ⇩β_def:
"ℛ⇩β l ≡ {Regions_Beta.region X I J r | I J r. Regions_Beta.valid_region X (k l) I J r}"
sublocale
AlphaClosure X k ℛ by (unfold_locales) (auto simp: finite ℛ_def V_def)
abbreviation "Approx⇩β l Z ≡ Beta_Regions'.Approx⇩β X (k l) v n not_in_X Z"
subsection ‹Single Step›
inductive step_z_beta ::
"('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 'a action ⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇘β(_)⇙ ⟨_, _⟩› [61,61,61,61] 61)
where
step_beta: "A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l', Approx⇩β l' Z'⟩"
inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ ↝⇘β(a)⇙ ⟨l',u'⟩"
declare step_z_beta.intros[intro]
context
fixes l' :: 's
begin
interpretation regions: Regions_global _ _ _ "k l'"
by standard (rule finite clock_numbering not_in_X non_empty)+
lemma step_z_V':
assumes "A ⊢ ⟨l,Z⟩ ↝⇘a⇙ ⟨l',Z'⟩" "valid_abstraction A X k" "∀c∈clk_set A. v c ≤ n" "Z ∈ V'"
shows "Z' ∈ V'"
proof -
from assms(3) clock_numbering have numbering: "global_clock_numbering A v n" by metis
from assms(4) obtain M where M:
"Z ⊆ V" "Z = [M]⇘v,n⇙" "dbm_int M n"
unfolding V'_def by auto
from valid_abstraction_pairsD[OF assms(2)] have "∀(x, m)∈Timed_Automata.clkp_set A. m ∈ ℕ"
by blast
from step_z_V[OF assms(1) M(1)] M(2) assms(1) step_z_dbm_DBM[OF _ numbering]
step_z_dbm_preserves_int[OF _ numbering this M(3)]
obtain M' where M': "Z' ⊆ V" "Z' = [M']⇘v,n⇙" "dbm_int M' n" by metis
then show ?thesis unfolding V'_def by blast
qed
lemma step_z_alpha_sound:
"A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ ∀c∈clk_set A. v c ≤ n ⟹ Z ∈ V'
⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z''⟩ ∧ Z'' ≠ {}"
apply (induction l' ≡ l' Z' rule: step_z_beta.induct)
apply (frule step_z_V')
apply assumption+
apply (rotate_tac 5)
apply (drule regions.apx_empty_iff')
by blast
lemma step_z_alpha_complete:
"A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ ∀c∈clk_set A. v c ≤ n ⟹ Z ∈ V'
⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l', Z''⟩ ∧ Z'' ≠ {}"
apply (frule step_z_V')
apply assumption+
apply (rotate_tac 4)
apply (drule regions.apx_empty_iff')
by blast
lemma alpha_beta_step:
"A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l', Z'⟩ ⟹ valid_abstraction A X k ⟹ ∀c∈clk_set A. v c ≤ n ⟹ Z ∈ V'
⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l', Z''⟩ ∧ Z' ⊆ Z''"
apply (induction l' ≡ l' Z' rule: step_z_beta.induct)
apply (frule step_z_V')
apply assumption+
apply (rotate_tac 4)
apply (drule regions.approx_β_closure_α')
apply auto
done
lemma alpha_beta_step':
"A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l', Z'⟩ ⟹ valid_abstraction A X k ⟹ ∀c∈clk_set A. v c ≤ n ⟹ Z ∈ V' ⟹ W ⊆ V
⟹ Z ⊆ W ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇘α(a)⇙ ⟨l', W'⟩ ∧ Z' ⊆ W'"
proof (induction l' ≡ l' Z' rule: step_z_beta.induct)
case (step_beta A l Z a Z')
from step_z_mono[OF step_beta(1,6)] obtain W' where W':
"A ⊢ ⟨l, W⟩ ↝⇘a⇙ ⟨l',W'⟩" "Z' ⊆ W'"
by blast
from regions.approx_β_closure_α'[OF step_z_V'[OF step_beta(1-4)]]
regions.alpha_interp.cla_mono[OF this(2)] this(1)
show ?case by auto
qed
lemma apx_mono:
"Z' ⊆ V ⟹ Z ⊆ Z' ⟹ Approx⇩β l' Z ⊆ Approx⇩β l' Z'"
proof (goal_cases)
case 1
with regions.beta_interp.apx_in have
"regions.Approx⇩β Z' ∈ {S. ∃U M. S = ⋃U ∧ U ⊆ regions.ℛ⇩β ∧ Z' ⊆ S ∧ regions.beta_interp.vabstr S M
∧ regions.beta_interp.normalized M}"
by auto
with 1 obtain U M where
"regions.Approx⇩β Z' = ⋃U" "U ⊆ regions.ℛ⇩β" "Z ⊆ regions.Approx⇩β Z'"
"regions.beta_interp.vabstr (regions.Approx⇩β Z') M"
"regions.beta_interp.normalized M"
by auto
with regions.beta_interp.apx_min show ?thesis by auto
qed
end
lemma step_z'_V':
assumes "A ⊢ ⟨l,Z⟩ ↝ ⟨l',Z'⟩" "valid_abstraction A X k" "∀c∈clk_set A. v c ≤ n" "Z ∈ V'"
shows "Z' ∈ V'"
using assms unfolding step_z'_def by (auto elim: step_z_V')
lemma steps_z_V':
"A ⊢ ⟨l,Z⟩ ↝* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ ∀c∈clk_set A. v c ≤ n ⟹ Z ∈ V' ⟹ Z' ∈ V'"
by (induction rule: rtranclp_induct2; blast intro: step_z'_V')
subsection ‹Multi step›
definition
step_z_beta' :: "('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇩β ⟨_, _⟩› [61,61,61] 61)
where
"A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z''⟩ = (∃ Z' a. A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l, Z'⟩ ∧ A ⊢ ⟨l, Z'⟩ ↝⇘β(↿a)⇙ ⟨l', Z''⟩)"
abbreviation
steps_z_beta :: "('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇩β* ⟨_, _⟩› [61,61,61] 61)
where
"A ⊢ ⟨l, Z⟩ ↝⇩β* ⟨l', Z''⟩ ≡ (λ (l, Z) (l', Z''). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z''⟩)⇧*⇧* (l, Z) (l', Z'')"
lemma V'_V: "Z ∈ V' ⟹ Z ⊆ V" unfolding V'_def by auto
context
fixes A :: "('a, 'c, t, 's) ta"
assumes valid_ta: "valid_abstraction A X k" "∀c∈clk_set A. v c ≤ n"
begin
interpretation alpha: AlphaClosure_global _ "k l'" "ℛ l'" by standard (rule finite)
lemma [simp]: "alpha.cla l' = cla l'" unfolding alpha.cla_def cla_def ..
lemma step_z_alpha'_V:
"Z' ⊆ V" if "Z ⊆ V" "A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Z'⟩"
using that alpha.closure_V[simplified] unfolding step_z_alpha'_def by blast
lemma step_z_beta'_V':
"Z' ∈ V'" if "A ⊢ ⟨l,Z⟩ ↝⇩β ⟨l',Z'⟩" "Z ∈ V'"
proof -
interpret regions: Regions_global _ _ _ "k l'"
by standard (rule finite clock_numbering not_in_X non_empty)+
from that valid_ta show ?thesis
unfolding step_z_beta'_def by (blast intro: step_z_V' regions.apx_V'[OF V'_V])
qed
lemma steps_z_beta_V':
"A ⊢ ⟨l,Z⟩ ↝⇩β* ⟨l',Z'⟩ ⟹ Z ∈ V' ⟹ Z' ∈ V'"
by (induction rule: rtranclp_induct2; blast intro: step_z_beta'_V')
subsubsection ‹Soundness›
lemma alpha'_beta'_step:
"A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩ ⟹ Z ∈ V' ⟹ W ⊆ V ⟹ Z ⊆ W ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇩α ⟨l', W'⟩ ∧ Z' ⊆ W'"
unfolding step_z_beta'_def step_z_alpha'_def
apply (elim exE conjE)
apply (frule step_z_mono, assumption)
apply (elim exE conjE)
apply (frule alpha_beta_step'[OF _ valid_ta])
prefer 3
using valid_ta by (blast intro: step_z_V' dest: step_z_V)+
lemma alpha_beta_sim:
"Simulation_Invariant
(λ(l, Z) (l', Z''). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z''⟩)
(λ(l, Z) (l', Z''). A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Z''⟩)
(λ(l, Z) (l', Z'). l = l' ∧ Z ⊆ Z') (λ(_, Z). Z ∈ V') (λ(_, Z). Z ⊆ V)"
by standard (auto elim: alpha'_beta'_step step_z_beta'_V' dest: step_z_alpha'_V)
interpretation
Simulation_Invariant
"λ (l, Z) (l', Z''). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z''⟩"
"λ (l, Z) (l', Z''). A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Z''⟩"
"λ (l, Z) (l', Z'). l = l' ∧ Z ⊆ Z'"
"λ (_, Z). Z ∈ V'" "λ (_, Z). Z ⊆ V"
by (fact alpha_beta_sim)
lemma alpha_beta_steps:
"A ⊢ ⟨l, Z⟩ ↝⇩β* ⟨l', Z'⟩ ⟹ Z ∈ V' ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l', Z''⟩ ∧ Z' ⊆ Z''"
using simulation_reaches[of "(l, Z)" "(l', Z')" "(l, Z)"] by (auto dest: V'_V)
end
subsubsection ‹Completeness›
lemma step_z_beta_mono:
"A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l', Z'⟩ ⟹ Z ⊆ W ⟹ W ⊆ V ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇘β(a)⇙ ⟨l', W'⟩ ∧ Z' ⊆ W'"
proof (goal_cases)
case 1
then obtain Z'' where *: "A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z''⟩" "Z' = Approx⇩β l' Z''" by auto
from step_z_mono[OF this(1) 1(2)] obtain W' where
"A ⊢ ⟨l, W⟩ ↝⇘a⇙ ⟨l',W'⟩" "Z'' ⊆ W'"
by auto
moreover with *(2) apx_mono[OF step_z_V] ‹W ⊆ V› have
"Z' ⊆ Approx⇩β l' W'"
by metis
ultimately show ?case by blast
qed
lemma step_z_beta'_V:
"Z' ⊆ V" if "A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩" "Z ⊆ V"
proof -
interpret regions: Regions_global _ _ _ "k l'"
by standard (rule finite clock_numbering not_in_X non_empty)+
from that show ?thesis unfolding step_z_beta'_def
by (auto intro: regions.apx_V dest: step_z_V del: subsetI)
qed
lemma steps_z_beta_V:
"Z' ⊆ V" if "A ⊢ ⟨l, Z⟩ ↝⇩β* ⟨l', Z'⟩" "Z ⊆ V"
using that by (induction rule: rtranclp_induct2; blast intro: step_z_beta'_V del: subsetI)
lemma step_z_beta'_mono:
"∃ W'. A ⊢ ⟨l, W⟩ ↝⇩β ⟨l', W'⟩ ∧ Z' ⊆ W'" if "A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩" "Z ⊆ W" "W ⊆ V"
using that unfolding step_z_beta'_def
apply (elim exE conjE)
apply (frule step_z_mono, assumption)
apply (elim exE conjE)
apply (drule step_z_beta_mono, assumption)
apply (auto dest: step_z_V)
done
lemma steps_z_beta_mono:
"A ⊢ ⟨l, Z⟩ ↝⇩β* ⟨l', Z'⟩ ⟹ Z ⊆ W ⟹ W ⊆ V ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇩β* ⟨l', W'⟩ ∧ Z' ⊆ W'"
apply (induction rule: rtranclp_induct2)
apply blast
apply (clarsimp; drule step_z_beta'_mono;
blast intro: rtranclp.intros(2) steps_z_beta_V del: subsetI)
done
end
end