*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Beginner's struggles*From*: Ian Lynagh <igloo at earth.li>*Date*: Sun, 15 Aug 2010 15:37:30 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.1.10.1008141659380.5958@atbroy100.informatik.tu-muenchen.de>*References*: <20100814004117.GA19807@matrix.chaos.earth.li> <alpine.LNX.1.10.1008141659380.5958@atbroy100.informatik.tu-muenchen.de>*User-agent*: Mutt/1.5.18 (2008-05-17)

Thanks for your reply Makarius. Some helpful tips there, although the main purpose of my mail was to try to highlight the sorts of difficulties that beginners (well, at least one beginner!) run into. Actually, I've just run into something that really does have me stumped: It seems that "fix a" does nothing at all, yet it can be necessary; looks like magic to me! e.g. in this proof: theory Test imports Main begin lemma assumes P: "! x. P x" shows "! x. P(f x)" proof fix a from P show "P(f a)" .. qed the "proof state" is the same before and after the "fix a" line (well, apart from the step counter being incremented, but I assume that's not relevant), as are the "cases", "facts", and "term bindings". So how am I meant to know whether I need to fix something, if doing so has no visible effect? Am I missing something? This is a real problem for me in the proof I'm trying to write. I have goals like !!bool. principalType (EBool bool) = Some t ==> STyping (EBool bool) t and I have no idea if the commands I'm giving are taking me in the right direction or not, as they seemingly do nothing. I am also surprised that "facts", and perhaps also "term bindings", are not shown by default. Not only that, but proof general has given me a toolbar button that tells me "theory Test", but not a toolbar button to tell me the current facts; is wanting the former really more common than wanting the latter? On Sat, Aug 14, 2010 at 05:22:29PM +0200, Makarius wrote: > > (We have the more conventional ";" for that, but it has almost > come out of use in recent years, since Proof General is good enough to > determine command boundaries from the keywords alone.) That reminds me of another minor irritation: If I write this partial proof: theory Test imports Main begin lemma "A & B ==> B & A" proof assume "A & B" thus B and then "Process whole buffer", and then complete the proof as: theory Test imports Main begin lemma "A & B ==> B & A" proof assume "A & B" thus B.. next assume "A & B" thus "A" .. qed then I can "Process whole buffer" again and the proof is accepted. But if I then "Retract whole buffer" and "Process whole buffer" again then the proof is now rejected (due to the missing space between "B" and ".."). Thanks Ian

**Follow-Ups**:**Re: [isabelle] Beginner's struggles***From:*Ian Lynagh

**Re: [isabelle] Beginner's struggles***From:*Makarius

**References**:**[isabelle] Beginner's struggles***From:*Ian Lynagh

**Re: [isabelle] Beginner's struggles***From:*Makarius

- Previous by Date: Re: [isabelle] Beginner's struggles
- Next by Date: [isabelle] König's Lemma?
- Previous by Thread: Re: [isabelle] Beginner's struggles
- Next by Thread: Re: [isabelle] Beginner's struggles
- Cl-isabelle-users August 2010 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