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)