author | haftmann |

Mon May 24 13:48:57 2010 +0200 (2010-05-24) | |

changeset 37107 | 1535aa1c943a |

parent 37106 | d56e0b30ce5a |

child 37108 | 00f13d3ad474 |

more lemmas

src/HOL/Library/Mapping.thy | file | annotate | diff | revisions | |

src/HOL/Library/Multiset.thy | file | annotate | diff | revisions | |

src/HOL/List.thy | file | annotate | diff | revisions |

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