# 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 (\<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
 
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