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, opaque_lifting) 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, opaque_lifting) 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, opaque_lifting) 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, opaque_lifting) 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, opaque_lifting) 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, opaque_lifting)  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 ( ts) c = len v1 ( ts) c + len v2 ( ts) c"
        proof (cases "left (len v ( ts) c) > left (ext v2)")
          assume inside_v2:"left (len v ( ts) c) > left (ext v2)"
          hence max_geq_v1:"max (left (ext v)) (left ((space ts v) c)) > left (ext v2)" 
            using Abs_real_int_inverse len_in_type len_def by (simp )
          hence outside_v1:"left ((space ts v) c) > right (ext v1)" 
          proof -
            have "left (ext v)  right (ext v1)"
              by (meson chop view.h_chop_middle1)
            then show ?thesis
              using chop max_geq_v1 real_int.rchop_def view.hchop_def by fastforce
          qed
          hence len_v1_0:"len v1 ts c = 0" 
            using Abs_real_int_inverse len_def real_int.length_zero_iff_borders_eq
              outside_v1 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_v2:"  ¬left (ext v2) > right ((space ts v) c) "
            by (meson inside_left less_max_iff_disj less_trans max_geq_v1 order.asym
                space_nonempty)
          have inside_right_v2:"¬left ((space ts v) c) > right (ext v2)" 
            using chop hchop_def inside_right real_int.rchop_def  by auto
          have len2_def:"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 inside_left_v2 inside_right_v2 hchop_def chop space_def
            by auto
          hence "len v ts c = len v2 ts c" 
          proof -
            have "left (ext v)  left (ext v2)"
              by (metis (no_types) chop real_int.rchop_def view.h_chop_middle1
                  view.hchop_def)
            then show ?thesis
              using chop inside_left inside_right len2_def len_def outside_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_v1_0 by (simp)
        next
          assume l_inside_v1: "¬left (len v ( ts) c) > left (ext v2)"
          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)" 
            using Abs_real_int_inverse chop hchop_def l_inside_v1 len_in_type
              len_def real_int.rchop_def
            by auto
          hence 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 inside_left_v1 inside_right_v1 len_def chop hchop_def space_def
            by (simp )
          from inside_left_v1 and inside_right_v1 have len1_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 CollectD CollectI Rep_real_int fst_conv snd_conv by auto
          have inside_left_v2:"  ¬left (ext v2) > right ((space ts v) c) " 
            using real_int.rchop_def hchop_def inside_left chop Abs_real_int_inverse 
              len_def_v len_in_type r_inside_v2 snd_conv
            by auto 
          have inside_right_v2:"¬left ((space ts v) c) > right (ext v2)" 
            using Abs_real_int_inverse chop hchop_def l_inside_v1 len_in_type len_def
              real_int.rchop_def
            by auto
          hence len2_def:"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 inside_left_v2 inside_right_v2 len_def chop hchop_def space_def
            by (auto )
          from inside_left_v2 and inside_right_v2 have len2_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 CollectD CollectI Rep_real_int fst_conv snd_conv 
            by auto
          have left_v_v1:"left (ext v) = left (ext v1)" 
            using chop hchop_def real_int.rchop_def  by auto
          have max: 
               "max (left (ext v)) (left (space ts v c)) = 
                max (left (ext v1)) (left (space ts v c))"
            using left_v_v1 by auto  
          have right_v_v2:"right (ext v) = right (ext v2)" 
            using chop hchop_def real_int.rchop_def  by auto
          have min: "(min (right (ext v)) (right ((space ts v) c))) = 
                (min (right (ext v2)) (right ((space ts v) c)))"                 
            using right_v_v2 by auto
          from max have left_len_v1_v:"left (len v ( ts) c) = left (len v1 ( ts) c)"
            using Abs_real_int_inverse fst_conv len1_def len1_in_type
              len_def_v len_in_type
            by auto
          from min have right_len_v2_v:"right (len v ( ts) c) = right (len v2 ( ts) c)"
            using Abs_real_int_inverse fst_conv len1_def len2_in_type len_def_v 
              len_in_type using len2_def snd_eqD by auto
          have "right (len v1 ( ts) c) = left (len v2 ( ts) c)" 
            using Abs_real_int_inverse chop hchop_def len1_def len1_in_type len2_def
              len2_in_type real_int.rchop_def
            by auto
          thus "len v ts c = len v1 ts c + len v2 ts c" 
            using left_len_v1_v real_int.consec_add right_len_v2_v  by simp 
        qed
      qed
    qed
  qed
qed

lemma len_non_empty_inside:
 "len v ( ts) c > 0 
   left (space ts v c) < right (ext v)  right (space ts v c) > left (ext v)"
proof
  assume assm: "len v ( ts) c > 0"
  show "left ((space ts v) c) < right (ext v)  right ((space ts v) c) > left (ext v)"
  proof (rule ccontr)
    assume "¬(left ((space ts v) c) < right (ext v) 
               right ((space ts v) c) > left (ext v))"
    hence "¬left ((space ts v) c) < right (ext v) 
           ¬right ((space ts v) c) > left (ext v)"
      by best
    thus False
    proof
      assume "¬left ((space ts v) c) < right (ext v)"
      hence "(left ((space ts v) c) = right (ext v)) 
             left ((space ts v) c) > right (ext v)"
        by auto
      thus False
      proof 
        assume left_eq:"left ((space ts v) c) = right (ext v)"
        hence inside_left:"right ((space ts v) c)  left (ext v)"
          by (metis order_trans real_int.left_leq_right)
        from left_eq and inside_left have 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)))"
          using len_def by auto
        hence "len v ( ts) c = Abs_real_int (left (space ts v c), left(space ts v c))" 
          by (metis left_eq max_def min_def real_int.left_leq_right)
        thus False using Abs_real_int_inverse assm real_int.length_def by auto
      next
        assume "left ((space ts v) c) > right (ext v)"
        thus False 
          using Abs_real_int_inverse assm len_def real_int.length_def by auto
      qed
    next
      assume "¬right ((space ts v) c) > left (ext v)"
      hence " right ((space ts v) c) = left (ext v) 
             right ((space ts v) c) < left (ext v)" 
        by auto
      thus False
      proof 
        assume right_eq:"right ((space ts v) c) = left (ext v)"
        hence inside_right:"right (ext v)  left ((space ts v) c)"
          by (metis order_trans real_int.left_leq_right)
        from right_eq and inside_right have 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)))"
          using len_def by auto
        hence 
          "len v ( ts) c = Abs_real_int(right (space ts v c), right (space ts v c))" 
          by (metis max.commute max_def min_def real_int.left_leq_right right_eq)
        thus False using Abs_real_int_inverse assm real_int.length_def by auto
      next
        assume right_le:"right ((space ts v) c) < left (ext v)"
        thus False 
          by (metis (no_types, opaque_lifting) Rep_real_int_inverse assm left.rep_eq len_def
              length_zero_iff_borders_eq less_irrefl prod.collapse real_int.rchop_def 
              right.rep_eq view.hchop_def view.horizontal_chop_empty_left 
              view.horizontal_chop_empty_right)
      qed
    qed
  qed
qed

lemma len_fills_subview:
  "len v ts c > 0 
       ( v1 v2 v3 v'. (v=v1v2)  (v2=v'v3)  len v' ts c = ext v'  
                          len v' ts c = len v ts c)"
proof
  assume assm: "len v ( ts) c > 0" 
  show "  v1 v2 v3 v'. (v=v1v2)  (v2=v'v3)  len v' ( ts) c = ext v'  
          len v' ( ts) c = len v ( ts) c"
  proof -
    from assm have inside:
      "left ((space ts v) c) < right (ext v)  right ((space ts v) c) > left (ext v)" 
      using len_non_empty_inside by auto
    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)))" 
      using len_def by auto
    obtain v1 and v2 and v3 and v' 
      where v1:
        "v1=ext =Abs_real_int(left(ext v), left (len v ts c)),
             lan = lan v,
             own = own v"
      and v2:
      "v2=ext =Abs_real_int(left(len v ts c), right (ext v)),
           lan = lan v,
           own = own v"
      and v':
      "v'=ext =Abs_real_int(left(len v ts c), right (len v ts c)),
           lan = lan v,
           own = own v"
      and v3:
      "v3=ext =Abs_real_int(right(len v ts c), right (ext v)),
           lan = lan v,
           own = own v" 
        by blast 
    hence 1:" (v=v1v2)  (v2=v'v3)"
      using inside hchop_def real_int.rchop_def Abs_real_int_inverse real_int.left_leq_right
        v1 v2 v' v3 len_def
      by auto
    have right:"right (ext v') = right (len v ts c)" 
      by (simp add: Rep_real_int_inverse  v')
    then have right':"left ((space ts v) c)  right (ext v')"
      by (metis inside len_space_left less_imp_le order_trans real_int.left_leq_right)
    have left:"left (ext v') = left (len v ts c)"
      by (simp add: Rep_real_int_inverse  v')
    then have left':"right ((space ts v) c)  left (ext v')"
      by (metis inside len_space_right less_imp_le order_trans real_int.left_leq_right)
    have inside':
      "left ((space ts v) c) < right (ext v')  right ((space ts v) c) > left (ext v')"
      by (metis (no_types) left' right' antisym_conv assm inside left len_space_left
          len_space_right less_imp_le not_le real_int.left_leq_right
          real_int.length_zero_iff_borders_eq right)
    have inside'':
      "left (space ts v' c) < right (ext v')  right (space ts v' c) > left (ext v')" 
      using "1" hchop_def inside' sensors.space_def sensors_axioms
      by auto
    have len_v_v':"len v ts c = ext v'" 
      by (metis left prod.collapse right left.rep_eq right.rep_eq Rep_real_int_inverse)
    have "left (len v ts c) = max (left (ext v)) (left ((space ts v) c)) "
      using len_v Abs_real_int_inverse Rep_real_int inside
      by auto
    with left have left_len':"left (ext v') = max (left (ext v)) (left (space ts v c))"
      by auto
    then have left_len:"left (ext v') = max (left (ext v')) (left (space ts v' c))" 
      using "1"  hchop_def space_def  by fastforce 
    have "right (len v ts c) = min (right (ext v)) (right ((space ts v) c))" 
      using len_v Abs_real_int_inverse inside Rep_real_int by auto
    with right have right_len':
      "right (ext v') = min (right (ext v)) (right (space ts v c))" 
      by auto
    then have right_len:
      "right (ext v') = min (right (ext v')) (right (space ts v' c))"         
      using "1"  hchop_def space_def by fastforce 
    have 2:"len v' ( ts) c = ext v'"
      by (metis left_len' right_len' len_v len_v_v' order.asym inside''
          len_def left_len right_len) 
    have 3:"  len v' ( ts) c = len v ( ts) c"
      using len_left len_right hchop_def 
      by (simp add: "2" len_v_v') 
    then show ?thesis using 1 2 3 by blast
  qed
qed

lemma ext_eq_len_eq:
  "ext v = ext v' own v = own v'  len v ts c = len v' ts c" 
  using left_space right_space sensors.len_def sensors_axioms by auto

lemma len_stable_down:"(v=v1--v2)  len v ts c = len v1 ts c" 
  using ext_eq_len_eq view.vchop_def by blast

lemma len_stable_up:"(v=v1--v2)  len v ts c = len v2 ts c"
  using ext_eq_len_eq view.vchop_def by blast

lemma len_empty_subview:"len v ts c = 0  (v'  v)  len v' ts c = 0" 
proof
  assume assm:"len v ts c = 0  (v'  v)"
  hence "v1 v2 v3 vl vr vu vd. (v=vlv1)  (v1=v2vr)  (v2=vd--v3)  (v3=v'--vu)" using
      somewhere_leq   by auto
  then obtain v1 v2 v3 vl vr vu vd 
    where views:"(v=vlv1)  (v1=v2vr)  (v2=vd--v3)  (v3=v'--vu)"
    by blast
  have "len v1 ts c = 0" using views assm len_empty_on_subview2 by blast
  hence "len v2 ts c = 0" using views len_empty_on_subview1 by blast
  hence "len v3 ts c  = 0" using views len_stable_up by auto
  thus "len v' ts c  = 0" using views len_stable_down by auto
qed

lemma view_leq_len_leq:"(ext v  ext v')  (own v = own v')  len v ts c > 0 
                           len v ts c  len v' ts c" 
  using Abs_real_int_inverse  length_def length_ge_zero less_eq_real_int_def 
    sensors.len_def sensors.space_def sensors_axioms by auto

end
end