# HG changeset patch
# User huffman
# Date 1181538606 -7200
# Node ID 678ee30499d281e29be2c63deee3a9999397c5c1
# Parent  95a01ddfb024eb0cf9d5a9ceef13c2c25883125b
remove references to constant int::nat=>int

diff -r 95a01ddfb024 -r 678ee30499d2 src/HOL/Library/Parity.thy
--- a/src/HOL/Library/Parity.thy	Mon Jun 11 06:14:32 2007 +0200
+++ b/src/HOL/Library/Parity.thy	Mon Jun 11 07:10:06 2007 +0200
@@ -20,7 +20,7 @@
   even_def: "even x \<equiv> x mod 2 = 0" ..
 
 instance nat :: even_odd
-  even_nat_def: "even x \<equiv> even (int x)" ..
+  even_nat_def: "even x \<equiv> even (int_of_nat x)" ..
 
 
 subsection {* Even and odd are mutually exclusive *}
@@ -135,7 +135,7 @@
   by (simp add: even_nat_def)
 
 lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
-  by (simp add: even_nat_def int_mult)
+  by (simp add: even_nat_def)
 
 lemma even_nat_sum: "even ((x::nat) + y) =
     ((even x & even y) | (odd x & odd y))"
@@ -143,16 +143,16 @@
 
 lemma even_nat_difference:
     "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
-  apply (auto simp add: even_nat_def zdiff_int [symmetric])
-  apply (case_tac "x < y", auto simp add: zdiff_int [symmetric])
-  apply (case_tac "x < y", auto simp add: zdiff_int [symmetric])
+  apply (auto simp add: even_nat_def)
+  apply (case_tac "x < y", auto)
+  apply (case_tac "x < y", auto)
   done
 
 lemma even_nat_Suc: "even (Suc x) = odd x"
   by (simp add: even_nat_def)
 
 lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
-  by (simp add: even_nat_def int_power)
+  by (simp add: even_nat_def of_nat_power)
 
 lemma even_nat_zero: "even (0::nat)"
   by (simp add: even_nat_def)
diff -r 95a01ddfb024 -r 678ee30499d2 src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Mon Jun 11 06:14:32 2007 +0200
+++ b/src/HOL/Real/RComplete.thy	Mon Jun 11 07:10:06 2007 +0200
@@ -480,36 +480,34 @@
 lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
 by auto
 
-lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
+lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int_of_nat n"
 apply (simp only: floor_def)
 apply (rule Least_equality)
-apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
+apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
 apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
-apply (simp_all add: real_of_int_real_of_nat)
+apply simp_all
 done
 
-lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
+lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int_of_nat n"
 apply (simp only: floor_def)
 apply (rule Least_equality)
-apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
+apply (drule_tac [2] real_of_int_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 add: real_of_int_real_of_nat)
+apply simp_all
 done
 
 lemma floor_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_real_of_nat [THEN ssubst])
-apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
+apply auto
 done
 
 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 (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
-apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
+apply auto
 done
 
 lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
@@ -755,7 +753,7 @@
 lemma ceiling_zero [simp]: "ceiling 0 = 0"
 by (simp add: ceiling_def)
 
-lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
+lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int_of_nat n"
 by (simp add: ceiling_def)
 
 lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0"
@@ -1045,9 +1043,9 @@
 
 lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
   apply (unfold natfloor_def)
-  apply (subgoal_tac "real a = real (int a)")
+  apply (subgoal_tac "real a = real (int_of_nat a)")
   apply (erule ssubst)
-  apply (simp add: nat_add_distrib)
+  apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq)
   apply simp
 done
 
@@ -1067,9 +1065,9 @@
 lemma natfloor_subtract [simp]: "real a <= x ==>
     natfloor(x - real a) = natfloor x - a"
   apply (unfold natfloor_def)
-  apply (subgoal_tac "real a = real (int a)")
+  apply (subgoal_tac "real a = real (int_of_nat a)")
   apply (erule ssubst)
-  apply simp
+  apply (simp del: real_of_int_of_nat_eq)
   apply simp
 done
 
@@ -1178,9 +1176,9 @@
 lemma natceiling_add [simp]: "0 <= x ==>
     natceiling (x + real a) = natceiling x + a"
   apply (unfold natceiling_def)
-  apply (subgoal_tac "real a = real (int a)")
+  apply (subgoal_tac "real a = real (int_of_nat a)")
   apply (erule ssubst)
-  apply simp
+  apply (simp del: real_of_int_of_nat_eq)
   apply (subst nat_add_distrib)
   apply (subgoal_tac "0 = ceiling 0")
   apply (erule ssubst)
@@ -1204,9 +1202,9 @@
 lemma natceiling_subtract [simp]: "real a <= x ==>
     natceiling(x - real a) = natceiling x - a"
   apply (unfold natceiling_def)
-  apply (subgoal_tac "real a = real (int a)")
+  apply (subgoal_tac "real a = real (int_of_nat a)")
   apply (erule ssubst)
-  apply simp
+  apply (simp del: real_of_int_of_nat_eq)
   apply simp
 done