*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Theorem-proving for a Bayesian model compiler*From*: Timothy McKenzie <tjm1983 at gmail.com>*Date*: Thu, 17 Mar 2011 12:52:17 +1300*In-reply-to*: <8AC639F1-C740-46CC-9F0C-C4093B16B51C@ksvanhorn.com>*References*: <8AC639F1-C740-46CC-9F0C-C4093B16B51C@ksvanhorn.com>*User-agent*: KMail/1.13.6 (Linux/2.6.34.8-68.fc13.x86_64; KDE/4.5.5; x86_64; ; )

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 <><

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Theorem-proving for a Bayesian model compiler***From:*Jeremy Dawson

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

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

**References**:**[isabelle] Theorem-proving for a Bayesian model compiler***From:*Kevin Van Horn

- Previous by Date: [isabelle] CFP: ICTSS-11 in Paris
- Next by Date: Re: [isabelle] Theorem-proving for a Bayesian model compiler
- Previous by Thread: Re: [isabelle] Theorem-proving for a Bayesian model compiler
- Next by Thread: Re: [isabelle] Theorem-proving for a Bayesian model compiler
- Cl-isabelle-users March 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list