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

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 6a3235445..a68378408 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -19,6 +19,12 @@ inductive And (A,B:CProp) : CProp ≝
  
 interpretation "constructive and" 'and x y = (And x y).
 
+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).
+
 inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝
   ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
 
@@ -29,6 +35,14 @@ for @{ 'powerset $A }.
 
 interpretation "powerset" 'powerset A = (powerset A).
 
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
+
 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
@@ -36,11 +50,39 @@ for @{ 'mem $a $b }.
 
 interpretation "mem" 'mem a S = (mem _ S a).
 
-record axiom_set : Type ≝
- { A:> Type;
-   i: A → Type;
-   C: ∀a:A. i a → 2 \sup 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).
+
+record axiom_set : Type ≝ { 
+  A:> Type;
+  i: A → Type;
+  C: ∀a:A. i a → 2 \sup A
+}.
 
 inductive for_all (A: axiom_set) (U,V: 2 \sup A) (covers: A → CProp) : CProp ≝
    iter: (∀a:A.a ∈ V → covers a) → for_all A U V covers.
@@ -58,13 +100,13 @@ 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.
-   λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → b ∈ P) → a ∈ 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
       [ refl a q ⇒ H1 a q
       | infinity a j q ⇒
          H2 a j q
-          match q return λ_:(C ? a j) ◃ U.∀b. b ∈ (C ? a j) → b ∈ P with
+          match q return λ_:(C ? a j) ◃ U. C ? a j ⊆ P with
           [ iter f ⇒ λb.λr. aux b (f b r) ]]
     in
      aux.
@@ -83,7 +125,7 @@ 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)
-  (H2: ∀a:A. a ∈ P → ∀j: i ? a. exT2 ? (λy.y ∈ C ? a j) (λy.y ∈ P)) :
+  (H2: ∀a:A. a ∈ P → ∀j: i ? a. C ? a j ≬ P):
    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝
  λa,p.
   mk_fish A U a
@@ -102,7 +144,7 @@ qed.
 
 theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
  intros;
- apply (covers_elim ?? (mk_powerset A (λa.a ◃ V)) ??? H); simplify; intros;
+ apply (covers_elim ?? {a | a ◃ V} ??? H); simplify; intros;
   [ cases H1 in H2; apply H2;
   | apply infinity;
      [ assumption
@@ -119,7 +161,7 @@ qed.
 theorem cotransitivity:
  ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V.
  intros;
- apply (fish_rec ?? (mk_powerset A (λa.a ⋉ U)) ??? H); simplify; intros;
+ apply (fish_rec ?? {a|a ⋉ U} ??? H); simplify; intros;
   [ apply H1; apply H2;
   | cases H2 in j; clear H2; intro i;
     cases (H4 i); clear H4; exists[apply a3] assumption]
@@ -128,14 +170,14 @@ qed.
 theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
  intros;
  generalize in match H; clear H; 
- apply (covers_elim ?? (mk_powerset A (λa.a ⋉ V → U ⋉ V)) ??? H1);
+ apply (covers_elim ?? {a|a ⋉ V → U ⋉ V} ??? H1);
  clear H1; simplify; intros;
   [ exists [apply a1] 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.mk_powerset ? (λb:A.a=b).
+definition singleton ≝ λA:axiom_set.λa:A.{b | a=b}.
 
 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
 
@@ -169,20 +211,6 @@ notation "↑a" with precedence 80 for @{ 'uparrow $a }.
 
 interpretation "uparrow" 'uparrow a = (uparrow _ 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 }.
-
-interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
-
-definition intersects ≝ λA:Type.λU,V:2 \sup A.mk_powerset ? (λa:A. a ∈ U ∧ a ∈ V).
-
-notation "hvbox(a break ∩ b)" non associative with precedence 55
-for @{ 'intersects $a $b }.
-
-interpretation "intersects" 'intersects U V = (intersects _ U V).
-
 definition downarrow ≝ λA:axiom_set.λU:2 \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
 
 notation "↓a" with precedence 80 for @{ 'downarrow $a }.