author | nipkow |

Thu Sep 14 19:21:32 2017 +0200 (21 months ago) | |

changeset 66658 | 59acf5e73176 |

parent 66657 | 6f82e2ad261a |

child 66659 | d5bf4bdb4fb7 |

two new simp rules

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