*To*: "Steven Obua" <obua at in.tum.de>*Subject*: Re: [isabelle] Simplication Confusion?*From*: "Richard Warburton" <richard.warburton at gmail.com>*Date*: Wed, 15 Aug 2007 13:33:07 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <46C2D8F9.9080708@in.tum.de>*References*: <749b5dd60708140826p5e7288cdh88072c3d806d6d10@mail.gmail.com> <46C2D8F9.9080708@in.tum.de>

On 8/15/07, Steven Obua <obua at in.tum.de> wrote: > Richard Warburton wrote: > > >I have an equivalence relation that I am trying to prove symmetric, > >which is defined as > > > >lemma "(p,q) : \<smile> ==> (q,p) : \<smile>" > > > >It seems a very trivia proof to me, simply unfold the definition of > >the induction, use the symmetry of disjunction and equality and then > >apply the rules of the inductive definition, I want to do something > >like: > > > >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 initially thought this might be a precedence/binding > >problem (which motivated the extensive bracket use) but it didn't seem > >to resolve anything. I apologise if this seems like a trivial > >problem, but I am rather confused as to why simp is happy to exchange > >the terms in either place, but not both. > > > > Richard > > > > > > > maybe "auto" instead of "simp" works there. Thanks for the suggestion, but I have already tried auto as well, in fact I have even tried the more powerful methods like best. Its also the case that this fails to prove in a two step scenario, ie I can't simplify to one of the intermediate goals and then simplify again to the desired goal. Is there a way of seeing a 'trace' of the automatic method in order to better identify what is happening? Richard

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

**Re: [isabelle] Simplication Confusion?***From:*Steven Obua

- Previous by Date: Re: [isabelle] Simplication Confusion?
- Next by Date: Re: [isabelle] update_thy
- 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