summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Mon, 24 May 2010 13:48:57 +0200 | |

changeset 37107 | 1535aa1c943a |

parent 37106 | d56e0b30ce5a |

child 37108 | 00f13d3ad474 |

more lemmas

--- 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 *}