# HG changeset patch # User nipkow # Date 1245829274 -7200 # Node ID 05c92381363cfda078e85cbeb2b6fd0cf6f9c1f4 # Parent c8a590599cb595a185216569832da12a49472789 corrected and unified thm names diff -r c8a590599cb5 -r 05c92381363c NEWS --- 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 diff -r c8a590599cb5 -r 05c92381363c src/HOL/Decision_Procs/Approximation.thy --- 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 "\ real x \ \ 1" using `0 \ real x` `real x \ 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 `\ real x \ \ 1`] Suc_plus1 . + show ?thesis unfolding arctan_series[OF `\ real x \ \ 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 \ 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 \ ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \ x`) } { fix n have "?a (Suc n) \ ?a n" unfolding inverse_eq_divide[symmetric] diff -r c8a590599cb5 -r 05c92381363c src/HOL/Decision_Procs/cooper_tac.ML --- 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 *) diff -r c8a590599cb5 -r 05c92381363c src/HOL/Decision_Procs/ferrack_tac.ML --- 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; diff -r c8a590599cb5 -r 05c92381363c src/HOL/Decision_Procs/mir_tac.ML --- 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 *) diff -r c8a590599cb5 -r 05c92381363c src/HOL/Groebner_Basis.thy --- 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 diff -r c8a590599cb5 -r 05c92381363c src/HOL/Import/HOL/arithmetic.imp --- 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 diff -r c8a590599cb5 -r 05c92381363c src/HOL/Library/Formal_Power_Series.thy --- 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 \ {xs \ natpermute n (Suc k). n \ set xs}" let ?ths = "(\j\{0..k}. a $ v ! j) = a $ n * (?r$0)^k" from v obtain i where i: "i \ {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 "(\j\{0..k}. a $ v ! j) = (\j\{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 "\ = 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 diff -r c8a590599cb5 -r 05c92381363c src/HOL/MetisExamples/BT.thy --- 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 diff -r c8a590599cb5 -r 05c92381363c src/HOL/Nat_Numeral.thy --- 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... *) diff -r c8a590599cb5 -r 05c92381363c src/HOL/Presburger.thy --- 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 \ (0::int) <= number_of (Int.Bit0 n) \ (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 diff -r c8a590599cb5 -r 05c92381363c src/HOL/Tools/Groebner_Basis/normalizer.ML --- 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; diff -r c8a590599cb5 -r 05c92381363c src/HOL/Tools/Qelim/presburger.ML --- 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 diff -r c8a590599cb5 -r 05c92381363c src/HOL/Tools/nat_numeral_simprocs.ML --- 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)) diff -r c8a590599cb5 -r 05c92381363c src/HOL/Transcendental.thy --- 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 \ x") case True from mono[OF this `x \ 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 \ -x" and "-x \ 1" using `-1 \ x` by auto from mono[OF this] have "\n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \ 1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \ -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 "(\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 \ x = 1" using `\x\ \ 1` by auto hence n_eq: "\ 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") diff -r c8a590599cb5 -r 05c92381363c src/HOL/Word/BinBoolList.thy --- 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