Re: [isabelle] Theorem-proving for a Bayesian model compiler

On Wed, 16 Mar 2011 04:11:54 Kevin Van Horn wrote:
> * Ability to do derivational proofs where I know the form of
> what I want to prove but don't know exactly what I'm proving
> until I reach the end.  For example, I'm doing a chain of A1 =
> A2 = ... An, and only when I reach an An that has the form I
> want do I know I'm done and know that A1 = An is what I'm
> proving.  Likewise, I might be trying to find a usable upper
> bound: B1 <= B2 <= ... Bn.

I'm a little surprised that no-one has yet mentioned the "also ... 
also ... finally ..." constructions in Isabelle/Isar.  There's an 
example in isar-overview in the documentation provided with 
Isabelle, and more technical documentation in isar-ref.  It can be 
used with both = and <= (and, I think, even mixing the two), but 
it behaves unusually with >=, because this is an abbreviation for 
<=, and the abbreviation seems to be expanded before Isabelle 
decides which is the left-hand side and which is the right-hand 
side for the purposes of the next step.

And if you don't know exactly what you want to prove before you've 
proven it, you can make the statement of the lemma almost 
arbitrary until you've figured out what you want to prove, and 
then go back and change it.  I haven't used the other HOLs, but I 
understand that they work backwards, manipulating the goal until 
it becomes "True", so in those you'd need to state the lemma 
correctly before you begin.


Attachment: signature.asc
Description: This is a digitally signed message part.

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