--- a/src/HOL/Library/DAList_Multiset.thy Mon Mar 03 15:14:00 2014 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy Mon Mar 03 16:44:46 2014 +0100
@@ -231,12 +231,17 @@
lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le> m2 \<and> m2 \<le> m1"
by (metis equal_multiset_def eq_iff)
-lemma mset_less_eq_Bag [code]:
+text{* By default the code for @{text "<"} is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
+With equality implemented by @{text"\<le>"}, this leads to three calls of @{text"\<le>"}.
+Here is a more efficient version: *}
+lemma mset_less[code]: "xs < (ys :: 'a multiset) \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+by (rule less_le_not_le)
+
+lemma mset_less_eq_Bag0:
"Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
- assume ?lhs then show ?rhs
- by (auto simp add: mset_le_def)
+ assume ?lhs thus ?rhs by (auto simp add: mset_le_def)
next
assume ?rhs
show ?lhs
@@ -244,15 +249,177 @@
fix x
from `?rhs` have "count_of (DAList.impl_of xs) x \<le> count A x"
by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
- then show "count (Bag xs) x \<le> count A x"
- by (simp add: mset_le_def)
+ thus "count (Bag xs) x \<le> count A x" by (simp add: mset_le_def)
qed
qed
+lemma mset_less_eq_Bag [code]:
+ "Bag xs \<le> (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
+proof -
+ {
+ fix x n
+ assume "(x,n) \<in> set (DAList.impl_of xs)"
+ hence "count_of (DAList.impl_of xs) x = n"
+ proof (transfer)
+ fix x n and xs :: "('a \<times> nat) list"
+ show "(distinct \<circ> map fst) xs \<Longrightarrow> (x, n) \<in> set xs \<Longrightarrow> count_of xs x = n"
+ proof (induct xs)
+ case (Cons ym ys)
+ obtain y m where ym: "ym = (y,m)" by force
+ note Cons = Cons[unfolded ym]
+ show ?case
+ proof (cases "x = y")
+ case False
+ with Cons show ?thesis unfolding ym by auto
+ next
+ case True
+ with Cons(2-3) have "m = n" by force
+ with True show ?thesis unfolding ym by auto
+ qed
+ qed auto
+ qed
+ }
+ thus ?thesis unfolding mset_less_eq_Bag0 by auto
+qed
+
declare multiset_inter_def [code]
declare sup_multiset_def [code]
declare multiset_of.simps [code]
+
+fun fold_impl :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<times> nat)list \<Rightarrow> 'b" where
+ "fold_impl fn e ((a,n) # ms) = (fold_impl fn ((fn a n) e) ms)"
+| "fold_impl fn e [] = e"
+
+definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat)alist \<Rightarrow> 'b" where
+"fold f e al = fold_impl f e (DAList.impl_of al)"
+
+hide_const (open) fold
+
+context comp_fun_commute
+begin
+
+lemma DAList_Multiset_fold: assumes fn: "\<And> a n x. fn a n x = (f a ^^ n) x"
+ shows "Multiset.fold f e (Bag al) = DAList_Multiset.fold fn e al"
+unfolding DAList_Multiset.fold_def
+proof (induct al)
+ fix ys
+ let ?inv = "{xs :: ('a \<times> nat)list. (distinct \<circ> map fst) xs}"
+ note cs[simp del] = count_simps
+ have count[simp]: "\<And> x. count (Abs_multiset (count_of x)) = count_of x"
+ by (rule Abs_multiset_inverse[OF count_of_multiset])
+ assume ys: "ys \<in> ?inv"
+ thus "Multiset.fold f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))"
+ unfolding Bag_def unfolding Alist_inverse[OF ys]
+ proof (induct ys arbitrary: e rule: list.induct)
+ case Nil
+ show ?case
+ by (rule trans[OF arg_cong[of _ "{#}" "Multiset.fold f e", OF multiset_eqI]])
+ (auto, simp add: cs)
+ next
+ case (Cons pair ys e)
+ obtain a n where pair: "pair = (a,n)" by force
+ from fn[of a n] have [simp]: "fn a n = (f a ^^ n)" by auto
+ have inv: "ys \<in> ?inv" using Cons(2) by auto
+ note IH = Cons(1)[OF inv]
+ def Ys \<equiv> "Abs_multiset (count_of ys)"
+ have id: "Abs_multiset (count_of ((a, n) # ys)) = ((op + {# a #}) ^^ n) Ys"
+ unfolding Ys_def
+ proof (rule multiset_eqI, unfold count)
+ fix c
+ show "count_of ((a, n) # ys) c = count ((op + {#a#} ^^ n) (Abs_multiset (count_of ys))) c" (is "?l = ?r")
+ proof (cases "c = a")
+ case False thus ?thesis unfolding cs by (induct n) auto
+ next
+ case True
+ hence "?l = n" by (simp add: cs)
+ also have "n = ?r" unfolding True
+ proof (induct n)
+ case 0
+ from Cons(2)[unfolded pair] have "a \<notin> fst ` set ys" by auto
+ thus ?case by (induct ys) (simp, auto simp: cs)
+ qed auto
+ finally show ?thesis .
+ qed
+ qed
+ show ?case unfolding pair
+ by (simp add: IH[symmetric], unfold id Ys_def[symmetric],
+ induct n, auto simp: fold_mset_fun_left_comm[symmetric])
+ qed
+qed
+
+end
+
+lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a,'b)alist" is "\<lambda> a b. [(a,b)]" by auto
+
+lemma image_mset_Bag[code]:
+ "image_mset f (Bag ms) =
+ DAList_Multiset.fold (\<lambda> a n m. Bag (single_alist_entry (f a) n) + m) {#} ms"
+unfolding image_mset_def
+proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1])
+ fix a n m
+ show "Bag (single_alist_entry (f a) n) + m = ((op + \<circ> single \<circ> f) a ^^ n) m" (is "?l = ?r")
+ proof (rule multiset_eqI)
+ fix x
+ have "count ?r x = (if x = f a then n + count m x else count m x)"
+ by (induct n, auto)
+ also have "\<dots> = count ?l x" by (simp add: single_alist_entry.rep_eq)
+ finally show "count ?l x = count ?r x" ..
+ qed
+qed
+
+hide_const single_alist_entry
+
+(* we cannot use (\<lambda> a n. op + (a * n)) for folding, since * is not defined
+ in comm_monoid_add *)
+lemma msetsum_Bag[code]:
+ "msetsum (Bag ms) = DAList_Multiset.fold (\<lambda> a n. ((op + a) ^^ n)) 0 ms"
+unfolding msetsum.eq_fold
+by (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, auto simp: ac_simps)
+
+(* we cannot use (\<lambda> a n. op * (a ^ n)) for folding, since ^ is not defined
+ in comm_monoid_mult *)
+lemma msetprod_Bag[code]:
+ "msetprod (Bag ms) = DAList_Multiset.fold (\<lambda> a n. ((op * a) ^^ n)) 1 ms"
+unfolding msetprod.eq_fold
+by (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, auto simp: ac_simps)
+
+lemma mcard_fold: "mcard A = Multiset.fold (\<lambda> _. Suc) 0 A" (is "_ = Multiset.fold ?f _ _")
+proof -
+ interpret comp_fun_commute ?f by (default, auto)
+ show ?thesis by (induct A) auto
+qed
+
+lemma mcard_Bag[code]:
+ "mcard (Bag ms) = DAList_Multiset.fold (\<lambda> a n. op + n) 0 ms"
+unfolding mcard_fold
+proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, simp)
+ fix a n x
+ show "n + x = (Suc ^^ n) x" by (induct n) auto
+qed
+
+
+lemma set_of_fold: "set_of A = Multiset.fold insert {} A" (is "_ = Multiset.fold ?f _ _")
+proof -
+ interpret comp_fun_commute ?f by (default, auto)
+ show ?thesis by (induct A, auto)
+qed
+
+lemma set_of_Bag[code]:
+ "set_of (Bag ms) = DAList_Multiset.fold (\<lambda> a n. (if n = 0 then (\<lambda> m. m) else insert a)) {} ms"
+unfolding set_of_fold
+proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1])
+ fix a n x
+ show "(if n = 0 then \<lambda>m. m else insert a) x = (insert a ^^ n) x" (is "?l n = ?r n")
+ proof (cases n)
+ case (Suc m)
+ hence "?l n = insert a x" by simp
+ moreover have "?r n = insert a x" unfolding Suc by (induct m) auto
+ ultimately show ?thesis by auto
+ qed auto
+qed
+
+
instantiation multiset :: (exhaustive) exhaustive
begin