Email Gateway (Aug 18 2022 at 19:59): Email Gateway (Aug 18 2022 at 19:59):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi all,
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 == 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.
Is this just not yet implemented or am I again abusing things here?
Andreas
Email Gateway (Aug 18 2022 at 20:00):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 18 2022 at 20:27):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
this is indeed a current restriction in the class target; it expects all
occuring auxiliary parameters to be class parameters, which is a very
strong assumption. I am currently testing a patch
(http://isabelle.in.tum.de/testboard/Isabelle/rev/d4b6b21b75e2) which is
supposed to lift this restriction.
Cheers,
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC