Some notation and additional lemmata.

[helm.git] / helm / software / matita / library / list / in.ma

diff --git a/helm/software/matita/library/list/in.ma b/helm/software/matita/library/list/in.ma
index cd372394bfcca4a3de87c1498648137a220b5d2c..3285fef2e0967f75a5bc601953eadba75bef148c 100644 (file)
--- 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
@@ -99,7 +106,7 @@ lemma mem_true_to_in_list :
   \forall x,l.mem A equ x l = true \to in_list A x l.
 intros 5.elim l
   [simplify in H1;destruct H1
-  |simplify in H2;apply (bool_elim ? (equ x t))
+  |simplify in H2;apply (bool_elim ? (equ x a))
      [intro;rewrite > (H ? ? H3);apply in_list_head
      |intro;rewrite > H3 in H2;simplify in H2;
       apply in_list_cons;apply H1;assumption]]
@@ -113,15 +120,14 @@ intros 5.elim l
   [elim (not_in_list_nil ? ? H1)
   |elim H2
     [simplify;rewrite > H;reflexivity
-    |simplify;rewrite > H4;apply (bool_elim ? (equ a a1));intro;rewrite > H5;
-     reflexivity]].
+    |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
 qed.
 
 lemma in_list_filter_to_p_true : \forall l,x,p.
 in_list nat x (filter nat l p) \to p x = true.
 intros 3;elim l
   [simplify in H;elim (not_in_list_nil ? ? H)
-  |simplify in H1;apply (bool_elim ? (p t));intro;rewrite > H2 in H1;
+  |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
    simplify in H1
      [elim (in_list_cons_case ? ? ? ? H1)
         [rewrite > H3;assumption
@@ -132,7 +138,7 @@ qed.
 lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
 intros 3;elim l
   [simplify in H;elim (not_in_list_nil ? ? H)
-  |simplify in H1;apply (bool_elim ? (p t));intro;rewrite > H2 in H1;
+  |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
    simplify in H1
      [elim (in_list_cons_case ? ? ? ? H1)
         [rewrite > H3;apply in_list_head
@@ -146,11 +152,24 @@ intros 3;elim l
   [elim (not_in_list_nil ? ? H)
   |elim (in_list_cons_case ? ? ? ? H1)
      [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
-     |simplify;apply (bool_elim ? (p t));intro;rewrite > H4;simplify
+     |simplify;apply (bool_elim ? (p a));intro;simplify;
         [apply in_list_cons;apply H;assumption
         |apply H;assumption]]]
 qed.
 
 lemma incl_A_A: ∀T,A.incl T A A.
 intros.unfold incl.intros.assumption.
-qed.
\ No newline at end of file
+qed.
+
+lemma incl_append_l : ∀T,A,B.incl T A (A @ B).
+unfold incl; intros;autobatch.
+qed.
+
+lemma incl_append_r : ∀T,A,B.incl T B (A @ B).
+unfold incl; intros;autobatch.
+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.
+