*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Strange behavior of equality?*From*: Christian Doczkal <c.doczkal at stud.uni-saarland.de>*Date*: Wed, 15 Apr 2009 12:25:41 +0200

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**

**Follow-Ups**:**Re: [isabelle] Strange behavior of equality?***From:*Andreas Lochbihler

**Re: [isabelle] Strange behavior of equality?***From:*Brian Huffman

**Re: [isabelle] Strange behavior of equality?***From:*Makarius

- Previous by Date: Re: [isabelle] Code generation for inductive predicates
- Next by Date: Re: [isabelle] Obtaining the instantiation of variables in a proof
- Previous by Thread: Re: [isabelle] Code generation for inductive predicates
- Next by Thread: Re: [isabelle] Strange behavior of equality?
- Cl-isabelle-users April 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list