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