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