src/HOL/Library/DAList_Multiset.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64587 8355a6e2df79
child 66148 5e60c2d0a1f1
permissions -rw-r--r--
executable domain membership checks
haftmann@51599
     1
(*  Title:      HOL/Library/DAList_Multiset.thy
haftmann@51599
     2
    Author:     Lukas Bulwahn, TU Muenchen
haftmann@51599
     3
*)
haftmann@51599
     4
wenzelm@58881
     5
section \<open>Multisets partially implemented by association lists\<close>
haftmann@51599
     6
haftmann@51599
     7
theory DAList_Multiset
haftmann@51599
     8
imports Multiset DAList
haftmann@51599
     9
begin
haftmann@51599
    10
wenzelm@58806
    11
text \<open>Delete prexisting code equations\<close>
haftmann@51600
    12
wenzelm@58806
    13
lemma [code, code del]: "{#} = {#}" ..
haftmann@51623
    14
eberlm@63195
    15
lemma [code, code del]: "Multiset.is_empty = Multiset.is_empty" ..
eberlm@63195
    16
Mathias@63793
    17
lemma [code, code del]: "add_mset = add_mset" ..
haftmann@51623
    18
wenzelm@58806
    19
lemma [code, code del]: "plus = (plus :: 'a multiset \<Rightarrow> _)" ..
haftmann@51600
    20
wenzelm@58806
    21
lemma [code, code del]: "minus = (minus :: 'a multiset \<Rightarrow> _)" ..
haftmann@51600
    22
Mathias@60397
    23
lemma [code, code del]: "inf_subset_mset = (inf_subset_mset :: 'a multiset \<Rightarrow> _)" ..
haftmann@51600
    24
Mathias@60397
    25
lemma [code, code del]: "sup_subset_mset = (sup_subset_mset :: 'a multiset \<Rightarrow> _)" ..
haftmann@51623
    26
wenzelm@58806
    27
lemma [code, code del]: "image_mset = image_mset" ..
haftmann@51600
    28
nipkow@59998
    29
lemma [code, code del]: "filter_mset = filter_mset" ..
haftmann@51600
    30
wenzelm@58806
    31
lemma [code, code del]: "count = count" ..
haftmann@51600
    32
nipkow@59949
    33
lemma [code, code del]: "size = (size :: _ multiset \<Rightarrow> nat)" ..
haftmann@51600
    34
nipkow@63830
    35
lemma [code, code del]: "sum_mset = sum_mset" ..
haftmann@51600
    36
nipkow@63830
    37
lemma [code, code del]: "prod_mset = prod_mset" ..
haftmann@51600
    38
nipkow@60495
    39
lemma [code, code del]: "set_mset = set_mset" ..
haftmann@51600
    40
wenzelm@58806
    41
lemma [code, code del]: "sorted_list_of_multiset = sorted_list_of_multiset" ..
haftmann@51600
    42
Mathias@60397
    43
lemma [code, code del]: "subset_mset = subset_mset" ..
nipkow@55808
    44
Mathias@60397
    45
lemma [code, code del]: "subseteq_mset = subseteq_mset" ..
nipkow@55808
    46
wenzelm@58806
    47
lemma [code, code del]: "equal_multiset_inst.equal_multiset = equal_multiset_inst.equal_multiset" ..
nipkow@55808
    48
haftmann@51600
    49
wenzelm@58806
    50
text \<open>Raw operations on lists\<close>
haftmann@51599
    51
wenzelm@58806
    52
definition join_raw ::
wenzelm@58806
    53
    "('key \<Rightarrow> 'val \<times> 'val \<Rightarrow> 'val) \<Rightarrow>
wenzelm@58806
    54
      ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@58806
    55
  where "join_raw f xs ys = foldr (\<lambda>(k, v). map_default k v (\<lambda>v'. f k (v', v))) ys xs"
haftmann@51599
    56
wenzelm@58806
    57
lemma join_raw_Nil [simp]: "join_raw f xs [] = xs"
wenzelm@58806
    58
  by (simp add: join_raw_def)
haftmann@51599
    59
haftmann@51599
    60
lemma join_raw_Cons [simp]:
wenzelm@58806
    61
  "join_raw f xs ((k, v) # ys) = map_default k v (\<lambda>v'. f k (v', v)) (join_raw f xs ys)"
wenzelm@58806
    62
  by (simp add: join_raw_def)
haftmann@51599
    63
haftmann@51599
    64
lemma map_of_join_raw:
haftmann@51599
    65
  assumes "distinct (map fst ys)"
wenzelm@58806
    66
  shows "map_of (join_raw f xs ys) x =
wenzelm@58806
    67
    (case map_of xs x of
wenzelm@58806
    68
      None \<Rightarrow> map_of ys x
wenzelm@58806
    69
    | Some v \<Rightarrow> (case map_of ys x of None \<Rightarrow> Some v | Some v' \<Rightarrow> Some (f x (v, v'))))"
wenzelm@58806
    70
  using assms
wenzelm@58806
    71
  apply (induct ys)
wenzelm@58806
    72
  apply (auto simp add: map_of_map_default split: option.split)
wenzelm@58806
    73
  apply (metis map_of_eq_None_iff option.simps(2) weak_map_of_SomeI)
wenzelm@58806
    74
  apply (metis Some_eq_map_of_iff map_of_eq_None_iff option.simps(2))
wenzelm@58806
    75
  done
haftmann@51599
    76
haftmann@51599
    77
lemma distinct_join_raw:
haftmann@51599
    78
  assumes "distinct (map fst xs)"
haftmann@51599
    79
  shows "distinct (map fst (join_raw f xs ys))"
wenzelm@58806
    80
  using assms
haftmann@51599
    81
proof (induct ys)
wenzelm@58806
    82
  case Nil
wenzelm@58806
    83
  then show ?case by simp
wenzelm@58806
    84
next
haftmann@51599
    85
  case (Cons y ys)
wenzelm@58806
    86
  then show ?case by (cases y) (simp add: distinct_map_default)
wenzelm@58806
    87
qed
haftmann@51599
    88
wenzelm@58806
    89
definition "subtract_entries_raw xs ys = foldr (\<lambda>(k, v). AList.map_entry k (\<lambda>v'. v' - v)) ys xs"
haftmann@51599
    90
haftmann@51599
    91
lemma map_of_subtract_entries_raw:
haftmann@51599
    92
  assumes "distinct (map fst ys)"
wenzelm@58806
    93
  shows "map_of (subtract_entries_raw xs ys) x =
wenzelm@58806
    94
    (case map_of xs x of
wenzelm@58806
    95
      None \<Rightarrow> None
wenzelm@58806
    96
    | Some v \<Rightarrow> (case map_of ys x of None \<Rightarrow> Some v | Some v' \<Rightarrow> Some (v - v')))"
wenzelm@58806
    97
  using assms
wenzelm@58806
    98
  unfolding subtract_entries_raw_def
wenzelm@58806
    99
  apply (induct ys)
wenzelm@58806
   100
  apply auto
wenzelm@58806
   101
  apply (simp split: option.split)
wenzelm@58806
   102
  apply (simp add: map_of_map_entry)
wenzelm@58806
   103
  apply (auto split: option.split)
wenzelm@58806
   104
  apply (metis map_of_eq_None_iff option.simps(3) option.simps(4))
wenzelm@58806
   105
  apply (metis map_of_eq_None_iff option.simps(4) option.simps(5))
wenzelm@58806
   106
  done
haftmann@51599
   107
haftmann@51599
   108
lemma distinct_subtract_entries_raw:
haftmann@51599
   109
  assumes "distinct (map fst xs)"
haftmann@51599
   110
  shows "distinct (map fst (subtract_entries_raw xs ys))"
wenzelm@58806
   111
  using assms
wenzelm@58806
   112
  unfolding subtract_entries_raw_def
wenzelm@58806
   113
  by (induct ys) (auto simp add: distinct_map_entry)
haftmann@51599
   114
haftmann@51599
   115
wenzelm@58806
   116
text \<open>Operations on alists with distinct keys\<close>
haftmann@51599
   117
wenzelm@58806
   118
lift_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
wenzelm@58806
   119
  is join_raw
wenzelm@58806
   120
  by (simp add: distinct_join_raw)
haftmann@51599
   121
haftmann@51599
   122
lift_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
wenzelm@58806
   123
  is subtract_entries_raw
wenzelm@58806
   124
  by (simp add: distinct_subtract_entries_raw)
haftmann@51599
   125
haftmann@51599
   126
wenzelm@58806
   127
text \<open>Implementing multisets by means of association lists\<close>
haftmann@51599
   128
wenzelm@58806
   129
definition count_of :: "('a \<times> nat) list \<Rightarrow> 'a \<Rightarrow> nat"
wenzelm@58806
   130
  where "count_of xs x = (case map_of xs x of None \<Rightarrow> 0 | Some n \<Rightarrow> n)"
wenzelm@58806
   131
wenzelm@58806
   132
lemma count_of_multiset: "count_of xs \<in> multiset"
haftmann@51599
   133
proof -
wenzelm@58806
   134
  let ?A = "{x::'a. 0 < (case map_of xs x of None \<Rightarrow> 0::nat | Some n \<Rightarrow> n)}"
haftmann@51599
   135
  have "?A \<subseteq> dom (map_of xs)"
haftmann@51599
   136
  proof
haftmann@51599
   137
    fix x
haftmann@51599
   138
    assume "x \<in> ?A"
wenzelm@58806
   139
    then have "0 < (case map_of xs x of None \<Rightarrow> 0::nat | Some n \<Rightarrow> n)"
wenzelm@58806
   140
      by simp
wenzelm@58806
   141
    then have "map_of xs x \<noteq> None"
wenzelm@58806
   142
      by (cases "map_of xs x") auto
wenzelm@58806
   143
    then show "x \<in> dom (map_of xs)"
wenzelm@58806
   144
      by auto
haftmann@51599
   145
  qed
haftmann@51599
   146
  with finite_dom_map_of [of xs] have "finite ?A"
haftmann@51599
   147
    by (auto intro: finite_subset)
haftmann@51599
   148
  then show ?thesis
haftmann@51599
   149
    by (simp add: count_of_def fun_eq_iff multiset_def)
haftmann@51599
   150
qed
haftmann@51599
   151
haftmann@51599
   152
lemma count_simps [simp]:
haftmann@51599
   153
  "count_of [] = (\<lambda>_. 0)"
haftmann@51599
   154
  "count_of ((x, n) # xs) = (\<lambda>y. if x = y then n else count_of xs y)"
haftmann@51599
   155
  by (simp_all add: count_of_def fun_eq_iff)
haftmann@51599
   156
wenzelm@58806
   157
lemma count_of_empty: "x \<notin> fst ` set xs \<Longrightarrow> count_of xs x = 0"
haftmann@51599
   158
  by (induct xs) (simp_all add: count_of_def)
haftmann@51599
   159
wenzelm@58806
   160
lemma count_of_filter: "count_of (List.filter (P \<circ> fst) xs) x = (if P x then count_of xs x else 0)"
haftmann@51599
   161
  by (induct xs) auto
haftmann@51599
   162
haftmann@51599
   163
lemma count_of_map_default [simp]:
wenzelm@58806
   164
  "count_of (map_default x b (\<lambda>x. x + b) xs) y =
wenzelm@58806
   165
    (if x = y then count_of xs x + b else count_of xs y)"
wenzelm@58806
   166
  unfolding count_of_def by (simp add: map_of_map_default split: option.split)
haftmann@51599
   167
haftmann@51599
   168
lemma count_of_join_raw:
wenzelm@58806
   169
  "distinct (map fst ys) \<Longrightarrow>
wenzelm@58806
   170
    count_of xs x + count_of ys x = count_of (join_raw (\<lambda>x (x, y). x + y) xs ys) x"
wenzelm@58806
   171
  unfolding count_of_def by (simp add: map_of_join_raw split: option.split)
haftmann@51599
   172
haftmann@51599
   173
lemma count_of_subtract_entries_raw:
wenzelm@58806
   174
  "distinct (map fst ys) \<Longrightarrow>
wenzelm@58806
   175
    count_of xs x - count_of ys x = count_of (subtract_entries_raw xs ys) x"
wenzelm@58806
   176
  unfolding count_of_def by (simp add: map_of_subtract_entries_raw split: option.split)
haftmann@51599
   177
haftmann@51599
   178
wenzelm@58806
   179
text \<open>Code equations for multiset operations\<close>
haftmann@51599
   180
wenzelm@58806
   181
definition Bag :: "('a, nat) alist \<Rightarrow> 'a multiset"
wenzelm@58806
   182
  where "Bag xs = Abs_multiset (count_of (DAList.impl_of xs))"
haftmann@51599
   183
haftmann@51599
   184
code_datatype Bag
haftmann@51599
   185
wenzelm@58806
   186
lemma count_Bag [simp, code]: "count (Bag xs) = count_of (DAList.impl_of xs)"
wenzelm@58806
   187
  by (simp add: Bag_def count_of_multiset)
haftmann@51599
   188
wenzelm@58806
   189
lemma Mempty_Bag [code]: "{#} = Bag (DAList.empty)"
haftmann@51599
   190
  by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def)
haftmann@51599
   191
eberlm@63195
   192
lift_definition is_empty_Bag_impl :: "('a, nat) alist \<Rightarrow> bool" is
eberlm@63195
   193
  "\<lambda>xs. list_all (\<lambda>x. snd x = 0) xs" .
eberlm@63195
   194
eberlm@63195
   195
lemma is_empty_Bag [code]: "Multiset.is_empty (Bag xs) \<longleftrightarrow> is_empty_Bag_impl xs"
eberlm@63195
   196
proof -
eberlm@63195
   197
  have "Multiset.is_empty (Bag xs) \<longleftrightarrow> (\<forall>x. count (Bag xs) x = 0)"
eberlm@63195
   198
    unfolding Multiset.is_empty_def multiset_eq_iff by simp
eberlm@63195
   199
  also have "\<dots> \<longleftrightarrow> (\<forall>x\<in>fst ` set (alist.impl_of xs). count (Bag xs) x = 0)"
eberlm@63195
   200
  proof (intro iffI allI ballI)
eberlm@63195
   201
    fix x assume A: "\<forall>x\<in>fst ` set (alist.impl_of xs). count (Bag xs) x = 0"
eberlm@63195
   202
    thus "count (Bag xs) x = 0"
eberlm@63195
   203
    proof (cases "x \<in> fst ` set (alist.impl_of xs)")
eberlm@63195
   204
      case False
eberlm@63195
   205
      thus ?thesis by (force simp: count_of_def split: option.splits)
eberlm@63195
   206
    qed (insert A, auto)
eberlm@63195
   207
  qed simp_all
eberlm@63195
   208
  also have "\<dots> \<longleftrightarrow> list_all (\<lambda>x. snd x = 0) (alist.impl_of xs)" 
eberlm@63195
   209
    by (auto simp: count_of_def list_all_def)
eberlm@63195
   210
  finally show ?thesis by (simp add: is_empty_Bag_impl.rep_eq)
eberlm@63195
   211
qed
eberlm@63195
   212
wenzelm@58806
   213
lemma union_Bag [code]: "Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)"
wenzelm@58806
   214
  by (rule multiset_eqI)
wenzelm@58806
   215
    (simp add: count_of_join_raw alist.Alist_inverse distinct_join_raw join_def)
haftmann@51599
   216
Mathias@63793
   217
lemma add_mset_Bag [code]: "add_mset x (Bag xs) =
Mathias@63793
   218
    Bag (join (\<lambda>x (n1, n2). n1 + n2) (DAList.update x 1 DAList.empty) xs)"
Mathias@63793
   219
  unfolding add_mset_add_single[of x "Bag xs"] union_Bag[symmetric]
Mathias@63793
   220
  by (simp add: multiset_eq_iff update.rep_eq empty.rep_eq)
Mathias@63793
   221
wenzelm@58806
   222
lemma minus_Bag [code]: "Bag xs - Bag ys = Bag (subtract_entries xs ys)"
wenzelm@58806
   223
  by (rule multiset_eqI)
wenzelm@58806
   224
    (simp add: count_of_subtract_entries_raw alist.Alist_inverse
wenzelm@58806
   225
      distinct_subtract_entries_raw subtract_entries_def)
haftmann@51599
   226
nipkow@59998
   227
lemma filter_Bag [code]: "filter_mset P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
wenzelm@58806
   228
  by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
haftmann@51599
   229
nipkow@55808
   230
haftmann@64587
   231
lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<subseteq># m2 \<and> m2 \<subseteq># m1"
Mathias@60397
   232
  by (metis equal_multiset_def subset_mset.eq_iff)
nipkow@55808
   233
wenzelm@61585
   234
text \<open>By default the code for \<open><\<close> is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
wenzelm@61585
   235
With equality implemented by \<open>\<le>\<close>, this leads to three calls of  \<open>\<le>\<close>.
wenzelm@58806
   236
Here is a more efficient version:\<close>
haftmann@64587
   237
lemma mset_less[code]: "xs \<subset># (ys :: 'a multiset) \<longleftrightarrow> xs \<subseteq># ys \<and> \<not> ys \<subseteq># xs"
Mathias@60397
   238
  by (rule subset_mset.less_le_not_le)
nipkow@55887
   239
nipkow@55887
   240
lemma mset_less_eq_Bag0:
haftmann@64587
   241
  "Bag xs \<subseteq># A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
haftmann@51599
   242
    (is "?lhs \<longleftrightarrow> ?rhs")
haftmann@51599
   243
proof
wenzelm@58806
   244
  assume ?lhs
Mathias@60397
   245
  then show ?rhs by (auto simp add: subseteq_mset_def)
haftmann@51599
   246
next
haftmann@51599
   247
  assume ?rhs
haftmann@51599
   248
  show ?lhs
Mathias@63310
   249
  proof (rule mset_subset_eqI)
haftmann@51599
   250
    fix x
wenzelm@58806
   251
    from \<open>?rhs\<close> have "count_of (DAList.impl_of xs) x \<le> count A x"
haftmann@51599
   252
      by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
Mathias@60397
   253
    then show "count (Bag xs) x \<le> count A x" by (simp add: subset_mset_def)
haftmann@51599
   254
  qed
haftmann@51599
   255
qed
haftmann@51599
   256
nipkow@55887
   257
lemma mset_less_eq_Bag [code]:
haftmann@64587
   258
  "Bag xs \<subseteq># (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
nipkow@55887
   259
proof -
nipkow@55887
   260
  {
nipkow@55887
   261
    fix x n
nipkow@55887
   262
    assume "(x,n) \<in> set (DAList.impl_of xs)"
wenzelm@58806
   263
    then have "count_of (DAList.impl_of xs) x = n"
wenzelm@58806
   264
    proof transfer
wenzelm@58806
   265
      fix x n
wenzelm@58806
   266
      fix xs :: "('a \<times> nat) list"
nipkow@55887
   267
      show "(distinct \<circ> map fst) xs \<Longrightarrow> (x, n) \<in> set xs \<Longrightarrow> count_of xs x = n"
wenzelm@58806
   268
      proof (induct xs)
wenzelm@58806
   269
        case Nil
wenzelm@58806
   270
        then show ?case by simp
wenzelm@58806
   271
      next
wenzelm@58806
   272
        case (Cons ym ys)
nipkow@55887
   273
        obtain y m where ym: "ym = (y,m)" by force
nipkow@55887
   274
        note Cons = Cons[unfolded ym]
nipkow@55887
   275
        show ?case
nipkow@55887
   276
        proof (cases "x = y")
nipkow@55887
   277
          case False
wenzelm@58806
   278
          with Cons show ?thesis
wenzelm@58806
   279
            unfolding ym by auto
nipkow@55887
   280
        next
nipkow@55887
   281
          case True
nipkow@55887
   282
          with Cons(2-3) have "m = n" by force
wenzelm@58806
   283
          with True show ?thesis
wenzelm@58806
   284
            unfolding ym by auto
nipkow@55887
   285
        qed
wenzelm@58806
   286
      qed
nipkow@55887
   287
    qed
nipkow@55887
   288
  }
wenzelm@58806
   289
  then show ?thesis
wenzelm@58806
   290
    unfolding mset_less_eq_Bag0 by auto
nipkow@55887
   291
qed
nipkow@55887
   292
haftmann@51600
   293
declare multiset_inter_def [code]
Mathias@60397
   294
declare sup_subset_mset_def [code]
nipkow@60515
   295
declare mset.simps [code]
haftmann@51600
   296
nipkow@55887
   297
wenzelm@58806
   298
fun fold_impl :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<times> nat) list \<Rightarrow> 'b"
wenzelm@58806
   299
where
nipkow@55887
   300
  "fold_impl fn e ((a,n) # ms) = (fold_impl fn ((fn a n) e) ms)"
nipkow@55887
   301
| "fold_impl fn e [] = e"
nipkow@55887
   302
wenzelm@61115
   303
context
wenzelm@61115
   304
begin
wenzelm@61115
   305
wenzelm@61115
   306
qualified definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat) alist \<Rightarrow> 'b"
wenzelm@58806
   307
  where "fold f e al = fold_impl f e (DAList.impl_of al)"
nipkow@55887
   308
wenzelm@61115
   309
end
nipkow@55887
   310
nipkow@55887
   311
context comp_fun_commute
nipkow@55887
   312
begin
nipkow@55887
   313
wenzelm@58806
   314
lemma DAList_Multiset_fold:
wenzelm@58806
   315
  assumes fn: "\<And>a n x. fn a n x = (f a ^^ n) x"
nipkow@59998
   316
  shows "fold_mset f e (Bag al) = DAList_Multiset.fold fn e al"
wenzelm@58806
   317
  unfolding DAList_Multiset.fold_def
nipkow@55887
   318
proof (induct al)
nipkow@55887
   319
  fix ys
wenzelm@58806
   320
  let ?inv = "{xs :: ('a \<times> nat) list. (distinct \<circ> map fst) xs}"
nipkow@55887
   321
  note cs[simp del] = count_simps
wenzelm@58806
   322
  have count[simp]: "\<And>x. count (Abs_multiset (count_of x)) = count_of x"
nipkow@55887
   323
    by (rule Abs_multiset_inverse[OF count_of_multiset])
nipkow@55887
   324
  assume ys: "ys \<in> ?inv"
nipkow@59998
   325
  then show "fold_mset f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))"
nipkow@55887
   326
    unfolding Bag_def unfolding Alist_inverse[OF ys]
nipkow@55887
   327
  proof (induct ys arbitrary: e rule: list.induct)
nipkow@55887
   328
    case Nil
nipkow@55887
   329
    show ?case
nipkow@59998
   330
      by (rule trans[OF arg_cong[of _ "{#}" "fold_mset f e", OF multiset_eqI]])
nipkow@55887
   331
         (auto, simp add: cs)
nipkow@55887
   332
  next
nipkow@55887
   333
    case (Cons pair ys e)
wenzelm@58806
   334
    obtain a n where pair: "pair = (a,n)"
wenzelm@58806
   335
      by force
wenzelm@58806
   336
    from fn[of a n] have [simp]: "fn a n = (f a ^^ n)"
wenzelm@58806
   337
      by auto
wenzelm@58806
   338
    have inv: "ys \<in> ?inv"
wenzelm@58806
   339
      using Cons(2) by auto
nipkow@55887
   340
    note IH = Cons(1)[OF inv]
wenzelm@63040
   341
    define Ys where "Ys = Abs_multiset (count_of ys)"
nipkow@55887
   342
    have id: "Abs_multiset (count_of ((a, n) # ys)) = ((op + {# a #}) ^^ n) Ys"
nipkow@55887
   343
      unfolding Ys_def
nipkow@55887
   344
    proof (rule multiset_eqI, unfold count)
wenzelm@58806
   345
      fix c
wenzelm@58806
   346
      show "count_of ((a, n) # ys) c =
wenzelm@58806
   347
        count ((op + {#a#} ^^ n) (Abs_multiset (count_of ys))) c" (is "?l = ?r")
nipkow@55887
   348
      proof (cases "c = a")
wenzelm@58806
   349
        case False
wenzelm@58806
   350
        then show ?thesis
wenzelm@58806
   351
          unfolding cs by (induct n) auto
nipkow@55887
   352
      next
nipkow@55887
   353
        case True
wenzelm@58806
   354
        then have "?l = n" by (simp add: cs)
nipkow@55887
   355
        also have "n = ?r" unfolding True
nipkow@55887
   356
        proof (induct n)
nipkow@55887
   357
          case 0
nipkow@55887
   358
          from Cons(2)[unfolded pair] have "a \<notin> fst ` set ys" by auto
wenzelm@58806
   359
          then show ?case by (induct ys) (simp, auto simp: cs)
wenzelm@58806
   360
        next
wenzelm@58806
   361
          case Suc
wenzelm@58806
   362
          then show ?case by simp
wenzelm@58806
   363
        qed
nipkow@55887
   364
        finally show ?thesis .
nipkow@55887
   365
      qed
nipkow@55887
   366
    qed
wenzelm@58806
   367
    show ?case
wenzelm@58806
   368
      unfolding pair
wenzelm@58806
   369
      apply (simp add: IH[symmetric])
wenzelm@58806
   370
      unfolding id Ys_def[symmetric]
wenzelm@58806
   371
      apply (induct n)
wenzelm@58806
   372
      apply (auto simp: fold_mset_fun_left_comm[symmetric])
wenzelm@58806
   373
      done
nipkow@55887
   374
  qed
nipkow@55887
   375
qed
nipkow@55887
   376
wenzelm@58806
   377
end
nipkow@55887
   378
wenzelm@61115
   379
context
wenzelm@61115
   380
begin
wenzelm@61115
   381
wenzelm@61115
   382
private lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) alist" is "\<lambda>a b. [(a, b)]"
wenzelm@58806
   383
  by auto
nipkow@55887
   384
wenzelm@58806
   385
lemma image_mset_Bag [code]:
nipkow@55887
   386
  "image_mset f (Bag ms) =
wenzelm@58806
   387
    DAList_Multiset.fold (\<lambda>a n m. Bag (single_alist_entry (f a) n) + m) {#} ms"
wenzelm@58806
   388
  unfolding image_mset_def
nipkow@55887
   389
proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1])
nipkow@55887
   390
  fix a n m
Mathias@63793
   391
  show "Bag (single_alist_entry (f a) n) + m = ((add_mset \<circ> f) a ^^ n) m" (is "?l = ?r")
nipkow@55887
   392
  proof (rule multiset_eqI)
nipkow@55887
   393
    fix x
nipkow@55887
   394
    have "count ?r x = (if x = f a then n + count m x else count m x)"
wenzelm@58806
   395
      by (induct n) auto
wenzelm@58806
   396
    also have "\<dots> = count ?l x"
wenzelm@58806
   397
      by (simp add: single_alist_entry.rep_eq)
nipkow@55887
   398
    finally show "count ?l x = count ?r x" ..
nipkow@55887
   399
  qed
nipkow@55887
   400
qed
nipkow@55887
   401
wenzelm@61115
   402
end
nipkow@55887
   403
wenzelm@58806
   404
(* we cannot use (\<lambda>a n. op + (a * n)) for folding, since * is not defined
nipkow@55887
   405
   in comm_monoid_add *)
nipkow@63830
   406
lemma sum_mset_Bag[code]: "sum_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((op + a) ^^ n)) 0 ms"
nipkow@63830
   407
  unfolding sum_mset.eq_fold
wenzelm@58806
   408
  apply (rule comp_fun_commute.DAList_Multiset_fold)
wenzelm@58806
   409
  apply unfold_locales
wenzelm@58806
   410
  apply (auto simp: ac_simps)
wenzelm@58806
   411
  done
nipkow@55887
   412
wenzelm@58806
   413
(* we cannot use (\<lambda>a n. op * (a ^ n)) for folding, since ^ is not defined
nipkow@55887
   414
   in comm_monoid_mult *)
nipkow@63830
   415
lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((op * a) ^^ n)) 1 ms"
nipkow@63830
   416
  unfolding prod_mset.eq_fold
wenzelm@58806
   417
  apply (rule comp_fun_commute.DAList_Multiset_fold)
wenzelm@58806
   418
  apply unfold_locales
wenzelm@58806
   419
  apply (auto simp: ac_simps)
wenzelm@58806
   420
  done
nipkow@55887
   421
nipkow@59998
   422
lemma size_fold: "size A = fold_mset (\<lambda>_. Suc) 0 A" (is "_ = fold_mset ?f _ _")
nipkow@55887
   423
proof -
wenzelm@60679
   424
  interpret comp_fun_commute ?f by standard auto
nipkow@55887
   425
  show ?thesis by (induct A) auto
nipkow@55887
   426
qed
nipkow@55887
   427
nipkow@59949
   428
lemma size_Bag[code]: "size (Bag ms) = DAList_Multiset.fold (\<lambda>a n. op + n) 0 ms"
nipkow@59949
   429
  unfolding size_fold
nipkow@55887
   430
proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, simp)
nipkow@55887
   431
  fix a n x
wenzelm@58806
   432
  show "n + x = (Suc ^^ n) x"
wenzelm@58806
   433
    by (induct n) auto
nipkow@55887
   434
qed
nipkow@55887
   435
nipkow@55887
   436
nipkow@60495
   437
lemma set_mset_fold: "set_mset A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
nipkow@55887
   438
proof -
wenzelm@60679
   439
  interpret comp_fun_commute ?f by standard auto
wenzelm@58806
   440
  show ?thesis by (induct A) auto
nipkow@55887
   441
qed
nipkow@55887
   442
nipkow@60495
   443
lemma set_mset_Bag[code]:
nipkow@60495
   444
  "set_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (if n = 0 then (\<lambda>m. m) else insert a)) {} ms"
nipkow@60495
   445
  unfolding set_mset_fold
nipkow@55887
   446
proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1])
nipkow@55887
   447
  fix a n x
nipkow@55887
   448
  show "(if n = 0 then \<lambda>m. m else insert a) x = (insert a ^^ n) x" (is "?l n = ?r n")
nipkow@55887
   449
  proof (cases n)
wenzelm@58806
   450
    case 0
wenzelm@58806
   451
    then show ?thesis by simp
wenzelm@58806
   452
  next
nipkow@55887
   453
    case (Suc m)
wenzelm@58806
   454
    then have "?l n = insert a x" by simp
nipkow@55887
   455
    moreover have "?r n = insert a x" unfolding Suc by (induct m) auto
nipkow@55887
   456
    ultimately show ?thesis by auto
wenzelm@58806
   457
  qed
nipkow@55887
   458
qed
nipkow@55887
   459
nipkow@55887
   460
haftmann@51600
   461
instantiation multiset :: (exhaustive) exhaustive
haftmann@51599
   462
begin
haftmann@51599
   463
wenzelm@58806
   464
definition exhaustive_multiset ::
wenzelm@58806
   465
  "('a multiset \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
wenzelm@58806
   466
  where "exhaustive_multiset f i = Quickcheck_Exhaustive.exhaustive (\<lambda>xs. f (Bag xs)) i"
haftmann@51599
   467
haftmann@51599
   468
instance ..
haftmann@51599
   469
haftmann@51599
   470
end
haftmann@51599
   471
haftmann@51599
   472
end
haftmann@51599
   473