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

lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
-  by (simp add: even_nat_def int_mult)

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"

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)"
```--- 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
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
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"

-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"

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
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 (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
```