[isabelle] Issues with locale interpretation



Having done quite a few proofs involving locales recently, I’ve noticed an issue with locale interpretation that is logically superficial but can make a big difference in proofs. It is that the argument lists of locales can grow drastically, and if users try to control this growth by “bundling up” adjacent, related arguments, they will be punished when the time comes to instantiate the locale. Example (thanks to Chelsea Edmonds):

interpretation add_point_in_sys: incidence_system "points (add_point p)" "blocks (add_point p)”
  sorry

interpretation del_point_sys: incidence_system "points (delete_point p)" "blocks (delete_point p)”
  sorry

Here we want the locale “incidence_system” to have virtually one argument, the pair of “points” and “blocks”, but the interpretation command requires the full argument list to be written out. It would be nice to be able to do something like this:

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)”

Any thoughts on this?

Larry





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