src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 60533 1e7ccd864b62 parent 59867 58043346ca64 child 60537 5398aa5a4df9
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 16:23:56 2015 +0200
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 16:31:44 2015 +0200
1.3 @@ -2,13 +2,13 @@
1.4      Author:     Amine Chaieb
1.5  *)
1.6
1.7 -section {* Implementation and verification of multivariate polynomials *}
1.8 +section \<open>Implementation and verification of multivariate polynomials\<close>
1.9
1.10  theory Reflected_Multivariate_Polynomial
1.11  imports Complex_Main Rat_Pair Polynomial_List
1.12  begin
1.13
1.14 -subsection{* Datatype of polynomial expressions *}
1.15 +subsection\<open>Datatype of polynomial expressions\<close>
1.16
1.17  datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly
1.18    | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
1.19 @@ -17,7 +17,7 @@
1.20  abbreviation poly_p :: "int \<Rightarrow> poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \<equiv> C (i)\<^sub>N"
1.21
1.22
1.23 -subsection{* Boundedness, substitution and all that *}
1.24 +subsection\<open>Boundedness, substitution and all that\<close>
1.25
1.26  primrec polysize:: "poly \<Rightarrow> nat"
1.27  where
1.28 @@ -30,7 +30,7 @@
1.29  | "polysize (Pw p n) = 1 + polysize p"
1.30  | "polysize (CN c n p) = 4 + polysize c + polysize p"
1.31
1.32 -primrec polybound0:: "poly \<Rightarrow> bool" -- {* a poly is INDEPENDENT of Bound 0 *}
1.33 +primrec polybound0:: "poly \<Rightarrow> bool" -- \<open>a poly is INDEPENDENT of Bound 0\<close>
1.34  where
1.35    "polybound0 (C c) \<longleftrightarrow> True"
1.36  | "polybound0 (Bound n) \<longleftrightarrow> n > 0"
1.37 @@ -41,7 +41,7 @@
1.38  | "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p"
1.39  | "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p"
1.40
1.41 -primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" -- {* substitute a poly into a poly for Bound 0 *}
1.42 +primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" -- \<open>substitute a poly into a poly for Bound 0\<close>
1.43  where
1.44    "polysubst0 t (C c) = C c"
1.45  | "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)"
1.46 @@ -66,7 +66,7 @@
1.47  | "decrpoly a = a"
1.48
1.49
1.50 -subsection{* Degrees and heads and coefficients *}
1.51 +subsection\<open>Degrees and heads and coefficients\<close>
1.52
1.53  fun degree :: "poly \<Rightarrow> nat"
1.54  where
1.55 @@ -110,7 +110,7 @@
1.56  | "headconst (C n) = n"
1.57
1.58
1.59 -subsection{* Operations for normalization *}
1.60 +subsection\<open>Operations for normalization\<close>
1.61
1.62  declare if_cong[fundef_cong del]
1.63  declare let_cong[fundef_cong del]
1.64 @@ -195,7 +195,7 @@
1.65       in if h = 0\<^sub>N then (p, False) else (C (Ninv h) *\<^sub>p p, 0>\<^sub>N h))"
1.66
1.67
1.68 -subsection {* Pseudo-division *}
1.69 +subsection \<open>Pseudo-division\<close>
1.70
1.71  definition shift1 :: "poly \<Rightarrow> poly"
1.72    where "shift1 p = CN 0\<^sub>p 0 p"
1.73 @@ -233,7 +233,7 @@
1.74  | "poly_deriv p = 0\<^sub>p"
1.75
1.76
1.77 -subsection{* Semantics of the polynomial representation *}
1.78 +subsection\<open>Semantics of the polynomial representation\<close>
1.79
1.80  primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
1.81  where
1.82 @@ -259,7 +259,7 @@
1.83  lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat
1.84
1.85
1.86 -subsection {* Normal form and normalization *}
1.87 +subsection \<open>Normal form and normalization\<close>
1.88
1.89  fun isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
1.90  where
1.91 @@ -273,7 +273,7 @@
1.92  definition isnpoly :: "poly \<Rightarrow> bool"
1.93    where "isnpoly p = isnpolyh p 0"
1.94
1.95 -text{* polyadd preserves normal forms *}
1.97
1.98  lemma polyadd_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)"
1.99  proof (induct p q arbitrary: n0 n1 rule: polyadd.induct)
1.100 @@ -380,7 +380,7 @@
1.101  lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)"
1.102    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
1.103
1.104 -text{* The degree of addition and other general lemmas needed for the normal form of polymul *}
1.105 +text\<open>The degree of addition and other general lemmas needed for the normal form of polymul\<close>
1.106
1.108    assumes "isnpolyh p n0"
1.109 @@ -720,7 +720,7 @@
1.110  qed
1.111
1.112
1.113 -text{* polyneg is a negation and preserves normal forms *}
1.114 +text\<open>polyneg is a negation and preserves normal forms\<close>
1.115
1.116  lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
1.117    by (induct p rule: polyneg.induct) auto
1.118 @@ -738,7 +738,7 @@
1.119    using isnpoly_def polyneg_normh by simp
1.120
1.121
1.122 -text{* polysub is a substraction and preserves normal forms *}
1.123 +text\<open>polysub is a substraction and preserves normal forms\<close>
1.124
1.125  lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p - Ipoly bs q"
1.127 @@ -762,7 +762,7 @@
1.128    by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
1.129      (auto simp: Nsub0[simplified Nsub_def] Let_def)
1.130
1.131 -text{* polypow is a power function and preserves normal forms *}
1.132 +text\<open>polypow is a power function and preserves normal forms\<close>
1.133
1.134  lemma polypow[simp]:
1.135    "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
1.136 @@ -830,7 +830,7 @@
1.137    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
1.138    by (simp add: polypow_normh isnpoly_def)
1.139
1.140 -text{* Finally the whole normalization *}
1.141 +text\<open>Finally the whole normalization\<close>
1.142
1.143  lemma polynate [simp]:
1.144    "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
1.145 @@ -843,7 +843,7 @@
1.148
1.149 -text{* shift1 *}
1.150 +text\<open>shift1\<close>
1.151
1.152
1.153  lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
1.154 @@ -905,7 +905,7 @@
1.155    using assms by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)
1.156
1.157
1.158 -subsection {* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
1.159 +subsection \<open>Miscellaneous lemmas about indexes, decrementation, substitution  etc ...\<close>
1.160
1.161  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
1.162  proof (induct p arbitrary: n rule: poly.induct, auto)
1.163 @@ -913,7 +913,7 @@
1.164    then have "n = Suc (n - 1)"
1.165      by simp
1.166    then have "isnpolyh p (Suc (n - 1))"
1.167 -    using `isnpolyh p n` by simp
1.168 +    using \<open>isnpolyh p n\<close> by simp
1.169    with goal1(2) show ?case
1.170      by simp
1.171  qed
1.172 @@ -1078,7 +1078,7 @@
1.173    using wf_bs_polyadd wf_bs_polyneg by blast
1.174
1.175
1.176 -subsection {* Canonicity of polynomial representation, see lemma isnpolyh_unique *}
1.177 +subsection \<open>Canonicity of polynomial representation, see lemma isnpolyh_unique\<close>
1.178
1.179  definition "polypoly bs p = map (Ipoly bs) (coefficients p)"
1.180  definition "polypoly' bs p = map (Ipoly bs \<circ> decrpoly) (coefficients p)"
1.181 @@ -1165,7 +1165,7 @@
1.182    using nq eq
1.183  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
1.184    case less
1.185 -  note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)`
1.186 +  note np = \<open>isnpolyh p n0\<close> and zp = \<open>\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)\<close>
1.187    {
1.188      assume nz: "maxindex p = 0"
1.189      then obtain c where "p = C c"
1.190 @@ -1254,7 +1254,7 @@
1.191  qed
1.192
1.193
1.194 -text{* consequences of unicity on the algorithms for polynomial normalization *}
1.195 +text\<open>consequences of unicity on the algorithms for polynomial normalization\<close>
1.196
1.198    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.199 @@ -1328,7 +1328,7 @@
1.200    unfolding poly_nate_polypoly' by auto
1.201
1.202
1.203 -subsection{* heads, degrees and all that *}
1.204 +subsection\<open>heads, degrees and all that\<close>
1.205
1.206  lemma degree_eq_degreen0: "degree p = degreen p 0"
1.207    by (induct p rule: degree.induct) simp_all
1.208 @@ -1647,7 +1647,7 @@
1.209    by (induct p arbitrary: n rule: degree.induct) auto
1.210
1.211
1.212 -subsection {* Correctness of polynomial pseudo division *}
1.213 +subsection \<open>Correctness of polynomial pseudo division\<close>
1.214
1.215  lemma polydivide_aux_properties:
1.216    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.217 @@ -1668,7 +1668,7 @@
1.218    let ?p' = "funpow (degree s - n) shift1 p"
1.219    let ?xdn = "funpow (degree s - n) shift1 (1)\<^sub>p"
1.220    let ?akk' = "a ^\<^sub>p (k' - k)"
1.221 -  note ns = `isnpolyh s n1`
1.222 +  note ns = \<open>isnpolyh s n1\<close>
1.223    from np have np0: "isnpolyh p 0"
1.224      using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp
1.225    have np': "isnpolyh ?p' 0"
1.226 @@ -1973,7 +1973,7 @@
1.227  qed
1.228
1.229
1.230 -subsection {* More about polypoly and pnormal etc *}
1.231 +subsection \<open>More about polypoly and pnormal etc\<close>
1.232
1.233  definition "isnonconstant p \<longleftrightarrow> \<not> isconstant p"
1.234
1.235 @@ -2071,7 +2071,7 @@
1.236  qed
1.237
1.238
1.239 -section {* Swaps ; Division by a certain variable *}
1.240 +section \<open>Swaps ; Division by a certain variable\<close>
1.241
1.242  primrec swap :: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly"
1.243  where
```