Added natfloor and floor rules for multiplication and power.
authorhoelzl
Thu Mar 04 17:28:45 2010 +0100 (2010-03-04)
changeset 35578384ad08a1d1b
parent 35577 43b93e294522
child 35579 cc9a5a0ab5ea
Added natfloor and floor rules for multiplication and power.
src/HOL/RComplete.thy
src/HOL/RealPow.thy
     1.1 --- a/src/HOL/RComplete.thy	Thu Mar 04 17:09:44 2010 +0100
     1.2 +++ b/src/HOL/RComplete.thy	Thu Mar 04 17:28:45 2010 +0100
     1.3 @@ -653,6 +653,18 @@
     1.4  lemma floor_subtract_one: "floor (x - 1) = floor x - 1"
     1.5    by (rule floor_diff_one) (* already declared [simp] *)
     1.6  
     1.7 +lemma le_mult_floor:
     1.8 +  assumes "0 \<le> (a :: real)" and "0 \<le> b"
     1.9 +  shows "floor a * floor b \<le> floor (a * b)"
    1.10 +proof -
    1.11 +  have "real (floor a) \<le> a"
    1.12 +    and "real (floor b) \<le> b" by auto
    1.13 +  hence "real (floor a * floor b) \<le> a * b"
    1.14 +    using assms by (auto intro!: mult_mono)
    1.15 +  also have "a * b < real (floor (a * b) + 1)" by auto
    1.16 +  finally show ?thesis unfolding real_of_int_less_iff by simp
    1.17 +qed
    1.18 +
    1.19  lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
    1.20    unfolding real_of_nat_def by simp
    1.21  
    1.22 @@ -821,6 +833,19 @@
    1.23    apply simp
    1.24  done
    1.25  
    1.26 +lemma less_natfloor:
    1.27 +  assumes "0 \<le> x" and "x < real (n :: nat)"
    1.28 +  shows "natfloor x < n"
    1.29 +proof (rule ccontr)
    1.30 +  assume "\<not> ?thesis" hence *: "n \<le> natfloor x" by simp
    1.31 +  note assms(2)
    1.32 +  also have "real n \<le> real (natfloor x)"
    1.33 +    using * unfolding real_of_nat_le_iff .
    1.34 +  finally have "x < real (natfloor x)" .
    1.35 +  with real_natfloor_le[OF assms(1)]
    1.36 +  show False by auto
    1.37 +qed
    1.38 +
    1.39  lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
    1.40    apply (rule iffI)
    1.41    apply (rule order_trans)
    1.42 @@ -851,7 +876,7 @@
    1.43  
    1.44  lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
    1.45    apply (unfold natfloor_def)
    1.46 -  apply (subst nat_int [THEN sym]);back;
    1.47 +  apply (subst (2) nat_int [THEN sym])
    1.48    apply (subst eq_nat_nat_iff)
    1.49    apply simp
    1.50    apply simp
    1.51 @@ -905,6 +930,83 @@
    1.52    apply simp
    1.53  done
    1.54  
    1.55 +lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
    1.56 +  natfloor (x / real y) = natfloor x div y"
    1.57 +proof -
    1.58 +  assume "1 <= (x::real)" and "(y::nat) > 0"
    1.59 +  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
    1.60 +    by simp
    1.61 +  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
    1.62 +    real((natfloor x) mod y)"
    1.63 +    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
    1.64 +  have "x = real(natfloor x) + (x - real(natfloor x))"
    1.65 +    by simp
    1.66 +  then have "x = real ((natfloor x) div y) * real y +
    1.67 +      real((natfloor x) mod y) + (x - real(natfloor x))"
    1.68 +    by (simp add: a)
    1.69 +  then have "x / real y = ... / real y"
    1.70 +    by simp
    1.71 +  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
    1.72 +    real y + (x - real(natfloor x)) / real y"
    1.73 +    by (auto simp add: algebra_simps add_divide_distrib
    1.74 +      diff_divide_distrib prems)
    1.75 +  finally have "natfloor (x / real y) = natfloor(...)" by simp
    1.76 +  also have "... = natfloor(real((natfloor x) mod y) /
    1.77 +    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
    1.78 +    by (simp add: add_ac)
    1.79 +  also have "... = natfloor(real((natfloor x) mod y) /
    1.80 +    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
    1.81 +    apply (rule natfloor_add)
    1.82 +    apply (rule add_nonneg_nonneg)
    1.83 +    apply (rule divide_nonneg_pos)
    1.84 +    apply simp
    1.85 +    apply (simp add: prems)
    1.86 +    apply (rule divide_nonneg_pos)
    1.87 +    apply (simp add: algebra_simps)
    1.88 +    apply (rule real_natfloor_le)
    1.89 +    apply (insert prems, auto)
    1.90 +    done
    1.91 +  also have "natfloor(real((natfloor x) mod y) /
    1.92 +    real y + (x - real(natfloor x)) / real y) = 0"
    1.93 +    apply (rule natfloor_eq)
    1.94 +    apply simp
    1.95 +    apply (rule add_nonneg_nonneg)
    1.96 +    apply (rule divide_nonneg_pos)
    1.97 +    apply force
    1.98 +    apply (force simp add: prems)
    1.99 +    apply (rule divide_nonneg_pos)
   1.100 +    apply (simp add: algebra_simps)
   1.101 +    apply (rule real_natfloor_le)
   1.102 +    apply (auto simp add: prems)
   1.103 +    apply (insert prems, arith)
   1.104 +    apply (simp add: add_divide_distrib [THEN sym])
   1.105 +    apply (subgoal_tac "real y = real y - 1 + 1")
   1.106 +    apply (erule ssubst)
   1.107 +    apply (rule add_le_less_mono)
   1.108 +    apply (simp add: algebra_simps)
   1.109 +    apply (subgoal_tac "1 + real(natfloor x mod y) =
   1.110 +      real(natfloor x mod y + 1)")
   1.111 +    apply (erule ssubst)
   1.112 +    apply (subst real_of_nat_le_iff)
   1.113 +    apply (subgoal_tac "natfloor x mod y < y")
   1.114 +    apply arith
   1.115 +    apply (rule mod_less_divisor)
   1.116 +    apply auto
   1.117 +    using real_natfloor_add_one_gt
   1.118 +    apply (simp add: algebra_simps)
   1.119 +    done
   1.120 +  finally show ?thesis by simp
   1.121 +qed
   1.122 +
   1.123 +lemma le_mult_natfloor:
   1.124 +  assumes "0 \<le> (a :: real)" and "0 \<le> b"
   1.125 +  shows "natfloor a * natfloor b \<le> natfloor (a * b)"
   1.126 +  unfolding natfloor_def
   1.127 +  apply (subst nat_mult_distrib[symmetric])
   1.128 +  using assms apply simp
   1.129 +  apply (subst nat_le_eq_zle)
   1.130 +  using assms le_mult_floor by (auto intro!: mult_nonneg_nonneg)
   1.131 +
   1.132  lemma natceiling_zero [simp]: "natceiling 0 = 0"
   1.133    by (unfold natceiling_def, simp)
   1.134  
   1.135 @@ -957,7 +1059,7 @@
   1.136    apply (unfold natceiling_def)
   1.137    apply (case_tac "x < 0")
   1.138    apply simp
   1.139 -  apply (subst nat_int [THEN sym]);back;
   1.140 +  apply (subst (2) nat_int [THEN sym])
   1.141    apply (subst nat_le_eq_zle)
   1.142    apply simp
   1.143    apply (rule ceiling_le)
   1.144 @@ -1042,72 +1144,5 @@
   1.145    apply simp
   1.146  done
   1.147  
   1.148 -lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
   1.149 -  natfloor (x / real y) = natfloor x div y"
   1.150 -proof -
   1.151 -  assume "1 <= (x::real)" and "(y::nat) > 0"
   1.152 -  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
   1.153 -    by simp
   1.154 -  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
   1.155 -    real((natfloor x) mod y)"
   1.156 -    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
   1.157 -  have "x = real(natfloor x) + (x - real(natfloor x))"
   1.158 -    by simp
   1.159 -  then have "x = real ((natfloor x) div y) * real y +
   1.160 -      real((natfloor x) mod y) + (x - real(natfloor x))"
   1.161 -    by (simp add: a)
   1.162 -  then have "x / real y = ... / real y"
   1.163 -    by simp
   1.164 -  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
   1.165 -    real y + (x - real(natfloor x)) / real y"
   1.166 -    by (auto simp add: algebra_simps add_divide_distrib
   1.167 -      diff_divide_distrib prems)
   1.168 -  finally have "natfloor (x / real y) = natfloor(...)" by simp
   1.169 -  also have "... = natfloor(real((natfloor x) mod y) /
   1.170 -    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
   1.171 -    by (simp add: add_ac)
   1.172 -  also have "... = natfloor(real((natfloor x) mod y) /
   1.173 -    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
   1.174 -    apply (rule natfloor_add)
   1.175 -    apply (rule add_nonneg_nonneg)
   1.176 -    apply (rule divide_nonneg_pos)
   1.177 -    apply simp
   1.178 -    apply (simp add: prems)
   1.179 -    apply (rule divide_nonneg_pos)
   1.180 -    apply (simp add: algebra_simps)
   1.181 -    apply (rule real_natfloor_le)
   1.182 -    apply (insert prems, auto)
   1.183 -    done
   1.184 -  also have "natfloor(real((natfloor x) mod y) /
   1.185 -    real y + (x - real(natfloor x)) / real y) = 0"
   1.186 -    apply (rule natfloor_eq)
   1.187 -    apply simp
   1.188 -    apply (rule add_nonneg_nonneg)
   1.189 -    apply (rule divide_nonneg_pos)
   1.190 -    apply force
   1.191 -    apply (force simp add: prems)
   1.192 -    apply (rule divide_nonneg_pos)
   1.193 -    apply (simp add: algebra_simps)
   1.194 -    apply (rule real_natfloor_le)
   1.195 -    apply (auto simp add: prems)
   1.196 -    apply (insert prems, arith)
   1.197 -    apply (simp add: add_divide_distrib [THEN sym])
   1.198 -    apply (subgoal_tac "real y = real y - 1 + 1")
   1.199 -    apply (erule ssubst)
   1.200 -    apply (rule add_le_less_mono)
   1.201 -    apply (simp add: algebra_simps)
   1.202 -    apply (subgoal_tac "1 + real(natfloor x mod y) =
   1.203 -      real(natfloor x mod y + 1)")
   1.204 -    apply (erule ssubst)
   1.205 -    apply (subst real_of_nat_le_iff)
   1.206 -    apply (subgoal_tac "natfloor x mod y < y")
   1.207 -    apply arith
   1.208 -    apply (rule mod_less_divisor)
   1.209 -    apply auto
   1.210 -    using real_natfloor_add_one_gt
   1.211 -    apply (simp add: algebra_simps)
   1.212 -    done
   1.213 -  finally show ?thesis by simp
   1.214 -qed
   1.215  
   1.216  end
     2.1 --- a/src/HOL/RealPow.thy	Thu Mar 04 17:09:44 2010 +0100
     2.2 +++ b/src/HOL/RealPow.thy	Thu Mar 04 17:28:45 2010 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* Natural powers theory *}
     2.5  
     2.6  theory RealPow
     2.7 -imports RealDef
     2.8 +imports RealDef RComplete
     2.9  begin
    2.10  
    2.11  (* FIXME: declare this in Rings.thy or not at all *)
    2.12 @@ -107,6 +107,28 @@
    2.13      by (rule power_le_imp_le_base)
    2.14  qed
    2.15  
    2.16 +subsection {*Floor*}
    2.17 +
    2.18 +lemma floor_power:
    2.19 +  assumes "x = real (floor x)"
    2.20 +  shows "floor (x ^ n) = floor x ^ n"
    2.21 +proof -
    2.22 +  have *: "x ^ n = real (floor x ^ n)"
    2.23 +    using assms by (induct n arbitrary: x) simp_all
    2.24 +  show ?thesis unfolding real_of_int_inject[symmetric]
    2.25 +    unfolding * floor_real_of_int ..
    2.26 +qed
    2.27 +
    2.28 +lemma natfloor_power:
    2.29 +  assumes "x = real (natfloor x)"
    2.30 +  shows "natfloor (x ^ n) = natfloor x ^ n"
    2.31 +proof -
    2.32 +  from assms have "0 \<le> floor x" by auto
    2.33 +  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
    2.34 +  from floor_power[OF this]
    2.35 +  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
    2.36 +    by simp
    2.37 +qed
    2.38  
    2.39  subsection {*Various Other Theorems*}
    2.40  
    2.41 @@ -131,4 +153,5 @@
    2.42  lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
    2.43  by (case_tac "n", auto)
    2.44  
    2.45 +
    2.46  end