author hoelzl Thu Mar 04 17:28:45 2010 +0100 (2010-03-04) changeset 35578 384ad08a1d1b parent 35577 43b93e294522 child 35579 cc9a5a0ab5ea
Added natfloor and floor rules for multiplication and power.
 src/HOL/RComplete.thy file | annotate | diff | revisions src/HOL/RealPow.thy file | annotate | diff | revisions
```     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.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.79 +  also have "... = natfloor(real((natfloor x) mod y) /
1.80 +    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
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.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.105 +    apply (subgoal_tac "real y = real y - 1 + 1")
1.106 +    apply (erule ssubst)
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.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.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.172 -  also have "... = natfloor(real((natfloor x) mod y) /
1.173 -    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
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.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.198 -    apply (subgoal_tac "real y = real y - 1 + 1")
1.199 -    apply (erule ssubst)
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.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
```