- "re": a part of reb.ma commented out since it cannot compile

diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma
index 9f40045aee9b6b923e0c911078066c5f8b6d0ef8..378a3a76298b9422ab4c8cfa04c88023068ef9e8 100644 (file)
--- a/matita/matita/lib/re/lang.ma
+++ b/matita/matita/lib/re/lang.ma
@@ -30,9 +30,6 @@ definition cat : ∀S,l1,l2,w.Prop ≝
 notation "a · b" non associative with precedence 65 for @{ 'middot $a $b}.
 interpretation "cat lang" 'middot a b = (cat ? a b).
 
-let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ 
-match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
-
 let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
 match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ]. 
 
@@ -89,7 +86,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/
 qed.
 
 lemma fix_star: ∀S.∀A:word S → Prop. 
@@ -98,7 +95,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/
   |* [2: whd in ⊢ (%→?); #eqw <eqw //]
    * #w1 * #w2 * * #eqw <eqw @cat_to_star 
   ]

diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma
index af0e921a6b9a1be5cbabe311860e2fb8d7d09c8b..234d522ae176dde98579f39ac9e6ac09bb11aa32 100644 (file)
--- a/matita/matita/lib/re/re.ma
+++ b/matita/matita/lib/re/re.ma
@@ -128,8 +128,7 @@ let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
   | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
   | pk E ⇒ (forget ? E)^* ].
  
-(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
-interpretation "forget" 'norm a = (forget ? a).
+interpretation "forget" 'card a = (forget ? a).
 
 lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
 // qed.

diff --git a/matita/matita/lib/re/reb.ma b/matita/matita/lib/re/reb.ma
index f4cd2e6c163cb007334f0a3c061fa1673364e2ce..73faed3770c6417cacc6eea1089fcc6fb1007b36 100644 (file)
--- a/matita/matita/lib/re/reb.ma
+++ b/matita/matita/lib/re/reb.ma
@@ -86,6 +86,8 @@ definition cat : ∀S,l1,l2,w.Prop ≝
   λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
 interpretation "cat lang" 'pc a b = (cat ? a b).
 
+(* BEGIN HERE 
+
 definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. 
 interpretation "star lang" 'pk l = (star ? l).
 
@@ -776,3 +778,4 @@ ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e.
      | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
 ##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;
 
+*)
\ No newline at end of file