*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Simplication Confusion?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 16 Aug 2007 21:38:56 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <200708150816.51192.brianh@cs.pdx.edu>*References*: <749b5dd60708140826p5e7288cdh88072c3d806d6d10@mail.gmail.com> <200708150816.51192.brianh@cs.pdx.edu>*User-agent*: Thunderbird 2.0.0.0 (Macintosh/20070326)

Brian Huffman schrieb:

On Tuesday 14 August 2007, Richard Warburton wrote:lemma "(p,q) : \<smile> ==> (q,p) : \<smile>" (* symmetry *) proof - assume "(p, q) : \<smile>" hence "(ALL i. (terminated(exec(p,i)) --> (exec(p,i) = exec(q,i)) | (terminated(exec(q,i)) --> (exec(p,i) = exec(q,i)))))" by (rule terminequivalent.induct) hence "(ALL i. (terminated(exec(q,i)) --> (exec(q,i) = exec(p,i)) | (terminated(exec(p,i)) --> (exec(q,i) = exec(p,i)))))" by simp thus "(q, p) : \<smile>" by (rule terminequivalent.step) qed However the middle simp step fails, it is happy to deduce "(ALL i. (terminated(exec(q,i)) --> (exec(q,i) = exec(p,i)) | (terminated(exec(p,i)) --> (exec(p,i) = exec(q,i)))))" or "(ALL i. (terminated(exec(q,i)) --> (exec(p,i) = exec(q,i)) | (terminated(exec(p,i)) --> (exec(q,i) = exec(p,i)))))" but it (and successive simp attempts) fail to recognise that equality is symmetric.I discovered some interesting simplifier quirks when I tried this out. This term: "(ALL i. (terminated(exec(p,i)) --> (exec(p,i) = exec(q,i)) | (terminated(exec(q,i)) --> (exec(p,i) = exec(q,i)))))" simplifies to this: "ALL i. terminated (exec (p, i)) --> terminated (exec (q, i)) --> exec (p, i) = exec (q, i)"When the above term is present in the assumptions, I assumed that thesimplifier would add a conditional rewrite like this:"!!i. [| terminated (exec (p, i)); terminated (exec (q, i)) |] ==> exec (p, i) == exec (q, i)"That rewrite would have been sufficient to solve the next subgoal. But when Ilooked at the simplifier trace, I found this rewrite instead:"!!i. [| terminated (exec (p, i)); terminated (exec (q, i)) |] ==> (exec (p, i) = exec (q, i)) == True" Very strange!

I tried tracing a few simple examples to figure out how the simplifierconverts assumptions into rewrites, and here is what I found:Assumption: "P --> x = y" Rewrite: "P ==> x == y" Assumption: "P y --> x = y" Rewrite: "P y ==> x == y" Assumption: "P x --> x = y" Rewrite: "P x ==> y == x" (* notice reversed orientation! *)

Assumption: "P x y --> x = y" Rewrite: "P x y ==> (x = y) == True" (* similar to example above *)

Same as above, this is the only way to avoid nontermination.

I imagine that this behavior took some extra work to implement, so there musthave been a reason for it. Can anyone explain?

Yes :-)

- Brian

Tobias

**References**:**[isabelle] Simplication Confusion?***From:*Richard Warburton

**Re: [isabelle] Simplication Confusion?***From:*Brian Huffman

- Previous by Date: [isabelle] help with recdef definition and induction
- Next by Date: Re: [isabelle] help with recdef definition and induction
- Previous by Thread: Re: [isabelle] Simplication Confusion?
- Next by Thread: [isabelle] update_thy
- Cl-isabelle-users August 2007 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