more notation

[helm.git] / helm / software / matita / contribs / dama / dama / uniform.ma

diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
index 348b99a8139cf14e3a0f8cf05ea321d99a633342..b8b77572b67a4f4646a73b44091521018c0287bb 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -31,11 +31,6 @@ notation "a \subseteq u" left associative with precedence 70
   for @{ 'subset $a $u }.
 interpretation "Bishop subset" 'subset a b = (subset _ a b). 
 
-notation "hvbox({ ident x : t | break p })" non associative with precedence 80
-  for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.  
-definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
-interpretation "explicit set" 'explicitset t = (mk_set _ t).
-
 notation < "s  2 \atop \neq" non associative with precedence 90
   for @{ 'square2 $s }.
 notation > "s 'square'" non associative with precedence 90
@@ -43,44 +38,41 @@ notation > "s 'square'" non associative with precedence 90
 interpretation "bishop set square" 'square x = (square_bishop_set x).    
 interpretation "bishop set square" 'square2 x = (square_bishop_set x).    
 
-
 alias symbol "exists" = "exists".
 alias symbol "and" = "logical and".
 definition compose_relations ≝
   λC:bishop_set.λU,V:C square → Prop.
    λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
    
-notation "a \circ b"  left associative with precedence 60
+notation "a \circ b"  left associative with precedence 70
   for @{'compose $a $b}.
 interpretation "relations composition" 'compose a b = (compose_relations _ a b).
-notation "hvbox(x \in break a \circ break b)"  non associative with precedence 50
-  for @{'compose2 $a $b $x}.
-interpretation "relations composition" 'compose2 a b x = 
- (compose_relations _ a b x).
 
 definition invert_relation ≝
   λC:bishop_set.λU:C square → Prop.
     λx:C square. U 〈snd x,fst x〉.
     
-notation < "s \sup (-1)"  non associative with precedence 90
+notation < "s \sup (-1)"  left associative with precedence 70
   for @{ 'invert $s }.
-notation < "s \sup (-1) x"  non associative with precedence 90
+notation < "s \sup (-1) x"  left associative with precedence 70
   for @{ 'invert2 $s $x}. 
-notation > "'inv' s" non associative with precedence 90
-  for @{ 'invert $s }.
+notation > "'inv'" right associative with precedence 70
+  for @{ 'invert0  }.
 interpretation "relation invertion" 'invert a = (invert_relation _ a).
+interpretation "relation invertion" 'invert0 = (invert_relation _).
 interpretation "relation invertion" 'invert2 a x = (invert_relation _ a x).
 
 alias symbol "exists" = "CProp exists".
-alias symbol "and" (instance 18) = "constructive and".
-alias symbol "and" (instance 10) = "constructive and".
+alias symbol "and" (instance 21) = "constructive and".
+alias symbol "and" (instance 16) = "constructive and".
+alias symbol "and" (instance 9) = "constructive and".
 record uniform_space : Type ≝ {
   us_carr:> bishop_set;
   us_unifbase: (us_carr square → Prop) → CProp;
   us_phi1: ∀U:us_carr square → Prop. us_unifbase U → 
-    {x:us_carr square|fst x ≈ snd x} ⊆ U;
+    (λx:us_carr square.fst x ≈ snd x) ⊆ U;
   us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V →
-    ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ {x:?|U x ∧ V x});
+    ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
   us_phi3: ∀U:us_carr square → Prop. us_unifbase U → 
     ∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
   us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x)
@@ -121,12 +113,3 @@ apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)]
 cases (us_phi4 ?? Hv 〈a i,x〉) (P1 P2); apply P2;
 apply (Hn ? H1);
 qed.
-
-(* Definition 2.17 *)
-definition mk_big_set ≝
-  λP:CProp.λF:P→CProp.F.
-interpretation "explicit big set" 'explicitset t = (mk_big_set _ t).
-    
-definition restrict_uniformity ≝
-  λC:uniform_space.λX:C→Prop.
-   {U:C square → Prop| (U ⊆ {x:C square|X (fst x) ∧ X(snd x)}) ∧ us_unifbase C U}.