# [isabelle] Problem with obtaining induction premises

Hello,
Most of my Isabelle/Isar proofs are based on induction, and sometimes I
have problems when extracting the premises of the current inductive case,
something like:
lemma "?Q xs ==> ?P xs"
proof (induct xs)
case (Cons x xs) hence "?Q xs" by auto ...
Sometimes I can extract the premises with ".", but in the most of cases I
need to apply "auto". However, even this method is some cases does not
work. I attached a small test case which does not work. I use the build of
2006 Sep 12. Am I doing something wrong? If not, is there any workaround
for this?
Greetings,
Vaidas

theory Test imports Main
begin
consts lookupEq :: "'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<Rightarrow> 'b option"
primrec
"lookupEq [] l2 a = None"
"lookupEq (x # t1) l2 a = (if (a = x) then Some(hd l2) else lookupEq t1 (tl l2) a)"
lemma lookupEq_exists:
"\<And>ys. \<lbrakk> length xs = length ys; a \<in> set xs \<rbrakk> \<Longrightarrow> (\<exists>y. lookupEq xs ys a = Some y)"
proof (induct xs)
case Nil thus ?case by auto
next
case (Cons z zs) hence "\<And>ys. \<lbrakk>length zs = length ys; a \<in> set zs\<rbrakk> \<Longrightarrow> (\<exists>y. lookupEq zs ys a = Some y)" by auto

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*