[isabelle] selector theorems for records WAS: simps_of_case has problems with records



Hi Jasmin,

Another application of the Ctr_Sugar/BNF machinery would be generating selector equations from a record specification or specifying a record via its selectors. Here is an example of what I have in mind:

  record point =
    x :: nat
    y :: nat

  definition my_point :: point where "my_point = (| x = 5, y = 7 |)"

Now, I have to manually state and derive

  lemma point_sel:
    "x my_point = 5"
    "y my_point = 7"
  by(simp_all add: my_point_def)

Conversely, it seems sensible to specify records by their fields, as in

  record_definition my_point :: point where "x my_point = 5" | "y my_point = 7"

which could internally derive

  my_point_ctr: "my_point = (| x = 5; y = 7 |)"


Johannes HÃlzl has changed the definition of the complex numbers to a codatatype to be able to use primcorec which does these conversions already internally. Is there already something similar for extensible records which I have missed?

Best,
Andreas

On 02/06/15 16:36, Jasmin Blanchette wrote:
Hi Andreas,

Though, I do not see why the free constructor architecture would have to be extended. An extended extensible record like 'a bar_scheme just abbreviates "'a bar_ext foo_ext" and the functions foo_ext and bar_ext can serve as constructors for foo_ext and bar_ext, respectively. That is, we just have nested types with free constructors. What am I missing?

Some of the architecture doesnât like complex types like ââa bar_ext foo_extâ â e.g. lookup is performed on a type name. Thatâs the main problem IIRC. It might be easy to fix. I thought there was also an issue with the âbar_extâ constant being an abbreviation, but I apparently remembered this wrong.

Another worry I have is just the naming and wealth of theorems. Automatically performing what you do when you manually do âfree_constructorsâ yields quite a few theorems coming from two worlds. It seems like the prefixes keep things apart, e.g. âfoo.splitsâ (generated by record) vs. âfoo_ext.splitsâ (generated by âfree_constructorsâ) â but the situation is still not entirely satisfactory IMO. Hence, I would rather tread carefully here, and perhaps wait one more iteration of Isabelle and new datatypes before doing more âreformsâ.

Iâm also not sure all infrastructure will be equally happy to have two views on records â the records one and the âctr_sugarâ one (which has largely displaced the old datatype one here and there). This is a minor issue that can be addressed one tool at a time (Nitpick, Quickcheck, etc.), but it might require some weeks before all problems have been identified and solved.

Finally, this would enable the datatype plugins on records â generation of a size function etc. Again, this is not completely impact-free, if nothing else on the number of theorems/constants/etc. generated and hence on the performance of the prover. This is another reason why Iâm inclined to wait.

All this having been said, I believe that records belong in âctr_sugarâ and that the convenience of having them in there by default would be appreciated by many users. If anybody is willing to jump in and make it happen faster than Iâm likely going to, theyâre welcome. ;)

Unfortunately, the record package is still completely unlocalised. That's probably the bigger hurdle.

I think thatâs fine as far as âCtr_Sugarâ goes, thanks to the âgeneric dataâ abstraction. âCtr_Sugarâ can also deal with old-style datatypes, after all.

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.