Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Eisbach match drule

Email Gateway (Aug 22 2022 at 13:50):

From: Zhe Hou <zhe.hou@hotmail.com>
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

Email Gateway (Aug 22 2022 at 13:51):

From: Thomas Sewell <thomas.sewell@nicta.com.au>
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.

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.

Email Gateway (Aug 22 2022 at 13:52):

From: Matthew.Brecknell@data61.csiro.au
On Fri, 2016-07-22 at 17:22 +0800, Zhe Hou wrote:

Dear Eisbach developers,

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

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)

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.

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

Thanks a lot,

Zhe

You're welcome!

Matthew

Last updated: Apr 18 2024 at 01:05 UTC