[isabelle] Problem with obtaining induction premises


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?

theory Test imports Main

consts lookupEq :: "'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<Rightarrow> 'b option"
  "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
  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.