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