# [isabelle] Strange behavior of equality?

```Hello

I want to prove that two relations are equal (I removed the actual
proofs since they do not matter here, rule iffI is also selected as
default rule)

theory Scratch
imports Main
begin

consts
R :: "nat => nat => bool"
R' :: "nat => nat => bool"

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

until * i get:
Successful attempt to solve goal by exported rule:
R n m ==> R' n m

Successful attempt to solve goal by exported rule:
R' n m ==> R n m

But the proof state is still:
goal (2 subgoals):
1. R n m ==> R' n m
2. R' n m ==> R n m

and hence the "qed" fails to finish the proof? Why are the goals not
removed after they have been successfully solved.

Strangely applying the initial rule at the end works as in:

lemma "R n m = R' n m"
proof -
have "R n m ==> R' n m" sorry
moreover have "R' n m ==> R n m" sorry
ultimately show ?thesis by (rule iffI)
qed

Can someone reproduce this or explain what is going on?

--
Gruß
Christian Doczkal
```

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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