X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fnlibrary%2Fre%2Fre-setoids.ma;h=79f6b49d9b22aab1d6f0bd37d7ea421a3803f9e1;hb=dca4170c5ce5f2cd6be8ae1dc0422bd6a680b43f;hp=03c8305380da1cd376d75c0f271dd231fb07cd0f;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/nlibrary/re/re-setoids.ma b/matita/matita/nlibrary/re/re-setoids.ma
index 03c830538..79f6b49d9 100644
--- a/matita/matita/nlibrary/re/re-setoids.ma
+++ b/matita/matita/nlibrary/re/re-setoids.ma
@@ -97,7 +97,7 @@ notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}.
 interpretation "star" 'pk a = (k ? a).
 interpretation "or" 'plus a b = (o ? a b).
            
-notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
+notation "a · b" non associative with precedence 65 for @{ 'pc $a $b}.
 interpretation "cat" 'pc a b = (c ? a b).
 
 (* to get rid of \middot *)
@@ -629,7 +629,7 @@ nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ([ ] ∈ (𝐋\p e)).
 nqed.
 
 ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
-notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
+notation "a ⊕ b" left associative with precedence 65 for @{'oplus $a $b}.
 interpretation "oplus" 'oplus a b = (lo ? a b).
 
 ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
@@ -638,9 +638,9 @@ ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
    [ false ⇒ 〈e1 · \fst b, \snd b〉 
    | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]].
    
-notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
+notation < "a ⊙ b" left associative with precedence 65 for @{'lc $op $a $b}.
 interpretation "lc" 'lc op a b = (lc ? op a b).
-notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}.
+notation > "a ⊙ b" left associative with precedence 65 for @{'lc eclose $a $b}.
 
 ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
    match a with [ mk_pair e1 b1 ⇒
@@ -652,7 +652,7 @@ notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}.
 interpretation "lk" 'lk op a = (lk ? op a).
 notation > "a ^ ⊛" non associative with precedence 75 for @{'lk eclose $a}.
 
-notation > "•" non associative with precedence 60 for @{eclose ?}.
+notation > "•" non associative with precedence 65 for @{eclose ?}.
 nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
  match E with
   [ pz ⇒ 〈 0, false 〉
@@ -662,9 +662,9 @@ nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
   | po E1 E2 ⇒ •E1 ⊕ •E2
   | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉 
   | pk E ⇒ 〈(\fst (•E))^*,true〉].
-notation < "• x" non associative with precedence 60 for @{'eclose $x}.
+notation < "• x" non associative with precedence 65 for @{'eclose $x}.
 interpretation "eclose" 'eclose x = (eclose ? x).
-notation > "• x" non associative with precedence 60 for @{'eclose $x}.
+notation > "• x" non associative with precedence 65 for @{'eclose $x}.
 
 ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
 interpretation "reclose" 'eclose x = (reclose ? x).
@@ -828,34 +828,41 @@ nlemma sub_dot_star :
     @; //;##]
 nqed.
 
-STOP
-
 (* theorem 16: 1 *)
 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; *;
+  ##[ #a; napply ext_set; #w; @; *; /3/ by or_introl, or_intror;
+  ##| #a; napply ext_set; #w; @; *; /3/ by or_introl; *;
   ##| #e1 e2 IH1 IH2;  
-      nchange in ⊢ (??(??(%))?) with (•e1 ⊙ 〈e2,false〉);
-      nrewrite > (odot_dot_aux S (•e1) 〈e2,false〉 IH2);
-      nrewrite > (IH1 …); nrewrite > (cup_dotD …);
-      nrewrite > (cupA …); nrewrite > (cupC ?? (𝐋\p ?) …);
-      nchange in match (𝐋\p 〈?,?〉) with (𝐋\p e2 ∪ {}); nrewrite > (cup0 …);
-      nrewrite < (erase_dot …); nrewrite < (cupA …); //;
+      nchange in match (•(e1·e2)) with (•e1 ⊙ 〈e2,false〉);
+      napply (.=_1 (odot_dot_aux ?? 〈e2,false〉 IH2));
+      napply (.=_1 (IH1 ╪_1 #) ╪_1 #);
+      napply (.=_1 (cup_dotD …) ╪_1 #);
+      napply (.=_1 (cupA …));
+      napply (.=_1 # ╪_1 ((erase_dot ???)^-1 ╪_1 (cup0 ??)));
+      napply (.=_1 # ╪_1 (cupC…));
+      napply (.=_1 (cupA …)^-1);
+      //;
   ##| #e1 e2 IH1 IH2;
-      nchange in match (•(?+?)) with (•e1 ⊕ •e2); nrewrite > (oplus_cup …);
-      nrewrite > (IH1 …); nrewrite > (IH2 …); nrewrite > (cupA …);
-      nrewrite > (cupC ? (𝐋\p e2)…);nrewrite < (cupA ??? (𝐋\p e2)…);
-      nrewrite > (cupC ?? (𝐋\p e2)…); nrewrite < (cupA …); 
-      nrewrite < (erase_plus …); //.
+      nchange in match (•(?+?)) with (•e1 ⊕ •e2);
+      napply (.=_1 (oplus_cup …));
+      napply (.=_1 IH1 ╪_1 IH2);
+      napply (.=_1 (cupA …));
+      napply (.=_1 # ╪_1 (# ╪_1 (cupC…)));
+      napply (.=_1 # ╪_1 (cupA ????)^-1);
+      napply (.=_1 # ╪_1 (cupC…));
+      napply (.=_1 (cupA ????)^-1);
+      napply (.=_1 # ╪_1 (erase_plus ???)^-1);
+      //;
   ##| #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'^*,true〉);
       nchange in match (𝐋\p ?) with (𝐋\p (e'^* ) ∪ {[ ]});
-      nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 .|e'|^* );
+STOP
+      nchange in match (𝐋\p (pk ? e')) with (𝐋\p e' · 𝐋  |e'|^* );
       nrewrite > (erase_bull…e);
       nrewrite > (erase_star …);
       nrewrite > (?: 𝐋\p e' =  𝐋\p e ∪ (𝐋 .|e| - ϵ b')); ##[##2:
@@ -866,7 +873,7 @@ ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S.  𝐋\p (•e) =  𝐋\p e ∪ 
       nrewrite > (cup_dotD…); nrewrite > (cupA…); 
       nrewrite > (?: ((?·?)∪{[]} = 𝐋 .|e^*|)); //;
       nchange in match (𝐋 .|e^*|) with ((𝐋. |e|)^* ); napply sub_dot_star;##]
- nqed.
+nqed.
 
 (* theorem 16: 3 *)      
 nlemma odot_dot: 
@@ -976,7 +983,7 @@ ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ .
 STOP
 
 notation > "\move term 90 x term 90 E" 
-non associative with precedence 60 for @{move ? $x $E}.
+non associative with precedence 65 for @{move ? $x $E}.
 nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
  match E with
   [ pz ⇒ 〈 ∅, false 〉
@@ -986,8 +993,8 @@ nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
   | po e1 e2 ⇒ \move x e1 ⊕ \move x e2 
   | pc e1 e2 ⇒ \move x e1 ⊙ \move x e2
   | pk e ⇒ (\move x e)^⊛ ].
-notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
-notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
+notation < "\move\shy x\shy E" non associative with precedence 65 for @{'move $x $E}.
+notation > "\move term 90 x term 90 E" non associative with precedence 65 for @{'move $x $E}.
 interpretation "move" 'move x E = (move ? x E).
 
 ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
@@ -1057,7 +1064,7 @@ ntheorem move_ok:
 nqed.
 
 
-notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}.
+notation > "x ↦* E" non associative with precedence 65 for @{move_star ? $x $E}.
 nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝
  match w with
   [ nil ⇒ E