two new simp rules
authornipkow
Thu Sep 14 19:21:32 2017 +0200 (21 months ago)
changeset 6665859acf5e73176
parent 66657 6f82e2ad261a
child 66659 d5bf4bdb4fb7
two new simp rules
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Thu Sep 14 17:36:06 2017 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Sep 14 19:21:32 2017 +0200
     1.3 @@ -2014,11 +2014,17 @@
     1.4  
     1.5  subsubsection \<open>@{const take} and @{const drop}\<close>
     1.6  
     1.7 -lemma take_0 [simp]: "take 0 xs = []"
     1.8 +lemma take_0: "take 0 xs = []"
     1.9 +by (induct xs) auto
    1.10 +
    1.11 +lemma drop_0: "drop 0 xs = xs"
    1.12  by (induct xs) auto
    1.13  
    1.14 -lemma drop_0 [simp]: "drop 0 xs = xs"
    1.15 -by (induct xs) auto
    1.16 +lemma take0[simp]: "take 0 = (\<lambda>xs. [])"
    1.17 +by(rule ext) (rule take_0)
    1.18 +
    1.19 +lemma drop0[simp]: "drop 0 = (\<lambda>x. x)"
    1.20 +by(rule ext) (rule drop_0)
    1.21  
    1.22  lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
    1.23  by simp