[isabelle-dev] Typerep again

[Florian Haftmann]

>>>> Our current policy is that Plain, Main (and Complex_Main) are either
>>>> ancestors or descendants of any theory.

> This rule does not tell me anything since it is trivally satisfied by
> any connected graph containing Plain, Main and Complex_Main.

The rule rules out the following situation:

   A
  / \
 B   Main
  \ /
   C

Here B is neither ancestor or descendant of Main, likewise the other way
round.

But to stick to the problem itself first (by example from an earlier
discussion):

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

Generally, each time such a typerep clash occurs, you can eliminate it
by finding a suitable meeting point.

>>>>> Our current policy is that Plain, Main (and Complex_Main) are either
>>>>> ancestors or descendants of any theory.

The point here is that parallelized proofs scale better if a huge theory
 development does not contain to many merges.  To reduce their number,
it is better to merge theories quite frequently.  This has recently be
done, by simply asserting that for each HOL theory holds:

  * Plain is either an ancestor or descendant of any HOL theory.
  * Main is either an ancestor or descendant of any HOL theory.

This gives funny wasp-waists in the thy graph.  The policy also avoids
the typerep problem since if any theory which is not part of Main
imports Main, the situation (*) above does not occur.

As a kind of stylized comment, this technical imports of Plain and Main
are appended to the import list rather then prepended, but this is a
matter of taste.

Hope this helps
	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090209/af48875d/attachment.sig>