src/HOL/Algebra/UnivPoly.thy
changeset 13940 c67798653056
child 13949 0ce528cd6f19
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Apr 30 18:32:06 2003 +0200
     1.3 @@ -0,0 +1,1546 @@
     1.4 +(*
     1.5 +  Title:     Univariate Polynomials
     1.6 +  Id:        $Id$
     1.7 +  Author:    Clemens Ballarin, started 9 December 1996
     1.8 +  Copyright: Clemens Ballarin
     1.9 +*)
    1.10 +
    1.11 +theory UnivPoly = Module:
    1.12 +
    1.13 +section {* Univariate Polynomials *}
    1.14 +
    1.15 +subsection
    1.16 +  {* Definition of the Constructor for Univariate Polynomials @{term UP} *}
    1.17 +
    1.18 +(* Could alternatively use locale ...
    1.19 +locale bound = cring + var bound +
    1.20 +  defines ...
    1.21 +*)
    1.22 +
    1.23 +constdefs
    1.24 +  bound  :: "['a, nat, nat => 'a] => bool"
    1.25 +  "bound z n f == (ALL i. n < i --> f i = z)"
    1.26 +
    1.27 +lemma boundI [intro!]:
    1.28 +  "[| !! m. n < m ==> f m = z |] ==> bound z n f"
    1.29 +  by (unfold bound_def) fast
    1.30 +
    1.31 +lemma boundE [elim?]:
    1.32 +  "[| bound z n f; (!! m. n < m ==> f m = z) ==> P |] ==> P"
    1.33 +  by (unfold bound_def) fast
    1.34 +
    1.35 +lemma boundD [dest]:
    1.36 +  "[| bound z n f; n < m |] ==> f m = z"
    1.37 +  by (unfold bound_def) fast
    1.38 +
    1.39 +lemma bound_below:
    1.40 +  assumes bound: "bound z m f" and nonzero: "f n ~= z" shows "n <= m"
    1.41 +proof (rule classical)
    1.42 +  assume "~ ?thesis"
    1.43 +  then have "m < n" by arith
    1.44 +  with bound have "f n = z" ..
    1.45 +  with nonzero show ?thesis by contradiction
    1.46 +qed
    1.47 +
    1.48 +record ('a, 'p) up_ring = "('a, 'p) module" +
    1.49 +  monom :: "['a, nat] => 'p"
    1.50 +  coeff :: "['p, nat] => 'a"
    1.51 +
    1.52 +constdefs
    1.53 +  up :: "('a, 'm) ring_scheme => (nat => 'a) set"
    1.54 +  "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound (zero R) n f)}"
    1.55 +  UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
    1.56 +  "UP R == (|
    1.57 +    carrier = up R,
    1.58 +    mult = (%p:up R. %q:up R. %n. finsum R (%i. mult R (p i) (q (n-i))) {..n}),
    1.59 +    one = (%i. if i=0 then one R else zero R),
    1.60 +    zero = (%i. zero R),
    1.61 +    add = (%p:up R. %q:up R. %i. add R (p i) (q i)),
    1.62 +    smult = (%a:carrier R. %p:up R. %i. mult R a (p i)),
    1.63 +    monom = (%a:carrier R. %n i. if i=n then a else zero R),
    1.64 +    coeff = (%p:up R. %n. p n) |)"
    1.65 +
    1.66 +text {*
    1.67 +  Properties of the set of polynomials @{term up}.
    1.68 +*}
    1.69 +
    1.70 +lemma mem_upI [intro]:
    1.71 +  "[| !!n. f n \<in> carrier R; EX n. bound (zero R) n f |] ==> f \<in> up R"
    1.72 +  by (simp add: up_def Pi_def)
    1.73 +
    1.74 +lemma mem_upD [dest]:
    1.75 +  "f \<in> up R ==> f n \<in> carrier R"
    1.76 +  by (simp add: up_def Pi_def)
    1.77 +
    1.78 +lemma (in cring) bound_upD [dest]:
    1.79 +  "f \<in> up R ==> EX n. bound \<zero> n f"
    1.80 +  by (simp add: up_def)
    1.81 +
    1.82 +lemma (in cring) up_one_closed:
    1.83 +   "(%n. if n = 0 then \<one> else \<zero>) \<in> up R"
    1.84 +  using up_def by force
    1.85 +
    1.86 +lemma (in cring) up_smult_closed:
    1.87 +  "[| a \<in> carrier R; p \<in> up R |] ==> (%i. a \<otimes> p i) \<in> up R"
    1.88 +  by force
    1.89 +
    1.90 +lemma (in cring) up_add_closed:
    1.91 +  "[| p \<in> up R; q \<in> up R |] ==> (%i. p i \<oplus> q i) \<in> up R"
    1.92 +proof
    1.93 +  fix n
    1.94 +  assume "p \<in> up R" and "q \<in> up R"
    1.95 +  then show "p n \<oplus> q n \<in> carrier R"
    1.96 +    by auto
    1.97 +next
    1.98 +  assume UP: "p \<in> up R" "q \<in> up R"
    1.99 +  show "EX n. bound \<zero> n (%i. p i \<oplus> q i)"
   1.100 +  proof -
   1.101 +    from UP obtain n where boundn: "bound \<zero> n p" by fast
   1.102 +    from UP obtain m where boundm: "bound \<zero> m q" by fast
   1.103 +    have "bound \<zero> (max n m) (%i. p i \<oplus> q i)"
   1.104 +    proof
   1.105 +      fix i
   1.106 +      assume "max n m < i"
   1.107 +      with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastsimp
   1.108 +    qed
   1.109 +    then show ?thesis ..
   1.110 +  qed
   1.111 +qed
   1.112 +
   1.113 +lemma (in cring) up_a_inv_closed:
   1.114 +  "p \<in> up R ==> (%i. \<ominus> (p i)) \<in> up R"
   1.115 +proof
   1.116 +  assume R: "p \<in> up R"
   1.117 +  then obtain n where "bound \<zero> n p" by auto
   1.118 +  then have "bound \<zero> n (%i. \<ominus> p i)" by auto
   1.119 +  then show "EX n. bound \<zero> n (%i. \<ominus> p i)" by auto
   1.120 +qed auto
   1.121 +
   1.122 +lemma (in cring) up_mult_closed:
   1.123 +  "[| p \<in> up R; q \<in> up R |] ==>
   1.124 +  (%n. finsum R (%i. p i \<otimes> q (n-i)) {..n}) \<in> up R"
   1.125 +proof
   1.126 +  fix n
   1.127 +  assume "p \<in> up R" "q \<in> up R"
   1.128 +  then show "finsum R (%i. p i \<otimes> q (n-i)) {..n} \<in> carrier R"
   1.129 +    by (simp add: mem_upD  funcsetI)
   1.130 +next
   1.131 +  assume UP: "p \<in> up R" "q \<in> up R"
   1.132 +  show "EX n. bound \<zero> n (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
   1.133 +  proof -
   1.134 +    from UP obtain n where boundn: "bound \<zero> n p" by fast
   1.135 +    from UP obtain m where boundm: "bound \<zero> m q" by fast
   1.136 +    have "bound \<zero> (n + m) (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
   1.137 +    proof
   1.138 +      fix k
   1.139 +      assume bound: "n + m < k"
   1.140 +      {
   1.141 +	fix i
   1.142 +	have "p i \<otimes> q (k-i) = \<zero>"
   1.143 +	proof (cases "n < i")
   1.144 +	  case True
   1.145 +	  with boundn have "p i = \<zero>" by auto
   1.146 +          moreover from UP have "q (k-i) \<in> carrier R" by auto
   1.147 +	  ultimately show ?thesis by simp
   1.148 +	next
   1.149 +	  case False
   1.150 +	  with bound have "m < k-i" by arith
   1.151 +	  with boundm have "q (k-i) = \<zero>" by auto
   1.152 +	  moreover from UP have "p i \<in> carrier R" by auto
   1.153 +	  ultimately show ?thesis by simp
   1.154 +	qed
   1.155 +      }
   1.156 +      then show "finsum R (%i. p i \<otimes> q (k-i)) {..k} = \<zero>"
   1.157 +	by (simp add: Pi_def)
   1.158 +    qed
   1.159 +    then show ?thesis by fast
   1.160 +  qed
   1.161 +qed
   1.162 +
   1.163 +subsection {* Effect of operations on coefficients *}
   1.164 +
   1.165 +locale UP = struct R + struct P +
   1.166 +  defines P_def: "P == UP R"
   1.167 +
   1.168 +locale UP_cring = UP + cring R
   1.169 +
   1.170 +locale UP_domain = UP_cring + "domain" R
   1.171 +
   1.172 +text {*
   1.173 +  Temporarily declare UP.P\_def as simp rule.
   1.174 +*}
   1.175 +(* TODO: use antiquotation once text (in locale) is supported. *)
   1.176 +
   1.177 +declare (in UP) P_def [simp]
   1.178 +
   1.179 +lemma (in UP_cring) coeff_monom [simp]:
   1.180 +  "a \<in> carrier R ==>
   1.181 +  coeff P (monom P a m) n = (if m=n then a else \<zero>)"
   1.182 +proof -
   1.183 +  assume R: "a \<in> carrier R"
   1.184 +  then have "(%n. if n = m then a else \<zero>) \<in> up R"
   1.185 +    using up_def by force
   1.186 +  with R show ?thesis by (simp add: UP_def)
   1.187 +qed
   1.188 +
   1.189 +lemma (in UP_cring) coeff_zero [simp]:
   1.190 +  "coeff P \<zero>\<^sub>2 n = \<zero>"
   1.191 +  by (auto simp add: UP_def)
   1.192 +
   1.193 +lemma (in UP_cring) coeff_one [simp]:
   1.194 +  "coeff P \<one>\<^sub>2 n = (if n=0 then \<one> else \<zero>)"
   1.195 +  using up_one_closed by (simp add: UP_def)
   1.196 +
   1.197 +lemma (in UP_cring) coeff_smult [simp]:
   1.198 +  "[| a \<in> carrier R; p \<in> carrier P |] ==>
   1.199 +  coeff P (a \<odot>\<^sub>2 p) n = a \<otimes> coeff P p n"
   1.200 +  by (simp add: UP_def up_smult_closed)
   1.201 +
   1.202 +lemma (in UP_cring) coeff_add [simp]:
   1.203 +  "[| p \<in> carrier P; q \<in> carrier P |] ==>
   1.204 +  coeff P (p \<oplus>\<^sub>2 q) n = coeff P p n \<oplus> coeff P q n"
   1.205 +  by (simp add: UP_def up_add_closed)
   1.206 +
   1.207 +lemma (in UP_cring) coeff_mult [simp]:
   1.208 +  "[| p \<in> carrier P; q \<in> carrier P |] ==>
   1.209 +  coeff P (p \<otimes>\<^sub>2 q) n = finsum R (%i. coeff P p i \<otimes> coeff P q (n-i)) {..n}"
   1.210 +  by (simp add: UP_def up_mult_closed)
   1.211 +
   1.212 +lemma (in UP) up_eqI:
   1.213 +  assumes prem: "!!n. coeff P p n = coeff P q n"
   1.214 +    and R: "p \<in> carrier P" "q \<in> carrier P"
   1.215 +  shows "p = q"
   1.216 +proof
   1.217 +  fix x
   1.218 +  from prem and R show "p x = q x" by (simp add: UP_def)
   1.219 +qed
   1.220 +  
   1.221 +subsection {* Polynomials form a commutative ring. *}
   1.222 +
   1.223 +text {* Operations are closed over @{term "P"}. *}
   1.224 +
   1.225 +lemma (in UP_cring) UP_mult_closed [simp]:
   1.226 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^sub>2 q \<in> carrier P"
   1.227 +  by (simp add: UP_def up_mult_closed)
   1.228 +
   1.229 +lemma (in UP_cring) UP_one_closed [simp]:
   1.230 +  "\<one>\<^sub>2 \<in> carrier P"
   1.231 +  by (simp add: UP_def up_one_closed)
   1.232 +
   1.233 +lemma (in UP_cring) UP_zero_closed [intro, simp]:
   1.234 +  "\<zero>\<^sub>2 \<in> carrier P"
   1.235 +  by (auto simp add: UP_def)
   1.236 +
   1.237 +lemma (in UP_cring) UP_a_closed [intro, simp]:
   1.238 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<oplus>\<^sub>2 q \<in> carrier P"
   1.239 +  by (simp add: UP_def up_add_closed)
   1.240 +
   1.241 +lemma (in UP_cring) monom_closed [simp]:
   1.242 +  "a \<in> carrier R ==> monom P a n \<in> carrier P"
   1.243 +  by (auto simp add: UP_def up_def Pi_def)
   1.244 +
   1.245 +lemma (in UP_cring) UP_smult_closed [simp]:
   1.246 +  "[| a \<in> carrier R; p \<in> carrier P |] ==> a \<odot>\<^sub>2 p \<in> carrier P"
   1.247 +  by (simp add: UP_def up_smult_closed)
   1.248 +
   1.249 +lemma (in UP) coeff_closed [simp]:
   1.250 +  "p \<in> carrier P ==> coeff P p n \<in> carrier R"
   1.251 +  by (auto simp add: UP_def)
   1.252 +
   1.253 +declare (in UP) P_def [simp del]
   1.254 +
   1.255 +text {* Algebraic ring properties *}
   1.256 +
   1.257 +lemma (in UP_cring) UP_a_assoc:
   1.258 +  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   1.259 +  shows "(p \<oplus>\<^sub>2 q) \<oplus>\<^sub>2 r = p \<oplus>\<^sub>2 (q \<oplus>\<^sub>2 r)"
   1.260 +  by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
   1.261 +
   1.262 +lemma (in UP_cring) UP_l_zero [simp]:
   1.263 +  assumes R: "p \<in> carrier P"
   1.264 +  shows "\<zero>\<^sub>2 \<oplus>\<^sub>2 p = p"
   1.265 +  by (rule up_eqI, simp_all add: R)
   1.266 +
   1.267 +lemma (in UP_cring) UP_l_neg_ex:
   1.268 +  assumes R: "p \<in> carrier P"
   1.269 +  shows "EX q : carrier P. q \<oplus>\<^sub>2 p = \<zero>\<^sub>2"
   1.270 +proof -
   1.271 +  let ?q = "%i. \<ominus> (p i)"
   1.272 +  from R have closed: "?q \<in> carrier P"
   1.273 +    by (simp add: UP_def P_def up_a_inv_closed)
   1.274 +  from R have coeff: "!!n. coeff P ?q n = \<ominus> (coeff P p n)"
   1.275 +    by (simp add: UP_def P_def up_a_inv_closed)
   1.276 +  show ?thesis
   1.277 +  proof
   1.278 +    show "?q \<oplus>\<^sub>2 p = \<zero>\<^sub>2"
   1.279 +      by (auto intro!: up_eqI simp add: R closed coeff R.l_neg)
   1.280 +  qed (rule closed)
   1.281 +qed
   1.282 +
   1.283 +lemma (in UP_cring) UP_a_comm:
   1.284 +  assumes R: "p \<in> carrier P" "q \<in> carrier P"
   1.285 +  shows "p \<oplus>\<^sub>2 q = q \<oplus>\<^sub>2 p"
   1.286 +  by (rule up_eqI, simp add: a_comm R, simp_all add: R)
   1.287 +
   1.288 +ML_setup {*
   1.289 +Context.>> (fn thy => (simpset_ref_of thy :=
   1.290 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   1.291 +
   1.292 +lemma (in UP_cring) UP_m_assoc:
   1.293 +  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   1.294 +  shows "(p \<otimes>\<^sub>2 q) \<otimes>\<^sub>2 r = p \<otimes>\<^sub>2 (q \<otimes>\<^sub>2 r)"
   1.295 +proof (rule up_eqI)
   1.296 +  fix n
   1.297 +  {
   1.298 +    fix k and a b c :: "nat=>'a"
   1.299 +    assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
   1.300 +      "c \<in> UNIV -> carrier R"
   1.301 +    then have "k <= n ==>
   1.302 +      finsum R (%j. finsum R (%i. a i \<otimes> b (j-i)) {..j} \<otimes> c (n-j)) {..k} =
   1.303 +      finsum R (%j. a j \<otimes> finsum R (%i. b i \<otimes> c (n-j-i)) {..k-j}) {..k}"
   1.304 +      (is "_ ==> ?eq k")
   1.305 +    proof (induct k)
   1.306 +      case 0 then show ?case by (simp add: Pi_def m_assoc)
   1.307 +    next
   1.308 +      case (Suc k)
   1.309 +      then have "k <= n" by arith
   1.310 +      then have "?eq k" by (rule Suc)
   1.311 +      with R show ?case
   1.312 +	by (simp cong: finsum_cong
   1.313 +             add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
   1.314 +          (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
   1.315 +    qed
   1.316 +  }
   1.317 +  with R show "coeff P ((p \<otimes>\<^sub>2 q) \<otimes>\<^sub>2 r) n = coeff P (p \<otimes>\<^sub>2 (q \<otimes>\<^sub>2 r)) n"
   1.318 +    by (simp add: Pi_def)
   1.319 +qed (simp_all add: R)
   1.320 +
   1.321 +ML_setup {*
   1.322 +Context.>> (fn thy => (simpset_ref_of thy :=
   1.323 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
   1.324 +
   1.325 +lemma (in UP_cring) UP_l_one [simp]:
   1.326 +  assumes R: "p \<in> carrier P"
   1.327 +  shows "\<one>\<^sub>2 \<otimes>\<^sub>2 p = p"
   1.328 +proof (rule up_eqI)
   1.329 +  fix n
   1.330 +  show "coeff P (\<one>\<^sub>2 \<otimes>\<^sub>2 p) n = coeff P p n"
   1.331 +  proof (cases n)
   1.332 +    case 0 with R show ?thesis by simp
   1.333 +  next
   1.334 +    case Suc with R show ?thesis
   1.335 +      by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)
   1.336 +  qed
   1.337 +qed (simp_all add: R)
   1.338 +
   1.339 +lemma (in UP_cring) UP_l_distr:
   1.340 +  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   1.341 +  shows "(p \<oplus>\<^sub>2 q) \<otimes>\<^sub>2 r = (p \<otimes>\<^sub>2 r) \<oplus>\<^sub>2 (q \<otimes>\<^sub>2 r)"
   1.342 +  by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R)
   1.343 +
   1.344 +lemma (in UP_cring) UP_m_comm:
   1.345 +  assumes R: "p \<in> carrier P" "q \<in> carrier P"
   1.346 +  shows "p \<otimes>\<^sub>2 q = q \<otimes>\<^sub>2 p"
   1.347 +proof (rule up_eqI)
   1.348 +  fix n 
   1.349 +  {
   1.350 +    fix k and a b :: "nat=>'a"
   1.351 +    assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
   1.352 +    then have "k <= n ==> 
   1.353 +      finsum R (%i. a i \<otimes> b (n-i)) {..k} =
   1.354 +      finsum R (%i. a (k-i) \<otimes> b (i+n-k)) {..k}"
   1.355 +      (is "_ ==> ?eq k")
   1.356 +    proof (induct k)
   1.357 +      case 0 then show ?case by (simp add: Pi_def)
   1.358 +    next
   1.359 +      case (Suc k) then show ?case
   1.360 +	by (subst finsum_Suc2) (simp add: Pi_def a_comm)+
   1.361 +    qed
   1.362 +  }
   1.363 +  note l = this
   1.364 +  from R show "coeff P (p \<otimes>\<^sub>2 q) n =  coeff P (q \<otimes>\<^sub>2 p) n"
   1.365 +    apply (simp add: Pi_def)
   1.366 +    apply (subst l)
   1.367 +    apply (auto simp add: Pi_def)
   1.368 +    apply (simp add: m_comm)
   1.369 +    done
   1.370 +qed (simp_all add: R)
   1.371 +
   1.372 +theorem (in UP_cring) UP_cring:
   1.373 +  "cring P"
   1.374 +  by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
   1.375 +    UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
   1.376 +
   1.377 +lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
   1.378 +  "p \<in> carrier P ==> \<ominus>\<^sub>2 p \<in> carrier P"
   1.379 +  by (rule abelian_group.a_inv_closed
   1.380 +    [OF cring.is_abelian_group [OF UP_cring]])
   1.381 +
   1.382 +lemma (in UP_cring) coeff_a_inv [simp]:
   1.383 +  assumes R: "p \<in> carrier P"
   1.384 +  shows "coeff P (\<ominus>\<^sub>2 p) n = \<ominus> (coeff P p n)"
   1.385 +proof -
   1.386 +  from R coeff_closed UP_a_inv_closed have
   1.387 +    "coeff P (\<ominus>\<^sub>2 p) n = \<ominus> coeff P p n \<oplus> (coeff P p n \<oplus> coeff P (\<ominus>\<^sub>2 p) n)"
   1.388 +    by algebra
   1.389 +  also from R have "... =  \<ominus> (coeff P p n)"
   1.390 +    by (simp del: coeff_add add: coeff_add [THEN sym]
   1.391 +      abelian_group.r_neg [OF cring.is_abelian_group [OF UP_cring]])
   1.392 +  finally show ?thesis .
   1.393 +qed
   1.394 +
   1.395 +text {*
   1.396 +  Instantiation of lemmas from @{term cring}.
   1.397 +*}
   1.398 +
   1.399 +lemma (in UP_cring) UP_monoid:
   1.400 +  "monoid P"
   1.401 +  by (fast intro!: cring.is_comm_monoid comm_monoid.axioms monoid.intro
   1.402 +    UP_cring)
   1.403 +(* TODO: provide cring.is_monoid *)
   1.404 +
   1.405 +lemma (in UP_cring) UP_comm_semigroup:
   1.406 +  "comm_semigroup P"
   1.407 +  by (fast intro!: cring.is_comm_monoid comm_monoid.axioms comm_semigroup.intro
   1.408 +    UP_cring)
   1.409 +
   1.410 +lemma (in UP_cring) UP_comm_monoid:
   1.411 +  "comm_monoid P"
   1.412 +  by (fast intro!: cring.is_comm_monoid UP_cring)
   1.413 +
   1.414 +lemma (in UP_cring) UP_abelian_monoid:
   1.415 +  "abelian_monoid P"
   1.416 +  by (fast intro!: abelian_group.axioms cring.is_abelian_group UP_cring)
   1.417 +
   1.418 +lemma (in UP_cring) UP_abelian_group:
   1.419 +  "abelian_group P"
   1.420 +  by (fast intro!: cring.is_abelian_group UP_cring)
   1.421 +
   1.422 +lemmas (in UP_cring) UP_r_one [simp] =
   1.423 +  monoid.r_one [OF UP_monoid]
   1.424 +
   1.425 +lemmas (in UP_cring) UP_nat_pow_closed [intro, simp] =
   1.426 +  monoid.nat_pow_closed [OF UP_monoid]
   1.427 +
   1.428 +lemmas (in UP_cring) UP_nat_pow_0 [simp] =
   1.429 +  monoid.nat_pow_0 [OF UP_monoid]
   1.430 +
   1.431 +lemmas (in UP_cring) UP_nat_pow_Suc [simp] =
   1.432 +  monoid.nat_pow_Suc [OF UP_monoid]
   1.433 +
   1.434 +lemmas (in UP_cring) UP_nat_pow_one [simp] =
   1.435 +  monoid.nat_pow_one [OF UP_monoid]
   1.436 +
   1.437 +lemmas (in UP_cring) UP_nat_pow_mult =
   1.438 +  monoid.nat_pow_mult [OF UP_monoid]
   1.439 +
   1.440 +lemmas (in UP_cring) UP_nat_pow_pow =
   1.441 +  monoid.nat_pow_pow [OF UP_monoid]
   1.442 +
   1.443 +lemmas (in UP_cring) UP_m_lcomm =
   1.444 +  comm_semigroup.m_lcomm [OF UP_comm_semigroup]
   1.445 +
   1.446 +lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm
   1.447 +
   1.448 +lemmas (in UP_cring) UP_nat_pow_distr =
   1.449 +  comm_monoid.nat_pow_distr [OF UP_comm_monoid]
   1.450 +
   1.451 +lemmas (in UP_cring) UP_a_lcomm = abelian_monoid.a_lcomm [OF UP_abelian_monoid]
   1.452 +
   1.453 +lemmas (in UP_cring) UP_r_zero [simp] =
   1.454 +  abelian_monoid.r_zero [OF UP_abelian_monoid]
   1.455 +
   1.456 +lemmas (in UP_cring) UP_a_ac = UP_a_assoc UP_a_comm UP_a_lcomm
   1.457 +
   1.458 +lemmas (in UP_cring) UP_finsum_empty [simp] =
   1.459 +  abelian_monoid.finsum_empty [OF UP_abelian_monoid]
   1.460 +
   1.461 +lemmas (in UP_cring) UP_finsum_insert [simp] =
   1.462 +  abelian_monoid.finsum_insert [OF UP_abelian_monoid]
   1.463 +
   1.464 +lemmas (in UP_cring) UP_finsum_zero [simp] =
   1.465 +  abelian_monoid.finsum_zero [OF UP_abelian_monoid]
   1.466 +
   1.467 +lemmas (in UP_cring) UP_finsum_closed [simp] =
   1.468 +  abelian_monoid.finsum_closed [OF UP_abelian_monoid]
   1.469 +
   1.470 +lemmas (in UP_cring) UP_finsum_Un_Int =
   1.471 +  abelian_monoid.finsum_Un_Int [OF UP_abelian_monoid]
   1.472 +
   1.473 +lemmas (in UP_cring) UP_finsum_Un_disjoint =
   1.474 +  abelian_monoid.finsum_Un_disjoint [OF UP_abelian_monoid]
   1.475 +
   1.476 +lemmas (in UP_cring) UP_finsum_addf =
   1.477 +  abelian_monoid.finsum_addf [OF UP_abelian_monoid]
   1.478 +
   1.479 +lemmas (in UP_cring) UP_finsum_cong' =
   1.480 +  abelian_monoid.finsum_cong' [OF UP_abelian_monoid]
   1.481 +
   1.482 +lemmas (in UP_cring) UP_finsum_0 [simp] =
   1.483 +  abelian_monoid.finsum_0 [OF UP_abelian_monoid]
   1.484 +
   1.485 +lemmas (in UP_cring) UP_finsum_Suc [simp] =
   1.486 +  abelian_monoid.finsum_Suc [OF UP_abelian_monoid]
   1.487 +
   1.488 +lemmas (in UP_cring) UP_finsum_Suc2 =
   1.489 +  abelian_monoid.finsum_Suc2 [OF UP_abelian_monoid]
   1.490 +
   1.491 +lemmas (in UP_cring) UP_finsum_add [simp] =
   1.492 +  abelian_monoid.finsum_add [OF UP_abelian_monoid]
   1.493 +
   1.494 +lemmas (in UP_cring) UP_finsum_cong =
   1.495 +  abelian_monoid.finsum_cong [OF UP_abelian_monoid]
   1.496 +
   1.497 +lemmas (in UP_cring) UP_minus_closed [intro, simp] =
   1.498 +  abelian_group.minus_closed [OF UP_abelian_group]
   1.499 +
   1.500 +lemmas (in UP_cring) UP_a_l_cancel [simp] =
   1.501 +  abelian_group.a_l_cancel [OF UP_abelian_group]
   1.502 +
   1.503 +lemmas (in UP_cring) UP_a_r_cancel [simp] =
   1.504 +  abelian_group.a_r_cancel [OF UP_abelian_group]
   1.505 +
   1.506 +lemmas (in UP_cring) UP_l_neg =
   1.507 +  abelian_group.l_neg [OF UP_abelian_group]
   1.508 +
   1.509 +lemmas (in UP_cring) UP_r_neg =
   1.510 +  abelian_group.r_neg [OF UP_abelian_group]
   1.511 +
   1.512 +lemmas (in UP_cring) UP_minus_zero [simp] =
   1.513 +  abelian_group.minus_zero [OF UP_abelian_group]
   1.514 +
   1.515 +lemmas (in UP_cring) UP_minus_minus [simp] =
   1.516 +  abelian_group.minus_minus [OF UP_abelian_group]
   1.517 +
   1.518 +lemmas (in UP_cring) UP_minus_add =
   1.519 +  abelian_group.minus_add [OF UP_abelian_group]
   1.520 +
   1.521 +lemmas (in UP_cring) UP_r_neg2 =
   1.522 +  abelian_group.r_neg2 [OF UP_abelian_group]
   1.523 +
   1.524 +lemmas (in UP_cring) UP_r_neg1 =
   1.525 +  abelian_group.r_neg1 [OF UP_abelian_group]
   1.526 +
   1.527 +lemmas (in UP_cring) UP_r_distr =
   1.528 +  cring.r_distr [OF UP_cring]
   1.529 +
   1.530 +lemmas (in UP_cring) UP_l_null [simp] =
   1.531 +  cring.l_null [OF UP_cring]
   1.532 +
   1.533 +lemmas (in UP_cring) UP_r_null [simp] =
   1.534 +  cring.r_null [OF UP_cring]
   1.535 +
   1.536 +lemmas (in UP_cring) UP_l_minus =
   1.537 +  cring.l_minus [OF UP_cring]
   1.538 +
   1.539 +lemmas (in UP_cring) UP_r_minus =
   1.540 +  cring.r_minus [OF UP_cring]
   1.541 +
   1.542 +lemmas (in UP_cring) UP_finsum_ldistr =
   1.543 +  cring.finsum_ldistr [OF UP_cring]
   1.544 +
   1.545 +lemmas (in UP_cring) UP_finsum_rdistr =
   1.546 +  cring.finsum_rdistr [OF UP_cring]
   1.547 +
   1.548 +subsection {* Polynomials form an Algebra *}
   1.549 +
   1.550 +lemma (in UP_cring) UP_smult_l_distr:
   1.551 +  "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
   1.552 +  (a \<oplus> b) \<odot>\<^sub>2 p = a \<odot>\<^sub>2 p \<oplus>\<^sub>2 b \<odot>\<^sub>2 p"
   1.553 +  by (rule up_eqI) (simp_all add: R.l_distr)
   1.554 +
   1.555 +lemma (in UP_cring) UP_smult_r_distr:
   1.556 +  "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
   1.557 +  a \<odot>\<^sub>2 (p \<oplus>\<^sub>2 q) = a \<odot>\<^sub>2 p \<oplus>\<^sub>2 a \<odot>\<^sub>2 q"
   1.558 +  by (rule up_eqI) (simp_all add: R.r_distr)
   1.559 +
   1.560 +lemma (in UP_cring) UP_smult_assoc1:
   1.561 +      "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
   1.562 +      (a \<otimes> b) \<odot>\<^sub>2 p = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 p)"
   1.563 +  by (rule up_eqI) (simp_all add: R.m_assoc)
   1.564 +
   1.565 +lemma (in UP_cring) UP_smult_one [simp]:
   1.566 +      "p \<in> carrier P ==> \<one> \<odot>\<^sub>2 p = p"
   1.567 +  by (rule up_eqI) simp_all
   1.568 +
   1.569 +lemma (in UP_cring) UP_smult_assoc2:
   1.570 +  "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
   1.571 +  (a \<odot>\<^sub>2 p) \<otimes>\<^sub>2 q = a \<odot>\<^sub>2 (p \<otimes>\<^sub>2 q)"
   1.572 +  by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def)
   1.573 +
   1.574 +text {*
   1.575 +  Instantiation of lemmas from @{term algebra}.
   1.576 +*}
   1.577 +
   1.578 +(* TODO: move to CRing.thy, really a fact missing from the locales package *)
   1.579 +
   1.580 +lemma (in cring) cring:
   1.581 +  "cring R"
   1.582 +  by (fast intro: cring.intro prems)
   1.583 +
   1.584 +lemma (in UP_cring) UP_algebra:
   1.585 +  "algebra R P"
   1.586 +  by (auto intro: algebraI cring UP_cring UP_smult_l_distr UP_smult_r_distr
   1.587 +    UP_smult_assoc1 UP_smult_assoc2)
   1.588 +
   1.589 +lemmas (in UP_cring) UP_smult_l_null [simp] =
   1.590 +  algebra.smult_l_null [OF UP_algebra]
   1.591 +
   1.592 +lemmas (in UP_cring) UP_smult_r_null [simp] =
   1.593 +  algebra.smult_r_null [OF UP_algebra]
   1.594 +
   1.595 +lemmas (in UP_cring) UP_smult_l_minus =
   1.596 +  algebra.smult_l_minus [OF UP_algebra]
   1.597 +
   1.598 +lemmas (in UP_cring) UP_smult_r_minus =
   1.599 +  algebra.smult_r_minus [OF UP_algebra]
   1.600 +
   1.601 +subsection {* Further Lemmas Involving @{term monom} *}
   1.602 +
   1.603 +lemma (in UP_cring) monom_zero [simp]:
   1.604 +  "monom P \<zero> n = \<zero>\<^sub>2"
   1.605 +  by (simp add: UP_def P_def)
   1.606 +
   1.607 +ML_setup {*
   1.608 +Context.>> (fn thy => (simpset_ref_of thy :=
   1.609 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   1.610 +
   1.611 +lemma (in UP_cring) monom_mult_is_smult:
   1.612 +  assumes R: "a \<in> carrier R" "p \<in> carrier P"
   1.613 +  shows "monom P a 0 \<otimes>\<^sub>2 p = a \<odot>\<^sub>2 p"
   1.614 +proof (rule up_eqI)
   1.615 +  fix n
   1.616 +  have "coeff P (p \<otimes>\<^sub>2 monom P a 0) n = coeff P (a \<odot>\<^sub>2 p) n"
   1.617 +  proof (cases n)
   1.618 +    case 0 with R show ?thesis by (simp add: R.m_comm)
   1.619 +  next
   1.620 +    case Suc with R show ?thesis
   1.621 +      by (simp cong: finsum_cong add: R.r_null Pi_def)
   1.622 +        (simp add: m_comm)
   1.623 +  qed
   1.624 +  with R show "coeff P (monom P a 0 \<otimes>\<^sub>2 p) n = coeff P (a \<odot>\<^sub>2 p) n"
   1.625 +    by (simp add: UP_m_comm)
   1.626 +qed (simp_all add: R)
   1.627 +
   1.628 +ML_setup {*
   1.629 +Context.>> (fn thy => (simpset_ref_of thy :=
   1.630 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
   1.631 +
   1.632 +lemma (in UP_cring) monom_add [simp]:
   1.633 +  "[| a \<in> carrier R; b \<in> carrier R |] ==>
   1.634 +  monom P (a \<oplus> b) n = monom P a n \<oplus>\<^sub>2 monom P b n"
   1.635 +  by (rule up_eqI) simp_all
   1.636 +
   1.637 +ML_setup {*
   1.638 +Context.>> (fn thy => (simpset_ref_of thy :=
   1.639 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   1.640 +
   1.641 +lemma (in UP_cring) monom_one_Suc:
   1.642 +  "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1"
   1.643 +proof (rule up_eqI)
   1.644 +  fix k
   1.645 +  show "coeff P (monom P \<one> (Suc n)) k = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k"
   1.646 +  proof (cases "k = Suc n")
   1.647 +    case True show ?thesis
   1.648 +    proof -
   1.649 +      from True have less_add_diff: 
   1.650 +	"!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
   1.651 +      from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
   1.652 +      also from True
   1.653 +      have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
   1.654 +	coeff P (monom P \<one> 1) (k - i)) ({..n(} Un {n})"
   1.655 +	by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
   1.656 +      also have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
   1.657 +	coeff P (monom P \<one> 1) (k - i)) {..n}"
   1.658 +	by (simp only: ivl_disj_un_singleton)
   1.659 +      also from True have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
   1.660 +	coeff P (monom P \<one> 1) (k - i)) ({..n} Un {)n..k})"
   1.661 +	by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
   1.662 +	  order_less_imp_not_eq Pi_def)
   1.663 +      also from True have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k"
   1.664 +	by (simp add: ivl_disj_un_one)
   1.665 +      finally show ?thesis .
   1.666 +    qed
   1.667 +  next
   1.668 +    case False
   1.669 +    note neq = False
   1.670 +    let ?s =
   1.671 +      "(\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>))"
   1.672 +    from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
   1.673 +    also have "... = finsum R ?s {..k}"
   1.674 +    proof -
   1.675 +      have f1: "finsum R ?s {..n(} = \<zero>" by (simp cong: finsum_cong add: Pi_def)
   1.676 +      from neq have f2: "finsum R ?s {n} = \<zero>"
   1.677 +	by (simp cong: finsum_cong add: Pi_def) arith
   1.678 +      have f3: "n < k ==> finsum R ?s {)n..k} = \<zero>"
   1.679 +	by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
   1.680 +      show ?thesis
   1.681 +      proof (cases "k < n")
   1.682 +	case True then show ?thesis by (simp cong: finsum_cong add: Pi_def)
   1.683 +      next
   1.684 +	case False then have n_le_k: "n <= k" by arith
   1.685 +	show ?thesis
   1.686 +	proof (cases "n = k")
   1.687 +	  case True
   1.688 +	  then have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
   1.689 +	    by (simp cong: finsum_cong add: finsum_Un_disjoint
   1.690 +	      ivl_disj_int_singleton Pi_def)
   1.691 +	  also from True have "... = finsum R ?s {..k}"
   1.692 +	    by (simp only: ivl_disj_un_singleton)
   1.693 +	  finally show ?thesis .
   1.694 +	next
   1.695 +	  case False with n_le_k have n_less_k: "n < k" by arith
   1.696 +	  with neq have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
   1.697 +	    by (simp add: finsum_Un_disjoint f1 f2
   1.698 +	      ivl_disj_int_singleton Pi_def del: Un_insert_right)
   1.699 +	  also have "... = finsum R ?s {..n}"
   1.700 +	    by (simp only: ivl_disj_un_singleton)
   1.701 +	  also from n_less_k neq have "... = finsum R ?s ({..n} \<union> {)n..k})"
   1.702 +	    by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
   1.703 +	  also from n_less_k have "... = finsum R ?s {..k}"
   1.704 +	    by (simp only: ivl_disj_un_one)
   1.705 +	  finally show ?thesis .
   1.706 +	qed
   1.707 +      qed
   1.708 +    qed
   1.709 +    also have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k" by simp
   1.710 +    finally show ?thesis .
   1.711 +  qed
   1.712 +qed (simp_all)
   1.713 +
   1.714 +ML_setup {*
   1.715 +Context.>> (fn thy => (simpset_ref_of thy :=
   1.716 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
   1.717 +
   1.718 +lemma (in UP_cring) monom_mult_smult:
   1.719 +  "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^sub>2 monom P b n"
   1.720 +  by (rule up_eqI) simp_all
   1.721 +
   1.722 +lemma (in UP_cring) monom_one [simp]:
   1.723 +  "monom P \<one> 0 = \<one>\<^sub>2"
   1.724 +  by (rule up_eqI) simp_all
   1.725 +
   1.726 +lemma (in UP_cring) monom_one_mult:
   1.727 +  "monom P \<one> (n + m) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m"
   1.728 +proof (induct n)
   1.729 +  case 0 show ?case by simp
   1.730 +next
   1.731 +  case Suc then show ?case
   1.732 +    by (simp only: add_Suc monom_one_Suc) (simp add: UP_m_ac)
   1.733 +qed
   1.734 +
   1.735 +lemma (in UP_cring) monom_mult [simp]:
   1.736 +  assumes R: "a \<in> carrier R" "b \<in> carrier R"
   1.737 +  shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^sub>2 monom P b m"
   1.738 +proof -
   1.739 +  from R have "monom P (a \<otimes> b) (n + m) = monom P (a \<otimes> b \<otimes> \<one>) (n + m)" by simp
   1.740 +  also from R have "... = a \<otimes> b \<odot>\<^sub>2 monom P \<one> (n + m)"
   1.741 +    by (simp add: monom_mult_smult del: r_one)
   1.742 +  also have "... = a \<otimes> b \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m)"
   1.743 +    by (simp only: monom_one_mult)
   1.744 +  also from R have "... = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m))"
   1.745 +    by (simp add: UP_smult_assoc1)
   1.746 +  also from R have "... = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 (monom P \<one> m \<otimes>\<^sub>2 monom P \<one> n))"
   1.747 +    by (simp add: UP_m_comm)
   1.748 +  also from R have "... = a \<odot>\<^sub>2 ((b \<odot>\<^sub>2 monom P \<one> m) \<otimes>\<^sub>2 monom P \<one> n)"
   1.749 +    by (simp add: UP_smult_assoc2)
   1.750 +  also from R have "... = a \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 (b \<odot>\<^sub>2 monom P \<one> m))"
   1.751 +    by (simp add: UP_m_comm)
   1.752 +  also from R have "... = (a \<odot>\<^sub>2 monom P \<one> n) \<otimes>\<^sub>2 (b \<odot>\<^sub>2 monom P \<one> m)"
   1.753 +    by (simp add: UP_smult_assoc2)
   1.754 +  also from R have "... = monom P (a \<otimes> \<one>) n \<otimes>\<^sub>2 monom P (b \<otimes> \<one>) m"
   1.755 +    by (simp add: monom_mult_smult del: r_one)
   1.756 +  also from R have "... = monom P a n \<otimes>\<^sub>2 monom P b m" by simp
   1.757 +  finally show ?thesis .
   1.758 +qed
   1.759 +
   1.760 +lemma (in UP_cring) monom_a_inv [simp]:
   1.761 +  "a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^sub>2 monom P a n"
   1.762 +  by (rule up_eqI) simp_all
   1.763 +
   1.764 +lemma (in UP_cring) monom_inj:
   1.765 +  "inj_on (%a. monom P a n) (carrier R)"
   1.766 +proof (rule inj_onI)
   1.767 +  fix x y
   1.768 +  assume R: "x \<in> carrier R" "y \<in> carrier R" and eq: "monom P x n = monom P y n"
   1.769 +  then have "coeff P (monom P x n) n = coeff P (monom P y n) n" by simp
   1.770 +  with R show "x = y" by simp
   1.771 +qed
   1.772 +
   1.773 +subsection {* The Degree Function *}
   1.774 +
   1.775 +constdefs
   1.776 +  deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
   1.777 +  "deg R p == LEAST n. bound (zero R) n (coeff (UP R) p)"
   1.778 +
   1.779 +lemma (in UP_cring) deg_aboveI:
   1.780 +  "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n" 
   1.781 +  by (unfold deg_def P_def) (fast intro: Least_le)
   1.782 +(*
   1.783 +lemma coeff_bound_ex: "EX n. bound n (coeff p)"
   1.784 +proof -
   1.785 +  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   1.786 +  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   1.787 +  then show ?thesis ..
   1.788 +qed
   1.789 +  
   1.790 +lemma bound_coeff_obtain:
   1.791 +  assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
   1.792 +proof -
   1.793 +  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   1.794 +  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   1.795 +  with prem show P .
   1.796 +qed
   1.797 +*)
   1.798 +lemma (in UP_cring) deg_aboveD:
   1.799 +  "[| deg R p < m; p \<in> carrier P |] ==> coeff P p m = \<zero>"
   1.800 +proof -
   1.801 +  assume R: "p \<in> carrier P" and "deg R p < m"
   1.802 +  from R obtain n where "bound \<zero> n (coeff P p)" 
   1.803 +    by (auto simp add: UP_def P_def)
   1.804 +  then have "bound \<zero> (deg R p) (coeff P p)"
   1.805 +    by (auto simp: deg_def P_def dest: LeastI)
   1.806 +  then show ?thesis by (rule boundD)
   1.807 +qed
   1.808 +
   1.809 +lemma (in UP_cring) deg_belowI:
   1.810 +  assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
   1.811 +    and R: "p \<in> carrier P"
   1.812 +  shows "n <= deg R p"
   1.813 +-- {* Logically, this is a slightly stronger version of 
   1.814 +  @{thm [source] deg_aboveD} *}
   1.815 +proof (cases "n=0")
   1.816 +  case True then show ?thesis by simp
   1.817 +next
   1.818 +  case False then have "coeff P p n ~= \<zero>" by (rule non_zero)
   1.819 +  then have "~ deg R p < n" by (fast dest: deg_aboveD intro: R)
   1.820 +  then show ?thesis by arith
   1.821 +qed
   1.822 +
   1.823 +lemma (in UP_cring) lcoeff_nonzero_deg:
   1.824 +  assumes deg: "deg R p ~= 0" and R: "p \<in> carrier P"
   1.825 +  shows "coeff P p (deg R p) ~= \<zero>"
   1.826 +proof -
   1.827 +  from R obtain m where "deg R p <= m" and m_coeff: "coeff P p m ~= \<zero>"
   1.828 +  proof -
   1.829 +    have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
   1.830 +      by arith
   1.831 +(* TODO: why does proof not work with "1" *)
   1.832 +    from deg have "deg R p - 1 < (LEAST n. bound \<zero> n (coeff P p))"
   1.833 +      by (unfold deg_def P_def) arith
   1.834 +    then have "~ bound \<zero> (deg R p - 1) (coeff P p)" by (rule not_less_Least)
   1.835 +    then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
   1.836 +      by (unfold bound_def) fast
   1.837 +    then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
   1.838 +    then show ?thesis by auto 
   1.839 +  qed
   1.840 +  with deg_belowI R have "deg R p = m" by fastsimp
   1.841 +  with m_coeff show ?thesis by simp
   1.842 +qed
   1.843 +
   1.844 +lemma (in UP_cring) lcoeff_nonzero_nonzero:
   1.845 +  assumes deg: "deg R p = 0" and nonzero: "p ~= \<zero>\<^sub>2" and R: "p \<in> carrier P"
   1.846 +  shows "coeff P p 0 ~= \<zero>"
   1.847 +proof -
   1.848 +  have "EX m. coeff P p m ~= \<zero>"
   1.849 +  proof (rule classical)
   1.850 +    assume "~ ?thesis"
   1.851 +    with R have "p = \<zero>\<^sub>2" by (auto intro: up_eqI)
   1.852 +    with nonzero show ?thesis by contradiction
   1.853 +  qed
   1.854 +  then obtain m where coeff: "coeff P p m ~= \<zero>" ..
   1.855 +  then have "m <= deg R p" by (rule deg_belowI)
   1.856 +  then have "m = 0" by (simp add: deg)
   1.857 +  with coeff show ?thesis by simp
   1.858 +qed
   1.859 +
   1.860 +lemma (in UP_cring) lcoeff_nonzero:
   1.861 +  assumes neq: "p ~= \<zero>\<^sub>2" and R: "p \<in> carrier P"
   1.862 +  shows "coeff P p (deg R p) ~= \<zero>"
   1.863 +proof (cases "deg R p = 0")
   1.864 +  case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero)
   1.865 +next
   1.866 +  case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg)
   1.867 +qed
   1.868 +
   1.869 +lemma (in UP_cring) deg_eqI:
   1.870 +  "[| !!m. n < m ==> coeff P p m = \<zero>;
   1.871 +      !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
   1.872 +by (fast intro: le_anti_sym deg_aboveI deg_belowI)
   1.873 +
   1.874 +(* Degree and polynomial operations *)
   1.875 +
   1.876 +lemma (in UP_cring) deg_add [simp]:
   1.877 +  assumes R: "p \<in> carrier P" "q \<in> carrier P"
   1.878 +  shows "deg R (p \<oplus>\<^sub>2 q) <= max (deg R p) (deg R q)"
   1.879 +proof (cases "deg R p <= deg R q")
   1.880 +  case True show ?thesis
   1.881 +    by (rule deg_aboveI) (simp_all add: True R deg_aboveD) 
   1.882 +next
   1.883 +  case False show ?thesis
   1.884 +    by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
   1.885 +qed
   1.886 +
   1.887 +lemma (in UP_cring) deg_monom_le:
   1.888 +  "a \<in> carrier R ==> deg R (monom P a n) <= n"
   1.889 +  by (intro deg_aboveI) simp_all
   1.890 +
   1.891 +lemma (in UP_cring) deg_monom [simp]:
   1.892 +  "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
   1.893 +  by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
   1.894 +
   1.895 +lemma (in UP_cring) deg_const [simp]:
   1.896 +  assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
   1.897 +proof (rule le_anti_sym)
   1.898 +  show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R)
   1.899 +next
   1.900 +  show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
   1.901 +qed
   1.902 +
   1.903 +lemma (in UP_cring) deg_zero [simp]:
   1.904 +  "deg R \<zero>\<^sub>2 = 0"
   1.905 +proof (rule le_anti_sym)
   1.906 +  show "deg R \<zero>\<^sub>2 <= 0" by (rule deg_aboveI) simp_all
   1.907 +next
   1.908 +  show "0 <= deg R \<zero>\<^sub>2" by (rule deg_belowI) simp_all
   1.909 +qed
   1.910 +
   1.911 +lemma (in UP_cring) deg_one [simp]:
   1.912 +  "deg R \<one>\<^sub>2 = 0"
   1.913 +proof (rule le_anti_sym)
   1.914 +  show "deg R \<one>\<^sub>2 <= 0" by (rule deg_aboveI) simp_all
   1.915 +next
   1.916 +  show "0 <= deg R \<one>\<^sub>2" by (rule deg_belowI) simp_all
   1.917 +qed
   1.918 +
   1.919 +lemma (in UP_cring) deg_uminus [simp]:
   1.920 +  assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^sub>2 p) = deg R p"
   1.921 +proof (rule le_anti_sym)
   1.922 +  show "deg R (\<ominus>\<^sub>2 p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
   1.923 +next
   1.924 +  show "deg R p <= deg R (\<ominus>\<^sub>2 p)" 
   1.925 +    by (simp add: deg_belowI lcoeff_nonzero_deg
   1.926 +      inj_on_iff [OF a_inv_inj, of _ "\<zero>", simplified] R)
   1.927 +qed
   1.928 +
   1.929 +lemma (in UP_domain) deg_smult_ring:
   1.930 +  "[| a \<in> carrier R; p \<in> carrier P |] ==>
   1.931 +  deg R (a \<odot>\<^sub>2 p) <= (if a = \<zero> then 0 else deg R p)"
   1.932 +  by (cases "a = \<zero>") (simp add: deg_aboveI deg_aboveD)+
   1.933 +
   1.934 +lemma (in UP_domain) deg_smult [simp]:
   1.935 +  assumes R: "a \<in> carrier R" "p \<in> carrier P"
   1.936 +  shows "deg R (a \<odot>\<^sub>2 p) = (if a = \<zero> then 0 else deg R p)"
   1.937 +proof (rule le_anti_sym)
   1.938 +  show "deg R (a \<odot>\<^sub>2 p) <= (if a = \<zero> then 0 else deg R p)"
   1.939 +    by (rule deg_smult_ring)
   1.940 +next
   1.941 +  show "(if a = \<zero> then 0 else deg R p) <= deg R (a \<odot>\<^sub>2 p)"
   1.942 +  proof (cases "a = \<zero>")
   1.943 +  qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R)
   1.944 +qed
   1.945 +
   1.946 +lemma (in UP_cring) deg_mult_cring:
   1.947 +  assumes R: "p \<in> carrier P" "q \<in> carrier P"
   1.948 +  shows "deg R (p \<otimes>\<^sub>2 q) <= deg R p + deg R q"
   1.949 +proof (rule deg_aboveI)
   1.950 +  fix m
   1.951 +  assume boundm: "deg R p + deg R q < m"
   1.952 +  {
   1.953 +    fix k i
   1.954 +    assume boundk: "deg R p + deg R q < k"
   1.955 +    then have "coeff P p i \<otimes> coeff P q (k - i) = \<zero>"
   1.956 +    proof (cases "deg R p < i")
   1.957 +      case True then show ?thesis by (simp add: deg_aboveD R)
   1.958 +    next
   1.959 +      case False with boundk have "deg R q < k - i" by arith
   1.960 +      then show ?thesis by (simp add: deg_aboveD R)
   1.961 +    qed
   1.962 +  }
   1.963 +  with boundm R show "coeff P (p \<otimes>\<^sub>2 q) m = \<zero>" by simp
   1.964 +qed (simp add: R)
   1.965 +
   1.966 +ML_setup {*
   1.967 +Context.>> (fn thy => (simpset_ref_of thy :=
   1.968 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   1.969 +
   1.970 +lemma (in UP_domain) deg_mult [simp]:
   1.971 +  "[| p ~= \<zero>\<^sub>2; q ~= \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P |] ==>
   1.972 +  deg R (p \<otimes>\<^sub>2 q) = deg R p + deg R q"
   1.973 +proof (rule le_anti_sym)
   1.974 +  assume "p \<in> carrier P" " q \<in> carrier P"
   1.975 +  show "deg R (p \<otimes>\<^sub>2 q) <= deg R p + deg R q" by (rule deg_mult_cring)
   1.976 +next
   1.977 +  let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
   1.978 +  assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^sub>2" "q ~= \<zero>\<^sub>2"
   1.979 +  have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
   1.980 +  show "deg R p + deg R q <= deg R (p \<otimes>\<^sub>2 q)"
   1.981 +  proof (rule deg_belowI, simp add: R)
   1.982 +    have "finsum R ?s {.. deg R p + deg R q}
   1.983 +      = finsum R ?s ({.. deg R p(} Un {deg R p .. deg R p + deg R q})"
   1.984 +      by (simp only: ivl_disj_un_one)
   1.985 +    also have "... = finsum R ?s {deg R p .. deg R p + deg R q}"
   1.986 +      by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
   1.987 +        deg_aboveD less_add_diff R Pi_def)
   1.988 +    also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})"
   1.989 +      by (simp only: ivl_disj_un_singleton)
   1.990 +    also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" 
   1.991 +      by (simp cong: finsum_cong add: finsum_Un_disjoint
   1.992 +	ivl_disj_int_singleton deg_aboveD R Pi_def)
   1.993 +    finally have "finsum R ?s {.. deg R p + deg R q} 
   1.994 +      = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
   1.995 +    with nz show "finsum R ?s {.. deg R p + deg R q} ~= \<zero>"
   1.996 +      by (simp add: integral_iff lcoeff_nonzero R)
   1.997 +    qed (simp add: R)
   1.998 +  qed
   1.999 +
  1.1000 +lemma (in UP_cring) coeff_finsum:
  1.1001 +  assumes fin: "finite A"
  1.1002 +  shows "p \<in> A -> carrier P ==>
  1.1003 +    coeff P (finsum P p A) k == finsum R (%i. coeff P (p i) k) A"
  1.1004 +  using fin by induct (auto simp: Pi_def)
  1.1005 +
  1.1006 +ML_setup {*
  1.1007 +Context.>> (fn thy => (simpset_ref_of thy :=
  1.1008 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
  1.1009 +
  1.1010 +lemma (in UP_cring) up_repr:
  1.1011 +  assumes R: "p \<in> carrier P"
  1.1012 +  shows "finsum P (%i. monom P (coeff P p i) i) {..deg R p} = p"
  1.1013 +proof (rule up_eqI)
  1.1014 +  let ?s = "(%i. monom P (coeff P p i) i)"
  1.1015 +  fix k
  1.1016 +  from R have RR: "!!i. (if i = k then coeff P p i else \<zero>) \<in> carrier R"
  1.1017 +    by simp
  1.1018 +  show "coeff P (finsum P ?s {..deg R p}) k = coeff P p k"
  1.1019 +  proof (cases "k <= deg R p")
  1.1020 +    case True
  1.1021 +    hence "coeff P (finsum P ?s {..deg R p}) k = 
  1.1022 +          coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k"
  1.1023 +      by (simp only: ivl_disj_un_one)
  1.1024 +    also from True
  1.1025 +    have "... = coeff P (finsum P ?s {..k}) k"
  1.1026 +      by (simp cong: finsum_cong add: finsum_Un_disjoint
  1.1027 +	ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
  1.1028 +    also
  1.1029 +    have "... = coeff P (finsum P ?s ({..k(} Un {k})) k"
  1.1030 +      by (simp only: ivl_disj_un_singleton)
  1.1031 +    also have "... = coeff P p k"
  1.1032 +      by (simp cong: finsum_cong add: setsum_Un_disjoint
  1.1033 +	ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
  1.1034 +    finally show ?thesis .
  1.1035 +  next
  1.1036 +    case False
  1.1037 +    hence "coeff P (finsum P ?s {..deg R p}) k = 
  1.1038 +          coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k"
  1.1039 +      by (simp only: ivl_disj_un_singleton)
  1.1040 +    also from False have "... = coeff P p k"
  1.1041 +      by (simp cong: finsum_cong add: setsum_Un_disjoint ivl_disj_int_singleton
  1.1042 +        coeff_finsum deg_aboveD R Pi_def)
  1.1043 +    finally show ?thesis .
  1.1044 +  qed
  1.1045 +qed (simp_all add: R Pi_def)
  1.1046 +
  1.1047 +lemma (in UP_cring) up_repr_le:
  1.1048 +  "[| deg R p <= n; p \<in> carrier P |] ==>
  1.1049 +  finsum P (%i. monom P (coeff P p i) i) {..n} = p"
  1.1050 +proof -
  1.1051 +  let ?s = "(%i. monom P (coeff P p i) i)"
  1.1052 +  assume R: "p \<in> carrier P" and "deg R p <= n"
  1.1053 +  then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {)deg R p..n})"
  1.1054 +    by (simp only: ivl_disj_un_one)
  1.1055 +  also have "... = finsum P ?s {..deg R p}"
  1.1056 +    by (simp cong: UP_finsum_cong add: UP_finsum_Un_disjoint ivl_disj_int_one
  1.1057 +      deg_aboveD R Pi_def)
  1.1058 +  also have "... = p" by (rule up_repr)
  1.1059 +  finally show ?thesis .
  1.1060 +qed
  1.1061 +
  1.1062 +ML_setup {*
  1.1063 +Context.>> (fn thy => (simpset_ref_of thy :=
  1.1064 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
  1.1065 +
  1.1066 +subsection {* Polynomial over an Integral Domain are an Integral Domain *}
  1.1067 +
  1.1068 +lemma domainI:
  1.1069 +  assumes cring: "cring R"
  1.1070 +    and one_not_zero: "one R ~= zero R"
  1.1071 +    and integral: "!!a b. [| mult R a b = zero R; a \<in> carrier R;
  1.1072 +      b \<in> carrier R |] ==> a = zero R | b = zero R"
  1.1073 +  shows "domain R"
  1.1074 +  by (auto intro!: domain.intro domain_axioms.intro cring.axioms prems
  1.1075 +    del: disjCI)
  1.1076 +
  1.1077 +lemma (in UP_domain) UP_one_not_zero:
  1.1078 +  "\<one>\<^sub>2 ~= \<zero>\<^sub>2"
  1.1079 +proof
  1.1080 +  assume "\<one>\<^sub>2 = \<zero>\<^sub>2"
  1.1081 +  hence "coeff P \<one>\<^sub>2 0 = (coeff P \<zero>\<^sub>2 0)" by simp
  1.1082 +  hence "\<one> = \<zero>" by simp
  1.1083 +  with one_not_zero show "False" by contradiction
  1.1084 +qed
  1.1085 +
  1.1086 +lemma (in UP_domain) UP_integral:
  1.1087 +  "[| p \<otimes>\<^sub>2 q = \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P |] ==> p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2"
  1.1088 +proof -
  1.1089 +  fix p q
  1.1090 +  assume pq: "p \<otimes>\<^sub>2 q = \<zero>\<^sub>2" and R: "p \<in> carrier P" "q \<in> carrier P"
  1.1091 +  show "p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2"
  1.1092 +  proof (rule classical)
  1.1093 +    assume c: "~ (p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2)"
  1.1094 +    with R have "deg R p + deg R q = deg R (p \<otimes>\<^sub>2 q)" by simp
  1.1095 +    also from pq have "... = 0" by simp
  1.1096 +    finally have "deg R p + deg R q = 0" .
  1.1097 +    then have f1: "deg R p = 0 & deg R q = 0" by simp
  1.1098 +    from f1 R have "p = finsum P (%i. (monom P (coeff P p i) i)) {..0}"
  1.1099 +      by (simp only: up_repr_le)
  1.1100 +    also from R have "... = monom P (coeff P p 0) 0" by simp
  1.1101 +    finally have p: "p = monom P (coeff P p 0) 0" .
  1.1102 +    from f1 R have "q = finsum P (%i. (monom P (coeff P q i) i)) {..0}"
  1.1103 +      by (simp only: up_repr_le)
  1.1104 +    also from R have "... = monom P (coeff P q 0) 0" by simp
  1.1105 +    finally have q: "q = monom P (coeff P q 0) 0" .
  1.1106 +    from R have "coeff P p 0 \<otimes> coeff P q 0 = coeff P (p \<otimes>\<^sub>2 q) 0" by simp
  1.1107 +    also from pq have "... = \<zero>" by simp
  1.1108 +    finally have "coeff P p 0 \<otimes> coeff P q 0 = \<zero>" .
  1.1109 +    with R have "coeff P p 0 = \<zero> | coeff P q 0 = \<zero>"
  1.1110 +      by (simp add: R.integral_iff)
  1.1111 +    with p q show "p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2" by fastsimp
  1.1112 +  qed
  1.1113 +qed
  1.1114 +
  1.1115 +theorem (in UP_domain) UP_domain:
  1.1116 +  "domain P"
  1.1117 +  by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI)
  1.1118 +
  1.1119 +text {*
  1.1120 +  Instantiation of results from @{term domain}.
  1.1121 +*}
  1.1122 +
  1.1123 +lemmas (in UP_domain) UP_zero_not_one [simp] =
  1.1124 +  domain.zero_not_one [OF UP_domain]
  1.1125 +
  1.1126 +lemmas (in UP_domain) UP_integral_iff =
  1.1127 +  domain.integral_iff [OF UP_domain]
  1.1128 +
  1.1129 +lemmas (in UP_domain) UP_m_lcancel =
  1.1130 +  domain.m_lcancel [OF UP_domain]
  1.1131 +
  1.1132 +lemmas (in UP_domain) UP_m_rcancel =
  1.1133 +  domain.m_rcancel [OF UP_domain]
  1.1134 +
  1.1135 +lemma (in UP_domain) smult_integral:
  1.1136 +  "[| a \<odot>\<^sub>2 p = \<zero>\<^sub>2; a \<in> carrier R; p \<in> carrier P |] ==> a = \<zero> | p = \<zero>\<^sub>2"
  1.1137 +  by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff
  1.1138 +    inj_on_iff [OF monom_inj, of _ "\<zero>", simplified])
  1.1139 +
  1.1140 +subsection {* Evaluation Homomorphism *}
  1.1141 +
  1.1142 +ML_setup {*
  1.1143 +Context.>> (fn thy => (simpset_ref_of thy :=
  1.1144 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
  1.1145 +
  1.1146 +(* alternative congruence rule (more efficient)
  1.1147 +lemma (in abelian_monoid) finsum_cong2:
  1.1148 +  "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
  1.1149 +  !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
  1.1150 +  sorry
  1.1151 +*)
  1.1152 +
  1.1153 +theorem (in cring) diagonal_sum:
  1.1154 +  "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
  1.1155 +  finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..n + m} =
  1.1156 +  finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
  1.1157 +proof -
  1.1158 +  assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
  1.1159 +  {
  1.1160 +    fix j
  1.1161 +    have "j <= n + m ==>
  1.1162 +      finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..j} =
  1.1163 +      finsum R (%k. finsum R (%i. f k \<otimes> g i) {..j - k}) {..j}"
  1.1164 +    proof (induct j)
  1.1165 +      case 0 from Rf Rg show ?case by (simp add: Pi_def)
  1.1166 +    next
  1.1167 +      case (Suc j) 
  1.1168 +      (* The following could be simplified if there was a reasoner for
  1.1169 +	total orders integrated with simip. *)
  1.1170 +      have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
  1.1171 +	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
  1.1172 +      have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
  1.1173 +	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
  1.1174 +      have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
  1.1175 +	using Suc by (auto intro!: funcset_mem [OF Rf])
  1.1176 +      have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
  1.1177 +	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
  1.1178 +      have R11: "g 0 \<in> carrier R"
  1.1179 +	using Suc by (auto intro!: funcset_mem [OF Rg])
  1.1180 +      from Suc show ?case
  1.1181 +	by (simp cong: finsum_cong add: Suc_diff_le a_ac
  1.1182 +	  Pi_def R6 R8 R9 R10 R11)
  1.1183 +    qed
  1.1184 +  }
  1.1185 +  then show ?thesis by fast
  1.1186 +qed
  1.1187 +
  1.1188 +lemma (in abelian_monoid) boundD_carrier:
  1.1189 +  "[| bound \<zero> n f; n < m |] ==> f m \<in> carrier G"
  1.1190 +  by auto
  1.1191 +
  1.1192 +theorem (in cring) cauchy_product:
  1.1193 +  assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
  1.1194 +    and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
  1.1195 +  shows "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
  1.1196 +    finsum R f {..n} \<otimes> finsum R g {..m}"
  1.1197 +(* State revese direction? *)
  1.1198 +proof -
  1.1199 +  have f: "!!x. f x \<in> carrier R"
  1.1200 +  proof -
  1.1201 +    fix x
  1.1202 +    show "f x \<in> carrier R"
  1.1203 +      using Rf bf boundD_carrier by (cases "x <= n") (auto simp: Pi_def)
  1.1204 +  qed
  1.1205 +  have g: "!!x. g x \<in> carrier R"
  1.1206 +  proof -
  1.1207 +    fix x
  1.1208 +    show "g x \<in> carrier R"
  1.1209 +      using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def)
  1.1210 +  qed
  1.1211 +  from f g have "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
  1.1212 +    finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
  1.1213 +    by (simp add: diagonal_sum Pi_def)
  1.1214 +  also have "... = finsum R
  1.1215 +      (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) ({..n} Un {)n..n + m})"
  1.1216 +    by (simp only: ivl_disj_un_one)
  1.1217 +  also from f g have "... = finsum R
  1.1218 +      (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n}"
  1.1219 +    by (simp cong: finsum_cong
  1.1220 +      add: boundD [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
  1.1221 +  also from f g have "... = finsum R
  1.1222 +      (%k. finsum R (%i. f k \<otimes> g i) ({..m} Un {)m..n + m - k})) {..n}"
  1.1223 +    by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
  1.1224 +  also from f g have "... = finsum R
  1.1225 +      (%k. finsum R (%i. f k \<otimes> g i) {..m}) {..n}"
  1.1226 +    by (simp cong: finsum_cong
  1.1227 +      add: boundD [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
  1.1228 +  also from f g have "... = finsum R f {..n} \<otimes> finsum R g {..m}"
  1.1229 +    by (simp add: finsum_ldistr diagonal_sum Pi_def,
  1.1230 +      simp cong: finsum_cong add: finsum_rdistr Pi_def)
  1.1231 +  finally show ?thesis .
  1.1232 +qed
  1.1233 +
  1.1234 +lemma (in UP_cring) const_ring_hom:
  1.1235 +  "(%a. monom P a 0) \<in> ring_hom R P"
  1.1236 +  by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
  1.1237 +
  1.1238 +constdefs
  1.1239 +  eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
  1.1240 +          'a => 'b, 'b, nat => 'a] => 'b"
  1.1241 +  "eval R S phi s == (\<lambda>p \<in> carrier (UP R).
  1.1242 +    finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p})"
  1.1243 +(*
  1.1244 +  "eval R S phi s p == if p \<in> carrier (UP R)
  1.1245 +  then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p}
  1.1246 +  else arbitrary"
  1.1247 +*)
  1.1248 +                                                         
  1.1249 +locale ring_hom_UP_cring = ring_hom_cring R S + UP_cring R
  1.1250 +
  1.1251 +lemma (in ring_hom_UP_cring) eval_on_carrier:
  1.1252 +  "p \<in> carrier P ==>
  1.1253 +    eval R S phi s p =
  1.1254 +    finsum S (%i. mult S (phi (coeff P p i)) (pow S s i)) {..deg R p}"
  1.1255 +  by (unfold eval_def, fold P_def) simp
  1.1256 +
  1.1257 +lemma (in ring_hom_UP_cring) eval_extensional:
  1.1258 +  "eval R S phi s \<in> extensional (carrier P)"
  1.1259 +  by (unfold eval_def, fold P_def) simp
  1.1260 +
  1.1261 +theorem (in ring_hom_UP_cring) eval_ring_hom:
  1.1262 +  "s \<in> carrier S ==> eval R S h s \<in> ring_hom P S"
  1.1263 +proof (rule ring_hom_memI)
  1.1264 +  fix p
  1.1265 +  assume RS: "p \<in> carrier P" "s \<in> carrier S"
  1.1266 +  then show "eval R S h s p \<in> carrier S"
  1.1267 +    by (simp only: eval_on_carrier) (simp add: Pi_def)
  1.1268 +next
  1.1269 +  fix p q
  1.1270 +  assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S"
  1.1271 +  then show "eval R S h s (p \<otimes>\<^sub>3 q) = eval R S h s p \<otimes>\<^sub>2 eval R S h s q"
  1.1272 +  proof (simp only: eval_on_carrier UP_mult_closed)
  1.1273 +    from RS have
  1.1274 +      "finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<otimes>\<^sub>3 q)} =
  1.1275 +      finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1.1276 +        ({..deg R (p \<otimes>\<^sub>3 q)} Un {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q})"
  1.1277 +      by (simp cong: finsum_cong
  1.1278 +	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
  1.1279 +	del: coeff_mult)
  1.1280 +    also from RS have "... =
  1.1281 +      finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p + deg R q}"
  1.1282 +      by (simp only: ivl_disj_un_one deg_mult_cring)
  1.1283 +    also from RS have "... =
  1.1284 +      finsum S (%i.
  1.1285 +        finsum S (%k. 
  1.1286 +        (h (coeff P p k) \<otimes>\<^sub>2 h (coeff P q (i-k))) \<otimes>\<^sub>2 (s (^)\<^sub>2 k \<otimes>\<^sub>2 s (^)\<^sub>2 (i-k)))
  1.1287 +      {..i}) {..deg R p + deg R q}"
  1.1288 +      by (simp cong: finsum_cong add: nat_pow_mult Pi_def
  1.1289 +	S.m_ac S.finsum_rdistr)
  1.1290 +    also from RS have "... =
  1.1291 +      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
  1.1292 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
  1.1293 +      by (simp add: S.cauchy_product [THEN sym] boundI deg_aboveD S.m_ac
  1.1294 +	Pi_def)
  1.1295 +    finally show
  1.1296 +      "finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<otimes>\<^sub>3 q)} =
  1.1297 +      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
  1.1298 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}" .
  1.1299 +  qed
  1.1300 +next
  1.1301 +  fix p q
  1.1302 +  assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S"
  1.1303 +  then show "eval R S h s (p \<oplus>\<^sub>3 q) = eval R S h s p \<oplus>\<^sub>2 eval R S h s q"
  1.1304 +  proof (simp only: eval_on_carrier UP_a_closed)
  1.1305 +    from RS have
  1.1306 +      "finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<oplus>\<^sub>3 q)} =
  1.1307 +      finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1.1308 +        ({..deg R (p \<oplus>\<^sub>3 q)} Un {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)})"
  1.1309 +      by (simp cong: finsum_cong
  1.1310 +	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
  1.1311 +	del: coeff_add)
  1.1312 +    also from RS have "... =
  1.1313 +      finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1.1314 +        {..max (deg R p) (deg R q)}"
  1.1315 +      by (simp add: ivl_disj_un_one)
  1.1316 +    also from RS have "... =
  1.1317 +      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)} \<oplus>\<^sub>2
  1.1318 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)}"
  1.1319 +      by (simp cong: finsum_cong
  1.1320 +	add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
  1.1321 +    also have "... =
  1.1322 +      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1.1323 +        ({..deg R p} Un {)deg R p..max (deg R p) (deg R q)}) \<oplus>\<^sub>2
  1.1324 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1.1325 +        ({..deg R q} Un {)deg R q..max (deg R p) (deg R q)})"
  1.1326 +      by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
  1.1327 +    also from RS have "... =
  1.1328 +      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
  1.1329 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
  1.1330 +      by (simp cong: finsum_cong
  1.1331 +	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
  1.1332 +    finally show
  1.1333 +      "finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<oplus>\<^sub>3 q)} =
  1.1334 +      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
  1.1335 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
  1.1336 +      .
  1.1337 +  qed
  1.1338 +next
  1.1339 +  assume S: "s \<in> carrier S"
  1.1340 +  then show "eval R S h s \<one>\<^sub>3 = \<one>\<^sub>2"
  1.1341 +    by (simp only: eval_on_carrier UP_one_closed) simp
  1.1342 +qed
  1.1343 +
  1.1344 +text {* Instantiation of ring homomorphism lemmas. *}
  1.1345 +
  1.1346 +lemma (in ring_hom_UP_cring) ring_hom_cring_P_S:
  1.1347 +  "s \<in> carrier S ==> ring_hom_cring P S (eval R S h s)"
  1.1348 +  by (fast intro!: ring_hom_cring.intro UP_cring cring.axioms prems
  1.1349 +  intro: ring_hom_cring_axioms.intro eval_ring_hom)
  1.1350 +
  1.1351 +lemma (in ring_hom_UP_cring) UP_hom_closed [intro, simp]:
  1.1352 +  "[| s \<in> carrier S; p \<in> carrier P |] ==> eval R S h s p \<in> carrier S"
  1.1353 +  by (rule ring_hom_cring.hom_closed [OF ring_hom_cring_P_S])
  1.1354 +
  1.1355 +lemma (in ring_hom_UP_cring) UP_hom_mult [simp]:
  1.1356 +  "[| s \<in> carrier S; p \<in> carrier P; q \<in> carrier P |] ==>
  1.1357 +  eval R S h s (p \<otimes>\<^sub>3 q) = eval R S h s p \<otimes>\<^sub>2 eval R S h s q"
  1.1358 +  by (rule ring_hom_cring.hom_mult [OF ring_hom_cring_P_S])
  1.1359 +
  1.1360 +lemma (in ring_hom_UP_cring) UP_hom_add [simp]:
  1.1361 +  "[| s \<in> carrier S; p \<in> carrier P; q \<in> carrier P |] ==>
  1.1362 +  eval R S h s (p \<oplus>\<^sub>3 q) = eval R S h s p \<oplus>\<^sub>2 eval R S h s q"
  1.1363 +  by (rule ring_hom_cring.hom_add [OF ring_hom_cring_P_S])
  1.1364 +
  1.1365 +lemma (in ring_hom_UP_cring) UP_hom_one [simp]:
  1.1366 +  "s \<in> carrier S ==> eval R S h s \<one>\<^sub>3 = \<one>\<^sub>2"
  1.1367 +  by (rule ring_hom_cring.hom_one [OF ring_hom_cring_P_S])
  1.1368 +
  1.1369 +lemma (in ring_hom_UP_cring) UP_hom_zero [simp]:
  1.1370 +  "s \<in> carrier S ==> eval R S h s \<zero>\<^sub>3 = \<zero>\<^sub>2"
  1.1371 +  by (rule ring_hom_cring.hom_zero [OF ring_hom_cring_P_S])
  1.1372 +
  1.1373 +lemma (in ring_hom_UP_cring) UP_hom_a_inv [simp]:
  1.1374 +  "[| s \<in> carrier S; p \<in> carrier P |] ==>
  1.1375 +  (eval R S h s) (\<ominus>\<^sub>3 p) = \<ominus>\<^sub>2 (eval R S h s) p"
  1.1376 +  by (rule ring_hom_cring.hom_a_inv [OF ring_hom_cring_P_S])
  1.1377 +
  1.1378 +lemma (in ring_hom_UP_cring) UP_hom_finsum [simp]:
  1.1379 +  "[| s \<in> carrier S; finite A; f \<in> A -> carrier P |] ==>
  1.1380 +  (eval R S h s) (finsum P f A) = finsum S (eval R S h s o f) A"
  1.1381 +  by (rule ring_hom_cring.hom_finsum [OF ring_hom_cring_P_S])
  1.1382 +
  1.1383 +lemma (in ring_hom_UP_cring) UP_hom_finprod [simp]:
  1.1384 +  "[| s \<in> carrier S; finite A; f \<in> A -> carrier P |] ==>
  1.1385 +  (eval R S h s) (finprod P f A) = finprod S (eval R S h s o f) A"
  1.1386 +  by (rule ring_hom_cring.hom_finprod [OF ring_hom_cring_P_S])
  1.1387 +
  1.1388 +text {* Further properties of the evaluation homomorphism. *}
  1.1389 +
  1.1390 +(* The following lemma could be proved in UP\_cring with the additional
  1.1391 +   assumption that h is closed. *)
  1.1392 +
  1.1393 +lemma (in ring_hom_UP_cring) eval_const:
  1.1394 +  "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
  1.1395 +  by (simp only: eval_on_carrier monom_closed) simp
  1.1396 +
  1.1397 +text {* The following proof is complicated by the fact that in arbitrary
  1.1398 +  rings one might have @{term "one R = zero R"}. *}
  1.1399 +
  1.1400 +(* TODO: simplify by cases "one R = zero R" *)
  1.1401 +
  1.1402 +lemma (in ring_hom_UP_cring) eval_monom1:
  1.1403 +  "s \<in> carrier S ==> eval R S h s (monom P \<one> 1) = s"
  1.1404 +proof (simp only: eval_on_carrier monom_closed R.one_closed)
  1.1405 +  assume S: "s \<in> carrier S"
  1.1406 +  then have "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1.1407 +      {..deg R (monom P \<one> 1)} =
  1.1408 +    finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1.1409 +      ({..deg R (monom P \<one> 1)} Un {)deg R (monom P \<one> 1)..1})"
  1.1410 +    by (simp cong: finsum_cong del: coeff_monom
  1.1411 +      add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
  1.1412 +  also have "... = 
  1.1413 +    finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..1}"
  1.1414 +    by (simp only: ivl_disj_un_one deg_monom_le R.one_closed)
  1.1415 +  also have "... = s"
  1.1416 +  proof (cases "s = \<zero>\<^sub>2")
  1.1417 +    case True then show ?thesis by (simp add: Pi_def)
  1.1418 +  next
  1.1419 +    case False with S show ?thesis by (simp add: Pi_def)
  1.1420 +  qed
  1.1421 +  finally show "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1.1422 +      {..deg R (monom P \<one> 1)} = s" .
  1.1423 +qed
  1.1424 +
  1.1425 +lemma (in UP_cring) monom_pow:
  1.1426 +  assumes R: "a \<in> carrier R"
  1.1427 +  shows "(monom P a n) (^)\<^sub>2 m = monom P (a (^) m) (n * m)"
  1.1428 +proof (induct m)
  1.1429 +  case 0 from R show ?case by simp
  1.1430 +next
  1.1431 +  case Suc with R show ?case
  1.1432 +    by (simp del: monom_mult add: monom_mult [THEN sym] add_commute)
  1.1433 +qed
  1.1434 +
  1.1435 +lemma (in ring_hom_cring) hom_pow [simp]:
  1.1436 +  "x \<in> carrier R ==> h (x (^) n) = h x (^)\<^sub>2 (n::nat)"
  1.1437 +  by (induct n) simp_all
  1.1438 +
  1.1439 +lemma (in ring_hom_UP_cring) UP_hom_pow [simp]:
  1.1440 +  "[| s \<in> carrier S; p \<in> carrier P |] ==>
  1.1441 +  (eval R S h s) (p (^)\<^sub>3 n) = eval R S h s p (^)\<^sub>2 (n::nat)"
  1.1442 +  by (rule ring_hom_cring.hom_pow [OF ring_hom_cring_P_S])
  1.1443 +
  1.1444 +lemma (in ring_hom_UP_cring) eval_monom:
  1.1445 +  "[| s \<in> carrier S; r \<in> carrier R |] ==>
  1.1446 +  eval R S h s (monom P r n) = h r \<otimes>\<^sub>2 s (^)\<^sub>2 n"
  1.1447 +proof -
  1.1448 +  assume RS: "s \<in> carrier S" "r \<in> carrier R"
  1.1449 +  then have "eval R S h s (monom P r n) =
  1.1450 +    eval R S h s (monom P r 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 n)"
  1.1451 +    by (simp del: monom_mult UP_hom_mult UP_hom_pow
  1.1452 +      add: monom_mult [THEN sym] monom_pow)
  1.1453 +  also from RS eval_monom1 have "... = h r \<otimes>\<^sub>2 s (^)\<^sub>2 n"
  1.1454 +    by (simp add: eval_const)
  1.1455 +  finally show ?thesis .
  1.1456 +qed
  1.1457 +
  1.1458 +lemma (in ring_hom_UP_cring) eval_smult:
  1.1459 +  "[| s \<in> carrier S; r \<in> carrier R; p \<in> carrier P |] ==>
  1.1460 +  eval R S h s (r \<odot>\<^sub>3 p) = h r \<otimes>\<^sub>2 eval R S h s p"
  1.1461 +  by (simp add: monom_mult_is_smult [THEN sym] eval_const)
  1.1462 +
  1.1463 +lemma ring_hom_cringI:
  1.1464 +  assumes "cring R"
  1.1465 +    and "cring S"
  1.1466 +    and "h \<in> ring_hom R S"
  1.1467 +  shows "ring_hom_cring R S h"
  1.1468 +  by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
  1.1469 +    cring.axioms prems)
  1.1470 +
  1.1471 +lemma (in ring_hom_UP_cring) UP_hom_unique:
  1.1472 +  assumes Phi: "Phi \<in> ring_hom P S" "Phi (monom P \<one> (Suc 0)) = s"
  1.1473 +      "!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r"
  1.1474 +    and Psi: "Psi \<in> ring_hom P S" "Psi (monom P \<one> (Suc 0)) = s"
  1.1475 +      "!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r"
  1.1476 +    and RS: "s \<in> carrier S" "p \<in> carrier P"
  1.1477 +  shows "Phi p = Psi p"
  1.1478 +proof -
  1.1479 +  have Phi_hom: "ring_hom_cring P S Phi"
  1.1480 +    by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
  1.1481 +  have Psi_hom: "ring_hom_cring P S Psi"
  1.1482 +    by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
  1.1483 +thm monom_mult
  1.1484 +  have "Phi p = Phi (finsum P
  1.1485 +    (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
  1.1486 +    by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
  1.1487 +  also have "... = Psi (finsum P
  1.1488 +    (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
  1.1489 +    by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom] 
  1.1490 +      ring_hom_cring.hom_mult [OF Phi_hom]
  1.1491 +      ring_hom_cring.hom_pow [OF Phi_hom] Phi
  1.1492 +      ring_hom_cring.hom_finsum [OF Psi_hom] 
  1.1493 +      ring_hom_cring.hom_mult [OF Psi_hom]
  1.1494 +      ring_hom_cring.hom_pow [OF Psi_hom] Psi RS Pi_def comp_def)
  1.1495 +  also have "... = Psi p"
  1.1496 +    by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
  1.1497 +  finally show ?thesis .
  1.1498 +qed
  1.1499 +
  1.1500 +
  1.1501 +theorem (in ring_hom_UP_cring) UP_universal_property:
  1.1502 +  "s \<in> carrier S ==>
  1.1503 +  EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
  1.1504 +    Phi (monom P \<one> 1) = s & 
  1.1505 +    (ALL r : carrier R. Phi (monom P r 0) = h r)"
  1.1506 +  using eval_monom1                              
  1.1507 +  apply (auto intro: eval_ring_hom eval_const eval_extensional)
  1.1508 +  apply (rule extensionalityI)                                 
  1.1509 +  apply (auto intro: UP_hom_unique)                            
  1.1510 +  done                                                         
  1.1511 +
  1.1512 +subsection {* Sample application of evaluation homomorphism *}
  1.1513 +
  1.1514 +lemma ring_hom_UP_cringI:
  1.1515 +  assumes "cring R"
  1.1516 +    and "cring S"
  1.1517 +    and "h \<in> ring_hom R S"
  1.1518 +  shows "ring_hom_UP_cring R S h"
  1.1519 +  by (fast intro: ring_hom_UP_cring.intro ring_hom_cring_axioms.intro
  1.1520 +    cring.axioms prems)
  1.1521 +
  1.1522 +lemma INTEG_id:
  1.1523 +  "ring_hom_UP_cring INTEG INTEG id"
  1.1524 +  by (fast intro: ring_hom_UP_cringI cring_INTEG id_ring_hom)
  1.1525 +
  1.1526 +text {*
  1.1527 +  An instantiation mechanism would now import all theorems and lemmas
  1.1528 +  valid in the context of homomorphisms between @{term INTEG} and @{term
  1.1529 +  "UP INTEG"}.  *}
  1.1530 +
  1.1531 +lemma INTEG_closed [intro, simp]:
  1.1532 +  "z \<in> carrier INTEG"
  1.1533 +  by (unfold INTEG_def) simp
  1.1534 +
  1.1535 +lemma INTEG_mult [simp]:
  1.1536 +  "mult INTEG z w = z * w"
  1.1537 +  by (unfold INTEG_def) simp
  1.1538 +
  1.1539 +lemma INTEG_pow [simp]:
  1.1540 +  "pow INTEG z n = z ^ n"
  1.1541 +  by (induct n) (simp_all add: INTEG_def nat_pow_def)
  1.1542 +
  1.1543 +lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500"
  1.1544 +  by (simp add: ring_hom_UP_cring.eval_monom [OF INTEG_id])
  1.1545 +
  1.1546 +-- {* Calculates @{term "x = 500"} *}
  1.1547 +
  1.1548 +
  1.1549 +end
  1.1550 \ No newline at end of file