X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flists%2Flist.ma;h=c89bb78560b5ac1b1a9dbb061a372e85318afd9a;hb=f0d422b660e11886ec4f9a823da795050f07e07f;hp=021e9d400185f02f4d4983fb65fec37090dc7de5;hpb=a65c5b3337075672736b1583b8519ff14bb16976;p=helm.git

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 021e9d400..c89bb7856 100644
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -31,12 +31,12 @@ notation "hvbox(l1 break @ l2)"
 interpretation "nil" 'nil = (nil ?).
 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
-definition not_nil: ∀A:Type[0].list A → Prop ≝
+definition is_nil: ∀A:Type[0].list A → Prop ≝
  λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
 
 theorem nil_cons:
   ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
-  #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+  #A #l #a @nmk #Heq (change with (is_nil ? (a::l))) >Heq //
 qed.
 
 (*
@@ -55,6 +55,11 @@ definition hd ≝ λA.λl: list A.λd:A.
 
 definition tail ≝  λA.λl: list A.
   match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
+  
+definition option_hd ≝ 
+  λA.λl:list A. match l with
+  [ nil ⇒ None ?
+  | cons a _ ⇒ Some ? a ].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
@@ -162,14 +167,22 @@ let rec length (A:Type[0]) (l:list A) on l ≝
     [ nil ⇒ 0
     | cons a tl ⇒ S (length A tl)].
 
-notation "|M|" non associative with precedence 60 for @{'norm $M}.
+notation "|M|" non associative with precedence 65 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l // 
+qed.
+
 lemma length_append: ∀A.∀l1,l2:list A. 
   |l1@l2| = |l1|+|l2|.
 #A #l1 elim l1 // normalize /2/
 qed.
 
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
 (****************************** nth ********************************)
 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
   match n with