decentralizing core notation

[helm.git] / matita / matita / lib / re / reb.ma

diff --git a/matita/matita/lib/re/reb.ma b/matita/matita/lib/re/reb.ma
index 79a74c24d3fde9dbb9c444a761a167976824e4a8..2c5b129d228e7c87bb4d537c39e47a28cb22dab1 100644 (file)
--- a/matita/matita/lib/re/reb.ma
+++ b/matita/matita/lib/re/reb.ma
@@ -14,6 +14,7 @@
 
 include "arithmetics/nat.ma".
 include "basics/lists/list.ma".
+include "basics/core_notation/singl_1.ma".
 
 interpretation "iff" 'iff a b = (iff a b).  
 
@@ -48,7 +49,7 @@ notation > "a ^ *" non associative with precedence 90 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 
@@ -86,6 +87,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).
 
@@ -134,7 +137,7 @@ interpretation "patom" 'ps a = (ps ? a).
 interpretation "pepsilon" 'epsilon = (pe ?).
 interpretation "pempty" 'empty = (pz ?).
 
-notation > "| e |" non associative with precedence 65 for @{forget ? $e}.
+notation > "| e |" non associative with precedence 66 for @{forget ? $e}.
 let rec forget (S: Alpha) (l : pitem S) on l: re S ≝
  match l with
   [ pz ⇒ ∅
@@ -195,7 +198,7 @@ lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → [ ] ∈ e.
 qed.
 
 definition 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).
 
 lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1||b2〉.
@@ -216,9 +219,9 @@ definition lift ≝ λf:∀S.pitem S →pre S.λS.λe:pre S.
   match e with 
   [ pair i b ⇒ 〈\fst (f S i), \snd (f S i) || 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 (lift eclose) $a $b}.
+notation > "a ⊙ b" left associative with precedence 65 for @{'lc (lift eclose) $a $b}.
 
 definition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λe:pre S.
   match e with 
@@ -234,7 +237,7 @@ interpretation "lk" 'lk op a = (lk ? op a).
 notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
 
 
-notation > "•" non associative with precedence 60 for @{eclose ?}.
+notation > "•" non associative with precedence 65 for @{eclose ?}.
 let rec eclose (S: Alpha) (i: pitem S) on i : pre S ≝
  match i with
   [ pz ⇒ 〈 ∅, false 〉
@@ -245,19 +248,19 @@ let rec eclose (S: Alpha) (i: pitem S) on i : pre S ≝
   | 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}.
 
 definition reclose ≝ lift eclose.
 interpretation "reclose" 'eclose x = (reclose ? x).
 
 definition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w.
-notation "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
+notation "A ≐ B" non associative with precedence 45 for @{'eq_f1 $A $B}.
 interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b).
 
 (*
-lemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) =1 ϵ b1 ∪ ϵ b2. 
+lemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) ≐ ϵ b1 ∪ ϵ b2. 
 ##[##2: napply S]
 #S b1 b2; ncases b1; ncases b2; napply extP; #w; nnormalize; @; /2/; *; //; *;
 nqed.
@@ -269,7 +272,7 @@ nlemma cupC : ∀S. ∀a,b:word S → Prop.a ∪ b = b ∪ a.
 #S a b; napply extP; #w; @; *; nnormalize; /2/; nqed.*)
 
 (* theorem 16: 2 *)
-lemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.\sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
+lemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.\sem{e1 ⊕ e2} ≐ \sem{e1} ∪ \sem{e2}.
 #S * #i1 #b1  * #i2 #b2 >lo_def normalize in ⊢ (?%?);
 
 #w cases b1 cases b2 normalize % #w r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2;
@@ -545,7 +548,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 〉
@@ -555,8 +558,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).
@@ -626,7 +629,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
@@ -776,3 +779,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;
 
+*)