# HG changeset patch # User nipkow # Date 1217330214 -7200 # Node ID 73253a4e3ee24d1d7cb3ddc7ea91ac8438136bde # Parent c9d461aad7f31f7a42ed1aa46c1ae6f1338c53b6 added removeAll diff -r c9d461aad7f3 -r 73253a4e3ee2 src/HOL/List.thy --- a/src/HOL/List.thy Tue Jul 29 08:15:44 2008 +0200 +++ b/src/HOL/List.thy Tue Jul 29 13:16:54 2008 +0200 @@ -39,6 +39,7 @@ upt :: "nat => nat => nat list" ("(1[_.. 'a list" remove1 :: "'a => 'a list => 'a list" + removeAll :: "'a => 'a list => 'a list" "distinct":: "'a list => bool" replicate :: "nat => 'a => 'a list" splice :: "'a list \ 'a list \ 'a list" @@ -186,6 +187,10 @@ "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)" primrec + "removeAll x [] = []" + "removeAll x (y#xs) = (if x=y then removeAll x xs else y # removeAll x xs)" + +primrec replicate_0: "replicate 0 x = []" replicate_Suc: "replicate (Suc n) x = x # replicate n x" @@ -241,6 +246,7 @@ @{lemma "distinct [2,0,1::nat]" by simp}\\ @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\ @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ +@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ @{lemma "nth [a,b,c,d] 2 = c" by simp}\\ @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\ @@ -2456,6 +2462,41 @@ by (induct xs) simp_all +subsubsection {* @{text removeAll} *} + +lemma removeAll_append[simp]: + "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys" +by (induct xs) auto + +lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}" +by (induct xs) auto + +lemma removeAll_id[simp]: "x \ set xs \ removeAll x xs = xs" +by (induct xs) auto + +(* Needs count:: 'a \ a' list \ nat +lemma length_removeAll: + "length(removeAll x xs) = length xs - count x xs" +*) + +lemma removeAll_filter_not[simp]: + "\ P x \ removeAll x (filter P xs) = filter P xs" +by(induct xs) auto + + +lemma distinct_remove1_removeAll: + "distinct xs ==> remove1 x xs = removeAll x xs" +by (induct xs) simp_all + +lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \ + map f (removeAll x xs) = removeAll (f x) (map f xs)" +by (induct xs) (simp_all add:inj_on_def) + +lemma map_removeAll_inj: "inj f \ + map f (removeAll x xs) = removeAll (f x) (map f xs)" +by(metis map_removeAll_inj_on subset_inj_on subset_UNIV) + + subsubsection {* @{text replicate} *} lemma length_replicate [simp]: "length (replicate n x) = n"