Re: [isabelle] Issues with locale interpretation



Hi Clemens, perhaps you’ve seen this recent AFP entry: 

	https://www.isa-afp.org/entries/Grothendieck_Schemes.html

It was inspired by your own work and builds upon it. In fact, we have other (very different) work in the pipeline also following your locale-based approach, which seems to be extremely general.

The suggestion in my email was intended as a minimal, lightweight solution to the issue. A more principled solution would be great provided it doesn’t introduce implementation or foundational issues.

Best.

Larry

> On 11 Apr 2021, at 10:52, Clemens Ballarin <ballarin at in.tum.de> wrote:
> 
> 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.
> 
> Clemens





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