helm/software/matita/contribs/limits/Subset/defs.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "Domain/defs.ma".
  16
  17 (* SUBSETS
  18    - We use predicative subsets encoded as propositional functions
  19      according to Sambin/Valentini "Toolbox".
  20 *)
  21
  22 record Subset (D:Domain): Type ≝ {
  23    subset       :1> D → Prop;
  24    ces_subset_fw:   ∀d1,d2. subset d1 → ces ? d1 d2 → subset d2;
  25    ces_subset_bw:   ∀d1,d2. subset d1 → ces ? d2 d1 → subset d2
  26 }.
  27
  28 (* subset membership (epsilon) ********************************************)
  29
  30 definition sin: ∀D. Subset D → D → Prop ≝
  31    λD. λU:Subset D. λd. cin D d ∧ U d.
  32
  33 theorem sin_i: ∀D. ∀U:Subset D. ∀d. cin D d → U d → sin ? U d.
  34  unfold sin; intros; autobatch.
  35 qed.
  36
  37 theorem sin_e1: ∀D. ∀U:Subset D. ∀d. sin ? U d → cin D d.
  38  intros; decompose; autobatch.
  39 qed.
  40
  41 theorem sin_e2: ∀D. ∀U:Subset D. ∀d. sin ? U d → U d.
  42  intros; decompose; autobatch.
  43 qed.
  44
  45 (* the domain built upon a subset *****************************************)
  46
  47 theorem ces_sin_fw: ∀D,U,d1,d2. sin D U d1 → ces ? d1 d2 → sin D U d2.
  48  intros;
  49  apply sin_i;
  50  [ autobatch
  51  | apply (ces_subset_fw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
  52  ].
  53 qed.
  54
  55 theorem ces_sin_bw: ∀D,U,d1,d2. sin D U d1 → ces ? d2 d1 → sin D U d2.
  56  intros;
  57  apply sin_i;
  58  [ autobatch
  59  | apply (ces_subset_bw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
  60  ].
  61 qed.
  62
  63 definition domain_of_subset: ∀D. Subset D → Domain ≝
  64    λD:Domain. λU.
  65    mk_Domain (mk_Class D (sin D U) (ces D) (ces_sin_fw ? ?) (ces_sin_bw ? ?)).
  66
  67 coercion domain_of_subset.
  68
  69 (* subset top (full subset) ***********************************************)
  70
  71 definition stop: ∀D. Subset D ≝
  72    λD. mk_Subset D (true_f ?) (true_fw ? ?) (true_bw ? ?).
  73
  74 coercion stop nocomposites.
  75
  76 (* subset bottom (empty subset) *******************************************)
  77
  78 definition sbot: ∀D. Subset D ≝
  79    λD. mk_Subset D (false_f ?) (false_fw ? ?) (false_bw ? ?).
  80
  81 (* subset and (binary intersection) ***************************************)
  82
  83 theorem ces_sand_fw:
  84    ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d1 d2 → U1 d2 ∧ U2 d2.
  85  intros; decompose; apply conj;
  86  [ apply (ces_subset_fw D U1 d1); autobatch (**)
  87  | apply (ces_subset_fw D U2 d1); autobatch
  88  ].
  89 qed.
  90
  91 theorem ces_sand_bw:
  92    ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d2 d1 → U1 d2 ∧ U2 d2.
  93  intros; decompose; apply conj;
  94  [ apply (ces_subset_bw D U1 d1); autobatch (**)
  95  | apply (ces_subset_bw D U2 d1); autobatch
  96  ].
  97 qed.
  98
  99 definition sand: ∀D. Subset D → Subset D → Subset D ≝
 100    λD,U1,U2.
 101    mk_Subset D (λd. U1 d ∧ U2 d) (ces_sand_fw ? U1 U2) (ces_sand_bw ? U1 U2).
 102
 103 (* subset or (binary union) ***********************************************)
 104
 105 theorem ces_sor_fw:
 106    ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d1 d2 → U1 d2 ∨ U2 d2.
 107  intros; decompose;
 108  [ apply or_introl; apply (ces_subset_fw D U1 d1); autobatch (**)
 109  | apply or_intror; apply (ces_subset_fw D U2 d1); autobatch
 110  ].
 111 qed.
 112
 113 theorem ces_sor_bw:
 114    ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d2 d1 → U1 d2 ∨ U2 d2.
 115  intros; decompose;
 116  [ apply or_introl; apply (ces_subset_bw D U1 d1); autobatch (**)
 117  | apply or_intror; apply (ces_subset_bw D U2 d1); autobatch
 118  ].
 119 qed.
 120
 121 definition sor: ∀D. Subset D → Subset D → Subset D ≝
 122    λD,U1,U2.
 123    mk_Subset D (λd. U1 d ∨ U2 d) (ces_sor_fw ? U1 U2) (ces_sor_bw ? U1 U2).
 124
 125 (* subset less or equal (inclusion) ***************************************)
 126
 127 definition sle: ∀D. Subset D → Subset D → Prop ≝
 128    λD. λU1,U2:Subset D. \iforall d. U1 d → U2 d.
 129
 130 (* subset overlap *********************************************************)
 131
 132 definition sover: ∀D. Subset D → Subset D → Prop ≝
 133    λD. λU1,U2:Subset D. \iexists d. U1 d ∧ U2 d.
 134
 135 (* the class of the subsets of a domain ***********************************)
 136
 137 definition power: Domain → Class ≝
 138    λD. mk_Class (Subset D) (true_f ?) (sle ?) (true_fw ? ?) (true_bw ? ?).