Kevin Lee (Jul 03 2023 at 10:31): Kevin Lee (Jul 03 2023 at 10:31):Hi, I've proved some lemmas assuming all the variables are real, but the theorem that I want to prove requires some of them to be ints. What's the best way to resolve this? Is there a way to say that since the lemmas hold for reals, they hold for ints too? Or do I have to modify the proofs of the lemmas?
Manuel Eberl (Jul 03 2023 at 10:38):It's probably best if you can show us what that theorem statement actually is.
Manuel Eberl (Jul 03 2023 at 10:39):Typically you can just instantiate your real-valued theorem with whatever integers you want to apply it to, cast to real, e.g. with the function of_int :: int ⇒ real. (well, of_int actually has a more general type, something like int ⇒ 'a :: ring or whatever)
Manuel Eberl (Jul 03 2023 at 10:40):But there are a few caveats. For example, if you have a theorem that talks about an indexed sum over some variable x or the set of values between {a..b} then it makes a huge difference whether the type in question is real or int and there is no way to convert one to the other because the statements are very different.
Kevin Lee (Jul 03 2023 at 10:51):lemma L_Greater_Than_lm:
fixes m N L l :: real
assumes "m ≥ 3"
assumes "N ≥ 2*m"
assumes "L = (2/3 + sqrt (8*N/m - 8)) - (1/2 + sqrt (6*N/m - 3))"
shows "l ≥ 2 ∧ N ≥ 7*l^2*m^3 ⟹ L > l*m"
lemmas L_Greater_Than_2m [simp] = L_Greater_Than_lm [where l=2, simplified]
In the theorem, m and N are ints, assumptions are m>=3, N>=28*m^3.
So how do I show the statement L > 2*m?
Yong Kiam (Jul 04 2023 at 01:04):manually, it seems you'll need to help it along by showing that 3 <= m and 28 * m^3 <= N implies 2*m <= N (if you dropped that assumption)
Last updated: Apr 27 2024 at 16:16 UTC