src/HOL/Library/Finite_Map.thy
 author Lars Hupel Thu Oct 13 14:15:34 2016 +0200 (2016-10-13) changeset 64179 ce205d1f8592 parent 63900 2359e9952641 child 64180 676763a9c269 permissions -rw-r--r--
remove accidentally oops'ed (and wrong) lemma
```     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
```
```     9 begin
```
```    10
```
```    11 subsection \<open>Auxiliary constants and lemmas over @{type map}\<close>
```
```    12
```
```    13 context includes lifting_syntax begin
```
```    14
```
```    15 abbreviation rel_map :: "('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c) \<Rightarrow> bool" where
```
```    16 "rel_map f \<equiv> op = ===> rel_option f"
```
```    17
```
```    18 lemma map_empty_transfer[transfer_rule]: "rel_map A Map.empty Map.empty"
```
```    19 by transfer_prover
```
```    20
```
```    21 lemma ran_transfer[transfer_rule]: "(rel_map A ===> rel_set A) ran ran"
```
```    22 proof
```
```    23   fix m n
```
```    24   assume "rel_map A m n"
```
```    25   show "rel_set A (ran m) (ran n)"
```
```    26     proof (rule rel_setI)
```
```    27       fix x
```
```    28       assume "x \<in> ran m"
```
```    29       then obtain a where "m a = Some x"
```
```    30         unfolding ran_def by auto
```
```    31
```
```    32       have "rel_option A (m a) (n a)"
```
```    33         using \<open>rel_map A m n\<close>
```
```    34         by (auto dest: rel_funD)
```
```    35       then obtain y where "n a = Some y" "A x y"
```
```    36         unfolding \<open>m a = _\<close>
```
```    37         by cases auto
```
```    38       thus "\<exists>y \<in> ran n. A x y"
```
```    39         unfolding ran_def by blast
```
```    40     next
```
```    41       fix y
```
```    42       assume "y \<in> ran n"
```
```    43       then obtain a where "n a = Some y"
```
```    44         unfolding ran_def by auto
```
```    45
```
```    46       have "rel_option A (m a) (n a)"
```
```    47         using \<open>rel_map A m n\<close>
```
```    48         by (auto dest: rel_funD)
```
```    49       then obtain x where "m a = Some x" "A x y"
```
```    50         unfolding \<open>n a = _\<close>
```
```    51         by cases auto
```
```    52       thus "\<exists>x \<in> ran m. A x y"
```
```    53         unfolding ran_def by blast
```
```    54     qed
```
```    55 qed
```
```    56
```
```    57 lemma ran_alt_def: "ran m = (the \<circ> m) ` dom m"
```
```    58 unfolding ran_def dom_def by force
```
```    59
```
```    60 lemma dom_transfer[transfer_rule]: "(rel_map A ===> op =) dom dom"
```
```    61 proof
```
```    62   fix m n
```
```    63   assume "rel_map A m n"
```
```    64   have "m a \<noteq> None \<longleftrightarrow> n a \<noteq> None" for a
```
```    65     proof -
```
```    66       from \<open>rel_map A m n\<close> have "rel_option A (m a) (n a)"
```
```    67         unfolding rel_fun_def by auto
```
```    68       thus ?thesis
```
```    69         by cases auto
```
```    70     qed
```
```    71   thus "dom m = dom n"
```
```    72     by auto
```
```    73 qed
```
```    74
```
```    75 definition map_upd :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
```
```    76 "map_upd k v m = m(k \<mapsto> v)"
```
```    77
```
```    78 lemma map_upd_transfer[transfer_rule]:
```
```    79   "(op = ===> A ===> rel_map A ===> rel_map A) map_upd map_upd"
```
```    80 unfolding map_upd_def[abs_def]
```
```    81 by transfer_prover
```
```    82
```
```    83 definition map_filter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
```
```    84 "map_filter P m = (\<lambda>x. if P x then m x else None)"
```
```    85
```
```    86 lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
```
```    87 proof
```
```    88   fix x
```
```    89   show "map_filter P (map_of m) x = map_of [(k, _) \<leftarrow> m. P k] x"
```
```    90     by (induct m) (auto simp: map_filter_def)
```
```    91 qed
```
```    92
```
```    93 lemma map_filter_transfer[transfer_rule]:
```
```    94   "(op = ===> rel_map A ===> rel_map A) map_filter map_filter"
```
```    95 unfolding map_filter_def[abs_def]
```
```    96 by transfer_prover
```
```    97
```
```    98 lemma map_filter_finite[intro]:
```
```    99   assumes "finite (dom m)"
```
```   100   shows "finite (dom (map_filter P m))"
```
```   101 proof -
```
```   102   have "dom (map_filter P m) = Set.filter P (dom m)"
```
```   103     unfolding map_filter_def Set.filter_def dom_def
```
```   104     by auto
```
```   105   thus ?thesis
```
```   106     using assms
```
```   107     by (simp add: Set.filter_def)
```
```   108 qed
```
```   109
```
```   110 definition map_drop :: "'a \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
```
```   111 "map_drop a = map_filter (\<lambda>a'. a' \<noteq> a)"
```
```   112
```
```   113 lemma map_drop_transfer[transfer_rule]:
```
```   114   "(op = ===> rel_map A ===> rel_map A) map_drop map_drop"
```
```   115 unfolding map_drop_def[abs_def]
```
```   116 by transfer_prover
```
```   117
```
```   118 definition map_drop_set :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
```
```   119 "map_drop_set A = map_filter (\<lambda>a. a \<notin> A)"
```
```   120
```
```   121 lemma map_drop_set_transfer[transfer_rule]:
```
```   122   "(op = ===> rel_map A ===> rel_map A) map_drop_set map_drop_set"
```
```   123 unfolding map_drop_set_def[abs_def]
```
```   124 by transfer_prover
```
```   125
```
```   126 definition map_restrict_set :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
```
```   127 "map_restrict_set A = map_filter (\<lambda>a. a \<in> A)"
```
```   128
```
```   129 lemma map_restrict_set_transfer[transfer_rule]:
```
```   130   "(op = ===> rel_map A ===> rel_map A) map_restrict_set map_restrict_set"
```
```   131 unfolding map_restrict_set_def[abs_def]
```
```   132 by transfer_prover
```
```   133
```
```   134 lemma map_add_transfer[transfer_rule]:
```
```   135   "(rel_map A ===> rel_map A ===> rel_map A) op ++ op ++"
```
```   136 unfolding map_add_def[abs_def]
```
```   137 by transfer_prover
```
```   138
```
```   139 definition map_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" where
```
```   140 "map_pred P m \<longleftrightarrow> (\<forall>x. case m x of None \<Rightarrow> True | Some y \<Rightarrow> P x y)"
```
```   141
```
```   142 lemma map_pred_transfer[transfer_rule]:
```
```   143   "((op = ===> A ===> op =) ===> rel_map A ===> op =) map_pred map_pred"
```
```   144 unfolding map_pred_def[abs_def]
```
```   145 by transfer_prover
```
```   146
```
```   147 definition rel_map_on_set :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c) \<Rightarrow> bool" where
```
```   148 "rel_map_on_set S P = eq_onp (\<lambda>x. x \<in> S) ===> rel_option P"
```
```   149
```
```   150 lemma map_of_transfer[transfer_rule]:
```
```   151   includes lifting_syntax
```
```   152   shows "(list_all2 (rel_prod op = A) ===> rel_map A) map_of map_of"
```
```   153 unfolding map_of_def by transfer_prover
```
```   154
```
```   155 end
```
```   156
```
```   157
```
```   158 subsection \<open>Abstract characterisation\<close>
```
```   159
```
```   160 typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a \<rightharpoonup> 'b) set"
```
```   161   morphisms fmlookup Abs_fmap
```
```   162 proof
```
```   163   show "Map.empty \<in> {m. finite (dom m)}"
```
```   164     by auto
```
```   165 qed
```
```   166
```
```   167 setup_lifting type_definition_fmap
```
```   168
```
```   169 lemma fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))"
```
```   170 using fmap.fmlookup by auto
```
```   171
```
```   172 lemma fmap_ext:
```
```   173   assumes "\<And>x. fmlookup m x = fmlookup n x"
```
```   174   shows "m = n"
```
```   175 using assms
```
```   176 by transfer' auto
```
```   177
```
```   178
```
```   179 subsection \<open>Operations\<close>
```
```   180
```
```   181 context
```
```   182   includes fset.lifting
```
```   183 begin
```
```   184
```
```   185 lift_definition fmran :: "('a, 'b) fmap \<Rightarrow> 'b fset"
```
```   186   is ran
```
```   187   parametric ran_transfer
```
```   188 unfolding ran_alt_def by auto
```
```   189
```
```   190 lemma fmranI: "fmlookup m x = Some y \<Longrightarrow> y |\<in>| fmran m" by transfer' (auto simp: ran_def)
```
```   191
```
```   192 lift_definition fmdom :: "('a, 'b) fmap \<Rightarrow> 'a fset"
```
```   193   is dom
```
```   194   parametric dom_transfer
```
```   195 .
```
```   196
```
```   197 lemma fmdom_notI: "fmlookup m x = None \<Longrightarrow> x |\<notin>| fmdom m" by transfer' auto
```
```   198 lemma fmdomI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| fmdom m" by transfer' auto
```
```   199 lemma fmdom_notD: "x |\<notin>| fmdom m \<Longrightarrow> fmlookup m x = None" by transfer' auto
```
```   200
```
```   201 lift_definition fmdom' :: "('a, 'b) fmap \<Rightarrow> 'a set"
```
```   202   is dom
```
```   203   parametric dom_transfer
```
```   204 .
```
```   205
```
```   206 lemma fmdom'_notI: "fmlookup m x = None \<Longrightarrow> x \<notin> fmdom' m" by transfer' auto
```
```   207 lemma fmdom'I: "fmlookup m x = Some y \<Longrightarrow> x \<in> fmdom' m" by transfer' auto
```
```   208 lemma fmdom'_notD: "x \<notin> fmdom' m \<Longrightarrow> fmlookup m x = None" by transfer' auto
```
```   209
```
```   210 lemma fmdom'_alt_def: "fmdom' = fset \<circ> fmdom"
```
```   211 by transfer' force
```
```   212
```
```   213 lemma fmlookup_dom_iff: "x |\<in>| fmdom m \<longleftrightarrow> (\<exists>a. fmlookup m x = Some a)"
```
```   214 by transfer' auto
```
```   215
```
```   216 lift_definition fmempty :: "('a, 'b) fmap"
```
```   217   is Map.empty
```
```   218   parametric map_empty_transfer
```
```   219 by simp
```
```   220
```
```   221 lemma fmempty_lookup[simp]: "fmlookup fmempty x = None"
```
```   222 by transfer' simp
```
```   223
```
```   224 lemma fmdom_empty[simp]: "fmdom fmempty = {||}" by transfer' simp
```
```   225 lemma fmdom'_empty[simp]: "fmdom' fmempty = {}" by transfer' simp
```
```   226
```
```   227 lift_definition fmupd :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   228   is map_upd
```
```   229   parametric map_upd_transfer
```
```   230 unfolding map_upd_def[abs_def]
```
```   231 by simp
```
```   232
```
```   233 lemma fmupd_lookup[simp]: "fmlookup (fmupd a b m) a' = (if a = a' then Some b else fmlookup m a')"
```
```   234 by transfer' (auto simp: map_upd_def)
```
```   235
```
```   236 lemma fmdom_fmupd[simp]: "fmdom (fmupd a b m) = finsert a (fmdom m)" by transfer (simp add: map_upd_def)
```
```   237 lemma fmdom'_fmupd[simp]: "fmdom' (fmupd a b m) = insert a (fmdom' m)" by transfer (simp add: map_upd_def)
```
```   238
```
```   239 lift_definition fmfilter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   240   is map_filter
```
```   241   parametric map_filter_transfer
```
```   242 by auto
```
```   243
```
```   244 lemma fmdom_filter[simp]: "fmdom (fmfilter P m) = ffilter P (fmdom m)"
```
```   245 by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
```
```   246
```
```   247 lemma fmdom'_filter[simp]: "fmdom' (fmfilter P m) = Set.filter P (fmdom' m)"
```
```   248 by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
```
```   249
```
```   250 lemma fmlookup_filter[simp]: "fmlookup (fmfilter P m) x = (if P x then fmlookup m x else None)"
```
```   251 by transfer' (auto simp: map_filter_def)
```
```   252
```
```   253 lemma fmfilter_empty[simp]: "fmfilter P fmempty = fmempty"
```
```   254 by transfer' (auto simp: map_filter_def)
```
```   255
```
```   256 lemma fmfilter_true[simp]:
```
```   257   assumes "\<And>x. x |\<in>| fmdom m \<Longrightarrow> P x"
```
```   258   shows "fmfilter P m = m"
```
```   259 proof (rule fmap_ext)
```
```   260   fix x
```
```   261   have "fmlookup m x = None" if "\<not> P x"
```
```   262     using that assms
```
```   263     unfolding fmlookup_dom_iff by fastforce
```
```   264   thus "fmlookup (fmfilter P m) x = fmlookup m x"
```
```   265     by simp
```
```   266 qed
```
```   267
```
```   268 lemma fmfilter_false[simp]: "(\<And>x. x |\<in>| fmdom m \<Longrightarrow> \<not> P x) \<Longrightarrow> fmfilter P m = fmempty"
```
```   269 by transfer' (auto simp: map_filter_def fun_eq_iff)
```
```   270
```
```   271 lemma fmfilter_comp[simp]: "fmfilter P (fmfilter Q m) = fmfilter (\<lambda>x. P x \<and> Q x) m"
```
```   272 by transfer' (auto simp: map_filter_def)
```
```   273
```
```   274 lemma fmfilter_comm: "fmfilter P (fmfilter Q m) = fmfilter Q (fmfilter P m)"
```
```   275 unfolding fmfilter_comp by meson
```
```   276
```
```   277 lemma fmfilter_cong[cong]:
```
```   278   assumes "\<And>x. x |\<in>| fmdom m \<Longrightarrow> P x = Q x"
```
```   279   shows "fmfilter P m = fmfilter Q m"
```
```   280 proof (rule fmap_ext)
```
```   281   fix x
```
```   282   have "fmlookup m x = None" if "P x \<noteq> Q x"
```
```   283     using that assms
```
```   284     unfolding fmlookup_dom_iff by fastforce
```
```   285   thus "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x"
```
```   286     by auto
```
```   287 qed
```
```   288
```
```   289 lemma fmfilter_cong'[fundef_cong]:
```
```   290   assumes "\<And>x. x \<in> fmdom' m \<Longrightarrow> P x = Q x"
```
```   291   shows "fmfilter P m = fmfilter Q m"
```
```   292 proof (rule fmfilter_cong)
```
```   293   fix x
```
```   294   assume "x |\<in>| fmdom m"
```
```   295   thus "P x = Q x"
```
```   296     using assms
```
```   297     unfolding fmdom'_alt_def fmember.rep_eq
```
```   298     by auto
```
```   299 qed
```
```   300
```
```   301 lemma fmfilter_upd[simp]:
```
```   302   "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)"
```
```   303 by transfer' (auto simp: map_upd_def map_filter_def)
```
```   304
```
```   305 lift_definition fmdrop :: "'a \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   306   is map_drop
```
```   307   parametric map_drop_transfer
```
```   308 unfolding map_drop_def by auto
```
```   309
```
```   310 lemma fmdrop_lookup[simp]: "fmlookup (fmdrop a m) a = None"
```
```   311 by transfer' (auto simp: map_drop_def map_filter_def)
```
```   312
```
```   313 lift_definition fmdrop_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   314   is map_drop_set
```
```   315   parametric map_drop_set_transfer
```
```   316 unfolding map_drop_set_def by auto
```
```   317
```
```   318 lift_definition fmdrop_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   319   is map_drop_set
```
```   320   parametric map_drop_set_transfer
```
```   321 unfolding map_drop_set_def by auto
```
```   322
```
```   323 lift_definition fmrestrict_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   324   is map_restrict_set
```
```   325   parametric map_restrict_set_transfer
```
```   326 unfolding map_restrict_set_def by auto
```
```   327
```
```   328 lift_definition fmrestrict_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
```
```   329   is map_restrict_set
```
```   330   parametric map_restrict_set_transfer
```
```   331 unfolding map_restrict_set_def by auto
```
```   332
```
```   333 lemma fmfilter_alt_defs:
```
```   334   "fmdrop a = fmfilter (\<lambda>a'. a' \<noteq> a)"
```
```   335   "fmdrop_set A = fmfilter (\<lambda>a. a \<notin> A)"
```
```   336   "fmdrop_fset B = fmfilter (\<lambda>a. a |\<notin>| B)"
```
```   337   "fmrestrict_set A = fmfilter (\<lambda>a. a \<in> A)"
```
```   338   "fmrestrict_fset B = fmfilter (\<lambda>a. a |\<in>| B)"
```
```   339 by (transfer'; simp add: map_drop_def map_drop_set_def map_restrict_set_def)+
```
```   340
```
```   341 lemma fmdom_drop[simp]: "fmdom (fmdrop a m) = fmdom m - {|a|}" unfolding fmfilter_alt_defs by auto
```
```   342 lemma fmdom'_drop[simp]: "fmdom' (fmdrop a m) = fmdom' m - {a}" unfolding fmfilter_alt_defs by auto
```
```   343 lemma fmdom'_drop_set[simp]: "fmdom' (fmdrop_set A m) = fmdom' m - A" unfolding fmfilter_alt_defs by auto
```
```   344 lemma fmdom_drop_fset[simp]: "fmdom (fmdrop_fset A m) = fmdom m - A" unfolding fmfilter_alt_defs by auto
```
```   345 lemma fmdom'_restrict_set: "fmdom' (fmrestrict_set A m) \<subseteq> A" unfolding fmfilter_alt_defs by auto
```
```   346 lemma fmdom_restrict_fset: "fmdom (fmrestrict_fset A m) |\<subseteq>| A" unfolding fmfilter_alt_defs by auto
```
```   347
```
```   348 lemma fmdom'_drop_fset[simp]: "fmdom' (fmdrop_fset A m) = fmdom' m - fset A"
```
```   349 unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def split: if_splits)
```
```   350
```
```   351 lemma fmdom'_restrict_fset: "fmdom' (fmrestrict_fset A m) \<subseteq> fset A"
```
```   352 unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def)
```
```   353
```
```   354 lemma fmlookup_drop[simp]:
```
```   355   "fmlookup (fmdrop a m) x = (if x \<noteq> a then fmlookup m x else None)"
```
```   356 unfolding fmfilter_alt_defs by simp
```
```   357
```
```   358 lemma fmlookup_drop_set[simp]:
```
```   359   "fmlookup (fmdrop_set A m) x = (if x \<notin> A then fmlookup m x else None)"
```
```   360 unfolding fmfilter_alt_defs by simp
```
```   361
```
```   362 lemma fmlookup_drop_fset[simp]:
```
```   363   "fmlookup (fmdrop_fset A m) x = (if x |\<notin>| A then fmlookup m x else None)"
```
```   364 unfolding fmfilter_alt_defs by simp
```
```   365
```
```   366 lemma fmlookup_restrict_set[simp]:
```
```   367   "fmlookup (fmrestrict_set A m) x = (if x \<in> A then fmlookup m x else None)"
```
```   368 unfolding fmfilter_alt_defs by simp
```
```   369
```
```   370 lemma fmlookup_restrict_fset[simp]:
```
```   371   "fmlookup (fmrestrict_fset A m) x = (if x |\<in>| A then fmlookup m x else None)"
```
```   372 unfolding fmfilter_alt_defs by simp
```
```   373
```
```   374 lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m"
```
```   375   by (rule fmap_ext) (auto dest: fmdom'_notD)
```
```   376
```
```   377 lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m"
```
```   378   by (rule fmap_ext) (auto dest: fmdom_notD)
```
```   379
```
```   380 lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty"
```
```   381   unfolding fmfilter_alt_defs by simp
```
```   382
```
```   383 lemma fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty"
```
```   384   unfolding fmfilter_alt_defs by simp
```
```   385
```
```   386 lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty"
```
```   387   unfolding fmfilter_alt_defs by simp
```
```   388
```
```   389 lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty"
```
```   390   unfolding fmfilter_alt_defs by simp
```
```   391
```
```   392 lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty"
```
```   393   unfolding fmfilter_alt_defs by simp
```
```   394
```
```   395 lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m"
```
```   396   unfolding fmfilter_alt_defs by simp
```
```   397
```
```   398 lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m"
```
```   399   unfolding fmfilter_alt_defs by simp
```
```   400
```
```   401 lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty"
```
```   402   unfolding fmfilter_alt_defs by simp
```
```   403
```
```   404 lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty"
```
```   405   unfolding fmfilter_alt_defs by simp
```
```   406
```
```   407 lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)"
```
```   408 unfolding fmfilter_alt_defs by (rule fmfilter_comm)
```
```   409
```
```   410 lift_definition fmadd :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap" (infixl "++\<^sub>f" 100)
```
```   411   is map_add
```
```   412   parametric map_add_transfer
```
```   413 by simp
```
```   414
```
```   415 lemma fmlookup_add[simp]:
```
```   416   "fmlookup (m ++\<^sub>f n) x = (if x |\<in>| fmdom n then fmlookup n x else fmlookup m x)"
```
```   417   by transfer' (auto simp: map_add_def split: option.splits)
```
```   418
```
```   419 lemma fmdom_add[simp]: "fmdom (m ++\<^sub>f n) = fmdom m |\<union>| fmdom n" by transfer' auto
```
```   420 lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \<union> fmdom' n" by transfer' auto
```
```   421
```
```   422 lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
```
```   423   by (rule fmap_ext) auto
```
```   424
```
```   425 lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
```
```   426   by (rule fmap_ext) (auto dest: fmdom_notD)
```
```   427
```
```   428 lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n"
```
```   429 by transfer' (auto simp: map_filter_def map_add_def)
```
```   430
```
```   431 lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n"
```
```   432   unfolding fmfilter_alt_defs by simp
```
```   433
```
```   434 lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n"
```
```   435   unfolding fmfilter_alt_defs by simp
```
```   436
```
```   437 lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n"
```
```   438   unfolding fmfilter_alt_defs by simp
```
```   439
```
```   440 lemma fmrestrict_set_add_distrib[simp]:
```
```   441   "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n"
```
```   442   unfolding fmfilter_alt_defs by simp
```
```   443
```
```   444 lemma fmrestrict_fset_add_distrib[simp]:
```
```   445   "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n"
```
```   446   unfolding fmfilter_alt_defs by simp
```
```   447
```
```   448 lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m"
```
```   449 by (transfer'; auto)+
```
```   450
```
```   451 lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m"
```
```   452 by transfer' (auto simp: map_add_def split: option.splits)
```
```   453
```
```   454 lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p"
```
```   455 by transfer' simp
```
```   456
```
```   457 lift_definition fmpred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool"
```
```   458   is map_pred
```
```   459   parametric map_pred_transfer
```
```   460 .
```
```   461
```
```   462 lemma fmpredI[intro]:
```
```   463   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y"
```
```   464   shows "fmpred P m"
```
```   465 using assms
```
```   466 by transfer' (auto simp: map_pred_def split: option.splits)
```
```   467
```
```   468 lemma fmpredD[dest]: "fmpred P m \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P x y"
```
```   469 by transfer' (auto simp: map_pred_def split: option.split_asm)
```
```   470
```
```   471 lemma fmpred_iff: "fmpred P m \<longleftrightarrow> (\<forall>x y. fmlookup m x = Some y \<longrightarrow> P x y)"
```
```   472 by auto
```
```   473
```
```   474 lemma fmpred_alt_def: "fmpred P m \<longleftrightarrow> fBall (fmdom m) (\<lambda>x. P x (the (fmlookup m x)))"
```
```   475 unfolding fmpred_iff
```
```   476 apply auto
```
```   477 apply (subst (asm) fmlookup_dom_iff)
```
```   478 apply simp
```
```   479 apply (rename_tac x y)
```
```   480 apply (erule_tac x = x in fBallE)
```
```   481 apply simp
```
```   482 by (simp add: fmlookup_dom_iff)
```
```   483
```
```   484 lemma fmpred_empty[intro!, simp]: "fmpred P fmempty"
```
```   485 by auto
```
```   486
```
```   487 lemma fmpred_upd[intro]: "fmpred P m \<Longrightarrow> P x y \<Longrightarrow> fmpred P (fmupd x y m)"
```
```   488 by transfer' (auto simp: map_pred_def map_upd_def)
```
```   489
```
```   490 lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \<Longrightarrow> P x y"
```
```   491 by auto
```
```   492
```
```   493 lemma fmpred_add[intro]: "fmpred P m \<Longrightarrow> fmpred P n \<Longrightarrow> fmpred P (m ++\<^sub>f n)"
```
```   494 by transfer' (auto simp: map_pred_def map_add_def split: option.splits)
```
```   495
```
```   496 lemma fmpred_filter[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmfilter Q m)"
```
```   497 by transfer' (auto simp: map_pred_def map_filter_def)
```
```   498
```
```   499 lemma fmpred_drop[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop a m)"
```
```   500   by (auto simp: fmfilter_alt_defs)
```
```   501
```
```   502 lemma fmpred_drop_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_set A m)"
```
```   503   by (auto simp: fmfilter_alt_defs)
```
```   504
```
```   505 lemma fmpred_drop_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_fset A m)"
```
```   506   by (auto simp: fmfilter_alt_defs)
```
```   507
```
```   508 lemma fmpred_restrict_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_set A m)"
```
```   509   by (auto simp: fmfilter_alt_defs)
```
```   510
```
```   511 lemma fmpred_restrict_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_fset A m)"
```
```   512   by (auto simp: fmfilter_alt_defs)
```
```   513
```
```   514 lemma fmpred_cases[consumes 1]:
```
```   515   assumes "fmpred P m"
```
```   516   obtains (none) "fmlookup m x = None" | (some) y where "fmlookup m x = Some y" "P x y"
```
```   517 using assms by auto
```
```   518
```
```   519 lift_definition fmsubset :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool" (infix "\<subseteq>\<^sub>f" 50)
```
```   520   is map_le
```
```   521 .
```
```   522
```
```   523 lemma fmsubset_alt_def: "m \<subseteq>\<^sub>f n \<longleftrightarrow> fmpred (\<lambda>k v. fmlookup n k = Some v) m"
```
```   524 by transfer' (auto simp: map_pred_def map_le_def dom_def split: option.splits)
```
```   525
```
```   526 lemma fmsubset_pred: "fmpred P m \<Longrightarrow> n \<subseteq>\<^sub>f m \<Longrightarrow> fmpred P n"
```
```   527 unfolding fmsubset_alt_def fmpred_iff
```
```   528 by auto
```
```   529
```
```   530 lemma fmsubset_filter_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmfilter P m \<subseteq>\<^sub>f fmfilter P n"
```
```   531 unfolding fmsubset_alt_def fmpred_iff
```
```   532 by auto
```
```   533
```
```   534 lemma fmsubset_drop_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop a m \<subseteq>\<^sub>f fmdrop a n"
```
```   535 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
```
```   536
```
```   537 lemma fmsubset_drop_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_set A m \<subseteq>\<^sub>f fmdrop_set A n"
```
```   538 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
```
```   539
```
```   540 lemma fmsubset_drop_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_fset A m \<subseteq>\<^sub>f fmdrop_fset A n"
```
```   541 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
```
```   542
```
```   543 lemma fmsubset_restrict_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_set A m \<subseteq>\<^sub>f fmrestrict_set A n"
```
```   544 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
```
```   545
```
```   546 lemma fmsubset_restrict_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_fset A m \<subseteq>\<^sub>f fmrestrict_fset A n"
```
```   547 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
```
```   548
```
```   549 lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
```
```   550   is map_of
```
```   551   parametric map_of_transfer
```
```   552 by (rule finite_dom_map_of)
```
```   553
```
```   554 lemma fmap_of_list_simps[simp]:
```
```   555   "fmap_of_list [] = fmempty"
```
```   556   "fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)"
```
```   557 by (transfer, simp add: map_upd_def)+
```
```   558
```
```   559 lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs"
```
```   560 by transfer' simp
```
```   561
```
```   562 lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]"
```
```   563 by transfer' (auto simp: map_upd_def)
```
```   564
```
```   565 lemma fmpred_of_list[intro]:
```
```   566   assumes "\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v"
```
```   567   shows "fmpred P (fmap_of_list xs)"
```
```   568 using assms
```
```   569 by (induction xs) (transfer'; auto simp: map_pred_def)+
```
```   570
```
```   571 lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \<Longrightarrow> (k, v) \<in> set xs"
```
```   572 by transfer' (auto dest: map_of_SomeD)
```
```   573
```
```   574 lift_definition fmrel_on_set :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
```
```   575   is rel_map_on_set
```
```   576 .
```
```   577
```
```   578 lift_definition fmrel_on_fset :: "'a fset \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
```
```   579   is rel_map_on_set
```
```   580 .
```
```   581
```
```   582 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))"
```
```   583 by transfer' (auto simp: rel_map_on_set_def eq_onp_def rel_fun_def)
```
```   584
```
```   585 lemma rel_map_on_fsetI[intro]:
```
```   586   assumes "\<And>x. x |\<in>| S \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
```
```   587   shows "fmrel_on_fset S P m n"
```
```   588 using assms
```
```   589 unfolding fmrel_on_fset_alt_def by auto
```
```   590
```
```   591 lemma fmrel_on_fset_mono[mono]: "R \<le> Q \<Longrightarrow> fmrel_on_fset S R \<le> fmrel_on_fset S Q"
```
```   592 unfolding fmrel_on_fset_alt_def[abs_def]
```
```   593 apply (intro le_funI fBall_mono)
```
```   594 using option.rel_mono by auto
```
```   595
```
```   596 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)"
```
```   597 unfolding fmrel_on_fset_alt_def
```
```   598 by auto
```
```   599
```
```   600 lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \<Longrightarrow> T |\<subseteq>| S \<Longrightarrow> fmrel_on_fset T R m n"
```
```   601 unfolding fmrel_on_fset_alt_def
```
```   602 by auto
```
```   603
```
```   604 end
```
```   605
```
```   606
```
```   607 subsection \<open>BNF setup\<close>
```
```   608
```
```   609 lift_bnf ('a, fmran': 'b) fmap [wits: Map.empty]
```
```   610   for map: fmmap
```
```   611       rel: fmrel
```
```   612   by auto
```
```   613
```
```   614 context includes lifting_syntax begin
```
```   615
```
```   616 lemma fmmap_transfer[transfer_rule]:
```
```   617   "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op =) (\<lambda>f. op \<circ> (map_option f)) fmmap"
```
```   618 apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\<close>)
```
```   619 apply (rule rel_funI ext)+
```
```   620 apply (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
```
```   621 done
```
```   622
```
```   623 lemma fmran'_transfer[transfer_rule]:
```
```   624   "(pcr_fmap op = op = ===> op =) (\<lambda>x. UNION (range x) set_option) fmran'"
```
```   625 apply (tactic \<open>Local_Defs.unfold_tac @{context} (BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.set_defs_of_bnf)\<close>)
```
```   626 unfolding fmap.pcr_cr_eq cr_fmap_def
```
```   627 by fastforce
```
```   628
```
```   629 lemma fmrel_transfer[transfer_rule]:
```
```   630   "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op = ===> op =) rel_map fmrel"
```
```   631 apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.rel_def_of_bnf]\<close>)
```
```   632 unfolding fmap.pcr_cr_eq cr_fmap_def vimage2p_def
```
```   633   by fastforce
```
```   634
```
```   635 end
```
```   636
```
```   637
```
```   638 lemma fmran'_alt_def: "fmran' = fset \<circ> fmran"
```
```   639 including fset.lifting
```
```   640 by transfer' (auto simp: ran_def fun_eq_iff)
```
```   641
```
```   642 lemma fmran'I: "fmlookup m x = Some y \<Longrightarrow> y \<in> fmran' m"
```
```   643 by transfer' auto
```
```   644
```
```   645 lemma fmrel_iff: "fmrel R m n \<longleftrightarrow> (\<forall>x. rel_option R (fmlookup m x) (fmlookup n x))"
```
```   646 by transfer' (auto simp: rel_fun_def)
```
```   647
```
```   648 lemma fmrelI[intro]:
```
```   649   assumes "\<And>x. rel_option R (fmlookup m x) (fmlookup n x)"
```
```   650   shows "fmrel R m n"
```
```   651 using assms
```
```   652 by transfer' auto
```
```   653
```
```   654 lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty"
```
```   655 by transfer auto
```
```   656
```
```   657 lemma fmrel_upd[intro]: "fmrel P m n \<Longrightarrow> P x y \<Longrightarrow> fmrel P (fmupd k x m) (fmupd k y n)"
```
```   658 by transfer' (auto simp: map_upd_def rel_fun_def)
```
```   659
```
```   660 lemma fmrelD[dest]: "fmrel P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
```
```   661 by transfer' (auto simp: rel_fun_def)
```
```   662
```
```   663 lemma fmrel_addI[intro]:
```
```   664   assumes "fmrel P m n" "fmrel P a b"
```
```   665   shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)"
```
```   666 using assms
```
```   667 apply transfer'
```
```   668 apply (auto simp: rel_fun_def map_add_def)
```
```   669 by (metis option.case_eq_if option.collapse option.rel_sel)
```
```   670
```
```   671 lemma fmrel_cases[consumes 1]:
```
```   672   assumes "fmrel P m n"
```
```   673   obtains (none) "fmlookup m x = None" "fmlookup n x = None"
```
```   674         | (some) a b where "fmlookup m x = Some a" "fmlookup n x = Some b" "P a b"
```
```   675 proof -
```
```   676   from assms have "rel_option P (fmlookup m x) (fmlookup n x)"
```
```   677     by auto
```
```   678   thus thesis
```
```   679     using none some
```
```   680     by (cases rule: option.rel_cases) auto
```
```   681 qed
```
```   682
```
```   683 lemma fmrel_filter[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmfilter Q m) (fmfilter Q n)"
```
```   684 unfolding fmrel_iff by auto
```
```   685
```
```   686 lemma fmrel_drop[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop a m) (fmdrop a n)"
```
```   687   unfolding fmfilter_alt_defs by blast
```
```   688
```
```   689 lemma fmrel_drop_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_set A m) (fmdrop_set A n)"
```
```   690   unfolding fmfilter_alt_defs by blast
```
```   691
```
```   692 lemma fmrel_drop_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_fset A m) (fmdrop_fset A n)"
```
```   693   unfolding fmfilter_alt_defs by blast
```
```   694
```
```   695 lemma fmrel_restrict_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_set A m) (fmrestrict_set A n)"
```
```   696   unfolding fmfilter_alt_defs by blast
```
```   697
```
```   698 lemma fmrel_restrict_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)"
```
```   699   unfolding fmfilter_alt_defs by blast
```
```   700
```
```   701 lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\<lambda>_. P)"
```
```   702 unfolding fmap.pred_set fmran'_alt_def
```
```   703 including fset.lifting
```
```   704 apply transfer'
```
```   705 apply (rule ext)
```
```   706 apply (auto simp: map_pred_def ran_def split: option.splits dest: )
```
```   707 done
```
```   708
```
```   709 lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \<longleftrightarrow> pred_fmap f m"
```
```   710 unfolding fmap.pred_set fmap.set_map
```
```   711 by simp
```
```   712
```
```   713 lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)"
```
```   714 apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\<close>)
```
```   715 apply (auto simp: fmap.Abs_fmap_inverse)
```
```   716 done
```
```   717
```
```   718 lemma fmpred_map[simp]: "fmpred P (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>k v. P k (f v)) m"
```
```   719 unfolding fmpred_iff pred_fmap_def fmap.set_map
```
```   720 by auto
```
```   721
```
```   722 lemma fmpred_id[simp]: "fmpred (\<lambda>_. id) (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>_. f) m"
```
```   723 by simp
```
```   724
```
```   725 lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n"
```
```   726 by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
```
```   727
```
```   728 lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty"
```
```   729 by transfer auto
```
```   730
```
```   731 lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m"
```
```   732 including fset.lifting
```
```   733 by transfer' simp
```
```   734
```
```   735 lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m"
```
```   736 by transfer' simp
```
```   737
```
```   738 lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)"
```
```   739 by transfer' (auto simp: map_filter_def)
```
```   740
```
```   741 lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" unfolding fmfilter_alt_defs by simp
```
```   742 lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp
```
```   743 lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp
```
```   744 lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp
```
```   745 lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp
```
```   746
```
```   747 lemma fmmap_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap f m \<subseteq>\<^sub>f fmmap f n"
```
```   748 by transfer' (auto simp: map_le_def)
```
```   749
```
```   750
```
```   751 subsection \<open>Code setup\<close>
```
```   752
```
```   753 instantiation fmap :: (type, equal) equal begin
```
```   754
```
```   755 definition "equal_fmap \<equiv> fmrel HOL.equal"
```
```   756
```
```   757 instance proof
```
```   758   fix m n :: "('a, 'b) fmap"
```
```   759   have "fmrel op = m n \<longleftrightarrow> (m = n)"
```
```   760     by transfer' (simp add: option.rel_eq rel_fun_eq)
```
```   761   thus "equal_class.equal m n \<longleftrightarrow> (m = n)"
```
```   762     unfolding equal_fmap_def
```
```   763     by (simp add: equal_eq[abs_def])
```
```   764 qed
```
```   765
```
```   766 end
```
```   767
```
```   768 lemma fBall_alt_def: "fBall S P \<longleftrightarrow> (\<forall>x. x |\<in>| S \<longrightarrow> P x)"
```
```   769 by force
```
```   770
```
```   771 lemma fmrel_code:
```
```   772   "fmrel R m n \<longleftrightarrow>
```
```   773     fBall (fmdom m) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x)) \<and>
```
```   774     fBall (fmdom n) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x))"
```
```   775 unfolding fmrel_iff fmlookup_dom_iff fBall_alt_def
```
```   776 by (metis option.collapse option.rel_sel)
```
```   777
```
```   778 lemmas fmap_generic_code =
```
```   779   fmrel_code
```
```   780   fmran'_alt_def
```
```   781   fmdom'_alt_def
```
```   782   fmfilter_alt_defs
```
```   783   pred_fmap_fmpred
```
```   784   fmsubset_alt_def
```
```   785   fmupd_alt_def
```
```   786   fmrel_on_fset_alt_def
```
```   787   fmpred_alt_def
```
```   788
```
```   789
```
```   790 code_datatype fmap_of_list
```
```   791 quickcheck_generator fmap constructors: fmap_of_list
```
```   792
```
```   793 context includes fset.lifting begin
```
```   794
```
```   795 lemma [code]: "fmlookup (fmap_of_list m) = map_of m"
```
```   796 by transfer simp
```
```   797
```
```   798 lemma [code]: "fmempty = fmap_of_list []"
```
```   799 by transfer simp
```
```   800
```
```   801 lemma [code]: "fmran (fmap_of_list m) = snd |`| fset_of_list (AList.clearjunk m)"
```
```   802 by transfer (auto simp: ran_map_of)
```
```   803
```
```   804 lemma [code]: "fmdom (fmap_of_list m) = fst |`| fset_of_list m"
```
```   805 by transfer (auto simp: dom_map_of_conv_image_fst)
```
```   806
```
```   807 lemma [code]: "fmfilter P (fmap_of_list m) = fmap_of_list (filter (\<lambda>(k, _). P k) m)"
```
```   808 by transfer' auto
```
```   809
```
```   810 lemma [code]: "fmap_of_list m ++\<^sub>f fmap_of_list n = fmap_of_list (AList.merge m n)"
```
```   811 by transfer (simp add: merge_conv')
```
```   812
```
```   813 lemma [code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)"
```
```   814 apply transfer
```
```   815 apply (subst map_of_map[symmetric])
```
```   816 apply (auto simp: apsnd_def map_prod_def)
```
```   817 done
```
```   818
```
```   819 end
```
```   820
```
```   821 declare fmap_generic_code[code]
```
```   822
```
```   823 lifting_update fmap.lifting
```
```   824 lifting_forget fmap.lifting
```
```   825
```
`   826 end`