src/HOL/Algebra/UnivPoly.thy
 changeset 68445 c183a6a69f2d parent 67613 ce654b0e6d69 child 69064 5840724b1d71
```     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Jun 12 16:09:12 2018 +0100
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Jun 14 14:23:38 2018 +0100
1.3 @@ -116,14 +116,15 @@
1.4  proof
1.5    assume R: "p \<in> up R"
1.6    then obtain n where "bound \<zero> n p" by auto
1.7 -  then have "bound \<zero> n (\<lambda>i. \<ominus> p i)" by auto
1.8 +  then have "bound \<zero> n (\<lambda>i. \<ominus> p i)"
1.9 +    by (simp add: bound_def minus_equality)
1.10    then show "\<exists>n. bound \<zero> n (\<lambda>i. \<ominus> p i)" by auto
1.11  qed auto
1.12
1.13  lemma up_minus_closed:
1.14    "[| p \<in> up R; q \<in> up R |] ==> (\<lambda>i. p i \<ominus> q i) \<in> up R"
1.15 -  using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed a_minus_def [of _ R]
1.16 -  by auto
1.17 +  unfolding a_minus_def
1.18 +  using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed  by auto
1.19
1.20  lemma up_mult_closed:
1.21    "[| p \<in> up R; q \<in> up R |] ==>
1.22 @@ -695,7 +696,7 @@
1.23
1.24  lemma monom_a_inv [simp]:
1.25    "a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n"
1.26 -  by (rule up_eqI) simp_all
1.27 +  by (rule up_eqI) auto
1.28
1.29  lemma monom_inj:
1.30    "inj_on (\<lambda>a. monom P a n) (carrier R)"
1.31 @@ -1462,9 +1463,9 @@
1.32  subsection\<open>The long division algorithm: some previous facts.\<close>
1.33
1.34  lemma coeff_minus [simp]:
1.35 -  assumes p: "p \<in> carrier P" and q: "q \<in> carrier P" shows "coeff P (p \<ominus>\<^bsub>P\<^esub> q) n = coeff P p n \<ominus> coeff P q n"
1.36 -  unfolding a_minus_def [OF p q] unfolding coeff_add [OF p a_inv_closed [OF q]] unfolding coeff_a_inv [OF q]
1.37 -  using coeff_closed [OF p, of n] using coeff_closed [OF q, of n] by algebra
1.38 +  assumes p: "p \<in> carrier P" and q: "q \<in> carrier P"
1.39 +  shows "coeff P (p \<ominus>\<^bsub>P\<^esub> q) n = coeff P p n \<ominus> coeff P q n"
1.40 +  by (simp add: a_minus_def p q)
1.41
1.42  lemma lcoeff_closed [simp]: assumes p: "p \<in> carrier P" shows "lcoeff p \<in> carrier R"
1.43    using coeff_closed [OF p, of "deg R p"] by simp
1.44 @@ -1719,10 +1720,7 @@
1.45      and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
1.46      using a R.a_inv_closed by auto
1.47    have "eval R R id a ?g = eval R R id a (monom P \<one> 1) \<ominus> eval R R id a (monom P a 0)"
1.48 -    unfolding P.minus_eq [OF mon1_closed mon0_closed]
1.49 -    unfolding hom_add [OF mon1_closed min_mon0_closed]
1.50 -    unfolding hom_a_inv [OF mon0_closed]
1.51 -    using R.minus_eq [symmetric] mon1_closed mon0_closed by auto
1.52 +    by (simp add: a_minus_def mon0_closed)
1.53    also have "\<dots> = a \<ominus> a"
1.54      using eval_monom [OF R.one_closed a, of 1] using eval_monom [OF a a, of 0] using a by simp
1.55    also have "\<dots> = \<zero>"
```