Re: [isabelle] Porting trouble: Interpretation of locale semiring_1



On Wed, 22 Apr 2009, Clemens Ballarin wrote:

*** Partially applied constant on left hand side of equation
*** "semiring_1.of_nat {[]} {} op \<union> ?n \<equiv>
semiring_1.of_nat_aux (\<lambda>i. i \<union> {[]}) ?n {}"
*** At command "done".

I do not know what this error message means, nor can I find any
documentation.
In Isabelle2008, the proof worked well.

This error is generated by the code generator (while processing the interpreted lemmas). It is apparently unable to deal with the equation generated by the interpretation.

I only partially agree with Florian that interpretation doesn't do the right thing for definitions. It is important to note that interpretation must always give the user the freedom to map defined concepts to what he or she wants, not something the code generator is willing to accept. This also applies to locales generated via the class commands. Getting it right once and for all for the code generator seems to me like introducing a serious design flaw to interpretation.

This is essentially an instance of the problem of "tool compliance" of morphisms, see also the hints about that in the paper by Chaieb & Wenzel http://www4.in.tum.de/~wenzelm/papers/context-methods.pdf

Arbitrary data declarations that are included in a locale body (or class or whatever) are subject to arbitrary transformations performed by other means later (here locale interpretation). While the primitive logic is stable under such morphisms (theorems are mapped to theorems etc.),
arbitrary tools are not.

"Tool compliance" means that the transformation by a given morphism "works" -- what exactly is meant by that depends on the particular tool (here the code generator).

The usual strategy to prevent breakdowns like above is as follows:

  * Internal declarations of tool data (via certain attributes) should be
    tolerant against illformed input, i.e. not insist on a certain form,
    but give in and ignore the declaration. (This should be
    done in way that does not cause too much surprise to the user, maybe
    via a suitable warning.)

  * The user should be able to modify the environment that results from an
    interpretation etc. by adding new declarations of replacement data.


	Makarius





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