[isabelle-dev] Checked "assume" command

[Lars Noschinski]

Hi everyone,

when using "assume" in structured proofs, one obviously needs to take 
care that the assumptions fit one of the pending goals. In particular, 
if the assumptions are more complex, we on can easily make an annoying 
mistake there. This is particularly relevant in teaching, but I myself 
also stumbled there a few times.

As an user, an easy method to test whether the current set of 
assumptions still fit one of the pending goals is "fix P show P sorry". 
As I don't know any scenario where wrong assumptions would have an 
useful effect, I propose to embed this check into the assume command.

I attached a patch against 61e222517d06 to achieve this. The 
modifications are based on the gen_show function in proof.ML, which 
already implements a similar check.

This is just a proof of concept; some things most probably need to change:

   * the check_goal function is a bit magic. This function should ensure
     that there is an open goal (i.e., we are not just in a notepad) and
     we are in the outermost block (in forward mode), which contains
     this goal (i.e., the innermost block is not opened by "{", but by
     "proof")).

   * I shuffled around some sets of functions in proof.ML to get the new
     call dependencies right. This needs more care to preserve the
     internal structure of the file

   * I fixed up all the callers of the assume functions by setting the
     "int" flag to false (which disables the new check) -- this needs
     closer investigation.

   -- Lars
-------------- next part --------------
A non-text attachment was scrubbed...
Name: checked_assume.patch
Type: text/x-patch
Size: 7878 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120904/58ae91d0/attachment.bin>