Theory HMLSL
section‹Basic HMLSL›
text‹
In this section, we define the basic formulas of HMLSL.
All of these basic formulas and theorems are independent
of the choice of sensor function. However, they show how
the general operators (chop, changes in perspective,
atomic formulas) work.
›
theory HMLSL
imports "Restriction" "Move" Length
begin
subsection‹Syntax of Basic HMLSL›
text ‹
Formulas are functions associating a traffic snapshot
and a view with a Boolean value.
›
type_synonym σ = " traffic ⇒ view ⇒ bool"
locale hmlsl = restriction+
fixes sensors::"cars ⇒ traffic ⇒ cars ⇒ real"
assumes sensors_ge:"(sensors e ts c) > 0" begin
end
sublocale hmlsl<sensors
by (simp add: sensors.intro sensors_ge)
context hmlsl
begin
text‹
All formulas are defined as abbreviations. As a consequence,
proofs will directly refer to the semantics of HMLSL, i.e.,
traffic snapshots and views.
›
text‹
The first-order operators are direct translations into HOL operators.
›
abbreviation mtrue :: "σ" ("❙⊤")
where "❙⊤ ≡ λ ts w. True"
abbreviation mfalse :: "σ" ("❙⊥")
where "❙⊥ ≡ λ ts w. False"
abbreviation mnot :: "σ⇒σ" ("❙¬_"[52]53)
where "❙¬φ ≡ λ ts w. ¬φ(ts)(w)"
abbreviation mnegpred :: "(cars⇒σ)⇒(cars⇒σ)" ("⇧¬_"[52]53)
where "⇧¬Φ ≡ λx.λ ts w. ¬Φ(x)(ts)(w)"
abbreviation mand :: "σ⇒σ⇒σ" (infixr"❙∧"51)
where "φ❙∧ψ ≡ λ ts w. φ(ts)(w)∧ψ(ts)(w)"
abbreviation mor :: "σ⇒σ⇒σ" (infix "❙∨"50 )
where "φ❙∨ψ ≡ λ ts w. φ(ts)(w)∨ψ(ts)(w)"
abbreviation mimp :: "σ⇒σ⇒σ" (infixr"❙→"49)
where "φ❙→ψ ≡ λ ts w. φ(ts)(w)⟶ψ(ts)(w)"
abbreviation mequ :: "σ⇒σ⇒σ" (infixr"❙↔"48)
where "φ❙↔ψ ≡ λ ts w. φ(ts)(w)⟷ψ(ts)(w)"
abbreviation mforall :: "('a⇒σ)⇒σ" ("❙∀")
where "❙∀Φ ≡ λ ts w.∀x. Φ(x)(ts)(w)"
abbreviation mforallB :: "('a⇒σ)⇒σ" (binder"❙∀"[8]9)
where "❙∀x. φ(x) ≡ ❙∀φ"
abbreviation mexists :: "('a⇒σ)⇒σ" ("❙∃")
where "❙∃Φ ≡ λ ts w.∃x. Φ(x)(ts)(w)"
abbreviation mexistsB :: "(('a)⇒σ)⇒σ" (binder"❙∃"[8]9)
where "❙∃x. φ(x) ≡ ❙∃φ"
abbreviation meq :: "'a⇒'a⇒σ" (infixr"❙="60)
where "x❙=y ≡ λ ts w. x = y"
abbreviation mgeq :: "('a::ord) ⇒ 'a ⇒ σ" (infix "❙≥" 60)
where "x ❙≥ y ≡ λ ts w. x ≥ y"
abbreviation mge ::"('a::ord) ⇒ 'a ⇒ σ" (infix "❙>" 60)
where "x ❙> y ≡ λ ts w. x > y"
text‹
For the spatial modalities, we use the chopping operations
defined on views. Observe that our chop modalities are existential.
›
abbreviation hchop :: "σ⇒σ⇒σ" (infixr "❙⌢" 53)
where "φ ❙⌢ ψ ≡ λ ts w.∃v u. (w=v∥u) ∧ φ(ts)(v)∧ψ(ts)(u)"
abbreviation vchop :: "σ⇒σ⇒σ" (infixr "❙⌣" 53)
where "φ ❙⌣ ψ ≡ λ ts w.∃v u. (w=v--u) ∧ φ(ts)(v) ∧ ψ(ts)(u)"
abbreviation somewhere ::"σ⇒σ" ( "❙⟨_❙⟩ " 55)
where "❙⟨φ❙⟩ ≡ ❙⊤ ❙⌢ (❙⊤❙⌣φ ❙⌣❙⊤)❙⌢❙⊤"
abbreviation everywhere::"σ⇒σ" ("❙[_❙]" 55)
where "❙[φ❙] ≡ ❙¬❙⟨❙¬φ❙⟩"
text‹
To change the perspective of a view, we use
an operator in the fashion of Hybrid Logic.
›
abbreviation at :: "cars ⇒ σ ⇒ σ " ("❙@ _ _" 56)
where "❙@c φ ≡ λts w . ∀v'. (w=c>v') ⟶ φ(ts)(v')"
text‹
The behavioural modalities are defined as usual modal
box-like modalities, where the accessibility relations
are given by the different types of transitions between
traffic snapshots.
›
abbreviation res_box::"cars ⇒ σ ⇒ σ" ("❙□r'(_') _" 55)
where "❙□r(c) φ ≡ λ ts w. ∀ts'. (ts❙─r(c)❙→ts') ⟶ φ(ts')(w)"
abbreviation clm_box::"cars ⇒ σ ⇒ σ" ("❙□c'(_') _" 55)
where "❙□c(c) φ ≡ λ ts w. ∀ts' n. (ts❙─c(c,n)❙→ts') ⟶ φ(ts')(w)"
abbreviation wdres_box::"cars ⇒ σ ⇒ σ" ("❙□wdr'(_') _" 55)
where "❙□wdr(c) φ ≡ λ ts w. ∀ts' n. (ts❙─wdr(c,n)❙→ts') ⟶ φ(ts')(w)"
abbreviation wdclm_box::"cars ⇒ σ ⇒ σ" ("❙□wdc'(_') _" 55)
where "❙□wdc(c) φ ≡ λ ts w. ∀ts'. (ts❙─wdc(c)❙→ts') ⟶ φ(ts')(w)"
abbreviation time_box::"σ ⇒ σ" ("❙□❙τ _" 55)
where "❙□❙τ φ ≡ λts w. ∀ts'. (ts❙↝ts') ⟶ φ(ts')(move ts ts' w)"
abbreviation globally::"σ ⇒ σ" ("❙G _" 55)
where "❙G φ ≡ λts w. ∀ts'. (ts ❙⇒ ts') ⟶ φ(ts')(move ts ts' w)"
text‹
The spatial atoms to refer to reservations, claims
and free space are direct translations of the original
definitions of MLSL \<^cite>‹"Hilscher2011"› into the Isabelle implementation.
›
abbreviation re:: "cars ⇒ σ" ("re'(_')" 70)
where
"re(c) ≡ λ ts v. ∥ext v∥> 0 ∧ len v ts c = ext v ∧
restrict v (res ts) c = lan v ∧ |lan v|=1"
abbreviation cl:: "cars ⇒ σ" ("cl'(_')" 70)
where
"cl(c) ≡ λ ts v. ∥ext v∥> 0 ∧ len v ts c = ext v ∧
restrict v (clm ts) c = lan v ∧ |lan v| = 1"
abbreviation free:: "σ" ("free")
where
"free ≡ λ ts v. ∥ext v∥ > 0 ∧ |lan v| = 1 ∧
(∀c. ∥len v ts c∥ = 0 ∨
(restrict v (clm ts) c = ∅ ∧ restrict v (res ts) c = ∅))"
text‹
Even though we do not need them for the subsequent proofs of safety,
we define ways to measure the number of lanes (width) and the
size of the extension (length) of a view. This allows us
to connect the atomic formulas for reservations and claims
with the atom denoting free space \<^cite>‹"Linker2015a"›.
›
abbreviation width_eq::"nat ⇒ σ" ("❙ω = _ " 60)
where "❙ω = n ≡ λ ts v. |lan v| = n"
abbreviation width_geq::"nat ⇒ σ" ("❙ω ≥ _" 60)
where "❙ω ≥ n ≡ λ ts v. |lan v| ≥ n"
abbreviation width_ge::"nat ⇒ σ" ("❙ω > _" 60)
where "❙ω > n ≡ (❙ω = n+1) ❙⌣ ❙⊤"
abbreviation length_eq::"real ⇒ σ" ("❙𝗅 = _ " 60)
where "❙𝗅 = r ≡ λ ts v. ∥ext v∥ = r"
abbreviation length_ge:: "real ⇒ σ" ("❙𝗅 > _" 60)
where "❙𝗅 > r ≡ λ ts v. ∥ext v∥ > r"
abbreviation length_geq::"real ⇒ σ" ("❙𝗅 ≥ _" 60)
where "❙𝗅 ≥ r ≡ (❙𝗅 = r) ❙∨ (❙𝗅 > r)"
text‹
For convenience, we use abbreviations for
the validity and satisfiability of formulas. While
the former gives a nice way to express theorems,
the latter is useful within proofs.
›
abbreviation valid :: "σ ⇒ bool" ("⊨ _" 10 )
where "⊨ φ ≡ ∀ts. ∀v. φ(ts)(v)"
abbreviation satisfies::" traffic ⇒ view ⇒ σ ⇒ bool" ("_ , _ ⊨ _" 10)
where "ts,v ⊨ φ ≡ φ(ts)(v)"
subsection ‹Theorems about Basic HMLSL›
lemma hchop_weaken1: " ⊨ φ ❙→ (φ ❙⌢ ❙⊤) "
using horizontal_chop_empty_right by fastforce
lemma hchop_weaken2: " ⊨ φ ❙→ (❙⊤ ❙⌢ φ) "
using horizontal_chop_empty_left by fastforce
lemma hchop_weaken: " ⊨ φ ❙→ (❙⊤ ❙⌢ φ ❙⌢ ❙⊤)"
using hchop_weaken1 hchop_weaken2 by metis
lemma hchop_neg1:"⊨ ❙¬ (φ ❙⌢ ❙⊤) ❙→ ((❙¬ φ) ❙⌢ ❙⊤)"
using horizontal_chop1 by fastforce
lemma hchop_neg2:"⊨ ❙¬ (❙⊤❙⌢φ ) ❙→ (❙⊤ ❙⌢ ❙¬ φ)"
using horizontal_chop1 by fastforce
lemma hchop_disj_distr1:"⊨ ((φ ❙⌢ (ψ ❙∨ χ)) ❙↔ ((φ ❙⌢ ψ)❙∨(φ ❙⌢ χ)))"
by blast
lemma hchop_disj_distr2:"⊨ (((ψ ❙∨ χ)❙⌢φ) ❙↔ ((ψ ❙⌢ φ)❙∨(χ ❙⌢ φ)))"
by blast
lemma hchop_assoc:"⊨φ ❙⌢ (ψ ❙⌢ χ) ❙↔ (φ ❙⌢ ψ) ❙⌢ χ"
using horizontal_chop_assoc1 horizontal_chop_assoc2 by fastforce
lemma v_chop_weaken1:"⊨ (φ ❙→ (φ ❙⌣ ❙⊤))"
using vertical_chop_empty_down by fastforce
lemma v_chop_weaken2:"⊨ (φ ❙→ (❙⊤ ❙⌣ φ))"
using vertical_chop_empty_up by fastforce
lemma v_chop_assoc:"⊨(φ ❙⌣ (ψ ❙⌣ χ)) ❙↔ ((φ ❙⌣ ψ) ❙⌣ χ)"
using vertical_chop_assoc1 vertical_chop_assoc2 by fastforce
lemma vchop_disj_distr1:"⊨ ((φ ❙⌣ (ψ ❙∨ χ)) ❙↔ ((φ ❙⌣ ψ)❙∨(φ ❙⌣ χ)))"
by blast
lemma vchop_disj_distr2:"⊨ (((ψ ❙∨ χ) ❙⌣ φ ) ❙↔ ((ψ ❙⌣ φ)❙∨(χ ❙⌣ φ)))"
by blast
lemma at_exists :"⊨ φ ❙→ (❙∃ c. ❙@c φ)"
proof (rule allI|rule impI)+
fix ts v
assume assm:"ts,v ⊨φ"
obtain d where d_def:"d=own v" by blast
then have "ts,v ⊨ ❙@d φ" using assm switch_refl switch_unique by fastforce
thus "ts,v ⊨ (❙∃ c. ❙@c φ)" ..
qed
lemma at_conj_distr:"⊨(❙@c ( φ ❙∧ ψ)) ❙↔ ((❙@c φ) ❙∧ (❙@c ψ))"
using switch_unique by blast
lemma at_disj_dist:"⊨(❙@c (φ ❙∨ ψ)) ❙↔ ((❙@c φ ) ❙∨ ( ❙@c ψ ))"
using switch_unique by fastforce
lemma at_hchop_dist1:"⊨(❙@c (φ ❙⌢ ψ)) ❙→ ((❙@c φ) ❙⌢ (❙@c ψ))"
proof (rule allI|rule impI)+
fix ts v
assume assm:"ts, v ⊨(❙@c (φ ❙⌢ ψ))"
obtain v' where v':"v=c>v'" using switch_always_exists by fastforce
with assm obtain v1' and v2'
where chop:"(v'=v1'∥v2') ∧ (ts,v1' ⊨ φ) ∧ (ts,v2'⊨ψ)"
by blast
from chop and v' obtain v1 and v2
where origin:"(v1=c>v1') ∧ (v2=c>v2') ∧ (v=v1∥v2)"
using switch_hchop2 by fastforce
hence v1:"ts,v1 ⊨ (❙@c φ)" and v2:"ts,v2 ⊨ (❙@c ψ)"
using switch_unique chop by fastforce+
from v1 and v2 and origin show "ts,v ⊨(❙@c φ) ❙⌢ (❙@c ψ)" by blast
qed
lemma at_hchop_dist2:"⊨( (❙@c φ) ❙⌢ (❙@c ψ)) ❙→ (❙@c (φ ❙⌢ ψ)) "
using switch_unique switch_hchop1 switch_def by metis
lemma at_hchop_dist:"⊨( (❙@c φ) ❙⌢ (❙@c ψ)) ❙↔ (❙@c (φ ❙⌢ ψ)) "
using at_hchop_dist1 at_hchop_dist2 by blast
lemma at_vchop_dist1:"⊨(❙@c (φ ❙⌣ ψ)) ❙→ ( (❙@c φ) ❙⌣ (❙@c ψ))"
proof (rule allI|rule impI)+
fix ts v
assume assm:"ts, v ⊨(❙@c (φ ❙⌣ ψ))"
obtain v' where v':"v=c>v'" using switch_always_exists by fastforce
with assm obtain v1' and v2'
where chop:"(v'=v1'--v2') ∧ (ts,v1' ⊨ φ) ∧ (ts,v2'⊨ψ)"
by blast
from chop and v' obtain v1 and v2
where origin:"(v1=c>v1') ∧ (v2=c>v2') ∧ (v=v1--v2)"
using switch_vchop2 by fastforce
hence v1:"ts,v1 ⊨ (❙@c φ)" and v2:"ts,v2 ⊨ (❙@c ψ)"
using switch_unique chop by fastforce+
from v1 and v2 and origin show "ts,v ⊨ (❙@c φ) ❙⌣ (❙@c ψ)" by blast
qed
lemma at_vchop_dist2:"⊨( (❙@c φ) ❙⌣ (❙@c ψ)) ❙→ (❙@c (φ ❙⌣ ψ)) "
using switch_unique switch_vchop1 switch_def by metis
lemma at_vchop_dist:"⊨( (❙@c φ) ❙⌣ (❙@c ψ)) ❙↔ (❙@c (φ ❙⌣ ψ)) "
using at_vchop_dist1 at_vchop_dist2 by blast
lemma at_eq:"⊨(❙@e c ❙= d) ❙↔ (c ❙= d)"
using switch_always_exists by (metis )
lemma at_neg1:"⊨(❙@c ❙¬ φ) ❙→ ❙¬ (❙@c φ)"
using switch_unique
by (metis select_convs switch_def)
lemma at_neg2:"⊨❙¬ (❙@c φ ) ❙→ ( (❙@c ❙¬ φ))"
using switch_unique by fastforce
lemma at_neg :"⊨(❙@c( ❙¬ φ)) ❙↔ ❙¬ (❙@c φ)"
using at_neg1 at_neg2 by metis
lemma at_neg':"ts,v ⊨ ❙¬ (❙@c φ) ❙↔ (❙@c( ❙¬ φ))" using at_neg by simp
lemma at_neg_neg1:"⊨(❙@c φ) ❙→ ❙¬(❙@c ❙¬ φ)"
using switch_unique switch_def switch_refl
by (metis select_convs switch_def)
lemma at_neg_neg2:"⊨❙¬(❙@c ❙¬ φ) ❙→ (❙@c φ)"
using switch_unique switch_def switch_refl
by metis
lemma at_neg_neg:"⊨ (❙@c φ) ❙↔ ❙¬(❙@c ❙¬ φ)"
using at_neg_neg1 at_neg_neg2 by metis
lemma globally_all_iff:"⊨ (❙G(❙∀c. φ)) ❙↔ (❙∀c.( ❙G φ))" by simp
lemma globally_all_iff':"ts,v⊨ (❙G(❙∀c. φ)) ❙↔ (❙∀c.( ❙G φ))" by simp
lemma globally_refl:" ⊨(❙G φ) ❙→ φ"
using traffic.abstract.refl traffic.move_nothing by fastforce
lemma globally_4: "⊨ (❙G φ) ❙→ ❙G ❙G φ"
proof (rule allI|rule impI)+
fix ts v ts' ts''
assume 1:"ts ❙⇒ ts'" and 2:"ts' ❙⇒ ts''" and 3:"ts,v ⊨ ❙G φ"
from 2 and 1 have "ts ❙⇒ ts''" using traffic.abs_trans by blast
moreover from 1 and 2 have "move ts' ts'' (move ts ts' v) = move ts ts'' v"
using traffic.move_trans by blast
with 3 show "ts'', move ts' ts'' (move ts ts' v) ⊨φ" using calculation by simp
qed
lemma spatial_weaken: "⊨ (φ ❙→ ❙⟨φ❙⟩)"
using horizontal_chop_empty_left horizontal_chop_empty_right vertical_chop_empty_down
vertical_chop_empty_up
by fastforce
lemma spatial_weaken2:"⊨ (φ ❙→ ψ) ❙→ (φ ❙→ ❙⟨ψ❙⟩)"
using spatial_weaken horizontal_chop_empty_left horizontal_chop_empty_right
vertical_chop_empty_down vertical_chop_empty_up
by blast
lemma somewhere_distr: "⊨ ❙⟨φ❙∨ψ❙⟩ ❙↔ ❙⟨φ❙⟩ ❙∨ ❙⟨ψ❙⟩"
by blast
lemma somewhere_and:"⊨ ❙⟨φ ❙∧ ψ❙⟩ ❙→ ❙⟨φ❙⟩ ❙∧ ❙⟨ψ❙⟩"
by blast
lemma somewhere_and_or_distr :"⊨(❙⟨ χ ❙∧ (φ ❙∨ ψ) ❙⟩ ❙↔ ❙⟨ χ ❙∧ φ ❙⟩ ❙∨ ❙⟨ χ ❙∧ ψ ❙⟩)"
by blast
lemma width_add1:"⊨((❙ω = x) ❙⌣ (❙ω = y) ❙→ ❙ω = x+y)"
using vertical_chop_add1 by fastforce
lemma width_add2:"⊨((❙ω = x+y) ❙→ (❙ω = x) ❙⌣ ❙ω = y)"
using vertical_chop_add2 by fastforce
lemma width_hchop_stable: "⊨((❙ω = x) ❙↔ ((❙ω = x) ❙⌢ (❙ω=x)))"
using hchop_def horizontal_chop1
by force
lemma length_geq_zero:"⊨ (❙𝗅 ≥ 0)"
by (metis order.not_eq_order_implies_strict real_int.length_ge_zero)
lemma length_split: "⊨((❙𝗅 > 0) ❙→ (❙𝗅 > 0) ❙⌢ (❙𝗅 > 0))"
using horizontal_chop_non_empty by fastforce
lemma length_meld: "⊨((❙𝗅 > 0) ❙⌢ (❙𝗅 > 0) ❙→ (❙𝗅 > 0))"
using hchop_def real_int.chop_add_length_ge_0
by (metis (no_types, lifting))
lemma length_dense:"⊨((❙𝗅 > 0) ❙↔ (❙𝗅 > 0) ❙⌢ (❙𝗅 > 0))"
using length_meld length_split by blast
lemma length_add1:"⊨((❙𝗅=x) ❙⌢ (❙𝗅= y)) ❙→ (❙𝗅= x+y)"
using hchop_def real_int.rchop_def real_int.length_def by fastforce
lemma length_add2:"⊨ (x ❙≥ 0 ❙∧ y ❙≥ 0) ❙→ ( (❙𝗅=x+y) ❙→ ((❙𝗅=x) ❙⌢ (❙𝗅=y)))"
using horizontal_chop_split_add by fastforce
lemma length_add:"⊨ (x ❙≥ 0 ❙∧ y ❙≥ 0) ❙→ ( (❙𝗅=x+y) ❙↔ ((❙𝗅=x) ❙⌢ (❙𝗅=y)))"
using length_add1 length_add2 by blast
lemma length_vchop_stable:"⊨(❙𝗅 = x) ❙↔ ((❙𝗅 = x) ❙⌣ ( ❙𝗅 = x))"
using vchop_def vertical_chop1 by fastforce
lemma res_ge_zero:"⊨(re(c) ❙→ ❙𝗅>0)"
by blast
lemma clm_ge_zero:"⊨(cl(c) ❙→ ❙𝗅>0)"
by blast
lemma free_ge_zero:"⊨free ❙→ ❙𝗅>0"
by blast
lemma width_res:"⊨(re(c) ❙→ ❙ω = 1)"
by auto
lemma width_clm:"⊨(cl(c) ❙→ ❙ω = 1)"
by simp
lemma width_free:"⊨(free ❙→ ❙ω = 1)"
by simp
lemma width_somewhere_res:"⊨ ❙⟨re(c)❙⟩ ❙→ (❙ω ≥ 1)"
proof (rule allI|rule impI)+
fix ts v
assume "ts,v ⊨ ❙⟨re(c)❙⟩"
then show "ts,v ⊨ (❙ω ≥ 1)"
using view.hchop_def view.vertical_chop_width_mon by fastforce
qed
lemma clm_disj_res:"⊨ ❙¬ ❙⟨ cl(c) ❙∧ re(c) ❙⟩"
proof (rule allI|rule notI)+
fix ts v
assume "ts,v ⊨❙⟨cl(c) ❙∧ re(c)❙⟩"
then obtain v' where "v' ≤ v ∧ (ts,v' ⊨ cl(c) ❙∧ re(c))"
by (meson view.somewhere_leq)
then show False using disjoint
by (metis card_non_empty_geq_one inf.idem restriction.restriction_clm_leq_one
restriction.restriction_clm_res_disjoint)
qed
lemma width_ge:"⊨ (❙ω> 0) ❙→ (❙∃ x. (❙ω = x) ❙∧ (x ❙> 0))"
using vertical_chop_add1 add_gr_0 zero_less_one by auto
lemma two_res_width: "⊨((re(c) ❙⌣ re(c)) ❙→ ❙ω = 2)"
by (metis one_add_one width_add1)
lemma res_at_most_two:"⊨❙¬ (re(c) ❙⌣ re(c) ❙⌣ re(c) )"
proof(rule allI| rule notI )+
fix ts v
assume "ts, v ⊨ (re(c) ❙⌣ re(c) ❙⌣ re(c) )"
then obtain v' and v1 and v2 and v3
where "v = v1--v'" and "v'=v2--v3"
and "ts,v1 ⊨re(c)" and "ts,v2 ⊨re(c)" and "ts,v3 ⊨re(c)"
by blast
then show False
proof -
have "|restrict v' (res ts) c| < |restrict v (res ts) c|"
using ‹ts,v1 ⊨re(c)› ‹v=v1--v'› restriction.restriction_add_res by auto
then show ?thesis
by (metis (no_types) ‹ts,v2 ⊨ re(c)› ‹ts,v3 ⊨re(c)› ‹v'=v2--v3› not_less
one_add_one restriction_add_res restriction_res_leq_two)
qed
qed
lemma res_at_most_two2:"⊨❙¬ ❙⟨re(c) ❙⌣ re(c) ❙⌣ re(c)❙⟩"
using res_at_most_two by blast
lemma res_at_most_somewhere:"⊨❙¬ ❙⟨re(c)❙⟩ ❙⌣ ❙⟨re(c)❙⟩ ❙⌣ ❙⟨re(c)❙⟩ "
proof (rule allI|rule notI)+
fix ts v
assume assm:"ts,v ⊨ (❙⟨re(c)❙⟩ ❙⌣ ❙⟨re(c)❙⟩ ❙⌣ ❙⟨re(c)❙⟩ )"
obtain vu and v1 and vm and vd
where chops:"(v=vu--v1) ∧ (v1 = vm--vd)∧ (ts,vu ⊨❙⟨re(c)❙⟩)
∧ (ts,vm ⊨ ❙⟨re(c)❙⟩ ) ∧( ts,vd ⊨ ❙⟨ re(c)❙⟩)"
using assm by blast
from chops have res_vu:"|restrict vu (res ts) c| ≥ 1"
by (metis restriction_card_somewhere_mon)
from chops have res_vm:"|restrict vm (res ts) c| ≥ 1"
by (metis restriction_card_somewhere_mon)
from chops have res_vd:"|restrict vd (res ts) c| ≥ 1"
by (metis restriction_card_somewhere_mon)
from chops have
"|restrict v (res ts) c | =
|restrict vu (res ts) c|+ |restrict vm (res ts) c| + |restrict vd (res ts) c| "
using restriction_add_res by force
with res_vu and res_vd res_vm have "|restrict v (res ts) c | ≥ 3"
by linarith
with restriction_res_leq_two show False
by (metis not_less_eq_eq numeral_2_eq_2 numeral_3_eq_3)
qed
lemma res_adj:"⊨❙¬ (re(c) ❙⌣ (❙ω > 0) ❙⌣ re(c)) "
proof (rule allI|rule notI)+
fix ts v
assume "ts,v ⊨ (re(c) ❙⌣ (❙ω > 0) ❙⌣ re(c)) "
then obtain v1 and v' and v2 and vn
where chop:"(v=v1--v') ∧ (v'=vn--v2) ∧ (ts,v1⊨re(c))
∧ (ts,vn ⊨ ❙ω > 0) ∧ (ts,v2⊨re(c))"
by blast
hence res1:"|restrict v1 (res ts) c| ≥ 1" by (simp add: le_numeral_extra(4))
from chop have res2: "|restrict v2 (res ts) c| ≥ 1" by (simp add: le_numeral_extra(4))
from res1 and res2 have "|restrict v (res ts) c| ≥ 2"
using chop restriction.restriction_add_res by auto
then have resv:"|restrict v (res ts) c| = 2"
using dual_order.antisym restriction.restriction_res_leq_two by blast
hence res_two_lanes:"|res ts c| =2" using atMostTwoRes restrict_res
by (metis (no_types, lifting) nat_int.card_subset_le dual_order.antisym)
from this obtain p where p_def:"Rep_nat_int (res ts c) = {p, p+1}"
using consecutiveRes by force
have "Abs_nat_int {p,p+1} ⊑ lan v"
by (metis Rep_nat_int_inverse atMostTwoRes card_seteq finite_atLeastAtMost
insert_not_empty nat_int.card'.rep_eq nat_int.card_seq less_eq_nat_int.rep_eq
p_def resv restrict_res restrict_view)
have vn_not_e:"lan vn ≠ ∅" using chop
by (metis nat_int.card_empty_zero less_irrefl width_ge)
hence consec_vn_v2:"nat_int.consec (lan vn) (lan v2)"
using nat_int.card_empty_zero chop nat_int.nchop_def one_neq_zero vchop_def
by auto
have v'_not_e:"lan v' ≠ ∅" using chop
by (metis less_irrefl nat_int.card_empty_zero view.vertical_chop_assoc2 width_ge)
hence consec_v1_v':"nat_int.consec (lan v1) (lan v')"
by (metis (no_types, lifting) nat_int.card_empty_zero chop nat_int.nchop_def
one_neq_zero vchop_def)
hence consec_v1_vn:"nat_int.consec (lan v1) (lan vn)"
by (metis (no_types, lifting) chop consec_vn_v2 nat_int.consec_def
nat_int.chop_min vchop_def)
hence lesser_con:"∀n m. (n ❙∈ (lan v1) ∧ m ❙∈ (lan v2) ⟶ n < m)"
using consec_v1_vn consec_vn_v2 nat_int.consec_trans_lesser
by auto
have p_in_v1:"p ❙∈ lan v1"
proof (rule ccontr)
assume "¬ p ❙∈ lan v1"
then have "p ❙∉ lan v1" by (simp )
hence "p ❙∉ restrict v1 (res ts) c" using chop by (simp add: chop )
then have "p+1 ❙∈ restrict v1 (res ts) c"
proof -
have "{p, p + 1} ∩ (Rep_nat_int (res ts c) ∩ Rep_nat_int (lan v1)) ≠ {}"
by (metis chop Rep_nat_int_inject bot_nat_int.rep_eq consec_v1_v'
inf_nat_int.rep_eq nat_int.consec_def p_def restriction.restrict_def)
then have "p + 1 ∈ Rep_nat_int (lan v1)"
using ‹p ❙∉ restrict v1 (res ts) c› inf_nat_int.rep_eq not_in.rep_eq
restriction.restrict_def by force
then show ?thesis
using chop el.rep_eq by presburger
qed
hence suc_p:"p+1 ❙∈ lan v1" using chop by (simp add: chop)
hence "p+1 ❙∉ lan v2" using p_def restrict_def using lesser_con nat_int.el.rep_eq
nat_int.not_in.rep_eq by auto
then have "p ❙∈ restrict v2 (res ts) c"
proof -
have f1: "minimum (lan v2) ∈ Rep_nat_int (lan v2)"
using consec_vn_v2 el.rep_eq minimum_in nat_int.consec_def by simp
have "lan v2 ⊑ res ts c"
by (metis (no_types) chop restriction.restrict_res)
then have "minimum (lan v2) = p"
using ‹p + 1 ❙∉ lan v2› f1 less_eq_nat_int.rep_eq not_in.rep_eq p_def by auto
then show ?thesis
using f1 by (metis chop el.rep_eq)
qed
hence p:"p ❙∈ lan v2" using p_def restrict_def
using chop by auto
show False using lesser_con suc_p p by blast
qed
hence p_not_in_v2:"p ❙∉ lan v2" using p_def restrict_def lesser_con
nat_int.el.rep_eq nat_int.not_in.rep_eq
by auto
then have "p+1 ❙∈ restrict v2 (res ts) c"
proof -
have f1: "minimum (lan v2) ❙∈ lan v2"
using consec_vn_v2 minimum_in nat_int.consec_def by simp
obtain x where mini:"x = minimum (lan v2)" by blast
have "x = p + 1"
by (metis IntD1 p_not_in_v2 chop el.rep_eq f1 inf_nat_int.rep_eq insertE mini
not_in.rep_eq p_def restriction.restrict_def singletonD)
then show ?thesis
using chop f1 mini by auto
qed
hence suc_p_in_v2:"p+1 ❙∈ lan v2" using p_def restrict_def using chop by auto
have "∀n m. (n ❙∈ (lan v1) ∧ m ❙∈ (lan vn) ⟶ n < m)"
using consec_v1_vn nat_int.consec_lesser by auto
with p_in_v1 have ge_p:"∀m. (m ❙∈ lan vn ⟶ p < m)"
by blast
have "∀n m. (n ❙∈ (lan vn) ∧ m ❙∈ (lan v2) ⟶ n < m)"
using consec_vn_v2 nat_int.consec_lesser by auto
with suc_p_in_v2 have less_suc_p:"∀m. (m ❙∈ lan vn ⟶ m< p+1)"
by blast
have "∀m. (m ❙∈ lan vn ⟶ (m< p+1 ∧ m > p) )"
using ge_p less_suc_p by auto
hence "¬(∃m. (m ❙∈ lan vn))"
by (metis One_nat_def Suc_leI add.right_neutral add_Suc_right linorder_not_less)
hence "lan vn = ∅" using nat_int.non_empty_elem_in by auto
with vn_not_e show False by blast
qed
lemma clm_sing:"⊨❙¬ (cl(c) ❙⌣ cl(c)) "
using atMostOneClm restriction_add_clm vchop_def restriction_clm_leq_one
by (metis (no_types, opaque_lifting) add_eq_self_zero le_add1 le_antisym one_neq_zero)
lemma clm_sing_somewhere:"⊨❙¬ ❙⟨cl(c) ❙⌣ cl(c)❙⟩ "
using clm_sing by blast
lemma clm_sing_not_interrupted:"⊨ ❙¬(cl(c) ❙⌣ ❙⊤ ❙⌣ cl(c))"
using atMostOneClm restriction_add_clm vchop_def restriction_clm_leq_one clm_sing
by (metis (no_types, opaque_lifting) add.commute add_eq_self_zero dual_order.antisym
le_add1 one_neq_zero)
lemma clm_sing_somewhere2:"⊨❙¬ (❙⊤ ❙⌣ cl(c) ❙⌣ ❙⊤ ❙⌣ cl(c) ❙⌣ ❙⊤) "
using clm_sing_not_interrupted vertical_chop_assoc1
by meson
lemma clm_sing_somewhere3:"⊨❙¬ ❙⟨(❙⊤ ❙⌣ cl(c) ❙⌣ ❙⊤ ❙⌣ cl(c) ❙⌣ ❙⊤)❙⟩ "
by (meson clm_sing_not_interrupted view.vertical_chop_assoc1)
lemma clm_at_most_somewhere:"⊨❙¬ (❙⟨cl(c)❙⟩ ❙⌣ ❙⟨cl(c)❙⟩)"
proof (rule allI| rule notI)+
fix ts v
assume assm:"ts,v ⊨ (❙⟨cl(c)❙⟩ ❙⌣ ❙⟨cl(c)❙⟩)"
obtain vu and vd
where chops:"(v=vu--vd)∧ (ts,vu ⊨❙⟨cl(c)❙⟩) ∧ ( ts,vd ⊨ ❙⟨ cl(c)❙⟩)"
using assm by blast
from chops have clm_vu:"|restrict vu (clm ts) c| ≥ 1"
by (metis restriction_card_somewhere_mon)
from chops have clm_vd:"|restrict vd (clm ts) c| ≥ 1"
by (metis restriction_card_somewhere_mon)
from chops have clm_add:
"|restrict v (clm ts) c | = |restrict vu (clm ts) c| + |restrict vd (clm ts) c|"
using restriction_add_clm by auto
with clm_vu and clm_vd have "|restrict v (clm ts) c | ≥ 2"
using add.commute add_eq_self_zero dual_order.antisym le_add1 less_one not_le
restriction_res_leq_two
by linarith
with restriction_clm_leq_one show False
by (metis One_nat_def not_less_eq_eq numeral_2_eq_2)
qed
lemma res_decompose: "⊨(re(c) ❙→ re(c) ❙⌢ re(c))"
proof (rule allI| rule impI)+
fix ts v
assume assm:"ts,v ⊨re(c)"
then obtain v1 and v2
where 1:"v=v1∥v2" and 2:"∥ext v1∥ > 0" and 3:"∥ext v2∥ > 0"
using view.horizontal_chop_non_empty by blast
then have 4:"|lan v1| = 1" and 5:"|lan v2| = 1"
using assm view.hchop_def by auto
then have 6:"ts,v1 ⊨re(c)"
by (metis 2 1 assm len_view_hchop_left restriction.restrict_eq_lan_subs
restriction.restrict_view restriction.restriction_stable1)
from 5 have 7:"ts,v2 ⊨re(c)"
by (metis "1" "3" "6" assm len_view_hchop_right restriction.restrict_eq_lan_subs
restriction.restrict_view restriction.restriction_stable)
from 1 and 6 and 7 show "ts,v ⊨re(c) ❙⌢ re(c)" by blast
qed
lemma res_compose: "⊨(re(c) ❙⌢ re(c) ❙→ re(c))"
using real_int.chop_dense len_compose_hchop hchop_def length_dense restrict_def
by (metis (no_types, lifting))
lemma res_dense:"⊨re(c) ❙↔ re(c) ❙⌢ re(c)"
using res_decompose res_compose by blast
lemma res_continuous :"⊨(re(c)) ❙→ (❙¬ (❙⊤ ❙⌢ ( ❙¬re(c) ❙∧ ❙𝗅 > 0) ❙⌢ ❙⊤))"
by (metis (no_types, lifting) hchop_def len_view_hchop_left len_view_hchop_right
restrict_def)
lemma no_clm_before_res:"⊨❙¬(cl(c) ❙⌢ re(c))"
by (metis (no_types, lifting) nat_int.card_empty_zero nat_int.card_subset_le
disjoint hchop_def inf_assoc inf_le1 not_one_le_zero restrict_def)
lemma no_clm_before_res2:"⊨❙¬ (cl(c) ❙⌢ ❙⊤ ❙⌢ re(c))"
proof (rule ccontr)
assume "¬ (⊨ ❙¬ (cl(c) ❙⌢ ❙⊤ ❙⌢ re(c)))"
then obtain ts and v where assm:"ts,v ⊨ (cl(c) ❙⌢ ❙⊤ ❙⌢ re(c))" by blast
then have clm_subs:"restrict v (clm ts) c = restrict v (res ts) c"
using restriction_stable
by (metis (no_types, lifting) hchop_def restrict_def)
have "restrict v (clm ts )c ≠ ∅"
using assm nat_int.card_non_empty_geq_one restriction_stable1
by auto
then have res_in_neq:"restrict v (clm ts) c ⊓ restrict v (res ts) c ≠∅"
using clm_subs inf_absorb1
by (simp )
then show False using restriction_clm_res_disjoint
by (metis inf_commute restriction.restriction_clm_res_disjoint)
qed
lemma clm_decompose: "⊨(cl(c) ❙→ cl(c) ❙⌢ cl(c))"
proof (rule allI|rule impI)+
fix ts v
assume assm: "ts,v ⊨ cl(c)"
have restr:"restrict v (clm ts) c = lan v" using assm by simp
have len_ge_zero:"∥len v ts c∥ > 0" using assm by simp
have len:"len v ts c = ext v" using assm by simp
obtain v1 v2 where chop:"(v=v1∥v2) ∧ ∥ext v1∥ > 0 ∧ ∥ext v2∥ > 0 "
using assm view.horizontal_chop_non_empty
using length_split by blast
from chop and len have len_v1:"len v1 ts c = ext v1"
using len_view_hchop_left by blast
from chop and len have len_v2:"len v2 ts c = ext v2"
using len_view_hchop_right by blast
from chop and restr have restr_v1:"restrict v1 (clm ts) c = lan v1"
by (metis (no_types, lifting) hchop_def restriction.restriction_stable1)
from chop and restr have restr_v2:"restrict v2 (clm ts) c = lan v2"
by (metis (no_types, lifting) hchop_def restriction.restriction_stable2)
from chop and len_v1 len_v2 restr_v1 restr_v2 show "ts,v ⊨cl(c) ❙⌢ cl(c)"
using hchop_def assm by force
qed
lemma clm_compose: "⊨(cl(c) ❙⌢ cl(c) ❙→ cl(c))"
using real_int.chop_dense len_compose_hchop hchop_def length_dense restrict_def
by (metis (no_types, lifting))
lemma clm_dense:"⊨cl(c) ❙↔ cl(c) ❙⌢ cl(c)"
using clm_decompose clm_compose by blast
lemma clm_continuous :"⊨(cl(c)) ❙→ (❙¬ (❙⊤ ❙⌢ ( ❙¬cl(c) ❙∧ ❙𝗅 > 0) ❙⌢ ❙⊤))"
by (metis (no_types, lifting) hchop_def len_view_hchop_left len_view_hchop_right
restrict_def)
lemma res_not_free: "⊨(❙∃ c. re(c) ❙→ ❙¬free)"
using nat_int.card_empty_zero one_neq_zero by auto
lemma clm_not_free: "⊨(❙∃ c. cl(c) ❙→ ❙¬free)"
using nat_int.card_empty_zero by auto
lemma free_no_res:"⊨(free ❙→ ❙¬(❙∃ c. re(c)))"
using nat_int.card_empty_zero one_neq_zero
by (metis less_irrefl)
lemma free_no_clm:"⊨(free ❙→ ❙¬(❙∃ c. cl(c)))"
using nat_int.card_empty_zero one_neq_zero by (metis less_irrefl)
lemma free_decompose:"⊨free ❙→ ( free ❙⌢ free)"
proof (rule allI|rule impI)+
fix ts v
assume assm:"ts,v ⊨free"
obtain v1 and v2
where non_empty_v1_v2:"(v=v1∥v2) ∧ ∥ext v1∥ > 0 ∧ ∥ext v2∥ > 0"
using assm length_dense by blast
have one_lane:"|lan v1| = 1 ∧ |lan v2| = 1"
using assm hchop_def non_empty_v1_v2
by auto
have nothing_on_v1:
" (∀c. ∥len v1 ts c∥ = 0
∨ (restrict v1 (clm ts) c = ∅ ∧ restrict v1 (res ts) c = ∅))"
by (metis (no_types, lifting) assm len_empty_on_subview1 non_empty_v1_v2
restriction_stable1)
have nothing_on_v2:
" (∀c. ∥len v2 ts c∥ = 0
∨ (restrict v2 (clm ts) c = ∅ ∧ restrict v2 (res ts) c = ∅))"
by (metis (no_types, lifting) assm len_empty_on_subview2 non_empty_v1_v2
restriction_stable2)
have
"(v=v1∥v2)
∧ 0 < ∥ext v1∥ ∧ |lan v1| = 1
∧ (∀c. ∥len v1 ts c∥ = 0
∨( restrict v1 (clm ts) c = ∅ ∧ restrict v1 (res ts) c = ∅))
∧ 0 < ∥ext v2∥ ∧ |lan v2| = 1
∧ (∀c. ∥len v2 ts c∥ = 0
∨( restrict v2 (clm ts) c = ∅ ∧ restrict v2 (res ts) c = ∅))"
using non_empty_v1_v2 nothing_on_v1 nothing_on_v2 one_lane by blast
then show "ts,v ⊨(free ❙⌢ free)" by blast
qed
lemma free_compose:"⊨(free ❙⌢ free) ❙→ free"
proof (rule allI|rule impI)+
fix ts v
assume assm:"ts,v ⊨free ❙⌢ free"
have len_ge_0:"∥ext v∥ > 0"
using assm length_meld by blast
have widt_one:"|lan v| = 1" using assm
by (metis horizontal_chop_width_stable)
have no_car:
"(∀c. ∥len v ts c∥ = 0 ∨ restrict v (clm ts) c = ∅ ∧ restrict v (res ts) c = ∅)"
proof (rule ccontr)
assume
"¬(∀c. ∥len v ts c∥ = 0
∨ (restrict v (clm ts) c = ∅ ∧ restrict v (res ts) c = ∅))"
then obtain c
where ex:
"∥len v ts c∥ ≠ 0 ∧ (restrict v (clm ts) c ≠ ∅ ∨ restrict v (res ts) c ≠ ∅)"
by blast
from ex have 1:"∥len v ts c∥ > 0"
using less_eq_real_def real_int.length_ge_zero by auto
have "(restrict v (clm ts) c ≠ ∅ ∨ restrict v (res ts) c ≠ ∅)" using ex ..
then show False
proof
assume "restrict v (clm ts) c ≠ ∅"
then show False
by (metis (no_types, opaque_lifting) assm add.left_neutral ex len_hchop_add
restriction.restrict_def view.hchop_def)
next
assume "restrict v (res ts) c ≠ ∅"
then show False
by (metis (no_types, opaque_lifting) assm add.left_neutral ex len_hchop_add
restriction.restrict_def view.hchop_def)
qed
qed
show "ts,v ⊨free"
using len_ge_0 widt_one no_car by blast
qed
lemma free_dense:"⊨free ❙↔ (free ❙⌢ free)"
using free_decompose free_compose by blast
lemma free_dense2:"⊨free ❙→ ❙⊤ ❙⌢ free ❙⌢ ❙⊤"
using horizontal_chop_empty_left horizontal_chop_empty_right by fastforce
text ‹
The next lemmas show the connection between the spatial. In particular,
if the view consists of one lane and a non-zero extension, where neither
a reservation nor a car resides, the view satisfies free (and vice versa).
›
lemma no_cars_means_free:
"⊨((❙𝗅>0) ❙∧ (❙ω = 1) ❙∧ (❙∀c. ❙¬ (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤))) ❙→ free"
proof (rule allI|rule impI)+
fix ts v
assume assm:
"ts,v ⊨ ((❙𝗅>0) ❙∧ (❙ω = 1) ❙∧ (❙∀c. ❙¬ (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤)))"
have ge_0:"ts,v ⊨ ❙𝗅 > 0" using assm by best
have one_lane:"ts,v ⊨❙ω = 1" using assm by best
show "ts,v ⊨ free"
proof (rule ccontr)
have no_car: "ts,v ⊨❙¬( ❙∃ c. (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤))"
using assm by best
assume "ts,v ⊨ ❙¬ free"
hence contra:
"¬(∀c. ∥len v ts c∥ = 0 ∨ restrict v (clm ts) c = ∅ ∧ restrict v (res ts) c = ∅)"
using ge_0 one_lane by blast
hence ex_car:
"∃c. ∥len v ts c∥ > 0 ∧ (restrict v (clm ts) c ≠ ∅ ∨ restrict v (res ts) c ≠ ∅)"
using real_int.length_ge_zero dual_order.antisym not_le
by metis
obtain c where c_def:
"∥len v ts c∥ > 0 ∧ (restrict v (clm ts) c ≠ ∅ ∨ restrict v (res ts) c ≠ ∅)"
using ex_car by blast
hence "(restrict v (clm ts) c ≠ ∅ ∨ restrict v (res ts) c ≠ ∅)" by best
thus False
proof
assume "restrict v (clm ts) c ≠ ∅"
with one_lane have clm_one:"|restrict v (clm ts) c| = 1"
using el_in_restriction_clm_singleton
by (metis card_non_empty_geq_one dual_order.antisym restriction.restriction_clm_leq_one)
obtain v1 and v2 and v3 and v4
where "v=v1∥v2" and "v2=v3∥v4"
and len_eq:"len v3 ts c = ext v3 ∧ ∥len v3 ts c∥ = ∥len v ts c∥ "
using horizontal_chop_empty_left horizontal_chop_empty_right
len_fills_subview c_def by blast
then have res_non_empty:"restrict v3 (clm ts) c ≠ ∅"
using ‹restrict v (clm ts) c ≠ ∅› restriction_stable restriction_stable1
by auto
have len_non_empty:"∥len v3 ts c∥ > 0"
using len_eq c_def by auto
have "|restrict v3 (clm ts) c| =1 "
using ‹v2=v3∥v4› ‹v=v1∥v2› clm_one restriction_stable restriction_stable1
by auto
have v3_one_lane:"|lan v3| = 1"
using ‹v2=v3∥v4› ‹v=v1∥v2› hchop_def one_lane
by auto
have clm_fills_v3:"restrict v3 (clm ts) c = lan v3"
proof (rule ccontr)
assume aux:"restrict v3 (clm ts) c ≠ lan v3"
have "restrict v3 (clm ts) c ⊑ lan v3"
by (simp add: restrict_view)
hence "∃n. n ❙∉ restrict v3 (clm ts) c ∧ n ❙∈ lan v3"
using aux ‹|restrict v3 (clm ts) c| = 1›
restriction.restrict_eq_lan_subs v3_one_lane
by auto
hence "|lan v3| > 1"
using ‹| (restrict v3 (clm ts) c)| = 1› ‹restrict v3 (clm ts) c ≤ lan v3› aux
restriction.restrict_eq_lan_subs v3_one_lane
by auto
thus False using v3_one_lane by auto
qed
have "∥ext v3∥ > 0" using c_def len_eq by auto
have "ts, v3 ⊨ cl(c)" using clm_one len_eq c_def clm_fills_v3 v3_one_lane
by auto
hence "ts,v ⊨ (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤)"
using ‹v2=v3∥v4› ‹v=v1∥v2› by blast
hence "ts,v ⊨❙∃ c. (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤)" by blast
thus False using no_car by best
next
assume "restrict v (res ts) c ≠ ∅"
with one_lane have clm_one:"|restrict v (res ts) c| = 1"
using el_in_restriction_clm_singleton
by (metis nat_int.card_non_empty_geq_one nat_int.card_subset_le
dual_order.antisym restrict_view)
obtain v1 and v2 and v3 and v4
where "v=v1∥v2" and "v2=v3∥v4"
and len_eq:"len v3 ts c = ext v3 ∧ ∥len v3 ts c∥ = ∥len v ts c∥ "
using horizontal_chop_empty_left horizontal_chop_empty_right
len_fills_subview c_def by blast
then have res_non_empty:"restrict v3 (res ts) c ≠ ∅"
using ‹restrict v (res ts) c ≠ ∅› restriction_stable restriction_stable1
by auto
have len_non_empty:"∥len v3 ts c∥ > 0"
using len_eq c_def by auto
have "|restrict v3 (res ts) c| =1 "
using ‹v2=v3∥v4› ‹v=v1∥v2› clm_one restriction_stable restriction_stable1
by auto
have v3_one_lane:"|lan v3| = 1"
using ‹v2=v3∥v4› ‹v=v1∥v2› hchop_def one_lane
by auto
have "restrict v3 (res ts) c = lan v3"
proof (rule ccontr)
assume aux:"restrict v3 (res ts) c ≠ lan v3"
have "restrict v3 (res ts) c ⊑ lan v3"
by (simp add: restrict_view)
hence "∃n. n ❙∉ restrict v3 (res ts) c ∧ n ❙∈ lan v3"
using aux ‹|restrict v3 (res ts) c| = 1› restriction.restrict_eq_lan_subs v3_one_lane
by auto
hence "|lan v3| > 1"
using ‹| (restrict v3 (res ts) c)| = 1› ‹restrict v3 (res ts) c ≤ lan v3› aux
restriction.restrict_eq_lan_subs v3_one_lane
by auto
thus False using v3_one_lane by auto
qed
have "∥ext v3∥ > 0" using c_def len_eq by auto
have "ts, v3 ⊨ re(c)"
using clm_one len_eq c_def ‹restrict v3 (res ts) c = lan v3› v3_one_lane
by auto
hence "ts,v ⊨ (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤)"
using ‹v2=v3∥v4› ‹v=v1∥v2› by blast
hence "ts,v ⊨❙∃ c. (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤)" by blast
thus False using no_car by best
qed
qed
qed
lemma free_means_no_cars:
"⊨free ❙→ ((❙𝗅>0) ❙∧ (❙ω = 1) ❙∧ (❙∀c. ❙¬ (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤)))"
proof (rule allI | rule impI)+
fix ts v
assume assm:"ts,v ⊨ free"
have no_car:"ts,v ⊨(❙∀c. ❙¬ (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤))"
proof (rule ccontr)
assume "¬ (ts,v ⊨(❙∀c. ❙¬ (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤)))"
hence contra:"ts,v ⊨ ❙∃ c. ❙⊤ ❙⌢ (cl(c) ❙∨ re(c)) ❙⌢ ❙⊤" by blast
from this obtain c and v1 and v' and v2 and vc where
vc_def:"(v=v1∥v') ∧ (v'=vc∥v2) ∧ (ts,vc ⊨ cl(c) ❙∨ re(c))" by blast
hence len_ge_zero:"∥len v ts c∥ > 0"
by (metis len_empty_on_subview1 len_empty_on_subview2 less_eq_real_def
real_int.length_ge_zero)
from vc_def have vc_ex_car:
"restrict vc (clm ts) c ≠ ∅ ∨ restrict vc (res ts) c ≠∅"
using nat_int.card_empty_zero one_neq_zero by auto
have eq_lan:"lan v = lan vc" using vc_def hchop_def by auto
hence v_ex_car:"restrict v (clm ts) c ≠ ∅ ∨ restrict v (res ts) c ≠∅"
using vc_ex_car by (simp add: restrict_def)
from len_ge_zero and v_ex_car and assm show False by force
qed
with assm show
"ts,v ⊨((❙𝗅>0) ❙∧ (❙ω = 1) ❙∧ (❙∀c. ❙¬ (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤)))"
by blast
qed
lemma free_eq_no_cars:
"⊨free ❙↔ ((❙𝗅>0) ❙∧ (❙ω = 1) ❙∧ (❙∀c. ❙¬ (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤)))"
using no_cars_means_free free_means_no_cars by blast
lemma free_nowhere_res:"⊨free ❙→ ❙¬(❙⊤ ❙⌢ (re(c)) ❙⌢ ❙⊤)"
using free_eq_no_cars by blast
lemma two_res_not_res: "⊨((re(c) ❙⌣ re(c)) ❙→ ❙¬re(c))"
by (metis add_eq_self_zero one_neq_zero width_add1)
lemma two_clm_width: "⊨((cl(c) ❙⌣ cl(c)) ❙→ ❙ω = 2)"
by (metis one_add_one width_add1)
lemma two_res_no_car: "⊨(re(c) ❙⌣ re(c)) ❙→ ❙¬(❙∃ c. ( cl(c) ❙∨ re(c)) )"
by (metis add_eq_self_zero one_neq_zero width_add1)
lemma two_lanes_no_car:"⊨(❙¬ ❙ω= 1) ❙→ ❙¬(❙∃ c.(cl(c) ❙∨ re(c)))"
by simp
lemma empty_no_car:"⊨( ❙𝗅 = 0) ❙→ ❙¬(❙∃ c.(cl(c) ❙∨ re(c)))"
by simp
lemma car_one_lane_non_empty: "⊨(❙∃ c.(cl(c) ❙∨ re(c))) ❙→ ((❙ω =1) ❙∧ (❙𝗅 > 0))"
by blast
lemma one_lane_notfree:
"⊨(❙ω =1) ❙∧(❙𝗅> 0) ❙∧ (❙¬ free) ❙→ ( (❙⊤ ❙⌢ (❙∃ c. (re(c) ❙∨ cl(c))) ❙⌢ ❙⊤ ))"
proof (rule allI|rule impI)+
fix ts v
assume assm:"ts,v ⊨(❙ω =1) ❙∧(❙𝗅> 0) ❙∧ (❙¬ free)"
hence not_free:"ts,v ⊨❙¬ free" by blast
with free_eq_no_cars have
"ts,v ⊨❙¬ ((❙𝗅>0) ❙∧ (❙ω = 1) ❙∧ (❙∀c. ❙¬ (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤)))"
by blast
hence "ts,v ⊨ ❙¬ (❙∀c. ❙¬ (❙⊤ ❙⌢ ( cl(c) ❙∨ re(c) ) ❙⌢ ❙⊤))"
using assm by blast
thus "ts,v ⊨(❙⊤ ❙⌢ (❙∃ c. (re(c) ❙∨ cl(c))) ❙⌢ ❙⊤ )" by blast
qed
lemma one_lane_empty_or_car:
"⊨(❙ω =1) ❙∧(❙𝗅> 0) ❙→ (free ❙∨ (❙⊤ ❙⌢ (❙∃ c. (re(c) ❙∨ cl(c))) ❙⌢ ❙⊤ ))"
using one_lane_notfree by blast
end
end