X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flimits%2Fetc%2FSubset%2Fdefs.etc;fp=matita%2Fmatita%2Fcontribs%2Flimits%2Fetc%2FSubset%2Fdefs.etc;h=729bdaba94cf87b1c779d9809628e7359cd63f7c;hb=34c69f5b13b3aafd36d2e8a7e36a96e0748c7938;hp=0000000000000000000000000000000000000000;hpb=59c3713b93251505ba4e00b2695bffe2dfaf3bc7;p=helm.git

diff --git a/matita/matita/contribs/limits/etc/Subset/defs.etc b/matita/matita/contribs/limits/etc/Subset/defs.etc
new file mode 100644
index 000000000..729bdaba9
--- /dev/null
+++ b/matita/matita/contribs/limits/etc/Subset/defs.etc
@@ -0,0 +1,138 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "Domain/defs.ma".
+
+(* SUBSETS
+   - We use predicative subsets encoded as propositional functions
+     according to Sambin/Valentini "Toolbox".
+*)
+
+record Subset (D:Domain): Type ≝ {
+   subset       :1> D → Prop;
+   ces_subset_fw:   ∀d1,d2. subset d1 → ces ? d1 d2 → subset d2;
+   ces_subset_bw:   ∀d1,d2. subset d1 → ces ? d2 d1 → subset d2
+}.
+
+(* subset membership (epsilon) ********************************************)
+
+definition sin: ∀D. Subset D → D → Prop ≝
+   λD. λU:Subset D. λd. cin D d ∧ U d.
+
+theorem sin_i: ∀D. ∀U:Subset D. ∀d. cin D d → U d → sin ? U d.
+ unfold sin; intros; autobatch.
+qed.
+
+theorem sin_e1: ∀D. ∀U:Subset D. ∀d. sin ? U d → cin D d.
+ intros; decompose; autobatch.
+qed.
+
+theorem sin_e2: ∀D. ∀U:Subset D. ∀d. sin ? U d → U d.
+ intros; decompose; autobatch.
+qed.
+
+(* the domain built upon a subset *****************************************)
+
+theorem ces_sin_fw: ∀D,U,d1,d2. sin D U d1 → ces ? d1 d2 → sin D U d2.
+ intros; 
+ apply sin_i; 
+ [ autobatch
+ | apply (ces_subset_fw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
+ ]. 
+qed.
+
+theorem ces_sin_bw: ∀D,U,d1,d2. sin D U d1 → ces ? d2 d1 → sin D U d2.
+ intros; 
+ apply sin_i; 
+ [ autobatch
+ | apply (ces_subset_bw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
+ ]. 
+qed.
+
+definition domain_of_subset: ∀D. Subset D → Domain ≝
+   λD:Domain. λU.
+   mk_Domain (mk_Class D (sin D U) (ces D) (ces_sin_fw ? ?) (ces_sin_bw ? ?)).
+
+coercion domain_of_subset.
+
+(* subset top (full subset) ***********************************************)
+
+definition stop: ∀D. Subset D ≝
+   λD. mk_Subset D (true_f ?) (true_fw ? ?) (true_bw ? ?).
+
+coercion stop nocomposites.
+
+(* subset bottom (empty subset) *******************************************)
+
+definition sbot: ∀D. Subset D ≝
+   λD. mk_Subset D (false_f ?) (false_fw ? ?) (false_bw ? ?).
+
+(* subset and (binary intersection) ***************************************)
+
+theorem ces_sand_fw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d1 d2 → U1 d2 ∧ U2 d2.
+ intros; decompose; apply conj;
+ [ apply (ces_subset_fw D U1 d1); autobatch (**)
+ | apply (ces_subset_fw D U2 d1); autobatch
+ ].
+qed.
+
+theorem ces_sand_bw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d2 d1 → U1 d2 ∧ U2 d2.
+ intros; decompose; apply conj;
+ [ apply (ces_subset_bw D U1 d1); autobatch (**)
+ | apply (ces_subset_bw D U2 d1); autobatch
+ ].
+qed.
+
+definition sand: ∀D. Subset D → Subset D → Subset D ≝
+   λD,U1,U2. 
+   mk_Subset D (λd. U1 d ∧ U2 d) (ces_sand_fw ? U1 U2) (ces_sand_bw ? U1 U2).
+
+(* subset or (binary union) ***********************************************)
+
+theorem ces_sor_fw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d1 d2 → U1 d2 ∨ U2 d2.
+ intros; decompose;
+ [ apply or_introl; apply (ces_subset_fw D U1 d1); autobatch (**)
+ | apply or_intror; apply (ces_subset_fw D U2 d1); autobatch
+ ].
+qed.
+
+theorem ces_sor_bw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d2 d1 → U1 d2 ∨ U2 d2.
+ intros; decompose;
+ [ apply or_introl; apply (ces_subset_bw D U1 d1); autobatch (**)
+ | apply or_intror; apply (ces_subset_bw D U2 d1); autobatch
+ ].
+qed.
+
+definition sor: ∀D. Subset D → Subset D → Subset D ≝
+   λD,U1,U2. 
+   mk_Subset D (λd. U1 d ∨ U2 d) (ces_sor_fw ? U1 U2) (ces_sor_bw ? U1 U2).
+
+(* subset less or equal (inclusion) ***************************************)
+
+definition sle: ∀D. Subset D → Subset D → Prop ≝
+   λD. λU1,U2:Subset D. \iforall d. U1 d → U2 d. 
+
+(* subset overlap *********************************************************)
+
+definition sover: ∀D. Subset D → Subset D → Prop ≝
+   λD. λU1,U2:Subset D. \iexists d. U1 d ∧ U2 d. 
+
+(* the class of the subsets of a domain ***********************************)
+
+definition power: Domain → Class ≝
+   λD. mk_Class (Subset D) (true_f ?) (sle ?) (true_fw ? ?) (true_bw ? ?).