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 <><
Description: This is a digitally signed message part.