# Theory NatInt

(*  Title:      NatInt.thy
Author:     Sven Linker, University of Liverpool

Intervals based on natural numbers. Defines a
bottom element (empty set), infimum (set intersection),
partial order (subset relation), cardinality (set cardinality).

The union of intervals i and j can only be created, if they are consecutive, i.e.,
max i +1 = min j (or vice versa). To express consecutiveness, we employ the
predicate consec.

Also contains a "chopping" predicate N_Chop(i,j,k): i can be divided into
consecutive intervals j and k.
*)

section ‹Discrete Intervals based on Natural Numbers›

text‹We define a type of intervals based on the natural numbers. To that
end, we employ standard operators of Isabelle, but in addition prove some
structural properties of the intervals. In particular, we show that this type
constitutes a meet-semilattice with a bottom element and equality.

Furthermore, we show that this semilattice allows for a constrained join, i.e.,
the union of two intervals is defined, if either one of them is empty, or they are
consecutive. Finally, we define the notion of \emph{chopping} an interval into
two consecutive subintervals.›

theory NatInt
imports Main
begin

text ‹A discrete interval is a set of consecutive natural numbers, or the empty
set.›

typedef nat_int = "{S . (∃ (m::nat) n . {m..n }=S) }"
by auto
setup_lifting type_definition_nat_int

subsection ‹Basic properties of discrete intervals.›

locale nat_int
interpretation nat_int_class?: nat_int .

context nat_int
begin

lemma un_consec_seq: "(m::nat)≤ n ∧ n+1 ≤ l ⟶ {m..n} ∪ {n+1..l} = {m..l}"
by auto

lemma int_conseq_seq: " {(m::nat)..n} ∩ {n+1..l} = {}"
by auto

lemma empty_type: "{} ∈ { S . ∃ (m:: nat) n . {m..n}=S}"
by auto

lemma inter_result: "∀x ∈ {S . (∃ (m::nat) n .  {m..n }=S) }.
∀y ∈ {S . (∃ (m::nat) n . {m..n }=S) }.
x ∩ y ∈{S . (∃ (m::nat) n .  {m..n }=S)}"
using Int_atLeastAtMost by blast

lemma union_result: "∀x ∈ {S . (∃ (m::nat) n .  {m..n }=S) }.
∀y ∈ {S . (∃ (m::nat) n .  {m..n }=S)  }.
x ≠ {} ∧ y ≠ {} ∧ Max x +1 = Min y
⟶ x ∪ y ∈{S . (∃ (m::nat) n . {m..n }=S)  }"
proof (rule ballI)+
fix x y
assume "x∈ {S . (∃ (m::nat) n .  {m..n }=S) }"
and "y∈ {S . (∃ (m::nat) n .  {m..n }=S) }"
then have x_def:"(∃m n.  {m..n} = x) "
and y_def:"(∃m n.  {m..n} = y) " by blast+
show   " x ≠ {} ∧ y ≠ {} ∧   Max x+1 = Min y
⟶ x ∪  y ∈ {S. (∃m n.  {m..n} = S) }"
proof
assume pre:"x ≠ {} ∧ y ≠ {} ∧ Max x + 1 = Min y"
then have x_int:"∃m n. m ≤ n ∧ {m..n} = x"
and y_int:"(∃m n. m ≤ n ∧ {m..n} = y)"
using  x_def y_def by force+
{
fix ya yb xa xb
assume y_prop:"ya ≤ yb ∧ {ya..yb} = y" and x_prop:"xa ≤ xb ∧ {xa..xb} = x"
then have upper_x:"Max x = xb" and lower_y: "Min y = ya"
by (auto simp: Max_eq_iff Min_eq_iff)
from upper_x and lower_y and pre have upper_eq_lower: "xb+1 = ya"
by blast
hence "y= {xb+1 .. yb}" using y_prop by blast
hence "x ∪ y = {xa..yb}"
using un_consec_seq upper_eq_lower x_prop y_prop by blast
then have " x ∪ y ∈ {S.(∃m n.  {m..n} = S) }"
by auto
}
then show "x ∪ y ∈ {S.(∃m n.  {m..n} = S)}"
using x_int y_int by blast
qed
qed

lemma union_empty_result1: "∀i ∈ {S . (∃ (m::nat) n .  {m..n }=S) }.
i ∪ {} ∈ {S . (∃ (m::nat) n .  {m..n }=S) }"
by blast

lemma union_empty_result2: "∀i ∈ {S . (∃ (m::nat) n . {m..n }=S)  }.
{} ∪ i ∈ {S . (∃ (m::nat) n . {m..n }=S)  }"
by blast

lemma finite:" ∀i ∈ {S . (∃ (m::nat) n .  {m..n }=S) } . (finite i)"
by blast

lemma not_empty_means_seq:"∀i ∈ {S . (∃ (m::nat) n .  {m..n }=S) } . i ≠ {}
⟶ ( ∃m n . m ≤ n ∧ {m..n} = i)"
using atLeastatMost_empty_iff
by force
end

text ‹The empty set is the bottom element of the type. The infimum/meet of
the semilattice is set intersection. The order is given by the subset relation.
›

instantiation nat_int :: bot
begin
lift_definition bot_nat_int :: "nat_int" is Set.empty by force
instance by standard
end

instantiation nat_int ::  inf
begin
lift_definition inf_nat_int  ::"nat_int ⇒ nat_int ⇒ nat_int" is Set.inter  by force
instance
proof qed
end

instantiation nat_int :: "order_bot"
begin
lift_definition less_eq_nat_int :: "nat_int ⇒ nat_int ⇒ bool" is Set.subset_eq .
lift_definition less_nat_int :: "nat_int ⇒ nat_int ⇒ bool" is Set.subset .
instance
proof
fix i j k ::nat_int
show "(i < j) = (i ≤ j ∧ ¬ j ≤ i)"
by (simp add: less_eq_nat_int.rep_eq less_le_not_le less_nat_int.rep_eq)
show "i ≤ i" by (simp add:less_eq_nat_int.rep_eq)
show " i ≤ j ⟹ j ≤ k ⟹ i ≤ k" by (simp add:less_eq_nat_int.rep_eq)
show "i ≤ j ⟹ j ≤ i ⟹ i = j"
by (simp add: Rep_nat_int_inject less_eq_nat_int.rep_eq )
show "bot ≤ i" using  less_eq_nat_int.rep_eq
using bot_nat_int.rep_eq by blast
qed
end

instantiation nat_int ::  "semilattice_inf"
begin
instance
proof
fix i j k :: nat_int
show "i ≤ j ⟹ i ≤ k ⟹ i ≤ inf j k"
show " inf i   j ≤ i"
show "inf i  j ≤ j"
qed
end

instantiation nat_int:: "equal"
begin
definition equal_nat_int :: "nat_int ⇒ nat_int ⇒ bool"
where "equal_nat_int i  j ≡ i ≤ j ∧ j ≤ i"
instance
proof
fix i j :: nat_int
show " equal_class.equal i j = (i = j)" using equal_nat_int_def  by auto
qed
end

context nat_int
begin
abbreviation subseteq :: "nat_int ⇒ nat_int⇒ bool" (infix "⊑" 30)
where  "i ⊑ j == i ≤ j "
abbreviation empty :: "nat_int" ("∅")
where "∅ ≡ bot"

notation inf (infix "⊓" 70)

text ‹The union of two intervals is only defined, if it is also
a discrete interval.›
definition union :: "nat_int ⇒ nat_int ⇒ nat_int" (infix "⊔" 65)
where "i ⊔ j = Abs_nat_int (Rep_nat_int i ∪ Rep_nat_int j)"

text ‹Non-empty intervals contain a minimal and maximal element.
Two non-empty intervals $$i$$ and $$j$$ are
consecutive, if the minimum of $$j$$ is the successor of the
maximum of $$i$$.
Furthermore, the interval $$i$$ can be chopped into the intervals $$j$$
and $$k$$, if the union of $$j$$ and $$k$$ equals $$i$$, and if $$j$$
and $$k$$ are not-empty, they must be consecutive. Finally, we define
the cardinality of discrete intervals by lifting the cardinality of
sets.
›
definition maximum :: "nat_int ⇒ nat"
where maximum_def: "i ≠ ∅ ⟹ maximum (i) =   Max (Rep_nat_int i)"

definition minimum :: "nat_int ⇒ nat"
where minimum_def: "i ≠ ∅ ⟹ minimum(i) = Min (Rep_nat_int i)"

definition consec:: "nat_int⇒nat_int ⇒ bool"
where "consec i j ≡ (i≠∅ ∧ j ≠ ∅ ∧ (maximum(i)+1 = minimum j))"

definition N_Chop :: "nat_int ⇒ nat_int ⇒ nat_int ⇒ bool" ("N'_Chop'(_,_,_')" 51)
where nchop_def :
"N_Chop(i,j,k) ≡ (i =  j ⊔ k   ∧ (j = ∅ ∨  k = ∅ ∨ consec j k))"

lift_definition card' ::"nat_int ⇒ nat"  ( "|_|" 70) is card .

text‹For convenience, we also lift the membership relation and its negation
to discrete intervals.›

lift_definition el::"nat ⇒ nat_int ⇒ bool" (infix "❙∈" 50) is "Set.member" .

lift_definition not_in ::"nat ⇒ nat_int ⇒ bool" (infix "❙∉" 40)  is Set.not_member .
end

lemmas[simp] = nat_int.el.rep_eq nat_int.not_in.rep_eq nat_int.card'.rep_eq

context nat_int
begin

lemma in_not_in_iff1 :"n ❙∈ i ⟷ ¬ n❙∉ i" by simp
lemma in_not_in_iff2: "n❙∉ i ⟷ ¬ n ❙∈ i" by simp

lemma rep_non_empty_means_seq:"i ≠∅
⟶ (∃m n. m ≤ n ∧ ({m..n} =( Rep_nat_int i)))"
by (metis Rep_nat_int Rep_nat_int_inject bot_nat_int.rep_eq nat_int.not_empty_means_seq)

lemma non_empty_max: "i ≠ ∅ ⟶ (∃m . maximum(i) = m)"
by auto

lemma non_empty_min: "i ≠ ∅ ⟶ (∃m . minimum(i) = m)"
by auto

lemma minimum_in: "i ≠ ∅ ⟶ minimum i ❙∈ i"
by (metis Min_in atLeastatMost_empty_iff2 finite_atLeastAtMost minimum_def
el.rep_eq rep_non_empty_means_seq)

lemma maximum_in: "i ≠ ∅ ⟶ maximum i ❙∈ i"
by (metis Max_in atLeastatMost_empty_iff2 finite_atLeastAtMost maximum_def
el.rep_eq rep_non_empty_means_seq)

lemma non_empty_elem_in:"i ≠ ∅ ⟷ (∃n. n ❙∈ i)"
proof
assume assm:"i ≠ ∅"
show "∃n . n ❙∈ i"
by (metis assm Rep_nat_int_inverse all_not_in_conv el.rep_eq bot_nat_int_def)
next
assume assm:"∃n. n ❙∈ i"
show "i ≠ ∅"
using Abs_nat_int_inverse assm el.rep_eq bot_nat_int_def by fastforce
qed

lemma leq_nat_non_empty:"(m::nat) ≤ n ⟶ Abs_nat_int{m..n} ≠ ∅"
proof
assume assm:"m ≤n"
then have non_empty:"{m..n} ≠ {} "
using atLeastatMost_empty_iff by blast
with assm have "{m..n} ∈ {S . (∃ (m::nat) n .  {m..n }=S)  }" by blast
then show "Abs_nat_int {m..n} ≠ ∅"
using Abs_nat_int_inject empty_type non_empty bot_nat_int_def
qed

lemma leq_max_sup:"(m::nat) ≤ n ⟶ Max {m..n} = n"
by (auto simp: Max_eq_iff)

lemma leq_min_inf: "(m::nat) ≤ n ⟶ Min {m..n} = m"
by (auto simp: Min_eq_iff)

lemma leq_max_sup':"(m::nat) ≤ n ⟶ maximum(Abs_nat_int{m..n}) = n"
proof
assume assm:"m ≤ n"
hence in_type:"{m..n} ∈ {S . (∃ (m::nat) n . m ≤ n ∧ {m..n }=S) ∨ S={} }" by blast
from assm have "Abs_nat_int{m..n} ≠ ∅" using leq_nat_non_empty by blast
hence max:"maximum(Abs_nat_int{m..n}) = Max (Rep_nat_int (Abs_nat_int {m..n}))"
using maximum_def by blast
from in_type have " (Rep_nat_int (Abs_nat_int {m..n})) = {m..n}"
using Abs_nat_int_inverse by blast
hence  "Max (Rep_nat_int (Abs_nat_int{m..n})) = Max {m..n}" by simp
with max have simp_max:"maximum(Abs_nat_int{m..n}) = Max {m..n}" by simp
from assm have "Max {m..n} = n" using leq_max_sup by blast
with simp_max show "maximum(Abs_nat_int{m..n}) = n" by simp
qed

lemma leq_min_inf':"(m::nat) ≤ n ⟶ minimum(Abs_nat_int{m..n}) = m"
proof
assume assm:"m ≤ n"
hence in_type:"{m..n} ∈ {S . (∃ (m::nat) n . m ≤ n ∧ {m..n }=S) ∨ S={} }" by blast
from assm have "Abs_nat_int{m..n} ≠ ∅" using leq_nat_non_empty by blast
hence min:"minimum(Abs_nat_int{m..n}) = Min(Rep_nat_int (Abs_nat_int {m..n}))"
using  minimum_def by blast
from in_type have " (Rep_nat_int (Abs_nat_int {m..n})) = {m..n}"
using Abs_nat_int_inverse by blast
hence  "Min (Rep_nat_int (Abs_nat_int{m..n})) = Min {m..n}" by simp
with min have simp_min:"minimum(Abs_nat_int{m..n}) = Min {m..n}" by simp
from assm have "Min {m..n} = m" using leq_min_inf by blast
with simp_min show "minimum(Abs_nat_int{m..n}) = m" by simp
qed

lemma in_refl:"(n::nat)  ❙∈ Abs_nat_int {n}"
proof -
have "(n::nat) ≤ n" by simp
hence "{n} ∈ {S . (∃ (m::nat) n . m ≤ n ∧ {m..n }=S) ∨ S={} }" by auto
then show "n ❙∈ Abs_nat_int {n}"
qed

lemma in_singleton:" m ❙∈ Abs_nat_int{n} ⟶ m = n"
proof
assume assm:" m ❙∈ Abs_nat_int{n}"
have "(n::nat) ≤ n" by simp
hence "{n} ∈ {S . (∃ (m::nat) n . m ≤ n ∧ {m..n }=S) ∨ S={} }" by auto
with assm show "m=n" by (simp add: Abs_nat_int_inverse el_def)
qed

subsection ‹Algebraic properties of intersection and union.›

lemma inter_empty1:"(i::nat_int) ⊓ ∅ = ∅"
using Rep_nat_int_inject inf_nat_int.rep_eq bot_nat_int.abs_eq bot_nat_int.rep_eq
by fastforce

lemma inter_empty2:"∅ ⊓ (i::nat_int) = ∅"
by (metis inf_commute nat_int.inter_empty1)

lemma un_empty_absorb1:"i ⊔ ∅ = i"
using  Abs_nat_int_inverse Rep_nat_int_inverse union_def empty_type bot_nat_int.rep_eq
by auto

lemma un_empty_absorb2:"∅ ⊔ i = i"
using  Abs_nat_int_inverse Rep_nat_int_inverse union_def empty_type bot_nat_int.rep_eq
by auto

text ‹Most properties of the union of two intervals depends on them being consectuive,
to ensure that their union exists.›

lemma consec_un:"consec i j ∧ n ∉ Rep_nat_int(i) ∪ Rep_nat_int j
⟶ n ❙∉  (i ⊔ j)"
proof
assume assm:"consec i j ∧ n ∉  Rep_nat_int i ∪ Rep_nat_int j"
thus "n ❙∉ (i ⊔ j)"
proof -
have f1: "Abs_nat_int (Rep_nat_int (i ⊔ j))
= Abs_nat_int (Rep_nat_int i ∪ Rep_nat_int j)"
using Rep_nat_int_inverse union_def by presburger
have "i ≠ ∅ ∧ j ≠ ∅ ∧ maximum i + 1 = minimum j"
using assm consec_def by auto
then have "∃n na. {n..na} = Rep_nat_int i ∪ Rep_nat_int j"
by (metis (no_types) leq_max_sup leq_min_inf maximum_def minimum_def
rep_non_empty_means_seq un_consec_seq)
then show ?thesis
using f1 Abs_nat_int_inject Rep_nat_int not_in.rep_eq assm by auto
qed
qed

lemma un_subset1: "consec i j ⟶ i ⊑ i ⊔ j"
proof
assume "consec i j"
then have assm:"i ≠ ∅ ∧ j ≠ ∅ ∧ maximum i+1 = minimum j"
using consec_def by blast
have "Rep_nat_int i ∪ Rep_nat_int j =  {minimum i.. maximum j}"
by (metis assm nat_int.leq_max_sup nat_int.leq_min_inf nat_int.maximum_def
nat_int.minimum_def nat_int.rep_non_empty_means_seq nat_int.un_consec_seq)
then show "i ⊑ i ⊔ j" using Abs_nat_int_inverse Rep_nat_int
by (metis (mono_tags, lifting) Un_upper1 less_eq_nat_int.rep_eq mem_Collect_eq
nat_int.union_def)
qed

lemma un_subset2: "consec i j ⟶ j ⊑ i ⊔ j"
proof
assume "consec i j"
then have assm:"i ≠ ∅ ∧ j ≠ ∅ ∧ maximum i+1 = minimum j"
using consec_def by blast
have "Rep_nat_int i ∪ Rep_nat_int j =  {minimum i.. maximum j}"
by (metis assm nat_int.leq_max_sup nat_int.leq_min_inf nat_int.maximum_def
nat_int.minimum_def nat_int.rep_non_empty_means_seq nat_int.un_consec_seq)
then show "j ⊑ i ⊔ j" using Abs_nat_int_inverse Rep_nat_int
by (metis (mono_tags, lifting) Un_upper2 less_eq_nat_int.rep_eq mem_Collect_eq
nat_int.union_def)
qed

lemma inter_distr1:"consec j k ⟶ i ⊓ (j ⊔ k) = (i ⊓ j) ⊔ (i ⊓ k)"
unfolding consec_def
proof
assume assm:"j ≠ ∅ ∧ k ≠ ∅ ∧ maximum j +1 = minimum k"
then show " i ⊓ (j ⊔ k) = (i ⊓ j) ⊔ (i ⊓ k)"
proof -
have f1: "∀n. n = ∅ ∨ maximum n = Max (Rep_nat_int n)"
using nat_int.maximum_def by auto
have f2: "Rep_nat_int j ≠ {}"
using assm nat_int.maximum_in by auto
have f3: "maximum j = Max (Rep_nat_int j)"
using f1 by (meson assm)
have "maximum k ❙∈ k"
using assm nat_int.maximum_in by blast
then have "Rep_nat_int k ≠ {}"
by fastforce
then have "Rep_nat_int (j ⊔ k) = Rep_nat_int j ∪ Rep_nat_int k"
using f3 f2 Abs_nat_int_inverse Rep_nat_int assm nat_int.minimum_def
nat_int.union_def union_result
by auto
then show ?thesis
by (metis Rep_nat_int_inverse inf_nat_int.rep_eq inf_sup_distrib1 nat_int.union_def)
qed
qed

lemma inter_distr2:"consec j k ⟶ (j ⊔ k) ⊓ i = (j ⊓ i) ⊔ (k ⊓ i)"

lemma consec_un_not_elem1:"consec i j ∧ n❙∉ i ⊔ j ⟶  n ❙∉ i"
using un_subset1 less_eq_nat_int.rep_eq not_in.rep_eq by blast

lemma consec_un_not_elem2:"consec i j ∧ n❙∉ i ⊔ j ⟶  n ❙∉ j"
using  un_subset2 less_eq_nat_int.rep_eq not_in.rep_eq by blast

lemma consec_un_element1:"consec i j ∧ n ❙∈ i ⟶ n ❙∈ i ⊔ j"
using less_eq_nat_int.rep_eq nat_int.el.rep_eq nat_int.un_subset1 by blast

lemma consec_un_element2:"consec i j ∧ n ❙∈ j ⟶ n ❙∈ i ⊔ j"
using less_eq_nat_int.rep_eq nat_int.el.rep_eq nat_int.un_subset2 by blast

lemma consec_lesser:" consec i j  ⟶ (∀n m. (n ❙∈ i ∧ m ❙∈ j ⟶ n < m))"
proof (rule allI|rule impI)+
assume "consec i j"
fix n and m
assume assump:"n ❙∈ i ∧ m ❙∈ j "
then have  max:"n ≤ maximum i"
by (metis ‹consec i j› atLeastAtMost_iff leq_max_sup maximum_def consec_def
el.rep_eq rep_non_empty_means_seq)
from assump have min: "m ≥ minimum j"
by (metis Min_le ‹consec i j› finite_atLeastAtMost minimum_def consec_def
el.rep_eq rep_non_empty_means_seq)
from min and max show less:"n < m"
dual_order.trans leD leI consec_def by auto
qed

lemma consec_in_exclusive1:"consec i j ∧ n ❙∈ i ⟶ n ❙∉ j"
using nat_int.consec_lesser nat_int.in_not_in_iff2 by blast

lemma consec_in_exclusive2:"consec i j ∧ n ❙∈ j ⟶ n ❙∉ i"
using consec_in_exclusive1 el.rep_eq not_in.rep_eq by blast

lemma consec_un_max:"consec i j ⟶ maximum j = maximum (i ⊔ j)"
proof
assume assm:"consec i j"
then have "(∀n m. (n ❙∈ i ∧ m ❙∈ j ⟶ n < m))"
using nat_int.consec_lesser by blast
then have "∀n . (n ❙∈ i ⟶ n < maximum j)"
using assm local.consec_def nat_int.maximum_in by auto
then have "∀n. (n ❙∈ i ⊔ j ⟶ n ≤ maximum j)"
by (metis (no_types, lifting) Rep_nat_int Rep_nat_int_inverse Un_iff assm atLeastAtMost_iff
bot_nat_int.rep_eq less_imp_le_nat local.consec_def local.not_empty_means_seq
nat_int.consec_un nat_int.el.rep_eq nat_int.in_not_in_iff1 nat_int.leq_max_sup')
then show "maximum j = maximum (i ⊔ j)"
by (metis Rep_nat_int_inverse assm atLeastAtMost_iff bot.extremum_uniqueI
le_antisym local.consec_def nat_int.consec_un_element2 nat_int.el.rep_eq
nat_int.leq_max_sup' nat_int.maximum_in nat_int.un_subset2 rep_non_empty_means_seq)
qed

lemma consec_un_min:"consec i j ⟶ minimum i = minimum (i ⊔ j)"
proof
assume assm:"consec i j"
then have "(∀n m. (n ❙∈ i ∧ m ❙∈ j ⟶ n < m))"
using nat_int.consec_lesser by blast
then have "∀n . (n ❙∈ j ⟶ n > minimum i)"
using assm local.consec_def nat_int.minimum_in by auto
then have 1:"∀n. (n ❙∈ i ⊔ j ⟶ n ≥ minimum i)"
using Rep_nat_int Rep_nat_int_inverse Un_iff assm atLeastAtMost_iff bot_nat_int.rep_eq
less_imp_le_nat local.consec_def local.not_empty_means_seq nat_int.consec_un
nat_int.el.rep_eq nat_int.in_not_in_iff1
by (metis (no_types, lifting) leq_min_inf local.minimum_def)
from assm have "i ⊔ j ≠ ∅"
by (metis bot.extremum_uniqueI nat_int.consec_def nat_int.un_subset2)
then show "minimum i = minimum (i ⊔ j)"
by (metis "1" antisym assm atLeastAtMost_iff leq_min_inf nat_int.consec_def
nat_int.consec_un_element1 nat_int.el.rep_eq nat_int.minimum_def nat_int.minimum_in
rep_non_empty_means_seq)
qed

lemma consec_un_defined:
"consec i j ⟶ (Rep_nat_int (i ⊔ j) ∈ {S . (∃ (m::nat) n . {m..n }=S) })"
using Rep_nat_int by auto

lemma consec_un_min_max:
"consec i j ⟶ Rep_nat_int(i ⊔ j) = {minimum i .. maximum j}"
proof
assume assm:"consec i j"
then have 1:"minimum j = maximum i +1"
have i:"Rep_nat_int i = {minimum i..maximum i}"
by (metis Rep_nat_int_inverse assm nat_int.consec_def nat_int.leq_max_sup' nat_int.leq_min_inf'
rep_non_empty_means_seq)
have j:"Rep_nat_int j = {minimum j..maximum j}"
by (metis Rep_nat_int_inverse assm nat_int.consec_def nat_int.leq_max_sup' nat_int.leq_min_inf'
rep_non_empty_means_seq)
show "Rep_nat_int(i ⊔ j) = {minimum i .. maximum j}"
by (metis Rep_nat_int_inverse antisym assm bot.extremum i nat_int.consec_un_max
nat_int.consec_un_min nat_int.leq_max_sup' nat_int.leq_min_inf' nat_int.un_subset1
rep_non_empty_means_seq)
qed

lemma consec_un_equality:
"(consec i j ∧ k ≠ ∅)
⟶( minimum (i ⊔ j) = minimum (k) ∧ maximum (i ⊔ j) = maximum (k))
⟶ i ⊔ j = k"
proof (rule impI)+
assume cons:"consec i j ∧ k ≠ ∅"
assume endpoints:" minimum(i ⊔ j) = minimum(k) ∧ maximum(i ⊔ j) = maximum(k)"
have "Rep_nat_int( i ⊔ j) = {minimum(i ⊔ j)..maximum(i ⊔ j)}"
by (metis cons leq_max_sup leq_min_inf local.consec_def nat_int.consec_un_element2
nat_int.maximum_def nat_int.minimum_def nat_int.non_empty_elem_in rep_non_empty_means_seq)
then have 1:"Rep_nat_int( i ⊔ j) = {minimum(k) .. maximum(k)}"
using endpoints by simp
have "Rep_nat_int( k) = {minimum(k) .. maximum(k)}"
by (metis cons leq_max_sup leq_min_inf nat_int.maximum_def nat_int.minimum_def
rep_non_empty_means_seq)
then  show " i ⊔ j = k" using 1
by (metis Rep_nat_int_inverse)
qed

lemma consec_trans_lesser:
"consec i j ∧ consec j k ⟶ (∀n m. (n ❙∈ i ∧ m ❙∈ k ⟶ n < m))"
proof (rule allI|rule impI)+
assume cons:" consec i j ∧ consec j k"
fix n and m
assume assump:"n ❙∈ i ∧ m ❙∈ k "
have "∀k . k ❙∈ j ⟶ k < m" using consec_lesser assump cons by blast
hence m_greater:"maximum j < m" using cons maximum_in consec_def by blast
then show "n < m"
by (metis assump cons consec_def dual_order.strict_trans nat_int.consec_lesser
nat_int.maximum_in)
qed

lemma consec_inter_empty:"consec i j ⟹ i ⊓ j = ∅"
proof -
assume "consec i j"
then have "i ≠ bot ∧ j ≠ bot ∧ maximum i + 1 = minimum j"
using consec_def by force
then show ?thesis
by (metis (no_types) Rep_nat_int_inverse bot_nat_int_def inf_nat_int.rep_eq int_conseq_seq
nat_int.leq_max_sup nat_int.leq_min_inf nat_int.maximum_def nat_int.minimum_def
nat_int.rep_non_empty_means_seq)
qed

lemma consec_intermediate1:"consec j k ∧ consec i (j ⊔ k) ⟶ consec i j "
proof
assume assm:"consec j k ∧ consec i (j ⊔ k)"
hence min_max_yz:"maximum j +1=minimum k" using consec_def by blast
hence min_max_xyz:"maximum i +1 = minimum (j ⊔ k)"
using consec_def assm by blast
have min_y_yz:"minimum j = minimum (j ⊔ k)"
hence min_max_xy:"maximum i+1 = minimum j"
using min_max_xyz by simp
thus consec_x_y:"consec i j" using assm consec_def by auto
qed

lemma consec_intermediate2:"consec i j ∧ consec (i ⊔ j) k ⟶ consec j k "
proof
assume assm:"consec i j ∧ consec (i ⊔ j) k"
hence min_max_yz:"maximum i +1=minimum j" using consec_def by blast
hence min_max_xyz:"maximum (i ⊔ j) +1 = minimum ( k)"
using consec_def assm by blast
have min_y_yz:"maximum j = maximum (i ⊔ j)"
using assm nat_int.consec_un_max by blast
then have min_max_xy:"maximum j+1 = minimum k"
using min_max_xyz by simp
thus consec_x_y:"consec j k" using assm consec_def by auto
qed

lemma un_assoc: "consec i j ∧ consec j k ⟶ (i ⊔ j) ⊔ k = i ⊔ (j ⊔ k)"
proof
assume assm:"consec i j ∧ consec j k"
from assm have 3:"maximum (i ⊔ j) = maximum j"
using nat_int.consec_un_max by auto
from assm have 4:"minimum (j ⊔ k) = minimum (j)"
using nat_int.consec_un_min by auto
have "i ⊔ j  = Abs_nat_int{minimum i .. maximum j}"
by (metis Rep_nat_int_inverse assm nat_int.consec_un_min_max)
then have 5:"(i ⊔ j) ⊔ k = Abs_nat_int{minimum i .. maximum k}"
by (metis (no_types, hide_lams) "3" Rep_nat_int_inverse antisym assm bot.extremum
nat_int.consec_def nat_int.consec_un_min nat_int.consec_un_min_max nat_int.un_subset1)
have "j ⊔ k = Abs_nat_int{minimum j .. maximum k}"
by (metis Rep_nat_int_inverse assm nat_int.consec_un_min_max)
then have 6:"i ⊔ (j ⊔ k) = Abs_nat_int{minimum i .. maximum k}"
by (metis (no_types, hide_lams) "4" Rep_nat_int_inverse antisym assm bot.extremum
nat_int.consec_def nat_int.consec_un_max nat_int.consec_un_min_max nat_int.un_subset2)
from 5 and 6 show " (i ⊔ j) ⊔ k = i ⊔ (j ⊔ k)" by simp
qed

lemma consec_assoc1:"consec j k ∧ consec i (j ⊔ k) ⟶ consec (i ⊔ j) k "
proof
assume assm:"consec j k ∧ consec i (j ⊔ k)"
hence min_max_yz:"maximum j +1=minimum k" using consec_def by blast
hence min_max_xyz:"maximum i +1 = minimum (j ⊔ k)"
using consec_def assm by blast
have min_y_yz:"minimum j = minimum (j ⊔ k)"
hence min_max_xy:"maximum i+1 = minimum j" using min_max_xyz by simp
hence consec_x_y:"consec i j" using assm _consec_def by auto
hence max_y_xy:"maximum j = maximum (i ⊔ j)" using consec_lesser assm
have none_empty:"i ≠ ∅ ∧ j ≠ ∅ ∧ k ≠ ∅" using assm by (simp add: consec_def)
hence un_non_empty:"i⊔j ≠ ∅"
using bot.extremum_uniqueI consec_x_y nat_int.un_subset2 by force
have max:"maximum (i⊔j) +1 = minimum k"
using min_max_yz max_y_xy by auto
thus "consec (i ⊔ j) k"  using max un_non_empty none_empty consec_def by blast
qed

lemma consec_assoc2:"consec i j ∧ consec (i⊔ j) k ⟶ consec i  (j⊔ k) "
proof
assume assm:"consec i j ∧ consec (i⊔ j) k"
hence consec_y_z:"consec j k" using assm consec_def consec_intermediate2
by blast
hence max_y_xy:"maximum j = maximum (i ⊔ j)"
have min_y_yz:"minimum j = minimum (j ⊔ k)"
have none_empty:"i ≠ ∅ ∧ j ≠ ∅ ∧ k ≠ ∅" using assm by (simp add: consec_def)
then have un_non_empty:"j⊔k ≠ ∅"
by (metis  bot_nat_int.rep_eq Rep_nat_int_inject consec_y_z  less_eq_nat_int.rep_eq
un_subset1 subset_empty)
have max:"maximum (i) +1 = minimum (j⊔ k)"
using assm min_y_yz consec_def by auto
thus "consec i ( j ⊔ k)"  using max un_non_empty none_empty consec_def by blast
qed

lemma consec_assoc_mult:
"(i2=∅∨ consec i1 i2 ) ∧ (i3 =∅ ∨ consec i3 i4) ∧ (consec (i1 ⊔ i2) (i3 ⊔ i4))
⟶ (i1 ⊔ i2) ⊔ (i3 ⊔ i4) = (i1 ⊔ (i2 ⊔ i3)) ⊔ i4"
proof
assume assm:"(i2=∅∨ consec i1 i2 ) ∧ (i3 =∅ ∨ consec i3 i4)
∧ (consec (i1 ⊔ i2) (i3 ⊔ i4))"
hence "(i2=∅∨ consec i1 i2 )" by simp
thus " (i1 ⊔ i2) ⊔ (i3 ⊔ i4) = (i1 ⊔ (i2 ⊔ i3)) ⊔ i4"
proof
assume empty2:"i2 = ∅"
hence only_l1:"(i1 ⊔ i2) = i1" using un_empty_absorb1 by simp
from assm have "(i3 =∅ ∨ consec i3 i4)" by simp
thus " (i1 ⊔ i2) ⊔ (i3 ⊔ i4) = (i1 ⊔ (i2 ⊔ i3)) ⊔ i4"
by (metis Rep_nat_int_inverse assm bot_nat_int.rep_eq empty2 local.union_def
nat_int.consec_intermediate1 nat_int.un_assoc only_l1 sup_bot.left_neutral)
next
assume consec12:" consec i1 i2"
from assm have "(i3 =∅ ∨ consec i3 i4)" by simp
thus " (i1 ⊔ i2) ⊔ (i3 ⊔ i4) = (i1 ⊔ (i2 ⊔ i3)) ⊔ i4"
proof
assume empty3:"i3 = ∅"
hence only_l4:"(i3 ⊔ i4) = i4 " using un_empty_absorb2 by simp
have "(i1 ⊔ (i2 ⊔ i3)) = i1 ⊔ i2" using empty3 by (simp add: un_empty_absorb1)
thus ?thesis by (simp add: only_l4)
next
assume  consec34:" consec i3 i4"
have consec12_3:"consec (i1 ⊔ i2) i3"
using assm consec34 consec_intermediate1 by blast
show ?thesis
by (metis consec12 consec12_3 consec34 consec_intermediate2 un_assoc)
qed
qed
qed

lemma card_subset_le: "i ⊑ i' ⟶ |i| ≤ |i'|"
by (metis bot_nat_int.rep_eq card_mono finite.intros(1) finite_atLeastAtMost
less_eq_nat_int.rep_eq local.card'.rep_eq rep_non_empty_means_seq)

lemma card_subset_less:"(i::nat_int) < i' ⟶ |i|<|i'|"
by (metis bot_nat_int.rep_eq finite.intros(1) finite_atLeastAtMost less_nat_int.rep_eq
local.card'.rep_eq psubset_card_mono rep_non_empty_means_seq)

lemma card_empty_zero:"|∅| = 0"
using Abs_nat_int_inverse empty_type card'.rep_eq bot_nat_int.rep_eq by auto

lemma card_non_empty_geq_one:"i ≠ ∅ ⟷ |i| ≥ 1"
proof
assume "i ≠ ∅"
hence "Rep_nat_int i ≠ {}" by (metis Rep_nat_int_inverse bot_nat_int.rep_eq)
hence "card (Rep_nat_int i) > 0"
by (metis ‹i ≠ ∅› card_0_eq finite_atLeastAtMost gr0I rep_non_empty_means_seq)
thus "|i| ≥ 1" by (simp add: card'_def)
next
assume "|i| ≥ 1" thus "i ≠∅"
using card_empty_zero by auto
qed

lemma card_min_max:"i ≠ ∅ ⟶ |i| = (maximum i - minimum i) + 1"
proof
assume assm:"i ≠ ∅"
then have "Rep_nat_int i = {minimum i .. maximum i}"
by (metis leq_max_sup leq_min_inf nat_int.maximum_def nat_int.minimum_def
rep_non_empty_means_seq)
then have "card (Rep_nat_int i) = maximum i - minimum i + 1"
using Rep_nat_int_inject assm bot_nat_int.rep_eq by fastforce
then show " |i| = (maximum i - minimum i) + 1"  by simp
qed

lemma card_un_add: " consec i j ⟶ |i ⊔ j| = |i| + |j|"
proof
assume assm:"consec i j"
then have 0:"i ⊓ j = ∅"
using nat_int.consec_inter_empty by auto
then have "(Rep_nat_int i) ∩ (Rep_nat_int j) = {}"
by (metis bot_nat_int.rep_eq inf_nat_int.rep_eq)
then have 1:
"card((Rep_nat_int i)∪(Rep_nat_int j))=card(Rep_nat_int i)+card(Rep_nat_int j)"
nat_int.card_min_max nat_int.el.rep_eq nat_int.maximum_in nat_int.minimum_in)
then show "|i ⊔ j| = |i| + |j|"
proof -
have f1: "i ≠ ∅ ∧ j ≠ ∅ ∧ maximum i + 1 = minimum j"
using assm nat_int.consec_def by blast
then have f2: "Rep_nat_int i ≠ {}"
using Rep_nat_int_inject bot_nat_int.rep_eq by auto
have "Rep_nat_int j ≠ {}"
using f1 Rep_nat_int_inject bot_nat_int.rep_eq by auto
then show ?thesis
using f2 f1 Abs_nat_int_inverse Rep_nat_int 1 local.union_result
nat_int.union_def nat_int_class.maximum_def nat_int_class.minimum_def
by force
qed
qed

lemma singleton:"|i| = 1 ⟶ (∃n. Rep_nat_int i = {n})"
using card_1_singletonE card'.rep_eq by fastforce

lemma singleton2:" (∃n. Rep_nat_int i = {n}) ⟶ |i| = 1"
using card_1_singletonE card'.rep_eq by fastforce

lemma card_seq:"
∀i .|i| = x ⟶ (Rep_nat_int i = {} ∨ (∃n. Rep_nat_int i = {n..n+(x-1)}))"
proof (induct x)
show IB:
"∀i. |i| = 0 ⟶ (Rep_nat_int i = {} ∨ (∃n. Rep_nat_int i = {n..n+(0-1)}))"
by (metis  card_non_empty_geq_one bot_nat_int.rep_eq  not_one_le_zero)
fix x
assume IH:
"∀i. |i| = x ⟶ Rep_nat_int i = {} ∨ (∃n. Rep_nat_int i = {n..n+(x-1)})"
show   " ∀i. |i| = Suc x ⟶
Rep_nat_int i = {} ∨ (∃n. Rep_nat_int i = {n.. n + (Suc x - 1)})"
proof (rule allI|rule impI)+
fix i
assume assm_IS:"|i| = Suc x"
show " Rep_nat_int i = {} ∨ (∃n. Rep_nat_int i = {n.. n + (Suc x -1)})"
proof (cases "x = 0")
assume "x=0"
hence "|i| = 1"
using assm_IS by auto
then have "∃n'. Rep_nat_int i = {n'}"
using nat_int.singleton by blast
hence "∃n'. Rep_nat_int i = {n'.. n' + (Suc x) -1}"
by (simp add: ‹x = 0›)
thus "Rep_nat_int i = {} ∨ (∃n. Rep_nat_int i = {n.. n + (Suc x - 1)})"
by simp
next
assume x_neq_0:"x ≠0 "
hence x_ge_0:"x > 0" using gr0I by blast
from assm_IS have i_is_seq:"∃n m. n ≤ m ∧ Rep_nat_int i = {n..m}"
by (metis One_nat_def Suc_le_mono card_non_empty_geq_one le0 rep_non_empty_means_seq)
obtain n and m where seq_def:" n  ≤ m ∧ Rep_nat_int i = {n..m}"
using i_is_seq by auto
have n_le_m:"n < m"
proof (rule ccontr)
assume "¬n < m"
hence "n = m" by (simp add: less_le seq_def)
hence "Rep_nat_int i = {n}" by (simp add: seq_def)
hence "x = 0" using assm_IS card'.rep_eq by auto
thus False by (simp add: x_neq_0)
qed
hence "n ≤ (m-1)" by simp
obtain i' where  i_def:"i' = Abs_nat_int {n..m-1}" by blast
then have card_i':"|i'| = x"
using assm_IS leq_nat_non_empty n_le_m
nat_int_class.card_min_max nat_int_class.leq_max_sup' nat_int_class.leq_min_inf'
seq_def by auto
hence "Rep_nat_int i' = {} ∨ (∃n. Rep_nat_int i' = {n.. n + (x - 1)})"
using IH by auto
hence " (∃n. Rep_nat_int i' = {n.. n + (x - 1)})" using x_neq_0
using card.empty card_i' card'.rep_eq by auto
hence "m-1 = n + x -1" using assm_IS card'.rep_eq seq_def by auto
hence "m = n +x" using n_le_m x_ge_0 by linarith
hence "( Rep_nat_int i = {n.. n + (Suc x -1) })" using seq_def by (simp )
hence "∃n. (Rep_nat_int i = {n.. n + (Suc x -1) })" ..
then show "Rep_nat_int i = {} ∨ (∃n. Rep_nat_int i ={n.. n + (Suc x-1)})"
by blast
qed
qed
qed

lemma rep_single: "Rep_nat_int (Abs_nat_int {m..m}) = {m}"

lemma chop_empty_right: "∀i. N_Chop(i,i,∅)"
using bot_nat_int.abs_eq nat_int.inter_empty1 nat_int.nchop_def nat_int.un_empty_absorb1
by auto

lemma chop_empty_left: "∀i. N_Chop(i, ∅, i)"
using bot_nat_int.abs_eq nat_int.inter_empty2 nat_int.nchop_def nat_int.un_empty_absorb2
by auto

lemma chop_empty : "N_Chop(∅,∅,∅)"

lemma chop_always_possible:"∀i.∃ j k. N_Chop(i,j,k)"
by (metis  chop_empty_right)

lemma chop_add1: "N_Chop(i,j,k) ⟶ |i| = |j| + |k|"
using card_empty_zero card_un_add un_empty_absorb1 un_empty_absorb2 nchop_def by auto

lemma chop_add2:"|i| = x+y ⟶ (∃ j k. N_Chop(i,j,k) ∧ |j|=x ∧ |k|=y)"
proof
assume assm:"|i| = x+y"
show "(∃ j k. N_Chop(i,j,k) ∧ |j|=x ∧ |k|=y)"
proof (cases "x+y = 0")
assume "x+y =0"
then show "∃ j k. N_Chop(i,j,k) ∧ |j|=x ∧ |k|=y"
using assm chop_empty_left nat_int.chop_add1 by fastforce
next
assume "x+y ≠ 0"
show "∃ j k. N_Chop(i,j,k) ∧ |j|=x ∧ |k|=y"
proof (cases "x = 0")
assume x_eq_0:"x=0"
then show "∃ j k. N_Chop(i,j,k) ∧ |j|=x ∧ |k|=y"
using assm nat_int.card_empty_zero nat_int.chop_empty_left by auto
next
assume x_neq_0:"x ≠0"
show "∃ j k. N_Chop(i,j,k) ∧ |j|=x ∧ |k|=y"
proof (cases "y = 0")
assume y_eq_0:"y=0"
then show "∃ j k. N_Chop(i,j,k) ∧ |j|=x ∧ |k|=y"
using assm nat_int.card_empty_zero nat_int.chop_empty_right by auto
next
assume y_neq_0:"y ≠ 0"
have rep_i:"∃n. Rep_nat_int i = {n..n + (x+y)-1}"
using assm card'.rep_eq card_seq x_neq_0 by fastforce
obtain n where n_def:"Rep_nat_int i = {n..n + (x+y) -1}"
using rep_i by auto
have n_le:"n ≤ n+(x-1)" by simp
have x_le:"n+(x) ≤ n + (x+y)-1" using y_neq_0 by linarith
obtain j  where j_def:" j = Abs_nat_int {n..n+(x-1)}" by blast
from n_le have j_in_type:
"{n..n+(x-1)} ∈ {S . (∃ (m::nat) n . m ≤ n ∧ {m..n }=S) ∨ S={}}"
by blast
obtain k where k_def:" k =Abs_nat_int {n+x..n+(x+y)-1}" by blast
from x_le have k_in_type:
"{n+x..n+(x+y)-1} ∈ {S.(∃ (m::nat) n . m ≤ n ∧ {m..n }=S) ∨ S={}}"
by blast
have consec: "consec j k"
leq_max_sup' leq_min_inf' leq_nat_non_empty neq0_conv x_le x_neq_0)
have union:"i = j ⊔ k"
by (metis Rep_nat_int_inverse consec j_def k_def n_def n_le nat_int.consec_un_min_max
nat_int.leq_max_sup' nat_int.leq_min_inf' x_le)
have disj:"j ⊓ k = ∅" using consec by (simp add: consec_inter_empty)
have chop:"N_Chop(i,j,k)" using consec union disj nchop_def by simp
have card_j:"|j| = x"
using Abs_nat_int_inverse j_def n_le card'.rep_eq x_neq_0 by auto
have card_k:"|k| = y"
using Abs_nat_int_inverse k_def x_le card'.rep_eq x_neq_0 y_neq_0 by auto
have "N_Chop(i,j,k) ∧ |j| = x ∧ |k| = y" using chop card_j card_k by blast
then show "∃ j k. N_Chop(i,j,k) ∧ |j|=x ∧ |k|=y" by blast
qed
qed
qed
qed

lemma chop_single:"(N_Chop(i,j,k) ∧ |i| = 1) ⟶ ( |j| =0 ∨ |k|=0)"

lemma chop_leq_max:"N_Chop(i,j,k) ∧ consec j k ⟶
(∀n . n ∈ Rep_nat_int i ∧ n ≤ maximum j ⟶ n ∈ Rep_nat_int j)"
by (metis Un_iff le_antisym less_imp_le_nat nat_int.consec_def nat_int.consec_lesser
nat_int.consec_un nat_int.el.rep_eq nat_int.maximum_in nat_int.nchop_def
nat_int.not_in.rep_eq)

lemma chop_geq_min:"N_Chop(i,j,k) ∧ consec j k ⟶
(∀n . n ∈ Rep_nat_int i ∧ minimum k ≤ n ⟶ n ∈ Rep_nat_int k)"
by (metis atLeastAtMost_iff bot_nat_int.rep_eq equals0D leq_max_sup leq_min_inf
nat_int.consec_def nat_int.consec_un_max nat_int.maximum_def nat_int.minimum_def
nat_int.nchop_def rep_non_empty_means_seq)

lemma chop_min:"N_Chop(i,j,k) ∧ consec j k ⟶ minimum i = minimum j"
using nat_int.consec_un_min nat_int.nchop_def by auto

lemma chop_max:"N_Chop(i,j,k) ∧ consec j k ⟶ maximum i = maximum k"
using nat_int.consec_un_max nat_int.nchop_def by auto

lemma chop_assoc1:
"N_Chop(i,i1,i2) ∧ N_Chop(i2,i3,i4)
⟶ (N_Chop(i, i1 ⊔ i3, i4) ∧ N_Chop(i1 ⊔ i3, i1, i3))"
proof
assume assm:"N_Chop(i,i1,i2) ∧ N_Chop(i2,i3,i4)"
then have chop_def:"(i =  i1 ⊔ i2   ∧
(i1 = ∅ ∨  i2 = ∅ ∨ ( consec i1 i2)))"
using nchop_def by blast
hence "(i1 = ∅ ∨  i2 = ∅ ∨ ( consec i1 i2))" by simp
then show "N_Chop(i, i1 ⊔ i3, i4) ∧ N_Chop(i1 ⊔ i3, i1, i3)"
proof
assume empty:"i1 = ∅"
then show "N_Chop(i,i1 ⊔ i3, i4) ∧ N_Chop(i1 ⊔ i3, i1, i3)"
by (simp add: assm chop_def nat_int.chop_empty_left nat_int.un_empty_absorb2)
next
assume "i2 = ∅ ∨ ( consec i1 i2)"
then show "N_Chop(i, i1 ⊔ i3, i4)∧ N_Chop(i1 ⊔ i3, i1, i3)"
proof
assume empty:"i2 = ∅"
then show "N_Chop(i, i1 ⊔ i3, i4)∧ N_Chop(i1 ⊔ i3, i1, i3)"
by (metis assm bot.extremum_uniqueI nat_int.chop_empty_right nat_int.nchop_def
nat_int.un_empty_absorb2 nat_int.un_subset1)
next
assume " consec i1 i2"
then have consec_i1_i2:"i1 ≠∅ ∧ i2 ≠∅ ∧ maximum i1 +1 = minimum i2"
using consec_def by blast
from assm have "i3 = ∅ ∨ i4 = ∅ ∨ consec i3 i4"
using nchop_def by blast
then show "N_Chop(i, i1 ⊔ i3, i4)∧ N_Chop(i1 ⊔ i3, i1, i3)"
proof
assume i3_empty:"i3 = ∅"
then show "N_Chop(i, i1 ⊔ i3, i4)∧ N_Chop(i1 ⊔ i3, i1, i3)"
using assm nat_int.chop_empty_right nat_int.nchop_def nat_int.un_empty_absorb2
by auto
next
assume "i4 = ∅ ∨ consec i3 i4"
then show "N_Chop(i, i1 ⊔ i3, i4)∧ N_Chop(i1 ⊔ i3, i1, i3)"
proof
assume i4_empty:"i4 = ∅"
then show "N_Chop(i, i1 ⊔ i3, i4)∧ N_Chop(i1 ⊔ i3, i1, i3)"
using assm nat_int.chop_empty_right nat_int.nchop_def by auto
next
assume consec_i3_i4:"consec i3 i4"
then show "N_Chop(i, i1 ⊔ i3, i4)∧ N_Chop(i1 ⊔ i3, i1, i3)"
by (metis ‹consec i1 i2› assm nat_int.consec_assoc1 nat_int.consec_intermediate1
nat_int.nchop_def nat_int.un_assoc)
qed
qed
qed
qed
qed

lemma chop_assoc2:
"N_Chop(i,i1,i2) ∧ N_Chop(i1,i3,i4)
⟶ N_Chop(i, i3, i4 ⊔ i2) ∧ N_Chop(i4 ⊔ i2, i4,i2)"
proof
assume assm: "N_Chop(i,i1,i2) ∧ N_Chop(i1,i3,i4)"
hence "(i1 = ∅ ∨  i2 = ∅ ∨ ( consec i1 i2))"
using nchop_def by blast
then show "N_Chop(i, i3, i4 ⊔ i2)∧ N_Chop(i4 ⊔ i2, i4,i2)"
proof
assume i1_empty:"i1 = ∅"
then show "N_Chop(i, i3, i4 ⊔ i2)∧ N_Chop(i4 ⊔ i2, i4,i2)"
by (metis assm nat_int.chop_empty_left nat_int.consec_un_not_elem1 nat_int.in_not_in_iff1
nat_int.nchop_def nat_int.non_empty_elem_in nat_int.un_empty_absorb1)
next
assume "i2 = ∅ ∨ consec i1 i2"
then show "N_Chop(i, i3, i4 ⊔ i2)∧ N_Chop(i4 ⊔ i2, i4,i2)"
proof
assume i2_empty:"i2=∅"
then show "N_Chop(i, i3, i4 ⊔ i2)∧ N_Chop(i4 ⊔ i2, i4,i2)"
using assm nat_int.chop_empty_right nat_int.nchop_def by auto
next
assume consec_i1_i2:"consec i1 i2"
from assm have "(i3 = ∅ ∨  i4 = ∅ ∨ ( consec i3 i4))"
then show "N_Chop(i, i3, i4 ⊔ i2)∧ N_Chop(i4 ⊔ i2, i4,i2)"
proof
assume i3_empty:"i3=∅"
then show "N_Chop(i, i3, i4 ⊔ i2)∧ N_Chop(i4 ⊔ i2, i4,i2)"
using assm nat_int.chop_empty_left nat_int.nchop_def by auto
next
assume " i4 = ∅ ∨ ( consec i3 i4)"
then show "N_Chop(i, i3, i4 ⊔ i2)∧ N_Chop(i4 ⊔ i2, i4,i2)"
proof
assume i4_empty:"i4=∅"
then show "N_Chop(i, i3, i4 ⊔ i2)∧ N_Chop(i4 ⊔ i2, i4,i2)"
using assm nat_int.nchop_def nat_int.un_empty_absorb1 nat_int.un_empty_absorb2
by auto
next
assume consec_i3_i4:"consec i3 i4"
then show "N_Chop(i, i3, i4 ⊔ i2)∧ N_Chop(i4 ⊔ i2, i4,i2)"
by (metis assm consec_i1_i2 nat_int.consec_assoc2 nat_int.consec_intermediate2
nat_int.nchop_def nat_int.un_assoc)
qed
qed
qed
qed
qed

lemma chop_subset1:"N_Chop(i,j,k) ⟶ j ⊑ i"
using nat_int.chop_empty_right nat_int.nchop_def nat_int.un_subset1 by auto

lemma chop_subset2:"N_Chop(i,j,k) ⟶ k ⊑ i"
using nat_int.chop_empty_left nat_int.nchop_def nat_int.un_subset2 by auto

end
end


# Theory RealInt

(*  Title:      RealInt.thy

Closed, non-empty intervals based on real numbers. Defines functions left, right
to refer to the left (resp. right) border of an interval.

Defines a length function as the difference between left and right border
and a function to shift an interval by a real value (i.e., the value is added
to both borders).

Instantiates "order", as a notion of sub-intervals.

Also contains a "chopping" predicate R_Chop(r,s,t): r can be divided into
sub-intervals s and t.
*)

section ‹Closed Real-valued Intervals›

text‹We define a type for real-valued intervals. It consists of pairs of real numbers, where
the first is lesser or equal to the second. Both endpoints are understood to be part of
the interval, i.e., the intervals are closed. This also implies that we do not
consider empty intervals.

We define a measure on these intervals as the difference between the left and
right endpoint. In addition, we introduce a notion of shifting an interval by
a real value $$x$$. Finally, an interval $$r$$ can be chopped into $$s$$ and
$$t$$, if the left endpoint of $$r$$ and $$s$$ as well as the right endpoint
of $$r$$ and $$t$$ coincides, and if the right endpoint of $$s$$ is
the left endpoint of $$t$$.
›

theory RealInt
imports HOL.Real
begin

typedef real_int = "{r::(real*real) . fst r ≤ snd r}"
by auto
setup_lifting type_definition_real_int

lift_definition left::"real_int ⇒ real" is fst proof - qed
lift_definition right::"real_int ⇒ real" is snd proof - qed

lemmas[simp] = left.rep_eq right.rep_eq

locale real_int
interpretation real_int_class?: real_int .

context real_int
begin

definition length :: "real_int ⇒ real" ("∥_∥" 70)
where "∥r∥ ≡ right r - left r"

definition shift::"real_int ⇒ real ⇒ real_int" (" shift _ _")
where "(shift r x) = Abs_real_int(left r +x, right r +x)"

definition R_Chop :: "real_int ⇒ real_int ⇒ real_int ⇒ bool" ("R'_Chop'(_,_,_')" 51)
where rchop_def :
"R_Chop(r,s,t) ==  left r  = left s ∧ right s = left t ∧ right r =  right t"

end

text ‹The intervals defined in this way allow for the definition of an order:
the subinterval relation.›

instantiation real_int :: order
begin
definition "less_eq_real_int r s ≡ (left r ≥ left s) ∧ (right r ≤ right s)"
definition "less_real_int r s ≡ (left r ≥ left s) ∧ (right r ≤ right s)
∧  ¬((left s ≥ left r) ∧ (right s ≤ right r))"
instance
proof
fix r s t :: real_int
show "(r < s) = (r ≤ s ∧ ¬ s ≤ r)" using less_eq_real_int_def less_real_int_def by auto
show "r ≤ r" using less_eq_real_int_def by auto
show "r ≤ s ⟹ s ≤ t ⟹ r ≤ t" using less_eq_real_int_def by auto
show "r ≤ s ⟹ s ≤ r ⟹ r = s"
by (metis Rep_real_int_inject left.rep_eq less_le less_eq_real_int_def
not_le prod.collapse right.rep_eq)
qed
end

context real_int
begin

lemma left_leq_right: "left r ≤ right r"
using Rep_real_int left.rep_eq right.rep_eq by auto

lemma length_ge_zero :" ∥r∥ ≥ 0"
using Rep_real_int left.rep_eq right.rep_eq length_def by auto

"left r = left s ∧ right r = right t ∧ right s = left t ⟹ ∥r∥ = ∥s∥ + ∥t∥"

lemma length_zero_iff_borders_eq:"∥r∥ = 0 ⟷ left r = right r"
using length_def by auto

lemma shift_left_eq_right:"left (shift r x) ≤ right (shift r x)"
using left_leq_right .

lemma shift_keeps_length:"∥r∥ = ∥ shift r x∥"
using Abs_real_int_inverse left.rep_eq real_int.length_def length_ge_zero shift_def
right.rep_eq by auto

lemma shift_zero:"(shift r 0) = r"
by (simp add: Rep_real_int_inverse shift_def )

lemma shift_additivity:"(shift r (x+y)) = shift (shift r x) y"
proof -
have 1:"(shift r (x+y)) = Abs_real_int ((left r) +(x+y), (right r)+(x+y))"
using shift_def by auto
have 2:"(left r) +(x+y) ≤ (right r)+(x+y)" using left_leq_right by auto
hence left:"left (shift r (x+y)) = (left r) +(x+y)"
from 2 have right:"right (shift r (x+y)) = (right r) +(x+y)"
have 3:"(shift (shift r x) y) = Abs_real_int(left (shift r x) +y, right(shift r x)+y)"
using shift_def by auto
have l1:"left (shift r x) = left r + x"
using shift_def  Abs_real_int_inverse "2" fstI mem_Collect_eq prod.sel(2) left.rep_eq
by auto
have r1:"right (shift r x) = right r + x"
using shift_def Abs_real_int_inverse "2" fstI mem_Collect_eq prod.sel(2) right.rep_eq
by auto
from 3 and l1 and r1 have
"(shift (shift r x) y) = Abs_real_int(left  r+x+y, right  r+x+y)"
by auto
qed

lemma chop_always_possible: "∀r .∃ s t. R_Chop(r,s,t)"
proof
fix x
obtain s where l:"left x ≤ s  ∧ s ≤ right x"
using left_leq_right by auto
obtain x1  where x1_def:"x1 = Abs_real_int(left x,s)"  by simp
obtain x2 where x2_def:"x2 = Abs_real_int(s, right x)" by simp
have x1_in_type:"(left x, s) ∈ {r :: real*real . fst r ≤ snd r }" using l by auto
have x2_in_type:"(s, right x) ∈ {r :: real*real . fst r ≤ snd r }" using l by auto
have 1:"left x = left x1" using x1_in_type l Abs_real_int_inverse
have 2:"right x1 = s"
using Abs_real_int_inverse x1_def x1_in_type right.rep_eq by auto
have 3:"right x1 = left x2"
using Abs_real_int_inverse x1_def x1_in_type x2_def x2_in_type left.rep_eq by auto
from 1 and 2 and 3 have "R_Chop(x,x1,x2)"
using Abs_real_int_inverse rchop_def snd_conv x2_def x2_in_type by auto
then show "∃x1 x2. R_Chop(x,x1,x2)" by blast
qed

lemma chop_singleton_right: "∀r.∃ s. R_Chop(r,r,s)"
proof
fix x
obtain y where  "y =  Abs_real_int(right x, right x)" by simp
then have "R_Chop(x,x,y)"
then show "∃y. R_Chop(x,x,y)" by blast
qed

lemma chop_singleton_left: "∀r.∃ s. R_Chop(r,s,r)"
proof
fix x
obtain y where  "y =  Abs_real_int(left x, left x)" by simp
then have "R_Chop(x,y,x)"
then show "∃y. R_Chop(x,y,x)" by blast
qed

lemma chop_add_length:"R_Chop(r,s,t) ⟹ ∥r∥ = ∥s∥ + ∥t∥"

lemma chop_add_length_ge_0:"R_Chop(r,s,t) ∧ ∥s∥ > 0 ∧ ∥t∥>0 ⟶ ∥r∥>0"

lemma chop_dense : "∥r∥ > 0 ⟶ (∃ s t. R_Chop(r,s,t) ∧ ∥s∥>0 ∧ ∥t∥>0)"
proof
assume "∥r∥ > 0"
have ff1: " left r < right r"
using Rep_real_int ‹0 < ∥r∥› length_def by auto
have l_in_type:"(left r, right r) ∈ {r :: real*real . fst r ≤ snd r }"
using Rep_real_int by auto
obtain x where  x_def:" x  = (left r + right r) / 2"
by blast
have x_gr:"x > left r" using ff1 field_less_half_sum x_def by blast
have x_le:"x < right r" using ff1 x_def by (simp add: field_sum_of_halves)
obtain s where s_def:"s = Abs_real_int(left r, x)"  by simp
obtain t where t_def:"t = Abs_real_int(x, right r)"  by simp
have s_in_type:"(left r, x) ∈ {r :: real*real . fst r ≤ snd r }"
using x_def x_le by auto
have t_in_type:"(x, right r) ∈ {r :: real*real . fst r ≤ snd r }"
using x_def x_gr by auto
have s_gr_0:"∥s∥ > 0"
using Abs_real_int_inverse s_def length_def x_gr by auto
have t_gr_0:"∥t∥ > 0"
using Abs_real_int_inverse t_def length_def x_le by auto
have "R_Chop(r,s,t)"
using Abs_real_int_inverse s_def s_in_type t_def t_in_type rchop_def by auto
hence "R_Chop(r,s,t) ∧ ∥s∥>0 ∧ ∥t∥>0"
using s_gr_0 t_gr_0 by blast
thus "∃ s t. R_Chop(r,s,t) ∧ ∥s∥>0 ∧ ∥t∥>0" by blast
qed

lemma chop_assoc1:
"R_Chop(r,r1,r2) ∧ R_Chop(r2,r3,r4)
⟶ R_Chop(r, Abs_real_int(left r1, right r3), r4)
∧ R_Chop(Abs_real_int(left r1, right r3), r1,r3)"
proof
assume assm: "R_Chop(r,r1,r2) ∧ R_Chop(r2,r3,r4)"
let ?y1 = " Abs_real_int(left r1, right r3)"
have l1:"left r1 = left ?y1"
by (metis  Abs_real_int_inverse assm fst_conv left.rep_eq mem_Collect_eq
order_trans real_int.left_leq_right real_int.rchop_def snd_conv)
have r1:"right ?y1 = right r3"
by (metis  Rep_real_int_cases Rep_real_int_inverse assm fst_conv mem_Collect_eq
order_trans real_int.left_leq_right real_int.rchop_def right.rep_eq snd_conv)
have g1:"R_Chop(r, ?y1, r4)" using assm  rchop_def r1 l1 by simp
have g2:"R_Chop(?y1, r1,r3)" using assm  rchop_def r1 l1 by simp
show "R_Chop(r, ?y1, r4) ∧ R_Chop(?y1, r1,r3)" using g1 g2 by simp
qed

lemma chop_assoc2:
"R_Chop(r,r1,r2) ∧ R_Chop(r1,r3,r4)
⟶ R_Chop(r,r3, Abs_real_int(left r4, right r2))
∧ R_Chop(Abs_real_int(left r4, right r2), r4,r2)"
proof
assume assm: "R_Chop(r,r1,r2) ∧ R_Chop(r1,r3,r4)"
let ?y1 = " Abs_real_int(left r4, right r2)"
have "left ?y1 ≤ right ?y1"
using real_int.left_leq_right by blast
have f1: "left r4 = right r3"
using assm real_int.rchop_def by force
then have right:"right r3 ≤ right r2"
by (metis (no_types) assm order_trans real_int.left_leq_right real_int.rchop_def)
then have l1:"left ?y1 = left r4" using f1 by (simp add: Abs_real_int_inverse)
have r1:"right ?y1 = right r2"
using Abs_real_int_inverse right f1 by auto
have g1:"R_Chop(r, r3, ?y1)" using assm  rchop_def r1 l1 by simp
have g2:"R_Chop(?y1, r4,r2)" using assm  rchop_def r1 l1 by simp
show "R_Chop(r, r3, ?y1) ∧ R_Chop(?y1, r4,r2)" using g1 g2 by simp
qed

lemma chop_leq1:"R_Chop(r,s,t) ⟶ s ≤ r"
by (metis (full_types) less_eq_real_int_def order_refl real_int.left_leq_right real_int.rchop_def)

lemma chop_leq2:"R_Chop(r,s,t) ⟶ t ≤ r"
by (metis (full_types) less_eq_real_int_def order_refl real_int.left_leq_right real_int.rchop_def)

lemma chop_empty1:"R_Chop(r,s,t) ∧ ∥s∥ = 0 ⟶ r = t "
by (metis (no_types, hide_lams) Rep_real_int_inject left.rep_eq prod.collapse
real_int.length_zero_iff_borders_eq real_int.rchop_def right.rep_eq)

lemma chop_empty2:"R_Chop(r,s,t) ∧ ∥t∥ = 0 ⟶ r = s "
by (metis (no_types, hide_lams) Rep_real_int_inject left.rep_eq prod.collapse
real_int.length_zero_iff_borders_eq real_int.rchop_def right.rep_eq)

end
(*lemmas[simp] = length_dict *)

end


# Theory Cars

(*  Title:      Cars.thy

A countably infinite type to denote cars in the model of HMLSL.
*)

section‹Cars›

text ‹
We define a type to refer to cars. For simplicity, we assume that (countably)
infinite cars exist.
›

theory Cars
imports Main
begin

text ‹
The type of cars consists of the natural numbers. However, we do not
›

typedef cars = "{n::nat. True} " by blast

locale cars
begin

text ‹
For the construction of possible counterexamples, it is beneficial to
prove that at least two cars exist. Furthermore, we show that there indeed
exist infinitely many cars.
›

lemma at_least_two_cars_exists:"∃c d ::cars . c≠d"
proof -
have "(0::nat) ≠ 1" by simp
then have "Abs_cars (0::nat) ≠ Abs_cars(1) " by (simp add:Abs_cars_inject)
thus ?thesis by blast
qed

lemma infinite_cars:"infinite {c::cars . True}"
proof -
have "infinite {n::nat. True}" by auto
then show ?thesis
by (metis UNIV_def finite_imageI type_definition.Rep_range type_definition_cars)
qed

end
end


# Theory Traffic

(*  Title:      Traffic.thy

Defines a type for traffic snapshots. Consists of six elements:
pos: positions of cars
res: reservations of cars
clm: claims of cars
dyn: current dynamic behaviour of cars
physical_size: the real sizes of cars
braking_distance: braking distance each car needs in emergency

Definitions for transitions between traffic snapshots.
*)

section‹Traffic Snapshots›
text‹
Traffic snapshots define the spatial and dynamical arrangement of cars
on the whole of the motorway at a single point in time. A traffic snapshot
consists of several functions assigning spatial properties and dynamical
behaviour to each car. The functions are named as follows.
\begin{itemize}
\item pos: positions of cars
\item res: reservations of cars
\item clm: claims of cars
\item dyn: current dynamic behaviour of cars
\item physical\_size: the real sizes of cars
\item braking\_distance: braking distance each car needs in emergency
\end{itemize}
›

theory Traffic
imports NatInt RealInt Cars
begin

type_synonym lanes = nat_int
type_synonym extension = real_int

text ‹Definition of the type of traffic snapshots.
The constraints on the different functions are the \emph{sanity conditions}
of traffic snapshots.›

typedef traffic =
"{ts :: (cars⇒real)*(cars⇒lanes)*(cars⇒lanes)*(cars⇒real⇒real)*(cars⇒real)*(cars⇒real).
(∀c. ((fst (snd ts))) c ⊓ ((fst (snd (snd ts)))) c = ∅ )  ∧
(∀c. |(fst (snd ts)) c| ≥ 1) ∧
(∀c. |(fst (snd ts)) c| ≤ 2) ∧
(∀c. |(fst (snd (snd ts)) c)| ≤ 1) ∧
(∀c. |(fst (snd ts)) c| + |(fst (snd (snd ts))) c| ≤ 2) ∧
(∀c. (fst(snd(snd (ts)))) c ≠ ∅ ⟶
(∃ n. Rep_nat_int(fst (snd ts) c)∪Rep_nat_int(fst (snd (snd ts)) c)
= {n, n+1})) ∧
(∀c . fst (snd (snd (snd (snd (ts))))) c > 0) ∧
(∀c.  snd (snd (snd (snd (snd (ts))))) c > 0)
} "
proof -
let ?type =
"{ts ::(cars⇒real)*(cars⇒lanes)*(cars⇒lanes)*(cars⇒real⇒real)*(cars⇒real)*(cars⇒real).
(∀c. ((fst (snd ts))) c ⊓ ((fst (snd (snd ts)))) c = ∅ )  ∧
(∀c. |(fst (snd ts)) c| ≥ 1) ∧
(∀c. |(fst (snd ts)) c| ≤ 2) ∧
(∀c. |(fst (snd (snd ts)) c)| ≤ 1) ∧
(∀c. |(fst (snd ts)) c| + |(fst (snd (snd ts))) c| ≤ 2) ∧
(∀c. (fst(snd(snd (ts)))) c ≠ ∅ ⟶
(∃ n. Rep_nat_int(fst (snd ts) c)∪Rep_nat_int(fst (snd (snd ts)) c)
= {n, n+1})) ∧
(∀c . fst (snd (snd (snd (snd (ts))))) c > 0) ∧
(∀c.  snd (snd (snd (snd (snd (ts))))) c > 0)
}"
obtain pos where sp_def:"∀c::cars. pos c = (1::real)" by force
obtain re where re_def:"∀c::cars. re c = Abs_nat_int {1}" by force
obtain cl where cl_def:"∀c::cars. cl c = ∅" by force
obtain dyn where dyn_def:"∀c::cars. ∀x::real . (dyn c) x  = (0::real)"  by force
obtain ps where ps_def :"∀c::cars . ps c = (1::real)" by force
obtain sd where sd_def:"∀c::cars . sd c = (1::real)" by force
obtain ts where ts_def:"ts =  (pos,re,cl, dyn, ps, sd)" by simp

have disj:"∀c .((re c) ⊓ (cl c) = ∅)"
have re_geq_one:"∀c. |re c| ≥ 1"
have re_leq_two:"∀c. |re c| ≤ 2"
using re_def nat_int.rep_single by auto
have cl_leq_one:"∀c. |cl c| ≤ 1"
using nat_int.card_empty_zero cl_def by auto
have add_leq_two:"∀c . |re c| + |cl c| ≤ 2"
using nat_int.card_empty_zero cl_def re_leq_two by (simp )
have consec_re:" ∀c. |(re c)| =2 ⟶ (∃n . Rep_nat_int (re c) = {n,n+1})"
have  clNextRe :
"∀c. ((cl c) ≠ ∅ ⟶ (∃ n. Rep_nat_int (re c) ∪ Rep_nat_int (cl c) = {n, n+1}))"
from dyn_def have dyn_geq_zero:"∀c. ∀x. dyn(c) x ≥ 0"
by auto
from ps_def have ps_ge_zero:"∀c. ps c > 0" by auto
from sd_def have sd_ge_zero:"∀c. sd c > 0" by auto

have "ts∈?type"
using sp_def re_def cl_def disj re_geq_one re_leq_two cl_leq_one add_leq_two
consec_re ps_def sd_def ts_def by auto
thus ?thesis by blast
qed

locale traffic
begin

notation nat_int.consec ("consec")

text‹For brevity, we define names for the different functions
within a traffic snapshot.›

definition pos::"traffic ⇒ (cars ⇒ real)"
where "pos ts ≡ fst (Rep_traffic ts)"

definition res::"traffic ⇒ (cars ⇒ lanes)"
where "res ts ≡ fst (snd (Rep_traffic ts))"

definition clm ::"traffic ⇒ (cars ⇒ lanes)"
where "clm ts ≡ fst (snd (snd (Rep_traffic ts)))"

definition dyn::"traffic ⇒ (cars ⇒ (real⇒ real))"
where "dyn ts ≡ fst (snd (snd (snd (Rep_traffic ts))))"

definition physical_size::"traffic ⇒ (cars ⇒ real)"
where "physical_size ts ≡ fst (snd (snd (snd (snd (Rep_traffic ts)))))"

definition braking_distance::"traffic ⇒ (cars ⇒ real)"
where "braking_distance ts ≡ snd (snd (snd (snd (snd (Rep_traffic ts)))))"

text ‹
It is helpful to be able to refer to the sanity conditions of a traffic
snapshot via lemmas, hence we prove that the sanity conditions hold
for each traffic snapshot.
›

lemma disjoint: "(res ts c) ⊓ (clm ts c) = ∅"
using Rep_traffic res_def clm_def   by auto

lemma atLeastOneRes: "1 ≤ |res ts c|"
using Rep_traffic  res_def by auto

lemma atMostTwoRes:" |res ts c| ≤ 2"
using Rep_traffic  res_def  by auto

lemma  atMostOneClm: "|clm ts c| ≤ 1"
using Rep_traffic  clm_def  by auto

lemma atMostTwoLanes: "|res ts c| +|clm ts c| ≤ 2"
using Rep_traffic  res_def clm_def  by auto

lemma  consecutiveRes:" |res ts  c| =2 ⟶ (∃n . Rep_nat_int (res ts c) = {n,n+1})"
proof
assume assump:"|res ts  c| =2"
then have not_empty:"(res ts c) ≠ ∅"
from assump and card_seq
have "Rep_nat_int (res ts  c) = {} ∨ (∃n . Rep_nat_int (res ts c) = {n,n+1})"
by (metis add_diff_cancel_left' atLeastAtMost_singleton insert_is_Un nat_int.un_consec_seq
with assump show "(∃n . Rep_nat_int (res ts c) = {n,n+1})"
using Rep_nat_int_inject bot_nat_int.rep_eq card_non_empty_geq_one
by (metis not_empty)
qed

lemma clmNextRes :
"(clm ts c) ≠ ∅ ⟶ (∃ n. Rep_nat_int(res ts c) ∪ Rep_nat_int(clm ts c) = {n, n+1})"
using Rep_traffic res_def clm_def by auto

lemma psGeZero:"∀c. (physical_size ts c > 0)"
using Rep_traffic physical_size_def by auto

lemma sdGeZero:"∀c. (braking_distance ts c > 0)"
using Rep_traffic braking_distance_def by auto

text ‹
While not a sanity condition directly, the following lemma helps to establish
general properties of HMLSL later on. It is a consequence of clmNextRes.
›

lemma clm_consec_res:
"(clm ts) c ≠ ∅ ⟶ consec (clm ts c) (res ts c) ∨ consec (res ts c) (clm ts c)"
proof
assume assm:"clm ts c ≠∅"
hence adj:"(∃ n. Rep_nat_int(res ts c) ∪ Rep_nat_int(clm ts c) = {n, n+1})"
using clmNextRes by blast
obtain n where n_def:"Rep_nat_int(res ts c)∪Rep_nat_int(clm ts c) = {n, n+1}"
have disj:"res ts c ⊓ clm ts c = ∅" using disjoint by blast
from n_def and disj
have "(n ❙∈ res ts c ∧ n ❙∉ clm ts c) ∨ (n ❙∈ clm ts c ∧ n ❙∉ res ts c)"
by (metis UnE bot_nat_int.rep_eq disjoint_insert(1) el.rep_eq inf_nat_int.rep_eq
insertI1 insert_absorb not_in.rep_eq)
thus "consec (clm ts c) (res ts c) ∨ consec (res ts c) (clm ts c)"
proof
assume n_in_res: "n ❙∈ res ts c ∧  n ❙∉ clm ts c"
hence suc_n_in_clm:"n+1 ❙∈ clm ts c"
by (metis UnCI assm el.rep_eq in_not_in_iff1 insert_iff n_def non_empty_elem_in
singletonD)
have "Rep_nat_int (res ts c) ≠ {n, n + 1}"
by (metis assm disj n_def inf_absorb1 inf_commute less_eq_nat_int.rep_eq
sup.cobounded2)
then have suc_n_not_in_res:"n+1 ❙∉ res ts c"
using n_def n_in_res nat_int.el.rep_eq nat_int.not_in.rep_eq
by auto
from n_in_res have n_not_in_clm:"n ❙∉ clm ts c" by blast
have max:"nat_int.maximum (res ts c) = n"
using n_in_res suc_n_not_in_res nat_int.el.rep_eq nat_int.not_in.rep_eq n_def
nat_int.maximum_in nat_int.non_empty_elem_in inf_sup_aci(4)
by fastforce
have min:"nat_int.minimum (clm ts c) = n+1"
using suc_n_in_clm n_not_in_clm nat_int.el.rep_eq nat_int.not_in.rep_eq
n_def nat_int.minimum_in nat_int.non_empty_elem_in  using inf_sup_aci(4)
not_in.rep_eq by fastforce
show ?thesis
using assm max min n_in_res nat_int.consec_def nat_int.non_empty_elem_in
by auto
next
assume n_in_clm: "n ❙∈ clm ts c ∧ n ❙∉ res ts c "
have suc_n_in_res:"n+1 ❙∈ res ts c"
proof (rule ccontr)
assume "¬n+1 ❙∈ res ts c"
then have "n ❙∈ res ts c "
atMostTwoRes el.rep_eq inf_bot_right inf_sup_absorb insert_not_empty le_antisym
traffic.consecutiveRes)
then show False using n_in_clm
using nat_int.el.rep_eq nat_int.not_in.rep_eq by auto
qed
have max:"nat_int.maximum (clm ts c) = n"
by (metis Rep_nat_int_inverse assm n_in_clm card_non_empty_geq_one
le_antisym nat_int.in_singleton nat_int.maximum_in singleton traffic.atMostOneClm)
have min:"nat_int.minimum (res ts c) = n+1"
by (metis Int_insert_right_if0 Int_insert_right_if1 Rep_nat_int_inverse
bot_nat_int.rep_eq el.rep_eq in_not_in_iff1 in_singleton inf_nat_int.rep_eq
inf_sup_absorb insert_not_empty inter_empty1 minimum_in n_def
n_in_clm suc_n_in_res)
then show ?thesis
using assm max min nat_int.consec_def nat_int.non_empty_elem_in
suc_n_in_res by auto
qed
qed

text ‹We define several possible transitions between traffic snapshots.
Cars may create or withdraw claims and reservations, as long as the sanity conditions
of the traffic snapshots are fullfilled.

In particular, a car can only create
a claim, if it possesses only a reservation on a single lane, and does not
already possess a claim. Withdrawing a claim can be done in any situation.
It only has an effect, if the car possesses a claim. Similarly, the
transition for a car to create a reservation is always possible, but only
changes the spatial situation on the road, if the car already has a claim.
Finally, a car may withdraw its reservation to a single lane, if its
current reservation consists of two lanes.

All of these transitions concern the spatial properties of a single car at a time, i.e.,
for several cars to change their properties, several transitions have to be taken.
›

definition create_claim ::
"traffic⇒cars⇒nat⇒traffic⇒bool" ("_ ❙─c'( _, _ ') ❙→ _" 27)
where "  (ts ❙─c(c,n)❙→ ts')  == (pos ts') = (pos ts)
∧ (res ts') = (res ts)
∧ (dyn ts') = (dyn ts)
∧ (physical_size ts') = (physical_size ts)
∧ (braking_distance ts') = (braking_distance ts)
∧ |clm ts c| = 0
∧ |res ts c| = 1
∧ ((n+1) ❙∈ res ts c ∨ (n-1 ❙∈ res ts c))
∧ (clm ts') = (clm ts)(c:=Abs_nat_int {n})"

definition withdraw_claim ::
"traffic⇒cars ⇒traffic⇒bool" ("_ ❙─wdc'( _ ') ❙→ _" 27)
where "  (ts ❙─wdc(c)❙→ ts')  == (pos ts') = (pos ts)
∧ (res ts') = (res ts)
∧ (dyn ts') = (dyn ts)
∧ (physical_size ts') = (physical_size ts)
∧ (braking_distance ts') = (braking_distance ts)
∧ (clm ts') = (clm ts)(c:=∅)"

definition create_reservation ::
"traffic⇒cars⇒traffic⇒bool" ("_ ❙─r'( _ ') ❙→ _" 27)
where "  (ts ❙─r(c)❙→ ts')  == (pos ts') = (pos ts)
∧ (res ts') = (res ts)(c:=( (res ts c)⊔ (clm ts c) ))
∧ (dyn ts') = (dyn ts)
∧ (clm ts') = (clm ts)(c:=∅)
∧ (physical_size ts') = (physical_size ts)
∧ (braking_distance ts') = (braking_distance ts)"

definition withdraw_reservation ::
"traffic⇒cars⇒nat⇒traffic⇒ bool" ("_ ❙─wdr'( _, _ ') ❙→ _" 27)
where "  (ts ❙─wdr(c,n)❙→ ts')  == (pos ts') = (pos ts)
∧ (res ts') = (res ts)(c:= Abs_nat_int{n} )
∧ (dyn ts') = (dyn ts)
∧ (clm ts') = (clm ts)
∧ (physical_size ts') = (physical_size ts)
∧ (braking_distance ts') = (braking_distance ts)
∧ n ❙∈ (res ts c)
∧ |res ts c| = 2"

text ‹
The following two transitions concern the dynamical behaviour of the cars.
Similar to the spatial properties, a car may change its dynamics, by setting
it to a new function $$f$$ from real to real. Observe that this function is indeed
arbitrary and does not constrain the possible behaviour in any way. However,
this transition allows a car to change the function determining their braking
distance (in fact, all cars are allowed to change this function, if a car changes
sets a new dynamical function). That is, our model describes an over-approximation
of a concrete situation, where the braking distance is determined by the dynamics.

The final transition describes the passing of $$x$$ time units. That is, all cars
update their position according to their current dynamical behaviour. Observe that
this transition requires that the dynamics of each car is at least $$0$$, for each time
point between $$0$$ and $$x$$. Hence, this condition denotes that all cars drive
into the same direction. If the current dynamics of a car violated this constraint,
it would have to reset its dynamics, until time may pass again.
›

definition change_dyn::
"traffic⇒cars⇒(real⇒real)⇒traffic⇒ bool" (" _ ❙─ dyn'(_,_') ❙→ _" 27)
where "(ts ❙─dyn(c, f)❙→ ts') == (pos ts' = pos ts)
∧ (res ts' = res ts)
∧ (clm ts' = clm ts)
∧ (dyn ts' = (dyn ts)(c:= f))
∧ (physical_size ts') = (physical_size ts)"

definition drive::
"traffic⇒real⇒traffic⇒bool" (" _ ❙─ _ ❙→ _" 27)
where "(ts ❙─ x ❙→ ts') == (∀c. (pos ts' c = (pos ts c) + (dyn ts c x)))
∧ (∀ c y. 0 ≤ y ∧ y ≤ x ⟶ dyn ts c y ≥ 0)
∧ (res ts' = res ts)
∧ (clm ts' = clm ts)
∧ (dyn ts' = dyn ts)
∧ (physical_size ts') = (physical_size ts)
∧ (braking_distance ts') = (braking_distance ts)"

text‹
We bundle the dynamical transitions into \emph{evolutions}, since
we will only reason about combinations of the dynamical behaviour.
This fits to the level of abstraction by hiding the dynamics completely
inside of the model.
›

inductive evolve::"traffic ⇒ traffic ⇒ bool" ("_ ❙↝ _")
where refl : "ts ❙↝ ts" |
change: "∃c. ∃f. (ts ❙─dyn(c,f)❙→ts') ⟹ ts' ❙↝ ts'' ⟹ ts ❙↝ ts''" |
drive:  "∃x. x ≥ 0 ∧  ( ts ❙─x❙→ ts') ⟹ ts' ❙↝ ts''    ⟹ ts ❙↝ ts''"

lemma evolve_trans:"(ts0 ❙↝ ts1) ⟹ (ts1 ❙↝ ts2) ⟹ (ts0 ❙↝ ts2)"
proof (induction rule:evolve.induct)
case (refl ts)
then show ?case by simp
next
case (drive ts ts' ts'')
then show ?case by (metis evolve.drive)
next
case (change ts ts' ts'')
then show ?case by (metis evolve.change)
qed

text ‹
For general transition sequences, we introduce \emph{abstract transitions}.
A traffic snapshot $$ts^\prime$$ is reachable from $$ts$$ via an abstract transition,
if there is an arbitrary sequence of transitions from $$ts$$ to $$ts^\prime$$.
›

inductive abstract::"traffic ⇒ traffic ⇒ bool"  ("_ ❙⇒ _") for ts
where refl: "(ts ❙⇒ ts)" |
evolve:"  ts ❙⇒ ts' ⟹ ts' ❙↝ ts''   ⟹ ts ❙⇒ ts''" |
cr_clm:" ts ❙⇒ ts' ⟹∃c. ∃ n.  (ts' ❙─c(c,n)❙→ ts'')     ⟹ ts ❙⇒ ts''" |
wd_clm:"ts ❙⇒ ts'  ⟹ ∃c.  (ts' ❙─wdc(c)❙→ ts'') ⟹  ts ❙⇒ ts''" |
cr_res:"ts ❙⇒ ts' ⟹ ∃c.  (ts' ❙─r(c)❙→ ts'') ⟹  ts ❙⇒ ts''" |
wd_res:"ts ❙⇒ ts' ⟹ ∃c. ∃ n.  (ts' ❙─wdr(c,n)❙→ ts'') ⟹  ts ❙⇒ ts''"

lemma abs_trans:" (ts1 ❙⇒ ts2) ⟹(ts0 ❙⇒ ts1) ⟹ (ts0 ❙⇒ ts2)"
proof (induction  rule:abstract.induct    )
case refl
then show ?case by simp
next
case (evolve ts' ts'')
then show ?case
using traffic.evolve by blast
next
case (cr_clm ts' ts'')
then show ?case
using traffic.cr_clm by blast
next
case (wd_clm ts' ts'')
then show ?case
using traffic.wd_clm by blast
next
case (cr_res ts' ts'')
then show ?case
using traffic.cr_res by blast
next
case (wd_res ts' ts'')
then show ?case
using traffic.wd_res by blast
qed

text ‹
Most properties of the transitions are straightforward. However, to show
that the transition to create a reservation is always possible,
we need to explicitly construct the resulting traffic snapshot. Due
to the size of such a snapshot, the proof is lengthy.
›

lemma create_res_subseteq1:"(ts ❙─r(c)❙→ ts') ⟶ res ts c ⊑ res ts' c "
proof
assume assm:"(ts ❙─r(c)❙→ ts')"
hence "res ts' c = res ts c ⊔ clm ts c" using create_reservation_def
using fun_upd_apply by auto
thus "res ts c ⊑ res ts' c"
by (metis (no_types, lifting) Un_commute clm_consec_res  nat_int.un_subset2
nat_int.union_def nat_int.chop_subset1 nat_int.nchop_def)
qed

lemma create_res_subseteq2:"(ts ❙─r(c)❙→ ts') ⟶ clm ts c ⊑ res ts' c "
proof
assume assm:"(ts ❙─r(c)❙→ ts')"
hence "res ts' c = res ts c ⊔ clm ts c" using create_reservation_def
using fun_upd_apply by auto
thus "clm ts c ⊑ res ts' c"
by (metis Un_commute clm_consec_res disjoint inf_le1 nat_int.un_subset1 nat_int.un_subset2
nat_int.union_def)
qed

lemma create_res_subseteq1_neq:"(ts ❙─r(d)❙→ ts') ∧ d ≠c ⟶ res ts c = res ts' c "
proof
assume assm:"(ts ❙─r(d)❙→ ts') ∧ d ≠c"
thus "res ts c = res ts' c" using create_reservation_def
using fun_upd_apply by auto
qed

lemma create_res_subseteq2_neq:"(ts ❙─r(d)❙→ ts') ∧ d ≠c ⟶ clm ts c= clm ts' c "
proof
assume assm:"(ts ❙─r(d)❙→ ts') ∧ d ≠c"
thus "clm ts c =  clm ts' c" using create_reservation_def
using fun_upd_apply by auto
qed

lemma always_create_res:"∀ts. ∃ts'. (ts ❙─r(c)❙→ ts')"
proof
let ?type =
"{ts ::(cars⇒real)*(cars⇒lanes)*(cars⇒lanes)*(cars⇒real⇒real)*(cars⇒real)*(cars⇒real).
(∀c. ((fst (snd ts))) c ⊓ ((fst (snd (snd ts)))) c = ∅ )  ∧
(∀c. |(fst (snd ts)) c| ≥ 1) ∧
(∀c. |(fst (snd ts)) c| ≤ 2) ∧
(∀c. |(fst (snd (snd ts)) c)| ≤ 1) ∧
(∀c. |(fst (snd ts)) c| + |(fst (snd (snd ts))) c| ≤ 2) ∧
(∀c. (fst(snd(snd (ts)))) c ≠ ∅ ⟶
(∃ n. Rep_nat_int(fst (snd ts) c)∪Rep_nat_int(fst (snd (snd ts)) c)
= {n, n+1})) ∧
(∀c . fst (snd (snd (snd (snd (ts))))) c > 0) ∧
(∀c.  snd (snd (snd (snd (snd (ts))))) c > 0)
}"
fix ts
show " ∃ts'. (ts ❙─r(c)❙→ ts')"
proof (cases "clm ts c = ∅")
case True
obtain ts' where ts'_def:"ts' = ts" by simp
then have "ts ❙─r(c)❙→ ts'"
using create_reservation_def True fun_upd_triv nat_int.un_empty_absorb1
by auto
thus ?thesis ..
next
case False
obtain ts' where ts'_def: "ts'=  (pos ts,
(res ts)(c:=( (res ts c)⊔ (clm ts c) )),
(clm ts)(c:=∅),
(dyn ts), (physical_size ts), (braking_distance ts))"
by blast
have disj:"∀c .(((fst (snd ts'))) c ⊓ ((fst (snd (snd ts')))) c = ∅)"
by (simp add: disjoint nat_int.inter_empty1 ts'_def)
have re_geq_one:"∀d. |fst (snd ts') d| ≥ 1"
proof
fix d
show " |fst (snd ts') d| ≥ 1"
proof (cases "c = d")
case True
then have "fst (snd ts') d = res ts d ⊔ clm ts c"
then have "res ts d ⊑ fst (snd ts') d"
by (metis False True Un_ac(3) nat_int.un_subset1 nat_int.un_subset2
nat_int.union_def traffic.clm_consec_res)
then show ?thesis
by (metis bot.extremum_uniqueI card_non_empty_geq_one traffic.atLeastOneRes)
next
case False
then show ?thesis
using traffic.atLeastOneRes ts'_def by auto
qed
qed
have re_leq_two:"∀c. |(fst (snd ts')) c| ≤ 2"
by (metis (no_types, lifting) Un_commute add.commute
nat_int.union_def False prod.sel(1) prod.sel(2) ts'_def)
have cl_leq_one:"∀c. |(fst (snd (snd ts'))) c| ≤ 1"
using atMostOneClm nat_int.card_empty_zero ts'_def by auto
have add_leq_two:"∀c . |(fst (snd ts')) c| + |(fst (snd (snd ts'))) c| ≤ 2"
fun_upd_apply le_SucE one_add_one prod.sel(1) prod.sel(2) re_leq_two
traffic.atMostTwoLanes ts'_def)
have clNextRe :
"∀c. (((fst (snd (snd ts'))) c) ≠ ∅ ⟶
(∃ n. Rep_nat_int ((fst (snd ts')) c) ∪ Rep_nat_int (fst (snd (snd ts')) c)
= {n, n+1}))"
using clmNextRes ts'_def by auto
have ps_ge_zero: "(∀c . fst (snd (snd (snd (snd (ts'))))) c > 0)"
using ts'_def psGeZero by simp
have sd_ge_zero: "(∀c . snd (snd (snd (snd (snd (ts'))))) c > 0)"
using ts'_def sdGeZero by simp
have ts'_type:
"ts'∈ ?type"
using  ts'_def disj  re_geq_one re_leq_two cl_leq_one add_leq_two
clNextRe mem_Collect_eq  ps_ge_zero  sd_ge_zero by blast
have rep_eq:"Rep_traffic (Abs_traffic ts') = ts'"
using ts'_def ts'_type Abs_traffic_inverse by blast
have sp_eq:"(pos (Abs_traffic ts')) = (pos ts) "
using rep_eq ts'_def Rep_traffic pos_def by auto
have res_eq:"(res  (Abs_traffic ts')) = (res ts)(c:=( (res ts c)⊔ (clm ts c) ))"
using Rep_traffic ts'_def ts'_type Abs_traffic_inverse rep_eq res_def clm_def
fstI sndI by auto
have dyn_eq:"(dyn  (Abs_traffic ts')) = (dyn ts)"
using Rep_traffic ts'_def ts'_type Abs_traffic_inverse rep_eq dyn_def fstI sndI
by auto
have clm_eq:"(clm  (Abs_traffic ts')) = (clm ts)(c:=∅)"
using ts'_def ts'_type Abs_traffic_inverse rep_eq clm_def fstI sndI Rep_traffic
by fastforce
then have "ts  ❙─r(c)❙→ Abs_traffic ts'"
using ts'_def ts'_type create_reservation_def
ts'_def disj re_geq_one re_leq_two cl_leq_one add_leq_two
fst_conv snd_conv rep_eq sp_eq res_eq dyn_eq clm_eq
Rep_traffic clm_def res_def clm_def dyn_def physical_size_def braking_distance_def
by auto
then show ?thesis ..
qed
qed

lemma create_clm_eq_res:"(ts ❙─c(d,n)❙→ ts')  ⟶ res ts c = res ts' c "
using create_claim_def by auto

lemma withdraw_clm_eq_res:"(ts ❙─wdc(d)❙→ ts') ⟶ res ts c= res ts' c "
using withdraw_claim_def by auto

lemma withdraw_res_subseteq:"(ts ❙─wdr(d,n)❙→ ts') ⟶ res ts' c ⊑ res ts c "
using withdraw_reservation_def order_refl less_eq_nat_int.rep_eq nat_int.el.rep_eq
nat_int.in_refl nat_int.in_singleton  fun_upd_apply subset_eq by fastforce

end
end


# Theory Views

(*  Title:      Views.thy
Author:     Sven Linker, University of Liverpool

Defines a type for views on traffic. Consists of closed real valued interval
denoting "extension" (length on the road visible", the visible interval of lanes,
and the owner of the view.

Contains chopping relations on extension and lanes and switching to
different owners.
*)

section‹Views on Traffic›
text‹
In this section, we define a notion of locality for each car. These
local parts of a road are called \emph{views} and define the part of
the model currently under consideration by a car. In particular, a
view consists of
\begin{itemize}
\item the \emph{extension}, a real-valued interval denoting the distance perceived,
\item the \emph{lanes}, a discrete interval, denoting which lanes are perceived,
\item the \emph{owner}, the car associated with this view.
\end{itemize}
›

theory Views
imports NatInt RealInt Cars
begin

type_synonym lanes = nat_int
type_synonym extension = real_int

record view =
ext::extension
lan ::lanes
own ::cars

text ‹
The orders on discrete and continuous intervals induce an order on views.
For two views $$v$$ and $$v^\prime$$ with $$v \leq v^\prime$$, we call $$v$$
a \emph{subview} of $$v^\prime$$.›

instantiation  view_ext:: (order) order
begin
definition "less_eq_view_ext (V:: 'a view_ext)  (V':: 'a view_ext)  ≡
(ext V ≤ ext V') ∧ (lan V ⊑  lan V') ∧ own V = own V'
∧ more V ≤ more V'"
definition "less_view_ext (V :: 'a view_ext) (V':: 'a view_ext)  ≡
(ext V ≤ ext V') ∧ (lan V ⊑  lan V') ∧ own V' = own V
∧ more V ≤ more V' ∧
¬((ext V' ≤ ext V) ∧ (lan V' ⊑  lan V) ∧ own V' = own V
∧ more V' ≤ more V)"
instance
proof
fix v v' v''::  "'a view_ext"
show "v ≤ v"
using less_eq_view_ext_def less_eq_nat_int.rep_eq by auto
show " (v < v') = (v ≤ v' ∧ ¬ v' ≤ v)"
using less_eq_view_ext_def less_view_ext_def by auto
show "v ≤ v' ⟹ v' ≤ v'' ⟹ v ≤ v''"
using less_eq_view_ext_def less_eq_nat_int.rep_eq order_trans by auto
show "v ≤ v' ⟹ v' ≤ v ⟹ v = v'"
using less_eq_view_ext_def by auto
qed
end

locale view
begin

notation nat_int.maximum ("maximum")
notation nat_int.minimum ("minimum")
notation nat_int.consec ("consec")

text‹We lift the chopping relations from discrete and continuous intervals
to views, and introduce new notation for these relations.›

definition       hchop :: "view ⇒ view ⇒  view ⇒ bool" ("_=_∥_")
where "(v=u∥w) == real_int.R_Chop(ext v)(ext u)(ext w) ∧
lan v=lan u ∧
lan v=lan w ∧
own v = own u ∧
own v = own w ∧
more v = more w ∧
more v = more u  "
definition   vchop :: "view ⇒ view ⇒  view ⇒ bool" ("_=_--_")
where "(v=u--w) == nat_int.N_Chop(lan v)(lan u)( lan w) ∧
ext v = ext u ∧
ext v = ext w ∧
own v = own u ∧
own  v = own w ∧
more v = more w ∧
more v = more u "

text‹We can also switch the perspective of a view to the car $$c$$. That is,
we substitute $$c$$ for the original owner of the view.›

definition switch :: "view ⇒ cars ⇒ view ⇒ bool" ("_ = _ > _")
where   "  (v=c>w) == ext v = ext w ∧
lan v = lan w ∧
own w = c ∧
more v = more w"

text‹Most of the lemmas in this theory are direct transfers of the corresponding
lemmas on discrete and continuous intervals, which implies rather simple proofs.
The only exception is
the connection between subviews and the chopping operations. This proof is rather lengthy,
since we need to distinguish several cases, and within each case, we need to
explicitly construct six different views for the chopping relations.›

lemma h_chop_middle1:"(v=u∥w) ⟶ left (ext v) ≤ right (ext u)"
by (metis hchop_def real_int.rchop_def real_int.left_leq_right)

lemma h_chop_middle2:"(v=u∥w) ⟶ right (ext v) ≥ left (ext w)"
using real_int.left_leq_right real_int.rchop_def view.hchop_def by auto

lemma horizontal_chop1: " ∃ u w. (v=u∥w)"
proof -
have real_chop:"∃x1 x2.  R_Chop(ext v, x1,x2)"
using real_int.chop_singleton_left by force
obtain x1 and x2 where x1_x2_def:" R_Chop(ext v, x1,x2)"
using real_chop by force
obtain V1 and V2
where v1:"V1 = ⦇ ext = x1, lan = lan v, own = own v⦈"
and v2:"V2 = ⦇ ext = x2,lan= lan v, own = own v⦈ "  by blast
from v1 and v2 have "v=V1∥V2"
using hchop_def x1_x2_def by (simp)
thus ?thesis by blast
qed

lemma horizontal_chop_empty_right :"∀v. ∃ u. (v=v∥u)"
using hchop_def real_int.chop_singleton_right
by (metis (no_types, hide_lams) select_convs)

lemma horizontal_chop_empty_left :"∀v. ∃u. (v=u∥v)"
using hchop_def real_int.chop_singleton_left
by (metis (no_types, hide_lams) select_convs)

lemma horizontal_chop_non_empty:
"∥ext v∥ > 0 ⟶ (∃u w. (v=u∥w) ∧ ∥ext u∥ > 0 ∧ ∥ext w∥>0)"
proof
assume "∥ext v∥ > 0"
then obtain l1 and l2
where chop:" R_Chop(ext v, l1,l2) ∧ ∥l1∥ > 0 ∧ ∥l2∥ > 0"
using real_int.chop_dense by force
obtain V1 where v1_def:"V1 = ⦇ ext = l1, lan = lan v, own = own v ⦈"
by simp
obtain V2 where v2_def:"V2 = ⦇ ext = l2, lan = lan v, own = own v ⦈"
by simp
then have  "(v=V1∥V2) ∧ ∥ext V1∥ > 0 ∧ ∥ext V2∥>0"
using  chop hchop_def v1_def by (simp)
then show " (∃V1 V2. (v=V1∥V2) ∧ ∥ext V1∥ > 0 ∧ ∥ext V2∥>0)"
by blast
qed

"x ≥ 0 ∧ y ≥ 0 ⟶ ∥ext v∥ = x+y ⟶ (∃u w. (v=u∥w) ∧ ∥ext u∥ = x ∧ ∥ext w∥ = y)"
proof (rule impI)+
assume geq_0:"x ≥ 0 ∧ y ≥ 0" and len_v:"∥ext v∥ = x+y"
obtain u
where v1_def:
"u = ⦇ ext = Abs_real_int (left (ext v), left (ext v) + x), lan = lan v, own = (own v) ⦈"
by simp
have v1_in_type:"(left (ext v), left (ext v) + x) ∈ {r::(real*real) . fst r ≤ snd r}"
obtain w
where v2_def:
"w = ⦇ ext = Abs_real_int (left (ext v)+x, left (ext v) + (x+y)),
lan = (lan v), own = (own v) ⦈" by simp
have v2_in_type:
"(left (ext v)+x, left (ext v) + (x+y)) ∈ {r::(real*real) . fst r ≤ snd r}"
from v1_def and geq_0 have len_v1:"∥ext u∥ = x" using v1_in_type
from v2_def and geq_0 have len_v2:"∥ext w∥= y" using v2_in_type
from v1_def and v2_def have "(v=u∥w)"
using Abs_real_int_inverse fst_conv hchop_def len_v prod.collapse real_int.rchop_def
real_int.length_def snd_conv v1_in_type v2_in_type by auto
with len_v1 and len_v2 have "(v=u∥w) ∧ ∥ext u∥ = x ∧ ∥ext w∥ = y" by simp
thus "(∃u w. (v=u∥w) ∧ ∥ext u∥ = x ∧ ∥ext w∥ = y)" by blast
qed

lemma horizontal_chop_assoc1:
"(v=v1∥v2) ∧ (v2=v3∥v4) ⟶ (∃v'. (v=v'∥v4) ∧ (v'=v1∥v3))"
proof
assume assm:"(v=v1∥v2) ∧ (v2=v3∥v4)"
obtain v'
where v'_def:
"v' =⦇ ext = Abs_real_int(left (ext v1), right (ext v3)),
lan = (lan v), own = (own v) ⦈"
by simp
hence 1:"v=v'∥v4"
using assm real_int.chop_assoc1 hchop_def by auto
have 2:"v'=v1∥v3" using v'_def assm real_int.chop_assoc1 hchop_def by auto
from 1 and 2 have "(v=v'∥v4) ∧  (v'=v1∥v3)" by best
thus "(∃v'. (v=v'∥v4)  ∧ (v'=v1∥v3))" ..
qed

lemma horizontal_chop_assoc2:
"(v=v1∥v2) ∧ (v1=v3∥v4) ⟶ (∃v'. (v=v3∥v') ∧ (v'=v4∥v2))"
proof
assume assm:"(v=v1∥v2) ∧ (v1=v3∥v4)"
obtain v'
where v'_def:
"v'=⦇ ext = Abs_real_int(left (ext v4),right (ext v2)),
lan = (lan v), own = (own v) ⦈"
by simp
hence 1:"v=v3∥v'"
using assm fst_conv real_int.chop_assoc2 snd_conv hchop_def by auto
have 2: "v'=v4∥v2"
using assm real_int.chop_assoc2 v'_def hchop_def by auto
from 1 and 2 have "(v=v3∥v') ∧ (v'=v4∥v2)" by best
thus "(∃v'. (v=v3∥v') ∧ (v'=v4∥v2))" ..
qed

lemma horizontal_chop_width_stable:"(v=u∥w)⟶|lan v|=|lan u|∧|lan v|=|lan w|"
using hchop_def by auto

lemma horizontal_chop_own_trans:"(v=u∥w) ⟶ own u = own w"
using hchop_def by auto

lemma vertical_chop1:"∀v. ∃ u w. (v=u--w)"
using vchop_def  nat_int.chop_always_possible
by (metis (no_types, hide_lams) select_convs)

lemma vertical_chop_empty_down:"∀v.∃ u.(v=v--u)"
using vchop_def nat_int.chop_empty_right
by (metis (no_types, hide_lams) select_convs)

lemma vertical_chop_empty_up:"∀v.∃u.(v=u--v)"
using vchop_def nat_int.chop_empty_left
by (metis (no_types, hide_lams) select_convs)

lemma vertical_chop_assoc1:
"(v=v1--v2) ∧ (v2=v3--v4) ⟶ (∃v'. (v=v'--v4) ∧ (v'=v1--v3))"
proof
assume assm:"(v=v1--v2) ∧ (v2=v3--v4)"
obtain v'
where v'_def:"v' =⦇ ext = ext v, lan=(lan v1) ⊔ (lan v3), own = (own v) ⦈"
by simp
then have 1:"v=v'--v4"
using assm nat_int.chop_assoc1 vchop_def by auto
have 2:"v'=v1--v3"
using v'_def assm nat_int.chop_assoc1 vchop_def by auto
from 1 and 2 have "(v=v'--v4) ∧  (v'=v1--v3)" by best
then show "(∃v'. (v=v'--v4)  ∧ (v'=v1--v3))" ..
qed

lemma vertical_chop_assoc2:
"(v=v1--v2) ∧ (v1=v3--v4) ⟶ (∃v'. (v=v3--v') ∧ (v'=v4--v2))"
proof
assume assm:"(v=v1--v2) ∧ (v1=v3--v4)"
obtain v'
where v'_def:"v'=⦇ ext = ext v, lan =(lan v4) ⊔ (lan v2), own = (own v) ⦈"
by simp
then have 1:"v=v3--v'"
using assm fst_conv nat_int.chop_assoc2 snd_conv vchop_def by auto
have 2: "v'=v4--v2"
using assm nat_int.chop_assoc2 v'_def vchop_def by auto
from 1 and 2 have "(v=v3--v') ∧ (v'=v4--v2)" by best
then show "(∃v'. (v=v3--v') ∧ (v'=v4--v2))" ..
qed

lemma vertical_chop_singleton:
"(v=u--w) ∧ |lan v| = 1 ⟶ ( |lan u| = 0 ∨ |lan w| = 0)"
using nat_int.chop_single vchop_def Rep_nat_int_inverse
by fastforce

lemma vertical_chop_add1:"(v=u--w) ⟶ |lan v| = |lan u| + |lan w|"

"|lan v| = x+y ⟶ (∃ u w.  (v=u--w) ∧ |lan u| = x ∧ |lan w| = y)"
proof
assume assm:"|lan v| = x+y"
hence add:"∃i j. N_Chop(lan v, i,j) ∧ |i| = x ∧ |j| = y"
obtain i and j where l1_l2_def:"N_Chop(lan v, i,j) ∧ |i| = x ∧ |j| = y"
obtain u and w where "u=⦇ext =  ext v, lan = i, own = (own v) ⦈"
and "w = ⦇ ext = ext v, lan = j, own = (own v) ⦈ " by blast
hence "(v=u--w) ∧ |lan u|=x ∧ |lan w|=y"
using l1_l2_def view.vchop_def
by (simp)
thus "(∃ u w.  (v=u--w) ∧ |lan u| = x ∧ |lan w| = y)" by blast
qed

lemma vertical_chop_length_stable:
"(v=u--w) ⟶ ∥ext v∥ = ∥ext u∥ ∧ ∥ext v∥ = ∥ext w∥"
using vchop_def by auto

lemma vertical_chop_own_trans:"(v=u--w) ⟶ own u = own w"
using vchop_def by auto

lemma vertical_chop_width_mon:
"(v=v1--v2) ∧ (v2=v3--v4) ∧ |lan v3| = x ⟶ |lan v| ≥ x"

lemma horizontal_chop_leq1:"(v=u∥w) ⟶ u ≤ v"
using real_int.chop_leq1 hchop_def less_eq_view_ext_def order_refl by fastforce

lemma horizontal_chop_leq2:"(v=u∥w) ⟶ w ≤ v"
using real_int.chop_leq2 hchop_def less_eq_view_ext_def order_refl by fastforce

lemma vertical_chop_leq1:"(v=u--w) ⟶ u ≤ v"
using nat_int.chop_subset1 vchop_def less_eq_view_ext_def order_refl by fastforce

lemma vertical_chop_leq2:"(v=u--w) ⟶ w ≤ v"
using nat_int.chop_subset2 vchop_def less_eq_view_ext_def order_refl by fastforce

lemma somewhere_leq:
"v ≤ v' ⟷ (∃v1 v2 v3 vl vr vu vd.
(v'=vl∥v1) ∧ (v1=v2∥vr) ∧ (v2=vd--v3) ∧ (v3=v--vu))"
proof
assume "v ≤ v'"
hence assm_exp:"(ext v ≤ ext v') ∧ (lan v ⊑ lan v') ∧ (own v = own v')"
using less_eq_view_ext_def by auto
obtain vl v1 v2 vr
where
vl:"vl=⦇ext=Abs_real_int(left(ext v'),left(ext v)), lan=lan v', own=own v'⦈"
and
v1:"v1=⦇ext=Abs_real_int(left(ext v),right(ext v')), lan=lan v', own=own v'⦈"
and
v2:"v2=⦇ext=Abs_real_int(left(ext v),right(ext v)), lan=lan v', own=own v'⦈"
and
vr:"vr=⦇ext=Abs_real_int(right(ext v),right(ext v')), lan=lan v', own=own v'⦈"
by blast
have vl_in_type:"(left (ext v'), left (ext v)) ∈ {r::(real*real) . fst r ≤ snd r}"
using less_eq_real_int_def assm_exp real_int.left_leq_right snd_conv
fst_conv mem_Collect_eq by simp
have v1_in_type:"(left (ext v), right (ext v')) ∈ {r::(real*real) . fst r ≤ snd r}"
using less_eq_real_int_def assm_exp real_int.left_leq_right snd_conv fst_conv
mem_Collect_eq order_trans by fastforce
have v2_in_type:"(left (ext v), right (ext v)) ∈ {r::(real*real) . fst r ≤ snd r}"
using less_eq_real_int_def assm_exp real_int.left_leq_right snd_conv fst_conv
mem_Collect_eq order_trans by fastforce
have vr_in_type:"(right (ext v), right (ext v')) ∈ {r::(real*real) . fst r ≤ snd r}"
using less_eq_real_int_def assm_exp real_int.left_leq_right snd_conv fst_conv
mem_Collect_eq order_trans by fastforce
then have hchops:"(v'=vl∥v1)∧ (v1=v2∥vr)"
using vl v1 v2 vr less_eq_real_int_def hchop_def real_int.rchop_def
vl_in_type  v1_in_type  v2_in_type vr_in_type Abs_real_int_inverse by auto
have lanes_v2:"lan v2 = lan v'" using v2 by auto
have own_v2:"own v2 = own v'" using v2 by auto
have ext_v2:"ext v2 =ext v"
using v2 v2_in_type Abs_real_int_inverse  by (simp add: Rep_real_int_inverse)
show
"∃v1 v2 v3 vl vr vu vd. (v'=vl∥v1) ∧ (v1=v2∥vr) ∧ (v2=vd--v3) ∧ (v3=v--vu)"
proof (cases "lan v' = lan v")
case True
obtain vd v3 vu
where vd:"vd = ⦇ ext = ext v2, lan = ∅, own = own v'⦈"
and v3:"v3 = ⦇ ext = ext v2, lan = lan v', own = own v' ⦈"
and vu:"vu = ⦇ ext = ext v2, lan = ∅, own = own v' ⦈" by blast
hence "(v2=vd--v3) ∧ (v3=v--vu)"
using vd v3 vu True vchop_def nat_int.nchop_def nat_int.un_empty_absorb1
nat_int.un_empty_absorb2 nat_int.inter_empty1 nat_int.inter_empty2 lanes_v2
own_v2 ext_v2 assm_exp by auto
then show ?thesis using hchops by blast
next
case False
then have v'_neq_empty:"lan v' ≠ ∅"
by (metis assm_exp nat_int.card_empty_zero nat_int.card_non_empty_geq_one
nat_int.card_subset_le le_0_eq)
show ?thesis
proof (cases "lan v ≠ ∅")
case False
obtain vd v3 vu where vd:"vd = ⦇ ext = ext v2, lan = ∅, own = own v'⦈"
and v3:"v3 = ⦇ ext = ext v2, lan = lan v', own = own v' ⦈"
and vu:"vu = ⦇ ext = ext v2, lan = lan v', own = own v' ⦈" by blast
then have "(v2=vd--v3) ∧ (v3=v--vu)"
using vd v3 vu False vchop_def nat_int.nchop_def
nat_int.un_empty_absorb1 nat_int.un_empty_absorb2
nat_int.inter_empty1 nat_int.inter_empty2 lanes_v2 own_v2 ext_v2 assm_exp
by auto
then show ?thesis
using hchops by blast
next
case True
show ?thesis
proof (cases "(minimum (lan v)) = minimum(lan v')")
assume min:"minimum ( lan v) = minimum (lan v')"
hence max:"maximum (lan v) <maximum (lan v')"
by (metis Rep_nat_int_inverse assm_exp atLeastatMost_subset_iff leI le_antisym
nat_int.leq_max_sup nat_int.leq_min_inf nat_int.maximum_def nat_int.minimum_def
nat_int.rep_non_empty_means_seq less_eq_nat_int.rep_eq False True
v'_neq_empty)
obtain vd v3 vu
where vd:"vd = ⦇ ext = ext v2, lan = ∅, own = own v'⦈"
and v3:"v3 = ⦇ ext = ext v2, lan = lan v', own = own v' ⦈"
and vu:"vu = ⦇ ext = ext v2, lan =
Abs_nat_int({maximum(lan v)+1..maximum(lan v')}), own = own v' ⦈"
by blast
have vu_in_type:
"{maximum(lan v)+1 ..maximum(lan v')} ∈ {S.(∃ (m::nat) n.{m..n }=S)}"
using max by auto
have consec:"consec (lan v) (lan vu)" using max
by (simp add:  Suc_leI   nat_int.consec_def nat_int.leq_min_inf'
nat_int.leq_nat_non_empty True  vu)
have disjoint:" lan v ⊓  lan vu = ∅"
have union:"lan v' = lan v ⊔ lan vu"
by (metis Suc_eq_plus1 Suc_leI consec leq_max_sup' max min
nat_int.consec_un_equality nat_int.consec_un_max nat_int.consec_un_min
select_convs(2) v'_neq_empty vu)
then have "(v2=vd--v3) ∧ (v3=v--vu)"
using vd v3 vu vchop_def nat_int.nchop_def nat_int.un_empty_absorb1
nat_int.un_empty_absorb2 nat_int.inter_empty1 nat_int.inter_empty2
lanes_v2 own_v2 ext_v2 assm_exp vu_in_type  Abs_nat_int_inverse
consec union disjoint select_convs
by force
then show ?thesis using hchops by blast
next
assume "(minimum (lan v)) ≠ minimum (lan v')"
then have  min:"minimum ( lan v) > minimum (lan v')"
by (metis Min_le True assm_exp finite_atLeastAtMost le_neq_implies_less
less_eq_nat_int.rep_eq nat_int.el.rep_eq nat_int.minimum_def
nat_int.minimum_in rep_non_empty_means_seq subsetCE v'_neq_empty)
show ?thesis
proof (cases "(maximum (lan v)) = maximum (lan v')")
assume max:"maximum(lan v) = maximum (lan v')"
obtain vd v3 vu
where
vd:"vd =
⦇ ext = ext v2,
lan = Abs_nat_int ({minimum(lan v')..minimum(lan v)-1}),
own = own v'⦈"
and
v3:"v3 = ⦇ ext = ext v2, lan = lan v, own = own v' ⦈"
and
vu:"vu = ⦇ ext = ext v2, lan = ∅ , own = own v' ⦈" by blast
have consec:"consec (lan vd) (lan v)"
using True leq_max_sup' leq_nat_non_empty min
nat_int.consec_def vd by auto
have "maximum (lan vd ⊔ lan v) = maximum (lan v)"
using consec consec_un_max by auto
then have max':"maximum (lan vd ⊔ lan v) = maximum (lan v')"
have "minimum (lan vd ⊔ lan v) = minimum (lan vd)"
using consec consec_un_min by auto
then have min':"minimum (lan vd ⊔ lan v) = minimum (lan v')"
by (metis atLeastatMost_empty_iff vd bot_nat_int.abs_eq consec
nat_int.consec_def nat_int.leq_min_inf' select_convs(2))
have union:" lan v' = lan vd ⊔ lan v"
using consec max' min' nat_int.consec_un_equality v'_neq_empty
by fastforce
then have "(v2=vd--v3) ∧ (v3=v--vu)"
using assm_exp consec ext_v2 lanes_v2 nat_int.nchop_def nat_int.un_empty_absorb1
own_v2 v3 vd view.vchop_def vu by force
then show ?thesis
using hchops by blast
next
assume "(maximum (lan v)) ≠ maximum (lan v')"
then have max:"maximum (lan v) < maximum (lan v')"
by (metis assm_exp atLeastatMost_subset_iff nat_int.leq_max_sup
nat_int.maximum_def nat_int.rep_non_empty_means_seq less_eq_nat_int.rep_eq
True order.not_eq_order_implies_strict v'_neq_empty)
obtain vd v3 vu
where vd:
"vd = ⦇ ext = ext v2,
lan = Abs_nat_int ({minimum(lan v')..minimum(lan v)-1}),
own = own v'⦈"
and v3:
"v3 = ⦇ ext = ext v2, lan = lan v ⊔ lan vu, own = own v' ⦈"
and vu:
"vu = ⦇ ext = ext v2,
lan = Abs_nat_int ({maximum(lan v)+1..maximum(lan v')}),
own = own v' ⦈" by blast
have consec:"consec (lan v) (lan vu)"
using True leq_nat_non_empty max nat_int.consec_def nat_int.leq_min_inf'
vu
by auto
have union:"lan v3 = lan v ⊔ lan vu"
by (simp add: v3 min max consec)
then have chop1:" (v3=v--vu)"
using assm_exp consec ext_v2 nat_int.nchop_def v3 view.vchop_def
vu
by auto
have min_eq:"minimum (lan v3) = minimum (lan v)"
using chop1 consec nat_int.chop_min vchop_def by blast
have neq3:"lan v3 ≠ ∅"
by (metis bot.extremum_uniqueI consec nat_int.consec_def nat_int.un_subset2
union)
have consec2:"consec (lan vd) (lan v3)"
using min consec union min_eq Suc_leI nat_int.consec_def nat_int.leq_max_sup'
nat_int.leq_min_inf' nat_int.leq_nat_non_empty neq3 v3 vd
by (auto)
have "minimum (lan vd ⊔ lan v3) = minimum (lan vd)"
using consec2 consec_un_min by auto
then have min':"minimum (lan vd ⊔ lan v3) = minimum (lan v')"
by (metis vd atLeastatMost_empty_iff2 bot_nat_int.abs_eq consec2 leq_min_inf'
nat_int.consec_def select_convs(2))
have "maximum (lan vd ⊔lan v3) = maximum (lan v3)"
using consec2 consec_un_max by auto
then have "maximum (lan vd ⊔lan v3) = maximum (lan vu)"
using consec consec_un_max union by auto
then have max':"maximum (lan vd ⊔lan v3) = maximum (lan v')"
by (metis Suc_eq_plus1 Suc_leI max nat_int.leq_max_sup'
select_convs(2) vu)
have union2:" lan v' = lan vd ⊔ lan v3"
using min max consec2 neq3 min' max' nat_int.consec_un_equality v'_neq_empty
by force
have "(v2=vd--v3) ∧ (v3=v--vu)"
using union2 chop1 consec2 nat_int.nchop_def v2 v3 vd
view.vchop_def
by fastforce
then show ?thesis using hchops by blast
qed
qed
qed
qed
next
assume
"∃v1 v2 v3 vl vr vu vd. (v'=vl∥v1) ∧ (v1=v2∥vr) ∧ (v2=vd--v3) ∧ (v3=v--vu)"
then obtain v1 v2 v3 vl vr vu vd
where " (v'=vl∥v1) ∧ (v1=v2∥vr) ∧ (v2=vd--v3) ∧ (v3=v--vu)" by blast
then show "v ≤ v'"
by (meson horizontal_chop_leq1 horizontal_chop_leq2 order_trans vertical_chop_leq1
vertical_chop_leq2)
qed

text‹The switch relation is compatible with the chopping relations, in the
following sense. If we can chop a view $$v$$ into two subviews $$u$$ and
$$w$$, and we can reach $$v^\prime$$ via the switch relation, then
there also exist two subviews $$u^\prime$$, $$w^\prime$$ of $$v^\prime$$,
such that $$u^\prime$$ is reachable from $$u$$ (and respectively for $$w^\prime$$, $$w$$).
›
(* switch lemmas *)
lemma switch_unique:"(v =c> u) ∧ (v =c> w) ⟶u = w"
using switch_def by auto

lemma switch_exists:"∃c u.( v=c>u)"
using switch_def by auto

lemma switch_always_exists:"∀c. ∃u. (v=c>u)"
by (metis select_convs switch_def)

lemma switch_origin:" ∃u. (u=(own v)>v)"
using switch_def  by auto

lemma switch_refl:"(v=(own v)>v)"

lemma switch_symm:"(v=c>u) ⟶ (u=(own v)>v)"

lemma switch_trans:"(v=c>u) ∧ (u=d>w) ⟶ (v=d>w)"

lemma switch_triangle:"(v=c>u) ∧ (v=d>w) ⟶ (u=d>w)"
using switch_def by auto

lemma switch_hchop1:
"(v=v1∥v2) ∧ (v=c>v') ⟶
(∃ v1' v2'. (v1 =c> v1') ∧ (v2 =c> v2') ∧ (v'=v1'∥v2'))"
by (metis (no_types, hide_lams) select_convs view.hchop_def view.switch_def)

lemma switch_hchop2:
"(v'=v1'∥v2') ∧ (v=c>v') ⟶
(∃ v1 v2. (v1 =c> v1') ∧ (v2 =c> v2') ∧ (v=v1∥v2))"
by (metis (no_types, hide_lams) select_convs view.hchop_def view.switch_def)

lemma switch_vchop1:
"(v=v1--v2) ∧ (v=c>v') ⟶
(∃ v1' v2'. (v1 =c> v1') ∧ (v2 =c> v2') ∧ (v'=v1'--v2'))"
by (metis (no_types, hide_lams) select_convs view.vchop_def view.switch_def)

lemma switch_vchop2:
"(v'=v1'--v2') ∧ (v=c>v') ⟶
(∃ v1 v2. (v1 =c> v1') ∧ (v2 =c> v2') ∧ (v=v1--v2))"
by (metis (no_types, hide_lams) select_convs view.vchop_def view.switch_def)

lemma switch_leq:"u' ≤ u ∧ (v=c>u) ⟶ (∃v'. (v'=c>u') ∧ v' ≤ v)"
proof
assume assm: "u' ≤ u ∧ (v=c>u)"
then have more_eq:"more v = more u"
using view.switch_def by blast
then obtain v' where v'_def:"v'= ⦇ ext =ext u', lan = lan u', own = own v⦈"
by blast
have ext:"ext v' ≤ ext v" using assm switch_def
have lan:"lan v' ≤ lan v" using assm switch_def
have more:"more v' ≤ more v" using more_eq assm by simp
have less: "v' ≤ v" using less_eq_view_ext_def ext lan more v'_def
have switch:"v' =c> u'" using v'_def switch_def assm
show  "(∃v'. ( v' = c > u') ∧ v' ≤ v)" using switch less by blast
qed
end
end


# Theory Restriction

(*  Title:      Restriction.thy

Restrict a function from cars to lanes to a given view. Will be
used for claim and reservation functions of Traffic Snapshots.
*)

section‹Restrict Claims and Reservations to a View›
text ‹
To model that a view restricts the number of lanes a car may
perceive, we define a function $$restrict$$ taking a view $$v$$, a function
$$f$$ from cars to lanes and a car $$f$$, and returning the intersection
between $$f(c)$$ and the set of lanes of $$v$$. This function
will in the following only be applied to the functions yielding
reservations and claims from traffic snapshots.

The lemmas of this section describe the connection between
$$restrict$$ and the different operations on traffic snapshots
and views (e.g., the transition relations or the fact that
reservations and claims are consecutive).
›

theory Restriction
imports Traffic Views
begin

locale restriction = view+traffic
begin

definition restrict :: "view ⇒ (cars ⇒ lanes) ⇒ cars ⇒ lanes"
where  "restrict v f c ==  (f c) ⊓  lan v"

lemma restrict_def':" restrict v f c = lan v ⊓ f c"
using inf_commute restriction.restrict_def by auto

lemma restrict_subseteq:"restrict v f c ⊑ f c"
using inf_le1 restrict_def by auto

lemma restrict_clm : "restrict v (clm ts) c ⊑ clm ts c"
using inf_le1 restrict_def by auto

lemma restrict_res: "restrict v (res ts) c ⊑ res ts c"
using inf_le1 restrict_def by auto

lemma restrict_view:"restrict v f c ⊑ lan v"
using inf_le1 restrict_def by auto

lemma restriction_stable:"(v=u∥w) ⟶ restrict u f  c = restrict w f  c"
using hchop_def restrict_def by auto

lemma restriction_stable1:"(v=u∥w) ⟶ restrict v f  c = restrict u f  c"

lemma restriction_stable2:"(v=u∥w) ⟶ restrict v f  c = restrict w f  c"

lemma restriction_un:
"(v=u--w) ⟶ restrict v f c = (restrict u f c ⊔ restrict w f c)"
using nat_int.inter_distr1 nat_int.inter_empty1 nat_int.un_empty_absorb1
nat_int.un_empty_absorb2 nat_int.nchop_def restrict_def vchop_def
by auto

lemma restriction_mon1:"(v=u--w) ⟶ restrict u f c ⊑ restrict v f c"
using inf_mono nat_int.chop_subset1 restrict_def vchop_def
by (metis (no_types, hide_lams) order_refl)

lemma restriction_mon2:"(v=u--w) ⟶ restrict w f c ⊑ restrict v f c"
using inf_mono nat_int.chop_subset2 restrict_def vchop_def
by (metis (no_types, hide_lams) order_refl)

lemma restriction_disj:"(v=u--w) ⟶ (restrict u f c) ⊓ (restrict w f c) = ∅"
proof
assume assm: "v=u--w"
then have 1:"lan u ⊓ lan w = ∅" using vchop_def
by (metis inf_commute inter_empty1 nat_int.consec_inter_empty nat_int.nchop_def)
from assm have "(restrict u f c) ⊓ (restrict w f c) ⊑ lan u ⊓ lan w "
by (meson inf_mono restriction.restrict_view)
with 1 show  "(restrict u f c) ⊓ (restrict w f c) = ∅"
qed

lemma vertical_chop_restriction_res_consec_or_empty:
"(v=v1--v2) ∧ restrict v1 (res ts) c ≠ ∅ ∧ consec ((lan v1)) ((lan v2)) ∧
¬consec (restrict v1 (res ts) c) (restrict v2 (res ts) c)
⟶ restrict v2 (res ts) c = ∅"
proof
assume assm:
"(v=v1--v2) ∧ restrict v1 (res ts) c ≠ ∅ ∧
consec ((lan v1)) ((lan v2)) ∧
¬consec (restrict v1 (res ts) c) (restrict v2 (res ts) c)"
hence "restrict v1 (res ts) c = ∅ ∨ restrict v2 (res ts) c = ∅ ∨
(maximum (restrict v1 (res ts) c)+1 ≠minimum (restrict v2 (res ts) c))"
using nat_int.consec_def by blast
hence empty_or_non_consec:"restrict v2 (res ts) c = ∅ ∨
(maximum (restrict v1 (res ts) c)+1 ≠minimum (restrict v2 (res ts) c))"
using assm by blast
have consec_lanes:"consec ((lan v1)) ((lan v2))" by (simp add: assm)
have subs:"restrict v2 (res ts) c ⊑ ((lan v2))" using restrict_view
by simp
show "restrict v2 (res ts) c = ∅"
proof (rule ccontr)
assume non_empty:"restrict v2 (res ts) c ≠ ∅"
hence max:
"(maximum (restrict v1 (res ts) c)+1 ≠minimum (restrict v2 (res ts) c))"
using empty_or_non_consec by blast
have ex_n:" ∃n. n ∈ Rep_nat_int (restrict v2 (res ts) c)"
using nat_int.el.rep_eq non_empty nat_int.non_empty_elem_in by auto
have res1_or2:"|(res ts) c| = 1 ∨ |(res ts) c| = 2"
by (metis Suc_1 atLeastOneRes atMostTwoRes dual_order.antisym le_SucE)
then show False
proof
assume res_one:"|(res ts) c|=1"
then obtain n where one_lane:"Rep_nat_int ((res ts) c) =  {n}"
using singleton by blast
then have "n ∈ Rep_nat_int (restrict v1 (res ts) c)"
by (metis assm equals0D nat_int.el.rep_eq less_eq_nat_int.rep_eq
nat_int.non_empty_elem_in restrict_res singletonI subset_singletonD)
then have "Rep_nat_int (restrict v2 (res ts) c) = {}"
by (metis one_lane assm inf.absorb1 less_eq_nat_int.rep_eq restriction.restrict_res
restriction_disj subset_singleton_iff)
thus False
using ex_n by blast
next
assume res_two:"|(res ts) c| = 2"
hence ex_two_ln:" (∃n . Rep_nat_int ((res ts) c) = {n,n+1})"
using consecutiveRes by blast
then obtain n where n_def:"Rep_nat_int ((res ts) c) = {n,n+1}"  by blast
hence rep_restrict_v1:"Rep_nat_int (restrict v1 (res ts) c) ⊆ {n,n+1}"
using less_eq_nat_int.rep_eq restrict_res by blast
hence
"n ∈ Rep_nat_int (restrict v1 (res ts) c) ∨
n+1 ∈ Rep_nat_int(restrict v1 (res ts) c)"
using assm bot.extremum_unique less_eq_nat_int.rep_eq by fastforce
thus False
proof
assume suc_n_in_res_v1:"n+1 ∈ Rep_nat_int (restrict v1 (res ts) c)"
hence suc_n_in_v1:"n+1 ∈ Rep_nat_int ((lan v1))"
using less_eq_nat_int.rep_eq restrict_view by blast
hence  "n+1 ∉ Rep_nat_int (lan v2)"
using assm vchop_def nat_int.nchop_def nat_int.consec_in_exclusive1
nat_int.el.rep_eq nat_int.not_in.rep_eq by blast
hence suc_n_not_in_res_v2:"n+1 ∉ Rep_nat_int (restrict v2 (res ts) c)"
using less_eq_nat_int.rep_eq subs by blast
have "∀m . m ❙∈ lan v2 ⟶ m ≥ minimum (lan v2)"
by (metis consec_lanes nat_int.minimum_def nat_int.consec_def
nat_int.el.rep_eq atLeastAtMost_iff nat_int.leq_min_inf
nat_int.rep_non_empty_means_seq)
then have "∀m . m ❙∈ lan v2 ⟶ m > maximum (lan v1)"
using assm nat_int.consec_def by fastforce
then have "∀m . m ❙∈ lan v2 ⟶ m > n+1"
using consec_lanes nat_int.maximum_def nat_int.card_seq
nat_int.consec_def suc_n_in_v1
then have "n ∉ Rep_nat_int ((lan v2))"
using suc_n_in_v1 assm nat_int.consec_def nat_int.el.rep_eq
by auto
hence "n∉ Rep_nat_int (restrict v2 (res ts) c)"
using less_eq_nat_int.rep_eq rev_subsetD subs by blast
hence "Rep_nat_int (restrict v2 (res ts) c) = {}"
using insert_absorb insert_ident insert_not_empty n_def less_eq_nat_int.rep_eq
restrict_res singleton_insert_inj_eq subset_insert suc_n_not_in_res_v2
by fastforce
thus False using ex_n by blast
next
assume n_in_res_v1:"n ∈ Rep_nat_int (restrict v1 (res ts) c)"
hence n_not_in_v2:"n ∉ Rep_nat_int ((lan v2))"
using assm vchop_def nat_int.nchop_def  nat_int.consec_in_exclusive1
nat_int.consec_in_exclusive2 nat_int.el.rep_eq nat_int.not_in.rep_eq
by (meson less_eq_nat_int.rep_eq restrict_view subsetCE)
hence n_not_in_res_v2:"n ∉ Rep_nat_int (restrict v2 (res ts) c)"
using less_eq_nat_int.rep_eq subs by blast
show False
proof (cases "n+1 ∈ Rep_nat_int(restrict v2 (res ts) c) ")
case False
hence "Rep_nat_int (restrict v2 (res ts) c) = {}"
using insert_absorb insert_ident insert_not_empty n_def n_not_in_res_v2
less_eq_nat_int.rep_eq restrict_res singleton_insert_inj_eq' subset_insert
by fastforce
thus False using ex_n by blast
next
case True
obtain NN :: "nat set ⇒ nat ⇒ nat set" where
"∀x0 x1. (∃v2. x0 = insert x1 v2 ∧ x1 ∉ v2)
= (x0 = insert x1 (NN x0 x1) ∧ x1 ∉ NN x0 x1)"
by moura
then have f1:
"Rep_nat_int (restrict v2 (res ts) c) =
insert (n + 1) (NN (Rep_nat_int (restrict v2 (res ts) c)) (n + 1))
∧ n + 1 ∉ NN (Rep_nat_int (restrict v2 (res ts) c)) (n + 1)"
by (meson mk_disjoint_insert True)
then have
"insert (n + 1) (NN (Rep_nat_int (restrict v2 (res ts) c)) (n+1))
⊆ {n+1}∪{}"
by (metis (no_types) insert_is_Un n_def n_not_in_res_v2 less_eq_nat_int.rep_eq
restrict_res subset_insert)
then have "{n + 1} = Rep_nat_int (restrict v2 (res ts) c)"
using f1 by blast
then have min:"nat_int.minimum (restrict v2 (res ts) c) = n+1"
by (metis (no_types) Min_singleton nat_int.minimum_def non_empty)
then have suc_n_in_v2:"n+1 ❙∈ (lan v2)"
using nat_int.el.rep_eq less_eq_nat_int.rep_eq subs True
by auto
have "∀m . m ❙∈ lan v1 ⟶ m ≤ maximum (lan v1)"
by (metis atLeastAtMost_iff consec_lanes nat_int.maximum_def  nat_int.consec_def
nat_int.el.rep_eq nat_int.leq_max_sup nat_int.rep_non_empty_means_seq)
then have "∀m . m ❙∈ lan v1 ⟶ m < minimum (lan v2)" using assm
using nat_int.consec_lesser nat_int.minimum_in nat_int.consec_def
by auto
then have "∀m . m ❙∈ lan v1 ⟶ m < n+1"
using consec_lanes  nat_int.card_seq nat_int.consec_def suc_n_in_v2
nat_int.consec_lesser by auto
then have suc_n_not_in_v1:"n+1 ∉ Rep_nat_int ((lan v1))"
using nat_int.el.rep_eq by auto
have suc_n_not_in_res_v1:"n+1 ∉ Rep_nat_int (restrict v1 (res ts) c)"
using less_eq_nat_int.rep_eq restrict_view suc_n_not_in_v1 by blast
from rep_restrict_v1 and n_in_res_v1 have res_v1_singleton:
"Rep_nat_int (restrict v1 (res ts) c) = {n}"
using Set.set_insert insert_absorb2 insert_commute singleton_insert_inj_eq'
subset_insert suc_n_not_in_res_v1 by blast
have max: "nat_int.maximum (restrict v1 (res ts) c) = n"
by (metis Rep_nat_int_inverse nat_int.leq_max_sup' order_refl
res_v1_singleton nat_int.rep_single)
from min and max have
"maximum (restrict v1 (res ts) c)+1 = minimum (restrict v2 (res ts) c)"
by auto
thus False
using empty_or_non_consec non_empty by blast
qed
qed
qed
qed
qed

lemma restriction_consec_res:"(v=u--w)
⟶ restrict u (res ts) c = ∅ ∨ restrict w (res ts) c = ∅
∨  consec (restrict u (res ts) c) ( restrict w (res ts) c)"
proof
assume assm:"v=u--w"
then show "restrict u (res ts) c = ∅ ∨ restrict w (res ts) c = ∅
∨  consec (restrict u (res ts) c) ( restrict w (res ts) c)"
proof (cases "res ts c =∅")
case True
show ?thesis
by (simp add: True inter_empty1 restriction.restrict_def')
next
case False
then have "res ts c ≠ ∅" by best
show ?thesis
by (metis (no_types, lifting) assm inter_empty1 nat_int.nchop_def
restriction.restrict_def restriction.vertical_chop_restriction_res_consec_or_empty
view.vchop_def)
qed
qed

lemma restriction_clm_res_disjoint:
"(restrict v (res ts) c) ⊓ (restrict v (clm ts) c) = ∅"
by (metis (no_types) inf_assoc nat_int.inter_empty2 restriction.restrict_def
restrict_def' traffic.disjoint)

lemma el_in_restriction_clm_singleton:
"n ❙∈ restrict v (clm ts) c ⟶ (clm ts) c = Abs_nat_int({n})"
proof
assume n_in_restr:"n ❙∈ restrict v (clm ts) c"
hence "n ❙∈ ((clm ts) c ⊓ (lan v))" by (simp add: restrict_def)
hence "n ∈ (Rep_nat_int (clm ts c) ∩ Rep_nat_int (lan v))"
hence n_in_rep_clm:"n ∈ (Rep_nat_int ((clm ts) c))" by simp
then have "(clm ts) c ≠ ∅" using nat_int.el.rep_eq nat_int.non_empty_elem_in
by auto
then have "|(clm ts) c| ≥ 1"
then have "|(clm ts) c| = 1" using atMostOneClm le_antisym
by blast
with n_in_rep_clm show "(clm ts) c = Abs_nat_int({n})"
by (metis Rep_nat_int_inverse nat_int.singleton singletonD)
qed

lemma restriction_clm_v2_non_empty_v1_empty:
"(v=u--w) ∧ restrict w (clm ts) c ≠ ∅ ∧
consec ((lan u)) ((lan w)) ⟶ restrict u (clm ts) c = ∅"
proof
assume assm:"(v=u--w) ∧ restrict w (clm ts) c ≠ ∅ ∧ consec (lan u) (lan w)"
obtain n where n_in_res_v2: "(n ❙∈ restrict w (clm ts) c)"
using assm maximum_in by blast
have "(clm ts) c = Abs_nat_int({n})"
using n_in_res_v2  by (simp add: el_in_restriction_clm_singleton)
then show "restrict u (clm ts) c = ∅"
by (metis assm inf.absorb_iff2 inf_commute less_eq_nat_int.rep_eq
n_in_res_v2 nat_int.el.rep_eq nat_int.in_singleton restriction.restrict_subseteq
restriction.restriction_disj subsetI)
qed

lemma restriction_consec_clm:
"(v=u--w) ∧ consec (lan u) (lan w)
⟶ restrict u (clm ts) c = ∅ ∨ restrict w (clm ts) c = ∅"
nat_int.un_empty_absorb2 nat_int.nchop_def restrict_def vchop_def
restriction_clm_v2_non_empty_v1_empty
by meson

"(v=u--w)
⟶ |restrict v (res ts) c|=|restrict u (res ts) c|+|restrict w (res ts) c|"
proof
assume assm: "v=u--w"
then have 1:"restrict u (res ts) c ⊓ restrict w (res ts) c = ∅"
using restriction.restriction_disj by auto
from assm have "restrict v (res ts) c=restrict u (res ts) c⊔restrict w (res ts) c"
using restriction.restriction_un by blast
with 1 show " |restrict v (res ts) c|=|restrict u (res ts) c|+|restrict w (res ts) c|"
restriction.restriction_consec_res)
qed

lemma restriction_eq_view_card:"restrict v f c = lan v ⟶ |restrict v f c| =|lan v|"
by simp

lemma restriction_card_mon1:"(v=u--w) ⟶ |restrict u f c| ≤ |restrict v f c|"
using nat_int.card_subset_le restriction_mon1 by (simp )

lemma restriction_card_mon2:"(v=u--w) ⟶ |restrict w f c| ≤ |restrict v f c|"
using nat_int.card_subset_le restriction_mon2 by (simp )

lemma restriction_res_leq_two:"|restrict v (res ts) c| ≤ 2"
using atMostTwoRes nat_int.card_subset_le le_trans restrict_res
by metis

lemma restriction_clm_leq_one:"|restrict v (clm ts) c| ≤ 1"
using atMostOneClm nat_int.card_subset_le le_trans restrict_clm
by metis

"(v=u--w)
⟶ |restrict v (clm ts) c|=|restrict u (clm ts) c|+|restrict w (clm ts) c|"
proof
assume assm:"v=u--w"
have "|restrict u (clm ts) c| = 1 ∨ |restrict u (clm ts) c| = 0"
by (metis One_nat_def le_0_eq le_SucE restriction.restriction_clm_leq_one)
then show "|restrict v (clm ts) c|=|restrict u (clm ts) c|+|restrict w (clm ts) c|"
proof
assume clm_u:"|restrict u (clm ts) c| = 1"
have "restrict u (clm ts) c ≠ ∅"
using clm_u card_non_empty_geq_one by auto
then have "|restrict w (clm ts) c| = 0"
by (metis (no_types) assm card_empty_zero inf_commute inter_empty2
nat_int.nchop_def restriction.restrict_def
restriction.restriction_clm_v2_non_empty_v1_empty view.vchop_def)
then show ?thesis
by (metis Nat.add_0_right assm clm_u inf.absorb1 inf_commute
restriction.restriction_card_mon1 restriction.restriction_clm_leq_one)
next
assume no_clm_u:"|restrict u (clm ts) c| = 0"
then have "|restrict w (clm ts) c| = 1 ∨ |restrict w (clm ts) c| = 0"
by (metis One_nat_def le_0_eq le_SucE restriction.restriction_clm_leq_one)
then show ?thesis
proof
assume "|restrict w (clm ts) c| = 1"
then show ?thesis
by (metis no_clm_u add_cancel_left_left antisym_conv3 assm leD
restriction.restriction_card_mon2 restriction.restriction_clm_leq_one)
next
assume no_clm_w:"|restrict w (clm ts) c| = 0"
then have "|restrict v (clm ts) c| = 0"
by (metis assm card_empty_zero chop_empty
nat_int.card_non_empty_geq_one nat_int.nchop_def no_clm_u
restriction.restriction_un)
then show ?thesis
using no_clm_u no_clm_w by linarith
qed
qed
qed

lemma restriction_card_mon_trans:
"(v=v1--v2) ∧ (v2=v3--v4) ∧ |restrict v3 f c| = 1 ⟶ |restrict v f c|≥1"
by (metis One_nat_def Suc_leI neq0_conv not_less_eq_eq
restriction_card_mon1 restriction_card_mon2)

lemma restriction_card_somewhere_mon:
"(v=vl∥v1)∧(v1=v2∥vr)∧(v2=vu--v3)∧(v3=v'--vd)∧|restrict v' f c|=1
⟶ |restrict v f c| ≥ 1"
proof
assume assm:
"(v=vl∥v1)∧(v1=v2∥vr)∧(v2=vu--v3)∧(v3=v'--vd)∧|restrict v' f c|=1"
then have "|restrict v2 f c| ≥ 1" using restriction_card_mon_trans by blast
then show "|restrict v f c| ≥ 1" using restriction_stable1 restriction_stable2 assm
by metis
qed

lemma restrict_eq_lan_subs:
"|restrict v f c| = |lan v| ∧ (restrict v f c ⊑ lan v) ⟶ restrict v f c = lan v"
proof
assume assm:"|restrict v f c| = |lan v| ∧ (restrict v f c ⊑ lan v)"
have "|restrict v f c| = 0 ∨ |restrict v f c| ≠ 0" by auto
thus "restrict v f c = lan v"
proof (cases "|restrict v f c| = 0")
case True
then have res_empty:"restrict v f c = ∅"
by (metis nat_int.card_non_empty_geq_one nat_int.card_empty_zero)
then have "lan v = ∅"
by (metis assm nat_int.card_empty_zero nat_int.card_non_empty_geq_one)
then show "restrict v f c = lan v"
using res_empty by auto
next
case False
show "restrict v f c = lan v"
proof (rule ccontr)
assume non_eq:"restrict v f c ≠ lan v"
then have "restrict v f c < lan v"
then have "|restrict v f c| < |lan v|"
using card_subset_less by blast
then show False using assm by simp
qed
qed
qed

lemma create_reservation_restrict_union:
"(ts❙─r(c)❙→ts')
⟶ restrict v (res ts') c = restrict v (res ts) c ⊔ restrict v (clm ts) c"
proof
assume assm:"(ts❙─r(c)❙→ts')"
hence res_ts':"res ts' c = res ts c ⊔ clm ts c"
show " restrict v (res ts') c = restrict v (res ts) c ⊔ restrict v (clm ts) c"
proof (cases "clm ts c = ∅")
case True
hence res_ts'eq_ts:"res ts' c = res ts c"
using res_ts' nat_int.un_empty_absorb1 by simp
from True have restrict_clm:"restrict v (clm ts) c = ∅"
using nat_int.inter_empty2 restrict_def by simp
from res_ts'eq_ts have "restrict v (res ts') c = restrict v (res ts) c"
thus ?thesis using restrict_clm
next
case False
hence "consec (clm ts c) (res ts c) ∨ consec (res ts c) (clm ts c)"
thus ?thesis
proof
assume consec:"consec (clm ts c) (res ts c)"
then show ?thesis
using inter_distr1 res_ts' restriction.restrict_def
by (simp add: Un_ac(3) inf_commute nat_int.union_def)
next
assume consec:"consec (res ts c) (clm ts c)"
then show ?thesis
by (simp add: inter_distr2 res_ts' restriction.restrict_def)
qed
qed
qed

(* switch lemmas *)
lemma switch_restrict_stable:"(v=c>u) ⟶ restrict v f d = restrict u f d"
using switch_def by (simp add: restrict_def)
end
end


# Theory Move

(*  Title:      Move.thy

The move function shifts a view by the difference in position of the owner of the view.
The lanes and owner itself are not changed.

*)

section‹Move a View according to Difference between Traffic Snapshots›
text ‹
In this section, we define a function to move a view according
to the changes between two traffic snapshots. The intuition is
that the view moves with the same speed as its owner. That is,
if we move a view $$v$$ from $$ts$$ to $$ts^\prime$$, we
shift the extension of the view by the difference in the
position of the owner of $$v$$.
›

theory Move
imports Traffic Views
begin

context traffic
begin

definition move::"traffic ⇒ traffic ⇒ view ⇒ view"
where
"move ts ts' v = ⦇ ext = shift (ext v) ((pos ts' (own v)) - pos ts (own v)),
lan = lan v,
own =own v ⦈"

lemma move_keeps_length:"∥ext v∥ = ∥ext (move ts ts' v)∥"
using real_int.shift_keeps_length by (simp add: move_def)

lemma move_keeps_lanes:"lan v = lan (move ts ts' v)" using move_def by simp

lemma move_keeps_owner:"own v = own (move ts ts' v)" using move_def by simp

lemma move_nothing :"move ts ts v = v" using real_int.shift_zero move_def by simp

lemma move_trans:
"(ts ❙⇒ ts') ∧ (ts' ❙⇒ts'') ⟶ move ts' ts'' (move ts ts' v) = move ts ts'' v"
proof
assume assm:"(ts ❙⇒ ts') ∧ (ts' ❙⇒ts'')"
have
"(pos ts'' (own v)) - pos ts (own v)
= (pos ts'' (own v) + pos ts' (own v)) - ( pos ts (own v) + pos ts' (own v))"
by simp
have
"move ts' ts'' (move ts ts' v) =
⦇ ext =
shift (ext (move ts ts' v))
(pos ts'' (own (move ts ts' v)) - pos ts' (own (move ts ts' v))),
lan = lan (move ts ts' v),
own = own (move ts ts' v) ⦈ "
using move_def by blast
hence "move ts' ts'' (move ts ts' v) =
⦇ ext = shift (ext (move ts ts' v)) (pos ts'' (own v) - pos ts' (own  v)),
lan = lan  v, own = own  v ⦈ "
using move_def by simp
then show "move ts' ts'' (move ts ts' v) = move ts ts'' v"
proof -
have f2: "∀x0 x1. (x1::real) + x0 = x0 + x1"
by auto
have
"pos ts'' (own v)
+ -1*pos ts' (own v)+(pos ts' (own v) + -1*pos ts (own v))
= pos ts'' (own v) + - 1 * pos ts (own v)"
by auto
then have
"(shift (ext v) ((pos ts'' (own v)) + ( -1 *  pos ts (own v)))) =
shift (shift  (ext v) (pos ts' (own v) + - 1 * pos ts (own v)))
(pos ts'' (own v) + - 1 * pos ts' (own v))"
then show ?thesis
using move_def f2 by simp
qed
qed

lemma move_stability_res:"(ts❙─r(c)❙→ts') ⟶ move ts ts' v = v"
and move_stability_clm: "(ts❙─c(c,n)❙→ts') ⟶ move ts ts' v = v"
and move_stability_wdr:"(ts❙─wdr(c,n)❙→ts') ⟶ move ts ts' v = v"
and move_stability_wdc:"(ts❙─wdc(c)❙→ts') ⟶ move ts ts' v = v"
using create_reservation_def create_claim_def withdraw_reservation_def
withdraw_claim_def move_def move_nothing
by (auto)+

end
end


# Theory Sensors

(*  Title:     Sensors.thy

Defines perfect sensors for cars. Cars can perceive both
the physical size and braking distance of all other cars.
*)

section‹ Sensors for Cars›
text‹
This section presents the abstract definition of a function
determining the sensor capabilities of cars. Such a function
takes a car $$e$$, a traffic snapshot $$ts$$ and another
car $$c$$, and returns the length of $$c$$ as perceived
by $$e$$ at the situation determined by $$ts$$. The
only restriction we impose is that this length is always
greater than zero.

With such a function, we define a derived notion of the
\emph{space} the car $$c$$ occupies as perceived by $$e$$.
However, this does not define the lanes $$c$$ occupies, but
only a continuous interval. The lanes occupied by $$c$$
are given by the reservation and claim functions of
the traffic snapshot $$ts$$.
›

theory Sensors
imports "Traffic" "Views"
begin

locale sensors = traffic + view +
fixes sensors::"(cars) ⇒ traffic ⇒ (cars) ⇒ real"
assumes sensors_ge:"(sensors e ts c) > 0"
begin

definition space ::" traffic ⇒ view ⇒ cars ⇒ real_int"
where "space ts v c ≡ Abs_real_int (pos ts c, pos ts c + sensors (own v) ts c)"

lemma left_space: "left (space ts v c) = pos ts c"
proof -
have 1:"pos ts c < pos ts c + sensors (own v) ts c" using sensors_ge
by (metis (no_types, hide_lams)  less_add_same_cancel1  )
show "left (space ts v c ) = pos ts c"
using space_def Abs_real_int_inverse 1 by simp
qed

lemma right_space: "right (space ts v c) =   pos ts c + sensors (own v) ts c"
proof -
have 1:"pos ts c < pos ts c + sensors (own v) ts c" using sensors_ge
by (metis (no_types, hide_lams)  less_add_same_cancel1  )
show 3:"right(space ts v c ) = pos ts c + sensors (own v) ts c"
using space_def Abs_real_int_inverse 1 by simp
qed

lemma space_nonempty:"left (space ts v c ) < right (space ts v c)"
using left_space right_space sensors_ge by simp

end
end


# Theory Length

(*  Title:      Length.thy

The length of cars visible to the owner of a given view.
*)

section‹Visible Length of Cars with Perfect Sensors›
text‹
Given a sensor function, we can define the length
of a car $$c$$ as perceived by the owner of a view $$v$$. This
length is restricted by the size of the extension of the view $$v$$,
but always given by a continuous interval, which may possibly
be degenerate (i.e., a point-interval).

The lemmas connect the end-points of the perceived length
with the end-points of the current view. Furthermore, they
show how the chopping and subview relations affect
the perceived length of a car.
›

theory Length
imports  Sensors
begin

context sensors
begin

definition len:: "view ⇒ traffic ⇒ cars ⇒ real_int"
where len_def :"len v ( ts ) c ==
if (left (space ts v c) > right (ext v))
then  Abs_real_int (right (ext v),right (ext v))
else
if (right (space ts v c) < left (ext v))
then Abs_real_int (left (ext v),left (ext v))
else
Abs_real_int (max (left (ext v)) (left (space ts v c)),
min (right (ext v)) (right (space ts v c)))"

lemma len_left: " left ((len v  ts) c) ≥ left (ext v)"
using Abs_real_int_inverse left_leq_right sensors.len_def sensors_axioms by auto

lemma len_right: " right ((len v  ts) c) ≤ right (ext v)"
using Abs_real_int_inverse left_leq_right sensors.len_def sensors_axioms by auto

lemma len_sub_int:"len v ts c ≤ ext v"
using less_eq_real_int_def len_left len_right by blast

lemma len_space_left:
"left (space ts v c) ≤ right (ext v) ⟶ left (len v ts c) ≥ left (space ts v c)"
proof
assume assm:"left (space ts v c) ≤ right (ext v)"
then show "left (len v ts c) ≥ left (space ts v c)"
proof (cases "right ((space ts v) c) < left (ext v)" )
case True
then show ?thesis using len_def len_left real_int.left_leq_right
by (meson le_less_trans not_less order.asym)
next
case False
then have "len v ts c =
Abs_real_int ((max (left (ext v)) (left ((space ts v) c))),
min (right (ext v)) (right ((space ts v) c)))"
using len_def assm by auto
then have "left (len v ts c) = max (left (ext v)) (left ((space ts v) c))"
using Abs_real_int_inverse False assm real_int.left_leq_right
by auto
then show ?thesis  by linarith
qed
qed

lemma len_space_right:
"right (space ts v c) ≥ left (ext v) ⟶ right (len v ts c) ≤ right (space ts v c)"
proof
assume assm:"right (space ts v c) ≥ left (ext v)"
then show "right (len v ts c) ≤ right (space ts v c)"
proof (cases "left ((space ts v) c) > right (ext v)" )
case True
then show ?thesis using len_def len_right real_int.left_leq_right
by (meson le_less_trans not_less order.asym)
next
case False
then have "len v ts c =
Abs_real_int (max (left (ext v)) (left ((space ts v) c)),
min (right (ext v)) (right ((space ts v) c)))"
using len_def assm by auto
then have "right (len v ts c) = min (right (ext v)) (right ((space ts v) c))"
using Abs_real_int_inverse False assm real_int.left_leq_right
by auto
then show ?thesis  by linarith
qed
qed

lemma len_hchop_left_right_border:
"(len v ts c = ext v) ∧ (v=v1∥v2) ⟶ (right (len v1 ts c) = right (ext v1))"
proof
assume assm:"((len v ts) c = ext v) ∧ (v=v1∥v2)"
have l1:"left ((len v ts) c) = left (ext v)" using assm by auto
from assm have l2:"left (ext v) = left (ext v1)"
from l1 and l2 have l3:"left ((len v ts) c) = left (ext v1)" by simp
have r1:"right ((len v ts) c) = right (ext v)" using assm by auto
have r2:"right (ext v1) ≤ right (ext v)"
by (metis (no_types, lifting) assm hchop_def real_int.rchop_def
real_int.left_leq_right )
have r3:"right ((len v1 ts) c) ≤ right (ext v1)"
using len_right by blast
show "right ((len v1 ts) c) = right (ext v1)"
proof (rule ccontr)
assume contra:"right ((len v1 ts) c) ≠ right (ext v1)"
with r3 have less:"right ((len v1 ts) c) < right (ext v1)" by simp
show False
proof (cases "left ((space ts v) c) ≤ right (ext v1)")
assume neg1:"¬ left ((space ts v) c) ≤ right (ext v1)"
have "right ((len v1 ts) c) = right (ext v1)"
using Abs_real_int_inverse left_space len_def neg1 right.rep_eq by auto
with contra show False ..
next
assume less1:"left ((space ts v) c) ≤ right (ext v1)"
show False
proof (cases "right ((space ts v) c) ≥ left (ext v1)")
assume neg2:"¬ left (ext v1) ≤ right ((space ts v) c)"
have "right ((len v1 ts) c) = right (ext v1)"
proof -
have "(len v1 ts) c = Abs_real_int (left (ext v1),left (ext v1))"
using len_def  neg2 assm hchop_def real_int.left_leq_right less1 space_def
by auto
hence  "right ((len v1 ts) c) = left ((len v1 ts )c)"
using l3 assm contra less1 len_def neg2 r2 r3  real_int.left_leq_right
by auto
with l1 have r4:"right((len v1 ts)c ) = right (ext v)"
using assm l2 len_def neg2 assm hchop_def less1 real_int.left_leq_right r2
space_def
by auto
hence "right (ext v) = right (ext v1)"
using r2 r3 by auto
thus "right ((len v1 ts) c) = right (ext v1)"
using r4 by auto
qed
with contra  show False ..
next
assume less2:"left (ext v1) ≤ right ((space ts v) c)"
have len_in_type:
"(max (left (ext v1)) (left ((space ts v) c)),
min (right (ext v1)) (right ((space ts v) c)))
∈ {r :: real*real . fst r ≤ snd r}"
using Rep_real_int less1 less2 by auto
from less1 and less2 have len_def_v1:"len v1 (ts) c =
Abs_real_int ((max (left (ext v1)) (left ((space ts v) c))),
min (right (ext v1)) (right ((space ts v) c)))"
using len_def assm hchop_def  space_def  by auto
with less have
"min (right (ext v1)) (right ((space ts v) c)) = right ((space ts v) c)"
using Abs_real_int_inverse len_in_type snd_conv by auto
hence "right ((space ts v) c) ≤ right (ext v1)" by simp
hence "right ((space ts v) c) ≤ right (ext v)"
using r2 by linarith
from len_def_v1 and less and len_in_type
have "right ((space ts v) c) < right (ext v1)"
using Abs_real_int_inverse sndI by auto
hence r4:"right ((space ts v) c) < right (ext v)"
using r2 by linarith
from assm have len_v_in_type:
"(max (left (ext v)) (left ((space ts v) c)),
min (right (ext v)) (right ((space ts v) c)))
∈ {r :: real*real . fst r ≤ snd r}"
using r4 l2 len_in_type by auto
hence " right (len v ( ts) c) ≠ right (ext v)"
using Abs_real_int_inverse Pair_inject r4 len_def real_int.left_leq_right
surjective_pairing by auto
with r1 show False by best
qed
qed
qed
qed

lemma len_hchop_left_left_border:
"((len v ts) c = ext v) ∧ (v=v1∥v2) ⟶ (left ((len v1 ts) c) = left (ext v1))"
proof
assume assm:"((len v ts) c = ext v) ∧ (v=v1∥v2)"
have l1:"left ((len v ts) c) = left (ext v)" using assm by auto
from assm have l2:"left (ext v) = left (ext v1)"
by (simp add: hchop_def real_int.rchop_def )
from l1 and l2 have l3:"left ((len v ts) c) = left (ext v1)" by simp
have r1:"right ((len v ts) c) = right (ext v)" using assm by auto
have r2:"right (ext v1) ≤ right (ext v)"
by (metis (no_types, lifting) assm hchop_def real_int.rchop_def
real_int.left_leq_right )
have r3:"right ((len v1 ts) c) ≤ right (ext v1)"
using len_right by blast
show "(left ((len v1 ts) c) = left (ext v1))"
proof (cases
"left ((space ts v) c) ≤ right (ext v1) ∧ right ((space ts v) c) ≥ left (ext v1)")
case True
show "(left ((len v1 ts) c) = left (ext v1))"
proof (rule ccontr)
assume neq:" left (len v1 ( ts) c) ≠ left (ext v1)"
then have greater: "left (len v1 ( ts) c) > left (ext v1)"
by (meson dual_order.order_iff_strict len_left)
have len_in_type:
"(max (left (ext v1)) (left ((space ts v) c)),
min (right (ext v1)) (right ((space ts v) c)))
∈ {r :: real*real . fst r ≤ snd r}"
using Rep_real_int True by auto
from True have "len v1 ( ts) c =
Abs_real_int ((max (left (ext v1)) (left ((space ts v) c))),
min (right (ext v1)) (right ((space ts v) c)))"
using len_def assm hchop_def space_def  by auto
hence maximum:
"left (len v1 ( ts) c) = max (left (ext v1)) (left ((space ts v) c))"
using Abs_real_int_inverse len_in_type by auto
have "max (left (ext v1)) (left ((space ts v) c)) = left ((space ts v) c)"
using maximum neq by linarith
hence "left ((space ts v) c) > left (ext v1)"
using greater maximum by auto
hence l4:"left ((space ts v) c) > left (ext v)" using l2 by auto
with assm have len_v_in_type:
"(max (left (ext v)) (left ((space ts v) c)),
min (right (ext v)) (right ((space ts v) c)))
∈ {r :: real*real . fst r ≤ snd r}"
using len_in_type r2 by auto
hence " left (len v ( ts) c) ≠ left (ext v)"
using Abs_real_int_inverse l4 sensors.len_def sensors_axioms by auto
thus False using l1 by best
qed
next
case False
then have
"¬left ((space ts v) c) ≤ right (ext v1) ∨ ¬right ((space ts v) c) ≥ left (ext v1)"
by auto
then show "(left ((len v1 ts) c) = left (ext v1))"
proof
assume negative:"¬ left ((space ts v) c) ≤ right (ext v1)"
then have "len v1 ( ts) c = Abs_real_int (right (ext v1),right (ext v1))"
using len_def assm hchop_def space_def by auto
hence empty:"left (len v1 ( ts) c) = right (len v1 ( ts) c)"
by (metis real_int.chop_assoc2 real_int.chop_singleton_right real_int.rchop_def)
have len_geq:"left(len v1 ( ts) c) ≥ left (ext v)"
using l2 len_left by auto
show "left (len v1 ( ts) c) = left (ext v1)"
proof (rule ccontr)
assume contra:"left (len v1 ( ts) c) ≠ left (ext v1)"
with len_left have "left (ext v1) < left (len v1 ( ts) c)  "
using dual_order.order_iff_strict by blast
hence l5:"left (ext v) < left (len v1 ( ts) c)" using l2 by auto
hence l6:"left (len v ( ts) c) < left (len v1 ( ts) c)" using l1 by auto
show "False"
proof (cases "left ((space ts v) c) ≤ right (ext v)")
case True
have well_sp:"left ((space ts v) c) ≤ right ((space ts v) c)"
using real_int.left_leq_right by auto
have well_v:"left (ext v) ≤ right (ext v)"
using real_int.left_leq_right by auto
hence rs_geq_vl:"right ((space ts v) c) ≥ left (ext v)"
using empty len_geq negative r3 well_sp by linarith
from True and rs_geq_vl have len_in_type:
"(max (left (ext v)) (left ((space ts v) c)),
min (right (ext v)) (right ((space ts v) c)))
∈ {r :: real*real . fst r ≤ snd r}"
using CollectD CollectI Rep_real_int fst_conv snd_conv by auto
have "len v (ts) c  =
Abs_real_int (max (left (ext v)) (left ((space ts v) c)),
min (right (ext v)) (right ((space ts v) c)))"
using len_def using True rs_geq_vl by auto
hence max_less:
"max (left (ext v)) (left ((space ts v) c)) <  left (len v1 ( ts) c)"
using Abs_real_int_inverse
by (metis (full_types) l5 assm fst_conv left.rep_eq len_in_type)
show False
using empty max_less negative r3 by auto
next
case False
then have "len v ( ts) c = Abs_real_int (right (ext v), right (ext v))"
using len_def by auto
hence empty_len_v:"left (len v ( ts) c) = right (ext v)" using Abs_real_int_inverse
by simp
show False
using l6 empty empty_len_v r2 r3 by linarith
qed
qed
next
have "space ts v1 c ≤ space ts v c" using assm hchop_def space_def  by auto
hence r4:"right (space ts v1 c) ≤ right (space ts v c)"
using  less_eq_real_int_def by auto
assume left_outside:"¬ left (ext v1) ≤ right ((space ts v) c)"
hence "left (ext v1 ) > right (space ts v1 c)" using r4 by linarith
then have "len v1 ( ts) c = Abs_real_int (left (ext v1),left (ext v1))"
using len_def assm hchop_def real_int.left_leq_right r1 r2 l1 l2 l3 r3
by (meson le_less_trans less_trans not_less)
thus "(left ((len v1 ts) c) = left (ext v1))"
using  Abs_real_int_inverse by auto
qed
qed
qed

lemma len_view_hchop_left:
"((len v ts) c = ext v) ∧ (v=v1∥v2) ⟶ ((len v1 ts) c = ext v1)"
by (metis Rep_real_int_inverse left.rep_eq len_hchop_left_left_border
len_hchop_left_right_border prod.collapse right.rep_eq)

lemma len_hchop_right_left_border:
"((len v ts) c = ext v) ∧ (v=v1∥v2) ⟶ (left ((len v2 ts) c) = left (ext v2))"
proof
assume assm:"((len v ts) c = ext v) ∧ (v=v1∥v2)"
have r1:"right ((len v ts) c) = right (ext v)" using assm by auto
from assm have r2:"right (ext v) = right (ext v2)"
by (simp add: hchop_def real_int.rchop_def )
from r1 and r2 have r3:"right ((len v ts) c) = right (ext v2)" by simp
have l1:"left ((len v ts) c) = left (ext v)" using assm by auto
have l2:"left (ext v2) ≥ left (ext v)"
using assm less_eq_real_int_def real_int.chop_leq2 view.hchop_def by blast
have l3:"left ((len v2 ts) c) ≥ left (ext v2)"
using len_left by blast
show "left ((len v2 ts) c) = left (ext v2)"
proof (rule ccontr)
assume contra:"left ((len v2 ts) c) ≠ left (ext v2)"
with l3 have less:"left ((len v2 ts) c) > left (ext v2)" by simp
show False
proof (cases "left ((space ts v) c) ≤ right (ext v2)")
assume neg1:"¬ left ((space ts v) c) ≤ right (ext v2)"
have "left ((len v2 ts) c) = left (ext v2)"
proof -
have "(len v2 ts) c = Abs_real_int (right (ext v2),right (ext v2))"
using len_def  neg1 assm hchop_def space_def  by auto
thus "left ((len v2 ts) c) = left (ext v2)"
using assm l2 l3 len_def neg1 r3 by auto
qed
with contra show False ..
next
assume less1:"left ((space ts v) c) ≤ right (ext v2)"
show False
proof (cases "right ((space ts v) c) ≥ left (ext v2)")
assume neg2:"¬ left (ext v2) ≤ right ((space ts v) c)"
have "space ts v2 c ≤ space ts v c" using assm hchop_def space_def  by auto
hence "right (space ts v2 c) ≤ right (space ts v c)" using less_eq_real_int_def
by auto
with neg2 have greater:"left (ext v2 ) > right (space ts v2 c)" by auto
have "left ((len v2 ts) c) = left (ext v2)"
proof -
have len_empty:"(len v2 ts) c = Abs_real_int (left (ext v2),left (ext v2))"
using len_def  neg2 assm hchop_def   less1 space_def by auto
have l4:"left((len v2 ts)c ) = left (ext v)"
using Abs_real_int_inverse len_def less neg2  assm hchop_def
CollectI len_empty prod.collapse prod.inject by auto
hence "left (ext v) = left (ext v2)"
using l2 l3 by auto
thus "left ((len v2 ts) c) = left (ext v2)" using l4 by auto
qed
with contra  show False ..
next
assume less2:"left (ext v2) ≤ right ((space ts v) c)"
have len_in_type:
"(max (left (ext v2)) (left ((space ts v) c)),
min (right (ext v2)) (right ((space ts v) c)))
∈ {r :: real*real . fst r ≤ snd r}"
using Rep_real_int less1 less2 by auto
from less1 and less2 have len_def_v2:"len v2 ( ts) c =
Abs_real_int (max (left (ext v2)) (left ((space ts v) c)),
min (right (ext v2)) (right ((space ts v) c)))"
using len_def assm hchop_def space_def  by auto
with less have
"max (left (ext v2)) (left ((space ts v) c)) = left ((space ts v) c)"
using Abs_real_int_inverse len_in_type snd_conv by auto
hence "left ((space ts v) c) ≥ left (ext v2)" by simp
hence "left ((space ts v) c) ≥ left (ext v)"
using l2 by auto
from len_def_v2 and less and len_in_type
have "left ((space ts v) c) > left (ext v2)"
using Abs_real_int_inverse sndI by auto
hence l5:"left ((space ts v) c) > left (ext v)"
using l2 by linarith
with assm have len_v_in_type:
"(max (left (ext v)) (left (space ts v c)),
min (right (ext v)) (right (space ts v c)))
∈ {r :: real*real . fst r ≤ snd r}"
using r2 len_in_type by auto
hence "left (len v ( ts) c) ≠ left (ext v)"
using Abs_real_int_inverse Pair_inject l5 len_def real_int.left_leq_right
surjective_pairing by auto
with l1 show False by best
qed
qed
qed
qed

lemma len_hchop_right_right_border:
"((len v ts) c = ext v) ∧ (v=v1∥v2) ⟶ (right ((len v2 ts) c) = right (ext v2))"
proof
assume assm:"((len v ts) c = ext v) ∧ (v=v1∥v2)"
have r1:"right ((len v ts) c) = right (ext v)" using assm by auto
from assm have r2:"right (ext v) = right (ext v2)"
by (simp add: hchop_def real_int.rchop_def )
from r1 and r2 have r3:"right ((len v ts) c) = right (ext v2)" by simp
have l1:"left ((len v ts) c) = left (ext v)" using assm by auto
have l2:"left (ext v2) ≤ right (ext v)"
using assm view.h_chop_middle2 by blast
have l3:"left ((len v2 ts) c) ≥ left (ext v2)"
using len_left by blast
show "(right ((len v2 ts) c) = right (ext v2))"
proof (cases
"left ((space ts v) c) ≤ right (ext v2) ∧ right ((space ts v) c) ≥ left (ext v2)")
case True
show "(right ((len v2 ts) c) = right (ext v2))"
proof (rule ccontr)
assume neq:" right (len v2 ( ts) c) ≠ right (ext v2)"
then have lesser: "right (len v2 ( ts) c) < right (ext v2)"
using len_right less_eq_real_def by blast
have len_in_type:
"(max (left (ext v2)) (left (space ts v c)),
min (right (ext v2)) (right (space ts v c)))
∈ {r :: real*real . fst r ≤ snd r}"
using Rep_real_int True by auto
from True have
"len v2 ( ts) c =
Abs_real_int (max (left (ext v2)) (left (space ts v c)),
min (right (ext v2)) (right (space ts v c)))"
using len_def assm hchop_def space_def by auto
hence maximum:
"right (len v2 ( ts) c) = min (right (ext v2)) (right ((space ts v) c))"
using Abs_real_int_inverse len_in_type by auto
have min_right:
"min (right (ext v2)) (right ((space ts v) c)) = right ((space ts v) c)"
using maximum neq by linarith
hence "right ((space ts v) c) < right (ext v2)"
using lesser maximum by auto
hence right_v:"right ((space ts v) c) < right (ext v)"
using r2 by auto
have right_inside:"right ((space ts v) c) ≥ left (ext v)"
by (meson True assm less_eq_real_int_def less_eq_view_ext_def
order_trans view.horizontal_chop_leq2)
with assm and True and right_inside
have len_v_in_type:
"(max (left (ext v)) (left (space ts v c)),
min (right (ext v)) (right (space ts v c)))
∈ {r :: real*real . fst r ≤ snd r}"
using min_right r2 real_int.left_leq_right by auto
hence " right (len v ( ts) c) ≠ right (ext v)"
using Abs_real_int_inverse Pair_inject right_v len_def
real_int.left_leq_right surjective_pairing
by auto
thus False using r1 by best
qed
next
case False
then have "¬left ((space ts v) c) ≤ right (ext v2) ∨
¬right ((space ts v) c) ≥ left (ext v2)"
by auto
thus "right ((len v2 ts) c) = right (ext v2)"
proof
assume negative:"¬ left ((space ts v) c) ≤ right (ext v2)"
show ?thesis
using left_space negative r1 r3 sensors.len_def sensors_axioms by auto
next
assume left_outside:"¬ left (ext v2) ≤ right ((space ts v) c)"
hence "left (ext v2) > right (space ts v2 c)"
using assm hchop_def space_def by auto
then have len:"len v2 ( ts) c = Abs_real_int (left (ext v2),left (ext v2))"
by (metis (no_types, hide_lams) len_def l2 le_less_trans not_less order.asym
space_nonempty r2)
show "(right ((len v2 ts) c) = right (ext v2))"
proof (cases "right ((space ts v) c) ≥ left (ext v)")
assume "¬ left (ext v) ≤ right ((space ts v) c)"
hence len_empty:"len v (ts) c = Abs_real_int (left (ext v), left (ext v))"
using len_def real_int.left_leq_right Abs_real_int_inverse
by (meson less_trans not_less space_nonempty)
show "(right ((len v2 ts) c) = right (ext v2))"
by (metis (no_types, hide_lams) Rep_real_int_inverse assm dual_order.antisym
left.rep_eq len len_empty prod.collapse real_int.chop_singleton_left
real_int.rchop_def right.rep_eq view.h_chop_middle1 view.hchop_def)
next
assume "left (ext v) ≤ right ((space ts v) c)"
then show ?thesis
using l2 left_outside len_space_right r1  by fastforce
qed
qed
qed
qed

lemma len_view_hchop_right:
"((len v ts) c = ext v) ∧ (v=v1∥v2) ⟶ ((len v2 ts) c = ext v2)"
by (metis Rep_real_int_inverse left.rep_eq len_hchop_right_left_border
len_hchop_right_right_border prod.collapse right.rep_eq)

lemma len_compose_hchop:
"(v=v1∥v2) ∧ (len v1 ( ts) c = ext v1) ∧ (len v2 ( ts) c = ext v2)
⟶ (len v ( ts) c = ext v)"
proof
assume assm:"(v=v1∥v2) ∧ (len v1 ( ts) c = ext v1) ∧ (len v2 ( ts) c = ext v2)"
then have left_v1:"left (len v1 ( ts) c) = left (ext v1)" by auto
from assm have right_v1:"right (len v1 ( ts) c) = left (ext v2)"
by (simp add: hchop_def real_int.rchop_def )
from assm have left_v2:"left (len v2 ( ts) c) = right (ext v1)"
using right_v1 by auto
from assm have right_v2:"right (len v2 ( ts) c) = right (ext v2)" by auto
show "(len v ( ts) c = ext v)"
proof (cases " left ((space ts v) c) > right (ext v)")
case True
then have "left (space ts v c) > right (ext v2)" using assm right_v2
by (simp add: hchop_def real_int.rchop_def )
then have "left (space ts v2 c) > right( ext v2)"
using assm hchop_def sensors.space_def sensors_axioms  by auto
then have "len v2 ts c = Abs_real_int(right (ext v2), right (ext v2))"
using len_def by simp
then have "ext v2 = Abs_real_int(right (ext v2), right (ext v2))" using assm by simp
then have "∥ext v2∥ = 0"
by (metis Rep_real_int_inverse fst_conv left.rep_eq
real_int.chop_singleton_right real_int.length_zero_iff_borders_eq
real_int.rchop_def right.rep_eq snd_conv surj_pair)
then have "ext v = ext v1"
using assm hchop_def real_int.rchop_def real_int.chop_empty2
by simp
then show ?thesis
using assm hchop_def len_def sensors.space_def sensors_axioms
by auto
next
case False
then have in_left:"left (space ts v c) ≤ right (ext v)" by simp
show "len v ts c = ext v"
proof (cases "right (space ts v c) < left (ext v)")
case True
then have "right (space ts v c) < left (ext v1)" using assm left_v1
then have out_v1:"right (space ts v1 c) < left (ext v1)"
using assm hchop_def sensors.space_def sensors_axioms  by auto
then have "len v1 ts c = Abs_real_int(left (ext v1), left (ext v1))"
using len_def in_left
by (meson le_less_trans less_trans not_le real_int.left_leq_right)
then have "ext v1 = Abs_real_int (left (ext v1), left (ext v1))" using assm by simp
then have "∥ext v1∥ = 0"
real_int.length_zero_iff_borders_eq real_int.rchop_def real_int.shift_def
real_int.shift_zero)
then have "ext v = ext v2" using assm hchop_def real_int.rchop_def real_int.chop_empty1
by auto
then show ?thesis
using assm hchop_def len_def sensors.space_def sensors_axioms by auto
next
case False
then  have in_right:"right (space ts v c) ≥ left (ext v)"  by simp
have f1: "own v = own v2" using assm hchop_def
by (auto)
have f2: "own v = own v1"
using assm hchop_def  by auto
have chop:"R_Chop(ext v,ext v1,ext v2)" using assm hchop_def
by (auto )
have len:"len v ts c = Abs_real_int(max (left (ext v)) (left (space ts v c)),
min (right (ext v)) (right (space ts v c)))"
using len_def in_left in_right by simp
have len1:"len v1 ts c = Abs_real_int(max (left (ext v1)) (left (space ts v1 c)),
min (right (ext v1)) (right (space ts v1 c)))"
by (metis assm f2 f1 chop assm in_left in_right len_def len_space_left
not_le real_int.rchop_def space_def)
then have "max (left (ext v1)) (left (space ts v1 c)) = left (len v1 ts c)"
by (metis assm chop f1 f2 in_left len_space_left max.orderE
real_int.rchop_def space_def)
then have left_border:"max (left (ext v1)) (left (space ts v1 c)) = left (ext v1)"
using left_v1 by simp
have len2:"len v2 ts c = Abs_real_int(max (left (ext v2)) (left (space ts v2 c)),
min (right (ext v2)) (right (space ts v2 c)))"
by (metis len_def in_left in_right assm f2 f1 chop len_space_right not_le
real_int.rchop_def space_def)
then have "min (right (ext v2)) (right (space ts v2 c)) = right (len v2 ts c)"
by (metis assm chop f1 f2 in_right len_space_right min.absorb_iff1
real_int.rchop_def space_def)
then have right_border:
"min (right (ext v2)) (right (space ts v2 c)) = right (ext v2)"
using right_v2 by simp
have "left (space ts v c) = left (space ts v1 c)"
using assm hchop_def sensors.space_def sensors_axioms by auto
then have max:
"  max (left (ext v)) (left (space ts v c))
= max (left (ext v1)) (left (space ts v1 c))"
using assm hchop_def real_int.rchop_def  by auto
have "right (space ts v c) = right (space ts v2 c)"
using assm hchop_def sensors.space_def sensors_axioms by auto
then have min:
"  min (right (ext v)) (right (space ts v c))
= min (right (ext v2)) (right (space ts v2 c))"
using assm hchop_def real_int.rchop_def by auto
show ?thesis
by (metis min max left_border right_border False add.right_neutral
chop in_left len_def not_le real_int.rchop_def real_int.shift_def
real_int.shift_zero)
qed
qed
qed

lemma len_stable:"(v=v1--v2) ⟶ len v1 ts c = len v2 ts c"
proof
assume assm:"v=v1--v2"
then have ext_eq1:"ext v = ext v1" and ext_eq2:"ext v = ext v2"
using vchop_def by auto
hence ext1_eq_ext2:"ext v1 = ext v2" by simp
show "len v1 ts c = len v2 ts c"
using assm ext1_eq_ext2 left_space right_space sensors.len_def sensors_axioms
view.vertical_chop_own_trans by auto
qed

lemma len_empty_on_subview1:
"∥len v ( ts) c∥ = 0 ∧ (v=v1∥v2) ⟶ ∥len v1 ( ts) c∥ = 0"
proof
assume assm:"∥len v ( ts) c∥ = 0 ∧ (v=v1∥v2)"
then have len_v_borders:"left (len v ( ts) c) = right (len v ( ts) c)"
show "∥len v1 ( ts) c∥ = 0"
proof (cases "left ((space ts v) c) > right (ext v1)")
assume left_outside_v1:"left ((space ts v) c) > right (ext v1)"
thus "∥len v1 ( ts) c∥ = 0"
using Abs_real_int_inverse assm fst_conv hchop_def len_def real_int.length_zero_iff_borders_eq
mem_Collect_eq snd_conv space_def  by auto
next
assume left_inside_v1:"¬left ((space ts v) c) > right (ext v1)"
show "∥len v1 ( ts) c∥ = 0"
proof (cases "left (ext v1) > right ((space ts v) c)")
assume right_outside_v1:"left (ext v1) > right ((space ts v) c)"
hence "left (ext v1) > right ((space ts v1) c)" using assm hchop_def space_def
by auto
thus "∥len v1 (ts) c∥ = 0"
using assm hchop_def len_def real_int.length_def  Abs_real_int_inverse by auto
next
assume right_inside_v1:"¬left (ext v1) > right ((space ts v) c)"
have len_v1:
"len v1 ( ts) c = Abs_real_int (max (left (ext v1)) (left (space ts v c)),
min (right (ext v1)) (right (space ts v c)))"
using left_inside_v1 len_def right_inside_v1 assm hchop_def space_def by auto
from left_inside_v1 and right_inside_v1 have inside_v:
"¬left (space ts v c) > right (ext v) ∧ ¬left (ext v) > right (space ts v c)"
proof -
have "fst (Rep_real_int (ext v2)) ≤ snd (Rep_real_int (ext v))"
using assm view.h_chop_middle2 by force
then show ?thesis
using assm left_inside_v1 real_int.rchop_def right_inside_v1 view.hchop_def
by force
qed
hence len_v:
"len v ts c = Abs_real_int (max (left (ext v)) (left (space ts v c)),
min (right (ext v)) (right (space ts v c)))"
have less_eq:
"  max (left (ext v)) (left (space ts v c))
≤ min (right (ext v)) (right (space ts v c))"
using inside_v real_int.left_leq_right by auto
from len_v have len_v_empty:
"  max (left (ext v)) (left ((space ts v) c))
= min (right (ext v)) (right ((space ts v) c))"
using Abs_real_int_inverse Rep_real_int_inverse inside_v
len_v_borders local.less_eq by auto
have left_len_eq:
" max (left (ext v)) (left (space ts v c))
= max (left (ext v1)) (left (space ts v c))"
using assm hchop_def real_int.rchop_def  by auto
have right_len_leq:
"  min (right (ext v)) (right (space ts v c))
≥ min (right (ext v1)) (right (space ts v c))"
by (metis (no_types, hide_lams) assm min.bounded_iff min_less_iff_conj not_le
order_refl real_int.rchop_def view.h_chop_middle2 view.hchop_def)
hence left_geq_right:
"  max (left (ext v1)) (left (space ts v c))
≥ min (right (ext v1)) (right (space ts v c))"
using left_len_eq len_v_empty by auto
thus "∥len v1 ( ts) c∥ = 0"
proof -
have f1:
" ¬ max (left (ext v)) (left (space ts v c))
≤ min (right (ext v1)) (right (space ts v c))
∨
min (right (ext v1)) (right (space ts v c))
= max (left (ext v)) (left (space ts v c))"
by (metis antisym_conv left_geq_right left_len_eq)
have
"⋀r. ¬ left (ext v1) ≤ r
∨ ¬ left (space ts v c) ≤ r
∨ max (left (ext v)) (left (space ts v c)) ≤ r"
using left_len_eq by auto
then have
"  min (right (ext v1)) (right (space ts v c))
= max (left (ext v)) (left (space ts v c))"
using f1 inside_v left_inside_v1 real_int.left_leq_right by force
then show ?thesis
using assm left_len_eq len_v len_v1 len_v_empty by auto
qed
qed
qed
qed

lemma len_empty_on_subview2:
"∥len v ts c∥ = 0 ∧ (v=v1∥v2) ⟶ ∥len v2 ts c∥ = 0"
proof
assume assm:"∥len v ( ts) c∥ = 0 ∧ (v=v1∥v2)"
then have len_v_borders:"left (len v ( ts) c) = right (len v ( ts) c)"
show "∥len v2 ( ts) c∥ = 0"
proof (cases "left ((space ts v) c) > right (ext v2)")
assume left_outside_v2:"left ((space ts v) c) > right (ext v2)"
thus "∥len v2 ( ts) c∥ = 0"
using Abs_real_int_inverse assm fst_conv hchop_def len_def
real_int.length_zero_iff_borders_eq mem_Collect_eq snd_conv space_def
by auto
next
assume left_inside_v2:"¬left (space ts v c) > right (ext v2)"
show "∥len v2 ( ts) c∥ = 0"
proof (cases "left (ext v2) > right (space ts v c)")
assume right_outside_v2:"left (ext v2) > right ((space ts v) c)"
thus "∥len v2 ( ts) c∥ = 0"
using Abs_real_int_inverse assm fst_conv hchop_def len_def
real_int.length_zero_iff_borders_eq mem_Collect_eq snd_conv
right_outside_v2 space_def
by auto
next
assume right_inside_v2:"¬left (ext v2) > right ((space ts v) c)"
have len_v2:
"len v2 ts c = Abs_real_int (max (left (ext v2)) (left (space ts v c)),
min (right (ext v2)) (right (space ts v c)))"
using left_inside_v2 len_def right_inside_v2 assm hchop_def space_def by auto
from left_inside_v2 and right_inside_v2 have inside_v:
"¬left ((space ts v) c) > right (ext v) ∧ ¬left (ext v) > right ((space ts v) c)"
proof -
have "left (ext v) ≤ right (ext v1)"
using assm view.h_chop_middle1 by auto
then show ?thesis
using assm left_inside_v2 real_int.rchop_def right_inside_v2 view.hchop_def
by force
qed
hence len_v:
"len v ts c = Abs_real_int (max (left (ext v)) (left (space ts v c)),
min (right (ext v)) (right (space ts v c)))"
have less_eq:
"  max (left (ext v)) (left (space ts v c))
≤ min (right (ext v)) (right (space ts v c))"
using inside_v real_int.left_leq_right by auto
from len_v have len_v_empty:
"  max (left (ext v)) (left (space ts v c))
= min (right (ext v)) (right (space ts v c))"
using Abs_real_int_inverse Rep_real_int_inverse inside_v
using len_v_borders local.less_eq by auto
have left_len_eq:
"  max (left (ext v)) (left (space ts v c))
≤ max (left (ext v2)) (left (space ts v c))"
by (metis (no_types, hide_lams) assm left_leq_right max.mono order_refl
real_int.rchop_def view.hchop_def)
have right_len_leq:
"  min (right (ext v)) (right (space ts v c))
= min (right (ext v2)) (right (space ts v c))"
using assm real_int.rchop_def view.hchop_def by auto
hence left_geq_right:
" max (left (ext v2)) (left (space ts v c))
≥ min (right (ext v2)) (right (space ts v c))"
using left_len_eq len_v_empty by auto
then have
"  max (left (ext v2)) (left (space ts v2 c))
≥ min (right (ext v2)) (right (space ts v2 c))"
using assm hchop_def space_def  by auto
then have
"  max (left (ext v2)) (left (space ts v2 c))
= min (right (ext v2)) (right (space ts v2 c))"
by (metis (no_types, hide_lams) antisym_conv assm hchop_def len_v_empty
max_def min.bounded_iff not_le space_def right_inside_v2 right_len_leq
view.h_chop_middle2)
thus "∥len v2 ( ts) c∥ = 0"
by (metis (no_types, hide_lams)  assm hchop_def len_v len_v2 len_v_empty
space_def right_len_leq)
qed
qed
qed

"(v=v1∥v2) ⟶ ∥len v ts c∥ = ∥len v1 ts c∥ + ∥len v2 ts c∥"
proof
assume chop:"v=v1∥v2"
show "∥len v ts c∥ = ∥len v1 ts c∥ + ∥len v2 ts c∥"
proof (cases "left ((space ts v) c) > right (ext v)")
assume outside_right:"left (space ts v c) > right (ext v)"
hence len_zero:"∥len v ( ts) c∥ = 0"
by (simp add: Abs_real_int_inverse  len_def real_int.length_zero_iff_borders_eq
snd_eqD)
with chop have "∥len v1 ts c∥ + ∥len v2 ts c∥ = 0"
thus ?thesis using len_zero by (simp)
next
assume inside_right:"¬left ((space ts v) c) > right (ext v)"
show "∥len v ts c∥ = ∥len v1 ts c∥ + ∥len v2 ts c∥"
proof (cases " left (ext v) > right ((space ts v) c) ")
assume outside_left:" left (ext v) > right (space ts v c) "
hence len_zero:"∥len v ( ts) c∥ = 0"
by (simp add: Abs_real_int_inverse len_def real_int.length_zero_iff_borders_eq
snd_eqD)
with chop have "∥len v1 ts c∥ + ∥len v2 ts c∥ = 0"
thus ?thesis using len_zero by (simp )
next
assume inside_left:" ¬left (ext v) > right ((space ts v) c) "
hence len_def_v:"len v ( ts) c =
Abs_real_int ((max (left (ext v)) (left ((space ts v) c))),
min (right (ext v)) (right ((space ts v) c)))"
using len_def inside_left inside_right by simp
from inside_left and inside_right have
len_in_type:"(max (left (ext v)) (left ((space ts v) c)),
min (right (ext v)) (right ((space ts v) c)))
∈ {r :: real*real . fst r ≤ snd r}"
using CollectD CollectI Rep_real_int fst_conv snd_conv by auto
show "∥len v ( ts) c∥ = ∥len v1 ( ts) c∥ + ∥len v2 ( ts) c∥"
proof (cases "right (len v ( ts) c) < right (ext v1)")
assume inside_v1:"right (len v ( ts) c) < right (ext v1)"
then have min_less_v1:
"min (right (ext v)) (right (space ts v c)) < right (ext v1)"
using Abs_real_int_inverse len_in_type len_def_v by auto
hence outside_v2:"right ((space ts v) c) < left (ext v2)"
proof -
have "left (ext v2) = right (ext v1)"
using chop real_int.rchop_def view.hchop_def by force
then show ?thesis
by (metis (no_types) chop dual_order.order_iff_strict
min_less_iff_conj min_less_v1 not_less view.h_chop_middle2)
qed
hence len_v2_0:"∥len v2 ( ts) c∥ = 0" using  Abs_real_int_inverse len_def
real_int.length_zero_iff_borders_eq outside_v2  snd_eqD Rep_real_int_inverse
chop hchop_def prod.collapse real_int.rchop_def real_int.chop_singleton_right
space_def
by auto
have inside_left_v1:"  ¬left (ext v1) > right ((space ts v) c) "
using chop hchop_def inside_left real_int.rchop_def  by auto
have inside_right_v1:"¬left ((space ts v) c) > right (ext v1)"
by (meson inside_right less_trans min_less_iff_disj min_less_v1
order.asym space_nonempty)
have len1_def:"len v1 ( ts) c =
Abs_real_int ((max (left (ext v1)) (left ((space ts v) c))),
min (right (ext v1)) (right ((space ts v) c)))"
using len_def inside_left_v1 inside_right_v1 chop hchop_def space_def
by auto
hence "∥len v ts c∥ = ∥len v1 ts c∥"
proof -
have "right (ext v1) ≤ right (ext v2)"
using chop left_leq_right real_int.rchop_def view.hchop_def by auto
then show ?thesis
using chop len1_def len_def_v min_less_v1 real_int.rchop_def view.hchop_def
by auto
qed
thus "∥len v ts c∥ = ∥len v1 ts c∥ + ∥len v2 ts c∥"
using len_v2_0 by (simp)
next
assume r_inside_v2:"¬ right (len v ( ts) c) < right (ext v1)"
show "∥len v (