From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 30 Jun 2010 13:29:50 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~2889
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=95ac064b854f31a49f2f8cd3c4b4f4929dc96fc0;p=helm.git

...
---

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma
index 68212c2ee..f00abe8f4 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma
@@ -17,22 +17,14 @@ include "o-basic_topologies.ma".
 include "relations_to_o-algebra.ma".
 
 definition o_basic_topology_of_basic_topology: basic_topology → Obasic_topology.
- intro;
- constructor 1;
-  [ apply (POW' b);
-  | apply (A b);
-  | apply (J b);
-  | apply (A_is_saturation b);
-  | apply (J_is_reduction b);
-  | apply (compatibility b); ]
+ intros (b); constructor 1;
+  [ apply (POW' b) | apply (A b) | apply (J b);
+  | apply (A_is_saturation b) | apply (J_is_reduction b) | apply (compatibility b) ]
 qed.
 
 definition o_continuous_relation_of_continuous_relation:
  ∀BT1,BT2.continuous_relation BT1 BT2 →
   Ocontinuous_relation (o_basic_topology_of_basic_topology BT1) (o_basic_topology_of_basic_topology BT2).
- intros;
- constructor 1;
-  [ apply (orelation_of_relation ?? c);
-  | apply (reduced ?? c);
-  | apply (saturated ?? c); ]
+ intros (BT1 BT2 c); constructor 1;
+  [ apply (orelation_of_relation ?? c) | apply (reduced ?? c) | apply (saturated ?? c) ]
 qed.
\ No newline at end of file
diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index fc2ab9d4d..9cf55bacf 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -426,6 +426,8 @@ notation "A × term 74 B ⇒\sub 2 term 19 C" non associative with precedence 72
 notation "A × term 74 B ⇒\sub 3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
 notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
 notation "B ⇒\sub 2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
+notation "B ⇒\sub 1. C" right associative with precedence 72 for @{'arrows1_SETlow $B $C}.
+notation "B ⇒\sub 2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}.
 
 interpretation "'binary_morphism1" 'binary_morphism1 A B C = (binary_morphism1 A B C).
 interpretation "'binary_morphism2" 'binary_morphism2 A B C = (binary_morphism2 A B C).
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index c1d766f7e..915afc26d 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -53,8 +53,8 @@ interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \e
 (* USARE L'ESISTENZIALE DEBOLE *)
 
 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
-notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation > "'If' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation < "'If' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
 
 notation > "hvbox(a break ≤ b)" non associative with precedence 45 for @{oa_leq $a $b}.
@@ -80,7 +80,7 @@ record OAlgebra : Type2 := {
   oa_zero_bot: ∀p:oa_P.𝟘 ≤ p;
   oa_one_top: ∀p:oa_P.p ≤ 𝟙;
   oa_overlap_preserves_meet_: ∀p,q:oa_P.p >< q → 
-        p >< (⋀ { x ∈ BOOL | if x then p else q(*match x with [ true ⇒ p | false ⇒ q ]*) | IF_THEN_ELSE_p oa_P p q });
+        p >< (⋀ { x ∈ BOOL | If x then p else q(*match x with [ true ⇒ p | false ⇒ q ]*) | IF_THEN_ELSE_p oa_P p q });
   oa_join_split: ∀I:SET.∀p.∀q:I ⇒_2 oa_P.p >< (⋁ q) = (∃i:I.p >< (q i));
   (*oa_base : setoid;
   1) enum non e' il nome giusto perche' non e' suriettiva
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
index b74565256..80fec0348 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
@@ -64,30 +64,30 @@ definition o_continuous_relation_of_o_relation_pair:
  intros (BP1 BP2 t);
  constructor 1;
   [ apply (t \sub \f);
-  | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
+  | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros (U e);
     apply sym1;
-    apply (.= †(†e));
-    change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
-    cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
-      cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩)* U));]
+    apply (.= †(†e)); 
+    change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩\sub BP1)* U));
+    cut ((t \sub \f ∘ (⊩)) ((⊩\sub BP1)* U) = ((⊩) ∘ t \sub \c) ((⊩\sub BP1)* U)) as COM;[2:
+      cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩\sub BP1)* U));]
     apply (.= †COM);
     change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
-    apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
+    apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩\sub BP1)* U))));
     apply (.= COM ^ -1);
-    change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
+    change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩\sub BP1)* ) U));
     change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
     apply (†e^-1);
   | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
     apply sym1;
     apply (.= †(†e));
-    change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
-    cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
-      cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
+    change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩\sub BP1)⎻ U));
+    cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩\sub BP1)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩\sub BP1)⎻ U)) as COM;[2:
+      cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩\sub BP1)⎻ U));]
     apply (.= †COM);
     change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
-    apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
+    apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩\sub BP1)⎻ U))));
     apply (.= COM ^ -1);
-    change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
+    change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩\sub BP1)⎻ ) U));
     change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
     apply (†e^-1);]
 qed.
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
index 4c725920b..2fb7a6b1d 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
@@ -15,20 +15,17 @@
 include "o-algebra.ma".
 include "o-saturations.ma".
 
-record Obasic_topology: Type2 ≝
- { Ocarrbt:> OA;
-   oA: Ocarrbt ⇒_2 Ocarrbt;
-   oJ: Ocarrbt ⇒_2 Ocarrbt;
-   oA_is_saturation: is_o_saturation ? oA;
-   oJ_is_reduction: is_o_reduction ? oJ;
+record Obasic_topology: Type2 ≝ { 
+   Ocarrbt:> OA;
+   oA: Ocarrbt ⇒_2 Ocarrbt; oJ: Ocarrbt ⇒_2 Ocarrbt;
+   oA_is_saturation: is_o_saturation ? oA; oJ_is_reduction: is_o_reduction ? oJ;
    Ocompatibility: ∀U,V. (oA U >< oJ V) =_1 (U >< oJ V)
  }.
 
-record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝
- { Ocont_rel:> arrows2 OA S T;
-   (* reduces uses eq1, saturated uses eq!!! *)
-   Oreduced: ∀U. U = oJ ? U → Ocont_rel U = oJ ? (Ocont_rel U);
-   Osaturated: ∀U. U = oA ? U → Ocont_rel⎻* U = oA ? (Ocont_rel⎻* U)
+record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝ { 
+   Ocont_rel:> arrows2 OA S T;
+   Oreduced: ∀U:S. U = oJ ? U → Ocont_rel U =_1 oJ ? (Ocont_rel U);
+   Osaturated: ∀U:S. U = oA ? U → Ocont_rel⎻* U =_1 oA ? (Ocont_rel⎻* U)
  }. 
 
 definition Ocontinuous_relation_setoid: Obasic_topology → Obasic_topology → setoid2.
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma
index a1c83e709..bb193508e 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma
@@ -14,29 +14,23 @@
 
 include "o-algebra.ma".
 
-alias symbol "eq" = "setoid1 eq".
-definition is_o_saturation: ∀C:OA. unary_morphism1 C C → CProp1 ≝
- λC:OA.λA:unary_morphism1 C C.
-  ∀U,V. (U ≤ A V) = (A U ≤ A V).
+definition is_o_saturation: ∀C:OA. C ⇒_1 C → CProp1 ≝
+ λC:OA.λA:C ⇒_1 C.∀U,V. (U ≤ A V) =_1 (A U ≤ A V).
 
-definition is_o_reduction: ∀C:OA. unary_morphism1 C C → CProp1 ≝
- λC:OA.λJ:unary_morphism1 C C.
-    ∀U,V. (J U ≤ V) = (J U ≤ J V).
+definition is_o_reduction: ∀C:OA. C ⇒_1 C → CProp1 ≝
+ λC:OA.λJ:C ⇒_1 C.∀U,V. (J U ≤ V) =_1 (J U ≤ J V).
 
 theorem o_saturation_expansive: ∀C,A. is_o_saturation C A → ∀U. U ≤ A U.
  intros; apply (fi ?? (i ??)); apply (oa_leq_refl C).
 qed.
 
-theorem o_saturation_monotone:
- ∀C,A. is_o_saturation C A →
-  ∀U,V. U ≤ V → A U ≤ A V.
+theorem o_saturation_monotone: ∀C:OA.∀A:C ⇒_1 C. is_o_saturation C A → ∀U,V. U ≤ V → A U ≤ A V.
  intros; apply (if ?? (i ??)); apply (oa_leq_trans C);
   [apply V|3: apply o_saturation_expansive ]
  assumption.
 qed.
 
-theorem o_saturation_idempotent: ∀C,A. is_o_saturation C A → ∀U. 
- eq1 C (A (A U)) (A U).
+theorem o_saturation_idempotent: ∀C:OA.∀A:C ⇒_1 C. is_o_saturation C A → ∀U. A (A U) =_1 A U.
  intros; apply (oa_leq_antisym C);
   [ apply (if ?? (i (A U) U)); apply (oa_leq_refl C).
   | apply o_saturation_expansive; assumption]
diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
index 0a6700568..4cbca0530 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
@@ -18,16 +18,12 @@ include "relations_to_o-algebra.ma".
 
 (* These are only conversions :-) *)
 
-definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)).
- intros (C t);apply t;
-qed.
+definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)) ≝ λC,t.t.
 
-definition is_o_saturation_of_is_saturation: ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.
-  is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
- intros; apply i;
-qed.
+definition is_o_saturation_of_is_saturation: 
+  ∀C:REL.∀R: Ω^C ⇒_1 Ω^C. is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
+intros (C R i); apply i; qed.
 
-definition is_o_reduction_of_is_reduction: ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.
-  is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R).
- intros; apply i;
-qed.
\ No newline at end of file
+definition is_o_reduction_of_is_reduction: 
+  ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R).
+intros (C R i); apply i; qed.