X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Ftutorial%2Fchapter6.ma;h=364ad35de8271523d3dc94b0bfb55548f6caadae;hb=3a9c3c16e7c7e3a35640a0afa53f044a4f87ed65;hp=150b07b76f62099d9b3c7a66de6acb7c44454480;hpb=770ba48ba232d7f1782629c572820a0f1bfe4fde;p=helm.git

diff --git a/matita/matita/lib/tutorial/chapter6.ma b/matita/matita/lib/tutorial/chapter6.ma
index 150b07b76..364ad35de 100644
--- a/matita/matita/lib/tutorial/chapter6.ma
+++ b/matita/matita/lib/tutorial/chapter6.ma
@@ -35,8 +35,9 @@ derivative of a language A w.r.t. a given character a. *)
 
 definition cat : ∀S,l1,l2,w.Prop ≝ 
   λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
-
+(*
 notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
+*)
 interpretation "cat lang" 'middot a b = (cat ? a b).
 
 
@@ -47,8 +48,10 @@ 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. *)
 
+(* Already in the library
 let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ 
 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
+*)
 
 (* Given a list of words l and a language r, (conjunct l r) is true if and only if
 all words in l are in r, that is for every w in l, r w holds. *)
@@ -60,6 +63,7 @@ match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ].
 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:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. 
 notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
 interpretation "star lang" 'star l = (star ? l).
@@ -154,7 +158,7 @@ qed.
 lemma cat_to_star:∀S.∀A:word S → Prop.
   ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
 #S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l)) 
-% normalize /2/
+% normalize destruct /2/ (* destruct added *)
 qed.
 
 lemma fix_star: ∀S.∀A:word S → Prop. 
@@ -163,7 +167,7 @@ lemma fix_star: ∀S.∀A:word S → Prop.
   [* #l generalize in match w; -w cases l [normalize #w * /2/]
    #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
    #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
-   % /2/ whd @(ex_intro … tl) /2/
+   % destruct /2/ whd @(ex_intro … tl) /2/ (* destruct added *)
   |* [2: whd in ⊢ (%→?); #eqw <eqw //]
    * #w1 * #w2 * * #eqw <eqw @cat_to_star 
   ]
@@ -190,4 +194,4 @@ lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
   A^* ∪ {ϵ} =1 A^*.
 #S #A #w % /2/ * // 
 qed.
-  
\ No newline at end of file
+