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.96 +text\<open>polyadd preserves normal forms\<close>
    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.107  lemma polyadd_different_degreen:
   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.126    by (simp add: polysub_def)
   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.146       (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
   1.147        simp_all add: isnpoly_def)
   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.197  lemma polyadd_commute:
   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