[isabelle] using identity for simplification with different type
in the following theory lemma tl1 proves an identity which lemma tl2 tries
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?
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)
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