# HG changeset patch
# User huffman
# Date 1228437877 28800
# Node ID a301dc6c6a37f710c806f285055c1adb6888fec8
# Parent  13d6f120992bfc3cbeb95bf45899dd242a03ad6b# Parent  f88fbb0c4f17bbbeb044d41fd8806018d56730cf
merged.

diff -r f88fbb0c4f17 -r a301dc6c6a37 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Fri Dec 05 11:35:07 2008 +1100
+++ b/src/HOL/Groebner_Basis.thy	Thu Dec 04 16:44:37 2008 -0800
@@ -169,16 +169,20 @@
   proof qed (auto simp add: ring_simps power_Suc)
 
 lemmas nat_arith =
-  add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
+  add_nat_number_of
+  diff_nat_number_of
+  mult_nat_number_of
+  eq_nat_number_of
+  less_nat_number_of
 
 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
   by (simp add: numeral_1_eq_1)
+
 lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False
   if_True add_0 add_Suc add_number_of_left mult_number_of_left
   numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
-  numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1
-  iszero_number_of_Bit1 iszero_number_of_Bit0 nonzero_number_of_Min
-  iszero_number_of_Pls iszero_0 not_iszero_Numeral1
+  numeral_0_eq_0[symmetric] numerals[symmetric]
+  iszero_simps not_iszero_Numeral1
 
 lemmas semiring_norm = comp_arith
 
@@ -458,7 +462,6 @@
 declare zmod_eq_dvd_iff[algebra]
 declare nat_mod_eq_iff[algebra]
 
-
 subsection{* Groebner Bases for fields *}
 
 interpretation class_fieldgb:
@@ -607,14 +610,6 @@
              @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
              name = "ord_frac_simproc", proc = proc3, identifier = []}
 
-val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of",
-               "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]
-
-val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0",
-                 "add_Suc", "add_number_of_left", "mult_number_of_left",
-                 "Suc_eq_add_numeral_1"])@
-                 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
-                 @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps}
 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
            @{thm "divide_Numeral1"},
            @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
@@ -630,7 +625,7 @@
 in
 val comp_conv = (Simplifier.rewrite
 (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
-              addsimps ths addsimps comp_arith addsimps simp_thms
+              addsimps ths addsimps simp_thms
               addsimprocs field_cancel_numeral_factors
                addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
                             ord_frac_simproc]
diff -r f88fbb0c4f17 -r a301dc6c6a37 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Dec 05 11:35:07 2008 +1100
+++ b/src/HOL/Int.thy	Thu Dec 04 16:44:37 2008 -0800
@@ -855,7 +855,7 @@
     add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
 qed
 
-lemma neg_simps:
+lemma bin_less_0_simps:
   "Pls < 0 \<longleftrightarrow> False"
   "Min < 0 \<longleftrightarrow> True"
   "Bit0 w < 0 \<longleftrightarrow> w < 0"
@@ -908,7 +908,7 @@
     less_bin_lemma [of "Bit1 k"]
     less_bin_lemma [of "pred Pls"]
     less_bin_lemma [of "pred k"]
-  by (simp_all add: neg_simps succ_pred)
+  by (simp_all add: bin_less_0_simps succ_pred)
 
 text {* Less-than-or-equal *}
 
@@ -1187,6 +1187,12 @@
     by (auto simp add: iszero_def number_of_eq numeral_simps)
 qed
 
+lemmas iszero_simps =
+  iszero_0 not_iszero_1
+  iszero_number_of_Pls nonzero_number_of_Min
+  iszero_number_of_Bit0 iszero_number_of_Bit1
+(* iszero_number_of_Pls would never normally be used
+   because its lhs simplifies to "iszero 0" *)
 
 subsubsection {* The Less-Than Relation *}
 
@@ -1248,6 +1254,10 @@
   by (simp add: neg_def number_of_eq numeral_simps)
 qed
 
+lemmas neg_simps =
+  not_neg_0 not_neg_1
+  not_neg_number_of_Pls neg_number_of_Min
+  neg_number_of_Bit0 neg_number_of_Bit1
 
 text {* Less-Than or Equals *}
 
@@ -1314,13 +1324,8 @@
 lemmas rel_simps [simp] = 
   less_number_of less_bin_simps
   le_number_of le_bin_simps
-  eq_number_of eq_bin_simps
-  iszero_0 nonzero_number_of_Min
-  iszero_number_of_Bit0 iszero_number_of_Bit1
-  not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
-  neg_number_of_Min neg_number_of_Bit0 neg_number_of_Bit1
-(* iszero_number_of_Pls would never be used
-   because its lhs simplifies to "iszero 0" *)
+  eq_number_of_eq eq_bin_simps
+  iszero_simps neg_simps
 
 
 subsubsection {* Simplification of arithmetic when nested to the right. *}
@@ -1581,17 +1586,17 @@
 
 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
 lemmas less_special =
-  binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard]
-  binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard]
-  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard]
-  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard]
+  binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard]
+  binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard]
+  binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard]
+  binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard]
 
 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
 lemmas le_special =
-    binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard]
-    binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard]
-    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
-    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
+    binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard]
+    binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard]
+    binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard]
+    binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard]
 
 lemmas arith_special[simp] = 
        add_special diff_special eq_special less_special le_special
diff -r f88fbb0c4f17 -r a301dc6c6a37 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Fri Dec 05 11:35:07 2008 +1100
+++ b/src/HOL/NatBin.thy	Thu Dec 04 16:44:37 2008 -0800
@@ -111,8 +111,8 @@
      "int (number_of v) =  
          (if neg (number_of v :: int) then 0  
           else (number_of v :: int))"
-by (simp del: nat_number_of
-	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by simp
 
 
 subsubsection{*Successor *}
@@ -124,10 +124,9 @@
 
 lemma Suc_nat_number_of_add:
      "Suc (number_of v + n) =  
-        (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)" 
-by (simp del: nat_number_of 
-         add: nat_number_of_def neg_nat
-              Suc_nat_eq_nat_zadd1 number_of_succ) 
+        (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
+  unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
+  by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
 
 lemma Suc_nat_number_of [simp]:
      "Suc (number_of v) =  
@@ -145,7 +144,8 @@
          (if neg (number_of v :: int) then number_of v'  
           else if neg (number_of v' :: int) then number_of v  
           else number_of (v + v'))"
-by (simp add: neg_nat nat_number_of_def nat_add_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_add_distrib)
 
 
 subsubsection{*Subtraction *}
@@ -172,7 +172,8 @@
 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'))"
-by (simp add: neg_nat nat_number_of_def nat_mult_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_mult_distrib)
 
 
 subsubsection{*Quotient *}
@@ -181,7 +182,8 @@
      "(number_of v :: nat)  div  number_of v' =  
           (if neg (number_of v :: int) then 0  
            else nat (number_of v div number_of v'))"
-by (simp add: neg_nat nat_number_of_def nat_div_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_div_distrib)
 
 lemma one_div_nat_number_of [simp]:
      "Suc 0 div number_of v' = nat (1 div number_of v')" 
@@ -195,7 +197,8 @@
         (if neg (number_of v :: int) then 0  
          else if neg (number_of v' :: int) then number_of v  
          else nat (number_of v mod number_of v'))"
-by (simp add: neg_nat nat_number_of_def nat_mod_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_mod_distrib)
 
 lemma one_mod_nat_number_of [simp]:
      "Suc 0 mod number_of v' =