Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Decision_Procs/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 77 kB

Quelle Reflected_Multivariate_Polynomial.thy Sprache: Isabelle

(*  Title:      HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
    Author:     Amine Chaieb
*)

section \<open>Implementation and verification of multivariate polynomials\<close>

theory Reflected_Multivariate_Polynomial
  imports Complex_Main Rat_Pair Polynomial_List
begin

subsection \<open>Datatype of polynomial expressions\<close>

datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly
  | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly

abbreviation poly_0 :: "poly" (\<open>0\<^sub>p\<close>) where "0\<^sub>p \<equiv> C (0\<^sub>N)"
abbreviation poly_p :: "int \ poly" (\'((_)')\<^sub>p\) where "(i)\<^sub>p \ C (i)\<^sub>N"

subsection\<open>Boundedness, substitution and all that\<close>

primrec polysize:: "poly \ nat"
  where
    "polysize (C c) = 1"
  | "polysize (Bound n) = 1"
  | "polysize (Neg p) = 1 + polysize p"
  | "polysize (Add p q) = 1 + polysize p + polysize q"
  | "polysize (Sub p q) = 1 + polysize p + polysize q"
  | "polysize (Mul p q) = 1 + polysize p + polysize q"
  | "polysize (Pw p n) = 1 + polysize p"
  | "polysize (CN c n p) = 4 + polysize c + polysize p"

primrec polybound0:: "poly \ bool" \ \a poly is INDEPENDENT of Bound 0\
  where
    "polybound0 (C c) \ True"
  | "polybound0 (Bound n) \ n > 0"
  | "polybound0 (Neg a) \ polybound0 a"
  | "polybound0 (Add a b) \ polybound0 a \ polybound0 b"
  | "polybound0 (Sub a b) \ polybound0 a \ polybound0 b"
  | "polybound0 (Mul a b) \ polybound0 a \ polybound0 b"
  | "polybound0 (Pw p n) \ polybound0 p"
  | "polybound0 (CN c n p) \ n \ 0 \ polybound0 c \ polybound0 p"

primrec polysubst0:: "poly \ poly \ poly" \ \substitute a poly into a poly for Bound 0\
  where
    "polysubst0 t (C c) = C c"
  | "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)"
  | "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
  | "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
  | "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)"
  | "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
  | "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
  | "polysubst0 t (CN c n p) =
      (if n = 0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
       else CN (polysubst0 t c) n (polysubst0 t p))"

fun decrpoly:: "poly \ poly"
  where
    "decrpoly (Bound n) = Bound (n - 1)"
  | "decrpoly (Neg a) = Neg (decrpoly a)"
  | "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)"
  | "decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)"
  | "decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)"
  | "decrpoly (Pw p n) = Pw (decrpoly p) n"
  | "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)"
  | "decrpoly a = a"

subsection \<open>Degrees and heads and coefficients\<close>

fun degree :: "poly \ nat"
  where
    "degree (CN c 0 p) = 1 + degree p"
  | "degree p = 0"

fun head :: "poly \ poly"
  where
    "head (CN c 0 p) = head p"
  | "head p = p"

text \<open>More general notions of degree and head.\<close>

fun degreen :: "poly \ nat \ nat"
  where
    "degreen (CN c n p) = (\m. if n = m then 1 + degreen p n else 0)"
  | "degreen p = (\m. 0)"

fun headn :: "poly \ nat \ poly"
  where
    "headn (CN c n p) = (\m. if n \ m then headn p m else CN c n p)"
  | "headn p = (\m. p)"

fun coefficients :: "poly \ poly list"
  where
    "coefficients (CN c 0 p) = c # coefficients p"
  | "coefficients p = [p]"

fun isconstant :: "poly \ bool"
  where
    "isconstant (CN c 0 p) = False"
  | "isconstant p = True"

fun behead :: "poly \ poly"
  where
    "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
  | "behead p = 0\<^sub>p"

fun headconst :: "poly \ Num"
  where
    "headconst (CN c n p) = headconst p"
  | "headconst (C n) = n"

subsection \<open>Operations for normalization\<close>

declare if_cong[fundef_cong del]
declare let_cong[fundef_cong del]

fun polyadd :: "poly \ poly \ poly" (infixl \+\<^sub>p\ 60)
  where
    "polyadd (C c) (C c') = C (c +\<^sub>N c')"
  | "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'"
  | "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p"
  | "polyadd (CN c n p) (CN c' n' p') =
      (if n < n' then CN (polyadd c (CN c' n' p')) n p
       else if n' < n then CN (polyadd (CN c n p) c') n' p'
       else
        let
          cc' = polyadd c c';
          pp' = polyadd p p'
        in if pp' = 0\<^sub>p then cc' else CN cc' n pp')"
  | "polyadd a b = Add a b"

fun polyneg :: "poly \ poly" (\~\<^sub>p\)
  where
    "polyneg (C c) = C (~\<^sub>N c)"
  | "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
  | "polyneg a = Neg a"

definition polysub :: "poly \ poly \ poly" (infixl \-\<^sub>p\ 60)
  where "p -\<^sub>p q = polyadd p (polyneg q)"

fun polymul :: "poly \ poly \ poly" (infixl \*\<^sub>p\ 60)
  where
    "polymul (C c) (C c') = C (c *\<^sub>N c')"
  | "polymul (C c) (CN c' n' p') =
      (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))"
  | "polymul (CN c n p) (C c') =
      (if c' = 0\<^sub>N then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))"
  | "polymul (CN c n p) (CN c' n' p') =
      (if n < n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p'))
       else if n' < n then CN (polymul (CN c n p) c') n' (polymul (CN c n p) p')
       else polyadd (polymul (CN c n p) c') (CN 0\<^sub>p n' (polymul (CN c n p) p')))"
  | "polymul a b = Mul a b"

declare if_cong[fundef_cong]
declare let_cong[fundef_cong]

fun polypow :: "nat \ poly \ poly"
  where
    "polypow 0 = (\p. (1)\<^sub>p)"
  | "polypow n =
      (\<lambda>p.
        let
          q = polypow (n div 2) p;
          d = polymul q q
        in if even n then d else polymul p d)"

abbreviation poly_pow :: "poly \ nat \ poly" (infixl \^\<^sub>p\ 60)
  where "a ^\<^sub>p k \ polypow k a"

function polynate :: "poly \ poly"
  where
    "polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p"
  | "polynate (Add p q) = polynate p +\<^sub>p polynate q"
  | "polynate (Sub p q) = polynate p -\<^sub>p polynate q"
  | "polynate (Mul p q) = polynate p *\<^sub>p polynate q"
  | "polynate (Neg p) = ~\<^sub>p (polynate p)"
  | "polynate (Pw p n) = polynate p ^\<^sub>p n"
  | "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
  | "polynate (C c) = C (normNum c)"
  by pat_completeness auto
termination by (relation "measure polysize") auto

fun poly_cmul :: "Num \ poly \ poly"
where
  "poly_cmul y (C x) = C (y *\<^sub>N x)"
| "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)"
| "poly_cmul y p = C y *\<^sub>p p"

definition monic :: "poly \ poly \ bool"
  where "monic p =
    (let h = headconst p
     in if h = 0\<^sub>N then (p, False) else (C (Ninv h) *\<^sub>p p, 0>\<^sub>N h))"

subsection \<open>Pseudo-division\<close>

definition shift1 :: "poly \ poly"
  where "shift1 p = CN 0\<^sub>p 0 p"

abbreviation funpow :: "nat \ ('a \ 'a) \ 'a \ 'a"
  where "funpow \ compow"

partial_function (tailrec) polydivide_aux :: "poly \ nat \ poly \ nat \ poly \ nat \ poly"
where
  "polydivide_aux a n p k s =
    (if s = 0\<^sub>p then (k, s)
     else
      let
        b = head s;
        m = degree s
      in
        if m < n then (k,s)
        else
          let p' = funpow (m - n) shift1 p
          in
            if a = b then polydivide_aux a n p k (s -\<^sub>p p')
            else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))"

definition polydivide :: "poly \ poly \ nat \ poly"
  where "polydivide s p = polydivide_aux (head p) (degree p) p 0 s"

fun poly_deriv_aux :: "nat \ poly \ poly"
  where
    "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"
  | "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p"

fun poly_deriv :: "poly \ poly"
  where
    "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
  | "poly_deriv p = 0\<^sub>p"

subsection \<open>Semantics of the polynomial representation\<close>

primrec Ipoly :: "'a list \ poly \ 'a::{field_char_0,power}"
  where
    "Ipoly bs (C c) = INum c"
  | "Ipoly bs (Bound n) = bs!n"
  | "Ipoly bs (Neg a) = - Ipoly bs a"
  | "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
  | "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
  | "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
  | "Ipoly bs (Pw t n) = Ipoly bs t ^ n"
  | "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p"

abbreviation Ipoly_syntax :: "poly \ 'a list \'a::{field_char_0,power}" (\\_\\<^sub>p\<^bsup>_\<^esup>\)
  where "\p\\<^sub>p\<^bsup>bs\<^esup> \ Ipoly bs p"

lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i"
  by (simp add: INum_def)

lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j"
  by (simp  add: INum_def)

lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat

subsection \<open>Normal form and normalization\<close>

fun isnpolyh:: "poly \ nat \ bool"
  where
    "isnpolyh (C c) = (\k. isnormNum c)"
  | "isnpolyh (CN c n p) = (\k. n \ k \ isnpolyh c (Suc n) \ isnpolyh p n \ p \ 0\<^sub>p)"
  | "isnpolyh p = (\k. False)"

lemma isnpolyh_mono: "n' \ n \ isnpolyh p n \ isnpolyh p n'"
  by (induct p rule: isnpolyh.induct) auto

definition isnpoly :: "poly \ bool"
  where "isnpoly p = isnpolyh p 0"

text \<open>polyadd preserves normal forms\<close>

lemma polyadd_normh: "isnpolyh p n0 \ isnpolyh q n1 \ isnpolyh (polyadd p q) (min n0 n1)"
proof (induct p q arbitrary: n0 n1 rule: polyadd.induct)
  case (2 ab c' n' p' n0 n1)
  from 2 have  th1: "isnpolyh (C ab) (Suc n')"
    by simp
  from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \ n1"
    by simp_all
  with isnpolyh_mono have cp: "isnpolyh c' (Suc n')"
    by simp
  with 2(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')"
    by simp
  from nplen1 have n01len1: "min n0 n1 \ n'"
    by simp
  then show ?case using 2 th3
    by simp
next
  case (3 c' n' p' ab n1 n0)
  from 3 have  th1: "isnpolyh (C ab) (Suc n')"
    by simp
  from 3(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \ n1"
    by simp_all
  with isnpolyh_mono have cp: "isnpolyh c' (Suc n')"
    by simp
  with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')"
    by simp
  from nplen1 have n01len1: "min n0 n1 \ n'"
    by simp
  then show ?case using 3 th3
    by simp
next
  case (4 c n p c' n' p' n0 n1)
  then have nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n"
    by simp_all
  from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'"
    by simp_all
  from 4 have ngen0: "n \ n0"
    by simp
  from 4 have n'gen1: "n' \<ge> n1"
    by simp
  consider (eq) "n = n'" | (lt) "n < n'" | (gt) "n > n'"
    by arith
  then show ?case
  proof cases
    case eq
    with "4.hyps"(3)[OF nc nc']
    have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)"
      by auto
    then have ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
      using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1
      by auto
    from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n"
      by simp
    have minle: "min n0 n1 \ n'"
      using ngen0 n'gen1 eq by simp
    from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' show ?thesis
      by (simp add: Let_def)
  next
    case lt
    have "min n0 n1 \ n0"
      by simp
    with 4 lt have th1:"min n0 n1 \ n"
      by auto
    from 4 have th21: "isnpolyh c (Suc n)"
      by simp
    from 4 have th22: "isnpolyh (CN c' n' p') n'"
      by simp
    from lt have th23: "min (Suc n) n' = Suc n"
      by arith
    from "4.hyps"(1)[OF th21 th22] have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)"
      using th23 by simp
    with 4 lt th1 show ?thesis
      by simp
  next
    case gt
    then have gt': "n' < n \<and> \<not> n < n'"
      by simp
    have "min n0 n1 \ n1"
      by simp
    with 4 gt have th1: "min n0 n1 \ n'"
      by auto
    from 4 have th21: "isnpolyh c' (Suc n')"
      by simp_all
    from 4 have th22: "isnpolyh (CN c n p) n"
      by simp
    from gt have th23: "min n (Suc n') = Suc n'"
      by arith
    from "4.hyps"(2)[OF th22 th21] have "isnpolyh (polyadd (CN c n p) c') (Suc n')"
      using th23 by simp
    with 4 gt th1 show ?thesis
      by simp
  qed
qed auto

lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
  by (induct p q rule: polyadd.induct)
     (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left_NO_MATCH)

lemma polyadd_norm: "isnpoly p \ isnpoly q \ isnpoly (polyadd p q)"
  using polyadd_normh[of p 0 q 0] isnpoly_def by simp

text \<open>The degree of addition and other general lemmas needed for the normal form of polymul.\<close>

lemma polyadd_different_degreen:
  assumes "isnpolyh p n0"
    and "isnpolyh q n1"
    and "degreen p m \ degreen q m"
    and "m \ min n0 n1"
  shows "degreen (polyadd p q) m = max (degreen p m) (degreen q m)"
  using assms
proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
  case (4 c n p c' n' p' m n0 n1)
  show ?case
  proof (cases "n = n'")
    case True
    with 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
    show ?thesis by (auto simp: Let_def)
  next
    case False
    with 4 show ?thesis by auto
  qed
qed auto

lemma headnz[simp]: "isnpolyh p n \ p \ 0\<^sub>p \ headn p m \ 0\<^sub>p"
  by (induct p arbitrary: n rule: headn.induct) auto

lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \ degree p = 0"
  by (induct p arbitrary: n rule: degree.induct) auto

lemma degreen_0[simp]: "isnpolyh p n \ m < n \ degreen p m = 0"
  by (induct p arbitrary: n rule: degreen.induct) auto

lemma degree_isnpolyh_Suc': "n > 0 \ isnpolyh p n \ degree p = 0"
  by (induct p arbitrary: n rule: degree.induct) auto

lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \ degree c = 0"
  using degree_isnpolyh_Suc by auto

lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \ degreen c n = 0"
  using degreen_0 by auto

lemma degreen_polyadd:
  assumes np: "isnpolyh p n0"
    and nq: "isnpolyh q n1"
    and m: "m \ max n0 n1"
  shows "degreen (p +\<^sub>p q) m \ max (degreen p m) (degreen q m)"
  using np nq m
proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct)
  case (2 c c' n' p' n0 n1)
  then show ?case
    by (cases n') simp_all
next
  case (3 c n p c' n0 n1)
  then show ?case
    by (cases n) auto
next
  case (4 c n p c' n' p' n0 n1 m)
  show ?case
  proof (cases "n = n'")
    case True
    with 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
    show ?thesis by (auto simp: Let_def)
  next
    case False
    then show ?thesis by simp
  qed
qed auto

lemma polyadd_eq_const_degreen:
  assumes "isnpolyh p n0"
    and "isnpolyh q n1"
    and "polyadd p q = C c"
  shows "degreen p m = degreen q m"
  using assms
proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
  case (4 c n p c' n' p' m n0 n1 x)
  consider "n = n'" | "n > n' \ n < n'" by arith
  then show ?case
  proof cases
    case 1
    with 4 show ?thesis
      by (cases "p +\<^sub>p p' = 0\<^sub>p") (auto simp add: Let_def)
  next
    case 2
    with 4 show ?thesis by auto
  qed
qed simp_all

lemma polymul_properties:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
    and np: "isnpolyh p n0"
    and nq: "isnpolyh q n1"
    and m: "m \ min n0 n1"
  shows "isnpolyh (p *\<^sub>p q) (min n0 n1)"
    and "p *\<^sub>p q = 0\<^sub>p \ p = 0\<^sub>p \ q = 0\<^sub>p"
    and "degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \ q = 0\<^sub>p then 0 else degreen p m + degreen q m)"
  using np nq m
proof (induct p q arbitrary: n0 n1 m rule: polymul.induct)
  case (2 c c' n' p')
  {
    case (1 n0 n1)
    with "2.hyps"(4-6)[of n' n' n'] and "2.hyps"(1-3)[of "Suc n'" "Suc n'" n']
    show ?case by (auto simp add: min_def)
  next
    case (2 n0 n1)
    then show ?case by auto
  next
    case (3 n0 n1)
    then show ?case using "2.hyps" by auto
  }
next
  case (3 c n p c')
  {
    case (1 n0 n1)
    with "3.hyps"(4-6)[of n n n] and "3.hyps"(1-3)[of "Suc n" "Suc n" n]
    show ?case by (auto simp add: min_def)
  next
    case (2 n0 n1)
    then show ?case by auto
  next
    case (3 n0 n1)
    then show ?case  using "3.hyps" by auto
  }
next
  case (4 c n p c' n' p')
  let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'"
  {
    case (1 n0 n1)
    then have cnp: "isnpolyh ?cnp n"
      and cnp': "isnpolyh ?cnp' n'"
      and np: "isnpolyh p n"
      and nc: "isnpolyh c (Suc n)"
      and np': "isnpolyh p' n'"
      and nc': "isnpolyh c' (Suc n')"
      and nn0: "n \ n0"
      and nn1: "n' \ n1"
      by simp_all
    consider "n < n'" | "n' < n" | "n' = n" by arith
    then show ?case
    proof cases
      case 1
      with "4.hyps"(4-5)[OF np cnp', of n] and "4.hyps"(1)[OF nc cnp', of n] nn0 cnp
      show ?thesis by (simp add: min_def)
    next
      case 2
      with "4.hyps"(16-17)[OF cnp np', of "n'"] and "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp'
      show ?thesis by (cases "Suc n' = n") (simp_all add: min_def)
    next
      case 3
      with "4.hyps"(16-17)[OF cnp np', of n] and "4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0
      show ?thesis
        by (auto intro!: polyadd_normh) (simp_all add: min_def isnpolyh_mono[OF nn0])
    qed
  next
    fix n0 n1 m
    assume np: "isnpolyh ?cnp n0"
    assume np':"isnpolyh ?cnp' n1"
    assume m: "m \ min n0 n1"
    let ?d = "degreen (?cnp *\<^sub>p ?cnp') m"
    let ?d1 = "degreen ?cnp m"
    let ?d2 = "degreen ?cnp' m"
    let ?eq = "?d = (if ?cnp = 0\<^sub>p \ ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)"
    consider "n' < n \ n < n'" | "n' = n" by linarith
    then show ?eq
    proof cases
      case 1
      with "4.hyps"(3,6,18) np np' m show ?thesis by auto
    next
      case 2
      have nn': "n' = n" by fact
      then have nn: "\ n' < n \ \ n < n'" by arith
      from "4.hyps"(16,18)[of n n' n]
        "4.hyps"(13,14)[of n "Suc n'" n]
        np np' nn'
      have norm:
        "isnpolyh ?cnp n"
        "isnpolyh c' (Suc n)"
        "isnpolyh (?cnp *\<^sub>p c') n"
        "isnpolyh p' n"
        "isnpolyh (?cnp *\<^sub>p p') n"
        "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
        "?cnp *\<^sub>p c' = 0\<^sub>p \ c' = 0\<^sub>p"
        "?cnp *\<^sub>p p' \ 0\<^sub>p"
        by (auto simp add: min_def)
      show ?thesis
      proof (cases "m = n")
        case mn: True
        from "4.hyps"(17,18)[OF norm(1,4), of n]
          "4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn
        have degs:
          "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else ?d1 + degreen c' n)"
          "degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n"
          by (simp_all add: min_def)
        from degs norm have th1: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
          by simp
        then have neq: "degreen (?cnp *\<^sub>p c') n \ degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
          by simp
        have nmin: "n \ min n n"
          by (simp add: min_def)
        from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
        have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n =
            degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
          by simp
        from "4.hyps"(16-18)[OF norm(1,4), of n]
          "4.hyps"(13-15)[OF norm(1,2), of n]
          mn norm m nn' deg
        show ?thesis by simp
      next
        case mn: False
        then have mn': "m < n"
          using m np by auto
        from nn' m np have max1: "m \ max n n"
          by simp
        then have min1: "m \ min n n"
          by simp
        then have min2: "m \ min n (Suc n)"
          by simp
        from "4.hyps"(16-18)[OF norm(1,4) min1]
          "4.hyps"(13-15)[OF norm(1,2) min2]
          degreen_polyadd[OF norm(3,6) max1]
        have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m \
            max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
          using mn nn' np np' by simp
        with "4.hyps"(16-18)[OF norm(1,4) min1]
          "4.hyps"(13-15)[OF norm(1,2) min2]
          degreen_0[OF norm(3) mn']
          nn' mn np np'
        show ?thesis by clarsimp
      qed
    qed
  }
  {
    case (2 n0 n1)
    then have np: "isnpolyh ?cnp n0"
      and np': "isnpolyh ?cnp' n1"
      and m: "m \ min n0 n1"
      by simp_all
    then have mn: "m \ n" by simp
    let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
    have False if C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
    proof -
      from C have nn: "\ n' < n \ \ n < n'"
        by simp
      from "4.hyps"(16-18) [of n n n]
        "4.hyps"(13-15)[of n "Suc n" n]
        np np' C(2) mn
      have norm:
        "isnpolyh ?cnp n"
        "isnpolyh c' (Suc n)"
        "isnpolyh (?cnp *\<^sub>p c') n"
        "isnpolyh p' n"
        "isnpolyh (?cnp *\<^sub>p p') n"
        "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
        "?cnp *\<^sub>p c' = 0\<^sub>p \ c' = 0\<^sub>p"
        "?cnp *\<^sub>p p' \ 0\<^sub>p"
        "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
        "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
        by (simp_all add: min_def)
      from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
        by simp
      have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
        using norm by simp
      from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq
      show ?thesis by simp
    qed
    then show ?case using "4.hyps" by clarsimp
  }
qed auto

lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = Ipoly bs p * Ipoly bs q"
  by (induct p q rule: polymul.induct) (auto simp add: field_simps)

lemma polymul_normh:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "isnpolyh p n0 \ isnpolyh q n1 \ isnpolyh (p *\<^sub>p q) (min n0 n1)"
  using polymul_properties(1) by blast

lemma polymul_eq0_iff:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "isnpolyh p n0 \ isnpolyh q n1 \ p *\<^sub>p q = 0\<^sub>p \ p = 0\<^sub>p \ q = 0\<^sub>p"
  using polymul_properties(2) by blast

lemma polymul_degreen:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "isnpolyh p n0 \ isnpolyh q n1 \ m \ min n0 n1 \
    degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \<or> q = 0\<^sub>p then 0 else degreen p m + degreen q m)"
  by (fact polymul_properties(3))

lemma polymul_norm:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "isnpoly p \ isnpoly q \ isnpoly (polymul p q)"
  using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp

lemma headconst_zero: "isnpolyh p n0 \ headconst p = 0\<^sub>N \ p = 0\<^sub>p"
  by (induct p arbitrary: n0 rule: headconst.induct) auto

lemma headconst_isnormNum: "isnpolyh p n0 \ isnormNum (headconst p)"
  by (induct p arbitrary: n0) auto

lemma monic_eqI:
  assumes np: "isnpolyh p n0"
  shows "INum (headconst p) * Ipoly bs (fst (monic p)) =
    (Ipoly bs p ::'a::{field_char_0, power})"
  unfolding monic_def Let_def
proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
  let ?h = "headconst p"
  assume pz: "p \ 0\<^sub>p"
  {
    assume hz: "INum ?h = (0::'a)"
    from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N"
      by simp_all
    from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N"
      by simp
    with headconst_zero[OF np] have "p = 0\<^sub>p"
      by blast
    with pz have False
      by blast
  }
  then show "INum (headconst p) = (0::'a) \ \p\\<^sub>p\<^bsup>bs\<^esup> = 0"
    by blast
qed

text \<open>polyneg is a negation and preserves normal forms\<close>

lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
  by (induct p rule: polyneg.induct) auto

lemma polyneg0: "isnpolyh p n \ (~\<^sub>p p) = 0\<^sub>p \ p = 0\<^sub>p"
  by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: Nneg_def)

lemma polyneg_polyneg: "isnpolyh p n0 \ ~\<^sub>p (~\<^sub>p p) = p"
  by (induct p arbitrary: n0 rule: polyneg.induct) auto

lemma polyneg_normh: "isnpolyh p n \ isnpolyh (polyneg p) n"
  by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: polyneg0)

lemma polyneg_norm: "isnpoly p \ isnpoly (polyneg p)"
  using isnpoly_def polyneg_normh by simp

text \<open>polysub is a substraction and preserves normal forms\<close>

lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p - Ipoly bs q"
  by (simp add: polysub_def)

lemma polysub_normh: "isnpolyh p n0 \ isnpolyh q n1 \ isnpolyh (polysub p q) (min n0 n1)"
  by (simp add: polysub_def polyneg_normh polyadd_normh)

lemma polysub_norm: "isnpoly p \ isnpoly q \ isnpoly (polysub p q)"
  using polyadd_norm polyneg_norm by (simp add: polysub_def)

lemma polysub_same_0[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "isnpolyh p n0 \ polysub p p = 0\<^sub>p"
  unfolding polysub_def split_def fst_conv snd_conv
  by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def])

lemma polysub_0:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "isnpolyh p n0 \ isnpolyh q n1 \ p -\<^sub>p q = 0\<^sub>p \ p = q"
  unfolding polysub_def split_def fst_conv snd_conv
  by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
    (auto simp: Nsub0[simplified Nsub_def] Let_def)

text \<open>polypow is a power function and preserves normal forms\<close>

lemma polypow[simp]: "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::field_char_0) ^ n"
proof (induct n rule: polypow.induct)
  case 1
  then show ?case by simp
next
  case (2 n)
  let ?q = "polypow ((Suc n) div 2) p"
  let ?d = "polymul ?q ?q"
  consider "odd (Suc n)" | "even (Suc n)" by auto
  then show ?case
  proof cases
    case odd: 1
    have *: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1"
      by arith
    from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)"
      by (simp add: Let_def)
    also have "\ = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2) * (Ipoly bs p)^(Suc n div 2)"
      using "2.hyps" by simp
    also have "\ = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
      by (simp only: power_add power_one_right) simp
    also have "\ = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
      by (simp only: *)
    finally show ?thesis
      unfolding numeral_2_eq_2 [symmetric]
      using odd_two_times_div_two_nat [OF odd] by simp
  next
    case even: 2
    from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d"
      by (simp add: Let_def)
    also have "\ = (Ipoly bs p) ^ (2 * (Suc n div 2))"
      using "2.hyps" by (simp only: mult_2 power_add) simp
    finally show ?thesis
      using even_two_times_div_two [OF even] by simp
  qed
qed

lemma polypow_normh:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "isnpolyh p n \ isnpolyh (polypow k p) n"
proof (induct k arbitrary: n rule: polypow.induct)
  case 1
  then show ?case by auto
next
  case (2 k n)
  let ?q = "polypow (Suc k div 2) p"
  let ?d = "polymul ?q ?q"
  from 2 have *: "isnpolyh ?q n" and **: "isnpolyh p n"
    by blast+
  from polymul_normh[OF * *] have dn: "isnpolyh ?d n"
    by simp
  from polymul_normh[OF ** dn] have on: "isnpolyh (polymul p ?d) n"
    by simp
  from dn on show ?case by (simp, unfold Let_def) auto
qed

lemma polypow_norm:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "isnpoly p \ isnpoly (polypow k p)"
  by (simp add: polypow_normh isnpoly_def)

text \<open>Finally the whole normalization\<close>

lemma polynate [simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::field_char_0)"
  by (induct p rule:polynate.induct) auto

lemma polynate_norm[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "isnpoly (polynate p)"
  by (induct p rule: polynate.induct)
     (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
      simp_all add: isnpoly_def)

text \<open>shift1\<close>

lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
  by (simp add: shift1_def)

lemma shift1_isnpoly:
  assumes "isnpoly p"
    and "p \ 0\<^sub>p"
  shows "isnpoly (shift1 p) "
  using assms by (simp add: shift1_def isnpoly_def)

lemma shift1_nz[simp]:"shift1 p \ 0\<^sub>p"
  by (simp add: shift1_def)

lemma funpow_shift1_isnpoly: "isnpoly p \ p \ 0\<^sub>p \ isnpoly (funpow n shift1 p)"
  by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)

lemma funpow_isnpolyh:
  assumes "\p. isnpolyh p n \ isnpolyh (f p) n"
    and "isnpolyh p n"
  shows "isnpolyh (funpow k f p) n"
  using assms by (induct k arbitrary: p) auto

lemma funpow_shift1:
  "(Ipoly bs (funpow n shift1 p) :: 'a :: field_char_0) =
    Ipoly bs (Mul (Pw (Bound 0) n) p)"
  by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)

lemma shift1_isnpolyh: "isnpolyh p n0 \ p \ 0\<^sub>p \ isnpolyh (shift1 p) 0"
  using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)

lemma funpow_shift1_1:
  "(Ipoly bs (funpow n shift1 p) :: 'a :: field_char_0) =
    Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
  by (simp add: funpow_shift1)

lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
  by (induct p rule: poly_cmul.induct) (auto simp add: field_simps)

lemma behead:
  assumes "isnpolyh p n"
  shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
    (Ipoly bs p :: 'a :: field_char_0)"
  using assms
proof (induct p arbitrary: n rule: behead.induct)
  case (1 c p n)
  then have pn: "isnpolyh p n" by simp
  from 1(1)[OF pn]
  have *: "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" .
  show ?case
  proof (cases "behead p = 0\<^sub>p")
    case True
    then show ?thesis
      using * by auto
  next
    case False
    then show ?thesis
      by (simp add: field_simps flip: *)
  qed
qed (auto simp add: Let_def)

lemma behead_isnpolyh:
  assumes "isnpolyh p n"
  shows "isnpolyh (behead p) n"
  using assms by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)

subsection \<open>Miscellaneous lemmas about indexes, decrementation, substitution  etc ...\<close>

lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \ polybound0 p"
proof (induct p arbitrary: n rule: poly.induct, auto, goal_cases)
  case prems: (1 c n p n')
  then have "n = Suc (n - 1)"
    by simp
  then have "isnpolyh p (Suc (n - 1))"
    using \<open>isnpolyh p n\<close> by simp
  with prems(2) show ?case
    by simp
qed

lemma isconstant_polybound0: "isnpolyh p n0 \ isconstant p \ polybound0 p"
  by (induct p arbitrary: n0 rule: isconstant.induct) (auto simp add: isnpolyh_polybound0)

lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \ p = 0\<^sub>p"
  by (induct p) auto

lemma decrpoly_normh: "isnpolyh p n0 \ polybound0 p \ isnpolyh (decrpoly p) (n0 - 1)"
  by (induct p arbitrary: n0) force+

lemma head_polybound0: "isnpolyh p n0 \ polybound0 (head p)"
  by (induct p  arbitrary: n0 rule: head.induct) (auto intro: isnpolyh_polybound0)

lemma polybound0_I:
  assumes "polybound0 a"
  shows "Ipoly (b # bs) a = Ipoly (b' # bs) a"
  using assms by (induct a rule: poly.induct) auto

lemma polysubst0_I: "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b # bs) a) # bs) t"
  by (induct t) simp_all

lemma polysubst0_I':
  assumes "polybound0 a"
  shows "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b' # bs) a) # bs) t"
  by (induct t) (simp_all add: polybound0_I[OF assms, where b="b" and b'="b'"])

lemma decrpoly:
  assumes "polybound0 t"
  shows "Ipoly (x # bs) t = Ipoly bs (decrpoly t)"
  using assms by (induct t rule: decrpoly.induct) simp_all

lemma polysubst0_polybound0:
  assumes "polybound0 t"
  shows "polybound0 (polysubst0 t a)"
  using assms by (induct a rule: poly.induct) auto

lemma degree0_polybound0: "isnpolyh p n \ degree p = 0 \ polybound0 p"
  by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0)

primrec maxindex :: "poly \ nat"
  where
    "maxindex (Bound n) = n + 1"
  | "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))"
  | "maxindex (Add p q) = max (maxindex p) (maxindex q)"
  | "maxindex (Sub p q) = max (maxindex p) (maxindex q)"
  | "maxindex (Mul p q) = max (maxindex p) (maxindex q)"
  | "maxindex (Neg p) = maxindex p"
  | "maxindex (Pw p n) = maxindex p"
  | "maxindex (C x) = 0"

definition wf_bs :: "'a list \ poly \ bool"
  where "wf_bs bs p \ length bs \ maxindex p"

lemma wf_bs_coefficients: "wf_bs bs p \ \c \ set (coefficients p). wf_bs bs c"
proof (induct p rule: coefficients.induct)
  case (1 c p)
  show ?case
  proof
    fix x
    assume "x \ set (coefficients (CN c 0 p))"
    then consider "x = c" | "x \ set (coefficients p)"
      by auto
    then show "wf_bs bs x"
    proof cases
      case prems: 1
      then show ?thesis
        using "1.prems" by (simp add: wf_bs_def)
    next
      case prems: 2
      from "1.prems" have "wf_bs bs p"
        by (simp add: wf_bs_def)
      with "1.hyps" prems show ?thesis
        by blast
    qed
  qed
qed simp_all

lemma maxindex_coefficients: "\c \ set (coefficients p). maxindex c \ maxindex p"
  by (induct p rule: coefficients.induct) auto

lemma wf_bs_I: "wf_bs bs p \ Ipoly (bs @ bs') p = Ipoly bs p"
  by (induct p) (auto simp add: nth_append wf_bs_def)

lemma take_maxindex_wf:
  assumes wf: "wf_bs bs p"
  shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p"
proof -
  let ?ip = "maxindex p"
  let ?tbs = "take ?ip bs"
  from wf have "length ?tbs = ?ip"
    unfolding wf_bs_def by simp
  then have wf': "wf_bs ?tbs p"
    unfolding wf_bs_def by  simp
  have eq: "bs = ?tbs @ drop ?ip bs"
    by simp
  from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis
    using eq by simp
qed

lemma decr_maxindex: "polybound0 p \ maxindex (decrpoly p) = maxindex p - 1"
  by (induct p) auto

lemma wf_bs_insensitive: "length bs = length bs' \ wf_bs bs p = wf_bs bs' p"
  by (simp add: wf_bs_def)

lemma wf_bs_insensitive': "wf_bs (x # bs) p = wf_bs (y # bs) p"
  by (simp add: wf_bs_def)

lemma wf_bs_coefficients': "\c \ set (coefficients p). wf_bs bs c \ wf_bs (x # bs) p"
  by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def)

lemma coefficients_Nil[simp]: "coefficients p \ []"
  by (induct p rule: coefficients.induct) simp_all

lemma coefficients_head: "last (coefficients p) = head p"
  by (induct p rule: coefficients.induct) auto

lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \ wf_bs (x # bs) p"
  unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto

lemma length_le_list_ex: "length xs \ n \ \ys. length (xs @ ys) = n"
  by (rule exI[where x="replicate (n - length xs) z" for z]) simp

lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \ isconstant p"
  by (simp add: isconstant_polybound0 isnpolyh_polybound0)

lemma wf_bs_polyadd: "\wf_bs bs p; wf_bs bs q\ \ wf_bs bs (p +\<^sub>p q)"
  by (induct p q rule: polyadd.induct) (auto simp add: Let_def wf_bs_def)

lemma wf_bs_polyul: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p *\<^sub>p q)"
proof (induct p q rule: polymul.induct)
  case (4 c n p c' n' p')
  then show ?case
    apply (simp add: wf_bs_def)
    by (metis "4.prems"(1) max.bounded_iff max_0L maxindex.simps(2,8) wf_bs_def wf_bs_polyadd)
qed (simp_all add: wf_bs_def)

lemma wf_bs_polyneg: "wf_bs bs p \ wf_bs bs (~\<^sub>p p)"
  by (induct p rule: polyneg.induct) (auto simp: wf_bs_def)

lemma wf_bs_polysub: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p -\<^sub>p q)"
  unfolding polysub_def split_def fst_conv snd_conv
  using wf_bs_polyadd wf_bs_polyneg by blast

subsection \<open>Canonicity of polynomial representation, see lemma isnpolyh_unique\<close>

definition "polypoly bs p = map (Ipoly bs) (coefficients p)"
definition "polypoly' bs p = map (Ipoly bs \ decrpoly) (coefficients p)"
definition "poly_nate bs p = map (Ipoly bs \ decrpoly) (coefficients (polynate p))"

lemma coefficients_normh: "isnpolyh p n0 \ \q \ set (coefficients p). isnpolyh q n0"
proof (induct p arbitrary: n0 rule: coefficients.induct)
  case (1 c p n0)
  have cp: "isnpolyh (CN c 0 p) n0"
    by fact
  then have norm: "isnpolyh c 0" "isnpolyh p 0" "p \ 0\<^sub>p" "n0 = 0"
    by (auto simp add: isnpolyh_mono[where n'=0])
  from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case
    by simp
qed auto

lemma coefficients_isconst: "isnpolyh p n \ \q \ set (coefficients p). isconstant q"
  by (induct p arbitrary: n rule: coefficients.induct) (auto simp add: isnpolyh_Suc_const)

lemma polypoly_polypoly':
  assumes np: "isnpolyh p n0"
  shows "polypoly (x # bs) p = polypoly' bs p"
proof -
  let ?cf = "set (coefficients p)"
  from coefficients_normh[OF np] have cn_norm: "\ q\ ?cf. isnpolyh q n0" .
  have "polybound0 q" if "q \ ?cf" for q
  proof -
    from that cn_norm have *: "isnpolyh q n0"
      by blast
    from coefficients_isconst[OF np] that have "isconstant q"
      by blast
    with isconstant_polybound0[OF *] show ?thesis
      by blast
  qed
  then have "\q \ ?cf. polybound0 q" ..
  then have "\q \ ?cf. Ipoly (x # bs) q = Ipoly bs (decrpoly q)"
    using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs]
    by auto
  then show ?thesis
    unfolding polypoly_def polypoly'_def by simp
qed

lemma polypoly_poly:
  assumes "isnpolyh p n0"
  shows "Ipoly (x # bs) p = poly (polypoly (x # bs) p) x"
  using assms
  by (induct p arbitrary: n0 bs rule: coefficients.induct) (auto simp add: polypoly_def)

lemma polypoly'_poly:
  assumes "isnpolyh p n0"
  shows "\p\\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x"
  using polypoly_poly[OF assms, simplified polypoly_polypoly'[OF assms]] .

lemma polypoly_poly_polybound0:
  assumes "isnpolyh p n0"
    and "polybound0 p"
  shows "polypoly bs p = [Ipoly bs p]"
  using assms
  unfolding polypoly_def
  by (cases p; use gr0_conv_Suc in force)

lemma head_isnpolyh: "isnpolyh p n0 \ isnpolyh (head p) n0"
  by (induct p rule: head.induct) auto

lemma headn_nz[simp]: "isnpolyh p n0 \ headn p m = 0\<^sub>p \ p = 0\<^sub>p"
  by (cases p) auto

lemma head_eq_headn0: "head p = headn p 0"
  by (induct p rule: head.induct) simp_all

lemma head_nz[simp]: "isnpolyh p n0 \ head p = 0\<^sub>p \ p = 0\<^sub>p"
  by (simp add: head_eq_headn0)

lemma isnpolyh_zero_iff:
  assumes nq: "isnpolyh p n0"
    and eq :"\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, power})"
  shows "p = 0\<^sub>p"
  using nq eq
proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
  case less
  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>
  show "p = 0\<^sub>p"
  proof (cases "maxindex p = 0")
    case True
    with np obtain c where "p = C c" by (cases p) auto
    with zp np show ?thesis by (simp add: wf_bs_def)
  next
    case nz: False
    let ?h = "head p"
    let ?hd = "decrpoly ?h"
    let ?ihd = "maxindex ?hd"
    from head_isnpolyh[OF np] head_polybound0[OF np]
    have h: "isnpolyh ?h n0" "polybound0 ?h"
      by simp_all
    then have nhd: "isnpolyh ?hd (n0 - 1)"
      using decrpoly_normh by blast

    from maxindex_coefficients[of p] coefficients_head[of p, symmetric]
    have mihn: "maxindex ?h \ maxindex p"
      by auto
    with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < maxindex p"
      by auto

    have "\?hd\\<^sub>p\<^bsup>bs\<^esup> = 0" if bs: "wf_bs bs ?hd" for bs :: "'a list"
    proof -
      let ?ts = "take ?ihd bs"
      let ?rs = "drop ?ihd bs"
      from bs have ts: "wf_bs ?ts ?hd"
        by (simp add: wf_bs_def)
      have bs_ts_eq: "?ts @ ?rs = bs"
        by simp
      from wf_bs_decrpoly[OF ts] have tsh: " \x. wf_bs (x # ?ts) ?h"
        by simp
      from ihd_lt_n have "\x. length (x # ?ts) \ maxindex p"
        by simp
      with length_le_list_ex obtain xs where xs: "length ((x # ?ts) @ xs) = maxindex p"
        by blast
      then have "\x. wf_bs ((x # ?ts) @ xs) p"
        by (simp add: wf_bs_def)
      with zp have "\x. Ipoly ((x # ?ts) @ xs) p = 0"
        by blast
      then have "\x. Ipoly (x # (?ts @ xs)) p = 0"
        by simp
      with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]
      have "\x. poly (polypoly' (?ts @ xs) p) x = poly [] x"
        by simp
      then have "poly (polypoly' (?ts @ xs) p) = poly []"
        by auto
      then have "\c \ set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
        using poly_zero[where ?'a='a] by (simp add: polypoly'_def)
      with coefficients_head[of p, symmetric]
      have *: "Ipoly (?ts @ xs) ?hd = 0"
        by simp
      from bs have wf'': "wf_bs ?ts ?hd"
        by (simp add: wf_bs_def)
      with * wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0"
        by simp
      with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq show ?thesis
        by simp
    qed
    then have hdz: "\bs. wf_bs bs ?hd \ \?hd\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)"
      by blast
    from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p"
      by blast
    then have "?h = 0\<^sub>p" by simp
    with head_nz[OF np] show ?thesis by simp
  qed
qed

lemma isnpolyh_unique:
  assumes np: "isnpolyh p n0"
    and nq: "isnpolyh q n1"
  shows "(\bs. \p\\<^sub>p\<^bsup>bs\<^esup> = (\q\\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,power})) \ p = q"
proof auto
  assume "\bs. (\p\\<^sub>p\<^bsup>bs\<^esup> ::'a) = \q\\<^sub>p\<^bsup>bs\<^esup>"
  then have "\bs.\p -\<^sub>p q\\<^sub>p\<^bsup>bs\<^esup>= (0::'a)"
    by simp
  then have "\bs. wf_bs bs (p -\<^sub>p q) \ \p -\<^sub>p q\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)"
    using wf_bs_polysub[where p=p and q=q] by auto
  with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq] show "p = q"
    by blast
qed

text \<open>Consequences of unicity on the algorithms for polynomial normalization.\<close>

lemma polyadd_commute:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
    and np: "isnpolyh p n0"
    and nq: "isnpolyh q n1"
  shows "p +\<^sub>p q = q +\<^sub>p p"
  using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]]
  by simp

lemma zero_normh: "isnpolyh 0\<^sub>p n"
  by simp

lemma one_normh: "isnpolyh (1)\<^sub>p n"
  by simp

lemma polyadd_0[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
    and np: "isnpolyh p n0"
  shows "p +\<^sub>p 0\<^sub>p = p"
    and "0\<^sub>p +\<^sub>p p = p"
  using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np]
    isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all

lemma polymul_1[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
    and np: "isnpolyh p n0"
  shows "p *\<^sub>p (1)\<^sub>p = p"
    and "(1)\<^sub>p *\<^sub>p p = p"
  using isnpolyh_unique[OF polymul_normh[OF np one_normh] np]
    isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all

lemma polymul_0[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
    and np: "isnpolyh p n0"
  shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p"
    and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
  using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh]
    isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all

lemma polymul_commute:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
    and np: "isnpolyh p n0"
    and nq: "isnpolyh q n1"
  shows "p *\<^sub>p q = q *\<^sub>p p"
  using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np],
    where ?'a = "'a::{field_char_0, power}"]
  by simp

declare polyneg_polyneg [simp]

lemma isnpolyh_polynate_id [simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
    and np: "isnpolyh p n0"
  shows "polynate p = p"
  using isnpolyh_unique[where ?'a= "'a::field_char_0",
      OF polynate_norm[of p, unfolded isnpoly_def] np]
    polynate[where ?'a = "'a::field_char_0"]
  by simp

lemma polynate_idempotent[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "polynate (polynate p) = polynate p"
  using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .

lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
  unfolding poly_nate_def polypoly'_def ..

lemma poly_nate_poly:
  "poly (poly_nate bs p) = (\x:: 'a ::field_char_0. \p\\<^sub>p\<^bsup>x # bs\<^esup>)"
  using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
  unfolding poly_nate_polypoly' by auto

subsection \<open>Heads, degrees and all that\<close>

lemma degree_eq_degreen0: "degree p = degreen p 0"
  by (induct p rule: degree.induct) simp_all

lemma degree_polyneg:
  assumes "isnpolyh p n"
  shows "degree (polyneg p) = degree p"
proof (induct p rule: polyneg.induct)
  case (2 c n p)
  then show ?case
  by simp (smt (verit) degree.elims degree.simps(1) poly.inject(8))
qed auto

lemma degree_polyadd:
  assumes np: "isnpolyh p n0"
    and nq: "isnpolyh q n1"
  shows "degree (p +\<^sub>p q) \ max (degree p) (degree q)"
  using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp

lemma degree_polysub:
  assumes np: "isnpolyh p n0"
    and nq: "isnpolyh q n1"
  shows "degree (p -\<^sub>p q) \ max (degree p) (degree q)"
proof-
  from nq have nq': "isnpolyh (~\<^sub>p q) n1"
    using polyneg_normh by simp
  from degree_polyadd[OF np nq'] show ?thesis
    by (simp add: polysub_def degree_polyneg[OF nq])
qed

lemma degree_polysub_samehead:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
    and np: "isnpolyh p n0"
    and nq: "isnpolyh q n1"
    and h: "head p = head q"
    and d: "degree p = degree q"
  shows "degree (p -\<^sub>p q) < degree p \ (p -\<^sub>p q = 0\<^sub>p)"
  unfolding polysub_def split_def fst_conv snd_conv
  using np nq h d
proof (induct p q rule: polyadd.induct)
  case (1 c c')
  then show ?case
    by (simp add: Nsub_def Nsub0[simplified Nsub_def])
next
  case (2 c c' n' p')
  from 2 have "degree (C c) = degree (CN c' n' p')"
    by simp
  then have nz: "n' > 0"
    by (cases n') auto
  then have "head (CN c' n' p') = CN c' n' p'"
    by (cases n') auto
  with 2 show ?case
    by simp
next
  case (3 c n p c')
  then have "degree (C c') = degree (CN c n p)"
    by simp
  then have nz: "n > 0"
    by (cases n) auto
  then have "head (CN c n p) = CN c n p"
    by (cases n) auto
  with 3 show ?case by simp
next
  case (4 c n p c' n' p')
  then have H:
    "isnpolyh (CN c n p) n0"
    "isnpolyh (CN c' n' p') n1"
    "head (CN c n p) = head (CN c' n' p')"
    "degree (CN c n p) = degree (CN c' n' p')"
    by simp_all
  then have degc: "degree c = 0" and degc': "degree c' = 0"
    by simp_all
  then have degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0"
    using H(1-2) degree_polyneg by auto
  from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')"
    by simp_all
  from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc'
  have degcmc': "degree (c +\<^sub>p ~\<^sub>pc') = 0"
    by simp
  from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'"
    by auto
  consider "n = n'" | "n < n'" | "n > n'"
    by arith
  then show ?case
  proof cases
    case nn': 1
    consider "n = 0" | "n > 0" by arith
    then show ?thesis
    proof cases
      case 1
      with 4 nn' show ?thesis
        by (auto simp add: Let_def degcmc')
    next
      case 2
      with nn' H(3) have "c = c'" and "p = p'"
        by (cases n; auto)+
      with nn' 4 show ?thesis
        using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv]
        using polysub_same_0[OF c'nh, simplified polysub_def]
        by (simp add: Let_def)
    qed
  next
    case nn': 2
    then have n'p: "n' > 0"
      by simp
    then have headcnp':"head (CN c' n' p') = CN c' n' p'"
      by (cases n') simp_all
    with 4 nn' have degcnp': "degree (CN c' n' p') = 0"
      and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')"
      by (cases n', simp_all)
    then have "n > 0"
      by (cases n) simp_all
    then have headcnp: "head (CN c n p) = CN c n p"
      by (cases n) auto
    from H(3) headcnp headcnp' nn' show ?thesis
      by auto
  next
    case nn': 3
    then have np: "n > 0" by simp
    then have headcnp:"head (CN c n p) = CN c n p"
      by (cases n) simp_all
    from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)"
      by simp
    from np have degcnp: "degree (CN c n p) = 0"
      by (cases n) simp_all
    with degcnpeq have "n' > 0"
      by (cases n') simp_all
    then have headcnp': "head (CN c' n' p') = CN c' n' p'"
      by (cases n') auto
    from H(3) headcnp headcnp' nn' show ?thesis by auto
  qed
qed auto

lemma shift1_head : "isnpolyh p n0 \ head (shift1 p) = head p"
  by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def)

lemma funpow_shift1_head: "isnpolyh p n0 \ p \ 0\<^sub>p \ head (funpow k shift1 p) = head p"
proof (induct k arbitrary: n0 p)
  case 0
  then show ?case
    by auto
next
  case (Suc k n0 p)
  then have "isnpolyh (shift1 p) 0"
    by (simp add: shift1_isnpolyh)
  with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
    and "head (shift1 p) = head p"
    by (simp_all add: shift1_head)
  then show ?case
    by (simp add: funpow_swap1)
qed

lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
  by (simp add: shift1_def)

lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p "
  by (induct k arbitrary: p) (auto simp add: shift1_degree)

lemma funpow_shift1_nz: "p \ 0\<^sub>p \ funpow n shift1 p \ 0\<^sub>p"
  by (induct n arbitrary: p) simp_all

lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \ head p = p"
  by (induct p arbitrary: n rule: degree.induct) auto
lemma headn_0[simp]: "isnpolyh p n \ m < n \ headn p m = p"
  by (induct p arbitrary: n rule: degreen.induct) auto
lemma head_isnpolyh_Suc': "n > 0 \ isnpolyh p n \ head p = p"
  by (induct p arbitrary: n rule: degree.induct) auto
lemma head_head[simp]: "isnpolyh p n0 \ head (head p) = head p"
  by (induct p rule: head.induct) auto

lemma polyadd_eq_const_degree:
  "isnpolyh p n0 \ isnpolyh q n1 \ polyadd p q = C c \ degree p = degree q"
  by (metis degree_eq_degreen0 polyadd_eq_const_degreen)

lemma polyadd_head_aux:
  assumes "isnpolyh p n0" "isnpolyh q n1"
  shows "head (p +\<^sub>p q)
           = (if degree p < degree q then head q
              else if degree p > degree q then head p else head (p +\<^sub>p q))"
  using assms
proof (induct p q rule: polyadd.induct)
  case (4 c n p c' n' p')
  then show ?case
    by (auto simp add: degree_eq_degreen0 Let_def; metis head_nz)
qed (auto simp: degree_eq_degreen0)

lemma polyadd_head:
  assumes "isnpolyh p n0" and "isnpolyh q n1" and "degree p \ degree q"
  shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)"
  by (meson assms nat_neq_iff polyadd_head_aux)

lemma polymul_head_polyeq:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "isnpolyh p n0 \ isnpolyh q n1 \ p \ 0\<^sub>p \ q \ 0\<^sub>p \ head (p *\<^sub>p q) = head p *\<^sub>p head q"
proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
  case (2 c c' n' p' n0 n1)
  then have "isnpolyh (head (CN c' n' p')) n1" "isnormNum c"
    by (simp_all add: head_isnpolyh)
  then show ?case
    using 2 by (cases n') auto
next
  case (3 c n p c' n0 n1)
  then have "isnpolyh (head (CN c n p)) n0" "isnormNum c'"
    by (simp_all add: head_isnpolyh)
  then show ?case
    using 3 by (cases n) auto
next
  case (4 c n p c' n' p' n0 n1)
  then have norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
    "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'"
    by simp_all
  consider "n < n'" | "n' < n" | "n' = n" by arith
  then show ?case
  proof cases
    case nn': 1
    then show ?thesis
      using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)]
      by (simp add: head_eq_headn0)
  next
    case nn': 2
    then show ?thesis
      using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)]
      by (simp add: head_eq_headn0)
  next
    case nn': 3
    from nn' polymul_normh[OF norm(5,4)]
    have ncnpc': "isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)
    from nn' polymul_normh[OF norm(5,3)] norm
    have ncnpp': "isnpolyh (CN c n p *\<^sub>p p') n" by simp
    from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6)
    have ncnpp0': "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
    from polyadd_normh[OF ncnpc' ncnpp0']
    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"
      by (simp add: min_def)
    consider "n > 0" | "n = 0" by auto
    then show ?thesis
    proof cases
      case np: 1
      with nn' head_isnpolyh_Suc'[OF np nth]
        head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
      show ?thesis by simp
    next
      case nz: 2
      from polymul_degreen[OF norm(5,4), where m="0"]
        polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
        norm(5,6) degree_npolyhCN[OF norm(6)]
      have dth: "degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))"
        by simp
      then have dth': "degree (CN c 0 p *\<^sub>p c') \ degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))"
        by simp
      from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
      show ?thesis
        using norm "4.hyps"(6)[OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] nn' nz
        by simp
    qed
  qed
qed simp_all

lemma degree_coefficients: "degree p = length (coefficients p) - 1"
  by (induct p rule: degree.induct) auto

lemma degree_head[simp]: "degree (head p) = 0"
  by (induct p rule: head.induct) auto

lemma degree_CN: "isnpolyh p n \ degree (CN c n p) \ 1 + degree p"
  by (cases n) simp_all

lemma degree_CN': "isnpolyh p n \ degree (CN c n p) \ degree p"
  by (cases n) simp_all

lemma polyadd_different_degree:
  "isnpolyh p n0 \ isnpolyh q n1 \ degree p \ degree q \
    degree (polyadd p q) = max (degree p) (degree q)"
  using polyadd_different_degreen degree_eq_degreen0 by simp

lemma degreen_polyneg: "isnpolyh p n0 \ degreen (~\<^sub>p p) m = degreen p m"
  by (induct p arbitrary: n0 rule: polyneg.induct) auto

lemma degree_polymul:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
    and np: "isnpolyh p n0"
    and nq: "isnpolyh q n1"
  shows "degree (p *\<^sub>p q) \ degree p + degree q"
  using polymul_degreen[OF np nq, where m="0"]  degree_eq_degreen0 by simp

lemma polyneg_degree: "isnpolyh p n \ degree (polyneg p) = degree p"
  by (induct p arbitrary: n rule: degree.induct) auto

lemma polyneg_head: "isnpolyh p n \ head (polyneg p) = polyneg (head p)"
  by (induct p arbitrary: n rule: degree.induct) auto

subsection \<open>Correctness of polynomial pseudo division\<close>

lemma polydivide_aux_properties:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
    and np: "isnpolyh p n0"
    and ns: "isnpolyh s n1"
    and ap: "head p = a"
    and ndp: "degree p = n"
    and pnz: "p \ 0\<^sub>p"
  shows "polydivide_aux a n p k s = (k', r) \ k' \ k \ (degree r = 0 \ degree r < degree p) \
    (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> (polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
  using ns
proof (induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
  case less
  let ?qths = "\q n1. isnpolyh q n1 \ (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
  let ?ths = "polydivide_aux a n p k s = (k', r) \ k \ k' \
    (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
  let ?b = "head s"
  let ?p' = "funpow (degree s - n) shift1 p"
  let ?xdn = "funpow (degree s - n) shift1 (1)\<^sub>p"
  let ?akk' = "a ^\<^sub>p (k' - k)"
  note ns = \<open>isnpolyh s n1\<close>
  from np have np0: "isnpolyh p 0"
    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp
  have np': "isnpolyh ?p' 0"
    using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="degree s - n"] isnpoly_def
    by simp
  have headp': "head ?p' = head p"
    using funpow_shift1_head[OF np pnz] by simp
  from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0"
    by (simp add: isnpoly_def)
  from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap
  have nakk':"isnpolyh ?akk' 0" by blast
  show ?ths
  proof (cases "s = 0\<^sub>p")
    case True
    with np polyadd_0 polymul_0 zero_normh show ?thesis
      by (metis degree.simps(2) nakk' polydivide_aux.simps prod.sel order.refl)
  next
    case sz: False
    show ?thesis
    proof (cases "degree s < n")
      case True
      then show ?thesis
        using ns ndp np polydivide_aux.simps
        apply clarsimp
        by (metis polyadd_0(2) polymul_0(1) polymul_1(2) zero_normh)
    next
      case dn': False
      then have dn: "degree s \ n"
        by arith
      have degsp': "degree s = degree ?p'"
        using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"]
        by simp
      show ?thesis
      proof (cases "?b = a")
        case ba: True
        then have headsp': "head s = head ?p'"
          using ap headp' by simp
        have nr: "isnpolyh (s -\<^sub>p ?p') 0"
          using polysub_normh[OF ns np'] by simp
        from degree_polysub_samehead[OF ns np' headsp' degsp']
        consider "degree (s -\<^sub>p ?p') < degree s" | "s -\<^sub>p ?p' = 0\<^sub>p" by auto
        then show ?thesis
        proof cases
          case deglt: 1
          from polydivide_aux.simps sz dn' ba
          have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
            by (simp add: Let_def)
          have "k \ k' \ (degree r = 0 \ degree r < degree p) \ (\nr. isnpolyh r nr) \ ?qths"
            if h1: "polydivide_aux a n p k s = (k', r)"
          proof -
            from less(1)[OF deglt nr, of k k' r] trans[OF eq[symmetric] h1]
            have kk': "k \ k'"
              and nr: "\nr. isnpolyh r nr"
              and dr: "degree r = 0 \ degree r < degree p"
              and q1: "\q nq. isnpolyh q nq \ a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"
              by auto
            from q1 obtain q n1 where nq: "isnpolyh q n1"
              and asp: "a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"
              by blast
            from nr obtain nr where nr': "isnpolyh r nr"
              by blast
            from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0"
              by simp
            from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
            have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
            from polyadd_normh[OF polymul_normh[OF np
              polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
            have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0"
              by simp
            from asp have "\bs :: 'a::field_char_0 list.
              Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)"
              by simp
            then have "\bs :: 'a::field_char_0 list.
              Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
              by (simp add: field_simps)
            then have "\bs :: 'a::field_char_0 list.
              Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) +
              Ipoly bs p * Ipoly bs q + Ipoly bs r"
              by (auto simp only: funpow_shift1_1)
            then have "\bs:: 'a::field_char_0 list.
              Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) +
              Ipoly bs q) + Ipoly bs r"
              by (simp add: field_simps)
            then have "\bs:: 'a::field_char_0 list.
              Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
              Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r)"
              by simp
            with isnpolyh_unique[OF nakks' nqr']
            have "a ^\<^sub>p (k' - k) *\<^sub>p s =
              p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r"
              by blast
            with nq' have ?qths
              apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q" in exI)
              apply (rule_tac x="0" in exI)
              apply simp
              done
            with kk' nr dr show ?thesis
              by blast
          qed
          then show ?thesis by blast
        next
          case spz: 2
          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::field_char_0"]
          have "\bs:: 'a::field_char_0 list. Ipoly bs s = Ipoly bs ?p'"
            by simp
          with np nxdn have "\bs:: 'a::field_char_0 list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
            by (simp only: funpow_shift1_1) simp
          then have sp': "s = ?xdn *\<^sub>p p"
            using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
            by blast
          have ?thesis if h1: "polydivide_aux a n p k s = (k', r)"
          proof -
            from sz dn' ba
            have "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
              by (simp add: Let_def polydivide_aux.simps)
            also have "\ = (k,0\<^sub>p)"
              using spz by (simp add: polydivide_aux.simps)
            finally have "(k', r) = (k, 0\<^sub>p)"
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.