Re: [isabelle] Auxiliary context in class target

On Wed, 30 May 2012, Andreas Lochbihler wrote:

I am having trouble to use Isabelle's new auxiliary contexts inside a class context, as in the following example:

context ord begin
context fixes x :: 'a begin
definition bar where "bar = x"

The definition is rejected because x is erroneously identified as a free variable:

*** Extra variables on rhs: "x"
*** The error(s) above occurred in definition "ord_class.ord_class.bar_dict":
***   "bar == x"
*** At command "definition"

The same error occurs when I use fun with a more complicated function. I would like to use such a context to emulate the "for" clause of inductive for function defintions, because the induction rule generated by fun is nicer.

I still did not find time to look again at this, and probably won't before getting on 3 weeks vacation at the end of the week.

Generally, context-begin-end needs to interact with various local theory targets, and some of them might not be ready for the nested context yet. Above it looks like the canonical interpretation that turns locale into class does not cope with additional parameters. It will probably take more than one more release cycle to get an almost complete coverage of all theses things.

Reporting such problems helps to see where the important applications are, and to assign priorities where to continue further refinement of nested context. Especially the still underdeveloped bundles should join the target context game at some point.


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