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



Timothy McKenzie wrote:
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.

Tim
<><

Well, in either system you can always start with a goal of the form
P1 ==> P2 ==> ... ==> Pn ==> X
where Pi are your real assumptions, and X is literally just "X", a placeholder, while you see what you can get from P1 to Pn - when you have decided what X should be you go back and repeat the same proof

Jeremy





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