[isabelle-dev] type class instantiation
makarius at sketis.net
Fri Apr 6 14:57:00 CEST 2012
On Fri, 6 Apr 2012, Christian Sternagel wrote:
> it seems as if a recent change (in the repo version; within the last 2
> weeks, but I do not know exactly when) fixed the naming of type
> variables inside instantiations.
There are various ongoing reforms (e.g. see changes leading up to
610d9c212376) that address open questions from the last 5 years of local
theory infrastructure. Any unexpected change certainly helps to
understand the situation, and figure out what is right or wrong in the
> I have a type "('f, 'v) term" for first-order terms with function
> symbols of type "'f" and variables of type "'v" and a type class "show"
> that provides a "shows_prec" and a "shows_list" function for efficient
> conversion into strings. To instantiate "term" I had (and this actually
> worked until recently)
> instantiation "term" :: ("show", "show") "show" begin
> abbreviation "shows_term t ≡ shows_term' shows shows t"
> definition "shows_prec (d::nat) t = shows_term t"
> definition "shows_list_term (is::('f::show, 'v::show) term list) =
> shows_list_aux shows is"
First, it has required me 1 more minute to parse the above, because it is
indented in such an odd way, with a dangling 'begin'. Isabelle/jEdit will
at some point support a certain text structure (with indentation and
folding etc.), but only in the standard style:
> lemma assoc_term:
> "shows_prec d (t::('f::show, 'v::show) term) r @ s = shows_prec d t
> (r @ s)"
> This no longer works and I'm forced to use "'a" and "'b" instead of "'f"
> and "'v".
Like the class target, interpretation uses canonical type variable names.
The change of behaviour is a consequence of more precise treatment of the
target context: results are not exported into the bare-bones theory
context as before, and then copied to the target, but exported into the
Florian can say, if he originally meant to support different type variable
names as shown above. There might be some type improvement in the context
that needs to be re-adjusted (or some now unused things to be removed).
More information about the isabelle-dev