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