src/HOL/List.thy
changeset 25112 98824cc791c0
parent 25082 c93a234ccf2b
child 25130 d91391a8705b
     1.1 --- a/src/HOL/List.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -950,7 +950,9 @@
     1.4    proof (cases)
     1.5      assume "p x"
     1.6      hence eq: "?S' = insert 0 (Suc ` ?S)"
     1.7 -      by(auto simp add: nth_Cons image_def split:nat.split elim:lessE)
     1.8 +      apply (auto simp add:  nth_Cons image_def neq0_conv split:nat.split elim:lessE)
     1.9 +      apply (rule_tac x="xa - 1" in exI, auto)
    1.10 +      done
    1.11      have "length (filter p (x # xs)) = Suc(card ?S)"
    1.12        using Cons `p x` by simp
    1.13      also have "\<dots> = Suc(card(Suc ` ?S))" using fin
    1.14 @@ -961,7 +963,9 @@
    1.15    next
    1.16      assume "\<not> p x"
    1.17      hence eq: "?S' = Suc ` ?S"
    1.18 -      by(auto simp add: nth_Cons image_def split:nat.split elim:lessE)
    1.19 +      apply(auto simp add: nth_Cons image_def split:nat.split elim:lessE)
    1.20 +      apply (rule_tac x="xa - 1" in exI, auto)
    1.21 +      done
    1.22      have "length (filter p (x # xs)) = card ?S"
    1.23        using Cons `\<not> p x` by simp
    1.24      also have "\<dots> = card(Suc ` ?S)" using fin
    1.25 @@ -2453,7 +2457,7 @@
    1.26  lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
    1.27  apply(induct xs arbitrary: I)
    1.28   apply simp
    1.29 -apply(auto simp add:sublist_Cons nth_Cons split:nat.split elim: lessE)
    1.30 +apply(auto simp add: neq0_conv sublist_Cons nth_Cons split:nat.split elim: lessE)
    1.31   apply(erule lessE)
    1.32    apply auto
    1.33  apply(erule lessE)