theory Approx_Beta imports DBM_Zone_Semantics Regions_Beta Closure begin chapter ‹Correctness of ‹β›-approximation from ‹α›-regions› text ‹Instantiating real› instantiation real :: linordered_ab_monoid_add 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 lemma add_inf[simp]: "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)) 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 < 𝟭" 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</}