# HG changeset patch
# User huffman
# Date 1181517749 -7200
# Node ID 83f3b6dc58b543cc58a3091812b6054f208bf607
# Parent  6091e530ff77f43962f42c66876f9acb8886b0ef
add int_of_nat versions of lemmas about int::nat=>int

diff -r 6091e530ff77 -r 83f3b6dc58b5 src/HOL/IntArith.thy
--- a/src/HOL/IntArith.thy	Mon Jun 11 00:53:18 2007 +0200
+++ b/src/HOL/IntArith.thy	Mon Jun 11 01:22:29 2007 +0200
@@ -196,6 +196,24 @@
       z is an integer literal.*}
 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
 
+lemmas int_of_nat_eq_iff_number_of [simp] =
+  int_of_nat_eq_iff [of _ "number_of v", standard]
+
+lemma split_nat':
+  "P(nat(i::int)) = ((\<forall>n. i = int_of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
+  (is "?P = (?L & ?R)")
+proof (cases "i < 0")
+  case True thus ?thesis by simp
+next
+  case False
+  have "?P = ?L"
+  proof
+    assume ?P thus ?L using False by clarsimp
+  next
+    assume ?L thus ?P using False by simp
+  qed
+  with False show ?thesis by simp
+qed
 
 lemma split_nat [arith_split]:
   "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"