Theory Regions_Beta

theory Regions_Beta
imports Misc DBM_Normalization DBM_Operations
begin

chapter ‹Refinement to ‹β›-regions›

section ‹Definition›

type_synonym 'c ceiling = "('c ⇒ nat)"

datatype intv =
  Const nat |
  Intv nat |
  Greater nat

datatype intv' =
  Const' int |
  Intv' int |
  Greater' int |
  Smaller' int

type_synonym t = real

instantiation real :: time
begin
  instance proof
    fix x y :: real
    assume "x < y" 
    then show "∃z>x. z < y" using dense_order_class.dense by blast 
  next
    have "(1 :: real) ≠ 0" by auto
    then show "∃x. (x::real) ≠ 0" ..
  qed
end

inductive valid_intv :: "nat ⇒ intv ⇒ bool"
where
  "0 ≤ d ⟹ d ≤ c ⟹ valid_intv c (Const d)" |
  "0 ≤ d ⟹ d < c  ⟹ valid_intv c (Intv d)" |
  "valid_intv c (Greater c)"

inductive valid_intv' :: "int ⇒ int ⇒ intv' ⇒ bool"
where
  "valid_intv' l _ (Smaller' (-l))" |
  "-l ≤ d ⟹ d ≤ u ⟹ valid_intv' l u (Const' d)" |
  "-l ≤ d ⟹ d < u  ⟹ valid_intv' l u (Intv' d)" |
  "valid_intv' _ u (Greater' u)"

inductive intv_elem :: "'c ⇒ ('c,t) cval ⇒ intv ⇒ bool"
where
  "u x = d ⟹ intv_elem x u (Const d)" |
  "d < u x ⟹ u x < d + 1 ⟹ intv_elem x u (Intv d)" |
  "c < u x ⟹ intv_elem x u (Greater c)"

inductive intv'_elem :: "'c ⇒ 'c ⇒ ('c,t) cval ⇒ intv' ⇒ bool"
where
  "u x - u y < c ⟹ intv'_elem x y u (Smaller' c)" |
  "u x - u y = d ⟹ intv'_elem x y u (Const' d)" |
  "d < u x - u y ⟹ u x - u y < d + 1 ⟹ intv'_elem x y u (Intv' d)" |
  "c < u x - u y ⟹ intv'_elem x y u (Greater' c)"

abbreviation "total_preorder r ≡ refl r ∧ trans r"

inductive isConst :: "intv ⇒ bool"
where
  "isConst (Const _)"

inductive isIntv :: "intv ⇒ bool"
where
  "isIntv (Intv _)"

inductive isGreater :: "intv ⇒ bool"
where
  "isGreater (Greater _)"

declare isIntv.intros[intro!] isConst.intros[intro!] isGreater.intros[intro!]

declare isIntv.cases[elim!] isConst.cases[elim!] isGreater.cases[elim!]

inductive valid_region :: "'c set ⇒ ('c ⇒ nat) ⇒ ('c ⇒ intv) ⇒ ('c ⇒ 'c ⇒ intv') ⇒ 'c rel ⇒ bool"
where
  "⟦X⇩0 = {x ∈ X. ∃ d. I x = Intv d}; refl_on X⇩0 r; trans r; total_on X⇩0 r; ∀ x ∈ X. valid_intv (k x) (I x);
    ∀ x ∈ X. ∀ y ∈ X. isGreater (I x) ∨ isGreater (I y) ⟶ valid_intv' (k y) (k x) (J x y)⟧
  ⟹ valid_region X k I J r"

inductive_set region for X I J r
where
  "∀ x ∈ X. u x ≥ 0 ⟹ ∀ x ∈ X. intv_elem x u (I x) ⟹ X⇩0 = {x ∈ X. ∃ d. I x = Intv d} ⟹
   ∀ x ∈ X⇩0. ∀ y ∈ X⇩0. (x, y) ∈ r ⟷ frac (u x) ≤ frac (u y) ⟹
   ∀ x ∈ X. ∀ y ∈ X. isGreater (I x) ∨ isGreater (I y) ⟶ intv'_elem x y u (J x y)
  ⟹ u ∈ region X I J r"


text ‹Defining the unique element of a partition that contains a valuation›

definition part ("[_]⇩_" [61,61] 61) where "part v ℛ ≡ THE R. R ∈ ℛ ∧ v ∈ R"

text ‹
  First we need to show that the set of regions is a partition of the set of all clock
  assignments. This property is only claimed by P. Bouyer.
›

inductive_cases[elim!]: "intv_elem x u (Const d)"
inductive_cases[elim!]: "intv_elem x u (Intv d)"
inductive_cases[elim!]: "intv_elem x u (Greater d)"
inductive_cases[elim!]: "valid_intv c (Greater d)"
inductive_cases[elim!]: "valid_intv c (Const d)"
inductive_cases[elim!]: "valid_intv c (Intv d)"
inductive_cases[elim!]: "intv'_elem x y u (Const' d)"
inductive_cases[elim!]: "intv'_elem x y u (Intv' d)"
inductive_cases[elim!]: "intv'_elem x y u (Greater' d)"
inductive_cases[elim!]: "intv'_elem x y u (Smaller' d)"
inductive_cases[elim!]: "valid_intv' l u (Greater' d)"
inductive_cases[elim!]: "valid_intv' l u (Smaller' d)"
inductive_cases[elim!]: "valid_intv' l u (Const' d)"
inductive_cases[elim!]: "valid_intv' l u (Intv' d)"

declare valid_intv.intros[intro]
declare valid_intv'.intros[intro]
declare intv_elem.intros[intro]
declare intv'_elem.intros[intro]

declare region.cases[elim]
declare valid_region.cases[elim]

section ‹Basic Properties›

text ‹First we show that all valid intervals are distinct›

lemma valid_intv_distinct:
  "valid_intv c I ⟹ valid_intv c I' ⟹ intv_elem x u I ⟹ intv_elem x u I' ⟹ I = I'"
by (cases I) (cases I', auto)+

lemma valid_intv'_distinct:
  "-c ≤ d ⟹ valid_intv' c d I ⟹ valid_intv' c d I' ⟹ intv'_elem x y u I ⟹ intv'_elem x y u I'
  ⟹ I = I'"
by (cases I) (cases I', auto)+

text ‹From this we show that all valid regions are distinct›

lemma valid_regions_distinct:
  "valid_region X k I J r ⟹ valid_region X k I' J' r' ⟹ v ∈ region X I J r ⟹ v ∈ region X I' J' r'
  ⟹ region X I J r = region X I' J' r'"
proof goal_cases
  case 1
  note A = 1
  { fix x assume x: "x ∈ X"
    with A(1) have "valid_intv (k x) (I x)" by auto
    moreover from A(2) x have "valid_intv (k x) (I' x)" by auto
    moreover from A(3) x have "intv_elem x v (I x)" by auto
    moreover from A(4) x have "intv_elem x v (I' x)" by auto
    ultimately have "I x = I' x" using valid_intv_distinct by fastforce
  } note * = this
  { fix x y assume x: "x ∈ X" and y: "y ∈ X" and B: "isGreater (I x) ∨ isGreater (I y)"
    with * have C: "isGreater (I' x) ∨ isGreater (I' y)" by auto
    from A(1) x y B have "valid_intv' (k y) (k x) (J x y)" by fastforce
    moreover from A(2) x y C have "valid_intv' (k y) (k x) (J' x y)" by fastforce
    moreover from A(3) x y B have "intv'_elem x y v (J x y)" by force
    moreover from A(4) x y C have "intv'_elem x y v (J' x y)" by force
    moreover from x y valid_intv'_distinct have "- int (k y) ≤ int (k x)" by simp
    ultimately have "J x y = J' x y" by (blast intro: valid_intv'_distinct)
  } note ** = this
  from A show ?thesis
  proof (auto, goal_cases)
    case (1 u)
    note A = this
    { fix x assume x: "x ∈ X"
      from A(5) x have "intv_elem x u (I x)" by auto
      with * x have "intv_elem x u (I' x)" by auto
    }
    then have "∀ x ∈ X. intv_elem x u (I' x)" by auto
    note B = this
    { fix x y assume x: "x ∈ X" and y: "y ∈ X" and B: "isGreater (I' x) ∨ isGreater (I' y)"
      with * have "isGreater (I x) ∨ isGreater (I y)" by auto
      with x y A(5) have "intv'_elem x y u (J x y)" by force
      with **[OF x y ‹isGreater (I x) ∨ _›] have "intv'_elem x y u (J' x y)" by simp
    } note C = this
    let ?X⇩0 = "{x ∈ X. ∃ d. I' x = Intv d}"
    { fix x y assume x: "x ∈ ?X⇩0" and y: "y ∈ ?X⇩0"
      have "(x, y) ∈ r' ⟷ frac (u x) ≤ frac (u y)"
      proof
        assume "frac (u x) ≤ frac (u y)"
        with A(5) x y * have "(x,y) ∈ r" by auto
        with A(3) x y * have "frac (v x) ≤ frac (v y)" by auto
        with A(4) x y   show "(x,y) ∈ r'" by auto
      next
        assume "(x,y) ∈ r'"
        with A(4) x y   have "frac (v x) ≤ frac (v y)" by auto
        with A(3) x y * have "(x,y) ∈ r" by auto
        with A(5) x y * show "frac (u x) ≤ frac (u y)" by auto
      qed
    }
    then have *: "∀ x ∈ ?X⇩0. ∀ y ∈ ?X⇩0. (x, y) ∈ r' ⟷ frac (u x) ≤ frac (u y)" by auto
    from A(5) have "∀x∈X. 0 ≤ u x" by auto
    from region.intros[OF this B _ *] C show ?case by auto
  next
    case (2 u)
    note A = this
    { fix x assume x: "x ∈ X"
      from A(5) x have "intv_elem x u (I' x)" by auto
      with * x have "intv_elem x u (I x)" by auto
    }
    then have "∀ x ∈ X. intv_elem x u (I x)" by auto
    note B = this
    { fix x y assume x: "x ∈ X" and y: "y ∈ X" and B: "isGreater (I x) ∨ isGreater (I y)"
      with * have "isGreater (I' x) ∨ isGreater (I' y)" by auto
      with x y A(5) have "intv'_elem x y u (J' x y)" by force
      with **[OF x y ‹isGreater (I x) ∨ _›] have "intv'_elem x y u (J x y)" by simp
    } note C = this
    let ?X⇩0 = "{x ∈ X. ∃ d. I x = Intv d}"
    { fix x y assume x: "x ∈ ?X⇩0" and y: "y ∈ ?X⇩0"
      have "(x, y) ∈ r ⟷ frac (u x) ≤ frac (u y)"
      proof
        assume "frac (u x) ≤ frac (u y)"
        with A(5) x y * have "(x,y) ∈ r'" by auto
        with A(4) x y * have "frac (v x) ≤ frac (v y)" by auto
        with A(3) x y   show "(x,y) ∈ r" by auto
      next
        assume "(x,y) ∈ r"
        with A(3) x y   have "frac (v x) ≤ frac (v y)" by auto
        with A(4) x y * have "(x,y) ∈ r'" by auto
        with A(5) x y * show "frac (u x) ≤ frac (u y)" by auto
      qed
    }
    then have *:"∀ x ∈ ?X⇩0. ∀ y ∈ ?X⇩0. (x, y) ∈ r ⟷ frac (u x) ≤ frac (u y)" by auto
    from A(5) have "∀x∈X. 0 ≤ u x" by auto
    from region.intros[OF this B _ *] C show ?case by auto
  qed
qed

locale Beta_Regions =
  fixes X k ℛ and V :: "('c, t) cval set"
  defines "ℛ ≡ {region X I J r | I J r. valid_region X k I J r}"
  defines "V ≡ {v . ∀ x ∈ X. v x ≥ 0}"
  assumes finite: "finite X"
  assumes non_empty: "X ≠ {}"
begin

lemma ℛ_regions_distinct:
  "⟦R ∈ ℛ; v ∈ R; R' ∈ ℛ; R ≠ R'⟧ ⟹ v ∉ R'"
unfolding ℛ_def using valid_regions_distinct by blast

text ‹
  Secondly, we also need to show that every valuations belongs to a region which is part of
  the partition.
›

definition intv_of :: "nat ⇒ t ⇒ intv" where
  "intv_of c v ≡
    if (v > c) then Greater c
    else if (∃ x :: nat. x = v) then (Const (nat (floor v)))
    else (Intv (nat (floor v)))"

definition intv'_of :: "int ⇒ int ⇒ t ⇒ intv'" where
  "intv'_of l u v ≡
    if (v > u) then Greater' u
    else if (v < l) then Smaller' l
    else if (∃ x :: int. x = v) then (Const' (floor v))
    else (Intv' (floor v))"

lemma region_cover:
  "∀ x ∈ X. v x ≥ 0 ⟹ ∃ R. R ∈ ℛ ∧ v ∈ R"
proof (standard, standard)
  assume assm: "∀ x ∈ X. 0 ≤ v x"
  let ?I = "λ x. intv_of (k x) (v x)"
  let ?J = "λ x y. intv'_of (-k y) (k x) (v x - v y)"
  let ?X⇩0 = "{x ∈ X. ∃ d. ?I x = Intv d}"
  let ?r = "{(x,y). x ∈ ?X⇩0 ∧ y ∈ ?X⇩0 ∧ frac (v x) ≤ frac (v y)}"
  { fix x y d assume A: "x ∈ X" "y ∈ X"
    then have "intv'_elem x y v (intv'_of (- int (k y)) (int (k x)) (v x - v y))" unfolding intv'_of_def
    proof (auto, goal_cases)
      case (1 a)
      then have "⌊v x - v y⌋ = v x - v y" by (metis of_int_floor_cancel)
      then show ?case by auto
    next
      case 2
      then have "⌊v x - v y⌋ < v x - v y" by (meson eq_iff floor_eq_iff not_less)
      with 2 show ?case by auto
    qed
  } note intro = this
  show "v ∈ region X ?I ?J ?r"
  proof (standard, auto simp: assm intro: intro, goal_cases)
    case (1 x)
    thus ?case unfolding intv_of_def
    proof (auto, goal_cases)
      case (1 a)
      note A = this
      from A(2) have "⌊v x⌋ = v x" by (metis floor_of_int of_int_of_nat_eq)
      with assm A(1) have "v x = real (nat ⌊v x⌋)" by auto
      then show ?case by auto
    next
      case 2
      note A = this
      from A(1,2) have "real (nat ⌊v x⌋) < v x"
      proof -
        have f1: "0 ≤ v x"
          using assm 1 by blast
        have "v x ≠ real_of_int (int (nat ⌊v x⌋))"
          by (metis (no_types) 2(2) of_int_of_nat_eq)
        then show ?thesis
          using f1 by linarith
      qed
      moreover from assm have "v x < real (nat (⌊v x⌋) + 1)" by linarith
      ultimately show ?case by auto
    qed
  qed
  { fix x y assume "x ∈ X" "y ∈ X"
    then have "valid_intv' (int (k y)) (int (k x)) (intv'_of (- int (k y)) (int (k x)) (v x - v y))"
    unfolding intv'_of_def
     apply auto
      apply (metis floor_of_int le_floor_iff linorder_not_less of_int_minus of_int_of_nat_eq valid_intv'.simps)
    by (metis floor_less_iff less_eq_real_def not_less of_int_minus of_int_of_nat_eq valid_intv'.intros(3))
  }
  moreover
  { fix x assume x: "x ∈ X"
    then have "valid_intv (k x) (intv_of (k x) (v x))"
    proof (auto simp: intv_of_def, goal_cases)
      case (1 a)
      then show ?case
      by (intro valid_intv.intros(1)) (auto, linarith)
    next
      case 2
      then show ?case
      apply (intro valid_intv.intros(2))
      using assm floor_less_iff nat_less_iff by fastforce+
    qed
  }
  ultimately have "valid_region X k ?I ?J ?r"
  by (intro valid_region.intros, auto simp: refl_on_def trans_def total_on_def)
  then show "region X ?I ?J ?r ∈ ℛ" unfolding ℛ_def by auto
qed

lemma region_cover_V: "v ∈ V ⟹ ∃ R. R ∈ ℛ ∧ v ∈ R" using region_cover unfolding V_def by simp

text ‹
  Note that we cannot show that every region is non-empty anymore.
  The problem are regions fixing differences between an 'infeasible' constant.
›

text ‹
  We can show that there is always exactly one region a valid valuation belongs to.
  Note that we do not need non-emptiness for that.
›
lemma regions_partition:
  "∀x ∈ X. 0 ≤ v x ⟹ ∃! R ∈ ℛ. v ∈ R"
proof goal_cases
  case 1
  note A = this
  with region_cover[OF ] obtain R where R: "R ∈ ℛ ∧ v ∈ R" by fastforce
  moreover 
  { fix R' assume "R' ∈ ℛ ∧ v ∈ R'"
   with R valid_regions_distinct[OF _ _ _ _] have "R' = R" unfolding ℛ_def by blast
  }
  ultimately show ?thesis by auto
qed

lemma region_unique:
  "v ∈ R ⟹ R ∈ ℛ ⟹ [v]⇩ℛ = R"
proof goal_cases
  case 1
  note A = this
  from A obtain I J r where *:
    "valid_region X k I J r" "R = region X I J r" "v ∈ region X I J r"
  by (auto simp: ℛ_def)
  from this(3) have "∀x∈X. 0 ≤ v x" by auto
  from theI'[OF regions_partition[OF this]] obtain I' J' r' where
    v: "valid_region X k I' J' r'" "[v]⇩ℛ = region X I' J' r'" "v ∈ region X I' J' r'"
  unfolding part_def ℛ_def by auto
  from valid_regions_distinct[OF *(1) v(1) *(3) v(3)] v(2) *(2) show ?case by auto
qed

lemma regions_partition':
  "∀x∈X. 0 ≤ v x ⟹ ∀x∈X. 0 ≤ v' x ⟹ v' ∈ [v]⇩ℛ ⟹ [v']⇩ℛ = [v]⇩ℛ"
proof goal_cases
  case 1
  note A = this
  from theI'[OF regions_partition[OF A(1)]] A(3) obtain I J r where
    v: "valid_region X k I J r" "[v]⇩ℛ = region X I J r" "v' ∈ region X I J r"
  unfolding part_def ℛ_def by blast
  from theI'[OF regions_partition[OF A(2)]] obtain I' J' r' where
    v': "valid_region X k I' J' r'" "[v']⇩ℛ = region X I' J' r'" "v' ∈ region X I' J' r'"
  unfolding part_def ℛ_def by auto
  from valid_regions_distinct[OF v'(1) v(1) v'(3) v(3)] v(2) v'(2) show ?case by simp
qed

lemma regions_closed:
  "R ∈ ℛ ⟹ v ∈ R ⟹ t ≥ 0 ⟹ [v ⊕ t]⇩ℛ ∈ ℛ"
proof goal_cases
  case 1
  note A = this
  then obtain I J r where "v ∈ region X I J r" unfolding ℛ_def by auto
  from this(1) have "∀ x ∈ X. v x ≥ 0" by auto
  with A(3) have "∀ x ∈ X. (v ⊕ t) x ≥ 0" unfolding cval_add_def by simp
  from regions_partition[OF this] obtain R' where "R' ∈ ℛ" "(v ⊕ t) ∈ R'" by auto
  with region_unique[OF this(2,1)] show ?case by auto
qed

lemma regions_closed':
  "R ∈ ℛ ⟹ v ∈ R ⟹ t ≥ 0 ⟹ (v ⊕ t) ∈ [v ⊕ t]⇩ℛ"
proof goal_cases
  case 1
  note A = this
  then obtain I J r where "v ∈ region X I J r" unfolding ℛ_def by auto
  from this(1) have "∀ x ∈ X. v x ≥ 0" by auto
  with A(3) have "∀ x ∈ X. (v ⊕ t) x ≥ 0" unfolding cval_add_def by simp
  from regions_partition[OF this] obtain R' where "R' ∈ ℛ" "(v ⊕ t) ∈ R'" by auto
  with region_unique[OF this(2,1)] show ?case by auto
qed

lemma valid_regions_I_cong:
  "valid_region X k I J r ⟹ ∀ x ∈ X. I x = I' x
  ⟹ ∀ x ∈ X. ∀ y ∈ X. (isGreater (I x) ∨ isGreater (I y)) ⟶ J x y = J' x y
  ⟹ region X I J r = region X I' J' r ∧ valid_region X k I' J' r"
proof (auto, goal_cases)
  case (1 v)
  note A = this
  then have [simp]:
    "⋀ x. x ∈ X ⟹ I' x = I x"
    "⋀ x y. x ∈ X ⟹ y ∈ X ⟹ isGreater (I x) ∨ isGreater (I y) ⟹ J x y = J' x y"
  by metis+
  show ?case
  proof (standard, goal_cases)
    case 1 from A(4) show ?case by auto
  next
    case 2 from A(4) show ?case by auto
  next
    case 3 show "{x ∈ X. ∃d. I x = Intv d} = {x ∈ X. ∃d. I' x = Intv d}" by auto
  next
    case 4
    let ?X⇩0 = "{x ∈ X. ∃d. I x = Intv d}"
    from A(4) show "∀ x ∈ ?X⇩0. ∀ y ∈ ?X⇩0. ((x, y) ∈ r) = (frac (v x) ≤ frac (v y))" by auto
  next
    case 5 from A(4) show ?case by force
  qed
next
  case (2 v)
  note A = this
  then have [simp]:
    "⋀ x. x ∈ X ⟹ I' x = I x"
    "⋀ x y. x ∈ X ⟹ y ∈ X ⟹ isGreater (I x) ∨ isGreater (I y) ⟹ J x y = J' x y"
  by metis+
  show ?case
  proof (standard, goal_cases)
    case 1 from A(4) show ?case by auto
  next
    case 2 from A(4) show ?case by auto
  next
    case 3
    show "{x ∈ X. ∃d. I' x = Intv d} = {x ∈ X. ∃d. I x = Intv d}" by auto
  next
    case 4
    let ?X⇩0 = "{x ∈ X. ∃d. I' x = Intv d}"
    from A(4) show "∀ x ∈ ?X⇩0. ∀ y ∈ ?X⇩0. ((x, y) ∈ r) = (frac (v x) ≤ frac (v y))" by auto
  next
    case 5 from A(4) show ?case by force
  qed
next
  case 3
  note A = this
  then have [simp]:
    "⋀ x. x ∈ X ⟹ I' x = I x"
    "⋀ x y. x ∈ X ⟹ y ∈ X ⟹ isGreater (I x) ∨ isGreater (I y) ⟹ J x y = J' x y"
  by metis+
  show ?case
    apply rule
         apply (subgoal_tac "{x ∈ X. ∃d. I x = Intv d} = {x ∈ X. ∃d. I' x = Intv d}")
          apply assumption
  using A by force+
qed

fun intv_const :: "intv ⇒ nat"
where
  "intv_const (Const d) = d" |
  "intv_const (Intv d) = d"  |
  "intv_const (Greater d) = d"

fun intv'_const :: "intv' ⇒ int"
where
  "intv'_const (Smaller' d) = d" |
  "intv'_const (Const' d) = d" |
  "intv'_const (Intv' d) = d"  |
  "intv'_const (Greater' d) = d"

lemma finite_ℛ_aux:
  fixes P A B assumes "finite {x. A x}" "finite {x. B x}"
  shows "finite {(I, J) | I J. P I J r ∧ A I ∧ B J}"
using assms by (fastforce intro: pairwise_finiteI finite_ex_and1 finite_ex_and2)

lemma finite_ℛ:
  notes [[simproc add: finite_Collect]]
  shows "finite ℛ"
proof -
  { fix I J r assume A: "valid_region X k I J r"
    let ?X⇩0 = "{x ∈ X. ∃d. I x = Intv d}"
    from A have "refl_on ?X⇩0 r" by auto
    then have "r ⊆ X × X" by (auto simp: refl_on_def)
    then have "r ∈ Pow (X × X)" by auto
  }
  then have "{r. ∃I J. valid_region X k I J r} ⊆ Pow (X × X)" by auto
  from finite_subset[OF this] finite have fin: "finite {r. ∃I J. valid_region X k I J r}" by auto
  let ?u = "Max {k x | x. x ∈ X}"
  let ?l = "- Max {k x | x. x ∈ X}"
  let ?I = "{intv. intv_const intv ≤ ?u}"
  let ?J = "{intv. ?l ≤ intv'_const intv ∧ intv'_const intv ≤ ?u}"
  let ?S = "{r. ∃I J. valid_region X k I J r}"
  let ?fin_mapI = "λ I. ∀x. (x ∈ X ⟶ I x ∈ ?I) ∧ (x ∉ X ⟶ I x = Const 0)"
  let ?fin_mapJ = "λ J. ∀x. ∀y. (x ∈ X ∧ y ∈ X ⟶ J x y ∈ ?J)
                              ∧ (x ∉ X ⟶ J x y = Const' 0) ∧ (y ∉ X ⟶ J x y = Const' 0)"
  let ?ℛ = "{region X I J r | I J r. valid_region X k I J r ∧ ?fin_mapI I ∧ ?fin_mapJ J}"
  let ?f = "λr. {region X I J r | I J . valid_region X k I J r ∧ ?fin_mapI I ∧ ?fin_mapJ J}"
  let ?g = "λr. {(I, J) | I J . valid_region X k I J r ∧ ?fin_mapI I ∧ ?fin_mapJ J}"
  have "?I = (Const ` {d. d ≤ ?u}) ∪ (Intv ` {d. d ≤ ?u}) ∪ (Greater ` {d. d ≤ ?u})"
  by auto (case_tac x, auto)
  then have "finite ?I" by auto
  from finite_set_of_finite_funs[OF ‹finite X› this] have finI: "finite {I. ?fin_mapI I}" .
  have "?J = (Smaller' ` {d. ?l ≤ d ∧ d ≤ ?u}) ∪ (Const' ` {d. ?l ≤ d ∧ d ≤ ?u})
           ∪ (Intv' ` {d. ?l ≤ d ∧ d ≤ ?u}) ∪ (Greater' ` {d. ?l ≤ d ∧ d ≤ ?u})"
  by auto (case_tac x, auto)
  then have "finite ?J" by auto
  from finite_set_of_finite_funs2[OF ‹finite X› ‹finite X› this] have finJ: "finite {J. ?fin_mapJ J}" .
  from finite_ℛ_aux[OF finI finJ, of "valid_region X k"] have "∀r ∈ ?S. finite (?g r)" by simp
  moreover have "∀ r ∈ ?S. ?f r = (λ (I, J). region X I J r) ` ?g r" by auto
  ultimately have "∀r ∈ ?S. finite (?f r)" by auto
  moreover have "?ℛ = ⋃ (?f `?S)" by auto
  ultimately have "finite ?ℛ" using fin by auto
  moreover have "ℛ ⊆ ?ℛ"
  proof
    fix R assume R: "R ∈ ℛ"
    then obtain I J r where I: "R = region X I J r" "valid_region X k I J r" unfolding ℛ_def by auto
    let ?I = "λ x. if x ∈ X then I x else Const 0"
    let ?J = "λ x y. if x ∈ X ∧ y ∈ X ∧ (isGreater (I x) ∨ isGreater (I y)) then J x y else Const' 0"
    let ?R = "region X ?I ?J r"
    from valid_regions_I_cong[OF I(2)] I have *: "R = ?R" "valid_region X k ?I ?J r" by auto
    have "∀x. x ∉ X ⟶ ?I x = Const 0" by auto
    moreover have "∀x. x ∈ X ⟶ intv_const (I x) ≤ ?u"
    proof auto
      fix x assume x: "x ∈ X"
      with I(2) have "valid_intv (k x) (I x)" by auto
      moreover from ‹finite X› x have "k x ≤ ?u" by (auto intro: Max_ge)
      ultimately  show "intv_const (I x) ≤ Max {k x |x. x ∈ X}" by (cases "I x") auto
    qed
    ultimately have **: "?fin_mapI ?I" by auto
    have "∀x y. x ∉ X ⟶ ?J x y = Const' 0" by auto
    moreover have "∀x y. y ∉ X ⟶ ?J x y = Const' 0" by auto
    moreover have "∀x. ∀ y. x ∈ X ∧ y ∈ X ⟶ ?l ≤ intv'_const (?J x y) ∧ intv'_const (?J x y) ≤ ?u"
    proof clarify
      fix x y assume x: "x ∈ X" assume y: "y ∈ X"
      show "?l ≤ intv'_const (?J x y) ∧ intv'_const (?J x y) ≤ ?u"
      proof (cases "isGreater (I x) ∨ isGreater (I y)")
        case True
        with x y I(2) have "valid_intv' (k y) (k x) (J x y)" by fastforce
        moreover from ‹finite X› x have "k x ≤ ?u" by (auto intro: Max_ge)
        moreover from ‹finite X› y have "?l ≤ -k y" by (auto intro: Max_ge)
        ultimately show ?thesis by (cases "J x y") auto
      next
        case False then show ?thesis by auto
      qed
    qed
    ultimately have "?fin_mapJ ?J" by auto
    with * ** show "R ∈ ?ℛ" by blast
  qed
  ultimately show "finite ℛ" by (blast intro: finite_subset)
qed

end

section ‹Approximation with ‹β›-regions›

locale Beta_Regions' = Beta_Regions +
  fixes v n not_in_X
  assumes clock_numbering: "∀ c. v c > 0 ∧ (∀x. ∀y. v x ≤ n ∧ v y ≤ n ∧ v x = v y ⟶ x = y)"
                           "∀k :: nat ≤n. k > 0 ⟶ (∃c ∈ X. v c = k)" "∀ c ∈ X. v c ≤ n"
  assumes not_in_X: "not_in_X ∉ X"
begin

definition "v' ≡ λ i. if i ≤ n then (THE c. c ∈ X ∧ v c = i) else not_in_X"

lemma v_v':
  "∀ c ∈ X. v' (v c) = c"
using clock_numbering unfolding v'_def by auto

abbreviation
  "vabstr (S :: ('a, t) zone) M ≡ S = [M]⇘v,n⇙ ∧ (∀ i≤n. ∀ j≤n. M i j ≠ ∞ ⟶ get_const (M i j) ∈ ℤ)"

definition normalized:
  "normalized M ≡
    (∀ i j. 0 < i ∧ i ≤ n ∧ 0 < j ∧ j ≤ n ∧ M i j ≠ ∞ ⟶
       Lt (- ((k o v') j)) ≤ M i j ∧ M i j ≤ Le ((k o v') i))
    ∧ (∀ i ≤ n. i > 0 ⟶ (M i 0 ≤ Le ((k o v') i) ∨ M i 0 = ∞) ∧ Lt (- ((k o v') i)) ≤ M 0 i)"

definition apx_def:
  "Approx⇩β Z ≡ ⋂ {S. ∃ U M. S = ⋃ U ∧ U ⊆ ℛ ∧ Z ⊆ S ∧ vabstr S M ∧ normalized M}"

lemma apx_min:
  "S = ⋃ U ⟹ U ⊆ ℛ ⟹ S = [M]⇘v,n⇙ ⟹ ∀ i≤n. ∀ j≤n. M i j ≠ ∞ ⟶ get_const (M i j) ∈ ℤ
  ⟹ normalized M ⟹ Z ⊆ S ⟹ Approx⇩β Z ⊆ S"
unfolding apx_def by blast

lemma "U ≠ {} ⟹ x ∈ ⋂ U ⟹ ∃ S ∈ U. x ∈ S" by auto

lemma ℛ_union: "⋃ ℛ = V" using region_cover unfolding V_def ℛ_def by auto

lemma all_dbm: "∃ M. vabstr (⋃ℛ) M ∧ normalized M"
proof -
  let ?M = "λ i j. if i = 0 then Le 0 else ∞"
  have "[?M]⇘v,n⇙ = V" unfolding V_def DBM_zone_repr_def DBM_val_bounded_def
  proof (auto, goal_cases)
    case (1 u c)
    with clock_numbering have "dbm_entry_val u None (Some c) (Le 0)" by auto
    then show ?case by auto
  next
    case (2 u c)
    from clock_numbering(1) have "0 ≠ v c" by auto
    with 2 show ?case by auto 
  next
    case (3 u c)
    from clock_numbering(1) have "0 ≠ v c" by auto
    with 3 show ?case by auto 
  next
    case (4 u c)
    with clock_numbering have "c ∈ X" by blast
    with 4(1) show ?case by auto
  next
    case (5 u c1)
    from clock_numbering(1) have "0 ≠ v c1" by auto
    with 5 show ?case by auto
  qed
  moreover have "∀ i≤n. ∀ j≤n. ?M i j ≠ ∞ ⟶ get_const (?M i j) ∈ ℤ" by auto
  moreover have "normalized ?M" unfolding normalized less_eq dbm_le_def by auto
  ultimately show ?thesis using ℛ_union by auto
qed

lemma ℛ_int:
  "R ∈ ℛ ⟹ R' ∈ ℛ ⟹ R ≠ R' ⟹ R ∩ R' = {}" using ℛ_regions_distinct by blast

lemma aux1:
  "u ∈ R ⟹ R ∈ ℛ ⟹ U ⊆ ℛ ⟹ u ∈ ⋃ U ⟹ R ⊆ ⋃ U" using ℛ_int by blast

lemma aux2: "x ∈ ⋂ U ⟹ U ≠ {} ⟹ ∃ S ∈ U. x ∈ S" by blast

lemma aux2': "x ∈ ⋂ U ⟹ U ≠ {} ⟹ ∀ S ∈ U. x ∈ S" by blast

lemma apx_subset: "Z ⊆ Approx⇩β Z" unfolding apx_def by auto

lemma aux3:
  "∀ X ∈ U. ∀ Y ∈ U. X ∩ Y ∈ U ⟹ S ⊆ U ⟹ S ≠ {} ⟹ finite S ⟹ ⋂ S ∈ U"
proof goal_cases
  case 1
  with finite_list obtain l where "set l = S" by blast
  then show ?thesis using 1
  proof (induction l arbitrary: S)
    case Nil thus ?case by auto
  next
    case (Cons x xs)
    show ?case
    proof (cases "set xs = {}")
      case False
      with Cons have "⋂(set xs) ∈ U" by auto
      with Cons.prems(1-3) show ?thesis by force
    next
      case True
      with Cons.prems show ?thesis by auto
    qed
  qed
qed

lemma empty_zone_dbm:
  "∃ M :: t DBM. vabstr {} M ∧ normalized M ∧ (∀k ≤ n. M k k ≤ Le 0)"
proof -
  from non_empty obtain c where c: "c ∈ X" by auto
  with clock_numbering have c': "v c > 0" "v c ≤ n" by auto
  let ?M = "λi j. if i = v c ∧ j = 0 ∨ i = j then Le (0::t) else if i = 0 ∧ j = v c then Lt 0 else ∞"
  have "[?M]⇘v,n⇙ = {}" unfolding DBM_zone_repr_def DBM_val_bounded_def using c' by auto
  moreover have "∀ i≤n. ∀ j≤n. ?M i j ≠ ∞ ⟶ get_const (?M i j) ∈ ℤ" by auto
  moreover have "normalized ?M" unfolding normalized less_eq dbm_le_def by auto
  ultimately show ?thesis by auto
qed

lemma valid_dbms_int:
  "∀X∈{S. ∃M. vabstr S M}. ∀Y∈{S. ∃M. vabstr S M}. X ∩ Y ∈ {S. ∃M. vabstr S M}"
proof (auto, goal_cases)
  case (1 M1 M2)
  obtain M' where M': "M' = And M1 M2" by fast
  from DBM_and_sound1[OF ] DBM_and_sound2[OF] DBM_and_complete[OF ]
  have "[M1]⇘v,n⇙ ∩ [M2]⇘v,n⇙ = [M']⇘v,n⇙" unfolding DBM_zone_repr_def M' by auto
  moreover from 1 have "∀ i≤n. ∀ j≤n. M' i j ≠ ∞ ⟶ get_const (M' i j) ∈ ℤ"
  unfolding M' by (auto split: split_min)
  ultimately show ?case by auto
qed

print_statement split_min

lemma split_min':
  "P (min i j) = ((min i j = i ⟶ P i) ∧ (min i j = j ⟶ P j))"
unfolding min_def by auto

lemma normalized_and_preservation:
  "normalized M1 ⟹ normalized M2 ⟹ normalized (And M1 M2)"
unfolding normalized by safe (subst And.simps, split split_min', fastforce)+

lemma valid_dbms_int':
  "∀X∈{S. ∃M. vabstr S M ∧ normalized M}. ∀Y∈{S. ∃M. vabstr S M ∧ normalized M}.
    X ∩ Y ∈ {S. ∃M. vabstr S M ∧ normalized M}"
proof (auto, goal_cases)
  case (1 M1 M2)
  obtain M' where M': "M' = And M1 M2" by fast
  from DBM_and_sound1 DBM_and_sound2 DBM_and_complete
  have "[M1]⇘v,n⇙ ∩ [M2]⇘v,n⇙ = [M']⇘v,n⇙" unfolding M' DBM_zone_repr_def by auto
  moreover from M' 1 have "∀ i≤n. ∀ j≤n. M' i j ≠ ∞ ⟶ get_const (M' i j) ∈ ℤ"
  by (auto split: split_min)
  moreover from normalized_and_preservation[OF 1(2,4)] have "normalized M'" unfolding M' .
  ultimately show ?case by auto
qed

lemma apx_in:
  "Z ⊆ V ⟹ Approx⇩β Z ∈ {S. ∃ U M. S = ⋃ U ∧ U ⊆ ℛ ∧ Z ⊆ S ∧ vabstr S M ∧ normalized M}"
proof -
  assume "Z ⊆ V"
  let ?A = "{S. ∃ U M. S = ⋃ U ∧ U ⊆ ℛ ∧ Z ⊆ S ∧ vabstr S M ∧ normalized M}"
  let ?U = "{R ∈ ℛ. ∀ S ∈ ?A. R ⊆ S}"
  have "?A ⊆ {S. ∃ U. S = ⋃ U ∧ U ⊆ ℛ}" by auto
  moreover from finite_ℛ have "finite …" by auto
  ultimately have "finite ?A" by (auto intro: finite_subset)
  from all_dbm obtain M where M:
    "vabstr (⋃ℛ) M" "normalized M"
  by auto
  with ‹_ ⊆ V› ℛ_union have "V ∈ ?A" by blast
  then have "?A ≠ {}" by blast
  have "?A ⊆ {S. ∃ M. vabstr S M ∧ normalized M}" by auto
  with aux3[OF valid_dbms_int' this ‹?A ≠ _› ‹finite ?A›] have
    "⋂ ?A ∈ {S. ∃ M. vabstr S M ∧ normalized M}"
  by blast
  then obtain M where *: "vabstr (Approx⇩β Z) M" "normalized M" unfolding apx_def by auto
  have "⋃ ?U = ⋂ ?A"
  proof (safe, goal_cases)
    case 1
    show ?case
    proof (cases "Z = {}")
      case False
      then obtain v where "v ∈ Z" by auto
      with region_cover ‹Z ⊆ V› obtain R where "R ∈ ℛ" "v ∈ R" unfolding V_def by blast
      with aux1[OF this(2,1)] ‹v ∈ Z› have "R ∈ ?U" by blast
      with 1 show ?thesis by blast
    next
      case True
      with empty_zone_dbm have "{} ∈ ?A" by auto
      with 1(1,3) show ?thesis by blast
    qed
  next
    case (2 v)
    from aux2[OF 2 ‹?A ≠ _›] obtain S where "v ∈ S" "S ∈ ?A" by blast
    then obtain R where "v ∈ R" "R ∈ ℛ" by auto
    { fix S assume "S ∈ ?A"
      with aux2'[OF 2 ‹?A ≠ _›] have "v ∈ S" by auto
      with ‹S ∈ ?A› obtain U M R' where *:
        "v ∈ R'" "R' ∈ ℛ" "S = ⋃U" "U ⊆ ℛ" "vabstr S M" "Z ⊆ S"
      by blast
      from aux1[OF this(1,2,4)] *(3) ‹v ∈ S› have "R' ⊆ S" by blast
      moreover from ℛ_regions_distinct[OF *(2,1) ‹R ∈ ℛ›] ‹v ∈ R› have "R' = R" by fast
      ultimately have "R ⊆ S" by fast
    }
    with ‹R ∈ ℛ› have "R ∈ ?U" by auto
    with ‹v ∈ R› show ?case by auto
  qed
  then have "Approx⇩β Z = ⋃?U" "?U ⊆ ℛ" "Z ⊆ Approx⇩β Z" unfolding apx_def by auto
  with * show ?thesis by blast
qed

lemma apx_empty:
  "Approx⇩β {} = {}"
unfolding apx_def using empty_zone_dbm by blast

end

section ‹Computing ‹β›-Approximation›

context Beta_Regions'
begin

lemma dbm_regions:
  "vabstr S M ⟹ normalized M ⟹ [M]⇘v,n⇙ ≠ {} ⟹ [M]⇘v,n⇙ ⊆ V ⟹ ∃ U ⊆ ℛ. S = ⋃ U"
proof goal_cases
  case A: 1
  let ?U =
    "{R ∈ ℛ. ∃ I J r. R = region X I J r ∧ valid_region X k I J r ∧
      (∀ c ∈ X.
        (∀ d. I c = Const d ⟶ M (v c) 0 ≥ Le d ∧ M 0 (v c) ≥ Le (-d)) ∧
        (∀ d. I c = Intv d ⟶  M (v c) 0 ≥ Lt (d + 1) ∧ M 0 (v c) ≥ Lt (-d)) ∧ 
        (I c = Greater (k c) ⟶  M (v c) 0 = ∞)
      ) ∧
      (∀ x ∈ X. ∀ y ∈ X.
        (∀ c d. I x = Intv c ∧ I y = Intv d ⟶ M (v x) (v y) ≥
          (if (x, y) ∈ r then if (y, x) ∈ r then Le (c - d) else Lt (c - d) else Lt (c - d + 1))) ∧
        (∀ c d. I x = Intv c ∧ I y = Intv d ⟶ M (v y) (v x) ≥
          (if (y, x) ∈ r then if (x, y) ∈ r then Le (d - c) else Lt (d - c) else Lt (d - c + 1))) ∧
        (∀ c d. I x = Const c ∧ I y = Const d ⟶ M (v x) (v y) ≥ Le (c - d)) ∧
        (∀ c d. I x = Const c ∧ I y = Const d ⟶ M (v y) (v x) ≥ Le (d - c)) ∧
        (∀ c d. I x = Intv c ∧ I y = Const d ⟶ M (v x) (v y) ≥ Lt (c - d + 1)) ∧
        (∀ c d. I x = Intv c ∧ I y = Const d ⟶ M (v y) (v x) ≥ Lt (d - c)) ∧
        (∀ c d. I x = Const c ∧ I y = Intv d ⟶ M (v x) (v y) ≥ Lt (c - d)) ∧
        (∀ c d. I x = Const c ∧ I y = Intv d ⟶ M (v y) (v x) ≥ Lt (d - c + 1)) ∧
        ((isGreater (I x) ∨ isGreater (I y)) ∧ J x y = Greater' (k x) ⟶ M (v x) (v y) = ∞) ∧
        (∀ c. (isGreater (I x) ∨ isGreater (I y)) ∧ J x y = Const' c
          ⟶ M (v x) (v y) ≥ Le c ∧ M (v y) (v x) ≥ Le (- c)) ∧
        (∀ c. (isGreater (I x) ∨ isGreater (I y)) ∧ J x y = Intv' c
          ⟶ M (v x) (v y) ≥ Lt (c + 1) ∧ M (v y) (v x) ≥ Lt (- c))
      )
     }"
  have "⋃ ?U = [M]⇘v,n⇙" unfolding DBM_zone_repr_def DBM_val_bounded_def
  proof (standard, goal_cases)
    case 1
    show ?case
    proof (auto, goal_cases)
      case 1
      from A(3) show "Le 0 ≼ M 0 0" unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
    next
      case (2 u I J r c)
      note B = this
      from B(6) clock_numbering have "c ∈ X" by blast
      with B(1) v_v' have *: "intv_elem c u (I c)" "v' (v c) = c" by auto
      from clock_numbering(1) have "v c > 0" by auto
      show ?case
      proof (cases "I c")
        case (Const d)
        with B(4) ‹c ∈ X› have "M 0 (v c) ≥ Le (- real d)" by auto
        with * Const show ?thesis by - (rule dbm_entry_val_mono_2[folded less_eq], auto)
      next
        case (Intv d)
        with B(4) ‹c ∈ X› have "M 0 (v c) ≥ Lt (- real d)" by auto
        with * Intv show ?thesis by - (rule dbm_entry_val_mono_2[folded less_eq], auto)
      next
        case (Greater d)
        with B(3) ‹c ∈ X› have "I c = Greater (k c)" by fastforce
        with * have "- u c < - k c" by auto
        moreover from A(2) *(2) ‹v c ≤ n› ‹v c > 0› have
          "Lt (- k c) ≤ M 0 (v c)"
        unfolding normalized by force
        ultimately show ?thesis by - (rule dbm_entry_val_mono_2[folded less_eq], auto)
      qed
    next
      case (3 u I J r c)
      note B = this
      from B(6) clock_numbering have "c ∈ X" by blast
      with B(1) v_v' have *: "intv_elem c u (I c)" "v' (v c) = c" by auto
      from clock_numbering(1) have "v c > 0" by auto
      show ?case
      proof (cases "I c")
        case (Const d)
        with B(4) ‹c ∈ X› have "M (v c) 0 ≥ Le d" by auto
        with * Const show ?thesis by - (rule dbm_entry_val_mono_3[folded less_eq], auto)
      next
        case (Intv d)
        with B(4) ‹c ∈ X› have "M (v c) 0 ≥ Lt (real d + 1)" by auto
        with * Intv show ?thesis by - (rule dbm_entry_val_mono_3[folded less_eq], auto)
      next
        case (Greater d)
        with B(3) ‹c ∈ X› have "I c = Greater (k c)" by fastforce
        with B(4) ‹c ∈ X› show ?thesis by auto
      qed
    next
      case B: (4 u I J r c1 c2)
      from B(6,7) clock_numbering have "c1 ∈ X" "c2 ∈ X" by blast+
      with B(1) v_v' have *:
        "intv_elem c1 u (I c1)" "intv_elem c2 u (I c2)" "v' (v c1) = c1" "v' (v c2) = c2"
      by auto
      from clock_numbering(1) have "v c1 > 0" "v c2 > 0" by auto
      { assume C: "isGreater (I c1) ∨ isGreater (I c2)"
        with B(1) ‹c1 ∈ X› ‹c2 ∈ X› have **: "intv'_elem c1 c2 u (J c1 c2)" by force
        have ?case
        proof (cases "J c1 c2")
          case (Smaller' c)
          with C B(3) ‹c1 ∈ X› ‹c2 ∈ X› have "c ≤ - k c2" by fastforce
          moreover from C ‹c1 ∈ X› ‹c2 ∈ X› ** Smaller' have "u c1 - u c2 < c" by auto
          moreover from A(2) *(3,4) B(6,7) ‹v c1 > 0› ‹v c2 > 0› have
            "M (v c1) (v c2) ≥ Lt (- k c2) ∨ M (v c1) (v c2) = ∞"
          unfolding normalized by fastforce
          ultimately show ?thesis by (safe) (rule dbm_entry_val_mono_1[folded less_eq], auto)
        next
          case (Const' c)
          with C B(5) ‹c1 ∈ X› ‹c2 ∈ X› have "M (v c1) (v c2) ≥ Le c" by auto
          with Const' ** ‹c1 ∈ X› ‹c2 ∈ X› show ?thesis
          by (auto intro: dbm_entry_val_mono_1[folded less_eq])
        next
          case (Intv' c)
          with C B(5) ‹c1 ∈ X› ‹c2 ∈ X› have "M (v c1) (v c2) ≥ Lt (real_of_int c + 1)" by auto
          with Intv' ** ‹c1 ∈ X› ‹c2 ∈ X› show ?thesis
          by (auto intro: dbm_entry_val_mono_1[folded less_eq])
        next
          case (Greater' c)
          with C B(3) ‹c1 ∈ X› ‹c2 ∈ X› have "c = k c1" by fastforce
          with Greater' C B(5) ‹c1 ∈ X› ‹c2 ∈ X› show ?thesis by auto
        qed
      } note GreaterI = this
      show ?case
      proof (cases "I c1")
        case (Const c)
        show ?thesis
        proof (cases "I c2", goal_cases)
          case (1 d)
          with Const ‹c1 ∈ X› ‹c2 ∈ X› *(1,2) have "u c1 = c" "u c2 = d" by auto
          moreover from ‹c1 ∈ X› ‹c2 ∈ X› 1 Const B(5) have
            "Le (real c - real d) ≤ M (v c1) (v c2)"
          by meson
          ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
        next
          case (Intv d)
          with Const ‹c1 ∈ X› ‹c2 ∈ X› *(1,2) have "u c1 = c" "d < u c2" by auto
          then have "u c1 - u c2 < c - real d" by auto
          moreover from Const ‹c1 ∈ X› ‹c2 ∈ X› Intv B(5) have
            "Lt (real c - d) ≤ M (v c1) (v c2)"
          by meson
          ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
        next
          case Greater then show ?thesis by (auto intro: GreaterI)
        qed
      next
        case (Intv c)
        show ?thesis
        proof (cases "I c2", goal_cases)
          case (Const d)
          with Intv ‹c1 ∈ X› ‹c2 ∈ X› *(1,2) have "u c1 < c + 1" "d = u c2" by auto
          then have "u c1 - u c2 < c - real d + 1" by auto
          moreover from ‹c1 ∈ X› ‹c2 ∈ X› Intv Const B(5) have
            "Lt (real c - real d + 1) ≤ M (v c1) (v c2)"
          by meson
          ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
        next
          case (2 d)
          show ?case
          proof (cases "(c1,c2) ∈ r")
            case True
            note T = this
            show ?thesis
            proof (cases "(c2,c1) ∈ r")
              case True
              with T B(5) 2 Intv ‹c1 ∈ X› ‹c2 ∈ X› have
                "Le (real c - real d) ≤ M (v c1) (v c2)"
              by auto
              moreover from nat_intv_frac_decomp[of c "u c1"] nat_intv_frac_decomp[of d "u c2"]
                            B(1,2) ‹c1 ∈ X› ‹c2 ∈ X› T True Intv 2 *(1,2)
              have "u c1 - u c2 = real c - d" by auto
              ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
            next
              case False
              with T B(5) 2 Intv ‹c1 ∈ X› ‹c2 ∈ X› have
                "Lt (real c - real d) ≤ M (v c1) (v c2)"
              by auto
              moreover from nat_intv_frac_decomp[of c "u c1"] nat_intv_frac_decomp[of d "u c2"]
                            B(1,2) ‹c1 ∈ X› ‹c2 ∈ X› T False Intv 2 *(1,2)
              have "u c1 - u c2 < real c - d" by auto
              ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
            qed
          next
            case False
            with B(5) 2 Intv ‹c1 ∈ X› ‹c2 ∈ X› have
                "Lt (real c - real d + 1) ≤ M (v c1) (v c2)"
            by meson
            moreover from 2 Intv ‹c1 ∈ X› ‹c2 ∈ X› * have "u c1 - u c2 < c - real d + 1" by auto
            ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
          qed
        next
          case Greater then show ?thesis by (auto intro: GreaterI)
        qed
      next
        case Greater then show ?thesis by (auto intro: GreaterI)
      qed
    qed
  next
    case 2 show ?case
    proof (safe, goal_cases)
      case (1 u)
      with A(4) have "u ∈ V" unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
      with region_cover obtain R where "R ∈ ℛ" "u ∈ R" unfolding V_def by auto
      then obtain I J r where R: "R = region X I J r" "valid_region X k I J r" unfolding ℛ_def by auto
      have "(∀c∈X. (∀d. I c = Const d ⟶ Le (real d) ≤ M (v c) 0 ∧ Le (- real d) ≤ M 0 (v c)) ∧
                 (∀d. I c = Intv d ⟶ Lt (real d + 1) ≤ M (v c) 0 ∧ Lt (- real d) ≤ M 0 (v c)) ∧
                 (I c = Greater (k c) ⟶ M (v c) 0 = ∞))"
      proof safe
        fix c assume "c ∈ X"
        with R ‹u ∈ R› have *: "intv_elem c u (I c)" by auto
        fix d assume **: "I c = Const d"
        with * have "u c = d" by fastforce
        moreover from ** clock_numbering(3) ‹c ∈ X› 1 have
          "dbm_entry_val u (Some c) None (M (v c) 0)"
        by auto
        ultimately show "Le (real d) ≤ M (v c) 0"
        unfolding less_eq dbm_le_def by (cases "M (v c) 0") auto
      next
        fix c assume "c ∈ X"
        with R ‹u ∈ R› have *: "intv_elem c u (I c)" by auto
        fix d assume **: "I c = Const d"
        with * have "u c = d" by fastforce
        moreover from ** clock_numbering(3) ‹c ∈ X› 1 have
          "dbm_entry_val u None (Some c) (M 0 (v c))"
        by auto
        ultimately show "Le (- real d) ≤ M 0 (v c)"
        unfolding less_eq dbm_le_def by (cases "M 0 (v c)") auto
      next
        fix c assume "c ∈ X"
        with R ‹u ∈ R› have *: "intv_elem c u (I c)" by auto
        fix d assume **: "I c = Intv d"
        with * have "d < u c" "u c < d + 1" by fastforce+
        moreover from ** clock_numbering(3) ‹c ∈ X› 1 have
          "dbm_entry_val u (Some c) None (M (v c) 0)"
        by auto
        moreover have
          "M (v c) 0 ≠ ∞ ⟹ get_const (M (v c) 0) ∈ ℤ"
        using ‹c ∈ X› clock_numbering A(1) by auto
        ultimately show "Lt (real d + 1) ≤ M (v c) 0" unfolding less_eq dbm_le_def
        apply (cases "M (v c) 0")
          apply auto
         apply (rename_tac x1)
         apply (subgoal_tac "x1 > d")
          apply (rule dbm_lt.intros(5))
          apply (metis nat_intv_frac_gt0 frac_eq_0_iff less_irrefl linorder_not_le of_nat_1 of_nat_add)
         apply simp
        apply (rename_tac x2)
        apply (subgoal_tac "x2 > d + 1")
         apply (rule dbm_lt.intros(6))
         apply (metis of_nat_1 of_nat_add)
        apply simp
        by (metis nat_intv_not_int One_nat_def add.commute add.right_neutral add_Suc_right le_less_trans
                  less_eq_real_def linorder_neqE_linordered_idom semiring_1_class.of_nat_simps(2))
      next
        fix c assume "c ∈ X"
        with R ‹u ∈ R› have *: "intv_elem c u (I c)" by auto
        fix d assume **: "I c = Intv d"
        with * have "d < u c" "u c < d + 1" by fastforce+
        moreover from ** clock_numbering(3) ‹c ∈ X› 1 have
          "dbm_entry_val u None (Some c) (M 0 (v c))"
        by auto
        moreover have "M 0 (v c) ≠ ∞ ⟹ get_const (M 0 (v c)) ∈ ℤ" using ‹c ∈ X› clock_numbering A(1) by auto
        ultimately show "Lt (- real d) ≤ M 0 (v c)" unfolding less_eq dbm_le_def
          proof (cases "M 0 (v c)", -, auto, goal_cases)
            case prems: (1 x1)
            then have "u c = d + frac (u c)" by (metis nat_intv_frac_decomp ‹u c < d + 1›) 
            with prems(5) have "- x1 ≤ d + frac (u c)" by auto
            with prems(1) frac_ge_0 frac_lt_1 have "- x1 ≤ d"
            by - (rule ints_le_add_frac2[of "frac (u c)" d "-x1"]; fastforce)
            with prems have "- d ≤ x1" by auto
            then show ?case by auto
          next
            case prems: (2 x1)
            then have "u c = d + frac (u c)" by (metis nat_intv_frac_decomp ‹u c < d + 1›) 
            with prems(5) have "- x1 ≤ d + frac (u c)" by auto
            with prems(1) frac_ge_0 frac_lt_1 have "- x1 ≤ d"
            by - (rule ints_le_add_frac2[of "frac (u c)" d "-x1"]; fastforce)
            with prems(6) have "- d < x1" by auto
            then show ?case by auto
        qed
      next
        fix c assume "c ∈ X"
        with R ‹u ∈ R› have *: "intv_elem c u (I c)" by auto
        fix d assume **: "I c = Greater (k c)"
        have "M (v c) 0 ≤ Le ((k o v') (v c)) ∨ M (v c) 0 = ∞"
        using A(2) ‹c ∈ X› clock_numbering unfolding normalized by auto
        with v_v' ‹c ∈ X› have "M (v c) 0 ≤ Le (k c) ∨ M (v c) 0 = ∞" by auto
        moreover from * ** have "k c < u c" by fastforce
        moreover from ** clock_numbering(3) ‹c ∈ X› 1 have
          "dbm_entry_val u (Some c) None (M (v c) 0)"
        by auto
        moreover have
          "M (v c) 0 ≠ ∞ ⟹ get_const (M (v c) 0) ∈ ℤ"
        using ‹c ∈ X› clock_numbering A(1) by auto
        ultimately show "M (v c) 0 = ∞" unfolding less_eq dbm_le_def
          apply -
          apply (rule ccontr)
          using ** apply (cases "M (v c) 0")
        by auto
      qed
      moreover
      { fix x y assume X: "x ∈ X" "y ∈ X"
        with R ‹u ∈ R› have *: "intv_elem x u (I x)" "intv_elem y u (I y)" by auto
        from X R ‹u ∈ R› have **:
          "isGreater (I x) ∨ isGreater (I y) ⟶ intv'_elem x y u (J x y)"
        by force
        have int: "M (v x) (v y) ≠ ∞ ⟹ get_const (M (v x) (v y)) ∈ ℤ" using X clock_numbering A(1)
        by auto
        have int2: "M (v y) (v x) ≠ ∞ ⟹ get_const (M (v y) (v x)) ∈ ℤ" using X clock_numbering A(1)
        by auto
        from 1 clock_numbering(3) X 1 have ***:
          "dbm_entry_val u (Some x) (Some y) (M (v x) (v y))"
          "dbm_entry_val u (Some y) (Some x) (M (v y) (v x))"
        by auto
        have
         "(∀ c d. I x = Intv c ∧ I y = Intv d ⟶ M (v x) (v y) ≥
            (if (x, y) ∈ r then if (y, x) ∈ r then Le (c - d) else Lt (c - d) else Lt (c - d + 1))) ∧
          (∀ c d. I x = Intv c ∧ I y = Intv d ⟶ M (v y) (v x) ≥
            (if (y, x) ∈ r then if (x, y) ∈ r then Le (d - c) else Lt (d - c) else Lt (d - c + 1))) ∧
          (∀ c d. I x = Const c ∧ I y = Const d ⟶ M (v x) (v y) ≥ Le (c - d)) ∧
          (∀ c d. I x = Const c ∧ I y = Const d ⟶ M (v y) (v x) ≥ Le (d - c)) ∧
          (∀ c d. I x = Intv c ∧ I y = Const d ⟶ M (v x) (v y) ≥ Lt (c - d + 1)) ∧
          (∀ c d. I x = Intv c ∧ I y = Const d ⟶ M (v y) (v x) ≥ Lt (d - c)) ∧
          (∀ c d. I x = Const c ∧ I y = Intv d ⟶ M (v x) (v y) ≥ Lt (c - d)) ∧
          (∀ c d. I x = Const c ∧ I y = Intv d ⟶ M (v y) (v x) ≥ Lt (d - c + 1)) ∧
          ((isGreater (I x) ∨ isGreater (I y)) ∧ J x y = Greater' (k x) ⟶ M (v x) (v y) = ∞) ∧
          (∀ c. (isGreater (I x) ∨ isGreater (I y)) ∧ J x y = Const' c
            ⟶ M (v x) (v y) ≥ Le c ∧ M (v y) (v x) ≥ Le (- c)) ∧
          (∀ c. (isGreater (I x) ∨ isGreater (I y)) ∧ J x y = Intv' c
            ⟶ M (v x) (v y) ≥ Lt (c + 1) ∧ M (v y) (v x) ≥ Lt (- c))"
        proof (auto, goal_cases)
          case **: (1 c d)
          with R ‹u ∈ R› X have "frac (u x) = frac (u y)" by auto
          with * ** nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have
            "u x - u y = real c - d"
          by auto
          with *** show ?case unfolding less_eq dbm_le_def by (cases "M (v x) (v y)") auto
        next
          case **: (2 c d)
          with R ‹u ∈ R› X have "frac (u x) > frac (u y)" by auto
          with * ** nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have
            "real c - d < u x - u y" "u x - u y < real c - d + 1"
          by auto
          with *** int show ?case unfolding less_eq dbm_le_def
          by (cases "M (v x) (v y)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        next
          case **: (3 c d)
          from ** R ‹u ∈ R› X have "frac (u x) < frac (u y)" by auto
          with * ** nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have
            "real c - d - 1 < u x - u y" "u x - u y < real c - d"
          by auto
          with *** int show ?case unfolding less_eq dbm_le_def
          by (cases "M (v x) (v y)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        next
          case (4 c d) with R(1) ‹u ∈ R› X show ?case by auto
        next
          case **: (5 c d)
          with R ‹u ∈ R› X have "frac (u x) = frac (u y)" by auto
          with * ** nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have
            "u x - u y = real c - d" by auto
          with *** show ?case unfolding less_eq dbm_le_def by (cases "M (v y) (v x)") auto
        next
          case **: (6 c d)
          from ** R ‹u ∈ R› X have "frac (u x) < frac (u y)" by auto
          with * ** nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have
            "real d - c < u y - u x" "u y - u x < real d - c + 1"
          by auto
          with *** int2 show ?case unfolding less_eq dbm_le_def
          by (cases "M (v y) (v x)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        next
          case **: (7 c d)
          from ** R ‹u ∈ R› X have "frac (u x) > frac (u y)" by auto
          with * ** nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have
            "real d - c - 1 < u y - u x" "u y - u x < real d - c"
          by auto
          with *** int2 show ?case unfolding less_eq dbm_le_def
          by (cases "M (v y) (v x)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        next
          case (8 c d) with R(1) ‹u ∈ R› X show ?case by auto
        next
          case (9 c d)
          with * nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have 
            "u x - u y = real c - d" by auto
          with *** show ?case unfolding less_eq dbm_le_def by (cases "M (v x) (v y)") auto
        next
          case (10 c d)
          with * nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have
            "u x - u y = real c - d"
          by auto
          with *** show ?case unfolding less_eq dbm_le_def by (cases "M (v y) (v x)") auto
        next
          case (11 c d)
          with * nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have
            "real c - d < u x - u y"
          by auto
          with *** int show ?case unfolding less_eq dbm_le_def
          by (cases "M (v x) (v y)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        next
          case (12 c d)
          with * nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have
            "real d - c - 1 < u y - u x"
          by auto
          with *** int2 show ?case unfolding less_eq dbm_le_def
          by (cases "M (v y) (v x)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        next
          case (13 c d)
          with * nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have
            "real c - d - 1 < u x - u y"
          by auto
          with *** int show ?case unfolding less_eq dbm_le_def
          by (cases "M (v x) (v y)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        next
          case (14 c d)
          with * nat_intv_frac_decomp[of c "u x"] nat_intv_frac_decomp[of d "u y"] have
            "real d - c < u y - u x"
          by auto
          with *** int2 show ?case unfolding less_eq dbm_le_def
          by (cases "M (v y) (v x)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        next
          case (15 d)
          have "M (v x) (v y) ≤ Le ((k o v') (v x)) ∨ M (v x) (v y) = ∞"
          using A(2) X clock_numbering unfolding normalized by auto
          with v_v' X have "M (v x) (v y) ≤ Le (k x) ∨ M (v x) (v y) = ∞" by auto
          moreover from 15 * ** have "u x - u y > k x" by auto
          ultimately show ?case unfolding less_eq dbm_le_def using *** by (cases "M (v x) (v y)", auto)
        next
          case (16 d)
          have "M (v x) (v y) ≤ Le ((k o v') (v x)) ∨ M (v x) (v y) = ∞"
          using A(2) X clock_numbering unfolding normalized by auto
          with v_v' X have "M (v x) (v y) ≤ Le (k x) ∨ M (v x) (v y) = ∞" by auto
          moreover from 16 * ** have "u x - u y > k x" by auto
          ultimately show ?case unfolding less_eq dbm_le_def using *** by (cases "M (v x) (v y)", auto)
        next
          case 17 with ** *** show ?case unfolding less_eq dbm_le_def by (cases "M (v x) (v y)", auto)
        next
          case 18 with ** *** show ?case unfolding less_eq dbm_le_def by (cases "M (v y) (v x)", auto)
        next
          case 19 with ** *** show ?case unfolding less_eq dbm_le_def by (cases "M (v x) (v y)", auto)
        next
          case 20 with ** *** show ?case unfolding less_eq dbm_le_def by (cases "M (v y) (v x)", auto)
        next
          case (21 c d)
          with ** have "c < u x - u y" by auto
          with *** int show ?case unfolding less_eq dbm_le_def
          by (cases "M (v x) (v y)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        next
          case (22 c d)
          with ** have "u x - u y < c + 1" by auto
          then have "u y - u x > - c - 1" by auto
          with *** int2 show ?case unfolding less_eq dbm_le_def
          by (cases "M (v y) (v x)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        next
          case (23 c d)
          with ** have "c < u x - u y" by auto
          with *** int show ?case unfolding less_eq dbm_le_def
          by (cases "M (v x) (v y)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        next
          case (24 c d)
          with ** have "u x - u y < c + 1" by auto
          then have "u y - u x > - c - 1" by auto
          with *** int2 show ?case unfolding less_eq dbm_le_def
          by (cases "M (v y) (v x)", auto) (fastforce intro: int_lt_Suc_le int_lt_neq_prev_lt)+
        qed
      }
      ultimately show ?case using R ‹u ∈ R› ‹R ∈ ℛ›
        apply -
        apply standard
         apply standard
         apply rule
          apply assumption
         apply (rule exI[where x = I], rule exI[where x = J], rule exI[where x = r])
      by auto
    qed
  qed
  with A have "S = ⋃?U" by auto
  moreover have "?U ⊆ ℛ" by blast
  ultimately show ?case by blast
qed

lemma dbm_regions':
  "vabstr S M ⟹ normalized M ⟹ S ⊆ V ⟹ ∃ U ⊆ ℛ. S = ⋃ U"
using dbm_regions by (cases "S = {}") auto

lemma dbm_regions'':
  "dbm_int M n ⟹ normalized M ⟹ [M]⇘v,n⇙ ⊆ V ⟹ ∃ U ⊆ ℛ. [M]⇘v,n⇙ = ⋃ U"
using dbm_regions' by auto

lemma canonical_saturated_1:
  assumes "Le r ≤ M (v c1) 0"
    and "Le (- r) ≤ M 0 (v c1)"
    and "cycle_free M n"
    and "canonical M n"
    and "v c1 ≤ n"
    and "v c1 > 0"
    and "∀c. v c ≤ n ⟶ 0 < v c"
  obtains u where "u ∈ [M]⇘v,n⇙" "u c1 = r"
proof -
  let ?M' = "λi' j'. if i'=v c1 ∧ j'=0 then Le r else if i'=0 ∧ j'=v c1 then Le (- r) else M i' j'"
  from fix_index'[OF assms(1-5)] assms(6) have M':
    "∀u. DBM_val_bounded v u ?M' n ⟶ DBM_val_bounded v u M n"
    "cycle_free ?M' n" "?M' (v c1) 0 = Le r" "?M' 0 (v c1) = Le (- r)"
  by auto
  with cyc_free_obtains_valuation[unfolded cycle_free_diag_equiv, of ?M' n v] assms(7) obtain u where
    u: "DBM_val_bounded v u ?M' n"
  by fastforce
  with assms(5,6) M'(3,4) have "u c1 = r" unfolding DBM_val_bounded_def by fastforce
  moreover from u M'(1) have "u ∈ [M]⇘v,n⇙" unfolding DBM_zone_repr_def by auto
  ultimately show thesis by (auto intro: that)
qed

lemma canonical_saturated_2:
  assumes "Le r ≤ M 0 (v c2)"
    and "Le (- r) ≤ M (v c2) 0"
    and "cycle_free M n"
    and "canonical M n"
    and "v c2 ≤ n"
    and "v c2 > 0"
    and "∀c. v c ≤ n ⟶ 0 < v c"
  obtains u where "u ∈ [M]⇘v,n⇙" "u c2 = - r"
proof -
  let ?M' = "λi' j'. if i'=0 ∧ j'=v c2 then Le r else if i'=v c2 ∧ j'=0 then Le (-r) else M i' j'"
  from fix_index'[OF assms(1-4)] assms(5,6) have M':
    "∀u. DBM_val_bounded v u ?M' n ⟶ DBM_val_bounded v u M n"
    "cycle_free ?M' n" "?M' 0 (v c2) = Le r" "?M' (v c2) 0 = Le (- r)"
  by auto
  with cyc_free_obtains_valuation[unfolded cycle_free_diag_equiv, of ?M' n v] assms(7) obtain u where
    u: "DBM_val_bounded v u ?M' n"
  by fastforce
  with assms(5,6) M'(3,4) have "u c2 ≤ -r" "- u c2 ≤ r" unfolding DBM_val_bounded_def by fastforce+
  then have "u c2 = -r" by (simp add: le_minus_iff)
  moreover from u M'(1) have "u ∈ [M]⇘v,n⇙" unfolding DBM_zone_repr_def by auto
  ultimately show thesis by (auto intro: that)
qed

lemma canonical_saturated_3:
  assumes "Le r ≤ M (v c1) (v c2)"
    and "Le (- r) ≤ M (v c2) (v c1)"
    and "cycle_free M n"
    and "canonical M n"
    and "v c1 ≤ n" "v c2 ≤ n"
    and "v c1 ≠ v c2"
    and "∀c. v c ≤ n ⟶ 0 < v c"
  obtains u where "u ∈ [M]⇘v,n⇙" "u c1 - u c2 = r"
proof -
  let ?M'="λi' j'. if i'=v c1 ∧ j'=v c2 then Le r else if i'=v c2 ∧ j'=v c1 then Le (-r) else M i' j'"
  from fix_index'[OF assms(1-7), of v] assms(7,8) have M':
    "∀u. DBM_val_bounded v u ?M' n ⟶ DBM_val_bounded v u M n"
    "cycle_free ?M' n" "?M' (v c1) (v c2) = Le r" "?M' (v c2) (v c1) = Le (- r)"
  by auto
  with cyc_free_obtains_valuation[unfolded cycle_free_diag_equiv, of ?M' n v] assms obtain u where u:
    "DBM_val_bounded v u ?M' n"
  by fastforce
  with assms(5,6) M'(3,4) have
    "u c1 - u c2 ≤ r" "u c2 - u c1 ≤ - r"
  unfolding DBM_val_bounded_def by fastforce+
  then have "u c1 - u c2 = r" by (simp add: le_minus_iff)
  moreover from u M'(1) have "u ∈ [M]⇘v,n⇙" unfolding DBM_zone_repr_def by auto
  ultimately show thesis by (auto intro: that)
qed

lemma DBM_canonical_subset_le:
  notes any_le_inf[intro]
  fixes M :: "t DBM"
  assumes "canonical M n" "[M]⇘v,n⇙ ⊆ [M']⇘v,n⇙" "[M]⇘v,n⇙ ≠ {}" "i ≤ n" "j ≤ n" "i ≠ j"
  shows "M i j ≤ M' i j"
proof -
  from non_empty_cycle_free[OF assms(3)] clock_numbering(2) have "cycle_free M n" by auto
  with assms(1,4,5) have non_neg:
    "M i j + M j i ≥ Le 0"
  by (metis cycle_free_diag order.trans neutral)
  
  from clock_numbering have cn: "∀c. v c ≤ n ⟶ 0 < v c" by auto
  show ?thesis
  proof (cases "i = 0")
    case True
    show ?thesis
    proof (cases "j = 0")
      case True
      with assms ‹i = 0› show ?thesis
      unfolding neutral DBM_zone_repr_def DBM_val_bounded_def less_eq by auto
    next
      case False
      then have "j > 0" by auto
      with ‹j ≤ n› clock_numbering obtain c2 where c2: "v c2 = j" by auto
      note t = canonical_saturated_2[OF _ _ ‹cycle_free M n› assms(1) assms(5)[folded c2] _ cn,unfolded c2]
      show ?thesis
      proof (rule ccontr, goal_cases)
        case 1
        { fix d assume 1: "M 0 j = ∞"
          obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "d < r"
          proof (cases "M j 0")
            case (Le d')
            obtain r where "r > - d'" using gt_ex by blast
            with Le 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
          next
            case (Lt d')
            obtain r where "r > - d'" using gt_ex by blast
            with Lt 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
          next
            case INF
            with 1 show ?thesis by (intro that[of "d + 1"]) auto
          qed
          then have "∃ r. Le r ≤ M 0 j ∧ Le (-r) ≤ M j 0 ∧ d < r" by auto
        } note inf_case = this
        { fix a b d :: real assume 1: "a < b" assume b: "b + d > 0"
          then have *: "b > -d" by auto
          obtain r where "r > - d" "r > a" "r < b"
          proof (cases "a ≥ - d")
            case True
            from 1 obtain r where "r > a" "r < b" using dense by auto
            with True show ?thesis by (auto intro: that[of r])
          next
            case False
            with * obtain r where "r > -d" "r < b" using dense by auto
            with False show ?thesis by (auto intro: that[of r])
          qed
          then have "∃ r. r > -d ∧ r > a ∧ r < b" by auto
        } note gt_case = this
        { fix a r assume r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "a < r" "M' 0 j = Le a ∨ M' 0 j = Lt a"
          from t[OF this(1,2) ‹0 < j›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c2 = - r" .
          with ‹j ≤ n› c2 assms(2) have "dbm_entry_val u None (Some c2) (M' 0 j)"
          unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
          with u(2) r(3,4) have False by auto
        } note contr = this
        from 1 True have "M' 0 j < M 0 j" by auto
        then show False unfolding less
        proof (cases rule: dbm_lt.cases)
          case (1 d)
          with inf_case obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "d < r" by auto
          from contr[OF this] 1 show False by fast
        next
          case (2 d)
          with inf_case obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "d < r" by auto
          from contr[OF this] 2 show False by fast
        next
          case (3 a b)
          obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "a < r"
          proof (cases "M j 0")
            case (Le d')
            with 3 non_neg ‹i = 0› have "b + d' ≥ 0" unfolding mult by auto
            then have "b ≥ - d'" by auto
            with 3 obtain r where "r ≥ - d'" "r > a" "r ≤ b" by blast
            with Le 3 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d')
            with 3 non_neg ‹i = 0› have "b + d' > 0" unfolding mult by auto
            from gt_case[OF 3(3) this] obtain r where "r > - d'" "r > a" "r ≤ b" by auto
            with Lt 3 show ?thesis by (intro that[of r]) auto
          next
            case INF
            with 3 show ?thesis by (intro that[of b]) auto
          qed
          from contr[OF this] 3 show False by fast
        next
          case (4 a b)
          obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "a < r"
          proof (cases "M j 0")
            case (Le d)
            with 4 non_neg ‹i = 0› have "b + d > 0" unfolding mult by auto
            from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Le 4 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d)
            with 4 non_neg ‹i = 0› have "b + d > 0" unfolding mult by auto
            from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Lt 4 show ?thesis by (intro that[of r]) auto
          next
            case INF
            from 4 dense obtain r where "r > a" "r < b" by auto
            with 4 INF show ?thesis by (intro that[of r]) auto
          qed
          from contr[OF this] 4 show False by fast
        next
          case (5 a b)
          obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "a ≤ r"
          proof (cases "M j 0")
            case (Le d')
            with 5 non_neg ‹i = 0› have "b + d' ≥ 0" unfolding mult by auto
            then have "b ≥ - d'" by auto
            with 5 obtain r where "r ≥ - d'" "r ≥ a" "r ≤ b" by blast
            with Le 5 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d')
            with 5 non_neg ‹i = 0› have "b + d' > 0" unfolding mult by auto
            then have "b > - d'" by auto
            with 5 obtain r where "r > - d'" "r ≥ a" "r ≤ b" by blast
            with Lt 5 show ?thesis by (intro that[of r]) auto
          next
            case INF
            with 5 show ?thesis by (intro that[of b]) auto
          qed
          from t[OF this(1,2) ‹j > 0›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c2 = - r" .
          with ‹j ≤ n› c2 assms(2) have "dbm_entry_val u None (Some c2) (M' 0 j)"
          unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
          with u(2) r(3) 5 show False by auto
        next
          case (6 a b)
          obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "a < r"
          proof (cases "M j 0")
            case (Le d)
            with 6 non_neg ‹i = 0› have "b + d > 0" unfolding mult by auto
            from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Le 6 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d)
            with 6 non_neg ‹i = 0› have "b + d > 0" unfolding mult by auto
            from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Lt 6 show ?thesis by (intro that[of r]) auto
          next
            case INF
            from 6 dense obtain r where "r > a" "r < b" by auto
            with 6 INF show ?thesis by (intro that[of r]) auto
          qed
          from contr[OF this] 6 show False by fast
        qed
      qed
    qed
  next
    case False
    then have "i > 0" by auto
    with ‹i ≤ n› clock_numbering obtain c1 where c1: "v c1 = i" by auto
    show ?thesis
    proof (cases "j = 0")
      case True
      note t = canonical_saturated_1[OF _ _ ‹cycle_free M n› assms(1) assms(4)[folded c1] _ cn,
                                     unfolded c1]
      show ?thesis
      proof (rule ccontr, goal_cases)
        case 1
        { fix d assume 1: "M i 0 = ∞"
          obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "d < r"
          proof (cases "M 0 i")
            case (Le d')
            obtain r where "r > - d'" using gt_ex by blast
            with Le 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
          next
            case (Lt d')
            obtain r where "r > - d'" using gt_ex by blast
            with Lt 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
          next
            case INF
            with 1 show ?thesis by (intro that[of "d + 1"]) auto
          qed
          then have "∃ r. Le r ≤ M i 0 ∧ Le (-r) ≤ M 0 i ∧ d < r" by auto
        } note inf_case = this
        { fix a b d :: real assume 1: "a < b" assume b: "b + d > 0"
          then have *: "b > -d" by auto
          obtain r where "r > - d" "r > a" "r < b"
          proof (cases "a ≥ - d")
            case True
            from 1 obtain r where "r > a" "r < b" using dense by auto
            with True show ?thesis by (auto intro: that[of r])
          next
            case False
            with * obtain r where "r > -d" "r < b" using dense by auto
            with False show ?thesis by (auto intro: that[of r])
          qed
          then have "∃ r. r > -d ∧ r > a ∧ r < b" by auto
        } note gt_case = this
        { fix a r assume r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "a < r" "M' i 0 = Le a ∨ M' i 0 = Lt a"
          from t[OF this(1,2) ‹i > 0›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c1 = r" .
          with ‹i ≤ n› c1 assms(2) have "dbm_entry_val u (Some c1) None (M' i 0)"
          unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
          with u(2) r(3,4) have False by auto
        } note contr = this
        from 1 True have "M' i 0 < M i 0" by auto
        then show False unfolding less
        proof (cases rule: dbm_lt.cases)
          case (1 d)
          with inf_case obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "d < r" by auto
          from contr[OF this] 1 show False by fast
        next
          case (2 d)
          with inf_case obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "d < r" by auto
          from contr[OF this] 2 show False by fast
        next
          case (3 a b)
          obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "a < r"
          proof (cases "M 0 i")
            case (Le d')
            with 3 non_neg ‹j = 0› have "b + d' ≥ 0" unfolding mult by auto
            then have "b ≥ - d'" by auto
            with 3 obtain r where "r ≥ - d'" "r > a" "r ≤ b" by blast
            with Le 3 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d')
            with 3 non_neg ‹j = 0› have "b + d' > 0" unfolding mult by auto
            from gt_case[OF 3(3) this] obtain r where "r > - d'" "r > a" "r ≤ b" by auto
            with Lt 3 show ?thesis by (intro that[of r]) auto
          next
            case INF
            with 3 show ?thesis by (intro that[of b]) auto
          qed
          from contr[OF this] 3 show False by fast
        next
          case (4 a b)
          obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "a < r"
          proof (cases "M 0 i")
            case (Le d)
            with 4 non_neg ‹j = 0› have "b + d > 0" unfolding mult by auto
            from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Le 4 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d)
            with 4 non_neg ‹j = 0› have "b + d > 0" unfolding mult by auto
            from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Lt 4 show ?thesis by (intro that[of r]) auto
          next
            case INF
            from 4 dense obtain r where "r > a" "r < b" by auto
            with 4 INF show ?thesis by (intro that[of r]) auto
          qed
          from contr[OF this] 4 show False by fast
        next
          case (5 a b)
          obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "a ≤ r"
          proof (cases "M 0 i")
            case (Le d')
            with 5 non_neg ‹j = 0› have "b + d' ≥ 0" unfolding mult by auto
            then have "b ≥ - d'" by auto
            with 5 obtain r where "r ≥ - d'" "r ≥ a" "r ≤ b" by blast
            with Le 5 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d')
            with 5 non_neg ‹j = 0› have "b + d' > 0" unfolding mult by auto
            then have "b > - d'" by auto
            with 5 obtain r where "r > - d'" "r ≥ a" "r ≤ b" by blast
            with Lt 5 show ?thesis by (intro that[of r]) auto
          next
            case INF
            with 5 show ?thesis by (intro that[of b]) auto
          qed
          from t[OF this(1,2) ‹i > 0›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c1 = r" .
          with ‹i ≤ n› c1 assms(2) have "dbm_entry_val u (Some c1) None (M' i 0)"
          unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
          with u(2) r(3) 5 show False by auto
        next
          case (6 a b)
          obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "a < r"
          proof (cases "M 0 i")
            case (Le d)
            with 6 non_neg ‹j = 0› have "b + d > 0" unfolding mult by auto
            from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Le 6 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d)
            with 6 non_neg ‹j = 0› have "b + d > 0" unfolding mult by auto
            from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Lt 6 show ?thesis by (intro that[of r]) auto
          next
            case INF
            from 6 dense obtain r where "r > a" "r < b" by auto
            with 6 INF show ?thesis by (intro that[of r]) auto
          qed
          from contr[OF this] 6 show False by fast
        qed
      qed
    next
      case False
      then have "j > 0" by auto
      with ‹j ≤ n› clock_numbering obtain c2 where c2: "v c2 = j" by auto
      note t = canonical_saturated_3[OF _ _ ‹cycle_free M n› assms(1) assms(4)[folded c1]
                                        assms(5)[folded c2] _ cn, unfolded c1 c2]
      show ?thesis
      proof (rule ccontr, goal_cases)
        case 1
        { fix d assume 1: "M i j = ∞"
          obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "d < r"
          proof (cases "M j i")
            case (Le d')
            obtain r where "r > - d'" using gt_ex by blast
            with Le 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
          next
            case (Lt d')
            obtain r where "r > - d'" using gt_ex by blast
            with Lt 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
          next
            case INF
            with 1 show ?thesis by (intro that[of "d + 1"]) auto
          qed
          then have "∃ r. Le r ≤ M i j ∧ Le (-r) ≤ M j i ∧ d < r" by auto
        } note inf_case = this
        { fix a b d :: real assume 1: "a < b" assume b: "b + d > 0"
          then have *: "b > -d" by auto
          obtain r where "r > - d" "r > a" "r < b"
          proof (cases "a ≥ - d")
            case True
            from 1 obtain r where "r > a" "r < b" using dense by auto
            with True show ?thesis by (auto intro: that[of r])
          next
            case False
            with * obtain r where "r > -d" "r < b" using dense by auto
            with False show ?thesis by (auto intro: that[of r])
          qed
          then have "∃ r. r > -d ∧ r > a ∧ r < b" by auto
        } note gt_case = this
        { fix a r assume r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "a < r" "M' i j = Le a ∨ M' i j = Lt a"
          from t[OF this(1,2) ‹i ≠ j›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c1 - u c2 = r" .
          with ‹i ≤ n› ‹j ≤ n› c1 c2 assms(2) have "dbm_entry_val u (Some c1) (Some c2) (M' i j)"
          unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
          with u(2) r(3,4) have False by auto
        } note contr = this
        from 1 have "M' i j < M i j" by auto
        then show False unfolding less
        proof (cases rule: dbm_lt.cases)
          case (1 d)
          with inf_case obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "d < r" by auto
          from contr[OF this] 1 show False by fast
        next
          case (2 d)
          with inf_case obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "d < r" by auto
          from contr[OF this] 2 show False by fast
        next
          case (3 a b)
          obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "a < r"
          proof (cases "M j i")
            case (Le d')
            with 3 non_neg have "b + d' ≥ 0" unfolding mult by auto
            then have "b ≥ - d'" by auto
            with 3 obtain r where "r ≥ - d'" "r > a" "r ≤ b" by blast
            with Le 3 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d')
            with 3 non_neg have "b + d' > 0" unfolding mult by auto
            from gt_case[OF 3(3) this] obtain r where "r > - d'" "r > a" "r ≤ b" by auto
            with Lt 3 show ?thesis by (intro that[of r]) auto
          next
            case INF
            with 3 show ?thesis by (intro that[of b]) auto
          qed
          from contr[OF this] 3 show False by fast
        next
          case (4 a b)
          obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "a < r"
          proof (cases "M j i")
            case (Le d)
            with 4 non_neg have "b + d > 0" unfolding mult by auto
            from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Le 4 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d)
            with 4 non_neg have "b + d > 0" unfolding mult by auto
            from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Lt 4 show ?thesis by (intro that[of r]) auto
          next
            case INF
            from 4 dense obtain r where "r > a" "r < b" by auto
            with 4 INF show ?thesis by (intro that[of r]) auto
          qed
          from contr[OF this] 4 show False by fast
        next
          case (5 a b)
          obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "a ≤ r"
          proof (cases "M j i")
            case (Le d')
            with 5 non_neg have "b + d' ≥ 0" unfolding mult by auto
            then have "b ≥ - d'" by auto
            with 5 obtain r where "r ≥ - d'" "r ≥ a" "r ≤ b" by blast
            with Le 5 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d')
            with 5 non_neg have "b + d' > 0" unfolding mult by auto
            then have "b > - d'" by auto
            with 5 obtain r where "r > - d'" "r ≥ a" "r ≤ b" by blast
            with Lt 5 show ?thesis by (intro that[of r]) auto
          next
            case INF
            with 5 show ?thesis by (intro that[of b]) auto
          qed
          from t[OF this(1,2) ‹i ≠ j›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c1 - u c2= r" .
          with ‹i ≤ n› ‹j ≤ n› c1 c2 assms(2) have "dbm_entry_val u (Some c1) (Some c2) (M' i j)"
          unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
          with u(2) r(3) 5 show False by auto
        next
          case (6 a b)
          obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "a < r"
          proof (cases "M j i")
            case (Le d)
            with 6 non_neg have "b + d > 0" unfolding mult by auto
            from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Le 6 show ?thesis by (intro that[of r]) auto
          next
            case (Lt d)
            with 6 non_neg have "b + d > 0" unfolding mult by auto
            from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
            with Lt 6 show ?thesis by (intro that[of r]) auto
          next
            case INF
            from 6 dense obtain r where "r > a" "r < b" by auto
            with 6 INF show ?thesis by (intro that[of r]) auto
          qed
          from contr[OF this] 6 show False by fast
        qed
      qed
    qed
  qed
qed

lemma DBM_set_diag:
  assumes "[M]⇘v,n⇙ ≠ {}"
  shows "[M]⇘v,n⇙ = [(λ i j. if i = j then Le 0 else M i j)]⇘v,n⇙"
using non_empty_dbm_diag_set[OF clock_numbering(1) assms] unfolding neutral by auto

lemma DBM_le_subset':
  assumes "∀i ≤ n. ∀ j ≤ n. i ≠ j ⟶ M i j ≤ M' i j"
  and "∀ i≤n. M' i i ≥ Le 0"
  and "u ∈ [M]⇘v,n⇙"
  shows "u ∈ [M']⇘v,n⇙"
proof -
  let ?M = "λ i j. if i = j then Le 0 else M i j"
  have "∀i j. i ≤ n ⟶ j ≤ n ⟶ ?M i j ≤ M' i j" using assms(1,2) by auto
  moreover from DBM_set_diag assms(3) have "u ∈ [?M]⇘v,n⇙" by auto
  ultimately show ?thesis using DBM_le_subset[folded less_eq, of n ?M M' u v] by auto
qed

lemma neg_diag_empty_spec:
  assumes "i ≤ n" "M i i < 𝟭"
  shows "[M]⇘v,n⇙ = {}"
using assms neg_diag_empty[where v= v and M = M, OF _ assms] clock_numbering(2) by auto

lemma canonical_empty_zone_spec:
  assumes "canonical M n"
  shows "[M]⇘v,n⇙ = {} ⟷ (∃i≤n. M i i < 𝟭)"
using canonical_empty_zone[of n v M, OF _ _ assms] clock_numbering by auto

lemma norm_set_diag:
  assumes "canonical M n" "[M]⇘v,n⇙ ≠ {}"
  obtains M' where "[M]⇘v,n⇙ = [M']⇘v,n⇙" "[norm M (k o v') n]⇘v,n⇙ = [norm M' (k o v') n]⇘v,n⇙"
                   "∀ i ≤ n. M' i i = 𝟭" "canonical M' n"
proof -
  from assms(2) neg_diag_empty_spec have *: "∀ i≤n. M i i ≥ Le 0" unfolding neutral by force
  let ?M = "λi j. if i = j then Le 0 else M i j"
  let ?NM = "norm M (k o v') n"
  let ?M2 = "λi j. if i = j then Le 0 else ?NM i j"
  from assms have "[?NM]⇘v,n⇙ ≠ {}"
  by (metis Collect_empty_eq norm_mono DBM_zone_repr_def clock_numbering(1) mem_Collect_eq)
  from DBM_set_diag[OF this] DBM_set_diag[OF assms(2)] have
    "[M]⇘v,n⇙ = [?M]⇘v,n⇙" "[?NM]⇘v,n⇙ = [?M2]⇘v,n⇙"
  by auto
  moreover have "norm ?M (k o v') n = ?M2" unfolding norm_def by fastforce
  moreover have "∀ i ≤ n. ?M i i = 𝟭" unfolding neutral by auto
  moreover have "canonical ?M n" using assms(1) *
  unfolding neutral[symmetric] less_eq[symmetric] mult[symmetric] by fastforce
  ultimately show ?thesis by (auto intro: that)
qed

lemma norm_normalizes:
  notes any_le_inf[intro]
  shows "normalized (norm M (k o v') n)"
unfolding normalized
proof (safe, goal_cases)
  case (1 i j)
  show ?case
  proof (cases "M i j < Lt (- real (k (v' j)))")
    case True with 1 show ?thesis unfolding norm_def less by (auto simp: Let_def)
  next
    case False
    with 1 show ?thesis unfolding norm_def by (auto simp: Let_def)
  qed
next
  case (2 i j)
  have **: "- real ((k o v') j) ≤ (k o v') i" by simp
  then have *: "Lt (- k (v' j)) < Le (k (v' i))" by (auto intro: Lt_lt_LeI)
  show ?case
  proof (cases "M i j ≤ Le (real (k (v' i)))")
    case False with 2 show ?thesis unfolding norm_def less_eq dbm_le_def by (auto simp: Let_def)
  next
    case True with 2 show ?thesis unfolding norm_def by (auto simp: Let_def)
  qed
next
  case (3 i)
  show ?case
  proof (cases "M i 0 ≤ Le (real (k (v' i)))")
    case False then have "Le (real (k (v' i))) ≺ M i 0" unfolding less_eq dbm_le_def by auto
    with 3 show ?thesis unfolding norm_def by auto
  next
    case True
    with 3 show ?thesis unfolding norm_def less_eq dbm_le_def by (auto simp: Let_def)
  qed
next
  case (4 i)
  show ?case
  proof (cases "M 0 i < Lt (- real (k (v' i)))")
    case True with 4 show ?thesis unfolding norm_def less by auto
  next
    case False with 4 show ?thesis unfolding norm_def by (auto simp: Let_def)
  qed
qed

lemma norm_int_preservation:
  assumes "dbm_int M n" "i ≤ n" "j ≤ n" "norm M (k o v') n i j ≠ ∞"
  shows "get_const (norm M (k o v') n i j) ∈ ℤ"
using assms unfolding norm_def by (auto simp: Let_def)

lemma norm_V_preservation':
  notes any_le_inf[intro]
  assumes "[M]⇘v,n⇙ ⊆ V" "canonical M n" "[M]⇘v,n⇙ ≠ {}"
  shows "[norm M (k o v') n]⇘v,n⇙ ⊆ V"
proof -
  let ?M = "norm M (k o v') n"
  from non_empty_cycle_free[OF assms(3)] clock_numbering(2) have *: "cycle_free M n" by auto
  { fix c assume "c ∈ X"
    with clock_numbering have c: "c ∈ X" "v c > 0" "v c ≤ n" by auto
    with assms(2) have
      "M 0 (v c) + M (v c) 0 ≥ M 0 0"
    unfolding mult less_eq by blast
    moreover from cycle_free_diag[OF *] have "M 0 0 ≥ Le 0" unfolding neutral by auto
    ultimately have ge_0: "M 0 (v c) + M (v c) 0 ≥ Le 0" by auto
    have "M 0 (v c) ≤ Le 0"
    proof (cases "M 0 (v c)")
      case (Le d)
      with ge_0 have "M (v c) 0 ≥ Le (-d)"
       apply (cases "M (v c) 0")
         unfolding mult apply auto
         apply (rename_tac x1)
         apply (subgoal_tac "-d ≤ x1")
         apply auto
       apply (rename_tac x2)
       apply (subgoal_tac "-d < x2")
      by auto
      with Le canonical_saturated_2[OF _ _ ‹cycle_free M n› assms(2) c(3)] clock_numbering(1)
      obtain u where "u ∈ [M]⇘v,n⇙" "u c = -d" by auto
      with assms(1) c(1) Le show ?thesis unfolding V_def by fastforce
    next
      case (Lt d)
      show ?thesis
      proof (cases "d ≤ 0")
        case True
        then have "Lt d < Le 0" by (auto intro: Lt_lt_LeI)
        with Lt show ?thesis by auto
      next
        case False
        then have "d > 0" by auto
        note Lt' = Lt
        show ?thesis
        proof (cases "M (v c) 0")
          case (Le d')
          with Lt ge_0 have *: "d > -d'" unfolding mult by auto
          show ?thesis
          proof (cases "d' < 0")
            case True
            from * clock_numbering(1) canonical_saturated_1[OF _ _ ‹cycle_free _ _› assms(2) c(3)] Lt Le
            obtain u where "u ∈ [M]⇘v,n⇙" "u c = d'" by auto
            with ‹d' < 0› assms(1) ‹c ∈ X› show ?thesis unfolding V_def by fastforce
          next
            case False
            then have "d' ≥ 0" by auto
            with ‹d > 0› have "Le (d / 2) ≤ Lt d" "Le (- (d /2)) ≤ Le d'" by auto
            with canonical_saturated_2[OF _ _ ‹cycle_free _ _› assms(2) c(3)] Lt Le clock_numbering(1)
            obtain u where "u ∈ [M]⇘v,n⇙" "u c = - (d / 2)" by auto
            with ‹d > 0› assms(1) ‹c ∈ X› show ?thesis unfolding V_def by fastforce
          qed
        next
          case (Lt d')
          with Lt' ge_0 have *: "d > -d'" unfolding mult by auto
          then have **: "-d < d'" by auto
          show ?thesis
          proof (cases "d' ≤ 0")
            case True
            from assms(1,3) c obtain u where u:
              "u ∈ V" "dbm_entry_val u (Some c) None (M (v c) 0)"
            unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
            with u(1) True Lt ‹c ∈ X› show ?thesis unfolding V_def by auto
          next
            case False
            with ‹d > 0› have "Le (d / 2) ≤ Lt d" "Le (- (d /2)) ≤ Lt d'" by auto
            with canonical_saturated_2[OF _ _ ‹cycle_free _ _› assms(2) c(3)] Lt Lt' clock_numbering(1)
            obtain u where "u ∈ [M]⇘v,n⇙" "u c = - (d / 2)" by auto
            with ‹d > 0› assms(1) ‹c ∈ X› show ?thesis unfolding V_def by fastforce
          qed
        next
          case INF
          show ?thesis
          proof (cases "d > 0")
            case True
            from ‹d > 0› have "Le (d / 2) ≤ Lt d" by auto
            with INF canonical_saturated_2[OF _ _ ‹cycle_free _ _› assms(2) c(3)] Lt clock_numbering(1)
            obtain u where "u ∈ [M]⇘v,n⇙" "u c = - (d / 2)" by auto
            with ‹d > 0› assms(1) ‹c ∈ X› show ?thesis unfolding V_def by fastforce
          next
            case False
            with Lt show ?thesis by auto
          qed
        qed
      qed
    next
      case INF
      obtain u r where "u ∈ [M]⇘v,n⇙" "u c = - r" "r > 0"
      proof (cases "M (v c) 0")
        case (Le d)
        let ?d = "if d ≤ 0 then -d + 1 else d"
        from Le INF canonical_saturated_2[OF _ _ ‹cycle_free _ _› assms(2) c(3), of ?d] clock_numbering(1)
        obtain u where "u ∈ [M]⇘v,n⇙" "u c = - ?d" by (cases "d < 0") force+
        from that[OF this] show thesis by auto
      next
        case (Lt d)
        let ?d = "if d ≤ 0 then -d + 1 else d"
        from Lt INF canonical_saturated_2[OF _ _ ‹cycle_free _ _› assms(2) c(3), of ?d] clock_numbering(1)
        obtain u where "u ∈ [M]⇘v,n⇙" "u c = - ?d" by (cases "d < 0") force+
        from that[OF this] show thesis by auto
      next
        case INF
        with ‹M 0 (v c) = ∞› canonical_saturated_2[OF _ _ ‹cycle_free _ _› assms(2) c(3)] clock_numbering(1)
        obtain u where "u ∈ [M]⇘v,n⇙" "u c = - 1" by auto
        from that[OF this] show thesis by auto
      qed
      with assms(1) ‹c ∈ X› show ?thesis unfolding V_def by fastforce
    qed
    moreover then have "¬ Le 0 ≺ M 0 (v c)" unfolding less[symmetric] by auto
    ultimately have *: "?M 0 (v c) ≤ Le 0" using assms(3) c unfolding norm_def by (auto simp: Let_def)
    fix u assume u: "u ∈ [?M]⇘v,n⇙"
    with c have "dbm_entry_val u None (Some c) (?M 0 (v c))"
    unfolding DBM_val_bounded_def DBM_zone_repr_def by auto
    with * have "u c ≥ 0" by (cases "?M 0 (v c)") auto
  } note ge_0 = this
  then show ?thesis unfolding V_def by auto
qed

lemma norm_V_preservation:
  assumes "[M]⇘v,n⇙ ⊆ V" "canonical M n"
  shows "[norm M (k o v') n]⇘v,n⇙ ⊆ V" (is "[?M]⇘v,n⇙ ⊆ V")
proof (cases "[M]⇘v,n⇙ = {}")
  case True
  obtain i where i: "i ≤ n" "M i i < 𝟭" by (metis True assms(2) canonical_empty_zone_spec)
  have "¬ Le (k (v' i)) < Le 0" unfolding less by (cases "k (v' i) = 0", auto)
  with i have "?M i i < 𝟭" unfolding norm_def by (auto simp: neutral less Let_def)
  with neg_diag_empty_spec[OF ‹i ≤ n›] have "[?M]⇘v,n⇙ = {}" .
  then show ?thesis by auto
next
  case False
  from norm_set_diag[OF assms(2) False] norm_V_preservation' False assms
  show ?thesis by metis
qed

lemma norm_min:
  assumes "normalized M1" "[M]⇘v,n⇙ ⊆ [M1]⇘v,n⇙"
          "canonical M n" "[M]⇘v,n⇙ ≠ {}" "[M]⇘v,n⇙ ⊆ V"
  shows "[norm M (k o v') n]⇘v,n⇙ ⊆ [M1]⇘v,n⇙" (is "[?M2]⇘v,n⇙ ⊆ [M1]⇘v,n⇙")
proof -
  have le: "⋀ i j. i ≤ n ⟹ j ≤ n ⟹ i ≠ j⟹ M i j ≤ M1 i j" using assms(2,3,4)
  by (auto intro!: DBM_canonical_subset_le)
  from assms have "[M1]⇘v,n⇙ ≠ {}" by auto
  with neg_diag_empty_spec have *: "∀ i≤n. M1 i i ≥ Le 0" unfolding neutral by force
  from assms norm_V_preservation have V: "[?M2]⇘v,n⇙ ⊆ V" by auto
  have "u ∈ [M1]⇘v,n⇙" if "u ∈ [?M2]⇘v,n⇙" for u
  proof -
    from that V have V: "u ∈ V" by fast
    show ?thesis unfolding DBM_zone_repr_def DBM_val_bounded_def
    proof (safe, goal_cases)
      case 1 with * show ?case unfolding less_eq by fast
    next
      case (2 c)
      then have c: "v c > 0" "v c ≤ n" "c ∈ X" "v' (v c) = c" using clock_numbering v_v' by metis+
      with V have v_bound: "dbm_entry_val u None (Some c) (Le 0)" unfolding V_def by auto
      from that c have bound:
        "dbm_entry_val u None (Some c) (?M2 0 (v c))"
      unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
      show ?case
      proof (cases "M 0 (v c) < Lt (- k c)")
        case False
        show ?thesis
        proof (cases "Le 0 < M 0 (v c)")
          case True
          with le c(1,2) have "Le 0 ≤ M1 0 (v c)" by fastforce
          with dbm_entry_val_mono_2[OF v_bound, folded less_eq] show ?thesis by fast
        next
          case F: False
          with assms(3) False c have "?M2 0 (v c) = M 0 (v c)" unfolding less norm_def by auto
          with le c bound show ?thesis by (auto intro: dbm_entry_val_mono_2[folded less_eq])
        qed
      next
        case True
        have "Lt (- k c) ≺ Le 0" by auto
        with True c assms(3) have "?M2 0 (v c) = Lt (- k c)" unfolding less norm_def by auto
        moreover from assms(1) c have "Lt (- k c) ≤ M1 0 (v c)" unfolding normalized by auto
        ultimately show ?thesis using le c bound by (auto intro: dbm_entry_val_mono_2[folded less_eq])
      qed
    next
      case (3 c)
      then have c: "v c > 0" "v c ≤ n" "c ∈ X" "v' (v c) = c" using clock_numbering v_v' by metis+
      from that c have bound:
        "dbm_entry_val u (Some c) None (?M2 (v c) 0)"
      unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
      show ?case
      proof (cases "M (v c) 0 ≤ Le (k c)")
        case False
        with le c have "¬ M1 (v c) 0 ≤ Le (k c)" by fastforce
        with assms(1) c show ?thesis unfolding normalized by fastforce
      next
        case True
        show ?thesis
        proof (cases "M (v c) 0 < Lt 0")
          case T: True
          have "¬ Le (real (k c)) ≺ Lt 0" by auto
          with T True c have "?M2 (v c) 0 = Lt 0" unfolding norm_def less by (auto simp: Let_def)
          with bound V c show ?thesis unfolding V_def by auto
        next
          case False
          with True assms(3) c have "?M2 (v c) 0 = M (v c) 0" unfolding less less_eq norm_def
          by (auto simp: Let_def)
          with dbm_entry_val_mono_3[OF bound, folded less_eq] le c show ?thesis by auto
        qed
      qed
    next
      case (4 c1 c2)
      then have c:
        "v c1 > 0" "v c1 ≤ n" "c1 ∈ X" "v' (v c1) = c1" "v c2 > 0" "v c2 ≤ n" "c2 ∈ X" "v' (v c2) = c2"
      using clock_numbering v_v' by metis+
      from that c have bound:
        "dbm_entry_val u (Some c1) (Some c2) (?M2 (v c1) (v c2))"
      unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
      show ?case
      proof (cases "c1 = c2")
        case True
        then have "dbm_entry_val u (Some c1) (Some c2) (Le 0)" by auto
        with c True * dbm_entry_val_mono_1[OF this, folded less_eq] show ?thesis by auto
      next
        case False
        with clock_numbering(1) ‹v c1 ≤ n› ‹v c2 ≤ n› have neq: "v c1 ≠ v c2" by auto
        show ?thesis
        proof (cases "Le (k c1) < M (v c1) (v c2)")
          case False
          show ?thesis
          proof (cases "M (v c1) (v c2) < Lt (- real (k c2))")
            case F: False
            with c False assms(3) have
              "?M2 (v c1) (v c2) = M (v c1) (v c2)"
            unfolding norm_def less by auto
            with dbm_entry_val_mono_1[OF bound, folded less_eq] le c neq show ?thesis by auto
          next
            case True
            with c False assms(3) have "?M2 (v c1) (v c2) = Lt (- k c2)" unfolding less norm_def
            by auto
            moreover from assms(1) c have "M1 (v c1) (v c2) = ∞ ∨ M1 (v c1) (v c2) ≥ Lt (- k c2)"
            unfolding normalized by fastforce
            ultimately show ?thesis using dbm_entry_val_mono_1[OF bound, folded less_eq] by auto
          qed
        next
          case True
          with le c neq have "M1 (v c1) (v c2) > Le (k c1)" by fastforce
          moreover from True c assms(3) have "?M2 (v c1) (v c2) = ∞" unfolding norm_def less
          by auto
          moreover from assms(1) c have "M1 (v c1) (v c2) = ∞ ∨ M1 (v c1) (v c2) ≤ Le (k c1)"
          unfolding normalized by fastforce
          ultimately show ?thesis by auto
        qed
      qed
    qed
  qed
  then show ?thesis by blast
qed

lemma apx_norm_eq:
  assumes "canonical M n" "[M]⇘v,n⇙ ⊆ V" "dbm_int M n"
  shows "Approx⇩β ([M]⇘v,n⇙) = [norm M (k o v') n]⇘v,n⇙"
proof -
  let ?M = "norm M (k o v') n"
  from assms norm_V_preservation norm_int_preservation norm_normalizes
  have *: "vabstr ([?M]⇘v,n⇙) ?M" "normalized ?M" "[?M]⇘v,n⇙ ⊆ V" by presburger+
  from dbm_regions'[OF this] obtain U where U: "U ⊆ ℛ" "[?M]⇘v,n⇙ = ⋃U" by auto
  from assms(3) have **: "[M]⇘v,n⇙ ⊆ [?M]⇘v,n⇙" by (simp add: norm_mono clock_numbering(1) subsetI) 
  show ?thesis
  proof (cases "[M]⇘v,n⇙ = {}")
    case True
    from canonical_empty_zone_spec[OF ‹canonical M n›] True obtain i where i:
      "i ≤ n" "M i i < 𝟭"
    by auto
    with assms(3) have "?M i i < 𝟭" unfolding neutral norm_def
    proof (cases "i = 0", auto intro: Lt_lt_LeI, goal_cases)
      case 1
      then show ?case unfolding less by auto
    next
      case 2
      have "¬ Le (real (k (v' i))) ≺ Le 0" by auto
      with 2 show ?case by (auto simp: Let_def less)
    qed
    from neg_diag_empty[of n v i ?M, OF _ ‹i ≤ n› this] clock_numbering have
      "[?M]⇘v,n⇙ = {}"
    by (auto intro: Lt_lt_LeI)
    with apx_empty True show ?thesis by auto
  next
    case False
    from apx_in[OF assms(2)] obtain U' M1 where U':
      "Approx⇩β ([M]⇘v,n⇙) = ⋃U'" "U' ⊆ ℛ" "[M]⇘v,n⇙ ⊆ Approx⇩β ([M]⇘v,n⇙)"
      "vabstr (Approx⇩β ([M]⇘v,n⇙)) M1" "normalized M1"
    by auto
    from norm_min[OF U'(5) _ assms(1) False assms(2)] U'(3,4) *(1) apx_min[OF U(2,1) _ _ *(2) **]
    show ?thesis by blast
  qed
qed

end        


section ‹Auxiliary ‹β›-boundedness Theorems›

context Beta_Regions'
begin

lemma β_boundedness_diag_lt:
  fixes m :: int
  assumes "- k y ≤ m" "m ≤ k x" "x ∈ X" "y ∈ X"
  shows "∃ U ⊆ ℛ. ⋃ U = {u ∈ V. u x - u y < m}"
proof -
  note A = assms
  note B = A(1,2)
  let ?U = "{R ∈ ℛ. ∃ I J r c d (e :: int). R = region X I J r ∧ valid_region X k I J r ∧
    (I x = Const c ∧ I y = Const d ∧ real c - d < m ∨
     I x = Const c ∧ I y = Intv d  ∧ real c - d ≤ m ∨
     I x = Intv c  ∧ I y = Const d ∧ real c + 1 - d ≤ m ∨
     I x = Intv c  ∧ I y = Intv d  ∧ real c - d ≤ m ∧ (x,y) ∈ r ∧ (y, x) ∉ r ∨
     I x = Intv c  ∧ I y = Intv d  ∧ real c - d < m ∧ (y, x) ∈ r ∨
     (I x = Greater (k x) ∨ I y = Greater (k y)) ∧ J x y = Smaller' (- k y) ∨
     (I x = Greater (k x) ∨ I y = Greater (k y)) ∧ J x y = Intv' e  ∧ e < m ∨
     (I x = Greater (k x) ∨ I y = Greater (k y)) ∧ J x y = Const' e ∧ e < m
    )}"
  { fix u I J r assume "u ∈ region X I J r" "I x = Greater (k x) ∨ I y = Greater (k y)"
    with A(3,4) have "intv'_elem x y u (J x y)" by force
  } note * = this
  { fix u I J r assume "u ∈ region X I J r"
    with A(3,4) have "intv_elem x u (I x)" "intv_elem y u (I y)" by force+
  } note ** = this
  have "⋃ ?U = {u ∈ V. u x - u y < m}"
  proof (safe, goal_cases)
    case (2 u) with **[OF this(1)] show ?case by auto
  next
    case (4 u) with **[OF this(1)] show ?case by auto
  next
    case (6 u) with **[OF this(1)] show ?case by auto
  next
    case (8 u X I J r c d)
    from this A(3,4) have "intv_elem x u (I x)" "intv_elem y u (I y)" "frac (u x) < frac (u y)" by force+
    with nat_intv_frac_decomp 8(4,5) have
      "u x = c + frac (u x)" "u y = d + frac (u y)" "frac (u x) < frac (u y)"
    by force+
    with 8(6) show ?case by linarith
  next
    case (10 u X I J r c d)
    with **[OF this(1)] 10(4,5) have "u x < c + 1" "d < u y" by auto
    then have "u x - u y < real (c + 1) - real d" by linarith
    moreover from 10(6) have "real c + 1 - d ≤ m"
    proof -
      have "int c - int d < m"
        using 10(6) by linarith
      then show ?thesis
        by simp
    qed
    ultimately show ?case by linarith
  next
    case 12 with *[OF this(1)] B show ?case by auto
  next
    case 14 with *[OF this(1)] B show ?case by auto
  next
    case (23 u)
    from region_cover_V[OF this(1)] obtain R where R: "R ∈ ℛ" "u ∈ R" by auto
    then obtain I J r where R': "R = region X I J r" "valid_region X k I J r" unfolding ℛ_def by auto
    with R' R(2) A have C:
      "intv_elem x u (I x)" "intv_elem y u (I y)" "valid_intv (k x) (I x)" "valid_intv (k y) (I y)"
    by auto
    { assume A: "I x = Greater (k x) ∨ I y = Greater (k y)"
      obtain intv and d :: int where intv:
        "valid_intv' (k y) (k x) intv" "intv'_elem x y u intv"
        "intv = Smaller' (- k y) ∨ intv = Intv' d ∧ d < m ∨ intv = Const' d ∧ d < m"
      proof (cases "u x - u y < - int (k y)")
        case True
        have "valid_intv' (k y) (k x) (Smaller' (- k y))" ..
        moreover with True have "intv'_elem x y u (Smaller' (- k y))" by auto
        ultimately show thesis by (auto intro: that)
      next
        case False
        show thesis
        proof (cases "∃ (c :: int). u x - u y = c")
          case True
          then obtain c :: int where c: "u x - u y = c" by auto
          have "valid_intv' (k y) (k x) (Const' c)" using False B(2) 23(2) c by fastforce
          moreover with c have "intv'_elem x y u (Const' c)" by auto
          moreover have "c < m" using c 23(2) by auto
          ultimately show thesis by (auto intro: that)
        next
          case False
          then obtain c :: real where c: "u x - u y = c" "c ∉ ℤ" by (metis Ints_cases)
          have "valid_intv' (k y) (k x) (Intv' (floor c))"
          proof
            show "- int (k y) ≤ ⌊c⌋" using ‹¬ _ < _› c by linarith
            show "⌊c⌋ < int (k x)" using B(2) 23(2) c by linarith
          qed
          moreover have "intv'_elem x y u (Intv' (floor c))"
          proof
            from c(1,2) show "⌊c⌋ < u x - u y" by (meson False eq_iff not_le of_int_floor_le)
            from c(1,2) show "u x - u y < ⌊c⌋ + 1" by simp
          qed
          moreover have "⌊c⌋ < m" using c 23(2) by linarith
          ultimately show thesis using that by auto
        qed
      qed
      let ?J = "λ a b. if x = a ∧ y = b then intv else J a b"
      let ?R = "region X I ?J r"
      let ?X⇩0 = "{x ∈ X. ∃d. I x = Intv d}"
      have "u ∈ ?R"
      proof (standard, goal_cases)
        case 1 from R R' show ?case by auto
      next
        case 2 from R R' show ?case by auto
      next
        case 3 show "?X⇩0 = ?X⇩0" by auto
      next
        case 4 from R R' show "∀x∈?X⇩0. ∀y∈?X⇩0. (x, y) ∈ r ⟷ frac (u x) ≤ frac (u y)" by auto
      next
        case 5
        show ?case
        proof (clarify, goal_cases)
          case (1 a b)
          show ?case
          proof (cases "x = a ∧ y = b")
            case True with intv show ?thesis by auto
          next
            case False
            with R(2) R'(1) 1 show ?thesis by force
          qed
        qed
      qed
      have "valid_region X k I ?J r"
      proof
        show "?X⇩0 = ?X⇩0" ..
        show "refl_on ?X⇩0 r" using R' by auto
        show "trans r" using R' by auto
        show "total_on ?X⇩0 r" using R' by auto
        show "∀x∈X. valid_intv (k x) (I x)" using R' by auto
        show "∀xa∈X. ∀ya∈X. isGreater (I xa) ∨ isGreater (I ya)
              ⟶ valid_intv' (int (k ya)) (int (k xa)) (if x = xa ∧ y = ya then intv else J xa ya)"
        proof (clarify, goal_cases)
          case (1 a b)
          show ?case
          proof (cases "x = a ∧ y = b")
            case True
            with B intv show ?thesis by auto
          next
            case False
            with R'(2) 1 show ?thesis by force
          qed
        qed
      qed
      moreover then have "?R ∈ ℛ" unfolding ℛ_def by auto
      ultimately have "?R ∈ ?U" using intv
        apply clarify
        apply (rule exI[where x = I], rule exI[where x = ?J], rule exI[where x = r])
      using A by fastforce
      with ‹u ∈ region _ _ _ _› have ?case by (intro Complete_Lattices.UnionI) blast+
    } note * = this
    show ?case
    proof (cases "I x")
      case (Const c)
      show ?thesis
      proof (cases "I y", goal_cases)
        case (1 d)
        with C(1,2) Const A(2,3) 23(2) have "real c - real d < m" by auto
        with Const 1 R R' show ?thesis by blast
      next
        case (Intv d)
        with C(1,2) Const A(2,3) 23(2) have "real c - (d + 1) < m" by auto
        then have "c < 1 + (d + m)" by linarith
        then have "real c - d ≤ m" by simp
        with Const Intv R R' show ?thesis by blast
      next
        case (Greater d) with * C(4) show ?thesis by auto
      qed
    next
      case (Intv c)
      show ?thesis
      proof (cases "I y", goal_cases)
        case (Const d)
        with C(1,2) Intv A(2,3) 23(2) have "real c - d < m" by auto
        then have "real c < m + d" by linarith
        then have "c < m + d" by linarith 
        then have "real c + 1 - d ≤ m" by simp
        with Const Intv R R' show ?thesis by blast
      next
        case (2 d)
        show ?thesis
        proof (cases "(y, x) ∈ r")
          case True
          with C(1,2) R R' Intv 2 A(3,4) have
            "c < u x" "u x < c + 1" "d < u y" "u y < d + 1" "frac (u x) ≥ frac (u y)"
          by force+
          with 23(2) nat_intv_frac_decomp have "c + frac (u x) - (d + frac (u y)) < m" by auto
          with ‹frac _ ≥ _› have "real c - real d < m" by linarith
          with Intv 2 True R R' show ?thesis by blast
        next
          case False
          with R R' A(3,4) Intv 2 have "(x,y) ∈ r" by fastforce
          with C(1,2) R R' Intv 2 have "c < u x" "u y < d + 1" by force+
          with 23(2) have "c < 1 + d + m" by auto
          then have "real c - d ≤ m" by simp
          with Intv 2 False ‹_ ∈ r› R R' show ?thesis by blast
        qed
      next
        case (Greater d) with * C(4) show ?thesis by auto
      qed
    next
      case (Greater d) with * C(3) show ?thesis by auto
    qed
  qed (auto intro: A simp: V_def, (fastforce dest!: *)+)
  moreover have "?U ⊆ ℛ" by fastforce
  ultimately show ?thesis by blast
qed

lemma β_boundedness_diag_eq:
  fixes m :: int
  assumes "- k y ≤ m" "m ≤ k x" "x ∈ X" "y ∈ X"
  shows "∃ U ⊆ ℛ. ⋃ U = {u ∈ V. u x - u y = m}"
proof -
  note A = assms
  note B = A(1,2)
  let ?U = "{R ∈ ℛ. ∃ I J r c d (e :: int). R = region X I J r ∧ valid_region X k I J r ∧
    (I x = Const c ∧ I y = Const d ∧ real c - d = m ∨
     I x = Intv c  ∧ I y = Intv d  ∧ real c - d = m ∧ (x, y) ∈ r ∧ (y, x) ∈ r ∨
     (I x = Greater (k x) ∨ I y = Greater (k y)) ∧ J x y = Const' e ∧ e = m
    )}"
  { fix u I J r assume "u ∈ region X I J r" "I x = Greater (k x) ∨ I y = Greater (k y)"
    with A(3,4) have "intv'_elem x y u (J x y)" by force
  } note * = this
  { fix u I J r assume "u ∈ region X I J r"
    with A(3,4) have "intv_elem x u (I x)" "intv_elem y u (I y)" by force+
  } note ** = this
  have "⋃ ?U = {u ∈ V. u x - u y = m}"
  proof (safe, goal_cases)
    case (2 u) with **[OF this(1)] show ?case by auto
  next
    case (4 u X I J r c d)
    from this A(3,4) have "intv_elem x u (I x)" "intv_elem y u (I y)" "frac (u x) = frac (u y)" by force+
    with nat_intv_frac_decomp 4(4,5) have
      "u x = c + frac (u x)" "u y = d + frac (u y)" "frac (u x) = frac (u y)"
    by force+
    with 4(6) show ?case by linarith
  next
    case (9 u)
    from region_cover_V[OF this(1)] obtain R where R: "R ∈ ℛ" "u ∈ R" by auto
    then obtain I J r where R': "R = region X I J r" "valid_region X k I J r" unfolding ℛ_def by auto
    with R' R(2) A have C:
      "intv_elem x u (I x)" "intv_elem y u (I y)" "valid_intv (k x) (I x)" "valid_intv (k y) (I y)"
    by auto
    { assume A: "I x = Greater (k x) ∨ I y = Greater (k y)"
      obtain intv where intv:
        "valid_intv' (k y) (k x) intv" "intv'_elem x y u intv" "intv = Const' m"
      proof (cases "u x - u y < - int (k y)")
        case True
        with 9 B show ?thesis by auto
      next
        case False
        show thesis
        proof (cases "∃ (c :: int). u x - u y = c")
          case True
          then obtain c :: int where c: "u x - u y = c" by auto
          have "valid_intv' (k y) (k x) (Const' c)" using False B(2) 9(2) c by fastforce
          moreover with c have "intv'_elem x y u (Const' c)" by auto
          moreover have "c = m" using c 9(2) by auto
          ultimately show thesis by (auto intro: that)
        next
          case False
          then have "u x - u y ∉ ℤ" by (metis Ints_cases)
          with 9 show ?thesis by auto
        qed
      qed
      let ?J = "λ a b. if x = a ∧ y = b then intv else J a b"
      let ?R = "region X I ?J r"
      let ?X⇩0 = "{x ∈ X. ∃d. I x = Intv d}"
      have "u ∈ ?R"
      proof (standard, goal_cases)
        case 1 from R R' show ?case by auto
      next
        case 2 from R R' show ?case by auto
      next
        case 3 show "?X⇩0 = ?X⇩0" by auto
      next
        case 4 from R R' show "∀x∈?X⇩0. ∀y∈?X⇩0. (x, y) ∈ r ⟷ frac (u x) ≤ frac (u y)" by auto
      next
        case 5
        show ?case
        proof (clarify, goal_cases)
          case (1 a b)
          show ?case
          proof (cases "x = a ∧ y = b")
            case True with intv show ?thesis by auto
          next
            case False with R(2) R'(1) 1 show ?thesis by force
          qed
        qed
      qed
      have "valid_region X k I ?J r"
      proof (standard, goal_cases)
        show "?X⇩0 = ?X⇩0" ..
        show "refl_on ?X⇩0 r" using R' by auto
        show "trans r" using R' by auto
        show "total_on ?X⇩0 r" using R' by auto
        show "∀x∈X. valid_intv (k x) (I x)" using R' by auto
      next
        case 6
        then show ?case
        proof (clarify, goal_cases)
          case (1 a b)
          show ?case
          proof (cases "x = a ∧ y = b")
            case True with B intv show ?thesis by auto
          next
            case False with R'(2) 1 show ?thesis by force
          qed
        qed
      qed
      moreover then have "?R ∈ ℛ" unfolding ℛ_def by auto
      ultimately have "?R ∈ ?U" using intv
        apply clarify
        apply (rule exI[where x = I], rule exI[where x = ?J], rule exI[where x = r])
      using A by fastforce
      with ‹u ∈ region _ _ _ _› have ?case by (intro Complete_Lattices.UnionI) blast+
    } note * = this
    show ?case
    proof (cases "I x")
      case (Const c)
      show ?thesis
      proof (cases "I y", goal_cases)
        case (1 d)
        with C(1,2) Const A(2,3) 9(2) have "real c - d = m" by auto
        with Const 1 R R' show ?thesis by blast
      next
        case (Intv d)
        from Intv Const C(1,2) have range: "d < u y" "u y < d + 1" and eq: "u x = c" by auto
        from eq have "u x ∈ ℤ" by auto
        with nat_intv_not_int[OF range] have "u x - u y ∉ ℤ" using Ints_diff by fastforce
        with 9 show ?thesis by auto
      next
        case Greater with C * show ?thesis by auto
      qed
    next
      case (Intv c)
      show ?thesis
      proof (cases "I y", goal_cases)
        case (Const d)
        from Intv Const C(1,2) have range: "c < u x" "u x < c + 1" and eq: "u y = d" by auto
        from eq have "u y ∈ ℤ" by auto
        with nat_intv_not_int[OF range] have "u x - u y ∉ ℤ" using Ints_add by fastforce
        with 9 show ?thesis by auto
      next
        case (2 d)
        with Intv C have range: "c < u x" "u x < c + 1" "d < u y" "u y < d + 1" by auto
        show ?thesis
        proof (cases "(x, y) ∈ r")
          case True
          note T = this
          show ?thesis
          proof (cases "(y, x) ∈ r")
            case True
            with Intv 2 T R' ‹u ∈ R› A(3,4) have "frac (u x) = frac (u y)" by force
            with nat_intv_frac_decomp[OF range(1,2)] nat_intv_frac_decomp[OF range(3,4)] have
              "u x - u y = real c - real d"
            by algebra
            with 9 have "real c - d = m" by auto
            with T True Intv 2 R R' show ?thesis by force
          next
            case False
            with Intv 2 T R' ‹u ∈ R› A(3,4) have "frac (u x) < frac (u y)" by force
            then have
              "frac (u x - u y) ≠ 0"
            by (metis add.left_neutral diff_add_cancel frac_add frac_unique_iff less_irrefl)
            then have "u x - u y ∉ ℤ" by (metis frac_eq_0_iff)
            with 9 show ?thesis by auto
          qed
        next
          case False
          note F = this
          show ?thesis
          proof (cases "x = y")
            case True
            with R'(2) Intv ‹x ∈ X› have "(x, y) ∈ r" "(y, x) ∈ r" by (auto simp: refl_on_def)
            with Intv True R' R 9(2) show ?thesis by force
          next
            case False
            with F R'(2) Intv 2 ‹x ∈ X› ‹y ∈ X› have "(y, x) ∈ r" by (fastforce simp: total_on_def)
            with F Intv 2 R' ‹u ∈ R› A(3,4) have "frac (u x) > frac (u y)" by force
            then have
              "frac (u x - u y) ≠ 0"
            by (metis add.left_neutral diff_add_cancel frac_add frac_unique_iff less_irrefl)
            then have "u x - u y ∉ ℤ" by (metis frac_eq_0_iff)
            with 9 show ?thesis by auto
          qed
        qed
      next
        case Greater with * C show ?thesis by force
      qed
    next
      case Greater with * C show ?thesis by force
    qed
  qed (auto intro: A simp: V_def dest: *)
  moreover have "?U ⊆ ℛ" by fastforce
  ultimately show ?thesis by blast
qed

lemma β_boundedness_lt:
  fixes m :: int
  assumes "m ≤ k x" "x ∈ X"
  shows "∃ U ⊆ ℛ. ⋃ U = {u ∈ V. u x < m}"
proof -
  note A = assms
  let ?U = "{R ∈ ℛ. ∃ I J r c. R = region X I J r ∧ valid_region X k I J r ∧
    (I x = Const c ∧ c < m ∨ I x = Intv c ∧ c < m)}"
  { fix u I J r assume "u ∈ region X I J r"
    with A have "intv_elem x u (I x)" by force+
  } note ** = this
  have "⋃ ?U = {u ∈ V. u x < m}"
  proof (safe, goal_cases)
    case (2 u) with **[OF this(1)] show ?case by auto
  next
    case (4 u) with **[OF this(1)] show ?case by auto
  next
    case (5 u)
    from region_cover_V[OF this(1)] obtain R where R: "R ∈ ℛ" "u ∈ R" by auto
    then obtain I J r where R': "R = region X I J r" "valid_region X k I J r" unfolding ℛ_def by auto
    with R' R(2) A have C:
      "intv_elem x u (I x)" "valid_intv (k x) (I x)"
    by auto
    show ?case
    proof (cases "I x")
      case (Const c)
      with 5 C(1) have "c < m" by auto
      with R R' Const show ?thesis by blast
    next
      case (Intv c)
      with 5 C(1) have "c < m" by auto
      with R R' Intv show ?thesis by blast
    next
      case (Greater c) with 5 C A Greater show ?thesis by auto
    qed
  qed (auto intro: A simp: V_def)
  moreover have "?U ⊆ ℛ" by fastforce
  ultimately show ?thesis by blast
qed

lemma β_boundedness_gt:
  fixes m :: int
  assumes "m ≤ k x" "x ∈ X"
  shows "∃ U ⊆ ℛ. ⋃ U = {u ∈ V. u x > m}"
proof -
  note A = assms
  let ?U = "{R ∈ ℛ. ∃ I J r c. R = region X I J r ∧ valid_region X k I J r ∧
    (I x = Const c ∧ c > m ∨ I x = Intv c ∧ c ≥ m ∨ I x = Greater (k x))}"
  { fix u I J r assume "u ∈ region X I J r"
    with A have "intv_elem x u (I x)" by force+
  } note ** = this
  have "⋃ ?U = {u ∈ V. u x > m}"
  proof (safe, goal_cases)
    case (2 u) with **[OF this(1)] show ?case by auto
  next
    case (4 u) with **[OF this(1)] show ?case by auto
  next
    case (6 u) with A **[OF this(1)] show ?case by auto
  next
    case (7 u)
    from region_cover_V[OF this(1)] obtain R where R: "R ∈ ℛ" "u ∈ R" by auto
    then obtain I J r where R': "R = region X I J r" "valid_region X k I J r" unfolding ℛ_def by auto
    with R' R(2) A have C:
      "intv_elem x u (I x)" "valid_intv (k x) (I x)"
    by auto
    show ?case
    proof (cases "I x")
      case (Const c)
      with 7 C(1) have "c > m" by auto
      with R R' Const show ?thesis by blast
    next
      case (Intv c)
      with 7 C(1) have "c ≥ m" by auto
      with R R' Intv show ?thesis by blast
    next
      case (Greater c)
      with C have "k x = c" by auto
      with R R' Greater show ?thesis by blast
    qed
  qed (auto intro: A simp: V_def)
  moreover have "?U ⊆ ℛ" by fastforce
  ultimately show ?thesis by blast
qed

lemma β_boundedness_eq:
  fixes m :: int
  assumes "m ≤ k x" "x ∈ X"
  shows "∃ U ⊆ ℛ. ⋃ U = {u ∈ V. u x = m}"
proof -
  note A = assms
  let ?U = "{R ∈ ℛ. ∃ I J r c. R = region X I J r ∧ valid_region X k I J r ∧ I x = Const c ∧ c = m}"
  have "⋃ ?U = {u ∈ V. u x = m}"
  proof (safe, goal_cases)
    case (2 u) with A show ?case by force
  next
    case (3 u)
    from region_cover_V[OF this(1)] obtain R where R: "R ∈ ℛ" "u ∈ R" by auto
    then obtain I J r where R': "R = region X I J r" "valid_region X k I J r" unfolding ℛ_def by auto
    with R' R(2) A have C: "intv_elem x u (I x)" "valid_intv (k x) (I x)" by auto
    show ?case
    proof (cases "I x")
      case (Const c)
      with 3 C(1) have "c = m" by auto
      with R R' Const show ?thesis by blast
    next
      case (Intv c)
      with C have "c < u x" "u x < c + 1" by auto
      from nat_intv_not_int[OF this] 3 show ?thesis by auto
    next
      case (Greater c)
      with C 3 A show ?thesis by auto
    qed
  qed (force intro: A simp: V_def)
  moreover have "?U ⊆ ℛ" by fastforce
  ultimately show ?thesis by blast
qed

lemma β_boundedness_diag_le:
  fixes m :: int
  assumes "- k y ≤ m" "m ≤ k x" "x ∈ X" "y ∈ X"
  shows "∃ U ⊆ ℛ. ⋃ U = {u ∈ V. u x - u y ≤ m}"
proof -
  from β_boundedness_diag_eq[OF assms] β_boundedness_diag_lt[OF assms] obtain U1 U2 where A:
    "U1 ⊆ ℛ" "⋃ U1 = {u ∈ V. u x - u y < m}" "U2 ⊆ ℛ" "⋃ U2 = {u ∈ V. u x - u y = m}"
  by blast
  then have "{u ∈ V. u x - u y ≤ m} = ⋃ (U1 ∪ U2)" "U1 ∪ U2 ⊆ ℛ" by auto
  then show ?thesis by blast
qed

lemma β_boundedness_le:
  fixes m :: int
  assumes "m ≤ k x" "x ∈ X"
  shows "∃ U ⊆ ℛ. ⋃ U = {u ∈ V. u x ≤ m}"
proof -
  from β_boundedness_lt[OF assms] β_boundedness_eq[OF assms] obtain U1 U2 where A:
    "U1 ⊆ ℛ" "⋃ U1 = {u ∈ V. u x  < m}" "U2 ⊆ ℛ" "⋃ U2 = {u ∈ V. u x = m}"
  by blast
  then have "{u ∈ V. u x ≤ m} = ⋃ (U1 ∪ U2)" "U1 ∪ U2 ⊆ ℛ" by auto
  then show ?thesis by blast
qed

lemma β_boundedness_ge:
  fixes m :: int
  assumes "m ≤ k x" "x ∈ X"
  shows "∃ U ⊆ ℛ. ⋃ U = {u ∈ V. u x ≥ m}"
proof -
  from β_boundedness_gt[OF assms] β_boundedness_eq[OF assms] obtain U1 U2 where A:
    "U1 ⊆ ℛ" "⋃ U1 = {u ∈ V. u x  > m}" "U2 ⊆ ℛ" "⋃ U2 = {u ∈ V. u x = m}"
  by blast
  then have "{u ∈ V. u x ≥ m} = ⋃ (U1 ∪ U2)" "U1 ∪ U2 ⊆ ℛ" by auto
  then show ?thesis by blast
qed

lemma β_boundedness_diag_lt':
  fixes m :: int
  shows
  "- k y ≤ (m :: int) ⟹ m ≤ k x ⟹ x ∈ X ⟹ y ∈ X ⟹ Z ⊆ {u ∈ V. u x - u y < m}
  ⟹ Approx⇩β Z ⊆ {u ∈ V. u x - u y < m}"
proof (goal_cases)
  case 1
  note A = this
  from β_boundedness_diag_lt[OF A(1-4)] obtain U where U:
    "U ⊆ ℛ" "{u ∈ V. u x - u y < m} = ⋃U"
  by auto
  from 1 clock_numbering have *: "v x > 0" "v y > 0" "v x ≤ n" "v y ≤ n" by auto
  have **: "⋀ c. v c = 0 ⟹ False"
  proof -
    fix c assume "v c = 0"
    moreover from clock_numbering(1) have "v c > 0" by auto
    ultimately show False by auto
  qed
  let ?M = "λ i j. if (i = v x ∧ j = v y) then Lt m else if i = j ∨ i = 0 then Le 0 else ∞"
  have "{u ∈ V. u x - u y < m} = [?M]⇘v,n⇙" unfolding DBM_zone_repr_def DBM_val_bounded_def
  using * ** proof (auto, goal_cases)
    case (1 u c)
    with clock_numbering have "c ∈ X" by metis
    with 1 show ?case unfolding V_def by auto
  next
    case (2 u c1 c2)
    with clock_numbering(1) have "x = c1" "y = c2" by auto
    with 2(5) show ?case by auto
  next
    case (3 u c1 c2)
    with clock_numbering(1) have "c1 = c2" by auto
    then show ?case by auto
  next
    case (4 u c1 c2)
    with clock_numbering(1) have "c1 = c2" by auto
    then show ?case by auto
  next
    case (5 u c1 c2)
    with clock_numbering(1) have "x = c1" "y = c2" by auto
    with 5(6) show ?case by auto
  next
    case (6 u)
    show ?case unfolding V_def
    proof safe
      fix c assume "c ∈ X"
      with clock_numbering have "v c > 0" "v c ≤ n" by auto
      with 6(6) show "u c ≥ 0" by auto
    qed
  next
    case (7 u)
    then have "dbm_entry_val u (Some x) (Some y) (Lt (real_of_int m))" by metis
    then show ?case by auto
  qed
  then have "vabstr {u ∈ V. u x - u y < m} ?M" by auto
  moreover have "normalized ?M" unfolding normalized less_eq dbm_le_def using A v_v' by auto
  ultimately show ?thesis using apx_min[OF U(2,1)] A(5) by blast
qed

lemma β_boundedness_diag_le':
  fixes m :: int
  shows
  "- k y ≤ (m :: int) ⟹ m ≤ k x ⟹ x ∈ X ⟹ y ∈ X ⟹ Z ⊆ {u ∈ V. u x - u y ≤ m}
  ⟹ Approx⇩β Z ⊆ {u ∈ V. u x - u y ≤ m}"
proof (goal_cases)
  case 1
  note A = this
  from β_boundedness_diag_le[OF A(1-4)] obtain U where U:
    "U ⊆ ℛ" "{u ∈ V. u x - u y ≤ m} = ⋃U"
  by auto
  from 1 clock_numbering have *: "v x > 0" "v y > 0" "v x ≤ n" "v y ≤ n" by auto
  have **: "⋀ c. v c = 0 ⟹ False"
  proof -
    fix c assume "v c = 0"
    moreover from clock_numbering(1) have "v c > 0" by auto
    ultimately show False by auto
  qed
  let ?M = "λ i j. if (i = v x ∧ j = v y) then Le m else if i = j ∨ i = 0 then Le 0 else ∞"
  have "{u ∈ V. u x - u y ≤ m} = [?M]⇘v,n⇙" unfolding DBM_zone_repr_def DBM_val_bounded_def
  using * **
  proof (auto, goal_cases)
    case (1 u c)
    with clock_numbering have "c ∈ X" by metis
    with 1 show ?case unfolding V_def by auto
  next
    case (2 u c1 c2)
    with clock_numbering(1) have "x = c1" "y = c2" by auto
    with 2(5) show ?case by auto
  next
    case (3 u c1 c2)
    with clock_numbering(1) have "c1 = c2" by auto
    then show ?case by auto
  next
    case (4 u c1 c2)
    with clock_numbering(1) have "c1 = c2" by auto
    then show ?case by auto
  next
    case (5 u c1 c2)
    with clock_numbering(1) have "x = c1" "y = c2" by auto
    with 5(6) show ?case by auto
  next
    case (6 u)
    show ?case unfolding V_def
    proof safe
      fix c assume "c ∈ X"
      with clock_numbering have "v c > 0" "v c ≤ n" by auto
      with 6(6) show "u c ≥ 0" by auto
    qed
  next
    case (7 u)
    then have "dbm_entry_val u (Some x) (Some y) (Le (real_of_int m))" by metis
    then show ?case by auto
  qed
  then have "vabstr {u ∈ V. u x - u y ≤ m} ?M" by auto
  moreover have "normalized ?M" unfolding normalized less_eq dbm_le_def using A v_v' by auto
  ultimately show ?thesis using apx_min[OF U(2,1)] A(5) by blast
qed

lemma β_boundedness_lt':
  fixes m :: int
  shows
  "m ≤ k x ⟹ x ∈ X ⟹ Z ⊆ {u ∈ V. u x < m} ⟹ Approx⇩β Z ⊆ {u ∈ V. u x < m}"
proof (goal_cases)
  case 1
  note A = this
  from β_boundedness_lt[OF A(1,2)] obtain U where U: "U ⊆ ℛ" "{u ∈ V. u x < m} = ⋃U" by auto
  from 1 clock_numbering have *: "v x > 0" "v x ≤ n" by auto
  have **: "⋀ c. v c = 0 ⟹ False"
  proof -
    fix c assume "v c = 0"
    moreover from clock_numbering(1) have "v c > 0" by auto
    ultimately show False by auto
  qed
  let ?M = "λ i j. if (i = v x ∧ j = 0) then Lt m else if i = j ∨ i = 0 then Le 0 else ∞"
  have "{u ∈ V. u x < m} = [?M]⇘v,n⇙" unfolding DBM_zone_repr_def DBM_val_bounded_def
  using * **
  proof (auto, goal_cases)
    case (1 u c)
    with clock_numbering have "c ∈ X" by metis
    with 1 show ?case unfolding V_def by auto
  next
    case (2 u c1)
    with clock_numbering(1) have "x = c1" by auto
    with 2(4) show ?case by auto
  next
    case (3 u c)
    with clock_numbering have "c ∈ X" by metis
    with 3 show ?case unfolding V_def by auto
  next
    case (4 u c1 c2)
    with clock_numbering(1) have "c1 = c2" by auto
    then show ?case by auto
  next
    case (5 u)
    show ?case unfolding V_def
    proof safe
      fix c assume "c ∈ X"
      with clock_numbering have "v c > 0" "v c ≤ n" by auto
      with 5(4) show "u c ≥ 0" by auto
    qed
  qed
  then have "vabstr {u ∈ V. u x < m} ?M" by auto
  moreover have "normalized ?M" unfolding normalized less_eq dbm_le_def using A v_v' by auto
  ultimately show ?thesis using apx_min[OF U(2,1)] A(3) by blast
qed

lemma β_boundedness_gt':
  fixes m :: int
  shows
  "m ≤ k x ⟹ x ∈ X ⟹ Z ⊆ {u ∈ V. u x > m} ⟹ Approx⇩β Z ⊆ {u ∈ V. u x > m}"
proof goal_cases
  case 1
  from β_boundedness_gt[OF this(1,2)] obtain U where U: "U ⊆ ℛ" "{u ∈ V. u x > m} = ⋃U" by auto
  from 1 clock_numbering have *: "v x > 0" "v x ≤ n" by auto
  have **: "⋀ c. v c = 0 ⟹ False"
  proof -
    fix c assume "v c = 0"
    moreover from clock_numbering(1) have "v c > 0" by auto
    ultimately show False by auto
  qed
  obtain M where "vabstr {u ∈ V. u x > m} M" "normalized M"
  proof (cases "m ≥ 0")
    case True
    let ?M = "λ i j. if (i = 0 ∧ j = v x) then Lt (-m) else if i = j ∨ i = 0 then Le 0 else ∞"
    have "{u ∈ V. u x > m} = [?M]⇘v,n⇙" unfolding DBM_zone_repr_def DBM_val_bounded_def
    using * **
    proof (auto, goal_cases)
      case (1 u c)
      with clock_numbering(1) have "x = c" by auto
      with 1(5) show ?case by auto
    next
      case (2 u c)
      with clock_numbering have "c ∈ X" by metis
      with 2 show ?case unfolding V_def by auto
    next
      case (3 u c1 c2)
      with clock_numbering(1) have "c1 = c2" by auto
      then show ?case by auto
    next
      case (4 u c1 c2)
      with clock_numbering(1) have "c1 = c2" by auto
      then show ?case by auto
    next
      case (5 u)
      show ?case unfolding V_def
      proof safe
        fix c assume "c ∈ X"
        with clock_numbering have c: "v c > 0" "v c ≤ n" by auto
        show "u c ≥ 0"
        proof (cases "v c = v x")
          case False
          with 5(4) c show ?thesis by auto
        next
          case True
          with 5(4) c have "- u c < - m" by auto
          with ‹m ≥ 0› show ?thesis by auto
        qed
      qed
    qed
    moreover have "normalized ?M" unfolding normalized using 1 v_v' by auto
    ultimately show ?thesis by (intro that[of ?M]) auto
  next
    case False
    then have "{u ∈ V. u x > m} = V" unfolding V_def using ‹x ∈ X› by auto
    with ℛ_union all_dbm that show ?thesis by auto
  qed
  with apx_min[OF U(2,1)] 1(3) show ?thesis by blast
qed

lemma obtains_dbm_le:
  fixes m :: int
  assumes "x ∈ X" "m ≤ k x"
  obtains M where "vabstr {u ∈ V. u x ≤ m} M" "normalized M"
proof -
  from assms clock_numbering have *: "v x > 0" "v x ≤ n" by auto
  have **: "⋀ c. v c = 0 ⟹ False"
  proof -
    fix c assume "v c = 0"
    moreover from clock_numbering(1) have "v c > 0" by auto
    ultimately show False by auto
  qed
  let ?M = "λ i j. if (i = v x ∧ j = 0) then Le m else if i = j ∨ i = 0 then Le 0 else ∞"
  have "{u ∈ V. u x ≤ m} = [?M]⇘v,n⇙" unfolding DBM_zone_repr_def DBM_val_bounded_def
  using * **
  proof (auto, goal_cases)
    case (1 u c)
    with clock_numbering have "c ∈ X" by metis
    with 1 show ?case unfolding V_def by auto
  next
    case (2 u c1)
    with clock_numbering(1) have "x = c1" by auto
    with 2(4) show ?case by auto
  next
    case (3 u c)
    with clock_numbering have "c ∈ X" by metis
    with 3 show ?case unfolding V_def by auto
  next
    case (4 u c1 c2)
    with clock_numbering(1) have "c1 = c2" by auto
    then show ?case by auto
  next
    case (5 u)
    show ?case unfolding V_def
    proof safe
      fix c assume "c ∈ X"
      with clock_numbering have "v c > 0" "v c ≤ n" by auto
      with 5(4) show "u c ≥ 0" by auto
    qed
  qed
  then have "vabstr {u ∈ V. u x ≤ m} ?M" by auto
  moreover have "normalized ?M" unfolding normalized using assms v_v' by auto
  ultimately show ?thesis ..
qed


lemma β_boundedness_le':
  fixes m :: int
  shows
  "m ≤ k x ⟹ x ∈ X ⟹ Z ⊆ {u ∈ V. u x ≤ m} ⟹ Approx⇩β Z ⊆ {u ∈ V. u x ≤ m}"
proof (goal_cases)
  case 1
  from β_boundedness_le[OF this(1,2)] obtain U where U: "U ⊆ ℛ" "{u ∈ V. u x ≤ m} = ⋃U" by auto
  from obtains_dbm_le 1 obtain M where "vabstr {u ∈ V. u x ≤ m} M" "normalized M" by auto
  with apx_min[OF U(2,1)] 1(3) show ?thesis by blast
qed

lemma obtains_dbm_ge:
  fixes m :: int
  assumes "x ∈ X" "m ≤ k x"
  obtains M where "vabstr {u ∈ V. u x ≥ m} M" "normalized M"
proof -
  from assms clock_numbering have *: "v x > 0" "v x ≤ n" by auto
  have **: "⋀ c. v c = 0 ⟹ False"
  proof -
    fix c assume "v c = 0"
    moreover from clock_numbering(1) have "v c > 0" by auto
    ultimately show False by auto
  qed
  obtain M where "vabstr {u ∈ V. u x ≥ m} M" "normalized M"
  proof (cases "m ≥ 0")
    case True
    let ?M = "λ i j. if (i = 0 ∧ j = v x) then Le (-m) else if i = j ∨ i = 0 then Le 0 else ∞"
    have "{u ∈ V. u x ≥ m} = [?M]⇘v,n⇙" unfolding DBM_zone_repr_def DBM_val_bounded_def
    using * **
    proof (auto, goal_cases)
      case (1 u c)
      with clock_numbering(1) have "x = c" by auto
      with 1(5) show ?case by auto
    next
      case (2 u c)
      with clock_numbering have "c ∈ X" by metis
      with 2 show ?case unfolding V_def by auto
    next
      case (3 u c1 c2)
      with clock_numbering(1) have "c1 = c2" by auto
      then show ?case by auto
    next
      case (4 u c1 c2)
      with clock_numbering(1) have "c1 = c2" by auto
      then show ?case by auto
    next
      case (5 u)
      show ?case unfolding V_def
      proof safe
        fix c assume "c ∈ X"
        with clock_numbering have c: "v c > 0" "v c ≤ n" by auto
        show "u c ≥ 0"
        proof (cases "v c = v x")
          case False
          with 5(4) c show ?thesis by auto
        next
          case True
          with 5(4) c have "- u c ≤ - m" by auto
          with ‹m ≥ 0› show ?thesis by auto
        qed
      qed
    qed
    moreover have "normalized ?M" unfolding normalized using assms v_v' by auto
    ultimately show ?thesis by (intro that[of ?M]) auto
  next
    case False
    then have "{u ∈ V. u x ≥ m} = V" unfolding V_def using ‹x ∈ X› by auto
    with ℛ_union all_dbm that show ?thesis by auto
  qed
  then show ?thesis ..
qed

lemma β_boundedness_ge':
  fixes m :: int
  shows "m ≤ k x ⟹ x ∈ X ⟹ Z ⊆ {u ∈ V. u x ≥ m} ⟹ Approx⇩β Z ⊆ {u ∈ V. u x ≥ m}"
proof (goal_cases)
  case 1
  from β_boundedness_ge[OF this(1,2)] obtain U where U: "U ⊆ ℛ" "{u ∈ V. u x ≥ m} = ⋃U" by auto
  from obtains_dbm_ge 1 obtain M where "vabstr {u ∈ V. u x ≥ m} M" "normalized M" by auto
  with apx_min[OF U(2,1)] 1(3) show ?thesis by blast
qed

end

end