[isabelle] using identity for simplification with different type



hi all,

in the following theory lemma tl1 proves an identity which lemma tl2 tries
to use.
however the proof of tl2 fails (tl1's proof works fine.)
I think the problem is that in tl1 the identity is between reals,
while in tl2 it is between nats.
am I correct, and is there a convenient way to use tl1 despite that?

thnx




theory tmp_arith
imports Complex_Main
begin

    lemma tl1: "(6::real)*2^(2^100) = 3*2^(2^100+1)"
    by (simp del: power_numeral add: power_add)

    lemma tl2: "(5::real)^(6*2^(2^100)) = 5^(3*2^(2^100+1))"
    by (simp only: tl1)

end


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