Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Lemmas with multiple goals

Email Gateway (Aug 18 2022 at 18:46):

From: filip@matf.bg.ac.rs
Hi,
here is a simple Isar technical question. Suppose that I have a lemma of
the form

lemma X:
assumes "Assumption"
shows "Goal1" and "Goal2"
sorry

Now, suppose that I want to apply this argument and prove

lemma "Goal1" and "Goal2"

Something that I would like to have is

lemma "Goal1" and "Goal2"
proof (rule X)
show "Assumption"
sorry
qed

However, this does not work (it seems that only X(1) is applied). Of
course, I could write a proof like

lemma "Goal1" and "Goal2"
proof-
have "Assumption"
sorry
thus "Goal1" and "Goal2"
using X
by auto
qed

but the first proofs structure seems most natural so I was wandering is
there a way to apply it. BTW, since there is no ?thesis when multiple
goals are present, is there a way of not retyping "Goal1" and "Goal2" in
the second proof?

Best regards,
Filip

Email Gateway (Aug 18 2022 at 18:46):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Filip,

You wrote:

lemma "Goal1" and "Goal2"
proof (rule X)
show "Assumption"
sorry
qed

However, this does not work (it seems that only X(1) is applied).

Perhaps the Isar gurus have a better solution, but the best I could get is

lemma "Goal1" (is ?g1) and "Goal2" (is ?g2)
proof -
have "Assumption" sorry
thus ?g1 and ?g2 by (rule X)+
qed

BTW, since there is no ?thesis when multiple
goals are present, is there a way of not retyping "Goal1" and "Goal2" in
the second proof?

Yes, using the "is" syntax above.

I hope this helps. Have a nice day.

Jasmin

Last updated: Nov 21 2024 at 12:39 UTC