[isabelle] A bug in chained proof mode
I think I have found a bug in the chained proof mode, that occurs for equality proofs if one of the proof used in the chain is a reflexive proof. As an example, the following proof fails, even though (as far as I understand the chain mode) it should succeed:
lemma chain_bug: "e1 = e2 ⟹ f e1 = f e2"
assume eq1: "e1 = e2"
have "f e1 = f e2" by (rule arg_cong[OF eq1])
have "f e2 = f e2" by (simp)
have "f e1 = f e2".
Although it may seem silly to write a proof that “f e2 = f e2”, the reason it comes up is that the proof is machine-generated, and sometimes it is easier to generate a proof that something equals itself rather than checking explicitly for that fact.
Anyway, just thought I would report this.
This archive was generated by a fusion of
Pipermail (Mailman edition) and