[isabelle] Simplication Confusion?



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





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