Proving with (co)free links does not work correctly

[till]

In source:trunk/Proofs/InferBasic.hs, the information about the free and cofree definition links is not assembled correctly. Strangely, changeset:11039 seems to cause this problem. Moreover, the theory in the target of the (co)free link needs to be assembled, but also this does not work correctly. The attached file can be used as a test file (with prover truthtables).

[maeder]

The theory displayed at the target of the blue link (with "Show Theory") is:

prop harry, john, mary
. (harry=>john) %(Ax_0)%
. (john=>not(harry)) %(Ax_1)%

Whereas much less is displayed without the change in source:trunk/Proofs/TheoremHideShift.hs in computeTheory. Maybe "Proofs-Automatic" or Proofs.Global also need to consider (co)free definition links?

[till]

OK, I have found and fixed the problem. But another problem is that with the attached file, I get two free links, differing in the following way:

13,18c13
<  propMap = fromList [(harry,
< harry),
< (john,
< john),
< (mary,
< mary)]},
---
>  propMap = fromList []},

[maeder]

These are two different representations of the identity morphism. In CASL a I avoid the longer version

[maeder]

Can this ticket be closed? I get only one free link. Darwin disproves the target, truthtables proves it.

[till]

Replying to maeder:

Can this ticket be closed? I get only one free link. Darwin disproves the target, truthtables proves it.

This behaviour is of course unsatisfactory. The function hidingWarning in source:Proofs/EdgeUtils.hs should be (adapted and) also called in the case of incoming free definition links.