HOL-Algebra: New polynomial development added.
authorballarin
Wed Apr 30 18:32:06 2003 +0200 (2003-04-30)
changeset 13940c67798653056
parent 13939 b3ef90abbd02
child 13941 2ae108fcd068
HOL-Algebra: New polynomial development added.
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/ROOT.ML
src/HOL/Algebra/UnivPoly.thy
     1.1 --- a/src/HOL/Algebra/Coset.thy	Wed Apr 30 18:31:38 2003 +0200
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Wed Apr 30 18:32:06 2003 +0200
     1.3 @@ -468,7 +468,7 @@
     1.4       "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
     1.5  by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup 
     1.6                     subgroup.subset)
     1.7 -
     1.8 +(*
     1.9  lemma (in group) factorgroup_is_magma:
    1.10    "H <| G ==> magma (G Mod H)"
    1.11    by rule (simp add: FactGroup_def coset.setmult_closed [OF is_coset])
    1.12 @@ -477,7 +477,7 @@
    1.13    "H <| G ==> semigroup_axioms (G Mod H)"
    1.14    by rule (simp add: FactGroup_def coset.setrcos_assoc [OF is_coset]
    1.15      coset.setmult_closed [OF is_coset])
    1.16 -
    1.17 +*)
    1.18  theorem (in group) factorgroup_is_group:
    1.19    "H <| G ==> group (G Mod H)"
    1.20  apply (insert is_coset) 
     2.1 --- a/src/HOL/Algebra/Group.thy	Wed Apr 30 18:31:38 2003 +0200
     2.2 +++ b/src/HOL/Algebra/Group.thy	Wed Apr 30 18:32:06 2003 +0200
     2.3 @@ -93,6 +93,10 @@
     2.4    finally show ?thesis .
     2.5  qed
     2.6  
     2.7 +lemma (in monoid) Units_one_closed [intro, simp]:
     2.8 +  "\<one> \<in> Units G"
     2.9 +  by (unfold Units_def) auto
    2.10 +
    2.11  lemma (in monoid) Units_inv_closed [intro, simp]:
    2.12    "x \<in> Units G ==> inv x \<in> carrier G"
    2.13    apply (unfold Units_def m_inv_def)
    2.14 @@ -162,6 +166,15 @@
    2.15    with G show "x = y" by simp
    2.16  qed
    2.17  
    2.18 +lemma (in monoid) Units_inv_comm:
    2.19 +  assumes inv: "x \<otimes> y = \<one>"
    2.20 +    and G: "x \<in> Units G" "y \<in> Units G"
    2.21 +  shows "y \<otimes> x = \<one>"
    2.22 +proof -
    2.23 +  from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed)
    2.24 +  with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
    2.25 +qed
    2.26 +
    2.27  text {* Power *}
    2.28  
    2.29  lemma (in monoid) nat_pow_closed [intro, simp]:
    2.30 @@ -287,16 +300,7 @@
    2.31    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    2.32     (x \<otimes> y = x \<otimes> z) = (y = z)"
    2.33    using Units_l_inv by simp
    2.34 -(*
    2.35 -lemma (in group) r_one [simp]:  
    2.36 -  "x \<in> carrier G ==> x \<otimes> \<one> = x"
    2.37 -proof -
    2.38 -  assume x: "x \<in> carrier G"
    2.39 -  then have "inv x \<otimes> (x \<otimes> \<one>) = inv x \<otimes> x"
    2.40 -    by (simp add: m_assoc [symmetric] l_inv)
    2.41 -  with x show ?thesis by simp 
    2.42 -qed
    2.43 -*)
    2.44 +
    2.45  lemma (in group) r_inv:
    2.46    "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
    2.47  proof -
    2.48 @@ -346,6 +350,10 @@
    2.49    with G show ?thesis by simp
    2.50  qed
    2.51  
    2.52 +lemma (in group) inv_comm:
    2.53 +  "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
    2.54 +  by (rule Units_inv_comm) auto                          
    2.55 +
    2.56  text {* Power *}
    2.57  
    2.58  lemma (in group) int_pow_def2:
     3.1 --- a/src/HOL/Algebra/Module.thy	Wed Apr 30 18:31:38 2003 +0200
     3.2 +++ b/src/HOL/Algebra/Module.thy	Wed Apr 30 18:32:06 2003 +0200
     3.3 @@ -139,7 +139,7 @@
     3.4    finally show ?thesis .
     3.5  qed
     3.6  
     3.7 -subsection {* Every Abelian Group is a $\mathbb{Z}$-module *}
     3.8 +subsection {* Every Abelian Group is a Z-module *}
     3.9  
    3.10  text {* Not finished. *}
    3.11  
     4.1 --- a/src/HOL/Algebra/ROOT.ML	Wed Apr 30 18:31:38 2003 +0200
     4.2 +++ b/src/HOL/Algebra/ROOT.ML	Wed Apr 30 18:32:06 2003 +0200
     4.3 @@ -6,8 +6,9 @@
     4.4  
     4.5  (* New development, based on explicit structures *)
     4.6  
     4.7 +no_document use_thy "FuncSet";
     4.8  use_thy "Sylow";		(* Groups *)
     4.9 -(* use_thy "UnivPoly"; *)	(* Rings and polynomials *)
    4.10 +use_thy "UnivPoly";		(* Rings and polynomials *)
    4.11  
    4.12  (* Old development, based on axiomatic type classes.
    4.13     Will be withdrawn in future. *)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Apr 30 18:32:06 2003 +0200
     5.3 @@ -0,0 +1,1546 @@
     5.4 +(*
     5.5 +  Title:     Univariate Polynomials
     5.6 +  Id:        $Id$
     5.7 +  Author:    Clemens Ballarin, started 9 December 1996
     5.8 +  Copyright: Clemens Ballarin
     5.9 +*)
    5.10 +
    5.11 +theory UnivPoly = Module:
    5.12 +
    5.13 +section {* Univariate Polynomials *}
    5.14 +
    5.15 +subsection
    5.16 +  {* Definition of the Constructor for Univariate Polynomials @{term UP} *}
    5.17 +
    5.18 +(* Could alternatively use locale ...
    5.19 +locale bound = cring + var bound +
    5.20 +  defines ...
    5.21 +*)
    5.22 +
    5.23 +constdefs
    5.24 +  bound  :: "['a, nat, nat => 'a] => bool"
    5.25 +  "bound z n f == (ALL i. n < i --> f i = z)"
    5.26 +
    5.27 +lemma boundI [intro!]:
    5.28 +  "[| !! m. n < m ==> f m = z |] ==> bound z n f"
    5.29 +  by (unfold bound_def) fast
    5.30 +
    5.31 +lemma boundE [elim?]:
    5.32 +  "[| bound z n f; (!! m. n < m ==> f m = z) ==> P |] ==> P"
    5.33 +  by (unfold bound_def) fast
    5.34 +
    5.35 +lemma boundD [dest]:
    5.36 +  "[| bound z n f; n < m |] ==> f m = z"
    5.37 +  by (unfold bound_def) fast
    5.38 +
    5.39 +lemma bound_below:
    5.40 +  assumes bound: "bound z m f" and nonzero: "f n ~= z" shows "n <= m"
    5.41 +proof (rule classical)
    5.42 +  assume "~ ?thesis"
    5.43 +  then have "m < n" by arith
    5.44 +  with bound have "f n = z" ..
    5.45 +  with nonzero show ?thesis by contradiction
    5.46 +qed
    5.47 +
    5.48 +record ('a, 'p) up_ring = "('a, 'p) module" +
    5.49 +  monom :: "['a, nat] => 'p"
    5.50 +  coeff :: "['p, nat] => 'a"
    5.51 +
    5.52 +constdefs
    5.53 +  up :: "('a, 'm) ring_scheme => (nat => 'a) set"
    5.54 +  "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound (zero R) n f)}"
    5.55 +  UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
    5.56 +  "UP R == (|
    5.57 +    carrier = up R,
    5.58 +    mult = (%p:up R. %q:up R. %n. finsum R (%i. mult R (p i) (q (n-i))) {..n}),
    5.59 +    one = (%i. if i=0 then one R else zero R),
    5.60 +    zero = (%i. zero R),
    5.61 +    add = (%p:up R. %q:up R. %i. add R (p i) (q i)),
    5.62 +    smult = (%a:carrier R. %p:up R. %i. mult R a (p i)),
    5.63 +    monom = (%a:carrier R. %n i. if i=n then a else zero R),
    5.64 +    coeff = (%p:up R. %n. p n) |)"
    5.65 +
    5.66 +text {*
    5.67 +  Properties of the set of polynomials @{term up}.
    5.68 +*}
    5.69 +
    5.70 +lemma mem_upI [intro]:
    5.71 +  "[| !!n. f n \<in> carrier R; EX n. bound (zero R) n f |] ==> f \<in> up R"
    5.72 +  by (simp add: up_def Pi_def)
    5.73 +
    5.74 +lemma mem_upD [dest]:
    5.75 +  "f \<in> up R ==> f n \<in> carrier R"
    5.76 +  by (simp add: up_def Pi_def)
    5.77 +
    5.78 +lemma (in cring) bound_upD [dest]:
    5.79 +  "f \<in> up R ==> EX n. bound \<zero> n f"
    5.80 +  by (simp add: up_def)
    5.81 +
    5.82 +lemma (in cring) up_one_closed:
    5.83 +   "(%n. if n = 0 then \<one> else \<zero>) \<in> up R"
    5.84 +  using up_def by force
    5.85 +
    5.86 +lemma (in cring) up_smult_closed:
    5.87 +  "[| a \<in> carrier R; p \<in> up R |] ==> (%i. a \<otimes> p i) \<in> up R"
    5.88 +  by force
    5.89 +
    5.90 +lemma (in cring) up_add_closed:
    5.91 +  "[| p \<in> up R; q \<in> up R |] ==> (%i. p i \<oplus> q i) \<in> up R"
    5.92 +proof
    5.93 +  fix n
    5.94 +  assume "p \<in> up R" and "q \<in> up R"
    5.95 +  then show "p n \<oplus> q n \<in> carrier R"
    5.96 +    by auto
    5.97 +next
    5.98 +  assume UP: "p \<in> up R" "q \<in> up R"
    5.99 +  show "EX n. bound \<zero> n (%i. p i \<oplus> q i)"
   5.100 +  proof -
   5.101 +    from UP obtain n where boundn: "bound \<zero> n p" by fast
   5.102 +    from UP obtain m where boundm: "bound \<zero> m q" by fast
   5.103 +    have "bound \<zero> (max n m) (%i. p i \<oplus> q i)"
   5.104 +    proof
   5.105 +      fix i
   5.106 +      assume "max n m < i"
   5.107 +      with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastsimp
   5.108 +    qed
   5.109 +    then show ?thesis ..
   5.110 +  qed
   5.111 +qed
   5.112 +
   5.113 +lemma (in cring) up_a_inv_closed:
   5.114 +  "p \<in> up R ==> (%i. \<ominus> (p i)) \<in> up R"
   5.115 +proof
   5.116 +  assume R: "p \<in> up R"
   5.117 +  then obtain n where "bound \<zero> n p" by auto
   5.118 +  then have "bound \<zero> n (%i. \<ominus> p i)" by auto
   5.119 +  then show "EX n. bound \<zero> n (%i. \<ominus> p i)" by auto
   5.120 +qed auto
   5.121 +
   5.122 +lemma (in cring) up_mult_closed:
   5.123 +  "[| p \<in> up R; q \<in> up R |] ==>
   5.124 +  (%n. finsum R (%i. p i \<otimes> q (n-i)) {..n}) \<in> up R"
   5.125 +proof
   5.126 +  fix n
   5.127 +  assume "p \<in> up R" "q \<in> up R"
   5.128 +  then show "finsum R (%i. p i \<otimes> q (n-i)) {..n} \<in> carrier R"
   5.129 +    by (simp add: mem_upD  funcsetI)
   5.130 +next
   5.131 +  assume UP: "p \<in> up R" "q \<in> up R"
   5.132 +  show "EX n. bound \<zero> n (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
   5.133 +  proof -
   5.134 +    from UP obtain n where boundn: "bound \<zero> n p" by fast
   5.135 +    from UP obtain m where boundm: "bound \<zero> m q" by fast
   5.136 +    have "bound \<zero> (n + m) (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
   5.137 +    proof
   5.138 +      fix k
   5.139 +      assume bound: "n + m < k"
   5.140 +      {
   5.141 +	fix i
   5.142 +	have "p i \<otimes> q (k-i) = \<zero>"
   5.143 +	proof (cases "n < i")
   5.144 +	  case True
   5.145 +	  with boundn have "p i = \<zero>" by auto
   5.146 +          moreover from UP have "q (k-i) \<in> carrier R" by auto
   5.147 +	  ultimately show ?thesis by simp
   5.148 +	next
   5.149 +	  case False
   5.150 +	  with bound have "m < k-i" by arith
   5.151 +	  with boundm have "q (k-i) = \<zero>" by auto
   5.152 +	  moreover from UP have "p i \<in> carrier R" by auto
   5.153 +	  ultimately show ?thesis by simp
   5.154 +	qed
   5.155 +      }
   5.156 +      then show "finsum R (%i. p i \<otimes> q (k-i)) {..k} = \<zero>"
   5.157 +	by (simp add: Pi_def)
   5.158 +    qed
   5.159 +    then show ?thesis by fast
   5.160 +  qed
   5.161 +qed
   5.162 +
   5.163 +subsection {* Effect of operations on coefficients *}
   5.164 +
   5.165 +locale UP = struct R + struct P +
   5.166 +  defines P_def: "P == UP R"
   5.167 +
   5.168 +locale UP_cring = UP + cring R
   5.169 +
   5.170 +locale UP_domain = UP_cring + "domain" R
   5.171 +
   5.172 +text {*
   5.173 +  Temporarily declare UP.P\_def as simp rule.
   5.174 +*}
   5.175 +(* TODO: use antiquotation once text (in locale) is supported. *)
   5.176 +
   5.177 +declare (in UP) P_def [simp]
   5.178 +
   5.179 +lemma (in UP_cring) coeff_monom [simp]:
   5.180 +  "a \<in> carrier R ==>
   5.181 +  coeff P (monom P a m) n = (if m=n then a else \<zero>)"
   5.182 +proof -
   5.183 +  assume R: "a \<in> carrier R"
   5.184 +  then have "(%n. if n = m then a else \<zero>) \<in> up R"
   5.185 +    using up_def by force
   5.186 +  with R show ?thesis by (simp add: UP_def)
   5.187 +qed
   5.188 +
   5.189 +lemma (in UP_cring) coeff_zero [simp]:
   5.190 +  "coeff P \<zero>\<^sub>2 n = \<zero>"
   5.191 +  by (auto simp add: UP_def)
   5.192 +
   5.193 +lemma (in UP_cring) coeff_one [simp]:
   5.194 +  "coeff P \<one>\<^sub>2 n = (if n=0 then \<one> else \<zero>)"
   5.195 +  using up_one_closed by (simp add: UP_def)
   5.196 +
   5.197 +lemma (in UP_cring) coeff_smult [simp]:
   5.198 +  "[| a \<in> carrier R; p \<in> carrier P |] ==>
   5.199 +  coeff P (a \<odot>\<^sub>2 p) n = a \<otimes> coeff P p n"
   5.200 +  by (simp add: UP_def up_smult_closed)
   5.201 +
   5.202 +lemma (in UP_cring) coeff_add [simp]:
   5.203 +  "[| p \<in> carrier P; q \<in> carrier P |] ==>
   5.204 +  coeff P (p \<oplus>\<^sub>2 q) n = coeff P p n \<oplus> coeff P q n"
   5.205 +  by (simp add: UP_def up_add_closed)
   5.206 +
   5.207 +lemma (in UP_cring) coeff_mult [simp]:
   5.208 +  "[| p \<in> carrier P; q \<in> carrier P |] ==>
   5.209 +  coeff P (p \<otimes>\<^sub>2 q) n = finsum R (%i. coeff P p i \<otimes> coeff P q (n-i)) {..n}"
   5.210 +  by (simp add: UP_def up_mult_closed)
   5.211 +
   5.212 +lemma (in UP) up_eqI:
   5.213 +  assumes prem: "!!n. coeff P p n = coeff P q n"
   5.214 +    and R: "p \<in> carrier P" "q \<in> carrier P"
   5.215 +  shows "p = q"
   5.216 +proof
   5.217 +  fix x
   5.218 +  from prem and R show "p x = q x" by (simp add: UP_def)
   5.219 +qed
   5.220 +  
   5.221 +subsection {* Polynomials form a commutative ring. *}
   5.222 +
   5.223 +text {* Operations are closed over @{term "P"}. *}
   5.224 +
   5.225 +lemma (in UP_cring) UP_mult_closed [simp]:
   5.226 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^sub>2 q \<in> carrier P"
   5.227 +  by (simp add: UP_def up_mult_closed)
   5.228 +
   5.229 +lemma (in UP_cring) UP_one_closed [simp]:
   5.230 +  "\<one>\<^sub>2 \<in> carrier P"
   5.231 +  by (simp add: UP_def up_one_closed)
   5.232 +
   5.233 +lemma (in UP_cring) UP_zero_closed [intro, simp]:
   5.234 +  "\<zero>\<^sub>2 \<in> carrier P"
   5.235 +  by (auto simp add: UP_def)
   5.236 +
   5.237 +lemma (in UP_cring) UP_a_closed [intro, simp]:
   5.238 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<oplus>\<^sub>2 q \<in> carrier P"
   5.239 +  by (simp add: UP_def up_add_closed)
   5.240 +
   5.241 +lemma (in UP_cring) monom_closed [simp]:
   5.242 +  "a \<in> carrier R ==> monom P a n \<in> carrier P"
   5.243 +  by (auto simp add: UP_def up_def Pi_def)
   5.244 +
   5.245 +lemma (in UP_cring) UP_smult_closed [simp]:
   5.246 +  "[| a \<in> carrier R; p \<in> carrier P |] ==> a \<odot>\<^sub>2 p \<in> carrier P"
   5.247 +  by (simp add: UP_def up_smult_closed)
   5.248 +
   5.249 +lemma (in UP) coeff_closed [simp]:
   5.250 +  "p \<in> carrier P ==> coeff P p n \<in> carrier R"
   5.251 +  by (auto simp add: UP_def)
   5.252 +
   5.253 +declare (in UP) P_def [simp del]
   5.254 +
   5.255 +text {* Algebraic ring properties *}
   5.256 +
   5.257 +lemma (in UP_cring) UP_a_assoc:
   5.258 +  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   5.259 +  shows "(p \<oplus>\<^sub>2 q) \<oplus>\<^sub>2 r = p \<oplus>\<^sub>2 (q \<oplus>\<^sub>2 r)"
   5.260 +  by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
   5.261 +
   5.262 +lemma (in UP_cring) UP_l_zero [simp]:
   5.263 +  assumes R: "p \<in> carrier P"
   5.264 +  shows "\<zero>\<^sub>2 \<oplus>\<^sub>2 p = p"
   5.265 +  by (rule up_eqI, simp_all add: R)
   5.266 +
   5.267 +lemma (in UP_cring) UP_l_neg_ex:
   5.268 +  assumes R: "p \<in> carrier P"
   5.269 +  shows "EX q : carrier P. q \<oplus>\<^sub>2 p = \<zero>\<^sub>2"
   5.270 +proof -
   5.271 +  let ?q = "%i. \<ominus> (p i)"
   5.272 +  from R have closed: "?q \<in> carrier P"
   5.273 +    by (simp add: UP_def P_def up_a_inv_closed)
   5.274 +  from R have coeff: "!!n. coeff P ?q n = \<ominus> (coeff P p n)"
   5.275 +    by (simp add: UP_def P_def up_a_inv_closed)
   5.276 +  show ?thesis
   5.277 +  proof
   5.278 +    show "?q \<oplus>\<^sub>2 p = \<zero>\<^sub>2"
   5.279 +      by (auto intro!: up_eqI simp add: R closed coeff R.l_neg)
   5.280 +  qed (rule closed)
   5.281 +qed
   5.282 +
   5.283 +lemma (in UP_cring) UP_a_comm:
   5.284 +  assumes R: "p \<in> carrier P" "q \<in> carrier P"
   5.285 +  shows "p \<oplus>\<^sub>2 q = q \<oplus>\<^sub>2 p"
   5.286 +  by (rule up_eqI, simp add: a_comm R, simp_all add: R)
   5.287 +
   5.288 +ML_setup {*
   5.289 +Context.>> (fn thy => (simpset_ref_of thy :=
   5.290 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   5.291 +
   5.292 +lemma (in UP_cring) UP_m_assoc:
   5.293 +  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   5.294 +  shows "(p \<otimes>\<^sub>2 q) \<otimes>\<^sub>2 r = p \<otimes>\<^sub>2 (q \<otimes>\<^sub>2 r)"
   5.295 +proof (rule up_eqI)
   5.296 +  fix n
   5.297 +  {
   5.298 +    fix k and a b c :: "nat=>'a"
   5.299 +    assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
   5.300 +      "c \<in> UNIV -> carrier R"
   5.301 +    then have "k <= n ==>
   5.302 +      finsum R (%j. finsum R (%i. a i \<otimes> b (j-i)) {..j} \<otimes> c (n-j)) {..k} =
   5.303 +      finsum R (%j. a j \<otimes> finsum R (%i. b i \<otimes> c (n-j-i)) {..k-j}) {..k}"
   5.304 +      (is "_ ==> ?eq k")
   5.305 +    proof (induct k)
   5.306 +      case 0 then show ?case by (simp add: Pi_def m_assoc)
   5.307 +    next
   5.308 +      case (Suc k)
   5.309 +      then have "k <= n" by arith
   5.310 +      then have "?eq k" by (rule Suc)
   5.311 +      with R show ?case
   5.312 +	by (simp cong: finsum_cong
   5.313 +             add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
   5.314 +          (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
   5.315 +    qed
   5.316 +  }
   5.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"
   5.318 +    by (simp add: Pi_def)
   5.319 +qed (simp_all add: R)
   5.320 +
   5.321 +ML_setup {*
   5.322 +Context.>> (fn thy => (simpset_ref_of thy :=
   5.323 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
   5.324 +
   5.325 +lemma (in UP_cring) UP_l_one [simp]:
   5.326 +  assumes R: "p \<in> carrier P"
   5.327 +  shows "\<one>\<^sub>2 \<otimes>\<^sub>2 p = p"
   5.328 +proof (rule up_eqI)
   5.329 +  fix n
   5.330 +  show "coeff P (\<one>\<^sub>2 \<otimes>\<^sub>2 p) n = coeff P p n"
   5.331 +  proof (cases n)
   5.332 +    case 0 with R show ?thesis by simp
   5.333 +  next
   5.334 +    case Suc with R show ?thesis
   5.335 +      by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)
   5.336 +  qed
   5.337 +qed (simp_all add: R)
   5.338 +
   5.339 +lemma (in UP_cring) UP_l_distr:
   5.340 +  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   5.341 +  shows "(p \<oplus>\<^sub>2 q) \<otimes>\<^sub>2 r = (p \<otimes>\<^sub>2 r) \<oplus>\<^sub>2 (q \<otimes>\<^sub>2 r)"
   5.342 +  by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R)
   5.343 +
   5.344 +lemma (in UP_cring) UP_m_comm:
   5.345 +  assumes R: "p \<in> carrier P" "q \<in> carrier P"
   5.346 +  shows "p \<otimes>\<^sub>2 q = q \<otimes>\<^sub>2 p"
   5.347 +proof (rule up_eqI)
   5.348 +  fix n 
   5.349 +  {
   5.350 +    fix k and a b :: "nat=>'a"
   5.351 +    assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
   5.352 +    then have "k <= n ==> 
   5.353 +      finsum R (%i. a i \<otimes> b (n-i)) {..k} =
   5.354 +      finsum R (%i. a (k-i) \<otimes> b (i+n-k)) {..k}"
   5.355 +      (is "_ ==> ?eq k")
   5.356 +    proof (induct k)
   5.357 +      case 0 then show ?case by (simp add: Pi_def)
   5.358 +    next
   5.359 +      case (Suc k) then show ?case
   5.360 +	by (subst finsum_Suc2) (simp add: Pi_def a_comm)+
   5.361 +    qed
   5.362 +  }
   5.363 +  note l = this
   5.364 +  from R show "coeff P (p \<otimes>\<^sub>2 q) n =  coeff P (q \<otimes>\<^sub>2 p) n"
   5.365 +    apply (simp add: Pi_def)
   5.366 +    apply (subst l)
   5.367 +    apply (auto simp add: Pi_def)
   5.368 +    apply (simp add: m_comm)
   5.369 +    done
   5.370 +qed (simp_all add: R)
   5.371 +
   5.372 +theorem (in UP_cring) UP_cring:
   5.373 +  "cring P"
   5.374 +  by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
   5.375 +    UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
   5.376 +
   5.377 +lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
   5.378 +  "p \<in> carrier P ==> \<ominus>\<^sub>2 p \<in> carrier P"
   5.379 +  by (rule abelian_group.a_inv_closed
   5.380 +    [OF cring.is_abelian_group [OF UP_cring]])
   5.381 +
   5.382 +lemma (in UP_cring) coeff_a_inv [simp]:
   5.383 +  assumes R: "p \<in> carrier P"
   5.384 +  shows "coeff P (\<ominus>\<^sub>2 p) n = \<ominus> (coeff P p n)"
   5.385 +proof -
   5.386 +  from R coeff_closed UP_a_inv_closed have
   5.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)"
   5.388 +    by algebra
   5.389 +  also from R have "... =  \<ominus> (coeff P p n)"
   5.390 +    by (simp del: coeff_add add: coeff_add [THEN sym]
   5.391 +      abelian_group.r_neg [OF cring.is_abelian_group [OF UP_cring]])
   5.392 +  finally show ?thesis .
   5.393 +qed
   5.394 +
   5.395 +text {*
   5.396 +  Instantiation of lemmas from @{term cring}.
   5.397 +*}
   5.398 +
   5.399 +lemma (in UP_cring) UP_monoid:
   5.400 +  "monoid P"
   5.401 +  by (fast intro!: cring.is_comm_monoid comm_monoid.axioms monoid.intro
   5.402 +    UP_cring)
   5.403 +(* TODO: provide cring.is_monoid *)
   5.404 +
   5.405 +lemma (in UP_cring) UP_comm_semigroup:
   5.406 +  "comm_semigroup P"
   5.407 +  by (fast intro!: cring.is_comm_monoid comm_monoid.axioms comm_semigroup.intro
   5.408 +    UP_cring)
   5.409 +
   5.410 +lemma (in UP_cring) UP_comm_monoid:
   5.411 +  "comm_monoid P"
   5.412 +  by (fast intro!: cring.is_comm_monoid UP_cring)
   5.413 +
   5.414 +lemma (in UP_cring) UP_abelian_monoid:
   5.415 +  "abelian_monoid P"
   5.416 +  by (fast intro!: abelian_group.axioms cring.is_abelian_group UP_cring)
   5.417 +
   5.418 +lemma (in UP_cring) UP_abelian_group:
   5.419 +  "abelian_group P"
   5.420 +  by (fast intro!: cring.is_abelian_group UP_cring)
   5.421 +
   5.422 +lemmas (in UP_cring) UP_r_one [simp] =
   5.423 +  monoid.r_one [OF UP_monoid]
   5.424 +
   5.425 +lemmas (in UP_cring) UP_nat_pow_closed [intro, simp] =
   5.426 +  monoid.nat_pow_closed [OF UP_monoid]
   5.427 +
   5.428 +lemmas (in UP_cring) UP_nat_pow_0 [simp] =
   5.429 +  monoid.nat_pow_0 [OF UP_monoid]
   5.430 +
   5.431 +lemmas (in UP_cring) UP_nat_pow_Suc [simp] =
   5.432 +  monoid.nat_pow_Suc [OF UP_monoid]
   5.433 +
   5.434 +lemmas (in UP_cring) UP_nat_pow_one [simp] =
   5.435 +  monoid.nat_pow_one [OF UP_monoid]
   5.436 +
   5.437 +lemmas (in UP_cring) UP_nat_pow_mult =
   5.438 +  monoid.nat_pow_mult [OF UP_monoid]
   5.439 +
   5.440 +lemmas (in UP_cring) UP_nat_pow_pow =
   5.441 +  monoid.nat_pow_pow [OF UP_monoid]
   5.442 +
   5.443 +lemmas (in UP_cring) UP_m_lcomm =
   5.444 +  comm_semigroup.m_lcomm [OF UP_comm_semigroup]
   5.445 +
   5.446 +lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm
   5.447 +
   5.448 +lemmas (in UP_cring) UP_nat_pow_distr =
   5.449 +  comm_monoid.nat_pow_distr [OF UP_comm_monoid]
   5.450 +
   5.451 +lemmas (in UP_cring) UP_a_lcomm = abelian_monoid.a_lcomm [OF UP_abelian_monoid]
   5.452 +
   5.453 +lemmas (in UP_cring) UP_r_zero [simp] =
   5.454 +  abelian_monoid.r_zero [OF UP_abelian_monoid]
   5.455 +
   5.456 +lemmas (in UP_cring) UP_a_ac = UP_a_assoc UP_a_comm UP_a_lcomm
   5.457 +
   5.458 +lemmas (in UP_cring) UP_finsum_empty [simp] =
   5.459 +  abelian_monoid.finsum_empty [OF UP_abelian_monoid]
   5.460 +
   5.461 +lemmas (in UP_cring) UP_finsum_insert [simp] =
   5.462 +  abelian_monoid.finsum_insert [OF UP_abelian_monoid]
   5.463 +
   5.464 +lemmas (in UP_cring) UP_finsum_zero [simp] =
   5.465 +  abelian_monoid.finsum_zero [OF UP_abelian_monoid]
   5.466 +
   5.467 +lemmas (in UP_cring) UP_finsum_closed [simp] =
   5.468 +  abelian_monoid.finsum_closed [OF UP_abelian_monoid]
   5.469 +
   5.470 +lemmas (in UP_cring) UP_finsum_Un_Int =
   5.471 +  abelian_monoid.finsum_Un_Int [OF UP_abelian_monoid]
   5.472 +
   5.473 +lemmas (in UP_cring) UP_finsum_Un_disjoint =
   5.474 +  abelian_monoid.finsum_Un_disjoint [OF UP_abelian_monoid]
   5.475 +
   5.476 +lemmas (in UP_cring) UP_finsum_addf =
   5.477 +  abelian_monoid.finsum_addf [OF UP_abelian_monoid]
   5.478 +
   5.479 +lemmas (in UP_cring) UP_finsum_cong' =
   5.480 +  abelian_monoid.finsum_cong' [OF UP_abelian_monoid]
   5.481 +
   5.482 +lemmas (in UP_cring) UP_finsum_0 [simp] =
   5.483 +  abelian_monoid.finsum_0 [OF UP_abelian_monoid]
   5.484 +
   5.485 +lemmas (in UP_cring) UP_finsum_Suc [simp] =
   5.486 +  abelian_monoid.finsum_Suc [OF UP_abelian_monoid]
   5.487 +
   5.488 +lemmas (in UP_cring) UP_finsum_Suc2 =
   5.489 +  abelian_monoid.finsum_Suc2 [OF UP_abelian_monoid]
   5.490 +
   5.491 +lemmas (in UP_cring) UP_finsum_add [simp] =
   5.492 +  abelian_monoid.finsum_add [OF UP_abelian_monoid]
   5.493 +
   5.494 +lemmas (in UP_cring) UP_finsum_cong =
   5.495 +  abelian_monoid.finsum_cong [OF UP_abelian_monoid]
   5.496 +
   5.497 +lemmas (in UP_cring) UP_minus_closed [intro, simp] =
   5.498 +  abelian_group.minus_closed [OF UP_abelian_group]
   5.499 +
   5.500 +lemmas (in UP_cring) UP_a_l_cancel [simp] =
   5.501 +  abelian_group.a_l_cancel [OF UP_abelian_group]
   5.502 +
   5.503 +lemmas (in UP_cring) UP_a_r_cancel [simp] =
   5.504 +  abelian_group.a_r_cancel [OF UP_abelian_group]
   5.505 +
   5.506 +lemmas (in UP_cring) UP_l_neg =
   5.507 +  abelian_group.l_neg [OF UP_abelian_group]
   5.508 +
   5.509 +lemmas (in UP_cring) UP_r_neg =
   5.510 +  abelian_group.r_neg [OF UP_abelian_group]
   5.511 +
   5.512 +lemmas (in UP_cring) UP_minus_zero [simp] =
   5.513 +  abelian_group.minus_zero [OF UP_abelian_group]
   5.514 +
   5.515 +lemmas (in UP_cring) UP_minus_minus [simp] =
   5.516 +  abelian_group.minus_minus [OF UP_abelian_group]
   5.517 +
   5.518 +lemmas (in UP_cring) UP_minus_add =
   5.519 +  abelian_group.minus_add [OF UP_abelian_group]
   5.520 +
   5.521 +lemmas (in UP_cring) UP_r_neg2 =
   5.522 +  abelian_group.r_neg2 [OF UP_abelian_group]
   5.523 +
   5.524 +lemmas (in UP_cring) UP_r_neg1 =
   5.525 +  abelian_group.r_neg1 [OF UP_abelian_group]
   5.526 +
   5.527 +lemmas (in UP_cring) UP_r_distr =
   5.528 +  cring.r_distr [OF UP_cring]
   5.529 +
   5.530 +lemmas (in UP_cring) UP_l_null [simp] =
   5.531 +  cring.l_null [OF UP_cring]
   5.532 +
   5.533 +lemmas (in UP_cring) UP_r_null [simp] =
   5.534 +  cring.r_null [OF UP_cring]
   5.535 +
   5.536 +lemmas (in UP_cring) UP_l_minus =
   5.537 +  cring.l_minus [OF UP_cring]
   5.538 +
   5.539 +lemmas (in UP_cring) UP_r_minus =
   5.540 +  cring.r_minus [OF UP_cring]
   5.541 +
   5.542 +lemmas (in UP_cring) UP_finsum_ldistr =
   5.543 +  cring.finsum_ldistr [OF UP_cring]
   5.544 +
   5.545 +lemmas (in UP_cring) UP_finsum_rdistr =
   5.546 +  cring.finsum_rdistr [OF UP_cring]
   5.547 +
   5.548 +subsection {* Polynomials form an Algebra *}
   5.549 +
   5.550 +lemma (in UP_cring) UP_smult_l_distr:
   5.551 +  "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
   5.552 +  (a \<oplus> b) \<odot>\<^sub>2 p = a \<odot>\<^sub>2 p \<oplus>\<^sub>2 b \<odot>\<^sub>2 p"
   5.553 +  by (rule up_eqI) (simp_all add: R.l_distr)
   5.554 +
   5.555 +lemma (in UP_cring) UP_smult_r_distr:
   5.556 +  "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
   5.557 +  a \<odot>\<^sub>2 (p \<oplus>\<^sub>2 q) = a \<odot>\<^sub>2 p \<oplus>\<^sub>2 a \<odot>\<^sub>2 q"
   5.558 +  by (rule up_eqI) (simp_all add: R.r_distr)
   5.559 +
   5.560 +lemma (in UP_cring) UP_smult_assoc1:
   5.561 +      "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
   5.562 +      (a \<otimes> b) \<odot>\<^sub>2 p = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 p)"
   5.563 +  by (rule up_eqI) (simp_all add: R.m_assoc)
   5.564 +
   5.565 +lemma (in UP_cring) UP_smult_one [simp]:
   5.566 +      "p \<in> carrier P ==> \<one> \<odot>\<^sub>2 p = p"
   5.567 +  by (rule up_eqI) simp_all
   5.568 +
   5.569 +lemma (in UP_cring) UP_smult_assoc2:
   5.570 +  "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
   5.571 +  (a \<odot>\<^sub>2 p) \<otimes>\<^sub>2 q = a \<odot>\<^sub>2 (p \<otimes>\<^sub>2 q)"
   5.572 +  by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def)
   5.573 +
   5.574 +text {*
   5.575 +  Instantiation of lemmas from @{term algebra}.
   5.576 +*}
   5.577 +
   5.578 +(* TODO: move to CRing.thy, really a fact missing from the locales package *)
   5.579 +
   5.580 +lemma (in cring) cring:
   5.581 +  "cring R"
   5.582 +  by (fast intro: cring.intro prems)
   5.583 +
   5.584 +lemma (in UP_cring) UP_algebra:
   5.585 +  "algebra R P"
   5.586 +  by (auto intro: algebraI cring UP_cring UP_smult_l_distr UP_smult_r_distr
   5.587 +    UP_smult_assoc1 UP_smult_assoc2)
   5.588 +
   5.589 +lemmas (in UP_cring) UP_smult_l_null [simp] =
   5.590 +  algebra.smult_l_null [OF UP_algebra]
   5.591 +
   5.592 +lemmas (in UP_cring) UP_smult_r_null [simp] =
   5.593 +  algebra.smult_r_null [OF UP_algebra]
   5.594 +
   5.595 +lemmas (in UP_cring) UP_smult_l_minus =
   5.596 +  algebra.smult_l_minus [OF UP_algebra]
   5.597 +
   5.598 +lemmas (in UP_cring) UP_smult_r_minus =
   5.599 +  algebra.smult_r_minus [OF UP_algebra]
   5.600 +
   5.601 +subsection {* Further Lemmas Involving @{term monom} *}
   5.602 +
   5.603 +lemma (in UP_cring) monom_zero [simp]:
   5.604 +  "monom P \<zero> n = \<zero>\<^sub>2"
   5.605 +  by (simp add: UP_def P_def)
   5.606 +
   5.607 +ML_setup {*
   5.608 +Context.>> (fn thy => (simpset_ref_of thy :=
   5.609 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   5.610 +
   5.611 +lemma (in UP_cring) monom_mult_is_smult:
   5.612 +  assumes R: "a \<in> carrier R" "p \<in> carrier P"
   5.613 +  shows "monom P a 0 \<otimes>\<^sub>2 p = a \<odot>\<^sub>2 p"
   5.614 +proof (rule up_eqI)
   5.615 +  fix n
   5.616 +  have "coeff P (p \<otimes>\<^sub>2 monom P a 0) n = coeff P (a \<odot>\<^sub>2 p) n"
   5.617 +  proof (cases n)
   5.618 +    case 0 with R show ?thesis by (simp add: R.m_comm)
   5.619 +  next
   5.620 +    case Suc with R show ?thesis
   5.621 +      by (simp cong: finsum_cong add: R.r_null Pi_def)
   5.622 +        (simp add: m_comm)
   5.623 +  qed
   5.624 +  with R show "coeff P (monom P a 0 \<otimes>\<^sub>2 p) n = coeff P (a \<odot>\<^sub>2 p) n"
   5.625 +    by (simp add: UP_m_comm)
   5.626 +qed (simp_all add: R)
   5.627 +
   5.628 +ML_setup {*
   5.629 +Context.>> (fn thy => (simpset_ref_of thy :=
   5.630 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
   5.631 +
   5.632 +lemma (in UP_cring) monom_add [simp]:
   5.633 +  "[| a \<in> carrier R; b \<in> carrier R |] ==>
   5.634 +  monom P (a \<oplus> b) n = monom P a n \<oplus>\<^sub>2 monom P b n"
   5.635 +  by (rule up_eqI) simp_all
   5.636 +
   5.637 +ML_setup {*
   5.638 +Context.>> (fn thy => (simpset_ref_of thy :=
   5.639 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   5.640 +
   5.641 +lemma (in UP_cring) monom_one_Suc:
   5.642 +  "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1"
   5.643 +proof (rule up_eqI)
   5.644 +  fix k
   5.645 +  show "coeff P (monom P \<one> (Suc n)) k = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k"
   5.646 +  proof (cases "k = Suc n")
   5.647 +    case True show ?thesis
   5.648 +    proof -
   5.649 +      from True have less_add_diff: 
   5.650 +	"!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
   5.651 +      from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
   5.652 +      also from True
   5.653 +      have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
   5.654 +	coeff P (monom P \<one> 1) (k - i)) ({..n(} Un {n})"
   5.655 +	by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
   5.656 +      also have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
   5.657 +	coeff P (monom P \<one> 1) (k - i)) {..n}"
   5.658 +	by (simp only: ivl_disj_un_singleton)
   5.659 +      also from True have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
   5.660 +	coeff P (monom P \<one> 1) (k - i)) ({..n} Un {)n..k})"
   5.661 +	by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
   5.662 +	  order_less_imp_not_eq Pi_def)
   5.663 +      also from True have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k"
   5.664 +	by (simp add: ivl_disj_un_one)
   5.665 +      finally show ?thesis .
   5.666 +    qed
   5.667 +  next
   5.668 +    case False
   5.669 +    note neq = False
   5.670 +    let ?s =
   5.671 +      "(\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>))"
   5.672 +    from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
   5.673 +    also have "... = finsum R ?s {..k}"
   5.674 +    proof -
   5.675 +      have f1: "finsum R ?s {..n(} = \<zero>" by (simp cong: finsum_cong add: Pi_def)
   5.676 +      from neq have f2: "finsum R ?s {n} = \<zero>"
   5.677 +	by (simp cong: finsum_cong add: Pi_def) arith
   5.678 +      have f3: "n < k ==> finsum R ?s {)n..k} = \<zero>"
   5.679 +	by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
   5.680 +      show ?thesis
   5.681 +      proof (cases "k < n")
   5.682 +	case True then show ?thesis by (simp cong: finsum_cong add: Pi_def)
   5.683 +      next
   5.684 +	case False then have n_le_k: "n <= k" by arith
   5.685 +	show ?thesis
   5.686 +	proof (cases "n = k")
   5.687 +	  case True
   5.688 +	  then have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
   5.689 +	    by (simp cong: finsum_cong add: finsum_Un_disjoint
   5.690 +	      ivl_disj_int_singleton Pi_def)
   5.691 +	  also from True have "... = finsum R ?s {..k}"
   5.692 +	    by (simp only: ivl_disj_un_singleton)
   5.693 +	  finally show ?thesis .
   5.694 +	next
   5.695 +	  case False with n_le_k have n_less_k: "n < k" by arith
   5.696 +	  with neq have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
   5.697 +	    by (simp add: finsum_Un_disjoint f1 f2
   5.698 +	      ivl_disj_int_singleton Pi_def del: Un_insert_right)
   5.699 +	  also have "... = finsum R ?s {..n}"
   5.700 +	    by (simp only: ivl_disj_un_singleton)
   5.701 +	  also from n_less_k neq have "... = finsum R ?s ({..n} \<union> {)n..k})"
   5.702 +	    by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
   5.703 +	  also from n_less_k have "... = finsum R ?s {..k}"
   5.704 +	    by (simp only: ivl_disj_un_one)
   5.705 +	  finally show ?thesis .
   5.706 +	qed
   5.707 +      qed
   5.708 +    qed
   5.709 +    also have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k" by simp
   5.710 +    finally show ?thesis .
   5.711 +  qed
   5.712 +qed (simp_all)
   5.713 +
   5.714 +ML_setup {*
   5.715 +Context.>> (fn thy => (simpset_ref_of thy :=
   5.716 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
   5.717 +
   5.718 +lemma (in UP_cring) monom_mult_smult:
   5.719 +  "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^sub>2 monom P b n"
   5.720 +  by (rule up_eqI) simp_all
   5.721 +
   5.722 +lemma (in UP_cring) monom_one [simp]:
   5.723 +  "monom P \<one> 0 = \<one>\<^sub>2"
   5.724 +  by (rule up_eqI) simp_all
   5.725 +
   5.726 +lemma (in UP_cring) monom_one_mult:
   5.727 +  "monom P \<one> (n + m) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m"
   5.728 +proof (induct n)
   5.729 +  case 0 show ?case by simp
   5.730 +next
   5.731 +  case Suc then show ?case
   5.732 +    by (simp only: add_Suc monom_one_Suc) (simp add: UP_m_ac)
   5.733 +qed
   5.734 +
   5.735 +lemma (in UP_cring) monom_mult [simp]:
   5.736 +  assumes R: "a \<in> carrier R" "b \<in> carrier R"
   5.737 +  shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^sub>2 monom P b m"
   5.738 +proof -
   5.739 +  from R have "monom P (a \<otimes> b) (n + m) = monom P (a \<otimes> b \<otimes> \<one>) (n + m)" by simp
   5.740 +  also from R have "... = a \<otimes> b \<odot>\<^sub>2 monom P \<one> (n + m)"
   5.741 +    by (simp add: monom_mult_smult del: r_one)
   5.742 +  also have "... = a \<otimes> b \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m)"
   5.743 +    by (simp only: monom_one_mult)
   5.744 +  also from R have "... = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m))"
   5.745 +    by (simp add: UP_smult_assoc1)
   5.746 +  also from R have "... = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 (monom P \<one> m \<otimes>\<^sub>2 monom P \<one> n))"
   5.747 +    by (simp add: UP_m_comm)
   5.748 +  also from R have "... = a \<odot>\<^sub>2 ((b \<odot>\<^sub>2 monom P \<one> m) \<otimes>\<^sub>2 monom P \<one> n)"
   5.749 +    by (simp add: UP_smult_assoc2)
   5.750 +  also from R have "... = a \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 (b \<odot>\<^sub>2 monom P \<one> m))"
   5.751 +    by (simp add: UP_m_comm)
   5.752 +  also from R have "... = (a \<odot>\<^sub>2 monom P \<one> n) \<otimes>\<^sub>2 (b \<odot>\<^sub>2 monom P \<one> m)"
   5.753 +    by (simp add: UP_smult_assoc2)
   5.754 +  also from R have "... = monom P (a \<otimes> \<one>) n \<otimes>\<^sub>2 monom P (b \<otimes> \<one>) m"
   5.755 +    by (simp add: monom_mult_smult del: r_one)
   5.756 +  also from R have "... = monom P a n \<otimes>\<^sub>2 monom P b m" by simp
   5.757 +  finally show ?thesis .
   5.758 +qed
   5.759 +
   5.760 +lemma (in UP_cring) monom_a_inv [simp]:
   5.761 +  "a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^sub>2 monom P a n"
   5.762 +  by (rule up_eqI) simp_all
   5.763 +
   5.764 +lemma (in UP_cring) monom_inj:
   5.765 +  "inj_on (%a. monom P a n) (carrier R)"
   5.766 +proof (rule inj_onI)
   5.767 +  fix x y
   5.768 +  assume R: "x \<in> carrier R" "y \<in> carrier R" and eq: "monom P x n = monom P y n"
   5.769 +  then have "coeff P (monom P x n) n = coeff P (monom P y n) n" by simp
   5.770 +  with R show "x = y" by simp
   5.771 +qed
   5.772 +
   5.773 +subsection {* The Degree Function *}
   5.774 +
   5.775 +constdefs
   5.776 +  deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
   5.777 +  "deg R p == LEAST n. bound (zero R) n (coeff (UP R) p)"
   5.778 +
   5.779 +lemma (in UP_cring) deg_aboveI:
   5.780 +  "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n" 
   5.781 +  by (unfold deg_def P_def) (fast intro: Least_le)
   5.782 +(*
   5.783 +lemma coeff_bound_ex: "EX n. bound n (coeff p)"
   5.784 +proof -
   5.785 +  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   5.786 +  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   5.787 +  then show ?thesis ..
   5.788 +qed
   5.789 +  
   5.790 +lemma bound_coeff_obtain:
   5.791 +  assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
   5.792 +proof -
   5.793 +  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   5.794 +  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   5.795 +  with prem show P .
   5.796 +qed
   5.797 +*)
   5.798 +lemma (in UP_cring) deg_aboveD:
   5.799 +  "[| deg R p < m; p \<in> carrier P |] ==> coeff P p m = \<zero>"
   5.800 +proof -
   5.801 +  assume R: "p \<in> carrier P" and "deg R p < m"
   5.802 +  from R obtain n where "bound \<zero> n (coeff P p)" 
   5.803 +    by (auto simp add: UP_def P_def)
   5.804 +  then have "bound \<zero> (deg R p) (coeff P p)"
   5.805 +    by (auto simp: deg_def P_def dest: LeastI)
   5.806 +  then show ?thesis by (rule boundD)
   5.807 +qed
   5.808 +
   5.809 +lemma (in UP_cring) deg_belowI:
   5.810 +  assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
   5.811 +    and R: "p \<in> carrier P"
   5.812 +  shows "n <= deg R p"
   5.813 +-- {* Logically, this is a slightly stronger version of 
   5.814 +  @{thm [source] deg_aboveD} *}
   5.815 +proof (cases "n=0")
   5.816 +  case True then show ?thesis by simp
   5.817 +next
   5.818 +  case False then have "coeff P p n ~= \<zero>" by (rule non_zero)
   5.819 +  then have "~ deg R p < n" by (fast dest: deg_aboveD intro: R)
   5.820 +  then show ?thesis by arith
   5.821 +qed
   5.822 +
   5.823 +lemma (in UP_cring) lcoeff_nonzero_deg:
   5.824 +  assumes deg: "deg R p ~= 0" and R: "p \<in> carrier P"
   5.825 +  shows "coeff P p (deg R p) ~= \<zero>"
   5.826 +proof -
   5.827 +  from R obtain m where "deg R p <= m" and m_coeff: "coeff P p m ~= \<zero>"
   5.828 +  proof -
   5.829 +    have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
   5.830 +      by arith
   5.831 +(* TODO: why does proof not work with "1" *)
   5.832 +    from deg have "deg R p - 1 < (LEAST n. bound \<zero> n (coeff P p))"
   5.833 +      by (unfold deg_def P_def) arith
   5.834 +    then have "~ bound \<zero> (deg R p - 1) (coeff P p)" by (rule not_less_Least)
   5.835 +    then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
   5.836 +      by (unfold bound_def) fast
   5.837 +    then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
   5.838 +    then show ?thesis by auto 
   5.839 +  qed
   5.840 +  with deg_belowI R have "deg R p = m" by fastsimp
   5.841 +  with m_coeff show ?thesis by simp
   5.842 +qed
   5.843 +
   5.844 +lemma (in UP_cring) lcoeff_nonzero_nonzero:
   5.845 +  assumes deg: "deg R p = 0" and nonzero: "p ~= \<zero>\<^sub>2" and R: "p \<in> carrier P"
   5.846 +  shows "coeff P p 0 ~= \<zero>"
   5.847 +proof -
   5.848 +  have "EX m. coeff P p m ~= \<zero>"
   5.849 +  proof (rule classical)
   5.850 +    assume "~ ?thesis"
   5.851 +    with R have "p = \<zero>\<^sub>2" by (auto intro: up_eqI)
   5.852 +    with nonzero show ?thesis by contradiction
   5.853 +  qed
   5.854 +  then obtain m where coeff: "coeff P p m ~= \<zero>" ..
   5.855 +  then have "m <= deg R p" by (rule deg_belowI)
   5.856 +  then have "m = 0" by (simp add: deg)
   5.857 +  with coeff show ?thesis by simp
   5.858 +qed
   5.859 +
   5.860 +lemma (in UP_cring) lcoeff_nonzero:
   5.861 +  assumes neq: "p ~= \<zero>\<^sub>2" and R: "p \<in> carrier P"
   5.862 +  shows "coeff P p (deg R p) ~= \<zero>"
   5.863 +proof (cases "deg R p = 0")
   5.864 +  case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero)
   5.865 +next
   5.866 +  case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg)
   5.867 +qed
   5.868 +
   5.869 +lemma (in UP_cring) deg_eqI:
   5.870 +  "[| !!m. n < m ==> coeff P p m = \<zero>;
   5.871 +      !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
   5.872 +by (fast intro: le_anti_sym deg_aboveI deg_belowI)
   5.873 +
   5.874 +(* Degree and polynomial operations *)
   5.875 +
   5.876 +lemma (in UP_cring) deg_add [simp]:
   5.877 +  assumes R: "p \<in> carrier P" "q \<in> carrier P"
   5.878 +  shows "deg R (p \<oplus>\<^sub>2 q) <= max (deg R p) (deg R q)"
   5.879 +proof (cases "deg R p <= deg R q")
   5.880 +  case True show ?thesis
   5.881 +    by (rule deg_aboveI) (simp_all add: True R deg_aboveD) 
   5.882 +next
   5.883 +  case False show ?thesis
   5.884 +    by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
   5.885 +qed
   5.886 +
   5.887 +lemma (in UP_cring) deg_monom_le:
   5.888 +  "a \<in> carrier R ==> deg R (monom P a n) <= n"
   5.889 +  by (intro deg_aboveI) simp_all
   5.890 +
   5.891 +lemma (in UP_cring) deg_monom [simp]:
   5.892 +  "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
   5.893 +  by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
   5.894 +
   5.895 +lemma (in UP_cring) deg_const [simp]:
   5.896 +  assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
   5.897 +proof (rule le_anti_sym)
   5.898 +  show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R)
   5.899 +next
   5.900 +  show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
   5.901 +qed
   5.902 +
   5.903 +lemma (in UP_cring) deg_zero [simp]:
   5.904 +  "deg R \<zero>\<^sub>2 = 0"
   5.905 +proof (rule le_anti_sym)
   5.906 +  show "deg R \<zero>\<^sub>2 <= 0" by (rule deg_aboveI) simp_all
   5.907 +next
   5.908 +  show "0 <= deg R \<zero>\<^sub>2" by (rule deg_belowI) simp_all
   5.909 +qed
   5.910 +
   5.911 +lemma (in UP_cring) deg_one [simp]:
   5.912 +  "deg R \<one>\<^sub>2 = 0"
   5.913 +proof (rule le_anti_sym)
   5.914 +  show "deg R \<one>\<^sub>2 <= 0" by (rule deg_aboveI) simp_all
   5.915 +next
   5.916 +  show "0 <= deg R \<one>\<^sub>2" by (rule deg_belowI) simp_all
   5.917 +qed
   5.918 +
   5.919 +lemma (in UP_cring) deg_uminus [simp]:
   5.920 +  assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^sub>2 p) = deg R p"
   5.921 +proof (rule le_anti_sym)
   5.922 +  show "deg R (\<ominus>\<^sub>2 p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
   5.923 +next
   5.924 +  show "deg R p <= deg R (\<ominus>\<^sub>2 p)" 
   5.925 +    by (simp add: deg_belowI lcoeff_nonzero_deg
   5.926 +      inj_on_iff [OF a_inv_inj, of _ "\<zero>", simplified] R)
   5.927 +qed
   5.928 +
   5.929 +lemma (in UP_domain) deg_smult_ring:
   5.930 +  "[| a \<in> carrier R; p \<in> carrier P |] ==>
   5.931 +  deg R (a \<odot>\<^sub>2 p) <= (if a = \<zero> then 0 else deg R p)"
   5.932 +  by (cases "a = \<zero>") (simp add: deg_aboveI deg_aboveD)+
   5.933 +
   5.934 +lemma (in UP_domain) deg_smult [simp]:
   5.935 +  assumes R: "a \<in> carrier R" "p \<in> carrier P"
   5.936 +  shows "deg R (a \<odot>\<^sub>2 p) = (if a = \<zero> then 0 else deg R p)"
   5.937 +proof (rule le_anti_sym)
   5.938 +  show "deg R (a \<odot>\<^sub>2 p) <= (if a = \<zero> then 0 else deg R p)"
   5.939 +    by (rule deg_smult_ring)
   5.940 +next
   5.941 +  show "(if a = \<zero> then 0 else deg R p) <= deg R (a \<odot>\<^sub>2 p)"
   5.942 +  proof (cases "a = \<zero>")
   5.943 +  qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R)
   5.944 +qed
   5.945 +
   5.946 +lemma (in UP_cring) deg_mult_cring:
   5.947 +  assumes R: "p \<in> carrier P" "q \<in> carrier P"
   5.948 +  shows "deg R (p \<otimes>\<^sub>2 q) <= deg R p + deg R q"
   5.949 +proof (rule deg_aboveI)
   5.950 +  fix m
   5.951 +  assume boundm: "deg R p + deg R q < m"
   5.952 +  {
   5.953 +    fix k i
   5.954 +    assume boundk: "deg R p + deg R q < k"
   5.955 +    then have "coeff P p i \<otimes> coeff P q (k - i) = \<zero>"
   5.956 +    proof (cases "deg R p < i")
   5.957 +      case True then show ?thesis by (simp add: deg_aboveD R)
   5.958 +    next
   5.959 +      case False with boundk have "deg R q < k - i" by arith
   5.960 +      then show ?thesis by (simp add: deg_aboveD R)
   5.961 +    qed
   5.962 +  }
   5.963 +  with boundm R show "coeff P (p \<otimes>\<^sub>2 q) m = \<zero>" by simp
   5.964 +qed (simp add: R)
   5.965 +
   5.966 +ML_setup {*
   5.967 +Context.>> (fn thy => (simpset_ref_of thy :=
   5.968 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   5.969 +
   5.970 +lemma (in UP_domain) deg_mult [simp]:
   5.971 +  "[| p ~= \<zero>\<^sub>2; q ~= \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P |] ==>
   5.972 +  deg R (p \<otimes>\<^sub>2 q) = deg R p + deg R q"
   5.973 +proof (rule le_anti_sym)
   5.974 +  assume "p \<in> carrier P" " q \<in> carrier P"
   5.975 +  show "deg R (p \<otimes>\<^sub>2 q) <= deg R p + deg R q" by (rule deg_mult_cring)
   5.976 +next
   5.977 +  let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
   5.978 +  assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^sub>2" "q ~= \<zero>\<^sub>2"
   5.979 +  have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
   5.980 +  show "deg R p + deg R q <= deg R (p \<otimes>\<^sub>2 q)"
   5.981 +  proof (rule deg_belowI, simp add: R)
   5.982 +    have "finsum R ?s {.. deg R p + deg R q}
   5.983 +      = finsum R ?s ({.. deg R p(} Un {deg R p .. deg R p + deg R q})"
   5.984 +      by (simp only: ivl_disj_un_one)
   5.985 +    also have "... = finsum R ?s {deg R p .. deg R p + deg R q}"
   5.986 +      by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
   5.987 +        deg_aboveD less_add_diff R Pi_def)
   5.988 +    also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})"
   5.989 +      by (simp only: ivl_disj_un_singleton)
   5.990 +    also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" 
   5.991 +      by (simp cong: finsum_cong add: finsum_Un_disjoint
   5.992 +	ivl_disj_int_singleton deg_aboveD R Pi_def)
   5.993 +    finally have "finsum R ?s {.. deg R p + deg R q} 
   5.994 +      = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
   5.995 +    with nz show "finsum R ?s {.. deg R p + deg R q} ~= \<zero>"
   5.996 +      by (simp add: integral_iff lcoeff_nonzero R)
   5.997 +    qed (simp add: R)
   5.998 +  qed
   5.999 +
  5.1000 +lemma (in UP_cring) coeff_finsum:
  5.1001 +  assumes fin: "finite A"
  5.1002 +  shows "p \<in> A -> carrier P ==>
  5.1003 +    coeff P (finsum P p A) k == finsum R (%i. coeff P (p i) k) A"
  5.1004 +  using fin by induct (auto simp: Pi_def)
  5.1005 +
  5.1006 +ML_setup {*
  5.1007 +Context.>> (fn thy => (simpset_ref_of thy :=
  5.1008 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
  5.1009 +
  5.1010 +lemma (in UP_cring) up_repr:
  5.1011 +  assumes R: "p \<in> carrier P"
  5.1012 +  shows "finsum P (%i. monom P (coeff P p i) i) {..deg R p} = p"
  5.1013 +proof (rule up_eqI)
  5.1014 +  let ?s = "(%i. monom P (coeff P p i) i)"
  5.1015 +  fix k
  5.1016 +  from R have RR: "!!i. (if i = k then coeff P p i else \<zero>) \<in> carrier R"
  5.1017 +    by simp
  5.1018 +  show "coeff P (finsum P ?s {..deg R p}) k = coeff P p k"
  5.1019 +  proof (cases "k <= deg R p")
  5.1020 +    case True
  5.1021 +    hence "coeff P (finsum P ?s {..deg R p}) k = 
  5.1022 +          coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k"
  5.1023 +      by (simp only: ivl_disj_un_one)
  5.1024 +    also from True
  5.1025 +    have "... = coeff P (finsum P ?s {..k}) k"
  5.1026 +      by (simp cong: finsum_cong add: finsum_Un_disjoint
  5.1027 +	ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
  5.1028 +    also
  5.1029 +    have "... = coeff P (finsum P ?s ({..k(} Un {k})) k"
  5.1030 +      by (simp only: ivl_disj_un_singleton)
  5.1031 +    also have "... = coeff P p k"
  5.1032 +      by (simp cong: finsum_cong add: setsum_Un_disjoint
  5.1033 +	ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
  5.1034 +    finally show ?thesis .
  5.1035 +  next
  5.1036 +    case False
  5.1037 +    hence "coeff P (finsum P ?s {..deg R p}) k = 
  5.1038 +          coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k"
  5.1039 +      by (simp only: ivl_disj_un_singleton)
  5.1040 +    also from False have "... = coeff P p k"
  5.1041 +      by (simp cong: finsum_cong add: setsum_Un_disjoint ivl_disj_int_singleton
  5.1042 +        coeff_finsum deg_aboveD R Pi_def)
  5.1043 +    finally show ?thesis .
  5.1044 +  qed
  5.1045 +qed (simp_all add: R Pi_def)
  5.1046 +
  5.1047 +lemma (in UP_cring) up_repr_le:
  5.1048 +  "[| deg R p <= n; p \<in> carrier P |] ==>
  5.1049 +  finsum P (%i. monom P (coeff P p i) i) {..n} = p"
  5.1050 +proof -
  5.1051 +  let ?s = "(%i. monom P (coeff P p i) i)"
  5.1052 +  assume R: "p \<in> carrier P" and "deg R p <= n"
  5.1053 +  then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {)deg R p..n})"
  5.1054 +    by (simp only: ivl_disj_un_one)
  5.1055 +  also have "... = finsum P ?s {..deg R p}"
  5.1056 +    by (simp cong: UP_finsum_cong add: UP_finsum_Un_disjoint ivl_disj_int_one
  5.1057 +      deg_aboveD R Pi_def)
  5.1058 +  also have "... = p" by (rule up_repr)
  5.1059 +  finally show ?thesis .
  5.1060 +qed
  5.1061 +
  5.1062 +ML_setup {*
  5.1063 +Context.>> (fn thy => (simpset_ref_of thy :=
  5.1064 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
  5.1065 +
  5.1066 +subsection {* Polynomial over an Integral Domain are an Integral Domain *}
  5.1067 +
  5.1068 +lemma domainI:
  5.1069 +  assumes cring: "cring R"
  5.1070 +    and one_not_zero: "one R ~= zero R"
  5.1071 +    and integral: "!!a b. [| mult R a b = zero R; a \<in> carrier R;
  5.1072 +      b \<in> carrier R |] ==> a = zero R | b = zero R"
  5.1073 +  shows "domain R"
  5.1074 +  by (auto intro!: domain.intro domain_axioms.intro cring.axioms prems
  5.1075 +    del: disjCI)
  5.1076 +
  5.1077 +lemma (in UP_domain) UP_one_not_zero:
  5.1078 +  "\<one>\<^sub>2 ~= \<zero>\<^sub>2"
  5.1079 +proof
  5.1080 +  assume "\<one>\<^sub>2 = \<zero>\<^sub>2"
  5.1081 +  hence "coeff P \<one>\<^sub>2 0 = (coeff P \<zero>\<^sub>2 0)" by simp
  5.1082 +  hence "\<one> = \<zero>" by simp
  5.1083 +  with one_not_zero show "False" by contradiction
  5.1084 +qed
  5.1085 +
  5.1086 +lemma (in UP_domain) UP_integral:
  5.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"
  5.1088 +proof -
  5.1089 +  fix p q
  5.1090 +  assume pq: "p \<otimes>\<^sub>2 q = \<zero>\<^sub>2" and R: "p \<in> carrier P" "q \<in> carrier P"
  5.1091 +  show "p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2"
  5.1092 +  proof (rule classical)
  5.1093 +    assume c: "~ (p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2)"
  5.1094 +    with R have "deg R p + deg R q = deg R (p \<otimes>\<^sub>2 q)" by simp
  5.1095 +    also from pq have "... = 0" by simp
  5.1096 +    finally have "deg R p + deg R q = 0" .
  5.1097 +    then have f1: "deg R p = 0 & deg R q = 0" by simp
  5.1098 +    from f1 R have "p = finsum P (%i. (monom P (coeff P p i) i)) {..0}"
  5.1099 +      by (simp only: up_repr_le)
  5.1100 +    also from R have "... = monom P (coeff P p 0) 0" by simp
  5.1101 +    finally have p: "p = monom P (coeff P p 0) 0" .
  5.1102 +    from f1 R have "q = finsum P (%i. (monom P (coeff P q i) i)) {..0}"
  5.1103 +      by (simp only: up_repr_le)
  5.1104 +    also from R have "... = monom P (coeff P q 0) 0" by simp
  5.1105 +    finally have q: "q = monom P (coeff P q 0) 0" .
  5.1106 +    from R have "coeff P p 0 \<otimes> coeff P q 0 = coeff P (p \<otimes>\<^sub>2 q) 0" by simp
  5.1107 +    also from pq have "... = \<zero>" by simp
  5.1108 +    finally have "coeff P p 0 \<otimes> coeff P q 0 = \<zero>" .
  5.1109 +    with R have "coeff P p 0 = \<zero> | coeff P q 0 = \<zero>"
  5.1110 +      by (simp add: R.integral_iff)
  5.1111 +    with p q show "p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2" by fastsimp
  5.1112 +  qed
  5.1113 +qed
  5.1114 +
  5.1115 +theorem (in UP_domain) UP_domain:
  5.1116 +  "domain P"
  5.1117 +  by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI)
  5.1118 +
  5.1119 +text {*
  5.1120 +  Instantiation of results from @{term domain}.
  5.1121 +*}
  5.1122 +
  5.1123 +lemmas (in UP_domain) UP_zero_not_one [simp] =
  5.1124 +  domain.zero_not_one [OF UP_domain]
  5.1125 +
  5.1126 +lemmas (in UP_domain) UP_integral_iff =
  5.1127 +  domain.integral_iff [OF UP_domain]
  5.1128 +
  5.1129 +lemmas (in UP_domain) UP_m_lcancel =
  5.1130 +  domain.m_lcancel [OF UP_domain]
  5.1131 +
  5.1132 +lemmas (in UP_domain) UP_m_rcancel =
  5.1133 +  domain.m_rcancel [OF UP_domain]
  5.1134 +
  5.1135 +lemma (in UP_domain) smult_integral:
  5.1136 +  "[| a \<odot>\<^sub>2 p = \<zero>\<^sub>2; a \<in> carrier R; p \<in> carrier P |] ==> a = \<zero> | p = \<zero>\<^sub>2"
  5.1137 +  by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff
  5.1138 +    inj_on_iff [OF monom_inj, of _ "\<zero>", simplified])
  5.1139 +
  5.1140 +subsection {* Evaluation Homomorphism *}
  5.1141 +
  5.1142 +ML_setup {*
  5.1143 +Context.>> (fn thy => (simpset_ref_of thy :=
  5.1144 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
  5.1145 +
  5.1146 +(* alternative congruence rule (more efficient)
  5.1147 +lemma (in abelian_monoid) finsum_cong2:
  5.1148 +  "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
  5.1149 +  !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
  5.1150 +  sorry
  5.1151 +*)
  5.1152 +
  5.1153 +theorem (in cring) diagonal_sum:
  5.1154 +  "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
  5.1155 +  finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..n + m} =
  5.1156 +  finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
  5.1157 +proof -
  5.1158 +  assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
  5.1159 +  {
  5.1160 +    fix j
  5.1161 +    have "j <= n + m ==>
  5.1162 +      finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..j} =
  5.1163 +      finsum R (%k. finsum R (%i. f k \<otimes> g i) {..j - k}) {..j}"
  5.1164 +    proof (induct j)
  5.1165 +      case 0 from Rf Rg show ?case by (simp add: Pi_def)
  5.1166 +    next
  5.1167 +      case (Suc j) 
  5.1168 +      (* The following could be simplified if there was a reasoner for
  5.1169 +	total orders integrated with simip. *)
  5.1170 +      have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
  5.1171 +	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
  5.1172 +      have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
  5.1173 +	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
  5.1174 +      have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
  5.1175 +	using Suc by (auto intro!: funcset_mem [OF Rf])
  5.1176 +      have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
  5.1177 +	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
  5.1178 +      have R11: "g 0 \<in> carrier R"
  5.1179 +	using Suc by (auto intro!: funcset_mem [OF Rg])
  5.1180 +      from Suc show ?case
  5.1181 +	by (simp cong: finsum_cong add: Suc_diff_le a_ac
  5.1182 +	  Pi_def R6 R8 R9 R10 R11)
  5.1183 +    qed
  5.1184 +  }
  5.1185 +  then show ?thesis by fast
  5.1186 +qed
  5.1187 +
  5.1188 +lemma (in abelian_monoid) boundD_carrier:
  5.1189 +  "[| bound \<zero> n f; n < m |] ==> f m \<in> carrier G"
  5.1190 +  by auto
  5.1191 +
  5.1192 +theorem (in cring) cauchy_product:
  5.1193 +  assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
  5.1194 +    and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
  5.1195 +  shows "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
  5.1196 +    finsum R f {..n} \<otimes> finsum R g {..m}"
  5.1197 +(* State revese direction? *)
  5.1198 +proof -
  5.1199 +  have f: "!!x. f x \<in> carrier R"
  5.1200 +  proof -
  5.1201 +    fix x
  5.1202 +    show "f x \<in> carrier R"
  5.1203 +      using Rf bf boundD_carrier by (cases "x <= n") (auto simp: Pi_def)
  5.1204 +  qed
  5.1205 +  have g: "!!x. g x \<in> carrier R"
  5.1206 +  proof -
  5.1207 +    fix x
  5.1208 +    show "g x \<in> carrier R"
  5.1209 +      using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def)
  5.1210 +  qed
  5.1211 +  from f g have "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
  5.1212 +    finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
  5.1213 +    by (simp add: diagonal_sum Pi_def)
  5.1214 +  also have "... = finsum R
  5.1215 +      (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) ({..n} Un {)n..n + m})"
  5.1216 +    by (simp only: ivl_disj_un_one)
  5.1217 +  also from f g have "... = finsum R
  5.1218 +      (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n}"
  5.1219 +    by (simp cong: finsum_cong
  5.1220 +      add: boundD [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
  5.1221 +  also from f g have "... = finsum R
  5.1222 +      (%k. finsum R (%i. f k \<otimes> g i) ({..m} Un {)m..n + m - k})) {..n}"
  5.1223 +    by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
  5.1224 +  also from f g have "... = finsum R
  5.1225 +      (%k. finsum R (%i. f k \<otimes> g i) {..m}) {..n}"
  5.1226 +    by (simp cong: finsum_cong
  5.1227 +      add: boundD [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
  5.1228 +  also from f g have "... = finsum R f {..n} \<otimes> finsum R g {..m}"
  5.1229 +    by (simp add: finsum_ldistr diagonal_sum Pi_def,
  5.1230 +      simp cong: finsum_cong add: finsum_rdistr Pi_def)
  5.1231 +  finally show ?thesis .
  5.1232 +qed
  5.1233 +
  5.1234 +lemma (in UP_cring) const_ring_hom:
  5.1235 +  "(%a. monom P a 0) \<in> ring_hom R P"
  5.1236 +  by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
  5.1237 +
  5.1238 +constdefs
  5.1239 +  eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
  5.1240 +          'a => 'b, 'b, nat => 'a] => 'b"
  5.1241 +  "eval R S phi s == (\<lambda>p \<in> carrier (UP R).
  5.1242 +    finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p})"
  5.1243 +(*
  5.1244 +  "eval R S phi s p == if p \<in> carrier (UP R)
  5.1245 +  then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p}
  5.1246 +  else arbitrary"
  5.1247 +*)
  5.1248 +                                                         
  5.1249 +locale ring_hom_UP_cring = ring_hom_cring R S + UP_cring R
  5.1250 +
  5.1251 +lemma (in ring_hom_UP_cring) eval_on_carrier:
  5.1252 +  "p \<in> carrier P ==>
  5.1253 +    eval R S phi s p =
  5.1254 +    finsum S (%i. mult S (phi (coeff P p i)) (pow S s i)) {..deg R p}"
  5.1255 +  by (unfold eval_def, fold P_def) simp
  5.1256 +
  5.1257 +lemma (in ring_hom_UP_cring) eval_extensional:
  5.1258 +  "eval R S phi s \<in> extensional (carrier P)"
  5.1259 +  by (unfold eval_def, fold P_def) simp
  5.1260 +
  5.1261 +theorem (in ring_hom_UP_cring) eval_ring_hom:
  5.1262 +  "s \<in> carrier S ==> eval R S h s \<in> ring_hom P S"
  5.1263 +proof (rule ring_hom_memI)
  5.1264 +  fix p
  5.1265 +  assume RS: "p \<in> carrier P" "s \<in> carrier S"
  5.1266 +  then show "eval R S h s p \<in> carrier S"
  5.1267 +    by (simp only: eval_on_carrier) (simp add: Pi_def)
  5.1268 +next
  5.1269 +  fix p q
  5.1270 +  assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S"
  5.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"
  5.1272 +  proof (simp only: eval_on_carrier UP_mult_closed)
  5.1273 +    from RS have
  5.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)} =
  5.1275 +      finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  5.1276 +        ({..deg R (p \<otimes>\<^sub>3 q)} Un {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q})"
  5.1277 +      by (simp cong: finsum_cong
  5.1278 +	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
  5.1279 +	del: coeff_mult)
  5.1280 +    also from RS have "... =
  5.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}"
  5.1282 +      by (simp only: ivl_disj_un_one deg_mult_cring)
  5.1283 +    also from RS have "... =
  5.1284 +      finsum S (%i.
  5.1285 +        finsum S (%k. 
  5.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)))
  5.1287 +      {..i}) {..deg R p + deg R q}"
  5.1288 +      by (simp cong: finsum_cong add: nat_pow_mult Pi_def
  5.1289 +	S.m_ac S.finsum_rdistr)
  5.1290 +    also from RS have "... =
  5.1291 +      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
  5.1292 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
  5.1293 +      by (simp add: S.cauchy_product [THEN sym] boundI deg_aboveD S.m_ac
  5.1294 +	Pi_def)
  5.1295 +    finally show
  5.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)} =
  5.1297 +      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
  5.1298 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}" .
  5.1299 +  qed
  5.1300 +next
  5.1301 +  fix p q
  5.1302 +  assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S"
  5.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"
  5.1304 +  proof (simp only: eval_on_carrier UP_a_closed)
  5.1305 +    from RS have
  5.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)} =
  5.1307 +      finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  5.1308 +        ({..deg R (p \<oplus>\<^sub>3 q)} Un {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)})"
  5.1309 +      by (simp cong: finsum_cong
  5.1310 +	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
  5.1311 +	del: coeff_add)
  5.1312 +    also from RS have "... =
  5.1313 +      finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  5.1314 +        {..max (deg R p) (deg R q)}"
  5.1315 +      by (simp add: ivl_disj_un_one)
  5.1316 +    also from RS have "... =
  5.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
  5.1318 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)}"
  5.1319 +      by (simp cong: finsum_cong
  5.1320 +	add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
  5.1321 +    also have "... =
  5.1322 +      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  5.1323 +        ({..deg R p} Un {)deg R p..max (deg R p) (deg R q)}) \<oplus>\<^sub>2
  5.1324 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  5.1325 +        ({..deg R q} Un {)deg R q..max (deg R p) (deg R q)})"
  5.1326 +      by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
  5.1327 +    also from RS have "... =
  5.1328 +      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
  5.1329 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
  5.1330 +      by (simp cong: finsum_cong
  5.1331 +	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
  5.1332 +    finally show
  5.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)} =
  5.1334 +      finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
  5.1335 +      finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
  5.1336 +      .
  5.1337 +  qed
  5.1338 +next
  5.1339 +  assume S: "s \<in> carrier S"
  5.1340 +  then show "eval R S h s \<one>\<^sub>3 = \<one>\<^sub>2"
  5.1341 +    by (simp only: eval_on_carrier UP_one_closed) simp
  5.1342 +qed
  5.1343 +
  5.1344 +text {* Instantiation of ring homomorphism lemmas. *}
  5.1345 +
  5.1346 +lemma (in ring_hom_UP_cring) ring_hom_cring_P_S:
  5.1347 +  "s \<in> carrier S ==> ring_hom_cring P S (eval R S h s)"
  5.1348 +  by (fast intro!: ring_hom_cring.intro UP_cring cring.axioms prems
  5.1349 +  intro: ring_hom_cring_axioms.intro eval_ring_hom)
  5.1350 +
  5.1351 +lemma (in ring_hom_UP_cring) UP_hom_closed [intro, simp]:
  5.1352 +  "[| s \<in> carrier S; p \<in> carrier P |] ==> eval R S h s p \<in> carrier S"
  5.1353 +  by (rule ring_hom_cring.hom_closed [OF ring_hom_cring_P_S])
  5.1354 +
  5.1355 +lemma (in ring_hom_UP_cring) UP_hom_mult [simp]:
  5.1356 +  "[| s \<in> carrier S; p \<in> carrier P; q \<in> carrier P |] ==>
  5.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"
  5.1358 +  by (rule ring_hom_cring.hom_mult [OF ring_hom_cring_P_S])
  5.1359 +
  5.1360 +lemma (in ring_hom_UP_cring) UP_hom_add [simp]:
  5.1361 +  "[| s \<in> carrier S; p \<in> carrier P; q \<in> carrier P |] ==>
  5.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"
  5.1363 +  by (rule ring_hom_cring.hom_add [OF ring_hom_cring_P_S])
  5.1364 +
  5.1365 +lemma (in ring_hom_UP_cring) UP_hom_one [simp]:
  5.1366 +  "s \<in> carrier S ==> eval R S h s \<one>\<^sub>3 = \<one>\<^sub>2"
  5.1367 +  by (rule ring_hom_cring.hom_one [OF ring_hom_cring_P_S])
  5.1368 +
  5.1369 +lemma (in ring_hom_UP_cring) UP_hom_zero [simp]:
  5.1370 +  "s \<in> carrier S ==> eval R S h s \<zero>\<^sub>3 = \<zero>\<^sub>2"
  5.1371 +  by (rule ring_hom_cring.hom_zero [OF ring_hom_cring_P_S])
  5.1372 +
  5.1373 +lemma (in ring_hom_UP_cring) UP_hom_a_inv [simp]:
  5.1374 +  "[| s \<in> carrier S; p \<in> carrier P |] ==>
  5.1375 +  (eval R S h s) (\<ominus>\<^sub>3 p) = \<ominus>\<^sub>2 (eval R S h s) p"
  5.1376 +  by (rule ring_hom_cring.hom_a_inv [OF ring_hom_cring_P_S])
  5.1377 +
  5.1378 +lemma (in ring_hom_UP_cring) UP_hom_finsum [simp]:
  5.1379 +  "[| s \<in> carrier S; finite A; f \<in> A -> carrier P |] ==>
  5.1380 +  (eval R S h s) (finsum P f A) = finsum S (eval R S h s o f) A"
  5.1381 +  by (rule ring_hom_cring.hom_finsum [OF ring_hom_cring_P_S])
  5.1382 +
  5.1383 +lemma (in ring_hom_UP_cring) UP_hom_finprod [simp]:
  5.1384 +  "[| s \<in> carrier S; finite A; f \<in> A -> carrier P |] ==>
  5.1385 +  (eval R S h s) (finprod P f A) = finprod S (eval R S h s o f) A"
  5.1386 +  by (rule ring_hom_cring.hom_finprod [OF ring_hom_cring_P_S])
  5.1387 +
  5.1388 +text {* Further properties of the evaluation homomorphism. *}
  5.1389 +
  5.1390 +(* The following lemma could be proved in UP\_cring with the additional
  5.1391 +   assumption that h is closed. *)
  5.1392 +
  5.1393 +lemma (in ring_hom_UP_cring) eval_const:
  5.1394 +  "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
  5.1395 +  by (simp only: eval_on_carrier monom_closed) simp
  5.1396 +
  5.1397 +text {* The following proof is complicated by the fact that in arbitrary
  5.1398 +  rings one might have @{term "one R = zero R"}. *}
  5.1399 +
  5.1400 +(* TODO: simplify by cases "one R = zero R" *)
  5.1401 +
  5.1402 +lemma (in ring_hom_UP_cring) eval_monom1:
  5.1403 +  "s \<in> carrier S ==> eval R S h s (monom P \<one> 1) = s"
  5.1404 +proof (simp only: eval_on_carrier monom_closed R.one_closed)
  5.1405 +  assume S: "s \<in> carrier S"
  5.1406 +  then have "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  5.1407 +      {..deg R (monom P \<one> 1)} =
  5.1408 +    finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  5.1409 +      ({..deg R (monom P \<one> 1)} Un {)deg R (monom P \<one> 1)..1})"
  5.1410 +    by (simp cong: finsum_cong del: coeff_monom
  5.1411 +      add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
  5.1412 +  also have "... = 
  5.1413 +    finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..1}"
  5.1414 +    by (simp only: ivl_disj_un_one deg_monom_le R.one_closed)
  5.1415 +  also have "... = s"
  5.1416 +  proof (cases "s = \<zero>\<^sub>2")
  5.1417 +    case True then show ?thesis by (simp add: Pi_def)
  5.1418 +  next
  5.1419 +    case False with S show ?thesis by (simp add: Pi_def)
  5.1420 +  qed
  5.1421 +  finally show "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  5.1422 +      {..deg R (monom P \<one> 1)} = s" .
  5.1423 +qed
  5.1424 +
  5.1425 +lemma (in UP_cring) monom_pow:
  5.1426 +  assumes R: "a \<in> carrier R"
  5.1427 +  shows "(monom P a n) (^)\<^sub>2 m = monom P (a (^) m) (n * m)"
  5.1428 +proof (induct m)
  5.1429 +  case 0 from R show ?case by simp
  5.1430 +next
  5.1431 +  case Suc with R show ?case
  5.1432 +    by (simp del: monom_mult add: monom_mult [THEN sym] add_commute)
  5.1433 +qed
  5.1434 +
  5.1435 +lemma (in ring_hom_cring) hom_pow [simp]:
  5.1436 +  "x \<in> carrier R ==> h (x (^) n) = h x (^)\<^sub>2 (n::nat)"
  5.1437 +  by (induct n) simp_all
  5.1438 +
  5.1439 +lemma (in ring_hom_UP_cring) UP_hom_pow [simp]:
  5.1440 +  "[| s \<in> carrier S; p \<in> carrier P |] ==>
  5.1441 +  (eval R S h s) (p (^)\<^sub>3 n) = eval R S h s p (^)\<^sub>2 (n::nat)"
  5.1442 +  by (rule ring_hom_cring.hom_pow [OF ring_hom_cring_P_S])
  5.1443 +
  5.1444 +lemma (in ring_hom_UP_cring) eval_monom:
  5.1445 +  "[| s \<in> carrier S; r \<in> carrier R |] ==>
  5.1446 +  eval R S h s (monom P r n) = h r \<otimes>\<^sub>2 s (^)\<^sub>2 n"
  5.1447 +proof -
  5.1448 +  assume RS: "s \<in> carrier S" "r \<in> carrier R"
  5.1449 +  then have "eval R S h s (monom P r n) =
  5.1450 +    eval R S h s (monom P r 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 n)"
  5.1451 +    by (simp del: monom_mult UP_hom_mult UP_hom_pow
  5.1452 +      add: monom_mult [THEN sym] monom_pow)
  5.1453 +  also from RS eval_monom1 have "... = h r \<otimes>\<^sub>2 s (^)\<^sub>2 n"
  5.1454 +    by (simp add: eval_const)
  5.1455 +  finally show ?thesis .
  5.1456 +qed
  5.1457 +
  5.1458 +lemma (in ring_hom_UP_cring) eval_smult:
  5.1459 +  "[| s \<in> carrier S; r \<in> carrier R; p \<in> carrier P |] ==>
  5.1460 +  eval R S h s (r \<odot>\<^sub>3 p) = h r \<otimes>\<^sub>2 eval R S h s p"
  5.1461 +  by (simp add: monom_mult_is_smult [THEN sym] eval_const)
  5.1462 +
  5.1463 +lemma ring_hom_cringI:
  5.1464 +  assumes "cring R"
  5.1465 +    and "cring S"
  5.1466 +    and "h \<in> ring_hom R S"
  5.1467 +  shows "ring_hom_cring R S h"
  5.1468 +  by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
  5.1469 +    cring.axioms prems)
  5.1470 +
  5.1471 +lemma (in ring_hom_UP_cring) UP_hom_unique:
  5.1472 +  assumes Phi: "Phi \<in> ring_hom P S" "Phi (monom P \<one> (Suc 0)) = s"
  5.1473 +      "!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r"
  5.1474 +    and Psi: "Psi \<in> ring_hom P S" "Psi (monom P \<one> (Suc 0)) = s"
  5.1475 +      "!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r"
  5.1476 +    and RS: "s \<in> carrier S" "p \<in> carrier P"
  5.1477 +  shows "Phi p = Psi p"
  5.1478 +proof -
  5.1479 +  have Phi_hom: "ring_hom_cring P S Phi"
  5.1480 +    by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
  5.1481 +  have Psi_hom: "ring_hom_cring P S Psi"
  5.1482 +    by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
  5.1483 +thm monom_mult
  5.1484 +  have "Phi p = Phi (finsum P
  5.1485 +    (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
  5.1486 +    by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
  5.1487 +  also have "... = Psi (finsum P
  5.1488 +    (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
  5.1489 +    by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom] 
  5.1490 +      ring_hom_cring.hom_mult [OF Phi_hom]
  5.1491 +      ring_hom_cring.hom_pow [OF Phi_hom] Phi
  5.1492 +      ring_hom_cring.hom_finsum [OF Psi_hom] 
  5.1493 +      ring_hom_cring.hom_mult [OF Psi_hom]
  5.1494 +      ring_hom_cring.hom_pow [OF Psi_hom] Psi RS Pi_def comp_def)
  5.1495 +  also have "... = Psi p"
  5.1496 +    by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
  5.1497 +  finally show ?thesis .
  5.1498 +qed
  5.1499 +
  5.1500 +
  5.1501 +theorem (in ring_hom_UP_cring) UP_universal_property:
  5.1502 +  "s \<in> carrier S ==>
  5.1503 +  EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
  5.1504 +    Phi (monom P \<one> 1) = s & 
  5.1505 +    (ALL r : carrier R. Phi (monom P r 0) = h r)"
  5.1506 +  using eval_monom1                              
  5.1507 +  apply (auto intro: eval_ring_hom eval_const eval_extensional)
  5.1508 +  apply (rule extensionalityI)                                 
  5.1509 +  apply (auto intro: UP_hom_unique)                            
  5.1510 +  done                                                         
  5.1511 +
  5.1512 +subsection {* Sample application of evaluation homomorphism *}
  5.1513 +
  5.1514 +lemma ring_hom_UP_cringI:
  5.1515 +  assumes "cring R"
  5.1516 +    and "cring S"
  5.1517 +    and "h \<in> ring_hom R S"
  5.1518 +  shows "ring_hom_UP_cring R S h"
  5.1519 +  by (fast intro: ring_hom_UP_cring.intro ring_hom_cring_axioms.intro
  5.1520 +    cring.axioms prems)
  5.1521 +
  5.1522 +lemma INTEG_id:
  5.1523 +  "ring_hom_UP_cring INTEG INTEG id"
  5.1524 +  by (fast intro: ring_hom_UP_cringI cring_INTEG id_ring_hom)
  5.1525 +
  5.1526 +text {*
  5.1527 +  An instantiation mechanism would now import all theorems and lemmas
  5.1528 +  valid in the context of homomorphisms between @{term INTEG} and @{term
  5.1529 +  "UP INTEG"}.  *}
  5.1530 +
  5.1531 +lemma INTEG_closed [intro, simp]:
  5.1532 +  "z \<in> carrier INTEG"
  5.1533 +  by (unfold INTEG_def) simp
  5.1534 +
  5.1535 +lemma INTEG_mult [simp]:
  5.1536 +  "mult INTEG z w = z * w"
  5.1537 +  by (unfold INTEG_def) simp
  5.1538 +
  5.1539 +lemma INTEG_pow [simp]:
  5.1540 +  "pow INTEG z n = z ^ n"
  5.1541 +  by (induct n) (simp_all add: INTEG_def nat_pow_def)
  5.1542 +
  5.1543 +lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500"
  5.1544 +  by (simp add: ring_hom_UP_cring.eval_monom [OF INTEG_id])
  5.1545 +
  5.1546 +-- {* Calculates @{term "x = 500"} *}
  5.1547 +
  5.1548 +
  5.1549 +end
  5.1550 \ No newline at end of file