Re: [isabelle-dev] record: fold_congs/unfold_congs

2012-04-26 Thread 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

[isabelle-dev] record: fold_congs/unfold_congs

2012-04-17 Thread Makarius
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:

Re: [isabelle-dev] record: fold_congs/unfold_congs

2012-04-17 Thread 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

Re: [isabelle-dev] record: fold_congs/unfold_congs

2012-04-17 Thread Michael Norrish
On 18/04/12 1:46 PM, Thomas Sewell wrote: 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