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