[isabelle-dev] Feature suggestion: apply (meth[1!])

[Joachim Breitner]

Hi,

Am Montag, den 11.03.2013, 18:11 +0100 schrieb Lars Noschinski:
> On 11.03.2013 17:51, Makarius wrote:
> > This looks just like making the meaning of indentation a bit more
> > formal. Lets say as a mode of checking in the Prover IDE: fail if
> > something is wrong in that respect, or paint things in funny colors.
> 
> We shortly thought about this earlier and it has the appeal of 
> formalizing an already established convention, which is definitely 
> useful. However, there are two things which make me slightly 
> uncomfortable with this solution:
> 
>    - when I'm exploring a proof which I expect to collapse into a
>      one-line by-statement I usually don't (and don't want to) bother
>      with indentation (this is obviously less of issue when using funny
>      colors).
> 
>    - Isabelle does not have significant whitespace anywhere else (I'm
>      aware of). It does not even consider linebreaks to be relevant. So
>      my initial feeling about this suggestion is "neat hack".

if you want to experiment with assertions about the number of goals at a
specific point in your proof, you can try this:

theory Assert_Goals imports Main
keywords "assert_goals" :: prf_script % "proof"

begin
ML {*
  fun check_goal_n n state = 
    let val {context = _, goal = thm} = Proof.simple_goal state
    in nprems_of thm = n
    end;

  Outer_Syntax.command @{command_spec "assert_goals"} "Assert number of goals"
    (Parse.nat >> (fn n => Toplevel.proof (fn state => if check_goal_n n state then state else error "Not the expected number of goals")));
*}

end

This lets you say "assert_goals 5" in your apply scripts where you think
there should be 5 goals. If that is not the case, then jEdit shows some
red wiggles, but otherwise allows you to continue as before. The error
message could be more verbose, e.g. showing the current goal.

It is a bit verbose and does not work inside a (...)+ nesting, so I’d
still like the [!] or a similar method-level syntax, but at least it
works without modifying the prover.

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130311/65d37c1f/attachment.sig>