[isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Florian Haftmann]

Hi Clemens,

> I'm not familiar with the termination argument for abbreviations, but
certainly we can say that abbreviations define a reduction system (in
fact a rewrite system), and I would assume that there are no cycles and
infinite paths.  Now my patch will clone part of this system,
introducing additional nodes and transitions, but I don't see how it
would introduce cycles if there were no cycles without it.  It could
introduce infinite chains, but only for infinite chains of
interpretations.  The latter are not allowed by the roundup algorithm.
Am I missing something?

Well, I am not so sure about the cycles:

As a starting point, take A --> B --> C.

Let the interpretation morphism map these as follows:

	A |-> D
	B |-> E
	C |-> D

Then under the morphism we have D --> E --> D.

But maybe this is forbidden by the properties of a morphism itself.

I did not work to contrieve a meaningful counterexample yet.

Cheers,
	Florian

> 
> Clemens
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

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: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151112/9cdba0cb/attachment.sig>