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

author | haftmann |

Fri, 17 Sep 2010 20:53:50 +0200 | |

changeset 39534 | c798d4f1b682 |

parent 39533 | 91a0ff0ff237 |

child 39535 | cd1bb7125d8a |

generalized lemma insort_remove1 to insort_key_remove1

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

--- a/src/HOL/List.thy Fri Sep 17 20:53:50 2010 +0200 +++ b/src/HOL/List.thy Fri Sep 17 20:53:50 2010 +0200 @@ -3264,6 +3264,10 @@ apply auto done +lemma replicate_length_filter: + "replicate (length (filter (\<lambda>y. x = y) xs)) x = filter (\<lambda>y. x = y) xs" + by (induct xs) auto + subsubsection{*@{text rotate1} and @{text rotate}*} @@ -3738,24 +3742,43 @@ lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs" by (cases xs) auto +lemma sorted_map_remove1: + "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))" + by (induct xs) (auto simp add: sorted_Cons) + lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)" -by(induct xs)(auto simp add: sorted_Cons) - -lemma insort_key_remove1: "\<lbrakk> a \<in> set xs; sorted (map f xs) ; inj_on f (set xs) \<rbrakk> - \<Longrightarrow> insort_key f a (remove1 a xs) = xs" -proof (induct xs) + using sorted_map_remove1 [of "\<lambda>x. x"] by simp + +lemma insort_key_remove1: + assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a" + shows "insort_key f a (remove1 a xs) = xs" +using assms proof (induct xs) case (Cons x xs) - thus ?case + then show ?case proof (cases "x = a") case False - hence "f x \<noteq> f a" using Cons.prems by auto - hence "f x < f a" using Cons.prems by (auto simp: sorted_Cons) - thus ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons) + then have "f x \<noteq> f a" using Cons.prems by auto + then have "f x < f a" using Cons.prems by (auto simp: sorted_Cons) + with `f x \<noteq> f a` show ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons) qed (auto simp: sorted_Cons insort_is_Cons) qed simp -lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs" -using insort_key_remove1[where f="\<lambda>x. x"] by simp +lemma insort_remove1: + assumes "a \<in> set xs" and "sorted xs" + shows "insort a (remove1 a xs) = xs" +proof (rule insort_key_remove1) + from `a \<in> set xs` show "a \<in> set xs" . + from `sorted xs` show "sorted (map (\<lambda>x. x) xs)" by simp + from `a \<in> set xs` have "a \<in> set (filter (op = a) xs)" by auto + then have "set (filter (op = a) xs) \<noteq> {}" by auto + then have "filter (op = a) xs \<noteq> []" by (auto simp only: set_empty) + then have "length (filter (op = a) xs) > 0" by simp + then obtain n where n: "Suc n = length (filter (op = a) xs)" + by (cases "length (filter (op = a) xs)") simp_all + moreover have "replicate (Suc n) a = a # replicate n a" + by simp + ultimately show "hd (filter (op = a) xs) = a" by (simp add: replicate_length_filter) +qed lemma sorted_remdups[simp]: "sorted l \<Longrightarrow> sorted (remdups l)"