# Theory Timed_Automata.DBM_Operations

```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"

lemma le_swap:
fixes a b c :: "'t :: time"
assumes "c ≤ a + b"
shows "c ≤ b + a"

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
"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)
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)
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)
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)
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)
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
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
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)"
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)"
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"
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"
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"
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"
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)"
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'"
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'"
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'"
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'"
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'"
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")