Re: [isabelle] Simplication Confusion?



On Tuesday 14 August 2007, Richard Warburton wrote:
> 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 discovered some interesting simplifier quirks when I tried this out.

This term:
 "(ALL i. (terminated(exec(p,i)) --> (exec(p,i) = exec(q,i)) |
  (terminated(exec(q,i)) --> (exec(p,i) = exec(q,i)))))"

simplifies to this:
  "ALL i. terminated (exec (p, i))  -->
        terminated (exec (q, i))  --> exec (p, i) = exec (q, i)"

When the above term is present in the assumptions, I assumed that the 
simplifier would add a conditional rewrite like this:
  "!!i. [| terminated (exec (p, i)); terminated (exec (q, i)) |]
        ==> exec (p, i) == exec (q, i)"

That rewrite would have been sufficient to solve the next subgoal. But when I 
looked at the simplifier trace, I found this rewrite instead:
  "!!i. [| terminated (exec (p, i)); terminated (exec (q, i)) |]
        ==> (exec (p, i) = exec (q, i)) == True"

Very strange!

I tried tracing a few simple examples to figure out how the simplifier 
converts assumptions into rewrites, and here is what I found:

Assumption: "P --> x = y"
Rewrite: "P ==> x == y"

Assumption: "P y --> x = y"
Rewrite: "P y ==> x == y"

Assumption: "P x --> x = y"
Rewrite: "P x ==> y == x"  (* notice reversed orientation! *)

Assumption: "P x y --> x = y"
Rewrite: "P x y ==> (x = y) == True"  (* similar to example above *)

I imagine that this behavior took some extra work to implement, so there must 
have been a reason for it. Can anyone explain?

- Brian









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