From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 4 Jul 2008 15:31:22 +0000 (+0000)
Subject: More definitions, following Ciraulo's Phd Thesis "Constructive Satisfiability".
X-Git-Tag: make_still_working~4955
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d57b04c45c3dafa7b56a3dc2019c2ab0de730406;p=helm.git

More definitions, following Ciraulo's Phd Thesis "Constructive Satisfiability".
---

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index ca544b598..50671aa41 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -147,4 +147,70 @@ theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U 
     cases (H4 i); clear H4; cases H; clear H;
     apply (H2 w); clear H2;
     assumption]
-qed.
\ No newline at end of file
+qed.
+
+definition singleton ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A.a=b).
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+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).
+
+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 overlaps ≝ λA:Type.λU,V:2 \sup A.∃a:A. a ∈ U ∧ 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 }.
+
+interpretation "downarrow" 'downarrow a = (downarrow _ a).
+
+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).
+
+record convergent_generated_topology : Type ≝
+ { AA:> axiom_set;
+   convergence: ∀a:AA.∀U,V:2 \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
+ }.
+