commit by user andrea

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 21a7a6c0ef80bf29230209b9ca91986666b13f67..77e42066e2fc65801c5de91e505aac57ebda1dc5 100644 (file)
--- 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:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop 
+  ≝ λS,b. \ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? b \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] } \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6.
 
-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 : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.λp:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S.  \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 (\ 5a title="fst" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p) \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="epsilon lang" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6_(\ 5a title="snd" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 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:\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 ((\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 pi) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]).
+#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.λ
+
+