Email Gateway (Aug 22 2022 at 10:54): Email Gateway (Aug 22 2022 at 10:54):From: noam neer <noamneer@gmail.com>
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
Email Gateway (Aug 22 2022 at 10:54):From: Lars Noschinski <noschinl@in.tum.de>
Yes, you are correct and no, there is no convenient way.
Last updated: Apr 26 2024 at 20:16 UTC