[isabelle] blast looping and backtracking

Dear list,

I like to tag unconditional facts (`0 < 1`, `X ⊆ X`, `x ∈ {x}`) as
[intro!] rules. In combination with a suitable elim rule and goal
statement, this lead to a looping behaviour of blast that I did not
expect. Here is a minimal, contrived example:

definition "P x ≡ True"

lemma [intro]: "P x"
  unfolding P_def ..

lemma [elim]:
  assumes "True"
  obtains "¬(P x)" | "P x"
  (*if we were to swap the order of the cases, blast does not loop*)
  (*obtains "P x" | "¬(P x)"*)
  by blast

lemma "True ⟹ False"
  by blast (*loops*)

Looking at the output of blast (`setup "Config.put_global Blast.trace
true"`), it seems to me that
1. the elim rule is applied
2. the first subgoal closed by the intro rule
3. the second subgoal cannot be closed and backtracking occurs
4. repeat with 1.

If, as written in the comment above, we were to swap the order of the
cases in the elim-rule, blast will not loop. Is this the expected
behaviour of blast? I would have expected that the elim-rule will not be
applied again after backtracking occurs.

For the sake of completeness, here is a more realistic example of the
same problem:

declare insertI1[intro] (*"a ∈ insert a A"*)
(*subsetCE is already declared as [elim] in the distro*)
declare subsetCE[elim] (*A ⊆ B ⟹ (c ∉ A ⟹ Q) ⟹ (c ∈ B ⟹ Q) ⟹ Q*)

lemma "(∀X. X ⊆ X) ⟹ 1 + 1 = 2"
  by blast (*loops*)

Best wishes,


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.