src/HOL/Algebra/UnivPoly.thy
changeset 27717 21bbd410ba04
parent 27714 27b4d7c01f8b
child 27933 4b867f6a65d3
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Aug 01 17:41:37 2008 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Aug 01 18:10:52 2008 +0200
     1.3 @@ -3,9 +3,11 @@
     1.4    Id:        $Id$
     1.5    Author:    Clemens Ballarin, started 9 December 1996
     1.6    Copyright: Clemens Ballarin
     1.7 +
     1.8 +Contributions by Jesus Aransay.
     1.9  *)
    1.10  
    1.11 -theory UnivPoly imports Module begin
    1.12 +theory UnivPoly imports Module RingHom begin
    1.13  
    1.14  
    1.15  section {* Univariate Polynomials *}
    1.16 @@ -77,19 +79,16 @@
    1.17    "f \<in> up R ==> f n \<in> carrier R"
    1.18    by (simp add: up_def Pi_def)
    1.19  
    1.20 -lemma (in cring) bound_upD [dest]:
    1.21 -  "f \<in> up R ==> EX n. bound \<zero> n f"
    1.22 -  by (simp add: up_def)
    1.23 +context ring
    1.24 +begin
    1.25 +
    1.26 +lemma bound_upD [dest]: "f \<in> up R ==> EX n. bound \<zero> n f" by (simp add: up_def)
    1.27  
    1.28 -lemma (in cring) up_one_closed:
    1.29 -   "(%n. if n = 0 then \<one> else \<zero>) \<in> up R"
    1.30 -  using up_def by force
    1.31 +lemma up_one_closed: "(%n. if n = 0 then \<one> else \<zero>) \<in> up R" using up_def by force
    1.32  
    1.33 -lemma (in cring) up_smult_closed:
    1.34 -  "[| a \<in> carrier R; p \<in> up R |] ==> (%i. a \<otimes> p i) \<in> up R"
    1.35 -  by force
    1.36 +lemma up_smult_closed: "[| a \<in> carrier R; p \<in> up R |] ==> (%i. a \<otimes> p i) \<in> up R" by force
    1.37  
    1.38 -lemma (in cring) up_add_closed:
    1.39 +lemma up_add_closed:
    1.40    "[| p \<in> up R; q \<in> up R |] ==> (%i. p i \<oplus> q i) \<in> up R"
    1.41  proof
    1.42    fix n
    1.43 @@ -112,7 +111,7 @@
    1.44    qed
    1.45  qed
    1.46  
    1.47 -lemma (in cring) up_a_inv_closed:
    1.48 +lemma up_a_inv_closed:
    1.49    "p \<in> up R ==> (%i. \<ominus> (p i)) \<in> up R"
    1.50  proof
    1.51    assume R: "p \<in> up R"
    1.52 @@ -121,7 +120,7 @@
    1.53    then show "EX n. bound \<zero> n (%i. \<ominus> p i)" by auto
    1.54  qed auto
    1.55  
    1.56 -lemma (in cring) up_mult_closed:
    1.57 +lemma up_mult_closed:
    1.58    "[| p \<in> up R; q \<in> up R |] ==>
    1.59    (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
    1.60  proof
    1.61 @@ -161,6 +160,8 @@
    1.62    qed
    1.63  qed
    1.64  
    1.65 +end
    1.66 +
    1.67  
    1.68  subsection {* Effect of Operations on Coefficients *}
    1.69  
    1.70 @@ -168,19 +169,45 @@
    1.71    fixes R (structure) and P (structure)
    1.72    defines P_def: "P == UP R"
    1.73  
    1.74 +locale UP_ring = UP + ring R
    1.75 +
    1.76  locale UP_cring = UP + cring R
    1.77  
    1.78 -locale UP_domain = UP_cring + "domain" R
    1.79 +interpretation UP_cring < UP_ring
    1.80 +  by (rule P_def) intro_locales
    1.81 +
    1.82 +locale UP_domain = UP + "domain" R
    1.83  
    1.84 -text {*
    1.85 -  Temporarily declare @{thm [locale=UP] P_def} as simp rule.
    1.86 -*}
    1.87 +interpretation UP_domain < UP_cring
    1.88 +  by (rule P_def) intro_locales
    1.89 +
    1.90 +context UP
    1.91 +begin
    1.92 +
    1.93 +text {*Temporarily declare @{thm [locale=UP] P_def} as simp rule.*}
    1.94 +
    1.95 +declare P_def [simp]
    1.96  
    1.97 -declare (in UP) P_def [simp]
    1.98 +lemma up_eqI:
    1.99 +  assumes prem: "!!n. coeff P p n = coeff P q n" and R: "p \<in> carrier P" "q \<in> carrier P"
   1.100 +  shows "p = q"
   1.101 +proof
   1.102 +  fix x
   1.103 +  from prem and R show "p x = q x" by (simp add: UP_def)
   1.104 +qed
   1.105  
   1.106 -lemma (in UP_cring) coeff_monom [simp]:
   1.107 -  "a \<in> carrier R ==>
   1.108 -  coeff P (monom P a m) n = (if m=n then a else \<zero>)"
   1.109 +lemma coeff_closed [simp]:
   1.110 +  "p \<in> carrier P ==> coeff P p n \<in> carrier R" by (auto simp add: UP_def)
   1.111 +
   1.112 +end
   1.113 +
   1.114 +context UP_ring 
   1.115 +begin
   1.116 +
   1.117 +(* Theorems generalised to rings by Jesus Aransay. *)
   1.118 +
   1.119 +lemma coeff_monom [simp]:
   1.120 +  "a \<in> carrier R ==> coeff P (monom P a m) n = (if m=n then a else \<zero>)"
   1.121  proof -
   1.122    assume R: "a \<in> carrier R"
   1.123    then have "(%n. if n = m then a else \<zero>) \<in> up R"
   1.124 @@ -188,86 +215,69 @@
   1.125    with R show ?thesis by (simp add: UP_def)
   1.126  qed
   1.127  
   1.128 -lemma (in UP_cring) coeff_zero [simp]:
   1.129 -  "coeff P \<zero>\<^bsub>P\<^esub> n = \<zero>"
   1.130 -  by (auto simp add: UP_def)
   1.131 +lemma coeff_zero [simp]: "coeff P \<zero>\<^bsub>P\<^esub> n = \<zero>" by (auto simp add: UP_def)
   1.132  
   1.133 -lemma (in UP_cring) coeff_one [simp]:
   1.134 -  "coeff P \<one>\<^bsub>P\<^esub> n = (if n=0 then \<one> else \<zero>)"
   1.135 +lemma coeff_one [simp]: "coeff P \<one>\<^bsub>P\<^esub> n = (if n=0 then \<one> else \<zero>)"
   1.136    using up_one_closed by (simp add: UP_def)
   1.137  
   1.138 -lemma (in UP_cring) coeff_smult [simp]:
   1.139 -  "[| a \<in> carrier R; p \<in> carrier P |] ==>
   1.140 -  coeff P (a \<odot>\<^bsub>P\<^esub> p) n = a \<otimes> coeff P p n"
   1.141 +lemma coeff_smult [simp]:
   1.142 +  "[| a \<in> carrier R; p \<in> carrier P |] ==> coeff P (a \<odot>\<^bsub>P\<^esub> p) n = a \<otimes> coeff P p n"
   1.143    by (simp add: UP_def up_smult_closed)
   1.144  
   1.145 -lemma (in UP_cring) coeff_add [simp]:
   1.146 -  "[| p \<in> carrier P; q \<in> carrier P |] ==>
   1.147 -  coeff P (p \<oplus>\<^bsub>P\<^esub> q) n = coeff P p n \<oplus> coeff P q n"
   1.148 +lemma coeff_add [simp]:
   1.149 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> coeff P (p \<oplus>\<^bsub>P\<^esub> q) n = coeff P p n \<oplus> coeff P q n"
   1.150    by (simp add: UP_def up_add_closed)
   1.151  
   1.152 -lemma (in UP_cring) coeff_mult [simp]:
   1.153 -  "[| p \<in> carrier P; q \<in> carrier P |] ==>
   1.154 -  coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (n-i))"
   1.155 +lemma coeff_mult [simp]:
   1.156 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (n-i))"
   1.157    by (simp add: UP_def up_mult_closed)
   1.158  
   1.159 -lemma (in UP) up_eqI:
   1.160 -  assumes prem: "!!n. coeff P p n = coeff P q n"
   1.161 -    and R: "p \<in> carrier P" "q \<in> carrier P"
   1.162 -  shows "p = q"
   1.163 -proof
   1.164 -  fix x
   1.165 -  from prem and R show "p x = q x" by (simp add: UP_def)
   1.166 -qed
   1.167 +end
   1.168  
   1.169  
   1.170 -subsection {* Polynomials Form a Commutative Ring. *}
   1.171 +subsection {* Polynomials Form a Ring. *}
   1.172 +
   1.173 +context UP_ring
   1.174 +begin
   1.175  
   1.176  text {* Operations are closed over @{term P}. *}
   1.177  
   1.178 -lemma (in UP_cring) UP_mult_closed [simp]:
   1.179 -  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P"
   1.180 -  by (simp add: UP_def up_mult_closed)
   1.181 +lemma UP_mult_closed [simp]:
   1.182 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P" by (simp add: UP_def up_mult_closed)
   1.183  
   1.184 -lemma (in UP_cring) UP_one_closed [simp]:
   1.185 -  "\<one>\<^bsub>P\<^esub> \<in> carrier P"
   1.186 -  by (simp add: UP_def up_one_closed)
   1.187 +lemma UP_one_closed [simp]:
   1.188 +  "\<one>\<^bsub>P\<^esub> \<in> carrier P" by (simp add: UP_def up_one_closed)
   1.189  
   1.190 -lemma (in UP_cring) UP_zero_closed [intro, simp]:
   1.191 -  "\<zero>\<^bsub>P\<^esub> \<in> carrier P"
   1.192 -  by (auto simp add: UP_def)
   1.193 +lemma UP_zero_closed [intro, simp]:
   1.194 +  "\<zero>\<^bsub>P\<^esub> \<in> carrier P" by (auto simp add: UP_def)
   1.195  
   1.196 -lemma (in UP_cring) UP_a_closed [intro, simp]:
   1.197 -  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<oplus>\<^bsub>P\<^esub> q \<in> carrier P"
   1.198 -  by (simp add: UP_def up_add_closed)
   1.199 -
   1.200 -lemma (in UP_cring) monom_closed [simp]:
   1.201 -  "a \<in> carrier R ==> monom P a n \<in> carrier P"
   1.202 -  by (auto simp add: UP_def up_def Pi_def)
   1.203 +lemma UP_a_closed [intro, simp]:
   1.204 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<oplus>\<^bsub>P\<^esub> q \<in> carrier P" by (simp add: UP_def up_add_closed)
   1.205  
   1.206 -lemma (in UP_cring) UP_smult_closed [simp]:
   1.207 -  "[| a \<in> carrier R; p \<in> carrier P |] ==> a \<odot>\<^bsub>P\<^esub> p \<in> carrier P"
   1.208 -  by (simp add: UP_def up_smult_closed)
   1.209 +lemma monom_closed [simp]:
   1.210 +  "a \<in> carrier R ==> monom P a n \<in> carrier P" by (auto simp add: UP_def up_def Pi_def)
   1.211  
   1.212 -lemma (in UP) coeff_closed [simp]:
   1.213 -  "p \<in> carrier P ==> coeff P p n \<in> carrier R"
   1.214 -  by (auto simp add: UP_def)
   1.215 +lemma UP_smult_closed [simp]:
   1.216 +  "[| a \<in> carrier R; p \<in> carrier P |] ==> a \<odot>\<^bsub>P\<^esub> p \<in> carrier P" by (simp add: UP_def up_smult_closed)
   1.217 +
   1.218 +end
   1.219  
   1.220  declare (in UP) P_def [simp del]
   1.221  
   1.222  text {* Algebraic ring properties *}
   1.223  
   1.224 -lemma (in UP_cring) UP_a_assoc:
   1.225 -  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   1.226 -  shows "(p \<oplus>\<^bsub>P\<^esub> q) \<oplus>\<^bsub>P\<^esub> r = p \<oplus>\<^bsub>P\<^esub> (q \<oplus>\<^bsub>P\<^esub> r)"
   1.227 -  by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
   1.228 +context UP_ring
   1.229 +begin
   1.230  
   1.231 -lemma (in UP_cring) UP_l_zero [simp]:
   1.232 +lemma UP_a_assoc:
   1.233 +  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   1.234 +  shows "(p \<oplus>\<^bsub>P\<^esub> q) \<oplus>\<^bsub>P\<^esub> r = p \<oplus>\<^bsub>P\<^esub> (q \<oplus>\<^bsub>P\<^esub> r)" by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
   1.235 +
   1.236 +lemma UP_l_zero [simp]:
   1.237    assumes R: "p \<in> carrier P"
   1.238 -  shows "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> p = p"
   1.239 -  by (rule up_eqI, simp_all add: R)
   1.240 +  shows "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> p = p" by (rule up_eqI, simp_all add: R)
   1.241  
   1.242 -lemma (in UP_cring) UP_l_neg_ex:
   1.243 +lemma UP_l_neg_ex:
   1.244    assumes R: "p \<in> carrier P"
   1.245    shows "EX q : carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
   1.246  proof -
   1.247 @@ -283,12 +293,17 @@
   1.248    qed (rule closed)
   1.249  qed
   1.250  
   1.251 -lemma (in UP_cring) UP_a_comm:
   1.252 +lemma UP_a_comm:
   1.253    assumes R: "p \<in> carrier P" "q \<in> carrier P"
   1.254 -  shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p"
   1.255 -  by (rule up_eqI, simp add: a_comm R, simp_all add: R)
   1.256 +  shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p" by (rule up_eqI, simp add: a_comm R, simp_all add: R)
   1.257 +
   1.258 +end
   1.259 +
   1.260  
   1.261 -lemma (in UP_cring) UP_m_assoc:
   1.262 +context UP_ring
   1.263 +begin
   1.264 +
   1.265 +lemma UP_m_assoc:
   1.266    assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   1.267    shows "(p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
   1.268  proof (rule up_eqI)
   1.269 @@ -310,14 +325,51 @@
   1.270        with R show ?case
   1.271          by (simp cong: finsum_cong
   1.272               add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
   1.273 -          (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
   1.274 +           (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
   1.275      qed
   1.276    }
   1.277    with R show "coeff P ((p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r) n = coeff P (p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)) n"
   1.278      by (simp add: Pi_def)
   1.279  qed (simp_all add: R)
   1.280  
   1.281 -lemma (in UP_cring) UP_l_one [simp]:
   1.282 +lemma UP_r_one [simp]:
   1.283 +  assumes R: "p \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub> = p"
   1.284 +proof (rule up_eqI)
   1.285 +  fix n
   1.286 +  show "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) n = coeff P p n"
   1.287 +  proof (cases n)
   1.288 +    case 0 
   1.289 +    {
   1.290 +      with R show ?thesis by simp
   1.291 +    }
   1.292 +  next
   1.293 +    case Suc
   1.294 +    {
   1.295 +      (*JE: in the locale UP_cring the proof was solved only with "by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)", but I did not
   1.296 +      get it to work here*)
   1.297 +      fix nn assume Succ: "n = Suc nn"
   1.298 +      have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = coeff P p (Suc nn)"
   1.299 +      proof -
   1.300 +	have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = (\<Oplus>i\<in>{..Suc nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" using R by simp
   1.301 +	also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>) \<oplus> (\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))"
   1.302 +	  using finsum_Suc [of "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "nn"] unfolding Pi_def using R by simp
   1.303 +	also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>)"
   1.304 +	proof -
   1.305 +	  have "(\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>)) = (\<Oplus>i\<in>{..nn}. \<zero>)"
   1.306 +	    using finsum_cong [of "{..nn}" "{..nn}" "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "(\<lambda>i::nat. \<zero>)"] using R 
   1.307 +	    unfolding Pi_def by simp
   1.308 +	  also have "\<dots> = \<zero>" by simp
   1.309 +	  finally show ?thesis using r_zero R by simp
   1.310 +	qed
   1.311 +	also have "\<dots> = coeff P p (Suc nn)" using R by simp
   1.312 +	finally show ?thesis by simp
   1.313 +      qed
   1.314 +      then show ?thesis using Succ by simp
   1.315 +    }
   1.316 +  qed
   1.317 +qed (simp_all add: R)
   1.318 +  
   1.319 +lemma UP_l_one [simp]:
   1.320    assumes R: "p \<in> carrier P"
   1.321    shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p"
   1.322  proof (rule up_eqI)
   1.323 @@ -331,22 +383,36 @@
   1.324    qed
   1.325  qed (simp_all add: R)
   1.326  
   1.327 -lemma (in UP_cring) UP_l_distr:
   1.328 +lemma UP_l_distr:
   1.329    assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   1.330    shows "(p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = (p \<otimes>\<^bsub>P\<^esub> r) \<oplus>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
   1.331    by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R)
   1.332  
   1.333 -lemma (in UP_cring) UP_m_comm:
   1.334 -  assumes R: "p \<in> carrier P" "q \<in> carrier P"
   1.335 -  shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p"
   1.336 +lemma UP_r_distr:
   1.337 +  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   1.338 +  shows "r \<otimes>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) = (r \<otimes>\<^bsub>P\<^esub> p) \<oplus>\<^bsub>P\<^esub> (r \<otimes>\<^bsub>P\<^esub> q)"
   1.339 +  by (rule up_eqI) (simp add: r_distr R Pi_def, simp_all add: R)
   1.340 +
   1.341 +theorem UP_ring: "ring P"
   1.342 +  by (auto intro!: ringI abelian_groupI monoidI UP_a_assoc)
   1.343 +(auto intro: UP_a_comm UP_l_neg_ex UP_m_assoc UP_l_distr UP_r_distr)
   1.344 +
   1.345 +end
   1.346 +
   1.347 +subsection {* Polynomials form a commutative Ring. *}
   1.348 +
   1.349 +context UP_cring
   1.350 +begin
   1.351 +
   1.352 +lemma UP_m_comm:
   1.353 +  assumes R1: "p \<in> carrier P" and R2: "q \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p"
   1.354  proof (rule up_eqI)
   1.355    fix n
   1.356    {
   1.357      fix k and a b :: "nat=>'a"
   1.358      assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
   1.359      then have "k <= n ==>
   1.360 -      (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) =
   1.361 -      (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
   1.362 +      (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) = (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
   1.363        (is "_ \<Longrightarrow> ?eq k")
   1.364      proof (induct k)
   1.365        case 0 then show ?case by (simp add: Pi_def)
   1.366 @@ -356,31 +422,27 @@
   1.367      qed
   1.368    }
   1.369    note l = this
   1.370 -  from R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n =  coeff P (q \<otimes>\<^bsub>P\<^esub> p) n"
   1.371 -    apply (simp add: Pi_def)
   1.372 -    apply (subst l)
   1.373 -    apply (auto simp add: Pi_def)
   1.374 -    apply (simp add: m_comm)
   1.375 -    done
   1.376 -qed (simp_all add: R)
   1.377 +  from R1 R2 show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n =  coeff P (q \<otimes>\<^bsub>P\<^esub> p) n"
   1.378 +    unfolding coeff_mult [OF R1 R2, of n] 
   1.379 +    unfolding coeff_mult [OF R2 R1, of n] 
   1.380 +    using l [of "(\<lambda>i. coeff P p i)" "(\<lambda>i. coeff P q i)" "n"] by (simp add: Pi_def m_comm)
   1.381 +qed (simp_all add: R1 R2)
   1.382  
   1.383 -theorem (in UP_cring) UP_cring:
   1.384 -  "cring P"
   1.385 -  by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
   1.386 -    UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
   1.387 +subsection{*Polynomials over a commutative ring for a commutative ring*}
   1.388 +
   1.389 +theorem UP_cring:
   1.390 +  "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
   1.391  
   1.392 -lemma (in UP_cring) UP_ring:
   1.393 -  (* preliminary,
   1.394 -     we want "UP_ring R P ==> ring P", not "UP_cring R P ==> ring P" *)
   1.395 -  "ring P"
   1.396 -  by (auto intro: ring.intro cring.axioms UP_cring)
   1.397 +end
   1.398 +
   1.399 +context UP_ring
   1.400 +begin
   1.401  
   1.402 -lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
   1.403 +lemma UP_a_inv_closed [intro, simp]:
   1.404    "p \<in> carrier P ==> \<ominus>\<^bsub>P\<^esub> p \<in> carrier P"
   1.405 -  by (rule abelian_group.a_inv_closed
   1.406 -    [OF ring.is_abelian_group [OF UP_ring]])
   1.407 +  by (rule abelian_group.a_inv_closed [OF ring.is_abelian_group [OF UP_ring]])
   1.408  
   1.409 -lemma (in UP_cring) coeff_a_inv [simp]:
   1.410 +lemma coeff_a_inv [simp]:
   1.411    assumes R: "p \<in> carrier P"
   1.412    shows "coeff P (\<ominus>\<^bsub>P\<^esub> p) n = \<ominus> (coeff P p n)"
   1.413  proof -
   1.414 @@ -393,42 +455,47 @@
   1.415    finally show ?thesis .
   1.416  qed
   1.417  
   1.418 -text {*
   1.419 -  Interpretation of lemmas from @{term cring}.  Saves lifting 43
   1.420 -  lemmas manually.
   1.421 -*}
   1.422 +end
   1.423  
   1.424 -interpretation UP_cring < cring P
   1.425 -  by intro_locales
   1.426 -    (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+
   1.427 +interpretation UP_ring < ring P using UP_ring .
   1.428 +interpretation UP_cring < cring P using UP_cring .
   1.429  
   1.430  
   1.431  subsection {* Polynomials Form an Algebra *}
   1.432  
   1.433 -lemma (in UP_cring) UP_smult_l_distr:
   1.434 +context UP_ring
   1.435 +begin
   1.436 +
   1.437 +lemma UP_smult_l_distr:
   1.438    "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
   1.439    (a \<oplus> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> b \<odot>\<^bsub>P\<^esub> p"
   1.440    by (rule up_eqI) (simp_all add: R.l_distr)
   1.441  
   1.442 -lemma (in UP_cring) UP_smult_r_distr:
   1.443 +lemma UP_smult_r_distr:
   1.444    "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
   1.445    a \<odot>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> a \<odot>\<^bsub>P\<^esub> q"
   1.446    by (rule up_eqI) (simp_all add: R.r_distr)
   1.447  
   1.448 -lemma (in UP_cring) UP_smult_assoc1:
   1.449 +lemma UP_smult_assoc1:
   1.450        "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
   1.451        (a \<otimes> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> p)"
   1.452    by (rule up_eqI) (simp_all add: R.m_assoc)
   1.453  
   1.454 -lemma (in UP_cring) UP_smult_one [simp]:
   1.455 +lemma UP_smult_zero [simp]:
   1.456 +      "p \<in> carrier P ==> \<zero> \<odot>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
   1.457 +  by (rule up_eqI) simp_all
   1.458 +
   1.459 +lemma UP_smult_one [simp]:
   1.460        "p \<in> carrier P ==> \<one> \<odot>\<^bsub>P\<^esub> p = p"
   1.461    by (rule up_eqI) simp_all
   1.462  
   1.463 -lemma (in UP_cring) UP_smult_assoc2:
   1.464 +lemma UP_smult_assoc2:
   1.465    "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
   1.466    (a \<odot>\<^bsub>P\<^esub> p) \<otimes>\<^bsub>P\<^esub> q = a \<odot>\<^bsub>P\<^esub> (p \<otimes>\<^bsub>P\<^esub> q)"
   1.467    by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def)
   1.468  
   1.469 +end
   1.470 +
   1.471  text {*
   1.472    Interpretation of lemmas from @{term algebra}.
   1.473  *}
   1.474 @@ -438,44 +505,44 @@
   1.475    by unfold_locales
   1.476  
   1.477  lemma (in UP_cring) UP_algebra:
   1.478 -  "algebra R P"
   1.479 -  by (auto intro: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
   1.480 +  "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
   1.481      UP_smult_assoc1 UP_smult_assoc2)
   1.482  
   1.483 -interpretation UP_cring < algebra R P
   1.484 -  by intro_locales
   1.485 -    (rule module.axioms algebra.axioms UP_algebra)+
   1.486 +interpretation UP_cring < algebra R P using UP_algebra .
   1.487  
   1.488  
   1.489  subsection {* Further Lemmas Involving Monomials *}
   1.490  
   1.491 -lemma (in UP_cring) monom_zero [simp]:
   1.492 -  "monom P \<zero> n = \<zero>\<^bsub>P\<^esub>"
   1.493 -  by (simp add: UP_def P_def)
   1.494 +context UP_ring
   1.495 +begin
   1.496  
   1.497 -lemma (in UP_cring) monom_mult_is_smult:
   1.498 +lemma monom_zero [simp]:
   1.499 +  "monom P \<zero> n = \<zero>\<^bsub>P\<^esub>" by (simp add: UP_def P_def)
   1.500 +
   1.501 +lemma monom_mult_is_smult:
   1.502    assumes R: "a \<in> carrier R" "p \<in> carrier P"
   1.503    shows "monom P a 0 \<otimes>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p"
   1.504  proof (rule up_eqI)
   1.505    fix n
   1.506 -  have "coeff P (p \<otimes>\<^bsub>P\<^esub> monom P a 0) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n"
   1.507 +  show "coeff P (monom P a 0 \<otimes>\<^bsub>P\<^esub> p) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n"
   1.508    proof (cases n)
   1.509 -    case 0 with R show ?thesis by (simp add: R.m_comm)
   1.510 +    case 0 with R show ?thesis by simp
   1.511    next
   1.512      case Suc with R show ?thesis
   1.513 -      by (simp cong: R.finsum_cong add: R.r_null Pi_def)
   1.514 -        (simp add: R.m_comm)
   1.515 +      using R.finsum_Suc2 by (simp del: R.finsum_Suc add: R.r_null Pi_def)
   1.516    qed
   1.517 -  with R show "coeff P (monom P a 0 \<otimes>\<^bsub>P\<^esub> p) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n"
   1.518 -    by (simp add: UP_m_comm)
   1.519  qed (simp_all add: R)
   1.520  
   1.521 -lemma (in UP_cring) monom_add [simp]:
   1.522 +lemma monom_one [simp]:
   1.523 +  "monom P \<one> 0 = \<one>\<^bsub>P\<^esub>"
   1.524 +  by (rule up_eqI) simp_all
   1.525 +
   1.526 +lemma monom_add [simp]:
   1.527    "[| a \<in> carrier R; b \<in> carrier R |] ==>
   1.528    monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n"
   1.529    by (rule up_eqI) simp_all
   1.530  
   1.531 -lemma (in UP_cring) monom_one_Suc:
   1.532 +lemma monom_one_Suc:
   1.533    "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
   1.534  proof (rule up_eqI)
   1.535    fix k
   1.536 @@ -550,24 +617,59 @@
   1.537    qed
   1.538  qed (simp_all)
   1.539  
   1.540 -lemma (in UP_cring) monom_mult_smult:
   1.541 +lemma monom_one_Suc2:
   1.542 +  "monom P \<one> (Suc n) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> n"
   1.543 +proof (induct n)
   1.544 +  case 0 show ?case by simp
   1.545 +next
   1.546 +  case Suc
   1.547 +  {
   1.548 +    fix k:: nat
   1.549 +    assume hypo: "monom P \<one> (Suc k) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
   1.550 +    then show "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k)"
   1.551 +    proof -
   1.552 +      have lhs: "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
   1.553 +	unfolding monom_one_Suc [of "Suc k"] unfolding hypo ..
   1.554 +      note cl = monom_closed [OF R.one_closed, of 1]
   1.555 +      note clk = monom_closed [OF R.one_closed, of k]
   1.556 +      have rhs: "monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
   1.557 +	unfolding monom_one_Suc [of k] unfolding sym [OF m_assoc  [OF cl clk cl]] ..
   1.558 +      from lhs rhs show ?thesis by simp
   1.559 +    qed
   1.560 +  }
   1.561 +qed
   1.562 +
   1.563 +text{*The following corollary follows from lemmas @{thm [locale=UP_ring] "monom_one_Suc"} 
   1.564 +  and @{thm [locale=UP_ring] "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
   1.565 +
   1.566 +corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
   1.567 +  unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..
   1.568 +
   1.569 +lemma monom_mult_smult:
   1.570    "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^bsub>P\<^esub> monom P b n"
   1.571    by (rule up_eqI) simp_all
   1.572  
   1.573 -lemma (in UP_cring) monom_one [simp]:
   1.574 -  "monom P \<one> 0 = \<one>\<^bsub>P\<^esub>"
   1.575 -  by (rule up_eqI) simp_all
   1.576 -
   1.577 -lemma (in UP_cring) monom_one_mult:
   1.578 +lemma monom_one_mult:
   1.579    "monom P \<one> (n + m) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m"
   1.580  proof (induct n)
   1.581    case 0 show ?case by simp
   1.582  next
   1.583    case Suc then show ?case
   1.584 -    by (simp only: add_Suc monom_one_Suc) (simp add: P.m_ac)
   1.585 +    unfolding add_Suc unfolding monom_one_Suc unfolding Suc.hyps
   1.586 +    using m_assoc monom_one_comm [of m] by simp
   1.587  qed
   1.588  
   1.589 -lemma (in UP_cring) monom_mult [simp]:
   1.590 +lemma monom_one_mult_comm: "monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m = monom P \<one> m \<otimes>\<^bsub>P\<^esub> monom P \<one> n"
   1.591 +  unfolding monom_one_mult [symmetric] by (rule up_eqI) simp_all
   1.592 +
   1.593 +end
   1.594 +
   1.595 +context UP_cring
   1.596 +begin
   1.597 +
   1.598 +(* Could got to UP_ring?  *)
   1.599 +
   1.600 +lemma monom_mult [simp]:
   1.601    assumes R: "a \<in> carrier R" "b \<in> carrier R"
   1.602    shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m"
   1.603  proof -
   1.604 @@ -579,11 +681,11 @@
   1.605    also from R have "... = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m))"
   1.606      by (simp add: UP_smult_assoc1)
   1.607    also from R have "... = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> (monom P \<one> m \<otimes>\<^bsub>P\<^esub> monom P \<one> n))"
   1.608 -    by (simp add: P.m_comm)
   1.609 +    unfolding monom_one_mult_comm by simp
   1.610    also from R have "... = a \<odot>\<^bsub>P\<^esub> ((b \<odot>\<^bsub>P\<^esub> monom P \<one> m) \<otimes>\<^bsub>P\<^esub> monom P \<one> n)"
   1.611      by (simp add: UP_smult_assoc2)
   1.612    also from R have "... = a \<odot>\<^bsub>P\<^esub> (monom P \<one> n \<otimes>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> monom P \<one> m))"
   1.613 -    by (simp add: P.m_comm)
   1.614 +    using monom_one_mult_comm [of n m] by (simp add: P.m_comm)
   1.615    also from R have "... = (a \<odot>\<^bsub>P\<^esub> monom P \<one> n) \<otimes>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> monom P \<one> m)"
   1.616      by (simp add: UP_smult_assoc2)
   1.617    also from R have "... = monom P (a \<otimes> \<one>) n \<otimes>\<^bsub>P\<^esub> monom P (b \<otimes> \<one>) m"
   1.618 @@ -592,11 +694,16 @@
   1.619    finally show ?thesis .
   1.620  qed
   1.621  
   1.622 -lemma (in UP_cring) monom_a_inv [simp]:
   1.623 +end
   1.624 +
   1.625 +context UP_ring
   1.626 +begin
   1.627 +
   1.628 +lemma monom_a_inv [simp]:
   1.629    "a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n"
   1.630    by (rule up_eqI) simp_all
   1.631  
   1.632 -lemma (in UP_cring) monom_inj:
   1.633 +lemma monom_inj:
   1.634    "inj_on (%a. monom P a n) (carrier R)"
   1.635  proof (rule inj_onI)
   1.636    fix x y
   1.637 @@ -605,6 +712,8 @@
   1.638    with R show "x = y" by simp
   1.639  qed
   1.640  
   1.641 +end
   1.642 +
   1.643  
   1.644  subsection {* The Degree Function *}
   1.645  
   1.646 @@ -612,7 +721,10 @@
   1.647    deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
   1.648    "deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
   1.649  
   1.650 -lemma (in UP_cring) deg_aboveI:
   1.651 +context UP_ring
   1.652 +begin
   1.653 +
   1.654 +lemma deg_aboveI:
   1.655    "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
   1.656    by (unfold deg_def P_def) (fast intro: Least_le)
   1.657  
   1.658 @@ -633,7 +745,7 @@
   1.659  qed
   1.660  *)
   1.661  
   1.662 -lemma (in UP_cring) deg_aboveD:
   1.663 +lemma deg_aboveD:
   1.664    assumes "deg R p < m" and "p \<in> carrier P"
   1.665    shows "coeff P p m = \<zero>"
   1.666  proof -
   1.667 @@ -644,7 +756,7 @@
   1.668    from this and `deg R p < m` show ?thesis ..
   1.669  qed
   1.670  
   1.671 -lemma (in UP_cring) deg_belowI:
   1.672 +lemma deg_belowI:
   1.673    assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
   1.674      and R: "p \<in> carrier P"
   1.675    shows "n <= deg R p"
   1.676 @@ -658,7 +770,7 @@
   1.677    then show ?thesis by arith
   1.678  qed
   1.679  
   1.680 -lemma (in UP_cring) lcoeff_nonzero_deg:
   1.681 +lemma lcoeff_nonzero_deg:
   1.682    assumes deg: "deg R p ~= 0" and R: "p \<in> carrier P"
   1.683    shows "coeff P p (deg R p) ~= \<zero>"
   1.684  proof -
   1.685 @@ -666,9 +778,8 @@
   1.686    proof -
   1.687      have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
   1.688        by arith
   1.689 -(* TODO: why does simplification below not work with "1" *)
   1.690      from deg have "deg R p - 1 < (LEAST n. bound \<zero> n (coeff P p))"
   1.691 -      by (unfold deg_def P_def) arith
   1.692 +      by (unfold deg_def P_def) simp
   1.693      then have "~ bound \<zero> (deg R p - 1) (coeff P p)" by (rule not_less_Least)
   1.694      then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
   1.695        by (unfold bound_def) fast
   1.696 @@ -679,7 +790,7 @@
   1.697    with m_coeff show ?thesis by simp
   1.698  qed
   1.699  
   1.700 -lemma (in UP_cring) lcoeff_nonzero_nonzero:
   1.701 +lemma lcoeff_nonzero_nonzero:
   1.702    assumes deg: "deg R p = 0" and nonzero: "p ~= \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P"
   1.703    shows "coeff P p 0 ~= \<zero>"
   1.704  proof -
   1.705 @@ -695,7 +806,7 @@
   1.706    with coeff show ?thesis by simp
   1.707  qed
   1.708  
   1.709 -lemma (in UP_cring) lcoeff_nonzero:
   1.710 +lemma lcoeff_nonzero:
   1.711    assumes neq: "p ~= \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P"
   1.712    shows "coeff P p (deg R p) ~= \<zero>"
   1.713  proof (cases "deg R p = 0")
   1.714 @@ -704,14 +815,14 @@
   1.715    case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg)
   1.716  qed
   1.717  
   1.718 -lemma (in UP_cring) deg_eqI:
   1.719 +lemma deg_eqI:
   1.720    "[| !!m. n < m ==> coeff P p m = \<zero>;
   1.721        !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
   1.722  by (fast intro: le_anti_sym deg_aboveI deg_belowI)
   1.723  
   1.724  text {* Degree and polynomial operations *}
   1.725  
   1.726 -lemma (in UP_cring) deg_add [simp]:
   1.727 +lemma deg_add [simp]:
   1.728    assumes R: "p \<in> carrier P" "q \<in> carrier P"
   1.729    shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
   1.730  proof (cases "deg R p <= deg R q")
   1.731 @@ -722,15 +833,15 @@
   1.732      by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
   1.733  qed
   1.734  
   1.735 -lemma (in UP_cring) deg_monom_le:
   1.736 +lemma deg_monom_le:
   1.737    "a \<in> carrier R ==> deg R (monom P a n) <= n"
   1.738    by (intro deg_aboveI) simp_all
   1.739  
   1.740 -lemma (in UP_cring) deg_monom [simp]:
   1.741 +lemma deg_monom [simp]:
   1.742    "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
   1.743    by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
   1.744  
   1.745 -lemma (in UP_cring) deg_const [simp]:
   1.746 +lemma deg_const [simp]:
   1.747    assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
   1.748  proof (rule le_anti_sym)
   1.749    show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R)
   1.750 @@ -738,7 +849,7 @@
   1.751    show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
   1.752  qed
   1.753  
   1.754 -lemma (in UP_cring) deg_zero [simp]:
   1.755 +lemma deg_zero [simp]:
   1.756    "deg R \<zero>\<^bsub>P\<^esub> = 0"
   1.757  proof (rule le_anti_sym)
   1.758    show "deg R \<zero>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
   1.759 @@ -746,7 +857,7 @@
   1.760    show "0 <= deg R \<zero>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
   1.761  qed
   1.762  
   1.763 -lemma (in UP_cring) deg_one [simp]:
   1.764 +lemma deg_one [simp]:
   1.765    "deg R \<one>\<^bsub>P\<^esub> = 0"
   1.766  proof (rule le_anti_sym)
   1.767    show "deg R \<one>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
   1.768 @@ -754,7 +865,7 @@
   1.769    show "0 <= deg R \<one>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
   1.770  qed
   1.771  
   1.772 -lemma (in UP_cring) deg_uminus [simp]:
   1.773 +lemma deg_uminus [simp]:
   1.774    assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^bsub>P\<^esub> p) = deg R p"
   1.775  proof (rule le_anti_sym)
   1.776    show "deg R (\<ominus>\<^bsub>P\<^esub> p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
   1.777 @@ -764,12 +875,20 @@
   1.778        inj_on_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R)
   1.779  qed
   1.780  
   1.781 -lemma (in UP_domain) deg_smult_ring:
   1.782 +text{*The following lemma is later \emph{overwritten} by the most
   1.783 +  specific one for domains, @{text deg_smult}.*}
   1.784 +
   1.785 +lemma deg_smult_ring [simp]:
   1.786    "[| a \<in> carrier R; p \<in> carrier P |] ==>
   1.787    deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)"
   1.788    by (cases "a = \<zero>") (simp add: deg_aboveI deg_aboveD)+
   1.789  
   1.790 -lemma (in UP_domain) deg_smult [simp]:
   1.791 +end
   1.792 +
   1.793 +context UP_domain
   1.794 +begin
   1.795 +
   1.796 +lemma deg_smult [simp]:
   1.797    assumes R: "a \<in> carrier R" "p \<in> carrier P"
   1.798    shows "deg R (a \<odot>\<^bsub>P\<^esub> p) = (if a = \<zero> then 0 else deg R p)"
   1.799  proof (rule le_anti_sym)
   1.800 @@ -781,7 +900,12 @@
   1.801    qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R)
   1.802  qed
   1.803  
   1.804 -lemma (in UP_cring) deg_mult_cring:
   1.805 +end
   1.806 +
   1.807 +context UP_ring
   1.808 +begin
   1.809 +
   1.810 +lemma deg_mult_ring:
   1.811    assumes R: "p \<in> carrier P" "q \<in> carrier P"
   1.812    shows "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q"
   1.813  proof (rule deg_aboveI)
   1.814 @@ -801,12 +925,17 @@
   1.815    with boundm R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) m = \<zero>" by simp
   1.816  qed (simp add: R)
   1.817  
   1.818 -lemma (in UP_domain) deg_mult [simp]:
   1.819 +end
   1.820 +
   1.821 +context UP_domain
   1.822 +begin
   1.823 +
   1.824 +lemma deg_mult [simp]:
   1.825    "[| p ~= \<zero>\<^bsub>P\<^esub>; q ~= \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==>
   1.826    deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
   1.827  proof (rule le_anti_sym)
   1.828    assume "p \<in> carrier P" " q \<in> carrier P"
   1.829 -  then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_cring)
   1.830 +  then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_ring)
   1.831  next
   1.832    let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
   1.833    assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^bsub>P\<^esub>" "q ~= \<zero>\<^bsub>P\<^esub>"
   1.834 @@ -828,16 +957,23 @@
   1.835        = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
   1.836      with nz show "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) ~= \<zero>"
   1.837        by (simp add: integral_iff lcoeff_nonzero R)
   1.838 -    qed (simp add: R)
   1.839 -  qed
   1.840 +  qed (simp add: R)
   1.841 +qed
   1.842 +
   1.843 +end
   1.844  
   1.845 -lemma (in UP_cring) coeff_finsum:
   1.846 +text{*The following lemmas also can be lifted to @{term UP_ring}.*}
   1.847 +
   1.848 +context UP_ring
   1.849 +begin
   1.850 +
   1.851 +lemma coeff_finsum:
   1.852    assumes fin: "finite A"
   1.853    shows "p \<in> A -> carrier P ==>
   1.854      coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
   1.855    using fin by induct (auto simp: Pi_def)
   1.856  
   1.857 -lemma (in UP_cring) up_repr:
   1.858 +lemma up_repr:
   1.859    assumes R: "p \<in> carrier P"
   1.860    shows "(\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
   1.861  proof (rule up_eqI)
   1.862 @@ -874,7 +1010,7 @@
   1.863    qed
   1.864  qed (simp_all add: R Pi_def)
   1.865  
   1.866 -lemma (in UP_cring) up_repr_le:
   1.867 +lemma up_repr_le:
   1.868    "[| deg R p <= n; p \<in> carrier P |] ==>
   1.869    (\<Oplus>\<^bsub>P\<^esub> i \<in> {..n}. monom P (coeff P p i) i) = p"
   1.870  proof -
   1.871 @@ -889,6 +1025,8 @@
   1.872    finally show ?thesis .
   1.873  qed
   1.874  
   1.875 +end
   1.876 +
   1.877  
   1.878  subsection {* Polynomials over Integral Domains *}
   1.879  
   1.880 @@ -901,16 +1039,19 @@
   1.881    by (auto intro!: domain.intro domain_axioms.intro cring.axioms assms
   1.882      del: disjCI)
   1.883  
   1.884 -lemma (in UP_domain) UP_one_not_zero:
   1.885 +context UP_domain
   1.886 +begin
   1.887 +
   1.888 +lemma UP_one_not_zero:
   1.889    "\<one>\<^bsub>P\<^esub> ~= \<zero>\<^bsub>P\<^esub>"
   1.890  proof
   1.891    assume "\<one>\<^bsub>P\<^esub> = \<zero>\<^bsub>P\<^esub>"
   1.892    hence "coeff P \<one>\<^bsub>P\<^esub> 0 = (coeff P \<zero>\<^bsub>P\<^esub> 0)" by simp
   1.893    hence "\<one> = \<zero>" by simp
   1.894 -  with one_not_zero show "False" by contradiction
   1.895 +  with R.one_not_zero show "False" by contradiction
   1.896  qed
   1.897  
   1.898 -lemma (in UP_domain) UP_integral:
   1.899 +lemma UP_integral:
   1.900    "[| p \<otimes>\<^bsub>P\<^esub> q = \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==> p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>"
   1.901  proof -
   1.902    fix p q
   1.903 @@ -939,10 +1080,12 @@
   1.904    qed
   1.905  qed
   1.906  
   1.907 -theorem (in UP_domain) UP_domain:
   1.908 +theorem UP_domain:
   1.909    "domain P"
   1.910    by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI)
   1.911  
   1.912 +end
   1.913 +
   1.914  text {*
   1.915    Interpretation of theorems from @{term domain}.
   1.916  *}
   1.917 @@ -959,7 +1102,14 @@
   1.918    !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
   1.919    sorry*)
   1.920  
   1.921 -theorem (in cring) diagonal_sum:
   1.922 +lemma (in abelian_monoid) boundD_carrier:
   1.923 +  "[| bound \<zero> n f; n < m |] ==> f m \<in> carrier G"
   1.924 +  by auto
   1.925 +
   1.926 +context ring
   1.927 +begin
   1.928 +
   1.929 +theorem diagonal_sum:
   1.930    "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
   1.931    (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
   1.932    (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
   1.933 @@ -992,11 +1142,7 @@
   1.934    then show ?thesis by fast
   1.935  qed
   1.936  
   1.937 -lemma (in abelian_monoid) boundD_carrier:
   1.938 -  "[| bound \<zero> n f; n < m |] ==> f m \<in> carrier G"
   1.939 -  by auto
   1.940 -
   1.941 -theorem (in cring) cauchy_product:
   1.942 +theorem cauchy_product:
   1.943    assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
   1.944      and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
   1.945    shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
   1.946 @@ -1034,7 +1180,9 @@
   1.947    finally show ?thesis .
   1.948  qed
   1.949  
   1.950 -lemma (in UP_cring) const_ring_hom:
   1.951 +end
   1.952 +
   1.953 +lemma (in UP_ring) const_ring_hom:
   1.954    "(%a. monom P a 0) \<in> ring_hom R P"
   1.955    by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
   1.956  
   1.957 @@ -1044,17 +1192,20 @@
   1.958    "eval R S phi s == \<lambda>p \<in> carrier (UP R).
   1.959      \<Oplus>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes> s (^) i"
   1.960  
   1.961 +context UP
   1.962 +begin
   1.963  
   1.964 -lemma (in UP) eval_on_carrier:
   1.965 +lemma eval_on_carrier:
   1.966    fixes S (structure)
   1.967    shows "p \<in> carrier P ==>
   1.968    eval R S phi s p = (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. phi (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
   1.969    by (unfold eval_def, fold P_def) simp
   1.970  
   1.971 -lemma (in UP) eval_extensional:
   1.972 +lemma eval_extensional:
   1.973    "eval R S phi p \<in> extensional (carrier P)"
   1.974    by (unfold eval_def, fold P_def) simp
   1.975  
   1.976 +end
   1.977  
   1.978  text {* The universal property of the polynomial ring *}
   1.979  
   1.980 @@ -1065,7 +1216,23 @@
   1.981    assumes indet_img_carrier [simp, intro]: "s \<in> carrier S"
   1.982    defines Eval_def: "Eval == eval R S h s"
   1.983  
   1.984 -theorem (in UP_pre_univ_prop) eval_ring_hom:
   1.985 +text{*JE: I have moved the following lemma from Ring.thy and lifted then to the locale @{term ring_hom_ring} from @{term ring_hom_cring}.*}
   1.986 +text{*JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so 
   1.987 +  maybe it is not that necessary.*}
   1.988 +
   1.989 +lemma (in ring_hom_ring) hom_finsum [simp]:
   1.990 +  "[| finite A; f \<in> A -> carrier R |] ==>
   1.991 +  h (finsum R f A) = finsum S (h o f) A"
   1.992 +proof (induct set: finite)
   1.993 +  case empty then show ?case by simp
   1.994 +next
   1.995 +  case insert then show ?case by (simp add: Pi_def)
   1.996 +qed
   1.997 +
   1.998 +context UP_pre_univ_prop
   1.999 +begin
  1.1000 +
  1.1001 +theorem eval_ring_hom:
  1.1002    assumes S: "s \<in> carrier S"
  1.1003    shows "eval R S h s \<in> ring_hom P S"
  1.1004  proof (rule ring_hom_memI)
  1.1005 @@ -1076,38 +1243,6 @@
  1.1006  next
  1.1007    fix p q
  1.1008    assume R: "p \<in> carrier P" "q \<in> carrier P"
  1.1009 -  then show "eval R S h s (p \<otimes>\<^bsub>P\<^esub> q) = eval R S h s p \<otimes>\<^bsub>S\<^esub> eval R S h s q"
  1.1010 -  proof (simp only: eval_on_carrier UP_mult_closed)
  1.1011 -    from R S have
  1.1012 -      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
  1.1013 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<otimes>\<^bsub>P\<^esub> q)<..deg R p + deg R q}.
  1.1014 -        h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
  1.1015 -      by (simp cong: S.finsum_cong
  1.1016 -        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def
  1.1017 -        del: coeff_mult)
  1.1018 -    also from R have "... =
  1.1019 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
  1.1020 -      by (simp only: ivl_disj_un_one deg_mult_cring)
  1.1021 -    also from R S have "... =
  1.1022 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}.
  1.1023 -         \<Oplus>\<^bsub>S\<^esub> k \<in> {..i}.
  1.1024 -           h (coeff P p k) \<otimes>\<^bsub>S\<^esub> h (coeff P q (i - k)) \<otimes>\<^bsub>S\<^esub>
  1.1025 -           (s (^)\<^bsub>S\<^esub> k \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> (i - k)))"
  1.1026 -      by (simp cong: S.finsum_cong add: S.nat_pow_mult Pi_def
  1.1027 -        S.m_ac S.finsum_rdistr)
  1.1028 -    also from R S have "... =
  1.1029 -      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
  1.1030 -      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
  1.1031 -      by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac
  1.1032 -        Pi_def)
  1.1033 -    finally show
  1.1034 -      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
  1.1035 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
  1.1036 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" .
  1.1037 -  qed
  1.1038 -next
  1.1039 -  fix p q
  1.1040 -  assume R: "p \<in> carrier P" "q \<in> carrier P"
  1.1041    then show "eval R S h s (p \<oplus>\<^bsub>P\<^esub> q) = eval R S h s p \<oplus>\<^bsub>S\<^esub> eval R S h s q"
  1.1042    proof (simp only: eval_on_carrier P.a_closed)
  1.1043      from S R have
  1.1044 @@ -1115,8 +1250,7 @@
  1.1045        (\<Oplus>\<^bsub>S \<^esub>i\<in>{..deg R (p \<oplus>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<oplus>\<^bsub>P\<^esub> q)<..max (deg R p) (deg R q)}.
  1.1046          h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
  1.1047        by (simp cong: S.finsum_cong
  1.1048 -        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def
  1.1049 -        del: coeff_add)
  1.1050 +        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def del: coeff_add)
  1.1051      also from R have "... =
  1.1052          (\<Oplus>\<^bsub>S\<^esub> i \<in> {..max (deg R p) (deg R q)}.
  1.1053            h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
  1.1054 @@ -1145,23 +1279,40 @@
  1.1055  next
  1.1056    show "eval R S h s \<one>\<^bsub>P\<^esub> = \<one>\<^bsub>S\<^esub>"
  1.1057      by (simp only: eval_on_carrier UP_one_closed) simp
  1.1058 +next
  1.1059 +  fix p q
  1.1060 +  assume R: "p \<in> carrier P" "q \<in> carrier P"
  1.1061 +  then show "eval R S h s (p \<otimes>\<^bsub>P\<^esub> q) = eval R S h s p \<otimes>\<^bsub>S\<^esub> eval R S h s q"
  1.1062 +  proof (simp only: eval_on_carrier UP_mult_closed)
  1.1063 +    from R S have
  1.1064 +      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
  1.1065 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<otimes>\<^bsub>P\<^esub> q)<..deg R p + deg R q}.
  1.1066 +        h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
  1.1067 +      by (simp cong: S.finsum_cong
  1.1068 +        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def
  1.1069 +        del: coeff_mult)
  1.1070 +    also from R have "... =
  1.1071 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
  1.1072 +      by (simp only: ivl_disj_un_one deg_mult_ring)
  1.1073 +    also from R S have "... =
  1.1074 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}.
  1.1075 +         \<Oplus>\<^bsub>S\<^esub> k \<in> {..i}.
  1.1076 +           h (coeff P p k) \<otimes>\<^bsub>S\<^esub> h (coeff P q (i - k)) \<otimes>\<^bsub>S\<^esub>
  1.1077 +           (s (^)\<^bsub>S\<^esub> k \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> (i - k)))"
  1.1078 +      by (simp cong: S.finsum_cong add: S.nat_pow_mult Pi_def
  1.1079 +        S.m_ac S.finsum_rdistr)
  1.1080 +    also from R S have "... =
  1.1081 +      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
  1.1082 +      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
  1.1083 +      by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac
  1.1084 +        Pi_def)
  1.1085 +    finally show
  1.1086 +      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
  1.1087 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
  1.1088 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" .
  1.1089 +  qed
  1.1090  qed
  1.1091  
  1.1092 -text {* Interpretation of ring homomorphism lemmas. *}
  1.1093 -
  1.1094 -interpretation UP_univ_prop < ring_hom_cring P S Eval
  1.1095 -  apply (unfold Eval_def)
  1.1096 -  apply intro_locales
  1.1097 -  apply (rule ring_hom_cring.axioms)
  1.1098 -  apply (rule ring_hom_cring.intro)
  1.1099 -  apply unfold_locales
  1.1100 -  apply (rule eval_ring_hom)
  1.1101 -  apply rule
  1.1102 -  done
  1.1103 -
  1.1104 -
  1.1105 -text {* Further properties of the evaluation homomorphism. *}
  1.1106 -
  1.1107  text {*
  1.1108    The following lemma could be proved in @{text UP_cring} with the additional
  1.1109    assumption that @{text h} is closed. *}
  1.1110 @@ -1170,6 +1321,8 @@
  1.1111    "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
  1.1112    by (simp only: eval_on_carrier monom_closed) simp
  1.1113  
  1.1114 +text {* Further properties of the evaluation homomorphism. *}
  1.1115 +
  1.1116  text {* The following proof is complicated by the fact that in arbitrary
  1.1117    rings one might have @{term "one R = zero R"}. *}
  1.1118  
  1.1119 @@ -1198,6 +1351,20 @@
  1.1120      h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = s" .
  1.1121  qed
  1.1122  
  1.1123 +end
  1.1124 +
  1.1125 +text {* Interpretation of ring homomorphism lemmas. *}
  1.1126 +
  1.1127 +interpretation UP_univ_prop < ring_hom_cring P S Eval
  1.1128 +  apply (unfold Eval_def)
  1.1129 +  apply intro_locales
  1.1130 +  apply (rule ring_hom_cring.axioms)
  1.1131 +  apply (rule ring_hom_cring.intro)
  1.1132 +  apply unfold_locales
  1.1133 +  apply (rule eval_ring_hom)
  1.1134 +  apply rule
  1.1135 +  done
  1.1136 +
  1.1137  lemma (in UP_cring) monom_pow:
  1.1138    assumes R: "a \<in> carrier R"
  1.1139    shows "(monom P a n) (^)\<^bsub>P\<^esub> m = monom P (a (^) m) (n * m)"
  1.1140 @@ -1253,7 +1420,10 @@
  1.1141    by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
  1.1142      cring.axioms assms)
  1.1143  
  1.1144 -lemma (in UP_pre_univ_prop) UP_hom_unique:
  1.1145 +context UP_pre_univ_prop
  1.1146 +begin
  1.1147 +
  1.1148 +lemma UP_hom_unique:
  1.1149    assumes "ring_hom_cring P S Phi"
  1.1150    assumes Phi: "Phi (monom P \<one> (Suc 0)) = s"
  1.1151        "!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r"
  1.1152 @@ -1277,7 +1447,7 @@
  1.1153    finally show ?thesis .
  1.1154  qed
  1.1155  
  1.1156 -lemma (in UP_pre_univ_prop) ring_homD:
  1.1157 +lemma ring_homD:
  1.1158    assumes Phi: "Phi \<in> ring_hom P S"
  1.1159    shows "ring_hom_cring P S Phi"
  1.1160  proof (rule ring_hom_cring.intro)
  1.1161 @@ -1285,7 +1455,7 @@
  1.1162    by (rule ring_hom_cring_axioms.intro) (rule Phi)
  1.1163  qed unfold_locales
  1.1164  
  1.1165 -theorem (in UP_pre_univ_prop) UP_universal_property:
  1.1166 +theorem UP_universal_property:
  1.1167    assumes S: "s \<in> carrier S"
  1.1168    shows "EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
  1.1169      Phi (monom P \<one> 1) = s &
  1.1170 @@ -1296,6 +1466,8 @@
  1.1171    apply (auto intro: UP_hom_unique ring_homD)
  1.1172    done
  1.1173  
  1.1174 +end
  1.1175 +
  1.1176  
  1.1177  subsection {* Sample Application of Evaluation Homomorphism *}
  1.1178  
  1.1179 @@ -1308,9 +1480,8 @@
  1.1180    by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
  1.1181      ring_hom_cring_axioms.intro UP_cring.intro)
  1.1182  
  1.1183 -constdefs
  1.1184 -  INTEG :: "int ring"
  1.1185 -  "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
  1.1186 +definition  INTEG :: "int ring"
  1.1187 +  where INTEG_def: "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
  1.1188  
  1.1189  lemma INTEG_cring:
  1.1190    "cring INTEG"
  1.1191 @@ -1327,11 +1498,7 @@
  1.1192    "UP INTEG"} globally.
  1.1193  *}
  1.1194  
  1.1195 -interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
  1.1196 -  apply simp
  1.1197 -  using INTEG_id_eval
  1.1198 -  apply simp
  1.1199 -  done
  1.1200 +interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id] using INTEG_id_eval by simp_all
  1.1201  
  1.1202  lemma INTEG_closed [intro, simp]:
  1.1203    "z \<in> carrier INTEG"