src/HOL/Library/Finite_Map.thy
author haftmann
Sun Nov 18 18:07:51 2018 +0000 (8 months ago)
changeset 69313 b021008c5397
parent 69142 c5e3212455ed
child 69593 3dda49e08b9d
permissions -rw-r--r--
removed legacy input syntax
     1 (*  Title:      HOL/Library/Finite_Map.thy
     2     Author:     Lars Hupel, TU M√ľnchen
     3 *)
     4 
     5 section \<open>Type of finite maps defined as a subtype of maps\<close>
     6 
     7 theory Finite_Map
     8   imports FSet AList Conditional_Parametricity
     9   abbrevs "(=" = "\<subseteq>\<^sub>f"
    10 begin
    11 
    12 subsection \<open>Auxiliary constants and lemmas over @{type map}\<close>
    13 
    14 parametric_constant map_add_transfer[transfer_rule]: map_add_def
    15 parametric_constant map_of_transfer[transfer_rule]: map_of_def
    16 
    17 context includes lifting_syntax begin
    18 
    19 abbreviation rel_map :: "('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c) \<Rightarrow> bool" where
    20 "rel_map f \<equiv> (=) ===> rel_option f"
    21 
    22 lemma ran_transfer[transfer_rule]: "(rel_map A ===> rel_set A) ran ran"
    23 proof
    24   fix m n
    25   assume "rel_map A m n"
    26   show "rel_set A (ran m) (ran n)"
    27     proof (rule rel_setI)
    28       fix x
    29       assume "x \<in> ran m"
    30       then obtain a where "m a = Some x"
    31         unfolding ran_def by auto
    32 
    33       have "rel_option A (m a) (n a)"
    34         using \<open>rel_map A m n\<close>
    35         by (auto dest: rel_funD)
    36       then obtain y where "n a = Some y" "A x y"
    37         unfolding \<open>m a = _\<close>
    38         by cases auto
    39       then show "\<exists>y \<in> ran n. A x y"
    40         unfolding ran_def by blast
    41     next
    42       fix y
    43       assume "y \<in> ran n"
    44       then obtain a where "n a = Some y"
    45         unfolding ran_def by auto
    46 
    47       have "rel_option A (m a) (n a)"
    48         using \<open>rel_map A m n\<close>
    49         by (auto dest: rel_funD)
    50       then obtain x where "m a = Some x" "A x y"
    51         unfolding \<open>n a = _\<close>
    52         by cases auto
    53       then show "\<exists>x \<in> ran m. A x y"
    54         unfolding ran_def by blast
    55     qed
    56 qed
    57 
    58 lemma ran_alt_def: "ran m = (the \<circ> m) ` dom m"
    59 unfolding ran_def dom_def by force
    60 
    61 parametric_constant dom_transfer[transfer_rule]: dom_def
    62 
    63 definition map_upd :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
    64 "map_upd k v m = m(k \<mapsto> v)"
    65 
    66 parametric_constant map_upd_transfer[transfer_rule]: map_upd_def
    67 
    68 definition map_filter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
    69 "map_filter P m = (\<lambda>x. if P x then m x else None)"
    70 
    71 parametric_constant map_filter_transfer[transfer_rule]: map_filter_def
    72 
    73 lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
    74 proof
    75   fix x
    76   show "map_filter P (map_of m) x = map_of [(k, _) \<leftarrow> m. P k] x"
    77     by (induct m) (auto simp: map_filter_def)
    78 qed
    79 
    80 lemma map_filter_finite[intro]:
    81   assumes "finite (dom m)"
    82   shows "finite (dom (map_filter P m))"
    83 proof -
    84   have "dom (map_filter P m) = Set.filter P (dom m)"
    85     unfolding map_filter_def Set.filter_def dom_def
    86     by auto
    87   then show ?thesis
    88     using assms
    89     by (simp add: Set.filter_def)
    90 qed
    91 
    92 definition map_drop :: "'a \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
    93 "map_drop a = map_filter (\<lambda>a'. a' \<noteq> a)"
    94 
    95 parametric_constant map_drop_transfer[transfer_rule]: map_drop_def
    96 
    97 definition map_drop_set :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
    98 "map_drop_set A = map_filter (\<lambda>a. a \<notin> A)"
    99 
   100 parametric_constant map_drop_set_transfer[transfer_rule]: map_drop_set_def
   101 
   102 definition map_restrict_set :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
   103 "map_restrict_set A = map_filter (\<lambda>a. a \<in> A)"
   104 
   105 parametric_constant map_restrict_set_transfer[transfer_rule]: map_restrict_set_def
   106 
   107 definition map_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" where
   108 "map_pred P m \<longleftrightarrow> (\<forall>x. case m x of None \<Rightarrow> True | Some y \<Rightarrow> P x y)"
   109 
   110 parametric_constant map_pred_transfer[transfer_rule]: map_pred_def
   111 
   112 definition rel_map_on_set :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c) \<Rightarrow> bool" where
   113 "rel_map_on_set S P = eq_onp (\<lambda>x. x \<in> S) ===> rel_option P"
   114 
   115 definition set_of_map :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<times> 'b) set" where
   116 "set_of_map m = {(k, v)|k v. m k = Some v}"
   117 
   118 lemma set_of_map_alt_def: "set_of_map m = (\<lambda>k. (k, the (m k))) ` dom m"
   119 unfolding set_of_map_def dom_def
   120 by auto
   121 
   122 lemma set_of_map_finite: "finite (dom m) \<Longrightarrow> finite (set_of_map m)"
   123 unfolding set_of_map_alt_def
   124 by auto
   125 
   126 lemma set_of_map_inj: "inj set_of_map"
   127 proof
   128   fix x y
   129   assume "set_of_map x = set_of_map y"
   130   hence "(x a = Some b) = (y a = Some b)" for a b
   131     unfolding set_of_map_def by auto
   132   hence "x k = y k" for k
   133     by (metis not_None_eq)
   134   thus "x = y" ..
   135 qed
   136 
   137 lemma dom_comp: "dom (m \<circ>\<^sub>m n) \<subseteq> dom n"
   138 unfolding map_comp_def dom_def
   139 by (auto split: option.splits)
   140 
   141 lemma dom_comp_finite: "finite (dom n) \<Longrightarrow> finite (dom (map_comp m n))"
   142 by (metis finite_subset dom_comp)
   143 
   144 parametric_constant map_comp_transfer[transfer_rule]: map_comp_def
   145 
   146 end
   147 
   148 
   149 subsection \<open>Abstract characterisation\<close>
   150 
   151 typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a \<rightharpoonup> 'b) set"
   152   morphisms fmlookup Abs_fmap
   153 proof
   154   show "Map.empty \<in> {m. finite (dom m)}"
   155     by auto
   156 qed
   157 
   158 setup_lifting type_definition_fmap
   159 
   160 lemma dom_fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))"
   161 using fmap.fmlookup by auto
   162 
   163 lemma fmap_ext:
   164   assumes "\<And>x. fmlookup m x = fmlookup n x"
   165   shows "m = n"
   166 using assms
   167 by transfer' auto
   168 
   169 
   170 subsection \<open>Operations\<close>
   171 
   172 context
   173   includes fset.lifting
   174 begin
   175 
   176 lift_definition fmran :: "('a, 'b) fmap \<Rightarrow> 'b fset"
   177   is ran
   178   parametric ran_transfer
   179 by (rule finite_ran)
   180 
   181 lemma fmlookup_ran_iff: "y |\<in>| fmran m \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y)"
   182 by transfer' (auto simp: ran_def)
   183 
   184 lemma fmranI: "fmlookup m x = Some y \<Longrightarrow> y |\<in>| fmran m" by (auto simp: fmlookup_ran_iff)
   185 
   186 lemma fmranE[elim]:
   187   assumes "y |\<in>| fmran m"
   188   obtains x where "fmlookup m x = Some y"
   189 using assms by (auto simp: fmlookup_ran_iff)
   190 
   191 lift_definition fmdom :: "('a, 'b) fmap \<Rightarrow> 'a fset"
   192   is dom
   193   parametric dom_transfer
   194 .
   195 
   196 lemma fmlookup_dom_iff: "x |\<in>| fmdom m \<longleftrightarrow> (\<exists>a. fmlookup m x = Some a)"
   197 by transfer' auto
   198 
   199 lemma fmdom_notI: "fmlookup m x = None \<Longrightarrow> x |\<notin>| fmdom m" by (simp add: fmlookup_dom_iff)
   200 lemma fmdomI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| fmdom m" by (simp add: fmlookup_dom_iff)
   201 lemma fmdom_notD[dest]: "x |\<notin>| fmdom m \<Longrightarrow> fmlookup m x = None" by (simp add: fmlookup_dom_iff)
   202 
   203 lemma fmdomE[elim]:
   204   assumes "x |\<in>| fmdom m"
   205   obtains y where "fmlookup m x = Some y"
   206 using assms by (auto simp: fmlookup_dom_iff)
   207 
   208 lift_definition fmdom' :: "('a, 'b) fmap \<Rightarrow> 'a set"
   209   is dom
   210   parametric dom_transfer
   211 .
   212 
   213 lemma fmlookup_dom'_iff: "x \<in> fmdom' m \<longleftrightarrow> (\<exists>a. fmlookup m x = Some a)"
   214 by transfer' auto
   215 
   216 lemma fmdom'_notI: "fmlookup m x = None \<Longrightarrow> x \<notin> fmdom' m" by (simp add: fmlookup_dom'_iff)
   217 lemma fmdom'I: "fmlookup m x = Some y \<Longrightarrow> x \<in> fmdom' m" by (simp add: fmlookup_dom'_iff)
   218 lemma fmdom'_notD[dest]: "x \<notin> fmdom' m \<Longrightarrow> fmlookup m x = None" by (simp add: fmlookup_dom'_iff)
   219 
   220 lemma fmdom'E[elim]:
   221   assumes "x \<in> fmdom' m"
   222   obtains x y where "fmlookup m x = Some y"
   223 using assms by (auto simp: fmlookup_dom'_iff)
   224 
   225 lemma fmdom'_alt_def: "fmdom' m = fset (fmdom m)"
   226 by transfer' force
   227 
   228 lemma finite_fmdom'[simp]: "finite (fmdom' m)"
   229 unfolding fmdom'_alt_def by simp
   230 
   231 lemma dom_fmlookup[simp]: "dom (fmlookup m) = fmdom' m"
   232 by transfer' simp
   233 
   234 lift_definition fmempty :: "('a, 'b) fmap"
   235   is Map.empty
   236 by simp
   237 
   238 lemma fmempty_lookup[simp]: "fmlookup fmempty x = None"
   239 by transfer' simp
   240 
   241 lemma fmdom_empty[simp]: "fmdom fmempty = {||}" by transfer' simp
   242 lemma fmdom'_empty[simp]: "fmdom' fmempty = {}" by transfer' simp
   243 lemma fmran_empty[simp]: "fmran fmempty = fempty" by transfer' (auto simp: ran_def map_filter_def)
   244 
   245 lift_definition fmupd :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   246   is map_upd
   247   parametric map_upd_transfer
   248 unfolding map_upd_def[abs_def]
   249 by simp
   250 
   251 lemma fmupd_lookup[simp]: "fmlookup (fmupd a b m) a' = (if a = a' then Some b else fmlookup m a')"
   252 by transfer' (auto simp: map_upd_def)
   253 
   254 lemma fmdom_fmupd[simp]: "fmdom (fmupd a b m) = finsert a (fmdom m)" by transfer (simp add: map_upd_def)
   255 lemma fmdom'_fmupd[simp]: "fmdom' (fmupd a b m) = insert a (fmdom' m)" by transfer (simp add: map_upd_def)
   256 
   257 lift_definition fmfilter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   258   is map_filter
   259   parametric map_filter_transfer
   260 by auto
   261 
   262 lemma fmdom_filter[simp]: "fmdom (fmfilter P m) = ffilter P (fmdom m)"
   263 by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
   264 
   265 lemma fmdom'_filter[simp]: "fmdom' (fmfilter P m) = Set.filter P (fmdom' m)"
   266 by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
   267 
   268 lemma fmlookup_filter[simp]: "fmlookup (fmfilter P m) x = (if P x then fmlookup m x else None)"
   269 by transfer' (auto simp: map_filter_def)
   270 
   271 lemma fmfilter_empty[simp]: "fmfilter P fmempty = fmempty"
   272 by transfer' (auto simp: map_filter_def)
   273 
   274 lemma fmfilter_true[simp]:
   275   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x"
   276   shows "fmfilter P m = m"
   277 proof (rule fmap_ext)
   278   fix x
   279   have "fmlookup m x = None" if "\<not> P x"
   280     using that assms by fastforce
   281   then show "fmlookup (fmfilter P m) x = fmlookup m x"
   282     by simp
   283 qed
   284 
   285 lemma fmfilter_false[simp]:
   286   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> \<not> P x"
   287   shows "fmfilter P m = fmempty"
   288 using assms by transfer' (fastforce simp: map_filter_def)
   289 
   290 lemma fmfilter_comp[simp]: "fmfilter P (fmfilter Q m) = fmfilter (\<lambda>x. P x \<and> Q x) m"
   291 by transfer' (auto simp: map_filter_def)
   292 
   293 lemma fmfilter_comm: "fmfilter P (fmfilter Q m) = fmfilter Q (fmfilter P m)"
   294 unfolding fmfilter_comp by meson
   295 
   296 lemma fmfilter_cong[cong]:
   297   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x = Q x"
   298   shows "fmfilter P m = fmfilter Q m"
   299 proof (rule fmap_ext)
   300   fix x
   301   have "fmlookup m x = None" if "P x \<noteq> Q x"
   302     using that assms by fastforce
   303   then show "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x"
   304     by auto
   305 qed
   306 
   307 lemma fmfilter_cong'[fundef_cong]:
   308   assumes "m = n" "\<And>x. x \<in> fmdom' m \<Longrightarrow> P x = Q x"
   309   shows "fmfilter P m = fmfilter Q n"
   310 using assms(2) unfolding assms(1)
   311 by (rule fmfilter_cong) (metis fmdom'I)
   312 
   313 lemma fmfilter_upd[simp]:
   314   "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)"
   315 by transfer' (auto simp: map_upd_def map_filter_def)
   316 
   317 lift_definition fmdrop :: "'a \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   318   is map_drop
   319   parametric map_drop_transfer
   320 unfolding map_drop_def by auto
   321 
   322 lemma fmdrop_lookup[simp]: "fmlookup (fmdrop a m) a = None"
   323 by transfer' (auto simp: map_drop_def map_filter_def)
   324 
   325 lift_definition fmdrop_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   326   is map_drop_set
   327   parametric map_drop_set_transfer
   328 unfolding map_drop_set_def by auto
   329 
   330 lift_definition fmdrop_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   331   is map_drop_set
   332   parametric map_drop_set_transfer
   333 unfolding map_drop_set_def by auto
   334 
   335 lift_definition fmrestrict_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   336   is map_restrict_set
   337   parametric map_restrict_set_transfer
   338 unfolding map_restrict_set_def by auto
   339 
   340 lift_definition fmrestrict_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   341   is map_restrict_set
   342   parametric map_restrict_set_transfer
   343 unfolding map_restrict_set_def by auto
   344 
   345 lemma fmfilter_alt_defs:
   346   "fmdrop a = fmfilter (\<lambda>a'. a' \<noteq> a)"
   347   "fmdrop_set A = fmfilter (\<lambda>a. a \<notin> A)"
   348   "fmdrop_fset B = fmfilter (\<lambda>a. a |\<notin>| B)"
   349   "fmrestrict_set A = fmfilter (\<lambda>a. a \<in> A)"
   350   "fmrestrict_fset B = fmfilter (\<lambda>a. a |\<in>| B)"
   351 by (transfer'; simp add: map_drop_def map_drop_set_def map_restrict_set_def)+
   352 
   353 lemma fmdom_drop[simp]: "fmdom (fmdrop a m) = fmdom m - {|a|}" unfolding fmfilter_alt_defs by auto
   354 lemma fmdom'_drop[simp]: "fmdom' (fmdrop a m) = fmdom' m - {a}" unfolding fmfilter_alt_defs by auto
   355 lemma fmdom'_drop_set[simp]: "fmdom' (fmdrop_set A m) = fmdom' m - A" unfolding fmfilter_alt_defs by auto
   356 lemma fmdom_drop_fset[simp]: "fmdom (fmdrop_fset A m) = fmdom m - A" unfolding fmfilter_alt_defs by auto
   357 lemma fmdom'_restrict_set: "fmdom' (fmrestrict_set A m) \<subseteq> A" unfolding fmfilter_alt_defs by auto
   358 lemma fmdom_restrict_fset: "fmdom (fmrestrict_fset A m) |\<subseteq>| A" unfolding fmfilter_alt_defs by auto
   359 
   360 lemma fmdom'_restrict_set_precise: "fmdom' (fmrestrict_set A m) = fmdom' m \<inter> A"
   361 unfolding fmfilter_alt_defs by auto
   362 
   363 lemma fmdom'_restrict_fset_precise: "fmdom (fmrestrict_fset A m) = fmdom m |\<inter>| A"
   364 unfolding fmfilter_alt_defs by auto
   365 
   366 lemma fmdom'_drop_fset[simp]: "fmdom' (fmdrop_fset A m) = fmdom' m - fset A"
   367 unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def split: if_splits)
   368 
   369 lemma fmdom'_restrict_fset: "fmdom' (fmrestrict_fset A m) \<subseteq> fset A"
   370 unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def)
   371 
   372 lemma fmlookup_drop[simp]:
   373   "fmlookup (fmdrop a m) x = (if x \<noteq> a then fmlookup m x else None)"
   374 unfolding fmfilter_alt_defs by simp
   375 
   376 lemma fmlookup_drop_set[simp]:
   377   "fmlookup (fmdrop_set A m) x = (if x \<notin> A then fmlookup m x else None)"
   378 unfolding fmfilter_alt_defs by simp
   379 
   380 lemma fmlookup_drop_fset[simp]:
   381   "fmlookup (fmdrop_fset A m) x = (if x |\<notin>| A then fmlookup m x else None)"
   382 unfolding fmfilter_alt_defs by simp
   383 
   384 lemma fmlookup_restrict_set[simp]:
   385   "fmlookup (fmrestrict_set A m) x = (if x \<in> A then fmlookup m x else None)"
   386 unfolding fmfilter_alt_defs by simp
   387 
   388 lemma fmlookup_restrict_fset[simp]:
   389   "fmlookup (fmrestrict_fset A m) x = (if x |\<in>| A then fmlookup m x else None)"
   390 unfolding fmfilter_alt_defs by simp
   391 
   392 lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m"
   393 by (rule fmap_ext) auto
   394 
   395 lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m"
   396 by (rule fmap_ext) auto
   397 
   398 lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty"
   399 unfolding fmfilter_alt_defs by simp
   400 
   401 lemma fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty"
   402 unfolding fmfilter_alt_defs by simp
   403 
   404 lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty"
   405 unfolding fmfilter_alt_defs by simp
   406 
   407 lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty"
   408 unfolding fmfilter_alt_defs by simp
   409 
   410 lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty"
   411 unfolding fmfilter_alt_defs by simp
   412 
   413 lemma fmdrop_set_null[simp]: "fmdrop_set {} m = m"
   414 by (rule fmap_ext) auto
   415 
   416 lemma fmdrop_fset_null[simp]: "fmdrop_fset {||} m = m"
   417 by (rule fmap_ext) auto
   418 
   419 lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m"
   420 unfolding fmfilter_alt_defs by simp
   421 
   422 lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m"
   423 unfolding fmfilter_alt_defs by simp
   424 
   425 lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty"
   426 unfolding fmfilter_alt_defs by simp
   427 
   428 lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty"
   429 unfolding fmfilter_alt_defs by simp
   430 
   431 lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)"
   432 unfolding fmfilter_alt_defs by (rule fmfilter_comm)
   433 
   434 lemma fmdrop_set_insert[simp]: "fmdrop_set (insert x S) m = fmdrop x (fmdrop_set S m)"
   435 by (rule fmap_ext) auto
   436 
   437 lemma fmdrop_fset_insert[simp]: "fmdrop_fset (finsert x S) m = fmdrop x (fmdrop_fset S m)"
   438 by (rule fmap_ext) auto
   439 
   440 lemma fmrestrict_set_twice[simp]: "fmrestrict_set S (fmrestrict_set T m) = fmrestrict_set (S \<inter> T) m"
   441 unfolding fmfilter_alt_defs by auto
   442 
   443 lemma fmrestrict_fset_twice[simp]: "fmrestrict_fset S (fmrestrict_fset T m) = fmrestrict_fset (S |\<inter>| T) m"
   444 unfolding fmfilter_alt_defs by auto
   445 
   446 lemma fmrestrict_set_drop[simp]: "fmrestrict_set S (fmdrop b m) = fmrestrict_set (S - {b}) m"
   447 unfolding fmfilter_alt_defs by auto
   448 
   449 lemma fmrestrict_fset_drop[simp]: "fmrestrict_fset S (fmdrop b m) = fmrestrict_fset (S - {| b |}) m"
   450 unfolding fmfilter_alt_defs by auto
   451 
   452 lemma fmdrop_fmrestrict_set[simp]: "fmdrop b (fmrestrict_set S m) = fmrestrict_set (S - {b}) m"
   453 by (rule fmap_ext) auto
   454 
   455 lemma fmdrop_fmrestrict_fset[simp]: "fmdrop b (fmrestrict_fset S m) = fmrestrict_fset (S - {| b |}) m"
   456 by (rule fmap_ext) auto
   457 
   458 lemma fmdrop_idem[simp]: "fmdrop a (fmdrop a m) = fmdrop a m"
   459 unfolding fmfilter_alt_defs by auto
   460 
   461 lemma fmdrop_set_twice[simp]: "fmdrop_set S (fmdrop_set T m) = fmdrop_set (S \<union> T) m"
   462 unfolding fmfilter_alt_defs by auto
   463 
   464 lemma fmdrop_fset_twice[simp]: "fmdrop_fset S (fmdrop_fset T m) = fmdrop_fset (S |\<union>| T) m"
   465 unfolding fmfilter_alt_defs by auto
   466 
   467 lemma fmdrop_set_fmdrop[simp]: "fmdrop_set S (fmdrop b m) = fmdrop_set (insert b S) m"
   468 by (rule fmap_ext) auto
   469 
   470 lemma fmdrop_fset_fmdrop[simp]: "fmdrop_fset S (fmdrop b m) = fmdrop_fset (finsert b S) m"
   471 by (rule fmap_ext) auto
   472 
   473 lift_definition fmadd :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap" (infixl "++\<^sub>f" 100)
   474   is map_add
   475   parametric map_add_transfer
   476 by simp
   477 
   478 lemma fmlookup_add[simp]:
   479   "fmlookup (m ++\<^sub>f n) x = (if x |\<in>| fmdom n then fmlookup n x else fmlookup m x)"
   480   by transfer' (auto simp: map_add_def split: option.splits)
   481 
   482 lemma fmdom_add[simp]: "fmdom (m ++\<^sub>f n) = fmdom m |\<union>| fmdom n" by transfer' auto
   483 lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \<union> fmdom' n" by transfer' auto
   484 
   485 lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
   486 by (rule fmap_ext) auto
   487 
   488 lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
   489 by (rule fmap_ext) auto
   490 
   491 lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n"
   492 by transfer' (auto simp: map_filter_def map_add_def)
   493 
   494 lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n"
   495 unfolding fmfilter_alt_defs by simp
   496 
   497 lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n"
   498 unfolding fmfilter_alt_defs by simp
   499 
   500 lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n"
   501 unfolding fmfilter_alt_defs by simp
   502 
   503 lemma fmrestrict_set_add_distrib[simp]:
   504   "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n"
   505 unfolding fmfilter_alt_defs by simp
   506 
   507 lemma fmrestrict_fset_add_distrib[simp]:
   508   "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n"
   509 unfolding fmfilter_alt_defs by simp
   510 
   511 lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m"
   512 by (transfer'; auto)+
   513 
   514 lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m"
   515 by transfer' (auto simp: map_add_def split: option.splits)
   516 
   517 lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p"
   518 by transfer' simp
   519 
   520 lemma fmadd_fmupd[simp]: "m ++\<^sub>f fmupd a b n = fmupd a b (m ++\<^sub>f n)"
   521 by (rule fmap_ext) simp
   522 
   523 lift_definition fmpred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool"
   524   is map_pred
   525   parametric map_pred_transfer
   526 .
   527 
   528 lemma fmpredI[intro]:
   529   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y"
   530   shows "fmpred P m"
   531 using assms
   532 by transfer' (auto simp: map_pred_def split: option.splits)
   533 
   534 lemma fmpredD[dest]: "fmpred P m \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P x y"
   535 by transfer' (auto simp: map_pred_def split: option.split_asm)
   536 
   537 lemma fmpred_iff: "fmpred P m \<longleftrightarrow> (\<forall>x y. fmlookup m x = Some y \<longrightarrow> P x y)"
   538 by auto
   539 
   540 lemma fmpred_alt_def: "fmpred P m \<longleftrightarrow> fBall (fmdom m) (\<lambda>x. P x (the (fmlookup m x)))"
   541 unfolding fmpred_iff
   542 apply auto
   543 apply (rename_tac x y)
   544 apply (erule_tac x = x in fBallE)
   545 apply simp
   546 by (simp add: fmlookup_dom_iff)
   547 
   548 lemma fmpred_mono_strong:
   549   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   550   shows "fmpred P m \<Longrightarrow> fmpred Q m"
   551 using assms unfolding fmpred_iff by auto
   552 
   553 lemma fmpred_mono[mono]: "P \<le> Q \<Longrightarrow> fmpred P \<le> fmpred Q"
   554 apply rule
   555 apply (rule fmpred_mono_strong[where P = P and Q = Q])
   556 apply auto
   557 done
   558 
   559 lemma fmpred_empty[intro!, simp]: "fmpred P fmempty"
   560 by auto
   561 
   562 lemma fmpred_upd[intro]: "fmpred P m \<Longrightarrow> P x y \<Longrightarrow> fmpred P (fmupd x y m)"
   563 by transfer' (auto simp: map_pred_def map_upd_def)
   564 
   565 lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \<Longrightarrow> P x y"
   566 by auto
   567 
   568 lemma fmpred_add[intro]: "fmpred P m \<Longrightarrow> fmpred P n \<Longrightarrow> fmpred P (m ++\<^sub>f n)"
   569 by transfer' (auto simp: map_pred_def map_add_def split: option.splits)
   570 
   571 lemma fmpred_filter[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmfilter Q m)"
   572 by transfer' (auto simp: map_pred_def map_filter_def)
   573 
   574 lemma fmpred_drop[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop a m)"
   575 by (auto simp: fmfilter_alt_defs)
   576 
   577 lemma fmpred_drop_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_set A m)"
   578 by (auto simp: fmfilter_alt_defs)
   579 
   580 lemma fmpred_drop_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_fset A m)"
   581 by (auto simp: fmfilter_alt_defs)
   582 
   583 lemma fmpred_restrict_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_set A m)"
   584 by (auto simp: fmfilter_alt_defs)
   585 
   586 lemma fmpred_restrict_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_fset A m)"
   587 by (auto simp: fmfilter_alt_defs)
   588 
   589 lemma fmpred_cases[consumes 1]:
   590   assumes "fmpred P m"
   591   obtains (none) "fmlookup m x = None" | (some) y where "fmlookup m x = Some y" "P x y"
   592 using assms by auto
   593 
   594 lift_definition fmsubset :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool" (infix "\<subseteq>\<^sub>f" 50)
   595   is map_le
   596 .
   597 
   598 lemma fmsubset_alt_def: "m \<subseteq>\<^sub>f n \<longleftrightarrow> fmpred (\<lambda>k v. fmlookup n k = Some v) m"
   599 by transfer' (auto simp: map_pred_def map_le_def dom_def split: option.splits)
   600 
   601 lemma fmsubset_pred: "fmpred P m \<Longrightarrow> n \<subseteq>\<^sub>f m \<Longrightarrow> fmpred P n"
   602 unfolding fmsubset_alt_def fmpred_iff
   603 by auto
   604 
   605 lemma fmsubset_filter_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmfilter P m \<subseteq>\<^sub>f fmfilter P n"
   606 unfolding fmsubset_alt_def fmpred_iff
   607 by auto
   608 
   609 lemma fmsubset_drop_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop a m \<subseteq>\<^sub>f fmdrop a n"
   610 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
   611 
   612 lemma fmsubset_drop_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_set A m \<subseteq>\<^sub>f fmdrop_set A n"
   613 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
   614 
   615 lemma fmsubset_drop_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_fset A m \<subseteq>\<^sub>f fmdrop_fset A n"
   616 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
   617 
   618 lemma fmsubset_restrict_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_set A m \<subseteq>\<^sub>f fmrestrict_set A n"
   619 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
   620 
   621 lemma fmsubset_restrict_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_fset A m \<subseteq>\<^sub>f fmrestrict_fset A n"
   622 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
   623 
   624 lemma fmfilter_subset[simp]: "fmfilter P m \<subseteq>\<^sub>f m"
   625 unfolding fmsubset_alt_def fmpred_iff by auto
   626 
   627 lemma fmsubset_drop[simp]: "fmdrop a m \<subseteq>\<^sub>f m"
   628 unfolding fmfilter_alt_defs by (rule fmfilter_subset)
   629 
   630 lemma fmsubset_drop_set[simp]: "fmdrop_set S m \<subseteq>\<^sub>f m"
   631 unfolding fmfilter_alt_defs by (rule fmfilter_subset)
   632 
   633 lemma fmsubset_drop_fset[simp]: "fmdrop_fset S m \<subseteq>\<^sub>f m"
   634 unfolding fmfilter_alt_defs by (rule fmfilter_subset)
   635 
   636 lemma fmsubset_restrict_set[simp]: "fmrestrict_set S m \<subseteq>\<^sub>f m"
   637 unfolding fmfilter_alt_defs by (rule fmfilter_subset)
   638 
   639 lemma fmsubset_restrict_fset[simp]: "fmrestrict_fset S m \<subseteq>\<^sub>f m"
   640 unfolding fmfilter_alt_defs by (rule fmfilter_subset)
   641 
   642 lift_definition fset_of_fmap :: "('a, 'b) fmap \<Rightarrow> ('a \<times> 'b) fset" is set_of_map
   643 by (rule set_of_map_finite)
   644 
   645 lemma fset_of_fmap_inj[intro, simp]: "inj fset_of_fmap"
   646 apply rule
   647 apply transfer'
   648 using set_of_map_inj unfolding inj_def by auto
   649 
   650 lemma fset_of_fmap_iff[simp]: "(a, b) |\<in>| fset_of_fmap m \<longleftrightarrow> fmlookup m a = Some b"
   651 by transfer' (auto simp: set_of_map_def)
   652 
   653 lemma fset_of_fmap_iff'[simp]: "(a, b) \<in> fset (fset_of_fmap m) \<longleftrightarrow> fmlookup m a = Some b"
   654 by transfer' (auto simp: set_of_map_def)
   655 
   656 lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
   657   is map_of
   658   parametric map_of_transfer
   659 by (rule finite_dom_map_of)
   660 
   661 lemma fmap_of_list_simps[simp]:
   662   "fmap_of_list [] = fmempty"
   663   "fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)"
   664 by (transfer, simp add: map_upd_def)+
   665 
   666 lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs"
   667 by transfer' simp
   668 
   669 lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]"
   670 by transfer' (auto simp: map_upd_def)
   671 
   672 lemma fmpred_of_list[intro]:
   673   assumes "\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v"
   674   shows "fmpred P (fmap_of_list xs)"
   675 using assms
   676 by (induction xs) (transfer'; auto simp: map_pred_def)+
   677 
   678 lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \<Longrightarrow> (k, v) \<in> set xs"
   679 by transfer' (auto dest: map_of_SomeD)
   680 
   681 lemma fmdom_fmap_of_list[simp]: "fmdom (fmap_of_list xs) = fset_of_list (map fst xs)"
   682 apply transfer'
   683 apply (subst dom_map_of_conv_image_fst)
   684 apply auto
   685 done
   686 
   687 lift_definition fmrel_on_fset :: "'a fset \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
   688   is rel_map_on_set
   689 .
   690 
   691 lemma fmrel_on_fset_alt_def: "fmrel_on_fset S P m n \<longleftrightarrow> fBall S (\<lambda>x. rel_option P (fmlookup m x) (fmlookup n x))"
   692 by transfer' (auto simp: rel_map_on_set_def eq_onp_def rel_fun_def)
   693 
   694 lemma fmrel_on_fsetI[intro]:
   695   assumes "\<And>x. x |\<in>| S \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
   696   shows "fmrel_on_fset S P m n"
   697 using assms
   698 unfolding fmrel_on_fset_alt_def by auto
   699 
   700 lemma fmrel_on_fset_mono[mono]: "R \<le> Q \<Longrightarrow> fmrel_on_fset S R \<le> fmrel_on_fset S Q"
   701 unfolding fmrel_on_fset_alt_def[abs_def]
   702 apply (intro le_funI fBall_mono)
   703 using option.rel_mono by auto
   704 
   705 lemma fmrel_on_fsetD: "x |\<in>| S \<Longrightarrow> fmrel_on_fset S P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
   706 unfolding fmrel_on_fset_alt_def
   707 by auto
   708 
   709 lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \<Longrightarrow> T |\<subseteq>| S \<Longrightarrow> fmrel_on_fset T R m n"
   710 unfolding fmrel_on_fset_alt_def
   711 by auto
   712 
   713 lemma fmrel_on_fset_unionI:
   714   "fmrel_on_fset A R m n \<Longrightarrow> fmrel_on_fset B R m n \<Longrightarrow> fmrel_on_fset (A |\<union>| B) R m n"
   715 unfolding fmrel_on_fset_alt_def
   716 by auto
   717 
   718 lemma fmrel_on_fset_updateI:
   719   assumes "fmrel_on_fset S P m n" "P v\<^sub>1 v\<^sub>2"
   720   shows "fmrel_on_fset (finsert k S) P (fmupd k v\<^sub>1 m) (fmupd k v\<^sub>2 n)"
   721 using assms
   722 unfolding fmrel_on_fset_alt_def
   723 by auto
   724 
   725 lift_definition fmimage :: "('a, 'b) fmap \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is "\<lambda>m S. {b|a b. m a = Some b \<and> a \<in> S}"
   726 subgoal for m S
   727   apply (rule finite_subset[where B = "ran m"])
   728   apply (auto simp: ran_def)[]
   729   by (rule finite_ran)
   730 done
   731 
   732 lemma fmimage_alt_def: "fmimage m S = fmran (fmrestrict_fset S m)"
   733 by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
   734 
   735 lemma fmimage_empty[simp]: "fmimage m fempty = fempty"
   736 by transfer' auto
   737 
   738 lemma fmimage_subset_ran[simp]: "fmimage m S |\<subseteq>| fmran m"
   739 by transfer' (auto simp: ran_def)
   740 
   741 lemma fmimage_dom[simp]: "fmimage m (fmdom m) = fmran m"
   742 by transfer' (auto simp: ran_def)
   743 
   744 lemma fmimage_inter: "fmimage m (A |\<inter>| B) |\<subseteq>| fmimage m A |\<inter>| fmimage m B"
   745 by transfer' auto
   746 
   747 lemma fimage_inter_dom[simp]:
   748   "fmimage m (fmdom m |\<inter>| A) = fmimage m A"
   749   "fmimage m (A |\<inter>| fmdom m) = fmimage m A"
   750 by (transfer'; auto)+
   751 
   752 lemma fmimage_union[simp]: "fmimage m (A |\<union>| B) = fmimage m A |\<union>| fmimage m B"
   753 by transfer' auto
   754 
   755 lemma fmimage_Union[simp]: "fmimage m (ffUnion A) = ffUnion (fmimage m |`| A)"
   756 by transfer' auto
   757 
   758 lemma fmimage_filter[simp]: "fmimage (fmfilter P m) A = fmimage m (ffilter P A)"
   759 by transfer' (auto simp: map_filter_def)
   760 
   761 lemma fmimage_drop[simp]: "fmimage (fmdrop a m) A = fmimage m (A - {|a|})"
   762 by transfer' (auto simp: map_filter_def map_drop_def)
   763 
   764 lemma fmimage_drop_fset[simp]: "fmimage (fmdrop_fset B m) A = fmimage m (A - B)"
   765 by transfer' (auto simp: map_filter_def map_drop_set_def)
   766 
   767 lemma fmimage_restrict_fset[simp]: "fmimage (fmrestrict_fset B m) A = fmimage m (A |\<inter>| B)"
   768 by transfer' (auto simp: map_filter_def map_restrict_set_def)
   769 
   770 lemma fmfilter_ran[simp]: "fmran (fmfilter P m) = fmimage m (ffilter P (fmdom m))"
   771 by transfer' (auto simp: ran_def map_filter_def)
   772 
   773 lemma fmran_drop[simp]: "fmran (fmdrop a m) = fmimage m (fmdom m - {|a|})"
   774 by transfer' (auto simp: ran_def map_drop_def map_filter_def)
   775 
   776 lemma fmran_drop_fset[simp]: "fmran (fmdrop_fset A m) = fmimage m (fmdom m - A)"
   777 by transfer' (auto simp: ran_def map_drop_set_def map_filter_def)
   778 
   779 lemma fmran_restrict_fset: "fmran (fmrestrict_fset A m) = fmimage m (fmdom m |\<inter>| A)"
   780 by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
   781 
   782 lemma fmlookup_image_iff: "y |\<in>| fmimage m A \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y \<and> x |\<in>| A)"
   783 by transfer' (auto simp: ran_def)
   784 
   785 lemma fmimageI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| A \<Longrightarrow> y |\<in>| fmimage m A"
   786 by (auto simp: fmlookup_image_iff)
   787 
   788 lemma fmimageE[elim]:
   789   assumes "y |\<in>| fmimage m A"
   790   obtains x where "fmlookup m x = Some y" "x |\<in>| A"
   791 using assms by (auto simp: fmlookup_image_iff)
   792 
   793 lift_definition fmcomp :: "('b, 'c) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap" (infixl "\<circ>\<^sub>f" 55)
   794   is map_comp
   795   parametric map_comp_transfer
   796 by (rule dom_comp_finite)
   797 
   798 lemma fmlookup_comp[simp]: "fmlookup (m \<circ>\<^sub>f n) x = Option.bind (fmlookup n x) (fmlookup m)"
   799 by transfer' (auto simp: map_comp_def split: option.splits)
   800 
   801 end
   802 
   803 
   804 subsection \<open>BNF setup\<close>
   805 
   806 lift_bnf ('a, fmran': 'b) fmap [wits: Map.empty]
   807   for map: fmmap
   808       rel: fmrel
   809   by auto
   810 
   811 declare fmap.pred_mono[mono]
   812 
   813 context includes lifting_syntax begin
   814 
   815 lemma fmmap_transfer[transfer_rule]:
   816   "((=) ===> pcr_fmap (=) (=) ===> pcr_fmap (=) (=)) (\<lambda>f. (\<circ>) (map_option f)) fmmap"
   817   unfolding fmmap_def
   818   by (rule rel_funI ext)+ (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
   819 
   820 lemma fmran'_transfer[transfer_rule]:
   821   "(pcr_fmap (=) (=) ===> (=)) (\<lambda>x. \<Union>(set_option ` (range x))) fmran'"
   822   unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce
   823 
   824 lemma fmrel_transfer[transfer_rule]:
   825   "((=) ===> pcr_fmap (=) (=) ===> pcr_fmap (=) (=) ===> (=)) rel_map fmrel"
   826   unfolding fmrel_def fmap.pcr_cr_eq cr_fmap_def vimage2p_def by fastforce
   827 
   828 end
   829 
   830 
   831 lemma fmran'_alt_def: "fmran' m = fset (fmran m)"
   832 including fset.lifting
   833 by transfer' (auto simp: ran_def fun_eq_iff)
   834 
   835 lemma fmlookup_ran'_iff: "y \<in> fmran' m \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y)"
   836 by transfer' (auto simp: ran_def)
   837 
   838 lemma fmran'I: "fmlookup m x = Some y \<Longrightarrow> y \<in> fmran' m" by (auto simp: fmlookup_ran'_iff)
   839 
   840 lemma fmran'E[elim]:
   841   assumes "y \<in> fmran' m"
   842   obtains x where "fmlookup m x = Some y"
   843 using assms by (auto simp: fmlookup_ran'_iff)
   844 
   845 lemma fmrel_iff: "fmrel R m n \<longleftrightarrow> (\<forall>x. rel_option R (fmlookup m x) (fmlookup n x))"
   846 by transfer' (auto simp: rel_fun_def)
   847 
   848 lemma fmrelI[intro]:
   849   assumes "\<And>x. rel_option R (fmlookup m x) (fmlookup n x)"
   850   shows "fmrel R m n"
   851 using assms
   852 by transfer' auto
   853 
   854 lemma fmrel_upd[intro]: "fmrel P m n \<Longrightarrow> P x y \<Longrightarrow> fmrel P (fmupd k x m) (fmupd k y n)"
   855 by transfer' (auto simp: map_upd_def rel_fun_def)
   856 
   857 lemma fmrelD[dest]: "fmrel P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
   858 by transfer' (auto simp: rel_fun_def)
   859 
   860 lemma fmrel_addI[intro]:
   861   assumes "fmrel P m n" "fmrel P a b"
   862   shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)"
   863 using assms
   864 apply transfer'
   865 apply (auto simp: rel_fun_def map_add_def)
   866 by (metis option.case_eq_if option.collapse option.rel_sel)
   867 
   868 lemma fmrel_cases[consumes 1]:
   869   assumes "fmrel P m n"
   870   obtains (none) "fmlookup m x = None" "fmlookup n x = None"
   871         | (some) a b where "fmlookup m x = Some a" "fmlookup n x = Some b" "P a b"
   872 proof -
   873   from assms have "rel_option P (fmlookup m x) (fmlookup n x)"
   874     by auto
   875   then show thesis
   876     using none some
   877     by (cases rule: option.rel_cases) auto
   878 qed
   879 
   880 lemma fmrel_filter[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmfilter Q m) (fmfilter Q n)"
   881 unfolding fmrel_iff by auto
   882 
   883 lemma fmrel_drop[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop a m) (fmdrop a n)"
   884 unfolding fmfilter_alt_defs by blast
   885 
   886 lemma fmrel_drop_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_set A m) (fmdrop_set A n)"
   887 unfolding fmfilter_alt_defs by blast
   888 
   889 lemma fmrel_drop_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_fset A m) (fmdrop_fset A n)"
   890 unfolding fmfilter_alt_defs by blast
   891 
   892 lemma fmrel_restrict_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_set A m) (fmrestrict_set A n)"
   893 unfolding fmfilter_alt_defs by blast
   894 
   895 lemma fmrel_restrict_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)"
   896 unfolding fmfilter_alt_defs by blast
   897 
   898 lemma fmrel_on_fset_fmrel_restrict:
   899   "fmrel_on_fset S P m n \<longleftrightarrow> fmrel P (fmrestrict_fset S m) (fmrestrict_fset S n)"
   900 unfolding fmrel_on_fset_alt_def fmrel_iff
   901 by auto
   902 
   903 lemma fmrel_on_fset_refl_strong:
   904   assumes "\<And>x y. x |\<in>| S \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P y y"
   905   shows "fmrel_on_fset S P m m"
   906 unfolding fmrel_on_fset_fmrel_restrict fmrel_iff
   907 using assms
   908 by (simp add: option.rel_sel)
   909 
   910 lemma fmrel_on_fset_addI:
   911   assumes "fmrel_on_fset S P m n" "fmrel_on_fset S P a b"
   912   shows "fmrel_on_fset S P (m ++\<^sub>f a) (n ++\<^sub>f b)"
   913 using assms
   914 unfolding fmrel_on_fset_fmrel_restrict
   915 by auto
   916 
   917 lemma fmrel_fmdom_eq:
   918   assumes "fmrel P x y"
   919   shows "fmdom x = fmdom y"
   920 proof -
   921   have "a |\<in>| fmdom x \<longleftrightarrow> a |\<in>| fmdom y" for a
   922     proof -
   923       have "rel_option P (fmlookup x a) (fmlookup y a)"
   924         using assms by (simp add: fmrel_iff)
   925       thus ?thesis
   926         by cases (auto intro: fmdomI)
   927     qed
   928   thus ?thesis
   929     by auto
   930 qed
   931 
   932 lemma fmrel_fmdom'_eq: "fmrel P x y \<Longrightarrow> fmdom' x = fmdom' y"
   933 unfolding fmdom'_alt_def
   934 by (metis fmrel_fmdom_eq)
   935 
   936 lemma fmrel_rel_fmran:
   937   assumes "fmrel P x y"
   938   shows "rel_fset P (fmran x) (fmran y)"
   939 proof -
   940   {
   941     fix b
   942     assume "b |\<in>| fmran x"
   943     then obtain a where "fmlookup x a = Some b"
   944       by auto
   945     moreover have "rel_option P (fmlookup x a) (fmlookup y a)"
   946       using assms by auto
   947     ultimately have "\<exists>b'. b' |\<in>| fmran y \<and> P b b'"
   948       by (metis option_rel_Some1 fmranI)
   949   }
   950   moreover
   951   {
   952     fix b
   953     assume "b |\<in>| fmran y"
   954     then obtain a where "fmlookup y a = Some b"
   955       by auto
   956     moreover have "rel_option P (fmlookup x a) (fmlookup y a)"
   957       using assms by auto
   958     ultimately have "\<exists>b'. b' |\<in>| fmran x \<and> P b' b"
   959       by (metis option_rel_Some2 fmranI)
   960   }
   961   ultimately show ?thesis
   962     unfolding rel_fset_alt_def
   963     by auto
   964 qed
   965 
   966 lemma fmrel_rel_fmran': "fmrel P x y \<Longrightarrow> rel_set P (fmran' x) (fmran' y)"
   967 unfolding fmran'_alt_def
   968 by (metis fmrel_rel_fmran rel_fset_fset)
   969 
   970 lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\<lambda>_. P)"
   971 unfolding fmap.pred_set fmran'_alt_def
   972 including fset.lifting
   973 apply transfer'
   974 apply (rule ext)
   975 apply (auto simp: map_pred_def ran_def split: option.splits dest: )
   976 done
   977 
   978 lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \<longleftrightarrow> pred_fmap f m"
   979 unfolding fmap.pred_set fmap.set_map
   980 by simp
   981 
   982 lemma pred_fmapD: "pred_fmap P m \<Longrightarrow> x |\<in>| fmran m \<Longrightarrow> P x"
   983 by auto
   984 
   985 lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)"
   986 by transfer' auto
   987 
   988 lemma fmpred_map[simp]: "fmpred P (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>k v. P k (f v)) m"
   989 unfolding fmpred_iff pred_fmap_def fmap.set_map
   990 by auto
   991 
   992 lemma fmpred_id[simp]: "fmpred (\<lambda>_. id) (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>_. f) m"
   993 by simp
   994 
   995 lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n"
   996 by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
   997 
   998 lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty"
   999 by transfer auto
  1000 
  1001 lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m"
  1002 including fset.lifting
  1003 by transfer' simp
  1004 
  1005 lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m"
  1006 by transfer' simp
  1007 
  1008 lemma fmran_fmmap[simp]: "fmran (fmmap f m) = f |`| fmran m"
  1009 including fset.lifting
  1010 by transfer' (auto simp: ran_def)
  1011 
  1012 lemma fmran'_fmmap[simp]: "fmran' (fmmap f m) = f ` fmran' m"
  1013 by transfer' (auto simp: ran_def)
  1014 
  1015 lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)"
  1016 by transfer' (auto simp: map_filter_def)
  1017 
  1018 lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" unfolding fmfilter_alt_defs by simp
  1019 lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp
  1020 lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp
  1021 lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp
  1022 lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp
  1023 
  1024 lemma fmmap_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap f m \<subseteq>\<^sub>f fmmap f n"
  1025 by transfer' (auto simp: map_le_def)
  1026 
  1027 lemma fmmap_fset_of_fmap: "fset_of_fmap (fmmap f m) = (\<lambda>(k, v). (k, f v)) |`| fset_of_fmap m"
  1028 including fset.lifting
  1029 by transfer' (auto simp: set_of_map_def)
  1030 
  1031 
  1032 subsection \<open>@{const size} setup\<close>
  1033 
  1034 definition size_fmap :: "('a \<Rightarrow> nat) \<Rightarrow> ('b \<Rightarrow> nat) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> nat" where
  1035 [simp]: "size_fmap f g m = size_fset (\<lambda>(a, b). f a + g b) (fset_of_fmap m)"
  1036 
  1037 instantiation fmap :: (type, type) size begin
  1038 
  1039 definition size_fmap where
  1040 size_fmap_overloaded_def: "size_fmap = Finite_Map.size_fmap (\<lambda>_. 0) (\<lambda>_. 0)"
  1041 
  1042 instance ..
  1043 
  1044 end
  1045 
  1046 lemma size_fmap_overloaded_simps[simp]: "size x = size (fset_of_fmap x)"
  1047 unfolding size_fmap_overloaded_def
  1048 by simp
  1049 
  1050 lemma fmap_size_o_map: "inj h \<Longrightarrow> size_fmap f g \<circ> fmmap h = size_fmap f (g \<circ> h)"
  1051   unfolding size_fmap_def
  1052   apply (auto simp: fun_eq_iff fmmap_fset_of_fmap)
  1053   apply (subst sum.reindex)
  1054   subgoal for m
  1055     using prod.inj_map[unfolded map_prod_def, of "\<lambda>x. x" h]
  1056     unfolding inj_on_def
  1057     by auto
  1058   subgoal
  1059     by (rule sum.cong) (auto split: prod.splits)
  1060   done
  1061 
  1062 setup \<open>
  1063 BNF_LFP_Size.register_size_global @{type_name fmap} @{const_name size_fmap}
  1064   @{thm size_fmap_overloaded_def} @{thms size_fmap_def size_fmap_overloaded_simps}
  1065   @{thms fmap_size_o_map}
  1066 \<close>
  1067 
  1068 
  1069 subsection \<open>Additional operations\<close>
  1070 
  1071 lift_definition fmmap_keys :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap" is
  1072   "\<lambda>f m a. map_option (f a) (m a)"
  1073 unfolding dom_def
  1074 by simp
  1075 
  1076 lemma fmpred_fmmap_keys[simp]: "fmpred P (fmmap_keys f m) = fmpred (\<lambda>a b. P a (f a b)) m"
  1077 by transfer' (auto simp: map_pred_def split: option.splits)
  1078 
  1079 lemma fmdom_fmmap_keys[simp]: "fmdom (fmmap_keys f m) = fmdom m"
  1080 including fset.lifting
  1081 by transfer' auto
  1082 
  1083 lemma fmlookup_fmmap_keys[simp]: "fmlookup (fmmap_keys f m) x = map_option (f x) (fmlookup m x)"
  1084 by transfer' simp
  1085 
  1086 lemma fmfilter_fmmap_keys[simp]: "fmfilter P (fmmap_keys f m) = fmmap_keys f (fmfilter P m)"
  1087 by transfer' (auto simp: map_filter_def)
  1088 
  1089 lemma fmdrop_fmmap_keys[simp]: "fmdrop a (fmmap_keys f m) = fmmap_keys f (fmdrop a m)"
  1090 unfolding fmfilter_alt_defs by simp
  1091 
  1092 lemma fmdrop_set_fmmap_keys[simp]: "fmdrop_set A (fmmap_keys f m) = fmmap_keys f (fmdrop_set A m)"
  1093 unfolding fmfilter_alt_defs by simp
  1094 
  1095 lemma fmdrop_fset_fmmap_keys[simp]: "fmdrop_fset A (fmmap_keys f m) = fmmap_keys f (fmdrop_fset A m)"
  1096 unfolding fmfilter_alt_defs by simp
  1097 
  1098 lemma fmrestrict_set_fmmap_keys[simp]: "fmrestrict_set A (fmmap_keys f m) = fmmap_keys f (fmrestrict_set A m)"
  1099 unfolding fmfilter_alt_defs by simp
  1100 
  1101 lemma fmrestrict_fset_fmmap_keys[simp]: "fmrestrict_fset A (fmmap_keys f m) = fmmap_keys f (fmrestrict_fset A m)"
  1102 unfolding fmfilter_alt_defs by simp
  1103 
  1104 lemma fmmap_keys_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap_keys f m \<subseteq>\<^sub>f fmmap_keys f n"
  1105 by transfer' (auto simp: map_le_def dom_def)
  1106 
  1107 definition sorted_list_of_fmap :: "('a::linorder, 'b) fmap \<Rightarrow> ('a \<times> 'b) list" where
  1108 "sorted_list_of_fmap m = map (\<lambda>k. (k, the (fmlookup m k))) (sorted_list_of_fset (fmdom m))"
  1109 
  1110 lemma list_all_sorted_list[simp]: "list_all P (sorted_list_of_fmap m) = fmpred (curry P) m"
  1111 unfolding sorted_list_of_fmap_def curry_def list.pred_map
  1112 apply (auto simp: list_all_iff)
  1113 including fset.lifting
  1114 by (transfer; auto simp: dom_def map_pred_def split: option.splits)+
  1115 
  1116 lemma map_of_sorted_list[simp]: "map_of (sorted_list_of_fmap m) = fmlookup m"
  1117 unfolding sorted_list_of_fmap_def
  1118 including fset.lifting
  1119 by transfer (simp add: map_of_map_keys)
  1120 
  1121 
  1122 subsection \<open>Additional properties\<close>
  1123 
  1124 lemma fmchoice':
  1125   assumes "finite S" "\<forall>x \<in> S. \<exists>y. Q x y"
  1126   shows "\<exists>m. fmdom' m = S \<and> fmpred Q m"
  1127 proof -
  1128   obtain f where f: "Q x (f x)" if "x \<in> S" for x
  1129     using assms by (metis bchoice)
  1130   define f' where "f' x = (if x \<in> S then Some (f x) else None)" for x
  1131 
  1132   have "eq_onp (\<lambda>m. finite (dom m)) f' f'"
  1133     unfolding eq_onp_def f'_def dom_def using assms by auto
  1134 
  1135   show ?thesis
  1136     apply (rule exI[where x = "Abs_fmap f'"])
  1137     apply (subst fmpred.abs_eq, fact)
  1138     apply (subst fmdom'.abs_eq, fact)
  1139     unfolding f'_def dom_def map_pred_def using f
  1140     by auto
  1141 qed
  1142 
  1143 subsection \<open>Lifting/transfer setup\<close>
  1144 
  1145 context includes lifting_syntax begin
  1146 
  1147 lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty"
  1148 by transfer auto
  1149 
  1150 lemma fmadd_transfer[transfer_rule]:
  1151   "(fmrel P ===> fmrel P ===> fmrel P) fmadd fmadd"
  1152 by (intro fmrel_addI rel_funI)
  1153 
  1154 lemma fmupd_transfer[transfer_rule]:
  1155   "((=) ===> P ===> fmrel P ===> fmrel P) fmupd fmupd"
  1156 by auto
  1157 
  1158 end
  1159 
  1160 lemma Quotient_fmap_bnf[quot_map]:
  1161   assumes "Quotient R Abs Rep T"
  1162   shows "Quotient (fmrel R) (fmmap Abs) (fmmap Rep) (fmrel T)"
  1163 unfolding Quotient_alt_def4 proof safe
  1164   fix m n
  1165   assume "fmrel T m n"
  1166   then have "fmlookup (fmmap Abs m) x = fmlookup n x" for x
  1167     apply (cases rule: fmrel_cases[where x = x])
  1168     using assms unfolding Quotient_alt_def by auto
  1169   then show "fmmap Abs m = n"
  1170     by (rule fmap_ext)
  1171 next
  1172   fix m
  1173   show "fmrel T (fmmap Rep m) m"
  1174     unfolding fmap.rel_map
  1175     apply (rule fmap.rel_refl)
  1176     using assms unfolding Quotient_alt_def
  1177     by auto
  1178 next
  1179   from assms have "R = T OO T\<inverse>\<inverse>"
  1180     unfolding Quotient_alt_def4 by simp
  1181 
  1182   then show "fmrel R = fmrel T OO (fmrel T)\<inverse>\<inverse>"
  1183     by (simp add: fmap.rel_compp fmap.rel_conversep)
  1184 qed
  1185 
  1186 
  1187 subsection \<open>View as datatype\<close>
  1188 
  1189 lemma fmap_distinct[simp]:
  1190   "fmempty \<noteq> fmupd k v m"
  1191   "fmupd k v m \<noteq> fmempty"
  1192 by (transfer'; auto simp: map_upd_def fun_eq_iff)+
  1193 
  1194 lifting_update fmap.lifting
  1195 
  1196 lemma fmap_exhaust[cases type: fmap]:
  1197   obtains (fmempty) "m = fmempty"
  1198         | (fmupd) x y m' where "m = fmupd x y m'" "x |\<notin>| fmdom m'"
  1199 using that including fmap.lifting fset.lifting
  1200 proof transfer
  1201   fix m P
  1202   assume "finite (dom m)"
  1203   assume empty: P if "m = Map.empty"
  1204   assume map_upd: P if "finite (dom m')" "m = map_upd x y m'" "x \<notin> dom m'" for x y m'
  1205 
  1206   show P
  1207     proof (cases "m = Map.empty")
  1208       case True thus ?thesis using empty by simp
  1209     next
  1210       case False
  1211       hence "dom m \<noteq> {}" by simp
  1212       then obtain x where "x \<in> dom m" by blast
  1213 
  1214       let ?m' = "map_drop x m"
  1215 
  1216       show ?thesis
  1217         proof (rule map_upd)
  1218           show "finite (dom ?m')"
  1219             using \<open>finite (dom m)\<close>
  1220             unfolding map_drop_def
  1221             by auto
  1222         next
  1223           show "m = map_upd x (the (m x)) ?m'"
  1224             using \<open>x \<in> dom m\<close> unfolding map_drop_def map_filter_def map_upd_def
  1225             by auto
  1226         next
  1227           show "x \<notin> dom ?m'"
  1228             unfolding map_drop_def map_filter_def
  1229             by auto
  1230         qed
  1231     qed
  1232 qed
  1233 
  1234 lemma fmap_induct[case_names fmempty fmupd, induct type: fmap]:
  1235   assumes "P fmempty"
  1236   assumes "(\<And>x y m. P m \<Longrightarrow> fmlookup m x = None \<Longrightarrow> P (fmupd x y m))"
  1237   shows "P m"
  1238 proof (induction "fmdom m" arbitrary: m rule: fset_induct_stronger)
  1239   case empty
  1240   hence "m = fmempty"
  1241     by (metis fmrestrict_fset_dom fmrestrict_fset_null)
  1242   with assms show ?case
  1243     by simp
  1244 next
  1245   case (insert x S)
  1246   hence "S = fmdom (fmdrop x m)"
  1247     by auto
  1248   with insert have "P (fmdrop x m)"
  1249     by auto
  1250 
  1251   have "x |\<in>| fmdom m"
  1252     using insert by auto
  1253   then obtain y where "fmlookup m x = Some y"
  1254     by auto
  1255   hence "m = fmupd x y (fmdrop x m)"
  1256     by (auto intro: fmap_ext)
  1257 
  1258   show ?case
  1259     apply (subst \<open>m = _\<close>)
  1260     apply (rule assms)
  1261     apply fact
  1262     apply simp
  1263     done
  1264 qed
  1265 
  1266 
  1267 subsection \<open>Code setup\<close>
  1268 
  1269 instantiation fmap :: (type, equal) equal begin
  1270 
  1271 definition "equal_fmap \<equiv> fmrel HOL.equal"
  1272 
  1273 instance proof
  1274   fix m n :: "('a, 'b) fmap"
  1275   have "fmrel (=) m n \<longleftrightarrow> (m = n)"
  1276     by transfer' (simp add: option.rel_eq rel_fun_eq)
  1277   then show "equal_class.equal m n \<longleftrightarrow> (m = n)"
  1278     unfolding equal_fmap_def
  1279     by (simp add: equal_eq[abs_def])
  1280 qed
  1281 
  1282 end
  1283 
  1284 lemma fBall_alt_def: "fBall S P \<longleftrightarrow> (\<forall>x. x |\<in>| S \<longrightarrow> P x)"
  1285 by force
  1286 
  1287 lemma fmrel_code:
  1288   "fmrel R m n \<longleftrightarrow>
  1289     fBall (fmdom m) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x)) \<and>
  1290     fBall (fmdom n) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x))"
  1291 unfolding fmrel_iff fmlookup_dom_iff fBall_alt_def
  1292 by (metis option.collapse option.rel_sel)
  1293 
  1294 lemmas [code] =
  1295   fmrel_code
  1296   fmran'_alt_def
  1297   fmdom'_alt_def
  1298   fmfilter_alt_defs
  1299   pred_fmap_fmpred
  1300   fmsubset_alt_def
  1301   fmupd_alt_def
  1302   fmrel_on_fset_alt_def
  1303   fmpred_alt_def
  1304 
  1305 
  1306 code_datatype fmap_of_list
  1307 quickcheck_generator fmap constructors: fmap_of_list
  1308 
  1309 context includes fset.lifting begin
  1310 
  1311 lemma fmlookup_of_list[code]: "fmlookup (fmap_of_list m) = map_of m"
  1312 by transfer simp
  1313 
  1314 lemma fmempty_of_list[code]: "fmempty = fmap_of_list []"
  1315 by transfer simp
  1316 
  1317 lemma fmran_of_list[code]: "fmran (fmap_of_list m) = snd |`| fset_of_list (AList.clearjunk m)"
  1318 by transfer (auto simp: ran_map_of)
  1319 
  1320 lemma fmdom_of_list[code]: "fmdom (fmap_of_list m) = fst |`| fset_of_list m"
  1321 by transfer (auto simp: dom_map_of_conv_image_fst)
  1322 
  1323 lemma fmfilter_of_list[code]: "fmfilter P (fmap_of_list m) = fmap_of_list (filter (\<lambda>(k, _). P k) m)"
  1324 by transfer' auto
  1325 
  1326 lemma fmadd_of_list[code]: "fmap_of_list m ++\<^sub>f fmap_of_list n = fmap_of_list (AList.merge m n)"
  1327 by transfer (simp add: merge_conv')
  1328 
  1329 lemma fmmap_of_list[code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)"
  1330 apply transfer
  1331 apply (subst map_of_map[symmetric])
  1332 apply (auto simp: apsnd_def map_prod_def)
  1333 done
  1334 
  1335 lemma fmmap_keys_of_list[code]:
  1336   "fmmap_keys f (fmap_of_list m) = fmap_of_list (map (\<lambda>(a, b). (a, f a b)) m)"
  1337 apply transfer
  1338 subgoal for f m by (induction m) (auto simp: apsnd_def map_prod_def fun_eq_iff)
  1339 done
  1340 
  1341 lemma fmimage_of_list[code]:
  1342   "fmimage (fmap_of_list m) A = fset_of_list (map snd (filter (\<lambda>(k, _). k |\<in>| A) (AList.clearjunk m)))"
  1343 apply (subst fmimage_alt_def)
  1344 apply (subst fmfilter_alt_defs)
  1345 apply (subst fmfilter_of_list)
  1346 apply (subst fmran_of_list)
  1347 apply transfer'
  1348 apply (subst AList.restrict_eq[symmetric])
  1349 apply (subst clearjunk_restrict)
  1350 apply (subst AList.restrict_eq)
  1351 by auto
  1352 
  1353 lemma fmcomp_list[code]:
  1354   "fmap_of_list m \<circ>\<^sub>f fmap_of_list n = fmap_of_list (AList.compose n m)"
  1355 by (rule fmap_ext) (simp add: fmlookup_of_list compose_conv map_comp_def split: option.splits)
  1356 
  1357 end
  1358 
  1359 
  1360 subsection \<open>Instances\<close>
  1361 
  1362 lemma exists_map_of:
  1363   assumes "finite (dom m)" shows "\<exists>xs. map_of xs = m"
  1364   using assms
  1365 proof (induction "dom m" arbitrary: m)
  1366   case empty
  1367   hence "m = Map.empty"
  1368     by auto
  1369   moreover have "map_of [] = Map.empty"
  1370     by simp
  1371   ultimately show ?case
  1372     by blast
  1373 next
  1374   case (insert x F)
  1375   hence "F = dom (map_drop x m)"
  1376     unfolding map_drop_def map_filter_def dom_def by auto
  1377   with insert have "\<exists>xs'. map_of xs' = map_drop x m"
  1378     by auto
  1379   then obtain xs' where "map_of xs' = map_drop x m"
  1380     ..
  1381   moreover obtain y where "m x = Some y"
  1382     using insert unfolding dom_def by blast
  1383   ultimately have "map_of ((x, y) # xs') = m"
  1384     using \<open>insert x F = dom m\<close>
  1385     unfolding map_drop_def map_filter_def
  1386     by auto
  1387   thus ?case
  1388     ..
  1389 qed
  1390 
  1391 lemma exists_fmap_of_list: "\<exists>xs. fmap_of_list xs = m"
  1392 by transfer (rule exists_map_of)
  1393 
  1394 lemma fmap_of_list_surj[simp, intro]: "surj fmap_of_list"
  1395 proof -
  1396   have "x \<in> range fmap_of_list" for x :: "('a, 'b) fmap"
  1397     unfolding image_iff
  1398     using exists_fmap_of_list by (metis UNIV_I)
  1399   thus ?thesis by auto
  1400 qed
  1401 
  1402 instance fmap :: (countable, countable) countable
  1403 proof
  1404   obtain to_nat :: "('a \<times> 'b) list \<Rightarrow> nat" where "inj to_nat"
  1405     by (metis ex_inj)
  1406   moreover have "inj (inv fmap_of_list)"
  1407     using fmap_of_list_surj by (rule surj_imp_inj_inv)
  1408   ultimately have "inj (to_nat \<circ> inv fmap_of_list)"
  1409     by (rule inj_comp)
  1410   thus "\<exists>to_nat::('a, 'b) fmap \<Rightarrow> nat. inj to_nat"
  1411     by auto
  1412 qed
  1413 
  1414 instance fmap :: (finite, finite) finite
  1415 proof
  1416   show "finite (UNIV :: ('a, 'b) fmap set)"
  1417     by (rule finite_imageD) auto
  1418 qed
  1419 
  1420 lifting_update fmap.lifting
  1421 lifting_forget fmap.lifting
  1422 
  1423 
  1424 subsection \<open>Tests\<close>
  1425 
  1426 \<comment> \<open>Code generation\<close>
  1427 
  1428 export_code
  1429   fBall fmrel fmran fmran' fmdom fmdom' fmpred pred_fmap fmsubset fmupd fmrel_on_fset
  1430   fmdrop fmdrop_set fmdrop_fset fmrestrict_set fmrestrict_fset fmimage fmlookup fmempty
  1431   fmfilter fmadd fmmap fmmap_keys fmcomp
  1432   checking SML Scala Haskell? OCaml?
  1433 
  1434 \<comment> \<open>\<open>lifting\<close> through @{type fmap}\<close>
  1435 
  1436 experiment begin
  1437 
  1438 context includes fset.lifting begin
  1439 
  1440 lift_definition test1 :: "('a, 'b fset) fmap" is "fmempty :: ('a, 'b set) fmap"
  1441   by auto
  1442 
  1443 lift_definition test2 :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b fset) fmap" is "\<lambda>a b. fmupd a {b} fmempty"
  1444   by auto
  1445 
  1446 end
  1447 
  1448 end
  1449 
  1450 end