*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simplication Confusion?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 15 Aug 2007 08:16:50 -0700*In-reply-to*: <749b5dd60708140826p5e7288cdh88072c3d806d6d10@mail.gmail.com>*References*: <749b5dd60708140826p5e7288cdh88072c3d806d6d10@mail.gmail.com>*User-agent*: KMail/1.9.6

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 the simplifier 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 I looked 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 simplifier converts 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 *) I imagine that this behavior took some extra work to implement, so there must have been a reason for it. Can anyone explain? - Brian

**Follow-Ups**:**Re: [isabelle] Simplication Confusion?***From:*Tobias Nipkow

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

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