--- a/src/HOL/Int.thy Sun Mar 07 07:42:46 2010 -0800
+++ b/src/HOL/Int.thy Sun Mar 07 08:40:38 2010 -0800
@@ -1262,6 +1262,15 @@
notation (xsymbols)
Ints ("\<int>")
+lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
+ by (simp add: Ints_def)
+
+lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
+apply (simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_of_nat_eq [symmetric])
+done
+
lemma Ints_0 [simp]: "0 \<in> \<int>"
apply (simp add: Ints_def)
apply (rule range_eqI)
@@ -1286,12 +1295,21 @@
apply (rule of_int_minus [symmetric])
done
+lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_diff [symmetric])
+done
+
lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
apply (auto simp add: Ints_def)
apply (rule range_eqI)
apply (rule of_int_mult [symmetric])
done
+lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
+by (induct n) simp_all
+
lemma Ints_cases [cases set: Ints]:
assumes "q \<in> \<int>"
obtains (of_int) z where "q = of_int z"
@@ -1308,12 +1326,6 @@
end
-lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a-b \<in> \<int>"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_diff [symmetric])
-done
-
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
lemma Ints_double_eq_0_iff:
@@ -1350,10 +1362,15 @@
qed
qed
-lemma Ints_number_of:
+lemma Ints_number_of [simp]:
"(number_of w :: 'a::number_ring) \<in> Ints"
unfolding number_of_eq Ints_def by simp
+lemma Nats_number_of [simp]:
+ "Int.Pls \<le> w \<Longrightarrow> (number_of w :: 'a::number_ring) \<in> Nats"
+unfolding Int.Pls_def number_of_eq
+by (simp only: of_nat_nat [symmetric] of_nat_in_Nats)
+
lemma Ints_odd_less_0:
assumes in_Ints: "a \<in> Ints"
shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"