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