Re: [isabelle] Strange behavior of equality?

Hello Christian,

> lemma "R n m = R' n m"
> proof (rule iffI)
>   show "R n m ==> R' n m" sorry
>   show "R' n m ==> R n m" sorry -- "*"
> qed

The problem here is that you use meta-implication "==>" within the "show" statement. "show" only tries to match the assumptions made by "assume" and the conclusion of the "show" with the goals to decide which goal to solve. Since you have no assumes, "R' n m" unifies with the first goal and the assumptions in the "show" statement become your new proof goals. However, the solved goal contained the assumption "R n m", so this is normally not a problem as qed can discharge this.

If you look at the proof state after the first sorry, you see the two goals:

"R n m ==> R n m"
"R' n m ==> R n m"

Unfortunately, your next "show" has the conclusion "R n m", which unifies with the first goal, so the first goal gets solved again instead of the second.

A simple solution would be to insert "prefer 2" between your two proofs, but it would be better style to use proper assumes:

lemma "R n m = R' n m"
proof (rule iffI)
  assume "R n m" thus "R' n m" sorry
  assume "R' n m" thus "R n m" sorry

Andreas Lochbihler

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