[isabelle] Lemmas with multiple goals



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.