# HG changeset patch
# User huffman
# Date 1228634384 28800
# Node ID 4546ccf7294277de9d0c1f8aa53fdbf3a756d269
# Parent  e515f42d1db7db702a0325a3b04b918ee9962641# Parent  3ad09b8d2534ae0927126d54349fb0930bf1508f
merged.

diff -r 3ad09b8d2534 -r 4546ccf72942 src/HOL/Arith_Tools.thy
--- a/src/HOL/Arith_Tools.thy	Sat Dec 06 12:18:05 2008 +0100
+++ b/src/HOL/Arith_Tools.thy	Sat Dec 06 23:19:44 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
diff -r 3ad09b8d2534 -r 4546ccf72942 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Sat Dec 06 12:18:05 2008 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy	Sat Dec 06 23:19:44 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]:
@@ -165,6 +165,58 @@
   unfolding iSuc_plus_1 by (simp_all add: add_ac)
 
 
+subsection {* Multiplication *}
+
+instantiation inat :: comm_semiring_1
+begin
+
+definition
+  times_inat_def [code del]:
+  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
+    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
+
+lemma times_inat_simps [simp, code]:
+  "Fin m * Fin n = Fin (m * n)"
+  "\<infinity> * \<infinity> = \<infinity>"
+  "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
+  "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
+  unfolding times_inat_def zero_inat_def
+  by (simp_all split: inat.split)
+
+instance proof
+  fix a b c :: inat
+  show "(a * b) * c = a * (b * c)"
+    unfolding times_inat_def zero_inat_def
+    by (simp split: inat.split)
+  show "a * b = b * a"
+    unfolding times_inat_def zero_inat_def
+    by (simp split: inat.split)
+  show "1 * a = a"
+    unfolding times_inat_def zero_inat_def one_inat_def
+    by (simp split: inat.split)
+  show "(a + b) * c = a * c + b * c"
+    unfolding times_inat_def zero_inat_def
+    by (simp split: inat.split add: left_distrib)
+  show "0 * a = 0"
+    unfolding times_inat_def zero_inat_def
+    by (simp split: inat.split)
+  show "a * 0 = 0"
+    unfolding times_inat_def zero_inat_def
+    by (simp split: inat.split)
+  show "(0::inat) \<noteq> 1"
+    unfolding zero_inat_def one_inat_def
+    by simp
+qed
+
+end
+
+lemma mult_iSuc: "iSuc m * n = n + m * n"
+  unfolding iSuc_plus_1 by (simp add: ring_simps)
+
+lemma mult_iSuc_right: "m * iSuc n = m + m * n"
+  unfolding iSuc_plus_1 by (simp add: ring_simps)
+
+
 subsection {* Ordering *}
 
 instantiation inat :: ordered_ab_semigroup_add
@@ -201,6 +253,15 @@
 
 end
 
+instance inat :: pordered_comm_semiring
+proof
+  fix a b c :: inat
+  assume "a \<le> b" and "0 \<le> c"
+  thus "c * a \<le> c * b"
+    unfolding times_inat_def less_eq_inat_def zero_inat_def
+    by (simp split: inat.splits)
+qed
+
 lemma inat_ord_number [simp]:
   "(number_of m \<Colon> inat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
   "(number_of m \<Colon> inat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
diff -r 3ad09b8d2534 -r 4546ccf72942 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Sat Dec 06 12:18:05 2008 +0100
+++ b/src/HOL/NatBin.thy	Sat Dec 06 23:19:44 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)
 
 
@@ -258,15 +258,21 @@
 
 subsubsection{*Less-than (<) *}
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma less_nat_number_of [simp]:
-     "((number_of v :: nat) < number_of v') =  
-         (if neg (number_of v :: int) then neg (number_of (uminus v') :: int)  
-          else neg (number_of (v + uminus v') :: int))"
-  unfolding neg_def nat_number_of_def number_of_is_id
+  "(number_of v :: nat) < number_of v' \<longleftrightarrow>
+    (if v < v' then Int.Pls < v' else False)"
+  unfolding nat_number_of_def number_of_is_id numeral_simps
   by auto
 
 
+subsubsection{*Less-than-or-equal *}
+
+lemma le_nat_number_of [simp]:
+  "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
+    (if v \<le> v' then True else v \<le> Int.Pls)"
+  unfolding nat_number_of_def number_of_is_id numeral_simps
+  by auto
+
 (*Maps #n to n for n = 0, 1, 2*)
 lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
 
@@ -440,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])
@@ -699,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
 
diff -r 3ad09b8d2534 -r 4546ccf72942 src/HOL/Tools/ComputeNumeral.thy
--- a/src/HOL/Tools/ComputeNumeral.thy	Sat Dec 06 12:18:05 2008 +0100
+++ b/src/HOL/Tools/ComputeNumeral.thy	Sat Dec 06 23:19:44 2008 -0800
@@ -129,7 +129,8 @@
 
 (* Addition for nat *)
 lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))"
-  by (auto simp add: number_of_is_id)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by auto
 
 (* Subtraction for nat *)
 lemma natsub: "(number_of x) - ((number_of y)::nat) = 
@@ -140,18 +141,14 @@
 (* Multiplication for nat *)
 lemma natmul: "(number_of x) * ((number_of y)::nat) = 
   (if neg x then 0 else (if neg y then 0 else number_of (x * y)))"
-  apply (auto simp add: number_of_is_id neg_def iszero_def)
-  apply (case_tac "x > 0")
-  apply auto
-  apply (rule order_less_imp_le)
-  apply (simp add: mult_strict_left_mono[where a=y and b=0 and c=x, simplified])
-  done
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_mult_distrib)
 
 lemma nateq: "(((number_of x)::nat) = (number_of y)) = ((lezero x \<and> lezero y) \<or> (x = y))"
   by (auto simp add: iszero_def lezero_def neg_def number_of_is_id)
 
 lemma natless: "(((number_of x)::nat) < (number_of y)) = ((x < y) \<and> (\<not> (lezero y)))"
-  by (auto simp add: number_of_is_id neg_def lezero_def)
+  by (simp add: lezero_def numeral_simps not_le)
 
 lemma natle: "(((number_of x)::nat) \<le> (number_of y)) = (y < x \<longrightarrow> lezero x)"
   by (auto simp add: number_of_is_id lezero_def nat_number_of_def)