--- a/src/HOL/Library/DAList_Multiset.thy Fri Feb 28 17:31:19 2014 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy Fri Feb 28 18:11:11 2014 +0100
@@ -66,6 +66,18 @@
"sorted_list_of_multiset = sorted_list_of_multiset"
..
+lemma [code, code del]:
+ "ord_multiset_inst.less_eq_multiset = ord_multiset_inst.less_eq_multiset"
+ ..
+
+lemma [code, code del]:
+ "ord_multiset_inst.less_multiset = ord_multiset_inst.less_multiset"
+ ..
+
+lemma [code, code del]:
+ "equal_multiset_inst.equal_multiset = equal_multiset_inst.equal_multiset"
+ ..
+
text {* Raw operations on lists *}
@@ -215,6 +227,10 @@
"Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
+
+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]:
"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")
--- a/src/HOL/Library/Multiset.thy Fri Feb 28 17:31:19 2014 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Feb 28 18:11:11 2014 +0100
@@ -358,6 +358,12 @@
lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
by (auto simp add: mset_less_def mset_le_def multiset_eq_iff)
+lemma empty_le[simp]: "{#} \<le> A"
+ unfolding mset_le_exists_conv by auto
+
+lemma le_empty[simp]: "(M \<le> {#}) = (M = {#})"
+ unfolding mset_le_exists_conv by auto
+
lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
by (auto simp: mset_le_def mset_less_def)
@@ -561,6 +567,9 @@
lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
unfolding set_of_def[symmetric] by simp
+lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"
+ by (metis mset_leD subsetI mem_set_of_iff)
+
subsubsection {* Size *}
instantiation multiset :: (type) size
@@ -2083,26 +2092,70 @@
"mcard (multiset_of xs) = length xs"
by (simp add: mcard_multiset_of)
-lemma [code]:
- "A \<le> B \<longleftrightarrow> A #\<inter> B = A"
- by (auto simp add: inf.order_iff)
+fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
+ "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
+| "ms_lesseq_impl (Cons x xs) ys = (case List.extract (op = x) ys of
+ None \<Rightarrow> None
+ | Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
+
+lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le> multiset_of ys) \<and>
+ (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs < multiset_of ys) \<and>
+ (ms_lesseq_impl xs ys = Some False \<longrightarrow> multiset_of xs = multiset_of ys)"
+proof (induct xs arbitrary: ys)
+ case (Nil ys)
+ show ?case by (auto simp: mset_less_empty_nonempty)
+next
+ case (Cons x xs ys)
+ show ?case
+ proof (cases "List.extract (op = x) ys")
+ case None
+ hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
+ {
+ assume "multiset_of (x # xs) \<le> multiset_of ys"
+ from set_of_mono[OF this] x have False by simp
+ } note nle = this
+ moreover
+ {
+ assume "multiset_of (x # xs) < multiset_of ys"
+ hence "multiset_of (x # xs) \<le> multiset_of ys" by auto
+ from nle[OF this] have False .
+ }
+ ultimately show ?thesis using None by auto
+ next
+ case (Some res)
+ obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto)
+ note Some = Some[unfolded res]
+ from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
+ hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}"
+ by (auto simp: ac_simps)
+ show ?thesis unfolding ms_lesseq_impl.simps
+ unfolding Some option.simps split
+ unfolding id
+ using Cons[of "ys1 @ ys2"]
+ unfolding mset_le_def mset_less_def by auto
+ qed
+qed
+
+lemma [code]: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
+ using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
+
+lemma [code]: "multiset_of xs < multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
+ using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
instantiation multiset :: (equal) equal
begin
definition
- [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
+ [code del]: "HOL.equal A (B :: 'a multiset) \<longleftrightarrow> A = B"
+lemma [code]: "HOL.equal (multiset_of xs) (multiset_of ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
+ unfolding equal_multiset_def
+ using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
instance
- by default (simp add: equal_multiset_def eq_iff)
-
+ by default (simp add: equal_multiset_def)
end
lemma [code]:
- "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
- by auto
-
-lemma [code]:
"msetsum (multiset_of xs) = listsum xs"
by (induct xs) (simp_all add: add.commute)
--- a/src/HOL/List.thy Fri Feb 28 17:31:19 2014 +0100
+++ b/src/HOL/List.thy Fri Feb 28 18:11:11 2014 +0100
@@ -182,6 +182,15 @@
hide_const (open) find
+definition
+ "extract" :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> ('a list * 'a * 'a list) option"
+where "extract P xs =
+ (case dropWhile (Not o P) xs of
+ [] \<Rightarrow> None |
+ y#ys \<Rightarrow> Some(takeWhile (Not o P) xs, y, ys))"
+
+hide_const (open) "extract"
+
primrec those :: "'a option list \<Rightarrow> 'a list option"
where
"those [] = Some []" |
@@ -287,6 +296,8 @@
@{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\
@{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\
@{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\
+@{lemma "List.extract (%i::int. i>0) [0,0] = None" by(simp add: extract_def)}\\
+@{lemma "List.extract (%i::int. i>0) [0,1,0,2] = Some([0], 1, [0,2])" by(simp add: extract_def)}\\
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\
@@ -3648,6 +3659,34 @@
by (induct xs) simp_all
+subsubsection {* @{const List.extract} *}
+
+lemma extract_None_iff: "List.extract P xs = None \<longleftrightarrow> \<not> (\<exists> x\<in>set xs. P x)"
+by(auto simp: extract_def dropWhile_eq_Cons_conv split: list.splits)
+ (metis in_set_conv_decomp)
+
+lemma extract_SomeE:
+ "List.extract P xs = Some (ys, y, zs) \<Longrightarrow>
+ xs = ys @ y # zs \<and> P y \<and> \<not> (\<exists> y \<in> set ys. P y)"
+by(auto simp: extract_def dropWhile_eq_Cons_conv split: list.splits)
+
+lemma extract_Some_iff:
+ "List.extract P xs = Some (ys, y, zs) \<longleftrightarrow>
+ xs = ys @ y # zs \<and> P y \<and> \<not> (\<exists> y \<in> set ys. P y)"
+by(auto simp: extract_def dropWhile_eq_Cons_conv dest: set_takeWhileD split: list.splits)
+
+lemma extract_Nil_code[code]: "List.extract P [] = None"
+by(simp add: extract_def)
+
+lemma extract_Cons_code[code]:
+ "List.extract P (x # xs) = (if P x then Some ([], x, xs) else
+ (case List.extract P xs of
+ None \<Rightarrow> None |
+ Some (ys, y, zs) \<Rightarrow> Some (x#ys, y, zs)))"
+by(auto simp add: extract_def split: list.splits)
+ (metis comp_def dropWhile_eq_Nil_conv list.distinct(1))
+
+
subsubsection {* @{const remove1} *}
lemma remove1_append: