Re: [isabelle] Odd failure to match local statement with pending goal.



Hello all,

As Larry stated, this is indeed a strange problem. I tried to find a minimal example; here is what I came up with:

-------------------
lemma
  shows  "⋀c d. d ∈ Z ⟹ x = c ⟹
        ∃e. e ∈ {_. ∃e. e ∈ Z ∧ y = e}"
  apply (unfold mem_Collect_eq)
proof -
  fix s t
  assume "x = s" and "t ∈ Z"
  then show "∃s t. t ∈ Z ∧ y = t"
    sorry
qed
-------------------

The show statement fails with

>    *** Local statement will fail to refine any pending goal
>    *** Failed attempt to solve goal by exported rule:
>    ...

Any of the following actions will make this example succeed:

 - Rename any of the two existentially bound variables in the shows
   statement
 - Rename any of the two existentially bound variables in the show
   statement
 - Rename any of the variables mentioned by fix
 - Remove any one of the assume statements
 - Remove the "apply (unfold ...)" and state the unfolded goal directly

This was tested on a relatively current repository version of Isabelle (last week or so).

  -- Lars





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