From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Sat, 20 Jun 2009 16:53:44 +0000 (+0000)
Subject: Some notation and additional lemmata.
X-Git-Tag: make_still_working~3830
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fe63c5efb416a23ee43ea61ee47fa8f4e3f99c52;p=helm.git

Some notation and additional lemmata.
---

diff --git a/helm/software/matita/library/list/in.ma b/helm/software/matita/library/list/in.ma
index 310c3f369..3285fef2e 100644
--- a/helm/software/matita/library/list/in.ma
+++ b/helm/software/matita/library/list/in.ma
@@ -23,6 +23,13 @@ inductive in_list (A:Type): A → (list A) → Prop ≝
 definition incl : \forall A.(list A) \to (list A) \to Prop \def
   \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
   
+notation "hvbox(a break ∉ b)" non associative with precedence 45
+for @{ 'notmem $a $b }. 
+  
+interpretation "list member" 'mem x l = (in_list ? x l).
+interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
+interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
+  
 lemma not_in_list_nil : \forall A,x.\lnot in_list A x [].
 intros.unfold.intro.inversion H
   [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
@@ -164,4 +171,5 @@ qed.
 
 lemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
 unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
-qed.
\ No newline at end of file
+qed.
+
diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index 19866cc29..077e1af6c 100644
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -195,3 +195,9 @@ intros;elim l
      [simplify;apply le_S_S;assumption
      |simplify;apply le_S;assumption]]
 qed.
+
+lemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
+intros;elim l
+[reflexivity
+|simplify;rewrite < H;reflexivity]
+qed.