Theory Timed_Automata.Regions_Beta

```theory Regions_Beta
imports Misc DBM_Normalization DBM_Operations
begin

chapter ‹Refinement to ‹β›-regions›

section ‹Definition›

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

datatype intv =
Const nat |
Intv nat |
Greater nat

datatype intv' =
Const' int |
Intv' int |
Greater' int |
Smaller' int

type_synonym t = real

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

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

inductive valid_intv' :: "int ⇒ int ⇒ intv' ⇒ bool"
where
"valid_intv' l _ (Smaller' (-l))" |
"-l ≤ d ⟹ d ≤ u ⟹ valid_intv' l u (Const' d)" |
"-l ≤ d ⟹ d < u  ⟹ valid_intv' l u (Intv' d)" |
"valid_intv' _ u (Greater' u)"

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

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

abbreviation "total_preorder r ≡ refl r ∧ trans r"

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

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

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

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

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

inductive valid_region :: "'c set ⇒ ('c ⇒ nat) ⇒ ('c ⇒ intv) ⇒ ('c ⇒ 'c ⇒ intv') ⇒ 'c rel ⇒ bool"
where
"⟦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);
∀ x ∈ X. ∀ y ∈ X. isGreater (I x) ∨ isGreater (I y) ⟶ valid_intv' (k y) (k x) (J x y)⟧
⟹ valid_region X k I J r"

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

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

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

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

inductive_cases[elim!]: "intv_elem x u (Const d)"
inductive_cases[elim!]: "intv_elem x u (Intv d)"
inductive_cases[elim!]: "intv_elem x u (Greater d)"
inductive_cases[elim!]: "valid_intv c (Greater d)"
inductive_cases[elim!]: "valid_intv c (Const d)"
inductive_cases[elim!]: "valid_intv c (Intv d)"
inductive_cases[elim!]: "intv'_elem x y u (Const' d)"
inductive_cases[elim!]: "intv'_elem x y u (Intv' d)"
inductive_cases[elim!]: "intv'_elem x y u (Greater' d)"
inductive_cases[elim!]: "intv'_elem x y u (Smaller' d)"
inductive_cases[elim!]: "valid_intv' l u (Greater' d)"
inductive_cases[elim!]: "valid_intv' l u (Smaller' d)"
inductive_cases[elim!]: "valid_intv' l u (Const' d)"
inductive_cases[elim!]: "valid_intv' l u (Intv' d)"

declare valid_intv.intros[intro]
declare valid_intv'.intros[intro]
declare intv_elem.intros[intro]
declare intv'_elem.intros[intro]

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

section ‹Basic Properties›

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

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

lemma valid_intv'_distinct:
"-c ≤ d ⟹ valid_intv' c d I ⟹ valid_intv' c d I' ⟹ intv'_elem x y u I ⟹ intv'_elem x y u I'
⟹ I = I'"
by (cases I) (cases I', auto)+

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

lemma valid_regions_distinct:
"valid_region X k I J r ⟹ valid_region X k I' J' r' ⟹ v ∈ region X I J r ⟹ v ∈ region X I' J' r'
⟹ region X I J r = region X I' J' r'"
proof goal_cases
case 1
note A = 1
{ fix x assume x: "x ∈ X"
with A(1) have "valid_intv (k x) (I x)" by auto
moreover from A(2) x have "valid_intv (k x) (I' x)" by auto
moreover from A(3) x have "intv_elem x v (I x)" by auto
moreover from A(4) x have "intv_elem x v (I' x)" by auto
ultimately have "I x = I' x" using valid_intv_distinct by fastforce
} note * = this
{ fix x y assume x: "x ∈ X" and y: "y ∈ X" and B: "isGreater (I x) ∨ isGreater (I y)"
with * have C: "isGreater (I' x) ∨ isGreater (I' y)" by auto
from A(1) x y B have "valid_intv' (k y) (k x) (J x y)" by fastforce
moreover from A(2) x y C have "valid_intv' (k y) (k x) (J' x y)" by fastforce
moreover from A(3) x y B have "intv'_elem x y v (J x y)" by force
moreover from A(4) x y C have "intv'_elem x y v (J' x y)" by force
moreover from x y valid_intv'_distinct have "- int (k y) ≤ int (k x)" by simp
ultimately have "J x y = J' x y" by (blast intro: valid_intv'_distinct)
} note ** = this
from A show ?thesis
proof (auto, goal_cases)
case (1 u)
note A = this
{ fix x assume x: "x ∈ X"
from A(5) x have "intv_elem x u (I x)" by auto
with * x have "intv_elem x u (I' x)" by auto
}
then have "∀ x ∈ X. intv_elem x u (I' x)" by auto
note B = this
{ fix x y assume x: "x ∈ X" and y: "y ∈ X" and B: "isGreater (I' x) ∨ isGreater (I' y)"
with * have "isGreater (I x) ∨ isGreater (I y)" by auto
with x y A(5) have "intv'_elem x y u (J x y)" by force
with **[OF x y ‹isGreater (I x) ∨ _›] have "intv'_elem x y u (J' x y)" by simp
} note C = this
let ?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 _ *] C show ?case by auto
next
case (2 u)
note A = this
{ fix x assume x: "x ∈ X"
from A(5) x have "intv_elem x u (I' x)" by auto
with * x have "intv_elem x u (I x)" by auto
}
then have "∀ x ∈ X. intv_elem x u (I x)" by auto
note B = this
{ fix x y assume x: "x ∈ X" and y: "y ∈ X" and B: "isGreater (I x) ∨ isGreater (I y)"
with * have "isGreater (I' x) ∨ isGreater (I' y)" by auto
with x y A(5) have "intv'_elem x y u (J' x y)" by force
with **[OF x y ‹isGreater (I x) ∨ _›] have "intv'_elem x y u (J x y)" by simp
} note C = this
let ?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 _ *] C show ?case by auto
qed
qed

locale Beta_Regions =
fixes X k ℛ and V :: "('c, t) cval set"
defines "ℛ ≡ {region X I J r | I J r. valid_region X k I J r}"
defines "V ≡ {v . ∀ x ∈ X. v x ≥ 0}"
assumes finite: "finite X"
assumes non_empty: "X ≠ {}"
begin

lemma ℛ_regions_distinct:
"⟦R ∈ ℛ; v ∈ R; R' ∈ ℛ; R ≠ R'⟧ ⟹ v ∉ R'"
unfolding ℛ_def using valid_regions_distinct by blast

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

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

definition intv'_of :: "int ⇒ int ⇒ t ⇒ intv'" where
"intv'_of l u v ≡
if (v > u) then Greater' u
else if (v < l) then Smaller' l
else if (∃ x :: int. x = v) then (Const' (floor v))
else (Intv' (floor v))"

lemma region_cover:
"∀ x ∈ X. v x ≥ 0 ⟹ ∃ R. R ∈ ℛ ∧ v ∈ R"
proof (standard, standard)
assume assm: "∀ x ∈ X. 0 ≤ v x"
let ?I = "λ x. intv_of (k x) (v x)"
let ?J = "λ x y. intv'_of (-k y) (k x) (v x - v y)"
let ?X⇩0 = "{x ∈ X. ∃ d. ?I x = Intv d}"
let ?r = "{(x,y). x ∈ ?X⇩0 ∧ y ∈ ?X⇩0 ∧ frac (v x) ≤ frac (v y)}"
{ fix x y d assume A: "x ∈ X" "y ∈ X"
then have "intv'_elem x y v (intv'_of (- int (k y)) (int (k x)) (v x - v y))" unfolding intv'_of_def
proof (auto, goal_cases)
case (1 a)
then have "⌊v x - v y⌋ = v x - v y" by (metis of_int_floor_cancel)
then show ?case by auto
next
case 2
then have "⌊v x - v y⌋ < v x - v y" by (meson eq_iff floor_eq_iff not_less)
with 2 show ?case by auto
qed
} note intro = this
show "v ∈ region X ?I ?J ?r"
proof (standard, auto simp: assm intro: intro, goal_cases)
case (1 x)
thus ?case unfolding intv_of_def
proof (auto, goal_cases)
case (1 a)
note A = this
from A(2) have "⌊v x⌋ = v x" by (metis floor_of_int of_int_of_nat_eq)
with assm A(1) have "v x = real (nat ⌊v x⌋)" by auto
then show ?case by auto
next
case 2
note A = this
from A(1,2) have "real (nat ⌊v x⌋) < v x"
proof -
have f1: "0 ≤ v x"
using assm 1 by blast
have "v x ≠ real_of_int (int (nat ⌊v x⌋))"
by (metis (no_types) 2(2) of_int_of_nat_eq)
then show ?thesis
using f1 by linarith
qed
moreover from assm have "v x < real (nat (⌊v x⌋) + 1)" by linarith
ultimately show ?case by auto
qed
qed
{ fix x y assume "x ∈ X" "y ∈ X"
then have "valid_intv' (int (k y)) (int (k x)) (intv'_of (- int (k y)) (int (k x)) (v x - v y))"
unfolding intv'_of_def
apply auto
apply (metis floor_of_int le_floor_iff linorder_not_less of_int_minus of_int_of_nat_eq valid_intv'.simps)
by (metis floor_less_iff less_eq_real_def not_less of_int_minus of_int_of_nat_eq valid_intv'.intros(3))
}
moreover
{ fix x assume x: "x ∈ X"
then have "valid_intv (k x) (intv_of (k x) (v x))"
proof (auto simp: intv_of_def, goal_cases)
case (1 a)
then show ?case
by (intro valid_intv.intros(1)) (auto, linarith)
next
case 2
then show ?case
apply (intro valid_intv.intros(2))
using assm floor_less_iff nat_less_iff by fastforce+
qed
}
ultimately have "valid_region X k ?I ?J ?r"
by (intro valid_region.intros, auto simp: refl_on_def trans_def total_on_def)
then show "region X ?I ?J ?r ∈ ℛ" unfolding ℛ_def by auto
qed

lemma region_cover_V: "v ∈ V ⟹ ∃ R. R ∈ ℛ ∧ v ∈ R" using region_cover unfolding V_def by simp

text ‹
Note that we cannot show that every region is non-empty anymore.
The problem are regions fixing differences between an 'infeasible' constant.
›

text ‹
We can show that there is always exactly one region a valid valuation belongs to.
Note that we do not need non-emptiness for that.
›
lemma regions_partition:
"∀x ∈ X. 0 ≤ v x ⟹ ∃! R ∈ ℛ. v ∈ R"
proof goal_cases
case 1
note A = this
with region_cover[OF ] obtain R where R: "R ∈ ℛ ∧ v ∈ R" by fastforce
moreover
{ fix R' assume "R' ∈ ℛ ∧ v ∈ R'"
with R valid_regions_distinct[OF _ _ _ _] have "R' = R" unfolding ℛ_def by blast
}
ultimately show ?thesis by auto
qed

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

lemma regions_partition':
"∀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)]] A(3) obtain I J r where
v: "valid_region X k I J r" "[v]⇩ℛ = region X I J r" "v' ∈ region X I J r"
unfolding part_def ℛ_def by blast
from theI'[OF regions_partition[OF A(2)]] obtain I' J' r' where
v': "valid_region X k I' J' r'" "[v']⇩ℛ = region X I' J' r'" "v' ∈ region X I' J' r'"
unfolding part_def ℛ_def by auto
from valid_regions_distinct[OF v'(1) v(1) v'(3) v(3)] v(2) v'(2) show ?case by simp
qed

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

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

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

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

fun intv'_const :: "intv' ⇒ int"
where
"intv'_const (Smaller' d) = d" |
"intv'_const (Const' d) = d" |
"intv'_const (Intv' d) = d"  |
"intv'_const (Greater' d) = d"

lemma finite_ℛ_aux:
fixes P A B assumes "finite {x. A x}" "finite {x. B x}"
shows "finite {(I, J) | I J. P I J r ∧ A I ∧ B J}"
using assms by (fastforce intro: pairwise_finiteI finite_ex_and1 finite_ex_and2)

lemma finite_ℛ:
shows "finite ℛ"
proof -
{ fix I J r assume A: "valid_region X k I J 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 J. valid_region X k I J r} ⊆ Pow (X × X)" by auto
from finite_subset[OF this] finite have fin: "finite {r. ∃I J. valid_region X k I J r}" by auto
let ?u = "Max {k x | x. x ∈ X}"
let ?l = "- Max {k x | x. x ∈ X}"
let ?I = "{intv. intv_const intv ≤ ?u}"
let ?J = "{intv. ?l ≤ intv'_const intv ∧ intv'_const intv ≤ ?u}"
let ?S = "{r. ∃I J. valid_region X k I J r}"
let ?fin_mapI = "λ I. ∀x. (x ∈ X ⟶ I x ∈ ?I) ∧ (x ∉ X ⟶ I x = Const 0)"
let ?fin_mapJ = "λ J. ∀x. ∀y. (x ∈ X ∧ y ∈ X ⟶ J x y ∈ ?J)
∧ (x ∉ X ⟶ J x y = Const' 0) ∧ (y ∉ X ⟶ J x y = Const' 0)"
let ?ℛ = "{region X I J r | I J r. valid_region X k I J r ∧ ?fin_mapI I ∧ ?fin_mapJ J}"
let ?f = "λr. {region X I J r | I J . valid_region X k I J r ∧ ?fin_mapI I ∧ ?fin_mapJ J}"
let ?g = "λr. {(I, J) | I J . valid_region X k I J r ∧ ?fin_mapI I ∧ ?fin_mapJ J}"
have "?I = (Const ` {d. d ≤ ?u}) ∪ (Intv ` {d. d ≤ ?u}) ∪ (Greater ` {d. d ≤ ?u})"
by auto (case_tac x, auto)
then have "finite ?I" by auto
from finite_set_of_finite_funs[OF ‹finite X› this] have finI: "finite {I. ?fin_mapI I}" .
have "?J = (Smaller' ` {d. ?l ≤ d ∧ d ≤ ?u}) ∪ (Const' ` {d. ?l ≤ d ∧ d ≤ ?u})
∪ (Intv' ` {d. ?l ≤ d ∧ d ≤ ?u}) ∪ (Greater' ` {d. ?l ≤ d ∧ d ≤ ?u})"
by auto (case_tac x, auto)
then have "finite ?J" by auto
from finite_set_of_finite_funs2[OF ‹finite X› ‹finite X› this] have finJ: "finite {J. ?fin_mapJ J}" .
from finite_ℛ_aux[OF finI finJ, of "valid_region X k"] have "∀r ∈ ?S. finite (?g r)" by simp
moreover have "∀ r ∈ ?S. ?f r = (λ (I, J). region X I J r) ` ?g r" by auto
ultimately have "∀r ∈ ?S. finite (?f r)" by auto
moreover have "?ℛ = ⋃ (?f `?S)" by auto
ultimately have "finite ?ℛ" using fin by auto
moreover have "ℛ ⊆ ?ℛ"
proof
fix R assume R: "R ∈ ℛ"
then obtain I J r where I: "R = region X I J r" "valid_region X k I J r" unfolding ℛ_def by auto
let ?I = "λ x. if x ∈ X then I x else Const 0"
let ?J = "λ x y. if x ∈ X ∧ y ∈ X ∧ (isGreater (I x) ∨ isGreater (I y)) then J x y else Const' 0"
let ?R = "region X ?I ?J r"
from valid_regions_I_cong[OF I(2)] I have *: "R = ?R" "valid_region X k ?I ?J r" by auto
have "∀x. x ∉ X ⟶ ?I x = Const 0" by auto
moreover have "∀x. x ∈ X ⟶ intv_const (I x) ≤ ?u"
proof auto
fix x assume x: "x ∈ X"
with I(2) have "valid_intv (k x) (I x)" by auto
moreover from ‹finite X› x have "k x ≤ ?u" by (auto intro: Max_ge)
ultimately  show "intv_const (I x) ≤ Max {k x |x. x ∈ X}" by (cases "I x") auto
qed
ultimately have **: "?fin_mapI ?I" by auto
have "∀x y. x ∉ X ⟶ ?J x y = Const' 0" by auto
moreover have "∀x y. y ∉ X ⟶ ?J x y = Const' 0" by auto
moreover have "∀x. ∀ y. x ∈ X ∧ y ∈ X ⟶ ?l ≤ intv'_const (?J x y) ∧ intv'_const (?J x y) ≤ ?u"
proof clarify
fix x y assume x: "x ∈ X" assume y: "y ∈ X"
show "?l ≤ intv'_const (?J x y) ∧ intv'_const (?J x y) ≤ ?u"
proof (cases "isGreater (I x) ∨ isGreater (I y)")
case True
with x y I(2) have "valid_intv' (k y) (k x) (J x y)" by fastforce
moreover from ‹finite X› x have "k x ≤ ?u" by (auto intro: Max_ge)
moreover from ‹finite X› y have "?l ≤ -k y" by (auto intro: Max_ge)
ultimately show ?thesis by (cases "J x y") auto
next
case False then show ?thesis by auto
qed
qed
ultimately have "?fin_mapJ ?J" by auto
with * ** show "R ∈ ?ℛ" by blast
qed
ultimately show "finite ℛ" by (blast intro: finite_subset)
qed

end

section ‹Approximation with ‹β›-regions›

locale Beta_Regions' = Beta_Regions +
fixes v n not_in_X
assumes clock_numbering: "∀ c. v c > 0 ∧ (∀x. ∀y. v x ≤ n ∧ v y ≤ n ∧ v x = v y ⟶ x = y)"
"∀k :: nat ≤n. k > 0 ⟶ (∃c ∈ X. v c = k)" "∀ c ∈ X. v c ≤ n"
assumes not_in_X: "not_in_X ∉ X"
begin

definition "v' ≡ λ i. if i ≤ n then (THE c. c ∈ X ∧ v c = i) else not_in_X"

lemma v_v':
"∀ c ∈ X. v' (v c) = c"
using clock_numbering unfolding v'_def by auto

abbreviation
"vabstr (S :: ('a, t) zone) M ≡ S = [M]⇘v,n⇙ ∧ (∀ i≤n. ∀ j≤n. M i j ≠ ∞ ⟶ get_const (M i j) ∈ ℤ)"

definition normalized:
"normalized M ≡
(∀ i j. 0 < i ∧ i ≤ n ∧ 0 < j ∧ j ≤ n ∧ M i j ≠ ∞ ⟶
Lt (- ((k o v') j)) ≤ M i j ∧ M i j ≤ Le ((k o v') i))
∧ (∀ i ≤ n. i > 0 ⟶ (M i 0 ≤ Le ((k o v') i) ∨ M i 0 = ∞) ∧ Lt (- ((k o v') i)) ≤ M 0 i)"

definition apx_def:
"Approx⇩β Z ≡ ⋂ {S. ∃ U M. S = ⋃ U ∧ U ⊆ ℛ ∧ Z ⊆ S ∧ vabstr S M ∧ normalized M}"

lemma apx_min:
"S = ⋃ U ⟹ U ⊆ ℛ ⟹ S = [M]⇘v,n⇙ ⟹ ∀ i≤n. ∀ j≤n. M i j ≠ ∞ ⟶ get_const (M i j) ∈ ℤ
⟹ normalized M ⟹ Z ⊆ S ⟹ Approx⇩β Z ⊆ S"
unfolding apx_def by blast

lemma "U ≠ {} ⟹ x ∈ ⋂ U ⟹ ∃ S ∈ U. x ∈ S" by auto

lemma ℛ_union: "⋃ ℛ = V" using region_cover unfolding V_def ℛ_def by auto

lemma all_dbm: "∃ M. vabstr (⋃ℛ) M ∧ normalized M"
proof -
let ?M = "λ i j. if i = 0 then Le 0 else ∞"
have "[?M]⇘v,n⇙ = V" unfolding V_def DBM_zone_repr_def DBM_val_bounded_def
proof (auto, goal_cases)
case (1 u c)
with clock_numbering have "dbm_entry_val u None (Some c) (Le 0)" by auto
then show ?case by auto
next
case (2 u c)
from clock_numbering(1) have "0 ≠ v c" by auto
with 2 show ?case by auto
next
case (3 u c)
from clock_numbering(1) have "0 ≠ v c" by auto
with 3 show ?case by auto
next
case (4 u c)
with clock_numbering have "c ∈ X" by blast
with 4(1) show ?case by auto
next
case (5 u c1)
from clock_numbering(1) have "0 ≠ v c1" by auto
with 5 show ?case by auto
qed
moreover have "∀ i≤n. ∀ j≤n. ?M i j ≠ ∞ ⟶ get_const (?M i j) ∈ ℤ" by auto
moreover have "normalized ?M" unfolding normalized less_eq dbm_le_def by auto
ultimately show ?thesis using ℛ_union by auto
qed

lemma ℛ_int:
"R ∈ ℛ ⟹ R' ∈ ℛ ⟹ R ≠ R' ⟹ R ∩ R' = {}" using ℛ_regions_distinct by blast

lemma aux1:
"u ∈ R ⟹ R ∈ ℛ ⟹ U ⊆ ℛ ⟹ u ∈ ⋃ U ⟹ R ⊆ ⋃ U" using ℛ_int by blast

lemma aux2: "x ∈ ⋂ U ⟹ U ≠ {} ⟹ ∃ S ∈ U. x ∈ S" by blast

lemma aux2': "x ∈ ⋂ U ⟹ U ≠ {} ⟹ ∀ S ∈ U. x ∈ S" by blast

lemma apx_subset: "Z ⊆ Approx⇩β Z" unfolding apx_def by auto

lemma aux3:
"∀ X ∈ U. ∀ Y ∈ U. X ∩ Y ∈ U ⟹ S ⊆ U ⟹ S ≠ {} ⟹ finite S ⟹ ⋂ S ∈ U"
proof goal_cases
case 1
with finite_list obtain l where "set l = S" by blast
then show ?thesis using 1
proof (induction l arbitrary: S)
case Nil thus ?case by auto
next
case (Cons x xs)
show ?case
proof (cases "set xs = {}")
case False
with Cons have "⋂(set xs) ∈ U" by auto
with Cons.prems(1-3) show ?thesis by force
next
case True
with Cons.prems show ?thesis by auto
qed
qed
qed

lemma empty_zone_dbm:
"∃ M :: t DBM. vabstr {} M ∧ normalized M ∧ (∀k ≤ n. M k k ≤ Le 0)"
proof -
from non_empty obtain c where c: "c ∈ X" by auto
with clock_numbering have c': "v c > 0" "v c ≤ n" by auto
let ?M = "λi j. if i = v c ∧ j = 0 ∨ i = j then Le (0::t) else if i = 0 ∧ j = v c then Lt 0 else ∞"
have "[?M]⇘v,n⇙ = {}" unfolding DBM_zone_repr_def DBM_val_bounded_def using c' by auto
moreover have "∀ i≤n. ∀ j≤n. ?M i j ≠ ∞ ⟶ get_const (?M i j) ∈ ℤ" by auto
moreover have "normalized ?M" unfolding normalized less_eq dbm_le_def by auto
ultimately show ?thesis by auto
qed

lemma valid_dbms_int:
"∀X∈{S. ∃M. vabstr S M}. ∀Y∈{S. ∃M. vabstr S M}. X ∩ Y ∈ {S. ∃M. vabstr S M}"
proof (auto, goal_cases)
case (1 M1 M2)
obtain M' where M': "M' = And M1 M2" by fast
from DBM_and_sound1[OF ] DBM_and_sound2[OF] DBM_and_complete[OF ]
have "[M1]⇘v,n⇙ ∩ [M2]⇘v,n⇙ = [M']⇘v,n⇙" unfolding DBM_zone_repr_def M' by auto
moreover from 1 have "∀ i≤n. ∀ j≤n. M' i j ≠ ∞ ⟶ get_const (M' i j) ∈ ℤ"
unfolding M' by (auto split: split_min)
ultimately show ?case by auto
qed

print_statement split_min

lemma split_min':
"P (min i j) = ((min i j = i ⟶ P i) ∧ (min i j = j ⟶ P j))"
unfolding min_def by auto

lemma normalized_and_preservation:
"normalized M1 ⟹ normalized M2 ⟹ normalized (And M1 M2)"
unfolding normalized by safe (subst And.simps, split split_min', fastforce)+

lemma valid_dbms_int':
"∀X∈{S. ∃M. vabstr S M ∧ normalized M}. ∀Y∈{S. ∃M. vabstr S M ∧ normalized M}.
X ∩ Y ∈ {S. ∃M. vabstr S M ∧ normalized M}"
proof (auto, goal_cases)
case (1 M1 M2)
obtain M' where M': "M' = And M1 M2" by fast
from DBM_and_sound1 DBM_and_sound2 DBM_and_complete
have "[M1]⇘v,n⇙ ∩ [M2]⇘v,n⇙ = [M']⇘v,n⇙" unfolding M' DBM_zone_repr_def by auto
moreover from M' 1 have "∀ i≤n. ∀ j≤n. M' i j ≠ ∞ ⟶ get_const (M' i j) ∈ ℤ"
by (auto split: split_min)
moreover from normalized_and_preservation[OF 1(2,4)] have "normalized M'" unfolding M' .
ultimately show ?case by auto
qed

lemma apx_in:
"Z ⊆ V ⟹ Approx⇩β Z ∈ {S. ∃ U M. S = ⋃ U ∧ U ⊆ ℛ ∧ Z ⊆ S ∧ vabstr S M ∧ normalized M}"
proof -
assume "Z ⊆ V"
let ?A = "{S. ∃ U M. S = ⋃ U ∧ U ⊆ ℛ ∧ Z ⊆ S ∧ vabstr S M ∧ normalized M}"
let ?U = "{R ∈ ℛ. ∀ S ∈ ?A. R ⊆ S}"
have "?A ⊆ {S. ∃ U. S = ⋃ U ∧ U ⊆ ℛ}" by auto
moreover from finite_ℛ have "finite …" by auto
ultimately have "finite ?A" by (auto intro: finite_subset)
from all_dbm obtain M where M:
"vabstr (⋃ℛ) M" "normalized M"
by auto
with ‹_ ⊆ V› ℛ_union have "V ∈ ?A" by blast
then have "?A ≠ {}" by blast
have "?A ⊆ {S. ∃ M. vabstr S M ∧ normalized M}" by auto
with aux3[OF valid_dbms_int' this ‹?A ≠ _› ‹finite ?A›] have
"⋂ ?A ∈ {S. ∃ M. vabstr S M ∧ normalized M}"
by blast
then obtain M where *: "vabstr (Approx⇩β Z) M" "normalized M" unfolding apx_def by auto
have "⋃ ?U = ⋂ ?A"
proof (safe, goal_cases)
case 1
show ?case
proof (cases "Z = {}")
case False
then obtain v where "v ∈ Z" by auto
with region_cover ‹Z ⊆ V› obtain R where "R ∈ ℛ" "v ∈ R" unfolding V_def by blast
with aux1[OF this(2,1)] ‹v ∈ Z› have "R ∈ ?U" by blast
with 1 show ?thesis by blast
next
case True
with empty_zone_dbm have "{} ∈ ?A" by auto
with 1(1,3) show ?thesis by blast
qed
next
case (2 v)
from aux2[OF 2 ‹?A ≠ _›] obtain S where "v ∈ S" "S ∈ ?A" by blast
then obtain R where "v ∈ R" "R ∈ ℛ" by auto
{ fix S assume "S ∈ ?A"
with aux2'[OF 2 ‹?A ≠ _›] have "v ∈ S" by auto
with ‹S ∈ ?A› obtain U M R' where *:
"v ∈ R'" "R' ∈ ℛ" "S = ⋃U" "U ⊆ ℛ" "vabstr S M" "Z ⊆ S"
by blast
from aux1[OF this(1,2,4)] *(3) ‹v ∈ S› have "R' ⊆ S" by blast
moreover from ℛ_regions_distinct[OF *(2,1) ‹R ∈ ℛ›] ‹v ∈ R› have "R' = R" by fast
ultimately have "R ⊆ S" by fast
}
with ‹R ∈ ℛ› have "R ∈ ?U" by auto
with ‹v ∈ R› show ?case by auto
qed
then have "Approx⇩β Z = ⋃?U" "?U ⊆ ℛ" "Z ⊆ Approx⇩β Z" unfolding apx_def by auto
with * show ?thesis by blast
qed

lemma apx_empty:
"Approx⇩β {} = {}"
unfolding apx_def using empty_zone_dbm by blast

end

section ‹Computing ‹β›-Approximation›

context Beta_Regions'
begin

lemma dbm_regions:
"vabstr S M ⟹ normalized M ⟹ [M]⇘v,n⇙ ≠ {} ⟹ [M]⇘v,n⇙ ⊆ V ⟹ ∃ U ⊆ ℛ. S = ⋃ U"
proof goal_cases
case A: 1
let ?U =
"{R ∈ ℛ. ∃ I J r. R = region X I J r ∧ valid_region X k I J r ∧
(∀ c ∈ X.
(∀ d. I c = Const d ⟶ M (v c) 0 ≥ Le d ∧ M 0 (v c) ≥ Le (-d)) ∧
(∀ d. I c = Intv d ⟶  M (v c) 0 ≥ Lt (d + 1) ∧ M 0 (v c) ≥ Lt (-d)) ∧
(I c = Greater (k c) ⟶  M (v c) 0 = ∞)
) ∧
(∀ x ∈ X. ∀ y ∈ X.
(∀ c d. I x = Intv c ∧ I y = Intv d ⟶ M (v x) (v y) ≥
(if (x, y) ∈ r then if (y, x) ∈ r then Le (c - d) else Lt (c - d) else Lt (c - d + 1))) ∧
(∀ c d. I x = Intv c ∧ I y = Intv d ⟶ M (v y) (v x) ≥
(if (y, x) ∈ r then if (x, y) ∈ r then Le (d - c) else Lt (d - c) else Lt (d - c + 1))) ∧
(∀ c d. I x = Const c ∧ I y = Const d ⟶ M (v x) (v y) ≥ Le (c - d)) ∧
(∀ c d. I x = Const c ∧ I y = Const d ⟶ M (v y) (v x) ≥ Le (d - c)) ∧
(∀ c d. I x = Intv c ∧ I y = Const d ⟶ M (v x) (v y) ≥ Lt (c - d + 1)) ∧
(∀ c d. I x = Intv c ∧ I y = Const d ⟶ M (v y) (v x) ≥ Lt (d - c)) ∧
(∀ c d. I x = Const c ∧ I y = Intv d ⟶ M (v x) (v y) ≥ Lt (c - d)) ∧
(∀ c d. I x = Const c ∧ I y = Intv d ⟶ M (v y) (v x) ≥ Lt (d - c + 1)) ∧
((isGreater (I x) ∨ isGreater (I y)) ∧ J x y = Greater' (k x) ⟶ M (v x) (v y) = ∞) ∧
(∀ c. (isGreater (I x) ∨ isGreater (I y)) ∧ J x y = Const' c
⟶ M (v x) (v y) ≥ Le c ∧ M (v y) (v x) ≥ Le (- c)) ∧
(∀ c. (isGreater (I x) ∨ isGreater (I y)) ∧ J x y = Intv' c
⟶ M (v x) (v y) ≥ Lt (c + 1) ∧ M (v y) (v x) ≥ Lt (- c))
)
}"
have "⋃ ?U = [M]⇘v,n⇙" unfolding DBM_zone_repr_def DBM_val_bounded_def
proof (standard, goal_cases)
case 1
show ?case
proof (auto, goal_cases)
case 1
from A(3) show "Le 0 ≼ M 0 0" unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
next
case (2 u I J r c)
note B = this
from B(6) clock_numbering have "c ∈ X" by blast
with B(1) v_v' have *: "intv_elem c u (I c)" "v' (v c) = c" by auto
from clock_numbering(1) have "v c > 0" by auto
show ?case
proof (cases "I c")
case (Const d)
with B(4) ‹c ∈ X› have "M 0 (v c) ≥ Le (- real d)" by auto
with * Const show ?thesis by - (rule dbm_entry_val_mono_2[folded less_eq], auto)
next
case (Intv d)
with B(4) ‹c ∈ X› have "M 0 (v c) ≥ Lt (- real d)" by auto
with * Intv show ?thesis by - (rule dbm_entry_val_mono_2[folded less_eq], auto)
next
case (Greater d)
with B(3) ‹c ∈ X› have "I c = Greater (k c)" by fastforce
with * have "- u c < - k c" by auto
moreover from A(2) *(2) ‹v c ≤ n› ‹v c > 0› have
"Lt (- k c) ≤ M 0 (v c)"
unfolding normalized by force
ultimately show ?thesis by - (rule dbm_entry_val_mono_2[folded less_eq], auto)
qed
next
case (3 u I J r c)
note B = this
from B(6) clock_numbering have "c ∈ X" by blast
with B(1) v_v' have *: "intv_elem c u (I c)" "v' (v c) = c" by auto
from clock_numbering(1) have "v c > 0" by auto
show ?case
proof (cases "I c")
case (Const d)
with B(4) ‹c ∈ X› have "M (v c) 0 ≥ Le d" by auto
with * Const show ?thesis by - (rule dbm_entry_val_mono_3[folded less_eq], auto)
next
case (Intv d)
with B(4) ‹c ∈ X› have "M (v c) 0 ≥ Lt (real d + 1)" by auto
with * Intv show ?thesis by - (rule dbm_entry_val_mono_3[folded less_eq], auto)
next
case (Greater d)
with B(3) ‹c ∈ X› have "I c = Greater (k c)" by fastforce
with B(4) ‹c ∈ X› show ?thesis by auto
qed
next
case B: (4 u I J r c1 c2)
from B(6,7) clock_numbering have "c1 ∈ X" "c2 ∈ X" by blast+
with B(1) v_v' have *:
"intv_elem c1 u (I c1)" "intv_elem c2 u (I c2)" "v' (v c1) = c1" "v' (v c2) = c2"
by auto
from clock_numbering(1) have "v c1 > 0" "v c2 > 0" by auto
{ assume C: "isGreater (I c1) ∨ isGreater (I c2)"
with B(1) ‹c1 ∈ X› ‹c2 ∈ X› have **: "intv'_elem c1 c2 u (J c1 c2)" by force
have ?case
proof (cases "J c1 c2")
case (Smaller' c)
with C B(3) ‹c1 ∈ X› ‹c2 ∈ X› have "c ≤ - k c2" by fastforce
moreover from C ‹c1 ∈ X› ‹c2 ∈ X› ** Smaller' have "u c1 - u c2 < c" by auto
moreover from A(2) *(3,4) B(6,7) ‹v c1 > 0› ‹v c2 > 0› have
"M (v c1) (v c2) ≥ Lt (- k c2) ∨ M (v c1) (v c2) = ∞"
unfolding normalized by fastforce
ultimately show ?thesis by (safe) (rule dbm_entry_val_mono_1[folded less_eq], auto)
next
case (Const' c)
with C B(5) ‹c1 ∈ X› ‹c2 ∈ X› have "M (v c1) (v c2) ≥ Le c" by auto
with Const' ** ‹c1 ∈ X› ‹c2 ∈ X› show ?thesis
by (auto intro: dbm_entry_val_mono_1[folded less_eq])
next
case (Intv' c)
with C B(5) ‹c1 ∈ X› ‹c2 ∈ X› have "M (v c1) (v c2) ≥ Lt (real_of_int c + 1)" by auto
with Intv' ** ‹c1 ∈ X› ‹c2 ∈ X› show ?thesis
by (auto intro: dbm_entry_val_mono_1[folded less_eq])
next
case (Greater' c)
with C B(3) ‹c1 ∈ X› ‹c2 ∈ X› have "c = k c1" by fastforce
with Greater' C B(5) ‹c1 ∈ X› ‹c2 ∈ X› show ?thesis by auto
qed
} note GreaterI = this
show ?case
proof (cases "I c1")
case (Const c)
show ?thesis
proof (cases "I c2", goal_cases)
case (1 d)
with Const ‹c1 ∈ X› ‹c2 ∈ X› *(1,2) have "u c1 = c" "u c2 = d" by auto
moreover from ‹c1 ∈ X› ‹c2 ∈ X› 1 Const B(5) have
"Le (real c - real d) ≤ M (v c1) (v c2)"
by meson
ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
next
case (Intv d)
with Const ‹c1 ∈ X› ‹c2 ∈ X› *(1,2) have "u c1 = c" "d < u c2" by auto
then have "u c1 - u c2 < c - real d" by auto
moreover from Const ‹c1 ∈ X› ‹c2 ∈ X› Intv B(5) have
"Lt (real c - d) ≤ M (v c1) (v c2)"
by meson
ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
next
case Greater then show ?thesis by (auto intro: GreaterI)
qed
next
case (Intv c)
show ?thesis
proof (cases "I c2", goal_cases)
case (Const d)
with Intv ‹c1 ∈ X› ‹c2 ∈ X› *(1,2) have "u c1 < c + 1" "d = u c2" by auto
then have "u c1 - u c2 < c - real d + 1" by auto
moreover from ‹c1 ∈ X› ‹c2 ∈ X› Intv Const B(5) have
"Lt (real c - real d + 1) ≤ M (v c1) (v c2)"
by meson
ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
next
case (2 d)
show ?case
proof (cases "(c1,c2) ∈ r")
case True
note T = this
show ?thesis
proof (cases "(c2,c1) ∈ r")
case True
with T B(5) 2 Intv ‹c1 ∈ X› ‹c2 ∈ X› have
"Le (real c - real d) ≤ M (v c1) (v c2)"
by auto
moreover from nat_intv_frac_decomp[of c "u c1"] nat_intv_frac_decomp[of d "u c2"]
B(1,2) ‹c1 ∈ X› ‹c2 ∈ X› T True Intv 2 *(1,2)
have "u c1 - u c2 = real c - d" by auto
ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
next
case False
with T B(5) 2 Intv ‹c1 ∈ X› ‹c2 ∈ X› have
"Lt (real c - real d) ≤ M (v c1) (v c2)"
by auto
moreover from nat_intv_frac_decomp[of c "u c1"] nat_intv_frac_decomp[of d "u c2"]
B(1,2) ‹c1 ∈ X› ‹c2 ∈ X› T False Intv 2 *(1,2)
have "u c1 - u c2 < real c - d" by auto
ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
qed
next
case False
with B(5) 2 Intv ‹c1 ∈ X› ‹c2 ∈ X› have
"Lt (real c - real d + 1) ≤ M (v c1) (v c2)"
by meson
moreover from 2 Intv ‹c1 ∈ X› ‹c2 ∈ X› * have "u c1 - u c2 < c - real d + 1" by auto
ultimately show ?thesis by (auto intro: dbm_entry_val_mono_1[folded less_eq])
qed
next
case Greater then show ?thesis by (auto intro: GreaterI)
qed
next
case Greater then show ?thesis by (auto intro: GreaterI)
qed
qed
next
case 2 show ?case
proof (safe, goal_cases)
case (1 u)
with A(4) have "u ∈ V" unfolding DBM_zone_repr_def DBM_val_bounded_def by auto
with region_cover obtain R where "R ∈ ℛ" "u ∈ R" unfolding V_def by auto
then obtain I J r where R: "R = region X I J r" "valid_region X k I J r" unfolding ℛ_def by auto
have "(∀c∈X. (∀d. I c = Const d ⟶ Le (real d) ≤ M (v c) 0 ∧ Le (- real d) ≤ M 0 (v c)) ∧
(∀d. I c = Intv d ⟶ Lt (real d + 1) ≤ M (v c) 0 ∧ Lt (- real d) ≤ M 0 (v c)) ∧
(I c = Greater (k c) ⟶ M (v c) 0 = ∞))"
proof safe
fix c assume "c ∈ X"
with R ‹u ∈ R› have *: "intv_elem c u (I c)" by auto
fix d assume **: "I c = Const d"
with * have "u c = d" by fastforce
moreover from ** clock_numbering(3) ‹c ∈ X› 1 have
"dbm_entry_val u (Some c) None (M (v c) 0)"
by auto
ultimately show "Le (real d) ≤ M (v c) 0"
unfolding less_eq dbm_le_def by (cases "M (v c) 0") auto
next
fix c assume "c ∈ X"
with R ‹u ∈ R› have *: "intv_elem c u (I c)" by auto
fix d assume **: "I c = Const d"
with * have "u c = d" by fastforce
moreover from ** clock_numbering(3) ‹c ∈ X› 1 have
"dbm_entry_val u None (Some c) (M 0 (v c))"
by auto
ultimately show "Le (- real d) ≤ M 0 (v c)"
unfolding less_eq dbm_le_def by (cases "M 0 (v c)") auto
next
fix c assume "c ∈ X"
with R ‹u ∈ R› have *: "intv_elem c u (I c)" by auto
fix d assume **: "I c = Intv d"
with * have "d < u c" "u c < d + 1" by fastforce+
moreover from ** clock_numbering(3) ‹c ∈ X› 1 have
"dbm_entry_val u (Some c) None (M (v c) 0)"
by auto
moreover have
"M (v c) 0 ≠ ∞ ⟹ get_const (M (v c) 0) ∈ ℤ"
using ‹c ∈ X› clock_numbering A(1) by auto
ultimately show "Lt (real d + 1) ≤ M (v c) 0" unfolding less_eq dbm_le_def
apply (cases "M (v c) 0")
apply auto
apply (rename_tac x1)
apply (subgoal_tac "x1 > d")
apply (rule dbm_lt.intros(5))
apply (metis nat_intv_frac_gt0 frac_eq_0_iff less_irrefl linorder_not_le of_nat_1 of_nat_add)
apply simp
apply (rename_tac x2)
apply (subgoal_tac "x2 > d + 1")
apply (rule dbm_lt.intros(6))
apply simp
less_eq_real_def linorder_neqE_linordered_idom semiring_1_class.of_nat_simps(2))
next
fix c assume "c ∈ X"
with R ‹u ∈ R› have *: "intv_elem c u (I c)" by auto
fix d assume **: "I c = Intv d"
with * have "d < u c" "u c < d + 1" by fastforce+
moreover from ** clock_numbering(3) ‹c ∈ X› 1 have
"dbm_entry_val u None (Some c) (M 0 (v c))"
by auto
moreover have "M 0 (v c) ≠ ∞ ⟹ get_const (M 0 (v c)) ∈ ℤ" using ‹c ∈ X› clock_numbering A(1) by auto
ultimately show "Lt (- real d) ≤ M 0 (v c)" unfolding less_eq dbm_le_def
proof (cases "M 0 (v c)", -, auto, goal_cases)
case prems: (1 x1)
then have "u c = d + frac (u c)" by (metis nat_intv_frac_decomp ‹u c < d + 1›)
with prems(5) have "- x1 ≤ d + frac (u c)" by auto
with prems(1) frac_ge_0 frac_lt_1 have "- x1 ≤ d"
by - (rule ints_le_add_frac2[of "frac (u c)" d "-x1"]; fastforce)
with prems have "- d ≤ x1" by auto
then show ?case by auto
next
case prems: (2 x1)
then have "u c = d + frac (u c)" by (metis nat_intv_frac_decomp ‹u c < d + 1›)
with prems(5) have "- x1 ≤ d + frac (u c)" by auto
with prems(1) frac_ge_0 frac_lt_1 have "- x1 ≤ d"
by - (rule ints_le_add_frac2[of "frac (u c)" d "-x1"]; fastforce)
with prems(6) have "- d < x1" by auto
then show ?case by auto
qed
next
fix c assume "c ∈ X"
with R ‹u ∈ R› have *: "intv_elem c u (I c)" by auto
fix d assume **: "I c = Greater (k c)"
have "M (v c) 0 ≤ Le ((k o v') (v c)) ∨ M (v c) 0 = ∞"
using A(2) ‹c ∈ X› clock_numbering unfolding normalized by auto
with v_v' ‹c ∈ X› have "M (v c) 0 ≤ Le (k c) ∨ M (v c```