author wenzelm Sat Mar 08 23:03:15 2014 +0100 (2014-03-08) changeset 56000 899ad5a3ad00 parent 55999 6477fc70cfa0 child 56001 2df1e7bca361
tuned proofs;
```     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.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.217 +
1.218  lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j"
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.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.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.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.395
1.396 @@ -738,7 +753,7 @@
1.398    assumes np: "isnpolyh p n"
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.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.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.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.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.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.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.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.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.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.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"
```