--- 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
--- 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"
--- 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)"
--- 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}
--- 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)
--- 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)
--- 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 =
--- 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;
--- 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
--- 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