src/HOL/HOLCF/FOCUS/Fstreams.thy
changeset 41855 c3b6e69da386
parent 41476 0fa9629aa399
child 42151 4da4fc77664b
equal deleted inserted replaced
41854:b2b5b965b59c 41855:c3b6e69da386
    81 by (simp add: first_def)
    81 by (simp add: first_def)
    82 
    82 
    83 lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a"
    83 lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a"
    84 apply (simp add: jth_def, auto)
    84 apply (simp add: jth_def, auto)
    85 apply (simp add: i_th_def rt_sconc1)
    85 apply (simp add: i_th_def rt_sconc1)
    86 by (simp add: inat_defs split: inat_splits)
    86 by (simp add: inat_defs split: inat.splits)
    87 
    87 
    88 lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
    88 lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
    89 apply (simp add: last_def)
    89 apply (simp add: last_def)
    90 apply (simp add: inat_defs split:inat_splits)
    90 apply (simp add: inat_defs split:inat.splits)
    91 by (drule sym, auto)
    91 by (drule sym, auto)
    92 
    92 
    93 lemma last_fsingleton[simp]: "last (<a>) = a"
    93 lemma last_fsingleton[simp]: "last (<a>) = a"
    94 by (simp add: last_def)
    94 by (simp add: last_def)
    95 
    95 
   101 
   101 
   102 lemma last_infinite[simp]:"#s = Infty ==> last s = undefined"
   102 lemma last_infinite[simp]:"#s = Infty ==> last s = undefined"
   103 by (simp add: last_def)
   103 by (simp add: last_def)
   104 
   104 
   105 lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
   105 lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
   106 by (simp add: jth_def inat_defs split:inat_splits, auto)
   106 by (simp add: jth_def inat_defs split:inat.splits, auto)
   107 
   107 
   108 lemma jth_UU[simp]:"jth n UU = undefined" 
   108 lemma jth_UU[simp]:"jth n UU = undefined" 
   109 by (simp add: jth_def)
   109 by (simp add: jth_def)
   110 
   110 
   111 lemma ext_last:"[|s ~= UU; Fin (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s" 
   111 lemma ext_last:"[|s ~= UU; Fin (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s"