[isabelle-dev] Checked "assume" command
Lars Noschinski
noschinl at in.tum.de
Tue Sep 4 21:18:02 CEST 2012
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>
More information about the isabelle-dev
mailing list