Re: [isabelle] Simplication Confusion?

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

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
 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)

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.


maybe "auto" instead of "simp" works there.


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
Raum: 01.11.059

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.