src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 67123 3fe40ff1b921 parent 62390 842917225d56 child 68442 477b3f7067c9
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Dec 03 19:09:42 2017 +0100
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Dec 03 22:28:19 2017 +0100
1.3 @@ -5,7 +5,7 @@
1.4  section \<open>Implementation and verification of multivariate polynomials\<close>
1.5
1.6  theory Reflected_Multivariate_Polynomial
1.7 -imports Complex_Main Rat_Pair Polynomial_List
1.8 +  imports Complex_Main Rat_Pair Polynomial_List
1.9  begin
1.10
1.11  subsection \<open>Datatype of polynomial expressions\<close>
1.12 @@ -20,95 +20,95 @@
1.13  subsection\<open>Boundedness, substitution and all that\<close>
1.14
1.15  primrec polysize:: "poly \<Rightarrow> nat"
1.16 -where
1.17 -  "polysize (C c) = 1"
1.18 -| "polysize (Bound n) = 1"
1.19 -| "polysize (Neg p) = 1 + polysize p"
1.20 -| "polysize (Add p q) = 1 + polysize p + polysize q"
1.21 -| "polysize (Sub p q) = 1 + polysize p + polysize q"
1.22 -| "polysize (Mul p q) = 1 + polysize p + polysize q"
1.23 -| "polysize (Pw p n) = 1 + polysize p"
1.24 -| "polysize (CN c n p) = 4 + polysize c + polysize p"
1.25 +  where
1.26 +    "polysize (C c) = 1"
1.27 +  | "polysize (Bound n) = 1"
1.28 +  | "polysize (Neg p) = 1 + polysize p"
1.29 +  | "polysize (Add p q) = 1 + polysize p + polysize q"
1.30 +  | "polysize (Sub p q) = 1 + polysize p + polysize q"
1.31 +  | "polysize (Mul p q) = 1 + polysize p + polysize q"
1.32 +  | "polysize (Pw p n) = 1 + polysize p"
1.33 +  | "polysize (CN c n p) = 4 + polysize c + polysize p"
1.34
1.35  primrec polybound0:: "poly \<Rightarrow> bool" \<comment> \<open>a poly is INDEPENDENT of Bound 0\<close>
1.36 -where
1.37 -  "polybound0 (C c) \<longleftrightarrow> True"
1.38 -| "polybound0 (Bound n) \<longleftrightarrow> n > 0"
1.39 -| "polybound0 (Neg a) \<longleftrightarrow> polybound0 a"
1.40 -| "polybound0 (Add a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
1.41 -| "polybound0 (Sub a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
1.42 -| "polybound0 (Mul a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
1.43 -| "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p"
1.44 -| "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p"
1.45 +  where
1.46 +    "polybound0 (C c) \<longleftrightarrow> True"
1.47 +  | "polybound0 (Bound n) \<longleftrightarrow> n > 0"
1.48 +  | "polybound0 (Neg a) \<longleftrightarrow> polybound0 a"
1.49 +  | "polybound0 (Add a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
1.50 +  | "polybound0 (Sub a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
1.51 +  | "polybound0 (Mul a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
1.52 +  | "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p"
1.53 +  | "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p"
1.54
1.55  primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" \<comment> \<open>substitute a poly into a poly for Bound 0\<close>
1.56 -where
1.57 -  "polysubst0 t (C c) = C c"
1.58 -| "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)"
1.59 -| "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
1.60 -| "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
1.61 -| "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)"
1.62 -| "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
1.63 -| "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
1.64 -| "polysubst0 t (CN c n p) =
1.65 -    (if n = 0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
1.66 -     else CN (polysubst0 t c) n (polysubst0 t p))"
1.67 +  where
1.68 +    "polysubst0 t (C c) = C c"
1.69 +  | "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)"
1.70 +  | "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
1.71 +  | "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
1.72 +  | "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)"
1.73 +  | "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
1.74 +  | "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
1.75 +  | "polysubst0 t (CN c n p) =
1.76 +      (if n = 0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
1.77 +       else CN (polysubst0 t c) n (polysubst0 t p))"
1.78
1.79  fun decrpoly:: "poly \<Rightarrow> poly"
1.80 -where
1.81 -  "decrpoly (Bound n) = Bound (n - 1)"
1.82 -| "decrpoly (Neg a) = Neg (decrpoly a)"
1.83 -| "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)"
1.84 -| "decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)"
1.85 -| "decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)"
1.86 -| "decrpoly (Pw p n) = Pw (decrpoly p) n"
1.87 -| "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)"
1.88 -| "decrpoly a = a"
1.89 +  where
1.90 +    "decrpoly (Bound n) = Bound (n - 1)"
1.91 +  | "decrpoly (Neg a) = Neg (decrpoly a)"
1.92 +  | "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)"
1.93 +  | "decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)"
1.94 +  | "decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)"
1.95 +  | "decrpoly (Pw p n) = Pw (decrpoly p) n"
1.96 +  | "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)"
1.97 +  | "decrpoly a = a"
1.98
1.99
1.100  subsection \<open>Degrees and heads and coefficients\<close>
1.101
1.102  fun degree :: "poly \<Rightarrow> nat"
1.103 -where
1.104 -  "degree (CN c 0 p) = 1 + degree p"
1.105 -| "degree p = 0"
1.106 +  where
1.107 +    "degree (CN c 0 p) = 1 + degree p"
1.108 +  | "degree p = 0"
1.109
1.110  fun head :: "poly \<Rightarrow> poly"
1.111 -where
1.112 -  "head (CN c 0 p) = head p"
1.113 -| "head p = p"
1.114 +  where
1.115 +    "head (CN c 0 p) = head p"
1.116 +  | "head p = p"
1.117
1.118  text \<open>More general notions of degree and head.\<close>
1.119
1.120  fun degreen :: "poly \<Rightarrow> nat \<Rightarrow> nat"
1.121 -where
1.122 -  "degreen (CN c n p) = (\<lambda>m. if n = m then 1 + degreen p n else 0)"
1.123 -| "degreen p = (\<lambda>m. 0)"
1.124 +  where
1.125 +    "degreen (CN c n p) = (\<lambda>m. if n = m then 1 + degreen p n else 0)"
1.126 +  | "degreen p = (\<lambda>m. 0)"
1.127
1.128  fun headn :: "poly \<Rightarrow> nat \<Rightarrow> poly"
1.129 -where
1.130 -  "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"
1.131 -| "headn p = (\<lambda>m. p)"
1.132 +  where
1.133 +    "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"
1.134 +  | "headn p = (\<lambda>m. p)"
1.135
1.136  fun coefficients :: "poly \<Rightarrow> poly list"
1.137 -where
1.138 -  "coefficients (CN c 0 p) = c # coefficients p"
1.139 -| "coefficients p = [p]"
1.140 +  where
1.141 +    "coefficients (CN c 0 p) = c # coefficients p"
1.142 +  | "coefficients p = [p]"
1.143
1.144  fun isconstant :: "poly \<Rightarrow> bool"
1.145 -where
1.146 -  "isconstant (CN c 0 p) = False"
1.147 -| "isconstant p = True"
1.148 +  where
1.149 +    "isconstant (CN c 0 p) = False"
1.150 +  | "isconstant p = True"
1.151
1.152  fun behead :: "poly \<Rightarrow> poly"
1.153 -where
1.154 -  "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
1.155 -| "behead p = 0\<^sub>p"
1.156 +  where
1.157 +    "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
1.158 +  | "behead p = 0\<^sub>p"
1.159
1.160  fun headconst :: "poly \<Rightarrow> Num"
1.161 -where
1.162 -  "headconst (CN c n p) = headconst p"
1.163 -| "headconst (C n) = n"
1.164 +  where
1.165 +    "headconst (CN c n p) = headconst p"
1.166 +  | "headconst (C n) = n"
1.167
1.168
1.169  subsection \<open>Operations for normalization\<close>
1.170 @@ -116,70 +116,69 @@
1.171  declare if_cong[fundef_cong del]
1.172  declare let_cong[fundef_cong del]
1.173
1.174 -fun polyadd :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
1.175 -where
1.176 -  "polyadd (C c) (C c') = C (c +\<^sub>N c')"
1.177 -| "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'"
1.178 -| "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p"
1.179 -| "polyadd (CN c n p) (CN c' n' p') =
1.180 -    (if n < n' then CN (polyadd c (CN c' n' p')) n p
1.181 -     else if n' < n then CN (polyadd (CN c n p) c') n' p'
1.182 -     else
1.183 -      let
1.184 -        cc' = polyadd c c';
1.185 -        pp' = polyadd p p'
1.186 -      in if pp' = 0\<^sub>p then cc' else CN cc' n pp')"
1.187 -| "polyadd a b = Add a b"
1.188 -
1.189 +fun polyadd :: "poly \<Rightarrow> poly \<Rightarrow> poly"  (infixl "+\<^sub>p" 60)
1.190 +  where
1.191 +    "polyadd (C c) (C c') = C (c +\<^sub>N c')"
1.192 +  | "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'"
1.193 +  | "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p"
1.194 +  | "polyadd (CN c n p) (CN c' n' p') =
1.195 +      (if n < n' then CN (polyadd c (CN c' n' p')) n p
1.196 +       else if n' < n then CN (polyadd (CN c n p) c') n' p'
1.197 +       else
1.198 +        let
1.199 +          cc' = polyadd c c';
1.200 +          pp' = polyadd p p'
1.201 +        in if pp' = 0\<^sub>p then cc' else CN cc' n pp')"
1.202 +  | "polyadd a b = Add a b"
1.203
1.204  fun polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p")
1.205 -where
1.206 -  "polyneg (C c) = C (~\<^sub>N c)"
1.207 -| "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
1.208 -| "polyneg a = Neg a"
1.209 +  where
1.210 +    "polyneg (C c) = C (~\<^sub>N c)"
1.211 +  | "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
1.212 +  | "polyneg a = Neg a"
1.213
1.214 -definition polysub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
1.215 +definition polysub :: "poly \<Rightarrow> poly \<Rightarrow> poly"  (infixl "-\<^sub>p" 60)
1.216    where "p -\<^sub>p q = polyadd p (polyneg q)"
1.217
1.218 -fun polymul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
1.219 -where
1.220 -  "polymul (C c) (C c') = C (c *\<^sub>N c')"
1.221 -| "polymul (C c) (CN c' n' p') =
1.222 -    (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))"
1.223 -| "polymul (CN c n p) (C c') =
1.224 -    (if c' = 0\<^sub>N  then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))"
1.225 -| "polymul (CN c n p) (CN c' n' p') =
1.226 -    (if n < n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p'))
1.227 -     else if n' < n then CN (polymul (CN c n p) c') n' (polymul (CN c n p) p')
1.228 -     else polyadd (polymul (CN c n p) c') (CN 0\<^sub>p n' (polymul (CN c n p) p')))"
1.229 -| "polymul a b = Mul a b"
1.230 +fun polymul :: "poly \<Rightarrow> poly \<Rightarrow> poly"  (infixl "*\<^sub>p" 60)
1.231 +  where
1.232 +    "polymul (C c) (C c') = C (c *\<^sub>N c')"
1.233 +  | "polymul (C c) (CN c' n' p') =
1.234 +      (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))"
1.235 +  | "polymul (CN c n p) (C c') =
1.236 +      (if c' = 0\<^sub>N  then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))"
1.237 +  | "polymul (CN c n p) (CN c' n' p') =
1.238 +      (if n < n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p'))
1.239 +       else if n' < n then CN (polymul (CN c n p) c') n' (polymul (CN c n p) p')
1.240 +       else polyadd (polymul (CN c n p) c') (CN 0\<^sub>p n' (polymul (CN c n p) p')))"
1.241 +  | "polymul a b = Mul a b"
1.242
1.243  declare if_cong[fundef_cong]
1.244  declare let_cong[fundef_cong]
1.245
1.246  fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
1.247 -where
1.248 -  "polypow 0 = (\<lambda>p. (1)\<^sub>p)"
1.249 -| "polypow n =
1.250 -    (\<lambda>p.
1.251 -      let
1.252 -        q = polypow (n div 2) p;
1.253 -        d = polymul q q
1.254 -      in if even n then d else polymul p d)"
1.255 +  where
1.256 +    "polypow 0 = (\<lambda>p. (1)\<^sub>p)"
1.257 +  | "polypow n =
1.258 +      (\<lambda>p.
1.259 +        let
1.260 +          q = polypow (n div 2) p;
1.261 +          d = polymul q q
1.262 +        in if even n then d else polymul p d)"
1.263
1.264 -abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
1.265 +abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly"  (infixl "^\<^sub>p" 60)
1.266    where "a ^\<^sub>p k \<equiv> polypow k a"
1.267
1.268  function polynate :: "poly \<Rightarrow> poly"
1.269 -where
1.270 -  "polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p"
1.271 -| "polynate (Add p q) = polynate p +\<^sub>p polynate q"
1.272 -| "polynate (Sub p q) = polynate p -\<^sub>p polynate q"
1.273 -| "polynate (Mul p q) = polynate p *\<^sub>p polynate q"
1.274 -| "polynate (Neg p) = ~\<^sub>p (polynate p)"
1.275 -| "polynate (Pw p n) = polynate p ^\<^sub>p n"
1.276 -| "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
1.277 -| "polynate (C c) = C (normNum c)"
1.278 +  where
1.279 +    "polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p"
1.280 +  | "polynate (Add p q) = polynate p +\<^sub>p polynate q"
1.281 +  | "polynate (Sub p q) = polynate p -\<^sub>p polynate q"
1.282 +  | "polynate (Mul p q) = polynate p *\<^sub>p polynate q"
1.283 +  | "polynate (Neg p) = ~\<^sub>p (polynate p)"
1.284 +  | "polynate (Pw p n) = polynate p ^\<^sub>p n"
1.285 +  | "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
1.286 +  | "polynate (C c) = C (normNum c)"
1.287    by pat_completeness auto
1.288  termination by (relation "measure polysize") auto
1.289
1.290 @@ -190,8 +189,7 @@
1.291  | "poly_cmul y p = C y *\<^sub>p p"
1.292
1.293  definition monic :: "poly \<Rightarrow> poly \<times> bool"
1.294 -where
1.295 -  "monic p =
1.296 +  where "monic p =
1.297      (let h = headconst p
1.298       in if h = 0\<^sub>N then (p, False) else (C (Ninv h) *\<^sub>p p, 0>\<^sub>N h))"
1.299
1.300 @@ -224,28 +222,28 @@
1.301    where "polydivide s p = polydivide_aux (head p) (degree p) p 0 s"
1.302
1.303  fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly"
1.304 -where
1.305 -  "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"
1.306 -| "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p"
1.307 +  where
1.308 +    "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"
1.309 +  | "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p"
1.310
1.311  fun poly_deriv :: "poly \<Rightarrow> poly"
1.312 -where
1.313 -  "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
1.314 -| "poly_deriv p = 0\<^sub>p"
1.315 +  where
1.316 +    "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
1.317 +  | "poly_deriv p = 0\<^sub>p"
1.318
1.319
1.320  subsection \<open>Semantics of the polynomial representation\<close>
1.321
1.322  primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
1.323 -where
1.324 -  "Ipoly bs (C c) = INum c"
1.325 -| "Ipoly bs (Bound n) = bs!n"
1.326 -| "Ipoly bs (Neg a) = - Ipoly bs a"
1.327 -| "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
1.328 -| "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
1.329 -| "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
1.330 -| "Ipoly bs (Pw t n) = Ipoly bs t ^ n"
1.331 -| "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p"
1.332 +  where
1.333 +    "Ipoly bs (C c) = INum c"
1.334 +  | "Ipoly bs (Bound n) = bs!n"
1.335 +  | "Ipoly bs (Neg a) = - Ipoly bs a"
1.336 +  | "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
1.337 +  | "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
1.338 +  | "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
1.339 +  | "Ipoly bs (Pw t n) = Ipoly bs t ^ n"
1.340 +  | "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p"
1.341
1.342  abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}"  ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
1.343    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
1.344 @@ -262,10 +260,10 @@
1.345  subsection \<open>Normal form and normalization\<close>
1.346
1.347  fun isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
1.348 -where
1.349 -  "isnpolyh (C c) = (\<lambda>k. isnormNum c)"
1.350 -| "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.351 -| "isnpolyh p = (\<lambda>k. False)"
1.352 +  where
1.353 +    "isnpolyh (C c) = (\<lambda>k. isnormNum c)"
1.354 +  | "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.355 +  | "isnpolyh p = (\<lambda>k. False)"
1.356
1.357  lemma isnpolyh_mono: "n' \<le> n \<Longrightarrow> isnpolyh p n \<Longrightarrow> isnpolyh p n'"
1.358    by (induct p rule: isnpolyh.induct) auto
1.359 @@ -512,23 +510,22 @@
1.360        and nn0: "n \<ge> n0"
1.361        and nn1: "n' \<ge> n1"
1.362        by simp_all
1.363 -    {
1.364 -      assume "n < n'"
1.365 +    consider "n < n'" | "n' < n" | "n' = n" by arith
1.366 +    then show ?case
1.367 +    proof cases
1.368 +      case 1
1.369        with "4.hyps"(4-5)[OF np cnp', of n] and "4.hyps"(1)[OF nc cnp', of n] nn0 cnp
1.370 -      have ?case by (simp add: min_def)
1.371 -    } moreover {
1.372 -      assume "n' < n"
1.373 +      show ?thesis by (simp add: min_def)
1.374 +    next
1.375 +      case 2
1.376        with "4.hyps"(16-17)[OF cnp np', of "n'"] and "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp'
1.377 -      have ?case by (cases "Suc n' = n") (simp_all add: min_def)
1.378 -    } moreover {
1.379 -      assume "n' = n"
1.380 +      show ?thesis by (cases "Suc n' = n") (simp_all add: min_def)
1.381 +    next
1.382 +      case 3
1.383        with "4.hyps"(16-17)[OF cnp np', of n] and "4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0
1.384 -      have ?case
1.385 -        apply (auto intro!: polyadd_normh)
1.386 -        apply (simp_all add: min_def isnpolyh_mono[OF nn0])
1.387 -        done
1.388 -    }
1.389 -    ultimately show ?case by arith
1.390 +      show ?thesis
1.391 +        by (auto intro!: polyadd_normh) (simp_all add: min_def isnpolyh_mono[OF nn0])
1.392 +    qed
1.393    next
1.394      fix n0 n1 m
1.395      assume np: "isnpolyh ?cnp n0"
1.396 @@ -538,16 +535,14 @@
1.397      let ?d1 = "degreen ?cnp m"
1.398      let ?d2 = "degreen ?cnp' m"
1.399      let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0  else ?d1 + ?d2)"
1.400 -    have "n' < n \<or> n < n' \<or> n' = n" by auto
1.401 -    moreover
1.402 -    {
1.403 -      assume "n' < n \<or> n < n'"
1.404 -      with "4.hyps"(3,6,18) np np' m have ?eq
1.405 -        by auto
1.406 -    }
1.407 -    moreover
1.408 -    {
1.409 -      assume nn': "n' = n"
1.410 +    consider "n' < n \<or> n < n'" | "n' = n" by linarith
1.411 +    then show ?eq
1.412 +    proof cases
1.413 +      case 1
1.414 +      with "4.hyps"(3,6,18) np np' m show ?thesis by auto
1.415 +    next
1.416 +      case 2
1.417 +      have nn': "n' = n" by fact
1.418        then have nn: "\<not> n' < n \<and> \<not> n < n'" by arith
1.419        from "4.hyps"(16,18)[of n n' n]
1.420          "4.hyps"(13,14)[of n "Suc n'" n]
1.421 @@ -562,8 +557,9 @@
1.422          "?cnp *\<^sub>p c' = 0\<^sub>p \<longleftrightarrow> c' = 0\<^sub>p"
1.423          "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"
1.424          by (auto simp add: min_def)
1.425 -      {
1.426 -        assume mn: "m = n"
1.427 +      show ?thesis
1.428 +      proof (cases "m = n")
1.429 +        case mn: True
1.430          from "4.hyps"(17,18)[OF norm(1,4), of n]
1.431            "4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn
1.432          have degs:
1.433 @@ -583,11 +579,9 @@
1.434          from "4.hyps"(16-18)[OF norm(1,4), of n]
1.435            "4.hyps"(13-15)[OF norm(1,2), of n]
1.436            mn norm m nn' deg
1.437 -        have ?eq by simp
1.438 -      }
1.439 -      moreover
1.440 -      {
1.441 -        assume mn: "m \<noteq> n"
1.442 +        show ?thesis by simp
1.443 +      next
1.444 +        case mn: False
1.445          then have mn': "m < n"
1.446            using m np by auto
1.447          from nn' m np have max1: "m \<le> max n n"
1.448 @@ -605,11 +599,10 @@
1.449          with "4.hyps"(16-18)[OF norm(1,4) min1]
1.450            "4.hyps"(13-15)[OF norm(1,2) min2]
1.451            degreen_0[OF norm(3) mn']
1.452 -        have ?eq using nn' mn np np' by clarsimp
1.453 -      }
1.454 -      ultimately have ?eq by blast
1.455 -    }
1.456 -    ultimately show ?eq by blast
1.457 +          nn' mn np np'
1.458 +        show ?thesis by clarsimp
1.459 +      qed
1.460 +    qed
1.461    }
1.462    {
1.463      case (2 n0 n1)
1.464 @@ -619,9 +612,9 @@
1.465        by simp_all
1.466      then have mn: "m \<le> n" by simp
1.467      let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
1.468 -    {
1.469 -      assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
1.470 -      then have nn: "\<not> n' < n \<and> \<not> n < n'"
1.471 +    have False if C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
1.472 +    proof -
1.473 +      from C have nn: "\<not> n' < n \<and> \<not> n < n'"
1.474          by simp
1.475        from "4.hyps"(16-18) [of n n n]
1.476          "4.hyps"(13-15)[of n "Suc n" n]
1.477 @@ -643,8 +636,8 @@
1.478        have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
1.479          using norm by simp
1.480        from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq
1.481 -      have False by simp
1.482 -    }
1.483 +      show ?thesis by simp
1.484 +    qed
1.485      then show ?case using "4.hyps" by clarsimp
1.486    }
1.487  qed auto
1.488 @@ -747,22 +740,19 @@
1.489
1.490  text \<open>polypow is a power function and preserves normal forms\<close>
1.491
1.492 -lemma polypow[simp]:
1.493 -  "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
1.494 +lemma polypow[simp]: "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
1.495  proof (induct n rule: polypow.induct)
1.496    case 1
1.497 -  then show ?case
1.498 -    by simp
1.499 +  then show ?case by simp
1.500  next
1.501    case (2 n)
1.502    let ?q = "polypow ((Suc n) div 2) p"
1.503    let ?d = "polymul ?q ?q"
1.504 -  have "odd (Suc n) \<or> even (Suc n)"
1.505 -    by simp
1.506 -  moreover
1.507 -  {
1.508 -    assume odd: "odd (Suc n)"
1.509 -    have th: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1"
1.510 +  consider "odd (Suc n)" | "even (Suc n)" by auto
1.511 +  then show ?case
1.512 +  proof cases
1.513 +    case odd: 1
1.514 +    have *: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1"
1.515        by arith
1.516      from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)"
1.517        by (simp add: Let_def)
1.518 @@ -771,21 +761,19 @@
1.519      also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
1.520        by (simp only: power_add power_one_right) simp
1.521      also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
1.522 -      by (simp only: th)
1.523 -    finally have ?case unfolding numeral_2_eq_2 [symmetric]
1.524 -    using odd_two_times_div_two_nat [OF odd] by simp
1.525 -  }
1.526 -  moreover
1.527 -  {
1.528 -    assume even: "even (Suc n)"
1.529 +      by (simp only: *)
1.530 +    finally show ?thesis
1.531 +      unfolding numeral_2_eq_2 [symmetric]
1.532 +      using odd_two_times_div_two_nat [OF odd] by simp
1.533 +  next
1.534 +    case even: 2
1.535      from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d"
1.536        by (simp add: Let_def)
1.537      also have "\<dots> = (Ipoly bs p) ^ (2 * (Suc n div 2))"
1.538        using "2.hyps" by (simp only: mult_2 power_add) simp
1.539 -    finally have ?case using even_two_times_div_two [OF even]
1.540 -      by simp
1.541 -  }
1.542 -  ultimately show ?case by blast
1.543 +    finally show ?thesis
1.544 +      using even_two_times_div_two [OF even] by simp
1.545 +  qed
1.546  qed
1.547
1.548  lemma polypow_normh:
1.549 @@ -798,14 +786,13 @@
1.550    case (2 k n)
1.551    let ?q = "polypow (Suc k div 2) p"
1.552    let ?d = "polymul ?q ?q"
1.553 -  from 2 have th1: "isnpolyh ?q n" and th2: "isnpolyh p n"
1.554 +  from 2 have *: "isnpolyh ?q n" and **: "isnpolyh p n"
1.555      by blast+
1.556 -  from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n"
1.557 +  from polymul_normh[OF * *] have dn: "isnpolyh ?d n"
1.558      by simp
1.559 -  from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n"
1.560 +  from polymul_normh[OF ** dn] have on: "isnpolyh (polymul p ?d) n"
1.561      by simp
1.562    from dn on show ?case by (simp, unfold Let_def) auto
1.563 -
1.564  qed
1.565
1.566  lemma polypow_norm:
1.567 @@ -815,8 +802,7 @@
1.568
1.569  text \<open>Finally the whole normalization\<close>
1.570
1.571 -lemma polynate [simp]:
1.572 -  "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
1.573 +lemma polynate [simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
1.574    by (induct p rule:polynate.induct) auto
1.575
1.576  lemma polynate_norm[simp]:
1.577 @@ -828,7 +814,6 @@
1.578
1.579  text \<open>shift1\<close>
1.580
1.581 -
1.582  lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
1.583    by (simp add: shift1_def)
1.584
1.585 @@ -909,7 +894,7 @@
1.586
1.587  lemma decrpoly_normh: "isnpolyh p n0 \<Longrightarrow> polybound0 p \<Longrightarrow> isnpolyh (decrpoly p) (n0 - 1)"
1.588    apply (induct p arbitrary: n0)
1.589 -  apply auto
1.590 +         apply auto
1.591    apply atomize
1.592    apply (rename_tac nat a b, erule_tac x = "Suc nat" in allE)
1.593    apply auto
1.594 @@ -945,15 +930,15 @@
1.595    by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0)
1.596
1.597  primrec maxindex :: "poly \<Rightarrow> nat"
1.598 -where
1.599 -  "maxindex (Bound n) = n + 1"
1.600 -| "maxindex (CN c n p) = max  (n + 1) (max (maxindex c) (maxindex p))"
1.601 -| "maxindex (Add p q) = max (maxindex p) (maxindex q)"
1.602 -| "maxindex (Sub p q) = max (maxindex p) (maxindex q)"
1.603 -| "maxindex (Mul p q) = max (maxindex p) (maxindex q)"
1.604 -| "maxindex (Neg p) = maxindex p"
1.605 -| "maxindex (Pw p n) = maxindex p"
1.606 -| "maxindex (C x) = 0"
1.607 +  where
1.608 +    "maxindex (Bound n) = n + 1"
1.609 +  | "maxindex (CN c n p) = max  (n + 1) (max (maxindex c) (maxindex p))"
1.610 +  | "maxindex (Add p q) = max (maxindex p) (maxindex q)"
1.611 +  | "maxindex (Sub p q) = max (maxindex p) (maxindex q)"
1.612 +  | "maxindex (Mul p q) = max (maxindex p) (maxindex q)"
1.613 +  | "maxindex (Neg p) = maxindex p"
1.614 +  | "maxindex (Pw p n) = maxindex p"
1.615 +  | "maxindex (C x) = 0"
1.616
1.617  definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool"
1.618    where "wf_bs bs p \<longleftrightarrow> length bs \<ge> maxindex p"
1.619 @@ -964,25 +949,21 @@
1.620    show ?case
1.621    proof
1.622      fix x
1.623 -    assume xc: "x \<in> set (coefficients (CN c 0 p))"
1.624 -    then have "x = c \<or> x \<in> set (coefficients p)"
1.625 -      by simp
1.626 -    moreover
1.627 -    {
1.628 -      assume "x = c"
1.629 -      then have "wf_bs bs x"
1.630 -        using "1.prems" unfolding wf_bs_def by simp
1.631 -    }
1.632 -    moreover
1.633 -    {
1.634 -      assume H: "x \<in> set (coefficients p)"
1.635 +    assume "x \<in> set (coefficients (CN c 0 p))"
1.636 +    then consider "x = c" | "x \<in> set (coefficients p)"
1.637 +      by auto
1.638 +    then show "wf_bs bs x"
1.639 +    proof cases
1.640 +      case prems: 1
1.641 +      then show ?thesis
1.642 +        using "1.prems" by (simp add: wf_bs_def)
1.643 +    next
1.644 +      case prems: 2
1.645        from "1.prems" have "wf_bs bs p"
1.646 -        unfolding wf_bs_def by simp
1.647 -      with "1.hyps" H have "wf_bs bs x"
1.648 +        by (simp add: wf_bs_def)
1.649 +      with "1.hyps" prems show ?thesis
1.650          by blast
1.651 -    }
1.652 -    ultimately show "wf_bs bs x"
1.653 -      by blast
1.654 +    qed
1.655    qed
1.656  qed simp_all
1.657
1.658 @@ -990,7 +971,7 @@
1.659    by (induct p rule: coefficients.induct) auto
1.660
1.661  lemma wf_bs_I: "wf_bs bs p \<Longrightarrow> Ipoly (bs @ bs') p = Ipoly bs p"
1.662 -  unfolding wf_bs_def by (induct p) (auto simp add: nth_append)
1.663 +  by (induct p) (auto simp add: nth_append wf_bs_def)
1.664
1.665  lemma take_maxindex_wf:
1.666    assumes wf: "wf_bs bs p"
1.667 @@ -1012,10 +993,10 @@
1.668    by (induct p) auto
1.669
1.670  lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
1.671 -  unfolding wf_bs_def by simp
1.672 +  by (simp add: wf_bs_def)
1.673
1.674  lemma wf_bs_insensitive': "wf_bs (x # bs) p = wf_bs (y # bs) p"
1.675 -  unfolding wf_bs_def by simp
1.676 +  by (simp add: wf_bs_def)
1.677
1.678  lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x # bs) p"
1.679    by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def)
1.680 @@ -1030,31 +1011,28 @@
1.681    unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto
1.682
1.683  lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists>ys. length (xs @ ys) = n"
1.684 -  apply (rule exI[where x="replicate (n - length xs) z" for z])
1.685 -  apply simp
1.686 -  done
1.687 +  by (rule exI[where x="replicate (n - length xs) z" for z]) simp
1.688
1.689  lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
1.690    apply (cases p)
1.691 -  apply auto
1.692 +         apply auto
1.693    apply (rename_tac nat a, case_tac "nat")
1.694 -  apply simp_all
1.695 +   apply simp_all
1.696    done
1.697
1.698  lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)"
1.699 -  unfolding wf_bs_def by (induct p q rule: polyadd.induct) (auto simp add: Let_def)
1.700 +  by (induct p q rule: polyadd.induct) (auto simp add: Let_def wf_bs_def)
1.701
1.702  lemma wf_bs_polyul: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p *\<^sub>p q)"
1.703 -  unfolding wf_bs_def
1.704    apply (induct p q arbitrary: bs rule: polymul.induct)
1.705 -  apply (simp_all add: wf_bs_polyadd)
1.706 +                      apply (simp_all add: wf_bs_polyadd wf_bs_def)
1.707    apply clarsimp
1.708    apply (rule wf_bs_polyadd[unfolded wf_bs_def, rule_format])
1.709    apply auto
1.710    done
1.711
1.712  lemma wf_bs_polyneg: "wf_bs bs p \<Longrightarrow> wf_bs bs (~\<^sub>p p)"
1.713 -  unfolding wf_bs_def by (induct p rule: polyneg.induct) auto
1.714 +  by (induct p rule: polyneg.induct) (auto simp: wf_bs_def)
1.715
1.716  lemma wf_bs_polysub: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p -\<^sub>p q)"
1.717    unfolding polysub_def split_def fst_conv snd_conv
1.718 @@ -1087,16 +1065,15 @@
1.719  proof -
1.720    let ?cf = "set (coefficients p)"
1.721    from coefficients_normh[OF np] have cn_norm: "\<forall> q\<in> ?cf. isnpolyh q n0" .
1.722 -  {
1.723 -    fix q
1.724 -    assume q: "q \<in> ?cf"
1.725 -    from q cn_norm have th: "isnpolyh q n0"
1.726 +  have "polybound0 q" if "q \<in> ?cf" for q
1.727 +  proof -
1.728 +    from that cn_norm have *: "isnpolyh q n0"
1.729        by blast
1.730 -    from coefficients_isconst[OF np] q have "isconstant q"
1.731 +    from coefficients_isconst[OF np] that have "isconstant q"
1.732        by blast
1.733 -    with isconstant_polybound0[OF th] have "polybound0 q"
1.734 +    with isconstant_polybound0[OF *] show ?thesis
1.735        by blast
1.736 -  }
1.737 +  qed
1.738    then have "\<forall>q \<in> ?cf. polybound0 q" ..
1.739    then have "\<forall>q \<in> ?cf. Ipoly (x # bs) q = Ipoly bs (decrpoly q)"
1.740      using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs]
1.741 @@ -1124,9 +1101,9 @@
1.742    using assms
1.743    unfolding polypoly_def
1.744    apply (cases p)
1.745 -  apply auto
1.746 +         apply auto
1.747    apply (rename_tac nat a, case_tac nat)
1.748 -  apply auto
1.749 +   apply auto
1.750    done
1.751
1.752  lemma head_isnpolyh: "isnpolyh p n0 \<Longrightarrow> isnpolyh (head p) n0"
1.753 @@ -1149,16 +1126,13 @@
1.754  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
1.755    case less
1.756    note np = \<open>isnpolyh p n0\<close> and zp = \<open>\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)\<close>
1.757 -  {
1.758 -    assume nz: "maxindex p = 0"
1.759 -    then obtain c where "p = C c"
1.760 -      using np by (cases p) auto
1.761 -    with zp np have "p = 0\<^sub>p"
1.762 -      unfolding wf_bs_def by simp
1.763 -  }
1.764 -  moreover
1.765 -  {
1.766 -    assume nz: "maxindex p \<noteq> 0"
1.767 +  show "p = 0\<^sub>p"
1.768 +  proof (cases "maxindex p = 0")
1.769 +    case True
1.770 +    with np obtain c where "p = C c" by (cases p) auto
1.771 +    with zp np show ?thesis by (simp add: wf_bs_def)
1.772 +  next
1.773 +    case nz: False
1.774      let ?h = "head p"
1.775      let ?hd = "decrpoly ?h"
1.776      let ?ihd = "maxindex ?hd"
1.777 @@ -1173,13 +1147,13 @@
1.778        by auto
1.779      with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < maxindex p"
1.780        by auto
1.781 -    {
1.782 -      fix bs :: "'a list"
1.783 -      assume bs: "wf_bs bs ?hd"
1.784 +
1.785 +    have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" if bs: "wf_bs bs ?hd" for bs :: "'a list"
1.786 +    proof -
1.787        let ?ts = "take ?ihd bs"
1.788        let ?rs = "drop ?ihd bs"
1.789 -      have ts: "wf_bs ?ts ?hd"
1.790 -        using bs unfolding wf_bs_def by simp
1.791 +      from bs have ts: "wf_bs ?ts ?hd"
1.792 +        by (simp add: wf_bs_def)
1.793        have bs_ts_eq: "?ts @ ?rs = bs"
1.794          by simp
1.795        from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x # ?ts) ?h"
1.796 @@ -1189,7 +1163,7 @@
1.797        with length_le_list_ex obtain xs where xs: "length ((x # ?ts) @ xs) = maxindex p"
1.798          by blast
1.799        then have "\<forall>x. wf_bs ((x # ?ts) @ xs) p"
1.800 -        unfolding wf_bs_def by simp
1.801 +        by (simp add: wf_bs_def)
1.802        with zp have "\<forall>x. Ipoly ((x # ?ts) @ xs) p = 0"
1.803          by blast
1.804        then have "\<forall>x. Ipoly (x # (?ts @ xs)) p = 0"
1.805 @@ -1202,24 +1176,22 @@
1.806        then have "\<forall>c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
1.807          using poly_zero[where ?'a='a] by (simp add: polypoly'_def)
1.808        with coefficients_head[of p, symmetric]
1.809 -      have th0: "Ipoly (?ts @ xs) ?hd = 0"
1.810 +      have *: "Ipoly (?ts @ xs) ?hd = 0"
1.811          by simp
1.812        from bs have wf'': "wf_bs ?ts ?hd"
1.813 -        unfolding wf_bs_def by simp
1.814 -      with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0"
1.815 +        by (simp add: wf_bs_def)
1.816 +      with * wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0"
1.817          by simp
1.818 -      with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0"
1.819 +      with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq show ?thesis
1.820          by simp
1.821 -    }
1.822 +    qed
1.823      then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)"
1.824        by blast
1.825      from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p"
1.826        by blast
1.827      then have "?h = 0\<^sub>p" by simp
1.828 -    with head_nz[OF np] have "p = 0\<^sub>p" by simp
1.829 -  }
1.830 -  ultimately show "p = 0\<^sub>p"
1.831 -    by blast
1.832 +    with head_nz[OF np] show ?thesis by simp
1.833 +  qed
1.834  qed
1.835
1.836  lemma isnpolyh_unique:
1.837 @@ -1227,7 +1199,7 @@
1.838      and nq: "isnpolyh q n1"
1.839    shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field,power})) \<longleftrightarrow> p = q"
1.840  proof auto
1.841 -  assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a) = \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
1.842 +  assume "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a) = \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
1.843    then have "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)"
1.844      by simp
1.845    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.846 @@ -1237,7 +1209,7 @@
1.847  qed
1.848
1.849
1.850 -text \<open>consequences of unicity on the algorithms for polynomial normalization\<close>
1.851 +text \<open>Consequences of unicity on the algorithms for polynomial normalization.\<close>
1.852
1.853  lemma polyadd_commute:
1.854    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.855 @@ -1311,7 +1283,7 @@
1.856    unfolding poly_nate_polypoly' by auto
1.857
1.858
1.859 -subsection \<open>heads, degrees and all that\<close>
1.860 +subsection \<open>Heads, degrees and all that\<close>
1.861
1.862  lemma degree_eq_degreen0: "degree p = degreen p 0"
1.863    by (induct p rule: degree.induct) simp_all
1.864 @@ -1321,9 +1293,9 @@
1.865    shows "degree (polyneg p) = degree p"
1.866    apply (induct p rule: polyneg.induct)
1.867    using assms
1.868 -  apply simp_all
1.869 +         apply simp_all
1.870    apply (case_tac na)
1.871 -  apply auto
1.872 +   apply auto
1.873    done
1.874
1.875  lemma degree_polyadd:
1.876 @@ -1395,50 +1367,43 @@
1.877      by simp
1.878    from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'"
1.879      by auto
1.880 -  have "n = n' \<or> n < n' \<or> n > n'"
1.881 +  consider "n = n'" | "n < n'" | "n > n'"
1.882      by arith
1.883 -  moreover
1.884 -  {
1.885 -    assume nn': "n = n'"
1.886 -    have "n = 0 \<or> n > 0" by arith
1.887 -    moreover
1.888 -    {
1.889 -      assume nz: "n = 0"
1.890 -      then have ?case using 4 nn'
1.891 +  then show ?case
1.892 +  proof cases
1.893 +    case nn': 1
1.894 +    consider "n = 0" | "n > 0" by arith
1.895 +    then show ?thesis
1.896 +    proof cases
1.897 +      case 1
1.898 +      with 4 nn' show ?thesis
1.899          by (auto simp add: Let_def degcmc')
1.900 -    }
1.901 -    moreover
1.902 -    {
1.903 -      assume nz: "n > 0"
1.904 -      with nn' H(3) have  cc': "c = c'" and pp': "p = p'"
1.905 -        by (cases n, auto)+
1.906 -      then have ?case
1.907 +    next
1.908 +      case 2
1.909 +      with nn' H(3) have "c = c'" and "p = p'"
1.910 +        by (cases n; auto)+
1.911 +      with nn' 4 show ?thesis
1.912          using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv]
1.913          using polysub_same_0[OF c'nh, simplified polysub_def]
1.914 -        using nn' 4 by (simp add: Let_def)
1.915 -    }
1.916 -    ultimately have ?case by blast
1.917 -  }
1.918 -  moreover
1.919 -  {
1.920 -    assume nn': "n < n'"
1.921 +        by (simp add: Let_def)
1.922 +    qed
1.923 +  next
1.924 +    case nn': 2
1.925      then have n'p: "n' > 0"
1.926        by simp
1.927      then have headcnp':"head (CN c' n' p') = CN c' n' p'"
1.928        by (cases n') simp_all
1.929 -    have degcnp': "degree (CN c' n' p') = 0"
1.930 +    with 4 nn' have degcnp': "degree (CN c' n' p') = 0"
1.931        and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')"
1.932 -      using 4 nn' by (cases n', simp_all)
1.933 +      by (cases n', simp_all)
1.934      then have "n > 0"
1.935        by (cases n) simp_all
1.936      then have headcnp: "head (CN c n p) = CN c n p"
1.937        by (cases n) auto
1.938 -    from H(3) headcnp headcnp' nn' have ?case
1.939 +    from H(3) headcnp headcnp' nn' show ?thesis
1.940        by auto
1.941 -  }
1.942 -  moreover
1.943 -  {
1.944 -    assume nn': "n > n'"
1.945 +  next
1.946 +    case nn': 3
1.947      then have np: "n > 0" by simp
1.948      then have headcnp:"head (CN c n p) = CN c n p"
1.949        by (cases n) simp_all
1.950 @@ -1450,15 +1415,14 @@
1.951        by (cases n') simp_all
1.952      then have headcnp': "head (CN c' n' p') = CN c' n' p'"
1.953        by (cases n') auto
1.954 -    from H(3) headcnp headcnp' nn' have ?case by auto
1.955 -  }
1.956 -  ultimately show ?case by blast
1.957 +    from H(3) headcnp headcnp' nn' show ?thesis by auto
1.958 +  qed
1.959  qed auto
1.960
1.961  lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p"
1.962    by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def)
1.963
1.964 -lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
1.965 +lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
1.966  proof (induct k arbitrary: n0 p)
1.967    case 0
1.968    then show ?case
1.969 @@ -1503,13 +1467,13 @@
1.970    shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)"
1.971    using np nq deg
1.972    apply (induct p q arbitrary: n0 n1 rule: polyadd.induct)
1.973 -  apply simp_all
1.974 -  apply (case_tac n', simp, simp)
1.975 -  apply (case_tac n, simp, simp)
1.976 +                      apply simp_all
1.977 +    apply (case_tac n', simp, simp)
1.978 +   apply (case_tac n, simp, simp)
1.979    apply (case_tac n, case_tac n', simp add: Let_def)
1.980 -  apply (auto simp add: polyadd_eq_const_degree)
1.981 -  apply (metis head_nz)
1.982 -  apply (metis head_nz)
1.983 +    apply (auto simp add: polyadd_eq_const_degree)
1.984 +    apply (metis head_nz)
1.985 +   apply (metis head_nz)
1.986    apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
1.987    done
1.988
1.989 @@ -1533,67 +1497,61 @@
1.990    then have norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
1.991      "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'"
1.992      by simp_all
1.993 -  have "n < n' \<or> n' < n \<or> n = n'" by arith
1.994 -  moreover
1.995 -  {
1.996 -    assume nn': "n < n'"
1.997 -    then have ?case
1.998 +  consider "n < n'" | "n' < n" | "n' = n" by arith
1.999 +  then show ?case
1.1000 +  proof cases
1.1001 +    case nn': 1
1.1002 +    then show ?thesis
1.1003        using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)]
1.1004        apply simp
1.1005        apply (cases n)
1.1006 -      apply simp
1.1007 +       apply simp
1.1008        apply (cases n')
1.1009 -      apply simp_all
1.1010 +       apply simp_all
1.1011        done
1.1012 -  }
1.1013 -  moreover {
1.1014 -    assume nn': "n'< n"
1.1015 -    then have ?case
1.1016 +  next
1.1017 +    case nn': 2
1.1018 +    then show ?thesis
1.1019        using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)]
1.1020        apply simp
1.1021        apply (cases n')
1.1022 -      apply simp
1.1023 +       apply simp
1.1024        apply (cases n)
1.1025 -      apply auto
1.1026 +       apply auto
1.1027        done
1.1028 -  }
1.1029 -  moreover
1.1030 -  {
1.1031 -    assume nn': "n' = n"
1.1032 +  next
1.1033 +    case nn': 3
1.1034      from nn' polymul_normh[OF norm(5,4)]
1.1035 -    have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)
1.1036 +    have ncnpc': "isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)
1.1037      from nn' polymul_normh[OF norm(5,3)] norm
1.1038 -    have ncnpp':"isnpolyh (CN c n p *\<^sub>p p') n" by simp
1.1039 +    have ncnpp': "isnpolyh (CN c n p *\<^sub>p p') n" by simp
1.1040      from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6)
1.1041 -    have ncnpp0':"isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
1.1042 +    have ncnpp0': "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
1.1043      from polyadd_normh[OF ncnpc' ncnpp0']
1.1044      have nth: "isnpolyh ((CN c n p *\<^sub>p c') +\<^sub>p (CN 0\<^sub>p n (CN c n p *\<^sub>p p'))) n"
1.1045        by (simp add: min_def)
1.1046 -    {
1.1047 -      assume np: "n > 0"
1.1048 +    consider "n > 0" | "n = 0" by auto
1.1049 +    then show ?thesis
1.1050 +    proof cases
1.1051 +      case np: 1
1.1052        with nn' head_isnpolyh_Suc'[OF np nth]
1.1053          head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
1.1054 -      have ?case by simp
1.1055 -    }
1.1056 -    moreover
1.1057 -    {
1.1058 -      assume nz: "n = 0"
1.1059 +      show ?thesis by simp
1.1060 +    next
1.1061 +      case nz: 2
1.1062        from polymul_degreen[OF norm(5,4), where m="0"]
1.1063          polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
1.1064 -      norm(5,6) degree_npolyhCN[OF norm(6)]
1.1065 -    have dth: "degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))"
1.1066 -      by simp
1.1067 -    then have dth': "degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))"
1.1068 -      by simp
1.1069 -    from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
1.1070 -    have ?case
1.1071 -      using norm "4.hyps"(6)[OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] nn' nz
1.1072 -      by simp
1.1073 -    }
1.1074 -    ultimately have ?case
1.1075 -      by (cases n) auto
1.1076 -  }
1.1077 -  ultimately show ?case by blast
1.1078 +        norm(5,6) degree_npolyhCN[OF norm(6)]
1.1079 +      have dth: "degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))"
1.1080 +        by simp
1.1081 +      then have dth': "degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))"
1.1082 +        by simp
1.1083 +      from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
1.1084 +      show ?thesis
1.1085 +        using norm "4.hyps"(6)[OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] nn' nz
1.1086 +        by simp
1.1087 +    qed
1.1088 +  qed
1.1089  qed simp_all
1.1090
1.1091  lemma degree_coefficients: "degree p = length (coefficients p) - 1"
1.1092 @@ -1663,52 +1621,50 @@
1.1093      by (simp add: isnpoly_def)
1.1094    from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap
1.1095    have nakk':"isnpolyh ?akk' 0" by blast
1.1096 -  {
1.1097 -    assume sz: "s = 0\<^sub>p"
1.1098 -    then have ?ths
1.1099 -      using np polydivide_aux.simps
1.1100 -      apply clarsimp
1.1101 +  show ?ths
1.1102 +  proof (cases "s = 0\<^sub>p")
1.1103 +    case True
1.1104 +    with np show ?thesis
1.1105 +      apply (clarsimp simp: polydivide_aux.simps)
1.1106        apply (rule exI[where x="0\<^sub>p"])
1.1107        apply simp
1.1108        done
1.1109 -  }
1.1110 -  moreover
1.1111 -  {
1.1112 -    assume sz: "s \<noteq> 0\<^sub>p"
1.1113 -    {
1.1114 -      assume dn: "degree s < n"
1.1115 -      then have "?ths"
1.1116 +  next
1.1117 +    case sz: False
1.1118 +    show ?thesis
1.1119 +    proof (cases "degree s < n")
1.1120 +      case True
1.1121 +      then show ?thesis
1.1122          using ns ndp np polydivide_aux.simps
1.1123          apply auto
1.1124          apply (rule exI[where x="0\<^sub>p"])
1.1125          apply simp
1.1126          done
1.1127 -    }
1.1128 -    moreover
1.1129 -    {
1.1130 -      assume dn': "\<not> degree s < n"
1.1131 +    next
1.1132 +      case dn': False
1.1133        then have dn: "degree s \<ge> n"
1.1134          by arith
1.1135        have degsp': "degree s = degree ?p'"
1.1136          using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"]
1.1137          by simp
1.1138 -      {
1.1139 -        assume ba: "?b = a"
1.1140 +      show ?thesis
1.1141 +      proof (cases "?b = a")
1.1142 +        case ba: True
1.1143          then have headsp': "head s = head ?p'"
1.1144            using ap headp' by simp
1.1145          have nr: "isnpolyh (s -\<^sub>p ?p') 0"
1.1146            using polysub_normh[OF ns np'] by simp
1.1147          from degree_polysub_samehead[OF ns np' headsp' degsp']
1.1148 -        have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p"
1.1149 -          by simp
1.1150 -        moreover
1.1151 -        {
1.1152 -          assume deglt:"degree (s -\<^sub>p ?p') < degree s"
1.1153 +        consider "degree (s -\<^sub>p ?p') < degree s" | "s -\<^sub>p ?p' = 0\<^sub>p" by auto
1.1154 +        then show ?thesis
1.1155 +        proof cases
1.1156 +          case deglt: 1
1.1157            from polydivide_aux.simps sz dn' ba
1.1158            have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
1.1159              by (simp add: Let_def)
1.1160 -          {
1.1161 -            assume h1: "polydivide_aux a n p k s = (k', r)"
1.1162 +          have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1.1163 +            if h1: "polydivide_aux a n p k s = (k', r)"
1.1164 +          proof -
1.1165              from less(1)[OF deglt nr, of k k' r] trans[OF eq[symmetric] h1]
1.1166              have kk': "k \<le> k'"
1.1167                and nr: "\<exists>nr. isnpolyh r nr"
1.1168 @@ -1753,54 +1709,45 @@
1.1169              have "a ^\<^sub>p (k' - k) *\<^sub>p s =
1.1170                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.1171                by blast
1.1172 -            then have ?qths using nq'
1.1173 +            with nq' have ?qths
1.1174                apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q" in exI)
1.1175                apply (rule_tac x="0" in exI)
1.1176                apply simp
1.1177                done
1.1178 -            with kk' nr dr have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and>
1.1179 -              (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1.1180 +            with kk' nr dr show ?thesis
1.1181                by blast
1.1182 -          }
1.1183 -          then have ?ths by blast
1.1184 -        }
1.1185 -        moreover
1.1186 -        {
1.1187 -          assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
1.1188 +          qed
1.1189 +          then show ?thesis by blast
1.1190 +        next
1.1191 +          case spz: 2
1.1192            from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field}"]
1.1193            have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'"
1.1194              by simp
1.1195 -          then have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
1.1196 -            using np nxdn
1.1197 -            apply simp
1.1198 -            apply (simp only: funpow_shift1_1)
1.1199 -            apply simp
1.1200 -            done
1.1201 +          with np nxdn have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
1.1202 +            by (simp only: funpow_shift1_1) simp
1.1203            then have sp': "s = ?xdn *\<^sub>p p"
1.1204              using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
1.1205              by blast
1.1206 -          {
1.1207 -            assume h1: "polydivide_aux a n p k s = (k', r)"
1.1208 -            from polydivide_aux.simps sz dn' ba
1.1209 -            have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
1.1210 -              by (simp add: Let_def)
1.1211 +          have ?thesis if h1: "polydivide_aux a n p k s = (k', r)"
1.1212 +          proof -
1.1213 +            from sz dn' ba
1.1214 +            have "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
1.1215 +              by (simp add: Let_def polydivide_aux.simps)
1.1216              also have "\<dots> = (k,0\<^sub>p)"
1.1217 -              using polydivide_aux.simps spz by simp
1.1218 +              using spz by (simp add: polydivide_aux.simps)
1.1219              finally have "(k', r) = (k, 0\<^sub>p)"
1.1220 -              using h1 by simp
1.1221 +              by (simp add: h1)
1.1222              with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
1.1223 -              polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?ths
1.1224 +              polyadd_0(2)[OF polymul_normh[OF np nxdn]] show ?thesis
1.1225                apply auto
1.1226                apply (rule exI[where x="?xdn"])
1.1227                apply (auto simp add: polymul_commute[of p])
1.1228                done
1.1229 -          }
1.1230 -        }
1.1231 -        ultimately have ?ths by blast
1.1232 -      }
1.1233 -      moreover
1.1234 -      {
1.1235 -        assume ba: "?b \<noteq> a"
1.1236 +          qed
1.1237 +          then show ?thesis by blast
1.1238 +        qed
1.1239 +      next
1.1240 +        case ba: False
1.1241          from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns]
1.1242            polymul_normh[OF head_isnpolyh[OF ns] np']]
1.1243          have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0"
1.1244 @@ -1811,7 +1758,8 @@
1.1245              funpow_shift1_nz[OF pnz]
1.1246            by simp_all
1.1247          from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
1.1248 -          polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="degree s - n"]
1.1249 +          polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz
1.1250 +          funpow_shift1_nz[OF pnz, where n="degree s - n"]
1.1251          have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')"
1.1252            using head_head[OF ns] funpow_shift1_head[OF np pnz]
1.1253              polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
1.1254 @@ -1823,14 +1771,22 @@
1.1255            ndp dn
1.1256          have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p')"
1.1257            by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
1.1258 -        {
1.1259 -          assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s"
1.1260 +
1.1261 +        consider "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s" | "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
1.1262 +          using degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns]
1.1263 +            polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth]
1.1264 +            polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
1.1265 +            head_nz[OF np] pnz sz ap[symmetric]
1.1266 +          by (auto simp add: degree_eq_degreen0[symmetric])
1.1267 +        then show ?thesis
1.1268 +        proof cases
1.1269 +          case dth: 1
1.1270            from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.1271              polymul_normh[OF head_isnpolyh[OF ns]np']] ap
1.1272            have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0"
1.1273              by simp
1.1274 -          {
1.1275 -            assume h1:"polydivide_aux a n p k s = (k', r)"
1.1276 +          have ?thesis if h1: "polydivide_aux a n p k s = (k', r)"
1.1277 +          proof -
1.1278              from h1 polydivide_aux.simps sz dn' ba
1.1279              have eq:"polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
1.1280                by (simp add: Let_def)
1.1281 @@ -1843,8 +1799,10 @@
1.1282                by auto
1.1283              from kk' have kk'': "Suc (k' - Suc k) = k' - k"
1.1284                by arith
1.1285 -            {
1.1286 -              fix bs :: "'a::{field_char_0,field} list"
1.1287 +            have "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.1288 +                Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
1.1289 +              for bs :: "'a::{field_char_0,field} list"
1.1290 +            proof -
1.1291                from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
1.1292                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.1293                  by simp
1.1294 @@ -1854,11 +1812,10 @@
1.1295                then have "Ipoly bs a ^ (k' - k)  * Ipoly bs s =
1.1296                  Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r"
1.1297                  by (simp add: kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
1.1298 -              then have "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.1299 -                Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
1.1300 +              then show ?thesis
1.1301                  by (simp add: field_simps)
1.1302 -            }
1.1303 -            then have ieq:"\<forall>bs :: 'a::{field_char_0,field} list.
1.1304 +            qed
1.1305 +            then have ieq: "\<forall>bs :: 'a::{field_char_0,field} list.
1.1306                  Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.1307                  Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
1.1308                by auto
1.1309 @@ -1869,62 +1826,53 @@
1.1310              from ieq isnpolyh_unique[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - k"] ns, simplified ap] polyadd_normh[OF polymul_normh[OF np nqw] nr]]
1.1311              have asth: "(a ^\<^sub>p (k' - k) *\<^sub>p s) = p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r"
1.1312                by blast
1.1313 -            from dr kk' nr h1 asth nqw have ?ths
1.1314 +            from dr kk' nr h1 asth nqw show ?thesis
1.1315                apply simp
1.1316                apply (rule conjI)
1.1317                apply (rule exI[where x="nr"], simp)
1.1318                apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
1.1319                apply (rule exI[where x="0"], simp)
1.1320                done
1.1321 -          }
1.1322 -          then have ?ths by blast
1.1323 -        }
1.1324 -        moreover
1.1325 -        {
1.1326 -          assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
1.1327 -          {
1.1328 +          qed
1.1329 +          then show ?thesis by blast
1.1330 +        next
1.1331 +          case spz: 2
1.1332 +          have hth: "\<forall>bs :: 'a::{field_char_0,field} list.
1.1333 +            Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
1.1334 +          proof
1.1335              fix bs :: "'a::{field_char_0,field} list"
1.1336              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
1.1337              have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'"
1.1338                by simp
1.1339              then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p"
1.1340                by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
1.1341 -            then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
1.1342 +            then show "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
1.1343                by simp
1.1344 -          }
1.1345 -          then have hth: "\<forall>bs :: 'a::{field_char_0,field} list.
1.1346 -            Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
1.1347 +          qed
1.1348            from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
1.1349              using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.1350                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
1.1351                simplified ap]
1.1352              by simp
1.1353 -          {
1.1354 -            assume h1: "polydivide_aux a n p k s = (k', r)"
1.1355 +          have ?ths if h1: "polydivide_aux a n p k s = (k', r)"
1.1356 +          proof -
1.1357              from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps
1.1358              have "(k', r) = (Suc k, 0\<^sub>p)"
1.1359                by (simp add: Let_def)
1.1360              with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
1.1361                polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
1.1362 -            have ?ths
1.1363 +            show ?thesis
1.1364                apply (clarsimp simp add: Let_def)
1.1365                apply (rule exI[where x="?b *\<^sub>p ?xdn"])
1.1366                apply simp
1.1367                apply (rule exI[where x="0"], simp)
1.1368                done
1.1369 -          }
1.1370 -          then have ?ths by blast
1.1371 -        }
1.1372 -        ultimately have ?ths
1.1373 -          using degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth] polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
1.1374 -            head_nz[OF np] pnz sz ap[symmetric]
1.1375 -          by (auto simp add: degree_eq_degreen0[symmetric])
1.1376 -      }
1.1377 -      ultimately have ?ths by blast
1.1378 -    }
1.1379 -    ultimately have ?ths by blast
1.1380 -  }
1.1381 -  ultimately show ?ths by blast
1.1382 +          qed
1.1383 +          then show ?thesis by blast
1.1384 +        qed
1.1385 +      qed
1.1386 +    qed
1.1387 +  qed
1.1388  qed
1.1389
1.1390  lemma polydivide_properties:
1.1391 @@ -1965,14 +1913,14 @@
1.1392    shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
1.1393  proof
1.1394    let ?p = "polypoly bs p"
1.1395 -  assume H: "pnormal ?p"
1.1396 -  have csz: "coefficients p \<noteq> []"
1.1397 +  assume *: "pnormal ?p"
1.1398 +  have "coefficients p \<noteq> []"
1.1399      using assms by (cases p) auto
1.1400 -  from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] pnormal_last_nonzero[OF H]
1.1401 +  from coefficients_head[of p] last_map[OF this, of "Ipoly bs"] pnormal_last_nonzero[OF *]
1.1402    show "Ipoly bs (head p) \<noteq> 0"
1.1403      by (simp add: polypoly_def)
1.1404  next
1.1405 -  assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.1406 +  assume *: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.1407    let ?p = "polypoly bs p"
1.1408    have csz: "coefficients p \<noteq> []"
1.1409      using assms by (cases p) auto
1.1410 @@ -1980,7 +1928,7 @@
1.1411      by (simp add: polypoly_def)
1.1412    then have lg: "length ?p > 0"
1.1413      by simp
1.1414 -  from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"]
1.1415 +  from * coefficients_head[of p] last_map[OF csz, of "Ipoly bs"]
1.1416    have lz: "last ?p \<noteq> 0"
1.1417      by (simp add: polypoly_def)
1.1418    from pnormal_last_length[OF lg lz] show "pnormal ?p" .
1.1419 @@ -1999,73 +1947,71 @@
1.1420    shows "nonconstant (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
1.1421  proof
1.1422    let ?p = "polypoly bs p"
1.1423 -  assume nc: "nonconstant ?p"
1.1424 -  from isnonconstant_pnormal_iff[OF assms, of bs] nc
1.1425 -  show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.1426 +  assume "nonconstant ?p"
1.1427 +  with isnonconstant_pnormal_iff[OF assms, of bs] show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.1428      unfolding nonconstant_def by blast
1.1429  next
1.1430    let ?p = "polypoly bs p"
1.1431 -  assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.1432 -  from isnonconstant_pnormal_iff[OF assms, of bs] h
1.1433 -  have pn: "pnormal ?p"
1.1434 +  assume "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.1435 +  with isnonconstant_pnormal_iff[OF assms, of bs] have pn: "pnormal ?p"
1.1436      by blast
1.1437 -  {
1.1438 -    fix x
1.1439 -    assume H: "?p = [x]"
1.1440 +  have False if H: "?p = [x]" for x
1.1441 +  proof -
1.1442      from H have "length (coefficients p) = 1"
1.1443 -      unfolding polypoly_def by auto
1.1444 +      by (auto simp: polypoly_def)
1.1445      with isnonconstant_coefficients_length[OF assms]
1.1446 -    have False by arith
1.1447 -  }
1.1448 +    show ?thesis by arith
1.1449 +  qed
1.1450    then show "nonconstant ?p"
1.1451      using pn unfolding nonconstant_def by blast
1.1452  qed
1.1453
1.1454  lemma pnormal_length: "p \<noteq> [] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
1.1455    apply (induct p)
1.1456 -  apply (simp_all add: pnormal_def)
1.1457 +   apply (simp_all add: pnormal_def)
1.1458    apply (case_tac "p = []")
1.1459 -  apply simp_all
1.1460 +   apply simp_all
1.1461    done
1.1462
1.1463  lemma degree_degree:
1.1464    assumes "isnonconstant p"
1.1465    shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.1466 +    (is "?lhs \<longleftrightarrow> ?rhs")
1.1467  proof
1.1468    let ?p = "polypoly bs p"
1.1469 -  assume H: "degree p = Polynomial_List.degree ?p"
1.1470 -  from isnonconstant_coefficients_length[OF assms] have pz: "?p \<noteq> []"
1.1471 -    unfolding polypoly_def by auto
1.1472 -  from H degree_coefficients[of p] isnonconstant_coefficients_length[OF assms]
1.1473 -  have lg: "length (pnormalize ?p) = length ?p"
1.1474 -    unfolding Polynomial_List.degree_def polypoly_def by simp
1.1475 -  then have "pnormal ?p"
1.1476 -    using pnormal_length[OF pz] by blast
1.1477 -  with isnonconstant_pnormal_iff[OF assms] show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.1478 -    by blast
1.1479 -next
1.1480 -  let ?p = "polypoly bs p"
1.1481 -  assume H: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.1482 -  with isnonconstant_pnormal_iff[OF assms] have "pnormal ?p"
1.1483 -    by blast
1.1484 -  with degree_coefficients[of p] isnonconstant_coefficients_length[OF assms]
1.1485 -  show "degree p = Polynomial_List.degree ?p"
1.1486 -    unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto
1.1487 +  {
1.1488 +    assume ?lhs
1.1489 +    from isnonconstant_coefficients_length[OF assms] have "?p \<noteq> []"
1.1490 +      by (auto simp: polypoly_def)
1.1491 +    from \<open>?lhs\<close> degree_coefficients[of p] isnonconstant_coefficients_length[OF assms]
1.1492 +    have "length (pnormalize ?p) = length ?p"
1.1493 +      by (simp add: Polynomial_List.degree_def polypoly_def)
1.1494 +    with pnormal_length[OF \<open>?p \<noteq> []\<close>] have "pnormal ?p"
1.1495 +      by blast
1.1496 +    with isnonconstant_pnormal_iff[OF assms] show ?rhs
1.1497 +      by blast
1.1498 +  next
1.1499 +    assume ?rhs
1.1500 +    with isnonconstant_pnormal_iff[OF assms] have "pnormal ?p"
1.1501 +      by blast
1.1502 +    with degree_coefficients[of p] isnonconstant_coefficients_length[OF assms] show ?lhs
1.1503 +      by (auto simp: polypoly_def pnormal_def Polynomial_List.degree_def)
1.1504 +  }
1.1505  qed
1.1506
1.1507
1.1508 -section \<open>Swaps ; Division by a certain variable\<close>
1.1509 +section \<open>Swaps -- division by a certain variable\<close>
1.1510
1.1511  primrec swap :: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly"
1.1512 -where
1.1513 -  "swap n m (C x) = C x"
1.1514 -| "swap n m (Bound k) = Bound (if k = n then m else if k = m then n else k)"
1.1515 -| "swap n m (Neg t) = Neg (swap n m t)"
1.1516 -| "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
1.1517 -| "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
1.1518 -| "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
1.1519 -| "swap n m (Pw t k) = Pw (swap n m t) k"
1.1520 -| "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k) (swap n m p)"
1.1521 +  where
1.1522 +    "swap n m (C x) = C x"
1.1523 +  | "swap n m (Bound k) = Bound (if k = n then m else if k = m then n else k)"
1.1524 +  | "swap n m (Neg t) = Neg (swap n m t)"
1.1525 +  | "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
1.1526 +  | "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
1.1527 +  | "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
1.1528 +  | "swap n m (Pw t k) = Pw (swap n m t) k"
1.1529 +  | "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k) (swap n m p)"
1.1530
1.1531  lemma swap:
1.1532    assumes "n < length bs"
1.1533 @@ -2116,10 +2062,10 @@
1.1534    by (induct p) simp_all
1.1535
1.1536  fun isweaknpoly :: "poly \<Rightarrow> bool"
1.1537 -where
1.1538 -  "isweaknpoly (C c) = True"
1.1539 -| "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
1.1540 -| "isweaknpoly p = False"
1.1541 +  where
1.1542 +    "isweaknpoly (C c) = True"
1.1543 +  | "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
1.1544 +  | "isweaknpoly p = False"
1.1545
1.1546  lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p"
1.1547    by (induct p arbitrary: n0) auto
```