src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 34915 7894c7dab132 parent 33268 02de0317f66f child 35046 1266f04f42ec
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Jan 10 18:41:07 2010 +0100
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Jan 10 18:43:45 2010 +0100
1.3 @@ -987,16 +987,14 @@
1.4    assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{ring_char_0,power,division_by_zero,field})"
1.5    shows "p = 0\<^sub>p"
1.6  using nq eq
1.7 -proof (induct n\<equiv>"maxindex p" arbitrary: p n0 rule: nat_less_induct)
1.8 -  fix n p n0
1.9 -  assume H: "\<forall>m<n. \<forall>p n0. isnpolyh p n0 \<longrightarrow>
1.10 -    (\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)) \<longrightarrow> m = maxindex p \<longrightarrow> p = 0\<^sub>p"
1.11 -    and np: "isnpolyh p n0" and zp: "\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" and n: "n = maxindex p"
1.12 -  {assume nz: "n = 0"
1.13 -    then obtain c where "p = C c" using n np by (cases p, auto)
1.14 +proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
1.15 +  case less
1.16 +  note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)`
1.17 +  {assume nz: "maxindex p = 0"
1.18 +    then obtain c where "p = C c" using np by (cases p, auto)
1.19      with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp}
1.20    moreover
1.21 -  {assume nz: "n \<noteq> 0"
1.22 +  {assume nz: "maxindex p \<noteq> 0"
1.23      let ?h = "head p"
1.24      let ?hd = "decrpoly ?h"
1.25      let ?ihd = "maxindex ?hd"
1.26 @@ -1005,24 +1003,23 @@
1.27      hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast
1.28
1.29      from maxindex_coefficients[of p] coefficients_head[of p, symmetric]
1.30 -    have mihn: "maxindex ?h \<le> n" unfolding n by auto
1.31 -    with decr_maxindex[OF h(2)] nz  have ihd_lt_n: "?ihd < n" by auto
1.32 +    have mihn: "maxindex ?h \<le> maxindex p" by auto
1.33 +    with decr_maxindex[OF h(2)] nz  have ihd_lt_n: "?ihd < maxindex p" by auto
1.34      {fix bs:: "'a list"  assume bs: "wf_bs bs ?hd"
1.35        let ?ts = "take ?ihd bs"
1.36        let ?rs = "drop ?ihd bs"
1.37        have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp
1.38        have bs_ts_eq: "?ts@ ?rs = bs" by simp
1.39        from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp
1.40 -      from ihd_lt_n have "ALL x. length (x#?ts) \<le> n" by simp
1.41 -      with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = n" by blast
1.42 -      hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" using n unfolding wf_bs_def by simp
1.43 +      from ihd_lt_n have "ALL x. length (x#?ts) \<le> maxindex p" by simp
1.44 +      with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast
1.45 +      hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" unfolding wf_bs_def by simp
1.46        with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast
1.47        hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp
1.48        with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]
1.49        have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
1.50        hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext)
1.51        hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
1.52 -        thm poly_zero
1.53          using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
1.55        have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
1.56 @@ -1031,7 +1028,7 @@
1.57        with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp }
1.58      then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast
1.59
1.60 -    from H[rule_format, OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast
1.61 +    from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast
1.62      hence "?h = 0\<^sub>p" by simp
1.63      with head_nz[OF np] have "p = 0\<^sub>p" by simp}
1.64    ultimately show "p = 0\<^sub>p" by blast
1.65 @@ -1357,8 +1354,8 @@
1.66    (polydivide_aux (a,n,p,k,s) = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p)
1.67            \<and> (\<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)))"
1.68    using ns
1.69 -proof(induct d\<equiv>"degree s" arbitrary: s k k' r n1 rule: nat_less_induct)
1.70 -  fix d s k k' r n1
1.71 +proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
1.72 +  case less
1.73    let ?D = "polydivide_aux_dom"
1.74    let ?dths = "?D (a, n, p, k, s)"
1.75    let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
1.76 @@ -1366,20 +1363,13 @@
1.77      \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1.78    let ?ths = "?dths \<and> ?qrths"
1.79    let ?b = "head s"
1.80 -  let ?p' = "funpow (d - n) shift1 p"
1.81 -  let ?xdn = "funpow (d - n) shift1 1\<^sub>p"
1.82 +  let ?p' = "funpow (degree s - n) shift1 p"
1.83 +  let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p"
1.84    let ?akk' = "a ^\<^sub>p (k' - k)"
1.85 -  assume H: "\<forall>m<d. \<forall>x xa xb xc xd.
1.86 -    isnpolyh x xd \<longrightarrow>
1.87 -    m = degree x \<longrightarrow> ?D (a, n, p, xa, x) \<and>
1.88 -    (polydivide_aux (a, n, p, xa, x) = (xb, xc) \<longrightarrow>
1.89 -    xa \<le> xb \<and> (degree xc = 0 \<or> degree xc < degree p) \<and>
1.90 -    (\<exists> nr. isnpolyh xc nr) \<and>
1.91 -    (\<exists>q n1. isnpolyh q n1 \<and> a ^\<^sub>p xb - xa *\<^sub>p x = p *\<^sub>p q +\<^sub>p xc))"
1.92 -    and ns: "isnpolyh s n1" and ds: "d = degree s"
1.93 +  note ns = `isnpolyh s n1`
1.94    from np have np0: "isnpolyh p 0"
1.95      using isnpolyh_mono[where n="n0" and n'="0" and p="p"]  by simp
1.96 -  have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="d -n"] isnpoly_def by simp
1.97 +  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
1.99    from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
1.100    from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap
1.101 @@ -1391,31 +1381,31 @@
1.102      hence ?ths using dom by blast}
1.103    moreover
1.104    {assume sz: "s \<noteq> 0\<^sub>p"
1.105 -    {assume dn: "d < n"
1.106 -      with sz ds  have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all)
1.107 -      from polydivide_aux.psimps[OF dom] sz dn ds
1.108 +    {assume dn: "degree s < n"
1.109 +      with sz have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all)
1.110 +      from polydivide_aux.psimps[OF dom] sz dn
1.111        have "?qrths" using ns ndp np by auto (rule exI[where x="0\<^sub>p"],simp)
1.112        with dom have ?ths by blast}
1.113      moreover
1.114 -    {assume dn': "\<not> d < n" hence dn: "d \<ge> n" by arith
1.115 +    {assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> n" by arith
1.116        have degsp': "degree s = degree ?p'"
1.117 -        using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
1.118 +        using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] by simp
1.119        {assume ba: "?b = a"
1.121          have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
1.123 -        have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
1.125 +        have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
1.126          moreover
1.127 -        {assume deglt:"degree (s -\<^sub>p ?p') < d"
1.128 -          from  H[rule_format, OF deglt nr,simplified]
1.129 +        {assume deglt:"degree (s -\<^sub>p ?p') < degree s"
1.130 +          from  less(1)[OF deglt nr]
1.131            have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast
1.132            have dom: ?dths apply (rule polydivide_aux_real_domintros)
1.133 -            using ba ds dn' domsp by simp_all
1.134 -          from polydivide_aux.psimps[OF dom] sz dn' ba ds
1.135 +            using ba dn' domsp by simp_all
1.136 +          from polydivide_aux.psimps[OF dom] sz dn' ba
1.137            have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
1.139            {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
1.140 -            from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
1.141 +            from less(1)[OF deglt nr, of k k' r]
1.142                trans[OF eq[symmetric] h1]
1.143              have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
1.144                and q1:"\<exists>q nq. isnpolyh q nq \<and> (a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r)" by auto
1.145 @@ -1434,19 +1424,19 @@
1.146                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.148              hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.149 -              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p)
1.150 +              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p)
1.151                + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.152                by (auto simp only: funpow_shift1_1)
1.153              hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.154 -              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p)
1.155 +              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p)
1.156                + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
1.157              hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.158 -              Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp
1.159 +              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
1.160              with isnpolyh_unique[OF nakks' nqr']
1.161              have "a ^\<^sub>p (k' - k) *\<^sub>p s =
1.162 -              p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast
1.163 +              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
1.164              hence ?qths using nq'
1.165 -              apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
1.166 +              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.167                apply (rule_tac x="0" in exI) by simp
1.168              with kk' nr dr have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1.169                by blast } hence ?qrths by blast
1.170 @@ -1456,25 +1446,23 @@
1.171            hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')"
1.172              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
1.173            have dom: ?dths apply (rule polydivide_aux_real_domintros)
1.174 -            using ba ds dn' domsp by simp_all
1.175 +            using ba dn' domsp by simp_all
1.176            from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{ring_char_0,division_by_zero,field}"]
1.177            have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
1.178            hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
1.179              by (simp only: funpow_shift1_1) simp
1.180            hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
1.181            {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
1.182 -            from polydivide_aux.psimps[OF dom] sz dn' ba ds
1.183 +            from polydivide_aux.psimps[OF dom] sz dn' ba
1.184              have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
1.186              also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
1.187              finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
1.188 -            with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
1.189 +            with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
1.190                polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
1.191                apply auto
1.192                apply (rule exI[where x="?xdn"])
1.193 -              apply auto
1.194 -              apply (rule polymul_commute)
1.195 -              apply simp_all
1.196 +              apply (auto simp add: polymul_commute[of p])
1.197                done}
1.198            with dom have ?ths by blast}
1.199          ultimately have ?ths by blast }
1.200 @@ -1488,31 +1476,30 @@
1.202              funpow_shift1_nz[OF pnz] by simp_all
1.205 +          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.206          have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')"
1.210          from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
1.211            head_nz[OF np] pnz sz ap[symmetric]
1.212 -          funpow_shift1_nz[OF pnz, where n="d - n"]
1.213 +          funpow_shift1_nz[OF pnz, where n="degree s - n"]
1.215 -          ndp ds[symmetric] dn
1.216 +          ndp dn
1.217          have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
1.218            by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
1.219 -        {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
1.220 +        {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s"
1.221            have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
1.222 -            using H[rule_format, OF dth nth, simplified] by blast
1.223 -          have dom: ?dths
1.224 -            using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)
1.225 -            using ba ds dn'  by simp_all
1.226 +            using less(1)[OF dth nth] by blast
1.227 +          have dom: ?dths using ba dn' th
1.228 +            by - (rule polydivide_aux_real_domintros, simp_all)
1.230            ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
1.231            {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
1.232 -            from h1  polydivide_aux.psimps[OF dom] sz dn' ba ds
1.233 +            from h1  polydivide_aux.psimps[OF dom] sz dn' ba
1.234              have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
1.236 -            with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
1.237 +            with less(1)[OF dth nasbp', of "Suc k" k' r]
1.238              obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq"
1.239                and dr: "degree r = 0 \<or> degree r < degree p"
1.240                and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto
1.241 @@ -1524,7 +1511,7 @@
1.242              hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r"
1.243                by (simp add: ring_simps power_Suc)
1.244              hence "Ipoly bs a ^ (k' - k)  * Ipoly bs s = 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.245 -              by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
1.246 +              by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
1.247              hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
1.249              hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.250 @@ -1546,13 +1533,13 @@
1.251          {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
1.252            hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))"
1.253              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
1.254 -          have dom: ?dths using sz ba dn' ds domsp
1.255 +          have dom: ?dths using sz ba dn' domsp
1.256              by - (rule polydivide_aux_real_domintros, simp_all)
1.257            {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
1.258              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
1.259            have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
1.260            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p"
1.261 -            by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
1.262 +            by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
1.263            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
1.264          }
1.265          hence hth: "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
1.266 @@ -1562,7 +1549,7 @@
1.267                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
1.268                simplified ap] by simp
1.269            {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
1.270 -          from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp]
1.271 +          from h1 sz ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp]
1.272            have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
1.273            with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
1.274              polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
1.275 @@ -1573,7 +1560,7 @@
1.276          hence ?qrths by blast
1.277          with dom have ?ths by blast}
1.278          ultimately have ?ths 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.279 -          head_nz[OF np] pnz sz ap[symmetric] ds[symmetric]
1.280 +          head_nz[OF np] pnz sz ap[symmetric]
1.281            by (simp add: degree_eq_degreen0[symmetric]) blast }
1.282        ultimately have ?ths by blast
1.283      }
```