Theory Timed_Automata.Regions

chapter ‹The Classic Construction for Decidability›

theory Regions
imports Timed_Automata TA_Misc
begin

text ‹
  The following is a formalization of regions in the correct version of Patricia Bouyer et al.
›

section ‹Definition of Regions›

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

datatype intv =
  Const nat |
  Intv nat |
  Greater nat

type_synonym t = real


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

abbreviation "total_preorder r ≡ refl r ∧ trans r"

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

inductive_set region for X I r
where
  "∀ x ∈ X. u x ≥ 0 ⟹ ∀ x ∈ X. intv_elem x u (I x) ⟹ X⇩0 = {x ∈ X. ∃ d. I x = Intv d} ⟹
   ∀ x ∈ X⇩0. ∀ y ∈ X⇩0. (x, y) ∈ r ⟷ frac (u x) ≤ frac (u y)
  ⟹ u ∈ region X I 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"

inductive_set Succ for ℛ R where
  "u ∈ R ⟹ R ∈ ℛ ⟹ R' ∈ ℛ ⟹ t ≥ 0 ⟹ R' = [u ⊕ t]⇩ℛ ⟹ R' ∈ Succ ℛ 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)"

declare valid_intv.intros[intro]
declare intv_elem.intros[intro]
declare Succ.intros[intro]

declare Succ.cases[elim]

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)

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

lemma valid_regions_distinct:
  "valid_region X k I r ⟹ valid_region X k I' r' ⟹ v ∈ region X I r ⟹ v ∈ region X I' r'
  ⟹ region X I r = region X I' r'"
proof goal_cases
  case 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
  from A show ?thesis
  proof (safe, goal_cases)
    case A: (1 u)
    have "intv_elem x u (I' x)" if "x ∈ X" for x using A(5) * that by auto
    then have B: "∀ x ∈ X. intv_elem x u (I' x)" by auto
    let ?X⇩0 = "{x ∈ X. ∃ d. I' x = Intv d}"
    { fix x y assume x: "x ∈ ?X⇩0" and y: "y ∈ ?X⇩0"
      have "(x, y) ∈ r' ⟷ frac (u x) ≤ frac (u y)"
      proof
        assume "frac (u x) ≤ frac (u y)"
        with A(5) x y * have "(x,y) ∈ r" by auto
        with A(3) x y * have "frac (v x) ≤ frac (v y)" by auto
        with A(4) x y   show "(x,y) ∈ r'" by auto
      next
        assume "(x,y) ∈ r'"
        with A(4) x y   have "frac (v x) ≤ frac (v y)" by auto
        with A(3) x y * have "(x,y) ∈ r" by auto
        with A(5) x y * show "frac (u x) ≤ frac (u y)" by auto
      qed
    }
    then have *: "∀ x ∈ ?X⇩0. ∀ y ∈ ?X⇩0. (x, y) ∈ r' ⟷ frac (u x) ≤ frac (u y)" by auto
    from A(5) have "∀x∈X. 0 ≤ u x" by auto
    from region.intros[OF this B _ *] show ?case by auto
  next
    case A: (2 u)
    have "intv_elem x u (I x)" if "x ∈ X" for x using * A(5) that by auto
    then have B: "∀ x ∈ X. intv_elem x u (I x)" by auto
    let ?X⇩0 = "{x ∈ X. ∃ d. I x = Intv d}"
    { fix x y assume x: "x ∈ ?X⇩0" and y: "y ∈ ?X⇩0"
      have "(x, y) ∈ r ⟷ frac (u x) ≤ frac (u y)"
      proof
        assume "frac (u x) ≤ frac (u y)"
        with A(5) x y * have "(x,y) ∈ r'" by auto
        with A(4) x y * have "frac (v x) ≤ frac (v y)" by auto
        with A(3) x y   show "(x,y) ∈ r" by auto
      next
        assume "(x,y) ∈ r"
        with A(3) x y   have "frac (v x) ≤ frac (v y)" by auto
        with A(4) x y * have "(x,y) ∈ r'" by auto
        with A(5) x y * show "frac (u x) ≤ frac (u y)" by auto
      qed
    }
    then have *:"∀ x ∈ ?X⇩0. ∀ y ∈ ?X⇩0. (x, y) ∈ r ⟷ frac (u x) ≤ frac (u y)" by auto
    from A(5) have "∀x∈X. 0 ≤ u x" by auto
    from region.intros[OF this B _ *] show ?case by auto
  qed
qed

lemma ℛ_regions_distinct:
  "⟦ℛ = {region X I r | I r. valid_region X k I r}; R ∈ ℛ; v ∈ R; R' ∈ ℛ; R ≠ R'⟧ ⟹ v ∉ R'"
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 k c ≡
    if (c > k) then Greater k
    else if (∃ x :: nat. x = c) then (Const (nat (floor c)))
    else (Intv (nat (floor c)))"

lemma region_cover:
  "∀ x ∈ X. u x ≥ 0 ⟹ ∃ R. R ∈ {region X I r | I r. valid_region X k I r} ∧ u ∈ R"
proof (standard, standard)
  assume assm: "∀ x ∈ X. 0 ≤ u x"
  let ?I = "λ x. intv_of (k x) (u x)"
  let ?X⇩0 = "{x ∈ X. ∃ d. ?I x = Intv d}"
  let ?r = "{(x,y). x ∈ ?X⇩0 ∧ y ∈ ?X⇩0 ∧ frac (u x) ≤ frac (u y)}"
  show "u ∈ region X ?I ?r"
  proof (standard, auto simp: assm, goal_cases)
    case (1 x)
    thus ?case unfolding intv_of_def
    proof (auto, goal_cases)
      case A: (1 a)
      from A(2) have "⌊u x⌋ = u x" by (metis of_int_floor_cancel of_int_of_nat_eq)
      with assm A(1) have "u x = real (nat ⌊u x⌋)" by auto
      then show ?case by auto
    next
      case A: 2
      from A(1,2) have "real (nat ⌊u x⌋) < u x"
      by (metis assm floor_less_iff int_nat_eq less_eq_real_def less_irrefl not_less
                of_int_of_nat_eq of_nat_0)
      moreover from assm have "u x < real (nat (⌊u x⌋) + 1)" by linarith
      ultimately show ?case by auto
    qed
  qed
  have "valid_intv (k x) (intv_of (k x) (u x))" if "x ∈ X" for x using that
  proof (auto simp: intv_of_def, goal_cases)
    case 1 then show ?case by (intro valid_intv.intros(1)) (auto, linarith)
  next
    case 2
    then show ?case using assm floor_less_iff nat_less_iff
    by (intro valid_intv.intros(2)) fastforce+
  qed
  then have "valid_region X k ?I ?r"
  by (intro valid_region.intros) (auto simp: refl_on_def trans_def total_on_def)
  then show "region X ?I ?r ∈ {region X I r | I r. valid_region X k I r}" by auto
qed

lemma intv_not_empty:
  obtains d where "intv_elem x (v(x := d)) (I x)"
proof (cases "I x", goal_cases)
  case (1 d)
  then have "intv_elem x (v(x := d)) (I x)" by auto
  with 1 show ?case by auto
next
  case (2 d)
  then have "intv_elem x (v(x := d + 0.5)) (I x)" by auto
  with 2 show ?case by auto
next
  case (3 d)
  then have "intv_elem x (v(x := d + 0.5)) (I x)" by auto
  with 3 show ?case by auto
qed

fun get_intv_val :: "intv ⇒ real ⇒ real"
where
  "get_intv_val (Const d)   _ = d" |
  "get_intv_val (Intv d)    f = d + f"  |
  "get_intv_val (Greater d) _ = d + 1"

lemma region_not_empty_aux:
  assumes "0 < f" "f < 1" "0 < g" "g < 1"
  shows "frac (get_intv_val (Intv d) f) ≤ frac (get_intv_val (Intv d') g) ⟷ f ≤ g"
using assms by (simp, metis frac_eq frac_nat_add_id less_eq_real_def)

lemma region_not_empty:
  assumes "finite X" "valid_region X k I r"
  shows "∃ u. u ∈ region X I r"
proof -
  let ?X⇩0 = "{x ∈ X. ∃d. I x = Intv d}"
  obtain f :: "'a ⇒ nat" where f:
    "∀x∈?X⇩0. ∀y∈?X⇩0. f x ≤ f y ⟷ (x, y) ∈ r"
     apply (rule finite_total_preorder_enumeration)
         apply (subgoal_tac "finite ?X⇩0")
          apply assumption
  using assms by auto
  let ?M = "if ?X⇩0 ≠ {} then Max {f x | x. x ∈ ?X⇩0} else 1"
  let ?f = "λ x. (f x + 1) / (?M + 2)"
  let ?v = "λ x. get_intv_val (I x) (if x ∈ ?X⇩0 then ?f x else 1)"
  have frac_intv: "∀x∈?X⇩0. 0 < ?f x ∧ ?f x < 1"
  proof (standard, goal_cases)
    case (1 x)
    then have *: "?X⇩0 ≠ {}" by auto
    have "f x ≤ Max {f x | x. x ∈ ?X⇩0}" apply (rule Max_ge) using ‹finite X› 1 by auto
    with 1 show ?case by auto
  qed
  with region_not_empty_aux have *:
    "∀x∈?X⇩0. ∀y∈?X⇩0. frac (?v x) ≤ frac (?v y) ⟷ ?f x ≤ ?f y"
  by force
  have "∀x∈?X⇩0. ∀y∈?X⇩0. ?f x ≤ ?f y ⟷ f x ≤ f y" by (simp add: divide_le_cancel)+
  with f have "∀x∈?X⇩0. ∀y∈?X⇩0. ?f x ≤ ?f y ⟷ (x, y) ∈ r" by auto
  with * have frac_order: "∀x∈?X⇩0. ∀y∈?X⇩0. frac (?v x) ≤ frac (?v y) ⟷ (x, y) ∈ r" by auto
  have "?v ∈ region X I r"
  proof standard
    show "∀x∈X. intv_elem x ?v (I x)"
    proof (standard, case_tac "I x", goal_cases)
      case (2 x d)
      then have *: "x ∈ ?X⇩0" by auto
      with frac_intv have "0 < ?f x" "?f x < 1" by auto
      moreover from 2 have "?v x = d + ?f x" by auto
      ultimately have "?v x < d + 1 ∧ d < ?v x" by linarith
      then show "intv_elem x ?v (I x)" by (subst 2(2)) (intro intv_elem.intros(2), auto)
    qed auto
  next
    show "∀x∈X. 0 ≤ get_intv_val (I x) (if x ∈ ?X⇩0 then ?f x else 1)"
    by (standard, case_tac "I x") auto
  next
    show "{x ∈ X. ∃d. I x = Intv d} = {x ∈ X. ∃d. I x = Intv d}" ..
  next
    from frac_order show "∀x∈?X⇩0. ∀y∈?X⇩0. ((x, y) ∈ r) = (frac (?v x) ≤ frac (?v y))" by blast
  qed
  then show ?thesis by auto
qed

text ‹
  Now we can show that there is always exactly one region a valid valuation belongs to.
›

lemma regions_partition:
  "ℛ = {region X I r | I r. valid_region X k I r} ⟹ ∀x ∈ X. 0 ≤ u x ⟹ ∃! R ∈ ℛ. u ∈ R"
proof (goal_cases)
  case 1
  note A = this
  with region_cover[OF A(2)] obtain R where R: "R ∈ ℛ ∧ u ∈ R" by fastforce
  moreover have "R' = R" if "R' ∈ ℛ ∧ u ∈ R'" for R'
  using that R valid_regions_distinct unfolding A(1) by blast
  ultimately show ?thesis by auto
qed

lemma region_unique:
  "ℛ = {region X I r | I r. valid_region X k I r} ⟹ u ∈ R ⟹ R ∈ ℛ ⟹ [u]⇩ℛ = R"
proof (goal_cases)
  case 1
  note A = this
  from A obtain I r where *: "valid_region X k I r" "R = region X I r" "u ∈ region X I r" by auto
  from this(3) have "∀x∈X. 0 ≤ u x" by auto
  from theI'[OF regions_partition[OF A(1) this]] A(1) obtain I' r' where
    v: "valid_region X k I' r'" "[u]⇩ℛ = region X I' r'" "u ∈ region X I' r'"
  unfolding part_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':
  "ℛ = {region X I r | I r. valid_region X k I r} ⟹ ∀x∈X. 0 ≤ v x ⟹ ∀x∈X. 0 ≤ v' x ⟹ v' ∈ [v]⇩ℛ
  ⟹ [v']⇩ℛ = [v]⇩ℛ"
proof (goal_cases)
  case 1
  note A = this
  from theI'[OF regions_partition[OF A(1,2)]] A(1,4) obtain I r where
    v: "valid_region X k I r" "[v]⇩ℛ = region X I r" "v' ∈ region X I r"
  unfolding part_def by auto
  from theI'[OF regions_partition[OF A(1,3)]] A(1) obtain I' r' where
    v': "valid_region X k I' r'" "[v']⇩ℛ = region X I' r'" "v' ∈ region X I' r'"
  unfolding part_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:
  "ℛ = {region X I r | I r. valid_region X k I r} ⟹ R ∈ ℛ ⟹ v ∈ R ⟹ t ≥ 0 ⟹ [v ⊕ t]⇩ℛ ∈ ℛ"
proof goal_cases
  case A: 1
  then obtain I r where "v ∈ region X I r" by auto
  from this(1) have "∀ x ∈ X. v x ≥ 0" by auto
  with A(4) have "∀ x ∈ X. (v ⊕ t) x ≥ 0" unfolding cval_add_def by simp
  from regions_partition[OF A(1) this] obtain R' where "R' ∈ ℛ" "(v ⊕ t) ∈ R'" by auto
  with region_unique[OF A(1) this(2,1)] show ?case by auto
qed

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

lemma valid_regions_I_cong:
  "valid_region X k I r ⟹ ∀ x ∈ X. I x = I' x ⟹ region X I r = region X I' r ∧ valid_region X k I' r"
proof (safe, goal_cases)
  case (1 v)
  note A = this
  then have [simp]:"⋀ x. x ∈ X ⟹ I' x = I x" by metis
  show ?case
  proof (standard, goal_cases)
    case 1
    from A(3) show ?case by auto
  next
    case 2
    from A(3) show ?case by auto
  next
    case 3
    show "{x ∈ X. ∃d. I x = Intv d} = {x ∈ X. ∃d. I' x = Intv d}" by auto
  next
    case 4
    let ?X⇩0 = "{x ∈ X. ∃d. I x = Intv d}"
    from A(3) show "∀ x ∈ ?X⇩0. ∀ y ∈ ?X⇩0. ((x, y) ∈ r) = (frac (v x) ≤ frac (v y))" by auto
  qed
next
  case (2 v)
  note A = this
  then have [simp]:"⋀ x. x ∈ X ⟹ I' x = I x" by metis
  show ?case
  proof (standard, goal_cases)
    case 1
    from A(3) show ?case by auto
  next
    case 2
    from A(3) show ?case by auto
  next
    case 3
    show "{x ∈ X. ∃d. I' x = Intv d} = {x ∈ X. ∃d. I x = Intv d}" by auto
  next
    case 4
    let ?X⇩0 = "{x ∈ X. ∃d. I' x = Intv d}"
    from A(3) show "∀ x ∈ ?X⇩0. ∀ y ∈ ?X⇩0. ((x, y) ∈ r) = (frac (v x) ≤ frac (v y))" by auto
  qed
next
  case 3
  note A = this
  then have [simp]:"⋀ x. x ∈ X ⟹ I' x = I x" 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 auto
qed

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

lemma finite_ℛ:
  notes [[simproc add: finite_Collect]] finite_subset[intro]
  fixes X k
  defines "ℛ ≡ {region X I r | I r. valid_region X k I r}"
  assumes "finite X"
  shows "finite ℛ"
proof -
  { fix I r assume A: "valid_region X k I r"
    let ?X⇩0 = "{x ∈ X. ∃d. I x = Intv d}"
    from A have "refl_on ?X⇩0 r" by auto
    then have "r ⊆ X × X" by (auto simp: refl_on_def)
    then have "r ∈ Pow (X × X)" by auto
  }
  then have "{r. ∃I. valid_region X k I r} ⊆ Pow (X × X)" by auto
  with ‹finite X› have fin: "finite {r. ∃I. valid_region X k I r}" by auto
  let ?m = "Max {k x | x. x ∈ X}"
  let ?I = "{intv. intv_const intv ≤ ?m}"
  let ?fin_map = "λ I. ∀x. (x ∈ X ⟶ I x ∈ ?I) ∧ (x ∉ X ⟶ I x = Const 0)"
  let ?ℛ = "{region X I r | I r. valid_region X k I r ∧ ?fin_map I}"
  have "?I = (Const ` {d. d ≤ ?m}) ∪ (Intv ` {d. d ≤ ?m}) ∪ (Greater ` {d. d ≤ ?m})"
  by auto (case_tac x, auto)
  then have "finite ?I" by auto
  from finite_set_of_finite_funs[OF ‹finite X› this] have "finite {I. ?fin_map I}" .
  with fin have "finite {(I, r). valid_region X k I r ∧ ?fin_map I}"
  by (fastforce intro: pairwise_finiteI finite_ex_and1 frac_add_le_preservation del: finite_subset)
  then have "finite ?ℛ" by fastforce
  moreover have "ℛ ⊆ ?ℛ"
  proof
    fix R assume R: "R ∈ ℛ"
    then obtain I r where I: "R = region X I r" "valid_region X k I r" unfolding ℛ_def by auto
    let ?I = "λ x. if x ∈ X then I x else Const 0"
    let ?R = "region X ?I r"
    from valid_regions_I_cong[OF I(2)] I have "R = ?R" "valid_region X k ?I r" by auto
    moreover have "∀x. x ∉ X ⟶ ?I x = Const 0" by auto
    moreover have "∀x. x ∈ X ⟶ intv_const (I x) ≤ ?m"
    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 ≤ ?m" by (auto intro: Max_ge)
      ultimately  show "intv_const (I x) ≤ Max {k x |x. x ∈ X}" by (cases "I x") auto
    qed
    ultimately show "R ∈ ?ℛ" by force
  qed
  ultimately show "finite ℛ" by blast
qed

lemma SuccI2:
  "ℛ = {region X I r | I r. valid_region X k I r} ⟹ v ∈ R ⟹ R ∈ ℛ ⟹ t ≥ 0 ⟹ R' = [v ⊕ t]⇩ℛ
  ⟹ R' ∈ Succ ℛ R"
proof goal_cases
  case A: 1
  from Succ.intros[OF A(2) A(3) regions_closed[OF A(1,3,2,4)] A(4)] A(5) show ?case by auto
qed


section ‹Set of Regions›

text ‹
  The first property Bouyer shows is that these regions form a 'set of regions'.
›

text ‹
  For the unbounded region in the upper right corner, the set of successors only
  contains itself.
›

lemma Succ_refl:
  "ℛ = {region X I r |I r. valid_region X k I r} ⟹ finite X ⟹ R ∈ ℛ ⟹ R ∈ Succ ℛ R"
proof goal_cases
  case A: 1
  then obtain I r where R: "valid_region X k I r" "R = region X I r" by auto
  with A region_not_empty obtain v where v: "v ∈ region X I r" by metis
  with R have *: "(v ⊕ 0) ∈ R" unfolding cval_add_def by auto
  from regions_closed'[OF A(1,3-)] v R have "(v ⊕ 0) ∈ [v ⊕ 0]⇩ℛ" by auto
  from region_unique[OF A(1) * A(3)] A(3) v[unfolded R(2)[symmetric]] show ?case by auto
qed

lemma Succ_refl':
  "ℛ = {region X I r |I r. valid_region X k I r} ⟹ finite X ⟹ ∀ x ∈ X. ∃ c. I x = Greater c
  ⟹ region X I r ∈ ℛ ⟹ Succ ℛ (region X I r) = {region X I r}"
proof goal_cases
  case A: 1
  have *: "(v ⊕ t) ∈ region X I r" if v: "v ∈ region X I r" and t: "t ≥ 0" for v and t :: t
  proof ((rule region.intros), auto, goal_cases)
    case 1
    with v t show ?case unfolding cval_add_def by auto
  next
    case (2 x)
    with A obtain c where c: "I x = Greater c" by auto
    with v 2 have "v x > c" by fastforce
    with t have "v x + t > c" by auto
    then have "(v ⊕ t) x > c" by (simp add: cval_add_def)
    from intv_elem.intros(3)[of c "v ⊕ t", OF this] c show ?case by auto
  next
    case (3 x)
    from this(1) A obtain c where "I x = Greater c" by auto
    with 3(2) show ?case by auto
  next
    case (4 x)
    from this(1) A obtain c where "I x = Greater c" by auto
    with 4(2) show ?case by auto
  qed
  show ?case
  proof (standard, standard)
    fix R assume R: "R ∈ Succ ℛ (region X I r)"
    then obtain v t where v:
      "v ∈ region X I r" "R = [v ⊕ t]⇩ℛ" "R ∈ ℛ" "t ≥ 0"
    by (cases rule: Succ.cases) auto
    from v(1) have **: "∀x ∈ X. 0 ≤ v x" by auto
    with v(4) have "∀x ∈ X. 0 ≤ (v ⊕ t) x" unfolding cval_add_def by auto
    from *[OF v(1,4)] regions_partition'[OF A(1) ** this] region_unique[OF A(1) v(1) A(4)] v(2)
    show "R ∈ {region X I r}" by auto
  next
    from A(4) obtain I' r' where R': "region X I r = region X I' r'" "valid_region X k I' r'"
    unfolding A(1) by auto
    with region_not_empty[OF A(2) this(2)] obtain v where v: "v ∈ region X I r" by auto
    from region_unique[OF A(1) this A(4)] have *: "[v ⊕ 0]⇩ℛ = region X I r"
    unfolding cval_add_def by auto
    with v A(4) have "[v ⊕ 0]⇩ℛ ∈ Succ ℛ (region X I r)" by (intro Succ.intros; auto)
    with * show "{region X I r} ⊆ Succ ℛ (region X I r)" by auto
  qed
qed

text ‹
  Defining the closest successor of a region. Only exists if at least one interval is upper-bounded.
›

definition
  "succ ℛ R =
  (SOME R'. R' ∈ Succ ℛ R ∧ (∀ u ∈ R. ∀ t ≥ 0. (u ⊕ t) ∉ R ⟶ (∃ t' ≤ t. (u ⊕ t') ∈ R' ∧ 0 ≤ t')))"

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!]

text ‹
  What Bouyer states at the end. However, we have to be a bit more precise than in her statement.
›

lemma closest_prestable_1:
  fixes I X k r
  defines "ℛ ≡ {region X I r |I r. valid_region X k I r}"
  defines "R ≡ region X I r"
  defines "Z ≡ {x ∈ X . ∃ c. I x = Const c}"
  assumes "Z ≠ {}"
  defines "I'≡ λ x. if x ∉ Z then I x else if intv_const (I x) = k x then Greater (k x) else Intv (intv_const (I x))"
  defines "r' ≡ r ∪ {(x,y) . x ∈ Z ∧ y ∈ X ∧ intv_const (I x) < k x ∧ isIntv (I' y)}"
  assumes "finite X"
  assumes "valid_region X k I r"
  shows   "∀ v ∈ R. ∀ t>0. ∃t'≤t. (v ⊕ t') ∈ region X I' r' ∧ t' ≥ 0"
  and     "∀ v ∈ region X I' r'. ∀ t≥0. (v ⊕ t) ∉ R"
  and     "∀ x ∈ X. ¬ isConst (I' x)"
  and     "∀ v ∈ R. ∀ t < 1. ∀ t' ≥ 0. (v ⊕ t') ∈ region X I' r'
           ⟶ {x. x ∈ X ∧ (∃ c. I x = Intv c ∧ v x + t ≥ c + 1)}
                = {x. x ∈ X ∧ (∃ c. I' x = Intv c ∧ (v ⊕ t') x + (t - t') ≥ c + 1)}"
proof (safe, goal_cases)
  fix v assume v: "v ∈ R" fix t :: t assume t: "0 < t"
  have elem: "intv_elem x v (I x)" if x: "x ∈ X" for x using v x unfolding R_def by auto
  have *: "(v ⊕ t) ∈ region X I' r'" if A: "∀ x ∈ X. ¬ isIntv (I x)" and t: "t > 0" "t < 1" for t
  proof (standard, goal_cases)
    case 1
    from v have "∀ x ∈ X. v x ≥ 0" unfolding R_def by auto
    with t show ?case unfolding cval_add_def by auto
  next
    case 2
    show ?case
    proof (standard, case_tac "I x", goal_cases)
      case (1 x c)
      with elem[OF ‹x ∈ X›] have "v x = c" by auto
      show ?case
      proof (cases "intv_const (I x) = k x", auto simp: 1 I'_def Z_def, goal_cases)
        case 1
        with ‹v x = c› have "v x = k x" by auto
        with t show ?case by (auto simp: cval_add_def)
      next
        case 2
        from assms(8) 1 have "c ≤ k x" by (cases rule: valid_region.cases) auto
        with 2 have "c < k x" by linarith
        from t ‹v x = c› show ?case by (auto simp: cval_add_def)
      qed
    next
      case (2 x c)
      with A show ?case by auto
    next
      case (3 x c)
      then have "I' x = Greater c" unfolding I'_def Z_def by auto
      with t 3 elem[OF ‹x ∈ X›] show ?case by (auto simp: cval_add_def)
    qed
  next
    case 3 show "{x ∈ X. ∃d. I' x = Intv d} = {x ∈ X. ∃d. I' x = Intv d}" ..
  next
    case 4
    let ?X⇩0' = "{x ∈ X. ∃d. I' x = Intv d}"
    show "∀x∈?X⇩0'. ∀y∈?X⇩0'. ((x, y) ∈ r') = (frac ((v ⊕ t) x) ≤ frac ((v ⊕ t) y))"
    proof (safe, goal_cases)
      case (1 x y d d')
      note B = this
      have "x ∈ Z" apply (rule ccontr) using A B by (auto simp: I'_def)
      with elem[OF B(1)] have "frac (v x) = 0 " unfolding Z_def by auto
      with frac_distr[of t "v x"] t have *: "frac (v x + t) = t" by auto
      have "y ∈ Z" apply (rule ccontr) using A B by (auto simp: I'_def)
      with elem[OF B(3)] have "frac (v y) = 0 " unfolding Z_def by auto
      with frac_distr[of t "v y"] t have "frac (v y + t) = t" by auto
      with * show ?case unfolding cval_add_def by auto
    next
      case B: (2 x)
      have "x ∈ Z" apply (rule ccontr) using A B by (auto simp: I'_def)
      with B have "intv_const (I x) ≠ k x" unfolding I'_def by auto
      with B(1) assms(8) have "intv_const (I x) < k x" by (fastforce elim!: valid_intv.cases)
      with B ‹x ∈ Z› show ?case unfolding r'_def by auto
    qed
  qed
  let ?S = "{1 - frac (v x) | x. x ∈ X ∧ isIntv (I x)}"
  let ?t = "Min ?S"
  { assume A: "∃ x ∈ X. isIntv (I x)"
    from ‹finite X› have "finite ?S" by auto
    from A have "?S ≠ {}" by auto
    from Min_in[OF ‹finite ?S› this] obtain x where
      x: "x ∈ X" "isIntv (I x)" "?t = 1 - frac (v x)"
    by force
    have "frac (v x) < 1" by (simp add: frac_lt_1)
    then have "?t > 0" by (simp add: x(3))
    then have "?t / 2 > 0" by auto
    from x(2) obtain c where "I x = Intv c" by (auto)
    with elem[OF x(1)] have v_x: "c < v x" "v x < c + 1" by auto
    from nat_intv_frac_gt0[OF this] have "frac (v x) > 0" .
    with x(3) have "?t < 1" by auto
    { fix t :: t assume t: "0 < t" "t ≤ ?t / 2"
      { fix y assume "y ∈ X" "isIntv (I y)"
        then have "1 - frac (v y) ∈ ?S" by auto
        from Min_le[OF ‹finite ?S› this] ‹?t > 0› t have "t  < 1 - frac (v y)" by linarith
      } note frac_bound = this
      have "(v ⊕ t) ∈ region X I' r'"
      proof (standard, goal_cases)
        case 1
        from v have "∀ x ∈ X. v x ≥ 0" unfolding R_def by auto
        with ‹?t > 0› t show ?case unfolding cval_add_def by auto
      next
        case 2
        show ?case
        proof (standard, case_tac "I x", goal_cases)
          case A: (1 x c)
          with elem[OF ‹x ∈ X›] have "v x = c" by auto
          show ?case
          proof (cases "intv_const (I x) = k x", auto simp: A I'_def Z_def, goal_cases)
            case 1
            with ‹v x = c› have "v x = k x" by auto
            with ‹?t > 0› t show ?case by (auto simp: cval_add_def)
          next
            case 2
            from assms(8) A have "c ≤ k x" by (cases rule: valid_region.cases) auto
            with 2 have "c < k x" by linarith
            from ‹v x = c› ‹?t < 1› t show ?case
            by (auto simp: cval_add_def)
          qed
        next
          case (2 x c)
          with elem[OF ‹x ∈ X›] have v: "c < v x" "v x < c + 1" by auto
          with ‹?t > 0› have "c < v x + (?t / 2)" by auto
          from 2 have "I' x = I x" unfolding I'_def Z_def by auto
          from frac_bound[OF 2(1)] 2(2) have "t  < 1 - frac (v x)" by auto
          from frac_add_le_preservation[OF v(2) this] t v(1) 2 show ?case
          unfolding cval_add_def ‹I' x = I x› by auto
        next
          case (3 x c)
          then have "I' x = Greater c" unfolding I'_def Z_def by auto
          with 3 elem[OF ‹x ∈ X›] t show ?case
          by (auto simp: cval_add_def)
        qed
      next
        case 3 show "{x ∈ X. ∃d. I' x = Intv d} = {x ∈ X. ∃d. I' x = Intv d}" ..
      next
        case 4
        let ?X⇩0  = "{x ∈ X. ∃d. I x = Intv d}"
        let ?X⇩0' = "{x ∈ X. ∃d. I' x = Intv d}"
        show "∀x∈?X⇩0'. ∀y∈?X⇩0'. ((x, y) ∈ r') = (frac ((v ⊕ t) x) ≤ frac ((v ⊕ t) y))"
        proof (safe, goal_cases)
          case (1 x y d d')
          note B = this
          show ?case
          proof (cases "x ∈ Z")
            case False
            note F = this
            show ?thesis
            proof (cases "y ∈ Z")
              case False
              with F B have *: "x ∈ ?X⇩0" "y ∈ ?X⇩0" unfolding I'_def by auto
              from B(5) show ?thesis unfolding r'_def
              proof (safe, goal_cases)
                case 1
                with v * have le: "frac (v x) <= frac (v y)" unfolding R_def by auto
                from frac_bound * have "t < 1 - frac (v x)" "t < 1 - frac (v y)" by fastforce+
                with frac_distr t have
                  "frac (v x) + t = frac (v x + t)" "frac (v y) + t = frac (v y + t)"
                by simp+
                with le show ?case unfolding cval_add_def by fastforce
              next
                case 2
                from this(1) elem have **: "frac (v x) = 0" unfolding Z_def by force
                from 2(4) obtain c where "I' y = Intv c" by (auto )
                then have "y ∈ Z ∨ I y = Intv c" unfolding I'_def by presburger
                then show ?case
                proof
                  assume "y ∈ Z"
                  with elem[OF 2(2)] have ***: "frac (v y) = 0" unfolding Z_def by force
                  show ?thesis by (simp add: ** *** frac_add cval_add_def)
                next
                  assume A: "I y = Intv c"
                  have le: "frac (v x) <= frac (v y)" by (simp add: **)
                  from frac_bound * have "t < 1 - frac (v x)" "t < 1 - frac (v y)" by fastforce+
                  with 2 t have
                    "frac (v x) + t = frac (v x + t)" "frac (v y) + t = frac (v y + t)"
                  using F by blast+
                  with le show ?case unfolding cval_add_def by fastforce
                qed
              qed
            next
              case True
              then obtain d' where d': "I y = Const d'" unfolding Z_def by auto
              from B(5) show ?thesis unfolding r'_def
              proof (safe, goal_cases)
                case 1
                from d' have "y ∉ ?X⇩0" by auto
                moreover from assms(8) have "refl_on ?X⇩0 r" by auto
                ultimately show ?case unfolding refl_on_def using 1 by auto
              next
                case 2
                with F show ?case by simp
              qed
            qed
          next
            case True
            with elem have **: "frac (v x) = 0" unfolding Z_def by force
            from B(4) have "y ∈ Z ∨ I y = Intv d'" unfolding I'_def by presburger
            then show ?thesis
            proof
              assume "y ∈ Z"
              with elem[OF B(3)] have ***: "frac (v y) = 0" unfolding Z_def by force
              show ?thesis by (simp add: ** *** frac_add cval_add_def)
            next
              assume A: "I y = Intv d'"
              with B(3) have "y ∈ ?X⇩0" by auto
              with frac_bound have "t < 1 - frac (v y)" by fastforce+
              moreover from ** ‹?t < 1› have "?t / 2 < 1 - frac (v x)" by linarith
              ultimately have
                "frac (v x) + t = frac (v x + t)" "frac (v y) + t = frac (v y + t)"
              using frac_distr t by simp+
              moreover have "frac (v x) <= frac (v y)" by (simp add: **)
              ultimately show ?thesis unfolding cval_add_def by fastforce
            qed
          qed
        next
          case B: (2 x y d d')
          show ?case
          proof (cases "x ∈ Z", goal_cases)
            case True
            with B(1,2) have "intv_const (I x) ≠ k x" unfolding I'_def by auto
            with B(1) assms(8) have "intv_const (I x) < k x" by (fastforce elim!: valid_intv.cases)
            with B True show ?thesis unfolding r'_def by auto
          next
            case (False)
            with B(1,2) have x_intv: "isIntv (I x)" unfolding Z_def I'_def by auto
            show ?thesis
            proof (cases "y ∈ Z")
              case False
              with B(3,4) have y_intv: "isIntv (I y)" unfolding Z_def I'_def by auto
              with frac_bound x_intv B(1,3) have "t < 1 - frac (v x)" "t < 1 - frac (v y)" by auto
              from frac_add_leD[OF _ this] B(5) t have
                "frac (v x) ≤ frac (v y)"
              by (auto simp: cval_add_def)
              with v assms(2) B(1,3) x_intv y_intv have "(x, y) ∈ r" by (auto )
              then show ?thesis by (simp add: r'_def)
            next
              case True
              from frac_bound x_intv B(1) have b: "t < 1 - frac (v x)" by auto
              from x_intv obtain c where "I x = Intv c" by auto
              with elem[OF ‹x ∈ X›] have v: "c < v x" "v x < c + 1" by auto
              from True elem[OF ‹y ∈ X›] have *: "frac (v y) = 0" unfolding Z_def by auto
              with t ‹?t < 1› floor_frac_add_preservation'[of t "v y"] have
                "floor (v y + t) = floor (v y)"
              by auto
              then have "frac (v y + t) = t"
              by (metis * add_diff_cancel_left' diff_add_cancel diff_self frac_def)
              moreover from nat_intv_frac_gt0[OF v] have "0 < frac (v x)" .
              moreover from frac_distr[OF _ b] t have "frac (v x + t) = frac (v x) + t" by auto
              ultimately show ?thesis using B(5) unfolding cval_add_def by auto
            qed
          qed
        qed
      qed
    }
    with ‹?t/2 > 0› have "0 < ?t/2 ∧ (∀ t. 0 < t ∧ t ≤ ?t/2 ⟶ (v ⊕ t) ∈ region X I' r')" by auto
  } note ** = this
  show "∃t'≤t. (v ⊕ t') ∈ region X I' r' ∧ 0 ≤ t'"
  proof (cases "∃ x ∈ X. isIntv (I x)")
    case True
    note T = this
    show ?thesis
    proof (cases "t ≤ ?t/2")
      case True with T t ** show ?thesis by auto
    next
      case False
      then have "?t/2 ≤ t" by auto
      moreover from T ** have "(v ⊕ ?t/2) ∈ region X I' r'" "?t/2 > 0" by auto
      ultimately show ?thesis by (fastforce del: region.cases)
    qed
  next
    case False
    note F = this
    show ?thesis
    proof (cases "t < 1")
      case True with F t * show ?thesis by auto
    next
      case False
      then have "0.5 ≤ t" by auto
      moreover from F * have "(v ⊕ 0.5) ∈ region X I' r'" by auto
      ultimately show ?thesis by (fastforce del: region.cases)
    qed
  qed
next
  fix v t assume A: "v ∈ region X I' r'" "0 ≤ t" "(v ⊕ t) ∈ R"
  from assms(3,4) obtain x c where x: "I x = Const c" "x ∈ Z" "x ∈ X" by auto
  with A(1) have "intv_elem x v (I' x)" by auto
  with x have "v x > c" unfolding I'_def
    apply (auto elim: intv_elem.cases)
    apply (cases "c = k x")
  by auto
  moreover from A(3) x(1,3) have "v x + t = c"
  by (fastforce elim!: intv_elem.cases simp: cval_add_def R_def)
  ultimately show False using A(2) by auto
next
  fix x c assume "x ∈ X" "I' x = Const c"
  then show False
    apply (auto simp: I'_def Z_def)
    apply (cases "∀c. I x ≠ Const c")
     apply auto
    apply (rename_tac c')
    apply (case_tac "c' = k x")
  by auto
next
  case (4 v t t' x c)
  note A = this
  then have "I' x = Intv c" unfolding I'_def Z_def by auto
  moreover from A have "real (c + 1) ≤ (v ⊕ t') x + (t - t')" unfolding cval_add_def by auto
  ultimately show ?case by blast
next
  case A: (5 v t t' x c)
  show ?case
  proof (cases "x ∈ Z")
    case False
    with A have "I x = Intv c" unfolding I'_def by auto
    with A show ?thesis unfolding cval_add_def by auto
  next
    case True
    with A(6) have "I x = Const c"
      apply (auto simp: I'_def)
      apply (cases "intv_const (I x) = k x")
    by (auto simp: Z_def)
    with A(1,5) R_def have "v x = c" by fastforce
    with A(2,7) show ?thesis by (auto simp: cval_add_def)
  qed
qed

lemma closest_valid_1:
  fixes I X k r
  defines "ℛ ≡ {region X I r |I r. valid_region X k I r}"
  defines "R ≡ region X I r"
  defines "Z ≡ {x ∈ X . ∃ c. I x = Const c}"
  assumes "Z ≠ {}"
  defines "I'≡ λ x. if x ∉ Z then I x else if intv_const (I x) = k x then Greater (k x) else Intv (intv_const (I x))"
  defines "r' ≡ r ∪ {(x,y) . x ∈ Z ∧ y ∈ X ∧ intv_const (I x) < k x ∧ isIntv (I' y)}"
  assumes "finite X"
  assumes "valid_region X k I r"
  shows "valid_region X k I' r'"
proof
  let ?X⇩0 = "{x ∈ X. ∃d. I x = Intv d}"
  let ?X⇩0' = "{x ∈ X. ∃d. I' x = Intv d}"
  let ?S = "{(x, y). x ∈ Z ∧ y ∈ X ∧ intv_const (I x) < k x ∧ isIntv (I' y)}"
  show "?X⇩0' = ?X⇩0'" ..
  from assms(8) have refl: "refl_on ?X⇩0 r" and total: "total_on ?X⇩0 r" and trans: "trans r"
    and valid: "⋀ x. x ∈ X ⟹ valid_intv (k x) (I x)"
  by auto
  then have "r ⊆ ?X⇩0 × ?X⇩0" unfolding refl_on_def by auto
  then have "r ⊆ ?X⇩0' × ?X⇩0'" unfolding I'_def Z_def by auto
  moreover have "?S ⊆ ?X⇩0' × ?X⇩0'"
    apply (auto)
    apply (auto simp: Z_def)[]
    apply (auto simp: I'_def)[]
  done
  ultimately have "r'⊆ ?X⇩0' × ?X⇩0'" unfolding r'_def by auto
  then show "refl_on ?X⇩0' r'" unfolding refl_on_def
  proof auto
    fix x d assume A: "x ∈ X" "I' x = Intv d"
    show "(x, x) ∈ r'"
    proof (cases "x ∈ Z")
      case True
      with A have "intv_const (I x) ≠ k x" unfolding I'_def by auto
      with assms(8) A(1) have "intv_const (I x) < k x" by (fastforce elim!: valid_intv.cases)
      with True A show "(x,x) ∈ r'" by (auto simp: r'_def)
    next
      case False
      with A refl show "(x,x) ∈ r'" by (auto simp: I'_def refl_on_def r'_def)
    qed
  qed
  show "total_on ?X⇩0' r'" unfolding total_on_def
  proof (standard, standard, standard)
    fix x y assume "x ∈ ?X⇩0'" "y ∈ ?X⇩0'" "x ≠ y"
    then obtain d d' where A: "x∈X""y∈X""I' x = (Intv d)" "I' y = (Intv d')" "x ≠ y" by auto
    let ?thesis = "(x, y) ∈ r' ∨ (y, x) ∈ r'"
    show ?thesis
    proof (cases "x ∈ Z")
      case True
      with A have "intv_const (I x) ≠ k x" unfolding I'_def by auto
      with assms(8) A(1) have "intv_const (I x) < k x" by (fastforce elim!: valid_intv.cases)
      with True A show ?thesis by (auto simp: r'_def)
    next
      case F: False
      show ?thesis
      proof (cases "y ∈ Z")
        case True
        with A have "intv_const (I y) ≠ k y" unfolding I'_def by auto
        with assms(8) A(2) have "intv_const (I y) < k y" by (fastforce elim!: valid_intv.cases)
        with True A show ?thesis by (auto simp: r'_def)
      next
        case False
        with A F have "I x = Intv d" "I y = Intv d'" by (auto simp: I'_def)
        with A(1,2,5) total show ?thesis unfolding total_on_def r'_def by auto
      qed
    qed
  qed
  show "trans r'" unfolding trans_def
  proof safe
    fix x y z assume A: "(x, y) ∈ r'" "(y, z) ∈ r'"
    show "(x, z) ∈ r'"
    proof (cases "(x,y) ∈ r")
      case True
      then have "y ∉ Z" using refl unfolding Z_def refl_on_def by auto
      then have "(y, z) ∈ r" using A unfolding r'_def by auto
      with trans True show ?thesis unfolding trans_def r'_def by blast
    next
      case False
      with A(1) have F: "x ∈ Z" "intv_const (I x) < k x" unfolding r'_def by auto
      moreover from A(2) refl have "z ∈ X" "isIntv (I' z)"
      by (auto simp: r'_def refl_on_def) (auto simp: I'_def Z_def)
      ultimately show ?thesis unfolding r'_def by auto
    qed
  qed
  show "∀x∈X. valid_intv (k x) (I' x)"
  proof (auto simp: I'_def intro: valid, goal_cases)
    case (1 x)
    with assms(8) have "intv_const (I x) < k x" by (fastforce elim!: valid_intv.cases)
    then show ?case by auto
  qed
qed

lemma closest_prestable_2:
  fixes I X k r
  defines "ℛ ≡ {region X I r |I r. valid_region X k I r}"
  defines "R ≡ region X I r"
  assumes "∀ x ∈ X. ¬ isConst (I x)"
  defines "X⇩0 ≡ {x ∈ X. isIntv (I x)}"
  defines "M ≡ {x ∈ X⇩0. ∀ y ∈ X⇩0. (x, y) ∈ r ⟶ (y, x) ∈ r}"
  defines "I'≡ λ x. if x ∉ M then I x else Const (intv_const (I x) + 1)"
  defines "r' ≡ {(x,y) ∈ r. x ∉ M ∧ y ∉ M}"
  assumes "finite X"
  assumes "valid_region X k I r"
  assumes "M ≠ {}"
  shows   "∀ v ∈ R. ∀ t≥0. (v ⊕ t) ∉ R ⟶ (∃t'≤t. (v ⊕ t') ∈ region X I' r' ∧ t' ≥ 0)"
  and     "∀ v ∈ region X I' r'. ∀ t≥0. (v ⊕ t) ∉ R"
  and     "∀ v ∈ R. ∀ t'. {x. x ∈ X ∧ (∃ c. I' x = Intv c ∧ (v ⊕ t') x + (t - t') ≥ real (c + 1))}
                  = {x. x ∈ X ∧ (∃ c. I x  = Intv c ∧ v x + t ≥ real (c + 1))} - M"
  and     "∃ x ∈ X. isConst (I' x)"
proof (safe, goal_cases)
  fix v assume v: "v ∈ R" fix t :: t assume t: "t ≥ 0" "(v ⊕ t) ∉ R"
  note M = assms(10)
  then obtain x c where x: "x ∈ M" "I x = Intv c" "x ∈ X" "x ∈ X⇩0" unfolding M_def X⇩0_def by force
  let ?t = "1 - frac (v x)"
  let ?v = "v ⊕ ?t"
  have elem: "intv_elem x v (I x)" if "x ∈ X" for x using that v unfolding R_def by auto
  from assms(9) have *: "trans r" "total_on {x ∈ X. ∃d. I x = Intv d} r" by auto
  then have trans[intro]: "⋀x y z. (x, y) ∈ r ⟹ (y, z) ∈ r ⟹ (x, z) ∈ r" unfolding trans_def
  by blast
  have "{x ∈ X. ∃d. I x = Intv d} = X⇩0" unfolding X⇩0_def by auto
  with *(2) have total: "total_on X⇩0 r" by auto
  { fix y assume y: "y ∉ M" "y ∈ X⇩0"
    have "¬ (x, y) ∈ r" using x y unfolding M_def by auto
    moreover with total x y have "(y, x) ∈ r" unfolding total_on_def by auto
    ultimately have "¬ (x, y) ∈ r ∧ (y, x) ∈ r" ..
  } note M_max = this
  { fix y assume T1: "y ∈ M" "x ≠ y"
    then have T2: "y ∈ X⇩0" unfolding M_def by auto
    with total x T1 have "(x, y) ∈ r ∨ (y, x) ∈ r" by (auto simp: total_on_def)
    with T1(1) x(1) have "(x, y) ∈ r" "(y, x) ∈ r" unfolding M_def by auto
  } note M_eq = this
  { fix y assume y: "y ∉ M" "y ∈ X⇩0"
    with M_max have "¬ (x, y) ∈ r" "(y, x) ∈ r" by auto
    with v[unfolded R_def] X⇩0_def x(4) y(2) have "frac (v y) < frac (v x)" by auto
    then have "?t < 1 - frac (v y)" by auto
  } note t_bound' = this
  { fix y assume y: "y ∈ X⇩0"
    have "?t ≤ 1 - frac (v y)"
    proof (cases "x = y")
      case True thus ?thesis by simp
    next
      case False
      have "(y, x) ∈ r"
      proof (cases "y ∈ M")
        case False with M_max y show ?thesis by auto
      next
        case True with False M_eq y show ?thesis by auto
      qed
      with v[unfolded R_def] X⇩0_def x(4) y have "frac (v y) ≤ frac (v x)" by auto
      then show "?t ≤ 1 - frac (v y)" by auto
    qed
  } note t_bound''' = this
  have "frac (v x) < 1" by (simp add: frac_lt_1)
  then have "?t > 0" by (simp add: x(3))
  { fix c y fix t :: t assume y: "y ∉ M" "I y = Intv c" "y ∈ X" and t: "t ≥ 0" "t ≤ ?t"
    then have "y ∈ X⇩0" unfolding X⇩0_def by auto
    with t_bound' y have "?t < 1 - frac (v y)" by auto
    with t have "t < 1 - frac (v y)" by auto
    moreover from elem[OF ‹y ∈ X›] y have "c < v y" "v y < c + 1" by auto
    ultimately have "(v y + t) < c + 1" using frac_add_le_preservation by blast
    with ‹c < v y› t have "intv_elem y (v ⊕ t) (I y)" by (auto simp: cval_add_def y)
  } note t_bound = this
  from elem[OF x(3)] x(2) have v_x: "c < v x" "v x < c + 1" by auto
  then have "floor (v x) = c" by linarith
  then have shift: "v x + ?t = c + 1" unfolding frac_def by auto
  have "v x + t ≥ c + 1"
  proof (rule ccontr, goal_cases)
    case 1
    then have AA: "v x + t < c + 1" by simp
    with shift have lt: "t < ?t" by auto
    let ?v = "v ⊕ t"
    have "?v ∈ region X I r"
    proof (standard, goal_cases)
      case 1
      from v have "∀ x ∈ X. v x ≥ 0" unfolding R_def by auto
      with t show ?case unfolding cval_add_def by auto
    next
      case 2
      show ?case
      proof (safe, goal_cases)
        case (1 y)
        note A = this
        with elem have e: "intv_elem y v (I y)" by auto
        show ?case
        proof (cases "y ∈ M")
          case False
          then have [simp]: "I' y = I y" by (auto simp: I'_def)
          show ?thesis
          proof (cases "I y", goal_cases)
            case 1 with assms(3) A show ?case by auto
          next
            case (2 c)
            from t_bound[OF False this A t(1)] lt show ?case by (auto simp: cval_add_def 2)
          next
            case (3 c)
            with e have "v y > c" by auto
            with 3 t(1) show ?case by (auto simp: cval_add_def)
          qed
        next
          case True
          then have "y ∈ X⇩0" by (auto simp: M_def)
          note T = this True
          show ?thesis
          proof (cases "x = y")
            case False
            with M_eq T have "(x, y) ∈ r" "(y, x) ∈ r" by presburger+
            with v[unfolded R_def] X⇩0_def x(4) T(1) have *: "frac (v y) = frac (v x)" by auto
            from T(1) obtain c where c: "I y = Intv c" by (auto simp: X⇩0_def)
            with elem T(1) have "c < v y" "v y < c + 1" by (fastforce simp: X⇩0_def)+
            then have "floor (v y) = c" by linarith
            with * lt have "(v y + t) < c + 1" unfolding frac_def by auto
            with ‹c < v y› t show ?thesis by (auto simp: c cval_add_def)
          next
            case True with ‹c < v x› t AA x show ?thesis by (auto simp: cval_add_def)
          qed
        qed
      qed
    next
      show "X⇩0 = {x ∈ X. ∃d. I x = Intv d}" by (auto simp add: X⇩0_def)
    next
      have "t > 0"
      proof (rule ccontr, goal_cases)
        case 1 with t v show False unfolding cval_add_def by auto
      qed
      show "∀y∈X⇩0. ∀z∈X⇩0. ((y, z) ∈ r) = (frac ((v ⊕ t)y) ≤ frac ((v ⊕ t) z))"
      proof (auto simp: X⇩0_def, goal_cases)
        case (1 y z d d')
        note A = this
        from A have [simp]: "y ∈ X⇩0" "z ∈ X⇩0" unfolding X⇩0_def I'_def by auto
        from A v[unfolded R_def] have le: "frac (v y) ≤ frac (v z)" by (auto simp: r'_def)
        from t_bound''' have "?t ≤ 1 - frac (v y)" "?t ≤ 1 - frac (v z)" by auto
        with lt have "t < 1 - frac (v y)" "t < 1 - frac (v z)" by auto
        with frac_distr[OF ‹t > 0›] have
          "frac (v y) + t = frac (v y + t)" "frac (v z) + t = frac (v z + t)"
        by auto
        with le show ?case by (auto simp: cval_add_def)
      next
        case (2 y z d d')
        note A = this
        from A have [simp]: "y ∈ X⇩0" "z ∈ X⇩0" unfolding X⇩0_def by auto
        from t_bound''' have "?t ≤ 1 - frac (v y)" "?t ≤ 1 - frac (v z)" by auto
        with lt have "t < 1 - frac (v y)" "t < 1 - frac (v z)" by auto
        from frac_add_leD[OF ‹t > 0› this] A(5) have
          "frac (v y) ≤ frac (v z)"
        by (auto simp: cval_add_def)
        with v[unfolded R_def] A show ?case by auto
      qed
    qed
    with t R_def show False by simp
  qed
  with shift have "t ≥ ?t" by simp
  let ?R = "region X