src/HOL/Decision_Procs/Polynomial_List.thy

 qed
 
 lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
   apply (induct a)
   apply (simp, clarify)
-  apply (case_tac b, simp_all add: add_ac)
+  apply (case_tac b, simp_all add: ac_simps)
   done
 
 lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)"
   apply (induct p arbitrary: q)
   apply simp

   case Nil
   thus ?case by simp
 next
   case (Cons a as p2)
   thus ?case
-    by (cases p2) (simp_all  add: add_ac distrib_left)
+    by (cases p2) (simp_all  add: ac_simps distrib_left)
 qed
 
 lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x"
   apply (induct p)
   apply (case_tac [2] "x = zero")
-  apply (auto simp add: distrib_left mult_ac)
+  apply (auto simp add: distrib_left ac_simps)
   done
 
 lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c*poly p x"
-  by (induct p) (auto simp add: distrib_left mult_ac)
+  by (induct p) (auto simp add: distrib_left ac_simps)
 
 lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
   apply (simp add: poly_minus_def)
   apply (auto simp add: poly_cmult)
   done

   case Nil
   thus ?case by simp
 next
   case (Cons a as p2)
   thus ?case by (cases as)
-    (simp_all add: poly_cmult poly_add distrib_right distrib_left mult_ac)
+    (simp_all add: poly_cmult poly_add distrib_right distrib_left ac_simps)
 qed
 
 class idom_char_0 = idom + ring_char_0
 
 subclass (in field_char_0) idom_char_0 ..

   apply clarsimp
 
   apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
   apply (rule_tac x = "pmult qa q" in exI)
   apply (rule_tac [2] x = "pmult p qa" in exI)
-  apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
+  apply (auto simp add: poly_add poly_mult poly_cmult ac_simps)
   done
 
 lemma (in comm_semiring_1) poly_divides_refl[simp]: "p divides p"
   apply (simp add: divides_def)
   apply (rule_tac x = "[one]" in exI)

   apply (auto simp add: le_iff_add)
   apply (induct_tac k)
   apply (rule_tac [2] poly_divides_trans)
   apply (auto simp add: divides_def)
   apply (rule_tac x = p in exI)
-  apply (auto simp add: poly_mult fun_eq mult_ac)
+  apply (auto simp add: poly_mult fun_eq ac_simps)
   done
 
 lemma (in comm_semiring_1) poly_exp_divides:
   "(p %^ n) divides q \<Longrightarrow> m \<le> n \<Longrightarrow> (p %^ m) divides q"
   by (blast intro: poly_divides_exp poly_divides_trans)

   done
 
 lemma (in comm_ring_1) poly_divides_diff2:
   "p divides r \<Longrightarrow> p divides (q +++ r) \<Longrightarrow> p divides q"
   apply (erule poly_divides_diff)
-  apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac)
+  apply (auto simp add: poly_add fun_eq poly_mult divides_def ac_simps)
   done
 
 lemma (in semiring_0) poly_divides_zero: "poly p = poly [] \<Longrightarrow> q divides p"
   apply (simp add: divides_def)
   apply (rule exI[where x="[]"])

   qed
 qed
 
 
 lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
-  by (induct n) (auto simp add: poly_mult mult_ac)
+  by (induct n) (auto simp add: poly_mult ac_simps)
 
 lemma (in comm_semiring_1) divides_left_mult:
   assumes d:"(p***q) divides r" shows "p divides r \<and> q divides r"
 proof-
   from d obtain t where r:"poly r = poly (p***q *** t)"
     unfolding divides_def by blast
   hence "poly r = poly (p *** (q *** t))"
-    "poly r = poly (q *** (p***t))" by(auto simp add: fun_eq poly_mult mult_ac)
+    "poly r = poly (q *** (p***t))" by(auto simp add: fun_eq poly_mult ac_simps)
   thus ?thesis unfolding divides_def by blast
 qed
 
 
 (* FIXME: Tidy up *)

   apply (unfold divides_def)
   apply (drule order2 [where a = a])
   apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
   apply (rule_tac x = q in exI, safe)
   apply (drule_tac x = qa in spec)
-  apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons)
+  apply (auto simp add: poly_mult fun_eq poly_exp ac_simps simp del: pmult_Cons)
   done
 
 text{*Important composition properties of orders.*}
 lemma order_mult:
   "poly (p *** q) \<noteq> poly [] \<Longrightarrow>

   apply (auto simp add: poly_entire simp del: pmult_Cons)
   apply (drule_tac a = a in order2)+
   apply safe
   apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
   apply (rule_tac x = "qa *** qaa" in exI)
-  apply (simp add: poly_mult mult_ac del: pmult_Cons)
+  apply (simp add: poly_mult ac_simps del: pmult_Cons)
   apply (drule_tac a = a in order_decomp)+
   apply safe
   apply (subgoal_tac "[-a,1] divides (qa *** qaa) ")
   apply (simp add: poly_primes del: pmult_Cons)
   apply (auto simp add: divides_def simp del: pmult_Cons)
   apply (rule_tac x = qb in exI)
   apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))")
   apply (drule poly_mult_left_cancel [THEN iffD1], force)
   apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) = poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ")
   apply (drule poly_mult_left_cancel [THEN iffD1], force)
-  apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
+  apply (simp add: fun_eq poly_exp_add poly_mult ac_simps del: pmult_Cons)
   done
 
 lemma (in idom_char_0) order_mult:
   assumes "poly (p *** q) \<noteq> poly []"
   shows "order a (p *** q) = order a p + order a q"

   apply (auto simp add: poly_entire simp del: pmult_Cons)
   apply (drule_tac a = a in order2)+
   apply safe
   apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
   apply (rule_tac x = "pmult qa qaa" in exI)
-  apply (simp add: poly_mult mult_ac del: pmult_Cons)
+  apply (simp add: poly_mult ac_simps del: pmult_Cons)
   apply (drule_tac a = a in order_decomp)+
   apply safe
   apply (subgoal_tac "[uminus a, one] divides pmult qa qaa")
   apply (simp add: poly_primes del: pmult_Cons)
   apply (auto simp add: divides_def simp del: pmult_Cons)

   apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a q))
       (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa))) =
     poly (pmult (pexp [uminus a, one] (order a q))
       (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb)))")
   apply (drule poly_mult_left_cancel [THEN iffD1], force)
-  apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
+  apply (simp add: fun_eq poly_exp_add poly_mult ac_simps del: pmult_Cons)
   done
 
 lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] \<Longrightarrow> poly p a = 0 \<longleftrightarrow> order a p \<noteq> 0"
   by (rule order_root [THEN ssubst]) auto
 

 next
   case (Suc n a p)
   have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))"
     apply (rule ext)
     apply (simp add: poly_mult poly_add poly_cmult)
-    apply (simp add: mult_ac add_ac distrib_left)
+    apply (simp add: ac_simps ac_simps distrib_left)
     done
   note deq = degree_unique[OF eq]
   show ?case
   proof (cases "poly p = poly []")
     case True