src/HOL/Library/Mapping.thy
author wenzelm
Wed Jul 13 19:02:23 2016 +0200 (2016-07-13)
changeset 63476 ff1d86b07751
parent 63462 c1fe30f2bc32
child 66251 cd935b7cb3fb
permissions -rw-r--r--
tuned;
kuncar@49929
     1
(*  Title:      HOL/Library/Mapping.thy
kuncar@49929
     2
    Author:     Florian Haftmann and Ondrej Kuncar
kuncar@49929
     3
*)
haftmann@29708
     4
wenzelm@60500
     5
section \<open>An abstract view on maps for code generation.\<close>
haftmann@29708
     6
haftmann@29708
     7
theory Mapping
kuncar@53013
     8
imports Main
haftmann@29708
     9
begin
haftmann@29708
    10
wenzelm@60500
    11
subsection \<open>Parametricity transfer rules\<close>
kuncar@51379
    12
wenzelm@63462
    13
lemma map_of_foldr: "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty"  (* FIXME move *)
haftmann@56529
    14
  using map_add_map_of_foldr [of Map.empty] by auto
haftmann@56529
    15
wenzelm@63343
    16
context includes lifting_syntax
kuncar@53013
    17
begin
haftmann@56528
    18
wenzelm@63462
    19
lemma empty_parametric: "(A ===> rel_option B) Map.empty Map.empty"
haftmann@56528
    20
  by transfer_prover
kuncar@51379
    21
haftmann@56529
    22
lemma lookup_parametric: "((A ===> B) ===> A ===> B) (\<lambda>m k. m k) (\<lambda>m k. m k)"
haftmann@56528
    23
  by transfer_prover
kuncar@51379
    24
haftmann@56529
    25
lemma update_parametric:
kuncar@51379
    26
  assumes [transfer_rule]: "bi_unique A"
haftmann@56528
    27
  shows "(A ===> B ===> (A ===> rel_option B) ===> A ===> rel_option B)
haftmann@56528
    28
    (\<lambda>k v m. m(k \<mapsto> v)) (\<lambda>k v m. m(k \<mapsto> v))"
haftmann@56528
    29
  by transfer_prover
kuncar@51379
    30
haftmann@56529
    31
lemma delete_parametric:
kuncar@51379
    32
  assumes [transfer_rule]: "bi_unique A"
wenzelm@63462
    33
  shows "(A ===> (A ===> rel_option B) ===> A ===> rel_option B)
haftmann@56528
    34
    (\<lambda>k m. m(k := None)) (\<lambda>k m. m(k := None))"
haftmann@56528
    35
  by transfer_prover
kuncar@51379
    36
haftmann@56528
    37
lemma is_none_parametric [transfer_rule]:
haftmann@56528
    38
  "(rel_option A ===> HOL.eq) Option.is_none Option.is_none"
wenzelm@61068
    39
  by (auto simp add: Option.is_none_def rel_fun_def rel_option_iff split: option.split)
kuncar@51379
    40
haftmann@56529
    41
lemma dom_parametric:
kuncar@51379
    42
  assumes [transfer_rule]: "bi_total A"
wenzelm@63462
    43
  shows "((A ===> rel_option B) ===> rel_set A) dom dom"
wenzelm@61068
    44
  unfolding dom_def [abs_def] Option.is_none_def [symmetric] by transfer_prover
kuncar@51379
    45
haftmann@56529
    46
lemma map_of_parametric [transfer_rule]:
kuncar@51379
    47
  assumes [transfer_rule]: "bi_unique R1"
blanchet@55944
    48
  shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
haftmann@56528
    49
  unfolding map_of_def by transfer_prover
kuncar@51379
    50
haftmann@56529
    51
lemma map_entry_parametric [transfer_rule]:
haftmann@56529
    52
  assumes [transfer_rule]: "bi_unique A"
wenzelm@63462
    53
  shows "(A ===> (B ===> B) ===> (A ===> rel_option B) ===> A ===> rel_option B)
haftmann@56529
    54
    (\<lambda>k f m. (case m k of None \<Rightarrow> m
haftmann@56529
    55
      | Some v \<Rightarrow> m (k \<mapsto> (f v)))) (\<lambda>k f m. (case m k of None \<Rightarrow> m
haftmann@56529
    56
      | Some v \<Rightarrow> m (k \<mapsto> (f v))))"
haftmann@56529
    57
  by transfer_prover
haftmann@56529
    58
wenzelm@63462
    59
lemma tabulate_parametric:
kuncar@51379
    60
  assumes [transfer_rule]: "bi_unique A"
wenzelm@63462
    61
  shows "(list_all2 A ===> (A ===> B) ===> A ===> rel_option B)
haftmann@56528
    62
    (\<lambda>ks f. (map_of (map (\<lambda>k. (k, f k)) ks))) (\<lambda>ks f. (map_of (map (\<lambda>k. (k, f k)) ks)))"
haftmann@56528
    63
  by transfer_prover
kuncar@51379
    64
wenzelm@63462
    65
lemma bulkload_parametric:
wenzelm@63462
    66
  "(list_all2 A ===> HOL.eq ===> rel_option A)
wenzelm@63462
    67
    (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)
wenzelm@63462
    68
    (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)"
haftmann@56528
    69
proof
haftmann@56528
    70
  fix xs ys
haftmann@56528
    71
  assume "list_all2 A xs ys"
wenzelm@63462
    72
  then show
wenzelm@63462
    73
    "(HOL.eq ===> rel_option A)
wenzelm@63462
    74
      (\<lambda>k. if k < length xs then Some (xs ! k) else None)
wenzelm@63462
    75
      (\<lambda>k. if k < length ys then Some (ys ! k) else None)"
haftmann@56528
    76
    apply induct
wenzelm@63476
    77
     apply auto
haftmann@56528
    78
    unfolding rel_fun_def
wenzelm@63462
    79
    apply clarsimp
wenzelm@63462
    80
    apply (case_tac xa)
wenzelm@63476
    81
     apply (auto dest: list_all2_lengthD list_all2_nthD)
haftmann@56528
    82
    done
haftmann@56528
    83
qed
kuncar@51379
    84
wenzelm@63462
    85
lemma map_parametric:
wenzelm@63462
    86
  "((A ===> B) ===> (C ===> D) ===> (B ===> rel_option C) ===> A ===> rel_option D)
haftmann@56528
    87
     (\<lambda>f g m. (map_option g \<circ> m \<circ> f)) (\<lambda>f g m. (map_option g \<circ> m \<circ> f))"
haftmann@56528
    88
  by transfer_prover
wenzelm@63462
    89
wenzelm@63462
    90
lemma combine_with_key_parametric:
wenzelm@63462
    91
  "((A ===> B ===> B ===> B) ===> (A ===> rel_option B) ===> (A ===> rel_option B) ===>
wenzelm@63462
    92
    (A ===> rel_option B)) (\<lambda>f m1 m2 x. combine_options (f x) (m1 x) (m2 x))
wenzelm@63462
    93
    (\<lambda>f m1 m2 x. combine_options (f x) (m1 x) (m2 x))"
eberlm@63194
    94
  unfolding combine_options_def by transfer_prover
wenzelm@63462
    95
wenzelm@63462
    96
lemma combine_parametric:
wenzelm@63462
    97
  "((B ===> B ===> B) ===> (A ===> rel_option B) ===> (A ===> rel_option B) ===>
wenzelm@63462
    98
    (A ===> rel_option B)) (\<lambda>f m1 m2 x. combine_options f (m1 x) (m2 x))
wenzelm@63462
    99
    (\<lambda>f m1 m2 x. combine_options f (m1 x) (m2 x))"
eberlm@63194
   100
  unfolding combine_options_def by transfer_prover
kuncar@51379
   101
haftmann@56529
   102
end
kuncar@51379
   103
kuncar@53013
   104
wenzelm@60500
   105
subsection \<open>Type definition and primitive operations\<close>
haftmann@29708
   106
wenzelm@49834
   107
typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
wenzelm@63462
   108
  morphisms rep Mapping ..
haftmann@37700
   109
haftmann@59485
   110
setup_lifting type_definition_mapping
haftmann@37700
   111
haftmann@56528
   112
lift_definition empty :: "('a, 'b) mapping"
haftmann@56529
   113
  is Map.empty parametric empty_parametric .
kuncar@49929
   114
haftmann@56528
   115
lift_definition lookup :: "('a, 'b) mapping \<Rightarrow> 'a \<Rightarrow> 'b option"
haftmann@56529
   116
  is "\<lambda>m k. m k" parametric lookup_parametric .
haftmann@56528
   117
eberlm@63194
   118
definition "lookup_default d m k = (case Mapping.lookup m k of None \<Rightarrow> d | Some v \<Rightarrow> v)"
eberlm@63194
   119
haftmann@59485
   120
declare [[code drop: Mapping.lookup]]
wenzelm@63462
   121
setup \<open>Code.add_eqn (Code.Equation, true) @{thm Mapping.lookup.abs_eq}\<close>  (* FIXME lifting *)
haftmann@59485
   122
haftmann@56528
   123
lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
haftmann@56529
   124
  is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric .
haftmann@37700
   125
haftmann@56528
   126
lift_definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
haftmann@56529
   127
  is "\<lambda>k m. m(k := None)" parametric delete_parametric .
haftmann@39380
   128
eberlm@63194
   129
lift_definition filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
wenzelm@63462
   130
  is "\<lambda>P m k. case m k of None \<Rightarrow> None | Some v \<Rightarrow> if P k v then Some v else None" .
eberlm@63194
   131
haftmann@56528
   132
lift_definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set"
haftmann@56529
   133
  is dom parametric dom_parametric .
haftmann@29708
   134
haftmann@56528
   135
lift_definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping"
haftmann@56529
   136
  is "\<lambda>ks f. (map_of (List.map (\<lambda>k. (k, f k)) ks))" parametric tabulate_parametric .
haftmann@29708
   137
haftmann@56528
   138
lift_definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping"
haftmann@56529
   139
  is "\<lambda>xs k. if k < length xs then Some (xs ! k) else None" parametric bulkload_parametric .
haftmann@29708
   140
haftmann@56528
   141
lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping"
haftmann@56529
   142
  is "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_parametric .
wenzelm@63462
   143
eberlm@63194
   144
lift_definition map_values :: "('c \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('c, 'a) mapping \<Rightarrow> ('c, 'b) mapping"
wenzelm@63462
   145
  is "\<lambda>f m x. map_option (f x) (m x)" .
eberlm@63194
   146
wenzelm@63462
   147
lift_definition combine_with_key ::
eberlm@63194
   148
  "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping"
eberlm@63194
   149
  is "\<lambda>f m1 m2 x. combine_options (f x) (m1 x) (m2 x)" parametric combine_with_key_parametric .
eberlm@63194
   150
wenzelm@63462
   151
lift_definition combine ::
eberlm@63194
   152
  "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping"
eberlm@63194
   153
  is "\<lambda>f m1 m2 x. combine_options f (m1 x) (m2 x)" parametric combine_parametric .
eberlm@63194
   154
wenzelm@63462
   155
definition "All_mapping m P \<longleftrightarrow>
wenzelm@63462
   156
  (\<forall>x. case Mapping.lookup m x of None \<Rightarrow> True | Some y \<Rightarrow> P x y)"
haftmann@29708
   157
haftmann@59485
   158
declare [[code drop: map]]
haftmann@59485
   159
haftmann@51161
   160
wenzelm@60500
   161
subsection \<open>Functorial structure\<close>
haftmann@40605
   162
blanchet@55467
   163
functor map: map
blanchet@55466
   164
  by (transfer, auto simp add: fun_eq_iff option.map_comp option.map_id)+
haftmann@40605
   165
haftmann@51161
   166
wenzelm@60500
   167
subsection \<open>Derived operations\<close>
haftmann@29708
   168
wenzelm@61076
   169
definition ordered_keys :: "('a::linorder, 'b) mapping \<Rightarrow> 'a list"
wenzelm@63462
   170
  where "ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])"
haftmann@35194
   171
haftmann@56528
   172
definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool"
wenzelm@63462
   173
  where "is_empty m \<longleftrightarrow> keys m = {}"
haftmann@35157
   174
haftmann@56528
   175
definition size :: "('a, 'b) mapping \<Rightarrow> nat"
wenzelm@63462
   176
  where "size m = (if finite (keys m) then card (keys m) else 0)"
haftmann@35157
   177
haftmann@56528
   178
definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
wenzelm@63462
   179
  where "replace k v m = (if k \<in> keys m then update k v m else m)"
haftmann@29814
   180
haftmann@56528
   181
definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
wenzelm@63462
   182
  where "default k v m = (if k \<in> keys m then m else update k v m)"
haftmann@37026
   183
wenzelm@60500
   184
text \<open>Manual derivation of transfer rule is non-trivial\<close>
haftmann@56529
   185
kuncar@49929
   186
lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" is
wenzelm@63462
   187
  "\<lambda>k f m.
wenzelm@63462
   188
    (case m k of
wenzelm@63462
   189
      None \<Rightarrow> m
haftmann@56529
   190
    | Some v \<Rightarrow> m (k \<mapsto> (f v)))" parametric map_entry_parametric .
kuncar@49929
   191
haftmann@56529
   192
lemma map_entry_code [code]:
wenzelm@63462
   193
  "map_entry k f m =
wenzelm@63462
   194
    (case lookup m k of
wenzelm@63462
   195
      None \<Rightarrow> m
huffman@49975
   196
    | Some v \<Rightarrow> update k (f v) m)"
huffman@49975
   197
  by transfer rule
haftmann@37026
   198
haftmann@56528
   199
definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
wenzelm@63462
   200
  where "map_default k v f m = map_entry k f (default k v m)"
haftmann@37026
   201
haftmann@56529
   202
definition of_alist :: "('k \<times> 'v) list \<Rightarrow> ('k, 'v) mapping"
wenzelm@63462
   203
  where "of_alist xs = foldr (\<lambda>(k, v) m. update k v m) xs empty"
kuncar@51379
   204
haftmann@51161
   205
instantiation mapping :: (type, type) equal
haftmann@51161
   206
begin
haftmann@51161
   207
wenzelm@63462
   208
definition "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)"
haftmann@51161
   209
wenzelm@60679
   210
instance
wenzelm@63462
   211
  apply standard
wenzelm@63462
   212
  unfolding equal_mapping_def
wenzelm@63462
   213
  apply transfer
wenzelm@63462
   214
  apply auto
wenzelm@63462
   215
  done
haftmann@51161
   216
haftmann@51161
   217
end
haftmann@51161
   218
wenzelm@63343
   219
context includes lifting_syntax
kuncar@53013
   220
begin
haftmann@56528
   221
haftmann@51161
   222
lemma [transfer_rule]:
kuncar@51379
   223
  assumes [transfer_rule]: "bi_total A"
wenzelm@63462
   224
    and [transfer_rule]: "bi_unique B"
haftmann@56528
   225
  shows "(pcr_mapping A B ===> pcr_mapping A B ===> op=) HOL.eq HOL.equal"
wenzelm@63462
   226
  unfolding equal by transfer_prover
haftmann@51161
   227
haftmann@56529
   228
lemma of_alist_transfer [transfer_rule]:
haftmann@56529
   229
  assumes [transfer_rule]: "bi_unique R1"
haftmann@56529
   230
  shows "(list_all2 (rel_prod R1 R2) ===> pcr_mapping R1 R2) map_of of_alist"
haftmann@56529
   231
  unfolding of_alist_def [abs_def] map_of_foldr [abs_def] by transfer_prover
haftmann@56529
   232
kuncar@53013
   233
end
haftmann@51161
   234
haftmann@56528
   235
wenzelm@60500
   236
subsection \<open>Properties\<close>
haftmann@29708
   237
wenzelm@63462
   238
lemma mapping_eqI: "(\<And>x. lookup m x = lookup m' x) \<Longrightarrow> m = m'"
eberlm@63195
   239
  by transfer (simp add: fun_eq_iff)
eberlm@63195
   240
wenzelm@63462
   241
lemma mapping_eqI':
wenzelm@63462
   242
  assumes "\<And>x. x \<in> Mapping.keys m \<Longrightarrow> Mapping.lookup_default d m x = Mapping.lookup_default d m' x"
wenzelm@63462
   243
    and "Mapping.keys m = Mapping.keys m'"
wenzelm@63462
   244
  shows "m = m'"
eberlm@63195
   245
proof (intro mapping_eqI)
wenzelm@63462
   246
  show "Mapping.lookup m x = Mapping.lookup m' x" for x
eberlm@63195
   247
  proof (cases "Mapping.lookup m x")
eberlm@63195
   248
    case None
wenzelm@63462
   249
    then have "x \<notin> Mapping.keys m"
wenzelm@63462
   250
      by transfer (simp add: dom_def)
wenzelm@63462
   251
    then have "x \<notin> Mapping.keys m'"
wenzelm@63462
   252
      by (simp add: assms)
wenzelm@63462
   253
    then have "Mapping.lookup m' x = None"
wenzelm@63462
   254
      by transfer (simp add: dom_def)
wenzelm@63462
   255
    with None show ?thesis
wenzelm@63462
   256
      by simp
eberlm@63195
   257
  next
eberlm@63195
   258
    case (Some y)
wenzelm@63462
   259
    then have A: "x \<in> Mapping.keys m"
wenzelm@63462
   260
      by transfer (simp add: dom_def)
wenzelm@63462
   261
    then have "x \<in> Mapping.keys m'"
wenzelm@63462
   262
      by (simp add: assms)
wenzelm@63462
   263
    then have "\<exists>y'. Mapping.lookup m' x = Some y'"
wenzelm@63462
   264
      by transfer (simp add: dom_def)
wenzelm@63462
   265
    with Some assms(1)[OF A] show ?thesis
wenzelm@63462
   266
      by (auto simp add: lookup_default_def)
eberlm@63195
   267
  qed
eberlm@63195
   268
qed
eberlm@63195
   269
wenzelm@63462
   270
lemma lookup_update: "lookup (update k v m) k = Some v"
kuncar@49973
   271
  by transfer simp
kuncar@49973
   272
wenzelm@63462
   273
lemma lookup_update_neq: "k \<noteq> k' \<Longrightarrow> lookup (update k v m) k' = lookup m k'"
kuncar@49973
   274
  by transfer simp
kuncar@49973
   275
wenzelm@63462
   276
lemma lookup_update': "Mapping.lookup (update k v m) k' = (if k = k' then Some v else lookup m k')"
eberlm@63194
   277
  by (auto simp: lookup_update lookup_update_neq)
eberlm@63194
   278
wenzelm@63462
   279
lemma lookup_empty: "lookup empty k = None"
kuncar@49973
   280
  by transfer simp
kuncar@49973
   281
eberlm@63194
   282
lemma lookup_filter:
wenzelm@63462
   283
  "lookup (filter P m) k =
wenzelm@63462
   284
    (case lookup m k of
wenzelm@63462
   285
      None \<Rightarrow> None
wenzelm@63462
   286
    | Some v \<Rightarrow> if P k v then Some v else None)"
eberlm@63194
   287
  by transfer simp_all
eberlm@63194
   288
wenzelm@63462
   289
lemma lookup_map_values: "lookup (map_values f m) k = map_option (f k) (lookup m k)"
eberlm@63194
   290
  by transfer simp_all
eberlm@63194
   291
eberlm@63194
   292
lemma lookup_default_empty: "lookup_default d empty k = d"
eberlm@63194
   293
  by (simp add: lookup_default_def lookup_empty)
eberlm@63194
   294
wenzelm@63462
   295
lemma lookup_default_update: "lookup_default d (update k v m) k = v"
eberlm@63194
   296
  by (simp add: lookup_default_def lookup_update)
eberlm@63194
   297
eberlm@63194
   298
lemma lookup_default_update_neq:
wenzelm@63462
   299
  "k \<noteq> k' \<Longrightarrow> lookup_default d (update k v m) k' = lookup_default d m k'"
eberlm@63194
   300
  by (simp add: lookup_default_def lookup_update_neq)
eberlm@63194
   301
wenzelm@63462
   302
lemma lookup_default_update':
eberlm@63194
   303
  "lookup_default d (update k v m) k' = (if k = k' then v else lookup_default d m k')"
eberlm@63194
   304
  by (auto simp: lookup_default_update lookup_default_update_neq)
eberlm@63194
   305
eberlm@63194
   306
lemma lookup_default_filter:
wenzelm@63462
   307
  "lookup_default d (filter P m) k =
eberlm@63194
   308
     (if P k (lookup_default d m k) then lookup_default d m k else d)"
eberlm@63194
   309
  by (simp add: lookup_default_def lookup_filter split: option.splits)
eberlm@63194
   310
eberlm@63194
   311
lemma lookup_default_map_values:
eberlm@63194
   312
  "lookup_default (f k d) (map_values f m) k = f k (lookup_default d m k)"
wenzelm@63462
   313
  by (simp add: lookup_default_def lookup_map_values split: option.splits)
eberlm@63194
   314
eberlm@63194
   315
lemma lookup_combine_with_key:
wenzelm@63462
   316
  "Mapping.lookup (combine_with_key f m1 m2) x =
wenzelm@63462
   317
    combine_options (f x) (Mapping.lookup m1 x) (Mapping.lookup m2 x)"
eberlm@63194
   318
  by transfer (auto split: option.splits)
wenzelm@63462
   319
eberlm@63194
   320
lemma combine_altdef: "combine f m1 m2 = combine_with_key (\<lambda>_. f) m1 m2"
eberlm@63194
   321
  by transfer' (rule refl)
eberlm@63194
   322
eberlm@63194
   323
lemma lookup_combine:
wenzelm@63462
   324
  "Mapping.lookup (combine f m1 m2) x =
eberlm@63194
   325
     combine_options f (Mapping.lookup m1 x) (Mapping.lookup m2 x)"
eberlm@63194
   326
  by transfer (auto split: option.splits)
wenzelm@63462
   327
wenzelm@63462
   328
lemma lookup_default_neutral_combine_with_key:
eberlm@63194
   329
  assumes "\<And>x. f k d x = x" "\<And>x. f k x d = x"
wenzelm@63462
   330
  shows "Mapping.lookup_default d (combine_with_key f m1 m2) k =
wenzelm@63462
   331
    f k (Mapping.lookup_default d m1 k) (Mapping.lookup_default d m2 k)"
eberlm@63194
   332
  by (auto simp: lookup_default_def lookup_combine_with_key assms split: option.splits)
wenzelm@63462
   333
wenzelm@63462
   334
lemma lookup_default_neutral_combine:
eberlm@63194
   335
  assumes "\<And>x. f d x = x" "\<And>x. f x d = x"
wenzelm@63462
   336
  shows "Mapping.lookup_default d (combine f m1 m2) x =
wenzelm@63462
   337
    f (Mapping.lookup_default d m1 x) (Mapping.lookup_default d m2 x)"
eberlm@63194
   338
  by (auto simp: lookup_default_def lookup_combine assms split: option.splits)
eberlm@63194
   339
wenzelm@63462
   340
lemma lookup_map_entry: "lookup (map_entry x f m) x = map_option f (lookup m x)"
eberlm@63195
   341
  by transfer (auto split: option.splits)
eberlm@63195
   342
wenzelm@63462
   343
lemma lookup_map_entry_neq: "x \<noteq> y \<Longrightarrow> lookup (map_entry x f m) y = lookup m y"
eberlm@63195
   344
  by transfer (auto split: option.splits)
eberlm@63195
   345
eberlm@63195
   346
lemma lookup_map_entry':
wenzelm@63462
   347
  "lookup (map_entry x f m) y =
eberlm@63195
   348
     (if x = y then map_option f (lookup m y) else lookup m y)"
eberlm@63195
   349
  by transfer (auto split: option.splits)
eberlm@63195
   350
wenzelm@63462
   351
lemma lookup_default: "lookup (default x d m) x = Some (lookup_default d m x)"
wenzelm@63462
   352
  unfolding lookup_default_def default_def
wenzelm@63462
   353
  by transfer (auto split: option.splits)
wenzelm@63462
   354
wenzelm@63462
   355
lemma lookup_default_neq: "x \<noteq> y \<Longrightarrow> lookup (default x d m) y = lookup m y"
wenzelm@63462
   356
  unfolding lookup_default_def default_def
wenzelm@63462
   357
  by transfer (auto split: option.splits)
eberlm@63195
   358
eberlm@63195
   359
lemma lookup_default':
wenzelm@63462
   360
  "lookup (default x d m) y =
wenzelm@63462
   361
    (if x = y then Some (lookup_default d m x) else lookup m y)"
eberlm@63195
   362
  unfolding lookup_default_def default_def
eberlm@63195
   363
  by transfer (auto split: option.splits)
eberlm@63195
   364
wenzelm@63462
   365
lemma lookup_map_default: "lookup (map_default x d f m) x = Some (f (lookup_default d m x))"
wenzelm@63462
   366
  unfolding lookup_default_def default_def
wenzelm@63462
   367
  by (simp add: map_default_def lookup_map_entry lookup_default lookup_default_def)
wenzelm@63462
   368
wenzelm@63462
   369
lemma lookup_map_default_neq: "x \<noteq> y \<Longrightarrow> lookup (map_default x d f m) y = lookup m y"
wenzelm@63462
   370
  unfolding lookup_default_def default_def
wenzelm@63462
   371
  by (simp add: map_default_def lookup_map_entry_neq lookup_default_neq)
eberlm@63195
   372
eberlm@63195
   373
lemma lookup_map_default':
wenzelm@63462
   374
  "lookup (map_default x d f m) y =
wenzelm@63462
   375
    (if x = y then Some (f (lookup_default d m x)) else lookup m y)"
wenzelm@63462
   376
  unfolding lookup_default_def default_def
wenzelm@63462
   377
  by (simp add: map_default_def lookup_map_entry' lookup_default' lookup_default_def)
eberlm@63195
   378
wenzelm@63462
   379
lemma lookup_tabulate:
eberlm@63194
   380
  assumes "distinct xs"
wenzelm@63462
   381
  shows "Mapping.lookup (Mapping.tabulate xs f) x = (if x \<in> set xs then Some (f x) else None)"
eberlm@63194
   382
  using assms by transfer (auto simp: map_of_eq_None_iff o_def dest!: map_of_SomeD)
eberlm@63194
   383
eberlm@63194
   384
lemma lookup_of_alist: "Mapping.lookup (Mapping.of_alist xs) k = map_of xs k"
eberlm@63194
   385
  by transfer simp_all
eberlm@63194
   386
wenzelm@63462
   387
lemma keys_is_none_rep [code_unfold]: "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
wenzelm@61068
   388
  by transfer (auto simp add: Option.is_none_def)
haftmann@29708
   389
haftmann@29708
   390
lemma update_update:
haftmann@29708
   391
  "update k v (update k w m) = update k v m"
haftmann@29708
   392
  "k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"
wenzelm@63462
   393
  by (transfer; simp add: fun_upd_twist)+
haftmann@29708
   394
wenzelm@63462
   395
lemma update_delete [simp]: "update k v (delete k m) = update k v m"
kuncar@49929
   396
  by transfer simp
haftmann@29708
   397
haftmann@29708
   398
lemma delete_update:
haftmann@29708
   399
  "delete k (update k v m) = delete k m"
haftmann@29708
   400
  "k \<noteq> l \<Longrightarrow> delete k (update l v m) = update l v (delete k m)"
wenzelm@63462
   401
  by (transfer; simp add: fun_upd_twist)+
haftmann@29708
   402
wenzelm@63462
   403
lemma delete_empty [simp]: "delete k empty = empty"
kuncar@49929
   404
  by transfer simp
haftmann@29708
   405
haftmann@35157
   406
lemma replace_update:
haftmann@37052
   407
  "k \<notin> keys m \<Longrightarrow> replace k v m = m"
haftmann@37052
   408
  "k \<in> keys m \<Longrightarrow> replace k v m = update k v m"
wenzelm@63462
   409
  by (transfer; auto simp add: replace_def fun_upd_twist)+
wenzelm@63462
   410
eberlm@63194
   411
lemma map_values_update: "map_values f (update k v m) = update k (f k v) (map_values f m)"
eberlm@63194
   412
  by transfer (simp_all add: fun_eq_iff)
wenzelm@63462
   413
wenzelm@63462
   414
lemma size_mono: "finite (keys m') \<Longrightarrow> keys m \<subseteq> keys m' \<Longrightarrow> size m \<le> size m'"
eberlm@63194
   415
  unfolding size_def by (auto intro: card_mono)
haftmann@29708
   416
wenzelm@63462
   417
lemma size_empty [simp]: "size empty = 0"
kuncar@49929
   418
  unfolding size_def by transfer simp
haftmann@29708
   419
haftmann@29708
   420
lemma size_update:
haftmann@37052
   421
  "finite (keys m) \<Longrightarrow> size (update k v m) =
haftmann@37052
   422
    (if k \<in> keys m then size m else Suc (size m))"
kuncar@49929
   423
  unfolding size_def by transfer (auto simp add: insert_dom)
haftmann@29708
   424
wenzelm@63462
   425
lemma size_delete: "size (delete k m) = (if k \<in> keys m then size m - 1 else size m)"
kuncar@49929
   426
  unfolding size_def by transfer simp
haftmann@29708
   427
wenzelm@63462
   428
lemma size_tabulate [simp]: "size (tabulate ks f) = length (remdups ks)"
wenzelm@63462
   429
  unfolding size_def by transfer (auto simp add: map_of_map_restrict card_set comp_def)
haftmann@29708
   430
eberlm@63194
   431
lemma keys_filter: "keys (filter P m) \<subseteq> keys m"
eberlm@63194
   432
  by transfer (auto split: option.splits)
eberlm@63194
   433
eberlm@63194
   434
lemma size_filter: "finite (keys m) \<Longrightarrow> size (filter P m) \<le> size m"
eberlm@63194
   435
  by (intro size_mono keys_filter)
eberlm@63194
   436
wenzelm@63462
   437
lemma bulkload_tabulate: "bulkload xs = tabulate [0..<length xs] (nth xs)"
haftmann@56528
   438
  by transfer (auto simp add: map_of_map_restrict)
haftmann@29826
   439
wenzelm@63462
   440
lemma is_empty_empty [simp]: "is_empty empty"
kuncar@49929
   441
  unfolding is_empty_def by transfer simp
haftmann@37052
   442
wenzelm@63462
   443
lemma is_empty_update [simp]: "\<not> is_empty (update k v m)"
wenzelm@63462
   444
  unfolding is_empty_def by transfer simp
wenzelm@63462
   445
wenzelm@63462
   446
lemma is_empty_delete: "is_empty (delete k m) \<longleftrightarrow> is_empty m \<or> keys m = {k}"
kuncar@49929
   447
  unfolding is_empty_def by transfer (auto simp del: dom_eq_empty_conv)
haftmann@37052
   448
wenzelm@63462
   449
lemma is_empty_replace [simp]: "is_empty (replace k v m) \<longleftrightarrow> is_empty m"
kuncar@49929
   450
  unfolding is_empty_def replace_def by transfer auto
haftmann@37052
   451
wenzelm@63462
   452
lemma is_empty_default [simp]: "\<not> is_empty (default k v m)"
kuncar@49929
   453
  unfolding is_empty_def default_def by transfer auto
haftmann@37052
   454
wenzelm@63462
   455
lemma is_empty_map_entry [simp]: "is_empty (map_entry k f m) \<longleftrightarrow> is_empty m"
haftmann@56528
   456
  unfolding is_empty_def by transfer (auto split: option.split)
haftmann@37052
   457
wenzelm@63462
   458
lemma is_empty_map_values [simp]: "is_empty (map_values f m) \<longleftrightarrow> is_empty m"
eberlm@63194
   459
  unfolding is_empty_def by transfer (auto simp: fun_eq_iff)
eberlm@63194
   460
wenzelm@63462
   461
lemma is_empty_map_default [simp]: "\<not> is_empty (map_default k v f m)"
haftmann@37052
   462
  by (simp add: map_default_def)
haftmann@37052
   463
wenzelm@63462
   464
lemma keys_dom_lookup: "keys m = dom (Mapping.lookup m)"
haftmann@56545
   465
  by transfer rule
haftmann@56545
   466
wenzelm@63462
   467
lemma keys_empty [simp]: "keys empty = {}"
kuncar@49929
   468
  by transfer simp
haftmann@37052
   469
wenzelm@63462
   470
lemma keys_update [simp]: "keys (update k v m) = insert k (keys m)"
kuncar@49929
   471
  by transfer simp
haftmann@37052
   472
wenzelm@63462
   473
lemma keys_delete [simp]: "keys (delete k m) = keys m - {k}"
kuncar@49929
   474
  by transfer simp
haftmann@37052
   475
wenzelm@63462
   476
lemma keys_replace [simp]: "keys (replace k v m) = keys m"
kuncar@49929
   477
  unfolding replace_def by transfer (simp add: insert_absorb)
haftmann@37052
   478
wenzelm@63462
   479
lemma keys_default [simp]: "keys (default k v m) = insert k (keys m)"
kuncar@49929
   480
  unfolding default_def by transfer (simp add: insert_absorb)
haftmann@37052
   481
wenzelm@63462
   482
lemma keys_map_entry [simp]: "keys (map_entry k f m) = keys m"
haftmann@56528
   483
  by transfer (auto split: option.split)
haftmann@37052
   484
wenzelm@63462
   485
lemma keys_map_default [simp]: "keys (map_default k v f m) = insert k (keys m)"
haftmann@37052
   486
  by (simp add: map_default_def)
haftmann@37052
   487
wenzelm@63462
   488
lemma keys_map_values [simp]: "keys (map_values f m) = keys m"
eberlm@63194
   489
  by transfer (simp_all add: dom_def)
eberlm@63194
   490
wenzelm@63462
   491
lemma keys_combine_with_key [simp]:
eberlm@63194
   492
  "Mapping.keys (combine_with_key f m1 m2) = Mapping.keys m1 \<union> Mapping.keys m2"
wenzelm@63462
   493
  by transfer (auto simp: dom_def combine_options_def split: option.splits)
eberlm@63194
   494
eberlm@63194
   495
lemma keys_combine [simp]: "Mapping.keys (combine f m1 m2) = Mapping.keys m1 \<union> Mapping.keys m2"
eberlm@63194
   496
  by (simp add: combine_altdef)
eberlm@63194
   497
wenzelm@63462
   498
lemma keys_tabulate [simp]: "keys (tabulate ks f) = set ks"
kuncar@49929
   499
  by transfer (simp add: map_of_map_restrict o_def)
haftmann@37026
   500
eberlm@63194
   501
lemma keys_of_alist [simp]: "keys (of_alist xs) = set (List.map fst xs)"
eberlm@63194
   502
  by transfer (simp_all add: dom_map_of_conv_image_fst)
eberlm@63194
   503
wenzelm@63462
   504
lemma keys_bulkload [simp]: "keys (bulkload xs) = {0..<length xs}"
haftmann@56528
   505
  by (simp add: bulkload_tabulate)
haftmann@37026
   506
wenzelm@63462
   507
lemma distinct_ordered_keys [simp]: "distinct (ordered_keys m)"
haftmann@37052
   508
  by (simp add: ordered_keys_def)
haftmann@37052
   509
wenzelm@63462
   510
lemma ordered_keys_infinite [simp]: "\<not> finite (keys m) \<Longrightarrow> ordered_keys m = []"
haftmann@37052
   511
  by (simp add: ordered_keys_def)
haftmann@37052
   512
wenzelm@63462
   513
lemma ordered_keys_empty [simp]: "ordered_keys empty = []"
haftmann@37052
   514
  by (simp add: ordered_keys_def)
haftmann@37052
   515
haftmann@37052
   516
lemma ordered_keys_update [simp]:
haftmann@37052
   517
  "k \<in> keys m \<Longrightarrow> ordered_keys (update k v m) = ordered_keys m"
wenzelm@63462
   518
  "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow>
wenzelm@63462
   519
    ordered_keys (update k v m) = insort k (ordered_keys m)"
wenzelm@63462
   520
  by (simp_all add: ordered_keys_def)
wenzelm@63462
   521
    (auto simp only: sorted_list_of_set_insert [symmetric] insert_absorb)
haftmann@37052
   522
wenzelm@63462
   523
lemma ordered_keys_delete [simp]: "ordered_keys (delete k m) = remove1 k (ordered_keys m)"
haftmann@37052
   524
proof (cases "finite (keys m)")
wenzelm@63462
   525
  case False
wenzelm@63462
   526
  then show ?thesis by simp
haftmann@37052
   527
next
wenzelm@63462
   528
  case fin: True
haftmann@37052
   529
  show ?thesis
haftmann@37052
   530
  proof (cases "k \<in> keys m")
wenzelm@63462
   531
    case False
wenzelm@63462
   532
    with fin have "k \<notin> set (sorted_list_of_set (keys m))"
wenzelm@63462
   533
      by simp
wenzelm@63462
   534
    with False show ?thesis
wenzelm@63462
   535
      by (simp add: ordered_keys_def remove1_idem)
haftmann@37052
   536
  next
wenzelm@63462
   537
    case True
wenzelm@63462
   538
    with fin show ?thesis
wenzelm@63462
   539
      by (simp add: ordered_keys_def sorted_list_of_set_remove)
haftmann@37052
   540
  qed
haftmann@37052
   541
qed
haftmann@37052
   542
wenzelm@63462
   543
lemma ordered_keys_replace [simp]: "ordered_keys (replace k v m) = ordered_keys m"
haftmann@37052
   544
  by (simp add: replace_def)
haftmann@37052
   545
haftmann@37052
   546
lemma ordered_keys_default [simp]:
haftmann@37052
   547
  "k \<in> keys m \<Longrightarrow> ordered_keys (default k v m) = ordered_keys m"
haftmann@37052
   548
  "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (default k v m) = insort k (ordered_keys m)"
haftmann@37052
   549
  by (simp_all add: default_def)
haftmann@37052
   550
wenzelm@63462
   551
lemma ordered_keys_map_entry [simp]: "ordered_keys (map_entry k f m) = ordered_keys m"
haftmann@37052
   552
  by (simp add: ordered_keys_def)
haftmann@37052
   553
haftmann@37052
   554
lemma ordered_keys_map_default [simp]:
haftmann@37052
   555
  "k \<in> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = ordered_keys m"
haftmann@37052
   556
  "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = insort k (ordered_keys m)"
haftmann@37052
   557
  by (simp_all add: map_default_def)
haftmann@37052
   558
wenzelm@63462
   559
lemma ordered_keys_tabulate [simp]: "ordered_keys (tabulate ks f) = sort (remdups ks)"
haftmann@37052
   560
  by (simp add: ordered_keys_def sorted_list_of_set_sort_remdups)
haftmann@37052
   561
wenzelm@63462
   562
lemma ordered_keys_bulkload [simp]: "ordered_keys (bulkload ks) = [0..<length ks]"
haftmann@37052
   563
  by (simp add: ordered_keys_def)
haftmann@36110
   564
wenzelm@63462
   565
lemma tabulate_fold: "tabulate xs f = fold (\<lambda>k m. update k (f k) m) xs empty"
haftmann@56528
   566
proof transfer
haftmann@56528
   567
  fix f :: "'a \<Rightarrow> 'b" and xs
haftmann@56529
   568
  have "map_of (List.map (\<lambda>k. (k, f k)) xs) = foldr (\<lambda>k m. m(k \<mapsto> f k)) xs Map.empty"
haftmann@56529
   569
    by (simp add: foldr_map comp_def map_of_foldr)
haftmann@56528
   570
  also have "foldr (\<lambda>k m. m(k \<mapsto> f k)) xs = fold (\<lambda>k m. m(k \<mapsto> f k)) xs"
haftmann@56528
   571
    by (rule foldr_fold) (simp add: fun_eq_iff)
haftmann@56528
   572
  ultimately show "map_of (List.map (\<lambda>k. (k, f k)) xs) = fold (\<lambda>k m. m(k \<mapsto> f k)) xs Map.empty"
haftmann@56528
   573
    by simp
haftmann@56528
   574
qed
haftmann@56528
   575
eberlm@63194
   576
lemma All_mapping_mono:
eberlm@63194
   577
  "(\<And>k v. k \<in> keys m \<Longrightarrow> P k v \<Longrightarrow> Q k v) \<Longrightarrow> All_mapping m P \<Longrightarrow> All_mapping m Q"
eberlm@63194
   578
  unfolding All_mapping_def by transfer (auto simp: All_mapping_def dom_def split: option.splits)
haftmann@31459
   579
eberlm@63194
   580
lemma All_mapping_empty [simp]: "All_mapping Mapping.empty P"
eberlm@63194
   581
  by (auto simp: All_mapping_def lookup_empty)
wenzelm@63462
   582
wenzelm@63462
   583
lemma All_mapping_update_iff:
eberlm@63194
   584
  "All_mapping (Mapping.update k v m) P \<longleftrightarrow> P k v \<and> All_mapping m (\<lambda>k' v'. k = k' \<or> P k' v')"
wenzelm@63462
   585
  unfolding All_mapping_def
eberlm@63194
   586
proof safe
eberlm@63194
   587
  assume "\<forall>x. case Mapping.lookup (Mapping.update k v m) x of None \<Rightarrow> True | Some y \<Rightarrow> P x y"
wenzelm@63462
   588
  then have *: "case Mapping.lookup (Mapping.update k v m) x of None \<Rightarrow> True | Some y \<Rightarrow> P x y" for x
eberlm@63194
   589
    by blast
wenzelm@63462
   590
  from *[of k] show "P k v"
wenzelm@63462
   591
    by (simp add: lookup_update)
eberlm@63194
   592
  show "case Mapping.lookup m x of None \<Rightarrow> True | Some v' \<Rightarrow> k = x \<or> P x v'" for x
wenzelm@63462
   593
    using *[of x] by (auto simp add: lookup_update' split: if_splits option.splits)
eberlm@63194
   594
next
eberlm@63194
   595
  assume "P k v"
eberlm@63194
   596
  assume "\<forall>x. case Mapping.lookup m x of None \<Rightarrow> True | Some v' \<Rightarrow> k = x \<or> P x v'"
wenzelm@63462
   597
  then have A: "case Mapping.lookup m x of None \<Rightarrow> True | Some v' \<Rightarrow> k = x \<or> P x v'" for x
wenzelm@63462
   598
    by blast
eberlm@63194
   599
  show "case Mapping.lookup (Mapping.update k v m) x of None \<Rightarrow> True | Some xa \<Rightarrow> P x xa" for x
eberlm@63194
   600
    using \<open>P k v\<close> A[of x] by (auto simp: lookup_update' split: option.splits)
eberlm@63194
   601
qed
eberlm@63194
   602
eberlm@63194
   603
lemma All_mapping_update:
eberlm@63194
   604
  "P k v \<Longrightarrow> All_mapping m (\<lambda>k' v'. k = k' \<or> P k' v') \<Longrightarrow> All_mapping (Mapping.update k v m) P"
eberlm@63194
   605
  by (simp add: All_mapping_update_iff)
eberlm@63194
   606
wenzelm@63462
   607
lemma All_mapping_filter_iff: "All_mapping (filter P m) Q \<longleftrightarrow> All_mapping m (\<lambda>k v. P k v \<longrightarrow> Q k v)"
eberlm@63194
   608
  by (auto simp: All_mapping_def lookup_filter split: option.splits)
eberlm@63194
   609
wenzelm@63462
   610
lemma All_mapping_filter: "All_mapping m Q \<Longrightarrow> All_mapping (filter P m) Q"
eberlm@63194
   611
  by (auto simp: All_mapping_filter_iff intro: All_mapping_mono)
haftmann@31459
   612
wenzelm@63462
   613
lemma All_mapping_map_values: "All_mapping (map_values f m) P \<longleftrightarrow> All_mapping m (\<lambda>k v. P k (f k v))"
eberlm@63194
   614
  by (auto simp: All_mapping_def lookup_map_values split: option.splits)
eberlm@63194
   615
wenzelm@63462
   616
lemma All_mapping_tabulate: "(\<forall>x\<in>set xs. P x (f x)) \<Longrightarrow> All_mapping (Mapping.tabulate xs f) P"
wenzelm@63462
   617
  unfolding All_mapping_def
wenzelm@63462
   618
  apply (intro allI)
wenzelm@63462
   619
  apply transfer
wenzelm@63462
   620
  apply (auto split: option.split dest!: map_of_SomeD)
wenzelm@63462
   621
  done
eberlm@63194
   622
eberlm@63194
   623
lemma All_mapping_alist:
eberlm@63194
   624
  "(\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v) \<Longrightarrow> All_mapping (Mapping.of_alist xs) P"
eberlm@63194
   625
  by (auto simp: All_mapping_def lookup_of_alist dest!: map_of_SomeD split: option.splits)
eberlm@63194
   626
wenzelm@63462
   627
lemma combine_empty [simp]: "combine f Mapping.empty y = y" "combine f y Mapping.empty = y"
wenzelm@63462
   628
  by (transfer; force)+
eberlm@63194
   629
eberlm@63194
   630
lemma (in abel_semigroup) comm_monoid_set_combine: "comm_monoid_set (combine f) Mapping.empty"
eberlm@63194
   631
  by standard (transfer fixing: f, simp add: combine_options_ac[of f] ac_simps)+
eberlm@63194
   632
eberlm@63194
   633
locale combine_mapping_abel_semigroup = abel_semigroup
eberlm@63194
   634
begin
eberlm@63194
   635
eberlm@63194
   636
sublocale combine: comm_monoid_set "combine f" Mapping.empty
eberlm@63194
   637
  by (rule comm_monoid_set_combine)
eberlm@63194
   638
eberlm@63194
   639
lemma fold_combine_code:
eberlm@63194
   640
  "combine.F g (set xs) = foldr (\<lambda>x. combine f (g x)) (remdups xs) Mapping.empty"
eberlm@63194
   641
proof -
eberlm@63194
   642
  have "combine.F g (set xs) = foldr (\<lambda>x. combine f (g x)) xs Mapping.empty"
eberlm@63194
   643
    if "distinct xs" for xs
eberlm@63194
   644
    using that by (induction xs) simp_all
eberlm@63194
   645
  from this[of "remdups xs"] show ?thesis by simp
eberlm@63194
   646
qed
wenzelm@63462
   647
wenzelm@63462
   648
lemma keys_fold_combine: "finite A \<Longrightarrow> Mapping.keys (combine.F g A) = (\<Union>x\<in>A. Mapping.keys (g x))"
wenzelm@63462
   649
  by (induct A rule: finite_induct) simp_all
haftmann@35157
   650
huffman@49975
   651
end
haftmann@59485
   652
wenzelm@63462
   653
eberlm@63194
   654
subsection \<open>Code generator setup\<close>
eberlm@63194
   655
eberlm@63194
   656
hide_const (open) empty is_empty rep lookup lookup_default filter update delete ordered_keys
eberlm@63194
   657
  keys size replace default map_entry map_default tabulate bulkload map map_values combine of_alist
eberlm@63194
   658
eberlm@63194
   659
end