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 coded as propositional functions
  19      according to G.Sambin and S.Valentini "Toolbox".
  20 *)
  21
  22 definition Subset ≝ λD:Domain. D → Prop.
  23
  24 (* subset membership (epsilon) *)
  25 definition sin : ∀D. Subset D → D → Prop ≝
  26    λD:Domain. λU,d. cin D d ∧ U d.
  27
  28 (* subset top (full subset) *)
  29 definition stop ≝ λD:Domain. true_f D.
  30
  31 (* subset bottom (empty subset) *)
  32 definition sbot ≝ λD:Domain. false_f D.
  33
  34 (* subset and (binary intersection) *)
  35 definition sand: ∀D. Subset D → Subset D → Subset D ≝
  36    λD,U1,U2,d. U1 d ∧ U2 d.
  37
  38 (* subset or (binary union) *)
  39 definition sor: ∀D. Subset D → Subset D → Subset D ≝
  40    λD,U1,U2,d. U1 d ∨ U2 d.
  41
  42 (* subset less or equal (inclusion) *)
  43 definition sle: ∀D. Subset D → Subset D → Prop ≝
  44    λD,U1,U2. \iforall d. U1 d → U2 d.
  45
  46 (* subset overlap *)
  47 definition sover: ∀D. Subset D → Subset D → Prop ≝
  48    λD,U1,U2. \iexists d. U1 d ∧ U2 d.
  49
  50 (* coercions **************************************************************)
  51
  52 (*
  53 (* the class of the subsets of a domain (not an implicit coercion) *)
  54 definition class_of_subsets_of \def
  55    \lambda D. mk_Class (Subset D) (true_f ?) (sle ?).
  56 *)
  57
  58 (* the domain built upon a subset (not an implicit coercion) *)
  59 definition domain_of_subset: ∀D. Subset D \to Domain ≝
  60    λD:Domain. λU. mk_Domain (mk_Class D (sin D U) (ces D)).
  61
  62 (* the full subset of a domain *)
  63 coercion stop.