From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Mar 2012 11:37:20 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1910
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f4b65ff26aaedeec8cd2a8d5ab79123173113a39;p=helm.git

commit by user andrea
---

diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma
index 31acc919e..8e62c1344 100644
--- a/weblib/tutorial/chapter8.ma
+++ b/weblib/tutorial/chapter8.ma
@@ -233,7 +233,12 @@ qed.
 
 (*
 h2Blank item/h2 
-*)
+
+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: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (i: a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on i :a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S ≝
  match i with
@@ -273,7 +278,9 @@ qed.
 
 (*
 h2Lifted Operators/h2 
-*)
+
+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:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. 
   a href="cic:/matita/tutorial/chapter8/lift.def(2)"lift/a S (a href="cic:/matita/tutorial/chapter8/pre_concat_l.def(3)"pre_concat_l/a S a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"eclose/a e).
@@ -297,6 +304,8 @@ lemma erase_odot:∀S.∀e1,e2:a href="cic:/matita/tutorial/chapter7/pre.def(1)
 #S * #i1 * * #i2 #b2 // >a href="cic:/matita/tutorial/chapter8/odot_true_b.def(6)"odot_true_b/a >a href="cic:/matita/tutorial/chapter7/erase_dot.def(4)"erase_dot/a //  
 qed.
 
+(* Let us come to the star operation: *)
+
 definition lk ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.
   match e with 
   [ mk_Prod i1 b1 ⇒
@@ -310,7 +319,6 @@ definition lk ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
 interpretation "lk" 'lk a = (lk ? a).
 notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
 
-
 lemma ostar_true: ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
   a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉a title="lk" href="cic:/fakeuri.def(1)"^/a⊛ a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*, a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉.
 // qed.
@@ -341,6 +349,9 @@ cut (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair
 cases (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a 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: a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a e2} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1}a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2}.
 #S #e1 * #i2 *