--- a/src/HOL/Arith_Tools.thy Fri Dec 05 17:35:22 2008 -0800
+++ b/src/HOL/Arith_Tools.thy Sat Dec 06 19:39:53 2008 -0800
@@ -40,7 +40,7 @@
text{*No longer required as a simprule because of the @{text inverse_fold}
simproc*}
lemma Suc_diff_number_of:
- "neg (number_of (uminus v)::int) ==>
+ "Int.Pls < v ==>
Suc m - (number_of v) = m - (number_of (Int.pred v))"
apply (subst Suc_diff_eq_diff_pred)
apply simp
--- a/src/HOL/Library/Nat_Infinity.thy Fri Dec 05 17:35:22 2008 -0800
+++ b/src/HOL/Library/Nat_Infinity.thy Sat Dec 06 19:39:53 2008 -0800
@@ -146,8 +146,8 @@
by (simp_all add: plus_inat_def zero_inat_def split: inat.splits)
lemma plus_inat_number [simp]:
- "(number_of k \<Colon> inat) + number_of l = (if neg (number_of k \<Colon> int) then number_of l
- else if neg (number_of l \<Colon> int) then number_of k else number_of (k + l))"
+ "(number_of k \<Colon> inat) + number_of l = (if k < Int.Pls then number_of l
+ else if l < Int.Pls then number_of k else number_of (k + l))"
unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
lemma iSuc_number [simp]:
--- a/src/HOL/NatBin.thy Fri Dec 05 17:35:22 2008 -0800
+++ b/src/HOL/NatBin.thy Sat Dec 06 19:39:53 2008 -0800
@@ -141,10 +141,10 @@
(*"neg" is used in rewrite rules for binary comparisons*)
lemma add_nat_number_of [simp]:
"(number_of v :: nat) + number_of v' =
- (if neg (number_of v :: int) then number_of v'
- else if neg (number_of v' :: int) then number_of v
+ (if v < Int.Pls then number_of v'
+ else if v' < Int.Pls then number_of v
else number_of (v + v'))"
- unfolding nat_number_of_def number_of_is_id neg_def
+ unfolding nat_number_of_def number_of_is_id numeral_simps
by (simp add: nat_add_distrib)
@@ -160,19 +160,19 @@
lemma diff_nat_number_of [simp]:
"(number_of v :: nat) - number_of v' =
- (if neg (number_of v' :: int) then number_of v
+ (if v' < Int.Pls then number_of v
else let d = number_of (v + uminus v') in
if neg d then 0 else nat d)"
-by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def)
-
+ unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
+ by auto
subsubsection{*Multiplication *}
lemma mult_nat_number_of [simp]:
"(number_of v :: nat) * number_of v' =
- (if neg (number_of v :: int) then 0 else number_of (v * v'))"
- unfolding nat_number_of_def number_of_is_id neg_def
+ (if v < Int.Pls then 0 else number_of (v * v'))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
by (simp add: nat_mult_distrib)
@@ -446,17 +446,18 @@
text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
lemma eq_number_of_0 [simp]:
- "number_of v = (0::nat) \<longleftrightarrow> number_of v \<le> (0::int)"
- unfolding nat_number_of_def number_of_is_id by auto
+ "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by auto
lemma eq_0_number_of [simp]:
- "(0::nat) = number_of v \<longleftrightarrow> number_of v \<le> (0::int)"
+ "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
by (rule trans [OF eq_sym_conv eq_number_of_0])
lemma less_0_number_of [simp]:
- "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
-by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
-
+ "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by simp
lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
@@ -705,7 +706,7 @@
lemma nat_number_of_mult_left:
"number_of v * (number_of v' * (k::nat)) =
- (if neg (number_of v :: int) then 0
+ (if v < Int.Pls then 0
else number_of (v * v') * k)"
by simp