Re: [isabelle] also and moreover



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

On 8 Mar 2012, at 03:10, Peter Gammie wrote:

> 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
> 
> -- 
> http://peteg.org/
> 
> 






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