# HG changeset patch
# User huffman
# Date 1315142879 25200
# Node ID 487ae6317f7bca261a4e0c5bbb0e04344d665c4b
# Parent  b99dfee76538969fad4018a656ddebb9ce9321b3
move lemmas nat_le_iff and nat_mono into Int.thy

diff -r b99dfee76538 -r 487ae6317f7b src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Sep 04 14:29:15 2011 +0200
+++ b/src/HOL/Int.thy	Sun Sep 04 06:27:59 2011 -0700
@@ -446,6 +446,12 @@
 apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
 done
 
+lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> of_nat n"
+  by (cases x, simp add: nat le int_def le_diff_conv)
+
+lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
+  by (cases x, cases y, simp add: nat le)
+
 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
 by(simp add: nat_eq_iff) arith
 
diff -r b99dfee76538 -r 487ae6317f7b src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Sun Sep 04 14:29:15 2011 +0200
+++ b/src/HOL/RComplete.thy	Sun Sep 04 06:27:59 2011 -0700
@@ -336,9 +336,6 @@
 lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
   unfolding natfloor_def by simp
 
-lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
-  by simp (* TODO: move to Int.thy *)
-
 lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
   unfolding natfloor_def by (intro nat_mono floor_mono)
 
@@ -474,9 +471,6 @@
 lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
   unfolding natceiling_def by (intro nat_mono ceiling_mono)
 
-lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
-  by auto (* TODO: move to Int.thy *)
-
 lemma natceiling_le: "x <= real a ==> natceiling x <= a"
   unfolding natceiling_def real_of_nat_def
   by (simp add: nat_le_iff ceiling_le_iff)