[isabelle-dev] Unproven class relation finite_lattice_complete < countable
florian.haftmann at informatik.tu-muenchen.de
Sat Dec 29 21:20:24 CET 2012
The last significant changeset seems to be
classrel and arity completion by krauss/schropp;
The critical code starting at
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
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
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev