Re: [isabelle] Problem with cases



On Sun, 18 Jan 2009, Peter Lammich wrote:

> 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)

You need to use explicit forward chaining of the "h\<in>Hpre" assumption 
in the "cases" proof step.  I.e. like this:

  lemma
    assumes "h\<in>Hpre"
    shows XXX
  using assms
  proof cases
    ...


Also note that elimination rules like HpreE can be written conveniently 
using the 'obtains' format.  Try 'print_statement' on your rule to see the 
general layout.  You can also add case names in parentheses here, to avoid 
slightly low-level attribute specification as above.


	Makarius






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