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.
33 (* subset bottom (empty subset) *)
34 definition sbot ≝ λD:Domain. false_f D.
36 (* subset and (binary intersection) *)
37 definition sand: ∀D. Subset D → Subset D → Subset D ≝
38 λD,U1,U2,d. U1 d ∧ U2 d.
40 (* subset or (binary union) *)
41 definition sor: ∀D. Subset D → Subset D → Subset D ≝
42 λD,U1,U2,d. U1 d ∨ U2 d.
44 (* subset less or equal (inclusion) *)
45 definition sle: ∀D. Subset D → Subset D → Prop ≝
46 λD,U1,U2. \iforall d. U1 d → U2 d.
49 definition sover: ∀D. Subset D → Subset D → Prop ≝
50 λD,U1,U2. \iexists d. U1 d ∧ U2 d.
52 (* the class of the subsets of a domain *)
53 definition subsets_of_domain ≝
54 λD. mk_Class (Subset D) (true_f ?) (sle ?).
56 (* the domain built upon a subset *)
57 definition domain_of_subset: ∀D. Subset D → Domain ≝
58 λD:Domain. λU. mk_Domain (mk_Class D (sin D U) (ces D)).