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.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.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.163 +subsection {* Effect of operations on coefficients *}
1.165 +locale UP = struct R + struct P +
1.166 +  defines P_def: "P == UP R"
1.168 +locale UP_cring = UP + cring R
1.170 +locale UP_domain = UP_cring + "domain" R
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.177 +declare (in UP) P_def [simp]
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.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.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.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.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.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.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.221 +subsection {* Polynomials form a commutative ring. *}
1.223 +text {* Operations are closed over @{term "P"}. *}
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.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.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.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.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.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.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.253 +declare (in UP) P_def [simp del]
1.255 +text {* Algebraic ring properties *}
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.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.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.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.288 +ML_setup {*
1.289 +Context.>> (fn thy => (simpset_ref_of thy :=
1.290 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
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.321 +ML_setup {*
1.322 +Context.>> (fn thy => (simpset_ref_of thy :=
1.323 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
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.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.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.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.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.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.395 +text {*
1.396 +  Instantiation of lemmas from @{term cring}.
1.397 +*}
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.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.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.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.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.422 +lemmas (in UP_cring) UP_r_one [simp] =
1.423 +  monoid.r_one [OF UP_monoid]
1.425 +lemmas (in UP_cring) UP_nat_pow_closed [intro, simp] =
1.426 +  monoid.nat_pow_closed [OF UP_monoid]
1.428 +lemmas (in UP_cring) UP_nat_pow_0 [simp] =
1.429 +  monoid.nat_pow_0 [OF UP_monoid]
1.431 +lemmas (in UP_cring) UP_nat_pow_Suc [simp] =
1.432 +  monoid.nat_pow_Suc [OF UP_monoid]
1.434 +lemmas (in UP_cring) UP_nat_pow_one [simp] =
1.435 +  monoid.nat_pow_one [OF UP_monoid]
1.437 +lemmas (in UP_cring) UP_nat_pow_mult =
1.438 +  monoid.nat_pow_mult [OF UP_monoid]
1.440 +lemmas (in UP_cring) UP_nat_pow_pow =
1.441 +  monoid.nat_pow_pow [OF UP_monoid]
1.443 +lemmas (in UP_cring) UP_m_lcomm =
1.444 +  comm_semigroup.m_lcomm [OF UP_comm_semigroup]
1.446 +lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm
1.448 +lemmas (in UP_cring) UP_nat_pow_distr =
1.449 +  comm_monoid.nat_pow_distr [OF UP_comm_monoid]
1.451 +lemmas (in UP_cring) UP_a_lcomm = abelian_monoid.a_lcomm [OF UP_abelian_monoid]
1.453 +lemmas (in UP_cring) UP_r_zero [simp] =
1.454 +  abelian_monoid.r_zero [OF UP_abelian_monoid]
1.456 +lemmas (in UP_cring) UP_a_ac = UP_a_assoc UP_a_comm UP_a_lcomm
1.458 +lemmas (in UP_cring) UP_finsum_empty [simp] =
1.459 +  abelian_monoid.finsum_empty [OF UP_abelian_monoid]
1.461 +lemmas (in UP_cring) UP_finsum_insert [simp] =
1.462 +  abelian_monoid.finsum_insert [OF UP_abelian_monoid]
1.464 +lemmas (in UP_cring) UP_finsum_zero [simp] =
1.465 +  abelian_monoid.finsum_zero [OF UP_abelian_monoid]
1.467 +lemmas (in UP_cring) UP_finsum_closed [simp] =
1.468 +  abelian_monoid.finsum_closed [OF UP_abelian_monoid]
1.470 +lemmas (in UP_cring) UP_finsum_Un_Int =
1.471 +  abelian_monoid.finsum_Un_Int [OF UP_abelian_monoid]
1.473 +lemmas (in UP_cring) UP_finsum_Un_disjoint =
1.474 +  abelian_monoid.finsum_Un_disjoint [OF UP_abelian_monoid]
1.476 +lemmas (in UP_cring) UP_finsum_addf =
1.477 +  abelian_monoid.finsum_addf [OF UP_abelian_monoid]
1.479 +lemmas (in UP_cring) UP_finsum_cong' =
1.480 +  abelian_monoid.finsum_cong' [OF UP_abelian_monoid]
1.482 +lemmas (in UP_cring) UP_finsum_0 [simp] =
1.483 +  abelian_monoid.finsum_0 [OF UP_abelian_monoid]
1.485 +lemmas (in UP_cring) UP_finsum_Suc [simp] =
1.486 +  abelian_monoid.finsum_Suc [OF UP_abelian_monoid]
1.488 +lemmas (in UP_cring) UP_finsum_Suc2 =
1.489 +  abelian_monoid.finsum_Suc2 [OF UP_abelian_monoid]
1.491 +lemmas (in UP_cring) UP_finsum_add [simp] =
1.492 +  abelian_monoid.finsum_add [OF UP_abelian_monoid]
1.494 +lemmas (in UP_cring) UP_finsum_cong =
1.495 +  abelian_monoid.finsum_cong [OF UP_abelian_monoid]
1.497 +lemmas (in UP_cring) UP_minus_closed [intro, simp] =
1.498 +  abelian_group.minus_closed [OF UP_abelian_group]
1.500 +lemmas (in UP_cring) UP_a_l_cancel [simp] =
1.501 +  abelian_group.a_l_cancel [OF UP_abelian_group]
1.503 +lemmas (in UP_cring) UP_a_r_cancel [simp] =
1.504 +  abelian_group.a_r_cancel [OF UP_abelian_group]
1.506 +lemmas (in UP_cring) UP_l_neg =
1.507 +  abelian_group.l_neg [OF UP_abelian_group]
1.509 +lemmas (in UP_cring) UP_r_neg =
1.510 +  abelian_group.r_neg [OF UP_abelian_group]
1.512 +lemmas (in UP_cring) UP_minus_zero [simp] =
1.513 +  abelian_group.minus_zero [OF UP_abelian_group]
1.515 +lemmas (in UP_cring) UP_minus_minus [simp] =
1.516 +  abelian_group.minus_minus [OF UP_abelian_group]
1.518 +lemmas (in UP_cring) UP_minus_add =
1.519 +  abelian_group.minus_add [OF UP_abelian_group]
1.521 +lemmas (in UP_cring) UP_r_neg2 =
1.522 +  abelian_group.r_neg2 [OF UP_abelian_group]
1.524 +lemmas (in UP_cring) UP_r_neg1 =
1.525 +  abelian_group.r_neg1 [OF UP_abelian_group]
1.527 +lemmas (in UP_cring) UP_r_distr =
1.528 +  cring.r_distr [OF UP_cring]
1.530 +lemmas (in UP_cring) UP_l_null [simp] =
1.531 +  cring.l_null [OF UP_cring]
1.533 +lemmas (in UP_cring) UP_r_null [simp] =
1.534 +  cring.r_null [OF UP_cring]
1.536 +lemmas (in UP_cring) UP_l_minus =
1.537 +  cring.l_minus [OF UP_cring]
1.539 +lemmas (in UP_cring) UP_r_minus =
1.540 +  cring.r_minus [OF UP_cring]
1.542 +lemmas (in UP_cring) UP_finsum_ldistr =
1.543 +  cring.finsum_ldistr [OF UP_cring]
1.545 +lemmas (in UP_cring) UP_finsum_rdistr =
1.546 +  cring.finsum_rdistr [OF UP_cring]
1.548 +subsection {* Polynomials form an Algebra *}
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.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.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.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.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.574 +text {*
1.575 +  Instantiation of lemmas from @{term algebra}.
1.576 +*}
1.578 +(* TODO: move to CRing.thy, really a fact missing from the locales package *)
1.580 +lemma (in cring) cring:
1.581 +  "cring R"
1.582 +  by (fast intro: cring.intro prems)
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.589 +lemmas (in UP_cring) UP_smult_l_null [simp] =
1.590 +  algebra.smult_l_null [OF UP_algebra]
1.592 +lemmas (in UP_cring) UP_smult_r_null [simp] =
1.593 +  algebra.smult_r_null [OF UP_algebra]
1.595 +lemmas (in UP_cring) UP_smult_l_minus =
1.596 +  algebra.smult_l_minus [OF UP_algebra]
1.598 +lemmas (in UP_cring) UP_smult_r_minus =
1.599 +  algebra.smult_r_minus [OF UP_algebra]
1.601 +subsection {* Further Lemmas Involving @{term monom} *}
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.607 +ML_setup {*
1.608 +Context.>> (fn thy => (simpset_ref_of thy :=
1.609 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
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.628 +ML_setup {*
1.629 +Context.>> (fn thy => (simpset_ref_of thy :=
1.630 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
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.637 +ML_setup {*
1.638 +Context.>> (fn thy => (simpset_ref_of thy :=
1.639 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
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.714 +ML_setup {*
1.715 +Context.>> (fn thy => (simpset_ref_of thy :=
1.716 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
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.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.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.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.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.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.773 +subsection {* The Degree Function *}
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.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.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.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.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.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.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.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.874 +(* Degree and polynomial operations *)
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.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.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.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.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.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.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.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.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.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.966 +ML_setup {*
1.967 +Context.>> (fn thy => (simpset_ref_of thy :=
1.968 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
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.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.1006 +ML_setup {*
1.1007 +Context.>> (fn thy => (simpset_ref_of thy :=
1.1008 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
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.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.1062 +ML_setup {*
1.1063 +Context.>> (fn thy => (simpset_ref_of thy :=
1.1064 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
1.1066 +subsection {* Polynomial over an Integral Domain are an Integral Domain *}
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.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.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.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.1119 +text {*
1.1120 +  Instantiation of results from @{term domain}.
1.1121 +*}
1.1123 +lemmas (in UP_domain) UP_zero_not_one [simp] =
1.1124 +  domain.zero_not_one [OF UP_domain]
1.1126 +lemmas (in UP_domain) UP_integral_iff =
1.1127 +  domain.integral_iff [OF UP_domain]
1.1129 +lemmas (in UP_domain) UP_m_lcancel =
1.1130 +  domain.m_lcancel [OF UP_domain]
1.1132 +lemmas (in UP_domain) UP_m_rcancel =
1.1133 +  domain.m_rcancel [OF UP_domain]
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.1140 +subsection {* Evaluation Homomorphism *}
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.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.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.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.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.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.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.1249 +locale ring_hom_UP_cring = ring_hom_cring R S + UP_cring R
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.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.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.1344 +text {* Instantiation of ring homomorphism lemmas. *}
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.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.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.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.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.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.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.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.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.1388 +text {* Further properties of the evaluation homomorphism. *}
1.1390 +(* The following lemma could be proved in UP\_cring with the additional
1.1391 +   assumption that h is closed. *)
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.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.1400 +(* TODO: simplify by cases "one R = zero R" *)
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.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.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.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.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.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.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.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.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.1512 +subsection {* Sample application of evaluation homomorphism *}
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.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.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.1531 +lemma INTEG_closed [intro, simp]:
1.1532 +  "z \<in> carrier INTEG"
1.1533 +  by (unfold INTEG_def) simp
1.1535 +lemma INTEG_mult [simp]:
1.1536 +  "mult INTEG z w = z * w"
1.1537 +  by (unfold INTEG_def) simp
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.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.1546 +-- {* Calculates @{term "x = 500"} *}
1.1549 +end
1.1550 \ No newline at end of file