src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 33268 02de0317f66f parent 33154 daa6ddece9f0 child 34915 7894c7dab132
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Oct 28 00:23:39 2009 +0100
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Oct 28 00:24:38 2009 +0100
1.3 @@ -391,7 +391,7 @@
1.4    {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
1.5      moreover {assume "n < n'" with prems have ?case by simp }
1.6      moreover {assume eq: "n = n'" hence ?case using prems
1.7 -	by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }
1.8 +        by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }
1.9      ultimately have ?case by blast}
1.10    ultimately show ?case by blast
1.11  qed simp_all
1.12 @@ -413,10 +413,10 @@
1.13        by simp_all
1.14      {assume "?c = 0\<^sub>N" hence ?case by auto}
1.15        moreover {assume cnz: "?c \<noteq> 0\<^sub>N"
1.16 -	from "2.hyps"(1)[rule_format,where xb="n'",  OF cnz n(1) n(3)]
1.17 -	  "2.hyps"(2)[rule_format, where x="Suc n'"
1.18 -	  and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
1.19 -	  by (auto simp add: min_def)}
1.20 +        from "2.hyps"(1)[rule_format,where xb="n'",  OF cnz n(1) n(3)]
1.21 +          "2.hyps"(2)[rule_format, where x="Suc n'"
1.22 +          and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
1.23 +          by (auto simp add: min_def)}
1.24        ultimately show ?case by blast
1.25    next
1.26      case (2 n0 n1) thus ?case by auto
1.27 @@ -431,10 +431,10 @@
1.28        by simp_all
1.29      {assume "?c' = 0\<^sub>N" hence ?case by auto}
1.30        moreover {assume cnz: "?c' \<noteq> 0\<^sub>N"
1.31 -	from "3.hyps"(1)[rule_format,where xb="n",  OF cnz n(3) n(1)]
1.32 -	  "3.hyps"(2)[rule_format, where x="Suc n"
1.33 -	  and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
1.34 -	  by (auto simp add: min_def)}
1.35 +        from "3.hyps"(1)[rule_format,where xb="n",  OF cnz n(3) n(1)]
1.36 +          "3.hyps"(2)[rule_format, where x="Suc n"
1.37 +          and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
1.38 +          by (auto simp add: min_def)}
1.39        ultimately show ?case by blast
1.40    next
1.41      case (2 n0 n1) thus ?case apply auto done
1.42 @@ -446,32 +446,32 @@
1.43      {fix n0 n1
1.44        assume "isnpolyh ?cnp n0" and "isnpolyh ?cnp' n1"
1.45        hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'"
1.46 -	and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)"
1.47 -	and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
1.48 -	and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
1.49 -	by simp_all
1.50 +        and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)"
1.51 +        and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
1.52 +        and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
1.53 +        by simp_all
1.54        have "n < n' \<or> n' < n \<or> n' = n" by auto
1.55        moreover
1.56        {assume nn': "n < n'"
1.57 -	with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"]
1.58 -	  "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
1.59 -	have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
1.60 -	  by (simp add: min_def) }
1.61 +        with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"]
1.62 +          "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
1.63 +        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
1.64 +          by (simp add: min_def) }
1.65        moreover
1.66
1.67        {assume nn': "n > n'" hence stupid: "n' < n \<and> \<not> n < n'" by arith
1.68 -	with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
1.69 -	  "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"]
1.70 -	  nn' nn0 nn1 cnp'
1.71 -	have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
1.72 -	  by (cases "Suc n' = n", simp_all add: min_def)}
1.73 +        with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
1.74 +          "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"]
1.75 +          nn' nn0 nn1 cnp'
1.76 +        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
1.77 +          by (cases "Suc n' = n", simp_all add: min_def)}
1.78        moreover
1.79        {assume nn': "n' = n" hence stupid: "\<not> n' < n \<and> \<not> n < n'" by arith
1.80 -	from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
1.81 -	  "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
1.82 -
1.83 -	have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
1.84 -	  by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
1.85 +        from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
1.86 +          "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
1.87 +
1.88 +        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
1.89 +          by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
1.90        ultimately show "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" by blast }
1.91      note th = this
1.92      {fix n0 n1 m
1.93 @@ -484,86 +484,86 @@
1.94        have "n'<n \<or> n < n' \<or> n' = n" by auto
1.95        moreover
1.96        {assume "n' < n \<or> n < n'"
1.97 -	with "4.hyps" np np' m
1.98 -	have ?eq apply (cases "n' < n", simp_all)
1.99 -	apply (erule allE[where x="n"],erule allE[where x="n"],auto)
1.100 -	done }
1.101 +        with "4.hyps" np np' m
1.102 +        have ?eq apply (cases "n' < n", simp_all)
1.103 +        apply (erule allE[where x="n"],erule allE[where x="n"],auto)
1.104 +        done }
1.105        moreover
1.106        {assume nn': "n' = n"  hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith
1.107 - 	from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
1.108 -	  "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"]
1.109 -	  np np' nn'
1.110 -	have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
1.111 -	  "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
1.112 -	  "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
1.113 -	  "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
1.114 -	{assume mn: "m = n"
1.115 -	  from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
1.116 -	    "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
1.117 -	  have degs:  "degreen (?cnp *\<^sub>p c') n =
1.118 -	    (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
1.119 -	    "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
1.120 -	  from degs norm
1.121 -	  have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
1.122 -	  hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
1.123 -	    by simp
1.124 -	  have nmin: "n \<le> min n n" by (simp add: min_def)
1.125 -	  from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
1.126 -	  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
1.127 -	  from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
1.128 -	    "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
1.129 -	    mn norm m nn' deg
1.130 -	  have ?eq by simp}
1.131 -	moreover
1.132 -	{assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
1.133 -	  from nn' m np have max1: "m \<le> max n n"  by simp
1.134 -	  hence min1: "m \<le> min n n" by simp
1.135 -	  hence min2: "m \<le> min n (Suc n)" by simp
1.136 -	  {assume "c' = 0\<^sub>p"
1.137 -	    from `c' = 0\<^sub>p` have ?eq
1.138 -	      using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
1.139 -	    "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
1.140 -	      apply simp
1.141 -	      done}
1.142 -	  moreover
1.143 -	  {assume cnz: "c' \<noteq> 0\<^sub>p"
1.144 -	    from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
1.145 -	      "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
1.146 -	      degreen_polyadd[OF norm(3,6) max1]
1.147 +        from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
1.148 +          "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"]
1.149 +          np np' nn'
1.150 +        have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
1.151 +          "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
1.152 +          "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
1.153 +          "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
1.154 +        {assume mn: "m = n"
1.155 +          from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
1.156 +            "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
1.157 +          have degs:  "degreen (?cnp *\<^sub>p c') n =
1.158 +            (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
1.159 +            "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
1.160 +          from degs norm
1.161 +          have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
1.162 +          hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
1.163 +            by simp
1.164 +          have nmin: "n \<le> min n n" by (simp add: min_def)
1.165 +          from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
1.166 +          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
1.167 +          from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
1.168 +            "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
1.169 +            mn norm m nn' deg
1.170 +          have ?eq by simp}
1.171 +        moreover
1.172 +        {assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
1.173 +          from nn' m np have max1: "m \<le> max n n"  by simp
1.174 +          hence min1: "m \<le> min n n" by simp
1.175 +          hence min2: "m \<le> min n (Suc n)" by simp
1.176 +          {assume "c' = 0\<^sub>p"
1.177 +            from `c' = 0\<^sub>p` have ?eq
1.178 +              using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
1.179 +            "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
1.180 +              apply simp
1.181 +              done}
1.182 +          moreover
1.183 +          {assume cnz: "c' \<noteq> 0\<^sub>p"
1.184 +            from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
1.185 +              "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
1.186 +              degreen_polyadd[OF norm(3,6) max1]
1.187
1.188 -	    have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m
1.189 -	      \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
1.190 -	      using mn nn' cnz np np' by simp
1.191 -	    with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
1.192 -	      "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
1.193 -	      degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
1.194 -	  ultimately have ?eq by blast }
1.195 -	ultimately have ?eq by blast}
1.196 +            have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m
1.197 +              \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
1.198 +              using mn nn' cnz np np' by simp
1.199 +            with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
1.200 +              "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
1.201 +              degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
1.202 +          ultimately have ?eq by blast }
1.203 +        ultimately have ?eq by blast}
1.204        ultimately show ?eq by blast}
1.205      note degth = this
1.206      { case (2 n0 n1)
1.207        hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1"
1.208 -	and m: "m \<le> min n0 n1" by simp_all
1.209 +        and m: "m \<le> min n0 n1" by simp_all
1.210        hence mn: "m \<le> n" by simp
1.211        let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
1.212        {assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
1.213 -	hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
1.214 -	from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"]
1.215 -	  "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"]
1.216 -	  np np' C(2) mn
1.217 -	have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
1.218 -	  "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
1.219 -	  "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
1.220 -	  "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"
1.221 -	  "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
1.222 -	    "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
1.223 -	  by (simp_all add: min_def)
1.224 -
1.225 -	  from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
1.226 -	  have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
1.227 -	    using norm by simp
1.228 -	from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"]  degneq
1.229 -	have "False" by simp }
1.230 +        hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
1.231 +        from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"]
1.232 +          "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"]
1.233 +          np np' C(2) mn
1.234 +        have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
1.235 +          "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
1.236 +          "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
1.237 +          "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"
1.238 +          "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
1.239 +            "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
1.240 +          by (simp_all add: min_def)
1.241 +
1.242 +          from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
1.243 +          have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
1.244 +            using norm by simp
1.245 +        from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"]  degneq
1.246 +        have "False" by simp }
1.247        thus ?case using "4.hyps" by clarsimp}
1.248  qed auto
1.249
1.250 @@ -1022,8 +1022,8 @@
1.251        have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
1.252        hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext)
1.253        hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
1.254 -	thm poly_zero
1.255 -	using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
1.256 +        thm poly_zero
1.257 +        using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
1.258        with coefficients_head[of p, symmetric]
1.259        have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
1.260        from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp
1.261 @@ -1272,18 +1272,18 @@
1.262        by (simp add: min_def)
1.263      {assume np: "n > 0"
1.264        with nn' head_isnpolyh_Suc'[OF np nth]
1.265 -	head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
1.266 +        head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
1.267        have ?case by simp}
1.268      moreover
1.269      {moreover assume nz: "n = 0"
1.270        from polymul_degreen[OF norm(5,4), where m="0"]
1.271 -	polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
1.272 +        polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
1.273        norm(5,6) degree_npolyhCN[OF norm(6)]
1.274      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
1.275      hence dth':"degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
1.276      from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
1.277      have ?case   using norm prems(2)[rule_format, OF stupid norm(5,3)]
1.278 -	prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
1.279 +        prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
1.280      ultimately have ?case by (cases n) auto}
1.281    ultimately show ?case by blast
1.282  qed simp_all
1.283 @@ -1399,182 +1399,182 @@
1.284      moreover
1.285      {assume dn': "\<not> d < n" hence dn: "d \<ge> n" by arith
1.286        have degsp': "degree s = degree ?p'"
1.287 -	using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
1.288 +        using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
1.289        {assume ba: "?b = a"
1.290 -	hence headsp': "head s = head ?p'" using ap headp' by simp
1.291 -	have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
1.292 -	from ds degree_polysub_samehead[OF ns np' headsp' degsp']
1.293 -	have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
1.294 -	moreover
1.295 -	{assume deglt:"degree (s -\<^sub>p ?p') < d"
1.296 -	  from  H[rule_format, OF deglt nr,simplified]
1.297 -	  have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast
1.298 -	  have dom: ?dths apply (rule polydivide_aux_real_domintros)
1.299 -	    using ba ds dn' domsp by simp_all
1.300 -	  from polydivide_aux.psimps[OF dom] sz dn' ba ds
1.301 -	  have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
1.302 -	    by (simp add: Let_def)
1.303 -	  {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
1.304 -	    from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
1.305 -	      trans[OF eq[symmetric] h1]
1.306 -	    have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
1.307 -	      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.308 -	    from q1 obtain q n1 where nq: "isnpolyh q n1"
1.309 -	      and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"  by blast
1.310 -	    from nr obtain nr where nr': "isnpolyh r nr" by blast
1.311 -	    from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp
1.312 -	    from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
1.313 -	    have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
1.314 -	    from polyadd_normh[OF polymul_normh[OF np
1.315 -	      polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
1.316 -	    have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp
1.317 -	    from asp have "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) =
1.318 -	      Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
1.319 -	    hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
1.320 -	      Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.321 -	      by (simp add: ring_simps)
1.322 -	    hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.323 -	      Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p)
1.324 -	      + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.325 -	      by (auto simp only: funpow_shift1_1)
1.326 -	    hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.327 -	      Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p)
1.328 -	      + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
1.329 -	    hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.330 -	      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.331 -	    with isnpolyh_unique[OF nakks' nqr']
1.332 -	    have "a ^\<^sub>p (k' - k) *\<^sub>p s =
1.333 -	      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.334 -	    hence ?qths using nq'
1.335 -	      apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
1.336 -	      apply (rule_tac x="0" in exI) by simp
1.337 -	    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.338 -	      by blast } hence ?qrths by blast
1.339 -	  with dom have ?ths by blast}
1.340 -	moreover
1.341 -	{assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
1.342 -	  hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')"
1.343 -	    apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
1.344 -	  have dom: ?dths apply (rule polydivide_aux_real_domintros)
1.345 -	    using ba ds dn' domsp by simp_all
1.346 -	  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.347 -	  have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
1.348 -	  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.349 -	    by (simp only: funpow_shift1_1) simp
1.350 -	  hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
1.351 -	  {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
1.352 -	    from polydivide_aux.psimps[OF dom] sz dn' ba ds
1.353 -	    have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
1.354 -	      by (simp add: Let_def)
1.355 -	    also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
1.356 -	    finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
1.357 -	    with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
1.358 -	      polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
1.359 -	      apply auto
1.360 -	      apply (rule exI[where x="?xdn"])
1.361 -	      apply auto
1.362 -	      apply (rule polymul_commute)
1.363 -	      apply simp_all
1.364 -	      done}
1.365 -	  with dom have ?ths by blast}
1.366 -	ultimately have ?ths by blast }
1.367 +        hence headsp': "head s = head ?p'" using ap headp' by simp
1.368 +        have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
1.369 +        from ds degree_polysub_samehead[OF ns np' headsp' degsp']
1.370 +        have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
1.371 +        moreover
1.372 +        {assume deglt:"degree (s -\<^sub>p ?p') < d"
1.373 +          from  H[rule_format, OF deglt nr,simplified]
1.374 +          have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast
1.375 +          have dom: ?dths apply (rule polydivide_aux_real_domintros)
1.376 +            using ba ds dn' domsp by simp_all
1.377 +          from polydivide_aux.psimps[OF dom] sz dn' ba ds
1.378 +          have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
1.379 +            by (simp add: Let_def)
1.380 +          {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
1.381 +            from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
1.382 +              trans[OF eq[symmetric] h1]
1.383 +            have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
1.384 +              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.385 +            from q1 obtain q n1 where nq: "isnpolyh q n1"
1.386 +              and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"  by blast
1.387 +            from nr obtain nr where nr': "isnpolyh r nr" by blast
1.388 +            from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp
1.389 +            from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
1.390 +            have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
1.391 +            from polyadd_normh[OF polymul_normh[OF np
1.392 +              polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
1.393 +            have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp
1.394 +            from asp have "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) =
1.395 +              Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
1.396 +            hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
1.397 +              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.398 +              by (simp add: ring_simps)
1.399 +            hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.400 +              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p)
1.401 +              + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.402 +              by (auto simp only: funpow_shift1_1)
1.403 +            hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.404 +              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p)
1.405 +              + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
1.406 +            hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.407 +              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.408 +            with isnpolyh_unique[OF nakks' nqr']
1.409 +            have "a ^\<^sub>p (k' - k) *\<^sub>p s =
1.410 +              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.411 +            hence ?qths using nq'
1.412 +              apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
1.413 +              apply (rule_tac x="0" in exI) by simp
1.414 +            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.415 +              by blast } hence ?qrths by blast
1.416 +          with dom have ?ths by blast}
1.417 +        moreover
1.418 +        {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
1.419 +          hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')"
1.420 +            apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
1.421 +          have dom: ?dths apply (rule polydivide_aux_real_domintros)
1.422 +            using ba ds dn' domsp by simp_all
1.423 +          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.424 +          have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
1.425 +          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.426 +            by (simp only: funpow_shift1_1) simp
1.427 +          hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
1.428 +          {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
1.429 +            from polydivide_aux.psimps[OF dom] sz dn' ba ds
1.430 +            have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
1.431 +              by (simp add: Let_def)
1.432 +            also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
1.433 +            finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
1.434 +            with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
1.435 +              polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
1.436 +              apply auto
1.437 +              apply (rule exI[where x="?xdn"])
1.438 +              apply auto
1.439 +              apply (rule polymul_commute)
1.440 +              apply simp_all
1.441 +              done}
1.442 +          with dom have ?ths by blast}
1.443 +        ultimately have ?ths by blast }
1.444        moreover
1.445        {assume ba: "?b \<noteq> a"
1.446 -	from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns]
1.447 -	  polymul_normh[OF head_isnpolyh[OF ns] np']]
1.448 -	have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def)
1.449 -	have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p"
1.450 -	  using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns]
1.451 -	    polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
1.452 -	    funpow_shift1_nz[OF pnz] by simp_all
1.453 -	from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
1.454 -	  polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
1.455 -	have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')"
1.456 -	  using head_head[OF ns] funpow_shift1_head[OF np pnz]
1.457 -	    polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
1.458 -	  by (simp add: ap)
1.459 -	from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
1.460 -	  head_nz[OF np] pnz sz ap[symmetric]
1.461 -	  funpow_shift1_nz[OF pnz, where n="d - n"]
1.462 -	  polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"]  head_nz[OF ns]
1.463 -	  ndp ds[symmetric] dn
1.464 -	have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
1.465 -	  by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
1.466 -	{assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
1.467 -	  have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
1.468 -	    using H[rule_format, OF dth nth, simplified] by blast
1.469 -	  have dom: ?dths
1.470 -	    using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)
1.471 -	    using ba ds dn'  by simp_all
1.472 -	  from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
1.473 -	  ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
1.474 -	  {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
1.475 -	    from h1  polydivide_aux.psimps[OF dom] sz dn' ba ds
1.476 -	    have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
1.477 -	      by (simp add: Let_def)
1.478 -	    with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
1.479 -	    obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq"
1.480 -	      and dr: "degree r = 0 \<or> degree r < degree p"
1.481 -	      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.482 -	    from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
1.483 -	    {fix bs:: "'a::{ring_char_0,division_by_zero,field} list"
1.484 -
1.485 -	    from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
1.486 -	    have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
1.487 -	    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.488 -	      by (simp add: ring_simps power_Suc)
1.489 -	    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.490 -	      by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
1.491 -	    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.492 -	      by (simp add: ring_simps)}
1.493 -	    hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.494 -	      Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto
1.495 -	    let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
1.496 -	    from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap ] nxdn]]
1.497 -	    have nqw: "isnpolyh ?q 0" by simp
1.498 -	    from ieq isnpolyh_unique[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - k"] ns, simplified ap] polyadd_normh[OF polymul_normh[OF np nqw] nr]]
1.499 -	    have asth: "(a ^\<^sub>p (k' - k) *\<^sub>p s) = p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r" by blast
1.500 -	    from dr kk' nr h1 asth nqw have ?qrths apply simp
1.501 -	      apply (rule conjI)
1.502 -	      apply (rule exI[where x="nr"], simp)
1.503 -	      apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
1.504 -	      apply (rule exI[where x="0"], simp)
1.505 -	      done}
1.506 -	  hence ?qrths by blast
1.507 -	  with dom have ?ths by blast}
1.508 -	moreover
1.509 -	{assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
1.510 -	  hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))"
1.511 -	    apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
1.512 -	  have dom: ?dths using sz ba dn' ds domsp
1.513 -	    by - (rule polydivide_aux_real_domintros, simp_all)
1.514 -	  {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
1.515 -	    from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
1.516 -	  have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
1.517 -	  hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p"
1.518 -	    by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
1.519 -	  hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
1.520 -	}
1.521 -	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.522 -	  from hth
1.523 -	  have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
1.524 -	    using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.525 +        from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns]
1.526 +          polymul_normh[OF head_isnpolyh[OF ns] np']]
1.527 +        have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def)
1.528 +        have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p"
1.529 +          using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns]
1.530 +            polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
1.531 +            funpow_shift1_nz[OF pnz] by simp_all
1.532 +        from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
1.533 +          polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
1.534 +        have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')"
1.535 +          using head_head[OF ns] funpow_shift1_head[OF np pnz]
1.536 +            polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
1.537 +          by (simp add: ap)
1.538 +        from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
1.539 +          head_nz[OF np] pnz sz ap[symmetric]
1.540 +          funpow_shift1_nz[OF pnz, where n="d - n"]
1.541 +          polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"]  head_nz[OF ns]
1.542 +          ndp ds[symmetric] dn
1.543 +        have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
1.544 +          by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
1.545 +        {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
1.546 +          have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
1.547 +            using H[rule_format, OF dth nth, simplified] by blast
1.548 +          have dom: ?dths
1.549 +            using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)
1.550 +            using ba ds dn'  by simp_all
1.551 +          from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
1.552 +          ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
1.553 +          {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
1.554 +            from h1  polydivide_aux.psimps[OF dom] sz dn' ba ds
1.555 +            have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
1.556 +              by (simp add: Let_def)
1.557 +            with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
1.558 +            obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq"
1.559 +              and dr: "degree r = 0 \<or> degree r < degree p"
1.560 +              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.561 +            from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
1.562 +            {fix bs:: "'a::{ring_char_0,division_by_zero,field} list"
1.563 +
1.564 +            from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
1.565 +            have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
1.566 +            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.567 +              by (simp add: ring_simps power_Suc)
1.568 +            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.569 +              by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
1.570 +            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.571 +              by (simp add: ring_simps)}
1.572 +            hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.573 +              Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto
1.574 +            let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
1.575 +            from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap ] nxdn]]
1.576 +            have nqw: "isnpolyh ?q 0" by simp
1.577 +            from ieq isnpolyh_unique[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - k"] ns, simplified ap] polyadd_normh[OF polymul_normh[OF np nqw] nr]]
1.578 +            have asth: "(a ^\<^sub>p (k' - k) *\<^sub>p s) = p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r" by blast
1.579 +            from dr kk' nr h1 asth nqw have ?qrths apply simp
1.580 +              apply (rule conjI)
1.581 +              apply (rule exI[where x="nr"], simp)
1.582 +              apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
1.583 +              apply (rule exI[where x="0"], simp)
1.584 +              done}
1.585 +          hence ?qrths by blast
1.586 +          with dom have ?ths by blast}
1.587 +        moreover
1.588 +        {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
1.589 +          hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))"
1.590 +            apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
1.591 +          have dom: ?dths using sz ba dn' ds domsp
1.592 +            by - (rule polydivide_aux_real_domintros, simp_all)
1.593 +          {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
1.594 +            from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
1.595 +          have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
1.596 +          hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p"
1.597 +            by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
1.598 +          hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
1.599 +        }
1.600 +        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.601 +          from hth
1.602 +          have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
1.603 +            using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.604                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
1.605 -	      simplified ap] by simp
1.606 -	  {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
1.607 -	  from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp]
1.608 -	  have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
1.609 -	  with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
1.610 -	    polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
1.611 -	  have ?qrths apply (clarsimp simp add: Let_def)
1.612 -	    apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
1.613 -	    apply (rule exI[where x="0"], simp)
1.614 -	    done}
1.615 -	hence ?qrths by blast
1.616 -	with dom have ?ths by blast}
1.617 -	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.618 -	  head_nz[OF np] pnz sz ap[symmetric] ds[symmetric]
1.619 -	  by (simp add: degree_eq_degreen0[symmetric]) blast }
1.620 +              simplified ap] by simp
1.621 +          {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
1.622 +          from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp]
1.623 +          have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
1.624 +          with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
1.625 +            polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
1.626 +          have ?qrths apply (clarsimp simp add: Let_def)
1.627 +            apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
1.628 +            apply (rule exI[where x="0"], simp)
1.629 +            done}
1.630 +        hence ?qrths by blast
1.631 +        with dom have ?ths by blast}
1.632 +        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.633 +          head_nz[OF np] pnz sz ap[symmetric] ds[symmetric]
1.634 +          by (simp add: degree_eq_degreen0[symmetric]) blast }
1.635        ultimately have ?ths by blast
1.636      }
1.637      ultimately have ?ths by blast}
1.638 @@ -1732,7 +1732,7 @@
1.639  recdef isweaknpoly "measure size"
1.640    "isweaknpoly (C c) = True"
1.641    "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
1.642 -  "isweaknpoly p = False"
1.643 +  "isweaknpoly p = False"
1.644
1.645  lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p"
1.646    by (induct p arbitrary: n0, auto)
```