Re: [isabelle] Simplication Confusion?



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





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