Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] also and moreover

Email Gateway (Aug 18 2022 at 19:15):

From: Peter Gammie <peteg42@gmail.com>
Hi,

I want to write a proof in this style:

lemma "XXX = ZZZ"
proof -
have "XXX = AAA" sorry
moreover
have "ZZZ = BBB" sorry
also have "... = AAA" sorry (* breaks here *)
ultimately show ?thesis by simp
qed

Would it be possible for "moreover" to use a different calculation (?) to "also"?

If not, can the reason be put in S1.2 of isar-ref please?

cheers
peter

Email Gateway (Aug 18 2022 at 19:16):

From: John Wickerson <jpw48@cam.ac.uk>
Just a comment: it seems to work out ok if I put the have-also-finally bit inside curly braces...

lemma "XXX = ZZZ"
proof -
have "XXX = AAA" sorry
moreover
{
have "ZZZ = BBB" sorry
also have "... = AAA" sorry
finally have "ZZZ = AAA" sorry (* line added *)
}
ultimately show ?thesis by simp
qed

Last updated: Apr 26 2024 at 08:19 UTC