Session Hybrid_Multi_Lane_Spatial_Logic

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" 
    by (simp add: inf_nat_int.rep_eq less_eq_nat_int.rep_eq)
  show " inf i   j  i" 
    by (simp add: inf_nat_int.rep_eq less_eq_nat_int.rep_eq) 
  show "inf i  j  j" 
    by (simp add: inf_nat_int.rep_eq less_eq_nat_int.rep_eq) 
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_intnat_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 
    by (simp add: bot_nat_int.abs_eq)
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}" 
    by (simp add: Abs_nat_int_inverse el_def)
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)"
  by (simp add: inter_distr1 inf_commute)
    
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" 
    using One_nat_def Suc_le_lessD ‹consec i j add.right_neutral add_Suc_right
      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" 
    by (simp add: nat_int.consec_def)
  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)" 
    by (simp add: assm nat_int.consec_un_min)
  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)" 
    by (simp add: assm nat_int.consec_un_min) 
  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 
    by (simp add: nat_int.consec_un_max)
  have none_empty:"i    j    k  " using assm by (simp add: consec_def)
  hence un_non_empty:"ij  " 
    using bot.extremum_uniqueI consec_x_y nat_int.un_subset2 by force
  have max:"maximum (ij) +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)" 
    by (simp add: assm nat_int.consec_un_max)  
  have min_y_yz:"minimum j = minimum (j  k)" 
    by (simp add: consec_y_z nat_int.consec_un_min)
  have none_empty:"i    j    k  " using assm by (simp add: consec_def)
  then have un_non_empty:"jk  " 
    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)"
    by (metis Int_iff add.commute add.left_neutral assm card.infinite card_Un_disjoint
        emptyE le_add1 le_antisym local.consec_def nat_int.card'.rep_eq
        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}"
  by (simp add: Abs_nat_int_inverse)

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(,,)"
  by (simp add: chop_empty_left)
    
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" 
          by (metis j_def k_def One_nat_def Suc_leI add.assoc diff_add n_le consec_def
              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)"
  using chop_add1 by force
    
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))" 
        by (simp add: nchop_def)
      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
    Author:     Sven Linker

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

lemma consec_add:
  "left r = left s  right r = right t  right s = left t  r = s + t"
  by (simp add:length_def)
    
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)" 
    by (simp add: Abs_real_int_inverse 1)
  from 2 have right:"right (shift r (x+y)) = (right r) +(x+y)" 
    by (simp add: Abs_real_int_inverse 1)
  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
  with 1 show ?thesis by (simp add: add.assoc)
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 
    by (simp add:  x1_def)
  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)" 
    by (simp add: Abs_real_int_inverse real_int.rchop_def)
  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)" 
    by (simp add: Abs_real_int_inverse real_int.rchop_def)
  then show "y. R_Chop(x,y,x)" by blast
qed
  
lemma chop_add_length:"R_Chop(r,s,t)  r = s + t"
  using consec_add by (simp add: rchop_def)
    
lemma chop_add_length_ge_0:"R_Chop(r,s,t)  s > 0  t>0  r>0"
  using chop_add_length by auto
    
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
    Author:     Sven Linker

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
define or prove any additional structure about it.
›

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 . cd" 
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
    Author:     Sven Linker

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 :: (carsreal)*(carslanes)*(carslanes)*(carsrealreal)*(carsreal)*(carsreal).
          (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 ::(carsreal)*(carslanes)*(carslanes)*(carsrealreal)*(carsreal)*(carsreal).
           (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 ::
  "trafficcarsnattrafficbool" ("_ 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 ::
  "trafficcars trafficbool" ("_ 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 ::
  "trafficcarstrafficbool" ("_ 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 ::
  "trafficcarsnattraffic 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::
  "trafficcars(realreal)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::
  "trafficrealtrafficbool" (" _  _  _" 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 ::(carsreal)*(carslanes)*(carslanes)*(carsrealreal)*(carsreal)*(carsreal).
           (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

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=uw) == 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=uw)  left (ext v)  right (ext u)" 
  by (metis hchop_def real_int.rchop_def real_int.left_leq_right)
    
lemma h_chop_middle2:"(v=uw)  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=uw)" 
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=V1V2" 
    using hchop_def x1_x2_def by (simp)
  thus ?thesis by blast
qed
  
lemma horizontal_chop_empty_right :"v.  u. (v=vu)" 
  using hchop_def real_int.chop_singleton_right 
  by (metis (no_types, hide_lams) select_convs) 
    
lemma horizontal_chop_empty_left :"v. u. (v=uv)" 
  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=uw)  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=V1V2)  ext V1 > 0  ext V2>0" 
   using  chop hchop_def v1_def by (simp)
  then show " (V1 V2. (v=V1V2)  ext V1 > 0  ext V2>0)"
    by blast
qed
  
  
lemma horizontal_chop_split_add:
  "x  0  y  0  ext v = x+y  (u w. (v=uw)  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}" 
    by (simp add: geq_0)
  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}" 
    by (simp add: geq_0)
  from v1_def and geq_0 have len_v1:"ext u = x" using v1_in_type 
    by (simp add: Abs_real_int_inverse  real_int.length_def) 
  from v2_def and geq_0 have len_v2:"ext w= y" using v2_in_type 
    by (simp add: Abs_real_int_inverse  real_int.length_def) 
  from v1_def and v2_def have "(v=uw)" 
    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=uw)  ext u = x  ext w = y" by simp
  thus "(u w. (v=uw)  ext u = x  ext w = y)" by blast
qed
  
lemma horizontal_chop_assoc1:
  "(v=v1v2)  (v2=v3v4)  (v'. (v=v'v4)  (v'=v1v3))"
proof
  assume assm:"(v=v1v2)  (v2=v3v4)"
  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'=v1v3" using v'_def assm real_int.chop_assoc1 hchop_def by auto
  from 1 and 2 have "(v=v'v4)   (v'=v1v3)" by best
  thus "(v'. (v=v'v4)   (v'=v1v3))" ..
qed
  
lemma horizontal_chop_assoc2:
  "(v=v1v2)  (v1=v3v4)  (v'. (v=v3v')  (v'=v4v2))"
proof
  assume assm:"(v=v1v2)  (v1=v3v4)"
  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=v3v'" 
    using assm fst_conv real_int.chop_assoc2 snd_conv hchop_def by auto
  have 2: "v'=v4v2" 
    using assm real_int.chop_assoc2 v'_def hchop_def by auto
  from 1 and 2 have "(v=v3v')  (v'=v4v2)" by best
  thus "(v'. (v=v3v')  (v'=v4v2))" ..
qed
  
  
  
  
lemma horizontal_chop_width_stable:"(v=uw)|lan v|=|lan u||lan v|=|lan w|"
  using hchop_def by auto
    
lemma horizontal_chop_own_trans:"(v=uw)  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|"
  using nat_int.chop_add1 vchop_def by fastforce

    
lemma vertical_chop_add2:
  "|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"
    using chop_add2 by blast
  obtain i and j where l1_l2_def:"N_Chop(lan v, i,j)  |i| = x  |j| = y"
    using add by blast
  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"
  by (metis le_add1 trans_le_add2 vertical_chop_add1)
    
lemma horizontal_chop_leq1:"(v=uw)  u  v"
  using real_int.chop_leq1 hchop_def less_eq_view_ext_def order_refl by fastforce
    
lemma horizontal_chop_leq2:"(v=uw)  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'=vlv1)  (v1=v2vr)  (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'=vlv1) (v1=v2vr)" 
    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'=vlv1)  (v1=v2vr)  (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 = " 
          by (simp add: consec nat_int.consec_inter_empty)
        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')"
            by (simp add: max)
          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'=vlv1)  (v1=v2vr)  (v2=vd--v3)  (v3=v--vu)"
  then obtain v1 v2 v3 vl vr vu vd 
    where " (v'=vlv1)  (v1=v2vr)  (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)"
  by (simp add:switch_def)
    
lemma switch_symm:"(v=c>u)  (u=(own v)>v)" 
  by (simp add:switch_def)
    
lemma switch_trans:"(v=c>u)  (u=d>w)  (v=d>w)"
  by (simp add: switch_def)
    
lemma switch_triangle:"(v=c>u)  (v=d>w)  (u=d>w)"
  using switch_def by auto
    
lemma switch_hchop1:
  "(v=v1v2)  (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=v1v2))"
  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 
    by (simp add: less_eq_view_ext_def v'_def)
  have lan:"lan v'  lan v" using assm switch_def 
    by (simp add: less_eq_view_ext_def v'_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 
    by (simp add: less_eq_view_ext_def)
  have switch:"v' =c> u'" using v'_def switch_def assm 
    by (simp add: less_eq_view_ext_def)     
  show  "(v'. ( v' = c > u')  v'  v)" using switch less by blast
qed
end
end

Theory Restriction

(*  Title:      Restriction.thy
    Author:     Sven Linker

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=uw)  restrict u f  c = restrict w f  c"
  using hchop_def restrict_def by auto
    
lemma restriction_stable1:"(v=uw)  restrict v f  c = restrict u f  c"
  by (simp add: hchop_def restrict_def)
    
lemma restriction_stable2:"(v=uw)  restrict v f  c = restrict w f  c"
  by (simp add: restriction_stable restriction_stable1)
    
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) = " 
    by (simp add: bot.extremum_uniqueI)
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
          by (simp add: nat_int.consec_lesser)
        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))" 
    by (simp add: inf_nat_int.rep_eq nat_int.el_def)
  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" 
    by (simp add: nat_int.card_non_empty_geq_one)
  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 = "
  using nat_int.card_un_add nat_int.card_empty_zero restriction_un atMostOneClm
    nat_int.chop_add1 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 
    restriction_clm_v2_non_empty_v1_empty
  by meson
    
    
    
lemma restriction_add_res:
  "(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) crestrict 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|" 
    by (metis add.right_neutral add_cancel_left_left assm nat_int.card_empty_zero
        nat_int.card_un_add nat_int.un_empty_absorb1 nat_int.un_empty_absorb2 
        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
    

lemma restriction_add_clm:
  "(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=vlv1)(v1=v2vr)(v2=vu--v3)(v3=v'--vd)|restrict v' f c|=1
       |restrict v f c|  1" 
proof
  assume assm:
    "(v=vlv1)(v1=v2vr)(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" 
         by (simp add: assm less_le)
       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:
  "(tsr(c)ts') 
     restrict v (res ts') c = restrict v (res ts) c  restrict v (clm ts) c"
proof
  assume assm:"(tsr(c)ts')"
  hence res_ts':"res ts' c = res ts c  clm ts c" 
    by (simp add: create_reservation_def)
  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" 
      by (simp add: restrict_def)
    thus ?thesis using restrict_clm 
      by (simp add: nat_int.un_empty_absorb1)
  next 
    case False
    hence "consec (clm ts c) (res ts c)  consec (res ts c) (clm ts c)" 
      by (simp add: clm_consec_res)
    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
    Author:     Sven Linker

  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))"  
      by (metis f2 real_int.shift_additivity)
    then show ?thesis
      using move_def f2 by simp
  qed
qed

lemma move_stability_res:"(tsr(c)ts')  move ts ts' v = v" 
  and move_stability_clm: "(tsc(c,n)ts')  move ts ts' v = v"
  and move_stability_wdr:"(tswdr(c,n)ts')  move ts ts' v = v"
  and move_stability_wdc:"(tswdc(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
    Author:     Sven Linker

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
    Author:     Sven Linker

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=v1v2)  (right (len v1 ts c) = right (ext v1))"
proof
  assume assm:"((len v ts) c = ext v)  (v=v1v2)"
  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 "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=v1v2)  (left ((len v1 ts) c) = left (ext v1))"
proof
  assume assm:"((len v ts) c = ext v)  (v=v1v2)"
  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=v1v2)  ((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=v1v2)  (left ((len v2 ts) c) = left (ext v2))"
proof
  assume assm:"((len v ts) c = ext v)  (v=v1v2)"
  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=v1v2)  (right ((len v2 ts) c) = right (ext v2))"
proof
  assume assm:"((len v ts) c = ext v)  (v=v1v2)"
  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=v1v2)  ((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=v1v2)  (len v1 ( ts) c = ext v1)  (len v2 ( ts) c = ext v2)
      (len v ( ts) c = ext v)" 
proof
  assume assm:"(v=v1v2)  (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
        by (simp add: hchop_def real_int.rchop_def)
      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"
        by (metis add.right_neutral real_int.chop_singleton_left
            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=v1v2)  len v1 ( ts) c = 0" 
proof
  assume assm:"len v ( ts) c = 0  (v=v1v2)"
  then have len_v_borders:"left (len v ( ts) c) = right (len v ( ts) c)" 
    by (simp add:real_int.length_zero_iff_borders_eq)  
  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)))" 
        by (simp add: len_def)
      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=v1v2)  len v2 ts c = 0"
proof
  assume assm:"len v ( ts) c = 0  (v=v1v2)"
  then have len_v_borders:"left (len v ( ts) c) = right (len v ( ts) c)"
     by (simp add:real_int.length_zero_iff_borders_eq)  
  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)))" 
        by (simp add: len_def)
      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

lemma len_hchop_add:
  "(v=v1v2)  len v ts c = len v1 ts c + len v2 ts c" 
proof
  assume chop:"v=v1v2"
  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" 
      by (metis add_cancel_right_left len_empty_on_subview1 len_empty_on_subview2)
    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" 
        by (metis add_cancel_right_left len_empty_on_subview1 len_empty_on_subview2)
      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 (