Theory stream

(*<*)
(*
   Title:  Theory  stream.thy (FOCUS streams)
   Author: Maria Spichkova <maria.spichkova at rmit.edu.au>, 2013
*)
(*>*)

section "FOCUS streams: operators and lemmas"
 
theory stream
  imports ListExtras ArithExtras
begin

subsection ‹Definition of the FOCUS stream types›

― ‹Finite timed FOCUS stream›
type_synonym 'a fstream = "'a list list"

― ‹Infinite timed FOCUS stream›
type_synonym 'a istream = "nat ⇒ 'a list"

― ‹Infinite untimed FOCUS stream›
type_synonym 'a iustream = "nat ⇒ 'a"

― ‹FOCUS stream (general)›
datatype 'a stream = 
          FinT "'a fstream" ― ‹finite timed streams›
        | FinU "'a list" ― ‹finite untimed streams›
        | InfT "'a istream" ― ‹infinite timed streams›
        | InfU "'a iustream" ― ‹infinite untimed streams›


subsection ‹Definitions of operators›
  
― ‹domain of an infinite untimed stream›
definition
   infU_dom :: "natInf set"
 where
  "infU_dom ≡ {x. ∃ i. x = (Fin i)} ∪ {∞}"
  
― ‹domain of a finite untimed stream (using natural numbers enriched by Infinity)›
definition
   finU_dom_natInf :: "'a list ⇒ natInf set"
   where
  "finU_dom_natInf s ≡ {x. ∃ i. x = (Fin i) ∧ i < (length s)}"

― ‹domain of a finite untimed stream›
primrec
finU_dom :: "'a list ⇒ nat set"
where
  "finU_dom [] = {}" |
  "finU_dom (x#xs) = {length xs} ∪ (finU_dom xs)"

― ‹range of a finite timed stream›
primrec
  finT_range :: "'a fstream ⇒ 'a set"
where  
  "finT_range [] = {}" |
  "finT_range (x#xs) = (set x) ∪ finT_range xs"

― ‹range of a finite untimed stream›
definition
   finU_range :: "'a list ⇒ 'a set"
where
  "finU_range x ≡ set x"

― ‹range of an infinite timed stream›
definition
   infT_range :: "'a istream ⇒ 'a set"
where
  "infT_range s ≡ {y. ∃ i::nat. y mem (s i)}"

― ‹range of a finite untimed stream›
definition
   infU_range :: "(nat ⇒ 'a) ⇒ 'a set"
where
  "infU_range s ≡ { y. ∃ i::nat. y = (s i) }"

― ‹range of a (general) stream›
definition
   stream_range :: "'a stream ⇒ 'a set"
where
 "stream_range s ≡ case s of
       FinT x ⇒ finT_range x 
     | FinU x ⇒ finU_range x 
     | InfT x ⇒ infT_range x  
     | InfU x ⇒ infU_range x" 

― ‹finite timed stream that consists of n empty time intervals› 
primrec
   nticks :: "nat ⇒ 'a fstream"
where
  "nticks 0 = []" |
  "nticks (Suc i) = [] # (nticks i)"

― ‹removing the first element from an infinite stream›
― ‹in the case of an untimed stream: removing the first data element›  
― ‹in the case of a timed stream: removing the first time interval› 
definition
   inf_tl :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a)"
where
  "inf_tl s ≡ (λ i. s (Suc i))"

― ‹removing i first elements from an infinite stream s›  
― ‹in the case of an untimed stream: removing i first data elements›  
― ‹in the case of a timed stream: removing i first time intervals› 
definition
   inf_drop :: "nat ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)"
where
  "inf_drop i s ≡  λ j. s (i+j)"  

― ‹finding the first nonempty time interval in a finite timed stream›
primrec
 fin_find1nonemp :: "'a fstream ⇒ 'a list"
where 
 "fin_find1nonemp [] = []" |
 "fin_find1nonemp (x#xs) =
    ( if x = []
      then fin_find1nonemp xs
      else x )"

― ‹finding the first nonempty time interval in an infinite timed stream›
definition 
  inf_find1nonemp :: "'a istream ⇒ 'a list"
where
 "inf_find1nonemp s 
  ≡
  ( if (∃ i. s i ≠ [])
    then s (LEAST i. s i ≠ [])
    else [] )"

― ‹finding the index of the first nonempty time interval in a finite timed stream›
primrec
 fin_find1nonemp_index :: "'a fstream ⇒ nat"
where
 "fin_find1nonemp_index [] = 0" |
 "fin_find1nonemp_index (x#xs) =
    ( if x = []
      then Suc (fin_find1nonemp_index xs)
      else 0 )"

― ‹finding the index of the first nonempty time interval in an infinite timed stream›
definition
  inf_find1nonemp_index :: "'a istream ⇒ nat"
where
 "inf_find1nonemp_index s 
  ≡
  ( if (∃ i. s i ≠ [])
    then (LEAST i. s i ≠ [])
    else 0 )"

― ‹length of a finite timed stream: number of data elements in this stream›  
primrec
  fin_length :: "'a fstream ⇒ nat"
where
  "fin_length [] = 0" |
  "fin_length (x#xs) = (length x) + (fin_length xs)"

― ‹length of a (general) stream›
definition
   stream_length :: "'a stream ⇒ natInf"
where
  "stream_length s ≡ 
      case s of 
                (FinT x) ⇒ Fin (fin_length x) 
              | (FinU x) ⇒ Fin (length x)  
              | (InfT x) ⇒ ∞ 
              | (InfU x) ⇒ ∞"

― ‹removing the first k elements from a finite (nonempty) timed stream›
axiomatization
  fin_nth :: "'a fstream ⇒ nat ⇒ 'a"
where 
   fin_nth_Cons:
  "fin_nth (hds # tls) k = 
      ( if hds = []
        then fin_nth tls k
        else ( if (k < (length hds))
               then nth hds k
               else fin_nth tls (k - length hds) ))"

― ‹removing i first data elements from an infinite timed stream s›   
primrec
  inf_nth :: "'a istream ⇒ nat ⇒ 'a"
where 
 "inf_nth s 0 =  hd (s (LEAST i.(s i) ≠ []))"  |
 "inf_nth s (Suc k) = 
      ( if ((Suc k) < (length (s 0))) 
        then (nth (s 0) (Suc k))
        else ( if (s 0) = []
               then (inf_nth (inf_tl (inf_drop 
                     (LEAST i. (s i) ≠ []) s)) k )
               else inf_nth (inf_tl s) k ))"

― ‹removing the first k data elements from a (general) stream›
definition
    stream_nth :: "'a stream ⇒ nat ⇒ 'a"
where
   "stream_nth s k ≡ 
         case s of (FinT x) ⇒ fin_nth x k
                 | (FinU x) ⇒ nth x k
                 | (InfT x) ⇒ inf_nth x k 
                 | (InfU x) ⇒ x k"

― ‹prefix of an infinite stream›
primrec 
  inf_prefix :: "'a list ⇒ (nat ⇒ 'a) ⇒ nat ⇒ bool"
where   
  "inf_prefix [] s k = True" |
  "inf_prefix (x#xs) s k = ( (x = (s k)) ∧ (inf_prefix xs s (Suc k)) )"

― ‹prefix of a finite stream›
primrec 
  fin_prefix :: "'a list ⇒ 'a list ⇒ bool"
where   
  "fin_prefix [] s = True" |
  "fin_prefix (x#xs) s = 
     (if (s = []) 
      then False
      else (x = (hd s)) ∧ (fin_prefix xs s) )"

― ‹prefix of a (general) stream›
definition
   stream_prefix :: "'a stream ⇒ 'a stream ⇒ bool"
where
  "stream_prefix p s ≡
   (case p of 
        (FinT x) ⇒ 
        (case s of (FinT y) ⇒  (fin_prefix x y)
                 | (FinU y) ⇒ False
                 | (InfT y) ⇒ inf_prefix x y 0
                 | (InfU y) ⇒ False )
      | (FinU x) ⇒ 
        (case s of (FinT y) ⇒ False
                 | (FinU y) ⇒  (fin_prefix x y)
                 | (InfT y) ⇒ False
                 | (InfU y) ⇒  inf_prefix x y 0 )    
      | (InfT x) ⇒
        (case s of (FinT y) ⇒ False
                 | (FinU y) ⇒ False
                 | (InfT y) ⇒ (∀ i. x i = y i)
                 | (InfU y) ⇒ False ) 
      | (InfU x) ⇒
        (case s of (FinT y) ⇒ False
                 | (FinU y) ⇒ False
                 | (InfT y) ⇒ False
                 | (InfU y) ⇒ (∀ i. x i = y i) )  )"

― ‹truncating a finite stream after the n-th element›
primrec  
fin_truncate :: "'a list ⇒ nat ⇒ 'a list"
where 
  "fin_truncate [] n = []" |
  "fin_truncate (x#xs) i = 
      (case i of 0 ⇒ [] 
         | (Suc n) ⇒ x # (fin_truncate xs n))"

― ‹truncating a finite stream after the n-th element›
― ‹n is of type of natural numbers enriched by Infinity›
definition
  fin_truncate_plus :: "'a list ⇒ natInf ⇒ 'a list"
 where
 "fin_truncate_plus s n 
  ≡ 
  case n of (Fin i) ⇒ fin_truncate s i
           |  ∞     ⇒ s "

― ‹truncating an infinite stream after the n-th element›
primrec
  inf_truncate :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a list"
where   
   "inf_truncate s 0 = [ s 0 ]" |
   "inf_truncate s (Suc k) = (inf_truncate s k) @ [s (Suc k)]"

― ‹truncating an infinite stream after the n-th element›
― ‹n is of type of natural numbers enriched by Infinity›
definition
  inf_truncate_plus :: "'a istream ⇒ natInf ⇒ 'a stream" 
 where
 "inf_truncate_plus s n 
  ≡ 
  case n of (Fin i) ⇒ FinT (inf_truncate s i)
           | ∞     ⇒ InfT s"

― ‹concatanation of a finite and an infinite stream›
definition
    fin_inf_append :: 
        "'a list ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)"
where
"fin_inf_append us s ≡  
 (λ i. ( if (i < (length us))
         then (nth us i)
         else s (i - (length us)) ))" 
 
― ‹insuring that the infinite timed stream is time-synchronous›
definition
   ts :: "'a istream ⇒ bool"
where
"ts s ≡  ∀ i. (length (s i) = 1)"

― ‹insuring that each time interval of an infinite timed stream contains at most n data elements›
definition
  msg :: "nat ⇒ 'a istream ⇒ bool"
where
 "msg n s ≡  ∀ t. length (s t) ≤ n"

― ‹insuring that each time interval of a finite timed stream contains at most n data elements›
primrec
  fin_msg :: "nat ⇒ 'a list list ⇒ bool"
where   
 "fin_msg n [] = True" |
 "fin_msg n (x#xs) = (((length x) ≤ n) ∧ (fin_msg n xs))" 

― ‹making a finite timed stream to a finite untimed stream›
definition
   fin_make_untimed :: "'a fstream  ⇒ 'a list"
where
  "fin_make_untimed x ≡  concat x"

― ‹making an infinite timed stream to an infinite untimed stream›
― ‹(auxiliary function)›
primrec
  inf_make_untimed1 :: "'a istream ⇒ nat ⇒ 'a "
where 
inf_make_untimed1_0:
  "inf_make_untimed1 s 0 =  hd (s (LEAST i.(s i) ≠ []))"  |
inf_make_untimed1_Suc:
  "inf_make_untimed1 s (Suc k) =
    ( if ((Suc k) < length (s 0))
      then nth (s 0) (Suc k)
      else ( if (s 0) = []
             then (inf_make_untimed1 (inf_tl (inf_drop 
                          (LEAST i. ∀ j. j < i ⟶ (s j) = [])
                           s)) k )
             else inf_make_untimed1 (inf_tl s) k ))"
             
― ‹making an infinite timed stream to an infinite untimed stream›
― ‹(main function)›
definition
   inf_make_untimed :: "'a istream ⇒ (nat ⇒ 'a) "
where
  "inf_make_untimed s
   ≡ 
   λ i. inf_make_untimed1 s i"

― ‹making a (general) stream untimed›
definition
    make_untimed :: "'a stream  ⇒ 'a stream"
where
   "make_untimed s ≡ 
      case s of (FinT x) ⇒ FinU (fin_make_untimed x)
              | (FinU x) ⇒ FinU x
              | (InfT x) ⇒ 
                (if (∃ i.∀ j. i < j ⟶ (x j) = [])
                 then FinU (fin_make_untimed (inf_truncate x 
                             (LEAST i.∀ j. i < j ⟶ (x j) = [])))
                 else InfU (inf_make_untimed x))
              | (InfU x) ⇒ InfU x"


― ‹finding the index of the time interval that contains the k-th data element›
― ‹defined over a finite timed stream›
primrec
  fin_tm :: "'a fstream ⇒ nat ⇒ nat"
where
  "fin_tm [] k = k" |
  "fin_tm (x#xs) k = 
    (if k = 0
     then 0
     else (if (k ≤ length x)
           then (Suc 0)
           else Suc(fin_tm xs (k - length x))))"

― ‹auxiliary lemma for the definition of the truncate operator›
lemma inf_tm_hint1:
  assumes "i2 = Suc i - length a"
      and "¬ Suc i ≤ length a" 
      and "a ≠ []" 
  shows "i2 < Suc i"
using assms
by auto


― ‹filtering a finite timed stream›
definition
   finT_filter :: "'a set => 'a fstream => 'a fstream"   
where 
  "finT_filter m s ≡  map (λ s. filter (λ y. y ∈ m) s) s"

― ‹filtering an infinite timed stream›
definition
   infT_filter :: "'a set => 'a istream => 'a istream"  
where
  "infT_filter m s ≡  (λi.( filter (λ x. x ∈ m) (s i)))"

― ‹removing duplications from a finite timed stream›
definition
   finT_remdups :: "'a fstream => 'a fstream"
where  
  "finT_remdups s ≡  map (λ s. remdups s) s"

― ‹removing duplications from an infinite timed stream›
definition
   infT_remdups :: "'a istream => 'a istream"  
where
  "infT_remdups s ≡  (λi.( remdups (s i)))"

― ‹removing duplications from a time interval of a stream›
primrec
   fst_remdups :: "'a list ⇒ 'a list"
where
 "fst_remdups [] = []" |
 "fst_remdups (x#xs) = 
    (if xs = [] 
     then [x]
     else (if x = (hd xs)
           then fst_remdups xs
           else (x#xs)))"

― ‹time interval operator›
definition
  ti :: "'a fstream ⇒ nat ⇒ 'a list"
where
 "ti s i ≡  
    (if s = []
     then []
     else (nth s i))"

― ‹insuring that a sheaf of channels is correctly defined›
definition
   CorrectSheaf :: "nat ⇒ bool"
where
  "CorrectSheaf n ≡ 0 < n"
 
― ‹insuring that all channels in a sheaf are disjunct›
― ‹indices in the sheaf are represented using an extra specified set›
definition
   inf_disjS :: "'b set ⇒ ('b ⇒ 'a istream) ⇒ bool"
where
  "inf_disjS IdSet nS
   ≡
   ∀ (t::nat) i j. (i:IdSet) ∧ (j:IdSet) ∧  
   ((nS i) t) ≠ []  ⟶ ((nS j) t) = []"  

― ‹insuring that all channels in a sheaf are disjunct›
― ‹indices in the sheaf are represented using natural numbers›
definition              
   inf_disj :: "nat ⇒ (nat ⇒ 'a istream) ⇒ bool"
where
  "inf_disj n nS
   ≡
   ∀ (t::nat) (i::nat) (j::nat). 
   i < n  ∧  j < n ∧ i ≠ j ∧ ((nS i) t) ≠ []  ⟶ 
   ((nS j) t) = []"  

― ‹taking the prefix of n data elements from a finite timed stream›
― ‹(defined over natural numbers)›
fun fin_get_prefix  :: "('a fstream × nat) ⇒ 'a fstream"
where
  "fin_get_prefix([], n) = []" |
  "fin_get_prefix(x#xs, i) = 
     ( if (length x) < i 
       then x # fin_get_prefix(xs, (i - (length x)))
       else [take i x] ) "

― ‹taking the prefix of n data elements from a finite timed stream›
― ‹(defined over natural numbers enriched by Infinity)›
definition
  fin_get_prefix_plus :: "'a fstream ⇒ natInf ⇒ 'a fstream"
where
 "fin_get_prefix_plus s n 
  ≡ 
  case n of (Fin i) ⇒ fin_get_prefix(s, i)
           | ∞      ⇒ s "

― ‹auxiliary lemmas›
lemma length_inf_drop_hint1: 
  assumes "s k ≠ []"
  shows    "length (inf_drop k s 0) ≠ 0"
using assms
by (auto simp: inf_drop_def)

lemma length_inf_drop_hint2:
"(s 0 ≠ [] ⟶ length (inf_drop 0 s 0) < Suc i 
  ⟶ Suc i - length (inf_drop 0 s 0) < Suc i)"
  by (simp add: inf_drop_def list_length_hint1)

― ‹taking the prefix of n data elements from an infinite timed stream›
― ‹(defined over natural numbers)›
fun infT_get_prefix  :: "('a istream × nat) ⇒ 'a fstream"
where   
  "infT_get_prefix(s, 0) = []"
|
  "infT_get_prefix(s, Suc i) = 
    ( if (s 0) = []
      then ( if (∀ i. s i = [])
             then []
             else (let 
                     k = (LEAST k. s k ≠ [] ∧ (∀i. i < k ⟶ s i = []));
                     s2 = inf_drop (k+1) s
                   in (if (length (s k)=0) 
                       then [] 
                       else (if (length (s k) < (Suc i)) 
                             then s k # infT_get_prefix (s2,Suc i - length (s k))
                             else [take (Suc i) (s k)] )))
           )
      else 
        (if ((length (s 0)) < (Suc i)) 
         then (s 0) # infT_get_prefix( inf_drop 1 s, (Suc i) - (length (s 0)))
         else [take (Suc i) (s 0)] 
         )
     )"

― ‹taking the prefix of n data elements from an infinite untimed stream›
― ‹(defined over natural numbers)›
primrec
  infU_get_prefix  :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a list"
where
  "infU_get_prefix s 0 = []" |
  "infU_get_prefix s (Suc i) 
         = (infU_get_prefix s i) @ [s i]"

― ‹taking the prefix of n data elements from an infinite timed stream›
― ‹(defined over natural numbers enriched by Infinity)›
definition
  infT_get_prefix_plus :: "'a istream ⇒ natInf ⇒ 'a stream"
where
"infT_get_prefix_plus s n 
  ≡ 
  case n of (Fin i) ⇒ FinT (infT_get_prefix(s, i)) 
           | ∞     ⇒ InfT s"

― ‹taking the prefix of n data elements from an infinite untimed stream›
― ‹(defined over natural numbers enriched by Infinity)›
definition
  infU_get_prefix_plus :: "(nat ⇒ 'a) ⇒ natInf ⇒ 'a stream"
where
 "infU_get_prefix_plus s n 
  ≡ 
  case n of (Fin i) ⇒ FinU (infU_get_prefix s i) 
           | ∞     ⇒ InfU s"

― ‹taking the prefix of n data elements from an infinite stream›
― ‹(defined over natural numbers enriched by Infinity)›
definition
  take_plus :: "natInf ⇒ 'a list ⇒ 'a list"
where
 "take_plus n s 
  ≡ 
  case n of (Fin i) ⇒ (take i s) 
           | ∞      ⇒ s"

― ‹taking the prefix of n data elements from a (general) stream›
― ‹(defined over natural numbers enriched by Infinity)›
definition 
   get_prefix :: "'a stream ⇒ natInf ⇒ 'a stream"
where
   "get_prefix s k ≡ 
        case s of  (FinT x) ⇒ FinT (fin_get_prefix_plus x k)
                 | (FinU x) ⇒ FinU (take_plus k x)
                 | (InfT x) ⇒ infT_get_prefix_plus x k
                 | (InfU x) ⇒ infU_get_prefix_plus x k"

― ‹merging time intervals of two finite timed streams›
primrec
   fin_merge_ti :: "'a fstream ⇒ 'a fstream ⇒ 'a fstream"
where
 "fin_merge_ti [] y = y" |
 "fin_merge_ti (x#xs) y = 
    ( case y of [] ⇒ (x#xs)
         | (z#zs) ⇒ (x@z) # (fin_merge_ti xs zs))"

― ‹merging time intervals of two infinite timed streams›
definition
 inf_merge_ti :: "'a istream ⇒ 'a istream ⇒ 'a istream"
where
 "inf_merge_ti x y 
  ≡ 
  λ i. (x i)@(y i)"

― ‹the last time interval of a finite timed stream›
primrec
  fin_last_ti :: "('a list) list ⇒ nat ⇒ 'a list"
where   
 "fin_last_ti s 0 = hd s" |
 "fin_last_ti s (Suc i) = 
     ( if s!(Suc i) ≠ []
       then s!(Suc i) 
       else fin_last_ti s i)"

― ‹the last nonempty time interval of a finite timed stream›
― ‹(can be applied to the streams which time intervals are empty from some moment)›
primrec
  inf_last_ti :: "'a istream ⇒ nat ⇒ 'a list"
where  
 "inf_last_ti s 0 = s 0" |
 "inf_last_ti s (Suc i) = 
     ( if s (Suc i) ≠ []
       then s (Suc i) 
       else inf_last_ti s i)"


subsection ‹Properties of operators›

lemma inf_last_ti_nonempty_k:
  assumes "inf_last_ti dt t ≠ []"
  shows    "inf_last_ti dt (t + k) ≠ []"
using assms  
by (induct k, auto)

lemma inf_last_ti_nonempty:
  assumes "s t ≠ []"
  shows    "inf_last_ti s (t + k) ≠ []"
using assms  
by (induct k, auto, induct t, auto)

lemma arith_sum_t2k:
"t + 2 + k = (Suc t) + (Suc k)" 
by arith 

lemma inf_last_ti_Suc2:
  assumes "dt (Suc t) ≠ [] ∨ dt (Suc (Suc t)) ≠ []"
  shows    "inf_last_ti dt (t + 2 + k) ≠ []"
proof (cases "dt (Suc t) ≠ []")
  assume a1:"dt (Suc t) ≠ []"
  from a1 have sg2:"inf_last_ti dt ((Suc t) + (Suc k)) ≠ []" 
    by (rule inf_last_ti_nonempty)
  from sg2 show ?thesis by (simp add: arith_sum_t2k) 
next
  assume a2:"¬ dt (Suc t) ≠ []"
  from a2 and assms have sg1:"dt (Suc (Suc t)) ≠ []" by simp
  from sg1 have sg2:"inf_last_ti dt (Suc (Suc t) + k) ≠ []" 
    by (rule inf_last_ti_nonempty)
  from sg2 show ?thesis by auto
qed


subsubsection ‹Lemmas for concatenation operator›

lemma fin_length_append:
  "fin_length (x@y) = (fin_length x) + (fin_length y)"
by (induct x, auto)

lemma fin_append_Nil:  "fin_inf_append [] z = z"
by (simp add: fin_inf_append_def)

lemma correct_fin_inf_append1:
  assumes "s1 = fin_inf_append [x] s"
  shows    "s1 (Suc i) = s i"
using assms  
by (simp add: fin_inf_append_def)

lemma correct_fin_inf_append2:
  "fin_inf_append [x] s (Suc i) = s i"
by (simp add: fin_inf_append_def)

lemma fin_append_com_Nil1:
  "fin_inf_append [] (fin_inf_append y z) 
   = fin_inf_append ([] @ y) z"
by (simp add: fin_append_Nil)

lemma fin_append_com_Nil2:
  "fin_inf_append x (fin_inf_append [] z) 
  = fin_inf_append (x @ []) z"
by (simp add: fin_append_Nil)

lemma fin_append_com_i:
  "fin_inf_append x (fin_inf_append y z) i = fin_inf_append (x @ y) z i "
proof (cases x)
  assume Nil:"x = []"
  thus ?thesis by (simp add: fin_append_com_Nil1)
next
  fix a l assume Cons:"x = a # l"
  thus ?thesis
  proof (cases y)
    assume "y = []"
    thus ?thesis by (simp add: fin_append_com_Nil2)
  next
    fix aa la assume Cons2:"y = aa # la"
    show ?thesis 
    apply (simp add: fin_inf_append_def, auto, simp add: list_nth_append0)
    by (simp add: nth_append)
  qed
qed


subsubsection ‹Lemmas for operators $ts$ and $msg$›

lemma ts_msg1:
  assumes "ts p"
  shows    "msg 1 p"
using assms 
by (simp add: ts_def msg_def)

lemma ts_inf_tl:
  assumes "ts x"
  shows    "ts (inf_tl x)"
using assms  
by (simp add: ts_def inf_tl_def)

lemma ts_length_hint1:
 assumes "ts x"
 shows    "x i ≠ []"
proof - 
  from assms have sg1:"length (x i) = Suc 0"  by (simp add: ts_def)
  thus ?thesis by auto
qed

lemma ts_length_hint2:
 assumes "ts x"
 shows    "length (x i) = Suc (0::nat)"
using assms
by (simp add: ts_def)

lemma ts_Least_0:
  assumes "ts x"
  shows    "(LEAST i. (x i) ≠ [] ) = (0::nat)"
proof - 
  from assms have sg1:"x 0 ≠ []" by (rule ts_length_hint1)
  thus ?thesis 
  apply (simp add: Least_def)
  by auto
qed

lemma inf_tl_Suc: "inf_tl x i = x (Suc i)"
by (simp add: inf_tl_def) 

lemma ts_Least_Suc0:
  assumes "ts x"
  shows    "(LEAST i. x (Suc i) ≠ []) = 0"
proof -
  from assms have "x (Suc 0) ≠ []" by (simp add: ts_length_hint1)
  thus ?thesis by (simp add: Least_def, auto)
qed

lemma ts_inf_make_untimed_inf_tl:
  assumes "ts x"
  shows     "inf_make_untimed (inf_tl x) i = inf_make_untimed x (Suc i)"
using assms
apply (simp add: inf_make_untimed_def)
by (metis Suc_less_eq gr_implies_not0 ts_length_hint1 ts_length_hint2) 

lemma ts_inf_make_untimed1_inf_tl:
  assumes "ts x"
  shows    "inf_make_untimed1 (inf_tl x) i = inf_make_untimed1 x (Suc i)"
using assms
by (metis inf_make_untimed_def ts_inf_make_untimed_inf_tl)

lemma msg_nonempty1:
  assumes h1:"msg (Suc 0) a" 
         and h2:"a t = aa # l"
  shows "l = []"
proof - 
  from h1 have "length (a t) ≤ Suc 0" by (simp add: msg_def)
  from h2 and this show ?thesis by auto
qed

lemma msg_nonempty2:
  assumes h1:"msg (Suc 0) a" 
         and h2:"a t  ≠ []"
  shows "length (a t) = (Suc 0)"
proof - 
  from h1 have sg1:"length (a t) ≤ Suc 0" by (simp add: msg_def)
  from h2 have sg2:"length (a t) ≠ 0" by auto
  from sg1 and sg2 show ?thesis by arith 
qed


subsubsection ‹Lemmas for $inf\_truncate$›

lemma inf_truncate_nonempty:
  assumes "z i ≠ []"
  shows    "inf_truncate z i ≠ []"
proof (induct i)
    case 0
    from assms  show ?case by auto
  next
    case (Suc i)
     from assms show ?case by auto
qed


lemma concat_inf_truncate_nonempty:
  assumes  "z i ≠ []"
  shows      "concat (inf_truncate z i) ≠ []"
using assms
proof (induct i)
    case 0
    thus ?case by auto
  next
    case (Suc i)
    thus ?case by auto
qed
  
lemma concat_inf_truncate_nonempty_a:
  assumes "z i = [a]" 
  shows    "concat (inf_truncate z i) ≠ []"
using assms
by (metis concat_inf_truncate_nonempty list.distinct(1))

lemma concat_inf_truncate_nonempty_el:
  assumes "z i ≠ []" 
  shows    "concat (inf_truncate z i) ≠ []"
using assms
by (metis concat_inf_truncate_nonempty)

lemma inf_truncate_append:
  "(inf_truncate z i @ [z (Suc i)]) = inf_truncate z (Suc i)"
by (metis inf_truncate.simps(2))


subsubsection ‹Lemmas for $fin\_make\_untimed$› 

lemma fin_make_untimed_append:
  assumes "fin_make_untimed x ≠ []"
  shows    "fin_make_untimed (x @ y) ≠ []"
using assms by (simp add: fin_make_untimed_def)


lemma fin_make_untimed_inf_truncate_Nonempty:
  assumes "z k ≠ []"
         and "k ≤ i"
  shows "fin_make_untimed (inf_truncate z i) ≠ []"
using assms
  apply (simp add: fin_make_untimed_def)
  proof (induct i)
    case 0
    thus ?case  by auto
  next
    case (Suc i)
    thus ?case 
    proof cases
      assume "k ≤ i"
      from Suc and this show "∃xs∈set (inf_truncate z (Suc i)). xs ≠ []"
        by auto
    next
      assume "¬ k ≤ i"
      from Suc and this have "k = Suc i" by arith
      from Suc and this show "∃xs∈set (inf_truncate z (Suc i)). xs ≠ []"
        by auto
     qed
qed

lemma last_fin_make_untimed_append:
  "last (fin_make_untimed (z @ [[a]])) = a"
by (simp add: fin_make_untimed_def)

lemma last_fin_make_untimed_inf_truncate:
  assumes "z i = [a]"
  shows    "last (fin_make_untimed (inf_truncate z i)) = a"
using assms
proof (induction i)
   case 0  thus ?case by (simp add: fin_make_untimed_def)
next
   case (Suc i)  thus ?case by (simp add: fin_make_untimed_def)
qed

lemma fin_make_untimed_append_empty:
  "fin_make_untimed (z @ [[]]) = fin_make_untimed z"
by (simp add: fin_make_untimed_def)

lemma fin_make_untimed_inf_truncate_append_a:
  "fin_make_untimed (inf_truncate z i @ [[a]]) ! 
  (length (fin_make_untimed (inf_truncate z i @ [[a]])) - Suc 0) = a"
by (simp add: fin_make_untimed_def)

lemma fin_make_untimed_inf_truncate_Nonempty_all:
  assumes "z k ≠ []" 
  shows    "∀ i. k ≤ i ⟶ fin_make_untimed (inf_truncate z i) ≠ []"
using assms by (simp add:  fin_make_untimed_inf_truncate_Nonempty)

lemma fin_make_untimed_inf_truncate_Nonempty_all0:
  assumes "z 0 ≠ []"
  shows    "∀ i. fin_make_untimed (inf_truncate z i) ≠ []"
using assms by (simp add: fin_make_untimed_inf_truncate_Nonempty)

lemma fin_make_untimed_inf_truncate_Nonempty_all0a:
  assumes "z 0 = [a]"
  shows    "∀ i. fin_make_untimed (inf_truncate z i) ≠ []"
using assms by (simp add: fin_make_untimed_inf_truncate_Nonempty_all0)

lemma fin_make_untimed_inf_truncate_Nonempty_all_app:
  assumes "z 0 = [a]" 
  shows    "∀ i. fin_make_untimed (inf_truncate z i @ [z (Suc i)]) ≠ []"
proof 
  fix i
  from assms have "fin_make_untimed (inf_truncate z i) ≠ []"
    by (simp add: fin_make_untimed_inf_truncate_Nonempty_all0a)
  from assms and this show 
    "fin_make_untimed (inf_truncate z i @ [z (Suc i)]) ≠ []"
    by (simp add: fin_make_untimed_append)
qed

lemma fin_make_untimed_nth_length:
  assumes "z i = [a]"
  shows 
  "fin_make_untimed (inf_truncate z i) ! 
     (length (fin_make_untimed (inf_truncate z i)) - Suc 0)
    = a"
proof - 
from assms have sg1:"last (fin_make_untimed (inf_truncate z i)) = a"
  by (simp add: last_fin_make_untimed_inf_truncate)
from assms have sg2:"concat (inf_truncate z i) ≠ []"
  by (rule concat_inf_truncate_nonempty_a)
from assms and sg1 and sg2 show ?thesis 
  by (simp add: fin_make_untimed_def last_nth_length)
qed


subsubsection ‹Lemmas for $inf\_disj$ and $inf\_disjS$› 

lemma inf_disj_index:
  assumes h1:"inf_disj n nS"
         and "nS k t ≠ []"
         and "k < n"
  shows  "(SOME i. i < n ∧  nS i t ≠ []) = k"
proof - 
  from h1 have "∀ j. k < n ∧ j < n ∧ k ≠ j ∧ nS k t ≠ [] ⟶ nS j t = []"
    by (simp add: inf_disj_def, auto)
  from this and assms show ?thesis by auto
qed
 
lemma inf_disjS_index:
  assumes h1:"inf_disjS IdSet nS"
      and "k:IdSet"
      and "nS k t ≠ []"
  shows "(SOME i. (i:IdSet) ∧ nSend i t ≠ []) = k"
proof -
  from h1 have "∀ j. k ∈ IdSet ∧ j ∈ IdSet ∧ nS k t ≠ [] ⟶ nS j t = []"
    by (simp add: inf_disjS_def, auto)
  from this and assms show ?thesis by auto
qed

end