Re: [isabelle] Strange behavior of equality?
> 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 -- "*"
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and