commit by user andrea

diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma
index 1a8b65aa35885a4ce7bfac32c1c9b9ca652f8a6d..679331198007d38a8d2734f08042587480be18de 100644 (file)
--- a/weblib/tutorial/chapter6.ma
+++ b/weblib/tutorial/chapter6.ma
@@ -1,10 +1,12 @@
-include "tutorial/chapter5.ma".
-
-(* In this chapter we shall apply our notion of DeqSet, and the list operations 
+(*
+\ 5h1 class="section"\ 6Formal Languages\ 5/h1\ 6
+In this chapter we shall apply our notion of DeqSet, and the list operations 
 defined in Chapter 4 to formal languages. A formal language is an arbitrary set
 of words over a given alphabet, that we shall represent as a predicate over words. 
-A word (or string) over an alphabet S is just a list of elements of S. *) 
+*)
+include "tutorial/chapter5.ma".
 
+(* A word (or string) over an alphabet S is just a list of elements of S.*)
 definition word ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6\ 5/span\ 6 S.
 
 (* For any alphabet there is only one word of length 0, the \ 5i\ 6empty word\ 5/i\ 6, which is 
@@ -19,7 +21,10 @@ String concatenation is just the append operation over lists, hence there is no
 point to define it. Similarly, many of its properties, such as the fact that 
 concatenating a word with the empty word gives the original word, follow by 
 general results over lists.
+*)
 
+(*
+\ 5h2 class="section"\ 6Operations over languages\ 5/h2\ 6
 Languages inherit all the basic operations for sets, namely union, intersection, 
 complementation, substraction, and so on. In addition, we may define some new 
 operations induced by string concatenation, and in particular the concatenation 
@@ -32,7 +37,13 @@ definition cat : ∀S,l1,l2,w.Prop ≝
 notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
 interpretation "cat lang" 'middot a b = (cat ? a b).
 
-(* Given a list of words, the flatten operation concatenates them all. *)
+
+(* Given a language l, the Kleene's star of l, denoted by l*, is the set of 
+finite-length strings that can be generated by concatenating arbitrary strings of 
+l. In other words, w belongs to l* is and only if there exists a list of strings 
+w1,w2,...wk all belonging to l, such that l = w1w2...wk. 
+We need to define the latter operations. The following flatten function takes in 
+input a list of words and concatenates them together. *)
 
 let rec flatten (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (l : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S)) on l : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S ≝ 
 match l with [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] | cons w tl ⇒ w \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 flatten ? tl ].
@@ -43,16 +54,22 @@ all words in l are in r, that is for every w in l, r w holds. *)
 let rec conjunct (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (l : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6\ 5/span\ 6 (\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S)) (r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop) on l: Prop ≝
 match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons w tl ⇒ r w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 conjunct ? tl r ]. 
 
-(* Given a language l, the kleene's star of l, denoted by l*, is the set of 
-finite-length strings that can be generated by concatenating arbitrary strings of 
-l. In other words, w belongs to l* is and only if there exists a list of strings 
-lw all belonging to l, such that l = flatten lw. *)
+(* We are ready to give the formal definition of the Kleene's star of l:
+a word w belongs to l* is and only if there exists a list of strings 
+lw such that (conjunct lw l) and  l = flatten lw. *)
 
 definition star ≝ λS.λl.λw:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6lw.\ 5a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 ? lw \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter6/conjunct.fix(0,1,4)"\ 6conjunct\ 5/a\ 6 ? lw l. 
 notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
 interpretation "star lang" 'star l = (star ? l).
 
-(* Equality between languages is just the usual extensional equality between
+(* The derivative of a language A with respect to a character a is the set of
+all strings w such that aw is in A. *)
+
+definition deriv ≝ λS.λA:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.λa,w. A (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w).
+
+(* 
+\ 5h2 class="section"\ 6Language equalities\ 5/h2\ 6
+Equality between languages is just the usual extensional equality between
 sets. The operation of concatenation behaves well with respect to this equality. *)
 
 lemma cat_ext_l: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop. 
@@ -106,10 +123,7 @@ lemma distr_cat_r_eps: ∀S.∀A,C:\ 5a href="cic:/matita/tutorial/chapter6/word.d
   #S #A #C @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6 |@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter6/epsilon_cat_l.def(5)"\ 6epsilon_cat_l\ 5/a\ 6]
 qed.
 
-(* The derivative of a language A with respect to a character a is the set of
-all strings w such that aw is in A. *)
-
-definition deriv ≝ λS.λA:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.λa,w. A (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w).
+(* The following is a major property of derivatives *)
 
 lemma deriv_middot: ∀S,A,B,a. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter6/deriv.def(4)"\ 6deriv\ 5/a\ 6 S (A\ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6B) a \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (\ 5a href="cic:/matita/tutorial/chapter6/deriv.def(4)"\ 6deriv\ 5/a\ 6 S A a) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B.
 #S #A #B #a #noteps #w normalize %
@@ -123,8 +137,10 @@ lemma deriv_middot: ∀S,A,B,a. \ 5a title="logical not" href="cic:/fakeuri.def(1)
   ]
 qed. 
 
-(* We conclude this section with some important properties of Kleene's
-star that will be usde in the following chapters. *)
+(* 
+\ 5h2 class="section"\ 6Main Properties of Kleene's star\ 5/h2\ 6
+We conclude this section with some important properties of Kleene's
+star that will be used in the following chapters. *)
 
 lemma espilon_in_star: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
   A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6.