Re: [isabelle] Eisbach match drule



Hello Zhe.

I'm not an Eisbach developer, but I think I know what the problem is.
When you match in the premises, the premises get lifted out of the usual
goal state. The matched premise becomes available as a rule, but isn't
in the goal any more.

So you could do this:

lemma "A & B ==> A | B"
   apply (match premises in f: "A & B" â âcut_tac dummy[OF f]â)
   by assumption

or this (put it back then drule):

lemma "A & B â True â A | B"
  by (match premises in f: "A & B" â âcut_tac f, drule dummyâ)

Does that help?

Cheers,
    Thomas.

On 22/07/16 19:22, Zhe Hou wrote:
Dear Eisbach developers,

I ran into a problem when using drule in match. It seems that drule is not supported, but rule is. For example, let's first define a silly lemma here:

lemma dummy: "A â B â B"
by auto

Then, when proving the following lemma, I try:

lemma "A â B â A â B"
apply (match premises in "A â B" â âdrule dummyâ)

But Isabelle says "Failed to apply proof method". However, the following is ok:

lemma "A â B â A â B"
apply (drule dummy)

Is there a way to use drule inside match? Or, is there an alternative to drule?

Thanks a lot,

Zhe



________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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