From: Enrico Tassi Date: Thu, 16 Sep 2010 21:28:13 +0000 (+0000) Subject: fixed notation X-Git-Tag: make_still_working~2830 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5624f8c904d539d889e4047c7a1358fd62339ac0;p=helm.git fixed notation --- diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma index c66c73791..40947401f 100644 --- a/helm/software/matita/nlibrary/re/re.ma +++ b/helm/software/matita/nlibrary/re/re.ma @@ -81,7 +81,7 @@ interpretation "cat lang" 'pc a b = (cat ? a b). ndefinition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. interpretation "star lang" 'pk l = (star ? l). -notation > "𝐋 term 90 E" non associative with precedence 90 for @{in_l ? $E}. +notation > "𝐋 term 70 E" non associative with precedence 75 for @{in_l ? $E}. nlet rec in_l (S : Alpha) (r : re S) on r : word S → Prop ≝ match r with [ z ⇒ {} @@ -90,7 +90,7 @@ match r with | c r1 r2 ⇒ 𝐋 r1 · 𝐋 r2 | o r1 r2 ⇒ 𝐋 r1 ∪ 𝐋 r2 | k r1 ⇒ (𝐋 r1) ^*]. -notation "𝐋 term 90 E" non associative with precedence 90 for @{'in_l $E}. +notation "𝐋 term 70 E" non associative with precedence 75 for @{'in_l $E}. interpretation "in_l" 'in_l E = (in_l ? E). interpretation "in_l mem" 'mem w l = (in_l ? l w). @@ -135,7 +135,7 @@ nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝ | pc E1 E2 ⇒ (|E1| · |E2|) | po E1 E2 ⇒ (|E1| + |E2|) | pk E ⇒ |E|^* ]. -notation < ".|term 19 e|" non associative with precedence 70 for @{'forget $e}. +notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}. interpretation "forget" 'forget a = (forget ? a). notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}. @@ -143,18 +143,18 @@ interpretation "fst" 'fst x = (fst ? ? x). notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}. interpretation "snd" 'snd x = (snd ? ? x). -notation > "𝐋\p\ term 90 E" non associative with precedence 90 for @{in_pl ? $E}. +notation > "𝐋\p\ term 70 E" non associative with precedence 75 for @{in_pl ? $E}. nlet rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝ match r with [ pz ⇒ {} | pe ⇒ {} | ps _ ⇒ {} | pp x ⇒ { [x] } -| pc r1 r2 ⇒ 𝐋\p\ r1 · 𝐋 .|r2| ∪ 𝐋\p\ r2 +| pc r1 r2 ⇒ 𝐋\p\ r1 · 𝐋 |r2| ∪ 𝐋\p\ r2 | po r1 r2 ⇒ 𝐋\p\ r1 ∪ 𝐋\p\ r2 -| pk r1 ⇒ 𝐋\p\ r1 · 𝐋 (.|r1|^* ) ]. -notation > "𝐋\p term 90 E" non associative with precedence 90 for @{'in_pl $E}. -notation "𝐋\sub(\p) term 90 E" non associative with precedence 90 for @{'in_pl $E}. +| pk r1 ⇒ 𝐋\p\ r1 · 𝐋 (|r1|^* ) ]. +notation > "𝐋\p term 70 E" non associative with precedence 75 for @{'in_pl $E}. +notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'in_pl $E}. interpretation "in_pl" 'in_pl E = (in_pl ? E). interpretation "in_pl mem" 'mem w l = (in_pl ? l w). @@ -164,7 +164,7 @@ interpretation "epsilon" 'epsilon = (epsilon ?). notation < "ϵ b" non associative with precedence 90 for @{'app_epsilon $b}. interpretation "epsilon lang" 'app_epsilon b = (epsilon ? b). -ndefinition in_prl ≝ λS : Alpha.λp:pre S. 𝐋\p\ (\fst p) ∪ ϵ (\snd p). +ndefinition in_prl ≝ λS : Alpha.λp:pre S. 𝐋\p (\fst p) ∪ ϵ (\snd p). interpretation "in_prl mem" 'mem w l = (in_prl ? l w). interpretation "in_prl" 'in_pl E = (in_prl ? E). @@ -182,7 +182,7 @@ nnormalize; *; ##[##2:*] nelim e; *; #w1; *; #w2; *; *; #defw1; nrewrite > (append_eq_nil … w1 w2 …); /3/ by {};//; nqed. -nlemma not_epsilon_lp : ∀S.∀e:pitem S. ¬ (𝐋\p e [ ]). +nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ((𝐋\p e) [ ]). #S e; nelim e; nnormalize; /2/ by nmk; ##[ #; @; #; ndestruct; ##| #r1 r2 n1 n2; @; *; /2/; *; #w1; *; #w2; *; *; #H; @@ -265,7 +265,7 @@ nlemma odotEt : ∀S.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = 〈e1 · \fst (•e2),b2 || \snd (•e2)〉. #S e1 e2 b2; nnormalize; ncases (•e2); //; nqed. -nlemma LcatE : ∀S.∀e1,e2:pitem S.𝐋\p (e1 · e2) = 𝐋\p e1 · 𝐋 .|e2| ∪ 𝐋\p e2. //; nqed. +nlemma LcatE : ∀S.∀e1,e2:pitem S.𝐋\p (e1 · e2) = 𝐋\p e1 · 𝐋 |e2| ∪ 𝐋\p e2. //; nqed. nlemma cup_dotD : ∀S.∀p,q,r:word S → Prop.(p ∪ q) · r = (p · r) ∪ (q · r). #S p q r; napply extP; #w; nnormalize; @; @@ -276,14 +276,14 @@ nqed. nlemma cup0 :∀S.∀p:word S → Prop.p ∪ {} = p. #S p; napply extP; #w; nnormalize; @; /2/; *; //; *; nqed. -nlemma erase_dot : ∀S.∀e1,e2:pitem S.𝐋 .|e1 · e2| = 𝐋 .|e1| · 𝐋 .|e2|. +nlemma erase_dot : ∀S.∀e1,e2:pitem S.𝐋 |e1 · e2| = 𝐋 |e1| · 𝐋 |e2|. #S e1 e2; napply extP; nnormalize; #w; @; *; #w1; *; #w2; *; *; /7/ by ex_intro, conj; nqed. -nlemma erase_plus : ∀S.∀e1,e2:pitem S.𝐋 .|e1 + e2| = 𝐋 .|e1| ∪ 𝐋 .|e2|. +nlemma erase_plus : ∀S.∀e1,e2:pitem S.𝐋 |e1 + e2| = 𝐋 |e1| ∪ 𝐋 |e2|. #S e1 e2; napply extP; nnormalize; #w; @; *; /4/ by or_introl, or_intror; nqed. -nlemma erase_star : ∀S.∀e1:pitem S.𝐋 .|e1|^* = 𝐋 .|e1^*|. //; nqed. +nlemma erase_star : ∀S.∀e1:pitem S.𝐋 |e1|^* = 𝐋 |e1^*|. //; nqed. ndefinition substract := λS.λp,q:word S → Prop.λw.p w ∧ ¬ q w. interpretation "substract" 'minus a b = (substract ? a b). @@ -300,18 +300,18 @@ nlemma subK : ∀S.∀a:word S → Prop. a - a = {}. nlemma subW : ∀S.∀a,b:word S → Prop.∀w.(a - b) w → a w. #S a b w; nnormalize; *; //; nqed. -nlemma erase_bull : ∀S.∀a:pitem S. .|\fst (•a)| = .|a|. +nlemma erase_bull : ∀S.∀a:pitem S. |\fst (•a)| = |a|. #S a; nelim a; // by {}; -##[ #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (.|e1| · .|e2|); +##[ #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (|e1| · |e2|); nrewrite < IH1; nrewrite < IH2; nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊙ 〈e2,false〉)); ncases (•e1); #e3 b; ncases b; nnormalize; ##[ ncases (•e2); //; ##| nrewrite > IH2; //] -##| #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (.|e1| + .|e2|); +##| #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (|e1| + |e2|); nrewrite < IH2; nrewrite < IH1; nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊕ •e2)); ncases (•e1); ncases (•e2); //; -##| #e IH; nchange in ⊢ (???%) with (.|e|^* ); nrewrite < IH; +##| #e IH; nchange in ⊢ (???%) with (|e|^* ); nrewrite < IH; nchange in ⊢ (??(??%)?) with (\fst (•e))^*; //; ##] nqed. @@ -325,8 +325,8 @@ napply Hw2; nqed. (* theorem 16: 1 → 3 *) nlemma odot_dot_aux : ∀S.∀e1,e2: pre S. - 𝐋\p (•(\fst e2)) = 𝐋\p (\fst e2) ∪ 𝐋 .|\fst e2| → - 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 .|\fst e2| ∪ 𝐋\p e2. + 𝐋\p (•(\fst e2)) = 𝐋\p (\fst e2) ∪ 𝐋 |\fst e2| → + 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 |\fst e2| ∪ 𝐋\p e2. #S e1 e2 th1; ncases e1; #e1' b1'; ncases b1'; ##[ nwhd in ⊢ (??(??%)?); nletin e2' ≝ (\fst e2); nletin b2' ≝ (\snd e2); nletin e2'' ≝ (\fst (•(\fst e2))); nletin b2'' ≝ (\snd (•(\fst e2))); @@ -335,8 +335,8 @@ nlemma odot_dot_aux : ∀S.∀e1,e2: pre S. nchange in match (𝐋\p 〈?,?〉) with (?∪?); nrewrite > (epsilon_or …); nrewrite > (cupC ? (ϵ ?)…); nrewrite > (cupA …);nrewrite < (cupA ?? (ϵ?)…); - nrewrite > (?: 𝐋\p e2'' ∪ ϵ b2'' = 𝐋\p e2' ∪ 𝐋 .|e2'|); ##[##2: - nchange with (𝐋\p 〈e2'',b2''〉 = 𝐋\p e2' ∪ 𝐋 .|e2'|); + nrewrite > (?: 𝐋\p e2'' ∪ ϵ b2'' = 𝐋\p e2' ∪ 𝐋 |e2'|); ##[##2: + nchange with (𝐋\p 〈e2'',b2''〉 = 𝐋\p e2' ∪ 𝐋 |e2'|); ngeneralize in match th1; nrewrite > (eta_lp…); #th1; nrewrite > th1; //;##] nrewrite > (eta_lp ? e2); @@ -385,7 +385,7 @@ alias symbol "pc" (instance 13) = "cat lang". alias symbol "in_pl" (instance 23) = "in_pl". alias symbol "in_pl" (instance 5) = "in_pl". alias symbol "eclose" (instance 21) = "eclose". -ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ 𝐋 .|e|. +ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ 𝐋 |e|. #S e; nelim e; //; ##[ #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl, or_intror; ##| #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl; *; @@ -405,22 +405,22 @@ ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ ##| #e; nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e)); #IH; nchange in match (𝐋\p ?) with (𝐋\p 〈e'^*,true〉); nchange in match (𝐋\p ?) with (𝐋\p (e'^* ) ∪ {[ ]}); - nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 .|e'|^* ); + nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* ); nrewrite > (erase_bull…e); nrewrite > (erase_star …); - nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 .|e| - ϵ b')); ##[##2: + nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b')); ##[##2: nchange in IH : (??%?) with (𝐋\p e' ∪ ϵ b'); ncases b' in IH; ##[ #IH; nrewrite > (cup_sub…); //; nrewrite < IH; nrewrite < (cup_sub…); //; nrewrite > (subK…); nrewrite > (cup0…);//; ##| nrewrite > (sub0 …); #IH; nrewrite < IH; nrewrite > (cup0 …);//; ##]##] nrewrite > (cup_dotD…); nrewrite > (cupA…); - nrewrite > (?: ((?·?)∪{[]} = 𝐋 .|e^*|)); //; - nchange in match (𝐋 .|e^*|) with ((𝐋. |e|)^* ); napply sub_dot_star;##] + nrewrite > (?: ((?·?)∪{[]} = 𝐋 |e^*|)); //; + nchange in match (𝐋 |e^*|) with ((𝐋 |e|)^* ); napply sub_dot_star;##] nqed. (* theorem 16: 3 *) nlemma odot_dot: - ∀S.∀e1,e2: pre S. 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 .|\fst e2| ∪ 𝐋\p e2. + ∀S.∀e1,e2: pre S. 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 |\fst e2| ∪ 𝐋\p e2. #S e1 e2; napply odot_dot_aux; napply (bull_cup S (\fst e2)); nqed. nlemma dot_star_epsilon : ∀S.∀e:re S.𝐋 e · 𝐋 e^* ∪ {[]} = 𝐋 e^*. @@ -449,13 +449,13 @@ nlemma rcanc_sing : ∀S.∀A,C:word S → Prop.∀b:word S . nqed. (* theorem 16: 4 *) -nlemma star_dot: ∀S.∀e:pre S. 𝐋\p (e^⊛) = 𝐋\p e · (𝐋 .|\fst e|)^*. +nlemma star_dot: ∀S.∀e:pre S. 𝐋\p (e^⊛) = 𝐋\p e · (𝐋 |\fst e|)^*. #S p; ncases p; #e b; ncases b; ##[ nchange in match (〈e,true〉^⊛) with 〈?,?〉; nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e)); nchange in ⊢ (??%?) with (?∪?); - nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 .|e'|^* ); - nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 .|e| - ϵ b' )); ##[##2: + nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* ); + nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b' )); ##[##2: nlapply (bull_cup ? e); #bc; nchange in match (𝐋\p (•e)) in bc with (?∪?); nchange in match b' in bc with b'; @@ -467,7 +467,7 @@ nlemma star_dot: ∀S.∀e:pre S. 𝐋\p (e^⊛) = 𝐋\p e · (𝐋 .|\fst e|)^ nrewrite > (cup_dotD…); nrewrite > (epsilon_dot…); //; ##| nwhd in match (〈e,false〉^⊛); nchange in match (𝐋\p 〈?,?〉) with (?∪?); nrewrite > (cup0…); - nchange in ⊢ (??%?) with (𝐋\p e · 𝐋 .|e|^* ); + nchange in ⊢ (??%?) with (𝐋\p e · 𝐋 |e|^* ); nrewrite < (cup0 ? (𝐋\p e)); //;##] nqed. @@ -496,7 +496,7 @@ nlemma Lp_pre_of_re : ∀S.∀e:re S. 𝐋\p (pre_of_re ? e) = {}. nrewrite > H1; napply dot0; ##] nqed. -nlemma erase_pre_of_reK : ∀S.∀e. 𝐋 .|pre_of_re S e| = 𝐋 e. +nlemma erase_pre_of_reK : ∀S.∀e. 𝐋 |pre_of_re S e| = 𝐋 e. #S A; nelim A; //; ##[ #e1 e2 H1 H2; nchange in match (𝐋 (e1 · e2)) with (𝐋 e1·?); nrewrite < H1; nrewrite < H2; // @@ -516,12 +516,11 @@ nlemma Pext : ∀S.∀f,g:word S → Prop. f = g → ∀w.f w → g w. #S f g H; nrewrite > H; //; nqed. (* corollary 18 *) -ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ .|e|. +ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ |e|. #S e; @; ##[ #defsnde; nlapply (bull_cup ? e); nchange in match (𝐋\p (•e)) with (?∪?); nrewrite > defsnde; #H; nlapply (Pext ??? H [ ] ?); ##[ @2; //] *; //; - E MO? STOP @@ -543,7 +542,7 @@ interpretation "move" 'move x E = (move ? x E). ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e). interpretation "rmove" 'move x E = (rmove ? x E). -nlemma XXz : ∀S:Alpha.∀w:word S. w .∈ ∅ → False. +nlemma XXz : ∀S:Alpha.∀w:word S. w ∈ ∅ → False. #S w abs; ninversion abs; #; ndestruct; nqed.