--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Archimedean_Field.thy Wed Feb 25 11:30:46 2009 -0800
@@ -0,0 +1,400 @@
+(* Title: Archimedean_Field.thy
+ Author: Brian Huffman
+*)
+
+header {* Archimedean Fields, Floor and Ceiling Functions *}
+
+theory Archimedean_Field
+imports Main
+begin
+
+subsection {* Class of Archimedean fields *}
+
+text {* Archimedean fields have no infinite elements. *}
+
+class archimedean_field = ordered_field + number_ring +
+ assumes ex_le_of_int: "\<exists>z. x \<le> of_int z"
+
+lemma ex_less_of_int:
+ fixes x :: "'a::archimedean_field" shows "\<exists>z. x < of_int z"
+proof -
+ from ex_le_of_int obtain z where "x \<le> of_int z" ..
+ then have "x < of_int (z + 1)" by simp
+ then show ?thesis ..
+qed
+
+lemma ex_of_int_less:
+ fixes x :: "'a::archimedean_field" shows "\<exists>z. of_int z < x"
+proof -
+ from ex_less_of_int obtain z where "- x < of_int z" ..
+ then have "of_int (- z) < x" by simp
+ then show ?thesis ..
+qed
+
+lemma ex_less_of_nat:
+ fixes x :: "'a::archimedean_field" shows "\<exists>n. x < of_nat n"
+proof -
+ obtain z where "x < of_int z" using ex_less_of_int ..
+ also have "\<dots> \<le> of_int (int (nat z))" by simp
+ also have "\<dots> = of_nat (nat z)" by (simp only: of_int_of_nat_eq)
+ finally show ?thesis ..
+qed
+
+lemma ex_le_of_nat:
+ fixes x :: "'a::archimedean_field" shows "\<exists>n. x \<le> of_nat n"
+proof -
+ obtain n where "x < of_nat n" using ex_less_of_nat ..
+ then have "x \<le> of_nat n" by simp
+ then show ?thesis ..
+qed
+
+text {* Archimedean fields have no infinitesimal elements. *}
+
+lemma ex_inverse_of_nat_Suc_less:
+ fixes x :: "'a::archimedean_field"
+ assumes "0 < x" shows "\<exists>n. inverse (of_nat (Suc n)) < x"
+proof -
+ from `0 < x` have "0 < inverse x"
+ by (rule positive_imp_inverse_positive)
+ obtain n where "inverse x < of_nat n"
+ using ex_less_of_nat ..
+ then obtain m where "inverse x < of_nat (Suc m)"
+ using `0 < inverse x` by (cases n) (simp_all del: of_nat_Suc)
+ then have "inverse (of_nat (Suc m)) < inverse (inverse x)"
+ using `0 < inverse x` by (rule less_imp_inverse_less)
+ then have "inverse (of_nat (Suc m)) < x"
+ using `0 < x` by (simp add: nonzero_inverse_inverse_eq)
+ then show ?thesis ..
+qed
+
+lemma ex_inverse_of_nat_less:
+ fixes x :: "'a::archimedean_field"
+ assumes "0 < x" shows "\<exists>n>0. inverse (of_nat n) < x"
+ using ex_inverse_of_nat_Suc_less [OF `0 < x`] by auto
+
+lemma ex_less_of_nat_mult:
+ fixes x :: "'a::archimedean_field"
+ assumes "0 < x" shows "\<exists>n. y < of_nat n * x"
+proof -
+ obtain n where "y / x < of_nat n" using ex_less_of_nat ..
+ with `0 < x` have "y < of_nat n * x" by (simp add: pos_divide_less_eq)
+ then show ?thesis ..
+qed
+
+
+subsection {* Existence and uniqueness of floor function *}
+
+lemma exists_least_lemma:
+ assumes "\<not> P 0" and "\<exists>n. P n"
+ shows "\<exists>n. \<not> P n \<and> P (Suc n)"
+proof -
+ from `\<exists>n. P n` have "P (Least P)" by (rule LeastI_ex)
+ with `\<not> P 0` obtain n where "Least P = Suc n"
+ by (cases "Least P") auto
+ then have "n < Least P" by simp
+ then have "\<not> P n" by (rule not_less_Least)
+ then have "\<not> P n \<and> P (Suc n)"
+ using `P (Least P)` `Least P = Suc n` by simp
+ then show ?thesis ..
+qed
+
+lemma floor_exists:
+ fixes x :: "'a::archimedean_field"
+ shows "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)"
+proof (cases)
+ assume "0 \<le> x"
+ then have "\<not> x < of_nat 0" by simp
+ then have "\<exists>n. \<not> x < of_nat n \<and> x < of_nat (Suc n)"
+ using ex_less_of_nat by (rule exists_least_lemma)
+ then obtain n where "\<not> x < of_nat n \<and> x < of_nat (Suc n)" ..
+ then have "of_int (int n) \<le> x \<and> x < of_int (int n + 1)" by simp
+ then show ?thesis ..
+next
+ assume "\<not> 0 \<le> x"
+ then have "\<not> - x \<le> of_nat 0" by simp
+ then have "\<exists>n. \<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)"
+ using ex_le_of_nat by (rule exists_least_lemma)
+ then obtain n where "\<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" ..
+ then have "of_int (- int n - 1) \<le> x \<and> x < of_int (- int n - 1 + 1)" by simp
+ then show ?thesis ..
+qed
+
+lemma floor_exists1:
+ fixes x :: "'a::archimedean_field"
+ shows "\<exists>!z. of_int z \<le> x \<and> x < of_int (z + 1)"
+proof (rule ex_ex1I)
+ show "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)"
+ by (rule floor_exists)
+next
+ fix y z assume
+ "of_int y \<le> x \<and> x < of_int (y + 1)"
+ "of_int z \<le> x \<and> x < of_int (z + 1)"
+ then have
+ "of_int y \<le> x" "x < of_int (y + 1)"
+ "of_int z \<le> x" "x < of_int (z + 1)"
+ by simp_all
+ from le_less_trans [OF `of_int y \<le> x` `x < of_int (z + 1)`]
+ le_less_trans [OF `of_int z \<le> x` `x < of_int (y + 1)`]
+ show "y = z" by (simp del: of_int_add)
+qed
+
+
+subsection {* Floor function *}
+
+definition
+ floor :: "'a::archimedean_field \<Rightarrow> int" where
+ [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+
+notation (xsymbols)
+ floor ("\<lfloor>_\<rfloor>")
+
+notation (HTML output)
+ floor ("\<lfloor>_\<rfloor>")
+
+lemma floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
+ unfolding floor_def using floor_exists1 by (rule theI')
+
+lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
+ using floor_correct [of x] floor_exists1 [of x] by auto
+
+lemma of_int_floor_le: "of_int (floor x) \<le> x"
+ using floor_correct ..
+
+lemma le_floor_iff: "z \<le> floor x \<longleftrightarrow> of_int z \<le> x"
+proof
+ assume "z \<le> floor x"
+ then have "(of_int z :: 'a) \<le> of_int (floor x)" by simp
+ also have "of_int (floor x) \<le> x" by (rule of_int_floor_le)
+ finally show "of_int z \<le> x" .
+next
+ assume "of_int z \<le> x"
+ also have "x < of_int (floor x + 1)" using floor_correct ..
+ finally show "z \<le> floor x" by (simp del: of_int_add)
+qed
+
+lemma floor_less_iff: "floor x < z \<longleftrightarrow> x < of_int z"
+ by (simp add: not_le [symmetric] le_floor_iff)
+
+lemma less_floor_iff: "z < floor x \<longleftrightarrow> of_int z + 1 \<le> x"
+ using le_floor_iff [of "z + 1" x] by auto
+
+lemma floor_le_iff: "floor x \<le> z \<longleftrightarrow> x < of_int z + 1"
+ by (simp add: not_less [symmetric] less_floor_iff)
+
+lemma floor_mono: assumes "x \<le> y" shows "floor x \<le> floor y"
+proof -
+ have "of_int (floor x) \<le> x" by (rule of_int_floor_le)
+ also note `x \<le> y`
+ finally show ?thesis by (simp add: le_floor_iff)
+qed
+
+lemma floor_less_cancel: "floor x < floor y \<Longrightarrow> x < y"
+ by (auto simp add: not_le [symmetric] floor_mono)
+
+lemma floor_of_int [simp]: "floor (of_int z) = z"
+ by (rule floor_unique) simp_all
+
+lemma floor_of_nat [simp]: "floor (of_nat n) = int n"
+ using floor_of_int [of "of_nat n"] by simp
+
+text {* Floor with numerals *}
+
+lemma floor_zero [simp]: "floor 0 = 0"
+ using floor_of_int [of 0] by simp
+
+lemma floor_one [simp]: "floor 1 = 1"
+ using floor_of_int [of 1] by simp
+
+lemma floor_number_of [simp]: "floor (number_of v) = number_of v"
+ using floor_of_int [of "number_of v"] by simp
+
+lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x"
+ by (simp add: le_floor_iff)
+
+lemma one_le_floor [simp]: "1 \<le> floor x \<longleftrightarrow> 1 \<le> x"
+ by (simp add: le_floor_iff)
+
+lemma number_of_le_floor [simp]: "number_of v \<le> floor x \<longleftrightarrow> number_of v \<le> x"
+ by (simp add: le_floor_iff)
+
+lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x"
+ by (simp add: less_floor_iff)
+
+lemma one_less_floor [simp]: "1 < floor x \<longleftrightarrow> 2 \<le> x"
+ by (simp add: less_floor_iff)
+
+lemma number_of_less_floor [simp]:
+ "number_of v < floor x \<longleftrightarrow> number_of v + 1 \<le> x"
+ by (simp add: less_floor_iff)
+
+lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1"
+ by (simp add: floor_le_iff)
+
+lemma floor_le_one [simp]: "floor x \<le> 1 \<longleftrightarrow> x < 2"
+ by (simp add: floor_le_iff)
+
+lemma floor_le_number_of [simp]:
+ "floor x \<le> number_of v \<longleftrightarrow> x < number_of v + 1"
+ by (simp add: floor_le_iff)
+
+lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0"
+ by (simp add: floor_less_iff)
+
+lemma floor_less_one [simp]: "floor x < 1 \<longleftrightarrow> x < 1"
+ by (simp add: floor_less_iff)
+
+lemma floor_less_number_of [simp]:
+ "floor x < number_of v \<longleftrightarrow> x < number_of v"
+ by (simp add: floor_less_iff)
+
+text {* Addition and subtraction of integers *}
+
+lemma floor_add_of_int [simp]: "floor (x + of_int z) = floor x + z"
+ using floor_correct [of x] by (simp add: floor_unique)
+
+lemma floor_add_number_of [simp]:
+ "floor (x + number_of v) = floor x + number_of v"
+ using floor_add_of_int [of x "number_of v"] by simp
+
+lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
+ using floor_add_of_int [of x 1] by simp
+
+lemma floor_diff_of_int [simp]: "floor (x - of_int z) = floor x - z"
+ using floor_add_of_int [of x "- z"] by (simp add: algebra_simps)
+
+lemma floor_diff_number_of [simp]:
+ "floor (x - number_of v) = floor x - number_of v"
+ using floor_diff_of_int [of x "number_of v"] by simp
+
+lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
+ using floor_diff_of_int [of x 1] by simp
+
+
+subsection {* Ceiling function *}
+
+definition
+ ceiling :: "'a::archimedean_field \<Rightarrow> int" where
+ [code del]: "ceiling x = - floor (- x)"
+
+notation (xsymbols)
+ ceiling ("\<lceil>_\<rceil>")
+
+notation (HTML output)
+ ceiling ("\<lceil>_\<rceil>")
+
+lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)"
+ unfolding ceiling_def using floor_correct [of "- x"] by simp
+
+lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> ceiling x = z"
+ unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
+
+lemma le_of_int_ceiling: "x \<le> of_int (ceiling x)"
+ using ceiling_correct ..
+
+lemma ceiling_le_iff: "ceiling x \<le> z \<longleftrightarrow> x \<le> of_int z"
+ unfolding ceiling_def using le_floor_iff [of "- z" "- x"] by auto
+
+lemma less_ceiling_iff: "z < ceiling x \<longleftrightarrow> of_int z < x"
+ by (simp add: not_le [symmetric] ceiling_le_iff)
+
+lemma ceiling_less_iff: "ceiling x < z \<longleftrightarrow> x \<le> of_int z - 1"
+ using ceiling_le_iff [of x "z - 1"] by simp
+
+lemma le_ceiling_iff: "z \<le> ceiling x \<longleftrightarrow> of_int z - 1 < x"
+ by (simp add: not_less [symmetric] ceiling_less_iff)
+
+lemma ceiling_mono: "x \<ge> y \<Longrightarrow> ceiling x \<ge> ceiling y"
+ unfolding ceiling_def by (simp add: floor_mono)
+
+lemma ceiling_less_cancel: "ceiling x < ceiling y \<Longrightarrow> x < y"
+ by (auto simp add: not_le [symmetric] ceiling_mono)
+
+lemma ceiling_of_int [simp]: "ceiling (of_int z) = z"
+ by (rule ceiling_unique) simp_all
+
+lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n"
+ using ceiling_of_int [of "of_nat n"] by simp
+
+text {* Ceiling with numerals *}
+
+lemma ceiling_zero [simp]: "ceiling 0 = 0"
+ using ceiling_of_int [of 0] by simp
+
+lemma ceiling_one [simp]: "ceiling 1 = 1"
+ using ceiling_of_int [of 1] by simp
+
+lemma ceiling_number_of [simp]: "ceiling (number_of v) = number_of v"
+ using ceiling_of_int [of "number_of v"] by simp
+
+lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0"
+ by (simp add: ceiling_le_iff)
+
+lemma ceiling_le_one [simp]: "ceiling x \<le> 1 \<longleftrightarrow> x \<le> 1"
+ by (simp add: ceiling_le_iff)
+
+lemma ceiling_le_number_of [simp]:
+ "ceiling x \<le> number_of v \<longleftrightarrow> x \<le> number_of v"
+ by (simp add: ceiling_le_iff)
+
+lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1"
+ by (simp add: ceiling_less_iff)
+
+lemma ceiling_less_one [simp]: "ceiling x < 1 \<longleftrightarrow> x \<le> 0"
+ by (simp add: ceiling_less_iff)
+
+lemma ceiling_less_number_of [simp]:
+ "ceiling x < number_of v \<longleftrightarrow> x \<le> number_of v - 1"
+ by (simp add: ceiling_less_iff)
+
+lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x"
+ by (simp add: le_ceiling_iff)
+
+lemma one_le_ceiling [simp]: "1 \<le> ceiling x \<longleftrightarrow> 0 < x"
+ by (simp add: le_ceiling_iff)
+
+lemma number_of_le_ceiling [simp]:
+ "number_of v \<le> ceiling x\<longleftrightarrow> number_of v - 1 < x"
+ by (simp add: le_ceiling_iff)
+
+lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x"
+ by (simp add: less_ceiling_iff)
+
+lemma one_less_ceiling [simp]: "1 < ceiling x \<longleftrightarrow> 1 < x"
+ by (simp add: less_ceiling_iff)
+
+lemma number_of_less_ceiling [simp]:
+ "number_of v < ceiling x \<longleftrightarrow> number_of v < x"
+ by (simp add: less_ceiling_iff)
+
+text {* Addition and subtraction of integers *}
+
+lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z"
+ using ceiling_correct [of x] by (simp add: ceiling_unique)
+
+lemma ceiling_add_number_of [simp]:
+ "ceiling (x + number_of v) = ceiling x + number_of v"
+ using ceiling_add_of_int [of x "number_of v"] by simp
+
+lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
+ using ceiling_add_of_int [of x 1] by simp
+
+lemma ceiling_diff_of_int [simp]: "ceiling (x - of_int z) = ceiling x - z"
+ using ceiling_add_of_int [of x "- z"] by (simp add: algebra_simps)
+
+lemma ceiling_diff_number_of [simp]:
+ "ceiling (x - number_of v) = ceiling x - number_of v"
+ using ceiling_diff_of_int [of x "number_of v"] by simp
+
+lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
+ using ceiling_diff_of_int [of x 1] by simp
+
+
+subsection {* Negation *}
+
+lemma floor_minus [simp]: "floor (- x) = - ceiling x"
+ unfolding ceiling_def by simp
+
+lemma ceiling_minus [simp]: "ceiling (- x) = - floor x"
+ unfolding ceiling_def by simp
+
+end
--- a/src/HOL/Decision_Procs/MIR.thy Wed Feb 25 19:34:00 2009 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Wed Feb 25 11:30:46 2009 -0800
@@ -83,7 +83,7 @@
have "real (floor x) \<le> x" by simp
hence "real (floor x) < real (n + 1) " using ub by arith
hence "floor x < n+1" by simp
- moreover from lb have "n \<le> floor x" using floor_mono2[where x="real n" and y="x"]
+ moreover from lb have "n \<le> floor x" using floor_mono[where x="real n" and y="x"]
by simp ultimately show "floor x = n" by simp
qed
@@ -1775,11 +1775,11 @@
"(real (a::int) \<le> b) = (a \<le> floor b \<or> (a = floor b \<and> real (floor b) < b))"
proof( auto)
assume alb: "real a \<le> b" and agb: "\<not> a \<le> floor b"
- from alb have "floor (real a) \<le> floor b " by (simp only: floor_mono2)
+ from alb have "floor (real a) \<le> floor b " by (simp only: floor_mono)
hence "a \<le> floor b" by simp with agb show "False" by simp
next
assume alb: "a \<le> floor b"
- hence "real a \<le> real (floor b)" by (simp only: floor_mono2)
+ hence "real a \<le> real (floor b)" by (simp only: floor_mono)
also have "\<dots>\<le> b" by simp finally show "real a \<le> b" .
qed
@@ -3697,7 +3697,7 @@
assumes xb: "real m \<le> x \<and> x < real ((n::int) + 1)"
shows "\<exists> j\<in> {m.. n}. real j \<le> x \<and> x < real (j+1)" (is "\<exists> j\<in> ?N. ?P j")
by (rule bexI[where P="?P" and x="floor x" and A="?N"])
-(auto simp add: floor_less_eq[where x="x" and a="n+1", simplified] xb[simplified] floor_mono2[where x="real m" and y="x", OF conjunct1[OF xb], simplified floor_real_of_int[where n="m"]])
+(auto simp add: floor_less_eq[where x="x" and a="n+1", simplified] xb[simplified] floor_mono[where x="real m" and y="x", OF conjunct1[OF xb], simplified floor_real_of_int[where n="m"]])
lemma rsplit0_complete:
assumes xp:"0 \<le> x" and x1:"x < 1"
--- a/src/HOL/IsaMakefile Wed Feb 25 19:34:00 2009 +0100
+++ b/src/HOL/IsaMakefile Wed Feb 25 11:30:46 2009 -0800
@@ -267,6 +267,7 @@
@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
$(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
+ Archimedean_Field.thy \
Complex_Main.thy \
Complex.thy \
Deriv.thy \
--- a/src/HOL/Nat.thy Wed Feb 25 19:34:00 2009 +0100
+++ b/src/HOL/Nat.thy Wed Feb 25 11:30:46 2009 -0800
@@ -280,6 +280,9 @@
lemma diff_add_0: "n - (n + m) = (0::nat)"
by (induct n) simp_all
+lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
+ unfolding One_nat_def by simp
+
text {* Difference distributes over multiplication *}
lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"
--- a/src/HOL/RComplete.thy Wed Feb 25 19:34:00 2009 +0100
+++ b/src/HOL/RComplete.thy Wed Feb 25 11:30:46 2009 -0800
@@ -380,33 +380,28 @@
thus "\<exists>(n::nat). x < real n" ..
qed
+instance real :: archimedean_field
+proof
+ fix r :: real
+ obtain n :: nat where "r < real n"
+ using reals_Archimedean2 ..
+ then have "r \<le> of_int (int n)"
+ unfolding real_eq_of_nat by simp
+ then show "\<exists>z. r \<le> of_int z" ..
+qed
+
lemma reals_Archimedean3:
assumes x_greater_zero: "0 < x"
shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x"
-proof
- fix y
- have x_not_zero: "x \<noteq> 0" using x_greater_zero by simp
- obtain n where "y * inverse x < real (n::nat)"
- using reals_Archimedean2 ..
- hence "y * inverse x * x < real n * x"
- using x_greater_zero by (simp add: mult_strict_right_mono)
- hence "x * inverse x * y < x * real n"
- by (simp add: algebra_simps)
- hence "y < real (n::nat) * x"
- using x_not_zero by (simp add: algebra_simps)
- thus "\<exists>(n::nat). y < real n * x" ..
-qed
+ unfolding real_of_nat_def using `0 < x`
+ by (auto intro: ex_less_of_nat_mult)
lemma reals_Archimedean6:
"0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
-apply (insert reals_Archimedean2 [of r], safe)
-apply (subgoal_tac "\<exists>x::nat. r < real x \<and> (\<forall>y. r < real y \<longrightarrow> x \<le> y)", auto)
-apply (rule_tac x = x in exI)
-apply (case_tac x, simp)
-apply (rename_tac x')
-apply (drule_tac x = x' in spec, simp)
-apply (rule_tac x="LEAST n. r < real n" in exI, safe)
-apply (erule LeastI, erule Least_le)
+unfolding real_of_nat_def
+apply (rule exI [where x="nat (floor r + 1)"])
+apply (insert floor_correct [of r])
+apply (simp add: nat_add_distrib of_nat_nat)
done
lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
@@ -414,19 +409,11 @@
lemma reals_Archimedean_6b_int:
"0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
-apply (drule reals_Archimedean6a, auto)
-apply (rule_tac x = "int n" in exI)
-apply (simp add: real_of_int_real_of_nat real_of_nat_Suc)
-done
+ unfolding real_of_int_def by (rule floor_exists)
lemma reals_Archimedean_6c_int:
"r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
-apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto)
-apply (rename_tac n)
-apply (drule order_le_imp_less_or_eq, auto)
-apply (rule_tac x = "- n - 1" in exI)
-apply (rule_tac [2] x = "- n" in exI, auto)
-done
+ unfolding real_of_int_def by (rule floor_exists)
subsection{*Density of the Rational Reals in the Reals*}
@@ -485,23 +472,6 @@
subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
-definition
- floor :: "real => int" where
- [code del]: "floor r = (LEAST n::int. r < real (n+1))"
-
-definition
- ceiling :: "real => int" where
- "ceiling r = - floor (- r)"
-
-notation (xsymbols)
- floor ("\<lfloor>_\<rfloor>") and
- ceiling ("\<lceil>_\<rceil>")
-
-notation (HTML output)
- floor ("\<lfloor>_\<rfloor>") and
- ceiling ("\<lceil>_\<rceil>")
-
-
lemma number_of_less_real_of_int_iff [simp]:
"((number_of n) < real (m::int)) = (number_of n < m)"
apply auto
@@ -524,51 +494,23 @@
"(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)"
by (simp add: linorder_not_less [symmetric])
-lemma floor_zero [simp]: "floor 0 = 0"
-apply (simp add: floor_def del: real_of_int_add)
-apply (rule Least_equality)
-apply simp_all
-done
-
-lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
-by auto
+lemma floor_real_of_nat_zero: "floor (real (0::nat)) = 0"
+by auto (* delete? *)
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
-apply (simp only: floor_def)
-apply (rule Least_equality)
-apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
-apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
-apply simp_all
-done
+unfolding real_of_nat_def by simp
lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
-apply (simp only: floor_def)
-apply (rule Least_equality)
-apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
-apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
-apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
-apply simp_all
-done
+unfolding real_of_nat_def by simp
lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
-apply (simp only: floor_def)
-apply (rule Least_equality)
-apply auto
-done
+unfolding real_of_int_def by simp
lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
-apply (simp only: floor_def)
-apply (rule Least_equality)
-apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
-apply auto
-done
+unfolding real_of_int_def by simp
lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
-apply (case_tac "r < 0")
-apply (blast intro: reals_Archimedean_6c_int)
-apply (simp only: linorder_not_less)
-apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int)
-done
+unfolding real_of_int_def by (rule floor_exists)
lemma lemma_floor:
assumes a1: "real m \<le> r" and a2: "r < real n + 1"
@@ -581,48 +523,20 @@
qed
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
-apply (simp add: floor_def Least_def)
-apply (insert real_lb_ub_int [of r], safe)
-apply (rule theI2)
-apply auto
-done
-
-lemma floor_mono: "x < y ==> floor x \<le> floor y"
-apply (simp add: floor_def Least_def)
-apply (insert real_lb_ub_int [of x])
-apply (insert real_lb_ub_int [of y], safe)
-apply (rule theI2)
-apply (rule_tac [3] theI2)
-apply simp
-apply (erule conjI)
-apply (auto simp add: order_eq_iff int_le_real_less)
-done
-
-lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y"
-by (auto dest: order_le_imp_less_or_eq simp add: floor_mono)
+unfolding real_of_int_def by (rule of_int_floor_le)
lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
by (auto intro: lemma_floor)
lemma real_of_int_floor_cancel [simp]:
"(real (floor x) = x) = (\<exists>n::int. x = real n)"
-apply (simp add: floor_def Least_def)
-apply (insert real_lb_ub_int [of x], erule exE)
-apply (rule theI2)
-apply (auto intro: lemma_floor)
-done
+ using floor_real_of_int by metis
lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
-apply (simp add: floor_def)
-apply (rule Least_equality)
-apply (auto intro: lemma_floor)
-done
+ unfolding real_of_int_def using floor_unique [of n x] by simp
lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
-apply (simp add: floor_def)
-apply (rule Least_equality)
-apply (auto intro: lemma_floor)
-done
+ unfolding real_of_int_def by (rule floor_unique)
lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
apply (rule inj_int [THEN injD])
@@ -635,353 +549,205 @@
apply (auto intro: floor_eq3)
done
-lemma floor_number_of_eq [simp]:
+lemma floor_number_of_eq:
"floor(number_of n :: real) = (number_of n :: int)"
-apply (subst real_number_of [symmetric])
-apply (rule floor_real_of_int)
-done
-
-lemma floor_one [simp]: "floor 1 = 1"
- apply (rule trans)
- prefer 2
- apply (rule floor_real_of_int)
- apply simp
-done
+ by (rule floor_number_of) (* already declared [simp] *)
lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
-apply (simp add: floor_def Least_def)
-apply (insert real_lb_ub_int [of r], safe)
-apply (rule theI2)
-apply (auto intro: lemma_floor)
-done
+ unfolding real_of_int_def using floor_correct [of r] by simp
lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
-apply (simp add: floor_def Least_def)
-apply (insert real_lb_ub_int [of r], safe)
-apply (rule theI2)
-apply (auto intro: lemma_floor)
-done
+ unfolding real_of_int_def using floor_correct [of r] by simp
lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
-apply (insert real_of_int_floor_ge_diff_one [of r])
-apply (auto simp del: real_of_int_floor_ge_diff_one)
-done
+ unfolding real_of_int_def using floor_correct [of r] by simp
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
-apply (insert real_of_int_floor_gt_diff_one [of r])
-apply (auto simp del: real_of_int_floor_gt_diff_one)
-done
+ unfolding real_of_int_def using floor_correct [of r] by simp
lemma le_floor: "real a <= x ==> a <= floor x"
- apply (subgoal_tac "a < floor x + 1")
- apply arith
- apply (subst real_of_int_less_iff [THEN sym])
- apply simp
- apply (insert real_of_int_floor_add_one_gt [of x])
- apply arith
-done
+ unfolding real_of_int_def by (simp add: le_floor_iff)
lemma real_le_floor: "a <= floor x ==> real a <= x"
- apply (rule order_trans)
- prefer 2
- apply (rule real_of_int_floor_le)
- apply (subst real_of_int_le_iff)
- apply assumption
-done
+ unfolding real_of_int_def by (simp add: le_floor_iff)
lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
- apply (rule iffI)
- apply (erule real_le_floor)
- apply (erule le_floor)
-done
+ unfolding real_of_int_def by (rule le_floor_iff)
-lemma le_floor_eq_number_of [simp]:
+lemma le_floor_eq_number_of:
"(number_of n <= floor x) = (number_of n <= x)"
-by (simp add: le_floor_eq)
+ by (rule number_of_le_floor) (* already declared [simp] *)
-lemma le_floor_eq_zero [simp]: "(0 <= floor x) = (0 <= x)"
-by (simp add: le_floor_eq)
+lemma le_floor_eq_zero: "(0 <= floor x) = (0 <= x)"
+ by (rule zero_le_floor) (* already declared [simp] *)
-lemma le_floor_eq_one [simp]: "(1 <= floor x) = (1 <= x)"
-by (simp add: le_floor_eq)
+lemma le_floor_eq_one: "(1 <= floor x) = (1 <= x)"
+ by (rule one_le_floor) (* already declared [simp] *)
lemma floor_less_eq: "(floor x < a) = (x < real a)"
- apply (subst linorder_not_le [THEN sym])+
- apply simp
- apply (rule le_floor_eq)
-done
+ unfolding real_of_int_def by (rule floor_less_iff)
-lemma floor_less_eq_number_of [simp]:
+lemma floor_less_eq_number_of:
"(floor x < number_of n) = (x < number_of n)"
-by (simp add: floor_less_eq)
+ by (rule floor_less_number_of) (* already declared [simp] *)
-lemma floor_less_eq_zero [simp]: "(floor x < 0) = (x < 0)"
-by (simp add: floor_less_eq)
+lemma floor_less_eq_zero: "(floor x < 0) = (x < 0)"
+ by (rule floor_less_zero) (* already declared [simp] *)
-lemma floor_less_eq_one [simp]: "(floor x < 1) = (x < 1)"
-by (simp add: floor_less_eq)
+lemma floor_less_eq_one: "(floor x < 1) = (x < 1)"
+ by (rule floor_less_one) (* already declared [simp] *)
lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
- apply (insert le_floor_eq [of "a + 1" x])
- apply auto
-done
+ unfolding real_of_int_def by (rule less_floor_iff)
-lemma less_floor_eq_number_of [simp]:
+lemma less_floor_eq_number_of:
"(number_of n < floor x) = (number_of n + 1 <= x)"
-by (simp add: less_floor_eq)
+ by (rule number_of_less_floor) (* already declared [simp] *)
-lemma less_floor_eq_zero [simp]: "(0 < floor x) = (1 <= x)"
-by (simp add: less_floor_eq)
+lemma less_floor_eq_zero: "(0 < floor x) = (1 <= x)"
+ by (rule zero_less_floor) (* already declared [simp] *)
-lemma less_floor_eq_one [simp]: "(1 < floor x) = (2 <= x)"
-by (simp add: less_floor_eq)
+lemma less_floor_eq_one: "(1 < floor x) = (2 <= x)"
+ by (rule one_less_floor) (* already declared [simp] *)
lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
- apply (insert floor_less_eq [of x "a + 1"])
- apply auto
-done
+ unfolding real_of_int_def by (rule floor_le_iff)
-lemma floor_le_eq_number_of [simp]:
+lemma floor_le_eq_number_of:
"(floor x <= number_of n) = (x < number_of n + 1)"
-by (simp add: floor_le_eq)
+ by (rule floor_le_number_of) (* already declared [simp] *)
-lemma floor_le_eq_zero [simp]: "(floor x <= 0) = (x < 1)"
-by (simp add: floor_le_eq)
+lemma floor_le_eq_zero: "(floor x <= 0) = (x < 1)"
+ by (rule floor_le_zero) (* already declared [simp] *)
-lemma floor_le_eq_one [simp]: "(floor x <= 1) = (x < 2)"
-by (simp add: floor_le_eq)
+lemma floor_le_eq_one: "(floor x <= 1) = (x < 2)"
+ by (rule floor_le_one) (* already declared [simp] *)
lemma floor_add [simp]: "floor (x + real a) = floor x + a"
- apply (subst order_eq_iff)
- apply (rule conjI)
- prefer 2
- apply (subgoal_tac "floor x + a < floor (x + real a) + 1")
- apply arith
- apply (subst real_of_int_less_iff [THEN sym])
- apply simp
- apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1")
- apply (subgoal_tac "real (floor x) <= x")
- apply arith
- apply (rule real_of_int_floor_le)
- apply (rule real_of_int_floor_add_one_gt)
- apply (subgoal_tac "floor (x + real a) < floor x + a + 1")
- apply arith
- apply (subst real_of_int_less_iff [THEN sym])
- apply simp
- apply (subgoal_tac "real(floor(x + real a)) <= x + real a")
- apply (subgoal_tac "x < real(floor x) + 1")
- apply arith
- apply (rule real_of_int_floor_add_one_gt)
- apply (rule real_of_int_floor_le)
-done
-
-lemma floor_add_number_of [simp]:
- "floor (x + number_of n) = floor x + number_of n"
- apply (subst floor_add [THEN sym])
- apply simp
-done
-
-lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
- apply (subst floor_add [THEN sym])
- apply simp
-done
+ unfolding real_of_int_def by (rule floor_add_of_int)
lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
- apply (subst diff_minus)+
- apply (subst real_of_int_minus [THEN sym])
- apply (rule floor_add)
-done
+ unfolding real_of_int_def by (rule floor_diff_of_int)
-lemma floor_subtract_number_of [simp]: "floor (x - number_of n) =
+lemma floor_subtract_number_of: "floor (x - number_of n) =
floor x - number_of n"
- apply (subst floor_subtract [THEN sym])
- apply simp
-done
+ by (rule floor_diff_number_of) (* already declared [simp] *)
-lemma floor_subtract_one [simp]: "floor (x - 1) = floor x - 1"
- apply (subst floor_subtract [THEN sym])
- apply simp
-done
-
-lemma ceiling_zero [simp]: "ceiling 0 = 0"
-by (simp add: ceiling_def)
+lemma floor_subtract_one: "floor (x - 1) = floor x - 1"
+ by (rule floor_diff_one) (* already declared [simp] *)
lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
-by (simp add: ceiling_def)
+ unfolding real_of_nat_def by simp
-lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0"
-by auto
+lemma ceiling_real_of_nat_zero: "ceiling (real (0::nat)) = 0"
+by auto (* delete? *)
lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
-by (simp add: ceiling_def)
+ unfolding real_of_int_def by simp
lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"
-by (simp add: ceiling_def)
+ unfolding real_of_int_def by simp
lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
-apply (simp add: ceiling_def)
-apply (subst le_minus_iff, simp)
-done
+ unfolding real_of_int_def by (rule le_of_int_ceiling)
-lemma ceiling_mono: "x < y ==> ceiling x \<le> ceiling y"
-by (simp add: floor_mono ceiling_def)
-
-lemma ceiling_mono2: "x \<le> y ==> ceiling x \<le> ceiling y"
-by (simp add: floor_mono2 ceiling_def)
+lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
+ unfolding real_of_int_def by simp
lemma real_of_int_ceiling_cancel [simp]:
"(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
-apply (auto simp add: ceiling_def)
-apply (drule arg_cong [where f = uminus], auto)
-apply (rule_tac x = "-n" in exI, auto)
-done
+ using ceiling_real_of_int by metis
lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
-apply (simp add: ceiling_def)
-apply (rule minus_equation_iff [THEN iffD1])
-apply (simp add: floor_eq [where n = "-(n+1)"])
-done
+ unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
-by (simp add: ceiling_def floor_eq2 [where n = "-(n+1)"])
+ unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n |] ==> ceiling x = n"
-by (simp add: ceiling_def floor_eq2 [where n = "-n"])
+ unfolding real_of_int_def using ceiling_unique [of n x] by simp
-lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
-by (simp add: ceiling_def)
-
-lemma ceiling_number_of_eq [simp]:
+lemma ceiling_number_of_eq:
"ceiling (number_of n :: real) = (number_of n)"
-apply (subst real_number_of [symmetric])
-apply (rule ceiling_real_of_int)
-done
-
-lemma ceiling_one [simp]: "ceiling 1 = 1"
- by (unfold ceiling_def, simp)
+ by (rule ceiling_number_of) (* already declared [simp] *)
lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
-apply (rule neg_le_iff_le [THEN iffD1])
-apply (simp add: ceiling_def diff_minus)
-done
+ unfolding real_of_int_def using ceiling_correct [of r] by simp
lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
-apply (insert real_of_int_ceiling_diff_one_le [of r])
-apply (simp del: real_of_int_ceiling_diff_one_le)
-done
+ unfolding real_of_int_def using ceiling_correct [of r] by simp
lemma ceiling_le: "x <= real a ==> ceiling x <= a"
- apply (unfold ceiling_def)
- apply (subgoal_tac "-a <= floor(- x)")
- apply simp
- apply (rule le_floor)
- apply simp
-done
+ unfolding real_of_int_def by (simp add: ceiling_le_iff)
lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
- apply (unfold ceiling_def)
- apply (subgoal_tac "real(- a) <= - x")
- apply simp
- apply (rule real_le_floor)
- apply simp
-done
+ unfolding real_of_int_def by (simp add: ceiling_le_iff)
lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
- apply (rule iffI)
- apply (erule ceiling_le_real)
- apply (erule ceiling_le)
-done
+ unfolding real_of_int_def by (rule ceiling_le_iff)
-lemma ceiling_le_eq_number_of [simp]:
+lemma ceiling_le_eq_number_of:
"(ceiling x <= number_of n) = (x <= number_of n)"
-by (simp add: ceiling_le_eq)
+ by (rule ceiling_le_number_of) (* already declared [simp] *)
-lemma ceiling_le_zero_eq [simp]: "(ceiling x <= 0) = (x <= 0)"
-by (simp add: ceiling_le_eq)
+lemma ceiling_le_zero_eq: "(ceiling x <= 0) = (x <= 0)"
+ by (rule ceiling_le_zero) (* already declared [simp] *)
-lemma ceiling_le_eq_one [simp]: "(ceiling x <= 1) = (x <= 1)"
-by (simp add: ceiling_le_eq)
+lemma ceiling_le_eq_one: "(ceiling x <= 1) = (x <= 1)"
+ by (rule ceiling_le_one) (* already declared [simp] *)
lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
- apply (subst linorder_not_le [THEN sym])+
- apply simp
- apply (rule ceiling_le_eq)
-done
+ unfolding real_of_int_def by (rule less_ceiling_iff)
-lemma less_ceiling_eq_number_of [simp]:
+lemma less_ceiling_eq_number_of:
"(number_of n < ceiling x) = (number_of n < x)"
-by (simp add: less_ceiling_eq)
+ by (rule number_of_less_ceiling) (* already declared [simp] *)
-lemma less_ceiling_eq_zero [simp]: "(0 < ceiling x) = (0 < x)"
-by (simp add: less_ceiling_eq)
+lemma less_ceiling_eq_zero: "(0 < ceiling x) = (0 < x)"
+ by (rule zero_less_ceiling) (* already declared [simp] *)
-lemma less_ceiling_eq_one [simp]: "(1 < ceiling x) = (1 < x)"
-by (simp add: less_ceiling_eq)
+lemma less_ceiling_eq_one: "(1 < ceiling x) = (1 < x)"
+ by (rule one_less_ceiling) (* already declared [simp] *)
lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
- apply (insert ceiling_le_eq [of x "a - 1"])
- apply auto
-done
+ unfolding real_of_int_def by (rule ceiling_less_iff)
-lemma ceiling_less_eq_number_of [simp]:
+lemma ceiling_less_eq_number_of:
"(ceiling x < number_of n) = (x <= number_of n - 1)"
-by (simp add: ceiling_less_eq)
+ by (rule ceiling_less_number_of) (* already declared [simp] *)
-lemma ceiling_less_eq_zero [simp]: "(ceiling x < 0) = (x <= -1)"
-by (simp add: ceiling_less_eq)
+lemma ceiling_less_eq_zero: "(ceiling x < 0) = (x <= -1)"
+ by (rule ceiling_less_zero) (* already declared [simp] *)
-lemma ceiling_less_eq_one [simp]: "(ceiling x < 1) = (x <= 0)"
-by (simp add: ceiling_less_eq)
+lemma ceiling_less_eq_one: "(ceiling x < 1) = (x <= 0)"
+ by (rule ceiling_less_one) (* already declared [simp] *)
lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
- apply (insert less_ceiling_eq [of "a - 1" x])
- apply auto
-done
+ unfolding real_of_int_def by (rule le_ceiling_iff)
-lemma le_ceiling_eq_number_of [simp]:
+lemma le_ceiling_eq_number_of:
"(number_of n <= ceiling x) = (number_of n - 1 < x)"
-by (simp add: le_ceiling_eq)
+ by (rule number_of_le_ceiling) (* already declared [simp] *)
-lemma le_ceiling_eq_zero [simp]: "(0 <= ceiling x) = (-1 < x)"
-by (simp add: le_ceiling_eq)
+lemma le_ceiling_eq_zero: "(0 <= ceiling x) = (-1 < x)"
+ by (rule zero_le_ceiling) (* already declared [simp] *)
-lemma le_ceiling_eq_one [simp]: "(1 <= ceiling x) = (0 < x)"
-by (simp add: le_ceiling_eq)
+lemma le_ceiling_eq_one: "(1 <= ceiling x) = (0 < x)"
+ by (rule one_le_ceiling) (* already declared [simp] *)
lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
- apply (unfold ceiling_def, simp)
- apply (subst real_of_int_minus [THEN sym])
- apply (subst floor_add)
- apply simp
-done
-
-lemma ceiling_add_number_of [simp]: "ceiling (x + number_of n) =
- ceiling x + number_of n"
- apply (subst ceiling_add [THEN sym])
- apply simp
-done
-
-lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
- apply (subst ceiling_add [THEN sym])
- apply simp
-done
+ unfolding real_of_int_def by (rule ceiling_add_of_int)
lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
- apply (subst diff_minus)+
- apply (subst real_of_int_minus [THEN sym])
- apply (rule ceiling_add)
-done
+ unfolding real_of_int_def by (rule ceiling_diff_of_int)
-lemma ceiling_subtract_number_of [simp]: "ceiling (x - number_of n) =
+lemma ceiling_subtract_number_of: "ceiling (x - number_of n) =
ceiling x - number_of n"
- apply (subst ceiling_subtract [THEN sym])
- apply simp
-done
+ by (rule ceiling_diff_number_of) (* already declared [simp] *)
-lemma ceiling_subtract_one [simp]: "ceiling (x - 1) = ceiling x - 1"
- apply (subst ceiling_subtract [THEN sym])
- apply simp
-done
+lemma ceiling_subtract_one: "ceiling (x - 1) = ceiling x - 1"
+ by (rule ceiling_diff_one) (* already declared [simp] *)
+
subsection {* Versions for the natural numbers *}
@@ -1015,7 +781,7 @@
apply (unfold natfloor_def)
apply (subgoal_tac "floor x <= floor 0")
apply simp
- apply (erule floor_mono2)
+ apply (erule floor_mono)
done
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
@@ -1023,7 +789,7 @@
apply (subst natfloor_def)+
apply (subst nat_le_eq_zle)
apply force
- apply (erule floor_mono2)
+ apply (erule floor_mono)
apply (subst natfloor_neg)
apply simp
apply simp
@@ -1144,7 +910,7 @@
apply (subst real_nat_eq_real)
apply (subgoal_tac "ceiling 0 <= ceiling x")
apply simp
- apply (rule ceiling_mono2)
+ apply (rule ceiling_mono)
apply simp
apply simp
done
@@ -1165,7 +931,7 @@
apply simp
apply (erule order_trans)
apply simp
- apply (erule ceiling_mono2)
+ apply (erule ceiling_mono)
apply (subst natceiling_neg)
apply simp_all
done
@@ -1215,7 +981,7 @@
apply (subst eq_nat_nat_iff)
apply (subgoal_tac "ceiling 0 <= ceiling x")
apply simp
- apply (rule ceiling_mono2)
+ apply (rule ceiling_mono)
apply force
apply force
apply (rule ceiling_eq2)
@@ -1233,7 +999,7 @@
apply (subst nat_add_distrib)
apply (subgoal_tac "0 = ceiling 0")
apply (erule ssubst)
- apply (erule ceiling_mono2)
+ apply (erule ceiling_mono)
apply simp_all
done
--- a/src/HOL/Rational.thy Wed Feb 25 19:34:00 2009 +0100
+++ b/src/HOL/Rational.thy Wed Feb 25 11:30:46 2009 -0800
@@ -5,7 +5,7 @@
header {* Rational numbers *}
theory Rational
-imports GCD
+imports GCD Archimedean_Field
uses ("Tools/rat_arith.ML")
begin
@@ -255,7 +255,6 @@
with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
with Fract `q = Fract a b` `b \<noteq> 0` show C by auto
qed
-
subsubsection {* The field of rational numbers *}
@@ -532,8 +531,67 @@
qed
lemma zero_less_Fract_iff:
- "0 < b ==> (0 < Fract a b) = (0 < a)"
-by (simp add: Zero_rat_def order_less_imp_not_eq2 zero_less_mult_iff)
+ "0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a"
+ by (simp add: Zero_rat_def zero_less_mult_iff)
+
+lemma Fract_less_zero_iff:
+ "0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0"
+ by (simp add: Zero_rat_def mult_less_0_iff)
+
+lemma zero_le_Fract_iff:
+ "0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a"
+ by (simp add: Zero_rat_def zero_le_mult_iff)
+
+lemma Fract_le_zero_iff:
+ "0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0"
+ by (simp add: Zero_rat_def mult_le_0_iff)
+
+lemma one_less_Fract_iff:
+ "0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a"
+ by (simp add: One_rat_def mult_less_cancel_right_disj)
+
+lemma Fract_less_one_iff:
+ "0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b"
+ by (simp add: One_rat_def mult_less_cancel_right_disj)
+
+lemma one_le_Fract_iff:
+ "0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a"
+ by (simp add: One_rat_def mult_le_cancel_right)
+
+lemma Fract_le_one_iff:
+ "0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b"
+ by (simp add: One_rat_def mult_le_cancel_right)
+
+
+subsubsection {* Rationals are an Archimedean field *}
+
+lemma rat_floor_lemma:
+ assumes "0 < b"
+ shows "of_int (a div b) \<le> Fract a b \<and> Fract a b < of_int (a div b + 1)"
+proof -
+ have "Fract a b = of_int (a div b) + Fract (a mod b) b"
+ using `0 < b` by (simp add: of_int_rat)
+ moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
+ using `0 < b` by (simp add: zero_le_Fract_iff Fract_less_one_iff)
+ ultimately show ?thesis by simp
+qed
+
+instance rat :: archimedean_field
+proof
+ fix r :: rat
+ show "\<exists>z. r \<le> of_int z"
+ proof (induct r)
+ case (Fract a b)
+ then have "Fract a b \<le> of_int (a div b + 1)"
+ using rat_floor_lemma [of b a] by simp
+ then show "\<exists>z. Fract a b \<le> of_int z" ..
+ qed
+qed
+
+lemma floor_Fract:
+ assumes "0 < b" shows "floor (Fract a b) = a div b"
+ using rat_floor_lemma [OF `0 < b`, of a]
+ by (simp add: floor_unique)
subsection {* Arithmetic setup *}