[isabelle-dev] type class instantiation

[Makarius]

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 
end.


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

instantiation ...
begin

abbreviation ...
definition ...

end

>   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 
target directly.

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).


 	Makarius