[isabelle] Incomplete goal may cause proof methods of later goals to loop.



I'd expect the following issue to be well known but didn't find it in the "known issues".

When inserting a new goal (have ...) into a proof, proof methods belonging to later goals seem to be applied wrongly sometimes causing them to loop and make my PC noisy after a while. ;)

Here's a small example:

lemma assumes "m ∈ M" and "M ⊆ N" shows "m ∈ N" proof -
have P(* incomplete goal *)
show "m ∈ N" using assms by (metis in_mono) (* loops *)
qed

The "show" already produces a syntax error but the later "by" is applied anyhow yet to the wrong goal causing it to loop.

A student of mine is highly skilled in producing such situations in many theorems simultaneously causing the editor to become very unresponsive.

Best Benedikt




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