| changeset 41842 | d8f76db6a207 |
| parent 41697 | 19890332febc |
| child 41986 | 95a67e3f29ad |
--- a/src/HOL/List.thy Fri Feb 25 08:46:52 2011 +0100 +++ b/src/HOL/List.thy Fri Feb 25 14:25:41 2011 +0100 @@ -1321,6 +1321,9 @@ declare nth.simps [simp del] +lemma nth_Cons_pos[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)" +by(auto simp: Nat.gr0_conv_Suc) + lemma nth_append: "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))" apply (induct xs arbitrary: n, simp)