*To*: Richard Warburton <richard.warburton at gmail.com>*Subject*: Re: [isabelle] Simplication Confusion?*From*: Steven Obua <obua at in.tum.de>*Date*: Wed, 15 Aug 2007 12:44:09 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <749b5dd60708140826p5e7288cdh88072c3d806d6d10@mail.gmail.com>*References*: <749b5dd60708140826p5e7288cdh88072c3d806d6d10@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.7.3) Gecko/20040915

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. Steven -- Steven Obua Technische Universität München Institut für Informatik Boltzmannstr. 3 D-85748 Garching Tel: ++49 (0)89 / 289-17328 EMail: obua at in.tum.de Raum: 01.11.059

**Follow-Ups**:**Re: [isabelle] Simplication Confusion?***From:*Richard Warburton

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

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