*To*: Christian Doczkal <c.doczkal at stud.uni-saarland.de>*Subject*: Re: [isabelle] Strange behavior of equality?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 16 Apr 2009 10:51:34 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1239791141.12445.15.camel@laptop>*References*: <1239791141.12445.15.camel@laptop>*Sender*: bhuffman0 at gmail.com

I have been annoyed by this behavior as well. To understand what is going on, it is helpful to look at the intermediate proof state using "next": lemma "R n m = R' n m" proof (rule iffI) The initial proof state is what you would expect: > goal (2 subgoals): > 1. R n m ==> R' n m > 2. R' n m ==> R n m show "R n m ==> R' n m" sorry next Now the proof state is: > goal (2 subgoals): > 1. R n m ==> R n m > 2. R' n m ==> R n m Instead of solving the first subgoal, it just replaced it with another one. Basically, it has applied "R n m ==> R' n m" to the first subgoal, as an introduction rule. show "R' n m ==> R n m" sorry next After this step, the proof state is: > goal (2 subgoals): > 1. R n m ==> R' n m > 2. R' n m ==> R n m Apparently, it applied "R' n m ==> R n m" to the first subgoal, which returns us to the original proof state. If it had applied the rule to the second subgoal instead, then qed would have worked. Evidently, Isar works by applying the rule to the first subgoal that matches. By the way, I just realized that your proof script works if you prove the subgoals in the opposite order: 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 Using "next" just before the "qed" shows the proof state to be nothing but trivial implications, which can be discharged by "qed". > goal (2 subgoals): > 1. R n m ==> R n m > 2. R' n m ==> R' n m Basically, it seems that using "show" with a meta-implication (==>) discharges the first subgoal that matches the conclusion, and adds new subgoals corresponding to each assumption. I would be surprised if this is an intentional feature of Isar; my guess is that it is an accidental feature of the way Isar proofs are implemented. Here's a proof script that I came up with that takes advantage of this "feature". lemma "Q & P ==> P & Q" proof - show "P ==> Q ==> P & Q" by (rule conjI) show "Q & P ==> P" by (rule conjunct2) show "Q & P ==> Q" by (rule conjunct1) qed - Brian On Wed, Apr 15, 2009 at 3:25 AM, Christian Doczkal < c.doczkal at stud.uni-saarland.de> wrote: > 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 >

**References**:**[isabelle] Strange behavior of equality?***From:*Christian Doczkal

- Previous by Date: [isabelle] locales & category theory
- Next by Date: Re: [isabelle] Strange behavior of equality?
- Previous by Thread: Re: [isabelle] Strange behavior of equality?
- 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