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.
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and