[isabelle-dev] typrep?

[Brian Huffman]

Hi Florian,

I, for one, am rather alarmed at the hurdles that Amine was forced to  
overcome to do a simple merge of two theories. Even before the  
typerep-related problems, merging Isabelle theories was already  
difficult enough! I think that merging theories is one of Isabelle's  
most serious weaknesses, and it has prevented many users from being  
able to borrow, share, and build upon each other's code. (Witness how  
little re-use of code there has been among AFP entries, in spite of  
the recommendation in the submission guidelines, "It is possible and  
encouraged to build on other archive entries in your submission.")

With this in mind, automatically-generated class instances are a step  
in the wrong direction. Assuming we can find solutions to name-space  
and syntax clashes, the only thing that can make two theories truly  
incompatible is having two different instantiations for overloaded  
constants at the same type. Adding class instantiations can introduce  
theory incompatibilities, and for this reason, adding class  
instantiations should not be taken lightly---and they should certainly  
not be done automatically!

I think that the automatic class-instantiations should be disabled  
immediately, and replaced with a new top-level command so that these  
instantiations can be done explicitly, and individually.

Facilitating the merging of theories written by different people  
should be a much higher priority. Arranging theory graphs should not  
have to be nearly so difficult as it is.

- Brian


Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> Hi Amine,
>
> I guess you are in the following thygraph situation:
>
>     Typrep  Real
>        | /  \ |
>        |/    \|
> Complex_Main  FPS
>        \      /
>         \    /
>          \  /
>           Foo
>
> Real defines type real, Typerep class typerep (;-)).  Then both in
> Complex_Main and FPS and instance for typerep on type real is generated
> automatically (thanks to generic interpretation), which clash on merge
> into theory Foo.
>
> The solution is too arrange that there is only one meeting point of
> Typrep and Real in the thygraph.  According to your second email you
> have already found a way.
>
> N.B. arranging the HOL thygraph is a nontrivial task!
>
> Cheers,
> 	Florian