src/HOL/Real/RComplete.thy
changeset 23309 678ee30499d2
parent 23012 496b42cf588d
child 23389 aaca6a8e5414
     1.1 --- a/src/HOL/Real/RComplete.thy	Mon Jun 11 06:14:32 2007 +0200
     1.2 +++ b/src/HOL/Real/RComplete.thy	Mon Jun 11 07:10:06 2007 +0200
     1.3 @@ -480,36 +480,34 @@
     1.4  lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
     1.5  by auto
     1.6  
     1.7 -lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
     1.8 +lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int_of_nat n"
     1.9  apply (simp only: floor_def)
    1.10  apply (rule Least_equality)
    1.11 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    1.12 +apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
    1.13  apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
    1.14 -apply (simp_all add: real_of_int_real_of_nat)
    1.15 +apply simp_all
    1.16  done
    1.17  
    1.18 -lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
    1.19 +lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int_of_nat n"
    1.20  apply (simp only: floor_def)
    1.21  apply (rule Least_equality)
    1.22 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    1.23 +apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
    1.24  apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
    1.25  apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
    1.26 -apply (simp_all add: real_of_int_real_of_nat)
    1.27 +apply simp_all
    1.28  done
    1.29  
    1.30  lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
    1.31  apply (simp only: floor_def)
    1.32  apply (rule Least_equality)
    1.33 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    1.34 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
    1.35 +apply auto
    1.36  done
    1.37  
    1.38  lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
    1.39  apply (simp only: floor_def)
    1.40  apply (rule Least_equality)
    1.41  apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
    1.42 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    1.43 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
    1.44 +apply auto
    1.45  done
    1.46  
    1.47  lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
    1.48 @@ -755,7 +753,7 @@
    1.49  lemma ceiling_zero [simp]: "ceiling 0 = 0"
    1.50  by (simp add: ceiling_def)
    1.51  
    1.52 -lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
    1.53 +lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int_of_nat n"
    1.54  by (simp add: ceiling_def)
    1.55  
    1.56  lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0"
    1.57 @@ -1045,9 +1043,9 @@
    1.58  
    1.59  lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
    1.60    apply (unfold natfloor_def)
    1.61 -  apply (subgoal_tac "real a = real (int a)")
    1.62 +  apply (subgoal_tac "real a = real (int_of_nat a)")
    1.63    apply (erule ssubst)
    1.64 -  apply (simp add: nat_add_distrib)
    1.65 +  apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq)
    1.66    apply simp
    1.67  done
    1.68  
    1.69 @@ -1067,9 +1065,9 @@
    1.70  lemma natfloor_subtract [simp]: "real a <= x ==>
    1.71      natfloor(x - real a) = natfloor x - a"
    1.72    apply (unfold natfloor_def)
    1.73 -  apply (subgoal_tac "real a = real (int a)")
    1.74 +  apply (subgoal_tac "real a = real (int_of_nat a)")
    1.75    apply (erule ssubst)
    1.76 -  apply simp
    1.77 +  apply (simp del: real_of_int_of_nat_eq)
    1.78    apply simp
    1.79  done
    1.80  
    1.81 @@ -1178,9 +1176,9 @@
    1.82  lemma natceiling_add [simp]: "0 <= x ==>
    1.83      natceiling (x + real a) = natceiling x + a"
    1.84    apply (unfold natceiling_def)
    1.85 -  apply (subgoal_tac "real a = real (int a)")
    1.86 +  apply (subgoal_tac "real a = real (int_of_nat a)")
    1.87    apply (erule ssubst)
    1.88 -  apply simp
    1.89 +  apply (simp del: real_of_int_of_nat_eq)
    1.90    apply (subst nat_add_distrib)
    1.91    apply (subgoal_tac "0 = ceiling 0")
    1.92    apply (erule ssubst)
    1.93 @@ -1204,9 +1202,9 @@
    1.94  lemma natceiling_subtract [simp]: "real a <= x ==>
    1.95      natceiling(x - real a) = natceiling x - a"
    1.96    apply (unfold natceiling_def)
    1.97 -  apply (subgoal_tac "real a = real (int a)")
    1.98 +  apply (subgoal_tac "real a = real (int_of_nat a)")
    1.99    apply (erule ssubst)
   1.100 -  apply simp
   1.101 +  apply (simp del: real_of_int_of_nat_eq)
   1.102    apply simp
   1.103  done
   1.104