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₀ = {x ∈ X. ∃ d. I x = Intv d}; r ⊆ X₀ × X₀; refl_on X₀ r; trans r; total_on X₀ 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₀ = {x ∈ X. ∃ d. I x = Intv d} ==>
   ∀ x ∈ X₀. ∀ y ∈ X₀. (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 R ≡ THE R. R ∈ R ∧ v ∈ R"

inductive_set Succ for R R where
  "u ∈ R ==> R ∈ R ==> R' ∈ R ==> t ≥ 0 ==> R' = [u ⊕ t]_\<R> ==> R' ∈ Succ R 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₀ = "{x ∈ X. ∃ d. I' x = Intv d}"
    { fix x y assume x: "x ∈ ?X₀" and y: "y ∈ ?X₀"
      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₀. ∀ y ∈ ?X₀. (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₀ = "{x ∈ X. ∃ d. I x = Intv d}"
    { fix x y assume x: "x ∈ ?X₀" and y: "y ∈ ?X₀"
      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₀. ∀ y ∈ ?X₀. (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 R_regions_distinct:
  "[R = {region X I r | I r. valid_region X k I r}; R ∈ R; v ∈ R; 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₀ = "{x ∈ X. ∃ d. ?I x = Intv d}"
  let ?r = "{(x,y). x ∈ ?X₀ ∧ y ∈ ?X₀ ∧ 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₀ = "{x ∈ X. ∃d. I x = Intv d}"
  obtain f :: "'a → nat" where f:
    "∀x∈?X₀. ∀y∈?X₀. f x ≤ f y ⟷ (x, y) ∈ r"
     apply (rule finite_total_preorder_enumeration)
         apply (subgoal_tac "finite ?X₀")
          apply assumption
  using assms by auto
  let ?M = "if ?X₀ ≠ {} then Max {f x | x. x ∈ ?X₀} else 1"
  let ?f = "λ x. (f x + 1) / (?M + 2)"
  let ?v = "λ x. get_intv_val (I x) (if x ∈ ?X₀ then ?f x else 1)"
  have frac_intv: "∀x∈?X₀. 0 < ?f x ∧ ?f x < 1"
  proof (standard, goal_cases)
    case (1 x)
    then have *: "?X₀ ≠ {}" by auto
    have "f x ≤ Max {f x | x. x ∈ ?X₀}" 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₀. ∀y∈?X₀. frac (?v x) ≤ frac (?v y) ⟷ ?f x ≤ ?f y"
  by force
  have "∀x∈?X₀. ∀y∈?X₀. ?f x ≤ ?f y ⟷ f x ≤ f y" by (simp add: divide_le_cancel)+
  with f have "∀x∈?X₀. ∀y∈?X₀. ?f x ≤ ?f y ⟷ (x, y) ∈ r" by auto
  with * have frac_order: "∀x∈?X₀. ∀y∈?X₀. 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₀" 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₀ 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₀. ∀y∈?X₀. ((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:
  "R = {region X I r | I r. valid_region X k I r} ==> ∀x ∈ X. 0 ≤ u x ==> ∃! R ∈ R. u ∈ R"
proof (goal_cases)
  case 1
  note A = this
  with region_cover[OF A(2)] obtain R where R: "R ∈ R ∧ u ∈ R" by fastforce
  moreover have "R' = R" if "R' ∈ 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:
  "R = {region X I r | I r. valid_region X k I r} ==> u ∈ R ==> R ∈ R ==> [u]_\<R> = 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]_\<R> = 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':
  "R = {region X I r | I r. valid_region X k I r} ==> ∀x∈X. 0 ≤ v x ==> ∀x∈X. 0 ≤ v' x ==> v' ∈ [v]_\<R>
  ==> [v']_\<R> = [v]_\<R>"
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]_\<R> = 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']_\<R> = 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:
  "R = {region X I r | I r. valid_region X k I r} ==> R ∈ R ==> v ∈ R ==> t ≥ 0 ==> [v ⊕ t]_\<R> ∈ R"
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' ∈ R" "(v ⊕ t) ∈ R'" by auto
  with region_unique[OF A(1) this(2,1)] show ?case by auto
qed

lemma regions_closed':
  "R = {region X I r | I r. valid_region X k I r} ==> R ∈ R ==> v ∈ R ==> t ≥ 0 ==> (v ⊕ t) ∈ [v ⊕ t]_\<R>"
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' ∈ 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₀ = "{x ∈ X. ∃d. I x = Intv d}"
    from A(3) show "∀ x ∈ ?X₀. ∀ y ∈ ?X₀. ((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₀ = "{x ∈ X. ∃d. I' x = Intv d}"
    from A(3) show "∀ x ∈ ?X₀. ∀ y ∈ ?X₀. ((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_R:
  notes [[simproc add: finite_Collect]] finite_subset[intro]
  fixes X k
  defines "R ≡ {region X I r | I r. valid_region X k I r}"
  assumes "finite X"
  shows "finite R"
proof -
  { fix I r assume A: "valid_region X k I r"
    let ?X₀ = "{x ∈ X. ∃d. I x = Intv d}"
    from A have "r ⊆ X × X" by auto
    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 ?R = "{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 ?R" by fastforce
  moreover have "R ⊆ ?R"
  proof
    fix R assume R: "R ∈ R"
    then obtain I r where I: "R = region X I r" "valid_region X k I r" unfolding R_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 ∈ ?R" by force
  qed
  ultimately show "finite R" by blast
qed

lemma SuccI2:
  "R = {region X I r | I r. valid_region X k I r} ==> v ∈ R ==> R ∈ R ==> t ≥ 0 ==> R' = [v ⊕ t]_\<R>
  ==> R' ∈ Succ R 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:
  "R = {region X I r |I r. valid_region X k I r} ==> finite X ==> R ∈ R ==> R ∈ Succ R 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]_\<R>" 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':
  "R = {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 ∈ R ==> Succ R (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 R (region X I r)"
    then obtain v t where v:
      "v ∈ region X I r" "R = [v ⊕ t]_\<R>" "R ∈ 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]_\<R> = region X I r"
    unfolding cval_add_def by auto
    with v A(4) have "[v ⊕ 0]_\<R> ∈ Succ R (region X I r)" by (intro Succ.intros; auto)
    with * show "{region X I r} ⊆ Succ R (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 R =
  (SOME R'. R' ∈ Succ R 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 "R ≡ {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₀' = "{x ∈ X. ∃d. I' x = Intv d}"
    show "∀x∈?X₀'. ∀y∈?X₀'. ((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₀  = "{x ∈ X. ∃d. I x = Intv d}"
        let ?X₀' = "{x ∈ X. ∃d. I' x = Intv d}"
        show "∀x∈?X₀'. ∀y∈?X₀'. ((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₀" "y ∈ ?X₀" 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₀" by auto
                with assms(8) show ?case 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₀" 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 "R ≡ {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₀ = "{x ∈ X. ∃d. I x = Intv d}"
  let ?X₀' = "{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₀' = ?X₀'" ..
  have r_subset: "r ⊆ ?X₀ × ?X₀" and refl: "refl_on ?X₀ r" and total: "total_on ?X₀ r" and
    trans: "trans r" and valid: "∧ x. x ∈ X ==> valid_intv (k x) (I x)"
    using assms(8) by auto
  then have "r ⊆ ?X₀' × ?X₀'" unfolding I'_def Z_def by auto
  moreover have "?S ⊆ ?X₀' × ?X₀'"
    apply (auto)
    apply (auto simp: Z_def)[]
    apply (auto simp: I'_def)[]
  done
  ultimately show "r'⊆ ?X₀' × ?X₀'" unfolding r'_def by auto

  show "refl_on ?X₀' 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₀' r'" unfolding total_on_def
  proof (standard, standard, standard)
    fix x y assume "x ∈ ?X₀'" "y ∈ ?X₀'" "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 r_subset unfolding Z_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) r_subset have "z ∈ X" "isIntv (I' z)"
        by (auto simp: r'_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 "R ≡ {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₀ ≡ {x ∈ X. isIntv (I x)}"
  defines "M ≡ {x ∈ X₀. ∀ y ∈ X₀. (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₀" unfolding M_def X₀_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₀" unfolding X₀_def by auto
  with *(2) have total: "total_on X₀ r" by auto
  { fix y assume y: "y ∉ M" "y ∈ X₀"
    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₀" 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₀"
    with M_max have "¬ (x, y) ∈ r" "(y, x) ∈ r" by auto
    with v[unfolded R_def] X₀_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₀"
    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₀_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₀" unfolding X₀_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₀" 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₀_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₀_def)
            with elem T(1) have "c < v y" "v y < c + 1" by (fastforce simp: X₀_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₀ = {x ∈ X. ∃d. I x = Intv d}" by (auto simp add: X₀_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₀. ∀z∈X₀. ((y, z) ∈ r) = (frac ((v ⊕ t)y) ≤ frac ((v ⊕ t) z))"
      proof (auto simp: X₀_def, goal_cases)
        case (1 y z d d')
        note A = this
        from A have [simp]: "y ∈ X₀" "z ∈ X₀" unfolding X₀_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₀" "z ∈ X₀" unfolding X₀_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 I' r'"
  let ?X₀ = "{x ∈ X. ∃d. I' x = Intv d}"
  have "(v ⊕ ?t) ∈ ?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 (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 > 0› show ?case by (auto simp: cval_add_def 2)
        next
          case (3 c)
          with e have "v y > c" by auto
          with 3 ‹?t > 0› show ?case by (auto simp: cval_add_def)
        qed
      next
        case True
        then have "y ∈ X₀" by (auto simp: M_def)
        note T = this True
        show ?thesis
        proof (cases "x = y")
          case False
          with M_eq T(2) have "(x, y) ∈ r" "(y, x) ∈ r" by auto
          with v[unfolded R_def] X₀_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₀_def)
          with elem T(1) have "c < v y" "v y < c + 1" by (fastforce simp: X₀_def)+
          then have "floor (v y) = c" by linarith
          with * have "(v y + ?t) = c + 1" unfolding frac_def by auto
          with T(2) show ?thesis by (auto simp: c cval_add_def I'_def)
        next
          case True with shift x show ?thesis by (auto simp: cval_add_def I'_def)
        qed
      qed
    qed
  next
    show "?X₀ = ?X₀" ..
  next
    show "∀y∈?X₀. ∀z∈?X₀. ((y, z) ∈ r') = (frac ((v ⊕ 1 - frac (v x))y) ≤ frac ((v ⊕ 1 - frac (v x)) z))"
    proof (safe, goal_cases)
      case (1 y z d d')
      note A = this
      then have "y ∉ M" "z ∉ M" unfolding I'_def by auto
      with A have [simp]: "I' y = I y" "I' z = I z" "y ∈ X₀" "z ∈ X₀" unfolding X₀_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' ‹y ∉ M› ‹z ∉ M› 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
      then have M: "y ∉ M" "z ∉ M" unfolding I'_def by auto
      with A have [simp]: "I' y = I y" "I' z = I z" "y ∈ X₀" "z ∈ X₀" unfolding X₀_def I'_def by auto
      from t_bound' ‹y ∉ M› ‹z ∉ M› 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 M show ?case by (auto simp: r'_def)
    qed
  qed
  with ‹?t > 0› ‹?t ≤ t› show "∃t'≤t. (v ⊕ t') ∈ region X I' r' ∧ 0 ≤ t'" by auto
next
  fix v t assume A: "v ∈ region X I' r'" "0 ≤ t" "(v ⊕ t) ∈ R"
  from assms(10) obtain x c where x:
    "x ∈ X₀" "I x = Intv c" "x ∈ X" "x ∈ M"
  unfolding M_def X₀_def by force
  with A(1) have "intv_elem x v (I' x)" by auto
  with x have "v x = c + 1" unfolding I'_def by auto
  moreover from A(3) x(2,3) have "v x + t < c + 1" by (fastforce simp: cval_add_def R_def)
  ultimately show False using A(2) by auto
next
  case A: (3 v t' x c)
  from A(3) have "I x = Intv c" by (auto simp: I'_def) (cases "x ∈ M", auto)
  with A(4) show ?case by (auto simp: cval_add_def)
next
  case 4
  then show ?case unfolding I'_def by auto
next
  case A: (5 v t' x c)
  then have "I' x = Intv c" unfolding I'_def by auto
  moreover from A have "real (c + 1) ≤ (v ⊕ t') x + (t - t')" by (auto simp: cval_add_def)
  ultimately show ?case by blast
next
  from assms(5,10) obtain x where x: "x ∈ M" by blast
  then have "isConst (I' x)" by (auto simp: I'_def)
  with x show "∃x∈X. isConst (I' x)" unfolding M_def X₀_def by force
qed

lemma closest_valid_2:
  fixes I X k r
  defines "R ≡ {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₀ ≡ {x ∈ X. isIntv (I x)}"
  defines "M ≡ {x ∈ X₀. ∀ y ∈ X₀. (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 "valid_region X k I' r'"
proof
  let ?X₀ = "{x ∈ X. ∃d. I x = Intv d}"
  let ?X₀' = "{x ∈ X. ∃d. I' x = Intv d}"
  show "?X₀' = ?X₀'" ..
  have r_subset: "r ⊆ ?X₀ × ?X₀" and refl: "refl_on ?X₀ r" and total: "total_on ?X₀ r" and
    trans: "trans r" and valid: "∧ x. x ∈ X ==> valid_intv (k x) (I x)"
    using assms(9) by auto
  have subs: "r' ⊆ r" unfolding r'_def by auto
  show "r'⊆ ?X₀' × ?X₀'" using r_subset unfolding r'_def I'_def by auto

  show "refl_on ?X₀' r'" unfolding refl_on_def
  proof auto
    fix x d assume A: "x ∈ X" "I' x = Intv d"
    then have "x ∉ M" by (force simp: I'_def)
    with A have "I x = Intv d" by (force simp: I'_def)
    with A refl have "(x,x) ∈ r" by (auto simp: refl_on_def)
    then show "(x, x) ∈ r'" by (auto simp: r'_def ‹x ∉ M›)
  qed
  show "total_on ?X₀' r'" unfolding total_on_def
  proof (safe, goal_cases)
    case (1 x y d d')
    note A = this
    then have *: "x ∉ M" "y ∉ M" by (force simp: I'_def)+
    with A have "I x = Intv d" "I y = Intv d'" by (force simp: I'_def)+
    with A total have "(x, y) ∈ r ∨ (y, x) ∈ r" by (auto simp: total_on_def)
    with A(6) * show ?case unfolding r'_def by auto
  qed
  show "trans r'" unfolding trans_def
  proof safe
    fix x y z assume A: "(x, y) ∈ r'" "(y, z) ∈ r'"
    from trans have [intro]:
      "∧ x y z. (x,y) ∈ r ==> (y, z) ∈ r ==> (x, z) ∈ r"
    unfolding trans_def by blast
    from A show "(x, z) ∈ r'" by (auto simp: r'_def)
  qed
  show "∀x∈X. valid_intv (k x) (I' x)"
  using valid  unfolding I'_def
  proof (auto simp: I'_def intro: valid, goal_cases)
    case (1 x)
    with assms(9) have "intv_const (I x) < k x" by (fastforce simp: M_def X₀_def)
    then show ?case by auto
  qed
qed

subsection ‹Putting the Proof for the 'Set of Regions' Property Together›

subsubsection ‹Misc›

lemma total_finite_trans_max:
  "X ≠ {} ==> finite X ==> total_on X r ==> trans r ==> ∃ x ∈ X. ∀ y ∈ X. x ≠ y ⟶ (y, x) ∈ r"
proof (induction "card X" arbitrary: X)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then obtain x where x: "x ∈ X" by blast
  show ?case
  proof (cases "n = 0")
    case True
    with Suc.hyps(2) ‹finite X› x have "X = {x}" by (metis card_Suc_eq empty_iff insertE)
    then show ?thesis by auto
  next
    case False
    show ?thesis
    proof (cases "∀y∈X. x ≠ y ⟶ (y, x) ∈ r")
      case True with x show ?thesis by auto
    next
      case False
      then obtain y where y: "y ∈ X" "x ≠ y" "¬ (y, x) ∈ r" by auto
      with x Suc.prems(3) have "(x, y) ∈ r" unfolding total_on_def by blast
      let ?X = "X - {x}"
      have tot: "total_on ?X r" using ‹total_on X r› unfolding total_on_def by auto
      from x Suc.hyps(2) ‹finite X› have card: "n = card ?X" by auto
      with ‹finite X› ‹n ≠ 0› have "?X ≠ {}" by auto
      from Suc.hyps(1)[OF card this _ tot ‹trans r›] ‹finite X› obtain x' where
        IH: "x' ∈ ?X" "∀ y ∈ ?X. x' ≠ y ⟶ (y, x') ∈ r"
      by auto
      have "(x', x) ∉ r"
      proof (rule ccontr, auto)
        assume A: "(x', x) ∈ r"
        with y(3) have "x' ≠ y" by auto
        with y IH have "(y, x') ∈ r" by auto
        with ‹trans r› A have "(y, x) ∈ r" unfolding trans_def by blast
        with y show False by auto
      qed
      with ‹x ∈ X› ‹x' ∈ ?X› ‹total_on X r› have "(x, x') ∈ r" unfolding total_on_def by auto
      with IH show ?thesis by auto
    qed
  qed
qed

lemma card_mono_strict_subset:
  "finite A ==> finite B ==> finite C ==> A ∩ B ≠ {} ==> C = A - B ==> card C < card A"
by (metis Diff_disjoint Diff_subset inf_commute less_le psubset_card_mono)

subsubsection ‹Proof›

text ‹
 First we show that a shift by a non-negative integer constant means that any two valuations from
 the same region are being shifted to the same region.
 ›

lemma int_shift_equiv:
  fixes X k fixes t :: int
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  assumes "v ∈ R" "v' ∈ R" "R ∈ R" "t ≥ 0"
  shows "(v' ⊕ t) ∈ [v ⊕ t]_\<R>" using assms
proof -
  from assms obtain I r where A: "R = region X I r" "valid_region X k I r" by auto
  from regions_closed[OF _ assms(4,2), of X k t] assms(1,5) obtain I' r' where RR:
    "[v ⊕ t]_\<R> = region X I' r'" "valid_region X k I' r'"
  by auto
  from regions_closed'[OF _ assms(4,2), of X k t] assms(1,5) have RR': "(v ⊕ t) ∈ [v ⊕ t]_\<R>" by auto
  show ?thesis
  proof (simp add: RR(1), rule, goal_cases)
    case 1
    from ‹v' ∈ R› A(1) have "∀x∈X. 0 ≤ v' x" by auto
    with ‹t ≥ 0› show ?case unfolding cval_add_def by auto
  next
    case 2
    show ?case
    proof safe
      fix x assume x: "x ∈ X"
      with ‹v' ∈ R› ‹v ∈ R› A(1) have I: "intv_elem x v (I x)" "intv_elem x v' (I x)" by auto
      from x RR RR' have I': "intv_elem x (v ⊕ t) (I' x)" by auto
      show "intv_elem x (v' ⊕ t) (I' x)"
      proof (cases "I' x")
        case (Const c)
        from Const I' have "v x + t = c" unfolding cval_add_def by auto
        with x A(1) ‹v ∈ R› ‹t ≥ 0› have *: "v x = c - nat t" "t ≤ c" by fastforce+
        have "I x = Const (c - nat t)"
        proof (cases "I x")
          case (Greater c')
          with RR(2) Const ‹x ∈ X› have "c ≤ k x" by fastforce
          with * ‹t ≥ 0› have *: "v x ≤ k x" by auto
          from Greater A(2) ‹x ∈ X› have "c' = k x" by fastforce
          moreover from I(1) Greater have "v x > c'" by auto
          ultimately show ?thesis
            using ‹c ≤ k x› * by auto
        qed (use I in ‹auto simp: *›)
        with I ‹t ≥ 0› *(2) have "v' x + t = c" by auto
        with Const show ?thesis unfolding cval_add_def by auto
      next
        case (Intv c)
        with I' have "c < v x + t" "v x + t < c + 1" unfolding cval_add_def by auto
        with x A(1) ‹v ∈ R› ‹t ≥ 0›
        have *: "c - nat t < v x" "v x < c - nat t + 1" "t ≤ c"
          by fastforce+
        have "I x = Intv (c - nat t)"
        proof (cases "I x")
          case (Greater c')
          with RR(2) Intv ‹x ∈ X› have "c ≤ k x" by fastforce
          with * have *: "v x ≤ k x" using Intv RR(2) x by fastforce
          from Greater A(2) ‹x ∈ X› have "c' = k x" by fastforce
          moreover from I(1) Greater have "v x > c'" by auto
          ultimately show ?thesis
            using ‹c ≤ k x› * by auto
        qed (use I * in ‹auto simp del: of_nat_diff›)
        with I ‹t ≤ c› have "c < v' x + nat t" "v' x + t < c + 1" by auto
        with Intv ‹t ≥ 0› show ?thesis unfolding cval_add_def by auto
      next
        case (Greater c)
        with I' have *: "c < v x + t" unfolding cval_add_def by auto
        show ?thesis
        proof (cases "I x")
          case (Const c')
          with x A(1) I(2) ‹v ∈ R› ‹v' ∈ R› have "v x = v' x" by fastforce
          with Greater * show ?thesis unfolding cval_add_def by auto
        next
          case (Intv c')
          with x A(1) I(2) ‹v ∈ R› ‹v' ∈ R› have **: "c' < v x" "v x < c' + 1" "c' < v' x"
          by fastforce+
          then have "c' + t < v x + t" "v x + t < c' + t + 1" by auto
          with * have "c ≤ c' + t" by auto
          with **(3) have "v' x + t > c" by auto
          with Greater * show ?thesis unfolding cval_add_def by auto
        next
          fix c' assume c': "I x = Greater c'"
          with x A(1) I(2) ‹v ∈ R› ‹v' ∈ R› have **: "c' < v x" "c' < v' x" by fastforce+
          from Greater RR(2) c' A(2) ‹x ∈ X› have "c' = k x" "c = k x" by fastforce+
          with ‹t ≥ 0› **(2) Greater show "intv_elem x (v' ⊕ real_of_int t) (I' x)"
          unfolding cval_add_def by auto
        qed
      qed
    qed
  next
    show "{x ∈ X. ∃d. I' x = Intv d} = {x ∈ X. ∃d. I' x = Intv d}" ..
  next
    let ?X₀ = "{x ∈ X. ∃d. I' x = Intv d}"
    { fix x y :: real
      have "frac (x + t) ≤ frac (y + t) ⟷ frac x ≤ frac y" by (simp add: frac_def)
    } note frac_equiv = this
    { fix x y
      have "frac ((v ⊕ t) x) ≤ frac ((v ⊕ t) y) ⟷ frac (v x) ≤ frac (v y)"
      unfolding cval_add_def using frac_equiv by auto
    } note frac_equiv' = this
    { fix x y
      have "frac ((v' ⊕ t) x) ≤ frac ((v' ⊕ t) y) ⟷ frac (v' x) ≤ frac (v' y)"
      unfolding cval_add_def using frac_equiv by auto
    } note frac_equiv'' = this
    { fix x y assume x: "x ∈ X" and y: "y ∈ X" and B: "¬ isGreater(I x)" "¬ isGreater(I y)"
      have "frac (v x) ≤ frac (v y) ⟷ frac (v' x) ≤ frac (v' y)"
      proof (cases "I x")
        case (Const c)
        with x ‹v ∈ R› ‹v' ∈ R› A(1) have "v x = c" "v' x = c" by fastforce+
        then have "frac (v x) ≤ frac (v y)" "frac (v' x) ≤ frac (v' y)" unfolding frac_def by simp+
        then show ?thesis by auto
      next
        case (Intv c)
        with x ‹v ∈ R› A(1) have v: "c < v x" "v x < c + 1" by fastforce+
        from Intv x ‹v' ∈ R› A(1) have v':"c < v' x" "v' x < c + 1" by fastforce+
        show ?thesis
        proof (cases "I y", goal_cases)
          case (Const c')
          with y ‹v ∈ R› ‹v' ∈ R› A(1) have "v y = c'" "v' y = c'" by fastforce+
          then have "frac (v y) = 0" "frac (v' y) = 0" by auto
          with nat_intv_frac_gt0[OF v] nat_intv_frac_gt0[OF v']
          have "¬ frac (v x) ≤ frac (v y)" "¬ frac (v' x) ≤ frac (v' y)" by linarith+
          then show ?thesis by auto
        next
          case 2: (Intv c')
          with x y Intv ‹v ∈ R› ‹v' ∈ R› A(1) have
            "(x, y) ∈ r ⟷ frac (v x) ≤ frac (v y)"
            "(x, y) ∈ r ⟷ frac (v' x) ≤ frac (v' y)"
          by auto
          then show ?thesis by auto
        next
          case Greater
          with B show ?thesis by auto
        qed
      next
        case Greater with B show ?thesis by auto
      qed
    } note frac_cong = this
    have not_greater: "¬ isGreater (I x)" if x: "x ∈ X" "¬ isGreater (I' x)" for x
    proof (rule ccontr, auto, goal_cases)
      case (1 c)
      with x ‹v ∈ R› A(1,2) have "c < v x" by fastforce+
      moreover from x A(2) 1 have "c = k x" by fastforce+
      ultimately have *: "k x < v x + t" using ‹t ≥ 0› by simp
      from RR(1,2) RR' x have I': "intv_elem x (v ⊕ t) (I' x)" "valid_intv (k x) (I' x)" by auto
      from x show False
      proof (cases "I' x", auto)
        case (Const c')
        with I' * show False by (auto simp: cval_add_def)
      next
        case (Intv c')
        with I' * show False by (auto simp: cval_add_def)
      qed
    qed
    show "∀ x ∈ ?X₀. ∀y ∈ ?X₀. ((x, y) ∈ r') = (frac ((v' ⊕ t) x) ≤ frac ((v' ⊕ t) y))"
    proof (standard, standard)
      fix x y assume x: "x ∈ ?X₀" and y: "y ∈ ?X₀"
      then have B: "¬ isGreater (I' x)" "¬ isGreater (I' y)" by auto
      with x y not_greater have "¬ isGreater (I x)" "¬ isGreater (I y)" by auto
      with x y frac_cong have "frac (v x) ≤ frac (v y) ⟷ frac (v' x) ≤ frac (v' y)" by auto
      moreover from x y RR(1) RR' have "(x, y) ∈ r' ⟷ frac ((v ⊕ t) x) ≤ frac ((v ⊕ t) y)"
      by fastforce
      ultimately show "(x, y) ∈ r' ⟷ frac ((v' ⊕ t) x) ≤ frac ((v' ⊕ t) y)"
      using frac_equiv' frac_equiv'' by blast
    qed
  qed
qed

text ‹
 Now, we can use the 'immediate' induction proposed by P. Bouyer for shifts smaller than one.
 The induction principle is not at all obvious: the induction is over the set of clocks for
 which the valuation is shifted beyond the current interval boundaries.
 Using the two successor operations, we can see that either the set of these clocks remains the
 same (Z ~= {}) or strictly decreases (Z = {}).
 ›

lemma set_of_regions_lt_1:
  fixes X k I r t v
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  defines "C ≡ {x. x ∈ X ∧ (∃ c. I x = Intv c ∧ v x + t ≥ c + 1)}"
  assumes "valid_region X k I r" "v ∈ region X I r" "v' ∈ region X I r" "finite X" "0 ≤ t" "t < 1"
  shows "∃ t'≥0. (v' ⊕ t') ∈ [v ⊕ t]_\<R>" using assms
proof (induction "card C" arbitrary: C I r v v' t rule: less_induct)
  case less
  let ?R = "region X I r"
  let ?C = "{x ∈ X. ∃c. I x = Intv c ∧ real (c + 1) ≤ v x + t}"
  from less have R: "?R ∈ R" by auto
  { fix v I k r fix t :: t
    assume no_consts: "∀x∈X. ¬isConst (I x)"
    assume v: "v ∈ region X I r"
    assume t: "t ≥ 0"
    let ?C = "{x ∈ X. ∃c. I x = Intv c ∧ real (c + 1) ≤ v x + t}"
    assume C: "?C = {}"
    let ?R = "region X I r"
    have "(v ⊕ t) ∈ ?R"
    proof (rule, goal_cases)
      case 1
      with ‹t ≥ 0› ‹v ∈ ?R› show ?case by (auto simp: cval_add_def)
    next
      case 2
      show ?case
      proof (standard, case_tac "I x", goal_cases)
        case (1 x c)
        with no_consts show ?case by auto
      next
        case (2 x c)
        with ‹v ∈ ?R› have "c < v x" by fastforce
        with ‹t ≥ 0› have "c < v x + t" by auto
        moreover from 2 C have "v x + t < c + 1" by fastforce
        ultimately show ?case by (auto simp: 2 cval_add_def)
      next
        case (3 x c)
        with ‹v ∈ ?R› have "c < v x" by fastforce
        with ‹t ≥ 0› have "c < v x + t" by auto
        then show ?case by (auto simp: 3 cval_add_def)
      qed
    next
        show "{x ∈ X. ∃d. I x = Intv d} = {x ∈ X. ∃d. I x = Intv d}" ..
    next
      let ?X₀ = "{x ∈ X. ∃d. I x = Intv d}"
      { fix x d :: real fix c:: nat assume A: "c < x" "x + d < c + 1" "d ≥ 0"
        then have "d < 1 - frac x" unfolding frac_def using floor_eq3 of_nat_Suc by fastforce
      } note intv_frac = this
      { fix x assume x: "x ∈ ?X₀"
        then obtain c where x: "x ∈ X" "I x = Intv c" by auto
        with ‹v ∈ ?R› have *: "c < v x" by fastforce
        with ‹t ≥ 0› have "c < v x + t" by auto
        from x C have "v x + t < c + 1" by auto
        from intv_frac[OF * this ‹t ≥ 0›] have "t < 1 - frac (v x) " by auto
      } note intv_frac = this
      { fix x y assume x: "x ∈ ?X₀" and y: "y ∈ ?X₀"
        from frac_add_leIFF[OF ‹t ≥ 0› intv_frac[OF x] intv_frac[OF y]]
        have "frac (v x) ≤ frac (v y) ⟷ frac ((v ⊕ t) x) ≤ frac ((v ⊕ t) y)"
        by (auto simp: cval_add_def)
      } note frac_cong = this
      show "∀ x ∈ ?X₀. ∀ y ∈ ?X₀. (x, y) ∈ r ⟷ frac ((v ⊕ t) x) ≤ frac ((v ⊕ t) y)"
      proof (standard, standard, goal_cases)
        case (1 x y)
        with ‹v ∈ ?R› have "(x, y) ∈ r ⟷ frac (v x) ≤ frac (v y)" by auto
        with frac_cong[OF 1] show ?case by simp
      qed
    qed
  } note critical_empty_intro = this
  { assume const: "∃x∈X. isConst (I x)"
    assume t: "t > 0"
    from const have "{x ∈ X. ∃c. I x = Const c} ≠ {}" by auto
    from closest_prestable_1[OF this less.prems(4) less(3)] R closest_valid_1[OF this less.prems(4) less(3)]
    obtain I'' r''
      where   stability: "∀ v ∈ ?R. ∀ t>0. ∃t'≤t. (v ⊕ t') ∈ region X I'' r'' ∧ t' ≥ 0"
      and succ_not_refl: "∀ v ∈ region X I'' r''. ∀ t≥0. (v ⊕ t) ∉ ?R"
      and no_consts:     "∀ x ∈ X. ¬ isConst (I'' x)"
      and crit_mono:     "∀ 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)}"
      and succ_valid:    "valid_region X k I'' r''"
    by auto
    let ?R'' = "region X I'' r''"
    from stability less(4) ‹t > 0› obtain t1 where t1: "t1 ≥ 0" "t1 ≤ t" "(v ⊕ t1) ∈ ?R''" by auto
    from stability less(5) ‹t > 0› obtain t2 where t2: "t2 ≥ 0" "t2 ≤ t" "(v' ⊕ t2) ∈ ?R''" by auto
    let ?v = "v ⊕ t1"
    let ?t = "t - t1"
    let ?C' = "{x ∈ X. ∃c. I'' x = Intv c ∧ real (c + 1) ≤ ?v x + ?t}"
    from t1 ‹t < 1› have tt: "0 ≤ ?t" "?t < 1" by auto
    from crit_mono ‹t < 1› t1(1,3) ‹v ∈ ?R› have crit:
      "?C = ?C'"
    by auto
    with t1 t2 succ_valid no_consts have
      "∃ t1 ≥ 0. ∃ t2 ≥ 0. ∃ I' r'. t1 ≤ t ∧ (v ⊕ t1) ∈ region X I' r'
       ∧ t2 ≤ t ∧ (v' ⊕ t2) ∈ region X I' r'
       ∧ valid_region X k I' r'
       ∧ (∀ x ∈ X. ¬ isConst (I' x))
       ∧ ?C = {x ∈ X. ∃c. I' x = Intv c ∧ real (c + 1) ≤ (v ⊕ t1) x + (t - t1)}"
    by blast
  } note const_dest = this
  { fix t :: real fix v I r x c v'
    let ?R = "region X I r"
    assume v: "v ∈ ?R"
    assume v': "v' ∈ ?R"
    assume valid: "valid_region X k I r"
    assume t: "t > 0" "t < 1"
    let ?C = "{x ∈ X. ∃c. I x = Intv c ∧ real (c + 1) ≤ v x + t}"
    assume C: "?C = {}"
    assume const: "∃ x ∈ X. isConst (I x)"
    then have "{x ∈ X. ∃c. I x = Const c} ≠ {}" by auto
    from closest_prestable_1[OF this less.prems(4) valid] R closest_valid_1[OF this less.prems(4) valid]
    obtain I'' r''
      where   stability: "∀ v ∈ ?R. ∀ t>0. ∃t'≤t. (v ⊕ t') ∈ region X I'' r'' ∧ t' ≥ 0"
      and succ_not_refl: "∀ v ∈ region X I'' r''. ∀ t≥0. (v ⊕ t) ∉ ?R"
      and no_consts:     "∀ x ∈ X. ¬ isConst (I'' x)"
      and crit_mono:     "∀ 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)}"
      and succ_valid:    "valid_region X k I'' r''"
    by auto
    let ?R'' = "region X I'' r''"
    from stability v ‹t > 0› obtain t1 where t1: "t1 ≥ 0" "t1 ≤ t" "(v ⊕ t1) ∈ ?R''" by auto
    from stability v' ‹t > 0› obtain t2 where t2: "t2 ≥ 0" "t2 ≤ t" "(v' ⊕ t2) ∈ ?R''" by auto
    let ?v = "v ⊕ t1"
    let ?t = "t - t1"
    let ?C' = "{x ∈ X. ∃c. I'' x = Intv c ∧ real (c + 1) ≤ ?v x + ?t}"
    from t1 ‹t < 1› have tt: "0 ≤ ?t" "?t < 1" by auto
    from crit_mono ‹t < 1› t1(1,3) ‹v ∈ ?R› have crit:
      "{x ∈ X. ∃c. I x = Intv c ∧ real (c + 1) ≤ v x + t}
        = {x ∈ X. ∃c. I'' x = Intv c ∧ real (c + 1) ≤ (v ⊕ t1) x + (t - t1)}"
    by auto
    with C have C: "?C' = {}" by blast
    from critical_empty_intro[OF no_consts t1(3) tt(1) this] have "((v ⊕ t1) ⊕ ?t) ∈ ?R''" .
    from region_unique[OF less(2) this] less(2) succ_valid t2 have "∃t'≥0. (v' ⊕ t') ∈ [v ⊕ t]_\<R>"
    by (auto simp: cval_add_def)
  } note intro_const = this
  { fix v I r t x c v'
    let ?R = "region X I r"
    assume v: "v ∈ ?R"
    assume v': "v' ∈ ?R"
    assume F2: "∀x∈X. ¬isConst (I x)"
    assume x: "x ∈ X" "I x = Intv c" "v x + t ≥ c + 1"
    assume valid: "valid_region X k I r"
    assume t: "t ≥ 0" "t < 1"
    let ?C' = "{x ∈ X. ∃c. I x = Intv c ∧ real (c + 1) ≤ v x + t}"
    assume C: "?C = ?C'"
    have not_in_R: "(v ⊕ t) ∉ ?R"
    proof (rule ccontr, auto)
      assume "(v ⊕ t) ∈ ?R"
      with x(1,2) have "v x + t < c + 1" by (fastforce simp: cval_add_def)
      with x(3) show False by simp
    qed
    have not_in_R': "(v' ⊕ 1) ∉ ?R"
    proof (rule ccontr, auto)
      assume "(v' ⊕ 1) ∈ ?R"
      with x have "v' x + 1 < c + 1" by (fastforce simp: cval_add_def)
      moreover from x v' have "c < v' x" by fastforce
      ultimately show False by simp
    qed
    let ?X₀ = "{x ∈ X. isIntv (I x)}"
    let ?M = "{x ∈ ?X₀. ∀y∈?X₀. (x, y) ∈ r ⟶ (y, x) ∈ r}"
    from x have x: "x ∈ X" "¬ isGreater (I x)" and c: "I x = Intv c" by auto
    with ‹x ∈ X› have *: "?X₀ ≠ {}" by auto
    have "?X₀ = {x ∈ X. ∃d. I x = Intv d}" by auto
    with valid have r: "total_on ?X₀ r" "trans r" by auto
    from total_finite_trans_max[OF * _ this] ‹finite X›
    obtain x' where x': "x' ∈ ?X₀" "∀ y ∈ ?X₀. x' ≠ y ⟶ (y, x') ∈ r" by fastforce
    from this(2) have "∀y∈?X₀. (x', y) ∈ r ⟶ (y, x') ∈ r" by auto
    with x'(1) have "?M ≠ {}" by fastforce
    from closest_prestable_2[OF F2 less.prems(4) valid this] closest_valid_2[OF F2 less.prems(4) valid this]
    obtain I' r'
      where   stability:
        "∀ v ∈ region X I r. ∀ t≥0. (v ⊕ t) ∉ region X I r ⟶ (∃t'≤t. (v ⊕ t') ∈ region X I' r' ∧ t' ≥ 0)"
      and critical_mono: "∀ v ∈ region X I r. ∀t. ∀ 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 const_ex:      "∃x∈X. isConst (I' x)"
      and succ_valid:    "valid_region X k I' r'"
    by auto
    let ?R' = "region X I' r'"
    from not_in_R stability ‹t ≥ 0› v obtain t' where
      t': "t' ≥ 0" "t' ≤ t" "(v ⊕ t') ∈ ?R'"
    by blast
    have "(1::t) ≥ 0" by auto
    with not_in_R' stability v' obtain t1 where
      t1: "t1 ≥ 0" "t1 ≤ 1" "(v' ⊕ t1) ∈ ?R'"
    by blast
    let ?v = "v ⊕ t'"
    let ?t = "t - t'"
    let ?C'' = "{x ∈ X. ∃c. I' x = Intv c ∧ real (c + 1) ≤ ?v x + ?t}"
    have "∃t'≥0. (v' ⊕ t') ∈ [v ⊕ t]_\<R>"
    proof (cases "t = t'")
      case True
      with t' have "(v ⊕ t) ∈ ?R'" by auto
      from region_unique[OF less(2) this] succ_valid R_def have "[v ⊕ t]_\<R> = ?R'" by blast
      with t1(1,3) show ?thesis by auto
    next
      case False
      with ‹t < 1› t' have tt: "0 ≤ ?t" "?t < 1" "?t > 0" by auto
      from critical_mono ‹v ∈ ?R› have C_eq: "?C'' = ?C' - ?M" by auto
      show "∃t'≥0. (v' ⊕ t') ∈ [v ⊕ t]_\<R>"
      proof (cases "?C' ∩ ?M = {}")
        case False
        from ‹finite X› have "finite ?C''" "finite ?C'" "finite ?M" by auto
        then have "card ?C'' < card ?C" using C_eq C False by (intro card_mono_strict_subset) auto
        from less(1)[OF this less(2) succ_valid t'(3) t1(3) ‹finite X› tt(1,2)]
        obtain t2 where "t2 ≥ 0" "((v' ⊕ t1) ⊕ t2) ∈ [(v ⊕ t)]_\<R>" by (auto simp: cval_add_def)
        moreover have "(v' ⊕ (t1 + t2)) = ((v' ⊕ t1) ⊕ t2)" by (auto simp: cval_add_def)
        moreover have "t1 + t2 ≥ 0" using ‹t2 ≥ 0› t1(1) by auto
        ultimately show ?thesis by metis
      next
        case True
        { fix x c assume x: "x ∈ X" "I x = Intv c" "real (c + 1) ≤ v x + t"
          with True have "x ∉ ?M" by force
          from x have "x ∈ ?X₀" by auto
          from x(1,2) ‹v ∈ ?R› have *: "c < v x" "v x < c + 1" by fastforce+
          with ‹t < 1› have "v x + t < c + 2" by auto
          have ge_1: "frac (v x) + t ≥ 1"
          proof (rule ccontr, goal_cases)
            case 1
            then have A: "frac (v x) + t < 1" by auto
            from * have "floor (v x) + frac (v x) < c + 1" unfolding frac_def by auto
            with nat_intv_frac_gt0[OF *] have "floor (v x) ≤ c" by linarith
            with A have "v x + t < c + 1" by (auto simp: frac_def)
            with x(3) show False by auto
          qed
          from ‹?M ≠ {}› obtain y where "y ∈ ?M" by force
          with ‹x ∈ ?X₀› have y: "y ∈ ?X₀" "(y, x) ∈ r ⟶ (x, y) ∈ r" by auto
          from y obtain c' where c': "y ∈ X" "I y = Intv c'" by auto
          with ‹v ∈ ?R› have "c' < v y" by fastforce
          from ‹y ∈ ?M› ‹x ∉ ?M› have "x ≠ y" by auto
          with y r(1) x(1,2) have "(x, y) ∈ r" unfolding total_on_def by fastforce
          with ‹v ∈ ?R› c' x have "frac (v x) ≤ frac (v y)" by fastforce
          with ge_1 have frac: "frac (v y) + t ≥ 1" by auto
          have "real (c' + 1) ≤ v y + t"
          proof (rule ccontr, goal_cases)
            case 1
            from ‹c' < v y› have "floor (v y) ≥ c'" by linarith
            with frac have "v y + t ≥ c' + 1" unfolding frac_def by linarith
            with 1 show False by simp
          qed
          with c' True ‹y ∈ ?M› have False by auto
        }
        then have C: "?C' = {}" by auto
        with C_eq have C'': "?C'' = {}" by auto
        from intro_const[OF t'(3) t1(3) succ_valid tt(3) tt(2) C'' const_ex]
        obtain t2 where "t2 ≥ 0" "((v' ⊕ t1) ⊕ t2) ∈ [v ⊕ t]_\<R>" by (auto simp: cval_add_def)
        moreover have "(v' ⊕ (t1 + t2)) = ((v' ⊕ t1) ⊕ t2)" by (auto simp: cval_add_def)
        moreover have "t1 + t2 ≥ 0" using ‹t2 ≥ 0› t1(1) by auto
        ultimately show ?thesis by metis
      qed
    qed
  } note intro_intv = this
  from regions_closed[OF less(2) R less(4,7)] less(2) obtain I' r' where R':
      "[v ⊕ t]_\<R> = region X I' r'" "valid_region X k I' r'"
  by auto
  with regions_closed'[OF less(2) R less(4,7)] assms(1) have
    R'2: "(v ⊕ t) ∈ [v ⊕ t]_\<R>" "(v ⊕ t) ∈ region X I' r'"
  by auto
  let ?R' = "region X I' r'"
  from less(2) R' have "?R' ∈ R" by auto
  show ?case
  proof (cases "?R' = ?R")
    case True with less(3,5) R'(1) have "(v' ⊕ 0) ∈ [v ⊕ t]_\<R>" by (auto simp: cval_add_def)
    then show ?thesis by auto
  next
    case False
    have "t > 0"
    proof (rule ccontr)
      assume "¬ 0 < t"
      with R' ‹t ≥ 0› have "[v]_\<R> = ?R'" by (simp add: cval_add_def)
      with region_unique[OF less(2) less(4) R] ‹?R' ≠ ?R› show False by auto
    qed
    show ?thesis
    proof (cases "?C = {}")
      case True
      show ?thesis
      proof (cases "∃ x ∈ X. isConst (I x)")
        case False
        then have no_consts: "∀x∈X. ¬isConst (I x)" by auto
        from critical_empty_intro[OF this ‹v ∈ ?R› ‹t ≥ 0› True] have "(v ⊕ t) ∈ ?R" .
        from region_unique[OF less(2) this R] less(5) have "(v' ⊕ 0) ∈ [v ⊕ t]_\<R>"
        by (auto simp: cval_add_def)
        then show ?thesis by blast
      next
        case True
        from const_dest[OF this ‹t > 0›] obtain t1 t2 I' r'
          where t1:  "t1 ≥ 0" "t1 ≤ t" "(v ⊕ t1) ∈ region X I' r'"
          and   t2:  "t2 ≥ 0" "t2 ≤ t" "(v' ⊕ t2) ∈ region X I' r'"
          and valid: "valid_region X k I' r'"
          and no_consts: "∀ x ∈ X. ¬ isConst (I' x)"
          and   C:   "?C = {x ∈ X. ∃c. I' x = Intv c ∧ real (c + 1) ≤ (v ⊕ t1) x + (t - t1)}"
        by auto
        let ?v = "v ⊕ t1"
        let ?t = "t - t1"
        let ?C' = "{x ∈ X. ∃c. I' x = Intv c ∧ real (c + 1) ≤ ?v x + ?t}"
        let ?R' = "region X I' r'"
        from C ‹?C = {}› have "?C' = {}" by blast
        from critical_empty_intro[OF no_consts t1(3) _ this] t1 have "(?v ⊕ ?t) ∈ ?R'" by auto
        from region_unique[OF less(2) this] less(2) valid t2 show ?thesis
        by (auto simp: cval_add_def)
      qed
    next
      case False
      then obtain x c where x: "x ∈ X" "I x = Intv c" "v x + t ≥ c + 1" by auto
      then have F: "¬ (∀ x ∈ X. ∃ c. I x = Greater c)" by force
      show ?thesis
      proof (cases "∃ x ∈ X. isConst (I x)")
        case False
        then have "∀x∈X. ¬isConst (I x)" by auto
        from intro_intv[OF ‹v ∈ ?R› ‹v' ∈ ?R› this x less(3,7,8)] show ?thesis by auto
      next
        case True
        then have "{x ∈ X. ∃c. I x = Const c} ≠ {}" by auto
        from const_dest[OF True ‹t > 0›] obtain t1 t2 I' r'
          where t1:  "t1 ≥ 0" "t1 ≤ t" "(v ⊕ t1) ∈ region X I' r'"
          and   t2:  "t2 ≥ 0" "t2 ≤ t" "(v' ⊕ t2) ∈ region X I' r'"
          and valid: "valid_region X k I' r'"
          and no_consts: "∀ x ∈ X. ¬ isConst (I' x)"
          and   C:   "?C = {x ∈ X. ∃c. I' x = Intv c ∧ real (c + 1) ≤ (v ⊕ t1) x + (t - t1)}"
        by auto
        let ?v = "v ⊕ t1"
        let ?t = "t - t1"
        let ?C' = "{x ∈ X. ∃c. I' x = Intv c ∧ real (c + 1) ≤ ?v x + ?t}"
        let ?R' = "region X I' r'"
        show ?thesis
        proof (cases "?C' = {}")
          case False
          with intro_intv[OF t1(3) t2(3) no_consts _ _ _ valid _ _ C] ‹t < 1› t1 obtain t' where
            "t' ≥ 0" "((v' ⊕ t2) ⊕ t') ∈ [(v ⊕ t)]_\<R>"
          by (auto simp: cval_add_def)
          moreover have "((v' ⊕ t2) ⊕ t') = (v' ⊕ (t2 + t'))" by (auto simp: cval_add_def)
          moreover have "t2 + t' ≥ 0" using ‹t' ≥ 0› ‹t2 ≥ 0› by auto
          ultimately show ?thesis by metis
        next
          case True
          from critical_empty_intro[OF no_consts t1(3) _ this] t1 have "((v ⊕ t1) ⊕ ?t) ∈ ?R'" by auto
          from region_unique[OF less(2) this] less(2) valid t2 show ?thesis
          by (auto simp: cval_add_def)
        qed
      qed
    qed
  qed
qed

text ‹
 Finally, we can put the two pieces together: for a non-negative shift @{term t}, we first shift
 @{term "floor t"} and then @{term "frac t"}.
 ›

lemma set_of_regions:
  fixes X k
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  assumes "R ∈ R" "v ∈ R" "R' ∈ Succ R R" "finite X"
  shows "∃ t≥0. [v ⊕ t]_\<R> = R'" using assms
proof -
  from assms(4) obtain v' t where v': "v' ∈ R" "R' ∈ R" "0 ≤ t" "R' = [v' ⊕ t]_\<R>" by fastforce
  obtain t1 :: int where t1: "t1 = floor t" by auto
  with v'(3) have "t1 ≥ 0" by auto
  from int_shift_equiv[OF v'(1) ‹v ∈ R› assms(2)[unfolded R_def] this] R_def
  have *: "(v ⊕ t1) ∈ [v' ⊕ t1]_\<R>" by auto
  let ?v = "(v ⊕ t1)"
  let ?t2 = "frac t"
  have frac: "0 ≤ ?t2" "?t2 < 1" by (auto simp: frac_lt_1)
  let ?R = "[v' ⊕ t1]_\<R>"
  from regions_closed[OF _ assms(2) v'(1)] ‹t1 ≥ 0› R_def have "?R ∈ R" by auto
  with assms obtain I r where R: "?R = region X I r" "valid_region X k I r" by auto
  with * have v: "?v ∈ region X I r" by auto
  from R regions_closed'[OF _ assms(2) v'(1)] ‹t1 ≥ 0› R_def have "(v' ⊕ t1) ∈ region X I r" by auto
  from set_of_regions_lt_1[OF R(2) this v assms(5) frac] R_def obtain t2 where
    "t2 ≥ 0" "(?v ⊕ t2) ∈ [(v' ⊕ t1) ⊕ ?t2]_\<R>"
  by auto
  moreover from t1 have "(v ⊕ (t1 + t2)) = (?v ⊕ t2)" "v' ⊕ t = ((v' ⊕ t1) ⊕ ?t2)"
  by (auto simp: frac_def cval_add_def)
  ultimately have "(v ⊕ (t1 + t2)) ∈ [v' ⊕ t]_\<R>" "t1 + t2 ≥ 0" using ‹t1 ≥ 0› ‹t2 ≥ 0› by auto
  with region_unique[OF _ this(1)] v'(2,4) R_def show ?thesis by blast
qed


section ‹Compability With Clock Constraints›

definition ccval (‹{_}› [100]) where "ccval cc ≡ {v. v ⊨ cc}"

definition acompatible
where
  "acompatible R ac ≡ ∀ R ∈ R. R ⊆ {v. v ⊨_a ac} ∨ {v. v ⊨_a ac} ∩ R = {}"

lemma acompatibleD:
  assumes "acompatible R ac" "R ∈ R" "u ∈ R" "v ∈ R" "u ⊨_a ac"
  shows "v ⊨_a ac"
  using assms unfolding acompatible_def by auto

lemma ccompatible1:
  fixes X k fixes c :: real
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  assumes "c ≤ k x" "c ∈ ℕ" "x ∈ X"
  shows "acompatible R (EQ x c)" using assms unfolding acompatible_def
proof (auto, goal_cases)
  case A: (1 I r v u)
  from A(3,9) obtain d where d: "c = of_nat d" unfolding Nats_def by auto
  with A(8,9) have u: "u x = c" "u x = d" unfolding ccval_def by auto
  have "I x = Const d"
  proof (cases "I x", goal_cases)
    case (1 c')
    with A have "u x = c'" by fastforce
    with 1 u show ?case by auto
  next
    case (2 c')
    with A have "c' < u x" "u x < c' + 1" by fastforce+
    with 2 u show ?case by auto
  next
    case (3 c')
    with A have "c' < u x" by fastforce
    moreover from 3 A(4,5) have "c' ≥ k x" by fastforce
    ultimately show ?case using u A(2) by auto
  qed
  with A(4,6) d have "v x = c" by fastforce
  with A(3,5) have "v ⊨_a EQ x c" by auto
  with A show False unfolding ccval_def by auto
qed

lemma ccompatible2:
  fixes X k fixes c :: real
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  assumes "c ≤ k x" "c ∈ ℕ" "x ∈ X"
  shows "acompatible R (LT x c)" using assms unfolding acompatible_def
proof (auto, goal_cases)
  case A: (1 I r v u)
  from A(3) obtain d :: nat where d: "c = of_nat d" unfolding Nats_def by blast
  with A have u: "u x < c" "u x < d" unfolding ccval_def by auto
  have "v x < c"
  proof (cases "I x", goal_cases)
    case (1 c')
    with A have "u x = c'" "v x = c'" by fastforce+
    with u show "v x < c" by auto
  next
    case (2 c')
    with A have B: "c' < u x" "u x < c' + 1" "c' < v x" "v x < c' + 1" by fastforce+
    with u A(3) have "c' + 1 ≤ d" by auto
    with d have "c' + 1 ≤ c" by auto
    with B u show "v x < c" by auto
  next
    case (3 c')
    with A have "c' < u x" by fastforce
    moreover from 3 A(4,5) have "c' ≥ k x" by fastforce
    ultimately show ?case using u A(2) by auto
  qed
  with A(4,6) have "v ⊨_a LT x c" by auto
  with A(7) show False unfolding ccval_def by auto
qed

lemma ccompatible3:
  fixes X k fixes c :: real
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  assumes "c ≤ k x" "c ∈ ℕ" "x ∈ X"
  shows "acompatible R (LE x c)" using assms unfolding acompatible_def
proof (auto, goal_cases)
  case A: (1 I r v u)
  from A(3) obtain d :: nat where d: "c = of_nat d" unfolding Nats_def by blast
  with A have u: "u x ≤ c" "u x ≤ d" unfolding ccval_def by auto
  have "v x ≤ c"
  proof (cases "I x", goal_cases)
    case (1 c') with A u show ?case by fastforce
  next
    case (2 c')
    with A have B: "c' < u x" "u x < c' + 1" "c' < v x" "v x < c' + 1" by fastforce+
    with u A(3) have "c' + 1 ≤ d" by auto
    with d u A(3) have "c' + 1 ≤ c" by auto
    with B u show "v x ≤ c" by auto
  next
    case (3 c')
    with A have "c' < u x" by fastforce
    moreover from 3 A(4,5) have "c' ≥ k x" by fastforce
    ultimately show ?case using u A(2) by auto
  qed
  with A(4,6) have "v ⊨_a LE x c" by auto
  with A(7) show False unfolding ccval_def by auto
qed

lemma ccompatible4:
  fixes X k fixes c :: real
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  assumes "c ≤ k x" "c ∈ ℕ" "x ∈ X"
  shows "acompatible R (GT x c)" using assms unfolding acompatible_def
proof (auto, goal_cases)
  case A: (1 I r v u)
  from A(3) obtain d :: nat where d: "c = of_nat d" unfolding Nats_def by blast
  with A have u: "u x > c" "u x > d" unfolding ccval_def by auto
  have "v x > c"
  proof (cases "I x", goal_cases)
    case (1 c') with A u show ?case by fastforce
  next
    case (2 c')
    with A have B: "c' < u x" "u x < c' + 1" "c' < v x" "v x < c' + 1" by fastforce+
    with d u have "c' ≥ c" by auto
    with B u show "v x > c" by auto
  next
    case (3 c')
    with A(4,6) have "c' < v x" by fastforce
    moreover from 3 A(4,5) have "c' ≥ k x" by fastforce
    ultimately show ?case using A(2) u(1) by auto
  qed
  with A(4,6) have "v ⊨_a GT x c" by auto
  with A(7) show False unfolding ccval_def by auto
qed

lemma ccompatible5:
  fixes X k fixes c :: real
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  assumes "c ≤ k x" "c ∈ ℕ" "x ∈ X"
  shows "acompatible R (GE x c)" using assms unfolding acompatible_def
proof (auto, goal_cases)
  case A: (1 I r v u)
  from A(3) obtain d :: nat where d: "c = of_nat d" unfolding Nats_def by blast
  with A have u: "u x ≥ c" "u x ≥ d" unfolding ccval_def by auto
  have "v x ≥ c"
  proof (cases "I x", goal_cases)
    case (1 c') with A u show ?case by fastforce
  next
    case (2 c')
    with A have B: "c' < u x" "u x < c' + 1" "c' < v x" "v x < c' + 1" by fastforce+
    with d u have "c' ≥ c" by auto
    with B u show "v x ≥ c" by auto
  next
    case (3 c')
    with A(4,6) have "c' < v x" by fastforce
    moreover from 3 A(4,5) have "c' ≥ k x" by fastforce
    ultimately show ?case using A(2) u(1) by auto
  qed
  with A(4,6) have "v ⊨_a GE x c" by auto
  with A(7) show False unfolding ccval_def by auto
qed

lemma acompatible:
  fixes X k fixes c :: real
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  assumes "c ≤ k x" "c ∈ ℕ" "x ∈ X" "constraint_pair ac = (x, c)"
  shows "acompatible R ac" using assms
by (cases ac) (auto intro: ccompatible1 ccompatible2 ccompatible3 ccompatible4 ccompatible5)

definition ccompatible
where
  "ccompatible R cc ≡ ∀ R ∈ R. R ⊆ {cc} ∨ {cc} ∩ R = {}"

lemma ccompatible:
  fixes X k fixes c :: nat
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  assumes "∀(x,m) ∈ collect_clock_pairs cc. m ≤ k x ∧ x ∈ X ∧ m ∈ ℕ"
  shows "ccompatible R cc" using assms
proof (induction cc)
  case Nil
  then show ?case by (auto simp: ccompatible_def ccval_def clock_val_def)
next
  case (Cons ac cc)
  then have "ccompatible R cc" by (auto simp: collect_clock_pairs_def)
  moreover have
    "acompatible R ac"
  using Cons.prems by (auto intro: acompatible simp: collect_clock_pairs_def R_def)
  ultimately show ?case
    unfolding ccompatible_def acompatible_def ccval_def by (fastforce simp: clock_val_def)
qed

section ‹Compability with Resets›

definition region_set
where
  "region_set R x c = {v(x := c) | v. v ∈ R}"

lemma region_set_id:
  fixes X k
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  assumes "R ∈ R" "v ∈ R" "finite X" "0 ≤ c" "c ≤ k x" "x ∈ X"
  shows "[v(x := c)]_\<R> = region_set R x c" "[v(x := c)]_\<R> ∈ R" "v(x := c) ∈ [v(x := c)]_\<R>"
proof -
  from assms obtain I r where R: "R = region X I r" "valid_region X k I r" "v ∈ region X I r" by auto
  let ?I = "λ y. if x = y then Const c else I y"
  let ?r = "{(y,z) ∈ r. x ≠ y ∧ x ≠ z}"
  let ?X₀ = "{x ∈ X. ∃ c. I x = Intv c}"
  let ?X₀' = "{x ∈ X. ∃ c. ?I x = Intv c}"

  have r_subset: "r ⊆ ?X₀ × ?X₀" and refl: "refl_on ?X₀ r" and trans: "trans r" and
    total: "total_on ?X₀ r"
    using R(2) by auto

  have valid: "valid_region X k ?I ?r"
  proof
    show "?X₀ - {x} = ?X₀'" by auto
  next
    show "?r ⊆ (?X₀ - {x}) × (?X₀ - {x})"
      using r_subset by blast
  next
    from refl show "refl_on (?X₀ - {x}) ?r" unfolding refl_on_def by auto
  next
    from trans show "trans ?r" unfolding trans_def by blast
  next
    from total show "total_on (?X₀ - {x}) ?r" unfolding total_on_def by auto
  next
    from R(2) have "∀ x ∈ X. valid_intv (k x) (I x)" by auto
    with ‹c ≤ k x› show "∀ x ∈ X. valid_intv (k x) (?I x)" by auto
  qed

  { fix v assume v: "v ∈ region_set R x c"
    with R(1) obtain v' where v': "v' ∈ region X I r" "v = v'(x := c)" unfolding region_set_def by auto
    have "v ∈ region X ?I ?r"
    proof (standard, goal_cases)
      case 1
      from v' ‹0 ≤ c› show ?case by auto
    next
      case 2
      from v' show ?case
      proof (auto, goal_cases)
        case (1 y)
        then have "intv_elem y v' (I y)" by auto
        with ‹x ≠ y› show "intv_elem y (v'(x := c)) (I y)" by (cases "I y") auto
      qed
    next
      show "?X₀ - {x} = ?X₀'" by auto
    next
      from v' show "∀ y ∈ ?X₀ - {x}. ∀ z ∈ ?X₀ - {x}. (y,z) ∈ ?r ⟷ frac (v y) ≤ frac (v z)" by auto
    qed
  } moreover
  { fix v assume v: "v ∈ region X ?I ?r"
    have "∃ c. v(x := c) ∈ region X I r"
    proof (cases "I x")
      case (Const c)
      from R(2) have "c ≥ 0" by auto
      let ?v = "v(x := c)"
      have "?v ∈ region X I r"
      proof (standard, goal_cases)
        case 1
        from ‹c≥0› v show ?case by auto
      next
        case 2
        show ?case
        proof (auto, goal_cases)
          case (1 y)
          with v have "intv_elem y v (?I y)" by fast
          with Const show "intv_elem y ?v (I y)" by (cases "x = y", auto) (cases "I y", auto)
        qed
      next
        from Const show "?X₀' = ?X₀" by auto
        with r_subset have "r ⊆ ?X₀' × ?X₀'" by auto
        then have r: "?r = r" by auto
        from v have "∀ y ∈ ?X₀'. ∀ z ∈ ?X₀'. (y,z) ∈ ?r ⟷ frac (v y) ≤ frac (v z)" by fastforce
        with r show "∀ y ∈ ?X₀'. ∀ z ∈ ?X₀'. (y,z) ∈ r ⟷ frac (?v y) ≤ frac (?v z)"
        by auto
      qed
      then show ?thesis by auto
    next
      case (Greater c)
      from R(2) have "c ≥ 0" by auto
      let ?v = "v(x := c + 1)"
      have "?v ∈ region X I r"
      proof (standard, goal_cases)
        case 1
        from ‹c≥0› v show ?case by auto
      next
        case 2
        show ?case
        proof (standard, goal_cases)
          case (1 y)
          with v have "intv_elem y v (?I y)" by fast
          with Greater show "intv_elem y ?v (I y)" by (cases "x = y", auto) (cases "I y", auto)
        qed
      next
        from Greater show "?X₀' = ?X₀" by auto
        with r_subset have "r ⊆ ?X₀' × ?X₀'" by auto
        then have r: "?r = r" by auto
        from v have "∀ y ∈ ?X₀'. ∀ z ∈ ?X₀'. (y,z) ∈ ?r ⟷ frac (v y) ≤ frac (v z)" by fastforce
        with r show "∀ y ∈ ?X₀'. ∀ z ∈ ?X₀'. (y,z) ∈ r ⟷ frac (?v y) ≤ frac (?v z)"
        by auto
      qed
      then show ?thesis by auto
    next
      case (Intv c)
      from R(2) have "c ≥ 0" by auto
      let ?L = "{frac (v y) | y. y ∈ ?X₀ ∧ x ≠ y ∧ (y,x) ∈ r}"
      let ?U = "{frac (v y) | y. y ∈ ?X₀ ∧ x ≠ y ∧ (x,y) ∈ r}"
      let ?l = "if ?L ≠ {} then c + Max ?L else if ?U ≠ {} then c else c + 0.5"
      let ?u = "if ?U ≠ {} then c + Min ?U else if ?L ≠ {} then c + 1 else c + 0.5"
      from ‹finite X› have fin: "finite ?L" "finite ?U" by auto
      { fix y assume y: "y ∈ ?X₀" "x ≠ y" "(y, x) ∈ r"
        then have L: "frac (v y) ∈ ?L" by auto
        with Max_in[OF fin(1)] have In: "Max ?L ∈ ?L" by auto
        then have "frac (Max ?L) = (Max ?L)" using frac_frac by fastforce
        from Max_ge[OF fin(1) L] have "frac (v y) ≤ Max ?L" .
        also have "… = frac (Max ?L)" using In frac_frac[symmetric] by fastforce
        also have "… = frac (c + Max ?L)" by (auto simp: frac_nat_add_id)
        finally have "frac (v y) ≤ frac ?l" using L by auto
      } note L_bound = this
      { fix y assume y: "y ∈ ?X₀" "x ≠ y" "(x,y) ∈ r"
        then have U: "frac (v y) ∈ ?U" by auto
        with Min_in[OF fin(2)] have In: "Min ?U ∈ ?U" by auto
        then have "frac (Min ?U) = (Min ?U)" using frac_frac by fastforce
        have "frac (c + Min ?U) = frac (Min ?U)" by (auto simp: frac_nat_add_id)
        also have "… = Min ?U" using In frac_frac by fastforce
        also from Min_le[OF fin(2) U] have "Min ?U ≤ frac (v y)" .
        finally have "frac ?u ≤ frac (v y)" using U by auto
      } note U_bound = this
      { assume "?L ≠ {}"
        from Max_in[OF fin(1) this] obtain l d where l:
          "Max ?L = frac (v l)" "l ∈ X" "x ≠ l" "I l = Intv d"
        by auto
        with v have "d < v l" "v l < d + 1" by fastforce+
        with nat_intv_frac_gt0[OF this] frac_lt_1 l(1) have "0 < Max ?L" "Max ?L < 1" by auto
        then have "c < c + Max ?L" "c + Max ?L < c + 1" by simp+
      } note L_intv = this
      { assume "?U ≠ {}"
        from Min_in[OF fin(2) this] obtain u d where u:
          "Min ?U = frac (v u)" "u∈ X" "x ≠ u" "I u = Intv d"
        by auto
        with v have "d < v u" "v u < d + 1" by fastforce+
        with nat_intv_frac_gt0[OF this] frac_lt_1 u(1) have "0 < Min ?U" "Min ?U < 1" by auto
        then have "c < c + Min ?U" "c + Min ?U < c + 1" by simp+
      } note U_intv = this
      have l_bound: "c ≤ ?l"
      proof (cases "?L = {}")
        case True
        note T = this
        show ?thesis
        proof (cases "?U = {}")
          case True
          with T show ?thesis by simp
        next
          case False
          with U_intv T show ?thesis by simp
        qed
      next
        case False
        with L_intv show ?thesis by simp
      qed
      have l_bound': "c < ?u"
      proof (cases "?L = {}")
        case True
        note T = this
        show ?thesis
        proof (cases "?U = {}")
          case True
          with T show ?thesis by simp
        next
          case False
          with U_intv T show ?thesis by simp
        qed
      next
        case False
        with U_intv show ?thesis by simp
      qed
      have u_bound: "?u ≤ c + 1"
      proof (cases "?U = {}")
        case True
        note T = this
        show ?thesis
        proof (cases "?L = {}")
          case True
          with T show ?thesis by simp
        next
          case False
          with L_intv T show ?thesis by simp
        qed
      next
        case False
        with U_intv show ?thesis by simp
      qed
      have u_bound': "?l < c + 1"
      proof (cases "?U = {}")
        case True
        note T = this
        show ?thesis
        proof (cases "?L = {}")
          case True
          with T show ?thesis by simp
        next
          case False
          with L_intv T show ?thesis by simp
        qed
      next
        case False
        with L_intv show ?thesis by simp
      qed
      have frac_c: "frac c = 0" "frac (c+1) = 0" by auto
      have l_u: "?l ≤ ?u"
      proof (cases "?L = {}")
        case True
        note T = this
        show ?thesis
        proof (cases "?U = {}")
          case True
          with T show ?thesis by simp
        next
          case False
          with T show ?thesis using Min_in[OF fin(2) False] by (auto simp: frac_c)
        qed
      next
        case False
        with Max_in[OF fin(1) this] have l: "?l = c + Max ?L" "Max ?L ∈ ?L" by auto
        note F = False
        from l(1) have *: "Max ?L < 1" using False L_intv(2) by linarith
        show ?thesis
        proof (cases "?U = {}")
          case True
          with F l * show ?thesis by simp
        next
          case False
          from Min_in[OF fin(2) this] l(2) obtain l u where l_u:
            "Max ?L = frac (v l)" "Min ?U = frac (v u)" "l ∈ ?X₀" "u ∈ ?X₀" "(l,x) ∈ r" "(x,u) ∈ r"
            "x ≠ l" "x ≠ u"
          by auto
          from trans l_u(5-) have "(l,u) ∈ ?r" unfolding trans_def by blast
          with l_u(1-4) v have *: "Max ?L ≤ Min ?U" by fastforce
          with l_u(1,2) have "frac (Max ?L) ≤ frac (Min ?U)" by (simp add: frac_frac)
          with frac_nat_add_id l(1) False have "frac ?l ≤ frac ?u" by simp
          with l(1) * False show ?thesis by simp
        qed
      qed
      obtain d where d: "d = (?l + ?u) / 2" by blast
      with l_u have d2: "?l ≤ d" "d ≤ ?u" by simp+
      from d l_bound l_bound' u_bound u_bound' have d3: "c < d" "d < c + 1" "d ≥ 0" by simp+
      have "floor ?l = c"
      proof (cases "?L = {}")
        case False
        from L_intv[OF False] have "0 ≤ Max ?L" "Max ?L < 1" by auto
        from floor_nat_add_id[OF this] False show ?thesis by simp
      next
        case True
        note T = this
        show ?thesis
        proof (cases "?U = {}")
          case True
          with T show ?thesis by (simp add: floor_nat_add_id)
        next
          case False
          from U_intv[OF False] have "0 ≤ Min ?U" "Min ?U < 1" by auto
          from floor_nat_add_id[OF this] T False show ?thesis by simp
        qed
      qed
      have floor_u: "floor ?u = (if ?U = {} ∧ ?L ≠ {} then c + 1 else c)"
      proof (cases "?U = {}")
        case False
        from U_intv[OF False] have "0 ≤ Min ?U" "Min ?U < 1" by auto
        from floor_nat_add_id[OF this] False show ?thesis by simp
      next
        case True
        note T = this
        show ?thesis
        proof (cases "?L = {}")
          case True
          with T show ?thesis by (simp add: floor_nat_add_id)
        next
          case False
          from L_intv[OF False] have "0 ≤ Max ?L" "Max ?L < 1" by auto
          from floor_nat_add_id[OF this] T False show ?thesis by auto
        qed
      qed
      { assume "?L ≠ {}" "?U ≠ {}"
        from Max_in[OF fin(1) ‹?L ≠ {}›] obtain w where w:
          "w ∈ ?X₀" "x ≠ w" "(w,x) ∈ r" "Max ?L = frac (v w)"
        by auto
        from Min_in[OF fin(2) ‹?U ≠ {}›] obtain z where z:
          "z ∈ ?X₀" "x ≠ z" "(x,z) ∈ r" "Min ?U = frac (v z)"
        by auto
        from w z trans have "(w,z) ∈ r" unfolding trans_def by blast
        with v w z have "Max ?L ≤ Min ?U" by fastforce
      } note l_le_u = this
      { fix y assume y: "y ∈ ?X₀" "x ≠ y"
        from total y ‹x ∈ X› Intv have total: "(x,y) ∈ r ∨ (y,x) ∈ r" unfolding total_on_def by auto
        have "frac (v y) = frac d ⟷ (y,x) ∈ r ∧ (x,y) ∈ r"
        proof safe
          assume A: "(y,x) ∈ r" "(x,y) ∈ r"
          from L_bound[OF y A(1)] U_bound[OF y A(2)] have *:
            "frac (v y) ≤ frac ?l" "frac ?u ≤ frac (v y)"
          by auto
          from A y have **: "?L ≠ {}" "?U ≠ {}" by auto
          with L_intv[OF this(1)] U_intv[OF this(2)] have "frac ?l = Max ?L" "frac ?u = Min ?U"
          by (auto simp: frac_nat_add_id frac_eq)
          with * ** l_le_u have "frac ?l = frac ?u" "frac (v y) = frac ?l" by auto
          with d have "d = ((floor ?l + floor ?u) + (frac (v y) + frac (v y))) / 2"
          unfolding frac_def by auto
          also have "… = c + frac (v y)" using ‹floor ?l = c› floor_u ‹?U ≠ {}› by auto
          finally show "frac (v y) = frac d" using frac_nat_add_id frac_frac by metis
        next
          assume A: "frac (v y) = frac d"
          show "(y, x) ∈ r"
          proof (rule ccontr)
            assume B: "(y,x) ∉ r"
            with total have B': "(x,y) ∈ r" by auto
            from U_bound[OF y this] have u_y:"frac ?u ≤ frac (v y)" by auto
            from y B' have U: "?U ≠ {}" and "frac (v y) ∈ ?U" by auto
            then have u: "frac ?u = Min ?U" using Min_in[OF fin(2) ‹?U ≠ {}›]
            by (auto simp: frac_nat_add_id frac_frac)
            show False
            proof (cases "?L = {}")
              case True
              from U_intv[OF U] have "0 < Min ?U" "Min ?U < 1" by auto
              then have *: "frac (Min ?U / 2) = Min ?U / 2" unfolding frac_eq by simp
              from d U True have "d = ((c + c) + Min ?U) / 2" by auto
              also have "… = c + Min ?U / 2" by simp
              finally have "frac d = Min ?U / 2" using * by (simp add: frac_nat_add_id)
              also have "… < Min ?U" using ‹0 < Min ?U› by auto
              finally have "frac d < frac ?u" using u by auto
              with u_y A show False by auto
            next
              case False
              then have l:  "?l = c + Max ?L" by simp
              from Max_in[OF fin(1) ‹?L ≠ {}›]
              obtain w where w:
                "w ∈ ?X₀" "x ≠ w" "(w,x) ∈ r" "Max ?L = frac (v w)"
              by auto
              with ‹(y,x) ∉ r› trans have **: "(y,w) ∉ r" unfolding trans_def by blast
              from Min_in[OF fin(2) ‹?U ≠ {}›] Max_in[OF fin(1) ‹?L ≠ {}›] frac_lt_1
              have "0 ≤ Max ?L" "Max ?L < 1" "0 ≤ Min ?U" "Min ?U < 1" by auto
              then have "0 ≤ (Max ?L + Min ?U) / 2" "(Max ?L + Min ?U) / 2 < 1" by auto
              then have ***: "frac ((Max ?L + Min ?U) / 2) = (Max ?L + Min ?U) / 2" unfolding frac_eq ..
              from y w have "y ∈ ?X₀'" "w ∈ ?X₀'" by auto
              with v ** have lt: "frac (v y) > frac (v w)" by fastforce
              from d U l have "d = ((c + c) + (Max ?L + Min ?U))/2" by auto
              also have "… = c + (Max ?L + Min ?U) / 2" by simp
              finally have "frac d = frac ((Max ?L + Min ?U) / 2)" by (simp add: frac_nat_add_id)
              also have "… = (Max ?L + Min ?U) / 2" using *** by simp
              also have "… < (frac (v y) + Min ?U) / 2" using lt w(4) by auto
              also have "… ≤ frac (v y)" using Min_le[OF fin(2) ‹frac (v y) ∈ ?U›] by auto
              finally show False using A by auto
            qed
          qed
        next
          assume A: "frac (v y) = frac d"
          show "(x, y) ∈ r"
          proof (rule ccontr)
            assume B: "(x,y) ∉ r"
            with total have B': "(y,x) ∈ r" by auto
            from L_bound[OF y this] have l_y:"frac ?l ≥ frac (v y)" by auto
            from y B' have L: "?L ≠ {}" and "frac (v y) ∈ ?L" by auto
            then have l: "frac ?l = Max ?L" using Max_in[OF fin(1) ‹?L ≠ {}›]
            by (auto simp: frac_nat_add_id frac_frac)
            show False
            proof (cases "?U = {}")
              case True
              from L_intv[OF L] have *: "0 < Max ?L" "Max ?L < 1" by auto
              from d L True have "d = ((c + c) + (1 + Max ?L)) / 2" by auto
              also have "… = c + (1 + Max ?L) / 2" by simp
              finally have "frac d = frac ((1 + Max ?L) / 2)" by (simp add: frac_nat_add_id)
              also have "… = (1 + Max ?L) / 2" using * unfolding frac_eq by auto
              also have "… > Max ?L" using * by auto
              finally have "frac d > frac ?l" using l by auto
              with l_y A show False by auto
            next
              case False
              then have u: "?u = c + Min ?U" by simp
              from Min_in[OF fin(2) ‹?U ≠ {}›]
              obtain w where w:
                "w ∈ ?X₀" "x ≠ w" "(x,w) ∈ r" "Min ?U = frac (v w)"
              by auto
              with ‹(x,y) ∉ r› trans have **: "(w,y) ∉ r" unfolding trans_def by blast
              from Min_in[OF fin(2) ‹?U ≠ {}›] Max_in[OF fin(1) ‹?L ≠ {}›] frac_lt_1
              have "0 ≤ Max ?L" "Max ?L < 1" "0 ≤ Min ?U" "Min ?U < 1" by auto
              then have "0 ≤ (Max ?L + Min ?U) / 2" "(Max ?L + Min ?U) / 2 < 1" by auto
              then have ***: "frac ((Max ?L + Min ?U) / 2) = (Max ?L + Min ?U) / 2" unfolding frac_eq ..
              from y w have "y ∈ ?X₀'" "w ∈ ?X₀'" by auto
              with v ** have lt: "frac (v y) < frac (v w)" by fastforce
              from d L u have "d = ((c + c) + (Max ?L + Min ?U))/2" by auto
              also have "… = c + (Max ?L + Min ?U) / 2" by simp
              finally have "frac d = frac ((Max ?L + Min ?U) / 2)" by (simp add: frac_nat_add_id)
              also have "… = (Max ?L + Min ?U) / 2" using *** by simp
              also have "… > (Max ?L + frac (v y)) / 2" using lt w(4) by auto
              finally have "frac d > frac (v y)" using Max_ge[OF fin(1) ‹frac (v y) ∈ ?L›] by auto
              then show False using A by auto
            qed
          qed
        qed
      } note d_frac_equiv = this
      have frac_l: "frac ?l ≤ frac d"
      proof (cases "?L = {}")
        case True
        note T = this
        show ?thesis
        proof (cases "?U = {}")
          case True
          with T have "?l = ?u" by auto
          with d have "d = ?l" by auto
          then show ?thesis by auto
        next
          case False
          with T have "frac ?l = 0" by auto
          moreover have "frac d ≥ 0" by auto
          ultimately show ?thesis by linarith
        qed
      next
        case False
        note F = this
        then have l: "?l = c + Max ?L" "frac ?l = Max ?L" using Max_in[OF fin(1) ‹?L ≠ {}›]
        by (auto simp: frac_nat_add_id frac_frac)
        from L_intv[OF F] have *: "0 < Max ?L" "Max ?L < 1" by auto
        show ?thesis
        proof (cases "?U = {}")
          case True
          from True F have "?u = c + 1" by auto
          with l d have "d = ((c + c) + (Max ?L + 1)) / 2" by auto
          also have "… = c + (1 + Max ?L) / 2" by simp
          finally have "frac d = frac ((1 + Max ?L) / 2)" by (simp add: frac_nat_add_id)
          also have "… = (1 + Max ?L) / 2" using * unfolding frac_eq by auto
          also have "… > Max ?L" using * by auto
          finally show "frac d ≥ frac ?l" using l by auto
        next
          case False
          then have u: "?u = c + Min ?U" "frac ?u = Min ?U" using Min_in[OF fin(2) False]
          by (auto simp: frac_nat_add_id frac_frac)
          from U_intv[OF False] have **: "0 < Min ?U" "Min ?U < 1" by auto
          from l u d have "d = ((c + c) + (Max ?L + Min ?U)) / 2" by auto
          also have "… = c + (Max ?L + Min ?U) / 2" by simp
          finally have "frac d = frac ((Max ?L + Min ?U) / 2)" by (simp add: frac_nat_add_id)
          also have "… = (Max ?L + Min ?U) / 2" using * ** unfolding frac_eq by auto
          also have "… ≥ Max ?L" using l_le_u[OF F False] by auto
          finally show ?thesis using l by auto
        qed
      qed
      have frac_u: "?U ≠ {} ∨ ?L = {} ⟶ frac d ≤ frac ?u"
      proof (cases "?U = {}")
        case True
        note T = this
        show ?thesis
        proof (cases "?L = {}")
          case True
          with T have "?l = ?u" by auto
          with d have "d = ?u" by auto
          then show ?thesis by auto
        next
          case False
          with T show ?thesis by auto
        qed
      next
        case False
        note F = this
        then have u: "?u = c + Min ?U" "frac ?u = Min ?U" using Min_in[OF fin(2) ‹?U ≠ {}›]
        by (auto simp: frac_nat_add_id frac_frac)
        from U_intv[OF F] have *: "0 < Min ?U" "Min ?U < 1" by auto
        show ?thesis
        proof (cases "?L = {}")
          case True
          from True F have "?l = c" by auto
          with u d have "d = ((c + c) + Min ?U) / 2" by auto
          also have "… = c + Min ?U / 2" by simp
          finally have "frac d = frac (Min ?U / 2)" by (simp add: frac_nat_add_id)
          also have "… = Min ?U / 2" unfolding frac_eq using * by auto
          also have "… ≤ Min ?U" using ‹0 < Min ?U› by auto
          finally have "frac d ≤ frac ?u" using u by auto
          then show ?thesis by auto
        next
          case False
          then have l: "?l = c + Max ?L" "frac ?l = Max ?L" using Max_in[OF fin(1) False]
          by (auto simp: frac_nat_add_id frac_frac)
          from L_intv[OF False] have **: "0 < Max ?L" "Max ?L < 1" by auto
          from l u d have "d = ((c + c) + (Max ?L + Min ?U)) / 2" by auto
          also have "… = c + (Max ?L + Min ?U) / 2" by simp
          finally have "frac d = frac ((Max ?L + Min ?U) / 2)" by (simp add: frac_nat_add_id)
          also have "… = (Max ?L + Min ?U) / 2" using * ** unfolding frac_eq by auto
          also have "… ≤ Min ?U" using l_le_u[OF False F] by auto
          finally show ?thesis using u by auto
        qed
      qed
      have "∀ y ∈ ?X₀ - {x}. (y,x) ∈ r ⟷ frac (v y) ≤ frac d"
      proof (safe, goal_cases)
        case (1 y k)
        with L_bound[of y] frac_l show ?case by auto
      next
        case (2 y k)
        show ?case
        proof (rule ccontr, goal_cases)
          case 1
          with total 2 ‹x ∈ X› Intv have "(x,y) ∈ r" unfolding total_on_def by auto
          with 2 U_bound[of y] have "?U ≠ {}" "frac ?u ≤ frac (v y)" by auto
          with frac_u have "frac d ≤ frac (v y)" by auto
          with 2 d_frac_equiv 1 show False by auto
        qed
      qed
      moreover have "∀ y ∈ ?X₀ - {x}. (x,y) ∈ r ⟷ frac d ≤ frac (v y)"
      proof (safe, goal_cases)
        case (1 y k)
        then have "?U ≠ {}" by auto
        with 1 U_bound[of y] frac_u show ?case by auto
      next
        case (2 y k)
        show ?case
        proof (rule ccontr, goal_cases)
          case 1
          with total 2 ‹x ∈ X› Intv have "(y,x) ∈ r" unfolding total_on_def by auto
          with 2 L_bound[of y] have "frac (v y) ≤ frac ?l" by auto
          with frac_l have "frac (v y) ≤ frac d" by auto
          with 2 d_frac_equiv 1 show False by auto
        qed
      qed
      ultimately have d:
        "c < d" "d < c + 1" "∀ y ∈ ?X₀ - {x}. (y,x) ∈ r ⟷ frac (v y) ≤ frac d"
        "∀ y ∈ ?X₀ - {x}. (x,y) ∈ r ⟷ frac d ≤ frac (v y)"
      using d3 by auto
      let ?v = "v(x := d)"
      have "?v ∈ region X I r"
      proof (standard, goal_cases)
        case 1
        from ‹d≥0› v show ?case by auto
      next
        case 2
        show ?case
        proof (safe, goal_cases)
          case (1 y)
          with v have "intv_elem y v (?I y)" by fast
          with Intv d(1,2) show "intv_elem y ?v (I y)" by (cases "x = y", auto) (cases "I y", auto)
        qed
      next
        from ‹x ∈ X› Intv show "?X₀' ∪ {x} = ?X₀" by auto
        with r_subset have "r ⊆ (?X₀' ∪ {x}) × (?X₀' ∪ {x})" by auto
        have "∀ x ∈ ?X₀'. ∀ y ∈ ?X₀'. (x,y) ∈ r ⟷ (x,y) ∈ ?r" by auto
        with v have "∀ x ∈ ?X₀'. ∀ y ∈ ?X₀'. (x,y) ∈ r ⟷ frac (v x) ≤ frac (v y)" by fastforce
        then have "∀ x ∈ ?X₀'. ∀ y ∈ ?X₀'. (x,y) ∈ r ⟷ frac (?v x) ≤ frac (?v y)" by auto
        with d(3,4) show "∀ y ∈ ?X₀' ∪ {x}. ∀ z ∈ ?X₀' ∪ {x}. (y,z) ∈ r ⟷ frac (?v y) ≤ frac (?v z)"
        proof (auto, goal_cases)
          case 1
          from refl ‹x ∈ X› Intv show ?case by (auto simp: refl_on_def)
        qed
      qed
      then show ?thesis by auto
    qed
    then obtain d where "v(x := d) ∈ R" using R by auto
    then have "(v(x := d))(x := c) ∈ region_set R x c" unfolding region_set_def by blast
    moreover from v ‹x ∈ X› have "(v(x := d))(x := c) = v" by fastforce
    ultimately have "v ∈ region_set R x c" by simp
  }

  ultimately have "region_set R x c = region X ?I ?r" by blast
  with valid R_def have *: "region_set R x c ∈ R" by auto
  moreover from assms have **: "v (x := c) ∈ region_set R x c" unfolding region_set_def by auto
  ultimately show "[v(x := c)]_\<R> = region_set R x c" "[v(x := c)]_\<R> ∈ R" "v(x := c) ∈ [v(x := c)]_\<R>"
  using region_unique[OF _ ** *] R_def by auto
qed

definition region_set'
where
  "region_set' R r c = {[r → c]v | v. v ∈ R}"

lemma region_set'_id:
  fixes X k and c :: nat
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  assumes "R ∈ R" "v ∈ R" "finite X" "0 ≤ c" "∀ x ∈ set r. c ≤ k x" "set r ⊆ X"
  shows "[[r → c]v]_\<R> = region_set' R r c ∧ [[r → c]v]_\<R> ∈ R ∧ [r → c]v ∈ [[r → c]v]_\<R>" using assms
proof (induction r)
  case Nil
  from regions_closed[OF _ Nil(2,3)] regions_closed'[OF _ Nil(2,3)] region_unique[OF _ Nil(3,2)] Nil(1)
  have "[v]_\<R> = R" "[v ⊕ 0]_\<R> ∈ R" "(v ⊕ 0) ∈ [v ⊕ 0]_\<R>" by auto
  then show ?case unfolding region_set'_def cval_add_def by simp
next
  case (Cons x xs)
  then have "[[xs→c]v]_\<R> = region_set' R xs c" "[[xs→c]v]_\<R> ∈ R" "[xs→c]v ∈ [[xs→c]v]_\<R>" by force+
  note IH = this[unfolded R_def]
  let ?v = "([xs→c]v)(x := c)"
  from region_set_id[OF IH(2,3) ‹finite X› ‹c ≥ 0›, of x] R_def Cons.prems(5,6)
  have "[?v]_\<R> = region_set ([[xs→real c]v]_\<R>) x c" "[?v]_\<R> ∈ R" "?v ∈ [?v]_\<R>" by auto
  moreover have "region_set' R (x # xs) (real c) = region_set ([[xs→real c]v]_\<R>) x c"
  unfolding region_set_def region_set'_def
  proof (safe, goal_cases)
    case (1 y u)
    let ?u = "[xs→real c]u"
    have "[x # xs→real c]u = ?u(x := real c)" by auto
    moreover from IH(1) 1 have "?u ∈ [[xs→real c]v]_\<R>" unfolding R_def region_set'_def by auto
    ultimately show ?case by auto
  next
    case (2 y u)
    with IH(1)[unfolded region_set'_def R_def[symmetric]] show ?case by auto
  qed
  moreover have "[x # xs→real c]v = ?v" by simp
  ultimately show ?case by presburger
qed

text ‹
 This is the only additional lemma necessary to make local ‹α›-closures work.
 ›
lemma region_set_subs:
  fixes X k k' and c :: nat
  defines "R ≡ {region X I r |I r. valid_region X k I r}"
  defines "R' ≡ {region X I r |I r. valid_region X k' I r}"
  assumes "R ∈ R" "v ∈ R" "finite X" "0 ≤ c" "set cs ⊆ X" "∀ y. y ∉ set cs ⟶ k y ≥ k' y"
  shows "[[cs → c]v]_\<R>' ⊇ region_set' R cs c" "[[cs → c]v]_\<R>' ∈ R'" "[cs → c]v ∈ [[cs → c]v]_\<R>'"
proof -
  from assms obtain I r where R: "R = region X I r" "valid_region X k I r" "v ∈ region X I r" by auto
  ― ‹The set of movers, that is all intervals that now are unbounded due to changing from ‹k› to ‹k'››
  let ?M = "{x ∈ X. isIntv (I x) ∧ intv_const (I x) ≥ k' x ∨ intv_const (I x) > k' x}"
  let ?I = "λ y.
    if y ∈ set cs then (if c ≤ k' y then Const c else Greater (k' y))
    else if (isIntv (I y) ∧ intv_const (I y) ≥ k' y ∨ intv_const (I y) > k' y) then Greater (k' y)
    else I y"
  let ?r = "{(y,z) ∈ r. y ∉ set cs ∧ z ∉ set cs ∧ y ∉ ?M ∧ z ∉ ?M}"
  let ?X₀ = "{x ∈ X. ∃ c. I x = Intv c}"
  let ?X₀' = "{x ∈ X. ∃ c. ?I x = Intv c}"

  have r_subset: "r ⊆ ?X₀ × ?X₀" and refl: "refl_on ?X₀ r" and trans: "trans r" and
    total: "total_on ?X₀ r"
    using R(2) by auto

  have valid: "valid_region X k' ?I ?r"
  proof
    show "?X₀' = ?X₀'" by auto
  next
    show "?r ⊆ ?X₀' × ?X₀'"
      using r_subset by auto
  next
    from refl show "refl_on ?X₀' ?r" unfolding refl_on_def by auto
  next
    from trans show "trans ?r" unfolding trans_def by auto
  next
    from total show "total_on ?X₀' ?r" unfolding total_on_def by auto
  next
    from R(2) have "∀ x ∈ X. valid_intv (k x) (I x)" by auto
    then show "∀ x ∈ X. valid_intv (k' x) (?I x)"
      apply safe
      subgoal for x'
        using ‹∀ y. y ∉ set cs ⟶ k y ≥ k' y›
        by (cases "I x'"; force)
      done
  qed

  { fix v assume v: "v ∈ region_set' R cs c"
    with R(1) obtain v' where v': "v' ∈ region X I r" "v = [cs → c]v'"
      unfolding region_set'_def by auto
    have "v ∈ region X ?I ?r"
    proof (standard, goal_cases)
      case 1
      from v' ‹0 ≤ c› show ?case
        apply -
        apply rule
        subgoal for x
          by (cases "x ∈ set cs") auto
        done
    next
      case 2
      from v' show ?case
        apply -
        apply rule
        subgoal for x'
            by (cases "I x'"; cases "x' ∈ set cs"; force)
        done
    next
      show "?X₀' = ?X₀'" by auto
    next
      from v' show "∀ y ∈ ?X₀'. ∀ z ∈ ?X₀'. (y,z) ∈ ?r ⟷ frac (v y) ≤ frac (v z)" by auto
    qed
  }
  then have "region_set' R cs c ⊆ region X ?I ?r" by blast
  moreover from valid have *: "region X ?I ?r ∈ R'" unfolding R'_def by blast
  moreover from assms have **: "[cs → c]v ∈ region_set' R cs c" unfolding region_set'_def by auto
  ultimately show
    "[[cs → c]v]_\<R>' ⊇ region_set' R cs c" "[[cs → c]v]_\<R>' ∈ R'" "[cs → c]v ∈ [[cs → c]v]_\<R>'"
    using region_unique[of R', OF _ _ *, unfolded R'_def, OF HOL.refl]
    unfolding R'_def[symmetric] by auto
qed

section ‹A Semantics Based on Regions›

subsection ‹Single step›

inductive step_r ::
  "('a, 'c, t, 's) ta → ('c, t) zone set → 's → ('c, t) zone → 's → ('c, t) zone → bool"
(‹_,_ ⊨ ⟨_, _⟩ ↝ ⟨_, _⟩› [61,61,61,61] 61)
where
  step_t_r:
  "[R = {region X I r |I r. valid_region X k I r}; valid_abstraction A X k; R ∈ R; R' ∈ Succ R R;
    R' ⊆ {inv_of A l}] ==> A,R ⊨ ⟨l,R⟩ ↝ ⟨l,R'⟩" |
  step_a_r:
  "[R = {region X I r |I r. valid_region X k I r}; valid_abstraction A X k; A ⊨ l ⟶^,a,r l'; R ∈ R]
    ==> A,R ⊨ ⟨l,R⟩ ↝ ⟨l',region_set' (R ∩ {u. u ⊨ g}) r 0 ∩ {u. u ⊨ inv_of A l'}⟩"

inductive_cases[elim!]: "A,R ⊨ ⟨l, u⟩ ↝ ⟨l', u'⟩"

declare step_r.intros[intro]

lemma region_cover':
  assumes "R = {region X I r |I r. valid_region X k I r}" and "∀x∈X. 0 ≤ v x"
  shows "v ∈ [v]_\<R>" "[v]_\<R> ∈ R"
proof -
  from region_cover[OF assms(2), of k] assms obtain R where R: "R ∈ R" "v ∈ R" by auto
  from regions_closed'[OF assms(1) R, of 0] show "v ∈ [v]_\<R>" unfolding cval_add_def by auto
  from regions_closed[OF assms(1) R, of 0] show "[v]_\<R> ∈ R" unfolding cval_add_def by auto
qed

lemma step_r_complete_aux:
  fixes R r A l' g
  defines "R' ≡ region_set' (R ∩ {u. u ⊨ g}) r 0 ∩ {u. u ⊨ inv_of A l'}"
  assumes "R = {region X I r |I r. valid_region X k I r}"
    and "valid_abstraction A X k"
    and "u ∈ R"
    and "R ∈ R"
    and "A ⊨ l ⟶^,a,r l'"
    and "u ⊨ g"
    and "[r→0]u ⊨ inv_of A l'"
  shows "R = R ∩ {u. u ⊨ g} ∧ R' = region_set' R r 0 ∧ R' ∈ R"
proof -
  note A = assms(2-)
  from A(2) have *:
    "∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
    "collect_clkvt (trans_of A) ⊆ X"
    "finite X"
  by (fastforce elim: valid_abstraction.cases)+
  from A(5) *(2) have r: "set r ⊆ X" unfolding collect_clkvt_def by fastforce
  from *(1) A(5) have "∀(x, m)∈collect_clock_pairs g. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
  unfolding clkp_set_def collect_clkt_def by fastforce
  from ccompatible[OF this, folded A(1)] A(3,4,6) have "R ⊆ {g}"
  unfolding ccompatible_def ccval_def by blast
  then have R_id: "R ∩ {u. u ⊨ g} = R" unfolding ccval_def by auto
  from region_set'_id[OF A(4)[unfolded A(1)] A(3) *(3) _ _ r, of 0, folded A(1)]
  have **:
    "[[r→0]u]_\<R> = region_set' R r 0" "[[r→0]u]_\<R> ∈ R" "[r→0]u ∈ [[r→0]u]_\<R>"
  by auto
  let ?R = "[[r→0]u]_\<R>"
  from *(1) A(5) have ***:
    "∀(x, m) ∈ collect_clock_pairs (inv_of A l'). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
  unfolding inv_of_def clkp_set_def collect_clki_def by fastforce
  from ccompatible[OF this, folded A(1)] **(2-) A(7) have "?R ⊆ {inv_of A l'}"
  unfolding ccompatible_def ccval_def by blast
  then have ***: "?R ∩ {u. u ⊨ inv_of A l'} = ?R" unfolding ccval_def by auto
  with **(1,2) R_id show ?thesis by (auto simp: R'_def)
qed

lemma step_r_complete:
  "[A ⊨ ⟨l, u⟩ → ⟨l',u'⟩; R = {region X I r |I r. valid_region X k I r}; valid_abstraction A X k;
    ∀ x ∈ X. u x ≥ 0] ==> ∃ R'. A,R ⊨ ⟨l, ([u]_\<R>)⟩ ↝ ⟨l',R'⟩ ∧ u' ∈ R' ∧ R' ∈ R"
proof (induction rule: step.induct, goal_cases)
  case (1 A l u a l' u')
  note A = this
  then obtain g r where u': "u' = [r→0]u" "A ⊨ l ⟶^,a,r l'" "u ⊨ g" "u' ⊨ inv_of A l'"
  by (cases rule: step_a.cases) auto
  let ?R'= "region_set' (([u]_\<R>) ∩ {u. u ⊨ g}) r 0 ∩ {u. u ⊨ inv_of A l'}"
  from region_cover'[OF A(2,4)] have R: "[u]_\<R> ∈ R" "u ∈ [u]_\<R>" by auto
  from step_r_complete_aux[OF A(2,3) this(2,1) u'(2,3)] u'
  have *: "[u]_\<R> = ([u]_\<R>) ∩ {u. u ⊨ g}" "?R' = region_set' ([u]_\<R>) r 0" "?R' ∈ R" by auto
  from 1(2,3) have "collect_clkvt (trans_of A) ⊆ X" "finite X" by (auto elim: valid_abstraction.cases)
  with u'(2) have r: "set r ⊆ X" unfolding collect_clkvt_def by fastforce
  from * u'(1) R(2) have "u' ∈ ?R'" unfolding region_set'_def by auto
  moreover have "A,R ⊨ ⟨l,([u]_\<R>)⟩ ↝ ⟨l',?R'⟩" using R(1) A(2,3) u'(2) by auto
  ultimately show ?case using *(3) by meson
next
  case (2 A l u d l' u')
  hence u': "u' = (u ⊕ d)" "u ⊕ d ⊨ inv_of A l" "0 ≤ d" and "l = l'" by (auto elim!: step_t.cases)
  from region_cover'[OF 2(2,4)] have R: "[u]_\<R> ∈ R" "u ∈ [u]_\<R>" by auto
  from SuccI2[OF 2(2) this(2,1) ‹0 ≤ d›, of "[u']_\<R>"] u'(1) have u'1:
    "[u']_\<R> ∈ Succ R ([u]_\<R>)" "[u']_\<R> ∈ R"
  by auto
  from regions_closed'[OF 2(2) R(1,2) ‹0 ≤ d›] u'(1) have u'2: "u' ∈ [u']_\<R>" by simp
  from 2(3) have *:
    "∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
    "collect_clkvt (trans_of A) ⊆ X"
    "finite X"
  by (fastforce elim: valid_abstraction.cases)+
  from *(1) u'(2) have "∀(x, m)∈collect_clock_pairs (inv_of A l). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
  unfolding clkp_set_def collect_clki_def inv_of_def by fastforce
  from ccompatible[OF this, folded 2(2)] u'1(2) u'2 u'(1,2,3) R have
    "[u']_\<R> ⊆ {inv_of A l}"
  unfolding ccompatible_def ccval_def by auto
  with 2 u'1 R(1) have "A,R ⊨ ⟨l, ([u]_\<R>)⟩ ↝ ⟨l,([u']_\<R>)⟩" by auto
  with u'1(2) u'2 ‹l = l'› show ?case by meson
qed

text ‹
 Compare this to lemma ‹step_z_sound›. This version is weaker because for regions we may very well
 arrive at a successor for which not every valuation can be reached by the predecessor.
 This is the case for e.g. the region with only Greater (k x) bounds.
 ›

lemma step_r_sound:
  "A,R ⊨ ⟨l, R⟩ ↝ ⟨l',R'⟩ ==> R = {region X I r |I r. valid_region X k I r}
  ==> R' ≠ {} ==> (∀ u ∈ R. ∃ u' ∈ R'. A ⊨ ⟨l, u⟩ → ⟨l',u'⟩)"
proof (induction rule: step_r.induct)
  case (step_t_r R X k A R R' l)
  note A = this[unfolded this(1)]
  show ?case
  proof
    fix u assume u: "u ∈ R"
    from set_of_regions[OF A(3) this A(4), folded step_t_r(1)] A(2)
    obtain t where t: "t ≥ 0" "[u ⊕ t]_\<R> = R'" by (auto elim: valid_abstraction.cases)
    with regions_closed'[OF A(1,3) u this(1)] step_t_r(1) have *: "(u ⊕ t) ∈ R'" by auto
    with u t(1) A(5,6) have "A ⊨ ⟨l, u⟩ → ⟨l,(u ⊕ t)⟩" unfolding ccval_def by auto
    with t * show "∃u'∈R'. A ⊨ ⟨l, u⟩ → ⟨l,u'⟩" by meson
  qed
next
  case A: (step_a_r R X k A l g a r l' R)
  show ?case
  proof
    fix u assume u: "u ∈ R"
    from A(6) obtain v where v: "v ∈ R" "v ⊨ g" "[r→0]v ⊨ inv_of A l'" unfolding region_set'_def by auto
    let ?R' = "region_set' (R ∩ {u. u ⊨ g}) r 0 ∩ {u. u ⊨ inv_of A l'}"
    from step_r_complete_aux[OF A(1,2) v(1) A(4,3) v(2-)] have R:
      "R = R ∩ {u. u ⊨ g}" "?R' = region_set' R r 0"
    by auto
    from A have "collect_clkvt (trans_of A) ⊆ X" by (auto elim: valid_abstraction.cases)
    with A(3) have r: "set r ⊆ X" unfolding collect_clkvt_def by fastforce
    from u R have *: "[r→0]u ∈ ?R'" "u ⊨ g" "[r→0]u ⊨ inv_of A l'" unfolding region_set'_def by auto
    with A(3) have "A ⊨ ⟨l, u⟩ → ⟨l',[r→0]u⟩" apply (intro step.intros(1)) apply rule by auto
    with * show "∃a∈?R'. A ⊨ ⟨l, u⟩ → ⟨l',a⟩" by meson
  qed
qed

subsection ‹Multi Step›

inductive
  steps_r :: "('a, 'c, t, 's) ta → ('c, t) zone set → 's → ('c, t) zone → 's → ('c, t) zone → bool"
(‹_,_ ⊨ ⟨_, _⟩ ↝* ⟨_, _⟩› [61,61,61,61,61,61] 61)
where
  refl: "A,R ⊨ ⟨l, R⟩ ↝* ⟨l, R⟩" |
  step: "A,R ⊨ ⟨l, R⟩ ↝* ⟨l', R'⟩ ==> A,R ⊨ ⟨l', R'⟩ ↝ ⟨l'', R''⟩ ==> A,R ⊨ ⟨l, R⟩ ↝* ⟨l'', R''⟩"

declare steps_r.intros[intro]

lemma steps_alt:
  "A ⊨ ⟨l, u⟩ →* ⟨l',u'⟩ ==> A ⊨ ⟨l', u'⟩ → ⟨l'',u''⟩ ==> A ⊨ ⟨l, u⟩ →* ⟨l'',u''⟩"
by (induction rule: steps.induct) auto

lemma emptiness_preservance: "A,R ⊨ ⟨l, R⟩ ↝ ⟨l',R'⟩ ==> R = {} ==> R' = {}"
by (induction rule: step_r.cases) (auto simp: region_set'_def)

lemma emptiness_preservance_steps: "A,R ⊨ ⟨l, R⟩ ↝* ⟨l',R'⟩ ==> R = {} ==> R' = {}"
 apply (induction rule: steps_r.induct)
  apply blast
 apply (subst emptiness_preservance)
by blast+

text ‹
 Note how it is important to define the multi-step semantics ``the right way round".
 This is also the direction Bouyer implies for her implicit induction.
 ›

lemma steps_r_sound:
  "A,R ⊨ ⟨l, R⟩ ↝* ⟨l', R'⟩ ==> R = {region X I r |I r. valid_region X k I r}
  ==> R' ≠ {} ==> u ∈ R ==> ∃ u' ∈ R'. A ⊨ ⟨l, u⟩ →* ⟨l', u'⟩"
proof (induction rule: steps_r.induct)
  case refl then show ?case by auto
next
  case (step A R l R l' R' l'' R'')
  from emptiness_preservance[OF step.hyps(2)] step.prems have "R' ≠ {}" by fastforce
  with step obtain u' where u': "u' ∈ R'" "A ⊨ ⟨l, u⟩ →* ⟨l',u'⟩" by auto
  with step_r_sound[OF step(2,4,5)] obtain u'' where "u'' ∈ R''" "A ⊨ ⟨l', u'⟩ → ⟨l'',u''⟩" by blast
  with u' show ?case by (auto 4 5 intro: steps_alt)
qed

lemma steps_r_sound':
  "A,R ⊨ ⟨l, R⟩ ↝* ⟨l', R'⟩ ==> R = {region X I r |I r. valid_region X k I r}
  ==> R' ≠ {} ==> (∃ u' ∈ R'. ∃ u ∈ R. A ⊨ ⟨l, u⟩ →* ⟨l', u'⟩)"
proof goal_cases
  case 1
  with emptiness_preservance_steps[OF this(1)] obtain u where "u ∈ R" by auto
  with steps_r_sound[OF 1 this] show ?case by auto
qed

lemma single_step_r:
  "A,R ⊨ ⟨l, R⟩ ↝ ⟨l', R'⟩ ==> A,R ⊨ ⟨l, R⟩ ↝* ⟨l', R'⟩"
by (metis steps_r.refl steps_r.step)

lemma steps_r_alt:
  "A,R ⊨ ⟨l', R'⟩ ↝* ⟨l'', R''⟩ ==> A,R ⊨ ⟨l, R⟩ ↝ ⟨l', R'⟩ ==> A,R ⊨ ⟨l, R⟩ ↝* ⟨l'', R''⟩"
 apply (induction rule: steps_r.induct)
  apply (rule single_step_r)
by auto

lemma single_step:
  "x1 ⊨ ⟨x2, x3⟩ → ⟨x4,x5⟩ ==> x1 ⊨ ⟨x2, x3⟩ →* ⟨x4,x5⟩"
by (metis steps.intros)

lemma steps_r_complete:
  "[A ⊨ ⟨l, u⟩ →* ⟨l',u'⟩; R = {region X I r |I r. valid_region X k I r}; valid_abstraction A X k;
    ∀ x ∈ X. u x ≥ 0] ==> ∃ R'. A,R ⊨ ⟨l, ([u]_\<R>)⟩ ↝* ⟨l',R'⟩ ∧ u' ∈ R'"
proof (induction rule: steps.induct)
  case (refl A l u)
  from region_cover'[OF refl(1,3)] show ?case by auto
next
  case (step A l u l' u' l'' u'')
  from step_r_complete[OF step(1,4-6)] obtain R' where R':
    "A,R ⊨ ⟨l, ([u]_\<R>)⟩ ↝ ⟨l',R'⟩" "u' ∈ R'" "R' ∈ R"
  by auto
  with step(4) ‹u' ∈ R'› have "∀x∈X. 0 ≤ u' x" by auto
  with step obtain R'' where R'': "A,R ⊨ ⟨l', ([u']_\<R>)⟩ ↝* ⟨l'',R''⟩" "u'' ∈ R''" by auto
  with region_unique[OF step(4) R'(2,3)] R'(1) have "A,R ⊨ ⟨l, ([u]_\<R>)⟩ ↝* ⟨l'',R''⟩"
  by (subst steps_r_alt) auto
  with R'' region_cover'[OF step(4,6)] show ?case by auto
qed

(*
section \<open>A Semantics Based on Regions\<close>

subsection \<open>Single step\<close>

inductive step_r ::
  "('a, 'c, t, 's) ta \<Rightarrow> ('c, t) zone set \<Rightarrow> 's \<Rightarrow> ('c, t) zone \<Rightarrow> 's \<Rightarrow> ('c, t) zone \<Rightarrow> bool"
("_,_ \<turnstile> \<langle>_, _\<rangle> \<leadsto> \<langle>_, _\<rangle>" [61,61,61,61] 61)
where
  step_r:
  "\<lbrakk>\<R> = {region X I r |I r. valid_region X k I r}; valid_abstraction A X k; A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l';
    R \<in> \<R>; R' \<in> Succ \<R> R; R' \<subseteq> \<lbrace>inv_of A l\<rbrace>
   \<rbrakk>
 \<Longrightarrow>
  A,\<R> \<turnstile> \<langle>l,R\<rangle> \<leadsto> \<langle>l', region_set' (R' \<inter> {u. u \<turnstile> g}) r 0 \<inter> {u. u \<turnstile> inv_of A l'}\<rangle>"

inductive_cases[elim!]: "A,\<R> \<turnstile> \<langle>l, u\<rangle> \<leadsto> \<langle>l', u'\<rangle>"

declare step_r.intros[intro]

lemma region_cover':
  assumes "\<R> = {region X I r |I r. valid_region X k I r}" and "\<forall>x\<in>X. 0 \<le> v x"
  shows "v \<in> [v]\<^sub>\<R>" "[v]\<^sub>\<R> \<in> \<R>"
proof -
  from region_cover[OF assms(2), of k] assms obtain R where R: "R \<in> \<R>" "v \<in> R" by auto
  from regions_closed'[OF assms(1) R, of 0] show "v \<in> [v]\<^sub>\<R>" unfolding cval_add_def by auto
  from regions_closed[OF assms(1) R, of 0] show "[v]\<^sub>\<R> \<in> \<R>" unfolding cval_add_def by auto
qed

lemma step_r_complete_aux:
  fixes R r A l' g
  defines "R' \<equiv> region_set' (R \<inter> {u. u \<turnstile> g}) r 0 \<inter> {u. u \<turnstile> inv_of A l'}"
  assumes "\<R> = {region X I r |I r. valid_region X k I r}"
    and "valid_abstraction A X k"
    and "u \<in> R"
    and "R \<in> \<R>"
    and "A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l'"
    and "u \<turnstile> g"
    and "[r\<rightarrow>0]u \<turnstile> inv_of A l'"
  shows "R = R \<inter> {u. u \<turnstile> g} \<and> R' = region_set' R r 0 \<and> R' \<in> \<R>"
proof -
  note A = assms(2-)
  from A(2) have *:
    "\<forall>(x, m)\<in>clkp_set A. m \<le> real (k x) \<and> x \<in> X \<and> m \<in> \<nat>"
    "collect_clkvt (trans_of A) \<subseteq> X"
    "finite X"
  by (fastforce elim: valid_abstraction.cases)+
  from A(5) *(2) have r: "set r \<subseteq> X" unfolding collect_clkvt_def by fastforce
  from *(1) A(5) have "\<forall>(x, m)\<in>collect_clock_pairs g. m \<le> real (k x) \<and> x \<in> X \<and> m \<in> \<nat>"
  unfolding clkp_set_def collect_clkt_def by fastforce
  from ccompatible[OF this, folded A(1)] A(3,4,6) have "R \<subseteq> \<lbrace>g\<rbrace>"
  unfolding ccompatible_def ccval_def by blast
  then have R_id: "R \<inter> {u. u \<turnstile> g} = R" unfolding ccval_def by auto
  from region_set'_id[OF A(4)[unfolded A(1)] A(3) *(3) _ _ r, of 0, folded A(1)]
  have **:
    "[[r\<rightarrow>0]u]\<^sub>\<R> = region_set' R r 0" "[[r\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>" "[r\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R>"
  by auto
  let ?R = "[[r\<rightarrow>0]u]\<^sub>\<R>"
  from *(1) A(5) have ***:
    "\<forall>(x, m) \<in> collect_clock_pairs (inv_of A l'). m \<le> real (k x) \<and> x \<in> X \<and> m \<in> \<nat>"
  unfolding inv_of_def clkp_set_def collect_clki_def by fastforce
  from ccompatible[OF this, folded A(1)] **(2-) A(7) have "?R \<subseteq> \<lbrace>inv_of A l'\<rbrace>"
  unfolding ccompatible_def ccval_def by blast
  then have ***: "?R \<inter> {u. u \<turnstile> inv_of A l'} = ?R" unfolding ccval_def by auto
  with **(1,2) R_id show ?thesis by (auto simp: R'_def)
qed

lemma step_r_complete:
  "\<lbrakk>A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow> \<langle>l',u'\<rangle>; \<R> = {region X I r |I r. valid_region X k I r}; valid_abstraction A X k;
    \<forall> x \<in> X. u x \<ge> 0\<rbrakk> \<Longrightarrow> \<exists> R'. A,\<R> \<turnstile> \<langle>l, ([u]\<^sub>\<R>)\<rangle> \<leadsto> \<langle>l',R'\<rangle> \<and> u' \<in> R' \<and> R' \<in> \<R>"
proof (induction rule: step'.induct)
  case prems: (step' A l u d l' u' a l'' u'')
  then have u': "u' = (u \<oplus> d)" "u \<oplus> d \<turnstile> inv_of A l" "0 \<le> d" and "l = l'" by auto
  from prems obtain g r where u'':
    "u'' = [r\<rightarrow>0]u'" "A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l''" "u' \<turnstile> g" "u'' \<turnstile> inv_of A l''"
    by atomize_elim (auto 4 4 elim: step_a.cases)
  from region_cover'[OF \<open>\<R> = _\<close> prems(5)] have R: "[u]\<^sub>\<R> \<in> \<R>" "u \<in> [u]\<^sub>\<R>" by auto
  from SuccI2[OF \<open>\<R> = _\<close> this(2,1) \<open>0 \<le> _\<close>, of "[u']\<^sub>\<R>"] \<open>u' = _\<close> have u'1:
    "[u']\<^sub>\<R> \<in> Succ \<R> ([u]\<^sub>\<R>)" "[u']\<^sub>\<R> \<in> \<R>"
    by auto
  from R(1,2) u'(1,3) have u'2: "[u']\<^sub>\<R> \<in> \<R>" "u' \<in> [u']\<^sub>\<R>"
    by (auto intro: regions_closed[OF \<open>\<R> = _\<close>] regions_closed'[OF \<open>\<R> = _\<close>])
  from prems(4) have *:
    "\<forall>(x, m)\<in>clkp_set A. m \<le> real (k x) \<and> x \<in> X \<and> m \<in> \<nat>"
    "collect_clkvt (trans_of A) \<subseteq> X"
    "finite X"
  by (fastforce elim: valid_abstraction.cases)+
  from *(1) u'(2) have
    "\<forall>(x, m)\<in>collect_clock_pairs (inv_of A l). m \<le> real (k x) \<and> x \<in> X \<and> m \<in> \<nat>"
    "\<forall>(x, m)\<in>collect_clock_pairs (inv_of A l''). m \<le> real (k x) \<and> x \<in> X \<and> m \<in> \<nat>"
  unfolding clkp_set_def collect_clki_def inv_of_def by fastforce+
  with u'2 u'(1,2) have
    "[u']\<^sub>\<R> \<subseteq> \<lbrace>inv_of A l\<rbrace>"
    by (auto 4 4 simp add: ccompatible_def ccval_def \<open>\<R> = _\<close>[symmetric] dest!: ccompatible)
  then have **: "([u']\<^sub>\<R>) \<inter> {u. u \<turnstile> inv_of A l} = ([u']\<^sub>\<R>)" by (auto simp: ccval_def)
  let ?R'= "region_set' (([u']\<^sub>\<R>) \<inter> {u. u \<turnstile> g}) r 0 \<inter> {u. u \<turnstile> inv_of A l''}"
  from step_r_complete_aux[OF \<open>\<R> = _\<close> prems(4) u'2(2,1) u''(2,3)] u''(1,4)
  have *: "([u']\<^sub>\<R>) \<inter> {u. u \<turnstile> g} = [u']\<^sub>\<R>" "?R' = region_set' ([u']\<^sub>\<R>) r 0" "?R' \<in> \<R>" by auto
  from prems(3,4) have "collect_clkvt (trans_of A) \<subseteq> X" "finite X"
    by (auto elim: valid_abstraction.cases)
  with u''(2) have r: "set r \<subseteq> X" unfolding collect_clkvt_def by fastforce
  from * \<open>u'' = _\<close> \<open>u' \<in> _\<close> have "u'' \<in> ?R'" unfolding region_set'_def by auto
  moreover from step_r[OF \<open>\<R> = _\<close> prems(4) u''(2) R(1) u'1(1) \<open>[u']\<^sub>\<R> \<subseteq> _\<close>] have
    "A,\<R> \<turnstile> \<langle>l, ([u]\<^sub>\<R>)\<rangle> \<leadsto> \<langle>l'', ?R'\<rangle>"
    by (simp add: ** )
  ultimately show ?case using \<open>?R' \<in> \<R>\<close> by (intro exI conjI; auto)
qed

text \<open>
  Compare this to lemma \<open>step_z_sound\<close>. This version is weaker because for regions we may very well
  arrive at a successor for which not every valuation can be reached by the predecessor.
  This is the case for e.g. the region with only Greater (k x) bounds.
\<close>

lemma step_r_sound:
  "A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto> \<langle>l',R'\<rangle> \<Longrightarrow> \<R> = {region X I r |I r. valid_region X k I r}
  \<Longrightarrow> R' \<noteq> {} \<Longrightarrow> (\<forall> u \<in> R. \<exists> u' \<in> R'. A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow> \<langle>l',u'\<rangle>)"
proof (induction rule: step_r.induct)
  case A: (step_r \<R> X k A l g a r l' R R')
  show ?case
  proof
    fix u assume u: "u \<in> R"
    from set_of_regions[OF A(4)[unfolded A(1)], folded A(1), OF  u A(5)] A(2)
    obtain t where t: "t \<ge> 0" "[u \<oplus> t]\<^sub>\<R> = R'" by (auto elim: valid_abstraction.cases)
    with regions_closed'[OF A(1,4) u] have *: "(u \<oplus> t) \<in> R'" by auto
    from A(6,8) obtain v where v: "v \<in> R'" "v \<turnstile> inv_of A l" "v \<turnstile> g" "[r\<rightarrow>0]v \<turnstile> inv_of A l'"
      unfolding region_set'_def ccval_def by auto
    let ?R' = "region_set' (R' \<inter> {u. u \<turnstile> g}) r 0 \<inter> {u. u \<turnstile> inv_of A l'}"
    from step_r_complete_aux[OF A(1,2) v(1) _ A(3)] \<open>R' \<in> _\<close> v have R:
      "R' = R' \<inter> {u. u \<turnstile> g}" "?R' = region_set' R' r 0"
      by auto
    from A have "collect_clkvt (trans_of A) \<subseteq> X" by (auto elim: valid_abstraction.cases)
    with A(3) have r: "set r \<subseteq> X" unfolding collect_clkvt_def by fastforce
    from * R A(6) have *:
      "u \<oplus> t \<turnstile> inv_of A l" "[r\<rightarrow>0](u \<oplus> t) \<in> ?R'" "(u \<oplus> t) \<turnstile> g" "[r\<rightarrow>0](u \<oplus> t) \<turnstile> inv_of A l'"
      unfolding region_set'_def ccval_def by auto
    with A(3) \<open>t \<ge> 0\<close> have "A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow> \<langle>l',[r\<rightarrow>0](u \<oplus> t)\<rangle>" by (auto intro: step_a.intros)
    with * show "\<exists>a\<in>?R'. A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow> \<langle>l',a\<rangle>" by meson
  qed
qed

subsection \<open>Multi Step\<close>

inductive
  steps_r :: "('a, 'c, t, 's) ta \<Rightarrow> ('c, t) zone set \<Rightarrow> 's \<Rightarrow> ('c, t) zone \<Rightarrow> 's \<Rightarrow> ('c, t) zone \<Rightarrow> bool"
("_,_ \<turnstile> \<langle>_, _\<rangle> \<leadsto>* \<langle>_, _\<rangle>" [61,61,61,61,61,61] 61)
where
  refl: "A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto>* \<langle>l, R\<rangle>" |
  step: "A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto>* \<langle>l', R'\<rangle> \<Longrightarrow> A,\<R> \<turnstile> \<langle>l', R'\<rangle> \<leadsto> \<langle>l'', R''\<rangle> \<Longrightarrow> A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto>* \<langle>l'', R''\<rangle>"

declare steps_r.intros[intro]

lemma steps_alt:
  "A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow>* \<langle>l',u'\<rangle> \<Longrightarrow> A \<turnstile>' \<langle>l', u'\<rangle> \<rightarrow> \<langle>l'',u''\<rangle> \<Longrightarrow> A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow>* \<langle>l'',u''\<rangle>"
by (induction rule: steps'.induct) auto

lemma emptiness_preservation: "A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto> \<langle>l',R'\<rangle> \<Longrightarrow> R = {} \<Longrightarrow> R' = {}"
by (induction rule: step_r.cases) (auto simp: region_set'_def)

lemma emptiness_preservation_steps: "A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto>* \<langle>l',R'\<rangle> \<Longrightarrow> R = {} \<Longrightarrow> R' = {}"
 apply (induction rule: steps_r.induct)
  apply blast
 apply (subst emptiness_preservation)
by blast+

text \<open>
  Note how it is important to define the multi-step semantics "the right way round".
  This also the direction Bouyer implies for her implicit induction.
\<close>

lemma steps_r_sound:
  "A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto>* \<langle>l', R'\<rangle> \<Longrightarrow> \<R> = {region X I r |I r. valid_region X k I r}
  \<Longrightarrow> R' \<noteq> {} \<Longrightarrow> u \<in> R \<Longrightarrow> \<exists> u' \<in> R'. A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow>* \<langle>l', u'\<rangle>"
proof (induction rule: steps_r.induct)
  case refl then show ?case by auto
next
  case (step A \<R> l R l' R' l'' R'')
  from emptiness_preservation[OF step.hyps(2)] step.prems have "R' \<noteq> {}" by fastforce
  with step obtain u' where u': "u' \<in> R'" "A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow>* \<langle>l',u'\<rangle>" by auto
  with step_r_sound[OF step(2,4,5)] obtain u'' where "u'' \<in> R''" "A \<turnstile>' \<langle>l', u'\<rangle> \<rightarrow> \<langle>l'',u''\<rangle>" by blast
  with u' show ?case by - (rule bexI[where x = u'']; blast intro: steps_alt)
qed

lemma steps_r_sound':
  "A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto>* \<langle>l', R'\<rangle> \<Longrightarrow> \<R> = {region X I r |I r. valid_region X k I r}
  \<Longrightarrow> R' \<noteq> {} \<Longrightarrow> (\<exists> u' \<in> R'. \<exists> u \<in> R.  A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow>* \<langle>l', u'\<rangle>)"
proof goal_cases
  case 1
  with emptiness_preservation_steps[OF this(1)] obtain u where "u \<in> R" by auto
  with steps_r_sound[OF 1 this] show ?case by auto
qed

lemma single_step_r:
  "A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto> \<langle>l', R'\<rangle> \<Longrightarrow> A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto>* \<langle>l', R'\<rangle>"
by (metis steps_r.refl steps_r.step)

lemma steps_r_alt:
  "A,\<R> \<turnstile> \<langle>l', R'\<rangle> \<leadsto>* \<langle>l'', R''\<rangle> \<Longrightarrow> A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto> \<langle>l', R'\<rangle> \<Longrightarrow> A,\<R> \<turnstile> \<langle>l, R\<rangle> \<leadsto>* \<langle>l'', R''\<rangle>"
 apply (induction rule: steps_r.induct)
  apply (rule single_step_r)
by auto

lemma steps_r_complete:
  "\<lbrakk>A \<turnstile>' \<langle>l, u\<rangle> \<rightarrow>* \<langle>l',u'\<rangle>; \<R> = {region X I r |I r. valid_region X k I r}; valid_abstraction A X k;
    \<forall> x \<in> X. u x \<ge> 0\<rbrakk> \<Longrightarrow> \<exists> R'. A,\<R> \<turnstile> \<langle>l, ([u]\<^sub>\<R>)\<rangle> \<leadsto>* \<langle>l',R'\<rangle> \<and> u' \<in> R'"
proof (induction rule: steps'.induct)
  case (refl' A l u)
  from region_cover'[OF refl'(1,3)] show ?case by auto
next
  case (step' A l u l' u' l'' u'')
  from step_r_complete[OF step'(1,4-6)] obtain R' where R':
    "A,\<R> \<turnstile> \<langle>l, ([u]\<^sub>\<R>)\<rangle> \<leadsto> \<langle>l',R'\<rangle>" "u' \<in> R'" "R' \<in> \<R>"
    by auto
  from R'(2,3) step'(4) have "\<forall>x\<in>X. 0 \<le> u' x" by auto
  with step' obtain R'' where R'': "A,\<R> \<turnstile> \<langle>l', ([u']\<^sub>\<R>)\<rangle> \<leadsto>* \<langle>l'',R''\<rangle>" "u'' \<in> R''" by auto
  with region_unique[OF step'(4) R'(2,3)] R'(1) have "A,\<R> \<turnstile> \<langle>l, ([u]\<^sub>\<R>)\<rangle> \<leadsto>* \<langle>l'',R''\<rangle>"
  by (subst steps_r_alt) auto
  with R'' region_cover'[OF step'(4,6)] show ?case by auto
qed

  *)

end