1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/notation/functions/drops_2.ma".
16 include "ground_2/lib/streams_hdtl.ma".
18 (* STREAMS ******************************************************************)
20 rec definition tls (A:Type[0]) (n:nat) on n: stream A → stream A ≝ ?.
21 cases n -n [ #t @t | #n #t @tl @(tls … n t) ]
24 interpretation "recursive tail (strams)" 'Drops n f = (tls ? n f).
26 (* basic properties *********************************************************)
28 lemma tls_rew_O (A) (t): t = tls A 0 t.
31 lemma tls_rew_S (A) (n) (t): ↓↓*[n]t = tls A (⫯n) t.
34 lemma tls_S1 (A) (n) (t): ↓*[n]↓t = tls A (⫯n) t.
38 lemma tls_eq_repl (A) (n): eq_stream_repl A (λt1,t2. ↓*[n] t1 ≐ ↓*[n] t2).
40 #n #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq … H) /2 width=7 by/