[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.