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 could be argued to be "folding".

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 explosion when updates of the form "% rec. rec (| x := rec x + 1 |)" are performed in sequence. (The problem is the repeated rec.)

The fold_congs can be provided manually to the simplifier if anyone knows to do so. I am probably the only person in the world who knows when to do so. This is usually done to equate the two forms given above, either of which may be the result of other simplification. There are 88 uses of fold_congs in the L4.verified proofs at this time.

The unfold_congs are meant to perform the reverse substitution, but the simplifier doesn't reliably play along. There are 5 uses in the L4.verified proofs at this time, and I suspect they can be easily removed.


On 18/04/12 00:37, Makarius wrote:
This is probably mainly relevant to NICTA users of the record package.

When doing some cleanup and performance tuning of the record package, I
discovered the following mysterious fold_congs and unfold_congs:

They appear to go back to the initial NICTA contribution 50406c4951d9. I
have also seen traces of that feature in the L4.verified C parser tool
that became publicly available recently.

Do these fold_congs/unfold_congs still have any purpose?  In the reachable
set of Isabelle and AFP applications they don't, as far as I can see.  So
it looks like a candidate for garbage collection on the sources.

isabelle-dev mailing list

isabelle-dev mailing list

Reply via email to