removing unnecessary premises in theorems of List theory
authorbulwahn
Thu Feb 16 09:18:23 2012 +0100 (2012-02-16)
changeset 465000196966d6d2d
parent 46499 ee996b8b0e5f
child 46501 fe51817749d1
removing unnecessary premises in theorems of List theory
src/HOL/List.thy
     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"