1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "Domain/defs.ma".
18 - We use predicative subsets coded as propositional functions
19 according to G.Sambin and S.Valentini "Toolbox".
22 definition Subset ≝ λD:Domain. D → Prop.
24 (* subset membership (epsilon) *)
25 definition sin : ∀D. Subset D → D → Prop ≝
26 λD:Domain. λU,d. cin D d ∧ U d.
28 (* subset top (full subset) *)
29 definition stop ≝ λD:Domain. true_f D.
31 (* subset bottom (empty subset) *)
32 definition sbot ≝ λD:Domain. false_f D.
34 (* subset and (binary intersection) *)
35 definition sand: ∀D. Subset D → Subset D → Subset D ≝
36 λD,U1,U2,d. U1 d ∧ U2 d.
38 (* subset or (binary union) *)
39 definition sor: ∀D. Subset D → Subset D → Subset D ≝
40 λD,U1,U2,d. U1 d ∨ U2 d.
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.
47 definition sover: ∀D. Subset D → Subset D → Prop ≝
48 λD,U1,U2. \iexists d. U1 d ∧ U2 d.
50 (* coercions **************************************************************)
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 ?).
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)).
62 (* the full subset of a domain *)