Additions to the Real (and Hyperreal) libraries:
authoravigad
Wed Jul 13 19:49:07 2005 +0200 (2005-07-13)
changeset 1681900d8f9300d13
parent 16818 2b82259cc7b2
child 16820 5c9d597e4cb9
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
src/HOL/Hyperreal/Log.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Real/RComplete.thy
src/HOL/Real/RealDef.thy
     1.1 --- a/src/HOL/Hyperreal/Log.thy	Wed Jul 13 16:47:23 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/Log.thy	Wed Jul 13 19:49:07 2005 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title       : Log.thy
     1.5      Author      : Jacques D. Fleuriot
     1.6 +                  Additional contributions by Jeremy Avigad
     1.7      Copyright   : 2000,2001 University of Edinburgh
     1.8  *)
     1.9  
    1.10 @@ -38,6 +39,9 @@
    1.11  lemma powr_gt_zero [simp]: "0 < x powr a"
    1.12  by (simp add: powr_def)
    1.13  
    1.14 +lemma powr_ge_pzero [simp]: "0 <= x powr y"
    1.15 +by (rule order_less_imp_le, rule powr_gt_zero)
    1.16 +
    1.17  lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
    1.18  by (simp add: powr_def)
    1.19  
    1.20 @@ -47,6 +51,12 @@
    1.21  apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
    1.22  done
    1.23  
    1.24 +lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
    1.25 +  apply (simp add: powr_def)
    1.26 +  apply (subst exp_diff [THEN sym])
    1.27 +  apply (simp add: left_diff_distrib)
    1.28 +done
    1.29 +
    1.30  lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
    1.31  by (simp add: powr_def exp_add [symmetric] left_distrib)
    1.32  
    1.33 @@ -129,8 +139,6 @@
    1.34  by (simp add: linorder_not_less [symmetric])
    1.35  
    1.36  
    1.37 -subsection{*Further Results Courtesy Jeremy Avigad*}
    1.38 -
    1.39  lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
    1.40    apply (induct n, simp)
    1.41    apply (subgoal_tac "real(Suc n) = real n + 1")
    1.42 @@ -176,13 +184,95 @@
    1.43    apply assumption+
    1.44  done
    1.45  
    1.46 -lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a";
    1.47 +lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a <
    1.48 +    x powr a"
    1.49 +  apply (unfold powr_def)
    1.50 +  apply (rule exp_less_mono)
    1.51 +  apply (rule mult_strict_left_mono_neg)
    1.52 +  apply (subst ln_less_cancel_iff)
    1.53 +  apply assumption
    1.54 +  apply (rule order_less_trans)
    1.55 +  prefer 2
    1.56 +  apply assumption+
    1.57 +done
    1.58 +
    1.59 +lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
    1.60    apply (case_tac "a = 0", simp)
    1.61    apply (case_tac "x = y", simp)
    1.62    apply (rule order_less_imp_le)
    1.63    apply (rule powr_less_mono2, auto)
    1.64  done
    1.65  
    1.66 +lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
    1.67 +  apply (rule mult_imp_le_div_pos)
    1.68 +  apply (assumption)
    1.69 +  apply (subst mult_commute)
    1.70 +  apply (subst ln_pwr [THEN sym])
    1.71 +  apply auto
    1.72 +  apply (rule ln_bound)
    1.73 +  apply (erule ge_one_powr_ge_zero)
    1.74 +  apply (erule order_less_imp_le)
    1.75 +done
    1.76 +
    1.77 +lemma ln_powr_bound2: "1 < x ==> 0 < a ==> (ln x) powr a <= (a powr a) * x"
    1.78 +proof -
    1.79 +  assume "1 < x" and "0 < a"
    1.80 +  then have "ln x <= (x powr (1 / a)) / (1 / a)"
    1.81 +    apply (intro ln_powr_bound)
    1.82 +    apply (erule order_less_imp_le)
    1.83 +    apply (rule divide_pos_pos)
    1.84 +    apply simp_all
    1.85 +    done
    1.86 +  also have "... = a * (x powr (1 / a))"
    1.87 +    by simp
    1.88 +  finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
    1.89 +    apply (intro powr_mono2)
    1.90 +    apply (rule order_less_imp_le, rule prems)
    1.91 +    apply (rule ln_gt_zero)
    1.92 +    apply (rule prems)
    1.93 +    apply assumption
    1.94 +    done
    1.95 +  also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
    1.96 +    apply (rule powr_mult)
    1.97 +    apply (rule prems)
    1.98 +    apply (rule powr_gt_zero)
    1.99 +    done
   1.100 +  also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
   1.101 +    by (rule powr_powr)
   1.102 +  also have "... = x"
   1.103 +    apply simp
   1.104 +    apply (subgoal_tac "a ~= 0")
   1.105 +    apply (insert prems, auto)
   1.106 +    done
   1.107 +  finally show ?thesis .
   1.108 +qed
   1.109 +
   1.110 +lemma LIMSEQ_neg_powr: "0 < s ==> (%x. (real x) powr - s) ----> 0"
   1.111 +  apply (unfold LIMSEQ_def)
   1.112 +  apply clarsimp
   1.113 +  apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI)
   1.114 +  apply clarify
   1.115 +  proof -
   1.116 +    fix r fix n
   1.117 +    assume "0 < s" and "0 < r" and "natfloor (r powr (1 / - s)) + 1 <= n"
   1.118 +    have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1"
   1.119 +      by (rule real_natfloor_add_one_gt)
   1.120 +    also have "... = real(natfloor(r powr (1 / -s)) + 1)"
   1.121 +      by simp
   1.122 +    also have "... <= real n"
   1.123 +      apply (subst real_of_nat_le_iff)
   1.124 +      apply (rule prems)
   1.125 +      done
   1.126 +    finally have "r powr (1 / - s) < real n".
   1.127 +    then have "real n powr (- s) < (r powr (1 / - s)) powr - s" 
   1.128 +      apply (intro powr_less_mono2_neg)
   1.129 +      apply (auto simp add: prems)
   1.130 +      done
   1.131 +    also have "... = r"
   1.132 +      by (simp add: powr_powr prems less_imp_neq [THEN not_sym])
   1.133 +    finally show "real n powr - s < r" .
   1.134 +  qed
   1.135 +
   1.136  
   1.137  
   1.138  ML
     2.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 13 16:47:23 2005 +0200
     2.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 13 19:49:07 2005 +0200
     2.3 @@ -10,33 +10,6 @@
     2.4  imports Log
     2.5  begin
     2.6  
     2.7 -(* FIXME generalize? *)
     2.8 -lemma sumr_offset:
     2.9 - "(\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
    2.10 -by (induct "n", auto)
    2.11 -
    2.12 -lemma sumr_offset2:
    2.13 - "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
    2.14 -by (induct "n", auto)
    2.15 -
    2.16 -lemma sumr_offset3:
    2.17 -  "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
    2.18 -by (simp  add: sumr_offset)
    2.19 -
    2.20 -lemma sumr_offset4:
    2.21 - "\<forall>n f. setsum f {0::nat..<n+k} =
    2.22 -        (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
    2.23 -by (simp add: sumr_offset)
    2.24 -
    2.25 -(*
    2.26 -lemma sumr_from_1_from_0: "0 < n ==>
    2.27 -      (\<Sum>n=Suc 0 ..< Suc n. if even(n) then 0 else
    2.28 -             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n =
    2.29 -      (\<Sum>n=0..<Suc n. if even(n) then 0 else
    2.30 -             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n"
    2.31 -by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto)
    2.32 -*)
    2.33 -
    2.34  subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
    2.35  
    2.36  text{*This is a very long, messy proof even now that it's been broken down
     3.1 --- a/src/HOL/Hyperreal/SEQ.thy	Wed Jul 13 16:47:23 2005 +0200
     3.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Wed Jul 13 19:49:07 2005 +0200
     3.3 @@ -3,6 +3,7 @@
     3.4      Copyright   : 1998  University of Cambridge
     3.5      Description : Convergence of sequences and series
     3.6      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     3.7 +    Additional contributions by Jeremy Avigad
     3.8  *)
     3.9  
    3.10  theory SEQ
    3.11 @@ -204,6 +205,15 @@
    3.12  lemma LIMSEQ_add: "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b"
    3.13  by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add)
    3.14  
    3.15 +lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b"
    3.16 +  apply (subgoal_tac "%n. (f n + b) == %n. (f n + (%n. b) n)")
    3.17 +  apply (subgoal_tac "(%n. b) ----> b")
    3.18 +  apply (auto simp add: LIMSEQ_add LIMSEQ_const)
    3.19 +done
    3.20 +
    3.21 +lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b"
    3.22 +by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_add_const)
    3.23 +
    3.24  lemma NSLIMSEQ_mult:
    3.25        "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
    3.26  by (auto intro!: approx_mult_HFinite 
    3.27 @@ -243,6 +253,15 @@
    3.28  apply (blast intro: NSLIMSEQ_add_minus)
    3.29  done
    3.30  
    3.31 +lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n  - b)) ----> a - b"
    3.32 +  apply (subgoal_tac "%n. (f n - b) == %n. (f n - (%n. b) n)")
    3.33 +  apply (subgoal_tac "(%n. b) ----> b")
    3.34 +  apply (auto simp add: LIMSEQ_diff LIMSEQ_const)
    3.35 +done
    3.36 +
    3.37 +lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
    3.38 +by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_diff_const)
    3.39 +
    3.40  text{*Proof is like that of @{text NSLIM_inverse}.*}
    3.41  lemma NSLIMSEQ_inverse:
    3.42       "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
    3.43 @@ -294,6 +313,66 @@
    3.44      by (simp add: setsum_def LIMSEQ_const)
    3.45  qed
    3.46  
    3.47 +lemma LIMSEQ_setprod:
    3.48 +  assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
    3.49 +  shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)"
    3.50 +proof (cases "finite S")
    3.51 +  case True
    3.52 +  thus ?thesis using n
    3.53 +  proof (induct)
    3.54 +    case empty
    3.55 +    show ?case
    3.56 +      by (simp add: LIMSEQ_const)
    3.57 +  next
    3.58 +    case insert
    3.59 +    thus ?case
    3.60 +      by (simp add: LIMSEQ_mult)
    3.61 +  qed
    3.62 +next
    3.63 +  case False
    3.64 +  thus ?thesis
    3.65 +    by (simp add: setprod_def LIMSEQ_const)
    3.66 +qed
    3.67 +
    3.68 +lemma LIMSEQ_ignore_initial_segment: "f ----> a 
    3.69 +  ==> (%n. f(n + k)) ----> a"
    3.70 +  apply (unfold LIMSEQ_def) 
    3.71 +  apply (clarify)
    3.72 +  apply (drule_tac x = r in spec)
    3.73 +  apply (clarify)
    3.74 +  apply (rule_tac x = "no + k" in exI)
    3.75 +  by auto
    3.76 +
    3.77 +lemma LIMSEQ_offset: "(%x. f (x + k)) ----> a ==>
    3.78 +    f ----> a"
    3.79 +  apply (unfold LIMSEQ_def)
    3.80 +  apply clarsimp
    3.81 +  apply (drule_tac x = r in spec)
    3.82 +  apply clarsimp
    3.83 +  apply (rule_tac x = "no + k" in exI)
    3.84 +  apply clarsimp
    3.85 +  apply (drule_tac x = "n - k" in spec)
    3.86 +  apply (frule mp)
    3.87 +  apply arith
    3.88 +  apply simp
    3.89 +done
    3.90 +
    3.91 +lemma LIMSEQ_diff_approach_zero: 
    3.92 +  "g ----> L ==> (%x. f x - g x) ----> 0  ==>
    3.93 +     f ----> L"
    3.94 +  apply (drule LIMSEQ_add)
    3.95 +  apply assumption
    3.96 +  apply simp
    3.97 +done
    3.98 +
    3.99 +lemma LIMSEQ_diff_approach_zero2: 
   3.100 +  "f ----> L ==> (%x. f x - g x) ----> 0  ==>
   3.101 +     g ----> L";
   3.102 +  apply (drule LIMSEQ_diff)
   3.103 +  apply assumption
   3.104 +  apply simp
   3.105 +done
   3.106 +
   3.107  
   3.108  subsection{*Nslim and Lim*}
   3.109  
     4.1 --- a/src/HOL/Hyperreal/Series.thy	Wed Jul 13 16:47:23 2005 +0200
     4.2 +++ b/src/HOL/Hyperreal/Series.thy	Wed Jul 13 19:49:07 2005 +0200
     4.3 @@ -4,6 +4,7 @@
     4.4  
     4.5  Converted to Isar and polished by lcp
     4.6  Converted to setsum and polished yet more by TNN
     4.7 +Additional contributions by Jeremy Avigad
     4.8  *) 
     4.9  
    4.10  header{*Finite Summation and Infinite Series*}
    4.11 @@ -60,6 +61,32 @@
    4.12  apply (simp_all add: setsum_add_nat_ivl add_commute)
    4.13  done
    4.14  
    4.15 +(* FIXME generalize? *)
    4.16 +lemma sumr_offset:
    4.17 + "(\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
    4.18 +by (induct "n", auto)
    4.19 +
    4.20 +lemma sumr_offset2:
    4.21 + "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
    4.22 +by (induct "n", auto)
    4.23 +
    4.24 +lemma sumr_offset3:
    4.25 +  "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
    4.26 +by (simp  add: sumr_offset)
    4.27 +
    4.28 +lemma sumr_offset4:
    4.29 + "\<forall>n f. setsum f {0::nat..<n+k} =
    4.30 +        (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
    4.31 +by (simp add: sumr_offset)
    4.32 +
    4.33 +(*
    4.34 +lemma sumr_from_1_from_0: "0 < n ==>
    4.35 +      (\<Sum>n=Suc 0 ..< Suc n. if even(n) then 0 else
    4.36 +             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n =
    4.37 +      (\<Sum>n=0..<Suc n. if even(n) then 0 else
    4.38 +             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n"
    4.39 +by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto)
    4.40 +*)
    4.41  
    4.42  subsection{* Infinite Sums, by the Properties of Limits*}
    4.43  
    4.44 @@ -88,6 +115,34 @@
    4.45  apply (auto intro!: LIMSEQ_unique simp add: sums_def)
    4.46  done
    4.47  
    4.48 +lemma sums_split_initial_segment: "f sums s ==> 
    4.49 +  (%n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
    4.50 +  apply (unfold sums_def);
    4.51 +  apply (simp add: sumr_offset); 
    4.52 +  apply (rule LIMSEQ_diff_const)
    4.53 +  apply (rule LIMSEQ_ignore_initial_segment)
    4.54 +  apply assumption
    4.55 +done
    4.56 +
    4.57 +lemma summable_ignore_initial_segment: "summable f ==> 
    4.58 +    summable (%n. f(n + k))"
    4.59 +  apply (unfold summable_def)
    4.60 +  apply (auto intro: sums_split_initial_segment)
    4.61 +done
    4.62 +
    4.63 +lemma suminf_minus_initial_segment: "summable f ==>
    4.64 +    suminf f = s ==> suminf (%n. f(n + k)) = s - (SUM i = 0..< k. f i)"
    4.65 +  apply (frule summable_ignore_initial_segment)
    4.66 +  apply (rule sums_unique [THEN sym])
    4.67 +  apply (frule summable_sums)
    4.68 +  apply (rule sums_split_initial_segment)
    4.69 +  apply auto
    4.70 +done
    4.71 +
    4.72 +lemma suminf_split_initial_segment: "summable f ==> 
    4.73 +    suminf f = (SUM i = 0..< k. f i) + suminf (%n. f(n + k))"
    4.74 +by (auto simp add: suminf_minus_initial_segment)
    4.75 +
    4.76  lemma series_zero: 
    4.77       "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
    4.78  apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
    4.79 @@ -95,30 +150,112 @@
    4.80  apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong)
    4.81  done
    4.82  
    4.83 +lemma sums_zero: "(%n. 0) sums 0";
    4.84 +  apply (unfold sums_def);
    4.85 +  apply simp;
    4.86 +  apply (rule LIMSEQ_const);
    4.87 +done;
    4.88  
    4.89 -lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"
    4.90 +lemma summable_zero: "summable (%n. 0)";
    4.91 +  apply (rule sums_summable);
    4.92 +  apply (rule sums_zero);
    4.93 +done;
    4.94 +
    4.95 +lemma suminf_zero: "suminf (%n. 0) = 0";
    4.96 +  apply (rule sym);
    4.97 +  apply (rule sums_unique);
    4.98 +  apply (rule sums_zero);
    4.99 +done;
   4.100 +  
   4.101 +lemma sums_mult: "f sums a ==> (%n. c * f n) sums (c * a)"
   4.102  by (auto simp add: sums_def setsum_mult [symmetric]
   4.103           intro!: LIMSEQ_mult intro: LIMSEQ_const)
   4.104  
   4.105 -lemma sums_divide: "x sums x' ==> (%n. x(n)/c) sums (x'/c)"
   4.106 +lemma summable_mult: "summable f ==> summable (%n. c * f n)";
   4.107 +  apply (unfold summable_def);
   4.108 +  apply (auto intro: sums_mult);
   4.109 +done;
   4.110 +
   4.111 +lemma suminf_mult: "summable f ==> suminf (%n. c * f n) = c * suminf f";
   4.112 +  apply (rule sym);
   4.113 +  apply (rule sums_unique);
   4.114 +  apply (rule sums_mult);
   4.115 +  apply (erule summable_sums);
   4.116 +done;
   4.117 +
   4.118 +lemma sums_mult2: "f sums a ==> (%n. f n * c) sums (a * c)"
   4.119 +apply (subst mult_commute)
   4.120 +apply (subst mult_commute);back;
   4.121 +apply (erule sums_mult)
   4.122 +done
   4.123 +
   4.124 +lemma summable_mult2: "summable f ==> summable (%n. f n * c)"
   4.125 +  apply (unfold summable_def)
   4.126 +  apply (auto intro: sums_mult2)
   4.127 +done
   4.128 +
   4.129 +lemma suminf_mult2: "summable f ==> suminf f * c = (\<Sum>n. f n * c)"
   4.130 +by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute)
   4.131 +
   4.132 +lemma sums_divide: "f sums a ==> (%n. (f n)/c) sums (a/c)"
   4.133  by (simp add: real_divide_def sums_mult mult_commute [of _ "inverse c"])
   4.134  
   4.135 +lemma summable_divide: "summable f ==> summable (%n. (f n) / c)";
   4.136 +  apply (unfold summable_def);
   4.137 +  apply (auto intro: sums_divide);
   4.138 +done;
   4.139 +
   4.140 +lemma suminf_divide: "summable f ==> suminf (%n. (f n) / c) = (suminf f) / c";
   4.141 +  apply (rule sym);
   4.142 +  apply (rule sums_unique);
   4.143 +  apply (rule sums_divide);
   4.144 +  apply (erule summable_sums);
   4.145 +done;
   4.146 +
   4.147 +lemma sums_add: "[| x sums x0; y sums y0 |] ==> (%n. x n + y n) sums (x0+y0)"
   4.148 +by (auto simp add: sums_def setsum_addf intro: LIMSEQ_add)
   4.149 +
   4.150 +lemma summable_add: "summable f ==> summable g ==> summable (%x. f x + g x)";
   4.151 +  apply (unfold summable_def);
   4.152 +  apply clarify;
   4.153 +  apply (rule exI);
   4.154 +  apply (erule sums_add);
   4.155 +  apply assumption;
   4.156 +done;
   4.157 +
   4.158 +lemma suminf_add:
   4.159 +     "[| summable f; summable g |]   
   4.160 +      ==> suminf f + suminf g  = (\<Sum>n. f n + g n)"
   4.161 +by (auto intro!: sums_add sums_unique summable_sums)
   4.162 +
   4.163  lemma sums_diff: "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)"
   4.164  by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff)
   4.165  
   4.166 -lemma suminf_mult: "summable f ==> suminf f * c = (\<Sum>n. f n * c)"
   4.167 -by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute)
   4.168 -
   4.169 -lemma suminf_mult2: "summable f ==> c * suminf f  = (\<Sum>n. c * f n)"
   4.170 -by (auto intro!: sums_unique sums_mult summable_sums)
   4.171 +lemma summable_diff: "summable f ==> summable g ==> summable (%x. f x - g x)";
   4.172 +  apply (unfold summable_def);
   4.173 +  apply clarify;
   4.174 +  apply (rule exI);
   4.175 +  apply (erule sums_diff);
   4.176 +  apply assumption;
   4.177 +done;
   4.178  
   4.179  lemma suminf_diff:
   4.180       "[| summable f; summable g |]   
   4.181        ==> suminf f - suminf g  = (\<Sum>n. f n - g n)"
   4.182  by (auto intro!: sums_diff sums_unique summable_sums)
   4.183  
   4.184 -lemma sums_minus: "x sums x0 ==> (%n. - x n) sums - x0"
   4.185 -by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf)
   4.186 +lemma sums_minus: "f sums s ==> (%x. - f x) sums (- s)";
   4.187 +  by (simp add: sums_def setsum_negf LIMSEQ_minus);
   4.188 +
   4.189 +lemma summable_minus: "summable f ==> summable (%x. - f x)";
   4.190 +  by (auto simp add: summable_def intro: sums_minus);
   4.191 +
   4.192 +lemma suminf_minus: "summable f ==> suminf (%x. - f x) = - (suminf f)";
   4.193 +  apply (rule sym);
   4.194 +  apply (rule sums_unique);
   4.195 +  apply (rule sums_minus);
   4.196 +  apply (erule summable_sums);
   4.197 +done;
   4.198  
   4.199  lemma sums_group:
   4.200       "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
     5.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jul 13 16:47:23 2005 +0200
     5.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Jul 13 19:49:07 2005 +0200
     5.3 @@ -568,7 +568,7 @@
     5.4   apply (rule_tac [2] g = "%n. f n * \<bar>h\<bar>" in summable_comparison_test)
     5.5    apply (rule_tac [2] x = 0 in exI, auto)
     5.6  apply (rule_tac j = "\<Sum>n. \<bar>g h n\<bar>" in real_le_trans)
     5.7 -apply (auto intro: summable_rabs summable_le simp add: sums_summable [THEN suminf_mult])
     5.8 +apply (auto intro: summable_rabs summable_le simp add: sums_summable [THEN suminf_mult2])
     5.9  done
    5.10  
    5.11  
    5.12 @@ -637,7 +637,6 @@
    5.13  apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
    5.14  done
    5.15  
    5.16 -
    5.17  lemma termdiffs: 
    5.18      "[| summable(%n. c(n) * (K ^ n));  
    5.19          summable(%n. (diffs c)(n) * (K ^ n));  
    5.20 @@ -657,7 +656,7 @@
    5.21  apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)
    5.22  apply (auto simp add: add_commute)
    5.23  apply (drule_tac x="(\<lambda>n. c n * (xa + x) ^ n)" in sums_diff, assumption) 
    5.24 -apply (drule_tac x = "(%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
    5.25 +apply (drule_tac f = "(%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
    5.26  apply (rule sums_unique)
    5.27  apply (simp add: diff_def divide_inverse add_ac mult_ac)
    5.28  apply (rule LIM_zero_cancel)
    5.29 @@ -680,17 +679,13 @@
    5.30  apply (frule_tac x = "(%n. c n * (xa + x) ^ n) " and y = "(%n. c n * x ^ n)" in sums_diff, assumption)
    5.31  apply (simp add: suminf_diff [OF sums_summable sums_summable] 
    5.32                 right_diff_distrib [symmetric])
    5.33 -apply (frule_tac x = "(%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult)
    5.34 -apply (simp add: sums_summable [THEN suminf_mult2])
    5.35 -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)
    5.36 -apply assumption
    5.37 -apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac)
    5.38 -apply (rule_tac f = suminf in arg_cong)
    5.39 -apply (rule ext)
    5.40 -apply (simp add: diff_def right_distrib add_ac mult_ac)
    5.41 +apply (subst suminf_diff)
    5.42 +apply (rule summable_mult2)
    5.43 +apply (erule sums_summable)
    5.44 +apply (erule sums_summable)
    5.45 +apply (simp add: ring_eq_simps)
    5.46  done
    5.47  
    5.48 -
    5.49  subsection{*Formal Derivatives of Exp, Sin, and Cos Series*} 
    5.50  
    5.51  lemma exp_fdiffs: 
     6.1 --- a/src/HOL/Real/RComplete.thy	Wed Jul 13 16:47:23 2005 +0200
     6.2 +++ b/src/HOL/Real/RComplete.thy	Wed Jul 13 19:49:07 2005 +0200
     6.3 @@ -1,9 +1,10 @@
     6.4  (*  Title       : RComplete.thy
     6.5      ID          : $Id$
     6.6      Author      : Jacques D. Fleuriot
     6.7 +                  Converted to Isar and polished by lcp
     6.8 +                  Most floor and ceiling lemmas by Jeremy Avigad
     6.9      Copyright   : 1998  University of Cambridge
    6.10      Copyright   : 2001,2002  University of Edinburgh
    6.11 -Converted to Isar and polished by lcp
    6.12  *) 
    6.13  
    6.14  header{*Completeness of the Reals; Floor and Ceiling Functions*}
    6.15 @@ -204,6 +205,37 @@
    6.16  apply (auto simp add: mult_assoc real_of_nat_def)
    6.17  done
    6.18  
    6.19 +lemma reals_Archimedean6:
    6.20 +     "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
    6.21 +apply (insert reals_Archimedean2 [of r], safe)
    6.22 +apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x"
    6.23 +       in ex_has_least_nat, auto)
    6.24 +apply (rule_tac x = x in exI)
    6.25 +apply (case_tac x, simp)
    6.26 +apply (rename_tac x')
    6.27 +apply (drule_tac x = x' in spec, simp)
    6.28 +done
    6.29 +
    6.30 +lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
    6.31 +by (drule reals_Archimedean6, auto)
    6.32 +
    6.33 +lemma reals_Archimedean_6b_int:
    6.34 +     "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
    6.35 +apply (drule reals_Archimedean6a, auto)
    6.36 +apply (rule_tac x = "int n" in exI)
    6.37 +apply (simp add: real_of_int_real_of_nat real_of_nat_Suc)
    6.38 +done
    6.39 +
    6.40 +lemma reals_Archimedean_6c_int:
    6.41 +     "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
    6.42 +apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto)
    6.43 +apply (rename_tac n)
    6.44 +apply (drule real_le_imp_less_or_eq, auto)
    6.45 +apply (rule_tac x = "- n - 1" in exI)
    6.46 +apply (rule_tac [2] x = "- n" in exI, auto)
    6.47 +done
    6.48 +
    6.49 +
    6.50  ML
    6.51  {*
    6.52  val real_sum_of_halves = thm "real_sum_of_halves";
    6.53 @@ -260,8 +292,9 @@
    6.54  by (simp add: linorder_not_less [symmetric])
    6.55  
    6.56  lemma floor_zero [simp]: "floor 0 = 0"
    6.57 -apply (simp add: floor_def)
    6.58 -apply (rule Least_equality, auto)
    6.59 +apply (simp add: floor_def del: real_of_int_add)
    6.60 +apply (rule Least_equality)
    6.61 +apply simp_all
    6.62  done
    6.63  
    6.64  lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
    6.65 @@ -279,7 +312,7 @@
    6.66  apply (simp only: floor_def)
    6.67  apply (rule Least_equality)
    6.68  apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    6.69 -apply (drule_tac [2] real_of_int_minus [THEN subst])
    6.70 +apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
    6.71  apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
    6.72  apply (simp_all add: real_of_int_real_of_nat)
    6.73  done
    6.74 @@ -294,41 +327,11 @@
    6.75  lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
    6.76  apply (simp only: floor_def)
    6.77  apply (rule Least_equality)
    6.78 -apply (drule_tac [2] real_of_int_minus [THEN subst])
    6.79 +apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
    6.80  apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    6.81  apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
    6.82  done
    6.83  
    6.84 -lemma reals_Archimedean6:
    6.85 -     "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
    6.86 -apply (insert reals_Archimedean2 [of r], safe)
    6.87 -apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x"
    6.88 -       in ex_has_least_nat, auto)
    6.89 -apply (rule_tac x = x in exI)
    6.90 -apply (case_tac x, simp)
    6.91 -apply (rename_tac x')
    6.92 -apply (drule_tac x = x' in spec, simp)
    6.93 -done
    6.94 -
    6.95 -lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
    6.96 -by (drule reals_Archimedean6, auto)
    6.97 -
    6.98 -lemma reals_Archimedean_6b_int:
    6.99 -     "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
   6.100 -apply (drule reals_Archimedean6a, auto)
   6.101 -apply (rule_tac x = "int n" in exI)
   6.102 -apply (simp add: real_of_int_real_of_nat real_of_nat_Suc)
   6.103 -done
   6.104 -
   6.105 -lemma reals_Archimedean_6c_int:
   6.106 -     "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
   6.107 -apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto)
   6.108 -apply (rename_tac n)
   6.109 -apply (drule real_le_imp_less_or_eq, auto)
   6.110 -apply (rule_tac x = "- n - 1" in exI)
   6.111 -apply (rule_tac [2] x = "- n" in exI, auto)
   6.112 -done
   6.113 -
   6.114  lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
   6.115  apply (case_tac "r < 0")
   6.116  apply (blast intro: reals_Archimedean_6c_int)
   6.117 @@ -349,19 +352,29 @@
   6.118  lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
   6.119  apply (simp add: floor_def Least_def)
   6.120  apply (insert real_lb_ub_int [of r], safe)
   6.121 -apply (rule theI2, auto)
   6.122 +apply (rule theI2)
   6.123 +apply auto
   6.124 +apply (subst int_le_real_less, simp)
   6.125 +apply (drule_tac x = n in spec)
   6.126 +apply auto
   6.127 +apply (subgoal_tac "n <= x")
   6.128 +apply simp
   6.129 +apply (subst int_le_real_less, simp)
   6.130  done
   6.131  
   6.132 -lemma floor_le: "x < y ==> floor x \<le> floor y"
   6.133 +lemma floor_mono: "x < y ==> floor x \<le> floor y"
   6.134  apply (simp add: floor_def Least_def)
   6.135  apply (insert real_lb_ub_int [of x])
   6.136  apply (insert real_lb_ub_int [of y], safe)
   6.137  apply (rule theI2)
   6.138 -apply (rule_tac [3] theI2, auto)
   6.139 +apply (rule_tac [3] theI2)
   6.140 +apply simp
   6.141 +apply (erule conjI)
   6.142 +apply (auto simp add: order_eq_iff int_le_real_less)
   6.143  done
   6.144  
   6.145 -lemma floor_le2: "x \<le> y ==> floor x \<le> floor y"
   6.146 -by (auto dest: real_le_imp_less_or_eq simp add: floor_le)
   6.147 +lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y"
   6.148 +by (auto dest: real_le_imp_less_or_eq simp add: floor_mono)
   6.149  
   6.150  lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
   6.151  by (auto intro: lemma_floor)
   6.152 @@ -371,7 +384,8 @@
   6.153  apply (simp add: floor_def Least_def)
   6.154  apply (insert real_lb_ub_int [of x], erule exE)
   6.155  apply (rule theI2)
   6.156 -apply (auto intro: lemma_floor)
   6.157 +apply (auto intro: lemma_floor) 
   6.158 +apply (auto simp add: order_eq_iff int_le_real_less)
   6.159  done
   6.160  
   6.161  lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
   6.162 @@ -403,11 +417,27 @@
   6.163  apply (rule floor_real_of_int)
   6.164  done
   6.165  
   6.166 +lemma floor_one [simp]: "floor 1 = 1"
   6.167 +  apply (rule trans)
   6.168 +  prefer 2
   6.169 +  apply (rule floor_real_of_int)
   6.170 +  apply simp
   6.171 +done
   6.172 +
   6.173  lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
   6.174  apply (simp add: floor_def Least_def)
   6.175  apply (insert real_lb_ub_int [of r], safe)
   6.176  apply (rule theI2)
   6.177  apply (auto intro: lemma_floor)
   6.178 +apply (auto simp add: order_eq_iff int_le_real_less)
   6.179 +done
   6.180 +
   6.181 +lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
   6.182 +apply (simp add: floor_def Least_def)
   6.183 +apply (insert real_lb_ub_int [of r], safe)
   6.184 +apply (rule theI2)
   6.185 +apply (auto intro: lemma_floor)
   6.186 +apply (auto simp add: order_eq_iff int_le_real_less)
   6.187  done
   6.188  
   6.189  lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
   6.190 @@ -415,8 +445,141 @@
   6.191  apply (auto simp del: real_of_int_floor_ge_diff_one)
   6.192  done
   6.193  
   6.194 +lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
   6.195 +apply (insert real_of_int_floor_gt_diff_one [of r])
   6.196 +apply (auto simp del: real_of_int_floor_gt_diff_one)
   6.197 +done
   6.198  
   6.199 -subsection{*Ceiling Function for Positive Reals*}
   6.200 +lemma le_floor: "real a <= x ==> a <= floor x"
   6.201 +  apply (subgoal_tac "a < floor x + 1")
   6.202 +  apply arith
   6.203 +  apply (subst real_of_int_less_iff [THEN sym])
   6.204 +  apply simp
   6.205 +  apply (insert real_of_int_floor_add_one_gt [of x]) 
   6.206 +  apply arith
   6.207 +done
   6.208 +
   6.209 +lemma real_le_floor: "a <= floor x ==> real a <= x"
   6.210 +  apply (rule order_trans)
   6.211 +  prefer 2
   6.212 +  apply (rule real_of_int_floor_le)
   6.213 +  apply (subst real_of_int_le_iff)
   6.214 +  apply assumption
   6.215 +done
   6.216 +
   6.217 +lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
   6.218 +  apply (rule iffI)
   6.219 +  apply (erule real_le_floor)
   6.220 +  apply (erule le_floor)
   6.221 +done
   6.222 +
   6.223 +lemma le_floor_eq_number_of [simp]: 
   6.224 +    "(number_of n <= floor x) = (number_of n <= x)"
   6.225 +by (simp add: le_floor_eq)
   6.226 +
   6.227 +lemma le_floor_eq_zero [simp]: "(0 <= floor x) = (0 <= x)"
   6.228 +by (simp add: le_floor_eq)
   6.229 +
   6.230 +lemma le_floor_eq_one [simp]: "(1 <= floor x) = (1 <= x)"
   6.231 +by (simp add: le_floor_eq)
   6.232 +
   6.233 +lemma floor_less_eq: "(floor x < a) = (x < real a)"
   6.234 +  apply (subst linorder_not_le [THEN sym])+
   6.235 +  apply simp
   6.236 +  apply (rule le_floor_eq)
   6.237 +done
   6.238 +
   6.239 +lemma floor_less_eq_number_of [simp]: 
   6.240 +    "(floor x < number_of n) = (x < number_of n)"
   6.241 +by (simp add: floor_less_eq)
   6.242 +
   6.243 +lemma floor_less_eq_zero [simp]: "(floor x < 0) = (x < 0)"
   6.244 +by (simp add: floor_less_eq)
   6.245 +
   6.246 +lemma floor_less_eq_one [simp]: "(floor x < 1) = (x < 1)"
   6.247 +by (simp add: floor_less_eq)
   6.248 +
   6.249 +lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
   6.250 +  apply (insert le_floor_eq [of "a + 1" x])
   6.251 +  apply auto
   6.252 +done
   6.253 +
   6.254 +lemma less_floor_eq_number_of [simp]: 
   6.255 +    "(number_of n < floor x) = (number_of n + 1 <= x)"
   6.256 +by (simp add: less_floor_eq)
   6.257 +
   6.258 +lemma less_floor_eq_zero [simp]: "(0 < floor x) = (1 <= x)"
   6.259 +by (simp add: less_floor_eq)
   6.260 +
   6.261 +lemma less_floor_eq_one [simp]: "(1 < floor x) = (2 <= x)"
   6.262 +by (simp add: less_floor_eq)
   6.263 +
   6.264 +lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
   6.265 +  apply (insert floor_less_eq [of x "a + 1"])
   6.266 +  apply auto
   6.267 +done
   6.268 +
   6.269 +lemma floor_le_eq_number_of [simp]: 
   6.270 +    "(floor x <= number_of n) = (x < number_of n + 1)"
   6.271 +by (simp add: floor_le_eq)
   6.272 +
   6.273 +lemma floor_le_eq_zero [simp]: "(floor x <= 0) = (x < 1)"
   6.274 +by (simp add: floor_le_eq)
   6.275 +
   6.276 +lemma floor_le_eq_one [simp]: "(floor x <= 1) = (x < 2)"
   6.277 +by (simp add: floor_le_eq)
   6.278 +
   6.279 +lemma floor_add [simp]: "floor (x + real a) = floor x + a"
   6.280 +  apply (subst order_eq_iff)
   6.281 +  apply (rule conjI)
   6.282 +  prefer 2
   6.283 +  apply (subgoal_tac "floor x + a < floor (x + real a) + 1")
   6.284 +  apply arith
   6.285 +  apply (subst real_of_int_less_iff [THEN sym])
   6.286 +  apply simp
   6.287 +  apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1")
   6.288 +  apply (subgoal_tac "real (floor x) <= x")
   6.289 +  apply arith
   6.290 +  apply (rule real_of_int_floor_le)
   6.291 +  apply (rule real_of_int_floor_add_one_gt)
   6.292 +  apply (subgoal_tac "floor (x + real a) < floor x + a + 1")
   6.293 +  apply arith
   6.294 +  apply (subst real_of_int_less_iff [THEN sym])  
   6.295 +  apply simp
   6.296 +  apply (subgoal_tac "real(floor(x + real a)) <= x + real a") 
   6.297 +  apply (subgoal_tac "x < real(floor x) + 1")
   6.298 +  apply arith
   6.299 +  apply (rule real_of_int_floor_add_one_gt)
   6.300 +  apply (rule real_of_int_floor_le)
   6.301 +done
   6.302 +
   6.303 +lemma floor_add_number_of [simp]: 
   6.304 +    "floor (x + number_of n) = floor x + number_of n"
   6.305 +  apply (subst floor_add [THEN sym])
   6.306 +  apply simp
   6.307 +done
   6.308 +
   6.309 +lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
   6.310 +  apply (subst floor_add [THEN sym])
   6.311 +  apply simp
   6.312 +done
   6.313 +
   6.314 +lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
   6.315 +  apply (subst diff_minus)+
   6.316 +  apply (subst real_of_int_minus [THEN sym])
   6.317 +  apply (rule floor_add)
   6.318 +done
   6.319 +
   6.320 +lemma floor_subtract_number_of [simp]: "floor (x - number_of n) = 
   6.321 +    floor x - number_of n"
   6.322 +  apply (subst floor_subtract [THEN sym])
   6.323 +  apply simp
   6.324 +done
   6.325 +
   6.326 +lemma floor_subtract_one [simp]: "floor (x - 1) = floor x - 1"
   6.327 +  apply (subst floor_subtract [THEN sym])
   6.328 +  apply simp
   6.329 +done
   6.330  
   6.331  lemma ceiling_zero [simp]: "ceiling 0 = 0"
   6.332  by (simp add: ceiling_def)
   6.333 @@ -438,11 +601,11 @@
   6.334  apply (subst le_minus_iff, simp)
   6.335  done
   6.336  
   6.337 -lemma ceiling_le: "x < y ==> ceiling x \<le> ceiling y"
   6.338 -by (simp add: floor_le ceiling_def)
   6.339 +lemma ceiling_mono: "x < y ==> ceiling x \<le> ceiling y"
   6.340 +by (simp add: floor_mono ceiling_def)
   6.341  
   6.342 -lemma ceiling_le2: "x \<le> y ==> ceiling x \<le> ceiling y"
   6.343 -by (simp add: floor_le2 ceiling_def)
   6.344 +lemma ceiling_mono2: "x \<le> y ==> ceiling x \<le> ceiling y"
   6.345 +by (simp add: floor_mono2 ceiling_def)
   6.346  
   6.347  lemma real_of_int_ceiling_cancel [simp]:
   6.348       "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
   6.349 @@ -472,6 +635,9 @@
   6.350  apply (rule ceiling_real_of_int)
   6.351  done
   6.352  
   6.353 +lemma ceiling_one [simp]: "ceiling 1 = 1"
   6.354 +  by (unfold ceiling_def, simp)
   6.355 +
   6.356  lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
   6.357  apply (rule neg_le_iff_le [THEN iffD1])
   6.358  apply (simp add: ceiling_def diff_minus)
   6.359 @@ -482,6 +648,473 @@
   6.360  apply (simp del: real_of_int_ceiling_diff_one_le)
   6.361  done
   6.362  
   6.363 +lemma ceiling_le: "x <= real a ==> ceiling x <= a"
   6.364 +  apply (unfold ceiling_def)
   6.365 +  apply (subgoal_tac "-a <= floor(- x)")
   6.366 +  apply simp
   6.367 +  apply (rule le_floor)
   6.368 +  apply simp
   6.369 +done
   6.370 +
   6.371 +lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
   6.372 +  apply (unfold ceiling_def)
   6.373 +  apply (subgoal_tac "real(- a) <= - x")
   6.374 +  apply simp
   6.375 +  apply (rule real_le_floor)
   6.376 +  apply simp
   6.377 +done
   6.378 +
   6.379 +lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
   6.380 +  apply (rule iffI)
   6.381 +  apply (erule ceiling_le_real)
   6.382 +  apply (erule ceiling_le)
   6.383 +done
   6.384 +
   6.385 +lemma ceiling_le_eq_number_of [simp]: 
   6.386 +    "(ceiling x <= number_of n) = (x <= number_of n)"
   6.387 +by (simp add: ceiling_le_eq)
   6.388 +
   6.389 +lemma ceiling_le_zero_eq [simp]: "(ceiling x <= 0) = (x <= 0)" 
   6.390 +by (simp add: ceiling_le_eq)
   6.391 +
   6.392 +lemma ceiling_le_eq_one [simp]: "(ceiling x <= 1) = (x <= 1)" 
   6.393 +by (simp add: ceiling_le_eq)
   6.394 +
   6.395 +lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
   6.396 +  apply (subst linorder_not_le [THEN sym])+
   6.397 +  apply simp
   6.398 +  apply (rule ceiling_le_eq)
   6.399 +done
   6.400 +
   6.401 +lemma less_ceiling_eq_number_of [simp]: 
   6.402 +    "(number_of n < ceiling x) = (number_of n < x)"
   6.403 +by (simp add: less_ceiling_eq)
   6.404 +
   6.405 +lemma less_ceiling_eq_zero [simp]: "(0 < ceiling x) = (0 < x)"
   6.406 +by (simp add: less_ceiling_eq)
   6.407 +
   6.408 +lemma less_ceiling_eq_one [simp]: "(1 < ceiling x) = (1 < x)"
   6.409 +by (simp add: less_ceiling_eq)
   6.410 +
   6.411 +lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
   6.412 +  apply (insert ceiling_le_eq [of x "a - 1"])
   6.413 +  apply auto
   6.414 +done
   6.415 +
   6.416 +lemma ceiling_less_eq_number_of [simp]: 
   6.417 +    "(ceiling x < number_of n) = (x <= number_of n - 1)"
   6.418 +by (simp add: ceiling_less_eq)
   6.419 +
   6.420 +lemma ceiling_less_eq_zero [simp]: "(ceiling x < 0) = (x <= -1)"
   6.421 +by (simp add: ceiling_less_eq)
   6.422 +
   6.423 +lemma ceiling_less_eq_one [simp]: "(ceiling x < 1) = (x <= 0)"
   6.424 +by (simp add: ceiling_less_eq)
   6.425 +
   6.426 +lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
   6.427 +  apply (insert less_ceiling_eq [of "a - 1" x])
   6.428 +  apply auto
   6.429 +done
   6.430 +
   6.431 +lemma le_ceiling_eq_number_of [simp]: 
   6.432 +    "(number_of n <= ceiling x) = (number_of n - 1 < x)"
   6.433 +by (simp add: le_ceiling_eq)
   6.434 +
   6.435 +lemma le_ceiling_eq_zero [simp]: "(0 <= ceiling x) = (-1 < x)"
   6.436 +by (simp add: le_ceiling_eq)
   6.437 +
   6.438 +lemma le_ceiling_eq_one [simp]: "(1 <= ceiling x) = (0 < x)"
   6.439 +by (simp add: le_ceiling_eq)
   6.440 +
   6.441 +lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
   6.442 +  apply (unfold ceiling_def, simp)
   6.443 +  apply (subst real_of_int_minus [THEN sym])
   6.444 +  apply (subst floor_add)
   6.445 +  apply simp
   6.446 +done
   6.447 +
   6.448 +lemma ceiling_add_number_of [simp]: "ceiling (x + number_of n) = 
   6.449 +    ceiling x + number_of n"
   6.450 +  apply (subst ceiling_add [THEN sym])
   6.451 +  apply simp
   6.452 +done
   6.453 +
   6.454 +lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
   6.455 +  apply (subst ceiling_add [THEN sym])
   6.456 +  apply simp
   6.457 +done
   6.458 +
   6.459 +lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
   6.460 +  apply (subst diff_minus)+
   6.461 +  apply (subst real_of_int_minus [THEN sym])
   6.462 +  apply (rule ceiling_add)
   6.463 +done
   6.464 +
   6.465 +lemma ceiling_subtract_number_of [simp]: "ceiling (x - number_of n) = 
   6.466 +    ceiling x - number_of n"
   6.467 +  apply (subst ceiling_subtract [THEN sym])
   6.468 +  apply simp
   6.469 +done
   6.470 +
   6.471 +lemma ceiling_subtract_one [simp]: "ceiling (x - 1) = ceiling x - 1"
   6.472 +  apply (subst ceiling_subtract [THEN sym])
   6.473 +  apply simp
   6.474 +done
   6.475 +
   6.476 +subsection {* Versions for the natural numbers *}
   6.477 +
   6.478 +constdefs
   6.479 +  natfloor :: "real => nat"
   6.480 +  "natfloor x == nat(floor x)"
   6.481 +  natceiling :: "real => nat"
   6.482 +  "natceiling x == nat(ceiling x)"
   6.483 +
   6.484 +lemma natfloor_zero [simp]: "natfloor 0 = 0"
   6.485 +  by (unfold natfloor_def, simp)
   6.486 +
   6.487 +lemma natfloor_one [simp]: "natfloor 1 = 1"
   6.488 +  by (unfold natfloor_def, simp)
   6.489 +
   6.490 +lemma zero_le_natfloor [simp]: "0 <= natfloor x"
   6.491 +  by (unfold natfloor_def, simp)
   6.492 +
   6.493 +lemma natfloor_number_of_eq [simp]: "natfloor (number_of n) = number_of n"
   6.494 +  by (unfold natfloor_def, simp)
   6.495 +
   6.496 +lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
   6.497 +  by (unfold natfloor_def, simp)
   6.498 +
   6.499 +lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
   6.500 +  by (unfold natfloor_def, simp)
   6.501 +
   6.502 +lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
   6.503 +  apply (unfold natfloor_def)
   6.504 +  apply (subgoal_tac "floor x <= floor 0")
   6.505 +  apply simp
   6.506 +  apply (erule floor_mono2)
   6.507 +done
   6.508 +
   6.509 +lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
   6.510 +  apply (case_tac "0 <= x")
   6.511 +  apply (subst natfloor_def)+
   6.512 +  apply (subst nat_le_eq_zle)
   6.513 +  apply force
   6.514 +  apply (erule floor_mono2) 
   6.515 +  apply (subst natfloor_neg)
   6.516 +  apply simp
   6.517 +  apply simp
   6.518 +done
   6.519 +
   6.520 +lemma le_natfloor: "real x <= a ==> x <= natfloor a"
   6.521 +  apply (unfold natfloor_def)
   6.522 +  apply (subst nat_int [THEN sym])
   6.523 +  apply (subst nat_le_eq_zle)
   6.524 +  apply simp
   6.525 +  apply (rule le_floor)
   6.526 +  apply simp
   6.527 +done
   6.528 +
   6.529 +lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
   6.530 +  apply (rule iffI)
   6.531 +  apply (rule order_trans)
   6.532 +  prefer 2
   6.533 +  apply (erule real_natfloor_le)
   6.534 +  apply (subst real_of_nat_le_iff)
   6.535 +  apply assumption
   6.536 +  apply (erule le_natfloor)
   6.537 +done
   6.538 +
   6.539 +lemma le_natfloor_eq_number_of [simp]: 
   6.540 +    "~ neg((number_of n)::int) ==> 0 <= x ==>
   6.541 +      (number_of n <= natfloor x) = (number_of n <= x)"
   6.542 +  apply (subst le_natfloor_eq, assumption)
   6.543 +  apply simp
   6.544 +done
   6.545 +
   6.546 +lemma le_natfloor_one_eq [simp]: "(1 <= natfloor x) = (1 <= x)"
   6.547 +  apply (case_tac "0 <= x")
   6.548 +  apply (subst le_natfloor_eq, assumption, simp)
   6.549 +  apply (rule iffI)
   6.550 +  apply (subgoal_tac "natfloor x <= natfloor 0") 
   6.551 +  apply simp
   6.552 +  apply (rule natfloor_mono)
   6.553 +  apply simp
   6.554 +  apply simp
   6.555 +done
   6.556 +
   6.557 +lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
   6.558 +  apply (unfold natfloor_def)
   6.559 +  apply (subst nat_int [THEN sym]);back;
   6.560 +  apply (subst eq_nat_nat_iff)
   6.561 +  apply simp
   6.562 +  apply simp
   6.563 +  apply (rule floor_eq2)
   6.564 +  apply auto
   6.565 +done
   6.566 +
   6.567 +lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
   6.568 +  apply (case_tac "0 <= x")
   6.569 +  apply (unfold natfloor_def)
   6.570 +  apply simp
   6.571 +  apply simp_all
   6.572 +done
   6.573 +
   6.574 +lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
   6.575 +  apply (simp add: compare_rls)
   6.576 +  apply (rule real_natfloor_add_one_gt)
   6.577 +done
   6.578 +
   6.579 +lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
   6.580 +  apply (subgoal_tac "z < real(natfloor z) + 1")
   6.581 +  apply arith
   6.582 +  apply (rule real_natfloor_add_one_gt)
   6.583 +done
   6.584 +
   6.585 +lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
   6.586 +  apply (unfold natfloor_def)
   6.587 +  apply (subgoal_tac "real a = real (int a)")
   6.588 +  apply (erule ssubst)
   6.589 +  apply (simp add: nat_add_distrib)
   6.590 +  apply simp
   6.591 +done
   6.592 +
   6.593 +lemma natfloor_add_number_of [simp]: 
   6.594 +    "~neg ((number_of n)::int) ==> 0 <= x ==> 
   6.595 +      natfloor (x + number_of n) = natfloor x + number_of n"
   6.596 +  apply (subst natfloor_add [THEN sym])
   6.597 +  apply simp_all
   6.598 +done
   6.599 +
   6.600 +lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
   6.601 +  apply (subst natfloor_add [THEN sym])
   6.602 +  apply assumption
   6.603 +  apply simp
   6.604 +done
   6.605 +
   6.606 +lemma natfloor_subtract [simp]: "real a <= x ==> 
   6.607 +    natfloor(x - real a) = natfloor x - a"
   6.608 +  apply (unfold natfloor_def)
   6.609 +  apply (subgoal_tac "real a = real (int a)")
   6.610 +  apply (erule ssubst)
   6.611 +  apply simp
   6.612 +  apply (subst nat_diff_distrib)
   6.613 +  apply simp
   6.614 +  apply (rule le_floor)
   6.615 +  apply simp_all
   6.616 +done
   6.617 +
   6.618 +lemma natceiling_zero [simp]: "natceiling 0 = 0"
   6.619 +  by (unfold natceiling_def, simp)
   6.620 +
   6.621 +lemma natceiling_one [simp]: "natceiling 1 = 1"
   6.622 +  by (unfold natceiling_def, simp)
   6.623 +
   6.624 +lemma zero_le_natceiling [simp]: "0 <= natceiling x"
   6.625 +  by (unfold natceiling_def, simp)
   6.626 +
   6.627 +lemma natceiling_number_of_eq [simp]: "natceiling (number_of n) = number_of n"
   6.628 +  by (unfold natceiling_def, simp)
   6.629 +
   6.630 +lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
   6.631 +  by (unfold natceiling_def, simp)
   6.632 +
   6.633 +lemma real_natceiling_ge: "x <= real(natceiling x)"
   6.634 +  apply (unfold natceiling_def)
   6.635 +  apply (case_tac "x < 0")
   6.636 +  apply simp
   6.637 +  apply (subst real_nat_eq_real)
   6.638 +  apply (subgoal_tac "ceiling 0 <= ceiling x")
   6.639 +  apply simp
   6.640 +  apply (rule ceiling_mono2)
   6.641 +  apply simp
   6.642 +  apply simp
   6.643 +done
   6.644 +
   6.645 +lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
   6.646 +  apply (unfold natceiling_def)
   6.647 +  apply simp
   6.648 +done
   6.649 +
   6.650 +lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
   6.651 +  apply (case_tac "0 <= x")
   6.652 +  apply (subst natceiling_def)+
   6.653 +  apply (subst nat_le_eq_zle)
   6.654 +  apply (rule disjI2)
   6.655 +  apply (subgoal_tac "real (0::int) <= real(ceiling y)")
   6.656 +  apply simp
   6.657 +  apply (rule order_trans)
   6.658 +  apply simp
   6.659 +  apply (erule order_trans)
   6.660 +  apply simp
   6.661 +  apply (erule ceiling_mono2)
   6.662 +  apply (subst natceiling_neg)
   6.663 +  apply simp_all
   6.664 +done
   6.665 +
   6.666 +lemma natceiling_le: "x <= real a ==> natceiling x <= a"
   6.667 +  apply (unfold natceiling_def)
   6.668 +  apply (case_tac "x < 0")
   6.669 +  apply simp
   6.670 +  apply (subst nat_int [THEN sym]);back;
   6.671 +  apply (subst nat_le_eq_zle)
   6.672 +  apply simp
   6.673 +  apply (rule ceiling_le)
   6.674 +  apply simp
   6.675 +done
   6.676 +
   6.677 +lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"
   6.678 +  apply (rule iffI)
   6.679 +  apply (rule order_trans)
   6.680 +  apply (rule real_natceiling_ge)
   6.681 +  apply (subst real_of_nat_le_iff)
   6.682 +  apply assumption
   6.683 +  apply (erule natceiling_le)
   6.684 +done
   6.685 +
   6.686 +lemma natceiling_le_eq2 [simp]: "~ neg((number_of n)::int) ==> 0 <= x ==>
   6.687 +    (natceiling x <= number_of n) = (x <= number_of n)"
   6.688 +  apply (subst natceiling_le_eq, assumption)
   6.689 +  apply simp
   6.690 +done
   6.691 +
   6.692 +lemma natceiling_one_le_eq: "(natceiling x <= 1) = (x <= 1)"
   6.693 +  apply (case_tac "0 <= x")
   6.694 +  apply (subst natceiling_le_eq)
   6.695 +  apply assumption
   6.696 +  apply simp
   6.697 +  apply (subst natceiling_neg)
   6.698 +  apply simp
   6.699 +  apply simp
   6.700 +done
   6.701 +
   6.702 +lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
   6.703 +  apply (unfold natceiling_def)
   6.704 +  apply (subst nat_int [THEN sym]);back;
   6.705 +  apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)")
   6.706 +  apply (erule ssubst)
   6.707 +  apply (subst eq_nat_nat_iff)
   6.708 +  apply (subgoal_tac "ceiling 0 <= ceiling x")
   6.709 +  apply simp
   6.710 +  apply (rule ceiling_mono2)
   6.711 +  apply force
   6.712 +  apply force
   6.713 +  apply (rule ceiling_eq2)
   6.714 +  apply (simp, simp)
   6.715 +  apply (subst nat_add_distrib)
   6.716 +  apply auto
   6.717 +done
   6.718 +
   6.719 +lemma natceiling_add [simp]: "0 <= x ==> 
   6.720 +    natceiling (x + real a) = natceiling x + a"
   6.721 +  apply (unfold natceiling_def)
   6.722 +  apply (subgoal_tac "real a = real (int a)")
   6.723 +  apply (erule ssubst)
   6.724 +  apply simp
   6.725 +  apply (subst nat_add_distrib)
   6.726 +  apply (subgoal_tac "0 = ceiling 0")
   6.727 +  apply (erule ssubst)
   6.728 +  apply (erule ceiling_mono2)
   6.729 +  apply simp_all
   6.730 +done
   6.731 +
   6.732 +lemma natceiling_add2 [simp]: "~ neg ((number_of n)::int) ==> 0 <= x ==> 
   6.733 +    natceiling (x + number_of n) = natceiling x + number_of n"
   6.734 +  apply (subst natceiling_add [THEN sym])
   6.735 +  apply simp_all
   6.736 +done
   6.737 +
   6.738 +lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
   6.739 +  apply (subst natceiling_add [THEN sym])
   6.740 +  apply assumption
   6.741 +  apply simp
   6.742 +done
   6.743 +
   6.744 +lemma natceiling_subtract [simp]: "real a <= x ==> 
   6.745 +    natceiling(x - real a) = natceiling x - a"
   6.746 +  apply (unfold natceiling_def)
   6.747 +  apply (subgoal_tac "real a = real (int a)")
   6.748 +  apply (erule ssubst)
   6.749 +  apply simp
   6.750 +  apply (subst nat_diff_distrib)
   6.751 +  apply simp
   6.752 +  apply (rule order_trans)
   6.753 +  prefer 2
   6.754 +  apply (rule ceiling_mono2)
   6.755 +  apply assumption
   6.756 +  apply simp_all
   6.757 +done
   6.758 +
   6.759 +lemma natfloor_div_nat: "1 <= x ==> 0 < y ==> 
   6.760 +  natfloor (x / real y) = natfloor x div y"
   6.761 +proof -
   6.762 +  assume "1 <= (x::real)" and "0 < (y::nat)"
   6.763 +  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
   6.764 +    by simp
   6.765 +  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y + 
   6.766 +    real((natfloor x) mod y)"
   6.767 +    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
   6.768 +  have "x = real(natfloor x) + (x - real(natfloor x))"
   6.769 +    by simp
   6.770 +  then have "x = real ((natfloor x) div y) * real y + 
   6.771 +      real((natfloor x) mod y) + (x - real(natfloor x))"
   6.772 +    by (simp add: a)
   6.773 +  then have "x / real y = ... / real y"
   6.774 +    by simp
   6.775 +  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / 
   6.776 +    real y + (x - real(natfloor x)) / real y"
   6.777 +    by (auto simp add: ring_distrib ring_eq_simps add_divide_distrib
   6.778 +      diff_divide_distrib prems)
   6.779 +  finally have "natfloor (x / real y) = natfloor(...)" by simp
   6.780 +  also have "... = natfloor(real((natfloor x) mod y) / 
   6.781 +    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
   6.782 +    by (simp add: add_ac)
   6.783 +  also have "... = natfloor(real((natfloor x) mod y) / 
   6.784 +    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
   6.785 +    apply (rule natfloor_add)
   6.786 +    apply (rule add_nonneg_nonneg)
   6.787 +    apply (rule divide_nonneg_pos)
   6.788 +    apply simp
   6.789 +    apply (simp add: prems)
   6.790 +    apply (rule divide_nonneg_pos)
   6.791 +    apply (simp add: compare_rls)
   6.792 +    apply (rule real_natfloor_le)
   6.793 +    apply (insert prems, auto)
   6.794 +    done
   6.795 +  also have "natfloor(real((natfloor x) mod y) / 
   6.796 +    real y + (x - real(natfloor x)) / real y) = 0"
   6.797 +    apply (rule natfloor_eq)
   6.798 +    apply simp
   6.799 +    apply (rule add_nonneg_nonneg)
   6.800 +    apply (rule divide_nonneg_pos)
   6.801 +    apply force
   6.802 +    apply (force simp add: prems)
   6.803 +    apply (rule divide_nonneg_pos)
   6.804 +    apply (simp add: compare_rls)
   6.805 +    apply (rule real_natfloor_le)
   6.806 +    apply (auto simp add: prems)
   6.807 +    apply (insert prems, arith)
   6.808 +    apply (simp add: add_divide_distrib [THEN sym])
   6.809 +    apply (subgoal_tac "real y = real y - 1 + 1")
   6.810 +    apply (erule ssubst)
   6.811 +    apply (rule add_le_less_mono)
   6.812 +    apply (simp add: compare_rls)
   6.813 +    apply (subgoal_tac "real(natfloor x mod y) + 1 = 
   6.814 +      real(natfloor x mod y + 1)")
   6.815 +    apply (erule ssubst)
   6.816 +    apply (subst real_of_nat_le_iff)
   6.817 +    apply (subgoal_tac "natfloor x mod y < y")
   6.818 +    apply arith
   6.819 +    apply (rule mod_less_divisor)
   6.820 +    apply assumption
   6.821 +    apply auto
   6.822 +    apply (simp add: compare_rls)
   6.823 +    apply (subst add_commute)
   6.824 +    apply (rule real_natfloor_add_one_gt)
   6.825 +    done
   6.826 +  finally show ?thesis
   6.827 +    by simp
   6.828 +qed
   6.829 +
   6.830  ML
   6.831  {*
   6.832  val number_of_less_real_of_int_iff = thm "number_of_less_real_of_int_iff";
   6.833 @@ -501,8 +1134,9 @@
   6.834  val real_lb_ub_int = thm "real_lb_ub_int";
   6.835  val lemma_floor = thm "lemma_floor";
   6.836  val real_of_int_floor_le = thm "real_of_int_floor_le";
   6.837 -val floor_le = thm "floor_le";
   6.838 +(*val floor_le = thm "floor_le";
   6.839  val floor_le2 = thm "floor_le2";
   6.840 +*)
   6.841  val lemma_floor2 = thm "lemma_floor2";
   6.842  val real_of_int_floor_cancel = thm "real_of_int_floor_cancel";
   6.843  val floor_eq = thm "floor_eq";
   6.844 @@ -518,8 +1152,10 @@
   6.845  val ceiling_floor = thm "ceiling_floor";
   6.846  val floor_ceiling = thm "floor_ceiling";
   6.847  val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge";
   6.848 +(*
   6.849  val ceiling_le = thm "ceiling_le";
   6.850  val ceiling_le2 = thm "ceiling_le2";
   6.851 +*)
   6.852  val real_of_int_ceiling_cancel = thm "real_of_int_ceiling_cancel";
   6.853  val ceiling_eq = thm "ceiling_eq";
   6.854  val ceiling_eq2 = thm "ceiling_eq2";
     7.1 --- a/src/HOL/Real/RealDef.thy	Wed Jul 13 16:47:23 2005 +0200
     7.2 +++ b/src/HOL/Real/RealDef.thy	Wed Jul 13 19:49:07 2005 +0200
     7.3 @@ -3,6 +3,7 @@
     7.4      Author      : Jacques D. Fleuriot
     7.5      Copyright   : 1998  University of Cambridge
     7.6      Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     7.7 +    Additional contributions by Jeremy Avigad
     7.8  *)
     7.9  
    7.10  header{*Defining the Reals from the Positive Reals*}
    7.11 @@ -635,27 +636,46 @@
    7.12    real_of_nat_def: "real z == of_nat z"
    7.13    real_of_int_def: "real z == of_int z"
    7.14  
    7.15 +lemma real_eq_of_nat: "real = of_nat"
    7.16 +  apply (rule ext)
    7.17 +  apply (unfold real_of_nat_def)
    7.18 +  apply (rule refl)
    7.19 +  done
    7.20 +
    7.21 +lemma real_eq_of_int: "real = of_int"
    7.22 +  apply (rule ext)
    7.23 +  apply (unfold real_of_int_def)
    7.24 +  apply (rule refl)
    7.25 +  done
    7.26 +
    7.27  lemma real_of_int_zero [simp]: "real (0::int) = 0"  
    7.28  by (simp add: real_of_int_def) 
    7.29  
    7.30  lemma real_of_one [simp]: "real (1::int) = (1::real)"
    7.31  by (simp add: real_of_int_def) 
    7.32  
    7.33 -lemma real_of_int_add: "real (x::int) + real y = real (x + y)"
    7.34 +lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y"
    7.35  by (simp add: real_of_int_def) 
    7.36 -declare real_of_int_add [symmetric, simp]
    7.37  
    7.38 -lemma real_of_int_minus: "-real (x::int) = real (-x)"
    7.39 +lemma real_of_int_minus [simp]: "real(-x) = -real (x::int)"
    7.40  by (simp add: real_of_int_def) 
    7.41 -declare real_of_int_minus [symmetric, simp]
    7.42 +
    7.43 +lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y"
    7.44 +by (simp add: real_of_int_def) 
    7.45  
    7.46 -lemma real_of_int_diff: "real (x::int) - real y = real (x - y)"
    7.47 +lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"
    7.48  by (simp add: real_of_int_def) 
    7.49 -declare real_of_int_diff [symmetric, simp]
    7.50  
    7.51 -lemma real_of_int_mult: "real (x::int) * real y = real (x * y)"
    7.52 -by (simp add: real_of_int_def) 
    7.53 -declare real_of_int_mult [symmetric, simp]
    7.54 +lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))"
    7.55 +  apply (subst real_eq_of_int)+
    7.56 +  apply (rule of_int_setsum)
    7.57 +done
    7.58 +
    7.59 +lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) = 
    7.60 +    (PROD x:A. real(f x))"
    7.61 +  apply (subst real_eq_of_int)+
    7.62 +  apply (rule of_int_setprod)
    7.63 +done
    7.64  
    7.65  lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = (0::int))"
    7.66  by (simp add: real_of_int_def) 
    7.67 @@ -669,6 +689,91 @@
    7.68  lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)"
    7.69  by (simp add: real_of_int_def) 
    7.70  
    7.71 +lemma real_of_int_gt_zero_cancel_iff [simp]: "(0 < real (n::int)) = (0 < n)"
    7.72 +by (simp add: real_of_int_def) 
    7.73 +
    7.74 +lemma real_of_int_ge_zero_cancel_iff [simp]: "(0 <= real (n::int)) = (0 <= n)"
    7.75 +by (simp add: real_of_int_def) 
    7.76 +
    7.77 +lemma real_of_int_lt_zero_cancel_iff [simp]: "(real (n::int) < 0) = (n < 0)"
    7.78 +by (simp add: real_of_int_def)
    7.79 +
    7.80 +lemma real_of_int_le_zero_cancel_iff [simp]: "(real (n::int) <= 0) = (n <= 0)"
    7.81 +by (simp add: real_of_int_def)
    7.82 +
    7.83 +lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)"
    7.84 +  apply (subgoal_tac "real n + 1 = real (n + 1)")
    7.85 +  apply (simp del: real_of_int_add)
    7.86 +  apply auto
    7.87 +done
    7.88 +
    7.89 +lemma int_le_real_less: "((n::int) <= m) = (real n < real m + 1)"
    7.90 +  apply (subgoal_tac "real m + 1 = real (m + 1)")
    7.91 +  apply (simp del: real_of_int_add)
    7.92 +  apply simp
    7.93 +done
    7.94 +
    7.95 +lemma real_of_int_div_aux: "d ~= 0 ==> (real (x::int)) / (real d) = 
    7.96 +    real (x div d) + (real (x mod d)) / (real d)"
    7.97 +proof -
    7.98 +  assume "d ~= 0"
    7.99 +  have "x = (x div d) * d + x mod d"
   7.100 +    by auto
   7.101 +  then have "real x = real (x div d) * real d + real(x mod d)"
   7.102 +    by (simp only: real_of_int_mult [THEN sym] real_of_int_add [THEN sym])
   7.103 +  then have "real x / real d = ... / real d"
   7.104 +    by simp
   7.105 +  then show ?thesis
   7.106 +    by (auto simp add: add_divide_distrib ring_eq_simps prems)
   7.107 +qed
   7.108 +
   7.109 +lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
   7.110 +    real(n div d) = real n / real d"
   7.111 +  apply (frule real_of_int_div_aux [of d n])
   7.112 +  apply simp
   7.113 +  apply (simp add: zdvd_iff_zmod_eq_0)
   7.114 +done
   7.115 +
   7.116 +lemma real_of_int_div2:
   7.117 +  "0 <= real (n::int) / real (x) - real (n div x)"
   7.118 +  apply (case_tac "x = 0")
   7.119 +  apply simp
   7.120 +  apply (case_tac "0 < x")
   7.121 +  apply (simp add: compare_rls)
   7.122 +  apply (subst real_of_int_div_aux)
   7.123 +  apply simp
   7.124 +  apply simp
   7.125 +  apply (subst zero_le_divide_iff)
   7.126 +  apply auto
   7.127 +  apply (simp add: compare_rls)
   7.128 +  apply (subst real_of_int_div_aux)
   7.129 +  apply simp
   7.130 +  apply simp
   7.131 +  apply (subst zero_le_divide_iff)
   7.132 +  apply auto
   7.133 +done
   7.134 +
   7.135 +lemma real_of_int_div3:
   7.136 +  "real (n::int) / real (x) - real (n div x) <= 1"
   7.137 +  apply(case_tac "x = 0")
   7.138 +  apply simp
   7.139 +  apply (simp add: compare_rls)
   7.140 +  apply (subst real_of_int_div_aux)
   7.141 +  apply assumption
   7.142 +  apply simp
   7.143 +  apply (subst divide_le_eq)
   7.144 +  apply clarsimp
   7.145 +  apply (rule conjI)
   7.146 +  apply (rule impI)
   7.147 +  apply (rule order_less_imp_le)
   7.148 +  apply simp
   7.149 +  apply (rule impI)
   7.150 +  apply (rule order_less_imp_le)
   7.151 +  apply simp
   7.152 +done
   7.153 +
   7.154 +lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" 
   7.155 +  by (insert real_of_int_div2 [of n x], simp)
   7.156  
   7.157  subsection{*Embedding the Naturals into the Reals*}
   7.158  
   7.159 @@ -701,6 +806,24 @@
   7.160  lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
   7.161  by (simp add: real_of_nat_def)
   7.162  
   7.163 +lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = 
   7.164 +    (SUM x:A. real(f x))"
   7.165 +  apply (subst real_eq_of_nat)+
   7.166 +  apply (rule of_nat_setsum)
   7.167 +done
   7.168 +
   7.169 +lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) = 
   7.170 +    (PROD x:A. real(f x))"
   7.171 +  apply (subst real_eq_of_nat)+
   7.172 +  apply (rule of_nat_setprod)
   7.173 +done
   7.174 +
   7.175 +lemma real_of_card: "real (card A) = setsum (%x.1) A"
   7.176 +  apply (subst card_eq_setsum)
   7.177 +  apply (subst real_of_nat_setsum)
   7.178 +  apply simp
   7.179 +done
   7.180 +
   7.181  lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
   7.182  by (simp add: real_of_nat_def)
   7.183  
   7.184 @@ -722,13 +845,76 @@
   7.185  lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat)) = (0 \<le> n)"
   7.186  by (simp add: add: real_of_nat_def)
   7.187  
   7.188 +lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
   7.189 +  apply (subgoal_tac "real n + 1 = real (Suc n)")
   7.190 +  apply simp
   7.191 +  apply (auto simp add: real_of_nat_Suc)
   7.192 +done
   7.193 +
   7.194 +lemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)"
   7.195 +  apply (subgoal_tac "real m + 1 = real (Suc m)")
   7.196 +  apply (simp add: less_Suc_eq_le)
   7.197 +  apply (simp add: real_of_nat_Suc)
   7.198 +done
   7.199 +
   7.200 +lemma real_of_nat_div_aux: "0 < d ==> (real (x::nat)) / (real d) = 
   7.201 +    real (x div d) + (real (x mod d)) / (real d)"
   7.202 +proof -
   7.203 +  assume "0 < d"
   7.204 +  have "x = (x div d) * d + x mod d"
   7.205 +    by auto
   7.206 +  then have "real x = real (x div d) * real d + real(x mod d)"
   7.207 +    by (simp only: real_of_nat_mult [THEN sym] real_of_nat_add [THEN sym])
   7.208 +  then have "real x / real d = \<dots> / real d"
   7.209 +    by simp
   7.210 +  then show ?thesis
   7.211 +    by (auto simp add: add_divide_distrib ring_eq_simps prems)
   7.212 +qed
   7.213 +
   7.214 +lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==>
   7.215 +    real(n div d) = real n / real d"
   7.216 +  apply (frule real_of_nat_div_aux [of d n])
   7.217 +  apply simp
   7.218 +  apply (subst dvd_eq_mod_eq_0 [THEN sym])
   7.219 +  apply assumption
   7.220 +done
   7.221 +
   7.222 +lemma real_of_nat_div2:
   7.223 +  "0 <= real (n::nat) / real (x) - real (n div x)"
   7.224 +  apply(case_tac "x = 0")
   7.225 +  apply simp
   7.226 +  apply (simp add: compare_rls)
   7.227 +  apply (subst real_of_nat_div_aux)
   7.228 +  apply assumption
   7.229 +  apply simp
   7.230 +  apply (subst zero_le_divide_iff)
   7.231 +  apply simp
   7.232 +done
   7.233 +
   7.234 +lemma real_of_nat_div3:
   7.235 +  "real (n::nat) / real (x) - real (n div x) <= 1"
   7.236 +  apply(case_tac "x = 0")
   7.237 +  apply simp
   7.238 +  apply (simp add: compare_rls)
   7.239 +  apply (subst real_of_nat_div_aux)
   7.240 +  apply assumption
   7.241 +  apply simp
   7.242 +done
   7.243 +
   7.244 +lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" 
   7.245 +  by (insert real_of_nat_div2 [of n x], simp)
   7.246 +
   7.247  lemma real_of_int_real_of_nat: "real (int n) = real n"
   7.248  by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat)
   7.249  
   7.250  lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
   7.251  by (simp add: real_of_int_def real_of_nat_def)
   7.252  
   7.253 -
   7.254 +lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x"
   7.255 +  apply (subgoal_tac "real(int(nat x)) = real(nat x)")
   7.256 +  apply force
   7.257 +  apply (simp only: real_of_int_real_of_nat)
   7.258 +done
   7.259  
   7.260  subsection{*Numerals and Arithmetic*}
   7.261