From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 9 Jul 2010 12:43:33 +0000 (+0000)
Subject: more notation
X-Git-Tag: make_still_working~2879
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5fee26d2afb3a67370c92481bfbfdbd9ebed741e;p=helm.git

more notation
---

diff --git a/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma
index ac137748f..fe4cbd10f 100644
--- a/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma
@@ -19,8 +19,7 @@ include "formal_topology/basic_topologies.ma".
 
 definition basic_topology_of_basic_pair: basic_pair → basic_topology.
  intro bp;
- letin obp ≝ (o_basic_pair_of_basic_pair bp);
- letin obt ≝ (o_basic_topology_of_o_basic_pair obp);
+ letin obt ≝ (OR (BP_to_OBP bp));
  constructor 1;
   [ apply (form bp);
   | apply (oA obt);
@@ -34,8 +33,7 @@ definition continuous_relation_of_relation_pair:
  ∀BP1,BP2.relation_pair BP1 BP2 →
   continuous_relation (basic_topology_of_basic_pair BP1) (basic_topology_of_basic_pair BP2).
  intros (BP1 BP2 rp);
- letin orp ≝ (o_relation_pair_of_relation_pair ?? rp);
- letin ocr ≝ (o_continuous_relation_of_o_relation_pair ?? orp);
+ letin ocr ≝ (OR⎽⇒ (BP_to_OBP⎽⇒ rp));
  constructor 1;
   [ apply (rp \sub \f);
   | apply (Oreduced ?? ocr);
diff --git a/helm/software/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma
index aee034683..2041cec40 100644
--- a/helm/software/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma
@@ -113,10 +113,8 @@ definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP).
   | apply o_relation_pair_of_relation_pair_morphism_respects_comp;]
 qed.
 
-theorem BP_to_OBP_faithful:
- ∀S,T.∀f,g:arrows2 (category2_of_category1 BP) S T.
-   BP_to_OBP⎽⇒ f = BP_to_OBP⎽⇒ g → f=g.
- intros; change with ( (⊩) ∘ f \sub \c = (⊩) ∘ g \sub \c);
+theorem BP_to_OBP_faithful: faithful2 ?? BP_to_OBP.
+ intros 5 (S T); change with ( (⊩) ∘ f \sub \c = (⊩) ∘ g \sub \c);
  apply (POW_faithful);
  apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) f \sub \c (⊩ \sub T));
  apply sym2;
@@ -125,9 +123,8 @@ theorem BP_to_OBP_faithful:
  apply e;
 qed.
 
-theorem BP_to_OBP_full: 
-   ∀S,T.∀f. exT22 ? (λg:arrows2 ? S T. BP_to_OBP⎽⇒ g = f).
- intros; 
+theorem BP_to_OBP_full: full2 ?? BP_to_OBP. 
+ intros 3 (S T); 
  cases (POW_full (concr S) (concr T) (Oconcr_rel ?? f)) (gc Hgc);
  cases (POW_full (form S) (form T) (Oform_rel ?? f)) (gf Hgf);
  exists[
diff --git a/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma
index 88f9e2393..b1592f6ea 100644
--- a/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma
+++ b/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma
@@ -41,7 +41,7 @@ intros (S T);
      | cases daemon (*apply (o_relation_pair_of_relation_pair_is_morphism S T)*)]
 qed.
 
-definition BTop_to_OBTop: carr3 (arrows3 CAT2 (category2_of_category1 BTop) OBTop).
+definition BTop_to_OBTop: carr3 ((category2_of_category1 BTop) ⇒_\c3 OBTop).
  constructor 1;
   [ apply o_basic_topology_of_basic_topology;
   | intros; apply o_continuous_relation_of_continuous_relation_morphism;
diff --git a/helm/software/matita/library/formal_topology/categories.ma b/helm/software/matita/library/formal_topology/categories.ma
index a9c2c9d9e..30769e536 100644
--- a/helm/software/matita/library/formal_topology/categories.ma
+++ b/helm/software/matita/library/formal_topology/categories.ma
@@ -413,6 +413,10 @@ coercion category2_of_objs3_CAT2.
 definition functor2_setoid_of_arrows3_CAT2: ∀S,T. arrows3 CAT2 S T → functor2_setoid S T ≝ λS,T,x.x.
 coercion functor2_setoid_of_arrows3_CAT2.
 
+notation > "B ⇒_\c3 C" right associative with precedence 72 for @{'arrows3_CAT $B $C}.
+notation "B ⇒\sub (\c 3) C" right associative with precedence 72 for @{'arrows3_CAT $B $C}.
+interpretation "'arrows3_CAT" 'arrows3_CAT A B = (arrows3 CAT2 A B).
+
 definition unary_morphism_setoid: setoid → setoid → setoid.
  intros;
  constructor 1;
@@ -496,3 +500,14 @@ coercion objs2_of_category1.
 
 prefer coercion Type_OF_setoid. (* we prefer the lower carrier projection *)
 prefer coercion Type_OF_objs1.
+
+alias symbol "exists" (instance 1) = "CProp2 exists".
+definition full2 ≝  
+  λA,B:CAT2.λF:carr3 (arrows3 CAT2 A B).
+    ∀o1,o2:A.∀f.∃g:arrows2 A o1 o2.F⎽⇒ g =_2 f.
+alias symbol "exists" (instance 1) = "CProp exists".
+    
+definition faithful2 ≝  
+  λA,B:CAT2.λF:carr3 (arrows3 CAT2 A B).
+    ∀o1,o2:A.∀f,g:arrows2 A o1 o2.F⎽⇒ f =_2 F⎽⇒ g → f =_2 g.
+    
diff --git a/helm/software/matita/library/formal_topology/o-algebra.ma b/helm/software/matita/library/formal_topology/o-algebra.ma
index ed363cd2d..67ff5140e 100644
--- a/helm/software/matita/library/formal_topology/o-algebra.ma
+++ b/helm/software/matita/library/formal_topology/o-algebra.ma
@@ -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 | 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/library/formal_topology/o-basic_pairs.ma b/helm/software/matita/library/formal_topology/o-basic_pairs.ma
index 3cd9699ac..e4bf8e5c7 100644
--- a/helm/software/matita/library/formal_topology/o-basic_pairs.ma
+++ b/helm/software/matita/library/formal_topology/o-basic_pairs.ma
@@ -179,6 +179,10 @@ definition Orelation_pair_setoid_of_arrows2_OBP:
   ∀P,Q.arrows2 OBP P Q → Orelation_pair_setoid P Q ≝ λP,Q,c.c.
 coercion Orelation_pair_setoid_of_arrows2_OBP.
 
+notation > "B ⇒_\obp2 C" right associative with precedence 72 for @{'arrows2_OBP $B $C}.
+notation "B ⇒\sub (\obp 2) C" right associative with precedence 72 for @{'arrows2_OBP $B $C}.
+interpretation "'arrows2_OBP" 'arrows2_OBP A B = (arrows2 OBP A B).
+
 (*
 definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
  intros; constructor 1;
diff --git a/helm/software/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma
index 1806408e0..fdd226f0f 100644
--- a/helm/software/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma
+++ b/helm/software/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma
@@ -59,8 +59,8 @@ definition o_basic_topology_of_o_basic_pair: OBP → OBTop.
 qed.
 
 definition o_continuous_relation_of_o_relation_pair:
- ∀BP1,BP2.arrows2 OBP BP1 BP2 →
-  arrows2 OBTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
+ ∀BP1,BP2.BP1 ⇒_\obp2 BP2 →
+  (o_basic_topology_of_o_basic_pair BP1) ⇒_\obt2 (o_basic_topology_of_o_basic_pair BP2).
  intros (BP1 BP2 t);
  constructor 1;
   [ apply (t \sub \f);
@@ -93,7 +93,7 @@ definition o_continuous_relation_of_o_relation_pair:
 qed.
 
 
-definition OR : carr3 (arrows3 CAT2 OBP OBTop).
+definition OR : carr3 (OBP ⇒_\c3 OBTop).
 constructor 1;
 [ apply o_basic_topology_of_o_basic_pair;
 | intros; constructor 1;
diff --git a/helm/software/matita/library/formal_topology/o-basic_topologies.ma b/helm/software/matita/library/formal_topology/o-basic_topologies.ma
index 03da27c41..4228e6450 100644
--- a/helm/software/matita/library/formal_topology/o-basic_topologies.ma
+++ b/helm/software/matita/library/formal_topology/o-basic_topologies.ma
@@ -157,6 +157,11 @@ definition Ocontinuous_relation_setoid_of_arrows2_OBTop :
   ∀P,Q. arrows2 OBTop P Q → Ocontinuous_relation_setoid P Q ≝ λP,Q,x.x.
 coercion Ocontinuous_relation_setoid_of_arrows2_OBTop.
 
+notation > "B ⇒_\obt2 C" right associative with precedence 72 for @{'arrows2_OBT $B $C}.
+notation "B ⇒\sub (\obt 2) C" right associative with precedence 72 for @{'arrows2_OBT $B $C}.
+interpretation "'arrows2_OBT" 'arrows2_OBT A B = (arrows2 OBTop A B).
+
+
 (*
 (*CSC: unused! *)
 (* this proof is more logic-oriented than set/lattice oriented *)
diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index 301e9487a..4b6c63635 100644
--- a/helm/software/matita/library/formal_topology/relations.ma
+++ b/helm/software/matita/library/formal_topology/relations.ma
@@ -108,7 +108,10 @@ coercion binary_relation_setoid_of_arrow1_REL.
 
 notation > "B ⇒_\r1 C" right associative with precedence 72 for @{'arrows1_REL $B $C}.
 notation "B ⇒\sub (\r 1) C" right associative with precedence 72 for @{'arrows1_REL $B $C}.
-interpretation "'arrows1_SET" 'arrows1_REL A B = (arrows1 REL A B).
+interpretation "'arrows1_REL" 'arrows1_REL A B = (arrows1 REL A B).
+notation > "B ⇒_\r2 C" right associative with precedence 72 for @{'arrows2_REL $B $C}.
+notation "B ⇒\sub (\r 2) C" right associative with precedence 72 for @{'arrows2_REL $B $C}.
+interpretation "'arrows2_REL" 'arrows2_REL A B = (arrows2 (category2_of_category1 REL) A B).
 
 
 definition full_subset: ∀s:REL. Ω^s.
diff --git a/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma b/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma
index 3a908657b..93bf2c609 100644
--- a/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma
+++ b/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma
@@ -170,10 +170,8 @@ definition POW: carr3 (arrows3 CAT2 (category2_of_category1 REL) OA).
   | apply orelation_of_relation_preserves_composition; ]
 qed.
 
-theorem POW_faithful:
- ∀S,T.∀f,g:arrows2 (category2_of_category1 REL) S T.
-   POW⎽⇒ f =_2 POW⎽⇒ g → f =_2 g.
- intros; unfold POW in e; simplify in e; cases e;
+theorem POW_faithful: faithful2 ?? POW.
+ intros 5; unfold POW in e; simplify in e; cases e;
  unfold orelation_of_relation in e3; simplify in e3; clear e e1 e2 e4;
  intros 2; cases (e3 {(x)}); 
  split; intro; [ lapply (s y); | lapply (s1 y); ]
@@ -181,13 +179,14 @@ theorem POW_faithful:
   |*: cases Hletin; cases x1; change in f3 with (x =_1 w); apply (. f3‡#); assumption;]
 qed.
 
-
+(*
 lemma currify: ∀A,B,C. (A × B ⇒_1 C) → A → (B ⇒_1 C).
 intros; constructor 1; [ apply (b c); | intros; apply (#‡e);]
 qed.
+*)
 
-theorem POW_full: ∀S,T.∀f: (POW S) ⇒_\o2 (POW T) . exT22 ? (λg. POW⎽⇒ g = f).
- intros; exists;
+theorem POW_full: full2 ?? POW. 
+ intros 3 (S T); exists;
   [ constructor 1; constructor 1;
      [ apply (λx:carr S.λy:carr T. y ∈ f {(x)});
      | intros; unfold FunClass_1_OF_carr2; lapply (.= e1‡#);