Re: [isabelle] Lemmas with multiple goals



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






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