rtmap (platform-indepent multple relocation): application and composition

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / streams_hdtl.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
index bdc740c82ff42646cbd6fb362c6ac714fa731cf3..050568754f5edc111fb8ccf948c73fc5fb34cfac 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/notation/functions/drop_1.ma".
 include "ground_2/lib/streams.ma".
 include "ground_2/lib/arith.ma".
 
@@ -23,17 +24,16 @@ definition hd (A:Type[0]): stream A → A ≝
 definition tl (A:Type[0]): stream A → stream A ≝
               λt. match t with [ seq _ t ⇒ t ].
 
-let rec tln (A:Type[0]) (i:nat) on i: stream A → stream A ≝ ?.
-cases i -i [ #t @t | #i * #_ #t @(tln … i t) ]
-qed.
+interpretation "tail (streams)" 'Drop t = (tl ? t).
 
 (* basic properties *********************************************************)
 
-lemma eq_stream_split (A) (t): (hd … t) @ (tl … t) ≐⦋A⦌ t.
-#A * //
-qed.
+lemma hd_rew (A) (a) (t): a = hd A (a@t).
+// qed.
 
-lemma tln_eq_repl (A) (i): eq_stream_repl A (λt1,t2. tln … i t1 ≐ tln … i t2).
-#A #i elim i -i //
-#i #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq … H) /2 width=7 by/
+lemma tl_rew (A) (a) (t): t = tl A (a@t).
+// qed.
+
+lemma eq_stream_split (A) (t): (hd … t) @ ↓t ≐⦋A⦌ t.
+#A * //
 qed.