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






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