]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/limits/Subset/defs.ma
milestone update in ground
[helm.git] / matitaB / 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 ? ?).