# HG changeset patch
# User avigad
# Date 1121276947 -7200
# Node ID 00d8f9300d13d6418f5c9e6f1e0a479d3dc5bd33
# Parent  2b82259cc7b2fe9e3d08ef63a6f10c32d251fb73
Additions to the Real (and Hyperreal) libraries:
RealDef.thy: lemmas relating nats, ints, and reals
  reversed direction of real_of_int_mult, etc. (now they agree with nat versions)
SEQ.thy and Series.thy: various additions
RComplete.thy: lemmas involving floor and ceiling
  introduced natfloor and natceiling
Log.thy: various additions

diff -r 2b82259cc7b2 -r 00d8f9300d13 src/HOL/Hyperreal/Log.thy
--- a/src/HOL/Hyperreal/Log.thy	Wed Jul 13 16:47:23 2005 +0200
+++ b/src/HOL/Hyperreal/Log.thy	Wed Jul 13 19:49:07 2005 +0200
@@ -1,5 +1,6 @@
 (*  Title       : Log.thy
     Author      : Jacques D. Fleuriot
+                  Additional contributions by Jeremy Avigad
     Copyright   : 2000,2001 University of Edinburgh
 *)
 
@@ -38,6 +39,9 @@
 lemma powr_gt_zero [simp]: "0 < x powr a"
 by (simp add: powr_def)
 
+lemma powr_ge_pzero [simp]: "0 <= x powr y"
+by (rule order_less_imp_le, rule powr_gt_zero)
+
 lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
 by (simp add: powr_def)
 
@@ -47,6 +51,12 @@
 apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
 done
 
+lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
+  apply (simp add: powr_def)
+  apply (subst exp_diff [THEN sym])
+  apply (simp add: left_diff_distrib)
+done
+
 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
 by (simp add: powr_def exp_add [symmetric] left_distrib)
 
@@ -129,8 +139,6 @@
 by (simp add: linorder_not_less [symmetric])
 
 
-subsection{*Further Results Courtesy Jeremy Avigad*}
-
 lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
   apply (induct n, simp)
   apply (subgoal_tac "real(Suc n) = real n + 1")
@@ -176,13 +184,95 @@
   apply assumption+
 done
 
-lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a";
+lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a <
+    x powr a"
+  apply (unfold powr_def)
+  apply (rule exp_less_mono)
+  apply (rule mult_strict_left_mono_neg)
+  apply (subst ln_less_cancel_iff)
+  apply assumption
+  apply (rule order_less_trans)
+  prefer 2
+  apply assumption+
+done
+
+lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
   apply (case_tac "a = 0", simp)
   apply (case_tac "x = y", simp)
   apply (rule order_less_imp_le)
   apply (rule powr_less_mono2, auto)
 done
 
+lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
+  apply (rule mult_imp_le_div_pos)
+  apply (assumption)
+  apply (subst mult_commute)
+  apply (subst ln_pwr [THEN sym])
+  apply auto
+  apply (rule ln_bound)
+  apply (erule ge_one_powr_ge_zero)
+  apply (erule order_less_imp_le)
+done
+
+lemma ln_powr_bound2: "1 < x ==> 0 < a ==> (ln x) powr a <= (a powr a) * x"
+proof -
+  assume "1 < x" and "0 < a"
+  then have "ln x <= (x powr (1 / a)) / (1 / a)"
+    apply (intro ln_powr_bound)
+    apply (erule order_less_imp_le)
+    apply (rule divide_pos_pos)
+    apply simp_all
+    done
+  also have "... = a * (x powr (1 / a))"
+    by simp
+  finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
+    apply (intro powr_mono2)
+    apply (rule order_less_imp_le, rule prems)
+    apply (rule ln_gt_zero)
+    apply (rule prems)
+    apply assumption
+    done
+  also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
+    apply (rule powr_mult)
+    apply (rule prems)
+    apply (rule powr_gt_zero)
+    done
+  also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
+    by (rule powr_powr)
+  also have "... = x"
+    apply simp
+    apply (subgoal_tac "a ~= 0")
+    apply (insert prems, auto)
+    done
+  finally show ?thesis .
+qed
+
+lemma LIMSEQ_neg_powr: "0 < s ==> (%x. (real x) powr - s) ----> 0"
+  apply (unfold LIMSEQ_def)
+  apply clarsimp
+  apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI)
+  apply clarify
+  proof -
+    fix r fix n
+    assume "0 < s" and "0 < r" and "natfloor (r powr (1 / - s)) + 1 <= n"
+    have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1"
+      by (rule real_natfloor_add_one_gt)
+    also have "... = real(natfloor(r powr (1 / -s)) + 1)"
+      by simp
+    also have "... <= real n"
+      apply (subst real_of_nat_le_iff)
+      apply (rule prems)
+      done
+    finally have "r powr (1 / - s) < real n".
+    then have "real n powr (- s) < (r powr (1 / - s)) powr - s" 
+      apply (intro powr_less_mono2_neg)
+      apply (auto simp add: prems)
+      done
+    also have "... = r"
+      by (simp add: powr_powr prems less_imp_neq [THEN not_sym])
+    finally show "real n powr - s < r" .
+  qed
+
 
 
 ML
diff -r 2b82259cc7b2 -r 00d8f9300d13 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 13 16:47:23 2005 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 13 19:49:07 2005 +0200
@@ -10,33 +10,6 @@
 imports Log
 begin
 
-(* FIXME generalize? *)
-lemma sumr_offset:
- "(\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
-by (induct "n", auto)
-
-lemma sumr_offset2:
- "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
-by (induct "n", auto)
-
-lemma sumr_offset3:
-  "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
-by (simp  add: sumr_offset)
-
-lemma sumr_offset4:
- "\<forall>n f. setsum f {0::nat..<n+k} =
-        (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
-by (simp add: sumr_offset)
-
-(*
-lemma sumr_from_1_from_0: "0 < n ==>
-      (\<Sum>n=Suc 0 ..< Suc n. if even(n) then 0 else
-             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n =
-      (\<Sum>n=0..<Suc n. if even(n) then 0 else
-             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n"
-by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto)
-*)
-
 subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
 
 text{*This is a very long, messy proof even now that it's been broken down
diff -r 2b82259cc7b2 -r 00d8f9300d13 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Wed Jul 13 16:47:23 2005 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Wed Jul 13 19:49:07 2005 +0200
@@ -3,6 +3,7 @@
     Copyright   : 1998  University of Cambridge
     Description : Convergence of sequences and series
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
+    Additional contributions by Jeremy Avigad
 *)
 
 theory SEQ
@@ -204,6 +205,15 @@
 lemma LIMSEQ_add: "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add)
 
+lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b"
+  apply (subgoal_tac "%n. (f n + b) == %n. (f n + (%n. b) n)")
+  apply (subgoal_tac "(%n. b) ----> b")
+  apply (auto simp add: LIMSEQ_add LIMSEQ_const)
+done
+
+lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b"
+by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_add_const)
+
 lemma NSLIMSEQ_mult:
       "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
 by (auto intro!: approx_mult_HFinite 
@@ -243,6 +253,15 @@
 apply (blast intro: NSLIMSEQ_add_minus)
 done
 
+lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n  - b)) ----> a - b"
+  apply (subgoal_tac "%n. (f n - b) == %n. (f n - (%n. b) n)")
+  apply (subgoal_tac "(%n. b) ----> b")
+  apply (auto simp add: LIMSEQ_diff LIMSEQ_const)
+done
+
+lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
+by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_diff_const)
+
 text{*Proof is like that of @{text NSLIM_inverse}.*}
 lemma NSLIMSEQ_inverse:
      "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
@@ -294,6 +313,66 @@
     by (simp add: setsum_def LIMSEQ_const)
 qed
 
+lemma LIMSEQ_setprod:
+  assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
+  shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)"
+proof (cases "finite S")
+  case True
+  thus ?thesis using n
+  proof (induct)
+    case empty
+    show ?case
+      by (simp add: LIMSEQ_const)
+  next
+    case insert
+    thus ?case
+      by (simp add: LIMSEQ_mult)
+  qed
+next
+  case False
+  thus ?thesis
+    by (simp add: setprod_def LIMSEQ_const)
+qed
+
+lemma LIMSEQ_ignore_initial_segment: "f ----> a 
+  ==> (%n. f(n + k)) ----> a"
+  apply (unfold LIMSEQ_def) 
+  apply (clarify)
+  apply (drule_tac x = r in spec)
+  apply (clarify)
+  apply (rule_tac x = "no + k" in exI)
+  by auto
+
+lemma LIMSEQ_offset: "(%x. f (x + k)) ----> a ==>
+    f ----> a"
+  apply (unfold LIMSEQ_def)
+  apply clarsimp
+  apply (drule_tac x = r in spec)
+  apply clarsimp
+  apply (rule_tac x = "no + k" in exI)
+  apply clarsimp
+  apply (drule_tac x = "n - k" in spec)
+  apply (frule mp)
+  apply arith
+  apply simp
+done
+
+lemma LIMSEQ_diff_approach_zero: 
+  "g ----> L ==> (%x. f x - g x) ----> 0  ==>
+     f ----> L"
+  apply (drule LIMSEQ_add)
+  apply assumption
+  apply simp
+done
+
+lemma LIMSEQ_diff_approach_zero2: 
+  "f ----> L ==> (%x. f x - g x) ----> 0  ==>
+     g ----> L";
+  apply (drule LIMSEQ_diff)
+  apply assumption
+  apply simp
+done
+
 
 subsection{*Nslim and Lim*}
 
diff -r 2b82259cc7b2 -r 00d8f9300d13 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Wed Jul 13 16:47:23 2005 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Wed Jul 13 19:49:07 2005 +0200
@@ -4,6 +4,7 @@
 
 Converted to Isar and polished by lcp
 Converted to setsum and polished yet more by TNN
+Additional contributions by Jeremy Avigad
 *) 
 
 header{*Finite Summation and Infinite Series*}
@@ -60,6 +61,32 @@
 apply (simp_all add: setsum_add_nat_ivl add_commute)
 done
 
+(* FIXME generalize? *)
+lemma sumr_offset:
+ "(\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
+by (induct "n", auto)
+
+lemma sumr_offset2:
+ "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
+by (induct "n", auto)
+
+lemma sumr_offset3:
+  "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
+by (simp  add: sumr_offset)
+
+lemma sumr_offset4:
+ "\<forall>n f. setsum f {0::nat..<n+k} =
+        (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
+by (simp add: sumr_offset)
+
+(*
+lemma sumr_from_1_from_0: "0 < n ==>
+      (\<Sum>n=Suc 0 ..< Suc n. if even(n) then 0 else
+             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n =
+      (\<Sum>n=0..<Suc n. if even(n) then 0 else
+             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n"
+by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto)
+*)
 
 subsection{* Infinite Sums, by the Properties of Limits*}
 
@@ -88,6 +115,34 @@
 apply (auto intro!: LIMSEQ_unique simp add: sums_def)
 done
 
+lemma sums_split_initial_segment: "f sums s ==> 
+  (%n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
+  apply (unfold sums_def);
+  apply (simp add: sumr_offset); 
+  apply (rule LIMSEQ_diff_const)
+  apply (rule LIMSEQ_ignore_initial_segment)
+  apply assumption
+done
+
+lemma summable_ignore_initial_segment: "summable f ==> 
+    summable (%n. f(n + k))"
+  apply (unfold summable_def)
+  apply (auto intro: sums_split_initial_segment)
+done
+
+lemma suminf_minus_initial_segment: "summable f ==>
+    suminf f = s ==> suminf (%n. f(n + k)) = s - (SUM i = 0..< k. f i)"
+  apply (frule summable_ignore_initial_segment)
+  apply (rule sums_unique [THEN sym])
+  apply (frule summable_sums)
+  apply (rule sums_split_initial_segment)
+  apply auto
+done
+
+lemma suminf_split_initial_segment: "summable f ==> 
+    suminf f = (SUM i = 0..< k. f i) + suminf (%n. f(n + k))"
+by (auto simp add: suminf_minus_initial_segment)
+
 lemma series_zero: 
      "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
 apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
@@ -95,30 +150,112 @@
 apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong)
 done
 
+lemma sums_zero: "(%n. 0) sums 0";
+  apply (unfold sums_def);
+  apply simp;
+  apply (rule LIMSEQ_const);
+done;
 
-lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"
+lemma summable_zero: "summable (%n. 0)";
+  apply (rule sums_summable);
+  apply (rule sums_zero);
+done;
+
+lemma suminf_zero: "suminf (%n. 0) = 0";
+  apply (rule sym);
+  apply (rule sums_unique);
+  apply (rule sums_zero);
+done;
+  
+lemma sums_mult: "f sums a ==> (%n. c * f n) sums (c * a)"
 by (auto simp add: sums_def setsum_mult [symmetric]
          intro!: LIMSEQ_mult intro: LIMSEQ_const)
 
-lemma sums_divide: "x sums x' ==> (%n. x(n)/c) sums (x'/c)"
+lemma summable_mult: "summable f ==> summable (%n. c * f n)";
+  apply (unfold summable_def);
+  apply (auto intro: sums_mult);
+done;
+
+lemma suminf_mult: "summable f ==> suminf (%n. c * f n) = c * suminf f";
+  apply (rule sym);
+  apply (rule sums_unique);
+  apply (rule sums_mult);
+  apply (erule summable_sums);
+done;
+
+lemma sums_mult2: "f sums a ==> (%n. f n * c) sums (a * c)"
+apply (subst mult_commute)
+apply (subst mult_commute);back;
+apply (erule sums_mult)
+done
+
+lemma summable_mult2: "summable f ==> summable (%n. f n * c)"
+  apply (unfold summable_def)
+  apply (auto intro: sums_mult2)
+done
+
+lemma suminf_mult2: "summable f ==> suminf f * c = (\<Sum>n. f n * c)"
+by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute)
+
+lemma sums_divide: "f sums a ==> (%n. (f n)/c) sums (a/c)"
 by (simp add: real_divide_def sums_mult mult_commute [of _ "inverse c"])
 
+lemma summable_divide: "summable f ==> summable (%n. (f n) / c)";
+  apply (unfold summable_def);
+  apply (auto intro: sums_divide);
+done;
+
+lemma suminf_divide: "summable f ==> suminf (%n. (f n) / c) = (suminf f) / c";
+  apply (rule sym);
+  apply (rule sums_unique);
+  apply (rule sums_divide);
+  apply (erule summable_sums);
+done;
+
+lemma sums_add: "[| x sums x0; y sums y0 |] ==> (%n. x n + y n) sums (x0+y0)"
+by (auto simp add: sums_def setsum_addf intro: LIMSEQ_add)
+
+lemma summable_add: "summable f ==> summable g ==> summable (%x. f x + g x)";
+  apply (unfold summable_def);
+  apply clarify;
+  apply (rule exI);
+  apply (erule sums_add);
+  apply assumption;
+done;
+
+lemma suminf_add:
+     "[| summable f; summable g |]   
+      ==> suminf f + suminf g  = (\<Sum>n. f n + g n)"
+by (auto intro!: sums_add sums_unique summable_sums)
+
 lemma sums_diff: "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)"
 by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff)
 
-lemma suminf_mult: "summable f ==> suminf f * c = (\<Sum>n. f n * c)"
-by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute)
-
-lemma suminf_mult2: "summable f ==> c * suminf f  = (\<Sum>n. c * f n)"
-by (auto intro!: sums_unique sums_mult summable_sums)
+lemma summable_diff: "summable f ==> summable g ==> summable (%x. f x - g x)";
+  apply (unfold summable_def);
+  apply clarify;
+  apply (rule exI);
+  apply (erule sums_diff);
+  apply assumption;
+done;
 
 lemma suminf_diff:
      "[| summable f; summable g |]   
       ==> suminf f - suminf g  = (\<Sum>n. f n - g n)"
 by (auto intro!: sums_diff sums_unique summable_sums)
 
-lemma sums_minus: "x sums x0 ==> (%n. - x n) sums - x0"
-by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf)
+lemma sums_minus: "f sums s ==> (%x. - f x) sums (- s)";
+  by (simp add: sums_def setsum_negf LIMSEQ_minus);
+
+lemma summable_minus: "summable f ==> summable (%x. - f x)";
+  by (auto simp add: summable_def intro: sums_minus);
+
+lemma suminf_minus: "summable f ==> suminf (%x. - f x) = - (suminf f)";
+  apply (rule sym);
+  apply (rule sums_unique);
+  apply (rule sums_minus);
+  apply (erule summable_sums);
+done;
 
 lemma sums_group:
      "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
diff -r 2b82259cc7b2 -r 00d8f9300d13 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jul 13 16:47:23 2005 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Jul 13 19:49:07 2005 +0200
@@ -568,7 +568,7 @@
  apply (rule_tac [2] g = "%n. f n * \<bar>h\<bar>" in summable_comparison_test)
   apply (rule_tac [2] x = 0 in exI, auto)
 apply (rule_tac j = "\<Sum>n. \<bar>g h n\<bar>" in real_le_trans)
-apply (auto intro: summable_rabs summable_le simp add: sums_summable [THEN suminf_mult])
+apply (auto intro: summable_rabs summable_le simp add: sums_summable [THEN suminf_mult2])
 done
 
 
@@ -637,7 +637,6 @@
 apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
 done
 
-
 lemma termdiffs: 
     "[| summable(%n. c(n) * (K ^ n));  
         summable(%n. (diffs c)(n) * (K ^ n));  
@@ -657,7 +656,7 @@
 apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)
 apply (auto simp add: add_commute)
 apply (drule_tac x="(\<lambda>n. c n * (xa + x) ^ n)" in sums_diff, assumption) 
-apply (drule_tac x = "(%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
+apply (drule_tac f = "(%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
 apply (rule sums_unique)
 apply (simp add: diff_def divide_inverse add_ac mult_ac)
 apply (rule LIM_zero_cancel)
@@ -680,17 +679,13 @@
 apply (frule_tac x = "(%n. c n * (xa + x) ^ n) " and y = "(%n. c n * x ^ n)" in sums_diff, assumption)
 apply (simp add: suminf_diff [OF sums_summable sums_summable] 
                right_diff_distrib [symmetric])
-apply (frule_tac x = "(%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult)
-apply (simp add: sums_summable [THEN suminf_mult2])
-apply (frule_tac x = "(%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = "(%n. real n * c n * x ^ (n - Suc 0))" in sums_diff)
-apply assumption
-apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac)
-apply (rule_tac f = suminf in arg_cong)
-apply (rule ext)
-apply (simp add: diff_def right_distrib add_ac mult_ac)
+apply (subst suminf_diff)
+apply (rule summable_mult2)
+apply (erule sums_summable)
+apply (erule sums_summable)
+apply (simp add: ring_eq_simps)
 done
 
-
 subsection{*Formal Derivatives of Exp, Sin, and Cos Series*} 
 
 lemma exp_fdiffs: 
diff -r 2b82259cc7b2 -r 00d8f9300d13 src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Wed Jul 13 16:47:23 2005 +0200
+++ b/src/HOL/Real/RComplete.thy	Wed Jul 13 19:49:07 2005 +0200
@@ -1,9 +1,10 @@
 (*  Title       : RComplete.thy
     ID          : $Id$
     Author      : Jacques D. Fleuriot
+                  Converted to Isar and polished by lcp
+                  Most floor and ceiling lemmas by Jeremy Avigad
     Copyright   : 1998  University of Cambridge
     Copyright   : 2001,2002  University of Edinburgh
-Converted to Isar and polished by lcp
 *) 
 
 header{*Completeness of the Reals; Floor and Ceiling Functions*}
@@ -204,6 +205,37 @@
 apply (auto simp add: mult_assoc real_of_nat_def)
 done
 
+lemma reals_Archimedean6:
+     "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
+apply (insert reals_Archimedean2 [of r], safe)
+apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x"
+       in ex_has_least_nat, auto)
+apply (rule_tac x = x in exI)
+apply (case_tac x, simp)
+apply (rename_tac x')
+apply (drule_tac x = x' in spec, simp)
+done
+
+lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
+by (drule reals_Archimedean6, auto)
+
+lemma reals_Archimedean_6b_int:
+     "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
+apply (drule reals_Archimedean6a, auto)
+apply (rule_tac x = "int n" in exI)
+apply (simp add: real_of_int_real_of_nat real_of_nat_Suc)
+done
+
+lemma reals_Archimedean_6c_int:
+     "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
+apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto)
+apply (rename_tac n)
+apply (drule real_le_imp_less_or_eq, auto)
+apply (rule_tac x = "- n - 1" in exI)
+apply (rule_tac [2] x = "- n" in exI, auto)
+done
+
+
 ML
 {*
 val real_sum_of_halves = thm "real_sum_of_halves";
@@ -260,8 +292,9 @@
 by (simp add: linorder_not_less [symmetric])
 
 lemma floor_zero [simp]: "floor 0 = 0"
-apply (simp add: floor_def)
-apply (rule Least_equality, auto)
+apply (simp add: floor_def del: real_of_int_add)
+apply (rule Least_equality)
+apply simp_all
 done
 
 lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
@@ -279,7 +312,7 @@
 apply (simp only: floor_def)
 apply (rule Least_equality)
 apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
-apply (drule_tac [2] real_of_int_minus [THEN subst])
+apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
 apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
 apply (simp_all add: real_of_int_real_of_nat)
 done
@@ -294,41 +327,11 @@
 lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
 apply (simp only: floor_def)
 apply (rule Least_equality)
-apply (drule_tac [2] real_of_int_minus [THEN subst])
+apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
 apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
 apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
 done
 
-lemma reals_Archimedean6:
-     "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
-apply (insert reals_Archimedean2 [of r], safe)
-apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x"
-       in ex_has_least_nat, auto)
-apply (rule_tac x = x in exI)
-apply (case_tac x, simp)
-apply (rename_tac x')
-apply (drule_tac x = x' in spec, simp)
-done
-
-lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
-by (drule reals_Archimedean6, auto)
-
-lemma reals_Archimedean_6b_int:
-     "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
-apply (drule reals_Archimedean6a, auto)
-apply (rule_tac x = "int n" in exI)
-apply (simp add: real_of_int_real_of_nat real_of_nat_Suc)
-done
-
-lemma reals_Archimedean_6c_int:
-     "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
-apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto)
-apply (rename_tac n)
-apply (drule real_le_imp_less_or_eq, auto)
-apply (rule_tac x = "- n - 1" in exI)
-apply (rule_tac [2] x = "- n" in exI, auto)
-done
-
 lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
 apply (case_tac "r < 0")
 apply (blast intro: reals_Archimedean_6c_int)
@@ -349,19 +352,29 @@
 lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
 apply (simp add: floor_def Least_def)
 apply (insert real_lb_ub_int [of r], safe)
-apply (rule theI2, auto)
+apply (rule theI2)
+apply auto
+apply (subst int_le_real_less, simp)
+apply (drule_tac x = n in spec)
+apply auto
+apply (subgoal_tac "n <= x")
+apply simp
+apply (subst int_le_real_less, simp)
 done
 
-lemma floor_le: "x < y ==> floor x \<le> floor y"
+lemma floor_mono: "x < y ==> floor x \<le> floor y"
 apply (simp add: floor_def Least_def)
 apply (insert real_lb_ub_int [of x])
 apply (insert real_lb_ub_int [of y], safe)
 apply (rule theI2)
-apply (rule_tac [3] theI2, auto)
+apply (rule_tac [3] theI2)
+apply simp
+apply (erule conjI)
+apply (auto simp add: order_eq_iff int_le_real_less)
 done
 
-lemma floor_le2: "x \<le> y ==> floor x \<le> floor y"
-by (auto dest: real_le_imp_less_or_eq simp add: floor_le)
+lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y"
+by (auto dest: real_le_imp_less_or_eq simp add: floor_mono)
 
 lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
 by (auto intro: lemma_floor)
@@ -371,7 +384,8 @@
 apply (simp add: floor_def Least_def)
 apply (insert real_lb_ub_int [of x], erule exE)
 apply (rule theI2)
-apply (auto intro: lemma_floor)
+apply (auto intro: lemma_floor) 
+apply (auto simp add: order_eq_iff int_le_real_less)
 done
 
 lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
@@ -403,11 +417,27 @@
 apply (rule floor_real_of_int)
 done
 
+lemma floor_one [simp]: "floor 1 = 1"
+  apply (rule trans)
+  prefer 2
+  apply (rule floor_real_of_int)
+  apply simp
+done
+
 lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
 apply (simp add: floor_def Least_def)
 apply (insert real_lb_ub_int [of r], safe)
 apply (rule theI2)
 apply (auto intro: lemma_floor)
+apply (auto simp add: order_eq_iff int_le_real_less)
+done
+
+lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
+apply (simp add: floor_def Least_def)
+apply (insert real_lb_ub_int [of r], safe)
+apply (rule theI2)
+apply (auto intro: lemma_floor)
+apply (auto simp add: order_eq_iff int_le_real_less)
 done
 
 lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
@@ -415,8 +445,141 @@
 apply (auto simp del: real_of_int_floor_ge_diff_one)
 done
 
+lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
+apply (insert real_of_int_floor_gt_diff_one [of r])
+apply (auto simp del: real_of_int_floor_gt_diff_one)
+done
 
-subsection{*Ceiling Function for Positive Reals*}
+lemma le_floor: "real a <= x ==> a <= floor x"
+  apply (subgoal_tac "a < floor x + 1")
+  apply arith
+  apply (subst real_of_int_less_iff [THEN sym])
+  apply simp
+  apply (insert real_of_int_floor_add_one_gt [of x]) 
+  apply arith
+done
+
+lemma real_le_floor: "a <= floor x ==> real a <= x"
+  apply (rule order_trans)
+  prefer 2
+  apply (rule real_of_int_floor_le)
+  apply (subst real_of_int_le_iff)
+  apply assumption
+done
+
+lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
+  apply (rule iffI)
+  apply (erule real_le_floor)
+  apply (erule le_floor)
+done
+
+lemma le_floor_eq_number_of [simp]: 
+    "(number_of n <= floor x) = (number_of n <= x)"
+by (simp add: le_floor_eq)
+
+lemma le_floor_eq_zero [simp]: "(0 <= floor x) = (0 <= x)"
+by (simp add: le_floor_eq)
+
+lemma le_floor_eq_one [simp]: "(1 <= floor x) = (1 <= x)"
+by (simp add: le_floor_eq)
+
+lemma floor_less_eq: "(floor x < a) = (x < real a)"
+  apply (subst linorder_not_le [THEN sym])+
+  apply simp
+  apply (rule le_floor_eq)
+done
+
+lemma floor_less_eq_number_of [simp]: 
+    "(floor x < number_of n) = (x < number_of n)"
+by (simp add: floor_less_eq)
+
+lemma floor_less_eq_zero [simp]: "(floor x < 0) = (x < 0)"
+by (simp add: floor_less_eq)
+
+lemma floor_less_eq_one [simp]: "(floor x < 1) = (x < 1)"
+by (simp add: floor_less_eq)
+
+lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
+  apply (insert le_floor_eq [of "a + 1" x])
+  apply auto
+done
+
+lemma less_floor_eq_number_of [simp]: 
+    "(number_of n < floor x) = (number_of n + 1 <= x)"
+by (simp add: less_floor_eq)
+
+lemma less_floor_eq_zero [simp]: "(0 < floor x) = (1 <= x)"
+by (simp add: less_floor_eq)
+
+lemma less_floor_eq_one [simp]: "(1 < floor x) = (2 <= x)"
+by (simp add: less_floor_eq)
+
+lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
+  apply (insert floor_less_eq [of x "a + 1"])
+  apply auto
+done
+
+lemma floor_le_eq_number_of [simp]: 
+    "(floor x <= number_of n) = (x < number_of n + 1)"
+by (simp add: floor_le_eq)
+
+lemma floor_le_eq_zero [simp]: "(floor x <= 0) = (x < 1)"
+by (simp add: floor_le_eq)
+
+lemma floor_le_eq_one [simp]: "(floor x <= 1) = (x < 2)"
+by (simp add: floor_le_eq)
+
+lemma floor_add [simp]: "floor (x + real a) = floor x + a"
+  apply (subst order_eq_iff)
+  apply (rule conjI)
+  prefer 2
+  apply (subgoal_tac "floor x + a < floor (x + real a) + 1")
+  apply arith
+  apply (subst real_of_int_less_iff [THEN sym])
+  apply simp
+  apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1")
+  apply (subgoal_tac "real (floor x) <= x")
+  apply arith
+  apply (rule real_of_int_floor_le)
+  apply (rule real_of_int_floor_add_one_gt)
+  apply (subgoal_tac "floor (x + real a) < floor x + a + 1")
+  apply arith
+  apply (subst real_of_int_less_iff [THEN sym])  
+  apply simp
+  apply (subgoal_tac "real(floor(x + real a)) <= x + real a") 
+  apply (subgoal_tac "x < real(floor x) + 1")
+  apply arith
+  apply (rule real_of_int_floor_add_one_gt)
+  apply (rule real_of_int_floor_le)
+done
+
+lemma floor_add_number_of [simp]: 
+    "floor (x + number_of n) = floor x + number_of n"
+  apply (subst floor_add [THEN sym])
+  apply simp
+done
+
+lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
+  apply (subst floor_add [THEN sym])
+  apply simp
+done
+
+lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
+  apply (subst diff_minus)+
+  apply (subst real_of_int_minus [THEN sym])
+  apply (rule floor_add)
+done
+
+lemma floor_subtract_number_of [simp]: "floor (x - number_of n) = 
+    floor x - number_of n"
+  apply (subst floor_subtract [THEN sym])
+  apply simp
+done
+
+lemma floor_subtract_one [simp]: "floor (x - 1) = floor x - 1"
+  apply (subst floor_subtract [THEN sym])
+  apply simp
+done
 
 lemma ceiling_zero [simp]: "ceiling 0 = 0"
 by (simp add: ceiling_def)
@@ -438,11 +601,11 @@
 apply (subst le_minus_iff, simp)
 done
 
-lemma ceiling_le: "x < y ==> ceiling x \<le> ceiling y"
-by (simp add: floor_le ceiling_def)
+lemma ceiling_mono: "x < y ==> ceiling x \<le> ceiling y"
+by (simp add: floor_mono ceiling_def)
 
-lemma ceiling_le2: "x \<le> y ==> ceiling x \<le> ceiling y"
-by (simp add: floor_le2 ceiling_def)
+lemma ceiling_mono2: "x \<le> y ==> ceiling x \<le> ceiling y"
+by (simp add: floor_mono2 ceiling_def)
 
 lemma real_of_int_ceiling_cancel [simp]:
      "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
@@ -472,6 +635,9 @@
 apply (rule ceiling_real_of_int)
 done
 
+lemma ceiling_one [simp]: "ceiling 1 = 1"
+  by (unfold ceiling_def, simp)
+
 lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
 apply (rule neg_le_iff_le [THEN iffD1])
 apply (simp add: ceiling_def diff_minus)
@@ -482,6 +648,473 @@
 apply (simp del: real_of_int_ceiling_diff_one_le)
 done
 
+lemma ceiling_le: "x <= real a ==> ceiling x <= a"
+  apply (unfold ceiling_def)
+  apply (subgoal_tac "-a <= floor(- x)")
+  apply simp
+  apply (rule le_floor)
+  apply simp
+done
+
+lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
+  apply (unfold ceiling_def)
+  apply (subgoal_tac "real(- a) <= - x")
+  apply simp
+  apply (rule real_le_floor)
+  apply simp
+done
+
+lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
+  apply (rule iffI)
+  apply (erule ceiling_le_real)
+  apply (erule ceiling_le)
+done
+
+lemma ceiling_le_eq_number_of [simp]: 
+    "(ceiling x <= number_of n) = (x <= number_of n)"
+by (simp add: ceiling_le_eq)
+
+lemma ceiling_le_zero_eq [simp]: "(ceiling x <= 0) = (x <= 0)" 
+by (simp add: ceiling_le_eq)
+
+lemma ceiling_le_eq_one [simp]: "(ceiling x <= 1) = (x <= 1)" 
+by (simp add: ceiling_le_eq)
+
+lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
+  apply (subst linorder_not_le [THEN sym])+
+  apply simp
+  apply (rule ceiling_le_eq)
+done
+
+lemma less_ceiling_eq_number_of [simp]: 
+    "(number_of n < ceiling x) = (number_of n < x)"
+by (simp add: less_ceiling_eq)
+
+lemma less_ceiling_eq_zero [simp]: "(0 < ceiling x) = (0 < x)"
+by (simp add: less_ceiling_eq)
+
+lemma less_ceiling_eq_one [simp]: "(1 < ceiling x) = (1 < x)"
+by (simp add: less_ceiling_eq)
+
+lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
+  apply (insert ceiling_le_eq [of x "a - 1"])
+  apply auto
+done
+
+lemma ceiling_less_eq_number_of [simp]: 
+    "(ceiling x < number_of n) = (x <= number_of n - 1)"
+by (simp add: ceiling_less_eq)
+
+lemma ceiling_less_eq_zero [simp]: "(ceiling x < 0) = (x <= -1)"
+by (simp add: ceiling_less_eq)
+
+lemma ceiling_less_eq_one [simp]: "(ceiling x < 1) = (x <= 0)"
+by (simp add: ceiling_less_eq)
+
+lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
+  apply (insert less_ceiling_eq [of "a - 1" x])
+  apply auto
+done
+
+lemma le_ceiling_eq_number_of [simp]: 
+    "(number_of n <= ceiling x) = (number_of n - 1 < x)"
+by (simp add: le_ceiling_eq)
+
+lemma le_ceiling_eq_zero [simp]: "(0 <= ceiling x) = (-1 < x)"
+by (simp add: le_ceiling_eq)
+
+lemma le_ceiling_eq_one [simp]: "(1 <= ceiling x) = (0 < x)"
+by (simp add: le_ceiling_eq)
+
+lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
+  apply (unfold ceiling_def, simp)
+  apply (subst real_of_int_minus [THEN sym])
+  apply (subst floor_add)
+  apply simp
+done
+
+lemma ceiling_add_number_of [simp]: "ceiling (x + number_of n) = 
+    ceiling x + number_of n"
+  apply (subst ceiling_add [THEN sym])
+  apply simp
+done
+
+lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
+  apply (subst ceiling_add [THEN sym])
+  apply simp
+done
+
+lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
+  apply (subst diff_minus)+
+  apply (subst real_of_int_minus [THEN sym])
+  apply (rule ceiling_add)
+done
+
+lemma ceiling_subtract_number_of [simp]: "ceiling (x - number_of n) = 
+    ceiling x - number_of n"
+  apply (subst ceiling_subtract [THEN sym])
+  apply simp
+done
+
+lemma ceiling_subtract_one [simp]: "ceiling (x - 1) = ceiling x - 1"
+  apply (subst ceiling_subtract [THEN sym])
+  apply simp
+done
+
+subsection {* Versions for the natural numbers *}
+
+constdefs
+  natfloor :: "real => nat"
+  "natfloor x == nat(floor x)"
+  natceiling :: "real => nat"
+  "natceiling x == nat(ceiling x)"
+
+lemma natfloor_zero [simp]: "natfloor 0 = 0"
+  by (unfold natfloor_def, simp)
+
+lemma natfloor_one [simp]: "natfloor 1 = 1"
+  by (unfold natfloor_def, simp)
+
+lemma zero_le_natfloor [simp]: "0 <= natfloor x"
+  by (unfold natfloor_def, simp)
+
+lemma natfloor_number_of_eq [simp]: "natfloor (number_of n) = number_of n"
+  by (unfold natfloor_def, simp)
+
+lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
+  by (unfold natfloor_def, simp)
+
+lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
+  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_mono2)
+done
+
+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_mono2) 
+  apply (subst natfloor_neg)
+  apply simp
+  apply simp
+done
+
+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 le_floor)
+  apply simp
+done
+
+lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
+  apply (rule iffI)
+  apply (rule order_trans)
+  prefer 2
+  apply (erule real_natfloor_le)
+  apply (subst real_of_nat_le_iff)
+  apply assumption
+  apply (erule le_natfloor)
+done
+
+lemma le_natfloor_eq_number_of [simp]: 
+    "~ neg((number_of n)::int) ==> 0 <= x ==>
+      (number_of n <= natfloor x) = (number_of n <= x)"
+  apply (subst le_natfloor_eq, assumption)
+  apply simp
+done
+
+lemma le_natfloor_one_eq [simp]: "(1 <= natfloor x) = (1 <= x)"
+  apply (case_tac "0 <= x")
+  apply (subst le_natfloor_eq, assumption, simp)
+  apply (rule iffI)
+  apply (subgoal_tac "natfloor x <= natfloor 0") 
+  apply simp
+  apply (rule natfloor_mono)
+  apply simp
+  apply simp
+done
+
+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 eq_nat_nat_iff)
+  apply simp
+  apply simp
+  apply (rule floor_eq2)
+  apply auto
+done
+
+lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
+  apply (case_tac "0 <= x")
+  apply (unfold natfloor_def)
+  apply simp
+  apply simp_all
+done
+
+lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
+  apply (simp add: compare_rls)
+  apply (rule real_natfloor_add_one_gt)
+done
+
+lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
+  apply (subgoal_tac "z < real(natfloor z) + 1")
+  apply arith
+  apply (rule real_natfloor_add_one_gt)
+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)
+  apply simp
+done
+
+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
+
+lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
+  apply (subst natfloor_add [THEN sym])
+  apply assumption
+  apply simp
+done
+
+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
+  apply (subst nat_diff_distrib)
+  apply simp
+  apply (rule le_floor)
+  apply simp_all
+done
+
+lemma natceiling_zero [simp]: "natceiling 0 = 0"
+  by (unfold natceiling_def, simp)
+
+lemma natceiling_one [simp]: "natceiling 1 = 1"
+  by (unfold natceiling_def, simp)
+
+lemma zero_le_natceiling [simp]: "0 <= natceiling x"
+  by (unfold natceiling_def, simp)
+
+lemma natceiling_number_of_eq [simp]: "natceiling (number_of n) = number_of n"
+  by (unfold natceiling_def, simp)
+
+lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
+  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_mono2)
+  apply simp
+  apply simp
+done
+
+lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
+  apply (unfold natceiling_def)
+  apply simp
+done
+
+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_mono2)
+  apply (subst natceiling_neg)
+  apply simp_all
+done
+
+lemma natceiling_le: "x <= real a ==> natceiling x <= a"
+  apply (unfold natceiling_def)
+  apply (case_tac "x < 0")
+  apply simp
+  apply (subst nat_int [THEN sym]);back;
+  apply (subst nat_le_eq_zle)
+  apply simp
+  apply (rule ceiling_le)
+  apply simp
+done
+
+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
+
+lemma natceiling_le_eq2 [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
+
+lemma natceiling_one_le_eq: "(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
+
+lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
+  apply (unfold natceiling_def)
+  apply (subst nat_int [THEN sym]);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_mono2)
+  apply force
+  apply force
+  apply (rule ceiling_eq2)
+  apply (simp, simp)
+  apply (subst nat_add_distrib)
+  apply auto
+done
+
+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
+  apply (subst nat_add_distrib)
+  apply (subgoal_tac "0 = ceiling 0")
+  apply (erule ssubst)
+  apply (erule ceiling_mono2)
+  apply simp_all
+done
+
+lemma natceiling_add2 [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
+
+lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
+  apply (subst natceiling_add [THEN sym])
+  apply assumption
+  apply simp
+done
+
+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
+  apply (subst nat_diff_distrib)
+  apply simp
+  apply (rule order_trans)
+  prefer 2
+  apply (rule ceiling_mono2)
+  apply assumption
+  apply simp_all
+done
+
+lemma natfloor_div_nat: "1 <= x ==> 0 < y ==> 
+  natfloor (x / real y) = natfloor x div y"
+proof -
+  assume "1 <= (x::real)" and "0 < (y::nat)"
+  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: ring_distrib ring_eq_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: compare_rls)
+    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: compare_rls)
+    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: compare_rls)
+    apply (subgoal_tac "real(natfloor x mod y) + 1 = 
+      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 assumption
+    apply auto
+    apply (simp add: compare_rls)
+    apply (subst add_commute)
+    apply (rule real_natfloor_add_one_gt)
+    done
+  finally show ?thesis
+    by simp
+qed
+
 ML
 {*
 val number_of_less_real_of_int_iff = thm "number_of_less_real_of_int_iff";
@@ -501,8 +1134,9 @@
 val real_lb_ub_int = thm "real_lb_ub_int";
 val lemma_floor = thm "lemma_floor";
 val real_of_int_floor_le = thm "real_of_int_floor_le";
-val floor_le = thm "floor_le";
+(*val floor_le = thm "floor_le";
 val floor_le2 = thm "floor_le2";
+*)
 val lemma_floor2 = thm "lemma_floor2";
 val real_of_int_floor_cancel = thm "real_of_int_floor_cancel";
 val floor_eq = thm "floor_eq";
@@ -518,8 +1152,10 @@
 val ceiling_floor = thm "ceiling_floor";
 val floor_ceiling = thm "floor_ceiling";
 val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge";
+(*
 val ceiling_le = thm "ceiling_le";
 val ceiling_le2 = thm "ceiling_le2";
+*)
 val real_of_int_ceiling_cancel = thm "real_of_int_ceiling_cancel";
 val ceiling_eq = thm "ceiling_eq";
 val ceiling_eq2 = thm "ceiling_eq2";
diff -r 2b82259cc7b2 -r 00d8f9300d13 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Wed Jul 13 16:47:23 2005 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed Jul 13 19:49:07 2005 +0200
@@ -3,6 +3,7 @@
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
+    Additional contributions by Jeremy Avigad
 *)
 
 header{*Defining the Reals from the Positive Reals*}
@@ -635,27 +636,46 @@
   real_of_nat_def: "real z == of_nat z"
   real_of_int_def: "real z == of_int z"
 
+lemma real_eq_of_nat: "real = of_nat"
+  apply (rule ext)
+  apply (unfold real_of_nat_def)
+  apply (rule refl)
+  done
+
+lemma real_eq_of_int: "real = of_int"
+  apply (rule ext)
+  apply (unfold real_of_int_def)
+  apply (rule refl)
+  done
+
 lemma real_of_int_zero [simp]: "real (0::int) = 0"  
 by (simp add: real_of_int_def) 
 
 lemma real_of_one [simp]: "real (1::int) = (1::real)"
 by (simp add: real_of_int_def) 
 
-lemma real_of_int_add: "real (x::int) + real y = real (x + y)"
+lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y"
 by (simp add: real_of_int_def) 
-declare real_of_int_add [symmetric, simp]
 
-lemma real_of_int_minus: "-real (x::int) = real (-x)"
+lemma real_of_int_minus [simp]: "real(-x) = -real (x::int)"
 by (simp add: real_of_int_def) 
-declare real_of_int_minus [symmetric, simp]
+
+lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y"
+by (simp add: real_of_int_def) 
 
-lemma real_of_int_diff: "real (x::int) - real y = real (x - y)"
+lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"
 by (simp add: real_of_int_def) 
-declare real_of_int_diff [symmetric, simp]
 
-lemma real_of_int_mult: "real (x::int) * real y = real (x * y)"
-by (simp add: real_of_int_def) 
-declare real_of_int_mult [symmetric, simp]
+lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))"
+  apply (subst real_eq_of_int)+
+  apply (rule of_int_setsum)
+done
+
+lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) = 
+    (PROD x:A. real(f x))"
+  apply (subst real_eq_of_int)+
+  apply (rule of_int_setprod)
+done
 
 lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = (0::int))"
 by (simp add: real_of_int_def) 
@@ -669,6 +689,91 @@
 lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)"
 by (simp add: real_of_int_def) 
 
+lemma real_of_int_gt_zero_cancel_iff [simp]: "(0 < real (n::int)) = (0 < n)"
+by (simp add: real_of_int_def) 
+
+lemma real_of_int_ge_zero_cancel_iff [simp]: "(0 <= real (n::int)) = (0 <= n)"
+by (simp add: real_of_int_def) 
+
+lemma real_of_int_lt_zero_cancel_iff [simp]: "(real (n::int) < 0) = (n < 0)"
+by (simp add: real_of_int_def)
+
+lemma real_of_int_le_zero_cancel_iff [simp]: "(real (n::int) <= 0) = (n <= 0)"
+by (simp add: real_of_int_def)
+
+lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)"
+  apply (subgoal_tac "real n + 1 = real (n + 1)")
+  apply (simp del: real_of_int_add)
+  apply auto
+done
+
+lemma int_le_real_less: "((n::int) <= m) = (real n < real m + 1)"
+  apply (subgoal_tac "real m + 1 = real (m + 1)")
+  apply (simp del: real_of_int_add)
+  apply simp
+done
+
+lemma real_of_int_div_aux: "d ~= 0 ==> (real (x::int)) / (real d) = 
+    real (x div d) + (real (x mod d)) / (real d)"
+proof -
+  assume "d ~= 0"
+  have "x = (x div d) * d + x mod d"
+    by auto
+  then have "real x = real (x div d) * real d + real(x mod d)"
+    by (simp only: real_of_int_mult [THEN sym] real_of_int_add [THEN sym])
+  then have "real x / real d = ... / real d"
+    by simp
+  then show ?thesis
+    by (auto simp add: add_divide_distrib ring_eq_simps prems)
+qed
+
+lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
+    real(n div d) = real n / real d"
+  apply (frule real_of_int_div_aux [of d n])
+  apply simp
+  apply (simp add: zdvd_iff_zmod_eq_0)
+done
+
+lemma real_of_int_div2:
+  "0 <= real (n::int) / real (x) - real (n div x)"
+  apply (case_tac "x = 0")
+  apply simp
+  apply (case_tac "0 < x")
+  apply (simp add: compare_rls)
+  apply (subst real_of_int_div_aux)
+  apply simp
+  apply simp
+  apply (subst zero_le_divide_iff)
+  apply auto
+  apply (simp add: compare_rls)
+  apply (subst real_of_int_div_aux)
+  apply simp
+  apply simp
+  apply (subst zero_le_divide_iff)
+  apply auto
+done
+
+lemma real_of_int_div3:
+  "real (n::int) / real (x) - real (n div x) <= 1"
+  apply(case_tac "x = 0")
+  apply simp
+  apply (simp add: compare_rls)
+  apply (subst real_of_int_div_aux)
+  apply assumption
+  apply simp
+  apply (subst divide_le_eq)
+  apply clarsimp
+  apply (rule conjI)
+  apply (rule impI)
+  apply (rule order_less_imp_le)
+  apply simp
+  apply (rule impI)
+  apply (rule order_less_imp_le)
+  apply simp
+done
+
+lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" 
+  by (insert real_of_int_div2 [of n x], simp)
 
 subsection{*Embedding the Naturals into the Reals*}
 
@@ -701,6 +806,24 @@
 lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
 by (simp add: real_of_nat_def)
 
+lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = 
+    (SUM x:A. real(f x))"
+  apply (subst real_eq_of_nat)+
+  apply (rule of_nat_setsum)
+done
+
+lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) = 
+    (PROD x:A. real(f x))"
+  apply (subst real_eq_of_nat)+
+  apply (rule of_nat_setprod)
+done
+
+lemma real_of_card: "real (card A) = setsum (%x.1) A"
+  apply (subst card_eq_setsum)
+  apply (subst real_of_nat_setsum)
+  apply simp
+done
+
 lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
 by (simp add: real_of_nat_def)
 
@@ -722,13 +845,76 @@
 lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat)) = (0 \<le> n)"
 by (simp add: add: real_of_nat_def)
 
+lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
+  apply (subgoal_tac "real n + 1 = real (Suc n)")
+  apply simp
+  apply (auto simp add: real_of_nat_Suc)
+done
+
+lemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)"
+  apply (subgoal_tac "real m + 1 = real (Suc m)")
+  apply (simp add: less_Suc_eq_le)
+  apply (simp add: real_of_nat_Suc)
+done
+
+lemma real_of_nat_div_aux: "0 < d ==> (real (x::nat)) / (real d) = 
+    real (x div d) + (real (x mod d)) / (real d)"
+proof -
+  assume "0 < d"
+  have "x = (x div d) * d + x mod d"
+    by auto
+  then have "real x = real (x div d) * real d + real(x mod d)"
+    by (simp only: real_of_nat_mult [THEN sym] real_of_nat_add [THEN sym])
+  then have "real x / real d = \<dots> / real d"
+    by simp
+  then show ?thesis
+    by (auto simp add: add_divide_distrib ring_eq_simps prems)
+qed
+
+lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==>
+    real(n div d) = real n / real d"
+  apply (frule real_of_nat_div_aux [of d n])
+  apply simp
+  apply (subst dvd_eq_mod_eq_0 [THEN sym])
+  apply assumption
+done
+
+lemma real_of_nat_div2:
+  "0 <= real (n::nat) / real (x) - real (n div x)"
+  apply(case_tac "x = 0")
+  apply simp
+  apply (simp add: compare_rls)
+  apply (subst real_of_nat_div_aux)
+  apply assumption
+  apply simp
+  apply (subst zero_le_divide_iff)
+  apply simp
+done
+
+lemma real_of_nat_div3:
+  "real (n::nat) / real (x) - real (n div x) <= 1"
+  apply(case_tac "x = 0")
+  apply simp
+  apply (simp add: compare_rls)
+  apply (subst real_of_nat_div_aux)
+  apply assumption
+  apply simp
+done
+
+lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" 
+  by (insert real_of_nat_div2 [of n x], simp)
+
 lemma real_of_int_real_of_nat: "real (int n) = real n"
 by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat)
 
 lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
 by (simp add: real_of_int_def real_of_nat_def)
 
-
+lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x"
+  apply (subgoal_tac "real(int(nat x)) = real(nat x)")
+  apply force
+  apply (simp only: real_of_int_real_of_nat)
+done
 
 subsection{*Numerals and Arithmetic*}