Re: [isabelle] Auxiliary context in class target



Hi Andreas,

> 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?

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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