# HG changeset patch
# User nipkow
# Date 1287944340 -7200
# Node ID c8a9eaaa2f5943e71101b322cb9553fc97c0c3b5
# Parent  6f012a209dac44c2e61d655c9ee2f735be966545
nat_number -> eval_nat_numeral

diff -r 6f012a209dac -r c8a9eaaa2f59 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Oct 24 20:19:00 2010 +0200
@@ -266,7 +266,7 @@
     proof cases
       assume "even l"
       then have "Suc l div 2 = l div 2"
-        by (simp add: nat_number even_nat_plus_one_div_two)
+        by (simp add: eval_nat_numeral even_nat_plus_one_div_two)
       moreover
       from Suc have "l < k" by simp
       with 1 have "\<And>P. Ipol ls (pow l P) = Ipol ls P ^ l" by simp
diff -r 6f012a209dac -r c8a9eaaa2f59 src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/Library/Char_nat.thy	Sun Oct 24 20:19:00 2010 +0200
@@ -171,7 +171,7 @@
   proof -
     fix n m
     have nat_of_nibble_less_eq_15: "\<And>n. nat_of_nibble n \<le> 15"
-      using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: nat_number)
+      using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: eval_nat_numeral)
     have less_eq_240: "nat_of_nibble n * 16 \<le> 240"
       using nat_of_nibble_less_eq_15 by auto
     have "nat_of_nibble n * 16 + nat_of_nibble m \<le> 240 + 15"
diff -r 6f012a209dac -r c8a9eaaa2f59 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/Library/Ramsey.thy	Sun Oct 24 20:19:00 2010 +0200
@@ -218,7 +218,7 @@
    "\<exists>Y t. Y \<subseteq> Z & infinite Y & t < s & (\<forall>x\<in>Y. \<forall>y\<in>Y. x\<noteq>y --> f{x,y} = t)"
 proof -
   have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
-    using part by (fastsimp simp add: nat_number card_Suc_eq)
+    using part by (fastsimp simp add: eval_nat_numeral card_Suc_eq)
   obtain Y t 
     where "Y \<subseteq> Z" "infinite Y" "t < s"
           "(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
diff -r 6f012a209dac -r c8a9eaaa2f59 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/List.thy	Sun Oct 24 20:19:00 2010 +0200
@@ -262,9 +262,9 @@
 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
-@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number')}\\
-@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\
-@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\
+@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def eval_nat_numeral)}\\
+@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
+@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
 @{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}
 \end{tabular}}
 \caption{Characteristic examples}
diff -r 6f012a209dac -r c8a9eaaa2f59 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sun Oct 24 20:19:00 2010 +0200
@@ -258,7 +258,7 @@
 lemma bounded_append [simp]:
   "check_bounded append_ins [(Suc 0, 2, 8, Xcpt NullPointer)]"
   apply (simp add: check_bounded_def)
-  apply (simp add: nat_number append_ins_def)
+  apply (simp add: eval_nat_numeral append_ins_def)
   apply (rule allI, rule impI)
   apply (elim pc_end pc_next pc_0)
   apply auto
@@ -327,7 +327,7 @@
 
 lemma bounded_makelist [simp]: "check_bounded make_list_ins []"
   apply (simp add: check_bounded_def)
-  apply (simp add: nat_number make_list_ins_def)
+  apply (simp add: eval_nat_numeral make_list_ins_def)
   apply (rule allI, rule impI)
   apply (elim pc_end pc_next pc_0)
   apply auto
@@ -343,7 +343,7 @@
   "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
   apply (simp add: wt_method_def)
   apply (simp add: make_list_ins_def phi_makelist_def)
-  apply (simp add: wt_start_def nat_number)
+  apply (simp add: wt_start_def eval_nat_numeral)
   apply (simp add: wt_instr_def)
   apply clarify
   apply (elim pc_end pc_next pc_0)
diff -r 6f012a209dac -r c8a9eaaa2f59 src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Oct 24 20:19:00 2010 +0200
@@ -1042,9 +1042,9 @@
 lemma setprod_1: "setprod f {(1::nat)..1} = f 1" by simp
 
 lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2"
-  by (simp add: nat_number setprod_numseg mult_commute)
+  by (simp add: eval_nat_numeral setprod_numseg mult_commute)
 lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3"
-  by (simp add: nat_number setprod_numseg mult_commute)
+  by (simp add: eval_nat_numeral setprod_numseg mult_commute)
 
 lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
   by (simp add: det_def sign_id UNIV_1)
diff -r 6f012a209dac -r c8a9eaaa2f59 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/Nat_Numeral.thy	Sun Oct 24 20:19:00 2010 +0200
@@ -693,11 +693,7 @@
 apply (simp only: nat_add_distrib, simp)
 done
 
-lemmas nat_number =
-  nat_number_of_Pls nat_number_of_Min
-  nat_number_of_Bit0 nat_number_of_Bit1
-
-lemmas nat_number' =
+lemmas eval_nat_numeral =
   nat_number_of_Bit0 nat_number_of_Bit1
 
 lemmas nat_arith =
diff -r 6f012a209dac -r c8a9eaaa2f59 src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Sun Oct 24 20:19:00 2010 +0200
@@ -826,7 +826,7 @@
 end;
 
 val nat_exp_ss =
-  HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
+  HOL_basic_ss addsimps (@{thms eval_nat_numeral} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
     addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}];
 
 fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
diff -r 6f012a209dac -r c8a9eaaa2f59 src/HOL/ex/HarmonicSeries.thy
--- a/src/HOL/ex/HarmonicSeries.thy	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/ex/HarmonicSeries.thy	Sun Oct 24 20:19:00 2010 +0200
@@ -153,7 +153,7 @@
              (auto simp: atLeastSucAtMost_greaterThanAtMost)
         also have
           "\<dots> = ((\<Sum>n\<in>{2..2::nat}. 1/real n) + 1/(real (1::nat)))"
-          by (simp add: nat_number)
+          by (simp add: eval_nat_numeral)
         also have
           "\<dots> =  1/(real (2::nat)) + 1/(real (1::nat))" by simp
         finally have
diff -r 6f012a209dac -r c8a9eaaa2f59 src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/ex/NatSum.thy	Sun Oct 24 20:19:00 2010 +0200
@@ -70,9 +70,9 @@
   have "(\<Sum>i = 0..Suc n. i)^2 =
         (\<Sum>i = 0..n. i^3) + (2*(\<Sum>i = 0..n. i)*(n+1) + (n+1)^2)"
     (is "_ = ?A + ?B")
-    using Suc by(simp add:nat_number)
+    using Suc by(simp add:eval_nat_numeral)
   also have "?B = (n+1)^3"
-    using sum_of_naturals by(simp add:nat_number)
+    using sum_of_naturals by(simp add:eval_nat_numeral)
   also have "?A + (n+1)^3 = (\<Sum>i=0..Suc n. i^3)" by simp
   finally show ?case .
 qed