Re: [isabelle] Beginner's struggles



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.