6 |
6 |
7 theory Quotient_Set |
7 theory Quotient_Set |
8 imports Main Quotient_Syntax |
8 imports Main Quotient_Syntax |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Relator for set type *} |
11 subsection {* Contravariant set map (vimage) and set relator, rules for the Quotient package *} |
12 |
|
13 definition set_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" |
|
14 where "set_rel R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))" |
|
15 |
|
16 lemma set_relI: |
|
17 assumes "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. R x y" |
|
18 assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. R x y" |
|
19 shows "set_rel R A B" |
|
20 using assms unfolding set_rel_def by simp |
|
21 |
|
22 lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)" |
|
23 unfolding set_rel_def by auto |
|
24 |
|
25 lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)" |
|
26 unfolding set_rel_def fun_eq_iff by auto |
|
27 |
|
28 lemma set_rel_mono[relator_mono]: |
|
29 assumes "A \<le> B" |
|
30 shows "set_rel A \<le> set_rel B" |
|
31 using assms unfolding set_rel_def by blast |
|
32 |
|
33 lemma set_rel_OO[relator_distr]: "set_rel R OO set_rel S = set_rel (R OO S)" |
|
34 apply (rule sym) |
|
35 apply (intro ext, rename_tac X Z) |
|
36 apply (rule iffI) |
|
37 apply (rule_tac b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}" in relcomppI) |
|
38 apply (simp add: set_rel_def, fast) |
|
39 apply (simp add: set_rel_def, fast) |
|
40 apply (simp add: set_rel_def, fast) |
|
41 done |
|
42 |
|
43 lemma Domainp_set[relator_domain]: |
|
44 assumes "Domainp T = R" |
|
45 shows "Domainp (set_rel T) = (\<lambda>A. Ball A R)" |
|
46 using assms unfolding set_rel_def Domainp_iff[abs_def] |
|
47 apply (intro ext) |
|
48 apply (rule iffI) |
|
49 apply blast |
|
50 apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast) |
|
51 done |
|
52 |
|
53 lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)" |
|
54 unfolding reflp_def set_rel_def by fast |
|
55 |
|
56 lemma left_total_set_rel[reflexivity_rule]: |
|
57 "left_total A \<Longrightarrow> left_total (set_rel A)" |
|
58 unfolding left_total_def set_rel_def |
|
59 apply safe |
|
60 apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast) |
|
61 done |
|
62 |
|
63 lemma left_unique_set_rel[reflexivity_rule]: |
|
64 "left_unique A \<Longrightarrow> left_unique (set_rel A)" |
|
65 unfolding left_unique_def set_rel_def |
|
66 by fast |
|
67 |
|
68 lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)" |
|
69 unfolding symp_def set_rel_def by fast |
|
70 |
|
71 lemma transp_set_rel: "transp R \<Longrightarrow> transp (set_rel R)" |
|
72 unfolding transp_def set_rel_def by fast |
|
73 |
|
74 lemma equivp_set_rel: "equivp R \<Longrightarrow> equivp (set_rel R)" |
|
75 by (blast intro: equivpI reflp_set_rel symp_set_rel transp_set_rel |
|
76 elim: equivpE) |
|
77 |
|
78 lemma right_total_set_rel [transfer_rule]: |
|
79 "right_total A \<Longrightarrow> right_total (set_rel A)" |
|
80 unfolding right_total_def set_rel_def |
|
81 by (rule allI, rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast) |
|
82 |
|
83 lemma right_unique_set_rel [transfer_rule]: |
|
84 "right_unique A \<Longrightarrow> right_unique (set_rel A)" |
|
85 unfolding right_unique_def set_rel_def by fast |
|
86 |
|
87 lemma bi_total_set_rel [transfer_rule]: |
|
88 "bi_total A \<Longrightarrow> bi_total (set_rel A)" |
|
89 unfolding bi_total_def set_rel_def |
|
90 apply safe |
|
91 apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast) |
|
92 apply (rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast) |
|
93 done |
|
94 |
|
95 lemma bi_unique_set_rel [transfer_rule]: |
|
96 "bi_unique A \<Longrightarrow> bi_unique (set_rel A)" |
|
97 unfolding bi_unique_def set_rel_def by fast |
|
98 |
|
99 subsection {* Transfer rules for transfer package *} |
|
100 |
|
101 subsubsection {* Unconditional transfer rules *} |
|
102 |
|
103 lemma empty_transfer [transfer_rule]: "(set_rel A) {} {}" |
|
104 unfolding set_rel_def by simp |
|
105 |
|
106 lemma insert_transfer [transfer_rule]: |
|
107 "(A ===> set_rel A ===> set_rel A) insert insert" |
|
108 unfolding fun_rel_def set_rel_def by auto |
|
109 |
|
110 lemma union_transfer [transfer_rule]: |
|
111 "(set_rel A ===> set_rel A ===> set_rel A) union union" |
|
112 unfolding fun_rel_def set_rel_def by auto |
|
113 |
|
114 lemma Union_transfer [transfer_rule]: |
|
115 "(set_rel (set_rel A) ===> set_rel A) Union Union" |
|
116 unfolding fun_rel_def set_rel_def by simp fast |
|
117 |
|
118 lemma image_transfer [transfer_rule]: |
|
119 "((A ===> B) ===> set_rel A ===> set_rel B) image image" |
|
120 unfolding fun_rel_def set_rel_def by simp fast |
|
121 |
|
122 lemma UNION_transfer [transfer_rule]: |
|
123 "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) UNION UNION" |
|
124 unfolding SUP_def [abs_def] by transfer_prover |
|
125 |
|
126 lemma Ball_transfer [transfer_rule]: |
|
127 "(set_rel A ===> (A ===> op =) ===> op =) Ball Ball" |
|
128 unfolding set_rel_def fun_rel_def by fast |
|
129 |
|
130 lemma Bex_transfer [transfer_rule]: |
|
131 "(set_rel A ===> (A ===> op =) ===> op =) Bex Bex" |
|
132 unfolding set_rel_def fun_rel_def by fast |
|
133 |
|
134 lemma Pow_transfer [transfer_rule]: |
|
135 "(set_rel A ===> set_rel (set_rel A)) Pow Pow" |
|
136 apply (rule fun_relI, rename_tac X Y, rule set_relI) |
|
137 apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp) |
|
138 apply (simp add: set_rel_def, fast) |
|
139 apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp) |
|
140 apply (simp add: set_rel_def, fast) |
|
141 done |
|
142 |
|
143 lemma set_rel_transfer [transfer_rule]: |
|
144 "((A ===> B ===> op =) ===> set_rel A ===> set_rel B ===> op =) |
|
145 set_rel set_rel" |
|
146 unfolding fun_rel_def set_rel_def by fast |
|
147 |
|
148 |
|
149 subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *} |
|
150 |
|
151 lemma member_transfer [transfer_rule]: |
|
152 assumes "bi_unique A" |
|
153 shows "(A ===> set_rel A ===> op =) (op \<in>) (op \<in>)" |
|
154 using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast |
|
155 |
|
156 lemma right_total_Collect_transfer[transfer_rule]: |
|
157 assumes "right_total A" |
|
158 shows "((A ===> op =) ===> set_rel A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect" |
|
159 using assms unfolding right_total_def set_rel_def fun_rel_def Domainp_iff by fast |
|
160 |
|
161 lemma Collect_transfer [transfer_rule]: |
|
162 assumes "bi_total A" |
|
163 shows "((A ===> op =) ===> set_rel A) Collect Collect" |
|
164 using assms unfolding fun_rel_def set_rel_def bi_total_def by fast |
|
165 |
|
166 lemma inter_transfer [transfer_rule]: |
|
167 assumes "bi_unique A" |
|
168 shows "(set_rel A ===> set_rel A ===> set_rel A) inter inter" |
|
169 using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast |
|
170 |
|
171 lemma Diff_transfer [transfer_rule]: |
|
172 assumes "bi_unique A" |
|
173 shows "(set_rel A ===> set_rel A ===> set_rel A) (op -) (op -)" |
|
174 using assms unfolding fun_rel_def set_rel_def bi_unique_def |
|
175 unfolding Ball_def Bex_def Diff_eq |
|
176 by (safe, simp, metis, simp, metis) |
|
177 |
|
178 lemma subset_transfer [transfer_rule]: |
|
179 assumes [transfer_rule]: "bi_unique A" |
|
180 shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)" |
|
181 unfolding subset_eq [abs_def] by transfer_prover |
|
182 |
|
183 lemma right_total_UNIV_transfer[transfer_rule]: |
|
184 assumes "right_total A" |
|
185 shows "(set_rel A) (Collect (Domainp A)) UNIV" |
|
186 using assms unfolding right_total_def set_rel_def Domainp_iff by blast |
|
187 |
|
188 lemma UNIV_transfer [transfer_rule]: |
|
189 assumes "bi_total A" |
|
190 shows "(set_rel A) UNIV UNIV" |
|
191 using assms unfolding set_rel_def bi_total_def by simp |
|
192 |
|
193 lemma right_total_Compl_transfer [transfer_rule]: |
|
194 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" |
|
195 shows "(set_rel A ===> set_rel A) (\<lambda>S. uminus S \<inter> Collect (Domainp A)) uminus" |
|
196 unfolding Compl_eq [abs_def] |
|
197 by (subst Collect_conj_eq[symmetric]) transfer_prover |
|
198 |
|
199 lemma Compl_transfer [transfer_rule]: |
|
200 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" |
|
201 shows "(set_rel A ===> set_rel A) uminus uminus" |
|
202 unfolding Compl_eq [abs_def] by transfer_prover |
|
203 |
|
204 lemma right_total_Inter_transfer [transfer_rule]: |
|
205 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" |
|
206 shows "(set_rel (set_rel A) ===> set_rel A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter" |
|
207 unfolding Inter_eq[abs_def] |
|
208 by (subst Collect_conj_eq[symmetric]) transfer_prover |
|
209 |
|
210 lemma Inter_transfer [transfer_rule]: |
|
211 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" |
|
212 shows "(set_rel (set_rel A) ===> set_rel A) Inter Inter" |
|
213 unfolding Inter_eq [abs_def] by transfer_prover |
|
214 |
|
215 lemma filter_transfer [transfer_rule]: |
|
216 assumes [transfer_rule]: "bi_unique A" |
|
217 shows "((A ===> op=) ===> set_rel A ===> set_rel A) Set.filter Set.filter" |
|
218 unfolding Set.filter_def[abs_def] fun_rel_def set_rel_def by blast |
|
219 |
|
220 lemma bi_unique_set_rel_lemma: |
|
221 assumes "bi_unique R" and "set_rel R X Y" |
|
222 obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)" |
|
223 proof |
|
224 let ?f = "\<lambda>x. THE y. R x y" |
|
225 from assms show f: "\<forall>x\<in>X. R x (?f x)" |
|
226 apply (clarsimp simp add: set_rel_def) |
|
227 apply (drule (1) bspec, clarify) |
|
228 apply (rule theI2, assumption) |
|
229 apply (simp add: bi_unique_def) |
|
230 apply assumption |
|
231 done |
|
232 from assms show "Y = image ?f X" |
|
233 apply safe |
|
234 apply (clarsimp simp add: set_rel_def) |
|
235 apply (drule (1) bspec, clarify) |
|
236 apply (rule image_eqI) |
|
237 apply (rule the_equality [symmetric], assumption) |
|
238 apply (simp add: bi_unique_def) |
|
239 apply assumption |
|
240 apply (clarsimp simp add: set_rel_def) |
|
241 apply (frule (1) bspec, clarify) |
|
242 apply (rule theI2, assumption) |
|
243 apply (clarsimp simp add: bi_unique_def) |
|
244 apply (simp add: bi_unique_def, metis) |
|
245 done |
|
246 show "inj_on ?f X" |
|
247 apply (rule inj_onI) |
|
248 apply (drule f [rule_format]) |
|
249 apply (drule f [rule_format]) |
|
250 apply (simp add: assms(1) [unfolded bi_unique_def]) |
|
251 done |
|
252 qed |
|
253 |
|
254 lemma finite_transfer [transfer_rule]: |
|
255 "bi_unique A \<Longrightarrow> (set_rel A ===> op =) finite finite" |
|
256 by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, |
|
257 auto dest: finite_imageD) |
|
258 |
|
259 lemma card_transfer [transfer_rule]: |
|
260 "bi_unique A \<Longrightarrow> (set_rel A ===> op =) card card" |
|
261 by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image) |
|
262 |
|
263 subsection {* Setup for lifting package *} |
|
264 |
|
265 lemma Quotient_set[quot_map]: |
|
266 assumes "Quotient R Abs Rep T" |
|
267 shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)" |
|
268 using assms unfolding Quotient_alt_def4 |
|
269 apply (simp add: set_rel_OO[symmetric] set_rel_conversep) |
|
270 apply (simp add: set_rel_def, fast) |
|
271 done |
|
272 |
|
273 lemma set_invariant_commute [invariant_commute]: |
|
274 "set_rel (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)" |
|
275 unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast |
|
276 |
|
277 subsection {* Contravariant set map (vimage) and set relator *} |
|
278 |
12 |
279 definition "vset_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys" |
13 definition "vset_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys" |
280 |
14 |
281 lemma vset_rel_eq [id_simps]: |
15 lemma vset_rel_eq [id_simps]: |
282 "vset_rel op = = op =" |
16 "vset_rel op = = op =" |