summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | kleing |

Mon, 05 Nov 2007 22:49:28 +0100 | |

changeset 25296 | c187b7422156 |

parent 25295 | 12985023be5e |

child 25297 | a5d689d04426 |

rev_nth

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- 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} *}