Improve corres rules whileLoop

[michaelmcinerney]

Please see the commit message for a brief explanation

[michaelmcinerney]

Sorry, forced pushed to correct the commit message

[Xaphiosis]

Having spent a bit of time poking that compare time while loop, this improvement makes a lot of sense!

[lsf37]

Cool, much nicer rules! Minor style nitpicks only.

[corlewis]

I'm undecided myself, but could using rv in these postconditions to distinguish from the bound r improve readability? I guess a potential concern is that it could also be confused with the final return value of the whole loop.

Suggested change

	and body_inv: "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>\<lambda>r. P r\<rbrace>"
	"\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>r'. P' r'\<rbrace>"
	and body_inv: "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>\<lambda>rv. P rv\<rbrace>"
	"\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>rv'. P' rv'\<rbrace>"

[michaelmcinerney]

The situation is quite tricky with these whileLoops. There is the (blue) initial value given to the whileLoop (you can see an example of this in the conclusion of the statement of corres_whileLoop_ret). Then there is the (green) return value given by the loop body. I think it would be nicer to stick with the r for here, to reinforce that connection. But happy to discuss it some more

[michaelmcinerney]

The other alternative for these valid bits is that I could just eta contract the postcondition. I left it written out to emphasise that these guards do talk about the return value, but maybe that's clear enough

[lsf37]

I would usually prefer the eta-contracted version unless we're trying to do the bound-name preservation trick where Isabelle would replace rv with whatever name was in the goal (which is not the case here).

[michaelmcinerney]

Also, most of these lemmas use the assumes... shows and I don't think they're properly indented. The autoindenter will indent will leave the assumes indented by 2, indent the subsequent ands by a further 2 spaces, and then have the shows indented by 2. Should I go with that?

[Xaphiosis]

Also, most of these lemmas use the assumes... shows and I don't think they're properly indented. The autoindenter will indent will leave the assumes indented by 2, indent the subsequent ands by a further 2 spaces, and then have the shows indented by 2. Should I go with that?

I thought it would do this:

assumes a: blah
    and dsad: blah2

hmm.

[lsf37]

Also, most of these lemmas use the assumes... shows and I don't think they're properly indented. The autoindenter will indent will leave the assumes indented by 2, indent the subsequent ands by a further 2 spaces, and then have the shows indented by 2. Should I go with that?

I usually avoid the and and just repeat the assumes, which is also more stable against moving things around. The correct indent of that is:

lemma name:
  assumes x: "..."
  assumes y: "..."
  shows "..."

The and is mostly useful if you really need two propositions to be parsed in a single assumes for typing reasons or similar, which is very rare. The other times I use it, if it's just very short statements like assumes a: "A" and b: "B".