src/HOL/Algebra/UnivPoly.thy
 changeset 61382 efac889fccbc parent 61169 4de9ff3ea29a child 61384 9f5145281888
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sat Oct 10 16:21:34 2015 +0200
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sat Oct 10 16:26:23 2015 +0200
1.3 @@ -9,9 +9,9 @@
1.4  imports Module RingHom
1.5  begin
1.6
1.7 -section {* Univariate Polynomials *}
1.8 +section \<open>Univariate Polynomials\<close>
1.9
1.10 -text {*
1.11 +text \<open>
1.12    Polynomials are formalised as modules with additional operations for
1.13    extracting coefficients from polynomials and for obtaining monomials
1.14    from coefficients and exponents (record @{text "up_ring"}).  The
1.15 @@ -21,14 +21,14 @@
1.16    formalisation of polynomials in the PhD thesis @{cite "Ballarin:1999"},
1.17    which was implemented with axiomatic type classes.  This was later
1.18    ported to Locales.
1.19 -*}
1.20 +\<close>
1.21
1.22
1.23 -subsection {* The Constructor for Univariate Polynomials *}
1.24 +subsection \<open>The Constructor for Univariate Polynomials\<close>
1.25
1.26 -text {*
1.27 +text \<open>
1.28    Functions with finite support.
1.29 -*}
1.30 +\<close>
1.31
1.32  locale bound =
1.33    fixes z :: 'a
1.34 @@ -67,9 +67,9 @@
1.35     monom = (%a:carrier R. %n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
1.36     coeff = (%p:up R. %n. p n)\<rparr>"
1.37
1.38 -text {*
1.39 +text \<open>
1.40    Properties of the set of polynomials @{term up}.
1.41 -*}
1.42 +\<close>
1.43
1.44  lemma mem_upI [intro]:
1.45    "[| !!n. f n \<in> carrier R; EX n. bound (zero R) n f |] ==> f \<in> up R"
1.46 @@ -168,7 +168,7 @@
1.47  end
1.48
1.49
1.50 -subsection {* Effect of Operations on Coefficients *}
1.51 +subsection \<open>Effect of Operations on Coefficients\<close>
1.52
1.53  locale UP =
1.54    fixes R (structure) and P (structure)
1.55 @@ -189,7 +189,7 @@
1.56  context UP
1.57  begin
1.58
1.59 -text {*Temporarily declare @{thm P_def} as simp rule.*}
1.60 +text \<open>Temporarily declare @{thm P_def} as simp rule.\<close>
1.61
1.62  declare P_def [simp]
1.63
1.64 @@ -240,12 +240,12 @@
1.65  end
1.66
1.67
1.68 -subsection {* Polynomials Form a Ring. *}
1.69 +subsection \<open>Polynomials Form a Ring.\<close>
1.70
1.71  context UP_ring
1.72  begin
1.73
1.74 -text {* Operations are closed over @{term P}. *}
1.75 +text \<open>Operations are closed over @{term P}.\<close>
1.76
1.77  lemma UP_mult_closed [simp]:
1.78    "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P" by (simp add: UP_def up_mult_closed)
1.79 @@ -269,7 +269,7 @@
1.80
1.81  declare (in UP) P_def [simp del]
1.82
1.83 -text {* Algebraic ring properties *}
1.84 +text \<open>Algebraic ring properties\<close>
1.85
1.86  context UP_ring
1.87  begin
1.88 @@ -398,7 +398,7 @@
1.89  end
1.90
1.91
1.92 -subsection {* Polynomials Form a Commutative Ring. *}
1.93 +subsection \<open>Polynomials Form a Commutative Ring.\<close>
1.94
1.95  context UP_cring
1.96  begin
1.97 @@ -428,7 +428,7 @@
1.98  qed (simp_all add: R1 R2)
1.99
1.100
1.101 -subsection {*Polynomials over a commutative ring for a commutative ring*}
1.102 +subsection \<open>Polynomials over a commutative ring for a commutative ring\<close>
1.103
1.104  theorem UP_cring:
1.105    "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
1.106 @@ -461,7 +461,7 @@
1.107  sublocale UP_cring < P: cring P using UP_cring .
1.108
1.109
1.110 -subsection {* Polynomials Form an Algebra *}
1.111 +subsection \<open>Polynomials Form an Algebra\<close>
1.112
1.113  context UP_ring
1.114  begin
1.115 @@ -496,9 +496,9 @@
1.116
1.117  end
1.118
1.119 -text {*
1.120 +text \<open>
1.121    Interpretation of lemmas from @{term algebra}.
1.122 -*}
1.123 +\<close>
1.124
1.125  lemma (in cring) cring:
1.126    "cring R" ..
1.127 @@ -510,7 +510,7 @@
1.128  sublocale UP_cring < algebra R P using UP_algebra .
1.129
1.130
1.131 -subsection {* Further Lemmas Involving Monomials *}
1.132 +subsection \<open>Further Lemmas Involving Monomials\<close>
1.133
1.134  context UP_ring
1.135  begin
1.136 @@ -637,8 +637,8 @@
1.137    }
1.138  qed
1.139
1.140 -text{*The following corollary follows from lemmas @{thm "monom_one_Suc"}
1.141 -  and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
1.142 +text\<open>The following corollary follows from lemmas @{thm "monom_one_Suc"}
1.143 +  and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}\<close>
1.144
1.145  corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
1.146    unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..
1.147 @@ -709,7 +709,7 @@
1.148  end
1.149
1.150
1.151 -subsection {* The Degree Function *}
1.152 +subsection \<open>The Degree Function\<close>
1.153
1.154  definition
1.155    deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
1.156 @@ -743,19 +743,19 @@
1.157    assumes "deg R p < m" and "p \<in> carrier P"
1.158    shows "coeff P p m = \<zero>"
1.159  proof -
1.160 -  from p \<in> carrier P obtain n where "bound \<zero> n (coeff P p)"
1.161 +  from \<open>p \<in> carrier P\<close> obtain n where "bound \<zero> n (coeff P p)"
1.162      by (auto simp add: UP_def P_def)
1.163    then have "bound \<zero> (deg R p) (coeff P p)"
1.164      by (auto simp: deg_def P_def dest: LeastI)
1.165 -  from this and deg R p < m show ?thesis ..
1.166 +  from this and \<open>deg R p < m\<close> show ?thesis ..
1.167  qed
1.168
1.169  lemma deg_belowI:
1.170    assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
1.171      and R: "p \<in> carrier P"
1.172    shows "n <= deg R p"
1.173 --- {* Logically, this is a slightly stronger version of
1.174 -   @{thm [source] deg_aboveD} *}
1.175 +-- \<open>Logically, this is a slightly stronger version of
1.176 +   @{thm [source] deg_aboveD}\<close>
1.177  proof (cases "n=0")
1.178    case True then show ?thesis by simp
1.179  next
1.180 @@ -814,7 +814,7 @@
1.181        !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
1.182  by (fast intro: le_antisym deg_aboveI deg_belowI)
1.183
1.184 -text {* Degree and polynomial operations *}
1.185 +text \<open>Degree and polynomial operations\<close>
1.186
1.187  lemma deg_add [simp]:
1.188    "p \<in> carrier P \<Longrightarrow> q \<in> carrier P \<Longrightarrow>
1.189 @@ -863,8 +863,8 @@
1.190        inj_on_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R)
1.191  qed
1.192
1.193 -text{*The following lemma is later \emph{overwritten} by the most
1.194 -  specific one for domains, @{text deg_smult}.*}
1.195 +text\<open>The following lemma is later \emph{overwritten} by the most
1.196 +  specific one for domains, @{text deg_smult}.\<close>
1.197
1.198  lemma deg_smult_ring [simp]:
1.199    "[| a \<in> carrier R; p \<in> carrier P |] ==>
1.200 @@ -949,7 +949,7 @@
1.201
1.202  end
1.203
1.204 -text{*The following lemmas also can be lifted to @{term UP_ring}.*}
1.205 +text\<open>The following lemmas also can be lifted to @{term UP_ring}.\<close>
1.206
1.207  context UP_ring
1.208  begin
1.209 @@ -1013,7 +1013,7 @@
1.210  end
1.211
1.212
1.213 -subsection {* Polynomials over Integral Domains *}
1.214 +subsection \<open>Polynomials over Integral Domains\<close>
1.215
1.216  lemma domainI:
1.217    assumes cring: "cring R"
1.218 @@ -1071,15 +1071,15 @@
1.219
1.220  end
1.221
1.222 -text {*
1.223 +text \<open>
1.224    Interpretation of theorems from @{term domain}.
1.225 -*}
1.226 +\<close>
1.227
1.228  sublocale UP_domain < "domain" P
1.229    by intro_locales (rule domain.axioms UP_domain)+
1.230
1.231
1.232 -subsection {* The Evaluation Homomorphism and Universal Property*}
1.233 +subsection \<open>The Evaluation Homomorphism and Universal Property\<close>
1.234
1.235  (* alternative congruence rule (possibly more efficient)
1.236  lemma (in abelian_monoid) finsum_cong2:
1.237 @@ -1192,7 +1192,7 @@
1.238
1.239  end
1.240
1.241 -text {* The universal property of the polynomial ring *}
1.242 +text \<open>The universal property of the polynomial ring\<close>
1.243
1.244  locale UP_pre_univ_prop = ring_hom_cring + UP_cring
1.245
1.246 @@ -1203,9 +1203,9 @@
1.247    assumes indet_img_carrier [simp, intro]: "s \<in> carrier S"
1.248    defines Eval_def: "Eval == eval R S h s"
1.249
1.250 -text{*JE: I have moved the following lemma from Ring.thy and lifted then to the locale @{term ring_hom_ring} from @{term ring_hom_cring}.*}
1.251 -text{*JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so
1.252 -  maybe it is not that necessary.*}
1.253 +text\<open>JE: I have moved the following lemma from Ring.thy and lifted then to the locale @{term ring_hom_ring} from @{term ring_hom_cring}.\<close>
1.254 +text\<open>JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so
1.255 +  maybe it is not that necessary.\<close>
1.256
1.257  lemma (in ring_hom_ring) hom_finsum [simp]:
1.258    "f \<in> A -> carrier R ==>
1.259 @@ -1296,18 +1296,18 @@
1.260    qed
1.261  qed
1.262
1.263 -text {*
1.264 +text \<open>
1.265    The following lemma could be proved in @{text UP_cring} with the additional
1.266 -  assumption that @{text h} is closed. *}
1.267 +  assumption that @{text h} is closed.\<close>
1.268
1.269  lemma (in UP_pre_univ_prop) eval_const:
1.270    "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
1.271    by (simp only: eval_on_carrier monom_closed) simp
1.272
1.273 -text {* Further properties of the evaluation homomorphism. *}
1.274 +text \<open>Further properties of the evaluation homomorphism.\<close>
1.275
1.276 -text {* The following proof is complicated by the fact that in arbitrary
1.277 -  rings one might have @{term "one R = zero R"}. *}
1.278 +text \<open>The following proof is complicated by the fact that in arbitrary
1.279 +  rings one might have @{term "one R = zero R"}.\<close>
1.280
1.281  (* TODO: simplify by cases "one R = zero R" *)
1.282
1.283 @@ -1336,7 +1336,7 @@
1.284
1.285  end
1.286
1.287 -text {* Interpretation of ring homomorphism lemmas. *}
1.288 +text \<open>Interpretation of ring homomorphism lemmas.\<close>
1.289
1.290  sublocale UP_univ_prop < ring_hom_cring P S Eval
1.291    unfolding Eval_def
1.292 @@ -1442,7 +1442,7 @@
1.293
1.294  end
1.295
1.296 -text{*JE: The following lemma was added by me; it might be even lifted to a simpler locale*}
1.297 +text\<open>JE: The following lemma was added by me; it might be even lifted to a simpler locale\<close>
1.298
1.299  context monoid
1.300  begin
1.301 @@ -1461,7 +1461,7 @@
1.302    using lcoeff_nonzero [OF p_not_zero p_in_R] .
1.303
1.304
1.305 -subsection{*The long division algorithm: some previous facts.*}
1.306 +subsection\<open>The long division algorithm: some previous facts.\<close>
1.307
1.308  lemma coeff_minus [simp]:
1.309    assumes p: "p \<in> carrier P" and q: "q \<in> carrier P" shows "coeff P (p \<ominus>\<^bsub>P\<^esub> q) n = coeff P p n \<ominus> coeff P q n"
1.310 @@ -1538,7 +1538,7 @@
1.311  end
1.312
1.313
1.314 -subsection {* The long division proof for commutative rings *}
1.315 +subsection \<open>The long division proof for commutative rings\<close>
1.316
1.317  context UP_cring
1.318  begin
1.319 @@ -1547,7 +1547,7 @@
1.320    shows "\<exists> x y z. Pred x y z"
1.321    using exist by blast
1.322
1.323 -text {* Jacobson's Theorem 2.14 *}
1.324 +text \<open>Jacobson's Theorem 2.14\<close>
1.325
1.326  lemma long_div_theorem:
1.327    assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
1.328 @@ -1648,7 +1648,7 @@
1.329  end
1.330
1.331
1.332 -text {*The remainder theorem as corollary of the long division theorem.*}
1.333 +text \<open>The remainder theorem as corollary of the long division theorem.\<close>
1.334
1.335  context UP_cring
1.336  begin
1.337 @@ -1797,7 +1797,7 @@
1.338  end
1.339
1.340
1.341 -subsection {* Sample Application of Evaluation Homomorphism *}
1.342 +subsection \<open>Sample Application of Evaluation Homomorphism\<close>
1.343
1.344  lemma UP_pre_univ_propI:
1.345    assumes "cring R"
1.346 @@ -1820,11 +1820,11 @@
1.347    "UP_pre_univ_prop INTEG INTEG id"
1.348    by (fast intro: UP_pre_univ_propI INTEG_cring id_ring_hom)
1.349
1.350 -text {*
1.351 +text \<open>
1.352    Interpretation now enables to import all theorems and lemmas
1.353    valid in the context of homomorphisms between @{term INTEG} and @{term
1.354    "UP INTEG"} globally.
1.355 -*}
1.356 +\<close>
1.357
1.358  interpretation INTEG: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
1.359    using INTEG_id_eval by simp_all