--- 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 *)
--- 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
--- 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 (\<lambda>(q, r, k). lcoeff g ^ k *s f = q * g + r \<and>
+ (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
--- 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