1.1 --- a/src/HOL/List.thy	Tue Jul 29 08:15:44 2008 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Jul 29 13:16:54 2008 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    upt :: "nat => nat => nat list" ("(1[_..</_'])")
     1.5    remdups :: "'a list => 'a list"
     1.6    remove1 :: "'a => 'a list => 'a list"
     1.7 +  removeAll :: "'a => 'a list => 'a list"
     1.8    "distinct":: "'a list => bool"
     1.9    replicate :: "nat => 'a => 'a list"
    1.10    splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.11 @@ -186,6 +187,10 @@
    1.12    "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
    1.13  
    1.14  primrec
    1.15 +  "removeAll x [] = []"
    1.16 +  "removeAll x (y#xs) = (if x=y then removeAll x xs else y # removeAll x xs)"
    1.17 +
    1.18 +primrec
    1.19    replicate_0: "replicate 0 x = []"
    1.20    replicate_Suc: "replicate (Suc n) x = x # replicate n x"
    1.21  
    1.22 @@ -241,6 +246,7 @@
    1.23  @{lemma "distinct [2,0,1::nat]" by simp}\\
    1.24  @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
    1.25  @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
    1.26 +@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
    1.27  @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
    1.28  @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
    1.29  @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
    1.30 @@ -2456,6 +2462,41 @@
    1.31  by (induct xs) simp_all
    1.32  
    1.33  
    1.34 +subsubsection {* @{text removeAll} *}
    1.35 +
    1.36 +lemma removeAll_append[simp]:
    1.37 +  "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
    1.38 +by (induct xs) auto
    1.39 +
    1.40 +lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
    1.41 +by (induct xs) auto
    1.42 +
    1.43 +lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
    1.44 +by (induct xs) auto
    1.45 +
    1.46 +(* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
    1.47 +lemma length_removeAll:
    1.48 +  "length(removeAll x xs) = length xs - count x xs"
    1.49 +*)
    1.50 +
    1.51 +lemma removeAll_filter_not[simp]:
    1.52 +  "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
    1.53 +by(induct xs) auto
    1.54 +
    1.55 +
    1.56 +lemma distinct_remove1_removeAll:
    1.57 +  "distinct xs ==> remove1 x xs = removeAll x xs"
    1.58 +by (induct xs) simp_all
    1.59 +
    1.60 +lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \<Longrightarrow>
    1.61 +  map f (removeAll x xs) = removeAll (f x) (map f xs)"
    1.62 +by (induct xs) (simp_all add:inj_on_def)
    1.63 +
    1.64 +lemma map_removeAll_inj: "inj f \<Longrightarrow>
    1.65 +  map f (removeAll x xs) = removeAll (f x) (map f xs)"
    1.66 +by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
    1.67 +
    1.68 +
    1.69  subsubsection {* @{text replicate} *}
    1.70  
    1.71  lemma length_replicate [simp]: "length (replicate n x) = n"