# [isabelle] question about using identities for rewriting

```this question is about the behaviour of 'auto' in problems that
require rewriting.
in both examples below the lemma states that "expr1^2 = expr2^2", which is true
since "expr1=expr2". in the first case the proof is short -

lemma tt1 :
fixes a b :: real
shows "(cos(a+b))^2 =
(cos(a)*cos(b) - sin(a)*sin(b))^2"
proof -
show ?thesis
by   auto
qed

in the second case the equality of the expressions is slightly more
complicated so it is
proved in a sub lemma. but using the result in an analogous way FAILS :

lemma tt2 :
fixes a b :: real
shows "(1 + 2*cos(a+b))^2 =
(1 + cos(a+b) + cos(a)*cos(b) - sin(a)*sin(b))^2"
proof -
{
fix  c d::real
have "1 + 2*cos(c+d) =
1 + cos(c+d) + cos(c)*cos(d) - sin(c)*sin(d)"
by auto
}
from this
show ?thesis
by   auto
(* DOESN'T TERMINATE*)
qed

I was able to fix the code s.t. the proof terminates successfully,
by adding an appropriate lemma to the 'from' part :

from this
Power.idom_class.power2_eq_iff
[of "1 + 2*cos(a+b)"
"1 + cos(a+b) + cos(a)*cos(b) - sin(a)*sin(b)"]
show ?thesis
by   auto

the added lemma states the obvious

lemma power2_eq_iff: "x\<^sup>2 = y\<^sup>2 \<longleftrightarrow>
x = y \<or> x = - y"

but since the first example must have used this lemma (or something
very similar,)
I'd like to understand why I had to add it explicitly and also to
instantiate it myself
(otherwise it refused to work,)
while in the first example this wasn't necessary.

thanx, Noam

--
I can't see very far,
I must be standing on the shoulders of midgets.

```

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