[isabelle-dev] Unproven class relation finite_lattice_complete < countable

[Florian Haftmann]

The last significant changeset seems to be

	http://isabelle.in.tum.de/repos/isabelle/rev/8715343af626
	classrel and arity completion by krauss/schropp;

The critical code starting at

	http://isabelle.in.tum.de/repos/isabelle/rev/8715343af626#l1.78

The problem is that during class hierarchy graph completion there is a
lookup for a not-yet existing edge.  (Since the minimal example does not
involve any instances, it cannot be arity completion).

Without having investigated thoroughly, I have two guesses what the
problem could be:

a) The lookup for existing edge thms happens wrt. to the background
theory
(http://isabelle.in.tum.de/repos/isabelle/rev/8715343af626#l1.80); this
fails if the edge to be looked up enters the stage in the course of
completion itself which does not immediately propagate to the background
theory (http://isabelle.in.tum.de/repos/isabelle/rev/8715343af626#l1.89)

b) Additionally, the completion needs to observe a topological order of
class hierarchy edges in order to when completing c -> d from c -> e and
e -> d that each edge has either been present from the very beginning or
has been added by completion before.  I do not know whether the current
code does the job.

So far.  I will stop for today, and I am not sure when I am able to turn
back on the issue.  But maybe I have found enough that the original
authors can comment on it.

Cheers,
	Florian

-- 

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: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121229/1184cd0b/attachment.sig>