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