[isabelle-dev] record: fold_congs/unfold_congs

[Thomas Sewell]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev