X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fformal_topology.ma;h=63da5347726baff4f1ab833606f54cef6c89b3d8;hb=e91eb82d2b5e032907758bff0b474d62d57463dc;hp=a683784081bcf5064d92690d3952309b172404a5;hpb=0e50062a04d72b333403d633a77dd113b32d6784;p=helm.git

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index a68378408..63da53477 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -13,93 +13,50 @@
 (**************************************************************************)
 
 include "logic/equality.ma".
+include "logic/cprop_connectives.ma".
 
-inductive And (A,B:CProp) : CProp ≝
- conj: A → B → And A B.
- 
-interpretation "constructive and" 'and x y = (And x y).
+record powerset (A : Type) : Type ≝ { char : A → CProp }.
 
-inductive Or (A,B:CProp) : CProp ≝
- | or_intro_l: A → Or A B
- | or_intro_r: B → Or A B. 
- 
-interpretation "constructive or" 'or x y = (Or x y).
+interpretation "char" 'subset p = (mk_powerset ? p).  
 
-inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝
-  ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
+interpretation "pwset" 'powerset a = (powerset a). 
 
-record powerset (A: Type) : Type ≝ { char: A → CProp }.
+interpretation "in" 'mem a X = (char ? X a). 
 
-notation "hvbox(2 \sup A)" non associative with precedence 45
-for @{ 'powerset $A }.
+definition subseteq ≝ λA.λu,v:\Omega \sup A.∀x.x ∈ u → x ∈ v.
 
-interpretation "powerset" 'powerset A = (powerset A).
+interpretation "subseteq" 'subseteq u v = (subseteq ? u v).
 
-notation < "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+definition overlaps ≝ λA.λU,V : Ω \sup A. exT2 ? (λx.x ∈ U) (λx.x ∈ V).
 
-notation > "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i}. $p)}.
+interpretation "overlaps" 'overlaps u v = (overlaps ? u v).
 
-interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
+definition intersect ≝ λA.λu,v:Ω\sup A.{ y | y ∈ u ∧ y ∈ v }.
 
-definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
-
-notation "hvbox(a break ∈ b)" non associative with precedence 45
-for @{ 'mem $a $b }.
-
-interpretation "mem" 'mem a S = (mem _ S a).
-
-definition overlaps ≝ λA:Type.λU,V:2 \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
-
-notation "hvbox(a break ≬ b)" non associative with precedence 45
-for @{ 'overlaps $a $b }. (* \between *)
-
-interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
-
-definition subseteq ≝ λA:Type.λU,V:2 \sup A.∀a:A. a ∈ U → a ∈ V.
-
-notation "hvbox(a break ⊆ b)" non associative with precedence 45
-for @{ 'subseteq $a $b }. (* \subseteq *)
-
-interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
-
-definition intersects ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∧ a ∈ V}.
-
-notation "hvbox(a break ∩ b)" non associative with precedence 55
-for @{ 'intersects $a $b }. (* \cap *)
-
-interpretation "intersects" 'intersects U V = (intersects _ U V).
-
-definition union ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∨ a ∈ V}.
-
-notation "hvbox(a break ∪ b)" non associative with precedence 55
-for @{ 'union $a $b }. (* \cup *)
-
-interpretation "union" 'union U V = (union _ U V).
+interpretation "intersect" 'intersects u v = (intersect ? u v). 
 
 record axiom_set : Type ≝ { 
   A:> Type;
   i: A → Type;
-  C: ∀a:A. i a → 2 \sup A
+  C: ∀a:A. i a → Ω \sup A
 }.
 
-inductive for_all (A: axiom_set) (U,V: 2 \sup A) (covers: A → CProp) : CProp ≝
+inductive for_all (A: axiom_set) (U,V: Ω \sup A) (covers: A → CProp) : CProp ≝
    iter: (∀a:A.a ∈ V → covers a) → for_all A U V covers.
 
-inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
+inductive covers (A: axiom_set) (U: \Omega \sup A) : A → CProp ≝
    refl: ∀a:A. a ∈ U → covers A U a
  | infinity: ∀a:A. ∀j: i ? a. for_all A U (C ? a j) (covers A U) → covers A U a.
 
 notation "hvbox(a break ◃ b)" non associative with precedence 45
 for @{ 'covers $a $b }. (* a \ltri b *)
 
-interpretation "coversl" 'covers A U = (for_all _ U A (covers _ U)).
-interpretation "covers" 'covers a U = (covers _ U a).
+interpretation "coversl" 'covers A U = (for_all ? U A (covers ? U)).
+interpretation "covers" 'covers a U = (covers ? U a).
 
 definition covers_elim ≝
- λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
-  λH1:∀a:A. a ∈ U → a ∈ P.
+ λA:axiom_set.λU: \Omega \sup A.λP:\Omega \sup A.
+  λH1: U ⊆ P. 
    λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → C ? a j ⊆ P → a ∈ P.
     let rec aux (a:A) (p:a ◃ U) on p : a ∈ P ≝
      match p return λaa.λ_:aa ◃ U.aa ∈ P with
@@ -111,20 +68,20 @@ definition covers_elim ≝
     in
      aux.
 
-inductive ex_such (A : axiom_set) (U,V : 2 \sup A) (fish: A → CProp) : CProp ≝
+inductive ex_such (A : axiom_set) (U,V : \Omega \sup A) (fish: A → CProp) : CProp ≝
  found : ∀a. a ∈ V → fish a → ex_such A U V fish.
 
-coinductive fish (A:axiom_set) (U: 2 \sup A) : A → CProp ≝
+coinductive fish (A:axiom_set) (U: \Omega \sup A) : A → CProp ≝
  mk_fish: ∀a:A. a ∈ U → (∀j: i ? a. ex_such A U (C ? a j) (fish A U)) → fish A U a.
 
 notation "hvbox(a break ⋉ b)" non associative with precedence 45
 for @{ 'fish $a $b }. (* a \ltimes b *)
 
-interpretation "fishl" 'fish A U = (ex_such _ U A (fish _ U)).
-interpretation "fish" 'fish a U = (fish _ U a).
+interpretation "fishl" 'fish A U = (ex_such ? U A (fish ? U)).
+interpretation "fish" 'fish a U = (fish ? U a).
 
-let corec fish_rec (A:axiom_set) (U: 2 \sup A)
- (P: 2 \sup A) (H1: ∀a:A. a ∈ P → a ∈ U)
+let corec fish_rec (A:axiom_set) (U: \Omega \sup A)
+ (P: Ω \sup A) (H1: P ⊆ U)
   (H2: ∀a:A. a ∈ P → ∀j: i ? a. C ? a j ≬ P):
    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝
  λa,p.
@@ -152,6 +109,24 @@ theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a 
        assumption]]
 qed.
 
+theorem covers_elim2:
+ ∀A: axiom_set. ∀U:Ω \sup A.∀P: A → CProp.
+  (∀a:A. a ∈ U → P a) →
+   (∀a:A.∀V:Ω \sup A. a ◃ V → V ◃ U → (∀y. y ∈ V → P y) → P a) →
+     ∀a:A. a ◃ U → P a.
+ intros;
+ change with (a ∈ {a | P a});
+ apply (covers_elim ?????? H2);
+  [ intros 2; simplify; apply H; assumption
+  | intros;
+    simplify in H4 ⊢ %;
+    apply H1;
+     [ apply (C ? a1 j);
+     | autobatch; 
+     | assumption;
+     | assumption]]
+qed.
+
 theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
  intros;
  cases H;
@@ -172,20 +147,14 @@ theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U 
  generalize in match H; clear H; 
  apply (covers_elim ?? {a|a ⋉ V → U ⋉ V} ??? H1);
  clear H1; simplify; intros;
-  [ exists [apply a1] assumption
+  [ exists [apply x] assumption
   | cases H2 in j H H1; clear H2 a1; intros; 
     cases (H1 i); clear H1; apply (H3 a1); assumption]
 qed.
 
-definition singleton ≝ λA:axiom_set.λa:A.{b | a=b}.
-
-notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}.
 
-interpretation "singleton" 'singl a = (singleton _ a).
-
-definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {b}.
-
-interpretation "covered by one" 'leq a b = (leq _ a b).
+interpretation "covered by one" 'leq a b = (leq ? a b).
 
 theorem leq_refl: ∀A:axiom_set.∀a:A. a ≤ a.
  intros;
@@ -207,24 +176,17 @@ qed.
 
 definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
 
-notation "↑a" with precedence 80 for @{ 'uparrow $a }.
-
-interpretation "uparrow" 'uparrow a = (uparrow _ a).
+interpretation "uparrow" 'uparrow a = (uparrow ? a).
 
-definition downarrow ≝ λA:axiom_set.λU:2 \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
+definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. (↑a) ≬ U).
 
-notation "↓a" with precedence 80 for @{ 'downarrow $a }.
+interpretation "downarrow" 'downarrow a = (downarrow ? a).
 
-interpretation "downarrow" 'downarrow a = (downarrow _ a).
+definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
 
-definition fintersects ≝ λA:axiom_set.λU,V:2 \sup A.↓U ∩ ↓V.
-
-notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }.
-
-interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
+interpretation "fintersects" 'fintersects U V = (fintersects ? U V).
 
 record convergent_generated_topology : Type ≝
  { AA:> axiom_set;
-   convergence: ∀a:AA.∀U,V:2 \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
+   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
  }.
-