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