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
*** Extra variables on rhs: "x"
*** The error(s) above occurred in definition "ord_class.ord_class.bar_dict":
*** "bar == ord.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
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