commit by user andrea

diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma
index 31acc919e7f14cdb1806214a2053dc946a34d225..8e62c13441b1731633a170832b6a21ee54b6bb72 100644 (file)
--- a/weblib/tutorial/chapter8.ma
+++ b/weblib/tutorial/chapter8.ma
@@ -233,7 +233,12 @@ qed.
 
 (*
 \ 5h2\ 6Blank item\ 5/h2\ 6 
-*)
+
+As a corollary of theorem sem_bullet, given a regular expression e, we can easily 
+find an item with the same semantics of $e$: it is enough to get an item (blank e) 
+having e as carrier and no point, and then broadcast a point in it. The semantics of
+(blank e) is obviously the empty language: from the point of view of the automaton,
+it corresponds with the pit state. *)
 
 let rec blank (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (i: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on i :\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S ≝
  match i with
@@ -273,7 +278,9 @@ qed.
 
 (*
 \ 5h2\ 6Lifted Operators\ 5/h2\ 6 
-*)
+
+Plus and bullet have been already lifted from items to pres. We can now 
+do a similar job for concatenation ⊙ and Kleene's star ⊛.*)
 
 definition lifted_cat ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
   \ 5a href="cic:/matita/tutorial/chapter8/lift.def(2)"\ 6lift\ 5/a\ 6 S (\ 5a href="cic:/matita/tutorial/chapter8/pre_concat_l.def(3)"\ 6pre_concat_l\ 5/a\ 6 S \ 5a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"\ 6eclose\ 5/a\ 6 e).
@@ -297,6 +304,8 @@ lemma erase_odot:∀S.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)
 #S * #i1 * * #i2 #b2 // >\ 5a href="cic:/matita/tutorial/chapter8/odot_true_b.def(6)"\ 6odot_true_b\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/erase_dot.def(4)"\ 6erase_dot\ 5/a\ 6 //  
 qed.
 
+(* Let us come to the star operation: *)
+
 definition lk ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
   match e with 
   [ mk_Prod i1 b1 ⇒
@@ -310,7 +319,6 @@ definition lk ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6
 interpretation "lk" 'lk a = (lk ? a).
 notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
 
-
 lemma ostar_true: ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
   \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛ \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i))\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*, \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉.
 // qed.
@@ -341,6 +349,9 @@ cut (e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair
 cases (e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i) #i1 #b1 cases b1 #H @H
 qed.
 
+(* We conclude this section with the proof of the main semantic properties
+of ⊙ and ⊛.)
+
 lemma sem_odot: 
   ∀S.∀e1,e2: \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 e2} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1}\ 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{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e2|} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2}.
 #S #e1 * #i2 *