# HG changeset patch
# User nipkow
# Date 1242374517 -7200
# Node ID bac0d673b6d669bb06eb547b8f7faa3004bf0668
# Parent  722459e60ea536b24e8f4f1f15925648579552bf
new lemma

diff -r 722459e60ea5 -r bac0d673b6d6 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 14 21:57:03 2009 +0200
+++ b/src/HOL/List.thy	Fri May 15 10:01:57 2009 +0200
@@ -1299,6 +1299,25 @@
   show ?case by (clarsimp simp add: Cons nth_append)
 qed
 
+lemma Skolem_list_nth:
+  "(ALL i<k. EX x. P i x) = (EX xs. size xs = k & (ALL i<k. P i (xs!i)))"
+  (is "_ = (EX xs. ?P k xs)")
+proof(induct k)
+  case 0 show ?case by simp
+next
+  case (Suc k)
+  show ?case (is "?L = ?R" is "_ = (EX xs. ?P' xs)")
+  proof
+    assume "?R" thus "?L" using Suc by auto
+  next
+    assume "?L"
+    with Suc obtain x xs where "?P k xs & P k x" by (metis less_Suc_eq)
+    hence "?P'(xs@[x])" by(simp add:nth_append less_Suc_eq)
+    thus "?R" ..
+  qed
+qed
+
+
 subsubsection {* @{text list_update} *}
 
 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"