*Post by Zhe Hou*Dear Eisbach developers,

I'm not an Eisbach developer, but I'll try to answer as best I can!

*Post by Zhe Hou*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

lemma dummy: "A ∧ B ⟹ B"

by auto

lemma "A ∧ B ⟹ A ∨ B"

apply (match premises in "A ∧ B" ⇒ ‹drule dummy›)

But Isabelle says "Failed to apply proof method". However, the

lemma "A ∧ B ⟹ A ∨ B"

apply (drule dummy)

This is not anything to do with drule in particular. Rather, it's

related to the subgoal focusing performed by the match method. You

might want to reread section 2.1 of the Eisbach user manual:

https://isabelle.in.tum.de/dist/Isabelle2016/doc/eisbach.pdf

In particular, drule is looking for an unstructured premise, but match

has removed these from the subgoal focus. Within the inner method, only

named premises are accessible.

*Post by Zhe Hou*Is there a way to use drule inside match? Or, is there an alternative to drule?

One way to make drule work would be to explicitly re-insert the premise

of interest:

lemma "A ∧ B ⟹ A ∨ B"

apply (match premises in H[thin]: "A ∧ B" ⇒

‹insert H; drule conjunct2›)

oops

Note that we had to name the matched premise to make it accessible.

I've also use the `thin` attribute to remove the original premise on

return from the match.

Perhaps this is a slight improvement:

lemma "A ∧ B ⟹ A ∨ B"

apply (match premises in H[thin]: "A ∧ B" ⇒

‹insert conjunct2[OF H]›)

oops

*Post by Zhe Hou*Thanks a lot,

Zhe

You're welcome!

Matthew