src/HOL/List.thy
changeset 39073 8520a1f89db1
parent 38857 97775f3e8722
child 39198 f967a16dfcdd
equal deleted inserted replaced
39072:1030b1a166ef 39073:8520a1f89db1
  3074 
  3074 
  3075 lemma remove1_filter_not[simp]:
  3075 lemma remove1_filter_not[simp]:
  3076   "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
  3076   "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
  3077 by(induct xs) auto
  3077 by(induct xs) auto
  3078 
  3078 
       
  3079 lemma filter_remove1:
       
  3080   "filter Q (remove1 x xs) = remove1 x (filter Q xs)"
       
  3081 by (induct xs) auto
       
  3082 
  3079 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
  3083 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
  3080 apply(insert set_remove1_subset)
  3084 apply(insert set_remove1_subset)
  3081 apply fast
  3085 apply fast
  3082 done
  3086 done
  3083 
  3087