# HG changeset patch # User wenzelm # Date 1305227643 -7200 # Node ID 4db4a8b164c1e62fe8d483dea05a89194fbfb7df # Parent e6d920bea7a6816022067cc2b7a4c79f4af5343f modernized simproc_setup; misc tuning and simplification; diff -r e6d920bea7a6 -r 4db4a8b164c1 src/HOL/Algebra/abstract/Ideal2.thy --- a/src/HOL/Algebra/abstract/Ideal2.thy Thu May 12 18:18:06 2011 +0200 +++ b/src/HOL/Algebra/abstract/Ideal2.thy Thu May 12 21:14:03 2011 +0200 @@ -115,8 +115,9 @@ apply (rule subsetI) apply (drule InterD) prefer 2 apply assumption - apply (tactic {* auto_tac (@{claset} addIs [@{thm is_ideal_2}], - @{simpset} delsimprocs [ring_simproc]) *}) + using [[simproc del: ring]] + apply (auto intro: is_ideal_2) + using [[simproc ring]] apply (rule_tac x = "1" in exI) apply (rule_tac x = "0" in exI) apply (rule_tac [2] x = "0" in exI) @@ -283,8 +284,8 @@ apply (drule_tac f = "op* aa" in arg_cong) apply (simp add: r_distr) apply (erule subst) - apply (tactic {* asm_simp_tac (@{simpset} addsimps [@{thm m_assoc} RS sym] - delsimprocs [ring_simproc]) 1 *}) + using [[simproc del: ring]] + apply (simp add: m_assoc [symmetric]) done (* Fields are Pid *) diff -r e6d920bea7a6 -r 4db4a8b164c1 src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Thu May 12 18:18:06 2011 +0200 +++ b/src/HOL/Algebra/abstract/Ring2.thy Thu May 12 21:14:03 2011 +0200 @@ -266,31 +266,22 @@ show "0 + x = x" by (rule l_zero) qed -ML {* - local - val lhss = - ["t + u::'a::ring", - "t - u::'a::ring", - "t * u::'a::ring", - "- t::'a::ring"]; - fun proc ss t = - let val rew = Goal.prove (Simplifier.the_context ss) [] [] - (HOLogic.mk_Trueprop - (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) - (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1) - |> mk_meta_eq; - val (t', u) = Logic.dest_equals (Thm.prop_of rew); - in if t' aconv u - then NONE - else SOME rew - end; - in - val ring_simproc = Simplifier.simproc_global @{theory} "ring" lhss (K proc); - end; +simproc_setup + ring ("t + u::'a::ring" | "t - u::'a::ring" | "t * u::'a::ring" | "- t::'a::ring") = +{* + fn _ => fn ss => fn ct => + let + val ctxt = Simplifier.the_context ss; + val {t, T, maxidx, ...} = Thm.rep_cterm ct; + val rew = + Goal.prove ctxt [] [] + (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, Var (("x", maxidx + 1), T)))) + (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1) + |> mk_meta_eq; + val (t', u) = Logic.dest_equals (Thm.prop_of rew); + in if t' aconv u then NONE else SOME rew end *} -ML {* Addsimprocs [ring_simproc] *} - lemma natsum_ldistr: "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}" by (induct n) simp_all @@ -444,7 +435,8 @@ lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1" apply (unfold inverse_def dvd_def) - apply (tactic {* asm_full_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *}) + using [[simproc del: ring]] + apply simp apply clarify apply (rule theI) apply assumption diff -r e6d920bea7a6 -r 4db4a8b164c1 src/HOL/Algebra/poly/LongDiv.thy --- a/src/HOL/Algebra/poly/LongDiv.thy Thu May 12 18:18:06 2011 +0200 +++ b/src/HOL/Algebra/poly/LongDiv.thy Thu May 12 21:14:03 2011 +0200 @@ -130,27 +130,33 @@ apply (rule_tac x = "((% (q,r,k) . (monom (lcoeff g ^ k * lcoeff x) (deg x - deg g) + q)) xa, (% (q,r,k) . r) xa, (% (q,r,k) . Suc k) xa) " in exI) apply clarify apply (drule sym) - apply (tactic {* simp_tac (@{simpset} addsimps [@{thm l_distr}, @{thm a_assoc}] - delsimprocs [ring_simproc]) 1 *}) - apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *}) - apply (tactic {* simp_tac (@{simpset} addsimps [@{thm minus_def}, @{thm smult_r_distr}, - @{thm smult_r_minus}, @{thm monom_mult_smult}, @{thm smult_assoc2}] - delsimprocs [ring_simproc]) 1 *}) + using [[simproc del: ring]] + apply (simp (no_asm_use) add: l_distr a_assoc) + apply (simp (no_asm_simp)) + apply (simp (no_asm_use) add: minus_def smult_r_distr smult_r_minus + monom_mult_smult smult_assoc2) + using [[simproc ring]] apply (simp add: smult_assoc1 [symmetric]) done -ML {* - bind_thm ("long_div_ring_aux", - simplify (@{simpset} addsimps [@{thm eucl_size_def}] - delsimprocs [ring_simproc]) (@{thm long_div_eucl_size})) -*} +lemma long_div_ring_aux: + "(g :: 'a::ring up) ~= 0 ==> + Ex (\(q, r, k). lcoeff g ^ k *s f = q * g + r \ + (if r = 0 then 0 else deg r + 1) < (if g = 0 then 0 else deg g + 1))" +proof - + note [[simproc del: ring]] + assume "g ~= 0" + then show ?thesis + by (rule long_div_eucl_size [simplified eucl_size_def]) +qed lemma long_div_ring: "!!g::('a::ring up). g ~= 0 ==> Ex (% (q, r, k). (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))" apply (frule_tac f = f in long_div_ring_aux) - apply (tactic {* auto_tac (@{claset}, @{simpset} delsimprocs [ring_simproc]) *}) + using [[simproc del: ring]] + apply auto apply (case_tac "aa = 0") apply blast (* case "aa ~= 0 *) @@ -168,9 +174,9 @@ apply clarify apply (rule conjI) apply (drule sym) - apply (tactic {* asm_simp_tac - (@{simpset} addsimps [@{thm smult_r_distr} RS sym, @{thm smult_assoc2}] - delsimprocs [ring_simproc]) 1 *}) + using [[simproc del: ring]] + apply (simp (no_asm_simp) add: smult_r_distr [symmetric] smult_assoc2) + using [[simproc ring]] apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric]) (* degree property *) apply (erule disjE) @@ -194,7 +200,6 @@ lemma diff_zero_imp_eq: "!!a::'a::ring. a - b = 0 ==> a = b" apply (rule_tac s = "a - (a - b) " in trans) - apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *}) apply simp apply (simp (no_asm)) done @@ -215,23 +220,19 @@ (* r1 = 0 *) apply (erule disjE) (* r2 = 0 *) - apply (tactic {* asm_full_simp_tac (@{simpset} - addsimps [@{thm integral_iff}, @{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] - delsimprocs [ring_simproc]) 1 *}) + using [[simproc del: ring]] + apply (simp add: integral_iff minus_def l_zero uminus_zero) (* r2 ~= 0 *) apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) - apply (tactic {* asm_full_simp_tac (@{simpset} addsimps - [@{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] delsimprocs [ring_simproc]) 1 *}) + apply (simp add: minus_def l_zero uminus_zero) (* r1 ~=0 *) apply (erule disjE) (* r2 = 0 *) apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) - apply (tactic {* asm_full_simp_tac (@{simpset} addsimps - [@{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] delsimprocs [ring_simproc]) 1 *}) + apply (simp add: minus_def l_zero uminus_zero) (* r2 ~= 0 *) apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) - apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [@{thm minus_def}] - delsimprocs [ring_simproc]) 1 *}) + apply (simp add: minus_def) apply (drule order_eq_refl [THEN add_leD2]) apply (drule leD) apply (erule notE, rule deg_add [THEN le_less_trans]) @@ -240,6 +241,7 @@ apply (rule diff_zero_imp_eq) apply hypsubst apply (drule_tac a = "?x+?y" in eq_imp_diff_zero) + using [[simproc ring]] apply simp done diff -r e6d920bea7a6 -r 4db4a8b164c1 src/HOL/Algebra/poly/UnivPoly2.thy --- a/src/HOL/Algebra/poly/UnivPoly2.thy Thu May 12 18:18:06 2011 +0200 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy Thu May 12 21:14:03 2011 +0200 @@ -271,8 +271,6 @@ finally show ?thesis . qed -(* ML {* Addsimprocs [ring_simproc] *} *) - instance up :: (ring) ring proof fix p q r :: "'a::ring up" @@ -365,11 +363,11 @@ qed qed *) -ML {* Delsimprocs [ring_simproc] *} lemma monom_mult_is_smult: "monom (a::'a::ring) 0 * p = a *s p" proof (rule up_eqI) + note [[simproc del: ring]] fix k have "coeff (p * monom a 0) k = coeff (a *s p) k" proof (cases k) @@ -380,8 +378,6 @@ then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring qed -ML {* Addsimprocs [ring_simproc] *} - lemma monom_add [simp]: "monom (a + b) n = monom (a::'a::ring) n + monom b n" by (rule up_eqI) simp @@ -429,14 +425,10 @@ (* Polynomials form an algebra *) -ML {* Delsimprocs [ring_simproc] *} - lemma smult_assoc2: "(a *s p) * q = (a::'a::ring) *s (p * q)" +using [[simproc del: ring]] by (rule up_eqI) (simp add: natsum_rdistr m_assoc) -(* Simproc fails. *) - -ML {* Addsimprocs [ring_simproc] *} (* the following can be derived from the above ones, for generality reasons, it is therefore done *) @@ -452,7 +444,7 @@ qed lemma smult_r_null [simp]: - "(a::'a::ring) *s 0 = 0"; + "(a::'a::ring) *s 0 = 0" proof - fix p have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp