removed old non-working file

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
deleted file mode 100644 (file)
index 67f0ffa..0000000
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ /dev/null
@@ -1,158 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "datatypes/subsets.ma".
-
-record axiom_set : Type ≝ { 
-  A:> Type;
-  i: A → Type;
-  C: ∀a:A. i a → Ω \sup A
-}.
-
-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: \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).
-
-definition covers_elim ≝
- λ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
-      [ refl a q ⇒ H1 a q
-      | infinity a j q ⇒
-         H2 a j q
-          match q return λ_:(C ? a j) ◃ U. C ? a j ⊆ P with
-          [ iter f ⇒ λb.λr. aux b (f b r) ]]
-    in
-     aux.
-
-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: \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).
-
-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.
-  mk_fish A U a
-   (H1 ? p)
-   (λj: i ? a.
-    match H2 a p j with
-     [ ex_introT2 (y: A) (HyC : y ∈ C ? a j) (HyP : y ∈ P) ⇒
-         found ???? y HyC (fish_rec A U P H1 H2 y HyP)
-     ]).
-
-theorem reflexivity: ∀A:axiom_set.∀a:A.∀V. a ∈ V → a ◃ V.
- intros;
- apply refl;
- assumption.
-qed.
-
-theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
- intros;
- apply (covers_elim ?? {a | a ◃ V} ??? H); simplify; intros;
-  [ cases H1 in H2; apply H2;
-  | apply infinity;
-     [ assumption
-     | constructor 1;
-       assumption]]
-qed.
-
-theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
- intros;
- cases H;
- assumption.
-qed.
-
-theorem cotransitivity:
- ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V.
- 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]
-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 ?? {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 leq ≝ λA:axiom_set.λa,b:A. a ◃ {b}.
-
-interpretation "covered by one" 'leq a b = (leq _ a b).
-
-theorem leq_refl: ∀A:axiom_set.∀a:A. a ≤ a.
- intros;
- apply refl;
- normalize;
- reflexivity.
-qed.
-
-theorem leq_trans: ∀A:axiom_set.∀a,b,c:A. a ≤ b → b ≤ c → a ≤ c.
- intros;
- unfold in H H1 ⊢ %;
- apply (transitivity ???? H);
- constructor 1;
- intros;
- normalize in H2;
- rewrite < H2;
- assumption.
-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).
-
-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).
-
-definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
-
-interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
-
-record convergent_generated_topology : Type ≝
- { AA:> axiom_set;
-   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
- }.
-