Email Gateway (Aug 22 2022 at 17:50): Email Gateway (Aug 22 2022 at 17:50):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
In informal mathematics, when an identity is true for real numbers, it is
automatically true for natural numbers. How this informal principle could
be formalized in Isabelle?
For example, I want to prove that
"a ≥ 1 ⟹ (k::nat)(k+2a-1) + 2(a + k) = (Suc k)((Suc k)+2*a-1)"
My idea was to prove it for real numbers first (without the unnecessary
restriction a ≥ 1) and then to use reductio ad absurdum with natural
numbers, but I think that there should be an easier way to do it. Also, if
I'm not mistaken, it is easier to prove identities for real in Isabelle
than for nat.
Kind Regards,
Jose M.
lemma HDGFHFreal: "(k::real)(k+2a-1) + 2(a + k) = (k+1)((k+1)+2*a-1)"
by (smt mult.commute semiring_normalization_rules(3))
lemma HDGFHF: "a ≥ 1 ⟹ (k::nat)(k+2a-1) + 2(a + k) = (Suc k)((Suc
k)+2*a-1)"
proof (rule classical)
obtain kk where "kk = real k" by simp
obtain aa where "aa = real a" by simp
assume "a ≥ 1"
assume "¬ (k(k+2a-1) + 2(a + k) = (Suc k)((Suc k)+2*a-1))"
then have "(k(k+2a-1) + 2(a + k) ≠ (k+1)((k+1)+2*a-1))" by simp
then have "real (k(k+2a-1) + 2(a + k)) ≠ real ((k+1)((k+1)+2*a-1))"
using of_nat_eq_iff by blast
then have "(kk(kk+2aa-1) + 2(aa + kk)) ≠ ((kk+1)((kk+1)+2*aa-1))"
using diff_mult_distrib2 by auto
then have False
using ‹k * (k + 2 * a - 1) + 2 * (a + k) ≠ (k + 1) * (k + 1 + 2 * a -
1)› diff_mult_distrib2 by auto
then show ?thesis by blast
qed
Last updated: Apr 24 2024 at 04:17 UTC