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