# HG changeset patch # User nipkow # Date 1505409692 -7200 # Node ID 59acf5e73176393fcd34d900e3bd4a85f3597bde # Parent 6f82e2ad261a08fffee1ed406b203772c3f8fdc4 two new simp rules diff -r 6f82e2ad261a -r 59acf5e73176 src/HOL/List.thy --- a/src/HOL/List.thy Thu Sep 14 17:36:06 2017 +0200 +++ b/src/HOL/List.thy Thu Sep 14 19:21:32 2017 +0200 @@ -2014,11 +2014,17 @@ subsubsection \@{const take} and @{const drop}\ -lemma take_0 [simp]: "take 0 xs = []" +lemma take_0: "take 0 xs = []" +by (induct xs) auto + +lemma drop_0: "drop 0 xs = xs" by (induct xs) auto -lemma drop_0 [simp]: "drop 0 xs = xs" -by (induct xs) auto +lemma take0[simp]: "take 0 = (\xs. [])" +by(rule ext) (rule take_0) + +lemma drop0[simp]: "drop 0 = (\x. x)" +by(rule ext) (rule drop_0) lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs" by simp