# HG changeset patch
# User hoelzl
# Date 1267720125 -3600
# Node ID 384ad08a1d1b285da60d5111c2a2374b8728f47c
# Parent  43b93e294522cb3e62a46479c276b92c8cff94c8
Added natfloor and floor rules for multiplication and power.

diff -r 43b93e294522 -r 384ad08a1d1b src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Thu Mar 04 17:09:44 2010 +0100
+++ b/src/HOL/RComplete.thy	Thu Mar 04 17:28:45 2010 +0100
@@ -653,6 +653,18 @@
 lemma floor_subtract_one: "floor (x - 1) = floor x - 1"
   by (rule floor_diff_one) (* already declared [simp] *)
 
+lemma le_mult_floor:
+  assumes "0 \<le> (a :: real)" and "0 \<le> b"
+  shows "floor a * floor b \<le> floor (a * b)"
+proof -
+  have "real (floor a) \<le> a"
+    and "real (floor b) \<le> b" by auto
+  hence "real (floor a * floor b) \<le> a * b"
+    using assms by (auto intro!: mult_mono)
+  also have "a * b < real (floor (a * b) + 1)" by auto
+  finally show ?thesis unfolding real_of_int_less_iff by simp
+qed
+
 lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   unfolding real_of_nat_def by simp
 
@@ -821,6 +833,19 @@
   apply simp
 done
 
+lemma less_natfloor:
+  assumes "0 \<le> x" and "x < real (n :: nat)"
+  shows "natfloor x < n"
+proof (rule ccontr)
+  assume "\<not> ?thesis" hence *: "n \<le> natfloor x" by simp
+  note assms(2)
+  also have "real n \<le> real (natfloor x)"
+    using * unfolding real_of_nat_le_iff .
+  finally have "x < real (natfloor x)" .
+  with real_natfloor_le[OF assms(1)]
+  show False by auto
+qed
+
 lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
   apply (rule iffI)
   apply (rule order_trans)
@@ -851,7 +876,7 @@
 
 lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
   apply (unfold natfloor_def)
-  apply (subst nat_int [THEN sym]);back;
+  apply (subst (2) nat_int [THEN sym])
   apply (subst eq_nat_nat_iff)
   apply simp
   apply simp
@@ -905,6 +930,83 @@
   apply simp
 done
 
+lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
+  natfloor (x / real y) = natfloor x div y"
+proof -
+  assume "1 <= (x::real)" and "(y::nat) > 0"
+  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
+    by simp
+  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
+    real((natfloor x) mod y)"
+    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
+  have "x = real(natfloor x) + (x - real(natfloor x))"
+    by simp
+  then have "x = real ((natfloor x) div y) * real y +
+      real((natfloor x) mod y) + (x - real(natfloor x))"
+    by (simp add: a)
+  then have "x / real y = ... / real y"
+    by simp
+  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
+    real y + (x - real(natfloor x)) / real y"
+    by (auto simp add: algebra_simps add_divide_distrib
+      diff_divide_distrib prems)
+  finally have "natfloor (x / real y) = natfloor(...)" by simp
+  also have "... = natfloor(real((natfloor x) mod y) /
+    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
+    by (simp add: add_ac)
+  also have "... = natfloor(real((natfloor x) mod y) /
+    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
+    apply (rule natfloor_add)
+    apply (rule add_nonneg_nonneg)
+    apply (rule divide_nonneg_pos)
+    apply simp
+    apply (simp add: prems)
+    apply (rule divide_nonneg_pos)
+    apply (simp add: algebra_simps)
+    apply (rule real_natfloor_le)
+    apply (insert prems, auto)
+    done
+  also have "natfloor(real((natfloor x) mod y) /
+    real y + (x - real(natfloor x)) / real y) = 0"
+    apply (rule natfloor_eq)
+    apply simp
+    apply (rule add_nonneg_nonneg)
+    apply (rule divide_nonneg_pos)
+    apply force
+    apply (force simp add: prems)
+    apply (rule divide_nonneg_pos)
+    apply (simp add: algebra_simps)
+    apply (rule real_natfloor_le)
+    apply (auto simp add: prems)
+    apply (insert prems, arith)
+    apply (simp add: add_divide_distrib [THEN sym])
+    apply (subgoal_tac "real y = real y - 1 + 1")
+    apply (erule ssubst)
+    apply (rule add_le_less_mono)
+    apply (simp add: algebra_simps)
+    apply (subgoal_tac "1 + real(natfloor x mod y) =
+      real(natfloor x mod y + 1)")
+    apply (erule ssubst)
+    apply (subst real_of_nat_le_iff)
+    apply (subgoal_tac "natfloor x mod y < y")
+    apply arith
+    apply (rule mod_less_divisor)
+    apply auto
+    using real_natfloor_add_one_gt
+    apply (simp add: algebra_simps)
+    done
+  finally show ?thesis by simp
+qed
+
+lemma le_mult_natfloor:
+  assumes "0 \<le> (a :: real)" and "0 \<le> b"
+  shows "natfloor a * natfloor b \<le> natfloor (a * b)"
+  unfolding natfloor_def
+  apply (subst nat_mult_distrib[symmetric])
+  using assms apply simp
+  apply (subst nat_le_eq_zle)
+  using assms le_mult_floor by (auto intro!: mult_nonneg_nonneg)
+
 lemma natceiling_zero [simp]: "natceiling 0 = 0"
   by (unfold natceiling_def, simp)
 
@@ -957,7 +1059,7 @@
   apply (unfold natceiling_def)
   apply (case_tac "x < 0")
   apply simp
-  apply (subst nat_int [THEN sym]);back;
+  apply (subst (2) nat_int [THEN sym])
   apply (subst nat_le_eq_zle)
   apply simp
   apply (rule ceiling_le)
@@ -1042,72 +1144,5 @@
   apply simp
 done
 
-lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
-  natfloor (x / real y) = natfloor x div y"
-proof -
-  assume "1 <= (x::real)" and "(y::nat) > 0"
-  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
-    by simp
-  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
-    real((natfloor x) mod y)"
-    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
-  have "x = real(natfloor x) + (x - real(natfloor x))"
-    by simp
-  then have "x = real ((natfloor x) div y) * real y +
-      real((natfloor x) mod y) + (x - real(natfloor x))"
-    by (simp add: a)
-  then have "x / real y = ... / real y"
-    by simp
-  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y"
-    by (auto simp add: algebra_simps add_divide_distrib
-      diff_divide_distrib prems)
-  finally have "natfloor (x / real y) = natfloor(...)" by simp
-  also have "... = natfloor(real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
-    by (simp add: add_ac)
-  also have "... = natfloor(real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
-    apply (rule natfloor_add)
-    apply (rule add_nonneg_nonneg)
-    apply (rule divide_nonneg_pos)
-    apply simp
-    apply (simp add: prems)
-    apply (rule divide_nonneg_pos)
-    apply (simp add: algebra_simps)
-    apply (rule real_natfloor_le)
-    apply (insert prems, auto)
-    done
-  also have "natfloor(real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y) = 0"
-    apply (rule natfloor_eq)
-    apply simp
-    apply (rule add_nonneg_nonneg)
-    apply (rule divide_nonneg_pos)
-    apply force
-    apply (force simp add: prems)
-    apply (rule divide_nonneg_pos)
-    apply (simp add: algebra_simps)
-    apply (rule real_natfloor_le)
-    apply (auto simp add: prems)
-    apply (insert prems, arith)
-    apply (simp add: add_divide_distrib [THEN sym])
-    apply (subgoal_tac "real y = real y - 1 + 1")
-    apply (erule ssubst)
-    apply (rule add_le_less_mono)
-    apply (simp add: algebra_simps)
-    apply (subgoal_tac "1 + real(natfloor x mod y) =
-      real(natfloor x mod y + 1)")
-    apply (erule ssubst)
-    apply (subst real_of_nat_le_iff)
-    apply (subgoal_tac "natfloor x mod y < y")
-    apply arith
-    apply (rule mod_less_divisor)
-    apply auto
-    using real_natfloor_add_one_gt
-    apply (simp add: algebra_simps)
-    done
-  finally show ?thesis by simp
-qed
 
 end
diff -r 43b93e294522 -r 384ad08a1d1b src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Thu Mar 04 17:09:44 2010 +0100
+++ b/src/HOL/RealPow.thy	Thu Mar 04 17:28:45 2010 +0100
@@ -6,7 +6,7 @@
 header {* Natural powers theory *}
 
 theory RealPow
-imports RealDef
+imports RealDef RComplete
 begin
 
 (* FIXME: declare this in Rings.thy or not at all *)
@@ -107,6 +107,28 @@
     by (rule power_le_imp_le_base)
 qed
 
+subsection {*Floor*}
+
+lemma floor_power:
+  assumes "x = real (floor x)"
+  shows "floor (x ^ n) = floor x ^ n"
+proof -
+  have *: "x ^ n = real (floor x ^ n)"
+    using assms by (induct n arbitrary: x) simp_all
+  show ?thesis unfolding real_of_int_inject[symmetric]
+    unfolding * floor_real_of_int ..
+qed
+
+lemma natfloor_power:
+  assumes "x = real (natfloor x)"
+  shows "natfloor (x ^ n) = natfloor x ^ n"
+proof -
+  from assms have "0 \<le> floor x" by auto
+  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
+  from floor_power[OF this]
+  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
+    by simp
+qed
 
 subsection {*Various Other Theorems*}
 
@@ -131,4 +153,5 @@
 lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
 by (case_tac "n", auto)
 
+
 end