src/HOL/Library/FSet.thy
changeset 55129 26bd1cba3ab5
parent 54258 adfc759263ab
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Library/FSet.thy	Thu Jan 23 19:02:22 2014 +0100
     1.2 +++ b/src/HOL/Library/FSet.thy	Fri Jan 24 11:51:45 2014 +0100
     1.3 @@ -1,12 +1,13 @@
     1.4  (*  Title:      HOL/Library/FSet.thy
     1.5      Author:     Ondrej Kuncar, TU Muenchen
     1.6      Author:     Cezary Kaliszyk and Christian Urban
     1.7 +    Author:     Andrei Popescu, TU Muenchen
     1.8  *)
     1.9  
    1.10  header {* Type of finite sets defined as a subtype of sets *}
    1.11  
    1.12  theory FSet
    1.13 -imports Main Conditionally_Complete_Lattices
    1.14 +imports Conditionally_Complete_Lattices
    1.15  begin
    1.16  
    1.17  subsection {* Definition of the type *}
    1.18 @@ -16,6 +17,7 @@
    1.19  
    1.20  setup_lifting type_definition_fset
    1.21  
    1.22 +
    1.23  subsection {* Basic operations and type class instantiations *}
    1.24  
    1.25  (* FIXME transfer and right_total vs. bi_total *)
    1.26 @@ -148,6 +150,7 @@
    1.27  abbreviation fUNIV :: "'a::finite fset" where "fUNIV \<equiv> top"
    1.28  abbreviation fuminus :: "'a::finite fset \<Rightarrow> 'a fset" ("|-| _" [81] 80) where "|-| x \<equiv> uminus x"
    1.29  
    1.30 +
    1.31  subsection {* Other operations *}
    1.32  
    1.33  lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer
    1.34 @@ -167,6 +170,7 @@
    1.35  
    1.36  context
    1.37  begin
    1.38 +
    1.39  interpretation lifting_syntax .
    1.40  
    1.41  lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter 
    1.42 @@ -203,6 +207,7 @@
    1.43  
    1.44  lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold ..
    1.45  
    1.46 +
    1.47  subsection {* Transferred lemmas from Set.thy *}
    1.48  
    1.49  lemmas fset_eqI = set_eqI[Transfer.transferred]
    1.50 @@ -442,12 +447,14 @@
    1.51  lemmas ffmember_filter[simp] = member_filter[Transfer.transferred]
    1.52  lemmas fequalityI = equalityI[Transfer.transferred]
    1.53  
    1.54 +
    1.55  subsection {* Additional lemmas*}
    1.56  
    1.57  subsubsection {* @{text fsingleton} *}
    1.58  
    1.59  lemmas fsingletonE = fsingletonD [elim_format]
    1.60  
    1.61 +
    1.62  subsubsection {* @{text femepty} *}
    1.63  
    1.64  lemma fempty_ffilter[simp]: "ffilter (\<lambda>_. False) A = {||}"
    1.65 @@ -457,6 +464,7 @@
    1.66  lemma femptyE [elim!]: "a |\<in>| {||} \<Longrightarrow> P"
    1.67    by simp
    1.68  
    1.69 +
    1.70  subsubsection {* @{text fset} *}
    1.71  
    1.72  lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq
    1.73 @@ -479,6 +487,7 @@
    1.74  
    1.75  lemmas minus_fset[simp] = minus_fset.rep_eq
    1.76  
    1.77 +
    1.78  subsubsection {* @{text filter_fset} *}
    1.79  
    1.80  lemma subset_ffilter: 
    1.81 @@ -494,6 +503,7 @@
    1.82      ffilter P A |\<subset>| ffilter Q A"
    1.83    unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
    1.84  
    1.85 +
    1.86  subsubsection {* @{text finsert} *}
    1.87  
    1.88  (* FIXME, transferred doesn't work here *)
    1.89 @@ -505,11 +515,13 @@
    1.90  lemma mk_disjoint_finsert: "a |\<in>| A \<Longrightarrow> \<exists>B. A = finsert a B \<and> a |\<notin>| B"
    1.91    by (rule_tac x = "A |-| {|a|}" in exI, blast)
    1.92  
    1.93 +
    1.94  subsubsection {* @{text fimage} *}
    1.95  
    1.96  lemma subset_fimage_iff: "(B |\<subseteq>| f|`|A) = (\<exists> AA. AA |\<subseteq>| A \<and> B = f|`|AA)"
    1.97  by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff)
    1.98  
    1.99 +
   1.100  subsubsection {* bounded quantification *}
   1.101  
   1.102  lemma bex_simps [simp, no_atp]:
   1.103 @@ -540,6 +552,7 @@
   1.104  
   1.105  end
   1.106  
   1.107 +
   1.108  subsubsection {* @{text fcard} *}
   1.109  
   1.110  (* FIXME: improve transferred to handle bounded meta quantification *)
   1.111 @@ -622,6 +635,7 @@
   1.112  lemma fcard_pfsubset: "A |\<subseteq>| B \<Longrightarrow> fcard A < fcard B \<Longrightarrow> A < B"
   1.113  by transfer (rule card_psubset)
   1.114  
   1.115 +
   1.116  subsubsection {* @{text ffold} *}
   1.117  
   1.118  (* FIXME: improve transferred to handle bounded meta quantification *)
   1.119 @@ -680,6 +694,7 @@
   1.120  
   1.121  end
   1.122  
   1.123 +
   1.124  subsection {* Choice in fsets *}
   1.125  
   1.126  lemma fset_choice: 
   1.127 @@ -687,6 +702,7 @@
   1.128    shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
   1.129    using assms by transfer metis
   1.130  
   1.131 +
   1.132  subsection {* Induction and Cases rules for fsets *}
   1.133  
   1.134  lemma fset_exhaust [case_names empty insert, cases type: fset]:
   1.135 @@ -752,6 +768,7 @@
   1.136    apply simp_all
   1.137    done
   1.138  
   1.139 +
   1.140  subsection {* Setup for Lifting/Transfer *}
   1.141  
   1.142  subsubsection {* Relator and predicator properties *}
   1.143 @@ -851,6 +868,7 @@
   1.144  
   1.145  lemmas fset_invariant_commute [invariant_commute] = set_invariant_commute[Transfer.transferred]
   1.146  
   1.147 +
   1.148  subsubsection {* Quotient theorem for the Lifting package *}
   1.149  
   1.150  lemma Quotient_fset_map[quot_map]:
   1.151 @@ -859,6 +877,7 @@
   1.152    using assms unfolding Quotient_alt_def4
   1.153    by (simp add: fset_rel_OO[symmetric] fset_rel_conversep) (simp add: fset_rel_alt_def, blast)
   1.154  
   1.155 +
   1.156  subsubsection {* Transfer rules for the Transfer package *}
   1.157  
   1.158  text {* Unconditional transfer rules *}
   1.159 @@ -971,4 +990,137 @@
   1.160  lifting_update fset.lifting
   1.161  lifting_forget fset.lifting
   1.162  
   1.163 +
   1.164 +subsection {* BNF setup *}
   1.165 +
   1.166 +context
   1.167 +includes fset.lifting
   1.168 +begin
   1.169 +
   1.170 +lemma fset_rel_alt:
   1.171 +  "fset_rel R a b \<longleftrightarrow> (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
   1.172 +by transfer (simp add: set_rel_def)
   1.173 +
   1.174 +lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
   1.175 +apply (rule f_the_inv_into_f[unfolded inj_on_def])
   1.176 +apply (simp add: fset_inject)
   1.177 +apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+
   1.178 +.
   1.179 +
   1.180 +lemma fset_rel_aux:
   1.181 +"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
   1.182 + ((BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
   1.183 +  BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
   1.184 +proof
   1.185 +  assume ?L
   1.186 +  def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
   1.187 +  have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
   1.188 +  hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
   1.189 +  show ?R unfolding Grp_def relcompp.simps conversep.simps
   1.190 +  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
   1.191 +    from * show "a = fimage fst R'" using conjunct1[OF `?L`]
   1.192 +      by (transfer, auto simp add: image_def Int_def split: prod.splits)
   1.193 +    from * show "b = fimage snd R'" using conjunct2[OF `?L`]
   1.194 +      by (transfer, auto simp add: image_def Int_def split: prod.splits)
   1.195 +  qed (auto simp add: *)
   1.196 +next
   1.197 +  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
   1.198 +  apply (simp add: subset_eq Ball_def)
   1.199 +  apply (rule conjI)
   1.200 +  apply (transfer, clarsimp, metis snd_conv)
   1.201 +  by (transfer, clarsimp, metis fst_conv)
   1.202 +qed
   1.203 +
   1.204 +bnf "'a fset"
   1.205 +  map: fimage
   1.206 +  sets: fset 
   1.207 +  bd: natLeq
   1.208 +  wits: "{||}"
   1.209 +  rel: fset_rel
   1.210 +apply -
   1.211 +          apply transfer' apply simp
   1.212 +         apply transfer' apply force
   1.213 +        apply transfer apply force
   1.214 +       apply transfer' apply force
   1.215 +      apply (rule natLeq_card_order)
   1.216 +     apply (rule natLeq_cinfinite)
   1.217 +    apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
   1.218 +   apply (fastforce simp: fset_rel_alt)
   1.219 + apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux) 
   1.220 +apply transfer apply simp
   1.221 +done
   1.222 +
   1.223 +lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
   1.224 +  by transfer (rule refl)
   1.225 +
   1.226  end
   1.227 +
   1.228 +lemmas [simp] = fset.map_comp fset.map_id fset.set_map
   1.229 +
   1.230 +
   1.231 +subsection {* Advanced relator customization *}
   1.232 +
   1.233 +(* Set vs. sum relators: *)
   1.234 +
   1.235 +lemma set_rel_sum_rel[simp]: 
   1.236 +"set_rel (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow> 
   1.237 + set_rel \<chi> (Inl -` A1) (Inl -` A2) \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
   1.238 +(is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
   1.239 +proof safe
   1.240 +  assume L: "?L"
   1.241 +  show ?Rl unfolding set_rel_def Bex_def vimage_eq proof safe
   1.242 +    fix l1 assume "Inl l1 \<in> A1"
   1.243 +    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inl l1) a2"
   1.244 +    using L unfolding set_rel_def by auto
   1.245 +    then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto)
   1.246 +    thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto
   1.247 +  next
   1.248 +    fix l2 assume "Inl l2 \<in> A2"
   1.249 +    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inl l2)"
   1.250 +    using L unfolding set_rel_def by auto
   1.251 +    then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto)
   1.252 +    thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto
   1.253 +  qed
   1.254 +  show ?Rr unfolding set_rel_def Bex_def vimage_eq proof safe
   1.255 +    fix r1 assume "Inr r1 \<in> A1"
   1.256 +    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inr r1) a2"
   1.257 +    using L unfolding set_rel_def by auto
   1.258 +    then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto)
   1.259 +    thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto
   1.260 +  next
   1.261 +    fix r2 assume "Inr r2 \<in> A2"
   1.262 +    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inr r2)"
   1.263 +    using L unfolding set_rel_def by auto
   1.264 +    then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto)
   1.265 +    thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto
   1.266 +  qed
   1.267 +next
   1.268 +  assume Rl: "?Rl" and Rr: "?Rr"
   1.269 +  show ?L unfolding set_rel_def Bex_def vimage_eq proof safe
   1.270 +    fix a1 assume a1: "a1 \<in> A1"
   1.271 +    show "\<exists> a2. a2 \<in> A2 \<and> sum_rel \<chi> \<phi> a1 a2"
   1.272 +    proof(cases a1)
   1.273 +      case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2"
   1.274 +      using Rl a1 unfolding set_rel_def by blast
   1.275 +      thus ?thesis unfolding Inl by auto
   1.276 +    next
   1.277 +      case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2"
   1.278 +      using Rr a1 unfolding set_rel_def by blast
   1.279 +      thus ?thesis unfolding Inr by auto
   1.280 +    qed
   1.281 +  next
   1.282 +    fix a2 assume a2: "a2 \<in> A2"
   1.283 +    show "\<exists> a1. a1 \<in> A1 \<and> sum_rel \<chi> \<phi> a1 a2"
   1.284 +    proof(cases a2)
   1.285 +      case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2"
   1.286 +      using Rl a2 unfolding set_rel_def by blast
   1.287 +      thus ?thesis unfolding Inl by auto
   1.288 +    next
   1.289 +      case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2"
   1.290 +      using Rr a2 unfolding set_rel_def by blast
   1.291 +      thus ?thesis unfolding Inr by auto
   1.292 +    qed
   1.293 +  qed
   1.294 +qed
   1.295 +
   1.296 +end