Referencing current assumptions in Isabelle

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?

Solution

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 or assmps) and bundling the assumptions together (i.e using ""..." "..." "..."" instead of ""..." and "..." and "...""):

lemma foo: ...
proof
  assume assumptions: "..." "..." "..."
  then have ...
  then have ... using assumptions ...
  then have ... using assumptions ...
  then show ...
  proof
   assume assumptions: "..." "..." "..."
   then have ...
   then have ... using assumptions ...
   ...

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), then using assumptions will always refer to the last set of assumptions.

Notice that once you close a subproof with qed, any assume 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:

You can bundle assumptions together by using assume A: "..." "..." "...", without and
You can accumulate statements with moreover ... ultimately ...
You can derive multiple statements in one shot with have ... and ... and ... by ...
If your assumptions are at lemma level, you can use lemma foo: assumes ... shows ... and they will be available to you as assms
You can directly quote previous facts with ‹...›

Using 1. already vastly reduces the clutter:

lemma foo: ...
proof
  assume A: "..." "..." "..."
  then have ...
  then have ... using A ...
  then have ... using A ...
  then show ...
  proof
   assume B: "..." "..." "..."
   then have ...
   then have ... using B ...
   ...

Alternatively, using 2. and 3. you can format it as such:

lemma foo: ...
proof
  assume "..." "..." "..."
  moreover from calculation have ...
  moreover from calculation have ...
  ultimately have ...
  then show ...
  proof
   assume "..." "..." "..."
   moreover from this have ...
   ultimately have ... and ...
   ...

Or alternatively, using 4. and 5.:

lemma foo:
  assumes: "..." "..." "..."
  shows: ...
proof
  have ... using assms ...
  then have ... using assms ...
  then have ... using assms ...
  then show ...
  proof
    assume "..." "..." "..."
    then have ...
    then have ... using ‹...› ‹...› ...