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.54        with coefficients_head[of p, symmetric]
    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.98    have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] 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.120          hence headsp': "head s = head ?p'" using ap headp' by simp
   1.121          have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
   1.122 -        from ds degree_polysub_samehead[OF ns np' headsp' degsp']
   1.123 -        have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
   1.124 +        from degree_polysub_samehead[OF ns np' headsp' degsp']
   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.138              by (simp add: Let_def)
   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.147                by (simp add: ring_simps)
   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.185                by (simp add: Let_def)
   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.201              polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
   1.202              funpow_shift1_nz[OF pnz] by simp_all
   1.203          from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
   1.204 -          polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
   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.207            using head_head[OF ns] funpow_shift1_head[OF np pnz]
   1.208              polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
   1.209            by (simp add: ap)
   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.214            polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"]  head_nz[OF ns]
   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.229            from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
   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.235                by (simp add: Let_def)
   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.248                by (simp add: ring_simps)}
   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      }