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