Okay I did some more experiments and I was now, interestingly enough,
completely unable to reproduce the situation where Green /didn't/
timeout. So I have no idea what was going on there; perhaps I made a
mistake in testing it. I don't know.
It might be wise to remove "continuous_on_discrete" etc. from
intro/continuous_intros and declare it as a simp rule instead. I'm still
not quite sure what causes these problems. I attached a log of blast
with "blast_trace" enabled.
Manuel
On 01/09/2018 14:20, Makarius 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.
>
> 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?
>
>
> Makarius
>
>
> On 01/09/18 13:19, Lawrence Paulson wrote:
>> Surely the main issue that blast somehow behaves differently depending upon
>> which machine it’s running on?
>>
>> Larry
>>
>>> On 31 Aug 2018, at 22:35, Makarius wrote:
>>>
>>> On 31/08/18 22:00, Manuel Eberl wrote:
That's interesting. I suspected one of the "continuous_on" rules would
be the cause. In any case, I don't know how the unification works
exactly w.r.t. sorts, but the "continuous_on_discrete" rule does not
apply to this goal at all due to its restrictive type class constraint.
>>> Blast does its own unification, without taking fully account of types
>>> and type classes. The found proof is then reconstructed as in "fast" and
>>> its friends, using regular Isabelle term + type unification.
>>>
>>> Larry should be able to say more precisely, what the limits of blast are.
[0]
¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc))
C1_differentiable_on S - Sa)) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool
moving formula to unsafe list
+
[0]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
[1]
¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc))
C1_differentiable_on S - Sa)) :: bool ⇒ bool
branch split: 2 new subgoals
+
[1]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool
moving formula to unsafe list
+
[1]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool (Unsafe)
branch closed by rule
(duplicating)
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool
moving formula to unsafe list
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool
(Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool
(Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool
(Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool
(Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
[2]
¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc))
C1_differentiable_on S - Sa)) :: bool ⇒ bool
branch split: 2 new subgoals
+
[2]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool
moving formula to unsafe list
+
[2]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool (Unsafe)
branch closed by rule
(duplicating)
[2]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool
moving formula to unsafe list
[2]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool
(Unsafe)
branch extended (1 new subgoal)
(duplicating)
[1]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split:
