From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 9 Nov 2011 09:34:13 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~2126
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8421cc771e2a316e028b6dab25bdacb8f8cd6c2b;p=helm.git

commit by user andrea
---

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 21a7a6c0e..77e42066e 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -158,18 +158,23 @@ match r with
 interpretation "in_pl" 'in_l E = (in_pl ? E).
 interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
 
-definition epsilon ≝ λS,b.if b then { ([ ] : word S) } else {}.
+definition eps: ∀S:a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"bool/a → a href="cic:/matita/tutorial/chapter4/word.def(3)"word/a S → Prop 
+  ≝ λS,b. a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? b a title="sing lang" href="cic:/fakeuri.def(1)"{/a: a title="nil" href="cic:/fakeuri.def(1)"[/a] } a title="empty lang" href="cic:/fakeuri.def(1)"∅/a.
 
-interpretation "epsilon" 'epsilon = (epsilon ?).
-notation < "ϵ b" non associative with precedence 90 for @{'app_epsilon $b}.
-interpretation "epsilon lang" 'app_epsilon b = (epsilon ? b).
+(* interpretation "epsilon" 'epsilon = (epsilon ?). *)
+notation "ϵ _ b" non associative with precedence 90 for @{'app_epsilon $b}.
+interpretation "epsilon lang" 'app_epsilon b = (eps ? b).
 
-ndefinition in_prl ≝ λS : Alpha.λp:pre S.  𝐋\p (\fst p) ∪ ϵ (\snd p).
+definition in_prl ≝ λS : a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.λp:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S.  a title="in_pl" href="cic:/fakeuri.def(1)"ℓ/a (a title="fst" href="cic:/fakeuri.def(1)"\fst/a p) a title="union lang" href="cic:/fakeuri.def(1)"∪/a a title="epsilon lang" href="cic:/fakeuri.def(1)"ϵ/a_(a title="snd" href="cic:/fakeuri.def(1)"\snd/a p).
   
 interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
-interpretation "in_prl" 'in_pl E = (in_prl ? E).
+interpretation "in_prl" 'in_l E = (in_prl ? E).
+
+lemma not_epsilon_lp :∀S.∀pi:a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S. a title="logical not" href="cic:/fakeuri.def(1)"¬/a ((a title="in_pl" href="cic:/fakeuri.def(1)"ℓ/a pi) a title="nil" href="cic:/fakeuri.def(1)"[/a]).
+#S #pi (elim pi) normalize /2/
+  [#pi1 #pi2 #H1 #H2 % * /2/ * #w1 * #w2 * * /2/;
 
-nlemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ].
+lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ].
 #S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct; nqed.
 
 (* lemma 12 *)
@@ -192,4 +197,6 @@ nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ((𝐋\p e) [ ]).
     nrewrite > (append_eq_nil …H…); /2/;##]
 nqed.
 
-ndefinition lo ≝ λS:Alpha.λ
\ No newline at end of file
+ndefinition lo ≝ λS:Alpha.λ
+
+