# HG changeset patch
# User huffman
# Date 1315062109 25200
# Node ID a89d0ad8ed203cb74174037a760080123d5207bd
# Parent  21eb31192850e886be43972b6994454c17ff1563
shorten some proofs

diff -r 21eb31192850 -r a89d0ad8ed20 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Fri Sep 02 20:58:31 2011 -0700
+++ b/src/HOL/RComplete.thy	Sat Sep 03 08:01:49 2011 -0700
@@ -334,44 +334,30 @@
   by (unfold natfloor_def, simp)
 
 lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
-  apply (unfold natfloor_def)
-  apply (subgoal_tac "floor x <= floor 0")
-  apply simp
-  apply (erule floor_mono)
-done
+  unfolding natfloor_def by simp
+
+lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
+  by simp (* TODO: move to Int.thy *)
 
 lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
-  apply (case_tac "0 <= x")
-  apply (subst natfloor_def)+
-  apply (subst nat_le_eq_zle)
-  apply force
-  apply (erule floor_mono)
-  apply (subst natfloor_neg)
-  apply simp
-  apply simp
-done
+  unfolding natfloor_def by (intro nat_mono floor_mono)
 
 lemma le_natfloor: "real x <= a ==> x <= natfloor a"
   apply (unfold natfloor_def)
   apply (subst nat_int [THEN sym])
-  apply (subst nat_le_eq_zle)
-  apply simp
+  apply (rule nat_mono)
   apply (rule le_floor)
   apply simp
 done
 
+lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n"
+  unfolding natfloor_def real_of_nat_def
+  by (simp add: nat_less_iff floor_less_iff)
+
 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
+  using assms by (simp add: natfloor_less_iff)
 
 lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
   apply (rule iffI)
@@ -402,14 +388,7 @@
 done
 
 lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
-  apply (unfold natfloor_def)
-  apply (subst (2) nat_int [THEN sym])
-  apply (subst eq_nat_nat_iff)
-  apply simp
-  apply simp
-  apply (rule floor_eq2)
-  apply auto
-done
+  unfolding natfloor_def by (simp add: floor_eq2 [where n="int n"])
 
 lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
   apply (case_tac "0 <= x")
@@ -428,110 +407,48 @@
 done
 
 lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
-  apply (unfold natfloor_def)
-  apply (subgoal_tac "real a = real (int a)")
-  apply (erule ssubst)
-  apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq)
-  apply simp
-done
+  unfolding natfloor_def
+  unfolding real_of_int_of_nat_eq [symmetric] floor_add
+  by (simp add: nat_add_distrib)
 
 lemma natfloor_add_number_of [simp]:
     "~neg ((number_of n)::int) ==> 0 <= x ==>
       natfloor (x + number_of n) = natfloor x + number_of n"
-  apply (subst natfloor_add [THEN sym])
-  apply simp_all
-done
+  by (simp add: natfloor_add [symmetric])
 
 lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
-  apply (subst natfloor_add [THEN sym])
-  apply assumption
-  apply simp
-done
+  by (simp add: natfloor_add [symmetric] del: One_nat_def)
 
 lemma natfloor_subtract [simp]: "real a <= x ==>
     natfloor(x - real a) = natfloor x - a"
-  apply (unfold natfloor_def)
-  apply (subgoal_tac "real a = real (int a)")
-  apply (erule ssubst)
-  apply (simp del: real_of_int_of_nat_eq)
-  apply simp
-done
+  unfolding natfloor_def
+  unfolding real_of_int_of_nat_eq [symmetric] floor_subtract
+  by simp
 
 lemma natfloor_div_nat:
   assumes "1 <= x" and "y > 0"
   shows "natfloor (x / real y) = natfloor x div y"
-proof -
-  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)
-  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: assms)
-    apply (rule divide_nonneg_pos)
-    apply (simp add: algebra_simps)
-    apply (rule real_natfloor_le)
-    using assms apply auto
+proof (rule natfloor_eq)
+  have "(natfloor x) div y * y \<le> natfloor x"
+    by (rule add_leD1 [where k="natfloor x mod y"], simp)
+  thus "real (natfloor x div y) \<le> x / real y"
+    using assms by (simp add: le_divide_eq le_natfloor_eq)
+  have "natfloor x < (natfloor x) div y * y + y"
+    apply (subst mod_div_equality [symmetric])
+    apply (rule add_strict_left_mono)
+    apply (rule mod_less_divisor)
+    apply fact
     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: assms)
-    apply (rule divide_nonneg_pos)
-    apply (simp add: algebra_simps)
-    apply (rule real_natfloor_le)
-    apply (auto simp add: assms)
-    using assms apply arith
-    using assms 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
+  thus "x / real y < real (natfloor x div y) + 1"
+    using assms
+    by (simp add: divide_less_eq natfloor_less_iff left_distrib)
 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)
+  using assms
+  by (simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le)
 
 lemma natceiling_zero [simp]: "natceiling 0 = 0"
   by (unfold natceiling_def, simp)
@@ -549,126 +466,57 @@
   by (unfold natceiling_def, simp)
 
 lemma real_natceiling_ge: "x <= real(natceiling x)"
-  apply (unfold natceiling_def)
-  apply (case_tac "x < 0")
-  apply simp
-  apply (subst real_nat_eq_real)
-  apply (subgoal_tac "ceiling 0 <= ceiling x")
-  apply simp
-  apply (rule ceiling_mono)
-  apply simp
-  apply simp
-done
+  unfolding natceiling_def by (cases "x < 0", simp_all)
 
 lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
-  apply (unfold natceiling_def)
-  apply simp
-done
+  unfolding natceiling_def by simp
 
 lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
-  apply (case_tac "0 <= x")
-  apply (subst natceiling_def)+
-  apply (subst nat_le_eq_zle)
-  apply (rule disjI2)
-  apply (subgoal_tac "real (0::int) <= real(ceiling y)")
-  apply simp
-  apply (rule order_trans)
-  apply simp
-  apply (erule order_trans)
-  apply simp
-  apply (erule ceiling_mono)
-  apply (subst natceiling_neg)
-  apply simp_all
-done
+  unfolding natceiling_def by (intro nat_mono ceiling_mono)
+
+lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
+  by auto (* TODO: move to Int.thy *)
 
 lemma natceiling_le: "x <= real a ==> natceiling x <= a"
-  apply (unfold natceiling_def)
-  apply (case_tac "x < 0")
-  apply simp
-  apply (subst (2) nat_int [THEN sym])
-  apply (subst nat_le_eq_zle)
-  apply simp
-  apply (rule ceiling_le)
-  apply simp
-done
+  unfolding natceiling_def real_of_nat_def
+  by (simp add: nat_le_iff ceiling_le_iff)
 
 lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"
-  apply (rule iffI)
-  apply (rule order_trans)
-  apply (rule real_natceiling_ge)
-  apply (subst real_of_nat_le_iff)
-  apply assumption
-  apply (erule natceiling_le)
-done
+  unfolding natceiling_def real_of_nat_def (* FIXME: unused assumption *)
+  by (simp add: nat_le_iff ceiling_le_iff)
 
 lemma natceiling_le_eq_number_of [simp]:
     "~ neg((number_of n)::int) ==> 0 <= x ==>
       (natceiling x <= number_of n) = (x <= number_of n)"
-  apply (subst natceiling_le_eq, assumption)
-  apply simp
-done
+  by (simp add: natceiling_le_eq)
 
 lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
-  apply (case_tac "0 <= x")
-  apply (subst natceiling_le_eq)
-  apply assumption
-  apply simp
-  apply (subst natceiling_neg)
-  apply simp
-  apply simp
-done
+  unfolding natceiling_def
+  by (simp add: nat_le_iff ceiling_le_iff)
 
 lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
-  apply (unfold natceiling_def)
-  apply (simplesubst nat_int [THEN sym]) back back
-  apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)")
-  apply (erule ssubst)
-  apply (subst eq_nat_nat_iff)
-  apply (subgoal_tac "ceiling 0 <= ceiling x")
-  apply simp
-  apply (rule ceiling_mono)
-  apply force
-  apply force
-  apply (rule ceiling_eq2)
-  apply (simp, simp)
-  apply (subst nat_add_distrib)
-  apply auto
-done
+  unfolding natceiling_def
+  by (simp add: ceiling_eq2 [where n="int n"])
 
 lemma natceiling_add [simp]: "0 <= x ==>
     natceiling (x + real a) = natceiling x + a"
-  apply (unfold natceiling_def)
-  apply (subgoal_tac "real a = real (int a)")
-  apply (erule ssubst)
-  apply (simp del: real_of_int_of_nat_eq)
-  apply (subst nat_add_distrib)
-  apply (subgoal_tac "0 = ceiling 0")
-  apply (erule ssubst)
-  apply (erule ceiling_mono)
-  apply simp_all
-done
+  unfolding natceiling_def
+  unfolding real_of_int_of_nat_eq [symmetric] ceiling_add
+  by (simp add: nat_add_distrib)
 
 lemma natceiling_add_number_of [simp]:
     "~ neg ((number_of n)::int) ==> 0 <= x ==>
       natceiling (x + number_of n) = natceiling x + number_of n"
-  apply (subst natceiling_add [THEN sym])
-  apply simp_all
-done
+  by (simp add: natceiling_add [symmetric])
 
 lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
-  apply (subst natceiling_add [THEN sym])
-  apply assumption
-  apply simp
-done
+  by (simp add: natceiling_add [symmetric] del: One_nat_def)
 
 lemma natceiling_subtract [simp]: "real a <= x ==>
     natceiling(x - real a) = natceiling x - a"
-  apply (unfold natceiling_def)
-  apply (subgoal_tac "real a = real (int a)")
-  apply (erule ssubst)
-  apply (simp del: real_of_int_of_nat_eq)
-  apply simp
-done
+  unfolding natceiling_def
+  unfolding real_of_int_of_nat_eq [symmetric] ceiling_subtract
+  by simp
 
 subsection {* Exponentiation with floor *}