Email Gateway (Aug 18 2022 at 12:51): Email Gateway (Aug 18 2022 at 12:51):From: Peter Lammich <peter.lammich@uni-muenster.de>
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@NNOSPAWN lab t'#h2; final h1; final
h2; final_t t'\<rbrakk> \<Longrightarrow> P;
!!h1 lab ts t' h2. \<lbrakk> h=h1@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):
\<lbrakk>h \<in> Hpre; sched h ll\<rbrakk> \<Longrightarrow> ?h
\<in> Hpre
\<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
\<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
Email Gateway (Aug 18 2022 at 12:51):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 04:19 UTC