Theory Traffic
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) = ∅)"
by (simp add: cl_def nat_int.inter_empty1)
have re_geq_one:"∀c. |re c| ≥ 1"
by (simp add: Abs_nat_int_inverse re_def)
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})"
by (simp add: Abs_nat_int_inverse re_def)
have clNextRe :
"∀c. ((cl c) ≠ ∅ ⟶ (∃ n. Rep_nat_int (re c) ∪ Rep_nat_int (cl c) = {n, n+1}))"
by (simp add: cl_def)
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) ≠ ∅"
by (simp add: card_non_empty_geq_one)
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
one_add_one order_refl)
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}"
using adj by blast
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 "
by (metis Int_insert_right_if0 One_nat_def Suc_leI add.right_neutral add_Suc_right
atMostTwoRes el.rep_eq inf_bot_right inf_sup_absorb insert_not_empty le_antisym
n_def one_add_one order.not_eq_order_implies_strict singleton traffic.atLeastOneRes
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"
by (simp add: ts'_def)
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
atMostTwoLanes atMostTwoRes nat_int.card_un_add clm_consec_res fun_upd_apply
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"
by (metis (no_types, lifting) Suc_1 add_Suc add_diff_cancel_left'
add_mono_thms_linordered_semiring(1) card_non_empty_geq_one cl_leq_one
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