# [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 -
from cos_add
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
from cos_add
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.*