src/ZF/List.ML
changeset 13149 773657d466cb
parent 13143 adb0c97883cf
child 13160 eca781285662
equal deleted inserted replaced
13148:fe118a977a6d 13149:773657d466cb
   236 (*Lemma for the inductive step of drop_length*)
   236 (*Lemma for the inductive step of drop_length*)
   237 Goal "xs: list(A) ==> \
   237 Goal "xs: list(A) ==> \
   238 \          ALL x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
   238 \          ALL x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
   239 by (etac list.induct 1);
   239 by (etac list.induct 1);
   240 by (ALLGOALS Asm_simp_tac);
   240 by (ALLGOALS Asm_simp_tac);
   241 by (Blast_tac 1);
       
   242 qed_spec_mp "drop_length_Cons";
   241 qed_spec_mp "drop_length_Cons";
   243 
   242 
   244 Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))";
   243 Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))";
   245 by (etac list.induct 1);
   244 by (etac list.induct 1);
   246 by (ALLGOALS Asm_simp_tac);
   245 by (ALLGOALS Asm_simp_tac);