remove references to constant int::nat=>int
authorhuffman
Mon Jun 11 07:10:06 2007 +0200 (2007-06-11)
changeset 23309678ee30499d2
parent 23308 95a01ddfb024
child 23310 22ddaef5fb92
remove references to constant int::nat=>int
src/HOL/Library/Parity.thy
src/HOL/Real/RComplete.thy
     1.1 --- a/src/HOL/Library/Parity.thy	Mon Jun 11 06:14:32 2007 +0200
     1.2 +++ b/src/HOL/Library/Parity.thy	Mon Jun 11 07:10:06 2007 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    even_def: "even x \<equiv> x mod 2 = 0" ..
     1.5  
     1.6  instance nat :: even_odd
     1.7 -  even_nat_def: "even x \<equiv> even (int x)" ..
     1.8 +  even_nat_def: "even x \<equiv> even (int_of_nat x)" ..
     1.9  
    1.10  
    1.11  subsection {* Even and odd are mutually exclusive *}
    1.12 @@ -135,7 +135,7 @@
    1.13    by (simp add: even_nat_def)
    1.14  
    1.15  lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
    1.16 -  by (simp add: even_nat_def int_mult)
    1.17 +  by (simp add: even_nat_def)
    1.18  
    1.19  lemma even_nat_sum: "even ((x::nat) + y) =
    1.20      ((even x & even y) | (odd x & odd y))"
    1.21 @@ -143,16 +143,16 @@
    1.22  
    1.23  lemma even_nat_difference:
    1.24      "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
    1.25 -  apply (auto simp add: even_nat_def zdiff_int [symmetric])
    1.26 -  apply (case_tac "x < y", auto simp add: zdiff_int [symmetric])
    1.27 -  apply (case_tac "x < y", auto simp add: zdiff_int [symmetric])
    1.28 +  apply (auto simp add: even_nat_def)
    1.29 +  apply (case_tac "x < y", auto)
    1.30 +  apply (case_tac "x < y", auto)
    1.31    done
    1.32  
    1.33  lemma even_nat_Suc: "even (Suc x) = odd x"
    1.34    by (simp add: even_nat_def)
    1.35  
    1.36  lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
    1.37 -  by (simp add: even_nat_def int_power)
    1.38 +  by (simp add: even_nat_def of_nat_power)
    1.39  
    1.40  lemma even_nat_zero: "even (0::nat)"
    1.41    by (simp add: even_nat_def)
     2.1 --- a/src/HOL/Real/RComplete.thy	Mon Jun 11 06:14:32 2007 +0200
     2.2 +++ b/src/HOL/Real/RComplete.thy	Mon Jun 11 07:10:06 2007 +0200
     2.3 @@ -480,36 +480,34 @@
     2.4  lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
     2.5  by auto
     2.6  
     2.7 -lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
     2.8 +lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int_of_nat n"
     2.9  apply (simp only: floor_def)
    2.10  apply (rule Least_equality)
    2.11 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    2.12 +apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
    2.13  apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
    2.14 -apply (simp_all add: real_of_int_real_of_nat)
    2.15 +apply simp_all
    2.16  done
    2.17  
    2.18 -lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
    2.19 +lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int_of_nat n"
    2.20  apply (simp only: floor_def)
    2.21  apply (rule Least_equality)
    2.22 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    2.23 +apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
    2.24  apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
    2.25  apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
    2.26 -apply (simp_all add: real_of_int_real_of_nat)
    2.27 +apply simp_all
    2.28  done
    2.29  
    2.30  lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
    2.31  apply (simp only: floor_def)
    2.32  apply (rule Least_equality)
    2.33 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    2.34 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
    2.35 +apply auto
    2.36  done
    2.37  
    2.38  lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
    2.39  apply (simp only: floor_def)
    2.40  apply (rule Least_equality)
    2.41  apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
    2.42 -apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
    2.43 -apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
    2.44 +apply auto
    2.45  done
    2.46  
    2.47  lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
    2.48 @@ -755,7 +753,7 @@
    2.49  lemma ceiling_zero [simp]: "ceiling 0 = 0"
    2.50  by (simp add: ceiling_def)
    2.51  
    2.52 -lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
    2.53 +lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int_of_nat n"
    2.54  by (simp add: ceiling_def)
    2.55  
    2.56  lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0"
    2.57 @@ -1045,9 +1043,9 @@
    2.58  
    2.59  lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
    2.60    apply (unfold natfloor_def)
    2.61 -  apply (subgoal_tac "real a = real (int a)")
    2.62 +  apply (subgoal_tac "real a = real (int_of_nat a)")
    2.63    apply (erule ssubst)
    2.64 -  apply (simp add: nat_add_distrib)
    2.65 +  apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq)
    2.66    apply simp
    2.67  done
    2.68  
    2.69 @@ -1067,9 +1065,9 @@
    2.70  lemma natfloor_subtract [simp]: "real a <= x ==>
    2.71      natfloor(x - real a) = natfloor x - a"
    2.72    apply (unfold natfloor_def)
    2.73 -  apply (subgoal_tac "real a = real (int a)")
    2.74 +  apply (subgoal_tac "real a = real (int_of_nat a)")
    2.75    apply (erule ssubst)
    2.76 -  apply simp
    2.77 +  apply (simp del: real_of_int_of_nat_eq)
    2.78    apply simp
    2.79  done
    2.80  
    2.81 @@ -1178,9 +1176,9 @@
    2.82  lemma natceiling_add [simp]: "0 <= x ==>
    2.83      natceiling (x + real a) = natceiling x + a"
    2.84    apply (unfold natceiling_def)
    2.85 -  apply (subgoal_tac "real a = real (int a)")
    2.86 +  apply (subgoal_tac "real a = real (int_of_nat a)")
    2.87    apply (erule ssubst)
    2.88 -  apply simp
    2.89 +  apply (simp del: real_of_int_of_nat_eq)
    2.90    apply (subst nat_add_distrib)
    2.91    apply (subgoal_tac "0 = ceiling 0")
    2.92    apply (erule ssubst)
    2.93 @@ -1204,9 +1202,9 @@
    2.94  lemma natceiling_subtract [simp]: "real a <= x ==>
    2.95      natceiling(x - real a) = natceiling x - a"
    2.96    apply (unfold natceiling_def)
    2.97 -  apply (subgoal_tac "real a = real (int a)")
    2.98 +  apply (subgoal_tac "real a = real (int_of_nat a)")
    2.99    apply (erule ssubst)
   2.100 -  apply simp
   2.101 +  apply (simp del: real_of_int_of_nat_eq)
   2.102    apply simp
   2.103  done
   2.104