bla bla bla

[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 2b5ed2cb8399af2dd5695c6d260b6d0b6a4e2d1d..25cfe67cb6da3e02adbfd4283078c1f619708d21 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -29,44 +29,51 @@ definition subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
 
 notation "a \subseteq u" left associative with precedence 70 
   for @{ 'subset $a $u }.
-interpretation "Bishop subset" 'subset a b =
-  (cic:/matita/dama/uniform/subset.con _ a b). 
+interpretation "Bishop subset" 'subset a b = (subset _ a b). 
 
-notation "{ ident x : t | p }" non associative with precedence 50
+notation "hvbox({ ident x : t | break p })" non associative with precedence 50
   for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.  
 definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
-interpretation "explicit set" 'explicitset t =
-  (cic:/matita/dama/uniform/mk_set.con _ t).
+interpretation "explicit set" 'explicitset t = (mk_set _ t).
 
-notation < "s \sup 2" non associative with precedence 90
-  for @{ 'square $s }.
+notation < "s  2 \atop \neq" non associative with precedence 90
+  for @{ 'square2 $s }.
 notation > "s 'square'" non associative with precedence 90
   for @{ 'square $s }.
-interpretation "bishop suqare set" 'square x =
-  (cic:/matita/dama/uniform/square_bishop_set.con x).    
+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 (prod ?? (fst x) y) ∧ V (prod ?? y (snd x)).
+   λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
    
 notation "a \circ b"  left associative with precedence 60
   for @{'compose $a $b}.
-interpretation "relations composition" 'compose a b = 
- (cic:/matita/dama/uniform/compose_relations.con _ 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 (prod ?? (snd x) (fst x)).
+    λx:C square. U 〈snd x,fst x〉.
     
 notation < "s \sup (-1)"  non associative with precedence 90
   for @{ 'invert $s }.
+notation < "s \sup (-1) x"  non associative with precedence 90
+  for @{ 'invert2 $s $x}. 
 notation > "'inv' s" non associative with precedence 90
   for @{ 'invert $s }.
-interpretation "relation invertion" 'invert a = 
- (cic:/matita/dama/uniform/invert_relation.con _ a).
+interpretation "relation invertion" 'invert a = (invert_relation _ a).
+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".
 record uniform_space : Type ≝ {
   us_carr:> bishop_set;
   us_unifbase: (us_carr square → Prop) → CProp;
@@ -76,33 +83,32 @@ record uniform_space : Type ≝ {
     ∃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 → U = inv U (* I should use double inclusion ... *)
+  us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x)
 }.
 
 (* Definition 2.14 *)  
 alias symbol "leq" = "natural 'less or equal to'".
 definition cauchy ≝
   λC:uniform_space.λa:sequence C.∀U.us_unifbase C U → 
-   ∃n. ∀i,j. n ≤ i → n ≤ j → U (prod ?? (a i) (a j)).
+   ∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉.
    
 notation < "a \nbsp 'is_cauchy'" non associative with precedence 50 
   for @{'cauchy $a}.
 notation > "a 'is_cauchy'" non associative with precedence 50 
   for @{'cauchy $a}.
-interpretation "Cauchy sequence" 'cauchy s =
- (cic:/matita/dama/uniform/cauchy.con _ s).  
+interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).  
    
 (* Definition 2.15 *)  
 definition uniform_converge ≝
   λC:uniform_space.λa:sequence C.λu:C.
-    ∀U.us_unifbase C U →  ∃n. ∀i. n ≤ i → U (prod ?? u (a i)).
+    ∀U.us_unifbase C U →  ∃n. ∀i. n ≤ i → U 〈u,a i〉.
     
 notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50 
   for @{'uniform_converge $a $x}.
 notation > "a 'uniform_converges' x" non associative with precedence 50 
   for @{'uniform_converge $a $x}.
 interpretation "Uniform convergence" 'uniform_converge s u =
- (cic:/matita/dama/uniform/uniform_converge.con _ s u).
+ (uniform_converge _ s u).
  
 (* Lemma 2.16 *)
 lemma uniform_converge_is_cauchy : 
@@ -112,17 +118,15 @@ intros (C a x Ha); intros 2 (u Hu);
 cases (us_phi3 ?? Hu) (v Hv0); cases Hv0 (Hv H); clear Hv0;
 cases (Ha ? Hv) (n Hn); exists [apply n]; intros;
 apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)]
-rewrite > (us_phi4 ?? Hv); simplify; apply (Hn ? H1);
+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 =
-  (cic:/matita/dama/uniform/mk_big_set.con _ t).
+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}.
-
-