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

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