theory Blatt8
imports Main
begin
lemma plus_div_less_self:
fixes a b c :: nat
assumes "a < c" and "b < c"
shows "(a + b) div c < c"
proof (cases "2 \ c")
case True
from assms have "a + b \ c + (c - 1)" by simp
then have "(a + b) div c \ (c + (c - 1)) div c" by (rule div_le_mono)
moreover have "(c + (c - 1)) div c < 2" using `2 \ c`
by (simp only: div_add_self1) simp
ultimately have "(a + b) div c < 2" by simp
with `2 \ c` show "(a + b) div c < c" by auto
next
case False then show ?thesis using assms by simp
qed
lemma times_div_less_self:
fixes a b c :: nat
assumes "a < c" and "b < c"
shows "(a * b) div c < c"
proof (cases "2 \ c")
case True
then obtain d where "c = Suc d" by (cases c) simp_all
then have "c * c - 1 = (c - 1) + (c - 1) * c" by simp
then have "(c * c - 1) div c = ((c - 1) + (c - 1) * c) div c" by simp
also have "\ = c - 1 + (c - 1) div c" using `c = Suc d`
by (simp only: div_mult_self1)
also have "\ = c - 1" using `c = Suc d` by simp
finally have dec_c: "(c * c - 1) div c = c - 1" .
from assms have "a * b < c * c" by (simp add: mult_strict_mono)
then have "a * b \ c * c - 1" by simp
then have "(a * b) div c \ (c * c - 1) div c" by (rule div_le_mono)
with dec_c have "(a * b) div c \ c - 1" by simp
then show "(a * b) div c < c" using `c = Suc d` by simp
next
case False then have "c = 0 \ c = 1" by arith
then show ?thesis using assms by simp
qed
find_theorems "(_ + _) * _ = _"
find_theorems "((_::nat) + _) * _ = _"
find_theorems "((?m::nat) + _) * _ = ?m * _ + _"