X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fre%2Fre.ma;h=234d522ae176dde98579f39ac9e6ac09bb11aa32;hb=64a752136a679bcab14a9cd01823c18b7cc991de;hp=9b63788461d53b8d90af8b2d73b0f4298a3e5754;hpb=65a3b93b01f2d00960c56df3563b879f36f3cbfd;p=helm.git

diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma
index 9b6378846..234d522ae 100644
--- 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.
@@ -274,8 +273,8 @@ lemma sem_star_w : ∀S.∀i:pitem S.∀w.
 (* Below are a few, simple, semantic properties of items. In particular:
 - not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
 - epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
-- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
-- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+- minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{[ ]}.
+- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} ≐ \sem{e}-{[ ]}.
 The first property is proved by a simple induction on $i$; the other
 results are easy corollaries. We need an auxiliary lemma first. *)
 
@@ -299,14 +298,14 @@ lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e.
 #S * #i #b #btrue normalize in btrue; >btrue %2 // 
 qed.
 
-lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
+lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{[ ]}.
 #S #i #w % 
   [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
   |* //
   ]
 qed.
 
-lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} ≐ \sem{e}-{[ ]}.
 #S * #i * 
   [>sem_pre_true normalize in ⊢ (??%?); #w % 
     [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
@@ -342,7 +341,7 @@ then, we just have •(i1+i2) = •(i1)⊕ •(i2).
 *)
 
 definition lo ≝ λS:DeqSet.λ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〉.
@@ -368,17 +367,17 @@ Let us come to the formalized definitions:
 definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
   match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
  
-notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
+notation "i ◃ e" left associative with precedence 65 for @{'lhd $i $e}.
 interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
 
 (* The behaviour of ◃ is summarized by the following, easy lemma: *)
 
 lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop. 
-  A = B → A =1 B. 
+  A = B → A ≐ B. 
 #S #A #B #H >H /2/ qed.
 
 lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
-  \sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
+  \sem{i ◃ e} ≐ \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
 #S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //] 
 >sem_pre_true >sem_cat >sem_pre_true /2/ 
 qed.
@@ -397,10 +396,10 @@ definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe
     ]
   ].
 
-notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
+notation "a ▹ b" left associative with precedence 65 for @{'tril eclose $a $b}.
 interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
 
-notation "•" non associative with precedence 60 for @{eclose ?}.
+notation "•" non associative with precedence 65 for @{eclose ?}.
 
 (* We are ready to give the formal definition of the broadcasting operation. *)
 
@@ -414,7 +413,7 @@ let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
   | pc i1 i2 ⇒ •i1 ▹ i2
   | pk i ⇒ 〈(\fst (•i))^*,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).
 
 (* Here are a few simple properties of ▹ and •(-) *)
@@ -471,14 +470,14 @@ qed.
 
 (* We are now ready to state the main semantic properties of ⊕, ◃ and •(-):
 
-sem_oplus:     \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2} 
-sem_pcl:       \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}
-sem_bullet     \sem{•i} =1 \sem{i} ∪ \sem{|i|}
+sem_oplus:     \sem{e1 ⊕ e2} ≐ \sem{e1} ∪ \sem{e2} 
+sem_pcl:       \sem{e1 ▹ i2} ≐  \sem{e1} · \sem{|i2|} ∪ \sem{i2}
+sem_bullet     \sem{•i} ≐ \sem{i} ∪ \sem{|i|}
 
 The proof of sem_oplus is straightforward. *)
 
 lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
-  \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}. 
+  \sem{e1 ⊕ e2} ≐ \sem{e1} ∪ \sem{e2}. 
 #S * #i1 #b1 * #i2 #b2 #w %
   [cases b1 cases b2 normalize /2/ * /3/ * /3/
   |cases b1 cases b2 normalize /2/ * /3/ * /3/
@@ -489,8 +488,8 @@ qed.
 auxiliary lemma, that assumes sem_bullet:
 
 sem_pcl_aux: 
-   \sem{•i2} =1  \sem{i2} ∪ \sem{|i2|} →
-   \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+   \sem{•i2} ≐  \sem{i2} ∪ \sem{|i2|} →
+   \sem{e1 ▹ i2} ≐  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
 
 Then, using the previous result, we prove sem_bullet by induction 
 on i. Finally, sem_pcl_aux and sem_bullet give sem_pcl. *)
@@ -500,8 +499,8 @@ lemma LcatE : ∀S.∀e1,e2:pitem S.
 // qed.
 
 lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
-   \sem{•i2} =1  \sem{i2} ∪ \sem{|i2|} →
-   \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+   \sem{•i2} ≐  \sem{i2} ∪ \sem{|i2|} →
+   \sem{e1 ▹ i2} ≐  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
 #S * #i1 #b1 #i2 cases b1
   [2:#th >odot_false >sem_pre_false >sem_pre_false >sem_cat /2/
   |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
@@ -512,7 +511,7 @@ lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
 qed.
   
 lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A. 
- \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
+ \sem{e} ≐ \sem{i} ∪ A → \sem{\fst e} ≐ \sem{i} ∪ (A - {[ ]}).
 #S #e #i #A #seme
 @eqP_trans [|@minus_eps_pre]
 @eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
@@ -520,7 +519,7 @@ lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
 @eqP_substract_r //
 qed.
 
-theorem sem_bull: ∀S:DeqSet. ∀i:pitem S.  \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
+theorem sem_bull: ∀S:DeqSet. ∀i:pitem S.  \sem{•i} ≐ \sem{i} ∪ \sem{|i|}.
 #S #e elim e 
   [#w normalize % [/2/ | * //]
   |/2/ 
@@ -583,7 +582,7 @@ lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
 #S #e elim e normalize //
 qed.
 
-lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
+lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} ≐ ∅.
 #S #e elim e 
   [1,2:@eq_to_ex_eq // 
   |#s @eq_to_ex_eq //
@@ -600,7 +599,7 @@ lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
 qed.
    
 theorem re_embedding: ∀S.∀e:re S. 
-  \sem{•(blank S e)} =1 \sem{e}.
+  \sem{•(blank S e)} ≐ \sem{e}.
 #S #e @eqP_trans [|@sem_bull] >forget_blank 
 @eqP_trans [|@eqP_union_r [|@sem_blank]]
 @eqP_trans [|@union_comm] @union_empty_r.
@@ -663,7 +662,7 @@ lemma erase_ostar: ∀S.∀e:pre S.
 #S * #i * // qed.
 
 lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i. 
-  \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
+  \sem{e1 ⊙ 〈i,true〉} ≐ \sem{e1 ▹ i} ∪ { [ ] }.
 #S #e1 #i 
 cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
 #H >H cases (e1 ▹ i) #i1 #b1 cases b1 
@@ -684,7 +683,7 @@ qed.
 of ⊙ and ⊛. *)
 
 lemma sem_odot: 
-  ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
+  ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} ≐ \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
 #S #e1 * #i2 * 
   [>sem_pre_true 
    @eqP_trans [|@sem_odot_true]
@@ -694,7 +693,7 @@ lemma sem_odot:
 qed.
       
 theorem sem_ostar: ∀S.∀e:pre S. 
-  \sem{e^⊛} =1  \sem{e} · \sem{|\fst e|}^*.
+  \sem{e^⊛} ≐  \sem{e} · \sem{|\fst e|}^*.
 #S * #i #b cases b
   [(* lhs = \sem{〈i,true〉^⊛} *)
    >sem_pre_true (* >sem_pre_true *)