chapter ‹Forward Analysis on DBMs› theory DBM_Operations imports DBM_Basics begin section ‹Auxiliary› lemma gt_swap: fixes a b c :: "'t :: time" assumes "c < a + b" shows "c < b + a" by (simp add: add.commute assms) lemma le_swap: fixes a b c :: "'t :: time" assumes "c ≤ a + b" shows "c ≤ b + a" by (simp add: add.commute assms) abbreviation clock_numbering :: "('c ⇒ nat) ⇒ bool" where "clock_numbering v ≡ ∀ c. v c > 0" section ‹Time Lapse› definition up :: "('t::time) DBM ⇒ ('t::time) DBM" where "up M ≡ λ i j. if i > 0 then if j = 0 then ∞ else min (dbm_add (M i 0) (M 0 j)) (M i j) else M i j" lemma dbm_entry_dbm_lt: assumes "dbm_entry_val u (Some c1) (Some c2) a" "a ≺ b" shows "dbm_entry_val u (Some c1) (Some c2) b" using assms proof (cases, auto, goal_cases) case 1 thus ?case by (cases, auto) next case 2 thus ?case by (cases, auto) qed lemma dbm_entry_dbm_min2: assumes "dbm_entry_val u None (Some c) (min a b)" shows "dbm_entry_val u None (Some c) b" using dbm_entry_val_mono_2[folded less_eq, OF assms] by auto lemma dbm_entry_dbm_min3: assumes "dbm_entry_val u (Some c) None (min a b)" shows "dbm_entry_val u (Some c) None b" using dbm_entry_val_mono_3[folded less_eq, OF assms] by auto lemma dbm_entry_dbm_min: assumes "dbm_entry_val u (Some c1) (Some c2) (min a b)" shows "dbm_entry_val u (Some c1) (Some c2) b" using dbm_entry_val_mono_1[folded less_eq, OF assms] by auto lemma dbm_entry_dbm_min3': assumes "dbm_entry_val u (Some c) None (min a b)" shows "dbm_entry_val u (Some c) None a" using dbm_entry_val_mono_3[folded less_eq, OF assms] by auto lemma dbm_entry_dbm_min2': assumes "dbm_entry_val u None (Some c) (min a b)" shows "dbm_entry_val u None (Some c) a" using dbm_entry_val_mono_2[folded less_eq, OF assms] by auto lemma dbm_entry_dbm_min': assumes "dbm_entry_val u (Some c1) (Some c2) (min a b)" shows "dbm_entry_val u (Some c1) (Some c2) a" using dbm_entry_val_mono_1[folded less_eq, OF assms] by auto lemma DBM_up_complete': "clock_numbering v ⟹ u ∈ ([M]⇘v,n⇙)⇧^{↑}⟹ u ∈ [up M]⇘v,n⇙" unfolding up_def DBM_zone_repr_def DBM_val_bounded_def zone_delay_def proof (safe, goal_cases) case prems: (2 u d c) hence *: "dbm_entry_val u None (Some c) (M 0 (v c))" by auto thus ?case proof (cases, goal_cases) case (1 d') have "- (u c + d) ≤ - u c" using ‹d ≥ 0› by simp with 1(2) have "- (u c + d)≤ d'" by (blast intro: order.trans) thus ?case unfolding cval_add_def using 1 by fastforce next case (2 d') have "- (u c + d) ≤ - u c" using ‹d ≥ 0› by simp with 2(2) have "- (u c + d) < d'" by (blast intro: order_le_less_trans) thus ?case unfolding cval_add_def using 2 by fastforce qed auto next case prems: (4 u d c1 c2) then have "dbm_entry_val u (Some c1) None (M (v c1) 0)" "dbm_entry_val u None (Some c2) (M 0 (v c2))" by auto from dbm_entry_val_add_4[OF this] prems have "dbm_entry_val u (Some c1) (Some c2) (min (dbm_add (M (v c1) 0) (M 0 (v c2))) (M (v c1) (v c2)))" by (auto split: split_min) with prems(1) show ?case by (cases "min (dbm_add (M (v c1) 0) (M 0 (v c2))) (M (v c1) (v c2))", auto simp: cval_add_def) qed auto fun theLe :: "('t::time) DBMEntry ⇒ 't" where "theLe (Le d) = d" | "theLe (Lt d) = d" | "theLe ∞ = 0" lemma DBM_up_sound': assumes "clock_numbering' v n" "u ∈ [up M]⇘v,n⇙" shows "u ∈ ([M]⇘v,n⇙)⇧^{↑}" unfolding DBM_zone_repr_def zone_delay_def using assms proof (clarsimp, goal_cases) case A: 1 obtain S_Max_Le where S_Max_Le: "S_Max_Le = {d - u c | c d. 0 < v c ∧ v c ≤ n ∧ M (v c) 0 = Le d}" by auto obtain S_Max_Lt where S_Max_Lt: "S_Max_Lt = {d - u c | c d. 0 < v c ∧ v c ≤ n ∧ M (v c) 0 = Lt d}" by auto obtain S_Min_Le where S_Min_Le: "S_Min_Le = {- d - u c| c d. 0 < v c ∧ v c ≤ n ∧ M 0 (v c) = Le d}" by auto obtain S_Min_Lt where S_Min_Lt: "S_Min_Lt = {- d - u c | c d. 0 < v c ∧ v c ≤ n ∧ M 0 (v c) = Lt d}" by auto have "finite {c. 0 < v c ∧ v c ≤ n}" using A(2,3) proof (induction n) case 0 then have "{c. 0 < v c ∧ v c ≤ 0} = {}" by auto then show ?case by (metis finite.emptyI) next case (Suc n) then have "finite {c. 0 < v c ∧ v c ≤ n}" by auto moreover have "{c. 0 < v c ∧ v c ≤ Suc n} = {c. 0 < v c ∧ v c ≤ n} ∪ {c. v c = Suc n}" by auto moreover have "finite {c. v c = Suc n}" proof (cases "{c. v c = Suc n} = {}", auto) fix c assume "v c = Suc n" then have "{c. v c = Suc n} = {c}" using Suc.prems(2) by auto then show ?thesis by auto qed ultimately show ?case by auto qed then have "∀ f. finite {(c,b) | c b. 0 < v c ∧ v c ≤ n ∧ f M (v c) = b}" by auto moreover have "∀ f K. {(c,K d) | c d. 0 < v c ∧ v c ≤ n ∧ f M (v c) = K d} ⊆ {(c,b) | c b. 0 < v c ∧ v c ≤ n ∧ f M (v c) = b}" by auto ultimately have 1: "∀ f K. finite {(c,K d) | c d. 0 < v c ∧ v c ≤ n ∧ f M (v c) = K d}" using finite_subset by fast have "∀ f K. theLe o K = id ⟶ finite {(c,d) | c d. 0 < v c ∧ v c ≤ n ∧ f M (v c) = K d}" proof (safe, goal_cases) case prems: (1 f K) then have "{(c,d) | c d. 0 < v c ∧ v c ≤ n ∧ f M (v c) = K d} = (λ (c,b). (c, theLe b)) ` {(c,K d) | c d. 0 < v c ∧ v c ≤ n ∧ f M (v c) = K d}" proof (auto simp add: pointfree_idE, goal_cases) case (1 a b) then have "(a, K b) ∈ {(c, K d) |c d. 0 < v c ∧ v c ≤ n ∧ f M (v c) = K d}" by auto moreover from 1(1) have "theLe (K b) = b" by (simp add: pointfree_idE) ultimately show ?case by force qed moreover from 1 have "finite ((λ (c,b). (c, theLe b)) ` {(c,K d) | c d. 0 < v c ∧ v c ≤ n ∧ f M (v c) = K d})" by auto ultimately show ?case by auto qed then have finI: "⋀ f g K. theLe o K = id ⟹ finite (g ` {(c,d) | c d. 0 < v c ∧ v c ≤ n ∧ f M (v c) = K d})" by auto have "finite ((λ(c,d). - d - u c) ` {(c,d) | c d. 0 < v c ∧ v c ≤ n ∧ M 0 (v c) = Le d})" by (rule finI, auto) moreover have "S_Min_Le = ((λ(c,d). - d - u c) ` {(c,d) | c d. 0 < v c ∧ v c ≤ n ∧ M 0 (v c) = Le d})" using S_Min_Le by auto ultimately have fin_min_le: "finite S_Min_Le" by auto have "finite ((λ(c,d). - d - u c) ` {(c,d) | c d. 0 < v c ∧ v c ≤ n ∧ M 0 (v c) = Lt d})" by (rule finI, auto) moreover have "S_Min_Lt = ((λ(c,d). - d - u c) ` {(c,d) | c d. 0 < v c ∧ v c ≤ n ∧ M 0 (v c) = Lt d})" using S_Min_Lt by auto ultimately have fin_min_lt: "finite S_Min_Lt" by auto have "finite ((λ(c,d). d - u c) ` {(c,d) | c d. 0 < v c ∧ v c ≤ n ∧ M (v c) 0 = Le d})" by (rule finI, auto) moreover have "S_Max_Le = ((λ(c,d). d - u c) ` {(c,d) | c d. 0 < v c ∧ v c ≤ n ∧ M (v c) 0 = Le d})" using S_Max_Le by auto ultimately have fin_max_le: "finite S_Max_Le" by auto have "finite ((λ(c,d). d - u c) ` {(c,d) | c d. 0 < v c ∧ v c ≤ n ∧ M (v c) 0 = Lt d})" by (rule finI, auto) moreover have "S_Max_Lt = ((λ(c,d). d - u c) ` {(c,d) | c d. 0 < v c ∧ v c ≤ n ∧ M (v c) 0 = Lt d})" using S_Max_Lt by auto ultimately have fin_max_lt: "finite S_Max_Lt" by auto { fix x assume "x ∈ S_Min_Le" hence "x ≤ 0" unfolding S_Min_Le proof (safe, goal_cases) case (1 c d) with A(1) have "- u c ≤ d" unfolding DBM_zone_repr_def DBM_val_bounded_def up_def by auto thus ?case by (simp add: minus_le_iff) qed } note Min_Le_le_0 = this have Min_Lt_le_0: "x < 0" if "x ∈ S_Min_Lt" for x using that unfolding S_Min_Lt proof (safe, goal_cases) case (1 c d) with A(1) have "- u c < d" unfolding DBM_zone_repr_def DBM_val_bounded_def up_def by auto thus ?case by (simp add: minus_less_iff) qed text ‹ The following basically all use the same proof. Only the first is not completely identical but nearly identical. › { fix l r assume "l ∈ S_Min_Le" "r ∈ S_Max_Le" with S_Min_Le S_Max_Le have "l ≤ r" proof (safe, goal_cases) case (1 c c' d d') note G1 = this hence *:"(up M) (v c') (v c) = min (dbm_add (M (v c') 0) (M 0 (v c))) (M (v c') (v c))" using A unfolding up_def by (auto split: split_min) have "dbm_entry_val u (Some c') (Some c) ((up M) (v c') (v c))" using A G1 unfolding DBM_zone_repr_def DBM_val_bounded_def by fastforce hence "dbm_entry_val u (Some c') (Some c) (dbm_add (M (v c') 0) (M 0 (v c)))" using dbm_entry_dbm_min' * by auto hence "u c' - u c ≤ d' + d" using G1 by auto hence "u c' + (- u c - d) ≤ d'" by (simp add: add_diff_eq diff_le_eq) hence "- u c - d ≤ d' - u c'" by (simp add: add.commute le_diff_eq) thus ?case by (metis add_uminus_conv_diff uminus_add_conv_diff) qed } note EE = this { fix l r assume "l ∈ S_Min_Le" "r ∈ S_Max_Le" with S_Min_Le S_Max_Le have "l ≤ r" proof (auto, goal_cases) case (1 c c' d d') note G1 = this hence *:"(up M) (v c') (v c) = min (dbm_add (M (v c') 0) (M 0 (v c))) (M (v c') (v c))" using A unfolding up_def by (auto split: split_min) have "dbm_entry_val u (Some c') (Some c) ((up M) (v c') (v c))" using A G1 unfolding DBM_zone_repr_def DBM_val_bounded_def by fastforce hence "dbm_entry_val u (Some c') (Some c) (dbm_add (M (v c') 0) (M 0 (v c)))" using dbm_entry_dbm_min' * by auto hence "u c' - u c ≤ d' + d" using G1 by auto hence "u c' + (- u c - d) ≤ d'" by (simp add: add_diff_eq diff_le_eq) hence "- u c - d ≤ d' - u c'" by (simp add: add.commute le_diff_eq) thus ?case by (metis add_uminus_conv_diff uminus_add_conv_diff) qed } note EE = this { fix l r assume "l ∈ S_Min_Lt" "r ∈ S_Max_Le" with S_Min_Lt S_Max_Le have "l < r" proof (auto, goal_cases) case (1 c c' d d') note G1 = this hence *:"(up M) (v c') (v c) = min (dbm_add (M (v c') 0) (M 0 (v c))) (M (v c') (v c))" using A unfolding up_def by (auto split: split_min) have "dbm_entry_val u (Some c') (Some c) ((up M) (v c') (v c))" using A G1 unfolding DBM_zone_repr_def DBM_val_bounded_def by fastforce hence "dbm_entry_val u (Some c') (Some c) (dbm_add (M (v c') 0) (M 0 (v c)))" using dbm_entry_dbm_min' * by auto hence "u c' - u c < d' + d" using G1 by auto hence "u c' + (- u c - d) < d'" by (simp add: add_diff_eq diff_less_eq) hence "- u c - d < d' - u c'" by (simp add: add.commute less_diff_eq) thus ?case by (metis add_uminus_conv_diff uminus_add_conv_diff) qed } note LE = this { fix l r assume "l ∈ S_Min_Le" "r ∈ S_Max_Lt" with S_Min_Le S_Max_Lt have "l < r" proof (auto, goal_cases) case (1 c c' d d') note G1 = this hence *:"(up M) (v c') (v c) = min (dbm_add (M (v c') 0) (M 0 (v c))) (M (v c') (v c))" using A unfolding up_def by (auto split: split_min) have "dbm_entry_val u (Some c') (Some c) ((up M) (v c') (v c))" using A G1 unfolding DBM_zone_repr_def DBM_val_bounded_def by fastforce hence "dbm_entry_val u (Some c') (Some c) (dbm_add (M (v c') 0) (M 0 (v c)))" using dbm_entry_dbm_min' * by auto hence "u c' - u c < d' + d" using G1 by auto hence "u c' + (- u c - d) < d'" by (simp add: add_diff_eq diff_less_eq) hence "- u c - d < d' - u c'" by (simp add: add.commute less_diff_eq) thus ?case by (metis add_uminus_conv_diff uminus_add_conv_diff) qed } note EL = this { fix l r assume "l ∈ S_Min_Lt" "r ∈ S_Max_Lt" with S_Min_Lt S_Max_Lt have "l < r" proof (auto, goal_cases) case (1 c c' d d') note G1 = this hence *:"(up M) (v c') (v c) = min (dbm_add (M (v c') 0) (M 0 (v c))) (M (v c') (v c))" using A unfolding up_def by (auto split: split_min) have "dbm_entry_val u (Some c') (Some c) ((up M) (v c') (v c))" using A G1 unfolding DBM_zone_repr_def DBM_val_bounded_def by fastforce hence "dbm_entry_val u (Some c') (Some c) (dbm_add (M (v c') 0) (M 0 (v c)))" using dbm_entry_dbm_min' * by auto hence "u c' - u c < d' + d" using G1 by auto hence "u c' + (- u c - d) < d'" by (simp add: add_diff_eq diff_less_eq) hence "- u c - d < d' - u c'" by (simp add: add.commute less_diff_eq) thus ?case by (metis add_uminus_conv_diff uminus_add_conv_diff) qed } note LL = this obtain m where m: "∀ t ∈ S_Min_Le. m ≥ t" "∀ t ∈ S_Min_Lt. m > t" "∀ t ∈ S_Max_Le. m ≤ t" "∀ t ∈ S_Max_Lt. m < t" "m ≤ 0" proof - assume m:"(⋀m. ∀t∈S_Min_Le. t ≤ m ⟹ ∀t∈S_Min_Lt. t < m ⟹ ∀t∈S_Max_Le. m ≤ t ⟹ ∀t∈S_Max_Lt. m < t ⟹ m ≤ 0 ⟹ thesis)" let ?min_le = "Max S_Min_Le" let ?min_lt = "Max S_Min_Lt" let ?max_le = "Min S_Max_Le" let ?max_lt = "Min S_Max_Lt" show thesis proof (cases "S_Min_Le = {} ∧ S_Min_Lt = {}") case True note T = this show thesis proof (cases "S_Max_Le = {} ∧ S_Max_Lt = {}") case True let ?d' = "0 :: 't :: time" show thesis using True T by (intro m[of ?d']) auto next case False let ?d = "if S_Max_Le ≠ {} then if S_Max_Lt ≠ {} then min ?max_lt ?max_le else ?max_le else ?max_lt" obtain a :: "'b" where a: "a < 0" using non_trivial_neg by auto let ?d' = "min 0 (?d + a)" { fix x assume "x ∈ S_Max_Le" with fin_max_le a have "min 0 (Min S_Max_Le + a) ≤ x" by (metis Min_le add_le_same_cancel1 le_less_trans less_imp_le min.cobounded2 not_less) then have "min 0 (Min S_Max_Le + a) ≤ x" by auto } note 1 = this { fix x assume x: "x ∈ S_Max_Lt" have "min 0 (min (Min S_Max_Lt) (Min S_Max_Le) + a) < ?max_lt" by (meson a add_less_same_cancel1 min.cobounded1 min.strict_coboundedI2 order.strict_trans2) also from fin_max_lt x have "… ≤ x" by auto finally have "min 0 (min (Min S_Max_Lt) (Min S_Max_Le) + a) < x" . } note 2 = this { fix x assume x: "x ∈ S_Max_Le" have "min 0 (min (Min S_Max_Lt) (Min S_Max_Le) + a) ≤ ?max_le" by (metis le_add_same_cancel1 linear not_le a min_le_iff_disj) also from fin_max_le x have "… ≤ x" by auto finally have "min 0 (min (Min S_Max_Lt) (Min S_Max_Le) + a) ≤ x" . } note 3 = this show thesis using False T a 1 2 3 proof ((intro m[of ?d']), auto, goal_cases) case 1 then show ?case by (metis Min.coboundedI add_less_same_cancel1 dual_order.strict_trans2 fin_max_lt min.boundedE not_le) qed qed next case False note F = this show thesis proof (cases "S_Max_Le = {} ∧ S_Max_Lt = {}") case True let ?d' = "0 :: 't :: time" show thesis using True Min_Le_le_0 Min_Lt_le_0 by (intro m[of ?d']) auto next case False let ?r = "if S_Max_Le ≠ {} then if S_Max_Lt ≠ {} then min ?max_lt ?max_le else ?max_le else ?max_lt" let ?l = "if S_Min_Le ≠ {} then if S_Min_Lt ≠ {} then max ?min_lt ?min_le else ?min_le else ?min_lt" have 1: "x ≤ max ?min_lt ?min_le" "x ≤ ?min_le" if "x ∈ S_Min_Le" for x using that fin_min_le by (simp add: max.coboundedI2)+ { fix x y assume x: "x ∈ S_Max_Le" "y ∈ S_Min_Lt" then have "S_Min_Lt ≠ {}" by auto from LE[OF Max_in[OF fin_min_lt], OF this, OF x(1)] have "?min_lt ≤ x" by auto } note 3 = this have 4: "?min_le ≤ x" if "x ∈ S_Max_Le" "y ∈ S_Min_Le" for x y using EE[OF Max_in[OF fin_min_le], OF _ that(1)] that by auto { fix x y assume x: "x ∈ S_Max_Lt" "y ∈ S_Min_Lt" then have "S_Min_Lt ≠ {}" by auto from LL[OF Max_in[OF fin_min_lt], OF this, OF x(1)] have "?min_lt < x" by auto } note 5 = this { fix x y assume x: "x ∈ S_Max_Lt" "y ∈ S_Min_Le" then have "S_Min_Le ≠ {}" by auto from EL[OF Max_in[OF fin_min_le], OF this, OF x(1)] have "?min_le < x" by auto } note 6 = this { fix x y assume x: "y ∈ S_Min_Le" then have "S_Min_Le ≠ {}" by auto from Min_Le_le_0[OF Max_in[OF fin_min_le], OF this] have "?min_le ≤ 0" by auto } note 7 = this { fix x y assume x: "y ∈ S_Min_Lt" then have "S_Min_Lt ≠ {}" by auto from Min_Lt_le_0[OF Max_in[OF fin_min_lt], OF this] have "?min_lt < 0" "?min_lt ≤ 0" by auto } note 8 = this show thesis proof (cases "?l < ?r") case False then have *: "S_Max_Le ≠ {}" proof (auto, goal_cases) case 1 with ‹¬ (S_Max_Le = {} ∧ S_Max_Lt = {})› obtain y where y:"y ∈ S_Max_Lt" by auto note 1 = 1 this { fix x y assume A: "x ∈ S_Min_Le" "y ∈ S_Max_Lt" with EL[OF Max_in[OF fin_min_le] Min_in[OF fin_max_lt]] have "Max S_Min_Le < Min S_Max_Lt" by auto } note ** = this { fix x y assume A: "x ∈ S_Min_Lt" "y ∈ S_Max_Lt" with LL[OF Max_in[OF fin_min_lt] Min_in[OF fin_max_lt]] have "Max S_Min_Lt < Min S_Max_Lt" by auto } note *** = this show ?case proof (cases "S_Min_Le ≠ {}") case True note T = this show ?thesis proof (cases "S_Min_Lt ≠ {}") case True then show False using 1 T True ** *** by auto next case False with 1 T ** show False by auto qed next case False with 1 False *** ‹¬ (S_Min_Le = {} ∧ S_Min_Lt = {})› show ?thesis by auto qed qed { fix x y assume A: "x ∈ S_Min_Lt" "y ∈ S_Max_Lt" with LL[OF Max_in[OF fin_min_lt] Min_in[OF fin_max_lt]] have "Max S_Min_Lt < Min S_Max_Lt" by auto } note *** = this { fix x y assume A: "x ∈ S_Min_Lt" "y ∈ S_Max_Le" with LE[OF Max_in[OF fin_min_lt] Min_in[OF fin_max_le]] have "Max S_Min_Lt < Min S_Max_Le" by auto } note **** = this from F False have **: "S_Min_Le ≠ {}" proof (auto, goal_cases) case 1 show ?case proof (cases "S_Max_Le ≠ {}") case True note T = this show ?thesis proof (cases "S_Max_Lt ≠ {}") case True then show False using 1 T True **** *** by auto next case False with 1 T **** show False by auto qed next case False with 1 False *** ‹¬ (S_Max_Le = {} ∧ S_Max_Lt = {})› show ?thesis by auto qed qed { fix x assume x: "x ∈ S_Min_Lt" then have "x ≤ ?min_lt" using fin_min_lt by (simp add: max.coboundedI2) also have "?min_lt < ?min_le" proof (rule ccontr, goal_cases) case 1 with x ** have 1: "?l = ?min_lt" by (auto simp: max.absorb1) have 2: "?min_lt < ?max_le" using * ****[OF x] by auto show False proof (cases "S_Max_Lt = {}") case False then have "?min_lt < ?max_lt" using * ***[OF x] by auto with 1 2 have "?l < ?r" by auto with ‹¬ ?l < ?r› show False by auto next case True with 1 2 have "?l < ?r" by auto with ‹¬ ?l < ?r› show False by auto qed qed finally have "x < max ?min_lt ?min_le" by (simp add: max.strict_coboundedI2) } note 2 = this show thesis using F False 1 2 3 4 5 6 7 8 * ** by ((intro m[of ?l]), auto) next case True then obtain d where d: "?l < d" "d < ?r" using dense by auto let ?d' = "min 0 d" { fix t assume "t ∈ S_Min_Le" then have "t ≤ ?l" using 1 by auto with d have "t ≤ d" by auto } moreover { fix t assume t: "t ∈ S_Min_Lt" then have "t ≤ max ?min_lt ?min_le" using fin_min_lt by (simp add: max.coboundedI1) with t Min_Lt_le_0 have "t ≤ ?l" using fin_min_lt by auto with d have "t < d" by auto } moreover { fix t assume t: "t ∈ S_Max_Le" then have "min ?max_lt ?max_le ≤ t" using fin_max_le by (simp add: min.coboundedI2) then have "?r ≤ t" using fin_max_le t by auto with d have "d ≤ t" by auto then have "min 0 d ≤ t" by (simp add: min.coboundedI2) } moreover { fix t assume t: "t ∈ S_Max_Lt" then have "min ?max_lt ?max_le ≤ t" using fin_max_lt by (simp add: min.coboundedI1) then have "?r ≤ t" using fin_max_lt t by auto with d have "d < t" by auto then have "min 0 d < t" by (simp add: min.strict_coboundedI2) } ultimately show thesis using Min_Le_le_0 Min_Lt_le_0 by ((intro m[of ?d']), auto) qed qed qed qed obtain u' where "u' = (u ⊕ m)" by blast hence u': "u = (u' ⊕ (-m))" unfolding cval_add_def by force have "DBM_val_bounded v u' M n" unfolding DBM_val_bounded_def proof (auto, goal_cases) case 1 with A(1,2) show ?case unfolding DBM_zone_repr_def DBM_val_bounded_def up_def by auto next case (3 c) thus ?case proof (cases "M (v c) 0", goal_cases) case (1 x1) hence "m ≤ x1 - u c" using m(3) S_Max_Le A(2) by blast hence "u c + m ≤ x1" by (simp add: add.commute le_diff_eq) thus ?case using u' 1(2) unfolding cval_add_def by auto next case (2 x2) hence "m < x2 - u c" using m(4) S_Max_Lt A(2) by blast hence "u c + m < x2" by (metis add_less_cancel_left diff_add_cancel gt_swap) thus ?case using u' 2(2) unfolding cval_add_def by auto next case 3 thus ?case by auto qed next case (2 c) thus ?case proof (cases "M 0 (v c)", goal_cases) case (1 x1) hence "- x1 - u c ≤ m" using m(1) S_Min_Le A(2) by blast hence "- u c - m ≤ x1" using diff_le_eq neg_le_iff_le by fastforce thus ?case using u' 1(2) unfolding cval_add_def by auto next case (2 x2) hence "- x2 - u c < m" using m(2) S_Min_Lt A(2) by blast hence "- u c - m < x2" using diff_less_eq neg_less_iff_less by fastforce thus ?case using u' 2(2) unfolding cval_add_def by auto next case 3 thus ?case by auto qed next case (4 c1 c2) from A(2) have "v c1 > 0" "v c2 ≠ 0" by auto then have B: "(up M) (v c1) (v c2) = min (dbm_add (M (v c1) 0) (M 0 (v c2))) (M (v c1) (v c2))" unfolding up_def by simp show ?case proof (cases "(dbm_add (M (v c1) 0) (M 0 (v c2))) < (M (v c1) (v c2))") case False with B have "(up M) (v c1) (v c2) = M (v c1) (v c2)" by (auto split: split_min) with A(1) 4 have "dbm_entry_val u (Some c1) (Some c2) (M (v c1) (v c2))" unfolding DBM_zone_repr_def unfolding DBM_val_bounded_def by fastforce thus ?thesis using u' by cases (auto simp add: cval_add_def) next case True with B have "(up M) (v c1) (v c2) = dbm_add (M (v c1) 0) (M 0 (v c2))" by (auto split: split_min) with A(1) 4 have "dbm_entry_val u (Some c1) (Some c2) (dbm_add (M (v c1) 0) (M 0 (v c2)))" unfolding DBM_zone_repr_def unfolding DBM_val_bounded_def by fastforce with True dbm_entry_dbm_lt have "dbm_entry_val u (Some c1) (Some c2) (M (v c1) (v c2))" unfolding less by fast thus ?thesis using u' by cases (auto simp add: cval_add_def) qed qed with m(5) u' show ?case by fastforce qed section ‹From Clock Constraints to DBMs› fun And :: "('t :: time) DBM ⇒ 't DBM ⇒ 't DBM" where "And M1 M2 = (λ i j. min (M1 i j) (M2 i j))" fun abstr :: "('c, 't::time) cconstraint ⇒ 't DBM ⇒ ('c ⇒ nat) ⇒ 't DBM" where "abstr (AND cc1 cc2) M v = And (abstr cc1 M v) (abstr cc2 M v)" | "abstr (EQ c d) M v = (λ i j . if i = 0 ∧ j = v c then Le (-d) else if i = v c ∧ j = 0 then Le d else M i j)" | "abstr (LT c d) M v = (λ i j . if i = 0 ∧ j = v c then ∞ else if i = v c ∧ j = 0 then Lt d else M i j)" | "abstr (LE c d) M v = (λ i j . if i = 0 ∧ j = v c then ∞ else if i = v c ∧ j = 0 then Le d else M i j)" | "abstr (GT c d) M v = (λ i j. if i = 0 ∧ j = v c then Lt (- d) else if i = v c ∧ j = 0 then ∞ else M i j)" | "abstr (GE c d) M v = (λ i j. if i = 0 ∧ j = v c then Le (- d) else if i = v c ∧ j = 0 then ∞ else M i j)" lemma abstr_id1: "c ∉ collect_clks cc ⟹ clock_numbering' v n ⟹ ∀ c ∈ collect_clks cc. v c ≤ n ⟹ abstr cc M v 0 (v c) = M 0 (v c)" by (induction cc) auto lemma abstr_id2: "c ∉ collect_clks cc ⟹ clock_numbering' v n ⟹ ∀ c ∈ collect_clks cc. v c ≤ n ⟹ abstr cc M v (v c) 0 = M (v c) 0" by (induction cc) auto text ‹ This lemma is trivial because we constrained our theory to difference constraints. › lemma abstr_id3: "clock_numbering v ⟹ abstr cc M v (v c1) (v c2) = M (v c1) (v c2)" proof goal_cases case 1 have "⋀c. v c = 0 ⟹ False" proof - fix c assume "v c = 0" moreover from 1 have "v c > 0" by auto ultimately show False by linarith qed then show ?case by ((induction cc), auto, fastforce) qed lemma dbm_abstr_soundness : "⟦u ⊢ cc; clock_numbering' v n; ∀ c ∈ collect_clks cc. v c ≤ n⟧ ⟹ DBM_val_bounded v u (abstr cc (λ i j. ∞) v) n" proof (unfold DBM_val_bounded_def, auto, goal_cases) case 1 from this(3) have "abstr cc (λi j. ∞) v 0 0 = ∞" by (induction cc) auto then show ?case unfolding dbm_le_def by auto next case (2 c) then have "clock_numbering' v n" by auto note A = 2(1) this 2(5,2) show ?case proof (cases "c ∈ collect_clks cc") case True then show ?thesis using A(1,4) proof (induction rule: collect_clks.induct) case (1 cc1 cc2) { assume cc: "c ∈ collect_clks cc1" "c ∈ collect_clks cc2" with 1 have ?case by auto linarith } note both = this show ?case proof (cases "c ∈ collect_clks cc1") case True note cc1 = this with 1 have *: "dbm_entry_val u None (Some c) (abstr cc1 (λi j. ∞) v 0 (v c))" by auto show ?thesis proof (cases "c ∈ collect_clks cc2") case True with cc1 both show ?thesis by auto next case False from abstr_id1[OF False A(2)] 1(5) have "min (abstr cc1 (λi j. ∞) v 0 (v c)) (abstr cc2 (λi j. ∞) v 0 (v c)) = abstr cc1 (λi j. ∞) v 0 (v c)" by (simp add: any_le_inf min.absorb1) with * show ?thesis by auto qed next case False note cc1 = this show ?thesis proof (cases "c ∈ collect_clks cc2") case True with 1 have *: "dbm_entry_val u None (Some c) (abstr cc2 (λi j. ∞) v 0 (v c))" by auto from abstr_id1[OF cc1 A(2)] 1(5) have "min (abstr cc1 (λi j. ∞) v 0 (v c)) (abstr cc2 (λi j. ∞) v 0 (v c)) = abstr cc2 (λi j. ∞) v 0 (v c)" by (simp add: any_le_inf min.absorb2) with * show ?thesis by auto next case False with 1 cc1 show ?thesis by auto qed qed qed auto next case False from abstr_id1[OF this A(2,4)] show ?thesis by auto qed next case (3 c) then have "clock_numbering' v n" by auto note A = 3(1) this 3(5,2) from A(2) have gt0: "v c > 0" by auto show ?case proof (cases "c ∈ collect_clks cc") case True then show ?thesis using A(1,4) proof (induction rule: collect_clks.induct) case (1 cc1 cc2) { assume cc: "c ∈ collect_clks cc1" "c ∈ collect_clks cc2" with 1 have ?case by auto linarith } note both = this show ?case proof (cases "c ∈ collect_clks cc1") case True note cc1 = this with 1 have *: "dbm_entry_val u (Some c) None (abstr cc1 (λi j. ∞) v (v c) 0)" by auto show ?thesis proof (cases "c ∈ collect_clks cc2") case True with cc1 both show ?thesis by auto next case False from abstr_id2[OF False A(2)] 1(5) have "min (abstr cc1 (λi j. ∞) v (v c) 0) (abstr cc2 (λi j. ∞) v (v c) 0) = abstr cc1 (λi j. ∞) v (v c) 0" by (simp add: any_le_inf min.absorb1) with * show ?thesis by auto qed next case False note cc1 = this show ?thesis proof (cases "c ∈ collect_clks cc2") case True with 1 have *: "dbm_entry_val u (Some c) None (abstr cc2 (λi j. ∞) v (v c) 0)" by auto from abstr_id2[OF cc1 A(2)] 1(5) have "min (abstr cc1 (λi j. ∞) v (v c) 0) (abstr cc2 (λi j. ∞) v (v c) 0) = abstr cc2 (λi j. ∞) v (v c) 0" by (simp add: any_le_inf min.absorb2) with * show ?thesis by auto next case False with 1 cc1 show ?thesis by auto qed qed qed (insert gt0, auto) next case False from abstr_id2[OF this A(2,4)] show ?thesis by auto qed next text ‹Trivial because of missing difference constraints› case (4 c1 c2) from abstr_id3[OF this(3)] have "abstr cc (λi j. ∞) v (v c1) (v c2) = ∞" by auto then show ?case by auto qed lemma dbm_abstr_completeness: "⟦DBM_val_bounded v u (abstr cc (λ i j. ∞) v) n; ∀c. v c > 0; ∀ c ∈ collect_clks cc. v c ≤ n⟧ ⟹ u ⊢ cc" proof (induction cc, goal_cases) case (1 cc1 cc2) then have AND: "u ∈ [abstr (AND cc1 cc2) (λi j. ∞) v]⇘v,n⇙" by (simp add: DBM_zone_repr_def) from 1 have "∀i j. i ≤ n ⟶ j ≤ n ⟶ (abstr (AND cc1 cc2) (λi j. ∞) v) i j ≼ (abstr cc1 (λi j. ∞) v) i j" by (simp add: less_eq[symmetric]) from DBM_le_subset[OF this AND] 1 have "u ⊢ cc1" unfolding DBM_zone_repr_def by auto from 1 have "∀i j. i ≤ n ⟶ j ≤ n ⟶ (abstr (AND cc1 cc2) (λi j. ∞) v) i j ≼ (abstr cc2 (λi j. ∞) v) i j" by (simp add: less_eq[symmetric]) from DBM_le_subset[OF this AND] 1 have "u ⊢ cc2" unfolding DBM_zone_repr_def by auto from ‹u ⊢ cc1› ‹u ⊢ cc2› show ?case by auto next case (2 c d) from this have "v c ≤ n" by auto with 2(1) have "dbm_entry_val u (Some c) None ((abstr (LT c d) (λi j. ∞) v) (v c) 0)" by (auto simp: DBM_val_bounded_def) moreover from 2(2) have "v c > 0" by auto ultimately show ?case by auto next case (3 c d) from this have "v c ≤ n" by auto with 3(1) have "dbm_entry_val u (Some c) None ((abstr (LE c d) (λi j. ∞) v) (v c) 0)" by (auto simp: DBM_val_bounded_def) moreover from 3(2) have "v c > 0" by auto ultimately show ?case by auto next case (4 c d) from this have c: "v c > 0" "v c ≤ n" by auto with 4(1) have B: "dbm_entry_val u (Some c) None ((abstr (EQ c d) (λi j. ∞) v) (v c) 0)" "dbm_entry_val u None (Some c) ((abstr (EQ c d) (λi j. ∞) v) 0 (v c))" by (auto simp: DBM_val_bounded_def) from c B have "u c ≤ d" "- u c ≤ -d" by auto then show ?case by auto next case (5 c d) from this have "v c ≤ n" by auto with 5(1) have "dbm_entry_val u None (Some c) ((abstr (GT c d) (λi j. ∞) v) 0 (v c))" by (auto simp: DBM_val_bounded_def) moreover from 5(2) have "v c > 0" by auto ultimately show ?case by auto next case (6 c d) from this have "v c ≤ n" by auto with 6(1) have "dbm_entry_val u None (Some c) ((abstr (GE c d) (λi j. ∞) v) 0 (v c))" by (auto simp: DBM_val_bounded_def) moreover from 6(2) have "v c > 0" by auto ultimately show ?case by auto qed lemma dbm_abstr_zone_eq: assumes "clock_numbering' v n" "∀c∈collect_clks cc. v c ≤ n" shows "[abstr cc (λi j. ∞) v]⇘v,n⇙ = {u. u ⊢ cc}" using dbm_abstr_soundness dbm_abstr_completeness assms unfolding DBM_zone_repr_def by metis section ‹Zone Intersection› lemma DBM_and_complete: assumes "DBM_val_bounded v u M1 n" "DBM_val_bounded v u M2 n" shows "DBM_val_bounded v u (And M1 M2) n" using assms unfolding DBM_val_bounded_def by (auto simp: min_def) lemma DBM_and_sound1: assumes "DBM_val_bounded v u (And M1 M2) n" shows "DBM_val_bounded v u M1 n" unfolding DBM_val_bounded_def using assms proof (safe, goal_cases) case 1 then show ?case unfolding DBM_val_bounded_def by (auto simp: less_eq[symmetric]) next case (2 c) then have "(And M1 M2) 0 (v c) ≤ M1 0 (v c)" by simp from dbm_entry_val_mono_2[folded less_eq, OF _ this, of u] 2 show ?case unfolding DBM_val_bounded_def by auto next case (3 c) then have "(And M1 M2) (v c) 0 ≤ M1 (v c) 0" by simp from dbm_entry_val_mono_3[folded less_eq, OF _ this, of u] 3 show ?case unfolding DBM_val_bounded_def by auto next case (4 c1 c2) then have "(And M1 M2) (v c1) (v c2) ≤ M1 (v c1) (v c2)" by simp from dbm_entry_val_mono_1[folded less_eq, OF _ this, of u] 4 show ?case unfolding DBM_val_bounded_def by auto qed lemma DBM_and_sound2: assumes "DBM_val_bounded v u (And M1 M2) n" shows "DBM_val_bounded v u M2 n" unfolding DBM_val_bounded_def using assms proof (safe, goal_cases) case 1 then show ?case unfolding DBM_val_bounded_def by (auto simp: less_eq[symmetric]) next case (2 c) then have "(And M1 M2) 0 (v c) ≤ M2 0 (v c)" by simp from dbm_entry_val_mono_2[folded less_eq, OF _ this, of u] 2 show ?case unfolding DBM_val_bounded_def by auto next case (3 c) then have "(And M1 M2) (v c) 0 ≤ M2 (v c) 0" by simp from dbm_entry_val_mono_3[folded less_eq, OF _ this, of u] 3 show ?case unfolding DBM_val_bounded_def by auto next case (4 c1 c2) then have "(And M1 M2) (v c1) (v c2) ≤ M2 (v c1) (v c2)" by simp from dbm_entry_val_mono_1[folded less_eq, OF _ this, of u] 4 show ?case unfolding DBM_val_bounded_def by auto qed section ‹Clock Reset› definition DBM_reset :: "('t :: time) DBM ⇒ nat ⇒ nat ⇒ 't ⇒ 't DBM ⇒ bool" where "DBM_reset M n k d M' ≡ (∀ j ≤ n. 0 < j ∧ k ≠ j⟶ M' k j = ∞ ∧ M' j k = ∞) ∧ M' k 0 = Le d ∧ M' 0 k = Le (- d) ∧ M' k k = M k k ∧ (∀i ≤ n. ∀j ≤ n. i ≠ k ∧ j ≠ k ⟶ M' i j = min (dbm_add (M i k) (M k j)) (M i j))" lemma DBM_reset_mono: assumes "DBM_reset M n k d M'" "i ≤ n" "j ≤ n" "i ≠ k" "j ≠ k" shows "M' i j ≤ M i j" using assms unfolding DBM_reset_def by auto lemma DBM_reset_len_mono: assumes "DBM_reset M n k d M'" "k ∉ set xs" "i ≠ k" "j ≠ k" "set (i # j # xs) ⊆ {0..n}" shows "len M' i j xs ≤ len M i j xs" using assms by (induction xs arbitrary: i) (auto intro: add_mono DBM_reset_mono) lemma DBM_reset_neg_cycle_preservation: assumes "DBM_reset M n k d M'" "len M i i xs < Le 0" "set (k # i # xs) ⊆ {0..n}" shows "∃ j. ∃ ys. set (j # ys) ⊆ {0..n} ∧ len M' j j ys < Le 0" proof (cases "xs = []") case Nil: True show ?thesis proof (cases "k = i") case True with Nil assms have "len M' i i [] < Le 0" unfolding DBM_reset_def by auto moreover from assms have "set (i # []) ⊆ {0..n}" by auto ultimately show ?thesis by blast next case False with Nil assms DBM_reset_mono have "len M' i i [] < Le 0" by fastforce moreover from assms have "set (i # []) ⊆ {0..n}" by auto ultimately show ?thesis by blast qed next case False with assms obtain j ys where cycle: "len M j j ys < Le 0" "distinct (j # ys)" "j ∈ set (i # xs)" "set ys ⊆ set xs" by (metis negative_len_shortest neutral) show ?thesis proof (cases "k ∈ set (j # ys)") case False with cycle assms have "len M' j j ys ≤ len M j j ys" by - (rule DBM_reset_len_mono, auto) moreover from cycle assms have "set (j # ys) ⊆ {0..n}" by auto ultimately show ?thesis using cycle(1) by fastforce next case True then obtain l where l: "(l, k) ∈ set (arcs j j ys)" proof (cases "j = k", goal_cases) case True show ?thesis proof (cases "ys = []") case T: True with True show ?thesis by (auto intro: that) next case False then obtain z zs where "ys = zs @ [z]" by (metis append_butlast_last_id) from arcs_decomp[OF this] True show ?thesis by (auto intro: that) qed next case False from arcs_set_elem2[OF False True] show ?thesis by (blast intro: that) qed show ?thesis proof (cases "ys = []") case False from cycle_rotate_2'[OF False l, of M] cycle(1) obtain zs where rotated: "len M l l (k # zs) < Le 0" "set (l # k # zs) = set (j # ys)" "1 + length zs = length ys" by auto with length_eq_distinct[OF this(2)[symmetric] cycle(2)] have "distinct (l # k # zs)" by auto note rotated = rotated(1,2) this from this(2) cycle(3,4) assms(3) have n_bound: "set (l # k # zs) ⊆ {0..n}" by auto then have "l ≤ n" by auto show ?thesis proof (cases zs) case Nil with rotated have "M l k + M k l < Le 0" "l ≠ k" by auto with assms(1) ‹l ≤ n› have "M' l l < Le 0" unfolding DBM_reset_def mult min_def by auto with ‹l ≤ n› have "len M' l l [] < Le 0" "set [l] ⊆ {0..n}" by auto then show ?thesis by blast next case (Cons w ws) with n_bound have *: "set (w # l # ws) ⊆ {0..n}" by auto from Cons n_bound rotated(3) have "w ≤ n" "w ≠ k" "l ≠ k" by auto with assms(1) ‹l ≤ n› have "M' l w ≤ M l k + M k w" unfolding DBM_reset_def mult min_def by auto moreover from Cons rotated assms * have "len M' w l ws ≤ len M w l ws" by - (rule DBM_reset_len_mono, auto) ultimately have "len M' l l zs ≤ len M l l (k # zs)" using Cons by (auto intro: add_mono simp add: assoc[symmetric]) with n_bound rotated(1) show ?thesis by fastforce qed next case T: True with True cycle have "M j j < Le 0" "j = k" by auto with assms(1) have "len M' k k [] < Le 0" unfolding DBM_reset_def by simp moreover from assms(3) have "set (k # []) ⊆ {0..n}" by auto ultimately show ?thesis by blast qed qed qed text ‹Implementation of DBM reset› definition reset :: "('t::time) DBM ⇒ nat ⇒ nat ⇒ 't ⇒ 't DBM" where "reset M n k d = (λ i j. if i = k ∧ j = 0 then Le d else if i = 0 ∧ j = k then Le (-d) else if i = k ∧ j ≠ k then ∞ else if i ≠ k ∧ j = k then ∞ else if i = k ∧ j = k then M k k else min (dbm_add (M i k) (M k j)) (M i j) )" fun reset' :: "('t::time) DBM ⇒ nat ⇒ 'c list ⇒ ('c ⇒ nat) ⇒ 't ⇒ 't DBM" where "reset' M n [] v d = M" | "reset' M n (c # cs) v d = reset (reset' M n cs v d) n (v c) d" lemma DBM_reset_reset: "0 < k ⟹ k ≤ n ⟹ DBM_reset M n k d (reset M n k d)" unfolding DBM_reset_def by (auto simp: reset_def) lemma DBM_reset_complete: assumes "clock_numbering' v n" "v c ≤ n" "DBM_reset M n (v c) d M'" "DBM_val_bounded v u M n" shows "DBM_val_bounded v (u(c := d)) M' n" unfolding DBM_val_bounded_def using assms proof (auto, goal_cases) case 1 then have *: "M 0 0 ≥ Le 0" unfolding DBM_val_bounded_def less_eq by auto from 1 have **: "M' 0 0 = min (M 0 (v c) + M (v c) 0) (M 0 0)" unfolding DBM_reset_def mult by auto show ?case proof (cases "M 0 (v c) + M (v c) 0 ≤ M 0 0") case False with * ** show ?thesis unfolding min_def less_eq by auto next case True have "dbm_entry_val u (Some c) (Some c) (M (v c) 0 + M 0 (v c))" by (metis DBM_val_bounded_def assms(2,4) dbm_entry_val_add_4 mult) then have "M (v c) 0 + M 0 (v c) ≥ Le 0" unfolding less_eq dbm_le_def by (cases "M (v c) 0 + M 0 (v c)") auto with True ** have "M' 0 0 ≥ Le 0" by (simp add: comm) then show ?thesis unfolding less_eq . qed next case (2 c') show ?case proof (cases "c = c'") case False hence F:"v c' ≠ v c" using 2 by metis hence *:"M' 0 (v c') = min (dbm_add (M 0 (v c)) (M (v c) (v c'))) (M 0 (v c'))" using F 2(1,2,4,6) unfolding DBM_reset_def by simp show ?thesis proof (cases "dbm_add (M 0 (v c)) (M (v c) (v c')) < M 0 (v c')") case False with * have "M' 0 (v c') = M 0 (v c')" by (auto split: split_min) hence "dbm_entry_val u None (Some c') (M' 0 (v c'))" using 2(3,6) unfolding DBM_val_bounded_def by auto thus ?thesis using F by cases fastforce+ next case True with * have **:"M' 0 (v c') = dbm_add (M 0 (v c)) (M (v c) (v c'))" by (auto split: split_min) from 2 have "dbm_entry_val u None (Some c) (M 0 (v c))" "dbm_entry_val u (Some c) (Some c') (M (v c) (v c'))" unfolding DBM_val_bounded_def by auto thus ?thesis proof (cases, auto simp add: **, goal_cases) case (1 d) note G1 = this from this(2) show ?case proof (cases, goal_cases) case (1 d') from this(2) G1(3) have "- u c' ≤ d + d'" by (metis diff_minus_eq_add less_diff_eq less_le_trans minus_diff_eq minus_le_iff not_le) thus ?case using 1 ‹c ≠ c'› by fastforce next case (2 d') from this(2) G1(3) have "u c - u c' - u c < d + d'" using add_le_less_mono by fastforce hence "- u c' < d + d'" by simp thus ?case using 2 ‹c ≠ c'› by fastforce next case (3) thus ?case by auto qed next case (2 d) note G2 = this from this(2) show ?case proof (cases, goal_cases) case (1 d') from this(2) G2(3) have "u c - u c' - u c < d' + d" using add_le_less_mono by fastforce hence "- u c' < d' + d" by simp hence "- u c' < d + d'" by (metis (opaque_lifting, no_types) diff_0_right diff_minus_eq_add minus_add_distrib minus_diff_eq) thus ?case using 1 ‹c ≠ c'› by fastforce next case (2 d') from this(2) G2(3) have "u c - u c' - u c < d + d'" using add_strict_mono by fastforce hence "- u c' < d + d'" by simp thus ?case using 2 ‹c ≠ c'› by fastforce next case (3) thus ?case by auto qed qed qed next case True with 2 show ?thesis unfolding DBM_reset_def by auto qed next case (3 c') show ?case proof (cases "c = c'") case False hence F:"v c' ≠ v c" using 3 by metis hence *:"M' (v c') 0 = min (dbm_add (M (v c') (v c)) (M (v c) 0)) (M (v c') 0)" using F 3(1,2,4,6) unfolding DBM_reset_def by simp show ?thesis proof (cases "dbm_add (M (v c') (v c)) (M (v c) 0) < M (v c') 0") case False with * have "M' (v c') 0 = M (v c') 0" by (auto split: split_min) hence "dbm_entry_val u (Some c') None (M' (v c') 0)" using 3(3,6) unfolding DBM_val_bounded_def by auto thus ?thesis using F by cases fastforce+ next case True with * have **:"M' (v c') 0 = dbm_add (M (v c') (v c)) (M (v c) 0)" by (auto split: split_min) from 3 have "dbm_entry_val u (Some c') (Some c) (M (v c') (v c))" "dbm_entry_val u (Some c) None (M (v c) 0)" unfolding DBM_val_bounded_def by auto thus ?thesis proof (cases, auto simp add: **, goal_cases) case (1 d) note G1 = this from this(2) show ?case proof (cases, goal_cases) case (1 d') from this(2) G1(3) have "u c' ≤ d + d'" using ordered_ab_semigroup_add_class.add_mono by fastforce thus ?case using 1 ‹c ≠ c'› by fastforce next case (2 d') from this(2) G1(3) have "u c + u c' - u c < d + d'" using add_le_less_mono by fastforce hence "u c' < d + d'" by simp thus ?case using 2 ‹c ≠ c'› by fastforce next case (3) thus ?case by auto qed next case (2 d) note G2 = this from this(2) show ?case proof (cases, goal_cases) case (1 d') from this(2) G2(3) have "u c + u c' - u c < d' + d" using add_le_less_mono by fastforce hence "u c' < d' + d" by simp hence "u c' < d + d'" by (metis (opaque_lifting, no_types) diff_0_right diff_minus_eq_add minus_add_distrib minus_diff_eq) thus ?case using 1 ‹c ≠ c'› by fastforce next case (2 d') from this(2) G2(3) have "u c + u c' - u c < d + d'" using add_strict_mono by fastforce hence "u c' < d + d'" by simp thus ?case using 2 ‹c ≠ c'› by fastforce next case 3 thus ?case by auto qed qed qed next case True with 3 show ?thesis unfolding DBM_reset_def by auto qed next case (4 c1 c2) show ?case proof (cases "c = c1") case False note F1 = this show ?thesis proof (cases "c = c2") case False with F1 4 have F: "v c ≠ v c1" "v c ≠ v c2" "v c1 ≠ 0" "v c2 ≠ 0" by force+ hence *:"M' (v c1) (v c2) = min (dbm_add (M (v c1) (v c)) (M (v c) (v c2))) (M (v c1) (v c2))" using 4(1,2,6,7) unfolding DBM_reset_def by simp show ?thesis proof (cases "dbm_add (M (v c1) (v c)) (M (v c) (v c2)) < M (v c1) (v c2)") case False with * have "M' (v c1) (v c2) = M (v c1) (v c2)" by (auto split: split_min) hence "dbm_entry_val u (Some c1) (Some c2) (M' (v c1) (v c2))" using 4(3,6,7) unfolding DBM_val_bounded_def by auto thus ?thesis using F by cases fastforce+ next case True with * have **:"M' (v c1) (v c2) = dbm_add (M (v c1) (v c)) (M (v c) (v c2))" by (auto split: split_min) from 4 have "dbm_entry_val u (Some c1) (Some c) (M (v c1) (v c))" "dbm_entry_val u (Some c) (Some c2) (M (v c) (v c2))" unfolding DBM_val_bounded_def by auto thus ?thesis proof (cases, auto simp add: **, goal_cases) case (1 d) note G1 = this from this(2) show ?case proof (cases, goal_cases) case (1 d') from this(2) G1(3) have "u c1 - u c2 ≤ d + d'" by (metis (opaque_lifting, no_types) ab_semigroup_add_class.add_ac(1) add_le_cancel_right add_left_mono diff_add_cancel dual_order.refl dual_order.trans) thus ?case using 1 ‹c ≠ c1› ‹c ≠ c2› by fastforce next case (2 d') from add_less_le_mono[OF this(2) G1(3)] have "- u c2 + u c1 < d' + d" by simp hence "u c1 - u c2 < d + d'" by (simp add: add.commute) thus ?case using 2 ‹c ≠ c1› ‹c ≠ c2› by fastforce next case (3) thus ?case by auto qed next case (2 d) note G2 = this from this(2) show ?case proof (cases, goal_cases) case (1 d') from add_less_le_mono[OF G2(3) this(2)] have "u c1 - u c2 < d + d'" by (metis (opaque_lifting, no_types) ab_semigroup_add_class.add_ac(1) add_le_cancel_right diff_add_cancel dual_order.order_iff_strict dual_order.strict_trans2) thus ?case using 1 ‹c ≠ c1› ‹c ≠ c2› by fastforce next case (2 d') from add_strict_mono[OF this(2) G2(3)] have "- u c2 + u c1 < d' + d" by simp hence "- u c2 + u c1 < d + d'" by (metis (full_types) diff_0 diff_minus_eq_add minus_add_distrib minus_diff_eq) hence "u c1 - u c2 < d + d'" by (metis add_diff_cancel_left diff_0 diff_0_right diff_add_cancel) thus ?case using 2 ‹c ≠ c1› ‹c ≠ c2› by fastforce next case (3) thus ?case by auto qed qed qed next case True with F1 4 have F: "v c ≠ v c1" "v c1 ≠ 0" "v c2 ≠ 0" by force+ thus ?thesis using 4(1,2,4,6,7) True unfolding DBM_reset_def by auto qed next case True note T1 = this show ?thesis proof (cases "c = c2") case False with T1 4 have F: "v c ≠ v c2" "v c1 ≠ 0" "v c2 ≠ 0" by force+ thus ?thesis using 4(1,2,7) True unfolding DBM_reset_def by auto next case True then have *: "M' (v c1) (v c1) = M (v c1) (v c1)" using T1 4 unfolding DBM_reset_def by auto from 4(1,3) True T1 have "dbm_entry_val u (Some c1) (Some c2) (M (v c1) (v c2))" unfolding DBM_val_bounded_def by auto then show ?thesis by (cases rule: dbm_entry_val.cases, auto simp: * True[symmetric] T1) qed qed qed lemma DBM_reset_sound_empty: assumes "clock_numbering' v n" "v c ≤ n" "DBM_reset M n (v c) d M'" "∀ u . ¬ DBM_val_bounded v u M' n" shows "¬ DBM_val_bounded v u M n" using assms DBM_reset_complete by metis lemma DBM_reset_diag_preservation: "∀k≤n. M k k ≤ 𝟭 ⟹ DBM_reset M n i d M' ⟹ ∀k≤n. M' k k ≤ 𝟭" apply auto apply (case_tac "k = i") apply (simp add: DBM_reset_def less[symmetric]) apply (case_tac "k = 0") by (auto simp add: DBM_reset_def less[symmetric] neutral split: split_min) lemma FW_diag_preservation: "∀k