src/HOL/Algebra/UnivPoly.thy
changeset 29237 e90d9d51106b
parent 28823 dcbef866c9e2
child 29240 bb81c3709fb6
equal deleted inserted replaced
29236:51526dd8da8e 29237:e90d9d51106b
     1 (*
     1 (*
     2   Title:     HOL/Algebra/UnivPoly.thy
     2   Title:     HOL/Algebra/UnivPoly.thy
     3   Id:        $Id$
       
     4   Author:    Clemens Ballarin, started 9 December 1996
     3   Author:    Clemens Ballarin, started 9 December 1996
     5   Copyright: Clemens Ballarin
     4   Copyright: Clemens Ballarin
     6 
     5 
     7 Contributions, in particular on long division, by Jesus Aransay.
     6 Contributions, in particular on long division, by Jesus Aransay.
     8 *)
     7 *)
   178 
   177 
   179 locale UP_ring = UP + ring R
   178 locale UP_ring = UP + ring R
   180 
   179 
   181 locale UP_cring = UP + cring R
   180 locale UP_cring = UP + cring R
   182 
   181 
   183 interpretation UP_cring < UP_ring
   182 sublocale UP_cring < UP_ring
   184   by (rule P_def) intro_locales
   183   by (rule P_def) intro_locales
   185 
   184 
   186 locale UP_domain = UP + "domain" R
   185 locale UP_domain = UP + "domain" R
   187 
   186 
   188 interpretation UP_domain < UP_cring
   187 sublocale UP_domain < UP_cring
   189   by (rule P_def) intro_locales
   188   by (rule P_def) intro_locales
   190 
   189 
   191 context UP
   190 context UP
   192 begin
   191 begin
   193 
   192 
   456   finally show ?thesis .
   455   finally show ?thesis .
   457 qed
   456 qed
   458 
   457 
   459 end
   458 end
   460 
   459 
   461 interpretation UP_ring < ring P using UP_ring .
   460 sublocale UP_ring < ring P using UP_ring .
   462 interpretation UP_cring < cring P using UP_cring .
   461 sublocale UP_cring < cring P using UP_cring .
   463 
   462 
   464 
   463 
   465 subsection {* Polynomials Form an Algebra *}
   464 subsection {* Polynomials Form an Algebra *}
   466 
   465 
   467 context UP_ring
   466 context UP_ring
   506 
   505 
   507 lemma (in UP_cring) UP_algebra:
   506 lemma (in UP_cring) UP_algebra:
   508   "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
   507   "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
   509     UP_smult_assoc1 UP_smult_assoc2)
   508     UP_smult_assoc1 UP_smult_assoc2)
   510 
   509 
   511 interpretation UP_cring < algebra R P using UP_algebra .
   510 sublocale UP_cring < algebra R P using UP_algebra .
   512 
   511 
   513 
   512 
   514 subsection {* Further Lemmas Involving Monomials *}
   513 subsection {* Further Lemmas Involving Monomials *}
   515 
   514 
   516 context UP_ring
   515 context UP_ring
  1083 
  1082 
  1084 text {*
  1083 text {*
  1085   Interpretation of theorems from @{term domain}.
  1084   Interpretation of theorems from @{term domain}.
  1086 *}
  1085 *}
  1087 
  1086 
  1088 interpretation UP_domain < "domain" P
  1087 sublocale UP_domain < "domain" P
  1089   by intro_locales (rule domain.axioms UP_domain)+
  1088   by intro_locales (rule domain.axioms UP_domain)+
  1090 
  1089 
  1091 
  1090 
  1092 subsection {* The Evaluation Homomorphism and Universal Property*}
  1091 subsection {* The Evaluation Homomorphism and Universal Property*}
  1093 
  1092 
  1348 
  1347 
  1349 end
  1348 end
  1350 
  1349 
  1351 text {* Interpretation of ring homomorphism lemmas. *}
  1350 text {* Interpretation of ring homomorphism lemmas. *}
  1352 
  1351 
  1353 interpretation UP_univ_prop < ring_hom_cring P S Eval
  1352 sublocale UP_univ_prop < ring_hom_cring P S Eval
  1354   apply (unfold Eval_def)
  1353   apply (unfold Eval_def)
  1355   apply intro_locales
  1354   apply intro_locales
  1356   apply (rule ring_hom_cring.axioms)
  1355   apply (rule ring_hom_cring.axioms)
  1357   apply (rule ring_hom_cring.intro)
  1356   apply (rule ring_hom_cring.intro)
  1358   apply unfold_locales
  1357   apply unfold_locales
  1389 
  1388 
  1390 lemma (in UP_pre_univ_prop) eval_monom:
  1389 lemma (in UP_pre_univ_prop) eval_monom:
  1391   assumes R: "r \<in> carrier R" and S: "s \<in> carrier S"
  1390   assumes R: "r \<in> carrier R" and S: "s \<in> carrier S"
  1392   shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
  1391   shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
  1393 proof -
  1392 proof -
  1394   interpret UP_univ_prop [R S h P s _]
  1393   interpret UP_univ_prop R S h P s "eval R S h s"
  1395     using UP_pre_univ_prop_axioms P_def R S
  1394     using UP_pre_univ_prop_axioms P_def R S
  1396     by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
  1395     by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
  1397   from R
  1396   from R
  1398   show ?thesis by (rule Eval_monom)
  1397   show ?thesis by (rule Eval_monom)
  1399 qed
  1398 qed
  1426   assumes Psi: "Psi (monom P \<one> (Suc 0)) = s"
  1425   assumes Psi: "Psi (monom P \<one> (Suc 0)) = s"
  1427       "!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r"
  1426       "!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r"
  1428     and P: "p \<in> carrier P" and S: "s \<in> carrier S"
  1427     and P: "p \<in> carrier P" and S: "s \<in> carrier S"
  1429   shows "Phi p = Psi p"
  1428   shows "Phi p = Psi p"
  1430 proof -
  1429 proof -
  1431   interpret ring_hom_cring [P S Phi] by fact
  1430   interpret ring_hom_cring P S Phi by fact
  1432   interpret ring_hom_cring [P S Psi] by fact
  1431   interpret ring_hom_cring P S Psi by fact
  1433   have "Phi p =
  1432   have "Phi p =
  1434       Phi (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)"
  1433       Phi (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)"
  1435     by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
  1434     by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
  1436   also
  1435   also
  1437   have "... =
  1436   have "... =
  1770 lemma eval_monom_expr:
  1769 lemma eval_monom_expr:
  1771   assumes a: "a \<in> carrier R"
  1770   assumes a: "a \<in> carrier R"
  1772   shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
  1771   shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
  1773   (is "eval R R id a ?g = _")
  1772   (is "eval R R id a ?g = _")
  1774 proof -
  1773 proof -
  1775   interpret UP_pre_univ_prop [R R id P] proof qed simp
  1774   interpret UP_pre_univ_prop R R id P proof qed simp
  1776   have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
  1775   have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
  1777   interpret ring_hom_cring [P R "eval R R id a"] proof qed (simp add: eval_ring_hom)
  1776   interpret ring_hom_cring P R "eval R R id a" proof qed (simp add: eval_ring_hom)
  1778   have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
  1777   have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
  1779     and mon0_closed: "monom P a 0 \<in> carrier P" 
  1778     and mon0_closed: "monom P a 0 \<in> carrier P" 
  1780     and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
  1779     and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
  1781     using a R.a_inv_closed by auto
  1780     using a R.a_inv_closed by auto
  1782   have "eval R R id a ?g = eval R R id a (monom P \<one> 1) \<ominus> eval R R id a (monom P a 0)"
  1781   have "eval R R id a ?g = eval R R id a (monom P \<one> 1) \<ominus> eval R R id a (monom P a 0)"
  1817   and f_expr: "f = (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r"
  1816   and f_expr: "f = (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r"
  1818   (is "f = ?g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r" is "f = ?gq \<oplus>\<^bsub>P\<^esub> r")
  1817   (is "f = ?g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r" is "f = ?gq \<oplus>\<^bsub>P\<^esub> r")
  1819     and deg_r_0: "deg R r = 0"
  1818     and deg_r_0: "deg R r = 0"
  1820     shows "r = monom P (eval R R id a f) 0"
  1819     shows "r = monom P (eval R R id a f) 0"
  1821 proof -
  1820 proof -
  1822   interpret UP_pre_univ_prop [R R id P] proof qed simp
  1821   interpret UP_pre_univ_prop R R id P proof qed simp
  1823   have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
  1822   have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
  1824     using eval_ring_hom [OF a] by simp
  1823     using eval_ring_hom [OF a] by simp
  1825   have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
  1824   have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
  1826     unfolding f_expr using ring_hom_add [OF eval_ring_hom] by auto
  1825     unfolding f_expr using ring_hom_add [OF eval_ring_hom] by auto
  1827   also have "\<dots> = ((eval R R id a ?g) \<otimes> (eval R R id a q)) \<oplus>\<^bsub>R\<^esub> eval R R id a r"
  1826   also have "\<dots> = ((eval R R id a ?g) \<otimes> (eval R R id a q)) \<oplus>\<^bsub>R\<^esub> eval R R id a r"
  1883   Interpretation now enables to import all theorems and lemmas
  1882   Interpretation now enables to import all theorems and lemmas
  1884   valid in the context of homomorphisms between @{term INTEG} and @{term
  1883   valid in the context of homomorphisms between @{term INTEG} and @{term
  1885   "UP INTEG"} globally.
  1884   "UP INTEG"} globally.
  1886 *}
  1885 *}
  1887 
  1886 
  1888 interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
  1887 interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id
  1889   using INTEG_id_eval by simp_all
  1888   using INTEG_id_eval by simp_all
  1890 
  1889 
  1891 lemma INTEG_closed [intro, simp]:
  1890 lemma INTEG_closed [intro, simp]:
  1892   "z \<in> carrier INTEG"
  1891   "z \<in> carrier INTEG"
  1893   by (unfold INTEG_def) simp
  1892   by (unfold INTEG_def) simp