From f4b65ff26aaedeec8cd2a8d5ab79123173113a39 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 6 Mar 2012 11:37:20 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter8.ma | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) 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 * -- 2.39.2