1(* Title: HOL/Lifting_Set.thy 2 Author: Brian Huffman and Ondrej Kuncar 3*) 4 5section \<open>Setup for Lifting/Transfer for the set type\<close> 6 7theory Lifting_Set 8imports Lifting 9begin 10 11subsection \<open>Relator and predicator properties\<close> 12 13lemma rel_setD1: "\<lbrakk> rel_set R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y" 14 and rel_setD2: "\<lbrakk> rel_set R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y" 15 by (simp_all add: rel_set_def) 16 17lemma rel_set_conversep [simp]: "rel_set A\<inverse>\<inverse> = (rel_set A)\<inverse>\<inverse>" 18 unfolding rel_set_def by auto 19 20lemma rel_set_eq [relator_eq]: "rel_set (=) = (=)" 21 unfolding rel_set_def fun_eq_iff by auto 22 23lemma rel_set_mono[relator_mono]: 24 assumes "A \<le> B" 25 shows "rel_set A \<le> rel_set B" 26 using assms unfolding rel_set_def by blast 27 28lemma rel_set_OO[relator_distr]: "rel_set R OO rel_set S = rel_set (R OO S)" 29 apply (rule sym) 30 apply (intro ext) 31 subgoal for X Z 32 apply (rule iffI) 33 apply (rule relcomppI [where b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}"]) 34 apply (simp add: rel_set_def, fast)+ 35 done 36 done 37 38lemma Domainp_set[relator_domain]: 39 "Domainp (rel_set T) = (\<lambda>A. Ball A (Domainp T))" 40 unfolding rel_set_def Domainp_iff[abs_def] 41 apply (intro ext) 42 apply (rule iffI) 43 apply blast 44 subgoal for A by (rule exI [where x="{y. \<exists>x\<in>A. T x y}"]) fast 45 done 46 47lemma left_total_rel_set[transfer_rule]: 48 "left_total A \<Longrightarrow> left_total (rel_set A)" 49 unfolding left_total_def rel_set_def 50 apply safe 51 subgoal for X by (rule exI [where x="{y. \<exists>x\<in>X. A x y}"]) fast 52 done 53 54lemma left_unique_rel_set[transfer_rule]: 55 "left_unique A \<Longrightarrow> left_unique (rel_set A)" 56 unfolding left_unique_def rel_set_def 57 by fast 58 59lemma right_total_rel_set [transfer_rule]: 60 "right_total A \<Longrightarrow> right_total (rel_set A)" 61 using left_total_rel_set[of "A\<inverse>\<inverse>"] by simp 62 63lemma right_unique_rel_set [transfer_rule]: 64 "right_unique A \<Longrightarrow> right_unique (rel_set A)" 65 unfolding right_unique_def rel_set_def by fast 66 67lemma bi_total_rel_set [transfer_rule]: 68 "bi_total A \<Longrightarrow> bi_total (rel_set A)" 69 by(simp add: bi_total_alt_def left_total_rel_set right_total_rel_set) 70 71lemma bi_unique_rel_set [transfer_rule]: 72 "bi_unique A \<Longrightarrow> bi_unique (rel_set A)" 73 unfolding bi_unique_def rel_set_def by fast 74 75lemma set_relator_eq_onp [relator_eq_onp]: 76 "rel_set (eq_onp P) = eq_onp (\<lambda>A. Ball A P)" 77 unfolding fun_eq_iff rel_set_def eq_onp_def Ball_def by fast 78 79lemma bi_unique_rel_set_lemma: 80 assumes "bi_unique R" and "rel_set R X Y" 81 obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)" 82proof 83 define f where "f x = (THE y. R x y)" for x 84 { fix x assume "x \<in> X" 85 with \<open>rel_set R X Y\<close> \<open>bi_unique R\<close> have "R x (f x)" 86 by (simp add: bi_unique_def rel_set_def f_def) (metis theI) 87 with assms \<open>x \<in> X\<close> 88 have "R x (f x)" "\<forall>x'\<in>X. R x' (f x) \<longrightarrow> x = x'" "\<forall>y\<in>Y. R x y \<longrightarrow> y = f x" "f x \<in> Y" 89 by (fastforce simp add: bi_unique_def rel_set_def)+ } 90 note * = this 91 moreover 92 { fix y assume "y \<in> Y" 93 with \<open>rel_set R X Y\<close> *(3) \<open>y \<in> Y\<close> have "\<exists>x\<in>X. y = f x" 94 by (fastforce simp: rel_set_def) } 95 ultimately show "\<forall>x\<in>X. R x (f x)" "Y = image f X" "inj_on f X" 96 by (auto simp: inj_on_def image_iff) 97qed 98 99subsection \<open>Quotient theorem for the Lifting package\<close> 100 101lemma Quotient_set[quot_map]: 102 assumes "Quotient R Abs Rep T" 103 shows "Quotient (rel_set R) (image Abs) (image Rep) (rel_set T)" 104 using assms unfolding Quotient_alt_def4 105 apply (simp add: rel_set_OO[symmetric]) 106 apply (simp add: rel_set_def) 107 apply fast 108 done 109 110 111subsection \<open>Transfer rules for the Transfer package\<close> 112 113subsubsection \<open>Unconditional transfer rules\<close> 114 115context includes lifting_syntax 116begin 117 118lemma empty_transfer [transfer_rule]: "(rel_set A) {} {}" 119 unfolding rel_set_def by simp 120 121lemma insert_transfer [transfer_rule]: 122 "(A ===> rel_set A ===> rel_set A) insert insert" 123 unfolding rel_fun_def rel_set_def by auto 124 125lemma union_transfer [transfer_rule]: 126 "(rel_set A ===> rel_set A ===> rel_set A) union union" 127 unfolding rel_fun_def rel_set_def by auto 128 129lemma Union_transfer [transfer_rule]: 130 "(rel_set (rel_set A) ===> rel_set A) Union Union" 131 unfolding rel_fun_def rel_set_def by simp fast 132 133lemma image_transfer [transfer_rule]: 134 "((A ===> B) ===> rel_set A ===> rel_set B) image image" 135 unfolding rel_fun_def rel_set_def by simp fast 136 137lemma UNION_transfer [transfer_rule]: 138 "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION" 139 by transfer_prover 140 141lemma Ball_transfer [transfer_rule]: 142 "(rel_set A ===> (A ===> (=)) ===> (=)) Ball Ball" 143 unfolding rel_set_def rel_fun_def by fast 144 145lemma Bex_transfer [transfer_rule]: 146 "(rel_set A ===> (A ===> (=)) ===> (=)) Bex Bex" 147 unfolding rel_set_def rel_fun_def by fast 148 149lemma Pow_transfer [transfer_rule]: 150 "(rel_set A ===> rel_set (rel_set A)) Pow Pow" 151 apply (rule rel_funI) 152 apply (rule rel_setI) 153 subgoal for X Y X' 154 apply (rule rev_bexI [where x="{y\<in>Y. \<exists>x\<in>X'. A x y}"]) 155 apply clarsimp 156 apply (simp add: rel_set_def) 157 apply fast 158 done 159 subgoal for X Y Y' 160 apply (rule rev_bexI [where x="{x\<in>X. \<exists>y\<in>Y'. A x y}"]) 161 apply clarsimp 162 apply (simp add: rel_set_def) 163 apply fast 164 done 165 done 166 167lemma rel_set_transfer [transfer_rule]: 168 "((A ===> B ===> (=)) ===> rel_set A ===> rel_set B ===> (=)) rel_set rel_set" 169 unfolding rel_fun_def rel_set_def by fast 170 171lemma bind_transfer [transfer_rule]: 172 "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) Set.bind Set.bind" 173 unfolding bind_UNION [abs_def] by transfer_prover 174 175lemma INF_parametric [transfer_rule]: 176 "(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) INFIMUM INFIMUM" 177 by transfer_prover 178 179lemma SUP_parametric [transfer_rule]: 180 "(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) SUPREMUM SUPREMUM" 181 by transfer_prover 182 183 184subsubsection \<open>Rules requiring bi-unique, bi-total or right-total relations\<close> 185 186lemma member_transfer [transfer_rule]: 187 assumes "bi_unique A" 188 shows "(A ===> rel_set A ===> (=)) (\<in>) (\<in>)" 189 using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast 190 191lemma right_total_Collect_transfer[transfer_rule]: 192 assumes "right_total A" 193 shows "((A ===> (=)) ===> rel_set A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect" 194 using assms unfolding right_total_def rel_set_def rel_fun_def Domainp_iff by fast 195 196lemma Collect_transfer [transfer_rule]: 197 assumes "bi_total A" 198 shows "((A ===> (=)) ===> rel_set A) Collect Collect" 199 using assms unfolding rel_fun_def rel_set_def bi_total_def by fast 200 201lemma inter_transfer [transfer_rule]: 202 assumes "bi_unique A" 203 shows "(rel_set A ===> rel_set A ===> rel_set A) inter inter" 204 using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast 205 206lemma Diff_transfer [transfer_rule]: 207 assumes "bi_unique A" 208 shows "(rel_set A ===> rel_set A ===> rel_set A) (-) (-)" 209 using assms unfolding rel_fun_def rel_set_def bi_unique_def 210 unfolding Ball_def Bex_def Diff_eq 211 by (safe, simp, metis, simp, metis) 212 213lemma subset_transfer [transfer_rule]: 214 assumes [transfer_rule]: "bi_unique A" 215 shows "(rel_set A ===> rel_set A ===> (=)) (\<subseteq>) (\<subseteq>)" 216 unfolding subset_eq [abs_def] by transfer_prover 217 218lemma strict_subset_transfer [transfer_rule]: 219 includes lifting_syntax 220 assumes [transfer_rule]: "bi_unique A" 221 shows "(rel_set A ===> rel_set A ===> (=)) (\<subset>) (\<subset>)" 222 unfolding subset_not_subset_eq by transfer_prover 223 224declare right_total_UNIV_transfer[transfer_rule] 225 226lemma UNIV_transfer [transfer_rule]: 227 assumes "bi_total A" 228 shows "(rel_set A) UNIV UNIV" 229 using assms unfolding rel_set_def bi_total_def by simp 230 231lemma right_total_Compl_transfer [transfer_rule]: 232 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" 233 shows "(rel_set A ===> rel_set A) (\<lambda>S. uminus S \<inter> Collect (Domainp A)) uminus" 234 unfolding Compl_eq [abs_def] 235 by (subst Collect_conj_eq[symmetric]) transfer_prover 236 237lemma Compl_transfer [transfer_rule]: 238 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" 239 shows "(rel_set A ===> rel_set A) uminus uminus" 240 unfolding Compl_eq [abs_def] by transfer_prover 241 242lemma right_total_Inter_transfer [transfer_rule]: 243 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" 244 shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>S. \<Inter>S \<inter> Collect (Domainp A)) Inter" 245 unfolding Inter_eq[abs_def] 246 by (subst Collect_conj_eq[symmetric]) transfer_prover 247 248lemma Inter_transfer [transfer_rule]: 249 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" 250 shows "(rel_set (rel_set A) ===> rel_set A) Inter Inter" 251 unfolding Inter_eq [abs_def] by transfer_prover 252 253lemma filter_transfer [transfer_rule]: 254 assumes [transfer_rule]: "bi_unique A" 255 shows "((A ===> (=)) ===> rel_set A ===> rel_set A) Set.filter Set.filter" 256 unfolding Set.filter_def[abs_def] rel_fun_def rel_set_def by blast 257 258lemma finite_transfer [transfer_rule]: 259 "bi_unique A \<Longrightarrow> (rel_set A ===> (=)) finite finite" 260 by (rule rel_funI, erule (1) bi_unique_rel_set_lemma) 261 (auto dest: finite_imageD) 262 263lemma card_transfer [transfer_rule]: 264 "bi_unique A \<Longrightarrow> (rel_set A ===> (=)) card card" 265 by (rule rel_funI, erule (1) bi_unique_rel_set_lemma) 266 (simp add: card_image) 267 268lemma vimage_right_total_transfer[transfer_rule]: 269 includes lifting_syntax 270 assumes [transfer_rule]: "bi_unique B" "right_total A" 271 shows "((A ===> B) ===> rel_set B ===> rel_set A) (\<lambda>f X. f -` X \<inter> Collect (Domainp A)) vimage" 272proof - 273 let ?vimage = "(\<lambda>f B. {x. f x \<in> B \<and> Domainp A x})" 274 have "((A ===> B) ===> rel_set B ===> rel_set A) ?vimage vimage" 275 unfolding vimage_def 276 by transfer_prover 277 also have "?vimage = (\<lambda>f X. f -` X \<inter> Collect (Domainp A))" 278 by auto 279 finally show ?thesis . 280qed 281 282lemma vimage_parametric [transfer_rule]: 283 assumes [transfer_rule]: "bi_total A" "bi_unique B" 284 shows "((A ===> B) ===> rel_set B ===> rel_set A) vimage vimage" 285 unfolding vimage_def[abs_def] by transfer_prover 286 287lemma Image_parametric [transfer_rule]: 288 assumes "bi_unique A" 289 shows "(rel_set (rel_prod A B) ===> rel_set A ===> rel_set B) (``) (``)" 290 by (intro rel_funI rel_setI) 291 (force dest: rel_setD1 bi_uniqueDr[OF assms], force dest: rel_setD2 bi_uniqueDl[OF assms]) 292 293lemma inj_on_transfer[transfer_rule]: 294 "((A ===> B) ===> rel_set A ===> (=)) inj_on inj_on" 295 if [transfer_rule]: "bi_unique A" "bi_unique B" 296 unfolding inj_on_def 297 by transfer_prover 298 299end 300 301lemma (in comm_monoid_set) F_parametric [transfer_rule]: 302 fixes A :: "'b \<Rightarrow> 'c \<Rightarrow> bool" 303 assumes "bi_unique A" 304 shows "rel_fun (rel_fun A (=)) (rel_fun (rel_set A) (=)) F F" 305proof (rule rel_funI)+ 306 fix f :: "'b \<Rightarrow> 'a" and g S T 307 assume "rel_fun A (=) f g" "rel_set A S T" 308 with \<open>bi_unique A\<close> obtain i where "bij_betw i S T" "\<And>x. x \<in> S \<Longrightarrow> f x = g (i x)" 309 by (auto elim: bi_unique_rel_set_lemma simp: rel_fun_def bij_betw_def) 310 then show "F f S = F g T" 311 by (simp add: reindex_bij_betw) 312qed 313 314lemmas sum_parametric = sum.F_parametric 315lemmas prod_parametric = prod.F_parametric 316 317lemma rel_set_UNION: 318 assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g" 319 shows "rel_set R (UNION A f) (UNION B g)" 320 by transfer_prover 321 322end 323