[isabelle] Problem with cases



I have the following problem with rule-setup for cases:

I have the following lemma:
lemma HpreE[cases set, case_names nospawn spawn]:
  "\<lbrakk>
    h\<in>Hpre;
    !!h1 lab t' h2. \<lbrakk>h=h1 at NNOSPAWN lab t'#h2; final h1; final
h2; final_t t'\<rbrakk> \<Longrightarrow> P;
    !!h1 lab ts t' h2. \<lbrakk> h=h1 at NSPAWN lab ts t'#h2; final h1;
final h2; final_t ts; final_t t'\<rbrakk> \<Longrightarrow> P
  \<rbrakk> \<Longrightarrow> P"
  by (unfold Hpre_def) blast

However, if I want  to use it with the cases method, it does not work:
lemma "\<lbrakk>h\<in>Hpre; sched h ll\<rbrakk> \<Longrightarrow> length
ll = 1"
proof (cases rule: HpreE)

The goals here are the following, and the assumptions of the generated
case_names are empty. However, I would have expected only two goals.
goal (3 subgoals):
 1. \<lbrakk>h \<in> Hpre; sched h ll\<rbrakk> \<Longrightarrow> ?h
\<in> Hpre
 2. \<And>h1 lab t' h2. \<lbrakk>h \<in> Hpre; sched h ll; ?h = h1 @
NNOSPAWN lab t' # h2; final h1; final h2; final_t t'\<rbrakk>
\<Longrightarrow> length ll = 1
 3. \<And>h1 lab ts t' h2. \<lbrakk>h \<in> Hpre; sched h ll; ?h = h1 @
NSPAWN lab ts t' # h2; final h1; final h2; final_t ts; final_t
t'\<rbrakk> \<Longrightarrow> length ll = 1


What is going wrong there ?

Regards & thanks in advance for any help
  Peter











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