[isabelle-dev] Problem in the AFP

[Thiemann, Rene]

Dear Peter,

>> It's the operation identification phase of Autoref,
>> quite difficult to debug ... I have not yet looked at it due to
>> ITP-deadline. 
> 
> I found the culprit:
> 
> summary:     adapting entries to new Deriving mechanism
> 
> in LTL_to_GBA-theory, this removes a linorder-constraint on
> create_name_igba, which causes the breakdown, because later,
> autoref is only given rules to refine create_name_igba for 
> 'a::linorder, but the respective lemmas do not repeat the
> linorder-constraint. 
> 
> I fixed it by adding the linorder-constraint to the refinement, leaving
> the abstract version general.

sorry, for this problem. I first locally tried to replace the linorder class-constraint
by some compare class-constraint, since the new derive-generator produces class-constraints
of the form mytype :: (compare,...,compare)compare. However, for lack of time I did not manage
to fully adapt your entry from linorder to compare before ITP submission. To this end, I 
manually adapted in 88dc498667ff the generation of linear orders in LTL_to_GBA_impl. 
Since also other entries prefer the mytype :: (linorder, ..., linorder)linorder constraint,
I adding support for it in derive in 470b9d92f174 and then integrate it in LTL_to_GBA_impl in
8afc741ecb48, so that the adaptation of LTL_to_GBA_impl in total only was a change of a single
line, namely the import statement from the old to the new derive.

However, the problem was that I overlooked in 88dc498667ff that it also contained a change in 
LTL_to_GBA which removed the linorder constraint, and which shouldn't have been checked in.

Anyway, thanks for fixing the problem,
René