Discussion:
[isabelle] Eisbach match drule
Zhe Hou
2016-07-22 09:27:28 UTC
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
Thomas Sewell
2016-07-25 02:50:30 UTC
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.
Post by Zhe Hou
Dear Eisbach developers,
lemma dummy: "A ∧ B ⟹ B"
by auto
lemma "A ∧ B ⟹ A ∨ B"
apply (match premises in "A ∧ B" ⇒ ‹drule dummy›)
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.
M***@data61.csiro.au
2016-07-25 10:52:40 UTC
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