[isabelle-dev] record: fold_congs/unfold_congs

[Makarius]

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 form (called x and x_update here) is 
fundamentally better that get/put.


> 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.

No need to take action.  We leave the status-quo.

I have recorded the conclusion of this mail thread in 
Isabelle/0eadfb89badb in the historically correct wording.


 	Makarius