Theory Timed_Automata.Regions

```chapter ‹The Classic Construction for Decidability›

theory Regions
imports Timed_Automata 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

instantiation real :: time
begin
instance proof
fix x y :: real assume "x < y"
then show "∃ z > x. z < y" using Rats_cases using dense_order_class.dense by blast
next
have "(1:: real) ≠ 0" by auto
then show "∃x. (x::real) ≠ 0" by blast
qed
end

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

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

abbreviation "total_preorder r ≡ refl r ∧ trans r"

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

inductive_set region for X I r
where
"∀ x ∈ X. u x ≥ 0 ⟹ ∀ x ∈ X. intv_elem x u (I x) ⟹ X⇩0 = {x ∈ X. ∃ d. I x = Intv d} ⟹
∀ x ∈ X⇩0. ∀ y ∈ X⇩0. (x, y) ∈ r ⟷ frac (u x) ≤ frac (u y)
⟹ u ∈ region X I r"

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

definition part ("[_]⇩_" [61,61] 61) where "part v ℛ ≡ THE R. R ∈ ℛ ∧ v ∈ R"

inductive_set Succ for ℛ R where
"u ∈ R ⟹ R ∈ ℛ ⟹ R' ∈ ℛ ⟹ t ≥ 0 ⟹ R' = [u ⊕ t]⇩ℛ ⟹ R' ∈ Succ ℛ R"

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

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

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

declare Succ.cases[elim]

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

section ‹Basic Properties›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

section ‹Set of Regions›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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