X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fre%2Flang.ma;h=17269392499df454725ef7597ff781d175534d72;hb=b2290acc0159c6ef4ccb1f628e3b649413fad87b;hp=a0a5a938d1785d58bf1422016caad88e5089c7f7;hpb=5c71d6a1d1461007f941f73d2cc7975c7116fd0d;p=helm.git

diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma
index a0a5a938d..172693924 100644
--- a/matita/matita/lib/re/lang.ma
+++ b/matita/matita/lib/re/lang.ma
@@ -17,6 +17,7 @@
 include "arithmetics/nat.ma".
 include "basics/lists/list.ma".
 include "basics/sets.ma".
+include "basics/deqsets.ma".
 
 definition word ≝ λS:DeqSet.list S.
 
@@ -52,12 +53,34 @@ lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop.
 cases (H w2) /6/ 
 qed.
   
+lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅.
+#S #A #w % [|*] * #w1 * #w2 * * #_ *
+qed.
+
 lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
   (A ∪ B) · C =1  A · C ∪ B · C. 
 #S #A #B #C #w %
   [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/] 
 qed.
 
+(* derivative *)
+
+definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w).
+
+lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ → 
+  deriv S (A·B) a =1 (deriv S A a) · B.
+#S #A #B #a #noteps #w normalize %
+  [* #w1 cases w1 
+    [* #w2 * * #_ #Aeps @False_ind /2/
+    |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct
+     #H #H1 @(ex_intro … w2) @(ex_intro … w3) % // % //
+    ]
+  |* #w1 * #w2 * * #H #H1 #H2 @(ex_intro … (a::w1))
+   @(ex_intro … w2) % // % normalize //
+  ]
+qed. 
+
+(* star properties *)
 lemma espilon_in_star: ∀S.∀A:word S → Prop.
   A^* ϵ.
 #S #A @(ex_intro … [ ]) normalize /2/