equal
deleted
inserted
replaced
959 by (simp add:card_insert_if) (simp add:image_def) |
959 by (simp add:card_insert_if) (simp add:image_def) |
960 finally show ?thesis . |
960 finally show ?thesis . |
961 next |
961 next |
962 assume "\<not> p x" |
962 assume "\<not> p x" |
963 hence eq: "?S' = Suc ` ?S" |
963 hence eq: "?S' = Suc ` ?S" |
964 apply(auto simp add: nth_Cons image_def split:nat.split elim:lessE) |
964 by(auto simp add: image_def neq0_conv split:nat.split elim:lessE) |
965 apply (rule_tac x="xa - 1" in exI, auto) |
|
966 done |
|
967 have "length (filter p (x # xs)) = card ?S" |
965 have "length (filter p (x # xs)) = card ?S" |
968 using Cons `\<not> p x` by simp |
966 using Cons `\<not> p x` by simp |
969 also have "\<dots> = card(Suc ` ?S)" using fin |
967 also have "\<dots> = card(Suc ` ?S)" using fin |
970 by (simp add: card_image inj_Suc) |
968 by (simp add: card_image inj_Suc) |
971 also have "\<dots> = card ?S'" using eq fin |
969 also have "\<dots> = card ?S'" using eq fin |