[isabelle-dev] Pending sort hypotheses

[Amine Chaieb]

I wonder why this restriction has been introduced in the first place. Is
it because sorts can be empty (i.e. there are no possible type
instances)? For sorts with instances it should even be logically correct
to eliminate such sorts constraints, when they are introduced
exclusively during the proof.


Amine.


Amine Chaieb wrote:

> OK, I see now that buried somewhere in Abstract_Rat old unconstrained
> rewrites have a new assupmtion
>
>
>   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
>
>
> That might explain some of the bahaviour.
>
>
> Amine.
>
>
> Amine Chaieb wrote:
>
>   
>> Dear all,
>>
>>
>> I am having problems with updating a theory, which used to work by the
>> end of last year.
>>
>>
>> Now I get at some point the following error: 
>>
>> Pending sort hypotheses: {ring_char_0,division_by_zero,field}
>>
>>
>> after simp has succeeded to solve the goal.
>>
>>
>> The problem is that none of by Hypotheses, assumptions or goal depend on
>> these sorts!!
>>
>>
>> I have tried to trace the simplifier (I had also a strange experience
>> here, even when I set the trace depth limit to 1000000 I still get a
>> broken trace at the same places with limit roughly 1000). In the over
>> 68K lines of trace there is no mention of any type 'a with those sorts.
>>
>>
>> The proof used to by one line (by simp).
>>
>>
>> Anybody knows how to explain this behaviour?
>>
>>
>> Best wishes,
>>
>> Amine.
>>
>> _______________________________________________
>> Isabelle-dev mailing list
>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>   
>>     
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>