*To*: Timothy McKenzie <tjm1983 at gmail.com>*Subject*: Re: [isabelle] Theorem-proving for a Bayesian model compiler*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Thu, 17 Mar 2011 12:33:21 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201103171252.29679.tjm1983@gmail.com>*References*: <8AC639F1-C740-46CC-9F0C-C4093B16B51C@ksvanhorn.com> <201103171252.29679.tjm1983@gmail.com>*User-agent*: Thunderbird 2.0.0.24 (X11/20101027)

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 anexample in isar-overview in the documentation provided withIsabelle, and more technical documentation in isar-ref. It can beused with both = and <= (and, I think, even mixing the two), butit behaves unusually with >=, because this is an abbreviation for<=, and the abbreviation seems to be expanded before Isabelledecides which is the left-hand side and which is the right-handside for the purposes of the next step.And if you don't know exactly what you want to prove before you'veproven it, you can make the statement of the lemma almostarbitrary until you've figured out what you want to prove, andthen go back and change it. I haven't used the other HOLs, but Iunderstand that they work backwards, manipulating the goal untilit becomes "True", so in those you'd need to state the lemmacorrectly before you begin.Tim <><

Well, in either system you can always start with a goal of the form P1 ==> P2 ==> ... ==> Pn ==> X

Jeremy

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

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

- Previous by Date: Re: [isabelle] Theorem-proving for a Bayesian model compiler
- 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