src/HOL/Library/Countable_Set_Type.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 63040 eb4ddd18d635 child 66453 cc19f7ca2ed6 permissions -rw-r--r--
bundle lifting_syntax;
```     1 (*  Title:      HOL/Library/Countable_Set_Type.thy
```
```     2     Author:     Andrei Popescu, TU Muenchen
```
```     3     Author:     Andreas Lochbihler, ETH Zurich
```
```     4     Copyright   2012
```
```     5
```
```     6 Type of (at most) countable sets.
```
```     7 *)
```
```     8
```
```     9 section \<open>Type of (at Most) Countable Sets\<close>
```
```    10
```
```    11 theory Countable_Set_Type
```
```    12 imports Countable_Set Cardinal_Notations Conditionally_Complete_Lattices
```
```    13 begin
```
```    14
```
```    15
```
```    16 subsection\<open>Cardinal stuff\<close>
```
```    17
```
```    18 lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
```
```    19   unfolding countable_def card_of_ordLeq[symmetric] by auto
```
```    20
```
```    21 lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq"
```
```    22   unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast
```
```    23
```
```    24 lemma countable_or_card_of:
```
```    25 assumes "countable A"
```
```    26 shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
```
```    27        (infinite A  \<and> |A| =o |UNIV::nat set| )"
```
```    28 by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq
```
```    29       ordLeq_iff_ordLess_or_ordIso)
```
```    30
```
```    31 lemma countable_cases_card_of[elim]:
```
```    32   assumes "countable A"
```
```    33   obtains (Fin) "finite A" "|A| <o |UNIV::nat set|"
```
```    34         | (Inf) "infinite A" "|A| =o |UNIV::nat set|"
```
```    35   using assms countable_or_card_of by blast
```
```    36
```
```    37 lemma countable_or:
```
```    38   "countable A \<Longrightarrow> (\<exists> f::'a\<Rightarrow>nat. finite A \<and> inj_on f A) \<or> (\<exists> f::'a\<Rightarrow>nat. infinite A \<and> bij_betw f A UNIV)"
```
```    39   by (elim countable_enum_cases) fastforce+
```
```    40
```
```    41 lemma countable_cases[elim]:
```
```    42   assumes "countable A"
```
```    43   obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A"
```
```    44         | (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV"
```
```    45   using assms countable_or by metis
```
```    46
```
```    47 lemma countable_ordLeq:
```
```    48 assumes "|A| \<le>o |B|" and "countable B"
```
```    49 shows "countable A"
```
```    50 using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
```
```    51
```
```    52 lemma countable_ordLess:
```
```    53 assumes AB: "|A| <o |B|" and B: "countable B"
```
```    54 shows "countable A"
```
```    55 using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
```
```    56
```
```    57 subsection \<open>The type of countable sets\<close>
```
```    58
```
```    59 typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset
```
```    60   by (rule exI[of _ "{}"]) simp
```
```    61
```
```    62 setup_lifting type_definition_cset
```
```    63
```
```    64 declare
```
```    65   rcset_inverse[simp]
```
```    66   acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp]
```
```    67   acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp]
```
```    68   rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
```
```    69
```
```    70 instantiation cset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
```
```    71 begin
```
```    72
```
```    73 lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp
```
```    74
```
```    75 lift_definition less_eq_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool"
```
```    76   is subset_eq parametric subset_transfer .
```
```    77
```
```    78 definition less_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool"
```
```    79 where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a cset)"
```
```    80
```
```    81 lemma less_cset_transfer[transfer_rule]:
```
```    82   includes lifting_syntax
```
```    83   assumes [transfer_rule]: "bi_unique A"
```
```    84   shows "((pcr_cset A) ===> (pcr_cset A) ===> op =) op \<subset> op <"
```
```    85 unfolding less_cset_def[abs_def] psubset_eq[abs_def] by transfer_prover
```
```    86
```
```    87 lift_definition sup_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset"
```
```    88 is union parametric union_transfer by simp
```
```    89
```
```    90 lift_definition inf_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset"
```
```    91 is inter parametric inter_transfer by simp
```
```    92
```
```    93 lift_definition minus_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset"
```
```    94 is minus parametric Diff_transfer by simp
```
```    95
```
```    96 instance by standard (transfer; auto)+
```
```    97
```
```    98 end
```
```    99
```
```   100 abbreviation cempty :: "'a cset" where "cempty \<equiv> bot"
```
```   101 abbreviation csubset_eq :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool" where "csubset_eq xs ys \<equiv> xs \<le> ys"
```
```   102 abbreviation csubset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool" where "csubset xs ys \<equiv> xs < ys"
```
```   103 abbreviation cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" where "cUn xs ys \<equiv> sup xs ys"
```
```   104 abbreviation cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" where "cInt xs ys \<equiv> inf xs ys"
```
```   105 abbreviation cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" where "cDiff xs ys \<equiv> minus xs ys"
```
```   106
```
```   107 lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
```
```   108   .
```
```   109 lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
```
```   110   by (rule countable_insert)
```
```   111 abbreviation csingle :: "'a \<Rightarrow> 'a cset" where "csingle x \<equiv> cinsert x cempty"
```
```   112 lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer
```
```   113   by (rule countable_image)
```
```   114 lift_definition cBall :: "'a cset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer .
```
```   115 lift_definition cBex :: "'a cset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer .
```
```   116 lift_definition cUNION :: "'a cset \<Rightarrow> ('a \<Rightarrow> 'b cset) \<Rightarrow> 'b cset"
```
```   117   is "UNION" parametric UNION_transfer by simp
```
```   118 definition cUnion :: "'a cset cset \<Rightarrow> 'a cset" where "cUnion A = cUNION A id"
```
```   119
```
```   120 lemma Union_conv_UNION: "\<Union>A = UNION A id"
```
```   121 by auto
```
```   122
```
```   123 lemma cUnion_transfer [transfer_rule]:
```
```   124   "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) Union cUnion"
```
```   125 proof -
```
```   126   have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. UNION A id) (\<lambda>A. cUNION A id)"
```
```   127     by transfer_prover
```
```   128   then show ?thesis by (simp add: cUnion_def [symmetric])
```
```   129 qed
```
```   130
```
```   131 lemmas cset_eqI = set_eqI[Transfer.transferred]
```
```   132 lemmas cset_eq_iff[no_atp] = set_eq_iff[Transfer.transferred]
```
```   133 lemmas cBallI[intro!] = ballI[Transfer.transferred]
```
```   134 lemmas cbspec[dest?] = bspec[Transfer.transferred]
```
```   135 lemmas cBallE[elim] = ballE[Transfer.transferred]
```
```   136 lemmas cBexI[intro] = bexI[Transfer.transferred]
```
```   137 lemmas rev_cBexI[intro?] = rev_bexI[Transfer.transferred]
```
```   138 lemmas cBexCI = bexCI[Transfer.transferred]
```
```   139 lemmas cBexE[elim!] = bexE[Transfer.transferred]
```
```   140 lemmas cBall_triv[simp] = ball_triv[Transfer.transferred]
```
```   141 lemmas cBex_triv[simp] = bex_triv[Transfer.transferred]
```
```   142 lemmas cBex_triv_one_point1[simp] = bex_triv_one_point1[Transfer.transferred]
```
```   143 lemmas cBex_triv_one_point2[simp] = bex_triv_one_point2[Transfer.transferred]
```
```   144 lemmas cBex_one_point1[simp] = bex_one_point1[Transfer.transferred]
```
```   145 lemmas cBex_one_point2[simp] = bex_one_point2[Transfer.transferred]
```
```   146 lemmas cBall_one_point1[simp] = ball_one_point1[Transfer.transferred]
```
```   147 lemmas cBall_one_point2[simp] = ball_one_point2[Transfer.transferred]
```
```   148 lemmas cBall_conj_distrib = ball_conj_distrib[Transfer.transferred]
```
```   149 lemmas cBex_disj_distrib = bex_disj_distrib[Transfer.transferred]
```
```   150 lemmas cBall_cong = ball_cong[Transfer.transferred]
```
```   151 lemmas cBex_cong = bex_cong[Transfer.transferred]
```
```   152 lemmas csubsetI[intro!] = subsetI[Transfer.transferred]
```
```   153 lemmas csubsetD[elim, intro?] = subsetD[Transfer.transferred]
```
```   154 lemmas rev_csubsetD[no_atp,intro?] = rev_subsetD[Transfer.transferred]
```
```   155 lemmas csubsetCE[no_atp,elim] = subsetCE[Transfer.transferred]
```
```   156 lemmas csubset_eq[no_atp] = subset_eq[Transfer.transferred]
```
```   157 lemmas contra_csubsetD[no_atp] = contra_subsetD[Transfer.transferred]
```
```   158 lemmas csubset_refl = subset_refl[Transfer.transferred]
```
```   159 lemmas csubset_trans = subset_trans[Transfer.transferred]
```
```   160 lemmas cset_rev_mp = set_rev_mp[Transfer.transferred]
```
```   161 lemmas cset_mp = set_mp[Transfer.transferred]
```
```   162 lemmas csubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred]
```
```   163 lemmas eq_cmem_trans = eq_mem_trans[Transfer.transferred]
```
```   164 lemmas csubset_antisym[intro!] = subset_antisym[Transfer.transferred]
```
```   165 lemmas cequalityD1 = equalityD1[Transfer.transferred]
```
```   166 lemmas cequalityD2 = equalityD2[Transfer.transferred]
```
```   167 lemmas cequalityE = equalityE[Transfer.transferred]
```
```   168 lemmas cequalityCE[elim] = equalityCE[Transfer.transferred]
```
```   169 lemmas eqcset_imp_iff = eqset_imp_iff[Transfer.transferred]
```
```   170 lemmas eqcelem_imp_iff = eqelem_imp_iff[Transfer.transferred]
```
```   171 lemmas cempty_iff[simp] = empty_iff[Transfer.transferred]
```
```   172 lemmas cempty_fsubsetI[iff] = empty_subsetI[Transfer.transferred]
```
```   173 lemmas equals_cemptyI = equals0I[Transfer.transferred]
```
```   174 lemmas equals_cemptyD = equals0D[Transfer.transferred]
```
```   175 lemmas cBall_cempty[simp] = ball_empty[Transfer.transferred]
```
```   176 lemmas cBex_cempty[simp] = bex_empty[Transfer.transferred]
```
```   177 lemmas cInt_iff[simp] = Int_iff[Transfer.transferred]
```
```   178 lemmas cIntI[intro!] = IntI[Transfer.transferred]
```
```   179 lemmas cIntD1 = IntD1[Transfer.transferred]
```
```   180 lemmas cIntD2 = IntD2[Transfer.transferred]
```
```   181 lemmas cIntE[elim!] = IntE[Transfer.transferred]
```
```   182 lemmas cUn_iff[simp] = Un_iff[Transfer.transferred]
```
```   183 lemmas cUnI1[elim?] = UnI1[Transfer.transferred]
```
```   184 lemmas cUnI2[elim?] = UnI2[Transfer.transferred]
```
```   185 lemmas cUnCI[intro!] = UnCI[Transfer.transferred]
```
```   186 lemmas cuUnE[elim!] = UnE[Transfer.transferred]
```
```   187 lemmas cDiff_iff[simp] = Diff_iff[Transfer.transferred]
```
```   188 lemmas cDiffI[intro!] = DiffI[Transfer.transferred]
```
```   189 lemmas cDiffD1 = DiffD1[Transfer.transferred]
```
```   190 lemmas cDiffD2 = DiffD2[Transfer.transferred]
```
```   191 lemmas cDiffE[elim!] = DiffE[Transfer.transferred]
```
```   192 lemmas cinsert_iff[simp] = insert_iff[Transfer.transferred]
```
```   193 lemmas cinsertI1 = insertI1[Transfer.transferred]
```
```   194 lemmas cinsertI2 = insertI2[Transfer.transferred]
```
```   195 lemmas cinsertE[elim!] = insertE[Transfer.transferred]
```
```   196 lemmas cinsertCI[intro!] = insertCI[Transfer.transferred]
```
```   197 lemmas csubset_cinsert_iff = subset_insert_iff[Transfer.transferred]
```
```   198 lemmas cinsert_ident = insert_ident[Transfer.transferred]
```
```   199 lemmas csingletonI[intro!,no_atp] = singletonI[Transfer.transferred]
```
```   200 lemmas csingletonD[dest!,no_atp] = singletonD[Transfer.transferred]
```
```   201 lemmas fsingletonE = csingletonD [elim_format]
```
```   202 lemmas csingleton_iff = singleton_iff[Transfer.transferred]
```
```   203 lemmas csingleton_inject[dest!] = singleton_inject[Transfer.transferred]
```
```   204 lemmas csingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred]
```
```   205 lemmas csingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred]
```
```   206 lemmas csubset_csingletonD = subset_singletonD[Transfer.transferred]
```
```   207 lemmas cDiff_single_cinsert = Diff_single_insert[Transfer.transferred]
```
```   208 lemmas cdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred]
```
```   209 lemmas cUn_csingleton_iff = Un_singleton_iff[Transfer.transferred]
```
```   210 lemmas csingleton_cUn_iff = singleton_Un_iff[Transfer.transferred]
```
```   211 lemmas cimage_eqI[simp, intro] = image_eqI[Transfer.transferred]
```
```   212 lemmas cimageI = imageI[Transfer.transferred]
```
```   213 lemmas rev_cimage_eqI = rev_image_eqI[Transfer.transferred]
```
```   214 lemmas cimageE[elim!] = imageE[Transfer.transferred]
```
```   215 lemmas Compr_cimage_eq = Compr_image_eq[Transfer.transferred]
```
```   216 lemmas cimage_cUn = image_Un[Transfer.transferred]
```
```   217 lemmas cimage_iff = image_iff[Transfer.transferred]
```
```   218 lemmas cimage_csubset_iff[no_atp] = image_subset_iff[Transfer.transferred]
```
```   219 lemmas cimage_csubsetI = image_subsetI[Transfer.transferred]
```
```   220 lemmas cimage_ident[simp] = image_ident[Transfer.transferred]
```
```   221 lemmas if_split_cin1 = if_split_mem1[Transfer.transferred]
```
```   222 lemmas if_split_cin2 = if_split_mem2[Transfer.transferred]
```
```   223 lemmas cpsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred]
```
```   224 lemmas cpsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred]
```
```   225 lemmas cpsubset_finsert_iff = psubset_insert_iff[Transfer.transferred]
```
```   226 lemmas cpsubset_eq = psubset_eq[Transfer.transferred]
```
```   227 lemmas cpsubset_imp_fsubset = psubset_imp_subset[Transfer.transferred]
```
```   228 lemmas cpsubset_trans = psubset_trans[Transfer.transferred]
```
```   229 lemmas cpsubsetD = psubsetD[Transfer.transferred]
```
```   230 lemmas cpsubset_csubset_trans = psubset_subset_trans[Transfer.transferred]
```
```   231 lemmas csubset_cpsubset_trans = subset_psubset_trans[Transfer.transferred]
```
```   232 lemmas cpsubset_imp_ex_fmem = psubset_imp_ex_mem[Transfer.transferred]
```
```   233 lemmas csubset_cinsertI = subset_insertI[Transfer.transferred]
```
```   234 lemmas csubset_cinsertI2 = subset_insertI2[Transfer.transferred]
```
```   235 lemmas csubset_cinsert = subset_insert[Transfer.transferred]
```
```   236 lemmas cUn_upper1 = Un_upper1[Transfer.transferred]
```
```   237 lemmas cUn_upper2 = Un_upper2[Transfer.transferred]
```
```   238 lemmas cUn_least = Un_least[Transfer.transferred]
```
```   239 lemmas cInt_lower1 = Int_lower1[Transfer.transferred]
```
```   240 lemmas cInt_lower2 = Int_lower2[Transfer.transferred]
```
```   241 lemmas cInt_greatest = Int_greatest[Transfer.transferred]
```
```   242 lemmas cDiff_csubset = Diff_subset[Transfer.transferred]
```
```   243 lemmas cDiff_csubset_conv = Diff_subset_conv[Transfer.transferred]
```
```   244 lemmas csubset_cempty[simp] = subset_empty[Transfer.transferred]
```
```   245 lemmas not_cpsubset_cempty[iff] = not_psubset_empty[Transfer.transferred]
```
```   246 lemmas cinsert_is_cUn = insert_is_Un[Transfer.transferred]
```
```   247 lemmas cinsert_not_cempty[simp] = insert_not_empty[Transfer.transferred]
```
```   248 lemmas cempty_not_cinsert = empty_not_insert[Transfer.transferred]
```
```   249 lemmas cinsert_absorb = insert_absorb[Transfer.transferred]
```
```   250 lemmas cinsert_absorb2[simp] = insert_absorb2[Transfer.transferred]
```
```   251 lemmas cinsert_commute = insert_commute[Transfer.transferred]
```
```   252 lemmas cinsert_csubset[simp] = insert_subset[Transfer.transferred]
```
```   253 lemmas cinsert_cinter_cinsert[simp] = insert_inter_insert[Transfer.transferred]
```
```   254 lemmas cinsert_disjoint[simp,no_atp] = insert_disjoint[Transfer.transferred]
```
```   255 lemmas disjoint_cinsert[simp,no_atp] = disjoint_insert[Transfer.transferred]
```
```   256 lemmas cimage_cempty[simp] = image_empty[Transfer.transferred]
```
```   257 lemmas cimage_cinsert[simp] = image_insert[Transfer.transferred]
```
```   258 lemmas cimage_constant = image_constant[Transfer.transferred]
```
```   259 lemmas cimage_constant_conv = image_constant_conv[Transfer.transferred]
```
```   260 lemmas cimage_cimage = image_image[Transfer.transferred]
```
```   261 lemmas cinsert_cimage[simp] = insert_image[Transfer.transferred]
```
```   262 lemmas cimage_is_cempty[iff] = image_is_empty[Transfer.transferred]
```
```   263 lemmas cempty_is_cimage[iff] = empty_is_image[Transfer.transferred]
```
```   264 lemmas cimage_cong = image_cong[Transfer.transferred]
```
```   265 lemmas cimage_cInt_csubset = image_Int_subset[Transfer.transferred]
```
```   266 lemmas cimage_cDiff_csubset = image_diff_subset[Transfer.transferred]
```
```   267 lemmas cInt_absorb = Int_absorb[Transfer.transferred]
```
```   268 lemmas cInt_left_absorb = Int_left_absorb[Transfer.transferred]
```
```   269 lemmas cInt_commute = Int_commute[Transfer.transferred]
```
```   270 lemmas cInt_left_commute = Int_left_commute[Transfer.transferred]
```
```   271 lemmas cInt_assoc = Int_assoc[Transfer.transferred]
```
```   272 lemmas cInt_ac = Int_ac[Transfer.transferred]
```
```   273 lemmas cInt_absorb1 = Int_absorb1[Transfer.transferred]
```
```   274 lemmas cInt_absorb2 = Int_absorb2[Transfer.transferred]
```
```   275 lemmas cInt_cempty_left = Int_empty_left[Transfer.transferred]
```
```   276 lemmas cInt_cempty_right = Int_empty_right[Transfer.transferred]
```
```   277 lemmas disjoint_iff_cnot_equal = disjoint_iff_not_equal[Transfer.transferred]
```
```   278 lemmas cInt_cUn_distrib = Int_Un_distrib[Transfer.transferred]
```
```   279 lemmas cInt_cUn_distrib2 = Int_Un_distrib2[Transfer.transferred]
```
```   280 lemmas cInt_csubset_iff[no_atp, simp] = Int_subset_iff[Transfer.transferred]
```
```   281 lemmas cUn_absorb = Un_absorb[Transfer.transferred]
```
```   282 lemmas cUn_left_absorb = Un_left_absorb[Transfer.transferred]
```
```   283 lemmas cUn_commute = Un_commute[Transfer.transferred]
```
```   284 lemmas cUn_left_commute = Un_left_commute[Transfer.transferred]
```
```   285 lemmas cUn_assoc = Un_assoc[Transfer.transferred]
```
```   286 lemmas cUn_ac = Un_ac[Transfer.transferred]
```
```   287 lemmas cUn_absorb1 = Un_absorb1[Transfer.transferred]
```
```   288 lemmas cUn_absorb2 = Un_absorb2[Transfer.transferred]
```
```   289 lemmas cUn_cempty_left = Un_empty_left[Transfer.transferred]
```
```   290 lemmas cUn_cempty_right = Un_empty_right[Transfer.transferred]
```
```   291 lemmas cUn_cinsert_left[simp] = Un_insert_left[Transfer.transferred]
```
```   292 lemmas cUn_cinsert_right[simp] = Un_insert_right[Transfer.transferred]
```
```   293 lemmas cInt_cinsert_left = Int_insert_left[Transfer.transferred]
```
```   294 lemmas cInt_cinsert_left_if0[simp] = Int_insert_left_if0[Transfer.transferred]
```
```   295 lemmas cInt_cinsert_left_if1[simp] = Int_insert_left_if1[Transfer.transferred]
```
```   296 lemmas cInt_cinsert_right = Int_insert_right[Transfer.transferred]
```
```   297 lemmas cInt_cinsert_right_if0[simp] = Int_insert_right_if0[Transfer.transferred]
```
```   298 lemmas cInt_cinsert_right_if1[simp] = Int_insert_right_if1[Transfer.transferred]
```
```   299 lemmas cUn_cInt_distrib = Un_Int_distrib[Transfer.transferred]
```
```   300 lemmas cUn_cInt_distrib2 = Un_Int_distrib2[Transfer.transferred]
```
```   301 lemmas cUn_cInt_crazy = Un_Int_crazy[Transfer.transferred]
```
```   302 lemmas csubset_cUn_eq = subset_Un_eq[Transfer.transferred]
```
```   303 lemmas cUn_cempty[iff] = Un_empty[Transfer.transferred]
```
```   304 lemmas cUn_csubset_iff[no_atp, simp] = Un_subset_iff[Transfer.transferred]
```
```   305 lemmas cUn_cDiff_cInt = Un_Diff_Int[Transfer.transferred]
```
```   306 lemmas cDiff_cInt2 = Diff_Int2[Transfer.transferred]
```
```   307 lemmas cUn_cInt_assoc_eq = Un_Int_assoc_eq[Transfer.transferred]
```
```   308 lemmas cBall_cUn = ball_Un[Transfer.transferred]
```
```   309 lemmas cBex_cUn = bex_Un[Transfer.transferred]
```
```   310 lemmas cDiff_eq_cempty_iff[simp,no_atp] = Diff_eq_empty_iff[Transfer.transferred]
```
```   311 lemmas cDiff_cancel[simp] = Diff_cancel[Transfer.transferred]
```
```   312 lemmas cDiff_idemp[simp] = Diff_idemp[Transfer.transferred]
```
```   313 lemmas cDiff_triv = Diff_triv[Transfer.transferred]
```
```   314 lemmas cempty_cDiff[simp] = empty_Diff[Transfer.transferred]
```
```   315 lemmas cDiff_cempty[simp] = Diff_empty[Transfer.transferred]
```
```   316 lemmas cDiff_cinsert0[simp,no_atp] = Diff_insert0[Transfer.transferred]
```
```   317 lemmas cDiff_cinsert = Diff_insert[Transfer.transferred]
```
```   318 lemmas cDiff_cinsert2 = Diff_insert2[Transfer.transferred]
```
```   319 lemmas cinsert_cDiff_if = insert_Diff_if[Transfer.transferred]
```
```   320 lemmas cinsert_cDiff1[simp] = insert_Diff1[Transfer.transferred]
```
```   321 lemmas cinsert_cDiff_single[simp] = insert_Diff_single[Transfer.transferred]
```
```   322 lemmas cinsert_cDiff = insert_Diff[Transfer.transferred]
```
```   323 lemmas cDiff_cinsert_absorb = Diff_insert_absorb[Transfer.transferred]
```
```   324 lemmas cDiff_disjoint[simp] = Diff_disjoint[Transfer.transferred]
```
```   325 lemmas cDiff_partition = Diff_partition[Transfer.transferred]
```
```   326 lemmas double_cDiff = double_diff[Transfer.transferred]
```
```   327 lemmas cUn_cDiff_cancel[simp] = Un_Diff_cancel[Transfer.transferred]
```
```   328 lemmas cUn_cDiff_cancel2[simp] = Un_Diff_cancel2[Transfer.transferred]
```
```   329 lemmas cDiff_cUn = Diff_Un[Transfer.transferred]
```
```   330 lemmas cDiff_cInt = Diff_Int[Transfer.transferred]
```
```   331 lemmas cUn_cDiff = Un_Diff[Transfer.transferred]
```
```   332 lemmas cInt_cDiff = Int_Diff[Transfer.transferred]
```
```   333 lemmas cDiff_cInt_distrib = Diff_Int_distrib[Transfer.transferred]
```
```   334 lemmas cDiff_cInt_distrib2 = Diff_Int_distrib2[Transfer.transferred]
```
```   335 lemmas cset_eq_csubset = set_eq_subset[Transfer.transferred]
```
```   336 lemmas csubset_iff[no_atp] = subset_iff[Transfer.transferred]
```
```   337 lemmas csubset_iff_pfsubset_eq = subset_iff_psubset_eq[Transfer.transferred]
```
```   338 lemmas all_not_cin_conv[simp] = all_not_in_conv[Transfer.transferred]
```
```   339 lemmas ex_cin_conv = ex_in_conv[Transfer.transferred]
```
```   340 lemmas cimage_mono = image_mono[Transfer.transferred]
```
```   341 lemmas cinsert_mono = insert_mono[Transfer.transferred]
```
```   342 lemmas cunion_mono = Un_mono[Transfer.transferred]
```
```   343 lemmas cinter_mono = Int_mono[Transfer.transferred]
```
```   344 lemmas cminus_mono = Diff_mono[Transfer.transferred]
```
```   345 lemmas cin_mono = in_mono[Transfer.transferred]
```
```   346 lemmas cLeast_mono = Least_mono[Transfer.transferred]
```
```   347 lemmas cequalityI = equalityI[Transfer.transferred]
```
```   348 lemmas cUN_iff [simp] = UN_iff[Transfer.transferred]
```
```   349 lemmas cUN_I [intro] = UN_I[Transfer.transferred]
```
```   350 lemmas cUN_E [elim!] = UN_E[Transfer.transferred]
```
```   351 lemmas cUN_upper = UN_upper[Transfer.transferred]
```
```   352 lemmas cUN_least = UN_least[Transfer.transferred]
```
```   353 lemmas cUN_cinsert_distrib = UN_insert_distrib[Transfer.transferred]
```
```   354 lemmas cUN_empty [simp] = UN_empty[Transfer.transferred]
```
```   355 lemmas cUN_empty2 [simp] = UN_empty2[Transfer.transferred]
```
```   356 lemmas cUN_absorb = UN_absorb[Transfer.transferred]
```
```   357 lemmas cUN_cinsert [simp] = UN_insert[Transfer.transferred]
```
```   358 lemmas cUN_cUn [simp] = UN_Un[Transfer.transferred]
```
```   359 lemmas cUN_cUN_flatten = UN_UN_flatten[Transfer.transferred]
```
```   360 lemmas cUN_csubset_iff = UN_subset_iff[Transfer.transferred]
```
```   361 lemmas cUN_constant [simp] = UN_constant[Transfer.transferred]
```
```   362 lemmas cimage_cUnion = image_Union[Transfer.transferred]
```
```   363 lemmas cUNION_cempty_conv [simp] = UNION_empty_conv[Transfer.transferred]
```
```   364 lemmas cBall_cUN = ball_UN[Transfer.transferred]
```
```   365 lemmas cBex_cUN = bex_UN[Transfer.transferred]
```
```   366 lemmas cUn_eq_cUN = Un_eq_UN[Transfer.transferred]
```
```   367 lemmas cUN_mono = UN_mono[Transfer.transferred]
```
```   368 lemmas cimage_cUN = image_UN[Transfer.transferred]
```
```   369 lemmas cUN_csingleton [simp] = UN_singleton[Transfer.transferred]
```
```   370
```
```   371 subsection \<open>Additional lemmas\<close>
```
```   372
```
```   373 subsubsection \<open>\<open>cempty\<close>\<close>
```
```   374
```
```   375 lemma cemptyE [elim!]: "cin a cempty \<Longrightarrow> P" by simp
```
```   376
```
```   377 subsubsection \<open>\<open>cinsert\<close>\<close>
```
```   378
```
```   379 lemma countable_insert_iff: "countable (insert x A) \<longleftrightarrow> countable A"
```
```   380 by (metis Diff_eq_empty_iff countable_empty countable_insert subset_insertI uncountable_minus_countable)
```
```   381
```
```   382 lemma set_cinsert:
```
```   383   assumes "cin x A"
```
```   384   obtains B where "A = cinsert x B" and "\<not> cin x B"
```
```   385 using assms by transfer(erule Set.set_insert, simp add: countable_insert_iff)
```
```   386
```
```   387 lemma mk_disjoint_cinsert: "cin a A \<Longrightarrow> \<exists>B. A = cinsert a B \<and> \<not> cin a B"
```
```   388   by (rule exI[where x = "cDiff A (csingle a)"]) blast
```
```   389
```
```   390 subsubsection \<open>\<open>cimage\<close>\<close>
```
```   391
```
```   392 lemma subset_cimage_iff: "csubset_eq B (cimage f A) \<longleftrightarrow> (\<exists>AA. csubset_eq AA A \<and> B = cimage f AA)"
```
```   393 by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE)
```
```   394
```
```   395 subsubsection \<open>bounded quantification\<close>
```
```   396
```
```   397 lemma cBex_simps [simp, no_atp]:
```
```   398   "\<And>A P Q. cBex A (\<lambda>x. P x \<and> Q) = (cBex A P \<and> Q)"
```
```   399   "\<And>A P Q. cBex A (\<lambda>x. P \<and> Q x) = (P \<and> cBex A Q)"
```
```   400   "\<And>P. cBex cempty P = False"
```
```   401   "\<And>a B P. cBex (cinsert a B) P = (P a \<or> cBex B P)"
```
```   402   "\<And>A P f. cBex (cimage f A) P = cBex A (\<lambda>x. P (f x))"
```
```   403   "\<And>A P. (\<not> cBex A P) = cBall A (\<lambda>x. \<not> P x)"
```
```   404 by auto
```
```   405
```
```   406 lemma cBall_simps [simp, no_atp]:
```
```   407   "\<And>A P Q. cBall A (\<lambda>x. P x \<or> Q) = (cBall A P \<or> Q)"
```
```   408   "\<And>A P Q. cBall A (\<lambda>x. P \<or> Q x) = (P \<or> cBall A Q)"
```
```   409   "\<And>A P Q. cBall A (\<lambda>x. P \<longrightarrow> Q x) = (P \<longrightarrow> cBall A Q)"
```
```   410   "\<And>A P Q. cBall A (\<lambda>x. P x \<longrightarrow> Q) = (cBex A P \<longrightarrow> Q)"
```
```   411   "\<And>P. cBall cempty P = True"
```
```   412   "\<And>a B P. cBall (cinsert a B) P = (P a \<and> cBall B P)"
```
```   413   "\<And>A P f. cBall (cimage f A) P = cBall A (\<lambda>x. P (f x))"
```
```   414   "\<And>A P. (\<not> cBall A P) = cBex A (\<lambda>x. \<not> P x)"
```
```   415 by auto
```
```   416
```
```   417 lemma atomize_cBall:
```
```   418     "(\<And>x. cin x A ==> P x) == Trueprop (cBall A (\<lambda>x. P x))"
```
```   419 apply (simp only: atomize_all atomize_imp)
```
```   420 apply (rule equal_intr_rule)
```
```   421 by (transfer, simp)+
```
```   422
```
```   423 subsubsection \<open>@{const cUnion}\<close>
```
```   424
```
```   425 lemma cUNION_cimage: "cUNION (cimage f A) g = cUNION A (g \<circ> f)"
```
```   426 including cset.lifting by transfer auto
```
```   427
```
```   428
```
```   429 subsection \<open>Setup for Lifting/Transfer\<close>
```
```   430
```
```   431 subsubsection \<open>Relator and predicator properties\<close>
```
```   432
```
```   433 lift_definition rel_cset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool"
```
```   434   is rel_set parametric rel_set_transfer .
```
```   435
```
```   436 lemma rel_cset_alt_def:
```
```   437   "rel_cset R a b \<longleftrightarrow>
```
```   438    (\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and>
```
```   439    (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t)"
```
```   440 by(simp add: rel_cset_def rel_set_def)
```
```   441
```
```   442 lemma rel_cset_iff:
```
```   443   "rel_cset R a b \<longleftrightarrow>
```
```   444    (\<forall>t. cin t a \<longrightarrow> (\<exists>u. cin u b \<and> R t u)) \<and>
```
```   445    (\<forall>t. cin t b \<longrightarrow> (\<exists>u. cin u a \<and> R u t))"
```
```   446 by transfer(auto simp add: rel_set_def)
```
```   447
```
```   448 lemma rel_cset_cUNION:
```
```   449   "\<lbrakk> rel_cset Q A B; rel_fun Q (rel_cset R) f g \<rbrakk>
```
```   450   \<Longrightarrow> rel_cset R (cUNION A f) (cUNION B g)"
```
```   451 unfolding rel_fun_def by transfer(erule rel_set_UNION, simp add: rel_fun_def)
```
```   452
```
```   453 lemma rel_cset_csingle_iff [simp]: "rel_cset R (csingle x) (csingle y) \<longleftrightarrow> R x y"
```
```   454 by transfer(auto simp add: rel_set_def)
```
```   455
```
```   456 subsubsection \<open>Transfer rules for the Transfer package\<close>
```
```   457
```
```   458 text \<open>Unconditional transfer rules\<close>
```
```   459
```
```   460 context includes lifting_syntax
```
```   461 begin
```
```   462
```
```   463 lemmas cempty_parametric [transfer_rule] = empty_transfer[Transfer.transferred]
```
```   464
```
```   465 lemma cinsert_parametric [transfer_rule]:
```
```   466   "(A ===> rel_cset A ===> rel_cset A) cinsert cinsert"
```
```   467   unfolding rel_fun_def rel_cset_iff by blast
```
```   468
```
```   469 lemma cUn_parametric [transfer_rule]:
```
```   470   "(rel_cset A ===> rel_cset A ===> rel_cset A) cUn cUn"
```
```   471   unfolding rel_fun_def rel_cset_iff by blast
```
```   472
```
```   473 lemma cUnion_parametric [transfer_rule]:
```
```   474   "(rel_cset (rel_cset A) ===> rel_cset A) cUnion cUnion"
```
```   475   unfolding rel_fun_def
```
```   476   by transfer (auto simp: rel_set_def, metis+)
```
```   477
```
```   478 lemma cimage_parametric [transfer_rule]:
```
```   479   "((A ===> B) ===> rel_cset A ===> rel_cset B) cimage cimage"
```
```   480   unfolding rel_fun_def rel_cset_iff by blast
```
```   481
```
```   482 lemma cBall_parametric [transfer_rule]:
```
```   483   "(rel_cset A ===> (A ===> op =) ===> op =) cBall cBall"
```
```   484   unfolding rel_cset_iff rel_fun_def by blast
```
```   485
```
```   486 lemma cBex_parametric [transfer_rule]:
```
```   487   "(rel_cset A ===> (A ===> op =) ===> op =) cBex cBex"
```
```   488   unfolding rel_cset_iff rel_fun_def by blast
```
```   489
```
```   490 lemma rel_cset_parametric [transfer_rule]:
```
```   491   "((A ===> B ===> op =) ===> rel_cset A ===> rel_cset B ===> op =) rel_cset rel_cset"
```
```   492   unfolding rel_fun_def
```
```   493   using rel_set_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred, where A = A and B = B]
```
```   494   by simp
```
```   495
```
```   496 text \<open>Rules requiring bi-unique, bi-total or right-total relations\<close>
```
```   497
```
```   498 lemma cin_parametric [transfer_rule]:
```
```   499   "bi_unique A \<Longrightarrow> (A ===> rel_cset A ===> op =) cin cin"
```
```   500 unfolding rel_fun_def rel_cset_iff bi_unique_def by metis
```
```   501
```
```   502 lemma cInt_parametric [transfer_rule]:
```
```   503   "bi_unique A \<Longrightarrow> (rel_cset A ===> rel_cset A ===> rel_cset A) cInt cInt"
```
```   504 unfolding rel_fun_def
```
```   505 using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred]
```
```   506 by blast
```
```   507
```
```   508 lemma cDiff_parametric [transfer_rule]:
```
```   509   "bi_unique A \<Longrightarrow> (rel_cset A ===> rel_cset A ===> rel_cset A) cDiff cDiff"
```
```   510 unfolding rel_fun_def
```
```   511 using Diff_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
```
```   512
```
```   513 lemma csubset_parametric [transfer_rule]:
```
```   514   "bi_unique A \<Longrightarrow> (rel_cset A ===> rel_cset A ===> op =) csubset_eq csubset_eq"
```
```   515 unfolding rel_fun_def
```
```   516 using subset_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
```
```   517
```
```   518 end
```
```   519
```
```   520 lifting_update cset.lifting
```
```   521 lifting_forget cset.lifting
```
```   522
```
```   523 subsection \<open>Registration as BNF\<close>
```
```   524
```
```   525 lemma card_of_countable_sets_range:
```
```   526 fixes A :: "'a set"
```
```   527 shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
```
```   528 apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into
```
```   529 unfolding inj_on_def by auto
```
```   530
```
```   531 lemma card_of_countable_sets_Func:
```
```   532 "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq"
```
```   533 using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric]
```
```   534 unfolding cexp_def Field_natLeq Field_card_of
```
```   535 by (rule ordLeq_ordIso_trans)
```
```   536
```
```   537 lemma ordLeq_countable_subsets:
```
```   538 "|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
```
```   539 apply (rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto
```
```   540
```
```   541 lemma finite_countable_subset:
```
```   542 "finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
```
```   543 apply (rule iffI)
```
```   544  apply (erule contrapos_pp)
```
```   545  apply (rule card_of_ordLeq_infinite)
```
```   546  apply (rule ordLeq_countable_subsets)
```
```   547  apply assumption
```
```   548 apply (rule finite_Collect_conjI)
```
```   549 apply (rule disjI1)
```
```   550 apply (erule finite_Collect_subsets)
```
```   551 done
```
```   552
```
```   553 lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
```
```   554   including cset.lifting
```
```   555   apply (rule f_the_inv_into_f[unfolded inj_on_def image_iff])
```
```   556    apply transfer' apply simp
```
```   557   apply transfer' apply simp
```
```   558   done
```
```   559
```
```   560 lemma Collect_Int_Times: "{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
```
```   561 by auto
```
```   562
```
```   563
```
```   564 lemma rel_cset_aux:
```
```   565 "(\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and> (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t) \<longleftrightarrow>
```
```   566  ((BNF_Def.Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage fst))\<inverse>\<inverse> OO
```
```   567    BNF_Def.Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R")
```
```   568 proof
```
```   569   assume ?L
```
```   570   define R' where "R' = the_inv rcset (Collect (case_prod R) \<inter> (rcset a \<times> rcset b))"
```
```   571     (is "_ = the_inv rcset ?L'")
```
```   572   have L: "countable ?L'" by auto
```
```   573   hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset)
```
```   574   thus ?R unfolding Grp_def relcompp.simps conversep.simps including cset.lifting
```
```   575   proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
```
```   576     from * \<open>?L\<close> show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times)
```
```   577     from * \<open>?L\<close> show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times)
```
```   578   qed simp_all
```
```   579 next
```
```   580   assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
```
```   581     by (simp add: subset_eq Ball_def)(transfer, auto simp add: cimage.rep_eq, metis snd_conv, metis fst_conv)
```
```   582 qed
```
```   583
```
```   584 bnf "'a cset"
```
```   585   map: cimage
```
```   586   sets: rcset
```
```   587   bd: natLeq
```
```   588   wits: "cempty"
```
```   589   rel: rel_cset
```
```   590 proof -
```
```   591   show "cimage id = id" by auto
```
```   592 next
```
```   593   fix f g show "cimage (g \<circ> f) = cimage g \<circ> cimage f" by fastforce
```
```   594 next
```
```   595   fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a"
```
```   596   thus "cimage f C = cimage g C" including cset.lifting by transfer force
```
```   597 next
```
```   598   fix f show "rcset \<circ> cimage f = op ` f \<circ> rcset" including cset.lifting by transfer' fastforce
```
```   599 next
```
```   600   show "card_order natLeq" by (rule natLeq_card_order)
```
```   601 next
```
```   602   show "cinfinite natLeq" by (rule natLeq_cinfinite)
```
```   603 next
```
```   604   fix C show "|rcset C| \<le>o natLeq"
```
```   605     including cset.lifting by transfer (unfold countable_card_le_natLeq)
```
```   606 next
```
```   607   fix R S
```
```   608   show "rel_cset R OO rel_cset S \<le> rel_cset (R OO S)"
```
```   609     unfolding rel_cset_alt_def[abs_def] by fast
```
```   610 next
```
```   611   fix R
```
```   612   show "rel_cset R = (\<lambda>x y. \<exists>z. rcset z \<subseteq> {(x, y). R x y} \<and>
```
```   613     cimage fst z = x \<and> cimage snd z = y)"
```
```   614   unfolding rel_cset_alt_def[abs_def] rel_cset_aux[unfolded OO_Grp_alt] by simp
```
```   615 qed(simp add: bot_cset.rep_eq)
```
```   616
```
```   617 end
```