It’s important to understand that blast knows nothing about type classes. This 
isn’t a problem for rules like order_trans, where the type class constraint 
would be satisfied in most cases. But it’s fatal for continuous_on_discrete: it 
will succeed in all cases, but if the type class constraint isn’t satisfied 
(and it usually won’t be), then the proof will fail and it’s not clear that 
backtracking will find an alternative. The PROOF FAILED message (if it still 
exists) alerts us to this.


> On 1 Sep 2018, at 13:39, Manuel Eberl <> wrote:
>> This thread consists of two sub-threads. The hardware / OS question
>> still needs to be sorted out: it might be something with Arch Linux.
> I don't really have much of an opportunity to test this on other systems
> atm, but I'll see what I can do.
>> Apart from that, my reading of blast.ML is that the "continuous_on" rule
>> is applied in the search independently of its fine-grained type
>> information. Is that correct?
> Even if it is, it has no preconditions, so I don't see how it could
> cause nontermination.
> Manuel

isabelle-dev mailing list

Reply via email to