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