Theory Timed_Automata.Regions

chapter ‹The Classic Construction for Decidability›

theory Regions
imports Timed_Automata TA_Misc
begin

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

section ‹Definition of Regions›

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

datatype intv =
  Const nat |
  Intv nat |
  Greater nat

type_synonym t = real


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

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

abbreviation "total_preorder r  refl r  trans r"

inductive valid_region :: "'c set  ('c  nat)  ('c  intv)  'c rel  bool"
where
  "X0 = {x  X.  d. I x = Intv d}; refl_on X0 r; trans r; total_on X0 r;  x  X. valid_intv (k x) (I x)
   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)  X0 = {x  X.  d. I x = Intv d} 
    x  X0.  y  X0. (x, y)  r  frac (u x)  frac (u y)
   u  region X I r"

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

definition part ([_]⇩_› [61,61] 61) where "part v   THE R. R    v  R"

inductive_set Succ for  R where
  "u  R  R    R'    t  0  R' = [u  t]⇩  R'  Succ  R"

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

inductive_cases[elim!]: "intv_elem x u (Const d)"
inductive_cases[elim!]: "intv_elem x u (Intv d)"
inductive_cases[elim!]: "intv_elem x u (Greater d)"
inductive_cases[elim!]: "valid_intv c (Greater d)"
inductive_cases[elim!]: "valid_intv c (Const d)"
inductive_cases[elim!]: "valid_intv c (Intv d)"

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

declare Succ.cases[elim]

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

section ‹Basic Properties›

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

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

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

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

lemma ℛ_regions_distinct:
  " = {region X I r | I r. valid_region X k I r}; R  ; v  R; R'  ; R  R'  v  R'"
using valid_regions_distinct by blast

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

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

lemma region_cover:
  " x  X. u x  0   R. R  {region X I r | I r. valid_region X k I r}  u  R"
proof (standard, standard)
  assume assm: " x  X. 0  u x"
  let ?I = "λ x. intv_of (k x) (u x)"
  let ?X0 = "{x  X.  d. ?I x = Intv d}"
  let ?r = "{(x,y). x  ?X0  y  ?X0  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 ?X0 = "{x  X. d. I x = Intv d}"
  obtain f :: "'a  nat" where f:
    "x?X0. y?X0. f x  f y  (x, y)  r"
     apply (rule finite_total_preorder_enumeration)
         apply (subgoal_tac "finite ?X0")
          apply assumption
  using assms by auto
  let ?M = "if ?X0  {} then Max {f x | x. x  ?X0} else 1"
  let ?f = "λ x. (f x + 1) / (?M + 2)"
  let ?v = "λ x. get_intv_val (I x) (if x  ?X0 then ?f x else 1)"
  have frac_intv: "x?X0. 0 < ?f x  ?f x < 1"
  proof (standard, goal_cases)
    case (1 x)
    then have *: "?X0  {}" by auto
    have "f x  Max {f x | x. x  ?X0}" apply (rule Max_ge) using finite X 1 by auto
    with 1 show ?case by auto
  qed
  with region_not_empty_aux have *:
    "x?X0. y?X0. frac (?v x)  frac (?v y)  ?f x  ?f y"
  by force
  have "x?X0. y?X0. ?f x  ?f y  f x  f y" by (simp add: divide_le_cancel)+
  with f have "x?X0. y?X0. ?f x  ?f y  (x, y)  r" by auto
  with * have frac_order: "x?X0. y?X0. frac (?v x)  frac (?v y)  (x, y)  r" by auto
  have "?v  region X I r"
  proof standard
    show "xX. intv_elem x ?v (I x)"
    proof (standard, case_tac "I x", goal_cases)
      case (2 x d)
      then have *: "x  ?X0" 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 "xX. 0  get_intv_val (I x) (if x  ?X0 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?X0. y?X0. ((x, y)  r) = (frac (?v x)  frac (?v y))" by blast
  qed
  then show ?thesis by auto
qed

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

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

lemma region_unique:
  " = {region X I r | I r. valid_region X k I r}  u  R  R    [u]⇩ = R"
proof (goal_cases)
  case 1
  note A = this
  from A obtain I r where *: "valid_region X k I r" "R = region X I r" "u  region X I r" by auto
  from this(3) have "xX. 0  u x" by auto
  from theI'[OF regions_partition[OF A(1) this]] A(1) obtain I' r' where
    v: "valid_region X k I' r'" "[u]⇩ = region X I' r'" "u  region X I' r'"
  unfolding part_def by auto
  from valid_regions_distinct[OF *(1) v(1) *(3) v(3)] v(2) *(2) show ?case by auto
qed

lemma regions_partition':
  " = {region X I r | I r. valid_region X k I r}  xX. 0  v x  xX. 0  v' x  v'  [v]⇩
   [v']⇩ = [v]⇩"
proof (goal_cases)
  case 1
  note A = this
  from theI'[OF regions_partition[OF A(1,2)]] A(1,4) obtain I r where
    v: "valid_region X k I r" "[v]⇩ = region X I r" "v'  region X I r"
  unfolding part_def by auto
  from theI'[OF regions_partition[OF A(1,3)]] A(1) obtain I' r' where
    v': "valid_region X k I' r'" "[v']⇩ = region X I' r'" "v'  region X I' r'"
  unfolding part_def by auto
  from valid_regions_distinct[OF v'(1) v(1) v'(3) v(3)] v(2) v'(2) show ?case by simp
qed

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

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

lemma valid_regions_I_cong:
  "valid_region X k I r   x  X. I x = I' x  region X I r = region X I' r  valid_region X k I' r"
proof (safe, goal_cases)
  case (1 v)
  note A = this
  then have [simp]:" x. x  X  I' x = I x" by metis
  show ?case
  proof (standard, goal_cases)
    case 1
    from A(3) show ?case by auto
  next
    case 2
    from A(3) show ?case by auto
  next
    case 3
    show "{x  X. d. I x = Intv d} = {x  X. d. I' x = Intv d}" by auto
  next
    case 4
    let ?X0 = "{x  X. d. I x = Intv d}"
    from A(3) show " x  ?X0.  y  ?X0. ((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 ?X0 = "{x  X. d. I' x = Intv d}"
    from A(3) show " x  ?X0.  y  ?X0. ((x, y)  r) = (frac (v x)  frac (v y))" by auto
  qed
next
  case 3
  note A = this
  then have [simp]:" x. x  X  I' x = I x" by metis
  show ?case
   apply rule
       apply (subgoal_tac "{x  X. d. I x = Intv d} = {x  X. d. I' x = Intv d}")
        apply assumption
  using A by auto
qed

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

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

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


section ‹Set of Regions›

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

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

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

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

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

definition
  "succ  R =
  (SOME R'. R'  Succ  R  ( u  R.  t  0. (u  t)  R  ( t'  t. (u  t')  R'  0  t')))"

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

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

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

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

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

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

lemma closest_prestable_1:
  fixes I X k r
  defines "  {region X I r |I r. valid_region X k I r}"
  defines "R  region X I r"
  defines "Z  {x  X .  c. I x = Const c}"
  assumes "Z  {}"
  defines "I' λ x. if x  Z then I x else if intv_const (I x) = k x then Greater (k x) else Intv (intv_const (I x))"
  defines "r'  r  {(x,y) . x  Z  y  X  intv_const (I x) < k x  isIntv (I' y)}"
  assumes "finite X"
  assumes "valid_region X k I r"
  shows   " v  R.  t>0. t't. (v  t')  region X I' r'  t'  0"
  and     " v  region X I' r'.  t0. (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 ?X0' = "{x  X. d. I' x = Intv d}"
    show "x?X0'. y?X0'. ((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 ?X0  = "{x  X. d. I x = Intv d}"
        let ?X0' = "{x  X. d. I' x = Intv d}"
        show "x?X0'. y?X0'. ((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  ?X0" "y  ?X0" 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  ?X0" by auto
                moreover from assms(8) have "refl_on ?X0 r" by auto
                ultimately show ?case unfolding refl_on_def using 1 by auto
              next
                case 2
                with F show ?case by simp
              qed
            qed
          next
            case True
            with elem have **: "frac (v x) = 0" unfolding Z_def by force
            from B(4) have "y  Z  I y = Intv d'" unfolding I'_def by presburger
            then show ?thesis
            proof
              assume "y  Z"
              with elem[OF B(3)] have ***: "frac (v y) = 0" unfolding Z_def by force
              show ?thesis by (simp add: ** *** frac_add cval_add_def)
            next
              assume A: "I y = Intv d'"
              with B(3) have "y  ?X0" by auto
              with frac_bound have "t < 1 - frac (v y)" by fastforce+
              moreover from ** ?t < 1 have "?t / 2 < 1 - frac (v x)" by linarith
              ultimately have
                "frac (v x) + t = frac (v x + t)" "frac (v y) + t = frac (v y + t)"
              using frac_distr t by simp+
              moreover have "frac (v x) <= frac (v y)" by (simp add: **)
              ultimately show ?thesis unfolding cval_add_def by fastforce
            qed
          qed
        next
          case B: (2 x y d d')
          show ?case
          proof (cases "x  Z", goal_cases)
            case True
            with B(1,2) have "intv_const (I x)  k x" unfolding I'_def by auto
            with B(1) assms(8) have "intv_const (I x) < k x" by (fastforce elim!: valid_intv.cases)
            with B True show ?thesis unfolding r'_def by auto
          next
            case (False)
            with B(1,2) have x_intv: "isIntv (I x)" unfolding Z_def I'_def by auto
            show ?thesis
            proof (cases "y  Z")
              case False
              with B(3,4) have y_intv: "isIntv (I y)" unfolding Z_def I'_def by auto
              with frac_bound x_intv B(1,3) have "t < 1 - frac (v x)" "t < 1 - frac (v y)" by auto
              from frac_add_leD[OF _ this] B(5) t have
                "frac (v x)  frac (v y)"
              by (auto simp: cval_add_def)
              with v assms(2) B(1,3) x_intv y_intv have "(x, y)  r" by (auto )
              then show ?thesis by (simp add: r'_def)
            next
              case True
              from frac_bound x_intv B(1) have b: "t < 1 - frac (v x)" by auto
              from x_intv obtain c where "I x = Intv c" by auto
              with elem[OF x  X] have v: "c < v x" "v x < c + 1" by auto
              from True elem[OF y  X] have *: "frac (v y) = 0" unfolding Z_def by auto
              with t ?t < 1 floor_frac_add_preservation'[of t "v y"] have
                "floor (v y + t) = floor (v y)"
              by auto
              then have "frac (v y + t) = t"
              by (metis * add_diff_cancel_left' diff_add_cancel diff_self frac_def)
              moreover from nat_intv_frac_gt0[OF v] have "0 < frac (v x)" .
              moreover from frac_distr[OF _ b] t have "frac (v x + t) = frac (v x) + t" by auto
              ultimately show ?thesis using B(5) unfolding cval_add_def by auto
            qed
          qed
        qed
      qed
    }
    with ?t/2 > 0 have "0 < ?t/2  ( t. 0 < t  t  ?t/2  (v  t)  region X I' r')" by auto
  } note ** = this
  show "t't. (v  t')  region X I' r'  0  t'"
  proof (cases " x  X. isIntv (I x)")
    case True
    note T = this
    show ?thesis
    proof (cases "t  ?t/2")
      case True with T t ** show ?thesis by auto
    next
      case False
      then have "?t/2  t" by auto
      moreover from T ** have "(v  ?t/2)  region X I' r'" "?t/2 > 0" by auto
      ultimately show ?thesis by (fastforce del: region.cases)
    qed
  next
    case False
    note F = this
    show ?thesis
    proof (cases "t < 1")
      case True with F t * show ?thesis by auto
    next
      case False
      then have "0.5  t" by auto
      moreover from F * have "(v  0.5)  region X I' r'" by auto
      ultimately show ?thesis by (fastforce del: region.cases)
    qed
  qed
next
  fix v t assume A: "v  region X I' r'" "0  t" "(v  t)  R"
  from assms(3,4) obtain x c where x: "I x = Const c" "x  Z" "x  X" by auto
  with A(1) have "intv_elem x v (I' x)" by auto
  with x have "v x > c" unfolding I'_def
    apply (auto elim: intv_elem.cases)
    apply (cases "c = k x")
  by auto
  moreover from A(3) x(1,3) have "v x + t = c"
  by (fastforce elim!: intv_elem.cases simp: cval_add_def R_def)
  ultimately show False using A(2) by auto
next
  fix x c assume "x  X" "I' x = Const c"
  then show False
    apply (auto simp: I'_def Z_def)
    apply (cases "c. I x  Const c")
     apply auto
    apply (rename_tac c')
    apply (case_tac "c' = k x")
  by auto
next
  case (4 v t t' x c)
  note A = this
  then have "I' x = Intv c" unfolding I'_def Z_def by auto
  moreover from A have "real (c + 1)  (v  t') x + (t - t')" unfolding cval_add_def by auto
  ultimately show ?case by blast
next
  case A: (5 v t t' x c)
  show ?case
  proof (cases "x  Z")
    case False
    with A have "I x = Intv c" unfolding I'_def by auto
    with A show ?thesis unfolding cval_add_def by auto
  next
    case True
    with A(6) have "I x = Const c"
      apply (auto simp: I'_def)
      apply (cases "intv_const (I x) = k x")
    by (auto simp: Z_def)
    with A(1,5) R_def have "v x = c" by fastforce
    with A(2,7) show ?thesis by (auto simp: cval_add_def)
  qed
qed

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

lemma closest_prestable_2:
  fixes I X k r
  defines "  {region X I r |I r. valid_region X k I r}"
  defines "R  region X I r"
  assumes " x  X. ¬ isConst (I x)"
  defines "X0  {x  X. isIntv (I x)}"
  defines "M  {x  X0.  y  X0. (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.  t0. (v  t)  R  (t't. (v  t')  region X I' r'  t'  0)"
  and     " v  region X I' r'.  t0. (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  X0" unfolding M_def X0_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} = X0" unfolding X0_def by auto
  with *(2) have total: "total_on X0 r" by auto
  { fix y assume y: "y  M" "y  X0"
    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  X0" 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  X0"
    with M_max have "¬ (x, y)  r" "(y, x)  r" by auto
    with v[unfolded R_def] X0_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  X0"
    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] X0_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  X0" unfolding X0_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  X0" 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] X0_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: X0_def)
            with elem T(1) have "c < v y" "v y < c + 1" by (fastforce simp: X0_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 "X0 = {x  X. d. I x = Intv d}" by (auto simp add: X0_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 "yX0. zX0. ((y, z)  r) = (frac ((v  t)y)  frac ((v  t) z))"
      proof (auto simp: X0_def, goal_cases)
        case (1 y z d d')
        note A = this
        from A have [simp]: "y  X0" "z  X0" unfolding X0_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  X0" "z  X0" unfolding X0_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