author huffman Mon Jun 11 07:10:06 2007 +0200 (2007-06-11) changeset 23309 678ee30499d2 parent 23308 95a01ddfb024 child 23310 22ddaef5fb92
remove references to constant int::nat=>int
 src/HOL/Library/Parity.thy file | annotate | diff | revisions src/HOL/Real/RComplete.thy file | annotate | diff | revisions
```     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.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.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)"
```
```     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.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.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.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.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.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.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
```