Email Gateway (Aug 19 2022 at 16:23): Email Gateway (Aug 19 2022 at 16:23):From: Joachim Breitner <breitner@kit.edu>
Hi,
Real.thy contains the lemma
lemma natfloor_div_nat:
assumes "1 <= x" and "y > 0"
shows "natfloor (x / real y) = natfloor x div y"
but the first assumption is redundant:
lemma natfloor_div_nat:
assumes "y > 0"
shows "natfloor (x / real y) = natfloor x div y"
proof-
have "x ≤ 0 ∨ x ≥ 0 ∧ x < 1 ∨ 1 ≤ x" by arith
thus ?thesis
proof(elim conjE disjE)
assume *: "1 ≤ x"
show ?thesis by (rule Real.natfloor_div_nat[OF * assms])
next
assume *: "x ≤ 0"
moreover
from * assms have "x / y ≤ 0" by (simp add: field_simps)
ultimately
show ?thesis by (simp add: natfloor_neg)
next
assume *: "x ≥ 0" "x < 1"
hence "natfloor x = 0" by (auto intro: natfloor_eq)
moreover
from * assms have "x / y ≥ 0" and "x / y < 1" by (auto simp add: field_simps)
hence "natfloor (x/y) = 0" by (auto intro: natfloor_eq)
ultimately
show ?thesis by simp
qed
qed
Greetings,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC