# HG changeset patch # User nipkow # Date 1393861486 -3600 # Node ID 25bd4745ee38ace9fa2388aabece6769f0636d72 # Parent b11b358fec5762373d5bc8af533d59d7fdd19cf5 more code lemmas by Rene Thiemann diff -r b11b358fec57 -r 25bd4745ee38 src/HOL/Library/DAList_Multiset.thy --- 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 \ m1 \ m2 \ m2 \ 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 \ xs \ ys \ \ xs = ys"}. +With equality implemented by @{text"\"}, this leads to three calls of @{text"\"}. +Here is a more efficient version: *} +lemma mset_less[code]: "xs < (ys :: 'a multiset) \ xs \ ys \ \ ys \ xs" +by (rule less_le_not_le) + +lemma mset_less_eq_Bag0: "Bag xs \ A \ (\(x, n) \ set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \ count A x)" (is "?lhs \ ?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 \ count A x" by (cases "x \ fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty) - then show "count (Bag xs) x \ count A x" - by (simp add: mset_le_def) + thus "count (Bag xs) x \ count A x" by (simp add: mset_le_def) qed qed +lemma mset_less_eq_Bag [code]: + "Bag xs \ (A :: 'a multiset) \ (\(x, n) \ set (DAList.impl_of xs). n \ count A x)" +proof - + { + fix x n + assume "(x,n) \ set (DAList.impl_of xs)" + hence "count_of (DAList.impl_of xs) x = n" + proof (transfer) + fix x n and xs :: "('a \ nat) list" + show "(distinct \ map fst) xs \ (x, n) \ set xs \ 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 \ nat \ 'b \ 'b) \ 'b \ ('a \ nat)list \ '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 \ nat \ 'b \ 'b) \ 'b \ ('a, nat)alist \ '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: "\ 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 \ nat)list. (distinct \ map fst) xs}" + note cs[simp del] = count_simps + have count[simp]: "\ x. count (Abs_multiset (count_of x)) = count_of x" + by (rule Abs_multiset_inverse[OF count_of_multiset]) + assume ys: "ys \ ?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 \ ?inv" using Cons(2) by auto + note IH = Cons(1)[OF inv] + def Ys \ "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 \ 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 \ 'b \ ('a,'b)alist" is "\ a b. [(a,b)]" by auto + +lemma image_mset_Bag[code]: + "image_mset f (Bag ms) = + DAList_Multiset.fold (\ 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 + \ single \ 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 "\ = 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 (\ 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 (\ 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 (\ 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 (\ 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 (\ _. 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 (\ 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 (\ a n. (if n = 0 then (\ 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 \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