commit by user andrea

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 6cb68782b99077fa38cb47f0ad02c9362981189b..27246556114db8b79129f2aa31a180ee0e948e35 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -84,8 +84,8 @@ match r with
  | star r1 ⇒ (in_l ? r1)\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* 
  ].
 
-notation "\sem{E}" non associative with precedence 75 for @{'in_l $E}.
-interpretation "in_l" 'in_l E = (in_l ? E).
+notation "\sem{E}" non associative with precedence 75 for @{'sem $E}.
+interpretation "in_l" 'sem E = (in_l ? E).
 interpretation "in_l mem" 'mem w l = (in_l ? l w).
 
 notation "a ∨ b" left associative with precedence 30 for @{'orb $a $b}.
@@ -137,55 +137,45 @@ let rec forget (S: \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alph
 notation "| e |" non associative with precedence 65 for @{'fmap $e}.
 interpretation "forget" 'fmap a = (forget ? a).
 
-lemma foo:∀a. 'fst a = 0. 
- 
-notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.  
-interpretation "fst" 'fst x = (fst ? ? x).  
-notation "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
-interpretation "snd" 'snd x = (snd ? ? x).
-
-(* notation "\sem{E}" non associative with precedence 75 for @{in_pl ? $E}. *)
-
-let rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝ 
+let rec in_pl (S : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝ 
 match r with
-  [ pzero ⇒ ∅ 
-  | pepsilon ⇒ ∅
-  | pchar _ ⇒ ∅
-  | ppoint x ⇒ {: x::[] } 
-  | pconcat pe1 pe2 ⇒ in_pl ? pe1 · \sem{|pe2|}  ∪ in_pl ? pe2 
-  | por pe1 pe2 ⇒ in_pl ? pe1 ∪ in_pl ? pe2
-  | pstar pe ⇒ in_pl ? pe · \sem{|pe|}^*
+  [ pzero ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6 
+  | pepsilon ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
+  | pchar _ ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
+  | ppoint x ⇒ \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] } 
+  | pconcat pe1 pe2 ⇒ in_pl ? pe1 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{|pe2|}  \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 in_pl ? pe2 
+  | por pe1 pe2 ⇒ in_pl ? pe1 \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 in_pl ? pe2
+  | pstar pe ⇒ in_pl ? pe \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{|pe|}\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
   ].
 
-interpretation "in_pl" 'in_l E = (in_pl ? E).
+interpretation "in_pl" 'sem E = (in_pl ? E).
 interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
 
-definition eps: ∀S:Alpha.bool → word S → Prop 
-  ≝ λS,b. if_then_else ? b {: [] } ∅.
+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)"\ 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 = (eps ? b).
 
-definition in_prl ≝ λS : Alpha.λp:pre S.  ℓ (\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\sem\ 5/a\ 6{\ 5a title="pair pi1" 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="pair pi2" 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_l E = (in_prl ? E).
-
-lemma not_epsilon_lp :∀S.∀pi:pitem S. ¬ ((ℓ pi) []).
-#S #pi (elim pi) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace nmk\ 5/span\ 6\ 5/span\ 6/
-  [#pi1 #pi2 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/ * #w1 * #w2 * * #appnil 
-   cases (nil_to_nil … appnil) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/
-  |#p11 #p12 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/
-  |#pi #H % * #w1 * #w2 * * #appnil (cases (nil_to_nil … appnil)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/
+interpretation "in_prl" 'sem 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\neg\ 5/a\ 6(\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="in_pl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 pi).
+#S #pi (elim pi) normalize /  \ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  [#pi1 #pi2 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * #w1 * #w2 * * #appnil 
+   cases (\ 5a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"\ 6nil_to_nil\ 5/a\ 6 … appnil) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  |#p11 #p12 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  |#pi #H % * #w1 * #w2 * * #appnil (cases (\ 5a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"\ 6nil_to_nil\ 5/a\ 6 … appnil)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
   ]
 qed.
 
-lemma if_true_epsilon: ∀S.∀e:pre S. \snd e = true → ((ℓ e) []).
+lemma if_true_epsilon: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → (\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e).
 #S #e #H %2 >H // qed.
 
-lemma if_epsilon_true : ∀S.∀e:pre S. [ ] ∈ e → \snd e = true.
-#S * #pi #b * [normalize #abs @False_ind /2/] cases b normalize // @False_ind
+lemma if_epsilon_true : ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e → \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#S * #pi #b * [normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] cases b normalize // @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
 qed.
 
 definition lor ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.