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
  "X0 = {x  X.  d. I x = Intv d}; refl_on X0 r; trans r; total_on X0 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)  X0 = {x  X.  d. I x = Intv d} 
    x  X0.  y  X0. (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 ?X0 = "{x  X.  d. I' x = Intv d}"
    { fix x y assume x: "x  ?X0" and y: "y  ?X0"
      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  ?X0.  y  ?X0. (x, y)  r'  frac (u x)  frac (u y)" by auto
    from A(5) have "xX. 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 ?X0 = "{x  X.  d. I x = Intv d}"
    { fix x y assume x: "x  ?X0" and y: "y  ?X0"
      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  ?X0.  y  ?X0. (x, y)  r  frac (u x)  frac (u y)" by auto
    from A(5) have "xX. 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 ?X0 = "{x  X.  d. ?I x = Intv d}"
  let ?r = "{(x,y). x  ?X0  y  ?X0  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 "xX. 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':
  "xX. 0  v x  xX. 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 ?X0 = "{x  X. d. I x = Intv d}"
    from A(4) show " x  ?X0.  y  ?X0. ((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 ?X0 = "{x  X. d. I' x = Intv d}"
    from A(4) show " x  ?X0.  y  ?X0. ((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 ?X0 = "{x  X. d. I x = Intv d}"
    from A have "refl_on ?X0 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 ( in.  jn. 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  in.  jn. 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 " in.  jn. ?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 " in.  jn. ?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 " in.  jn. 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 " in.  jn. 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 "(cX. (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 " in. 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= {}  (in. 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 *: " in. 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 *: " in. 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 ?X0 = "{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 "?X0 = ?X0" by auto
      next
        case 4 from R R' show "x?X0. y?X0. (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 "?X0 = ?X0" ..
        show "refl_on ?X0 r" using R' by auto
        show "trans r" using R' by auto
        show "total_on ?X0 r" using R' by auto
        show "xX. valid_intv (k x) (I x)" using R' by auto
        show "xaX. yaX. 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 ?X0 = "{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 "?X0 = ?X0" by auto
      next
        case 4 from R R' show "x?X0. y?X0. (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 "?X0 = ?X0" ..
        show "refl_on ?X0 r" using R' by auto
        show "trans r" using R' by auto
        show "total_on ?X0 r" using R' by auto
        show "xX. 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