# HG changeset patch
# User kleing
# Date 1194299368 -3600
# Node ID c187b7422156fc1ddc730721fdb01a6c51001256
# Parent  12985023be5e43f742d5c8af4308736b30b92e53
rev_nth

diff -r 12985023be5e -r c187b7422156 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 05 22:48:37 2007 +0100
+++ b/src/HOL/List.thy	Mon Nov 05 22:49:28 2007 +0100
@@ -1118,6 +1118,25 @@
 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))"
 by (auto simp add: set_conv_nth)
 
+lemma rev_nth:
+  "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
+proof (induct xs arbitrary: n)
+  case Nil thus ?case by simp
+next
+  case (Cons x xs)
+  hence n: "n < Suc (length xs)" by simp
+  moreover
+  { assume "n < length xs"
+    with n obtain n' where "length xs - n = Suc n'"
+      by (cases "length xs - n", auto)
+    moreover
+    then have "length xs - Suc n = n'" by simp
+    ultimately
+    have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
+  }
+  ultimately
+  show ?case by (clarsimp simp add: Cons nth_append)
+qed
 
 subsubsection {* @{text list_update} *}