# HG changeset patch
# User haftmann
# Date 1274701737 -7200
# Node ID 1535aa1c943a2c9eb0acb389ba5c8953fdfa79d5
# Parent  d56e0b30ce5a620f896fb42b2ea64619d7332a8f
more lemmas

diff -r d56e0b30ce5a -r 1535aa1c943a src/HOL/Library/Mapping.thy
--- 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"
diff -r d56e0b30ce5a -r 1535aa1c943a src/HOL/Library/Multiset.thy
--- 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.
diff -r d56e0b30ce5a -r 1535aa1c943a src/HOL/List.thy
--- 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 *}