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]:
> !!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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and