1.1 --- a/src/HOL/Library/Mapping.thy Mon May 24 13:48:56 2010 +0200
1.2 +++ b/src/HOL/Library/Mapping.thy Mon May 24 13:48:57 2010 +0200
1.3 @@ -6,30 +6,6 @@
1.4 imports Main
1.5 begin
1.6
1.7 -lemma remove1_idem: (*FIXME move to List.thy*)
1.8 - assumes "x \<notin> set xs"
1.9 - shows "remove1 x xs = xs"
1.10 - using assms by (induct xs) simp_all
1.11 -
1.12 -lemma remove1_insort [simp]:
1.13 - "remove1 x (insort x xs) = xs"
1.14 - by (induct xs) simp_all
1.15 -
1.16 -lemma sorted_list_of_set_remove:
1.17 - assumes "finite A"
1.18 - shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
1.19 -proof (cases "x \<in> A")
1.20 - case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
1.21 - with False show ?thesis by (simp add: remove1_idem)
1.22 -next
1.23 - case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
1.24 - with assms show ?thesis by simp
1.25 -qed
1.26 -
1.27 -lemma sorted_list_of_set_range [simp]:
1.28 - "sorted_list_of_set {m..<n} = [m..<n]"
1.29 - by (rule sorted_distinct_set_unique) simp_all
1.30 -
1.31 subsection {* Type definition and primitive operations *}
1.32
1.33 datatype ('a, 'b) mapping = Mapping "'a \<rightharpoonup> 'b"
2.1 --- a/src/HOL/Library/Multiset.thy Mon May 24 13:48:56 2010 +0200
2.2 +++ b/src/HOL/Library/Multiset.thy Mon May 24 13:48:57 2010 +0200
2.3 @@ -708,6 +708,14 @@
2.4 "multiset_of [] = {#}" |
2.5 "multiset_of (a # x) = multiset_of x + {# a #}"
2.6
2.7 +lemma in_multiset_in_set:
2.8 + "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
2.9 + by (induct xs) simp_all
2.10 +
2.11 +lemma count_multiset_of:
2.12 + "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
2.13 + by (induct xs) simp_all
2.14 +
2.15 lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
2.16 by (induct x) auto
2.17
2.18 @@ -783,45 +791,29 @@
2.19 by (induct xs) (auto simp add: multiset_ext_iff)
2.20
2.21 lemma multiset_of_eq_length:
2.22 -assumes "multiset_of xs = multiset_of ys"
2.23 -shows "length xs = length ys"
2.24 -using assms
2.25 -proof (induct arbitrary: ys rule: length_induct)
2.26 - case (1 xs ys)
2.27 - show ?case
2.28 - proof (cases xs)
2.29 - case Nil with "1.prems" show ?thesis by simp
2.30 - next
2.31 - case (Cons x xs')
2.32 - note xCons = Cons
2.33 - show ?thesis
2.34 - proof (cases ys)
2.35 - case Nil
2.36 - with "1.prems" Cons show ?thesis by simp
2.37 - next
2.38 - case (Cons y ys')
2.39 - have x_in_ys: "x = y \<or> x \<in> set ys'"
2.40 - proof (cases "x = y")
2.41 - case True then show ?thesis ..
2.42 - next
2.43 - case False
2.44 - from "1.prems" [symmetric] xCons Cons have "x :# multiset_of ys' + {#y#}" by simp
2.45 - with False show ?thesis by (simp add: mem_set_multiset_eq)
2.46 - qed
2.47 - from "1.hyps" have IH: "length xs' < length xs \<longrightarrow>
2.48 - (\<forall>x. multiset_of xs' = multiset_of x \<longrightarrow> length xs' = length x)" by blast
2.49 - from "1.prems" x_in_ys Cons xCons have "multiset_of xs' = multiset_of (remove1 x (y#ys'))"
2.50 - apply -
2.51 - apply (simp add: multiset_of_remove1, simp only: add_eq_conv_diff)
2.52 - apply fastsimp
2.53 - done
2.54 - with IH xCons have IH': "length xs' = length (remove1 x (y#ys'))" by fastsimp
2.55 - from x_in_ys have "x \<noteq> y \<Longrightarrow> length ys' > 0" by auto
2.56 - with Cons xCons x_in_ys IH' show ?thesis by (auto simp add: length_remove1)
2.57 - qed
2.58 - qed
2.59 + assumes "multiset_of xs = multiset_of ys"
2.60 + shows "length xs = length ys"
2.61 +using assms proof (induct xs arbitrary: ys)
2.62 + case Nil then show ?case by simp
2.63 +next
2.64 + case (Cons x xs)
2.65 + then have "x \<in># multiset_of ys" by (simp add: union_single_eq_member)
2.66 + then have "x \<in> set ys" by (simp add: in_multiset_in_set)
2.67 + from Cons.prems [symmetric] have "multiset_of xs = multiset_of (remove1 x ys)"
2.68 + by simp
2.69 + with Cons.hyps have "length xs = length (remove1 x ys)" .
2.70 + with `x \<in> set ys` show ?case
2.71 + by (auto simp add: length_remove1 dest: length_pos_if_in_set)
2.72 qed
2.73
2.74 +lemma (in linorder) multiset_of_insort [simp]:
2.75 + "multiset_of (insort x xs) = {#x#} + multiset_of xs"
2.76 + by (induct xs) (simp_all add: ac_simps)
2.77 +
2.78 +lemma (in linorder) multiset_of_sort [simp]:
2.79 + "multiset_of (sort xs) = multiset_of xs"
2.80 + by (induct xs) (simp_all add: ac_simps)
2.81 +
2.82 text {*
2.83 This lemma shows which properties suffice to show that a function
2.84 @{text "f"} with @{text "f xs = ys"} behaves like sort.
3.1 --- a/src/HOL/List.thy Mon May 24 13:48:56 2010 +0200
3.2 +++ b/src/HOL/List.thy Mon May 24 13:48:57 2010 +0200
3.3 @@ -2970,6 +2970,21 @@
3.4 "List.insert x (remdups xs) = remdups (List.insert x xs)"
3.5 by (simp add: List.insert_def)
3.6
3.7 +lemma distinct_induct [consumes 1, case_names Nil insert]:
3.8 + assumes "distinct xs"
3.9 + assumes "P []"
3.10 + assumes insert: "\<And>x xs. distinct xs \<Longrightarrow> x \<notin> set xs
3.11 + \<Longrightarrow> P xs \<Longrightarrow> P (List.insert x xs)"
3.12 + shows "P xs"
3.13 +using `distinct xs` proof (induct xs)
3.14 + case Nil from `P []` show ?case .
3.15 +next
3.16 + case (Cons x xs)
3.17 + then have "distinct xs" and "x \<notin> set xs" and "P xs" by simp_all
3.18 + with insert have "P (List.insert x xs)" .
3.19 + with `x \<notin> set xs` show ?case by simp
3.20 +qed
3.21 +
3.22
3.23 subsubsection {* @{text remove1} *}
3.24
3.25 @@ -3023,6 +3038,11 @@
3.26 "distinct xs \<Longrightarrow> remove1 x (remdups xs) = remdups (remove1 x xs)"
3.27 by (induct xs) simp_all
3.28
3.29 +lemma remove1_idem:
3.30 + assumes "x \<notin> set xs"
3.31 + shows "remove1 x xs = xs"
3.32 + using assms by (induct xs) simp_all
3.33 +
3.34
3.35 subsubsection {* @{text removeAll} *}
3.36
3.37 @@ -3801,6 +3821,34 @@
3.38 shows "sorted (insort_insert x xs)"
3.39 using assms by (simp add: insort_insert_def sorted_insort)
3.40
3.41 +lemma filter_insort_key_triv:
3.42 + "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
3.43 + by (induct xs) simp_all
3.44 +
3.45 +lemma filter_insort_key:
3.46 + "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
3.47 + using assms by (induct xs)
3.48 + (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
3.49 +
3.50 +lemma filter_sort_key:
3.51 + "filter P (sort_key f xs) = sort_key f (filter P xs)"
3.52 + by (induct xs) (simp_all add: filter_insort_key_triv filter_insort_key)
3.53 +
3.54 +lemma sorted_same [simp]:
3.55 + "sorted [x\<leftarrow>xs. x = f xs]"
3.56 +proof (induct xs arbitrary: f)
3.57 + case Nil then show ?case by simp
3.58 +next
3.59 + case (Cons x xs)
3.60 + then have "sorted [y\<leftarrow>xs . y = (\<lambda>xs. x) xs]" .
3.61 + moreover from Cons have "sorted [y\<leftarrow>xs . y = (f \<circ> Cons x) xs]" .
3.62 + ultimately show ?case by (simp_all add: sorted_Cons)
3.63 +qed
3.64 +
3.65 +lemma remove1_insort [simp]:
3.66 + "remove1 x (insort x xs) = xs"
3.67 + by (induct xs) simp_all
3.68 +
3.69 end
3.70
3.71 lemma sorted_upt[simp]: "sorted[i..<j]"
3.72 @@ -3999,8 +4047,24 @@
3.73 show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
3.74 qed
3.75
3.76 +lemma sorted_list_of_set_remove:
3.77 + assumes "finite A"
3.78 + shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
3.79 +proof (cases "x \<in> A")
3.80 + case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
3.81 + with False show ?thesis by (simp add: remove1_idem)
3.82 +next
3.83 + case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
3.84 + with assms show ?thesis by simp
3.85 +qed
3.86 +
3.87 end
3.88
3.89 +lemma sorted_list_of_set_range [simp]:
3.90 + "sorted_list_of_set {m..<n} = [m..<n]"
3.91 + by (rule sorted_distinct_set_unique) simp_all
3.92 +
3.93 +
3.94
3.95 subsubsection {* @{text lists}: the list-forming operator over sets *}
3.96