summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/List.thy

changeset 46500 | 0196966d6d2d |

parent 46448 | f1201fac7398 |

child 46635 | cde737f9c911 |

1.1 --- a/src/HOL/List.thy Thu Feb 16 09:18:21 2012 +0100 1.2 +++ b/src/HOL/List.thy Thu Feb 16 09:18:23 2012 +0100 1.3 @@ -1801,7 +1801,7 @@ 1.4 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)" 1.5 by (simp add: butlast_conv_take drop_take add_ac) 1.6 1.7 -lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n" 1.8 +lemma hd_drop_conv_nth: "n < length xs \<Longrightarrow> hd(drop n xs) = xs!n" 1.9 by(simp add: hd_conv_nth) 1.10 1.11 lemma set_take_subset_set_take: 1.12 @@ -2040,7 +2040,7 @@ 1.13 done 1.14 1.15 lemma takeWhile_not_last: 1.16 - "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs" 1.17 + "distinct xs \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs" 1.18 apply(induct xs) 1.19 apply simp 1.20 apply(case_tac xs) 1.21 @@ -2110,7 +2110,7 @@ 1.22 by (induct xs ys rule:list_induct2') auto 1.23 1.24 lemma zip_append [simp]: 1.25 - "[| length xs = length us; length ys = length vs |] ==> 1.26 + "[| length xs = length us |] ==> 1.27 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs" 1.28 by (simp add: zip_append1) 1.29 1.30 @@ -3056,12 +3056,13 @@ 1.31 by (induct xs) simp_all 1.32 1.33 lemma distinct_butlast: 1.34 - assumes "xs \<noteq> []" and "distinct xs" 1.35 + assumes "distinct xs" 1.36 shows "distinct (butlast xs)" 1.37 -proof - 1.38 - from `xs \<noteq> []` obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto 1.39 - with `distinct xs` show ?thesis by simp 1.40 -qed 1.41 +proof (cases "xs = []") 1.42 + case False 1.43 + from `xs \<noteq> []` obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto 1.44 + with `distinct xs` show ?thesis by simp 1.45 +qed (auto) 1.46 1.47 lemma remdups_map_remdups: 1.48 "remdups (map f (remdups xs)) = remdups (map f xs)" 1.49 @@ -3440,7 +3441,7 @@ 1.50 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x" 1.51 by (induct n) auto 1.52 1.53 -lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x" 1.54 +lemma tl_replicate [simp]: "tl (replicate n x) = replicate (n - 1) x" 1.55 by (induct n) auto 1.56 1.57 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"