src/HOL/Algebra/UnivPoly.thy
author wenzelm
Thu Apr 22 11:01:34 2004 +0200 (2004-04-22)
changeset 14651 02b8f3bcf7fe
parent 14590 276ef51cedbf
child 14666 65f8680c3f16
permissions -rw-r--r--
improved notation;
     1 (*
     2   Title:     Univariate Polynomials
     3   Id:        $Id$
     4   Author:    Clemens Ballarin, started 9 December 1996
     5   Copyright: Clemens Ballarin
     6 *)
     7 
     8 header {* Univariate Polynomials *}
     9 
    10 theory UnivPoly = Module:
    11 
    12 text {*
    13   Polynomials are formalised as modules with additional operations for 
    14   extracting coefficients from polynomials and for obtaining monomials 
    15   from coefficients and exponents (record @{text "up_ring"}).
    16   The carrier set is 
    17   a set of bounded functions from Nat to the coefficient domain.  
    18   Bounded means that these functions return zero above a certain bound 
    19   (the degree).  There is a chapter on the formalisation of polynomials 
    20   in my PhD thesis (http://www4.in.tum.de/\~{}ballarin/publications/), 
    21   which was implemented with axiomatic type classes.  This was later
    22   ported to Locales.
    23 *}
    24 
    25 subsection {* The Constructor for Univariate Polynomials *}
    26 
    27 (* Could alternatively use locale ...
    28 locale bound = cring + var bound +
    29   defines ...
    30 *)
    31 
    32 constdefs
    33   bound  :: "['a, nat, nat => 'a] => bool"
    34   "bound z n f == (ALL i. n < i --> f i = z)"
    35 
    36 lemma boundI [intro!]:
    37   "[| !! m. n < m ==> f m = z |] ==> bound z n f"
    38   by (unfold bound_def) fast
    39 
    40 lemma boundE [elim?]:
    41   "[| bound z n f; (!! m. n < m ==> f m = z) ==> P |] ==> P"
    42   by (unfold bound_def) fast
    43 
    44 lemma boundD [dest]:
    45   "[| bound z n f; n < m |] ==> f m = z"
    46   by (unfold bound_def) fast
    47 
    48 lemma bound_below:
    49   assumes bound: "bound z m f" and nonzero: "f n ~= z" shows "n <= m"
    50 proof (rule classical)
    51   assume "~ ?thesis"
    52   then have "m < n" by arith
    53   with bound have "f n = z" ..
    54   with nonzero show ?thesis by contradiction
    55 qed
    56 
    57 record ('a, 'p) up_ring = "('a, 'p) module" +
    58   monom :: "['a, nat] => 'p"
    59   coeff :: "['p, nat] => 'a"
    60 
    61 constdefs (structure R)
    62   up :: "_ => (nat => 'a) set"
    63   "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero> n f)}"
    64   UP :: "_ => ('a, nat => 'a) up_ring"
    65   "UP R == (|
    66     carrier = up R,
    67     mult = (%p:up R. %q:up R. %n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)),
    68     one = (%i. if i=0 then \<one> else \<zero>),
    69     zero = (%i. \<zero>),
    70     add = (%p:up R. %q:up R. %i. p i \<oplus> q i),
    71     smult = (%a:carrier R. %p:up R. %i. a \<otimes> p i),
    72     monom = (%a:carrier R. %n i. if i=n then a else \<zero>),
    73     coeff = (%p:up R. %n. p n) |)"
    74 
    75 text {*
    76   Properties of the set of polynomials @{term up}.
    77 *}
    78 
    79 lemma mem_upI [intro]:
    80   "[| !!n. f n \<in> carrier R; EX n. bound (zero R) n f |] ==> f \<in> up R"
    81   by (simp add: up_def Pi_def)
    82 
    83 lemma mem_upD [dest]:
    84   "f \<in> up R ==> f n \<in> carrier R"
    85   by (simp add: up_def Pi_def)
    86 
    87 lemma (in cring) bound_upD [dest]:
    88   "f \<in> up R ==> EX n. bound \<zero> n f"
    89   by (simp add: up_def)
    90 
    91 lemma (in cring) up_one_closed:
    92    "(%n. if n = 0 then \<one> else \<zero>) \<in> up R"
    93   using up_def by force
    94 
    95 lemma (in cring) up_smult_closed:
    96   "[| a \<in> carrier R; p \<in> up R |] ==> (%i. a \<otimes> p i) \<in> up R"
    97   by force
    98 
    99 lemma (in cring) up_add_closed:
   100   "[| p \<in> up R; q \<in> up R |] ==> (%i. p i \<oplus> q i) \<in> up R"
   101 proof
   102   fix n
   103   assume "p \<in> up R" and "q \<in> up R"
   104   then show "p n \<oplus> q n \<in> carrier R"
   105     by auto
   106 next
   107   assume UP: "p \<in> up R" "q \<in> up R"
   108   show "EX n. bound \<zero> n (%i. p i \<oplus> q i)"
   109   proof -
   110     from UP obtain n where boundn: "bound \<zero> n p" by fast
   111     from UP obtain m where boundm: "bound \<zero> m q" by fast
   112     have "bound \<zero> (max n m) (%i. p i \<oplus> q i)"
   113     proof
   114       fix i
   115       assume "max n m < i"
   116       with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastsimp
   117     qed
   118     then show ?thesis ..
   119   qed
   120 qed
   121 
   122 lemma (in cring) up_a_inv_closed:
   123   "p \<in> up R ==> (%i. \<ominus> (p i)) \<in> up R"
   124 proof
   125   assume R: "p \<in> up R"
   126   then obtain n where "bound \<zero> n p" by auto
   127   then have "bound \<zero> n (%i. \<ominus> p i)" by auto
   128   then show "EX n. bound \<zero> n (%i. \<ominus> p i)" by auto
   129 qed auto
   130 
   131 lemma (in cring) up_mult_closed:
   132   "[| p \<in> up R; q \<in> up R |] ==>
   133   (%n. finsum R (%i. p i \<otimes> q (n-i)) {..n}) \<in> up R"
   134 proof
   135   fix n
   136   assume "p \<in> up R" "q \<in> up R"
   137   then show "finsum R (%i. p i \<otimes> q (n-i)) {..n} \<in> carrier R"
   138     by (simp add: mem_upD  funcsetI)
   139 next
   140   assume UP: "p \<in> up R" "q \<in> up R"
   141   show "EX n. bound \<zero> n (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
   142   proof -
   143     from UP obtain n where boundn: "bound \<zero> n p" by fast
   144     from UP obtain m where boundm: "bound \<zero> m q" by fast
   145     have "bound \<zero> (n + m) (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
   146     proof
   147       fix k
   148       assume bound: "n + m < k"
   149       {
   150 	fix i
   151 	have "p i \<otimes> q (k-i) = \<zero>"
   152 	proof (cases "n < i")
   153 	  case True
   154 	  with boundn have "p i = \<zero>" by auto
   155           moreover from UP have "q (k-i) \<in> carrier R" by auto
   156 	  ultimately show ?thesis by simp
   157 	next
   158 	  case False
   159 	  with bound have "m < k-i" by arith
   160 	  with boundm have "q (k-i) = \<zero>" by auto
   161 	  moreover from UP have "p i \<in> carrier R" by auto
   162 	  ultimately show ?thesis by simp
   163 	qed
   164       }
   165       then show "finsum R (%i. p i \<otimes> q (k-i)) {..k} = \<zero>"
   166 	by (simp add: Pi_def)
   167     qed
   168     then show ?thesis by fast
   169   qed
   170 qed
   171 
   172 subsection {* Effect of operations on coefficients *}
   173 
   174 locale UP = struct R + struct P +
   175   defines P_def: "P == UP R"
   176 
   177 locale UP_cring = UP + cring R
   178 
   179 locale UP_domain = UP_cring + "domain" R
   180 
   181 text {*
   182   Temporarily declare @{text UP.P_def} as simp rule.
   183 *}  (* TODO: use antiquotation once text (in locale) is supported. *)
   184 
   185 declare (in UP) P_def [simp]
   186 
   187 lemma (in UP_cring) coeff_monom [simp]:
   188   "a \<in> carrier R ==>
   189   coeff P (monom P a m) n = (if m=n then a else \<zero>)"
   190 proof -
   191   assume R: "a \<in> carrier R"
   192   then have "(%n. if n = m then a else \<zero>) \<in> up R"
   193     using up_def by force
   194   with R show ?thesis by (simp add: UP_def)
   195 qed
   196 
   197 lemma (in UP_cring) coeff_zero [simp]:
   198   "coeff P \<zero>\<^sub>2 n = \<zero>"
   199   by (auto simp add: UP_def)
   200 
   201 lemma (in UP_cring) coeff_one [simp]:
   202   "coeff P \<one>\<^sub>2 n = (if n=0 then \<one> else \<zero>)"
   203   using up_one_closed by (simp add: UP_def)
   204 
   205 lemma (in UP_cring) coeff_smult [simp]:
   206   "[| a \<in> carrier R; p \<in> carrier P |] ==>
   207   coeff P (a \<odot>\<^sub>2 p) n = a \<otimes> coeff P p n"
   208   by (simp add: UP_def up_smult_closed)
   209 
   210 lemma (in UP_cring) coeff_add [simp]:
   211   "[| p \<in> carrier P; q \<in> carrier P |] ==>
   212   coeff P (p \<oplus>\<^sub>2 q) n = coeff P p n \<oplus> coeff P q n"
   213   by (simp add: UP_def up_add_closed)
   214 
   215 lemma (in UP_cring) coeff_mult [simp]:
   216   "[| p \<in> carrier P; q \<in> carrier P |] ==>
   217   coeff P (p \<otimes>\<^sub>2 q) n = finsum R (%i. coeff P p i \<otimes> coeff P q (n-i)) {..n}"
   218   by (simp add: UP_def up_mult_closed)
   219 
   220 lemma (in UP) up_eqI:
   221   assumes prem: "!!n. coeff P p n = coeff P q n"
   222     and R: "p \<in> carrier P" "q \<in> carrier P"
   223   shows "p = q"
   224 proof
   225   fix x
   226   from prem and R show "p x = q x" by (simp add: UP_def)
   227 qed
   228   
   229 subsection {* Polynomials form a commutative ring. *}
   230 
   231 text {* Operations are closed over @{term "P"}. *}
   232 
   233 lemma (in UP_cring) UP_mult_closed [simp]:
   234   "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^sub>2 q \<in> carrier P"
   235   by (simp add: UP_def up_mult_closed)
   236 
   237 lemma (in UP_cring) UP_one_closed [simp]:
   238   "\<one>\<^sub>2 \<in> carrier P"
   239   by (simp add: UP_def up_one_closed)
   240 
   241 lemma (in UP_cring) UP_zero_closed [intro, simp]:
   242   "\<zero>\<^sub>2 \<in> carrier P"
   243   by (auto simp add: UP_def)
   244 
   245 lemma (in UP_cring) UP_a_closed [intro, simp]:
   246   "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<oplus>\<^sub>2 q \<in> carrier P"
   247   by (simp add: UP_def up_add_closed)
   248 
   249 lemma (in UP_cring) monom_closed [simp]:
   250   "a \<in> carrier R ==> monom P a n \<in> carrier P"
   251   by (auto simp add: UP_def up_def Pi_def)
   252 
   253 lemma (in UP_cring) UP_smult_closed [simp]:
   254   "[| a \<in> carrier R; p \<in> carrier P |] ==> a \<odot>\<^sub>2 p \<in> carrier P"
   255   by (simp add: UP_def up_smult_closed)
   256 
   257 lemma (in UP) coeff_closed [simp]:
   258   "p \<in> carrier P ==> coeff P p n \<in> carrier R"
   259   by (auto simp add: UP_def)
   260 
   261 declare (in UP) P_def [simp del]
   262 
   263 text {* Algebraic ring properties *}
   264 
   265 lemma (in UP_cring) UP_a_assoc:
   266   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   267   shows "(p \<oplus>\<^sub>2 q) \<oplus>\<^sub>2 r = p \<oplus>\<^sub>2 (q \<oplus>\<^sub>2 r)"
   268   by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
   269 
   270 lemma (in UP_cring) UP_l_zero [simp]:
   271   assumes R: "p \<in> carrier P"
   272   shows "\<zero>\<^sub>2 \<oplus>\<^sub>2 p = p"
   273   by (rule up_eqI, simp_all add: R)
   274 
   275 lemma (in UP_cring) UP_l_neg_ex:
   276   assumes R: "p \<in> carrier P"
   277   shows "EX q : carrier P. q \<oplus>\<^sub>2 p = \<zero>\<^sub>2"
   278 proof -
   279   let ?q = "%i. \<ominus> (p i)"
   280   from R have closed: "?q \<in> carrier P"
   281     by (simp add: UP_def P_def up_a_inv_closed)
   282   from R have coeff: "!!n. coeff P ?q n = \<ominus> (coeff P p n)"
   283     by (simp add: UP_def P_def up_a_inv_closed)
   284   show ?thesis
   285   proof
   286     show "?q \<oplus>\<^sub>2 p = \<zero>\<^sub>2"
   287       by (auto intro!: up_eqI simp add: R closed coeff R.l_neg)
   288   qed (rule closed)
   289 qed
   290 
   291 lemma (in UP_cring) UP_a_comm:
   292   assumes R: "p \<in> carrier P" "q \<in> carrier P"
   293   shows "p \<oplus>\<^sub>2 q = q \<oplus>\<^sub>2 p"
   294   by (rule up_eqI, simp add: a_comm R, simp_all add: R)
   295 
   296 ML_setup {*
   297   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
   298 *}
   299 
   300 lemma (in UP_cring) UP_m_assoc:
   301   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   302   shows "(p \<otimes>\<^sub>2 q) \<otimes>\<^sub>2 r = p \<otimes>\<^sub>2 (q \<otimes>\<^sub>2 r)"
   303 proof (rule up_eqI)
   304   fix n
   305   {
   306     fix k and a b c :: "nat=>'a"
   307     assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
   308       "c \<in> UNIV -> carrier R"
   309     then have "k <= n ==>
   310       finsum R (%j. finsum R (%i. a i \<otimes> b (j-i)) {..j} \<otimes> c (n-j)) {..k} =
   311       finsum R (%j. a j \<otimes> finsum R (%i. b i \<otimes> c (n-j-i)) {..k-j}) {..k}"
   312       (is "_ ==> ?eq k")
   313     proof (induct k)
   314       case 0 then show ?case by (simp add: Pi_def m_assoc)
   315     next
   316       case (Suc k)
   317       then have "k <= n" by arith
   318       then have "?eq k" by (rule Suc)
   319       with R show ?case
   320 	by (simp cong: finsum_cong
   321              add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
   322           (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
   323     qed
   324   }
   325   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"
   326     by (simp add: Pi_def)
   327 qed (simp_all add: R)
   328 
   329 ML_setup {*
   330   simpset_ref() := simpset() setsubgoaler asm_simp_tac;
   331 *}
   332 
   333 lemma (in UP_cring) UP_l_one [simp]:
   334   assumes R: "p \<in> carrier P"
   335   shows "\<one>\<^sub>2 \<otimes>\<^sub>2 p = p"
   336 proof (rule up_eqI)
   337   fix n
   338   show "coeff P (\<one>\<^sub>2 \<otimes>\<^sub>2 p) n = coeff P p n"
   339   proof (cases n)
   340     case 0 with R show ?thesis by simp
   341   next
   342     case Suc with R show ?thesis
   343       by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)
   344   qed
   345 qed (simp_all add: R)
   346 
   347 lemma (in UP_cring) UP_l_distr:
   348   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   349   shows "(p \<oplus>\<^sub>2 q) \<otimes>\<^sub>2 r = (p \<otimes>\<^sub>2 r) \<oplus>\<^sub>2 (q \<otimes>\<^sub>2 r)"
   350   by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R)
   351 
   352 lemma (in UP_cring) UP_m_comm:
   353   assumes R: "p \<in> carrier P" "q \<in> carrier P"
   354   shows "p \<otimes>\<^sub>2 q = q \<otimes>\<^sub>2 p"
   355 proof (rule up_eqI)
   356   fix n 
   357   {
   358     fix k and a b :: "nat=>'a"
   359     assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
   360     then have "k <= n ==> 
   361       finsum R (%i. a i \<otimes> b (n-i)) {..k} =
   362       finsum R (%i. a (k-i) \<otimes> b (i+n-k)) {..k}"
   363       (is "_ ==> ?eq k")
   364     proof (induct k)
   365       case 0 then show ?case by (simp add: Pi_def)
   366     next
   367       case (Suc k) then show ?case
   368 	by (subst finsum_Suc2) (simp add: Pi_def a_comm)+
   369     qed
   370   }
   371   note l = this
   372   from R show "coeff P (p \<otimes>\<^sub>2 q) n =  coeff P (q \<otimes>\<^sub>2 p) n"
   373     apply (simp add: Pi_def)
   374     apply (subst l)
   375     apply (auto simp add: Pi_def)
   376     apply (simp add: m_comm)
   377     done
   378 qed (simp_all add: R)
   379 
   380 theorem (in UP_cring) UP_cring:
   381   "cring P"
   382   by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
   383     UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
   384 
   385 lemma (in UP_cring) UP_ring:  (* preliminary *)
   386   "ring P"
   387   by (auto intro: ring.intro cring.axioms UP_cring)
   388 
   389 lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
   390   "p \<in> carrier P ==> \<ominus>\<^sub>2 p \<in> carrier P"
   391   by (rule abelian_group.a_inv_closed
   392     [OF ring.is_abelian_group [OF UP_ring]])
   393 
   394 lemma (in UP_cring) coeff_a_inv [simp]:
   395   assumes R: "p \<in> carrier P"
   396   shows "coeff P (\<ominus>\<^sub>2 p) n = \<ominus> (coeff P p n)"
   397 proof -
   398   from R coeff_closed UP_a_inv_closed have
   399     "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)"
   400     by algebra
   401   also from R have "... =  \<ominus> (coeff P p n)"
   402     by (simp del: coeff_add add: coeff_add [THEN sym]
   403       abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]])
   404   finally show ?thesis .
   405 qed
   406 
   407 text {*
   408   Instantiation of lemmas from @{term cring}.
   409 *}
   410 
   411 lemma (in UP_cring) UP_monoid:
   412   "monoid P"
   413   by (fast intro!: cring.is_comm_monoid comm_monoid.axioms monoid.intro
   414     UP_cring)
   415 (* TODO: provide cring.is_monoid *)
   416 
   417 lemma (in UP_cring) UP_comm_semigroup:
   418   "comm_semigroup P"
   419   by (fast intro!: cring.is_comm_monoid comm_monoid.axioms comm_semigroup.intro
   420     UP_cring)
   421 
   422 lemma (in UP_cring) UP_comm_monoid:
   423   "comm_monoid P"
   424   by (fast intro!: cring.is_comm_monoid UP_cring)
   425 
   426 lemma (in UP_cring) UP_abelian_monoid:
   427   "abelian_monoid P"
   428   by (fast intro!: abelian_group.axioms ring.is_abelian_group UP_ring)
   429 
   430 lemma (in UP_cring) UP_abelian_group:
   431   "abelian_group P"
   432   by (fast intro!: ring.is_abelian_group UP_ring)
   433 
   434 lemmas (in UP_cring) UP_r_one [simp] =
   435   monoid.r_one [OF UP_monoid]
   436 
   437 lemmas (in UP_cring) UP_nat_pow_closed [intro, simp] =
   438   monoid.nat_pow_closed [OF UP_monoid]
   439 
   440 lemmas (in UP_cring) UP_nat_pow_0 [simp] =
   441   monoid.nat_pow_0 [OF UP_monoid]
   442 
   443 lemmas (in UP_cring) UP_nat_pow_Suc [simp] =
   444   monoid.nat_pow_Suc [OF UP_monoid]
   445 
   446 lemmas (in UP_cring) UP_nat_pow_one [simp] =
   447   monoid.nat_pow_one [OF UP_monoid]
   448 
   449 lemmas (in UP_cring) UP_nat_pow_mult =
   450   monoid.nat_pow_mult [OF UP_monoid]
   451 
   452 lemmas (in UP_cring) UP_nat_pow_pow =
   453   monoid.nat_pow_pow [OF UP_monoid]
   454 
   455 lemmas (in UP_cring) UP_m_lcomm =
   456   comm_semigroup.m_lcomm [OF UP_comm_semigroup]
   457 
   458 lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm
   459 
   460 lemmas (in UP_cring) UP_nat_pow_distr =
   461   comm_monoid.nat_pow_distr [OF UP_comm_monoid]
   462 
   463 lemmas (in UP_cring) UP_a_lcomm = abelian_monoid.a_lcomm [OF UP_abelian_monoid]
   464 
   465 lemmas (in UP_cring) UP_r_zero [simp] =
   466   abelian_monoid.r_zero [OF UP_abelian_monoid]
   467 
   468 lemmas (in UP_cring) UP_a_ac = UP_a_assoc UP_a_comm UP_a_lcomm
   469 
   470 lemmas (in UP_cring) UP_finsum_empty [simp] =
   471   abelian_monoid.finsum_empty [OF UP_abelian_monoid]
   472 
   473 lemmas (in UP_cring) UP_finsum_insert [simp] =
   474   abelian_monoid.finsum_insert [OF UP_abelian_monoid]
   475 
   476 lemmas (in UP_cring) UP_finsum_zero [simp] =
   477   abelian_monoid.finsum_zero [OF UP_abelian_monoid]
   478 
   479 lemmas (in UP_cring) UP_finsum_closed [simp] =
   480   abelian_monoid.finsum_closed [OF UP_abelian_monoid]
   481 
   482 lemmas (in UP_cring) UP_finsum_Un_Int =
   483   abelian_monoid.finsum_Un_Int [OF UP_abelian_monoid]
   484 
   485 lemmas (in UP_cring) UP_finsum_Un_disjoint =
   486   abelian_monoid.finsum_Un_disjoint [OF UP_abelian_monoid]
   487 
   488 lemmas (in UP_cring) UP_finsum_addf =
   489   abelian_monoid.finsum_addf [OF UP_abelian_monoid]
   490 
   491 lemmas (in UP_cring) UP_finsum_cong' =
   492   abelian_monoid.finsum_cong' [OF UP_abelian_monoid]
   493 
   494 lemmas (in UP_cring) UP_finsum_0 [simp] =
   495   abelian_monoid.finsum_0 [OF UP_abelian_monoid]
   496 
   497 lemmas (in UP_cring) UP_finsum_Suc [simp] =
   498   abelian_monoid.finsum_Suc [OF UP_abelian_monoid]
   499 
   500 lemmas (in UP_cring) UP_finsum_Suc2 =
   501   abelian_monoid.finsum_Suc2 [OF UP_abelian_monoid]
   502 
   503 lemmas (in UP_cring) UP_finsum_add [simp] =
   504   abelian_monoid.finsum_add [OF UP_abelian_monoid]
   505 
   506 lemmas (in UP_cring) UP_finsum_cong =
   507   abelian_monoid.finsum_cong [OF UP_abelian_monoid]
   508 
   509 lemmas (in UP_cring) UP_minus_closed [intro, simp] =
   510   abelian_group.minus_closed [OF UP_abelian_group]
   511 
   512 lemmas (in UP_cring) UP_a_l_cancel [simp] =
   513   abelian_group.a_l_cancel [OF UP_abelian_group]
   514 
   515 lemmas (in UP_cring) UP_a_r_cancel [simp] =
   516   abelian_group.a_r_cancel [OF UP_abelian_group]
   517 
   518 lemmas (in UP_cring) UP_l_neg =
   519   abelian_group.l_neg [OF UP_abelian_group]
   520 
   521 lemmas (in UP_cring) UP_r_neg =
   522   abelian_group.r_neg [OF UP_abelian_group]
   523 
   524 lemmas (in UP_cring) UP_minus_zero [simp] =
   525   abelian_group.minus_zero [OF UP_abelian_group]
   526 
   527 lemmas (in UP_cring) UP_minus_minus [simp] =
   528   abelian_group.minus_minus [OF UP_abelian_group]
   529 
   530 lemmas (in UP_cring) UP_minus_add =
   531   abelian_group.minus_add [OF UP_abelian_group]
   532 
   533 lemmas (in UP_cring) UP_r_neg2 =
   534   abelian_group.r_neg2 [OF UP_abelian_group]
   535 
   536 lemmas (in UP_cring) UP_r_neg1 =
   537   abelian_group.r_neg1 [OF UP_abelian_group]
   538 
   539 lemmas (in UP_cring) UP_r_distr =
   540   ring.r_distr [OF UP_ring]
   541 
   542 lemmas (in UP_cring) UP_l_null [simp] =
   543   ring.l_null [OF UP_ring]
   544 
   545 lemmas (in UP_cring) UP_r_null [simp] =
   546   ring.r_null [OF UP_ring]
   547 
   548 lemmas (in UP_cring) UP_l_minus =
   549   ring.l_minus [OF UP_ring]
   550 
   551 lemmas (in UP_cring) UP_r_minus =
   552   ring.r_minus [OF UP_ring]
   553 
   554 lemmas (in UP_cring) UP_finsum_ldistr =
   555   cring.finsum_ldistr [OF UP_cring]
   556 
   557 lemmas (in UP_cring) UP_finsum_rdistr =
   558   cring.finsum_rdistr [OF UP_cring]
   559 
   560 subsection {* Polynomials form an Algebra *}
   561 
   562 lemma (in UP_cring) UP_smult_l_distr:
   563   "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
   564   (a \<oplus> b) \<odot>\<^sub>2 p = a \<odot>\<^sub>2 p \<oplus>\<^sub>2 b \<odot>\<^sub>2 p"
   565   by (rule up_eqI) (simp_all add: R.l_distr)
   566 
   567 lemma (in UP_cring) UP_smult_r_distr:
   568   "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
   569   a \<odot>\<^sub>2 (p \<oplus>\<^sub>2 q) = a \<odot>\<^sub>2 p \<oplus>\<^sub>2 a \<odot>\<^sub>2 q"
   570   by (rule up_eqI) (simp_all add: R.r_distr)
   571 
   572 lemma (in UP_cring) UP_smult_assoc1:
   573       "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
   574       (a \<otimes> b) \<odot>\<^sub>2 p = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 p)"
   575   by (rule up_eqI) (simp_all add: R.m_assoc)
   576 
   577 lemma (in UP_cring) UP_smult_one [simp]:
   578       "p \<in> carrier P ==> \<one> \<odot>\<^sub>2 p = p"
   579   by (rule up_eqI) simp_all
   580 
   581 lemma (in UP_cring) UP_smult_assoc2:
   582   "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
   583   (a \<odot>\<^sub>2 p) \<otimes>\<^sub>2 q = a \<odot>\<^sub>2 (p \<otimes>\<^sub>2 q)"
   584   by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def)
   585 
   586 text {*
   587   Instantiation of lemmas from @{term algebra}.
   588 *}
   589 
   590 (* TODO: move to CRing.thy, really a fact missing from the locales package *)
   591 
   592 lemma (in cring) cring:
   593   "cring R"
   594   by (fast intro: cring.intro prems)
   595 
   596 lemma (in UP_cring) UP_algebra:
   597   "algebra R P"
   598   by (auto intro: algebraI cring UP_cring UP_smult_l_distr UP_smult_r_distr
   599     UP_smult_assoc1 UP_smult_assoc2)
   600 
   601 lemmas (in UP_cring) UP_smult_l_null [simp] =
   602   algebra.smult_l_null [OF UP_algebra]
   603 
   604 lemmas (in UP_cring) UP_smult_r_null [simp] =
   605   algebra.smult_r_null [OF UP_algebra]
   606 
   607 lemmas (in UP_cring) UP_smult_l_minus =
   608   algebra.smult_l_minus [OF UP_algebra]
   609 
   610 lemmas (in UP_cring) UP_smult_r_minus =
   611   algebra.smult_r_minus [OF UP_algebra]
   612 
   613 subsection {* Further lemmas involving monomials *}
   614 
   615 lemma (in UP_cring) monom_zero [simp]:
   616   "monom P \<zero> n = \<zero>\<^sub>2"
   617   by (simp add: UP_def P_def)
   618 
   619 ML_setup {*
   620   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
   621 *}
   622 
   623 lemma (in UP_cring) monom_mult_is_smult:
   624   assumes R: "a \<in> carrier R" "p \<in> carrier P"
   625   shows "monom P a 0 \<otimes>\<^sub>2 p = a \<odot>\<^sub>2 p"
   626 proof (rule up_eqI)
   627   fix n
   628   have "coeff P (p \<otimes>\<^sub>2 monom P a 0) n = coeff P (a \<odot>\<^sub>2 p) n"
   629   proof (cases n)
   630     case 0 with R show ?thesis by (simp add: R.m_comm)
   631   next
   632     case Suc with R show ?thesis
   633       by (simp cong: finsum_cong add: R.r_null Pi_def)
   634         (simp add: m_comm)
   635   qed
   636   with R show "coeff P (monom P a 0 \<otimes>\<^sub>2 p) n = coeff P (a \<odot>\<^sub>2 p) n"
   637     by (simp add: UP_m_comm)
   638 qed (simp_all add: R)
   639 
   640 ML_setup {*
   641   simpset_ref() := simpset() setsubgoaler asm_simp_tac;
   642 *}
   643 
   644 lemma (in UP_cring) monom_add [simp]:
   645   "[| a \<in> carrier R; b \<in> carrier R |] ==>
   646   monom P (a \<oplus> b) n = monom P a n \<oplus>\<^sub>2 monom P b n"
   647   by (rule up_eqI) simp_all
   648 
   649 ML_setup {*
   650   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
   651 *}
   652 
   653 lemma (in UP_cring) monom_one_Suc:
   654   "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1"
   655 proof (rule up_eqI)
   656   fix k
   657   show "coeff P (monom P \<one> (Suc n)) k = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k"
   658   proof (cases "k = Suc n")
   659     case True show ?thesis
   660     proof -
   661       from True have less_add_diff: 
   662 	"!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
   663       from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
   664       also from True
   665       have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
   666 	coeff P (monom P \<one> 1) (k - i)) ({..n(} Un {n})"
   667 	by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
   668       also have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
   669 	coeff P (monom P \<one> 1) (k - i)) {..n}"
   670 	by (simp only: ivl_disj_un_singleton)
   671       also from True have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
   672 	coeff P (monom P \<one> 1) (k - i)) ({..n} Un {)n..k})"
   673 	by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
   674 	  order_less_imp_not_eq Pi_def)
   675       also from True have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k"
   676 	by (simp add: ivl_disj_un_one)
   677       finally show ?thesis .
   678     qed
   679   next
   680     case False
   681     note neq = False
   682     let ?s =
   683       "(\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>))"
   684     from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
   685     also have "... = finsum R ?s {..k}"
   686     proof -
   687       have f1: "finsum R ?s {..n(} = \<zero>" by (simp cong: finsum_cong add: Pi_def)
   688       from neq have f2: "finsum R ?s {n} = \<zero>"
   689 	by (simp cong: finsum_cong add: Pi_def) arith
   690       have f3: "n < k ==> finsum R ?s {)n..k} = \<zero>"
   691 	by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
   692       show ?thesis
   693       proof (cases "k < n")
   694 	case True then show ?thesis by (simp cong: finsum_cong add: Pi_def)
   695       next
   696 	case False then have n_le_k: "n <= k" by arith
   697 	show ?thesis
   698 	proof (cases "n = k")
   699 	  case True
   700 	  then have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
   701 	    by (simp cong: finsum_cong add: finsum_Un_disjoint
   702 	      ivl_disj_int_singleton Pi_def)
   703 	  also from True have "... = finsum R ?s {..k}"
   704 	    by (simp only: ivl_disj_un_singleton)
   705 	  finally show ?thesis .
   706 	next
   707 	  case False with n_le_k have n_less_k: "n < k" by arith
   708 	  with neq have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
   709 	    by (simp add: finsum_Un_disjoint f1 f2
   710 	      ivl_disj_int_singleton Pi_def del: Un_insert_right)
   711 	  also have "... = finsum R ?s {..n}"
   712 	    by (simp only: ivl_disj_un_singleton)
   713 	  also from n_less_k neq have "... = finsum R ?s ({..n} \<union> {)n..k})"
   714 	    by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
   715 	  also from n_less_k have "... = finsum R ?s {..k}"
   716 	    by (simp only: ivl_disj_un_one)
   717 	  finally show ?thesis .
   718 	qed
   719       qed
   720     qed
   721     also have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k" by simp
   722     finally show ?thesis .
   723   qed
   724 qed (simp_all)
   725 
   726 ML_setup {*
   727   simpset_ref() := simpset() setsubgoaler asm_simp_tac;
   728 *}
   729 
   730 lemma (in UP_cring) monom_mult_smult:
   731   "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^sub>2 monom P b n"
   732   by (rule up_eqI) simp_all
   733 
   734 lemma (in UP_cring) monom_one [simp]:
   735   "monom P \<one> 0 = \<one>\<^sub>2"
   736   by (rule up_eqI) simp_all
   737 
   738 lemma (in UP_cring) monom_one_mult:
   739   "monom P \<one> (n + m) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m"
   740 proof (induct n)
   741   case 0 show ?case by simp
   742 next
   743   case Suc then show ?case
   744     by (simp only: add_Suc monom_one_Suc) (simp add: UP_m_ac)
   745 qed
   746 
   747 lemma (in UP_cring) monom_mult [simp]:
   748   assumes R: "a \<in> carrier R" "b \<in> carrier R"
   749   shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^sub>2 monom P b m"
   750 proof -
   751   from R have "monom P (a \<otimes> b) (n + m) = monom P (a \<otimes> b \<otimes> \<one>) (n + m)" by simp
   752   also from R have "... = a \<otimes> b \<odot>\<^sub>2 monom P \<one> (n + m)"
   753     by (simp add: monom_mult_smult del: r_one)
   754   also have "... = a \<otimes> b \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m)"
   755     by (simp only: monom_one_mult)
   756   also from R have "... = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m))"
   757     by (simp add: UP_smult_assoc1)
   758   also from R have "... = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 (monom P \<one> m \<otimes>\<^sub>2 monom P \<one> n))"
   759     by (simp add: UP_m_comm)
   760   also from R have "... = a \<odot>\<^sub>2 ((b \<odot>\<^sub>2 monom P \<one> m) \<otimes>\<^sub>2 monom P \<one> n)"
   761     by (simp add: UP_smult_assoc2)
   762   also from R have "... = a \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 (b \<odot>\<^sub>2 monom P \<one> m))"
   763     by (simp add: UP_m_comm)
   764   also from R have "... = (a \<odot>\<^sub>2 monom P \<one> n) \<otimes>\<^sub>2 (b \<odot>\<^sub>2 monom P \<one> m)"
   765     by (simp add: UP_smult_assoc2)
   766   also from R have "... = monom P (a \<otimes> \<one>) n \<otimes>\<^sub>2 monom P (b \<otimes> \<one>) m"
   767     by (simp add: monom_mult_smult del: r_one)
   768   also from R have "... = monom P a n \<otimes>\<^sub>2 monom P b m" by simp
   769   finally show ?thesis .
   770 qed
   771 
   772 lemma (in UP_cring) monom_a_inv [simp]:
   773   "a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^sub>2 monom P a n"
   774   by (rule up_eqI) simp_all
   775 
   776 lemma (in UP_cring) monom_inj:
   777   "inj_on (%a. monom P a n) (carrier R)"
   778 proof (rule inj_onI)
   779   fix x y
   780   assume R: "x \<in> carrier R" "y \<in> carrier R" and eq: "monom P x n = monom P y n"
   781   then have "coeff P (monom P x n) n = coeff P (monom P y n) n" by simp
   782   with R show "x = y" by simp
   783 qed
   784 
   785 subsection {* The degree function *}
   786 
   787 constdefs (structure R)
   788   deg :: "[_, nat => 'a] => nat"
   789   "deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
   790 
   791 lemma (in UP_cring) deg_aboveI:
   792   "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n" 
   793   by (unfold deg_def P_def) (fast intro: Least_le)
   794 (*
   795 lemma coeff_bound_ex: "EX n. bound n (coeff p)"
   796 proof -
   797   have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   798   then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   799   then show ?thesis ..
   800 qed
   801   
   802 lemma bound_coeff_obtain:
   803   assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
   804 proof -
   805   have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   806   then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   807   with prem show P .
   808 qed
   809 *)
   810 lemma (in UP_cring) deg_aboveD:
   811   "[| deg R p < m; p \<in> carrier P |] ==> coeff P p m = \<zero>"
   812 proof -
   813   assume R: "p \<in> carrier P" and "deg R p < m"
   814   from R obtain n where "bound \<zero> n (coeff P p)" 
   815     by (auto simp add: UP_def P_def)
   816   then have "bound \<zero> (deg R p) (coeff P p)"
   817     by (auto simp: deg_def P_def dest: LeastI)
   818   then show ?thesis by (rule boundD)
   819 qed
   820 
   821 lemma (in UP_cring) deg_belowI:
   822   assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
   823     and R: "p \<in> carrier P"
   824   shows "n <= deg R p"
   825 -- {* Logically, this is a slightly stronger version of 
   826   @{thm [source] deg_aboveD} *}
   827 proof (cases "n=0")
   828   case True then show ?thesis by simp
   829 next
   830   case False then have "coeff P p n ~= \<zero>" by (rule non_zero)
   831   then have "~ deg R p < n" by (fast dest: deg_aboveD intro: R)
   832   then show ?thesis by arith
   833 qed
   834 
   835 lemma (in UP_cring) lcoeff_nonzero_deg:
   836   assumes deg: "deg R p ~= 0" and R: "p \<in> carrier P"
   837   shows "coeff P p (deg R p) ~= \<zero>"
   838 proof -
   839   from R obtain m where "deg R p <= m" and m_coeff: "coeff P p m ~= \<zero>"
   840   proof -
   841     have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
   842       by arith
   843 (* TODO: why does proof not work with "1" *)
   844     from deg have "deg R p - 1 < (LEAST n. bound \<zero> n (coeff P p))"
   845       by (unfold deg_def P_def) arith
   846     then have "~ bound \<zero> (deg R p - 1) (coeff P p)" by (rule not_less_Least)
   847     then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
   848       by (unfold bound_def) fast
   849     then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
   850     then show ?thesis by auto 
   851   qed
   852   with deg_belowI R have "deg R p = m" by fastsimp
   853   with m_coeff show ?thesis by simp
   854 qed
   855 
   856 lemma (in UP_cring) lcoeff_nonzero_nonzero:
   857   assumes deg: "deg R p = 0" and nonzero: "p ~= \<zero>\<^sub>2" and R: "p \<in> carrier P"
   858   shows "coeff P p 0 ~= \<zero>"
   859 proof -
   860   have "EX m. coeff P p m ~= \<zero>"
   861   proof (rule classical)
   862     assume "~ ?thesis"
   863     with R have "p = \<zero>\<^sub>2" by (auto intro: up_eqI)
   864     with nonzero show ?thesis by contradiction
   865   qed
   866   then obtain m where coeff: "coeff P p m ~= \<zero>" ..
   867   then have "m <= deg R p" by (rule deg_belowI)
   868   then have "m = 0" by (simp add: deg)
   869   with coeff show ?thesis by simp
   870 qed
   871 
   872 lemma (in UP_cring) lcoeff_nonzero:
   873   assumes neq: "p ~= \<zero>\<^sub>2" and R: "p \<in> carrier P"
   874   shows "coeff P p (deg R p) ~= \<zero>"
   875 proof (cases "deg R p = 0")
   876   case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero)
   877 next
   878   case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg)
   879 qed
   880 
   881 lemma (in UP_cring) deg_eqI:
   882   "[| !!m. n < m ==> coeff P p m = \<zero>;
   883       !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
   884 by (fast intro: le_anti_sym deg_aboveI deg_belowI)
   885 
   886 (* Degree and polynomial operations *)
   887 
   888 lemma (in UP_cring) deg_add [simp]:
   889   assumes R: "p \<in> carrier P" "q \<in> carrier P"
   890   shows "deg R (p \<oplus>\<^sub>2 q) <= max (deg R p) (deg R q)"
   891 proof (cases "deg R p <= deg R q")
   892   case True show ?thesis
   893     by (rule deg_aboveI) (simp_all add: True R deg_aboveD) 
   894 next
   895   case False show ?thesis
   896     by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
   897 qed
   898 
   899 lemma (in UP_cring) deg_monom_le:
   900   "a \<in> carrier R ==> deg R (monom P a n) <= n"
   901   by (intro deg_aboveI) simp_all
   902 
   903 lemma (in UP_cring) deg_monom [simp]:
   904   "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
   905   by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
   906 
   907 lemma (in UP_cring) deg_const [simp]:
   908   assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
   909 proof (rule le_anti_sym)
   910   show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R)
   911 next
   912   show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
   913 qed
   914 
   915 lemma (in UP_cring) deg_zero [simp]:
   916   "deg R \<zero>\<^sub>2 = 0"
   917 proof (rule le_anti_sym)
   918   show "deg R \<zero>\<^sub>2 <= 0" by (rule deg_aboveI) simp_all
   919 next
   920   show "0 <= deg R \<zero>\<^sub>2" by (rule deg_belowI) simp_all
   921 qed
   922 
   923 lemma (in UP_cring) deg_one [simp]:
   924   "deg R \<one>\<^sub>2 = 0"
   925 proof (rule le_anti_sym)
   926   show "deg R \<one>\<^sub>2 <= 0" by (rule deg_aboveI) simp_all
   927 next
   928   show "0 <= deg R \<one>\<^sub>2" by (rule deg_belowI) simp_all
   929 qed
   930 
   931 lemma (in UP_cring) deg_uminus [simp]:
   932   assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^sub>2 p) = deg R p"
   933 proof (rule le_anti_sym)
   934   show "deg R (\<ominus>\<^sub>2 p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
   935 next
   936   show "deg R p <= deg R (\<ominus>\<^sub>2 p)" 
   937     by (simp add: deg_belowI lcoeff_nonzero_deg
   938       inj_on_iff [OF a_inv_inj, of _ "\<zero>", simplified] R)
   939 qed
   940 
   941 lemma (in UP_domain) deg_smult_ring:
   942   "[| a \<in> carrier R; p \<in> carrier P |] ==>
   943   deg R (a \<odot>\<^sub>2 p) <= (if a = \<zero> then 0 else deg R p)"
   944   by (cases "a = \<zero>") (simp add: deg_aboveI deg_aboveD)+
   945 
   946 lemma (in UP_domain) deg_smult [simp]:
   947   assumes R: "a \<in> carrier R" "p \<in> carrier P"
   948   shows "deg R (a \<odot>\<^sub>2 p) = (if a = \<zero> then 0 else deg R p)"
   949 proof (rule le_anti_sym)
   950   show "deg R (a \<odot>\<^sub>2 p) <= (if a = \<zero> then 0 else deg R p)"
   951     by (rule deg_smult_ring)
   952 next
   953   show "(if a = \<zero> then 0 else deg R p) <= deg R (a \<odot>\<^sub>2 p)"
   954   proof (cases "a = \<zero>")
   955   qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R)
   956 qed
   957 
   958 lemma (in UP_cring) deg_mult_cring:
   959   assumes R: "p \<in> carrier P" "q \<in> carrier P"
   960   shows "deg R (p \<otimes>\<^sub>2 q) <= deg R p + deg R q"
   961 proof (rule deg_aboveI)
   962   fix m
   963   assume boundm: "deg R p + deg R q < m"
   964   {
   965     fix k i
   966     assume boundk: "deg R p + deg R q < k"
   967     then have "coeff P p i \<otimes> coeff P q (k - i) = \<zero>"
   968     proof (cases "deg R p < i")
   969       case True then show ?thesis by (simp add: deg_aboveD R)
   970     next
   971       case False with boundk have "deg R q < k - i" by arith
   972       then show ?thesis by (simp add: deg_aboveD R)
   973     qed
   974   }
   975   with boundm R show "coeff P (p \<otimes>\<^sub>2 q) m = \<zero>" by simp
   976 qed (simp add: R)
   977 
   978 ML_setup {*
   979   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
   980 *}
   981 
   982 lemma (in UP_domain) deg_mult [simp]:
   983   "[| p ~= \<zero>\<^sub>2; q ~= \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P |] ==>
   984   deg R (p \<otimes>\<^sub>2 q) = deg R p + deg R q"
   985 proof (rule le_anti_sym)
   986   assume "p \<in> carrier P" " q \<in> carrier P"
   987   show "deg R (p \<otimes>\<^sub>2 q) <= deg R p + deg R q" by (rule deg_mult_cring)
   988 next
   989   let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
   990   assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^sub>2" "q ~= \<zero>\<^sub>2"
   991   have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
   992   show "deg R p + deg R q <= deg R (p \<otimes>\<^sub>2 q)"
   993   proof (rule deg_belowI, simp add: R)
   994     have "finsum R ?s {.. deg R p + deg R q}
   995       = finsum R ?s ({.. deg R p(} Un {deg R p .. deg R p + deg R q})"
   996       by (simp only: ivl_disj_un_one)
   997     also have "... = finsum R ?s {deg R p .. deg R p + deg R q}"
   998       by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
   999         deg_aboveD less_add_diff R Pi_def)
  1000     also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})"
  1001       by (simp only: ivl_disj_un_singleton)
  1002     also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" 
  1003       by (simp cong: finsum_cong add: finsum_Un_disjoint
  1004 	ivl_disj_int_singleton deg_aboveD R Pi_def)
  1005     finally have "finsum R ?s {.. deg R p + deg R q} 
  1006       = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
  1007     with nz show "finsum R ?s {.. deg R p + deg R q} ~= \<zero>"
  1008       by (simp add: integral_iff lcoeff_nonzero R)
  1009     qed (simp add: R)
  1010   qed
  1011 
  1012 lemma (in UP_cring) coeff_finsum:
  1013   assumes fin: "finite A"
  1014   shows "p \<in> A -> carrier P ==>
  1015     coeff P (finsum P p A) k == finsum R (%i. coeff P (p i) k) A"
  1016   using fin by induct (auto simp: Pi_def)
  1017 
  1018 ML_setup {*
  1019   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
  1020 *}
  1021 
  1022 lemma (in UP_cring) up_repr:
  1023   assumes R: "p \<in> carrier P"
  1024   shows "finsum P (%i. monom P (coeff P p i) i) {..deg R p} = p"
  1025 proof (rule up_eqI)
  1026   let ?s = "(%i. monom P (coeff P p i) i)"
  1027   fix k
  1028   from R have RR: "!!i. (if i = k then coeff P p i else \<zero>) \<in> carrier R"
  1029     by simp
  1030   show "coeff P (finsum P ?s {..deg R p}) k = coeff P p k"
  1031   proof (cases "k <= deg R p")
  1032     case True
  1033     hence "coeff P (finsum P ?s {..deg R p}) k = 
  1034           coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k"
  1035       by (simp only: ivl_disj_un_one)
  1036     also from True
  1037     have "... = coeff P (finsum P ?s {..k}) k"
  1038       by (simp cong: finsum_cong add: finsum_Un_disjoint
  1039 	ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
  1040     also
  1041     have "... = coeff P (finsum P ?s ({..k(} Un {k})) k"
  1042       by (simp only: ivl_disj_un_singleton)
  1043     also have "... = coeff P p k"
  1044       by (simp cong: finsum_cong add: setsum_Un_disjoint
  1045 	ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
  1046     finally show ?thesis .
  1047   next
  1048     case False
  1049     hence "coeff P (finsum P ?s {..deg R p}) k = 
  1050           coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k"
  1051       by (simp only: ivl_disj_un_singleton)
  1052     also from False have "... = coeff P p k"
  1053       by (simp cong: finsum_cong add: setsum_Un_disjoint ivl_disj_int_singleton
  1054         coeff_finsum deg_aboveD R Pi_def)
  1055     finally show ?thesis .
  1056   qed
  1057 qed (simp_all add: R Pi_def)
  1058 
  1059 lemma (in UP_cring) up_repr_le:
  1060   "[| deg R p <= n; p \<in> carrier P |] ==>
  1061   finsum P (%i. monom P (coeff P p i) i) {..n} = p"
  1062 proof -
  1063   let ?s = "(%i. monom P (coeff P p i) i)"
  1064   assume R: "p \<in> carrier P" and "deg R p <= n"
  1065   then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {)deg R p..n})"
  1066     by (simp only: ivl_disj_un_one)
  1067   also have "... = finsum P ?s {..deg R p}"
  1068     by (simp cong: UP_finsum_cong add: UP_finsum_Un_disjoint ivl_disj_int_one
  1069       deg_aboveD R Pi_def)
  1070   also have "... = p" by (rule up_repr)
  1071   finally show ?thesis .
  1072 qed
  1073 
  1074 ML_setup {*
  1075   simpset_ref() := simpset() setsubgoaler asm_simp_tac;
  1076 *}
  1077 
  1078 subsection {* Polynomials over an integral domain form an integral domain *}
  1079 
  1080 lemma domainI:
  1081   assumes cring: "cring R"
  1082     and one_not_zero: "one R ~= zero R"
  1083     and integral: "!!a b. [| mult R a b = zero R; a \<in> carrier R;
  1084       b \<in> carrier R |] ==> a = zero R | b = zero R"
  1085   shows "domain R"
  1086   by (auto intro!: domain.intro domain_axioms.intro cring.axioms prems
  1087     del: disjCI)
  1088 
  1089 lemma (in UP_domain) UP_one_not_zero:
  1090   "\<one>\<^sub>2 ~= \<zero>\<^sub>2"
  1091 proof
  1092   assume "\<one>\<^sub>2 = \<zero>\<^sub>2"
  1093   hence "coeff P \<one>\<^sub>2 0 = (coeff P \<zero>\<^sub>2 0)" by simp
  1094   hence "\<one> = \<zero>" by simp
  1095   with one_not_zero show "False" by contradiction
  1096 qed
  1097 
  1098 lemma (in UP_domain) UP_integral:
  1099   "[| p \<otimes>\<^sub>2 q = \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P |] ==> p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2"
  1100 proof -
  1101   fix p q
  1102   assume pq: "p \<otimes>\<^sub>2 q = \<zero>\<^sub>2" and R: "p \<in> carrier P" "q \<in> carrier P"
  1103   show "p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2"
  1104   proof (rule classical)
  1105     assume c: "~ (p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2)"
  1106     with R have "deg R p + deg R q = deg R (p \<otimes>\<^sub>2 q)" by simp
  1107     also from pq have "... = 0" by simp
  1108     finally have "deg R p + deg R q = 0" .
  1109     then have f1: "deg R p = 0 & deg R q = 0" by simp
  1110     from f1 R have "p = finsum P (%i. (monom P (coeff P p i) i)) {..0}"
  1111       by (simp only: up_repr_le)
  1112     also from R have "... = monom P (coeff P p 0) 0" by simp
  1113     finally have p: "p = monom P (coeff P p 0) 0" .
  1114     from f1 R have "q = finsum P (%i. (monom P (coeff P q i) i)) {..0}"
  1115       by (simp only: up_repr_le)
  1116     also from R have "... = monom P (coeff P q 0) 0" by simp
  1117     finally have q: "q = monom P (coeff P q 0) 0" .
  1118     from R have "coeff P p 0 \<otimes> coeff P q 0 = coeff P (p \<otimes>\<^sub>2 q) 0" by simp
  1119     also from pq have "... = \<zero>" by simp
  1120     finally have "coeff P p 0 \<otimes> coeff P q 0 = \<zero>" .
  1121     with R have "coeff P p 0 = \<zero> | coeff P q 0 = \<zero>"
  1122       by (simp add: R.integral_iff)
  1123     with p q show "p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2" by fastsimp
  1124   qed
  1125 qed
  1126 
  1127 theorem (in UP_domain) UP_domain:
  1128   "domain P"
  1129   by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI)
  1130 
  1131 text {*
  1132   Instantiation of results from @{term domain}.
  1133 *}
  1134 
  1135 lemmas (in UP_domain) UP_zero_not_one [simp] =
  1136   domain.zero_not_one [OF UP_domain]
  1137 
  1138 lemmas (in UP_domain) UP_integral_iff =
  1139   domain.integral_iff [OF UP_domain]
  1140 
  1141 lemmas (in UP_domain) UP_m_lcancel =
  1142   domain.m_lcancel [OF UP_domain]
  1143 
  1144 lemmas (in UP_domain) UP_m_rcancel =
  1145   domain.m_rcancel [OF UP_domain]
  1146 
  1147 lemma (in UP_domain) smult_integral:
  1148   "[| a \<odot>\<^sub>2 p = \<zero>\<^sub>2; a \<in> carrier R; p \<in> carrier P |] ==> a = \<zero> | p = \<zero>\<^sub>2"
  1149   by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff
  1150     inj_on_iff [OF monom_inj, of _ "\<zero>", simplified])
  1151 
  1152 subsection {* Evaluation Homomorphism and Universal Property*}
  1153 
  1154 ML_setup {*
  1155   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
  1156 *}
  1157 
  1158 (* alternative congruence rule (possibly more efficient)
  1159 lemma (in abelian_monoid) finsum_cong2:
  1160   "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
  1161   !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
  1162   sorry
  1163 *)
  1164 
  1165 theorem (in cring) diagonal_sum:
  1166   "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
  1167   finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..n + m} =
  1168   finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
  1169 proof -
  1170   assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
  1171   {
  1172     fix j
  1173     have "j <= n + m ==>
  1174       finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..j} =
  1175       finsum R (%k. finsum R (%i. f k \<otimes> g i) {..j - k}) {..j}"
  1176     proof (induct j)
  1177       case 0 from Rf Rg show ?case by (simp add: Pi_def)
  1178     next
  1179       case (Suc j) 
  1180       (* The following could be simplified if there was a reasoner for
  1181 	total orders integrated with simip. *)
  1182       have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
  1183 	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
  1184       have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
  1185 	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
  1186       have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
  1187 	using Suc by (auto intro!: funcset_mem [OF Rf])
  1188       have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
  1189 	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
  1190       have R11: "g 0 \<in> carrier R"
  1191 	using Suc by (auto intro!: funcset_mem [OF Rg])
  1192       from Suc show ?case
  1193 	by (simp cong: finsum_cong add: Suc_diff_le a_ac
  1194 	  Pi_def R6 R8 R9 R10 R11)
  1195     qed
  1196   }
  1197   then show ?thesis by fast
  1198 qed
  1199 
  1200 lemma (in abelian_monoid) boundD_carrier:
  1201   "[| bound \<zero> n f; n < m |] ==> f m \<in> carrier G"
  1202   by auto
  1203 
  1204 theorem (in cring) cauchy_product:
  1205   assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
  1206     and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
  1207   shows "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
  1208     finsum R f {..n} \<otimes> finsum R g {..m}"
  1209 (* State revese direction? *)
  1210 proof -
  1211   have f: "!!x. f x \<in> carrier R"
  1212   proof -
  1213     fix x
  1214     show "f x \<in> carrier R"
  1215       using Rf bf boundD_carrier by (cases "x <= n") (auto simp: Pi_def)
  1216   qed
  1217   have g: "!!x. g x \<in> carrier R"
  1218   proof -
  1219     fix x
  1220     show "g x \<in> carrier R"
  1221       using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def)
  1222   qed
  1223   from f g have "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
  1224     finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
  1225     by (simp add: diagonal_sum Pi_def)
  1226   also have "... = finsum R
  1227       (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) ({..n} Un {)n..n + m})"
  1228     by (simp only: ivl_disj_un_one)
  1229   also from f g have "... = finsum R
  1230       (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n}"
  1231     by (simp cong: finsum_cong
  1232       add: boundD [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
  1233   also from f g have "... = finsum R
  1234       (%k. finsum R (%i. f k \<otimes> g i) ({..m} Un {)m..n + m - k})) {..n}"
  1235     by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
  1236   also from f g have "... = finsum R
  1237       (%k. finsum R (%i. f k \<otimes> g i) {..m}) {..n}"
  1238     by (simp cong: finsum_cong
  1239       add: boundD [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
  1240   also from f g have "... = finsum R f {..n} \<otimes> finsum R g {..m}"
  1241     by (simp add: finsum_ldistr diagonal_sum Pi_def,
  1242       simp cong: finsum_cong add: finsum_rdistr Pi_def)
  1243   finally show ?thesis .
  1244 qed
  1245 
  1246 lemma (in UP_cring) const_ring_hom:
  1247   "(%a. monom P a 0) \<in> ring_hom R P"
  1248   by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
  1249 
  1250 constdefs (structure S)
  1251   eval :: "[_, _, 'a => 'b, 'b, nat => 'a] => 'b"
  1252   "eval R S phi s == \<lambda>p \<in> carrier (UP R).
  1253     \<Oplus>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes> pow S s i"
  1254 (*
  1255   "eval R S phi s p == if p \<in> carrier (UP R)
  1256   then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p}
  1257   else arbitrary"
  1258 *)
  1259                                                          
  1260 locale ring_hom_UP_cring = ring_hom_cring R S + UP_cring R
  1261 
  1262 lemma (in ring_hom_UP_cring) eval_on_carrier:
  1263   "p \<in> carrier P ==>
  1264     eval R S phi s p =
  1265     finsum S (%i. mult S (phi (coeff P p i)) (pow S s i)) {..deg R p}"
  1266   by (unfold eval_def, fold P_def) simp
  1267 
  1268 lemma (in ring_hom_UP_cring) eval_extensional:
  1269   "eval R S phi s \<in> extensional (carrier P)"
  1270   by (unfold eval_def, fold P_def) simp
  1271 
  1272 theorem (in ring_hom_UP_cring) eval_ring_hom:
  1273   "s \<in> carrier S ==> eval R S h s \<in> ring_hom P S"
  1274 proof (rule ring_hom_memI)
  1275   fix p
  1276   assume RS: "p \<in> carrier P" "s \<in> carrier S"
  1277   then show "eval R S h s p \<in> carrier S"
  1278     by (simp only: eval_on_carrier) (simp add: Pi_def)
  1279 next
  1280   fix p q
  1281   assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S"
  1282   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"
  1283   proof (simp only: eval_on_carrier UP_mult_closed)
  1284     from RS have
  1285       "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)} =
  1286       finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1287         ({..deg R (p \<otimes>\<^sub>3 q)} Un {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q})"
  1288       by (simp cong: finsum_cong
  1289 	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
  1290 	del: coeff_mult)
  1291     also from RS have "... =
  1292       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}"
  1293       by (simp only: ivl_disj_un_one deg_mult_cring)
  1294     also from RS have "... =
  1295       finsum S (%i.
  1296         finsum S (%k. 
  1297         (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)))
  1298       {..i}) {..deg R p + deg R q}"
  1299       by (simp cong: finsum_cong add: nat_pow_mult Pi_def
  1300 	S.m_ac S.finsum_rdistr)
  1301     also from RS have "... =
  1302       finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
  1303       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
  1304       by (simp add: S.cauchy_product [THEN sym] boundI deg_aboveD S.m_ac
  1305 	Pi_def)
  1306     finally show
  1307       "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)} =
  1308       finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
  1309       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}" .
  1310   qed
  1311 next
  1312   fix p q
  1313   assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S"
  1314   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"
  1315   proof (simp only: eval_on_carrier UP_a_closed)
  1316     from RS have
  1317       "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)} =
  1318       finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1319         ({..deg R (p \<oplus>\<^sub>3 q)} Un {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)})"
  1320       by (simp cong: finsum_cong
  1321 	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
  1322 	del: coeff_add)
  1323     also from RS have "... =
  1324       finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1325         {..max (deg R p) (deg R q)}"
  1326       by (simp add: ivl_disj_un_one)
  1327     also from RS have "... =
  1328       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
  1329       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)}"
  1330       by (simp cong: finsum_cong
  1331 	add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
  1332     also have "... =
  1333       finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1334         ({..deg R p} Un {)deg R p..max (deg R p) (deg R q)}) \<oplus>\<^sub>2
  1335       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1336         ({..deg R q} Un {)deg R q..max (deg R p) (deg R q)})"
  1337       by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
  1338     also from RS have "... =
  1339       finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
  1340       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
  1341       by (simp cong: finsum_cong
  1342 	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
  1343     finally show
  1344       "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)} =
  1345       finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
  1346       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
  1347       .
  1348   qed
  1349 next
  1350   assume S: "s \<in> carrier S"
  1351   then show "eval R S h s \<one>\<^sub>3 = \<one>\<^sub>2"
  1352     by (simp only: eval_on_carrier UP_one_closed) simp
  1353 qed
  1354 
  1355 text {* Instantiation of ring homomorphism lemmas. *}
  1356 
  1357 lemma (in ring_hom_UP_cring) ring_hom_cring_P_S:
  1358   "s \<in> carrier S ==> ring_hom_cring P S (eval R S h s)"
  1359   by (fast intro!: ring_hom_cring.intro UP_cring cring.axioms prems
  1360   intro: ring_hom_cring_axioms.intro eval_ring_hom)
  1361 
  1362 lemma (in ring_hom_UP_cring) UP_hom_closed [intro, simp]:
  1363   "[| s \<in> carrier S; p \<in> carrier P |] ==> eval R S h s p \<in> carrier S"
  1364   by (rule ring_hom_cring.hom_closed [OF ring_hom_cring_P_S])
  1365 
  1366 lemma (in ring_hom_UP_cring) UP_hom_mult [simp]:
  1367   "[| s \<in> carrier S; p \<in> carrier P; q \<in> carrier P |] ==>
  1368   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"
  1369   by (rule ring_hom_cring.hom_mult [OF ring_hom_cring_P_S])
  1370 
  1371 lemma (in ring_hom_UP_cring) UP_hom_add [simp]:
  1372   "[| s \<in> carrier S; p \<in> carrier P; q \<in> carrier P |] ==>
  1373   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"
  1374   by (rule ring_hom_cring.hom_add [OF ring_hom_cring_P_S])
  1375 
  1376 lemma (in ring_hom_UP_cring) UP_hom_one [simp]:
  1377   "s \<in> carrier S ==> eval R S h s \<one>\<^sub>3 = \<one>\<^sub>2"
  1378   by (rule ring_hom_cring.hom_one [OF ring_hom_cring_P_S])
  1379 
  1380 lemma (in ring_hom_UP_cring) UP_hom_zero [simp]:
  1381   "s \<in> carrier S ==> eval R S h s \<zero>\<^sub>3 = \<zero>\<^sub>2"
  1382   by (rule ring_hom_cring.hom_zero [OF ring_hom_cring_P_S])
  1383 
  1384 lemma (in ring_hom_UP_cring) UP_hom_a_inv [simp]:
  1385   "[| s \<in> carrier S; p \<in> carrier P |] ==>
  1386   (eval R S h s) (\<ominus>\<^sub>3 p) = \<ominus>\<^sub>2 (eval R S h s) p"
  1387   by (rule ring_hom_cring.hom_a_inv [OF ring_hom_cring_P_S])
  1388 
  1389 lemma (in ring_hom_UP_cring) UP_hom_finsum [simp]:
  1390   "[| s \<in> carrier S; finite A; f \<in> A -> carrier P |] ==>
  1391   (eval R S h s) (finsum P f A) = finsum S (eval R S h s o f) A"
  1392   by (rule ring_hom_cring.hom_finsum [OF ring_hom_cring_P_S])
  1393 
  1394 lemma (in ring_hom_UP_cring) UP_hom_finprod [simp]:
  1395   "[| s \<in> carrier S; finite A; f \<in> A -> carrier P |] ==>
  1396   (eval R S h s) (finprod P f A) = finprod S (eval R S h s o f) A"
  1397   by (rule ring_hom_cring.hom_finprod [OF ring_hom_cring_P_S])
  1398 
  1399 text {* Further properties of the evaluation homomorphism. *}
  1400 
  1401 (* The following lemma could be proved in UP\_cring with the additional
  1402    assumption that h is closed. *)
  1403 
  1404 lemma (in ring_hom_UP_cring) eval_const:
  1405   "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
  1406   by (simp only: eval_on_carrier monom_closed) simp
  1407 
  1408 text {* The following proof is complicated by the fact that in arbitrary
  1409   rings one might have @{term "one R = zero R"}. *}
  1410 
  1411 (* TODO: simplify by cases "one R = zero R" *)
  1412 
  1413 lemma (in ring_hom_UP_cring) eval_monom1:
  1414   "s \<in> carrier S ==> eval R S h s (monom P \<one> 1) = s"
  1415 proof (simp only: eval_on_carrier monom_closed R.one_closed)
  1416   assume S: "s \<in> carrier S"
  1417   then have "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1418       {..deg R (monom P \<one> 1)} =
  1419     finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1420       ({..deg R (monom P \<one> 1)} Un {)deg R (monom P \<one> 1)..1})"
  1421     by (simp cong: finsum_cong del: coeff_monom
  1422       add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
  1423   also have "... = 
  1424     finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..1}"
  1425     by (simp only: ivl_disj_un_one deg_monom_le R.one_closed)
  1426   also have "... = s"
  1427   proof (cases "s = \<zero>\<^sub>2")
  1428     case True then show ?thesis by (simp add: Pi_def)
  1429   next
  1430     case False with S show ?thesis by (simp add: Pi_def)
  1431   qed
  1432   finally show "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
  1433       {..deg R (monom P \<one> 1)} = s" .
  1434 qed
  1435 
  1436 lemma (in UP_cring) monom_pow:
  1437   assumes R: "a \<in> carrier R"
  1438   shows "(monom P a n) (^)\<^sub>2 m = monom P (a (^) m) (n * m)"
  1439 proof (induct m)
  1440   case 0 from R show ?case by simp
  1441 next
  1442   case Suc with R show ?case
  1443     by (simp del: monom_mult add: monom_mult [THEN sym] add_commute)
  1444 qed
  1445 
  1446 lemma (in ring_hom_cring) hom_pow [simp]:
  1447   "x \<in> carrier R ==> h (x (^) n) = h x (^)\<^sub>2 (n::nat)"
  1448   by (induct n) simp_all
  1449 
  1450 lemma (in ring_hom_UP_cring) UP_hom_pow [simp]:
  1451   "[| s \<in> carrier S; p \<in> carrier P |] ==>
  1452   (eval R S h s) (p (^)\<^sub>3 n) = eval R S h s p (^)\<^sub>2 (n::nat)"
  1453   by (rule ring_hom_cring.hom_pow [OF ring_hom_cring_P_S])
  1454 
  1455 lemma (in ring_hom_UP_cring) eval_monom:
  1456   "[| s \<in> carrier S; r \<in> carrier R |] ==>
  1457   eval R S h s (monom P r n) = h r \<otimes>\<^sub>2 s (^)\<^sub>2 n"
  1458 proof -
  1459   assume RS: "s \<in> carrier S" "r \<in> carrier R"
  1460   then have "eval R S h s (monom P r n) =
  1461     eval R S h s (monom P r 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 n)"
  1462     by (simp del: monom_mult UP_hom_mult UP_hom_pow
  1463       add: monom_mult [THEN sym] monom_pow)
  1464   also from RS eval_monom1 have "... = h r \<otimes>\<^sub>2 s (^)\<^sub>2 n"
  1465     by (simp add: eval_const)
  1466   finally show ?thesis .
  1467 qed
  1468 
  1469 lemma (in ring_hom_UP_cring) eval_smult:
  1470   "[| s \<in> carrier S; r \<in> carrier R; p \<in> carrier P |] ==>
  1471   eval R S h s (r \<odot>\<^sub>3 p) = h r \<otimes>\<^sub>2 eval R S h s p"
  1472   by (simp add: monom_mult_is_smult [THEN sym] eval_const)
  1473 
  1474 lemma ring_hom_cringI:
  1475   assumes "cring R"
  1476     and "cring S"
  1477     and "h \<in> ring_hom R S"
  1478   shows "ring_hom_cring R S h"
  1479   by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
  1480     cring.axioms prems)
  1481 
  1482 lemma (in ring_hom_UP_cring) UP_hom_unique:
  1483   assumes Phi: "Phi \<in> ring_hom P S" "Phi (monom P \<one> (Suc 0)) = s"
  1484       "!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r"
  1485     and Psi: "Psi \<in> ring_hom P S" "Psi (monom P \<one> (Suc 0)) = s"
  1486       "!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r"
  1487     and RS: "s \<in> carrier S" "p \<in> carrier P"
  1488   shows "Phi p = Psi p"
  1489 proof -
  1490   have Phi_hom: "ring_hom_cring P S Phi"
  1491     by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
  1492   have Psi_hom: "ring_hom_cring P S Psi"
  1493     by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
  1494   have "Phi p = Phi (finsum P
  1495     (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
  1496     by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
  1497   also have "... = Psi (finsum P
  1498     (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
  1499     by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom] 
  1500       ring_hom_cring.hom_mult [OF Phi_hom]
  1501       ring_hom_cring.hom_pow [OF Phi_hom] Phi
  1502       ring_hom_cring.hom_finsum [OF Psi_hom] 
  1503       ring_hom_cring.hom_mult [OF Psi_hom]
  1504       ring_hom_cring.hom_pow [OF Psi_hom] Psi RS Pi_def comp_def)
  1505   also have "... = Psi p"
  1506     by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
  1507   finally show ?thesis .
  1508 qed
  1509 
  1510 
  1511 theorem (in ring_hom_UP_cring) UP_universal_property:
  1512   "s \<in> carrier S ==>
  1513   EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
  1514     Phi (monom P \<one> 1) = s & 
  1515     (ALL r : carrier R. Phi (monom P r 0) = h r)"
  1516   using eval_monom1                              
  1517   apply (auto intro: eval_ring_hom eval_const eval_extensional)
  1518   apply (rule extensionalityI)                                 
  1519   apply (auto intro: UP_hom_unique)                            
  1520   done                                                         
  1521 
  1522 subsection {* Sample application of evaluation homomorphism *}
  1523 
  1524 lemma ring_hom_UP_cringI:
  1525   assumes "cring R"
  1526     and "cring S"
  1527     and "h \<in> ring_hom R S"
  1528   shows "ring_hom_UP_cring R S h"
  1529   by (fast intro: ring_hom_UP_cring.intro ring_hom_cring_axioms.intro
  1530     cring.axioms prems)
  1531 
  1532 constdefs
  1533   INTEG :: "int ring"
  1534   "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
  1535 
  1536 lemma cring_INTEG:
  1537   "cring INTEG"
  1538   by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
  1539     zadd_zminus_inverse2 zadd_zmult_distrib)
  1540 
  1541 lemma INTEG_id:
  1542   "ring_hom_UP_cring INTEG INTEG id"
  1543   by (fast intro: ring_hom_UP_cringI cring_INTEG id_ring_hom)
  1544 
  1545 text {*
  1546   An instantiation mechanism would now import all theorems and lemmas
  1547   valid in the context of homomorphisms between @{term INTEG} and @{term
  1548   "UP INTEG"}.  *}
  1549 
  1550 lemma INTEG_closed [intro, simp]:
  1551   "z \<in> carrier INTEG"
  1552   by (unfold INTEG_def) simp
  1553 
  1554 lemma INTEG_mult [simp]:
  1555   "mult INTEG z w = z * w"
  1556   by (unfold INTEG_def) simp
  1557 
  1558 lemma INTEG_pow [simp]:
  1559   "pow INTEG z n = z ^ n"
  1560   by (induct n) (simp_all add: INTEG_def nat_pow_def)
  1561 
  1562 lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500"
  1563   by (simp add: ring_hom_UP_cring.eval_monom [OF INTEG_id])
  1564 
  1565 -- {* Calculates @{term "x = 500"} *}
  1566 
  1567 end