|
1 (* Title: HOL/Lifting_Set.thy |
|
2 Author: Brian Huffman and Ondrej Kuncar |
|
3 *) |
|
4 |
|
5 header {* Setup for Lifting/Transfer for the set type *} |
|
6 |
|
7 theory Lifting_Set |
|
8 imports Lifting |
|
9 begin |
|
10 |
|
11 subsection {* Relator and predicator properties *} |
|
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 right_total_set_rel [transfer_rule]: |
|
69 "right_total A \<Longrightarrow> right_total (set_rel A)" |
|
70 unfolding right_total_def set_rel_def |
|
71 by (rule allI, rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast) |
|
72 |
|
73 lemma right_unique_set_rel [transfer_rule]: |
|
74 "right_unique A \<Longrightarrow> right_unique (set_rel A)" |
|
75 unfolding right_unique_def set_rel_def by fast |
|
76 |
|
77 lemma bi_total_set_rel [transfer_rule]: |
|
78 "bi_total A \<Longrightarrow> bi_total (set_rel A)" |
|
79 unfolding bi_total_def set_rel_def |
|
80 apply safe |
|
81 apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast) |
|
82 apply (rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast) |
|
83 done |
|
84 |
|
85 lemma bi_unique_set_rel [transfer_rule]: |
|
86 "bi_unique A \<Longrightarrow> bi_unique (set_rel A)" |
|
87 unfolding bi_unique_def set_rel_def by fast |
|
88 |
|
89 lemma set_invariant_commute [invariant_commute]: |
|
90 "set_rel (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)" |
|
91 unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast |
|
92 |
|
93 subsection {* Quotient theorem for the Lifting package *} |
|
94 |
|
95 lemma Quotient_set[quot_map]: |
|
96 assumes "Quotient R Abs Rep T" |
|
97 shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)" |
|
98 using assms unfolding Quotient_alt_def4 |
|
99 apply (simp add: set_rel_OO[symmetric] set_rel_conversep) |
|
100 apply (simp add: set_rel_def, fast) |
|
101 done |
|
102 |
|
103 subsection {* Transfer rules for the Transfer package *} |
|
104 |
|
105 subsubsection {* Unconditional transfer rules *} |
|
106 |
|
107 context |
|
108 begin |
|
109 interpretation lifting_syntax . |
|
110 |
|
111 lemma empty_transfer [transfer_rule]: "(set_rel A) {} {}" |
|
112 unfolding set_rel_def by simp |
|
113 |
|
114 lemma insert_transfer [transfer_rule]: |
|
115 "(A ===> set_rel A ===> set_rel A) insert insert" |
|
116 unfolding fun_rel_def set_rel_def by auto |
|
117 |
|
118 lemma union_transfer [transfer_rule]: |
|
119 "(set_rel A ===> set_rel A ===> set_rel A) union union" |
|
120 unfolding fun_rel_def set_rel_def by auto |
|
121 |
|
122 lemma Union_transfer [transfer_rule]: |
|
123 "(set_rel (set_rel A) ===> set_rel A) Union Union" |
|
124 unfolding fun_rel_def set_rel_def by simp fast |
|
125 |
|
126 lemma image_transfer [transfer_rule]: |
|
127 "((A ===> B) ===> set_rel A ===> set_rel B) image image" |
|
128 unfolding fun_rel_def set_rel_def by simp fast |
|
129 |
|
130 lemma UNION_transfer [transfer_rule]: |
|
131 "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) UNION UNION" |
|
132 unfolding SUP_def [abs_def] by transfer_prover |
|
133 |
|
134 lemma Ball_transfer [transfer_rule]: |
|
135 "(set_rel A ===> (A ===> op =) ===> op =) Ball Ball" |
|
136 unfolding set_rel_def fun_rel_def by fast |
|
137 |
|
138 lemma Bex_transfer [transfer_rule]: |
|
139 "(set_rel A ===> (A ===> op =) ===> op =) Bex Bex" |
|
140 unfolding set_rel_def fun_rel_def by fast |
|
141 |
|
142 lemma Pow_transfer [transfer_rule]: |
|
143 "(set_rel A ===> set_rel (set_rel A)) Pow Pow" |
|
144 apply (rule fun_relI, rename_tac X Y, rule set_relI) |
|
145 apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp) |
|
146 apply (simp add: set_rel_def, fast) |
|
147 apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp) |
|
148 apply (simp add: set_rel_def, fast) |
|
149 done |
|
150 |
|
151 lemma set_rel_transfer [transfer_rule]: |
|
152 "((A ===> B ===> op =) ===> set_rel A ===> set_rel B ===> op =) |
|
153 set_rel set_rel" |
|
154 unfolding fun_rel_def set_rel_def by fast |
|
155 |
|
156 |
|
157 subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *} |
|
158 |
|
159 lemma member_transfer [transfer_rule]: |
|
160 assumes "bi_unique A" |
|
161 shows "(A ===> set_rel A ===> op =) (op \<in>) (op \<in>)" |
|
162 using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast |
|
163 |
|
164 lemma right_total_Collect_transfer[transfer_rule]: |
|
165 assumes "right_total A" |
|
166 shows "((A ===> op =) ===> set_rel A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect" |
|
167 using assms unfolding right_total_def set_rel_def fun_rel_def Domainp_iff by fast |
|
168 |
|
169 lemma Collect_transfer [transfer_rule]: |
|
170 assumes "bi_total A" |
|
171 shows "((A ===> op =) ===> set_rel A) Collect Collect" |
|
172 using assms unfolding fun_rel_def set_rel_def bi_total_def by fast |
|
173 |
|
174 lemma inter_transfer [transfer_rule]: |
|
175 assumes "bi_unique A" |
|
176 shows "(set_rel A ===> set_rel A ===> set_rel A) inter inter" |
|
177 using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast |
|
178 |
|
179 lemma Diff_transfer [transfer_rule]: |
|
180 assumes "bi_unique A" |
|
181 shows "(set_rel A ===> set_rel A ===> set_rel A) (op -) (op -)" |
|
182 using assms unfolding fun_rel_def set_rel_def bi_unique_def |
|
183 unfolding Ball_def Bex_def Diff_eq |
|
184 by (safe, simp, metis, simp, metis) |
|
185 |
|
186 lemma subset_transfer [transfer_rule]: |
|
187 assumes [transfer_rule]: "bi_unique A" |
|
188 shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)" |
|
189 unfolding subset_eq [abs_def] by transfer_prover |
|
190 |
|
191 lemma right_total_UNIV_transfer[transfer_rule]: |
|
192 assumes "right_total A" |
|
193 shows "(set_rel A) (Collect (Domainp A)) UNIV" |
|
194 using assms unfolding right_total_def set_rel_def Domainp_iff by blast |
|
195 |
|
196 lemma UNIV_transfer [transfer_rule]: |
|
197 assumes "bi_total A" |
|
198 shows "(set_rel A) UNIV UNIV" |
|
199 using assms unfolding set_rel_def bi_total_def by simp |
|
200 |
|
201 lemma right_total_Compl_transfer [transfer_rule]: |
|
202 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" |
|
203 shows "(set_rel A ===> set_rel A) (\<lambda>S. uminus S \<inter> Collect (Domainp A)) uminus" |
|
204 unfolding Compl_eq [abs_def] |
|
205 by (subst Collect_conj_eq[symmetric]) transfer_prover |
|
206 |
|
207 lemma Compl_transfer [transfer_rule]: |
|
208 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" |
|
209 shows "(set_rel A ===> set_rel A) uminus uminus" |
|
210 unfolding Compl_eq [abs_def] by transfer_prover |
|
211 |
|
212 lemma right_total_Inter_transfer [transfer_rule]: |
|
213 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" |
|
214 shows "(set_rel (set_rel A) ===> set_rel A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter" |
|
215 unfolding Inter_eq[abs_def] |
|
216 by (subst Collect_conj_eq[symmetric]) transfer_prover |
|
217 |
|
218 lemma Inter_transfer [transfer_rule]: |
|
219 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" |
|
220 shows "(set_rel (set_rel A) ===> set_rel A) Inter Inter" |
|
221 unfolding Inter_eq [abs_def] by transfer_prover |
|
222 |
|
223 lemma filter_transfer [transfer_rule]: |
|
224 assumes [transfer_rule]: "bi_unique A" |
|
225 shows "((A ===> op=) ===> set_rel A ===> set_rel A) Set.filter Set.filter" |
|
226 unfolding Set.filter_def[abs_def] fun_rel_def set_rel_def by blast |
|
227 |
|
228 lemma bi_unique_set_rel_lemma: |
|
229 assumes "bi_unique R" and "set_rel R X Y" |
|
230 obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)" |
|
231 proof |
|
232 let ?f = "\<lambda>x. THE y. R x y" |
|
233 from assms show f: "\<forall>x\<in>X. R x (?f x)" |
|
234 apply (clarsimp simp add: set_rel_def) |
|
235 apply (drule (1) bspec, clarify) |
|
236 apply (rule theI2, assumption) |
|
237 apply (simp add: bi_unique_def) |
|
238 apply assumption |
|
239 done |
|
240 from assms show "Y = image ?f X" |
|
241 apply safe |
|
242 apply (clarsimp simp add: set_rel_def) |
|
243 apply (drule (1) bspec, clarify) |
|
244 apply (rule image_eqI) |
|
245 apply (rule the_equality [symmetric], assumption) |
|
246 apply (simp add: bi_unique_def) |
|
247 apply assumption |
|
248 apply (clarsimp simp add: set_rel_def) |
|
249 apply (frule (1) bspec, clarify) |
|
250 apply (rule theI2, assumption) |
|
251 apply (clarsimp simp add: bi_unique_def) |
|
252 apply (simp add: bi_unique_def, metis) |
|
253 done |
|
254 show "inj_on ?f X" |
|
255 apply (rule inj_onI) |
|
256 apply (drule f [rule_format]) |
|
257 apply (drule f [rule_format]) |
|
258 apply (simp add: assms(1) [unfolded bi_unique_def]) |
|
259 done |
|
260 qed |
|
261 |
|
262 lemma finite_transfer [transfer_rule]: |
|
263 "bi_unique A \<Longrightarrow> (set_rel A ===> op =) finite finite" |
|
264 by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, |
|
265 auto dest: finite_imageD) |
|
266 |
|
267 lemma card_transfer [transfer_rule]: |
|
268 "bi_unique A \<Longrightarrow> (set_rel A ===> op =) card card" |
|
269 by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image) |
|
270 |
|
271 end |
|
272 |
|
273 end |