summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/List.thy

changeset 25296 | c187b7422156 |

parent 25287 | 094dab519ff5 |

child 25502 | 9200b36280c0 |

1.1 --- a/src/HOL/List.thy Mon Nov 05 22:48:37 2007 +0100 1.2 +++ b/src/HOL/List.thy Mon Nov 05 22:49:28 2007 +0100 1.3 @@ -1118,6 +1118,25 @@ 1.4 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))" 1.5 by (auto simp add: set_conv_nth) 1.6 1.7 +lemma rev_nth: 1.8 + "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)" 1.9 +proof (induct xs arbitrary: n) 1.10 + case Nil thus ?case by simp 1.11 +next 1.12 + case (Cons x xs) 1.13 + hence n: "n < Suc (length xs)" by simp 1.14 + moreover 1.15 + { assume "n < length xs" 1.16 + with n obtain n' where "length xs - n = Suc n'" 1.17 + by (cases "length xs - n", auto) 1.18 + moreover 1.19 + then have "length xs - Suc n = n'" by simp 1.20 + ultimately 1.21 + have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp 1.22 + } 1.23 + ultimately 1.24 + show ?case by (clarsimp simp add: Cons nth_append) 1.25 +qed 1.26 1.27 subsubsection {* @{text list_update} *} 1.28