On Wed, 18 Apr 2012, Thomas Sewell wrote:
The fold_congs theorems are not an accident. They are used as congruence
rules to perform conversions such as
"rec (| x := rec x + 1 |) = x_update (%x. x + 1) rec". Note this removes the
duplicated mention of the name rec.
OK, I knew that the get/map
On 18/04/12 1:46 PM, Thomas Sewell wrote:
> This is used in our modified version of the Schirmer Hoare VCG. I
> suppose that we've released the c-parser sources (which load extra
> fold_congs) but not the modified Hoare package (which uses them). The
> point is to avoid an exponential time/space e
The fold_congs theorems are not an accident. They are used as congruence
rules to perform conversions such as
"rec (| x := rec x + 1 |) = x_update (%x. x + 1) rec". Note this removes
the duplicated mention of the name rec.
The name fold_congs is somewhat arbitrary, since either direction above
