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