--- a/NEWS Tue Jun 23 21:07:39 2009 +0200
+++ b/NEWS Wed Jun 24 09:41:14 2009 +0200
@@ -43,6 +43,11 @@
* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions
Set.Pow_def and Set.image_def. INCOMPATIBILITY.
+* Renamed theorems:
+Suc_eq_add_numeral_1 -> Suc_eq_plus1
+Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
+Suc_plus1 -> Suc_eq_plus1
+
* Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.:
DatatypePackage ~> Datatype
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Jun 24 09:41:14 2009 +0200
@@ -422,7 +422,7 @@
have "\<bar> real x \<bar> \<le> 1" using `0 \<le> real x` `real x \<le> 1` by auto
from mp[OF summable_Leibniz(2)[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]] prem, THEN spec, of m, unfolded `2 * m = n`]
- show ?thesis unfolding arctan_series[OF `\<bar> real x \<bar> \<le> 1`] Suc_plus1 .
+ show ?thesis unfolding arctan_series[OF `\<bar> real x \<bar> \<le> 1`] Suc_eq_plus1 .
qed auto
note arctan_bounds = this[unfolded atLeastAtMost_iff]
@@ -1179,7 +1179,7 @@
proof (induct n arbitrary: x)
case (Suc n)
have split_pi_off: "x + real (Suc n) * 2 * pi = (x + real n * 2 * pi) + 2 * pi"
- unfolding Suc_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
+ unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
show ?case unfolding split_pi_off using Suc by auto
qed auto
@@ -1676,7 +1676,7 @@
using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
have "norm x < 1" using assms by auto
- have "?a ----> 0" unfolding Suc_plus1[symmetric] inverse_eq_divide[symmetric]
+ have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric]
using LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto
{ fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) }
{ fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]
--- a/src/HOL/Decision_Procs/cooper_tac.ML Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Jun 24 09:41:14 2009 +0200
@@ -31,7 +31,7 @@
val split_zmod = @{thm split_zmod};
val mod_div_equality' = @{thm mod_div_equality'};
val split_div' = @{thm split_div'};
-val Suc_plus1 = @{thm Suc_plus1};
+val Suc_eq_plus1 = @{thm Suc_eq_plus1};
val imp_le_cong = @{thm imp_le_cong};
val conj_le_cong = @{thm conj_le_cong};
val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
@@ -81,11 +81,11 @@
@{thm mod_by_0}, @{thm div_by_0},
@{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
@{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
- Suc_plus1]
+ Suc_eq_plus1]
addsimps @{thms add_ac}
addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
val simpset0 = HOL_basic_ss
- addsimps [mod_div_equality', Suc_plus1]
+ addsimps [mod_div_equality', Suc_eq_plus1]
addsimps comp_arith
addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
(* Simp rules for changing (n::int) to int n *)
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed Jun 24 09:41:14 2009 +0200
@@ -35,7 +35,7 @@
val split_zmod = @{thm split_zmod};
val mod_div_equality' = @{thm mod_div_equality'};
val split_div' = @{thm split_div'};
-val Suc_plus1 = @{thm Suc_plus1};
+val Suc_eq_plus1 = @{thm Suc_eq_plus1};
val imp_le_cong = @{thm imp_le_cong};
val conj_le_cong = @{thm conj_le_cong};
val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
--- a/src/HOL/Decision_Procs/mir_tac.ML Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Jun 24 09:41:14 2009 +0200
@@ -26,7 +26,7 @@
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"])@
+ "Suc_eq_plus1"])@
(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"},
@@ -50,7 +50,6 @@
val split_zmod = @{thm "split_zmod"};
val mod_div_equality' = @{thm "mod_div_equality'"};
val split_div' = @{thm "split_div'"};
-val Suc_plus1 = @{thm "Suc_plus1"};
val imp_le_cong = @{thm "imp_le_cong"};
val conj_le_cong = @{thm "conj_le_cong"};
val mod_add_eq = @{thm "mod_add_eq"} RS sym;
@@ -104,11 +103,11 @@
@{thm "mod_self"}, @{thm "zmod_self"},
@{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
@{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
- @{thm "Suc_plus1"}]
+ @{thm "Suc_eq_plus1"}]
addsimps @{thms add_ac}
addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
val simpset0 = HOL_basic_ss
- addsimps [mod_div_equality', Suc_plus1]
+ addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
addsimps comp_ths
addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}]
(* Simp rules for changing (n::int) to int n *)
--- a/src/HOL/Groebner_Basis.thy Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Groebner_Basis.thy Wed Jun 24 09:41:14 2009 +0200
@@ -180,7 +180,7 @@
lemmas comp_arith =
Let_def arith_simps nat_arith rel_simps neg_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_1_eq_1[symmetric] Suc_eq_plus1
numeral_0_eq_0[symmetric] numerals[symmetric]
iszero_simps not_iszero_Numeral1
--- a/src/HOL/Import/HOL/arithmetic.imp Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp Wed Jun 24 09:41:14 2009 +0200
@@ -43,7 +43,7 @@
"TWO" > "HOL4Base.arithmetic.TWO"
"TIMES2" > "NatSimprocs.nat_mult_2"
"SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1"
- "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_add_numeral_1_left"
+ "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_plus1_left"
"SUC_NOT" > "Nat.nat.simps_2"
"SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
"SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
@@ -265,7 +265,7 @@
"ADD_CLAUSES" > "HOL4Base.arithmetic.ADD_CLAUSES"
"ADD_ASSOC" > "Finite_Set.AC_add.f.AC_1"
"ADD_0" > "Finite_Set.AC_add.f_e.ident"
- "ADD1" > "Presburger.Suc_plus1"
+ "ADD1" > "Nat_Numeral.Suc_eq_plus1"
"ADD" > "HOL4Compat.ADD"
end
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Jun 24 09:41:14 2009 +0200
@@ -1615,7 +1615,7 @@
fix v assume v: "v \<in> {xs \<in> natpermute n (Suc k). n \<in> set xs}"
let ?ths = "(\<Prod>j\<in>{0..k}. a $ v ! j) = a $ n * (?r$0)^k"
from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]"
- unfolding Suc_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps)
+ unfolding Suc_eq_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps)
have "(\<Prod>j\<in>{0..k}. a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then a $ n else r (Suc k) (b$0))"
apply (rule setprod_cong, simp)
using i a0 by (simp del: replicate.simps)
@@ -1651,7 +1651,7 @@
from H have "b$n = a^Suc k $ n" by (simp add: fps_eq_iff)
also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn"
unfolding fps_power_nth_Suc
- using setsum_Un_disjoint[OF f d, unfolded Suc_plus1[symmetric],
+ using setsum_Un_disjoint[OF f d, unfolded Suc_eq_plus1[symmetric],
unfolded eq, of ?g] by simp
also have "\<dots> = of_nat (k+1) * a $ n * (?r $ 0)^k + setsum ?f ?Pnknn" unfolding th0 th1 ..
finally have "of_nat (k+1) * a $ n * (?r $ 0)^k = b$n - setsum ?f ?Pnknn" by simp
--- a/src/HOL/MetisExamples/BT.thy Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/MetisExamples/BT.thy Wed Jun 24 09:41:14 2009 +0200
@@ -171,7 +171,7 @@
ML {*AtpWrapper.problem_name := "BT__n_leaves_bt_map"*}
lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
apply (induct t)
- apply (metis One_nat_def Suc_eq_add_numeral_1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
+ apply (metis One_nat_def Suc_eq_plus1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
apply (metis bt_map.simps(2) n_leaves.simps(2))
done
--- a/src/HOL/Nat_Numeral.thy Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Wed Jun 24 09:41:14 2009 +0200
@@ -521,10 +521,10 @@
subsubsection{*Arith *}
-lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
+lemma Suc_eq_plus1: "Suc n = n + 1"
by (simp add: numerals)
-lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
+lemma Suc_eq_plus1_left: "Suc n = 1 + n"
by (simp add: numerals)
(* These two can be useful when m = number_of... *)
--- a/src/HOL/Presburger.thy Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Presburger.thy Wed Jun 24 09:41:14 2009 +0200
@@ -399,7 +399,6 @@
lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (Int.Bit0 n) \<and> (0::int) <= number_of (Int.Bit1 n)"
by simp
lemma number_of2: "(0::int) <= Numeral0" by simp
-lemma Suc_plus1: "Suc n = n + 1" by simp
text {*
\medskip Specific instances of congruence rules, to prevent
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Wed Jun 24 09:41:14 2009 +0200
@@ -61,7 +61,7 @@
(HOL_basic_ss
addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
@ [if_False, if_True, @{thm add_0}, @{thm add_Suc},
- @{thm add_number_of_left}, @{thm Suc_eq_add_numeral_1}]
+ @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
@ map (fn th => th RS sym) @{thms numerals}));
val nat_mul_conv = nat_add_conv;
--- a/src/HOL/Tools/Qelim/presburger.ML Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML Wed Jun 24 09:41:14 2009 +0200
@@ -118,7 +118,7 @@
val ss2 = HOL_basic_ss
addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
@{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"},
- @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_plus1"}]
+ @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
val div_mod_ss = HOL_basic_ss addsimps simp_thms
@ map (symmetric o mk_meta_eq)
@@ -129,7 +129,7 @@
@{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
@{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"},
@{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
- @{thm "mod_1"}, @{thm "Suc_plus1"}]
+ @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
@ @{thms add_ac}
addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Wed Jun 24 09:41:14 2009 +0200
@@ -152,7 +152,7 @@
fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
- [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
+ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -240,7 +240,7 @@
val prove_conv = Arith_Data.prove_conv_nohyps
fun trans_tac _ = Arith_Data.trans_tac
- val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
+ val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac}
val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -266,7 +266,7 @@
fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps
- numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
+ numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
--- a/src/HOL/Transcendental.thy Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Transcendental.thy Wed Jun 24 09:41:14 2009 +0200
@@ -2242,7 +2242,7 @@
lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x"
proof (induct n arbitrary: x)
case (Suc n)
- have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
+ have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
show ?case unfolding split_pi_off using Suc by auto
qed auto
@@ -2779,12 +2779,12 @@
show ?thesis
proof (cases "0 \<le> x")
case True from mono[OF this `x \<le> 1`, THEN allI]
- show ?thesis unfolding Suc_plus1[symmetric] by (rule mono_SucI2)
+ show ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI2)
next
case False hence "0 \<le> -x" and "-x \<le> 1" using `-1 \<le> x` by auto
from mono[OF this]
have "\<And>n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<ge> 1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \<le> -x` by auto
- thus ?thesis unfolding Suc_plus1[symmetric] by (rule mono_SucI1[OF allI])
+ thus ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI1[OF allI])
qed
qed
qed
@@ -2800,13 +2800,13 @@
case True hence "norm x < 1" by auto
from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
- unfolding inverse_eq_divide Suc_plus1 by simp
+ unfolding inverse_eq_divide Suc_eq_plus1 by simp
then show ?thesis using pos2 by (rule LIMSEQ_linear)
next
case False hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" unfolding One_nat_def by auto
from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] LIMSEQ_const[of x]]
- show ?thesis unfolding n_eq Suc_plus1 by auto
+ show ?thesis unfolding n_eq Suc_eq_plus1 by auto
qed
qed
@@ -2921,7 +2921,7 @@
qed
have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
- unfolding Suc_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero by auto
+ unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero by auto
have "suminf (?c x) - arctan x = 0"
proof (cases "x = 0")
--- a/src/HOL/Word/BinBoolList.thy Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Word/BinBoolList.thy Wed Jun 24 09:41:14 2009 +0200
@@ -658,7 +658,7 @@
apply (unfold bl_to_bin_def)
apply (induct n)
apply simp
- apply (simp only: Suc_eq_add_numeral_1 replicate_add
+ apply (simp only: Suc_eq_plus1 replicate_add
append_Cons [symmetric] bl_to_bin_aux_append)
apply simp
done