From c65d9defbebaf4e2e4135c669496a2a8ec3943aa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 4 Sep 2008 10:03:22 +0000 Subject: [PATCH] removed old non-working file --- .../matita/library/demo/formal_topology.ma | 158 ------------------ 1 file changed, 158 deletions(-) delete mode 100644 helm/software/matita/library/demo/formal_topology.ma diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma deleted file mode 100644 index 67f0ffa54..000000000 --- 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 - }. - -- 2.39.2