src/HOL/List.thy
changeset 44921 58eef4843641
parent 44916 840d8c3d9113
child 44928 7ef6505bde7f
     1.1 --- a/src/HOL/List.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/List.thy	Tue Sep 13 17:07:33 2011 -0700
     1.3 @@ -1176,7 +1176,7 @@
     1.4      have "length (filter p (x # xs)) = Suc(card ?S)"
     1.5        using Cons `p x` by simp
     1.6      also have "\<dots> = Suc(card(Suc ` ?S))" using fin
     1.7 -      by (simp add: card_image inj_Suc)
     1.8 +      by (simp add: card_image)
     1.9      also have "\<dots> = card ?S'" using eq fin
    1.10        by (simp add:card_insert_if) (simp add:image_def)
    1.11      finally show ?thesis .
    1.12 @@ -1187,7 +1187,7 @@
    1.13      have "length (filter p (x # xs)) = card ?S"
    1.14        using Cons `\<not> p x` by simp
    1.15      also have "\<dots> = card(Suc ` ?S)" using fin
    1.16 -      by (simp add: card_image inj_Suc)
    1.17 +      by (simp add: card_image)
    1.18      also have "\<dots> = card ?S'" using eq fin
    1.19        by (simp add:card_insert_if)
    1.20      finally show ?thesis .
    1.21 @@ -1529,10 +1529,10 @@
    1.22  by (induct xs) auto
    1.23  
    1.24  lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
    1.25 -by(simp add:last.simps)
    1.26 +  by simp
    1.27  
    1.28  lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
    1.29 -by(simp add:last.simps)
    1.30 +  by simp
    1.31  
    1.32  lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
    1.33  by (induct xs) (auto)
    1.34 @@ -2627,7 +2627,7 @@
    1.35  lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
    1.36  apply (induct n m  arbitrary: i rule: diff_induct)
    1.37  prefer 3 apply (subst map_Suc_upt[symmetric])
    1.38 -apply (auto simp add: less_diff_conv nth_upt)
    1.39 +apply (auto simp add: less_diff_conv)
    1.40  done
    1.41  
    1.42  lemma nth_take_lemma:
    1.43 @@ -2647,9 +2647,7 @@
    1.44  
    1.45  lemma nth_equalityI:
    1.46   "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
    1.47 -apply (frule nth_take_lemma [OF le_refl eq_imp_le])
    1.48 -apply (simp_all add: take_all)
    1.49 -done
    1.50 +  by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
    1.51  
    1.52  lemma map_nth:
    1.53    "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
    1.54 @@ -2666,7 +2664,7 @@
    1.55  lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
    1.56  -- {* The famous take-lemma. *}
    1.57  apply (drule_tac x = "max (length xs) (length ys)" in spec)
    1.58 -apply (simp add: le_max_iff_disj take_all)
    1.59 +apply (simp add: le_max_iff_disj)
    1.60  done
    1.61  
    1.62  
    1.63 @@ -2880,8 +2878,8 @@
    1.64  done
    1.65  
    1.66  lemma length_remdups_concat:
    1.67 - "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
    1.68 -by(simp add: set_concat distinct_card[symmetric])
    1.69 +  "length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
    1.70 +  by (simp add: distinct_card [symmetric])
    1.71  
    1.72  lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)"
    1.73  proof -
    1.74 @@ -3519,7 +3517,7 @@
    1.75       "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
    1.76  apply (unfold sublist_def)
    1.77  apply (induct l' rule: rev_induct, simp)
    1.78 -apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
    1.79 +apply (simp add: upt_add_eq_append[of 0] sublist_shift_lemma)
    1.80  apply (simp add: add_commute)
    1.81  done
    1.82  
    1.83 @@ -3838,7 +3836,7 @@
    1.84  by(induct xs)(auto simp:set_insort)
    1.85  
    1.86  lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
    1.87 -by(induct xs)(simp_all add:distinct_insort set_sort)
    1.88 +  by (induct xs) (simp_all add: distinct_insort)
    1.89  
    1.90  lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
    1.91    by (induct xs) (auto simp:sorted_Cons set_insort)