# [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.