--- a/src/HOL/Library/Mapping.thy Mon May 24 13:48:56 2010 +0200
+++ b/src/HOL/Library/Mapping.thy Mon May 24 13:48:57 2010 +0200
@@ -6,30 +6,6 @@
imports Main
begin
-lemma remove1_idem: (*FIXME move to List.thy*)
- assumes "x \<notin> set xs"
- shows "remove1 x xs = xs"
- using assms by (induct xs) simp_all
-
-lemma remove1_insort [simp]:
- "remove1 x (insort x xs) = xs"
- by (induct xs) simp_all
-
-lemma sorted_list_of_set_remove:
- assumes "finite A"
- shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
-proof (cases "x \<in> A")
- case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
- with False show ?thesis by (simp add: remove1_idem)
-next
- case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
- with assms show ?thesis by simp
-qed
-
-lemma sorted_list_of_set_range [simp]:
- "sorted_list_of_set {m..<n} = [m..<n]"
- by (rule sorted_distinct_set_unique) simp_all
-
subsection {* Type definition and primitive operations *}
datatype ('a, 'b) mapping = Mapping "'a \<rightharpoonup> 'b"
--- a/src/HOL/Library/Multiset.thy Mon May 24 13:48:56 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Mon May 24 13:48:57 2010 +0200
@@ -708,6 +708,14 @@
"multiset_of [] = {#}" |
"multiset_of (a # x) = multiset_of x + {# a #}"
+lemma in_multiset_in_set:
+ "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
+ by (induct xs) simp_all
+
+lemma count_multiset_of:
+ "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
+ by (induct xs) simp_all
+
lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
by (induct x) auto
@@ -783,45 +791,29 @@
by (induct xs) (auto simp add: multiset_ext_iff)
lemma multiset_of_eq_length:
-assumes "multiset_of xs = multiset_of ys"
-shows "length xs = length ys"
-using assms
-proof (induct arbitrary: ys rule: length_induct)
- case (1 xs ys)
- show ?case
- proof (cases xs)
- case Nil with "1.prems" show ?thesis by simp
- next
- case (Cons x xs')
- note xCons = Cons
- show ?thesis
- proof (cases ys)
- case Nil
- with "1.prems" Cons show ?thesis by simp
- next
- case (Cons y ys')
- have x_in_ys: "x = y \<or> x \<in> set ys'"
- proof (cases "x = y")
- case True then show ?thesis ..
- next
- case False
- from "1.prems" [symmetric] xCons Cons have "x :# multiset_of ys' + {#y#}" by simp
- with False show ?thesis by (simp add: mem_set_multiset_eq)
- qed
- from "1.hyps" have IH: "length xs' < length xs \<longrightarrow>
- (\<forall>x. multiset_of xs' = multiset_of x \<longrightarrow> length xs' = length x)" by blast
- from "1.prems" x_in_ys Cons xCons have "multiset_of xs' = multiset_of (remove1 x (y#ys'))"
- apply -
- apply (simp add: multiset_of_remove1, simp only: add_eq_conv_diff)
- apply fastsimp
- done
- with IH xCons have IH': "length xs' = length (remove1 x (y#ys'))" by fastsimp
- from x_in_ys have "x \<noteq> y \<Longrightarrow> length ys' > 0" by auto
- with Cons xCons x_in_ys IH' show ?thesis by (auto simp add: length_remove1)
- qed
- qed
+ assumes "multiset_of xs = multiset_of ys"
+ shows "length xs = length ys"
+using assms proof (induct xs arbitrary: ys)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs)
+ then have "x \<in># multiset_of ys" by (simp add: union_single_eq_member)
+ then have "x \<in> set ys" by (simp add: in_multiset_in_set)
+ from Cons.prems [symmetric] have "multiset_of xs = multiset_of (remove1 x ys)"
+ by simp
+ with Cons.hyps have "length xs = length (remove1 x ys)" .
+ with `x \<in> set ys` show ?case
+ by (auto simp add: length_remove1 dest: length_pos_if_in_set)
qed
+lemma (in linorder) multiset_of_insort [simp]:
+ "multiset_of (insort x xs) = {#x#} + multiset_of xs"
+ by (induct xs) (simp_all add: ac_simps)
+
+lemma (in linorder) multiset_of_sort [simp]:
+ "multiset_of (sort xs) = multiset_of xs"
+ by (induct xs) (simp_all add: ac_simps)
+
text {*
This lemma shows which properties suffice to show that a function
@{text "f"} with @{text "f xs = ys"} behaves like sort.
--- a/src/HOL/List.thy Mon May 24 13:48:56 2010 +0200
+++ b/src/HOL/List.thy Mon May 24 13:48:57 2010 +0200
@@ -2970,6 +2970,21 @@
"List.insert x (remdups xs) = remdups (List.insert x xs)"
by (simp add: List.insert_def)
+lemma distinct_induct [consumes 1, case_names Nil insert]:
+ assumes "distinct xs"
+ assumes "P []"
+ assumes insert: "\<And>x xs. distinct xs \<Longrightarrow> x \<notin> set xs
+ \<Longrightarrow> P xs \<Longrightarrow> P (List.insert x xs)"
+ shows "P xs"
+using `distinct xs` proof (induct xs)
+ case Nil from `P []` show ?case .
+next
+ case (Cons x xs)
+ then have "distinct xs" and "x \<notin> set xs" and "P xs" by simp_all
+ with insert have "P (List.insert x xs)" .
+ with `x \<notin> set xs` show ?case by simp
+qed
+
subsubsection {* @{text remove1} *}
@@ -3023,6 +3038,11 @@
"distinct xs \<Longrightarrow> remove1 x (remdups xs) = remdups (remove1 x xs)"
by (induct xs) simp_all
+lemma remove1_idem:
+ assumes "x \<notin> set xs"
+ shows "remove1 x xs = xs"
+ using assms by (induct xs) simp_all
+
subsubsection {* @{text removeAll} *}
@@ -3801,6 +3821,34 @@
shows "sorted (insort_insert x xs)"
using assms by (simp add: insort_insert_def sorted_insort)
+lemma filter_insort_key_triv:
+ "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
+ by (induct xs) simp_all
+
+lemma filter_insort_key:
+ "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
+ using assms by (induct xs)
+ (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
+
+lemma filter_sort_key:
+ "filter P (sort_key f xs) = sort_key f (filter P xs)"
+ by (induct xs) (simp_all add: filter_insort_key_triv filter_insort_key)
+
+lemma sorted_same [simp]:
+ "sorted [x\<leftarrow>xs. x = f xs]"
+proof (induct xs arbitrary: f)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs)
+ then have "sorted [y\<leftarrow>xs . y = (\<lambda>xs. x) xs]" .
+ moreover from Cons have "sorted [y\<leftarrow>xs . y = (f \<circ> Cons x) xs]" .
+ ultimately show ?case by (simp_all add: sorted_Cons)
+qed
+
+lemma remove1_insort [simp]:
+ "remove1 x (insort x xs) = xs"
+ by (induct xs) simp_all
+
end
lemma sorted_upt[simp]: "sorted[i..<j]"
@@ -3999,8 +4047,24 @@
show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
qed
+lemma sorted_list_of_set_remove:
+ assumes "finite A"
+ shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
+proof (cases "x \<in> A")
+ case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
+ with False show ?thesis by (simp add: remove1_idem)
+next
+ case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
+ with assms show ?thesis by simp
+qed
+
end
+lemma sorted_list_of_set_range [simp]:
+ "sorted_list_of_set {m..<n} = [m..<n]"
+ by (rule sorted_distinct_set_unique) simp_all
+
+
subsubsection {* @{text lists}: the list-forming operator over sets *}