When I have a lot of assumptions, sometimes I end up with a lot of temporary names that clutter the proof.
I'm talking about things like this:
lemma foo: ...
proof
assume P: ... and Q: ... and R: ...
then have ...
then have ... using P ...
then have ... using P R ...
then show ...
proof
assume A: ... and B: ... and C: ...
then have ...
then have ... using B C ...
...
and can you imagine how that evolves. A lot of names for statements that, in the grand scheme of things, are not worthy of naming, but are named nonetheless because we need to reference them some lines later.
If we used all current assumptions on the other hand, the superfluous names wouldn't clutter the proof:
lemma foo: ...
proof
assume ... and ... and ...
then have ...
then have ... using assumptions ...
then have ... using assumptions ...
then show ...
proof
assume ... and ... and ...
then have ...
then have ... using assumptions ...
...
Of course, using assumptions
is not a valid statement in Isabelle. I know about assms
, which references the assumes
clause, but I don't know if there exists such a thing for assume
.
Is there a way to reference the all current assumptions created by assume
?
In case you really need it...
If all you want are the last assumptions that you made (and not all of them), you can simulate the effect presented by using a name convention (e.g.
assumptions
orassmps
) and bundling the assumptions together (i.e using ""..." "..." "..."
" instead of ""..." and "..." and "..."
"):In the example above, the second
assume assumptions
shadows the first one, so if you always name your assumptions "assumptions
" (or whatever naming convention you prefer), thenusing assumptions
will always refer to the last set of assumptions.Notice that once you close a subproof with
qed
, anyassume assumptions
in the current scope is forgot, so as expected, you can continue using it the previous assumptions after you finish the subproof.The downside of this method is that, since every new name shadows the rest, only your most recent assumptions in the scope are accessible, which may be a problem if you intend to use any assumptions made before the most recent ones.
... but you probably don't need it.
Although you can use that, Isabelle has other constructs that may solve the same problem in a better way, depending on the situation. Here's some useful tools to keep in mind:
assume A: "..." "..." "..."
, withoutand
moreover ... ultimately ...
have ... and ... and ... by ...
lemma foo: assumes ... shows ...
and they will be available to you asassms
‹...›
Using 1. already vastly reduces the clutter:
Alternatively, using 2. and 3. you can format it as such:
Or alternatively, using 4. and 5.: