[isabelle-dev] record: fold_congs/unfold_congs
makarius at sketis.net
Thu Apr 26 20:27:33 CEST 2012
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
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.
More information about the isabelle-dev