Re: [isabelle] Issues with locale interpretation

Hi Larry,

There is indeed functionality missing in locales: there are no means of declaring and reusing morphisms in interpretations, so each parameter needs to be dealt with manually in every interpretation. This creates the desire of "bundling up" parameters, which I believe is not a good thing as it reduces flexibility. As you say, this is not a logical but a significant practical limitation.

I haven't understood what the parameters of the "unbundled" locale "incidence_system" would have looked like. For unbundling them you would have to have fixed sets of point and block parameters.

abbreviation “incidence_system’ X == incidence_system (points X) (blocks X)”

interpretation add_point_in_sys: "incidence_system’ (add_point p)”
interpretation del_point_in_sys: "incidence_system’ (del_point p)”

This approach would require an abbreviation per locale, so it's probably not as effective as dealing with morphisms directly.


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