src/HOL/Cardinals/Bounded_Set.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 63167 0909deb8059b
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned;
wenzelm@60247
     1
(*  Title:      HOL/Cardinals/Bounded_Set.thy
traytel@59747
     2
    Author:     Dmitriy Traytel, TU Muenchen
traytel@59747
     3
    Copyright   2015
traytel@59747
     4
traytel@59747
     5
Bounded powerset type.
traytel@59747
     6
*)
traytel@59747
     7
traytel@59747
     8
section \<open>Sets Strictly Bounded by an Infinite Cardinal\<close>
traytel@59747
     9
traytel@59747
    10
theory Bounded_Set
traytel@59747
    11
imports Cardinals
traytel@59747
    12
begin
traytel@59747
    13
traytel@59747
    14
typedef ('a, 'k) bset ("_ set[_]" [22, 21] 21) =
traytel@59747
    15
  "{A :: 'a set. |A| <o natLeq +c |UNIV :: 'k set|}"
traytel@59747
    16
  morphisms set_bset Abs_bset
traytel@59747
    17
  by (rule exI[of _ "{}"]) (auto simp: card_of_empty4 csum_def)
traytel@59747
    18
traytel@59747
    19
setup_lifting type_definition_bset
traytel@59747
    20
traytel@59747
    21
lift_definition map_bset ::
traytel@59747
    22
  "('a \<Rightarrow> 'b) \<Rightarrow> 'a set['k] \<Rightarrow> 'b set['k]" is image
traytel@59747
    23
  using card_of_image ordLeq_ordLess_trans by blast
traytel@59747
    24
traytel@59747
    25
lift_definition rel_bset ::
traytel@59747
    26
  "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set['k] \<Rightarrow> 'b set['k] \<Rightarrow> bool" is rel_set
traytel@59747
    27
  .
traytel@59747
    28
traytel@59747
    29
lift_definition bempty :: "'a set['k]" is "{}"
traytel@59747
    30
  by (auto simp: card_of_empty4 csum_def)
traytel@59747
    31
traytel@59747
    32
lift_definition binsert :: "'a \<Rightarrow> 'a set['k] \<Rightarrow> 'a set['k]" is "insert"
traytel@59747
    33
  using infinite_card_of_insert ordIso_ordLess_trans Field_card_of Field_natLeq UNIV_Plus_UNIV
traytel@59747
    34
   csum_def finite_Plus_UNIV_iff finite_insert finite_ordLess_infinite2 infinite_UNIV_nat by metis
traytel@59747
    35
traytel@59747
    36
definition bsingleton where
traytel@59747
    37
  "bsingleton x = binsert x bempty"
traytel@59747
    38
traytel@59747
    39
lemma set_bset_to_set_bset: "|A| <o natLeq +c |UNIV :: 'k set| \<Longrightarrow>
traytel@59747
    40
  set_bset (the_inv set_bset A :: 'a set['k]) = A"
traytel@59747
    41
  apply (rule f_the_inv_into_f[unfolded inj_on_def])
traytel@59747
    42
  apply (simp add: set_bset_inject range_eqI Abs_bset_inverse[symmetric])
traytel@59747
    43
  apply (rule range_eqI Abs_bset_inverse[symmetric] CollectI)+
traytel@59747
    44
  .
traytel@59747
    45
traytel@59747
    46
lemma rel_bset_aux_infinite:
traytel@59747
    47
  fixes a :: "'a set['k]" and b :: "'b set['k]"
traytel@59747
    48
  shows "(\<forall>t \<in> set_bset a. \<exists>u \<in> set_bset b. R t u) \<and> (\<forall>u \<in> set_bset b. \<exists>t \<in> set_bset a. R t u) \<longleftrightarrow>
traytel@59747
    49
   ((BNF_Def.Grp {a. set_bset a \<subseteq> {(a, b). R a b}} (map_bset fst))\<inverse>\<inverse> OO
traytel@59747
    50
    BNF_Def.Grp {a. set_bset a \<subseteq> {(a, b). R a b}} (map_bset snd)) a b" (is "?L \<longleftrightarrow> ?R")
traytel@59747
    51
proof
traytel@59747
    52
  assume ?L
wenzelm@63040
    53
  define R' :: "('a \<times> 'b) set['k]"
wenzelm@63040
    54
    where "R' = the_inv set_bset (Collect (case_prod R) \<inter> (set_bset a \<times> set_bset b))"
wenzelm@63040
    55
      (is "_ = the_inv set_bset ?L'")
traytel@59747
    56
  have "|?L'| <o natLeq +c |UNIV :: 'k set|"
traytel@59747
    57
    unfolding csum_def Field_natLeq
traytel@59747
    58
    by (intro ordLeq_ordLess_trans[OF card_of_mono1[OF Int_lower2]]
traytel@59747
    59
      card_of_Times_ordLess_infinite)
traytel@59747
    60
      (simp, (transfer, simp add: csum_def Field_natLeq)+)
traytel@59747
    61
  hence *: "set_bset R' = ?L'" unfolding R'_def by (intro set_bset_to_set_bset)
traytel@59747
    62
  show ?R unfolding Grp_def relcompp.simps conversep.simps
traytel@59747
    63
  proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
wenzelm@63167
    64
    from * show "a = map_bset fst R'" using conjunct1[OF \<open>?L\<close>]
traytel@59747
    65
      by (transfer, auto simp add: image_def Int_def split: prod.splits)
wenzelm@63167
    66
    from * show "b = map_bset snd R'" using conjunct2[OF \<open>?L\<close>]
traytel@59747
    67
      by (transfer, auto simp add: image_def Int_def split: prod.splits)
traytel@59747
    68
  qed (auto simp add: *)
traytel@59747
    69
next
traytel@59747
    70
  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
traytel@59747
    71
    by transfer force
traytel@59747
    72
qed
traytel@59747
    73
traytel@59747
    74
bnf "'a set['k]"
traytel@59747
    75
  map: map_bset
traytel@59747
    76
  sets: set_bset
traytel@59747
    77
  bd: "natLeq +c |UNIV :: 'k set|"
traytel@59747
    78
  wits: bempty
traytel@59747
    79
  rel: rel_bset
traytel@59747
    80
proof -
traytel@59747
    81
  show "map_bset id = id" by (rule ext, transfer) simp
traytel@59747
    82
next
traytel@59747
    83
  fix f g
traytel@59747
    84
  show "map_bset (f o g) = map_bset f o map_bset g" by (rule ext, transfer) auto
traytel@59747
    85
next
traytel@59747
    86
  fix X f g
traytel@59747
    87
  assume "\<And>z. z \<in> set_bset X \<Longrightarrow> f z = g z"
traytel@59747
    88
  then show "map_bset f X = map_bset g X" by transfer force
traytel@59747
    89
next
traytel@59747
    90
  fix f
traytel@59747
    91
  show "set_bset \<circ> map_bset f = op ` f \<circ> set_bset" by (rule ext, transfer) auto
traytel@59747
    92
next
traytel@59747
    93
  fix X :: "'a set['k]"
traytel@59747
    94
  show "|set_bset X| \<le>o natLeq +c |UNIV :: 'k set|"
traytel@59747
    95
    by transfer (blast dest: ordLess_imp_ordLeq)
traytel@59747
    96
next
traytel@59747
    97
  fix R S
traytel@59747
    98
  show "rel_bset R OO rel_bset S \<le> rel_bset (R OO S)"
traytel@59747
    99
    by (rule predicate2I, transfer) (auto simp: rel_set_OO[symmetric])
traytel@59747
   100
next
traytel@59747
   101
  fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
traytel@62324
   102
  show "rel_bset R = ((\<lambda>x y. \<exists>z. set_bset z \<subseteq> {(x, y). R x y} \<and>
traytel@62324
   103
    map_bset fst z = x \<and> map_bset snd z = y) :: 'a set['k] \<Rightarrow> 'b set['k] \<Rightarrow> bool)"
traytel@62324
   104
    by (simp add: rel_bset_def map_fun_def o_def rel_set_def
traytel@62324
   105
      rel_bset_aux_infinite[unfolded OO_Grp_alt])
traytel@59747
   106
next
traytel@59747
   107
  fix x
traytel@59747
   108
  assume "x \<in> set_bset bempty"
traytel@59747
   109
  then show False by transfer simp
traytel@59747
   110
qed (simp_all add: card_order_csum natLeq_card_order cinfinite_csum natLeq_cinfinite)
traytel@59747
   111
traytel@59747
   112
traytel@59747
   113
lemma map_bset_bempty[simp]: "map_bset f bempty = bempty"
traytel@59747
   114
  by transfer auto
traytel@59747
   115
traytel@59747
   116
lemma map_bset_binsert[simp]: "map_bset f (binsert x X) = binsert (f x) (map_bset f X)"
traytel@59747
   117
  by transfer auto
traytel@59747
   118
traytel@59747
   119
lemma map_bset_bsingleton: "map_bset f (bsingleton x) = bsingleton (f x)"
traytel@59747
   120
  unfolding bsingleton_def by simp
traytel@59747
   121
traytel@59747
   122
lemma bempty_not_binsert: "bempty \<noteq> binsert x X" "binsert x X \<noteq> bempty"
traytel@59747
   123
  by (transfer, auto)+
traytel@59747
   124
traytel@59747
   125
lemma bempty_not_bsingleton[simp]: "bempty \<noteq> bsingleton x" "bsingleton x \<noteq> bempty"
traytel@59747
   126
  unfolding bsingleton_def by (simp_all add: bempty_not_binsert)
traytel@59747
   127
traytel@59747
   128
lemma bsingleton_inj[simp]: "bsingleton x = bsingleton y \<longleftrightarrow> x = y"
traytel@59747
   129
  unfolding bsingleton_def by transfer auto
traytel@59747
   130
traytel@59747
   131
lemma rel_bsingleton[simp]:
traytel@59747
   132
  "rel_bset R (bsingleton x1) (bsingleton x2) = R x1 x2"
traytel@59747
   133
  unfolding bsingleton_def
traytel@59747
   134
  by transfer (auto simp: rel_set_def)
traytel@59747
   135
traytel@59747
   136
lemma rel_bset_bsingleton[simp]:
traytel@59747
   137
  "rel_bset R (bsingleton x1) = (\<lambda>X. X \<noteq> bempty \<and> (\<forall>x2\<in>set_bset X. R x1 x2))"
traytel@59747
   138
  "rel_bset R X (bsingleton x2) = (X \<noteq> bempty \<and> (\<forall>x1\<in>set_bset X. R x1 x2))"
traytel@59747
   139
  unfolding bsingleton_def fun_eq_iff
traytel@59747
   140
  by (transfer, force simp add: rel_set_def)+
traytel@59747
   141
traytel@59747
   142
lemma rel_bset_bempty[simp]:
traytel@59747
   143
  "rel_bset R bempty X = (X = bempty)"
traytel@59747
   144
  "rel_bset R Y bempty = (Y = bempty)"
traytel@59747
   145
  by (transfer, simp add: rel_set_def)+
traytel@59747
   146
traytel@59747
   147
definition bset_of_option where
traytel@59747
   148
  "bset_of_option = case_option bempty bsingleton"
traytel@59747
   149
traytel@59747
   150
lift_definition bgraph :: "('a \<Rightarrow> 'b option) \<Rightarrow> ('a \<times> 'b) set['a set]" is
traytel@59747
   151
  "\<lambda>f. {(a, b). f a = Some b}"
traytel@59747
   152
proof -
traytel@59747
   153
  fix f :: "'a \<Rightarrow> 'b option"
traytel@59747
   154
  have "|{(a, b). f a = Some b}| \<le>o |UNIV :: 'a set|"
traytel@59747
   155
    by (rule surj_imp_ordLeq[of _ "\<lambda>x. (x, the (f x))"]) auto
traytel@59747
   156
  also have "|UNIV :: 'a set| <o |UNIV :: 'a set set|"
traytel@59747
   157
    by simp
traytel@59747
   158
  also have "|UNIV :: 'a set set| \<le>o natLeq +c |UNIV :: 'a set set|"
traytel@59747
   159
    by (rule ordLeq_csum2) simp
traytel@59747
   160
  finally show "|{(a, b). f a = Some b}| <o natLeq +c |UNIV :: 'a set set|" .
traytel@59747
   161
qed
traytel@59747
   162
traytel@59747
   163
lemma rel_bset_False[simp]: "rel_bset (\<lambda>x y. False) x y = (x = bempty \<and> y = bempty)"
traytel@59747
   164
  by transfer (auto simp: rel_set_def)
traytel@59747
   165
traytel@59747
   166
lemma rel_bset_of_option[simp]:
traytel@59747
   167
  "rel_bset R (bset_of_option x1) (bset_of_option x2) = rel_option R x1 x2"
traytel@59747
   168
  unfolding bset_of_option_def bsingleton_def[abs_def]
traytel@59747
   169
  by transfer (auto simp: rel_set_def split: option.splits)
traytel@59747
   170
traytel@59747
   171
lemma rel_bgraph[simp]:
traytel@59747
   172
  "rel_bset (rel_prod (op =) R) (bgraph f1) (bgraph f2) = rel_fun (op =) (rel_option R) f1 f2"
traytel@59747
   173
  apply transfer
traytel@59747
   174
  apply (auto simp: rel_fun_def rel_option_iff rel_set_def split: option.splits)
traytel@59747
   175
  using option.collapse apply fastforce+
traytel@59747
   176
  done
traytel@59747
   177
traytel@59747
   178
lemma set_bset_bsingleton[simp]:
traytel@59747
   179
  "set_bset (bsingleton x) = {x}"
traytel@59747
   180
  unfolding bsingleton_def by transfer auto
traytel@59747
   181
traytel@59747
   182
lemma binsert_absorb[simp]: "binsert a (binsert a x) = binsert a x"
traytel@59747
   183
  by transfer simp
traytel@59747
   184
traytel@59747
   185
lemma map_bset_eq_bempty_iff[simp]: "map_bset f X = bempty \<longleftrightarrow> X = bempty"
traytel@59747
   186
  by transfer auto
traytel@59747
   187
traytel@59747
   188
lemma map_bset_eq_bsingleton_iff[simp]:
traytel@59747
   189
  "map_bset f X = bsingleton x \<longleftrightarrow> (set_bset X \<noteq> {} \<and> (\<forall>y \<in> set_bset X. f y = x))"
traytel@59747
   190
  unfolding bsingleton_def by transfer auto
traytel@59747
   191
traytel@59747
   192
lift_definition bCollect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set['a set]" is Collect
traytel@59747
   193
  apply (rule ordLeq_ordLess_trans[OF card_of_mono1[OF subset_UNIV]])
traytel@59747
   194
  apply (rule ordLess_ordLeq_trans[OF card_of_set_type])
traytel@59747
   195
  apply (rule ordLeq_csum2[OF card_of_Card_order])
traytel@59747
   196
  done
traytel@59747
   197
traytel@59747
   198
lift_definition bmember :: "'a \<Rightarrow> 'a set['k] \<Rightarrow> bool" is "op \<in>" .
traytel@59747
   199
traytel@59747
   200
lemma bmember_bCollect[simp]: "bmember a (bCollect P) = P a"
traytel@59747
   201
  by transfer simp
traytel@59747
   202
traytel@59747
   203
lemma bset_eq_iff: "A = B \<longleftrightarrow> (\<forall>a. bmember a A = bmember a B)"
traytel@59747
   204
  by transfer auto
traytel@59747
   205
traytel@59747
   206
(* FIXME: Lifting does not work with dead variables,
traytel@59747
   207
   that is why we are hiding the below setup in a locale*)
traytel@59747
   208
locale bset_lifting
traytel@59747
   209
begin
traytel@59747
   210
traytel@59747
   211
declare bset.rel_eq[relator_eq]
traytel@59747
   212
declare bset.rel_mono[relator_mono]
traytel@59747
   213
declare bset.rel_compp[symmetric, relator_distr]
traytel@59747
   214
declare bset.rel_transfer[transfer_rule]
traytel@59747
   215
traytel@59747
   216
lemma bset_quot_map[quot_map]: "Quotient R Abs Rep T \<Longrightarrow>
traytel@59747
   217
  Quotient (rel_bset R) (map_bset Abs) (map_bset Rep) (rel_bset T)"
traytel@59747
   218
  unfolding Quotient_alt_def5 bset.rel_Grp[of UNIV, simplified, symmetric]
traytel@59747
   219
    bset.rel_conversep[symmetric] bset.rel_compp[symmetric]
traytel@59747
   220
    by (auto elim: bset.rel_mono_strong)
traytel@59747
   221
traytel@59747
   222
lemma set_relator_eq_onp [relator_eq_onp]:
traytel@59747
   223
  "rel_bset (eq_onp P) = eq_onp (\<lambda>A. Ball (set_bset A) P)"
traytel@59747
   224
  unfolding fun_eq_iff eq_onp_def by transfer (auto simp: rel_set_def)
traytel@59747
   225
traytel@59747
   226
end
traytel@59747
   227
traytel@59747
   228
end