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>"