src/HOL/Library/Finite_Map.thy
 author haftmann Wed Jul 18 20:51:21 2018 +0200 (11 months ago) changeset 68658 16cc1161ad7f parent 68463 410818a69ee3 child 68757 e7e3776385ba permissions -rw-r--r--
tuned equation
```     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 end
```
```   138
```
```   139
```
```   140 subsection \<open>Abstract characterisation\<close>
```
```   141
```
```   142 typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a \<rightharpoonup> 'b) set"
```
```   143   morphisms fmlookup Abs_fmap
```
```   144 proof
```
```   145   show "Map.empty \<in> {m. finite (dom m)}"
```
```   146     by auto
```
```   147 qed
```
```   148
```
```   149 setup_lifting type_definition_fmap
```
```   150
```
```   151 lemma fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))"
```
```   152 using fmap.fmlookup by auto
```
```   153
```
```   154 lemma fmap_ext:
```
```   155   assumes "\<And>x. fmlookup m x = fmlookup n x"
```
```   156   shows "m = n"
```
```   157 using assms
```
```   158 by transfer' auto
```
```   159
```
```   160
```
```   161 subsection \<open>Operations\<close>
```
```   162
```
```   163 context
```
```   164   includes fset.lifting
```
```   165 begin
```
```   166
```
```   167 lift_definition fmran :: "('a, 'b) fmap \<Rightarrow> 'b fset"
```
```   168   is ran
```
```   169   parametric ran_transfer
```
```   170 by (rule finite_ran)
```
```   171
```
```   172 lemma fmlookup_ran_iff: "y |\<in>| fmran m \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y)"
```
```   173 by transfer' (auto simp: ran_def)
```
```   174
```
```   175 lemma fmranI: "fmlookup m x = Some y \<Longrightarrow> y |\<in>| fmran m" by (auto simp: fmlookup_ran_iff)
```
```   176
```
```   177 lemma fmranE[elim]:
```
```   178   assumes "y |\<in>| fmran m"
```
```   179   obtains x where "fmlookup m x = Some y"
```
```   180 using assms by (auto simp: fmlookup_ran_iff)
```
```   181
```
```   182 lift_definition fmdom :: "('a, 'b) fmap \<Rightarrow> 'a fset"
```
```   183   is dom
```
```   184   parametric dom_transfer
```
```   185 .
```
```   186
```
```   187 lemma fmlookup_dom_iff: "x |\<in>| fmdom m \<longleftrightarrow> (\<exists>a. fmlookup m x = Some a)"
```
```   188 by transfer' auto
```
```   189
```
```   190 lemma fmdom_notI: "fmlookup m x = None \<Longrightarrow> x |\<notin>| fmdom m" by (simp add: fmlookup_dom_iff)
```
```   191 lemma fmdomI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| fmdom m" by (simp add: fmlookup_dom_iff)
```
```   192 lemma fmdom_notD[dest]: "x |\<notin>| fmdom m \<Longrightarrow> fmlookup m x = None" by (simp add: fmlookup_dom_iff)
```
```   193
```
```   194 lemma fmdomE[elim]:
```
```   195   assumes "x |\<in>| fmdom m"
```
```   196   obtains y where "fmlookup m x = Some y"
```
```   197 using assms by (auto simp: fmlookup_dom_iff)
```
```   198
```
```   199 lift_definition fmdom' :: "('a, 'b) fmap \<Rightarrow> 'a set"
```
```   200   is dom
```
```   201   parametric dom_transfer
```
```   202 .
```
```   203
```
```   204 lemma fmlookup_dom'_iff: "x \<in> fmdom' m \<longleftrightarrow> (\<exists>a. fmlookup m x = Some a)"
```
```   205 by transfer' auto
```
```   206
```
```   207 lemma fmdom'_notI: "fmlookup m x = None \<Longrightarrow> x \<notin> fmdom' m" by (simp add: fmlookup_dom'_iff)
```
```   208 lemma fmdom'I: "fmlookup m x = Some y \<Longrightarrow> x \<in> fmdom' m" by (simp add: fmlookup_dom'_iff)
```
```   209 lemma fmdom'_notD[dest]: "x \<notin> fmdom' m \<Longrightarrow> fmlookup m x = None" by (simp add: fmlookup_dom'_iff)
```
```   210
```
```   211 lemma fmdom'E[elim]:
```
```   212   assumes "x \<in> fmdom' m"
```
```   213   obtains x y where "fmlookup m x = Some y"
```
```   214 using assms by (auto simp: fmlookup_dom'_iff)
```
```   215
```
```   216 lemma fmdom'_alt_def: "fmdom' m = fset (fmdom m)"
```
```   217 by transfer' force
```
```   218
```
```   219 lift_definition fmempty :: "('a, 'b) fmap"
```
```   220   is Map.empty
```
```   221 by simp
```
```   222
```
```   223 lemma fmempty_lookup[simp]: "fmlookup fmempty x = None"
```
```   224 by transfer' simp
```
```   225
```
```   226 lemma fmdom_empty[simp]: "fmdom fmempty = {||}" by transfer' simp
```
```   227 lemma fmdom'_empty[simp]: "fmdom' fmempty = {}" by transfer' simp
```
```   228 lemma fmran_empty[simp]: "fmran fmempty = fempty" by transfer' (auto simp: ran_def map_filter_def)
```
```   229
```
```   230 lift_definition fmupd :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   231   is map_upd
```
```   232   parametric map_upd_transfer
```
```   233 unfolding map_upd_def[abs_def]
```
```   234 by simp
```
```   235
```
```   236 lemma fmupd_lookup[simp]: "fmlookup (fmupd a b m) a' = (if a = a' then Some b else fmlookup m a')"
```
```   237 by transfer' (auto simp: map_upd_def)
```
```   238
```
```   239 lemma fmdom_fmupd[simp]: "fmdom (fmupd a b m) = finsert a (fmdom m)" by transfer (simp add: map_upd_def)
```
```   240 lemma fmdom'_fmupd[simp]: "fmdom' (fmupd a b m) = insert a (fmdom' m)" by transfer (simp add: map_upd_def)
```
```   241
```
```   242 lift_definition fmfilter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   243   is map_filter
```
```   244   parametric map_filter_transfer
```
```   245 by auto
```
```   246
```
```   247 lemma fmdom_filter[simp]: "fmdom (fmfilter P m) = ffilter P (fmdom m)"
```
```   248 by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
```
```   249
```
```   250 lemma fmdom'_filter[simp]: "fmdom' (fmfilter P m) = Set.filter P (fmdom' m)"
```
```   251 by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
```
```   252
```
```   253 lemma fmlookup_filter[simp]: "fmlookup (fmfilter P m) x = (if P x then fmlookup m x else None)"
```
```   254 by transfer' (auto simp: map_filter_def)
```
```   255
```
```   256 lemma fmfilter_empty[simp]: "fmfilter P fmempty = fmempty"
```
```   257 by transfer' (auto simp: map_filter_def)
```
```   258
```
```   259 lemma fmfilter_true[simp]:
```
```   260   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x"
```
```   261   shows "fmfilter P m = m"
```
```   262 proof (rule fmap_ext)
```
```   263   fix x
```
```   264   have "fmlookup m x = None" if "\<not> P x"
```
```   265     using that assms by fastforce
```
```   266   then show "fmlookup (fmfilter P m) x = fmlookup m x"
```
```   267     by simp
```
```   268 qed
```
```   269
```
```   270 lemma fmfilter_false[simp]:
```
```   271   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> \<not> P x"
```
```   272   shows "fmfilter P m = fmempty"
```
```   273 using assms by transfer' (fastforce simp: map_filter_def)
```
```   274
```
```   275 lemma fmfilter_comp[simp]: "fmfilter P (fmfilter Q m) = fmfilter (\<lambda>x. P x \<and> Q x) m"
```
```   276 by transfer' (auto simp: map_filter_def)
```
```   277
```
```   278 lemma fmfilter_comm: "fmfilter P (fmfilter Q m) = fmfilter Q (fmfilter P m)"
```
```   279 unfolding fmfilter_comp by meson
```
```   280
```
```   281 lemma fmfilter_cong[cong]:
```
```   282   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x = Q x"
```
```   283   shows "fmfilter P m = fmfilter Q m"
```
```   284 proof (rule fmap_ext)
```
```   285   fix x
```
```   286   have "fmlookup m x = None" if "P x \<noteq> Q x"
```
```   287     using that assms by fastforce
```
```   288   then show "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x"
```
```   289     by auto
```
```   290 qed
```
```   291
```
```   292 lemma fmfilter_cong'[fundef_cong]:
```
```   293   assumes "m = n" "\<And>x. x \<in> fmdom' m \<Longrightarrow> P x = Q x"
```
```   294   shows "fmfilter P m = fmfilter Q n"
```
```   295 using assms(2) unfolding assms(1)
```
```   296 by (rule fmfilter_cong) (metis fmdom'I)
```
```   297
```
```   298 lemma fmfilter_upd[simp]:
```
```   299   "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)"
```
```   300 by transfer' (auto simp: map_upd_def map_filter_def)
```
```   301
```
```   302 lift_definition fmdrop :: "'a \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   303   is map_drop
```
```   304   parametric map_drop_transfer
```
```   305 unfolding map_drop_def by auto
```
```   306
```
```   307 lemma fmdrop_lookup[simp]: "fmlookup (fmdrop a m) a = None"
```
```   308 by transfer' (auto simp: map_drop_def map_filter_def)
```
```   309
```
```   310 lift_definition fmdrop_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   311   is map_drop_set
```
```   312   parametric map_drop_set_transfer
```
```   313 unfolding map_drop_set_def by auto
```
```   314
```
```   315 lift_definition fmdrop_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   316   is map_drop_set
```
```   317   parametric map_drop_set_transfer
```
```   318 unfolding map_drop_set_def by auto
```
```   319
```
```   320 lift_definition fmrestrict_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   321   is map_restrict_set
```
```   322   parametric map_restrict_set_transfer
```
```   323 unfolding map_restrict_set_def by auto
```
```   324
```
```   325 lift_definition fmrestrict_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   326   is map_restrict_set
```
```   327   parametric map_restrict_set_transfer
```
```   328 unfolding map_restrict_set_def by auto
```
```   329
```
```   330 lemma fmfilter_alt_defs:
```
```   331   "fmdrop a = fmfilter (\<lambda>a'. a' \<noteq> a)"
```
```   332   "fmdrop_set A = fmfilter (\<lambda>a. a \<notin> A)"
```
```   333   "fmdrop_fset B = fmfilter (\<lambda>a. a |\<notin>| B)"
```
```   334   "fmrestrict_set A = fmfilter (\<lambda>a. a \<in> A)"
```
```   335   "fmrestrict_fset B = fmfilter (\<lambda>a. a |\<in>| B)"
```
```   336 by (transfer'; simp add: map_drop_def map_drop_set_def map_restrict_set_def)+
```
```   337
```
```   338 lemma fmdom_drop[simp]: "fmdom (fmdrop a m) = fmdom m - {|a|}" unfolding fmfilter_alt_defs by auto
```
```   339 lemma fmdom'_drop[simp]: "fmdom' (fmdrop a m) = fmdom' m - {a}" unfolding fmfilter_alt_defs by auto
```
```   340 lemma fmdom'_drop_set[simp]: "fmdom' (fmdrop_set A m) = fmdom' m - A" unfolding fmfilter_alt_defs by auto
```
```   341 lemma fmdom_drop_fset[simp]: "fmdom (fmdrop_fset A m) = fmdom m - A" unfolding fmfilter_alt_defs by auto
```
```   342 lemma fmdom'_restrict_set: "fmdom' (fmrestrict_set A m) \<subseteq> A" unfolding fmfilter_alt_defs by auto
```
```   343 lemma fmdom_restrict_fset: "fmdom (fmrestrict_fset A m) |\<subseteq>| A" unfolding fmfilter_alt_defs by auto
```
```   344
```
```   345 lemma fmdom'_drop_fset[simp]: "fmdom' (fmdrop_fset A m) = fmdom' m - fset A"
```
```   346 unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def split: if_splits)
```
```   347
```
```   348 lemma fmdom'_restrict_fset: "fmdom' (fmrestrict_fset A m) \<subseteq> fset A"
```
```   349 unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def)
```
```   350
```
```   351 lemma fmlookup_drop[simp]:
```
```   352   "fmlookup (fmdrop a m) x = (if x \<noteq> a then fmlookup m x else None)"
```
```   353 unfolding fmfilter_alt_defs by simp
```
```   354
```
```   355 lemma fmlookup_drop_set[simp]:
```
```   356   "fmlookup (fmdrop_set A m) x = (if x \<notin> A then fmlookup m x else None)"
```
```   357 unfolding fmfilter_alt_defs by simp
```
```   358
```
```   359 lemma fmlookup_drop_fset[simp]:
```
```   360   "fmlookup (fmdrop_fset A m) x = (if x |\<notin>| A then fmlookup m x else None)"
```
```   361 unfolding fmfilter_alt_defs by simp
```
```   362
```
```   363 lemma fmlookup_restrict_set[simp]:
```
```   364   "fmlookup (fmrestrict_set A m) x = (if x \<in> A then fmlookup m x else None)"
```
```   365 unfolding fmfilter_alt_defs by simp
```
```   366
```
```   367 lemma fmlookup_restrict_fset[simp]:
```
```   368   "fmlookup (fmrestrict_fset A m) x = (if x |\<in>| A then fmlookup m x else None)"
```
```   369 unfolding fmfilter_alt_defs by simp
```
```   370
```
```   371 lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m"
```
```   372   by (rule fmap_ext) auto
```
```   373
```
```   374 lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m"
```
```   375   by (rule fmap_ext) auto
```
```   376
```
```   377 lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty"
```
```   378   unfolding fmfilter_alt_defs by simp
```
```   379
```
```   380 lemma fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty"
```
```   381   unfolding fmfilter_alt_defs by simp
```
```   382
```
```   383 lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty"
```
```   384   unfolding fmfilter_alt_defs by simp
```
```   385
```
```   386 lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty"
```
```   387   unfolding fmfilter_alt_defs by simp
```
```   388
```
```   389 lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty"
```
```   390   unfolding fmfilter_alt_defs by simp
```
```   391
```
```   392 lemma fmdrop_set_null[simp]: "fmdrop_set {} m = m"
```
```   393   by (rule fmap_ext) auto
```
```   394
```
```   395 lemma fmdrop_fset_null[simp]: "fmdrop_fset {||} m = m"
```
```   396   by (rule fmap_ext) auto
```
```   397
```
```   398 lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m"
```
```   399   unfolding fmfilter_alt_defs by simp
```
```   400
```
```   401 lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m"
```
```   402   unfolding fmfilter_alt_defs by simp
```
```   403
```
```   404 lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty"
```
```   405   unfolding fmfilter_alt_defs by simp
```
```   406
```
```   407 lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty"
```
```   408   unfolding fmfilter_alt_defs by simp
```
```   409
```
```   410 lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)"
```
```   411 unfolding fmfilter_alt_defs by (rule fmfilter_comm)
```
```   412
```
```   413 lemma fmdrop_set_insert[simp]: "fmdrop_set (insert x S) m = fmdrop x (fmdrop_set S m)"
```
```   414 by (rule fmap_ext) auto
```
```   415
```
```   416 lemma fmdrop_fset_insert[simp]: "fmdrop_fset (finsert x S) m = fmdrop x (fmdrop_fset S m)"
```
```   417 by (rule fmap_ext) auto
```
```   418
```
```   419 lift_definition fmadd :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap" (infixl "++\<^sub>f" 100)
```
```   420   is map_add
```
```   421   parametric map_add_transfer
```
```   422 by simp
```
```   423
```
```   424 lemma fmlookup_add[simp]:
```
```   425   "fmlookup (m ++\<^sub>f n) x = (if x |\<in>| fmdom n then fmlookup n x else fmlookup m x)"
```
```   426   by transfer' (auto simp: map_add_def split: option.splits)
```
```   427
```
```   428 lemma fmdom_add[simp]: "fmdom (m ++\<^sub>f n) = fmdom m |\<union>| fmdom n" by transfer' auto
```
```   429 lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \<union> fmdom' n" by transfer' auto
```
```   430
```
```   431 lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
```
```   432   by (rule fmap_ext) auto
```
```   433
```
```   434 lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
```
```   435   by (rule fmap_ext) auto
```
```   436
```
```   437 lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n"
```
```   438 by transfer' (auto simp: map_filter_def map_add_def)
```
```   439
```
```   440 lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n"
```
```   441   unfolding fmfilter_alt_defs by simp
```
```   442
```
```   443 lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n"
```
```   444   unfolding fmfilter_alt_defs by simp
```
```   445
```
```   446 lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n"
```
```   447   unfolding fmfilter_alt_defs by simp
```
```   448
```
```   449 lemma fmrestrict_set_add_distrib[simp]:
```
```   450   "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n"
```
```   451   unfolding fmfilter_alt_defs by simp
```
```   452
```
```   453 lemma fmrestrict_fset_add_distrib[simp]:
```
```   454   "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n"
```
```   455   unfolding fmfilter_alt_defs by simp
```
```   456
```
```   457 lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m"
```
```   458 by (transfer'; auto)+
```
```   459
```
```   460 lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m"
```
```   461 by transfer' (auto simp: map_add_def split: option.splits)
```
```   462
```
```   463 lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p"
```
```   464 by transfer' simp
```
```   465
```
```   466 lemma fmadd_fmupd[simp]: "m ++\<^sub>f fmupd a b n = fmupd a b (m ++\<^sub>f n)"
```
```   467 by (rule fmap_ext) simp
```
```   468
```
```   469 lift_definition fmpred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool"
```
```   470   is map_pred
```
```   471   parametric map_pred_transfer
```
```   472 .
```
```   473
```
```   474 lemma fmpredI[intro]:
```
```   475   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y"
```
```   476   shows "fmpred P m"
```
```   477 using assms
```
```   478 by transfer' (auto simp: map_pred_def split: option.splits)
```
```   479
```
```   480 lemma fmpredD[dest]: "fmpred P m \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P x y"
```
```   481 by transfer' (auto simp: map_pred_def split: option.split_asm)
```
```   482
```
```   483 lemma fmpred_iff: "fmpred P m \<longleftrightarrow> (\<forall>x y. fmlookup m x = Some y \<longrightarrow> P x y)"
```
```   484 by auto
```
```   485
```
```   486 lemma fmpred_alt_def: "fmpred P m \<longleftrightarrow> fBall (fmdom m) (\<lambda>x. P x (the (fmlookup m x)))"
```
```   487 unfolding fmpred_iff
```
```   488 apply auto
```
```   489 apply (rename_tac x y)
```
```   490 apply (erule_tac x = x in fBallE)
```
```   491 apply simp
```
```   492 by (simp add: fmlookup_dom_iff)
```
```   493
```
```   494 lemma fmpred_empty[intro!, simp]: "fmpred P fmempty"
```
```   495 by auto
```
```   496
```
```   497 lemma fmpred_upd[intro]: "fmpred P m \<Longrightarrow> P x y \<Longrightarrow> fmpred P (fmupd x y m)"
```
```   498 by transfer' (auto simp: map_pred_def map_upd_def)
```
```   499
```
```   500 lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \<Longrightarrow> P x y"
```
```   501 by auto
```
```   502
```
```   503 lemma fmpred_add[intro]: "fmpred P m \<Longrightarrow> fmpred P n \<Longrightarrow> fmpred P (m ++\<^sub>f n)"
```
```   504 by transfer' (auto simp: map_pred_def map_add_def split: option.splits)
```
```   505
```
```   506 lemma fmpred_filter[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmfilter Q m)"
```
```   507 by transfer' (auto simp: map_pred_def map_filter_def)
```
```   508
```
```   509 lemma fmpred_drop[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop a m)"
```
```   510   by (auto simp: fmfilter_alt_defs)
```
```   511
```
```   512 lemma fmpred_drop_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_set A m)"
```
```   513   by (auto simp: fmfilter_alt_defs)
```
```   514
```
```   515 lemma fmpred_drop_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_fset A m)"
```
```   516   by (auto simp: fmfilter_alt_defs)
```
```   517
```
```   518 lemma fmpred_restrict_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_set A m)"
```
```   519   by (auto simp: fmfilter_alt_defs)
```
```   520
```
```   521 lemma fmpred_restrict_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_fset A m)"
```
```   522   by (auto simp: fmfilter_alt_defs)
```
```   523
```
```   524 lemma fmpred_cases[consumes 1]:
```
```   525   assumes "fmpred P m"
```
```   526   obtains (none) "fmlookup m x = None" | (some) y where "fmlookup m x = Some y" "P x y"
```
```   527 using assms by auto
```
```   528
```
```   529 lift_definition fmsubset :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool" (infix "\<subseteq>\<^sub>f" 50)
```
```   530   is map_le
```
```   531 .
```
```   532
```
```   533 lemma fmsubset_alt_def: "m \<subseteq>\<^sub>f n \<longleftrightarrow> fmpred (\<lambda>k v. fmlookup n k = Some v) m"
```
```   534 by transfer' (auto simp: map_pred_def map_le_def dom_def split: option.splits)
```
```   535
```
```   536 lemma fmsubset_pred: "fmpred P m \<Longrightarrow> n \<subseteq>\<^sub>f m \<Longrightarrow> fmpred P n"
```
```   537 unfolding fmsubset_alt_def fmpred_iff
```
```   538 by auto
```
```   539
```
```   540 lemma fmsubset_filter_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmfilter P m \<subseteq>\<^sub>f fmfilter P n"
```
```   541 unfolding fmsubset_alt_def fmpred_iff
```
```   542 by auto
```
```   543
```
```   544 lemma fmsubset_drop_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop a m \<subseteq>\<^sub>f fmdrop a n"
```
```   545 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
```
```   546
```
```   547 lemma fmsubset_drop_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_set A m \<subseteq>\<^sub>f fmdrop_set A n"
```
```   548 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
```
```   549
```
```   550 lemma fmsubset_drop_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_fset A m \<subseteq>\<^sub>f fmdrop_fset A n"
```
```   551 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
```
```   552
```
```   553 lemma fmsubset_restrict_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_set A m \<subseteq>\<^sub>f fmrestrict_set A n"
```
```   554 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
```
```   555
```
```   556 lemma fmsubset_restrict_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_fset A m \<subseteq>\<^sub>f fmrestrict_fset A n"
```
```   557 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
```
```   558
```
```   559 lift_definition fset_of_fmap :: "('a, 'b) fmap \<Rightarrow> ('a \<times> 'b) fset" is set_of_map
```
```   560 by (rule set_of_map_finite)
```
```   561
```
```   562 lemma fset_of_fmap_inj[intro, simp]: "inj fset_of_fmap"
```
```   563 apply rule
```
```   564 apply transfer'
```
```   565 using set_of_map_inj unfolding inj_def by auto
```
```   566
```
```   567 lemma fset_of_fmap_iff[simp]: "(a, b) |\<in>| fset_of_fmap m \<longleftrightarrow> fmlookup m a = Some b"
```
```   568 by transfer' (auto simp: set_of_map_def)
```
```   569
```
```   570 lemma fset_of_fmap_iff'[simp]: "(a, b) \<in> fset (fset_of_fmap m) \<longleftrightarrow> fmlookup m a = Some b"
```
```   571 by transfer' (auto simp: set_of_map_def)
```
```   572
```
```   573
```
```   574 lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
```
```   575   is map_of
```
```   576   parametric map_of_transfer
```
```   577 by (rule finite_dom_map_of)
```
```   578
```
```   579 lemma fmap_of_list_simps[simp]:
```
```   580   "fmap_of_list [] = fmempty"
```
```   581   "fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)"
```
```   582 by (transfer, simp add: map_upd_def)+
```
```   583
```
```   584 lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs"
```
```   585 by transfer' simp
```
```   586
```
```   587 lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]"
```
```   588 by transfer' (auto simp: map_upd_def)
```
```   589
```
```   590 lemma fmpred_of_list[intro]:
```
```   591   assumes "\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v"
```
```   592   shows "fmpred P (fmap_of_list xs)"
```
```   593 using assms
```
```   594 by (induction xs) (transfer'; auto simp: map_pred_def)+
```
```   595
```
```   596 lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \<Longrightarrow> (k, v) \<in> set xs"
```
```   597 by transfer' (auto dest: map_of_SomeD)
```
```   598
```
```   599 lemma fmdom_fmap_of_list[simp]: "fmdom (fmap_of_list xs) = fset_of_list (map fst xs)"
```
```   600 apply transfer'
```
```   601 apply (subst dom_map_of_conv_image_fst)
```
```   602 apply auto
```
```   603 done
```
```   604
```
```   605 lift_definition fmrel_on_fset :: "'a fset \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
```
```   606   is rel_map_on_set
```
```   607 .
```
```   608
```
```   609 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))"
```
```   610 by transfer' (auto simp: rel_map_on_set_def eq_onp_def rel_fun_def)
```
```   611
```
```   612 lemma fmrel_on_fsetI[intro]:
```
```   613   assumes "\<And>x. x |\<in>| S \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
```
```   614   shows "fmrel_on_fset S P m n"
```
```   615 using assms
```
```   616 unfolding fmrel_on_fset_alt_def by auto
```
```   617
```
```   618 lemma fmrel_on_fset_mono[mono]: "R \<le> Q \<Longrightarrow> fmrel_on_fset S R \<le> fmrel_on_fset S Q"
```
```   619 unfolding fmrel_on_fset_alt_def[abs_def]
```
```   620 apply (intro le_funI fBall_mono)
```
```   621 using option.rel_mono by auto
```
```   622
```
```   623 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)"
```
```   624 unfolding fmrel_on_fset_alt_def
```
```   625 by auto
```
```   626
```
```   627 lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \<Longrightarrow> T |\<subseteq>| S \<Longrightarrow> fmrel_on_fset T R m n"
```
```   628 unfolding fmrel_on_fset_alt_def
```
```   629 by auto
```
```   630
```
```   631 lemma fmrel_on_fset_unionI:
```
```   632   "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"
```
```   633 unfolding fmrel_on_fset_alt_def
```
```   634 by auto
```
```   635
```
```   636 lemma fmrel_on_fset_updateI:
```
```   637   assumes "fmrel_on_fset S P m n" "P v\<^sub>1 v\<^sub>2"
```
```   638   shows "fmrel_on_fset (finsert k S) P (fmupd k v\<^sub>1 m) (fmupd k v\<^sub>2 n)"
```
```   639 using assms
```
```   640 unfolding fmrel_on_fset_alt_def
```
```   641 by auto
```
```   642
```
```   643 end
```
```   644
```
```   645
```
```   646 subsection \<open>BNF setup\<close>
```
```   647
```
```   648 lift_bnf ('a, fmran': 'b) fmap [wits: Map.empty]
```
```   649   for map: fmmap
```
```   650       rel: fmrel
```
```   651   by auto
```
```   652
```
```   653 declare fmap.pred_mono[mono]
```
```   654
```
```   655 context includes lifting_syntax begin
```
```   656
```
```   657 lemma fmmap_transfer[transfer_rule]:
```
```   658   "((=) ===> pcr_fmap (=) (=) ===> pcr_fmap (=) (=)) (\<lambda>f. (\<circ>) (map_option f)) fmmap"
```
```   659   unfolding fmmap_def
```
```   660   by (rule rel_funI ext)+ (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
```
```   661
```
```   662 lemma fmran'_transfer[transfer_rule]:
```
```   663   "(pcr_fmap (=) (=) ===> (=)) (\<lambda>x. UNION (range x) set_option) fmran'"
```
```   664   unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce
```
```   665
```
```   666 lemma fmrel_transfer[transfer_rule]:
```
```   667   "((=) ===> pcr_fmap (=) (=) ===> pcr_fmap (=) (=) ===> (=)) rel_map fmrel"
```
```   668   unfolding fmrel_def fmap.pcr_cr_eq cr_fmap_def vimage2p_def by fastforce
```
```   669
```
```   670 end
```
```   671
```
```   672
```
```   673 lemma fmran'_alt_def: "fmran' m = fset (fmran m)"
```
```   674 including fset.lifting
```
```   675 by transfer' (auto simp: ran_def fun_eq_iff)
```
```   676
```
```   677 lemma fmlookup_ran'_iff: "y \<in> fmran' m \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y)"
```
```   678 by transfer' (auto simp: ran_def)
```
```   679
```
```   680 lemma fmran'I: "fmlookup m x = Some y \<Longrightarrow> y \<in> fmran' m" by (auto simp: fmlookup_ran'_iff)
```
```   681
```
```   682 lemma fmran'E[elim]:
```
```   683   assumes "y \<in> fmran' m"
```
```   684   obtains x where "fmlookup m x = Some y"
```
```   685 using assms by (auto simp: fmlookup_ran'_iff)
```
```   686
```
```   687 lemma fmrel_iff: "fmrel R m n \<longleftrightarrow> (\<forall>x. rel_option R (fmlookup m x) (fmlookup n x))"
```
```   688 by transfer' (auto simp: rel_fun_def)
```
```   689
```
```   690 lemma fmrelI[intro]:
```
```   691   assumes "\<And>x. rel_option R (fmlookup m x) (fmlookup n x)"
```
```   692   shows "fmrel R m n"
```
```   693 using assms
```
```   694 by transfer' auto
```
```   695
```
```   696 lemma fmrel_upd[intro]: "fmrel P m n \<Longrightarrow> P x y \<Longrightarrow> fmrel P (fmupd k x m) (fmupd k y n)"
```
```   697 by transfer' (auto simp: map_upd_def rel_fun_def)
```
```   698
```
```   699 lemma fmrelD[dest]: "fmrel P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
```
```   700 by transfer' (auto simp: rel_fun_def)
```
```   701
```
```   702 lemma fmrel_addI[intro]:
```
```   703   assumes "fmrel P m n" "fmrel P a b"
```
```   704   shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)"
```
```   705 using assms
```
```   706 apply transfer'
```
```   707 apply (auto simp: rel_fun_def map_add_def)
```
```   708 by (metis option.case_eq_if option.collapse option.rel_sel)
```
```   709
```
```   710 lemma fmrel_cases[consumes 1]:
```
```   711   assumes "fmrel P m n"
```
```   712   obtains (none) "fmlookup m x = None" "fmlookup n x = None"
```
```   713         | (some) a b where "fmlookup m x = Some a" "fmlookup n x = Some b" "P a b"
```
```   714 proof -
```
```   715   from assms have "rel_option P (fmlookup m x) (fmlookup n x)"
```
```   716     by auto
```
```   717   then show thesis
```
```   718     using none some
```
```   719     by (cases rule: option.rel_cases) auto
```
```   720 qed
```
```   721
```
```   722 lemma fmrel_filter[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmfilter Q m) (fmfilter Q n)"
```
```   723 unfolding fmrel_iff by auto
```
```   724
```
```   725 lemma fmrel_drop[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop a m) (fmdrop a n)"
```
```   726   unfolding fmfilter_alt_defs by blast
```
```   727
```
```   728 lemma fmrel_drop_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_set A m) (fmdrop_set A n)"
```
```   729   unfolding fmfilter_alt_defs by blast
```
```   730
```
```   731 lemma fmrel_drop_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_fset A m) (fmdrop_fset A n)"
```
```   732   unfolding fmfilter_alt_defs by blast
```
```   733
```
```   734 lemma fmrel_restrict_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_set A m) (fmrestrict_set A n)"
```
```   735   unfolding fmfilter_alt_defs by blast
```
```   736
```
```   737 lemma fmrel_restrict_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)"
```
```   738   unfolding fmfilter_alt_defs by blast
```
```   739
```
```   740 lemma fmrel_on_fset_fmrel_restrict:
```
```   741   "fmrel_on_fset S P m n \<longleftrightarrow> fmrel P (fmrestrict_fset S m) (fmrestrict_fset S n)"
```
```   742 unfolding fmrel_on_fset_alt_def fmrel_iff
```
```   743 by auto
```
```   744
```
```   745 lemma fmrel_on_fset_refl_strong:
```
```   746   assumes "\<And>x y. x |\<in>| S \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P y y"
```
```   747   shows "fmrel_on_fset S P m m"
```
```   748 unfolding fmrel_on_fset_fmrel_restrict fmrel_iff
```
```   749 using assms
```
```   750 by (simp add: option.rel_sel)
```
```   751
```
```   752 lemma fmrel_on_fset_addI:
```
```   753   assumes "fmrel_on_fset S P m n" "fmrel_on_fset S P a b"
```
```   754   shows "fmrel_on_fset S P (m ++\<^sub>f a) (n ++\<^sub>f b)"
```
```   755 using assms
```
```   756 unfolding fmrel_on_fset_fmrel_restrict
```
```   757 by auto
```
```   758
```
```   759 lemma fmrel_fmdom_eq:
```
```   760   assumes "fmrel P x y"
```
```   761   shows "fmdom x = fmdom y"
```
```   762 proof -
```
```   763   have "a |\<in>| fmdom x \<longleftrightarrow> a |\<in>| fmdom y" for a
```
```   764     proof -
```
```   765       have "rel_option P (fmlookup x a) (fmlookup y a)"
```
```   766         using assms by (simp add: fmrel_iff)
```
```   767       thus ?thesis
```
```   768         by cases (auto intro: fmdomI)
```
```   769     qed
```
```   770   thus ?thesis
```
```   771     by auto
```
```   772 qed
```
```   773
```
```   774 lemma fmrel_fmdom'_eq: "fmrel P x y \<Longrightarrow> fmdom' x = fmdom' y"
```
```   775 unfolding fmdom'_alt_def
```
```   776 by (metis fmrel_fmdom_eq)
```
```   777
```
```   778 lemma fmrel_rel_fmran:
```
```   779   assumes "fmrel P x y"
```
```   780   shows "rel_fset P (fmran x) (fmran y)"
```
```   781 proof -
```
```   782   {
```
```   783     fix b
```
```   784     assume "b |\<in>| fmran x"
```
```   785     then obtain a where "fmlookup x a = Some b"
```
```   786       by auto
```
```   787     moreover have "rel_option P (fmlookup x a) (fmlookup y a)"
```
```   788       using assms by auto
```
```   789     ultimately have "\<exists>b'. b' |\<in>| fmran y \<and> P b b'"
```
```   790       by (metis option_rel_Some1 fmranI)
```
```   791   }
```
```   792   moreover
```
```   793   {
```
```   794     fix b
```
```   795     assume "b |\<in>| fmran y"
```
```   796     then obtain a where "fmlookup y a = Some b"
```
```   797       by auto
```
```   798     moreover have "rel_option P (fmlookup x a) (fmlookup y a)"
```
```   799       using assms by auto
```
```   800     ultimately have "\<exists>b'. b' |\<in>| fmran x \<and> P b' b"
```
```   801       by (metis option_rel_Some2 fmranI)
```
```   802   }
```
```   803   ultimately show ?thesis
```
```   804     unfolding rel_fset_alt_def
```
```   805     by auto
```
```   806 qed
```
```   807
```
```   808 lemma fmrel_rel_fmran': "fmrel P x y \<Longrightarrow> rel_set P (fmran' x) (fmran' y)"
```
```   809 unfolding fmran'_alt_def
```
```   810 by (metis fmrel_rel_fmran rel_fset_fset)
```
```   811
```
```   812 lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\<lambda>_. P)"
```
```   813 unfolding fmap.pred_set fmran'_alt_def
```
```   814 including fset.lifting
```
```   815 apply transfer'
```
```   816 apply (rule ext)
```
```   817 apply (auto simp: map_pred_def ran_def split: option.splits dest: )
```
```   818 done
```
```   819
```
```   820 lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \<longleftrightarrow> pred_fmap f m"
```
```   821 unfolding fmap.pred_set fmap.set_map
```
```   822 by simp
```
```   823
```
```   824 lemma pred_fmapD: "pred_fmap P m \<Longrightarrow> x |\<in>| fmran m \<Longrightarrow> P x"
```
```   825 by auto
```
```   826
```
```   827 lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)"
```
```   828 by transfer' auto
```
```   829
```
```   830 lemma fmpred_map[simp]: "fmpred P (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>k v. P k (f v)) m"
```
```   831 unfolding fmpred_iff pred_fmap_def fmap.set_map
```
```   832 by auto
```
```   833
```
```   834 lemma fmpred_id[simp]: "fmpred (\<lambda>_. id) (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>_. f) m"
```
```   835 by simp
```
```   836
```
```   837 lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n"
```
```   838 by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
```
```   839
```
```   840 lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty"
```
```   841 by transfer auto
```
```   842
```
```   843 lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m"
```
```   844 including fset.lifting
```
```   845 by transfer' simp
```
```   846
```
```   847 lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m"
```
```   848 by transfer' simp
```
```   849
```
```   850 lemma fmran_fmmap[simp]: "fmran (fmmap f m) = f |`| fmran m"
```
```   851 including fset.lifting
```
```   852 by transfer' (auto simp: ran_def)
```
```   853
```
```   854 lemma fmran'_fmmap[simp]: "fmran' (fmmap f m) = f ` fmran' m"
```
```   855 by transfer' (auto simp: ran_def)
```
```   856
```
```   857 lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)"
```
```   858 by transfer' (auto simp: map_filter_def)
```
```   859
```
```   860 lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" unfolding fmfilter_alt_defs by simp
```
```   861 lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp
```
```   862 lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp
```
```   863 lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp
```
```   864 lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp
```
```   865
```
```   866 lemma fmmap_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap f m \<subseteq>\<^sub>f fmmap f n"
```
```   867 by transfer' (auto simp: map_le_def)
```
```   868
```
```   869 lemma fmmap_fset_of_fmap: "fset_of_fmap (fmmap f m) = (\<lambda>(k, v). (k, f v)) |`| fset_of_fmap m"
```
```   870 including fset.lifting
```
```   871 by transfer' (auto simp: set_of_map_def)
```
```   872
```
```   873
```
```   874 subsection \<open>@{const size} setup\<close>
```
```   875
```
```   876 definition size_fmap :: "('a \<Rightarrow> nat) \<Rightarrow> ('b \<Rightarrow> nat) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> nat" where
```
```   877 [simp]: "size_fmap f g m = size_fset (\<lambda>(a, b). f a + g b) (fset_of_fmap m)"
```
```   878
```
```   879 instantiation fmap :: (type, type) size begin
```
```   880
```
```   881 definition size_fmap where
```
```   882 size_fmap_overloaded_def: "size_fmap = Finite_Map.size_fmap (\<lambda>_. 0) (\<lambda>_. 0)"
```
```   883
```
```   884 instance ..
```
```   885
```
```   886 end
```
```   887
```
```   888 lemma size_fmap_overloaded_simps[simp]: "size x = size (fset_of_fmap x)"
```
```   889 unfolding size_fmap_overloaded_def
```
```   890 by simp
```
```   891
```
```   892 lemma fmap_size_o_map: "inj h \<Longrightarrow> size_fmap f g \<circ> fmmap h = size_fmap f (g \<circ> h)"
```
```   893   unfolding size_fmap_def
```
```   894   apply (auto simp: fun_eq_iff fmmap_fset_of_fmap)
```
```   895   apply (subst sum.reindex)
```
```   896   subgoal for m
```
```   897     using prod.inj_map[unfolded map_prod_def, of "\<lambda>x. x" h]
```
```   898     unfolding inj_on_def
```
```   899     by auto
```
```   900   subgoal
```
```   901     by (rule sum.cong) (auto split: prod.splits)
```
```   902   done
```
```   903
```
```   904 setup \<open>
```
```   905 BNF_LFP_Size.register_size_global @{type_name fmap} @{const_name size_fmap}
```
```   906   @{thm size_fmap_overloaded_def} @{thms size_fmap_def size_fmap_overloaded_simps}
```
```   907   @{thms fmap_size_o_map}
```
```   908 \<close>
```
```   909
```
```   910
```
```   911 subsection \<open>Additional operations\<close>
```
```   912
```
```   913 lift_definition fmmap_keys :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap" is
```
```   914   "\<lambda>f m a. map_option (f a) (m a)"
```
```   915 unfolding dom_def
```
```   916 by simp
```
```   917
```
```   918 lemma fmpred_fmmap_keys[simp]: "fmpred P (fmmap_keys f m) = fmpred (\<lambda>a b. P a (f a b)) m"
```
```   919 by transfer' (auto simp: map_pred_def split: option.splits)
```
```   920
```
```   921 lemma fmdom_fmmap_keys[simp]: "fmdom (fmmap_keys f m) = fmdom m"
```
```   922 including fset.lifting
```
```   923 by transfer' auto
```
```   924
```
```   925 lemma fmlookup_fmmap_keys[simp]: "fmlookup (fmmap_keys f m) x = map_option (f x) (fmlookup m x)"
```
```   926 by transfer' simp
```
```   927
```
```   928 lemma fmfilter_fmmap_keys[simp]: "fmfilter P (fmmap_keys f m) = fmmap_keys f (fmfilter P m)"
```
```   929 by transfer' (auto simp: map_filter_def)
```
```   930
```
```   931 lemma fmdrop_fmmap_keys[simp]: "fmdrop a (fmmap_keys f m) = fmmap_keys f (fmdrop a m)"
```
```   932 unfolding fmfilter_alt_defs by simp
```
```   933
```
```   934 lemma fmdrop_set_fmmap_keys[simp]: "fmdrop_set A (fmmap_keys f m) = fmmap_keys f (fmdrop_set A m)"
```
```   935 unfolding fmfilter_alt_defs by simp
```
```   936
```
```   937 lemma fmdrop_fset_fmmap_keys[simp]: "fmdrop_fset A (fmmap_keys f m) = fmmap_keys f (fmdrop_fset A m)"
```
```   938 unfolding fmfilter_alt_defs by simp
```
```   939
```
```   940 lemma fmrestrict_set_fmmap_keys[simp]: "fmrestrict_set A (fmmap_keys f m) = fmmap_keys f (fmrestrict_set A m)"
```
```   941 unfolding fmfilter_alt_defs by simp
```
```   942
```
```   943 lemma fmrestrict_fset_fmmap_keys[simp]: "fmrestrict_fset A (fmmap_keys f m) = fmmap_keys f (fmrestrict_fset A m)"
```
```   944 unfolding fmfilter_alt_defs by simp
```
```   945
```
```   946 lemma fmmap_keys_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap_keys f m \<subseteq>\<^sub>f fmmap_keys f n"
```
```   947 by transfer' (auto simp: map_le_def dom_def)
```
```   948
```
```   949 definition sorted_list_of_fmap :: "('a::linorder, 'b) fmap \<Rightarrow> ('a \<times> 'b) list" where
```
```   950 "sorted_list_of_fmap m = map (\<lambda>k. (k, the (fmlookup m k))) (sorted_list_of_fset (fmdom m))"
```
```   951
```
```   952 lemma list_all_sorted_list[simp]: "list_all P (sorted_list_of_fmap m) = fmpred (curry P) m"
```
```   953 unfolding sorted_list_of_fmap_def curry_def list.pred_map
```
```   954 apply (auto simp: list_all_iff)
```
```   955 including fmap.lifting fset.lifting
```
```   956 by (transfer; auto simp: dom_def map_pred_def split: option.splits)+
```
```   957
```
```   958 lemma map_of_sorted_list[simp]: "map_of (sorted_list_of_fmap m) = fmlookup m"
```
```   959 unfolding sorted_list_of_fmap_def
```
```   960 including fmap.lifting fset.lifting
```
```   961 by transfer (simp add: map_of_map_keys)
```
```   962
```
```   963
```
```   964 subsection \<open>Lifting/transfer setup\<close>
```
```   965
```
```   966 context includes lifting_syntax begin
```
```   967
```
```   968 lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty"
```
```   969 by transfer auto
```
```   970
```
```   971 lemma fmadd_transfer[transfer_rule]:
```
```   972   "(fmrel P ===> fmrel P ===> fmrel P) fmadd fmadd"
```
```   973   by (intro fmrel_addI rel_funI)
```
```   974
```
```   975 lemma fmupd_transfer[transfer_rule]:
```
```   976   "((=) ===> P ===> fmrel P ===> fmrel P) fmupd fmupd"
```
```   977   by auto
```
```   978
```
```   979 end
```
```   980
```
```   981
```
```   982 subsection \<open>View as datatype\<close>
```
```   983
```
```   984 lemma fmap_distinct[simp]:
```
```   985   "fmempty \<noteq> fmupd k v m"
```
```   986   "fmupd k v m \<noteq> fmempty"
```
```   987 by (transfer'; auto simp: map_upd_def fun_eq_iff)+
```
```   988
```
```   989 lifting_update fmap.lifting
```
```   990
```
```   991 lemma fmap_exhaust[case_names fmempty fmupd, cases type: fmap]:
```
```   992   assumes fmempty: "m = fmempty \<Longrightarrow> P"
```
```   993   assumes fmupd: "\<And>x y m'. m = fmupd x y m' \<Longrightarrow> x |\<notin>| fmdom m' \<Longrightarrow> P"
```
```   994   shows "P"
```
```   995 using assms including fmap.lifting fset.lifting
```
```   996 proof transfer
```
```   997   fix m P
```
```   998   assume "finite (dom m)"
```
```   999   assume empty: P if "m = Map.empty"
```
```  1000   assume map_upd: P if "finite (dom m')" "m = map_upd x y m'" "x \<notin> dom m'" for x y m'
```
```  1001
```
```  1002   show P
```
```  1003     proof (cases "m = Map.empty")
```
```  1004       case True thus ?thesis using empty by simp
```
```  1005     next
```
```  1006       case False
```
```  1007       hence "dom m \<noteq> {}" by simp
```
```  1008       then obtain x where "x \<in> dom m" by blast
```
```  1009
```
```  1010       let ?m' = "map_drop x m"
```
```  1011
```
```  1012       show ?thesis
```
```  1013         proof (rule map_upd)
```
```  1014           show "finite (dom ?m')"
```
```  1015             using \<open>finite (dom m)\<close>
```
```  1016             unfolding map_drop_def
```
```  1017             by auto
```
```  1018         next
```
```  1019           show "m = map_upd x (the (m x)) ?m'"
```
```  1020             using \<open>x \<in> dom m\<close> unfolding map_drop_def map_filter_def map_upd_def
```
```  1021             by auto
```
```  1022         next
```
```  1023           show "x \<notin> dom ?m'"
```
```  1024             unfolding map_drop_def map_filter_def
```
```  1025             by auto
```
```  1026         qed
```
```  1027     qed
```
```  1028 qed
```
```  1029
```
```  1030 lemma fmap_induct[case_names fmempty fmupd, induct type: fmap]:
```
```  1031   assumes "P fmempty"
```
```  1032   assumes "(\<And>x y m. P m \<Longrightarrow> fmlookup m x = None \<Longrightarrow> P (fmupd x y m))"
```
```  1033   shows "P m"
```
```  1034 proof (induction "fmdom m" arbitrary: m rule: fset_induct_stronger)
```
```  1035   case empty
```
```  1036   hence "m = fmempty"
```
```  1037     by (metis fmrestrict_fset_dom fmrestrict_fset_null)
```
```  1038   with assms show ?case
```
```  1039     by simp
```
```  1040 next
```
```  1041   case (insert x S)
```
```  1042   hence "S = fmdom (fmdrop x m)"
```
```  1043     by auto
```
```  1044   with insert have "P (fmdrop x m)"
```
```  1045     by auto
```
```  1046
```
```  1047   have "x |\<in>| fmdom m"
```
```  1048     using insert by auto
```
```  1049   then obtain y where "fmlookup m x = Some y"
```
```  1050     by auto
```
```  1051   hence "m = fmupd x y (fmdrop x m)"
```
```  1052     by (auto intro: fmap_ext)
```
```  1053
```
```  1054   show ?case
```
```  1055     apply (subst \<open>m = _\<close>)
```
```  1056     apply (rule assms)
```
```  1057     apply fact
```
```  1058     apply simp
```
```  1059     done
```
```  1060 qed
```
```  1061
```
```  1062
```
```  1063 subsection \<open>Code setup\<close>
```
```  1064
```
```  1065 instantiation fmap :: (type, equal) equal begin
```
```  1066
```
```  1067 definition "equal_fmap \<equiv> fmrel HOL.equal"
```
```  1068
```
```  1069 instance proof
```
```  1070   fix m n :: "('a, 'b) fmap"
```
```  1071   have "fmrel (=) m n \<longleftrightarrow> (m = n)"
```
```  1072     by transfer' (simp add: option.rel_eq rel_fun_eq)
```
```  1073   then show "equal_class.equal m n \<longleftrightarrow> (m = n)"
```
```  1074     unfolding equal_fmap_def
```
```  1075     by (simp add: equal_eq[abs_def])
```
```  1076 qed
```
```  1077
```
```  1078 end
```
```  1079
```
```  1080 lemma fBall_alt_def: "fBall S P \<longleftrightarrow> (\<forall>x. x |\<in>| S \<longrightarrow> P x)"
```
```  1081 by force
```
```  1082
```
```  1083 lemma fmrel_code:
```
```  1084   "fmrel R m n \<longleftrightarrow>
```
```  1085     fBall (fmdom m) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x)) \<and>
```
```  1086     fBall (fmdom n) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x))"
```
```  1087 unfolding fmrel_iff fmlookup_dom_iff fBall_alt_def
```
```  1088 by (metis option.collapse option.rel_sel)
```
```  1089
```
```  1090 lemmas [code] =
```
```  1091   fmrel_code
```
```  1092   fmran'_alt_def
```
```  1093   fmdom'_alt_def
```
```  1094   fmfilter_alt_defs
```
```  1095   pred_fmap_fmpred
```
```  1096   fmsubset_alt_def
```
```  1097   fmupd_alt_def
```
```  1098   fmrel_on_fset_alt_def
```
```  1099   fmpred_alt_def
```
```  1100
```
```  1101
```
```  1102 code_datatype fmap_of_list
```
```  1103 quickcheck_generator fmap constructors: fmap_of_list
```
```  1104
```
```  1105 context includes fset.lifting begin
```
```  1106
```
```  1107 lemma fmlookup_of_list[code]: "fmlookup (fmap_of_list m) = map_of m"
```
```  1108 by transfer simp
```
```  1109
```
```  1110 lemma fmempty_of_list[code]: "fmempty = fmap_of_list []"
```
```  1111 by transfer simp
```
```  1112
```
```  1113 lemma fmran_of_list[code]: "fmran (fmap_of_list m) = snd |`| fset_of_list (AList.clearjunk m)"
```
```  1114 by transfer (auto simp: ran_map_of)
```
```  1115
```
```  1116 lemma fmdom_of_list[code]: "fmdom (fmap_of_list m) = fst |`| fset_of_list m"
```
```  1117 by transfer (auto simp: dom_map_of_conv_image_fst)
```
```  1118
```
```  1119 lemma fmfilter_of_list[code]: "fmfilter P (fmap_of_list m) = fmap_of_list (filter (\<lambda>(k, _). P k) m)"
```
```  1120 by transfer' auto
```
```  1121
```
```  1122 lemma fmadd_of_list[code]: "fmap_of_list m ++\<^sub>f fmap_of_list n = fmap_of_list (AList.merge m n)"
```
```  1123 by transfer (simp add: merge_conv')
```
```  1124
```
```  1125 lemma fmmap_of_list[code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)"
```
```  1126 apply transfer
```
```  1127 apply (subst map_of_map[symmetric])
```
```  1128 apply (auto simp: apsnd_def map_prod_def)
```
```  1129 done
```
```  1130
```
```  1131 lemma fmmap_keys_of_list[code]: "fmmap_keys f (fmap_of_list m) = fmap_of_list (map (\<lambda>(a, b). (a, f a b)) m)"
```
```  1132 apply transfer
```
```  1133 subgoal for f m by (induction m) (auto simp: apsnd_def map_prod_def fun_eq_iff)
```
```  1134 done
```
```  1135
```
```  1136 end
```
```  1137
```
```  1138
```
```  1139 subsection \<open>Instances\<close>
```
```  1140
```
```  1141 lemma exists_map_of:
```
```  1142   assumes "finite (dom m)" shows "\<exists>xs. map_of xs = m"
```
```  1143   using assms
```
```  1144 proof (induction "dom m" arbitrary: m)
```
```  1145   case empty
```
```  1146   hence "m = Map.empty"
```
```  1147     by auto
```
```  1148   moreover have "map_of [] = Map.empty"
```
```  1149     by simp
```
```  1150   ultimately show ?case
```
```  1151     by blast
```
```  1152 next
```
```  1153   case (insert x F)
```
```  1154   hence "F = dom (map_drop x m)"
```
```  1155     unfolding map_drop_def map_filter_def dom_def by auto
```
```  1156   with insert have "\<exists>xs'. map_of xs' = map_drop x m"
```
```  1157     by auto
```
```  1158   then obtain xs' where "map_of xs' = map_drop x m"
```
```  1159     ..
```
```  1160   moreover obtain y where "m x = Some y"
```
```  1161     using insert unfolding dom_def by blast
```
```  1162   ultimately have "map_of ((x, y) # xs') = m"
```
```  1163     using \<open>insert x F = dom m\<close>
```
```  1164     unfolding map_drop_def map_filter_def
```
```  1165     by auto
```
```  1166   thus ?case
```
```  1167     ..
```
```  1168 qed
```
```  1169
```
```  1170 lemma exists_fmap_of_list: "\<exists>xs. fmap_of_list xs = m"
```
```  1171 by transfer (rule exists_map_of)
```
```  1172
```
```  1173 lemma fmap_of_list_surj[simp, intro]: "surj fmap_of_list"
```
```  1174 proof -
```
```  1175   have "x \<in> range fmap_of_list" for x :: "('a, 'b) fmap"
```
```  1176     unfolding image_iff
```
```  1177     using exists_fmap_of_list by (metis UNIV_I)
```
```  1178   thus ?thesis by auto
```
```  1179 qed
```
```  1180
```
```  1181 instance fmap :: (countable, countable) countable
```
```  1182 proof
```
```  1183   obtain to_nat :: "('a \<times> 'b) list \<Rightarrow> nat" where "inj to_nat"
```
```  1184     by (metis ex_inj)
```
```  1185   moreover have "inj (inv fmap_of_list)"
```
```  1186     using fmap_of_list_surj by (rule surj_imp_inj_inv)
```
```  1187   ultimately have "inj (to_nat \<circ> inv fmap_of_list)"
```
```  1188     by (rule inj_comp)
```
```  1189   thus "\<exists>to_nat::('a, 'b) fmap \<Rightarrow> nat. inj to_nat"
```
```  1190     by auto
```
```  1191 qed
```
```  1192
```
```  1193 instance fmap :: (finite, finite) finite
```
```  1194 proof
```
```  1195   show "finite (UNIV :: ('a, 'b) fmap set)"
```
```  1196     by (rule finite_imageD) auto
```
```  1197 qed
```
```  1198
```
```  1199 lifting_update fmap.lifting
```
```  1200 lifting_forget fmap.lifting
```
```  1201
```
`  1202 end`