# HG changeset patch
# User huffman
# Date 1267980038 28800
# Node ID 6fdfe37b84d68e821af557c7d935dd462fe4f714
# Parent  5da59c1ddece31dd5a74f7bec07df5ca2988d3d6
add more simp rules for Ints

diff -r 5da59c1ddece -r 6fdfe37b84d6 src/HOL/Int.thy
--- 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))"