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