Theory Timed_Automata.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