Re: [isabelle] Simplication Confusion?



Brian Huffman schrieb:
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!

Admittedly, I had to ponder this for quite some time before I realized what was going on: Isabelle tried to orient the rule in either direction but failed because this would immediately lead to death by nontermination: both exec(p,i) and exec(q,i) appear in the premises and this would lead to a recursive call of the simplifier again and again. Hence all that is left is the == True version - better than nothing.

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

This one is easy. The direction x==y is no good: which y should we take when applying the rule? The chosen orientation means that any y will get rewritten to some x for which we happen to have the fact "P x" available.

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

Same as above, this is the only way to avoid nontermination.

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

Yes :-)

- Brian

Tobias





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