material on finite sets
authorLars Hupel <lars.hupel@mytum.de>
Thu Aug 30 10:42:42 2018 +0200 (9 months ago)
changeset 6890934e777447ed5
parent 68908 abc338d25640
child 68910 a21202dfe3eb
material on finite sets
src/HOL/Library/Finite_Map.thy
     1.1 --- a/src/HOL/Library/Finite_Map.thy	Tue Sep 04 16:23:54 2018 +0200
     1.2 +++ b/src/HOL/Library/Finite_Map.thy	Thu Aug 30 10:42:42 2018 +0200
     1.3 @@ -378,43 +378,43 @@
     1.4  unfolding fmfilter_alt_defs by simp
     1.5  
     1.6  lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m"
     1.7 -  by (rule fmap_ext) auto
     1.8 +by (rule fmap_ext) auto
     1.9  
    1.10  lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m"
    1.11 -  by (rule fmap_ext) auto
    1.12 +by (rule fmap_ext) auto
    1.13  
    1.14  lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty"
    1.15 -  unfolding fmfilter_alt_defs by simp
    1.16 +unfolding fmfilter_alt_defs by simp
    1.17  
    1.18  lemma fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty"
    1.19 -  unfolding fmfilter_alt_defs by simp
    1.20 +unfolding fmfilter_alt_defs by simp
    1.21  
    1.22  lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty"
    1.23 -  unfolding fmfilter_alt_defs by simp
    1.24 +unfolding fmfilter_alt_defs by simp
    1.25  
    1.26  lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty"
    1.27 -  unfolding fmfilter_alt_defs by simp
    1.28 +unfolding fmfilter_alt_defs by simp
    1.29  
    1.30  lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty"
    1.31 -  unfolding fmfilter_alt_defs by simp
    1.32 +unfolding fmfilter_alt_defs by simp
    1.33  
    1.34  lemma fmdrop_set_null[simp]: "fmdrop_set {} m = m"
    1.35 -  by (rule fmap_ext) auto
    1.36 +by (rule fmap_ext) auto
    1.37  
    1.38  lemma fmdrop_fset_null[simp]: "fmdrop_fset {||} m = m"
    1.39 -  by (rule fmap_ext) auto
    1.40 +by (rule fmap_ext) auto
    1.41  
    1.42  lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m"
    1.43 -  unfolding fmfilter_alt_defs by simp
    1.44 +unfolding fmfilter_alt_defs by simp
    1.45  
    1.46  lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m"
    1.47 -  unfolding fmfilter_alt_defs by simp
    1.48 +unfolding fmfilter_alt_defs by simp
    1.49  
    1.50  lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty"
    1.51 -  unfolding fmfilter_alt_defs by simp
    1.52 +unfolding fmfilter_alt_defs by simp
    1.53  
    1.54  lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty"
    1.55 -  unfolding fmfilter_alt_defs by simp
    1.56 +unfolding fmfilter_alt_defs by simp
    1.57  
    1.58  lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)"
    1.59  unfolding fmfilter_alt_defs by (rule fmfilter_comm)
    1.60 @@ -438,30 +438,30 @@
    1.61  lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \<union> fmdom' n" by transfer' auto
    1.62  
    1.63  lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
    1.64 -  by (rule fmap_ext) auto
    1.65 +by (rule fmap_ext) auto
    1.66  
    1.67  lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
    1.68 -  by (rule fmap_ext) auto
    1.69 +by (rule fmap_ext) auto
    1.70  
    1.71  lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n"
    1.72  by transfer' (auto simp: map_filter_def map_add_def)
    1.73  
    1.74  lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n"
    1.75 -  unfolding fmfilter_alt_defs by simp
    1.76 +unfolding fmfilter_alt_defs by simp
    1.77  
    1.78  lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n"
    1.79 -  unfolding fmfilter_alt_defs by simp
    1.80 +unfolding fmfilter_alt_defs by simp
    1.81  
    1.82  lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n"
    1.83 -  unfolding fmfilter_alt_defs by simp
    1.84 +unfolding fmfilter_alt_defs by simp
    1.85  
    1.86  lemma fmrestrict_set_add_distrib[simp]:
    1.87    "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n"
    1.88 -  unfolding fmfilter_alt_defs by simp
    1.89 +unfolding fmfilter_alt_defs by simp
    1.90  
    1.91  lemma fmrestrict_fset_add_distrib[simp]:
    1.92    "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n"
    1.93 -  unfolding fmfilter_alt_defs by simp
    1.94 +unfolding fmfilter_alt_defs by simp
    1.95  
    1.96  lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m"
    1.97  by (transfer'; auto)+
    1.98 @@ -527,19 +527,19 @@
    1.99  by transfer' (auto simp: map_pred_def map_filter_def)
   1.100  
   1.101  lemma fmpred_drop[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop a m)"
   1.102 -  by (auto simp: fmfilter_alt_defs)
   1.103 +by (auto simp: fmfilter_alt_defs)
   1.104  
   1.105  lemma fmpred_drop_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_set A m)"
   1.106 -  by (auto simp: fmfilter_alt_defs)
   1.107 +by (auto simp: fmfilter_alt_defs)
   1.108  
   1.109  lemma fmpred_drop_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_fset A m)"
   1.110 -  by (auto simp: fmfilter_alt_defs)
   1.111 +by (auto simp: fmfilter_alt_defs)
   1.112  
   1.113  lemma fmpred_restrict_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_set A m)"
   1.114 -  by (auto simp: fmfilter_alt_defs)
   1.115 +by (auto simp: fmfilter_alt_defs)
   1.116  
   1.117  lemma fmpred_restrict_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_fset A m)"
   1.118 -  by (auto simp: fmfilter_alt_defs)
   1.119 +by (auto simp: fmfilter_alt_defs)
   1.120  
   1.121  lemma fmpred_cases[consumes 1]:
   1.122    assumes "fmpred P m"
   1.123 @@ -590,7 +590,6 @@
   1.124  lemma fset_of_fmap_iff'[simp]: "(a, b) \<in> fset (fset_of_fmap m) \<longleftrightarrow> fmlookup m a = Some b"
   1.125  by transfer' (auto simp: set_of_map_def)
   1.126  
   1.127 -
   1.128  lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
   1.129    is map_of
   1.130    parametric map_of_transfer
   1.131 @@ -819,19 +818,19 @@
   1.132  unfolding fmrel_iff by auto
   1.133  
   1.134  lemma fmrel_drop[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop a m) (fmdrop a n)"
   1.135 -  unfolding fmfilter_alt_defs by blast
   1.136 +unfolding fmfilter_alt_defs by blast
   1.137  
   1.138  lemma fmrel_drop_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_set A m) (fmdrop_set A n)"
   1.139 -  unfolding fmfilter_alt_defs by blast
   1.140 +unfolding fmfilter_alt_defs by blast
   1.141  
   1.142  lemma fmrel_drop_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_fset A m) (fmdrop_fset A n)"
   1.143 -  unfolding fmfilter_alt_defs by blast
   1.144 +unfolding fmfilter_alt_defs by blast
   1.145  
   1.146  lemma fmrel_restrict_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_set A m) (fmrestrict_set A n)"
   1.147 -  unfolding fmfilter_alt_defs by blast
   1.148 +unfolding fmfilter_alt_defs by blast
   1.149  
   1.150  lemma fmrel_restrict_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)"
   1.151 -  unfolding fmfilter_alt_defs by blast
   1.152 +unfolding fmfilter_alt_defs by blast
   1.153  
   1.154  lemma fmrel_on_fset_fmrel_restrict:
   1.155    "fmrel_on_fset S P m n \<longleftrightarrow> fmrel P (fmrestrict_fset S m) (fmrestrict_fset S n)"
   1.156 @@ -1057,6 +1056,27 @@
   1.157  by transfer (simp add: map_of_map_keys)
   1.158  
   1.159  
   1.160 +subsection \<open>Additional properties\<close>
   1.161 +
   1.162 +lemma fmchoice':
   1.163 +  assumes "finite S" "\<forall>x \<in> S. \<exists>y. Q x y"
   1.164 +  shows "\<exists>m. fmdom' m = S \<and> fmpred Q m"
   1.165 +proof -
   1.166 +  obtain f where f: "Q x (f x)" if "x \<in> S" for x
   1.167 +    using assms by (metis bchoice)
   1.168 +  define f' where "f' x = (if x \<in> S then Some (f x) else None)" for x
   1.169 +
   1.170 +  have "eq_onp (\<lambda>m. finite (dom m)) f' f'"
   1.171 +    unfolding eq_onp_def f'_def dom_def using assms by auto
   1.172 +
   1.173 +  show ?thesis
   1.174 +    apply (rule exI[where x = "Abs_fmap f'"])
   1.175 +    apply (subst fmpred.abs_eq, fact)
   1.176 +    apply (subst fmdom'.abs_eq, fact)
   1.177 +    unfolding f'_def dom_def map_pred_def using f
   1.178 +    by auto
   1.179 +qed
   1.180 +
   1.181  subsection \<open>Lifting/transfer setup\<close>
   1.182  
   1.183  context includes lifting_syntax begin
   1.184 @@ -1066,14 +1086,40 @@
   1.185  
   1.186  lemma fmadd_transfer[transfer_rule]:
   1.187    "(fmrel P ===> fmrel P ===> fmrel P) fmadd fmadd"
   1.188 -  by (intro fmrel_addI rel_funI)
   1.189 +by (intro fmrel_addI rel_funI)
   1.190  
   1.191  lemma fmupd_transfer[transfer_rule]:
   1.192    "((=) ===> P ===> fmrel P ===> fmrel P) fmupd fmupd"
   1.193 -  by auto
   1.194 +by auto
   1.195  
   1.196  end
   1.197  
   1.198 +lemma Quotient_fmap_bnf[quot_map]:
   1.199 +  assumes "Quotient R Abs Rep T"
   1.200 +  shows "Quotient (fmrel R) (fmmap Abs) (fmmap Rep) (fmrel T)"
   1.201 +unfolding Quotient_alt_def4 proof safe
   1.202 +  fix m n
   1.203 +  assume "fmrel T m n"
   1.204 +  then have "fmlookup (fmmap Abs m) x = fmlookup n x" for x
   1.205 +    apply (cases rule: fmrel_cases[where x = x])
   1.206 +    using assms unfolding Quotient_alt_def by auto
   1.207 +  then show "fmmap Abs m = n"
   1.208 +    by (rule fmap_ext)
   1.209 +next
   1.210 +  fix m
   1.211 +  show "fmrel T (fmmap Rep m) m"
   1.212 +    unfolding fmap.rel_map
   1.213 +    apply (rule fmap.rel_refl)
   1.214 +    using assms unfolding Quotient_alt_def
   1.215 +    by auto
   1.216 +next
   1.217 +  from assms have "R = T OO T\<inverse>\<inverse>"
   1.218 +    unfolding Quotient_alt_def4 by simp
   1.219 +
   1.220 +  then show "fmrel R = fmrel T OO (fmrel T)\<inverse>\<inverse>"
   1.221 +    by (simp add: fmap.rel_compp fmap.rel_conversep)
   1.222 +qed
   1.223 +
   1.224  
   1.225  subsection \<open>View as datatype\<close>
   1.226  
   1.227 @@ -1311,4 +1357,31 @@
   1.228  lifting_update fmap.lifting
   1.229  lifting_forget fmap.lifting
   1.230  
   1.231 +
   1.232 +subsection \<open>Tests\<close>
   1.233 +
   1.234 +\<comment> \<open>Code generation\<close>
   1.235 +
   1.236 +export_code
   1.237 +  fBall fmrel fmran fmran' fmdom fmdom' fmpred pred_fmap fmsubset fmupd fmrel_on_fset
   1.238 +  fmdrop fmdrop_set fmdrop_fset fmrestrict_set fmrestrict_fset fmimage fmlookup fmempty
   1.239 +  fmfilter fmadd fmmap fmmap_keys fmcomp
   1.240 +  checking SML Scala Haskell? OCaml?
   1.241 +
   1.242 +\<comment> \<open>\<open>lifting\<close> through @{type fmap}\<close>
   1.243 +
   1.244 +experiment begin
   1.245 +
   1.246 +context includes fset.lifting begin
   1.247 +
   1.248 +lift_definition test1 :: "('a, 'b fset) fmap" is "fmempty :: ('a, 'b set) fmap"
   1.249 +  by auto
   1.250 +
   1.251 +lift_definition test2 :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b fset) fmap" is "\<lambda>a b. fmupd a {b} fmempty"
   1.252 +  by auto
   1.253 +
   1.254 +end
   1.255 +
   1.256 +end
   1.257 +
   1.258  end
   1.259 \ No newline at end of file