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