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.
Yours,
Thomas.
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:
http://isabelle.in.tum.de/repos/isabelle/file/d52da3e7aa4c/src/HOL/Tools/record.ML#l334
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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
