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)[2]
   1.981 -  apply (metis head_nz)
   1.982 -  apply (metis head_nz)
   1.983 +    apply (auto simp add: polyadd_eq_const_degree)[2]
   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