src/HOL/RComplete.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47108 2a1953f0d20d
child 47596 c031e65c8ddc
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30122
1c912a9d8200 standard headers;
wenzelm
parents: 30102
diff changeset
     1
(*  Title:      HOL/RComplete.thy
1c912a9d8200 standard headers;
wenzelm
parents: 30102
diff changeset
     2
    Author:     Jacques D. Fleuriot, University of Edinburgh
1c912a9d8200 standard headers;
wenzelm
parents: 30102
diff changeset
     3
    Author:     Larry Paulson, University of Cambridge
1c912a9d8200 standard headers;
wenzelm
parents: 30102
diff changeset
     4
    Author:     Jeremy Avigad, Carnegie Mellon University
1c912a9d8200 standard headers;
wenzelm
parents: 30102
diff changeset
     5
    Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
     6
*)
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     7
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
     8
header {* Completeness of the Reals; Floor and Ceiling Functions *}
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
     9
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14641
diff changeset
    10
theory RComplete
15140
322485b816ac import -> imports
nipkow
parents: 15131
diff changeset
    11
imports Lubs RealDef
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14641
diff changeset
    12
begin
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    13
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    14
lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    15
  by simp
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    16
32707
836ec9d0a0c8 New lemmas involving the real numbers, especially limits and series
paulson
parents: 30242
diff changeset
    17
lemma abs_diff_less_iff:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 32960
diff changeset
    18
  "(\<bar>x - a\<bar> < (r::'a::linordered_idom)) = (a - r < x \<and> x < a + r)"
32707
836ec9d0a0c8 New lemmas involving the real numbers, especially limits and series
paulson
parents: 30242
diff changeset
    19
  by auto
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    20
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    21
subsection {* Completeness of Positive Reals *}
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    22
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    23
text {*
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    24
  Supremum property for the set of positive reals
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    25
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    26
  Let @{text "P"} be a non-empty set of positive reals, with an upper
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    27
  bound @{text "y"}.  Then @{text "P"} has a least upper bound
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    28
  (written @{text "S"}).
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    29
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    30
  FIXME: Can the premise be weakened to @{text "\<forall>x \<in> P. x\<le> y"}?
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    31
*}
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    32
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    33
text {* Only used in HOL/Import/HOL4Compat.thy; delete? *}
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    34
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    35
lemma posreal_complete:
44690
b6d8b11ed399 remove unused assumption from lemma posreal_complete
huffman
parents: 44679
diff changeset
    36
  fixes P :: "real set"
b6d8b11ed399 remove unused assumption from lemma posreal_complete
huffman
parents: 44679
diff changeset
    37
  assumes not_empty_P: "\<exists>x. x \<in> P"
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    38
    and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y"
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    39
  shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    40
proof -
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    41
  from upper_bound_Ex have "\<exists>z. \<forall>x\<in>P. x \<le> z"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    42
    by (auto intro: less_imp_le)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    43
  from complete_real [OF not_empty_P this] obtain S
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    44
  where S1: "\<And>x. x \<in> P \<Longrightarrow> x \<le> S" and S2: "\<And>z. \<forall>x\<in>P. x \<le> z \<Longrightarrow> S \<le> z" by fast
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    45
  have "\<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    46
  proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    47
    fix y show "(\<exists>x\<in>P. y < x) = (y < S)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    48
      apply (cases "\<exists>x\<in>P. y < x", simp_all)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    49
      apply (clarify, drule S1, simp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    50
      apply (simp add: not_less S2)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    51
      done
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    52
  qed
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    53
  thus ?thesis ..
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    54
qed
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    55
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    56
text {*
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    57
  \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    58
*}
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    59
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    60
lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)"
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    61
  apply (frule isLub_isUb)
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    62
  apply (frule_tac x = y in isLub_isUb)
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    63
  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    64
  done
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    65
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    66
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    67
text {*
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    68
  \medskip reals Completeness (again!)
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    69
*}
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    70
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    71
lemma reals_complete:
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    72
  assumes notempty_S: "\<exists>X. X \<in> S"
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    73
    and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y"
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    74
  shows "\<exists>t. isLub (UNIV :: real set) S t"
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    75
proof -
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    76
  from assms have "\<exists>X. X \<in> S" and "\<exists>Y. \<forall>x\<in>S. x \<le> Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    77
    unfolding isUb_def setle_def by simp_all
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    78
  from complete_real [OF this] show ?thesis
45966
03ce2b2a29a2 tuned proofs
haftmann
parents: 44708
diff changeset
    79
    by (simp add: isLub_def leastP_def isUb_def setle_def setge_def)
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    80
qed
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    81
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    82
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    83
subsection {* The Archimedean Property of the Reals *}
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    84
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    85
theorem reals_Archimedean:
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    86
  assumes x_pos: "0 < x"
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    87
  shows "\<exists>n. inverse (real (Suc n)) < x"
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    88
  unfolding real_of_nat_def using x_pos
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    89
  by (rule ex_inverse_of_nat_Suc_less)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    90
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    91
lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)"
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 35578
diff changeset
    92
  unfolding real_of_nat_def by (rule ex_less_of_nat)
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
    93
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    94
lemma reals_Archimedean3:
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    95
  assumes x_greater_zero: "0 < x"
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
    96
  shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
    97
  unfolding real_of_nat_def using `0 < x`
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
    98
  by (auto intro: ex_less_of_nat_mult)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
    99
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   100
28091
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   101
subsection{*Density of the Rational Reals in the Reals*}
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   102
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   103
text{* This density proof is due to Stefan Richter and was ported by TN.  The
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   104
original source is \emph{Real Analysis} by H.L. Royden.
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   105
It employs the Archimedean property of the reals. *}
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   106
44668
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   107
lemma Rats_dense_in_real:
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   108
  fixes x :: real
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   109
  assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
28091
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   110
proof -
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   111
  from `x<y` have "0 < y-x" by simp
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   112
  with reals_Archimedean obtain q::nat 
44668
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   113
    where q: "inverse (real q) < y-x" and "0 < q" by auto
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   114
  def p \<equiv> "ceiling (y * real q) - 1"
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   115
  def r \<equiv> "of_int p / real q"
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   116
  from q have "x < y - inverse (real q)" by simp
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   117
  also have "y - inverse (real q) \<le> r"
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   118
    unfolding r_def p_def
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   119
    by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling `0 < q`)
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   120
  finally have "x < r" .
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   121
  moreover have "r < y"
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   122
    unfolding r_def p_def
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   123
    by (simp add: divide_less_eq diff_less_eq `0 < q`
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   124
      less_ceiling_iff [symmetric])
31d41a0f6b5d simplify proof of Rats_dense_in_real;
huffman
parents: 44667
diff changeset
   125
  moreover from r_def have "r \<in> \<rat>" by simp
28091
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   126
  ultimately show ?thesis by fast
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   127
qed
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   128
50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents: 27435
diff changeset
   129
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   130
subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   131
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   132
(* FIXME: theorems for negative numerals *)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   133
lemma numeral_less_real_of_int_iff [simp]:
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   134
     "((numeral n) < real (m::int)) = (numeral n < m)"
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   135
apply auto
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   136
apply (rule real_of_int_less_iff [THEN iffD1])
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   137
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   138
done
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   139
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   140
lemma numeral_less_real_of_int_iff2 [simp]:
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   141
     "(real (m::int) < (numeral n)) = (m < numeral n)"
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   142
apply auto
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   143
apply (rule real_of_int_less_iff [THEN iffD1])
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   144
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   145
done
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   146
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   147
lemma numeral_le_real_of_int_iff [simp]:
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   148
     "((numeral n) \<le> real (m::int)) = (numeral n \<le> m)"
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   149
by (simp add: linorder_not_less [symmetric])
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   150
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   151
lemma numeral_le_real_of_int_iff2 [simp]:
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   152
     "(real (m::int) \<le> (numeral n)) = (m \<le> numeral n)"
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   153
by (simp add: linorder_not_less [symmetric])
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   154
24355
93d78fdeb55a remove int_of_nat
huffman
parents: 23477
diff changeset
   155
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   156
unfolding real_of_nat_def by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   157
24355
93d78fdeb55a remove int_of_nat
huffman
parents: 23477
diff changeset
   158
lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
30102
799b687e4aac disable floor_minus and ceiling_minus [simp]
huffman
parents: 30097
diff changeset
   159
unfolding real_of_nat_def by (simp add: floor_minus)
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   160
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   161
lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   162
unfolding real_of_int_def by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   163
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   164
lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
30102
799b687e4aac disable floor_minus and ceiling_minus [simp]
huffman
parents: 30097
diff changeset
   165
unfolding real_of_int_def by (simp add: floor_minus)
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   166
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   167
lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   168
unfolding real_of_int_def by (rule floor_exists)
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   169
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   170
lemma lemma_floor:
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   171
  assumes a1: "real m \<le> r" and a2: "r < real n + 1"
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   172
  shows "m \<le> (n::int)"
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   173
proof -
23389
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 23309
diff changeset
   174
  have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 23309
diff changeset
   175
  also have "... = real (n + 1)" by simp
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 23309
diff changeset
   176
  finally have "m < n + 1" by (simp only: real_of_int_less_iff)
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   177
  thus ?thesis by arith
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   178
qed
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   179
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   180
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   181
unfolding real_of_int_def by (rule of_int_floor_le)
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   182
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   183
lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   184
by (auto intro: lemma_floor)
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   185
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   186
lemma real_of_int_floor_cancel [simp]:
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   187
    "(real (floor x) = x) = (\<exists>n::int. x = real n)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   188
  using floor_real_of_int by metis
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   189
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   190
lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   191
  unfolding real_of_int_def using floor_unique [of n x] by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   192
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   193
lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   194
  unfolding real_of_int_def by (rule floor_unique)
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   195
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   196
lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   197
apply (rule inj_int [THEN injD])
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   198
apply (simp add: real_of_nat_Suc)
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15234
diff changeset
   199
apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   200
done
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   201
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   202
lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   203
apply (drule order_le_imp_less_or_eq)
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   204
apply (auto intro: floor_eq3)
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   205
done
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   206
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   207
lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   208
  unfolding real_of_int_def using floor_correct [of r] by simp
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   209
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   210
lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   211
  unfolding real_of_int_def using floor_correct [of r] by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   212
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   213
lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   214
  unfolding real_of_int_def using floor_correct [of r] by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   215
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   216
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   217
  unfolding real_of_int_def using floor_correct [of r] by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   218
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   219
lemma le_floor: "real a <= x ==> a <= floor x"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   220
  unfolding real_of_int_def by (simp add: le_floor_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   221
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   222
lemma real_le_floor: "a <= floor x ==> real a <= x"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   223
  unfolding real_of_int_def by (simp add: le_floor_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   224
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   225
lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   226
  unfolding real_of_int_def by (rule le_floor_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   227
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   228
lemma floor_less_eq: "(floor x < a) = (x < real a)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   229
  unfolding real_of_int_def by (rule floor_less_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   230
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   231
lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   232
  unfolding real_of_int_def by (rule less_floor_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   233
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   234
lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   235
  unfolding real_of_int_def by (rule floor_le_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   236
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   237
lemma floor_add [simp]: "floor (x + real a) = floor x + a"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   238
  unfolding real_of_int_def by (rule floor_add_of_int)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   239
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   240
lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   241
  unfolding real_of_int_def by (rule floor_diff_of_int)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   242
35578
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   243
lemma le_mult_floor:
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   244
  assumes "0 \<le> (a :: real)" and "0 \<le> b"
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   245
  shows "floor a * floor b \<le> floor (a * b)"
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   246
proof -
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   247
  have "real (floor a) \<le> a"
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   248
    and "real (floor b) \<le> b" by auto
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   249
  hence "real (floor a * floor b) \<le> a * b"
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   250
    using assms by (auto intro!: mult_mono)
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   251
  also have "a * b < real (floor (a * b) + 1)" by auto
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   252
  finally show ?thesis unfolding real_of_int_less_iff by simp
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   253
qed
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   254
24355
93d78fdeb55a remove int_of_nat
huffman
parents: 23477
diff changeset
   255
lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   256
  unfolding real_of_nat_def by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   257
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   258
lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   259
  unfolding real_of_int_def by (rule le_of_int_ceiling)
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   260
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   261
lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   262
  unfolding real_of_int_def by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   263
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   264
lemma real_of_int_ceiling_cancel [simp]:
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   265
     "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   266
  using ceiling_real_of_int by metis
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   267
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   268
lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   269
  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   270
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   271
lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   272
  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   273
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   274
lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   275
  unfolding real_of_int_def using ceiling_unique [of n x] by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   276
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   277
lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   278
  unfolding real_of_int_def using ceiling_correct [of r] by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   279
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   280
lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   281
  unfolding real_of_int_def using ceiling_correct [of r] by simp
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14476
diff changeset
   282
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   283
lemma ceiling_le: "x <= real a ==> ceiling x <= a"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   284
  unfolding real_of_int_def by (simp add: ceiling_le_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   285
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   286
lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   287
  unfolding real_of_int_def by (simp add: ceiling_le_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   288
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   289
lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   290
  unfolding real_of_int_def by (rule ceiling_le_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   291
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   292
lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   293
  unfolding real_of_int_def by (rule less_ceiling_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   294
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   295
lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   296
  unfolding real_of_int_def by (rule ceiling_less_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   297
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   298
lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   299
  unfolding real_of_int_def by (rule le_ceiling_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   300
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   301
lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   302
  unfolding real_of_int_def by (rule ceiling_add_of_int)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   303
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   304
lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
30097
57df8626c23b generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents: 29667
diff changeset
   305
  unfolding real_of_int_def by (rule ceiling_diff_of_int)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   306
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   307
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   308
subsection {* Versions for the natural numbers *}
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   309
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16893
diff changeset
   310
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   311
  natfloor :: "real => nat" where
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16893
diff changeset
   312
  "natfloor x = nat(floor x)"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   313
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   314
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   315
  natceiling :: "real => nat" where
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16893
diff changeset
   316
  "natceiling x = nat(ceiling x)"
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   317
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   318
lemma natfloor_zero [simp]: "natfloor 0 = 0"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   319
  by (unfold natfloor_def, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   320
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   321
lemma natfloor_one [simp]: "natfloor 1 = 1"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   322
  by (unfold natfloor_def, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   323
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   324
lemma zero_le_natfloor [simp]: "0 <= natfloor x"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   325
  by (unfold natfloor_def, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   326
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   327
lemma natfloor_numeral_eq [simp]: "natfloor (numeral n) = numeral n"
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   328
  by (unfold natfloor_def, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   329
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   330
lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   331
  by (unfold natfloor_def, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   332
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   333
lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   334
  by (unfold natfloor_def, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   335
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   336
lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   337
  unfolding natfloor_def by simp
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   338
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   339
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   340
  unfolding natfloor_def by (intro nat_mono floor_mono)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   341
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   342
lemma le_natfloor: "real x <= a ==> x <= natfloor a"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   343
  apply (unfold natfloor_def)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   344
  apply (subst nat_int [THEN sym])
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   345
  apply (rule nat_mono)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   346
  apply (rule le_floor)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   347
  apply simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   348
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   349
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   350
lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n"
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   351
  unfolding natfloor_def real_of_nat_def
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   352
  by (simp add: nat_less_iff floor_less_iff)
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   353
35578
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   354
lemma less_natfloor:
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   355
  assumes "0 \<le> x" and "x < real (n :: nat)"
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   356
  shows "natfloor x < n"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   357
  using assms by (simp add: natfloor_less_iff)
35578
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   358
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   359
lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   360
  apply (rule iffI)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   361
  apply (rule order_trans)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   362
  prefer 2
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   363
  apply (erule real_natfloor_le)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   364
  apply (subst real_of_nat_le_iff)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   365
  apply assumption
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   366
  apply (erule le_natfloor)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   367
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   368
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   369
lemma le_natfloor_eq_numeral [simp]:
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   370
    "~ neg((numeral n)::int) ==> 0 <= x ==>
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   371
      (numeral n <= natfloor x) = (numeral n <= x)"
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   372
  apply (subst le_natfloor_eq, assumption)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   373
  apply simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   374
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   375
16820
5c9d597e4cb9 fixed typos in theorem names
avigad
parents: 16819
diff changeset
   376
lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   377
  apply (case_tac "0 <= x")
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   378
  apply (subst le_natfloor_eq, assumption, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   379
  apply (rule iffI)
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
   380
  apply (subgoal_tac "natfloor x <= natfloor 0")
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   381
  apply simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   382
  apply (rule natfloor_mono)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   383
  apply simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   384
  apply simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   385
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   386
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   387
lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   388
  unfolding natfloor_def by (simp add: floor_eq2 [where n="int n"])
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   389
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   390
lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   391
  apply (case_tac "0 <= x")
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   392
  apply (unfold natfloor_def)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   393
  apply simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   394
  apply simp_all
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   395
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   396
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   397
lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 28952
diff changeset
   398
using real_natfloor_add_one_gt by (simp add: algebra_simps)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   399
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   400
lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   401
  apply (subgoal_tac "z < real(natfloor z) + 1")
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   402
  apply arith
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   403
  apply (rule real_natfloor_add_one_gt)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   404
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   405
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   406
lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   407
  unfolding natfloor_def
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   408
  unfolding real_of_int_of_nat_eq [symmetric] floor_add
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   409
  by (simp add: nat_add_distrib)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   410
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   411
lemma natfloor_add_numeral [simp]:
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   412
    "~neg ((numeral n)::int) ==> 0 <= x ==>
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   413
      natfloor (x + numeral n) = natfloor x + numeral n"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   414
  by (simp add: natfloor_add [symmetric])
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   415
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   416
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   417
  by (simp add: natfloor_add [symmetric] del: One_nat_def)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   418
46671
3a40ea076230 removing unnecessary assumptions in RComplete;
bulwahn
parents: 45966
diff changeset
   419
lemma natfloor_subtract [simp]:
3a40ea076230 removing unnecessary assumptions in RComplete;
bulwahn
parents: 45966
diff changeset
   420
    "natfloor(x - real a) = natfloor x - a"
3a40ea076230 removing unnecessary assumptions in RComplete;
bulwahn
parents: 45966
diff changeset
   421
  unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   422
  by simp
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   423
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 37887
diff changeset
   424
lemma natfloor_div_nat:
efa734d9b221 eliminated global prems;
wenzelm
parents: 37887
diff changeset
   425
  assumes "1 <= x" and "y > 0"
efa734d9b221 eliminated global prems;
wenzelm
parents: 37887
diff changeset
   426
  shows "natfloor (x / real y) = natfloor x div y"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   427
proof (rule natfloor_eq)
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   428
  have "(natfloor x) div y * y \<le> natfloor x"
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   429
    by (rule add_leD1 [where k="natfloor x mod y"], simp)
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   430
  thus "real (natfloor x div y) \<le> x / real y"
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   431
    using assms by (simp add: le_divide_eq le_natfloor_eq)
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   432
  have "natfloor x < (natfloor x) div y * y + y"
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   433
    apply (subst mod_div_equality [symmetric])
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   434
    apply (rule add_strict_left_mono)
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   435
    apply (rule mod_less_divisor)
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   436
    apply fact
35578
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   437
    done
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   438
  thus "x / real y < real (natfloor x div y) + 1"
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   439
    using assms
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   440
    by (simp add: divide_less_eq natfloor_less_iff left_distrib)
35578
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   441
qed
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   442
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   443
lemma le_mult_natfloor:
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   444
  shows "natfloor a * natfloor b \<le> natfloor (a * b)"
46671
3a40ea076230 removing unnecessary assumptions in RComplete;
bulwahn
parents: 45966
diff changeset
   445
  by (cases "0 <= a & 0 <= b")
3a40ea076230 removing unnecessary assumptions in RComplete;
bulwahn
parents: 45966
diff changeset
   446
    (auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)
35578
384ad08a1d1b Added natfloor and floor rules for multiplication and power.
hoelzl
parents: 35028
diff changeset
   447
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   448
lemma natceiling_zero [simp]: "natceiling 0 = 0"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   449
  by (unfold natceiling_def, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   450
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   451
lemma natceiling_one [simp]: "natceiling 1 = 1"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   452
  by (unfold natceiling_def, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   453
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   454
lemma zero_le_natceiling [simp]: "0 <= natceiling x"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   455
  by (unfold natceiling_def, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   456
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   457
lemma natceiling_numeral_eq [simp]: "natceiling (numeral n) = numeral n"
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   458
  by (unfold natceiling_def, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   459
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   460
lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   461
  by (unfold natceiling_def, simp)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   462
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   463
lemma real_natceiling_ge: "x <= real(natceiling x)"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   464
  unfolding natceiling_def by (cases "x < 0", simp_all)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   465
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   466
lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   467
  unfolding natceiling_def by simp
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   468
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   469
lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   470
  unfolding natceiling_def by (intro nat_mono ceiling_mono)
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   471
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   472
lemma natceiling_le: "x <= real a ==> natceiling x <= a"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   473
  unfolding natceiling_def real_of_nat_def
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   474
  by (simp add: nat_le_iff ceiling_le_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   475
44708
37ce74ff4203 remove unused assumptions from natceiling lemmas
huffman
parents: 44707
diff changeset
   476
lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
37ce74ff4203 remove unused assumptions from natceiling lemmas
huffman
parents: 44707
diff changeset
   477
  unfolding natceiling_def real_of_nat_def
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   478
  by (simp add: nat_le_iff ceiling_le_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   479
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   480
lemma natceiling_le_eq_numeral [simp]:
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   481
    "~ neg((numeral n)::int) ==>
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   482
      (natceiling x <= numeral n) = (x <= numeral n)"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   483
  by (simp add: natceiling_le_eq)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   484
16820
5c9d597e4cb9 fixed typos in theorem names
avigad
parents: 16819
diff changeset
   485
lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   486
  unfolding natceiling_def
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   487
  by (simp add: nat_le_iff ceiling_le_iff)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   488
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   489
lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   490
  unfolding natceiling_def
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   491
  by (simp add: ceiling_eq2 [where n="int n"])
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   492
16893
0cc94e6f6ae5 some structured proofs on completeness;
wenzelm
parents: 16827
diff changeset
   493
lemma natceiling_add [simp]: "0 <= x ==>
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   494
    natceiling (x + real a) = natceiling x + a"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   495
  unfolding natceiling_def
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   496
  unfolding real_of_int_of_nat_eq [symmetric] ceiling_add
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   497
  by (simp add: nat_add_distrib)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   498
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   499
lemma natceiling_add_numeral [simp]:
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   500
    "~ neg ((numeral n)::int) ==> 0 <= x ==>
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46671
diff changeset
   501
      natceiling (x + numeral n) = natceiling x + numeral n"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   502
  by (simp add: natceiling_add [symmetric])
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   503
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   504
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   505
  by (simp add: natceiling_add [symmetric] del: One_nat_def)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   506
46671
3a40ea076230 removing unnecessary assumptions in RComplete;
bulwahn
parents: 45966
diff changeset
   507
lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
3a40ea076230 removing unnecessary assumptions in RComplete;
bulwahn
parents: 45966
diff changeset
   508
  unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
44679
a89d0ad8ed20 shorten some proofs
huffman
parents: 44678
diff changeset
   509
  by simp
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   510
36826
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   511
subsection {* Exponentiation with floor *}
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   512
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   513
lemma floor_power:
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   514
  assumes "x = real (floor x)"
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   515
  shows "floor (x ^ n) = floor x ^ n"
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   516
proof -
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   517
  have *: "x ^ n = real (floor x ^ n)"
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   518
    using assms by (induct n arbitrary: x) simp_all
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   519
  show ?thesis unfolding real_of_int_inject[symmetric]
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   520
    unfolding * floor_real_of_int ..
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   521
qed
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   522
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   523
lemma natfloor_power:
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   524
  assumes "x = real (natfloor x)"
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   525
  shows "natfloor (x ^ n) = natfloor x ^ n"
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   526
proof -
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   527
  from assms have "0 \<le> floor x" by auto
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   528
  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   529
  from floor_power[OF this]
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   530
  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   531
    by simp
4d4462d644ae move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents: 36795
diff changeset
   532
qed
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 15539
diff changeset
   533
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 9429
diff changeset
   534
end