src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 56000 899ad5a3ad00
parent 54489 03ff4d1e6784
child 56009 dda076a32aea
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Mar 08 22:21:44 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Mar 08 23:03:15 2014 +0100
     1.3 @@ -32,26 +32,27 @@
     1.4  
     1.5  primrec polybound0:: "poly \<Rightarrow> bool" -- {* a poly is INDEPENDENT of Bound 0 *}
     1.6  where
     1.7 -  "polybound0 (C c) = True"
     1.8 -| "polybound0 (Bound n) = (n>0)"
     1.9 -| "polybound0 (Neg a) = polybound0 a"
    1.10 -| "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"
    1.11 -| "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)"
    1.12 -| "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"
    1.13 -| "polybound0 (Pw p n) = (polybound0 p)"
    1.14 -| "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
    1.15 +  "polybound0 (C c) \<longleftrightarrow> True"
    1.16 +| "polybound0 (Bound n) \<longleftrightarrow> n > 0"
    1.17 +| "polybound0 (Neg a) \<longleftrightarrow> polybound0 a"
    1.18 +| "polybound0 (Add a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
    1.19 +| "polybound0 (Sub a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
    1.20 +| "polybound0 (Mul a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
    1.21 +| "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p"
    1.22 +| "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p"
    1.23  
    1.24  primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" -- {* substitute a poly into a poly for Bound 0 *}
    1.25  where
    1.26 -  "polysubst0 t (C c) = (C c)"
    1.27 -| "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
    1.28 +  "polysubst0 t (C c) = C c"
    1.29 +| "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)"
    1.30  | "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
    1.31  | "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
    1.32  | "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)"
    1.33  | "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
    1.34  | "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
    1.35 -| "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
    1.36 -                             else CN (polysubst0 t c) n (polysubst0 t p))"
    1.37 +| "polysubst0 t (CN c n p) =
    1.38 +    (if n = 0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
    1.39 +     else CN (polysubst0 t c) n (polysubst0 t p))"
    1.40  
    1.41  fun decrpoly:: "poly \<Rightarrow> poly"
    1.42  where
    1.43 @@ -80,8 +81,8 @@
    1.44  (* More general notions of degree and head *)
    1.45  fun degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat"
    1.46  where
    1.47 -  "degreen (CN c n p) = (\<lambda>m. if n=m then 1 + degreen p n else 0)"
    1.48 - |"degreen p = (\<lambda>m. 0)"
    1.49 +  "degreen (CN c n p) = (\<lambda>m. if n = m then 1 + degreen p n else 0)"
    1.50 +| "degreen p = (\<lambda>m. 0)"
    1.51  
    1.52  fun headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"
    1.53  where
    1.54 @@ -90,7 +91,7 @@
    1.55  
    1.56  fun coefficients:: "poly \<Rightarrow> poly list"
    1.57  where
    1.58 -  "coefficients (CN c 0 p) = c#(coefficients p)"
    1.59 +  "coefficients (CN c 0 p) = c # coefficients p"
    1.60  | "coefficients p = [p]"
    1.61  
    1.62  fun isconstant:: "poly \<Rightarrow> bool"
    1.63 @@ -116,15 +117,17 @@
    1.64  
    1.65  fun polyadd :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
    1.66  where
    1.67 -  "polyadd (C c) (C c') = C (c+\<^sub>Nc')"
    1.68 +  "polyadd (C c) (C c') = C (c +\<^sub>N c')"
    1.69  | "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'"
    1.70  | "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p"
    1.71  | "polyadd (CN c n p) (CN c' n' p') =
    1.72      (if n < n' then CN (polyadd c (CN c' n' p')) n p
    1.73 -     else if n'<n then CN (polyadd (CN c n p) c') n' p'
    1.74 -     else (let cc' = polyadd c c' ;
    1.75 -               pp' = polyadd p p'
    1.76 -           in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"
    1.77 +     else if n' < n then CN (polyadd (CN c n p) c') n' p'
    1.78 +     else
    1.79 +      let
    1.80 +        cc' = polyadd c c';
    1.81 +        pp' = polyadd p p'
    1.82 +      in if pp' = 0\<^sub>p then cc' else CN cc' n pp')"
    1.83  | "polyadd a b = Add a b"
    1.84  
    1.85  
    1.86 @@ -141,14 +144,13 @@
    1.87  where
    1.88    "polymul (C c) (C c') = C (c*\<^sub>Nc')"
    1.89  | "polymul (C c) (CN c' n' p') =
    1.90 -      (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))"
    1.91 +    (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))"
    1.92  | "polymul (CN c n p) (C c') =
    1.93 -      (if c' = 0\<^sub>N  then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))"
    1.94 +    (if c' = 0\<^sub>N  then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))"
    1.95  | "polymul (CN c n p) (CN c' n' p') =
    1.96 -  (if n<n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p'))
    1.97 -  else if n' < n
    1.98 -  then CN (polymul (CN c n p) c') n' (polymul (CN c n p) p')
    1.99 -  else polyadd (polymul (CN c n p) c') (CN 0\<^sub>p n' (polymul (CN c n p) p')))"
   1.100 +    (if n < n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p'))
   1.101 +     else if n' < n then CN (polymul (CN c n p) c') n' (polymul (CN c n p) p')
   1.102 +     else polyadd (polymul (CN c n p) c') (CN 0\<^sub>p n' (polymul (CN c n p) p')))"
   1.103  | "polymul a b = Mul a b"
   1.104  
   1.105  declare if_cong[fundef_cong]
   1.106 @@ -157,8 +159,12 @@
   1.107  fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
   1.108  where
   1.109    "polypow 0 = (\<lambda>p. (1)\<^sub>p)"
   1.110 -| "polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul q q in
   1.111 -                    if even n then d else polymul p d)"
   1.112 +| "polypow n =
   1.113 +    (\<lambda>p.
   1.114 +      let
   1.115 +        q = polypow (n div 2) p;
   1.116 +        d = polymul q q
   1.117 +      in if even n then d else polymul p d)"
   1.118  
   1.119  abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
   1.120    where "a ^\<^sub>p k \<equiv> polypow k a"
   1.121 @@ -166,11 +172,11 @@
   1.122  function polynate :: "poly \<Rightarrow> poly"
   1.123  where
   1.124    "polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p"
   1.125 -| "polynate (Add p q) = (polynate p +\<^sub>p polynate q)"
   1.126 -| "polynate (Sub p q) = (polynate p -\<^sub>p polynate q)"
   1.127 -| "polynate (Mul p q) = (polynate p *\<^sub>p polynate q)"
   1.128 -| "polynate (Neg p) = (~\<^sub>p (polynate p))"
   1.129 -| "polynate (Pw p n) = ((polynate p) ^\<^sub>p n)"
   1.130 +| "polynate (Add p q) = polynate p +\<^sub>p polynate q"
   1.131 +| "polynate (Sub p q) = polynate p -\<^sub>p polynate q"
   1.132 +| "polynate (Mul p q) = polynate p *\<^sub>p polynate q"
   1.133 +| "polynate (Neg p) = ~\<^sub>p (polynate p)"
   1.134 +| "polynate (Pw p n) = polynate p ^\<^sub>p n"
   1.135  | "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
   1.136  | "polynate (C c) = C (normNum c)"
   1.137  by pat_completeness auto
   1.138 @@ -182,14 +188,17 @@
   1.139  | "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)"
   1.140  | "poly_cmul y p = C y *\<^sub>p p"
   1.141  
   1.142 -definition monic :: "poly \<Rightarrow> (poly \<times> bool)" where
   1.143 -  "monic p \<equiv> (let h = headconst p in if h = 0\<^sub>N then (p,False) else ((C (Ninv h)) *\<^sub>p p, 0>\<^sub>N h))"
   1.144 +definition monic :: "poly \<Rightarrow> (poly \<times> bool)"
   1.145 +where
   1.146 +  "monic p =
   1.147 +    (let h = headconst p
   1.148 +     in if h = 0\<^sub>N then (p, False) else (C (Ninv h) *\<^sub>p p, 0>\<^sub>N h))"
   1.149  
   1.150  
   1.151 -subsection{* Pseudo-division *}
   1.152 +subsection {* Pseudo-division *}
   1.153  
   1.154  definition shift1 :: "poly \<Rightarrow> poly"
   1.155 -  where "shift1 p \<equiv> CN 0\<^sub>p 0 p"
   1.156 +  where "shift1 p = CN 0\<^sub>p 0 p"
   1.157  
   1.158  abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
   1.159    where "funpow \<equiv> compow"
   1.160 @@ -197,17 +206,21 @@
   1.161  partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly"
   1.162  where
   1.163    "polydivide_aux a n p k s =
   1.164 -    (if s = 0\<^sub>p then (k,s)
   1.165 +    (if s = 0\<^sub>p then (k, s)
   1.166       else
   1.167 -      (let b = head s; m = degree s in
   1.168 -        (if m < n then (k,s)
   1.169 -         else
   1.170 -          (let p'= funpow (m - n) shift1 p in
   1.171 -            (if a = b then polydivide_aux a n p k (s -\<^sub>p p')
   1.172 -             else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
   1.173 +      let
   1.174 +        b = head s;
   1.175 +        m = degree s
   1.176 +      in
   1.177 +        if m < n then (k,s)
   1.178 +        else
   1.179 +          let p' = funpow (m - n) shift1 p
   1.180 +          in
   1.181 +            if a = b then polydivide_aux a n p k (s -\<^sub>p p')
   1.182 +            else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))"
   1.183  
   1.184 -definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)"
   1.185 -  where "polydivide s p \<equiv> polydivide_aux (head p) (degree p) p 0 s"
   1.186 +definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> nat \<times> poly"
   1.187 +  where "polydivide s p = polydivide_aux (head p) (degree p) p 0 s"
   1.188  
   1.189  fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly"
   1.190  where
   1.191 @@ -222,22 +235,24 @@
   1.192  
   1.193  subsection{* Semantics of the polynomial representation *}
   1.194  
   1.195 -primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
   1.196 +primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field_inverse_zero,power}"
   1.197 +where
   1.198    "Ipoly bs (C c) = INum c"
   1.199  | "Ipoly bs (Bound n) = bs!n"
   1.200  | "Ipoly bs (Neg a) = - Ipoly bs a"
   1.201  | "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
   1.202  | "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
   1.203  | "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
   1.204 -| "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
   1.205 -| "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
   1.206 +| "Ipoly bs (Pw t n) = Ipoly bs t ^ n"
   1.207 +| "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p"
   1.208  
   1.209 -abbreviation
   1.210 -  Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
   1.211 +abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field_inverse_zero,power}"
   1.212 +    ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
   1.213    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
   1.214  
   1.215  lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i"
   1.216    by (simp add: INum_def)
   1.217 +
   1.218  lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j"
   1.219    by (simp  add: INum_def)
   1.220  
   1.221 @@ -249,19 +264,18 @@
   1.222  fun isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
   1.223  where
   1.224    "isnpolyh (C c) = (\<lambda>k. isnormNum c)"
   1.225 -| "isnpolyh (CN c n p) = (\<lambda>k. n \<ge> k \<and> (isnpolyh c (Suc n)) \<and> (isnpolyh p n) \<and> (p \<noteq> 0\<^sub>p))"
   1.226 +| "isnpolyh (CN c n p) = (\<lambda>k. n \<ge> k \<and> isnpolyh c (Suc n) \<and> isnpolyh p n \<and> p \<noteq> 0\<^sub>p)"
   1.227  | "isnpolyh p = (\<lambda>k. False)"
   1.228  
   1.229 -lemma isnpolyh_mono: "\<lbrakk>n' \<le> n ; isnpolyh p n\<rbrakk> \<Longrightarrow> isnpolyh p n'"
   1.230 +lemma isnpolyh_mono: "n' \<le> n \<Longrightarrow> isnpolyh p n \<Longrightarrow> isnpolyh p n'"
   1.231    by (induct p rule: isnpolyh.induct) auto
   1.232  
   1.233  definition isnpoly :: "poly \<Rightarrow> bool"
   1.234 -  where "isnpoly p \<equiv> isnpolyh p 0"
   1.235 +  where "isnpoly p = isnpolyh p 0"
   1.236  
   1.237  text{* polyadd preserves normal forms *}
   1.238  
   1.239 -lemma polyadd_normh: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk>
   1.240 -      \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)"
   1.241 +lemma polyadd_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)"
   1.242  proof (induct p q arbitrary: n0 n1 rule: polyadd.induct)
   1.243    case (2 ab c' n' p' n0 n1)
   1.244    from 2 have  th1: "isnpolyh (C ab) (Suc n')" by simp
   1.245 @@ -402,7 +416,7 @@
   1.246  qed simp_all
   1.247  
   1.248  lemma polymul_properties:
   1.249 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.250 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.251      and np: "isnpolyh p n0"
   1.252      and nq: "isnpolyh q n1"
   1.253      and m: "m \<le> min n0 n1"
   1.254 @@ -548,23 +562,23 @@
   1.255    by (induct p q rule: polymul.induct) (auto simp add: field_simps)
   1.256  
   1.257  lemma polymul_normh:
   1.258 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.259 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.260    shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
   1.261    using polymul_properties(1) by blast
   1.262  
   1.263  lemma polymul_eq0_iff:
   1.264 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.265 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.266    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p) "
   1.267    using polymul_properties(2) by blast
   1.268  
   1.269  lemma polymul_degreen:  (* FIXME duplicate? *)
   1.270 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.271 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.272    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow>
   1.273      degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 else degreen p m + degreen q m)"
   1.274    using polymul_properties(3) by blast
   1.275  
   1.276  lemma polymul_norm:
   1.277 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.278 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.279    shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul p q)"
   1.280    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
   1.281  
   1.282 @@ -577,12 +591,13 @@
   1.283  lemma monic_eqI:
   1.284    assumes np: "isnpolyh p n0"
   1.285    shows "INum (headconst p) * Ipoly bs (fst (monic p)) =
   1.286 -    (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
   1.287 +    (Ipoly bs p ::'a::{field_char_0,field_inverse_zero, power})"
   1.288    unfolding monic_def Let_def
   1.289  proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
   1.290    let ?h = "headconst p"
   1.291    assume pz: "p \<noteq> 0\<^sub>p"
   1.292 -  { assume hz: "INum ?h = (0::'a)"
   1.293 +  {
   1.294 +    assume hz: "INum ?h = (0::'a)"
   1.295      from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all
   1.296      from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp
   1.297      with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast}
   1.298 @@ -617,13 +632,13 @@
   1.299  lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub p q)"
   1.300    using polyadd_norm polyneg_norm by (simp add: polysub_def)
   1.301  lemma polysub_same_0[simp]:
   1.302 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.303 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.304    shows "isnpolyh p n0 \<Longrightarrow> polysub p p = 0\<^sub>p"
   1.305    unfolding polysub_def split_def fst_conv snd_conv
   1.306    by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def])
   1.307  
   1.308  lemma polysub_0:
   1.309 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.310 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.311    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
   1.312    unfolding polysub_def split_def fst_conv snd_conv
   1.313    by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
   1.314 @@ -631,7 +646,7 @@
   1.315  
   1.316  text{* polypow is a power function and preserves normal forms *}
   1.317  
   1.318 -lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n"
   1.319 +lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0,field_inverse_zero})) ^ n"
   1.320  proof (induct n rule: polypow.induct)
   1.321    case 1
   1.322    thus ?case by simp
   1.323 @@ -642,20 +657,20 @@
   1.324    have "odd (Suc n) \<or> even (Suc n)" by simp
   1.325    moreover
   1.326    { assume odd: "odd (Suc n)"
   1.327 -    have th: "(Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat))))) = Suc n div 2 + Suc n div 2 + 1"
   1.328 +    have th: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1"
   1.329        by arith
   1.330      from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" by (simp add: Let_def)
   1.331      also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)"
   1.332        using "2.hyps" by simp
   1.333      also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
   1.334        by (simp only: power_add power_one_right) simp
   1.335 -    also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat)))))"
   1.336 +    also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
   1.337        by (simp only: th)
   1.338      finally have ?case
   1.339      using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp  }
   1.340    moreover
   1.341    { assume even: "even (Suc n)"
   1.342 -    have th: "(Suc (Suc (0\<Colon>nat))) * (Suc n div Suc (Suc (0\<Colon>nat))) = Suc n div 2 + Suc n div 2"
   1.343 +    have th: "(Suc (Suc 0)) * (Suc n div Suc (Suc 0)) = Suc n div 2 + Suc n div 2"
   1.344        by arith
   1.345      from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def)
   1.346      also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"
   1.347 @@ -665,7 +680,7 @@
   1.348  qed
   1.349  
   1.350  lemma polypow_normh:
   1.351 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.352 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.353    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
   1.354  proof (induct k arbitrary: n rule: polypow.induct)
   1.355    case (2 k n)
   1.356 @@ -678,18 +693,18 @@
   1.357  qed auto
   1.358  
   1.359  lemma polypow_norm:
   1.360 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.361 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.362    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
   1.363    by (simp add: polypow_normh isnpoly_def)
   1.364  
   1.365  text{* Finally the whole normalization *}
   1.366  
   1.367  lemma polynate [simp]:
   1.368 -  "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
   1.369 +  "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field_inverse_zero})"
   1.370    by (induct p rule:polynate.induct) auto
   1.371  
   1.372  lemma polynate_norm[simp]:
   1.373 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.374 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.375    shows "isnpoly (polynate p)"
   1.376    by (induct p rule: polynate.induct)
   1.377       (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
   1.378 @@ -720,7 +735,7 @@
   1.379    using f np by (induct k arbitrary: p) auto
   1.380  
   1.381  lemma funpow_shift1:
   1.382 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) =
   1.383 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
   1.384      Ipoly bs (Mul (Pw (Bound 0) n) p)"
   1.385    by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
   1.386  
   1.387 @@ -728,7 +743,7 @@
   1.388    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   1.389  
   1.390  lemma funpow_shift1_1:
   1.391 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) =
   1.392 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
   1.393      Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
   1.394    by (simp add: funpow_shift1)
   1.395  
   1.396 @@ -738,7 +753,7 @@
   1.397  lemma behead:
   1.398    assumes np: "isnpolyh p n"
   1.399    shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
   1.400 -    (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})"
   1.401 +    (Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})"
   1.402    using np
   1.403  proof (induct p arbitrary: n rule: behead.induct)
   1.404    case (1 c p n) hence pn: "isnpolyh p n" by simp
   1.405 @@ -821,7 +836,7 @@
   1.406  | "maxindex (C x) = 0"
   1.407  
   1.408  definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool"
   1.409 -  where "wf_bs bs p = (length bs \<ge> maxindex p)"
   1.410 +  where "wf_bs bs p \<longleftrightarrow> length bs \<ge> maxindex p"
   1.411  
   1.412  lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall> c \<in> set (coefficients p). wf_bs bs c"
   1.413  proof (induct p rule: coefficients.induct)
   1.414 @@ -843,7 +858,7 @@
   1.415  lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"
   1.416    by (induct p rule: coefficients.induct) auto
   1.417  
   1.418 -lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p"
   1.419 +lemma wf_bs_I: "wf_bs bs p \<Longrightarrow> Ipoly (bs @ bs') p = Ipoly bs p"
   1.420    unfolding wf_bs_def by (induct p) (auto simp add: nth_append)
   1.421  
   1.422  lemma take_maxindex_wf:
   1.423 @@ -989,122 +1004,159 @@
   1.424  
   1.425  lemma isnpolyh_zero_iff:
   1.426    assumes nq: "isnpolyh p n0"
   1.427 -    and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, field_inverse_zero, power})"
   1.428 +    and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field_inverse_zero, power})"
   1.429    shows "p = 0\<^sub>p"
   1.430    using nq eq
   1.431  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
   1.432    case less
   1.433    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.434 -  {assume nz: "maxindex p = 0"
   1.435 -    then obtain c where "p = C c" using np by (cases p) auto
   1.436 -    with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp}
   1.437 +  {
   1.438 +    assume nz: "maxindex p = 0"
   1.439 +    then obtain c where "p = C c"
   1.440 +      using np by (cases p) auto
   1.441 +    with zp np have "p = 0\<^sub>p"
   1.442 +      unfolding wf_bs_def by simp
   1.443 +  }
   1.444    moreover
   1.445 -  {assume nz: "maxindex p \<noteq> 0"
   1.446 +  {
   1.447 +    assume nz: "maxindex p \<noteq> 0"
   1.448      let ?h = "head p"
   1.449      let ?hd = "decrpoly ?h"
   1.450      let ?ihd = "maxindex ?hd"
   1.451 -    from head_isnpolyh[OF np] head_polybound0[OF np] have h:"isnpolyh ?h n0" "polybound0 ?h"
   1.452 +    from head_isnpolyh[OF np] head_polybound0[OF np]
   1.453 +    have h: "isnpolyh ?h n0" "polybound0 ?h"
   1.454        by simp_all
   1.455 -    hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast
   1.456 +    then have nhd: "isnpolyh ?hd (n0 - 1)"
   1.457 +      using decrpoly_normh by blast
   1.458  
   1.459      from maxindex_coefficients[of p] coefficients_head[of p, symmetric]
   1.460 -    have mihn: "maxindex ?h \<le> maxindex p" by auto
   1.461 -    with decr_maxindex[OF h(2)] nz  have ihd_lt_n: "?ihd < maxindex p" by auto
   1.462 -    {fix bs:: "'a list"  assume bs: "wf_bs bs ?hd"
   1.463 +    have mihn: "maxindex ?h \<le> maxindex p"
   1.464 +      by auto
   1.465 +    with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < maxindex p"
   1.466 +      by auto
   1.467 +    {
   1.468 +      fix bs :: "'a list"
   1.469 +      assume bs: "wf_bs bs ?hd"
   1.470        let ?ts = "take ?ihd bs"
   1.471        let ?rs = "drop ?ihd bs"
   1.472 -      have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp
   1.473 -      have bs_ts_eq: "?ts@ ?rs = bs" by simp
   1.474 -      from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp
   1.475 -      from ihd_lt_n have "ALL x. length (x#?ts) \<le> maxindex p" by simp
   1.476 -      with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast
   1.477 -      hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" unfolding wf_bs_def by simp
   1.478 -      with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast
   1.479 -      hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp
   1.480 +      have ts: "wf_bs ?ts ?hd"
   1.481 +        using bs unfolding wf_bs_def by simp
   1.482 +      have bs_ts_eq: "?ts @ ?rs = bs"
   1.483 +        by simp
   1.484 +      from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x # ?ts) ?h"
   1.485 +        by simp
   1.486 +      from ihd_lt_n have "\<forall>x. length (x # ?ts) \<le> maxindex p"
   1.487 +        by simp
   1.488 +      with length_le_list_ex obtain xs where xs: "length ((x # ?ts) @ xs) = maxindex p"
   1.489 +        by blast
   1.490 +      then have "\<forall>x. wf_bs ((x # ?ts) @ xs) p"
   1.491 +        unfolding wf_bs_def by simp
   1.492 +      with zp have "\<forall>x. Ipoly ((x # ?ts) @ xs) p = 0"
   1.493 +        by blast
   1.494 +      then have "\<forall>x. Ipoly (x # (?ts @ xs)) p = 0"
   1.495 +        by simp
   1.496        with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]
   1.497 -      have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
   1.498 -      hence "poly (polypoly' (?ts @ xs) p) = poly []" by auto
   1.499 -      hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
   1.500 +      have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"
   1.501 +        by simp
   1.502 +      then have "poly (polypoly' (?ts @ xs) p) = poly []"
   1.503 +        by auto
   1.504 +      then have "\<forall>c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
   1.505          using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
   1.506        with coefficients_head[of p, symmetric]
   1.507 -      have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
   1.508 -      from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp
   1.509 -      with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" by simp
   1.510 -      with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp }
   1.511 -    then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast
   1.512 -
   1.513 -    from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast
   1.514 -    hence "?h = 0\<^sub>p" by simp
   1.515 -    with head_nz[OF np] have "p = 0\<^sub>p" by simp}
   1.516 -  ultimately show "p = 0\<^sub>p" by blast
   1.517 +      have th0: "Ipoly (?ts @ xs) ?hd = 0"
   1.518 +        by simp
   1.519 +      from bs have wf'': "wf_bs ?ts ?hd"
   1.520 +        unfolding wf_bs_def by simp
   1.521 +      with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0"
   1.522 +        by simp
   1.523 +      with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0"
   1.524 +        by simp
   1.525 +    }
   1.526 +    then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)"
   1.527 +      by blast
   1.528 +    from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p"
   1.529 +      by blast
   1.530 +    then have "?h = 0\<^sub>p" by simp
   1.531 +    with head_nz[OF np] have "p = 0\<^sub>p" by simp
   1.532 +  }
   1.533 +  ultimately show "p = 0\<^sub>p"
   1.534 +    by blast
   1.535  qed
   1.536  
   1.537  lemma isnpolyh_unique:
   1.538 -  assumes np:"isnpolyh p n0"
   1.539 +  assumes np: "isnpolyh p n0"
   1.540      and nq: "isnpolyh q n1"
   1.541 -  shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0, field_inverse_zero, power})) \<longleftrightarrow>  p = q"
   1.542 -proof(auto)
   1.543 -  assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
   1.544 -  hence "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp
   1.545 -  hence "\<forall>bs. wf_bs bs (p -\<^sub>p q) \<longrightarrow> \<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)"
   1.546 +  shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field_inverse_zero,power})) \<longleftrightarrow> p = q"
   1.547 +proof auto
   1.548 +  assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a) = \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
   1.549 +  then have "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)"
   1.550 +    by simp
   1.551 +  then have "\<forall>bs. wf_bs bs (p -\<^sub>p q) \<longrightarrow> \<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)"
   1.552      using wf_bs_polysub[where p=p and q=q] by auto
   1.553 -  with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq]
   1.554 -  show "p = q" by blast
   1.555 +  with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq] show "p = q"
   1.556 +    by blast
   1.557  qed
   1.558  
   1.559  
   1.560  text{* consequences of unicity on the algorithms for polynomial normalization *}
   1.561  
   1.562  lemma polyadd_commute:
   1.563 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.564 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.565      and np: "isnpolyh p n0"
   1.566      and nq: "isnpolyh q n1"
   1.567    shows "p +\<^sub>p q = q +\<^sub>p p"
   1.568 -  using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
   1.569 +  using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]]
   1.570 +  by simp
   1.571  
   1.572 -lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
   1.573 -lemma one_normh: "isnpolyh (1)\<^sub>p n" by simp
   1.574 +lemma zero_normh: "isnpolyh 0\<^sub>p n"
   1.575 +  by simp
   1.576 +
   1.577 +lemma one_normh: "isnpolyh (1)\<^sub>p n"
   1.578 +  by simp
   1.579  
   1.580  lemma polyadd_0[simp]:
   1.581 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.582 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.583      and np: "isnpolyh p n0"
   1.584 -  shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
   1.585 +  shows "p +\<^sub>p 0\<^sub>p = p"
   1.586 +    and "0\<^sub>p +\<^sub>p p = p"
   1.587    using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np]
   1.588      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
   1.589  
   1.590  lemma polymul_1[simp]:
   1.591 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.592 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.593      and np: "isnpolyh p n0"
   1.594 -  shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p"
   1.595 +  shows "p *\<^sub>p (1)\<^sub>p = p"
   1.596 +    and "(1)\<^sub>p *\<^sub>p p = p"
   1.597    using isnpolyh_unique[OF polymul_normh[OF np one_normh] np]
   1.598      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
   1.599  
   1.600  lemma polymul_0[simp]:
   1.601 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.602 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.603      and np: "isnpolyh p n0"
   1.604 -  shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
   1.605 +  shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p"
   1.606 +    and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
   1.607    using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh]
   1.608      isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
   1.609  
   1.610  lemma polymul_commute:
   1.611 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.612 -    and np:"isnpolyh p n0"
   1.613 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.614 +    and np: "isnpolyh p n0"
   1.615      and nq: "isnpolyh q n1"
   1.616    shows "p *\<^sub>p q = q *\<^sub>p p"
   1.617 -  using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{field_char_0, field_inverse_zero, power}"]
   1.618 +  using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a::{field_char_0,field_inverse_zero, power}"]
   1.619    by simp
   1.620  
   1.621  declare polyneg_polyneg [simp]
   1.622  
   1.623  lemma isnpolyh_polynate_id [simp]:
   1.624 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.625 -    and np:"isnpolyh p n0"
   1.626 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.627 +    and np: "isnpolyh p n0"
   1.628    shows "polynate p = p"
   1.629 -  using isnpolyh_unique[where ?'a= "'a::{field_char_0, field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0, field_inverse_zero}"]
   1.630 +  using isnpolyh_unique[where ?'a= "'a::{field_char_0,field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0,field_inverse_zero}"]
   1.631    by simp
   1.632  
   1.633  lemma polynate_idempotent[simp]:
   1.634 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.635 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.636    shows "polynate (polynate p) = polynate p"
   1.637    using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
   1.638  
   1.639 @@ -1112,7 +1164,7 @@
   1.640    unfolding poly_nate_def polypoly'_def ..
   1.641  
   1.642  lemma poly_nate_poly:
   1.643 -  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0, field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   1.644 +  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   1.645    using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
   1.646    unfolding poly_nate_polypoly' by auto
   1.647  
   1.648 @@ -1147,7 +1199,7 @@
   1.649  qed
   1.650  
   1.651  lemma degree_polysub_samehead:
   1.652 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.653 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.654      and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q"
   1.655      and d: "degree p = degree q"
   1.656    shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
   1.657 @@ -1263,7 +1315,7 @@
   1.658    done
   1.659  
   1.660  lemma polymul_head_polyeq:
   1.661 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.662 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.663    shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
   1.664  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   1.665    case (2 c c' n' p' n0 n1)
   1.666 @@ -1345,7 +1397,7 @@
   1.667    by (induct p arbitrary: n0 rule: polyneg.induct) auto
   1.668  
   1.669  lemma degree_polymul:
   1.670 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.671 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.672      and np: "isnpolyh p n0"
   1.673      and nq: "isnpolyh q n1"
   1.674    shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
   1.675 @@ -1361,7 +1413,7 @@
   1.676  subsection {* Correctness of polynomial pseudo division *}
   1.677  
   1.678  lemma polydivide_aux_properties:
   1.679 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.680 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.681      and np: "isnpolyh p n0"
   1.682      and ns: "isnpolyh s n1"
   1.683      and ap: "head p = a"
   1.684 @@ -1438,20 +1490,20 @@
   1.685                polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
   1.686              have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0"
   1.687                by simp
   1.688 -            from asp have "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) =
   1.689 +            from asp have "\<forall> (bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) =
   1.690                Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
   1.691 -            hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
   1.692 +            hence " \<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
   1.693                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
   1.694                by (simp add: field_simps)
   1.695 -            hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.696 +            hence " \<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.697                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) +
   1.698                Ipoly bs p * Ipoly bs q + Ipoly bs r"
   1.699                by (auto simp only: funpow_shift1_1)
   1.700 -            hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.701 +            hence "\<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.702                Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) +
   1.703                Ipoly bs q) + Ipoly bs r"
   1.704                by (simp add: field_simps)
   1.705 -            hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.706 +            hence "\<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.707                Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r)"
   1.708                by simp
   1.709              with isnpolyh_unique[OF nakks' nqr']
   1.710 @@ -1470,10 +1522,10 @@
   1.711          }
   1.712          moreover
   1.713          { assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
   1.714 -          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0, field_inverse_zero}"]
   1.715 -          have " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'"
   1.716 +          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field_inverse_zero}"]
   1.717 +          have " \<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'"
   1.718              by simp
   1.719 -          hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
   1.720 +          hence "\<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
   1.721              using np nxdn
   1.722              apply simp
   1.723              apply (simp only: funpow_shift1_1)
   1.724 @@ -1540,7 +1592,7 @@
   1.725                by auto
   1.726              from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
   1.727              {
   1.728 -              fix bs:: "'a::{field_char_0, field_inverse_zero} list"
   1.729 +              fix bs:: "'a::{field_char_0,field_inverse_zero} list"
   1.730                from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
   1.731                have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)"
   1.732                  by simp
   1.733 @@ -1554,7 +1606,7 @@
   1.734                  Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
   1.735                  by (simp add: field_simps)
   1.736              }
   1.737 -            hence ieq:"\<forall>(bs :: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.738 +            hence ieq:"\<forall>(bs :: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.739                Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
   1.740                by auto
   1.741              let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
   1.742 @@ -1577,7 +1629,7 @@
   1.743          moreover
   1.744          { assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
   1.745            {
   1.746 -            fix bs :: "'a::{field_char_0, field_inverse_zero} list"
   1.747 +            fix bs :: "'a::{field_char_0,field_inverse_zero} list"
   1.748              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
   1.749              have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'"
   1.750                by simp
   1.751 @@ -1586,10 +1638,10 @@
   1.752              hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
   1.753                by simp
   1.754            }
   1.755 -          hence hth: "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) =
   1.756 +          hence hth: "\<forall> (bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) =
   1.757              Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
   1.758            from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
   1.759 -            using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
   1.760 +            using isnpolyh_unique[where ?'a = "'a::{field_char_0,field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
   1.761                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
   1.762                simplified ap] by simp
   1.763            { assume h1: "polydivide_aux a n p k s = (k', r)"
   1.764 @@ -1619,7 +1671,7 @@
   1.765  qed
   1.766  
   1.767  lemma polydivide_properties:
   1.768 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.769 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.770      and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \<noteq> 0\<^sub>p"
   1.771    shows "\<exists>k r. polydivide s p = (k,r) \<and>
   1.772      (\<exists>nr. isnpolyh r nr) \<and> (degree r = 0 \<or> degree r < degree p) \<and>
   1.773 @@ -1631,7 +1683,7 @@
   1.774      by auto
   1.775    then obtain k r where kr: "polydivide s p = (k,r)"
   1.776      by blast
   1.777 -  from trans[OF meta_eq_to_obj_eq[OF polydivide_def[where s="s"and p="p"], symmetric] kr]
   1.778 +  from trans[OF polydivide_def[where s="s"and p="p", symmetric] kr]
   1.779      polydivide_aux_properties[OF np ns trv pnz, where k="0" and k'="k" and r="r"]
   1.780    have "(degree r = 0 \<or> degree r < degree p) \<and>
   1.781      (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> head p ^\<^sub>p k - 0 *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
   1.782 @@ -1647,7 +1699,7 @@
   1.783  
   1.784  subsection{* More about polypoly and pnormal etc *}
   1.785  
   1.786 -definition "isnonconstant p = (\<not> isconstant p)"
   1.787 +definition "isnonconstant p \<longleftrightarrow> \<not> isconstant p"
   1.788  
   1.789  lemma isnonconstant_pnormal_iff:
   1.790    assumes nc: "isnonconstant p"
   1.791 @@ -1768,20 +1820,24 @@
   1.792  lemma swapnorm:
   1.793    assumes nbs: "n < length bs"
   1.794      and mbs: "m < length bs"
   1.795 -  shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) =
   1.796 +  shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field_inverse_zero})) =
   1.797      Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
   1.798    using swap[OF assms] swapnorm_def by simp
   1.799  
   1.800  lemma swapnorm_isnpoly [simp]:
   1.801 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.802 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.803    shows "isnpoly (swapnorm n m p)"
   1.804    unfolding swapnorm_def by simp
   1.805  
   1.806  definition "polydivideby n s p =
   1.807 -  (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp
   1.808 -   in (k, swapnorm 0 n h,swapnorm 0 n r))"
   1.809 +  (let
   1.810 +    ss = swapnorm 0 n s;
   1.811 +    sp = swapnorm 0 n p;
   1.812 +    h = head sp;
   1.813 +    (k, r) = polydivide ss sp
   1.814 +   in (k, swapnorm 0 n h, swapnorm 0 n r))"
   1.815  
   1.816 -lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)"
   1.817 +lemma swap_nz [simp]: "swap n m p = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p"
   1.818    by (induct p) simp_all
   1.819  
   1.820  fun isweaknpoly :: "poly \<Rightarrow> bool"