--- a/src/HOL/Integ/IntArith.thy Thu Mar 06 12:22:28 2003 +0100
+++ b/src/HOL/Integ/IntArith.thy Thu Mar 06 15:02:51 2003 +0100
@@ -14,6 +14,9 @@
"(abs (z::int) = w) = (z = w \<and> 0 <= z \<or> z = -w \<and> z < 0)"
by (auto simp add: zabs_def)
+lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
+ by simp
+
lemma split_nat[arith_split]:
"P(nat(i::int)) = ((ALL n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
(is "?P = (?L & ?R)")
@@ -107,3 +110,4 @@
done
end
+