src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 56066 cce36efe32eb parent 56043 0b25c3d34b77 child 56073 29e308b56d23
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Mar 12 17:02:05 2014 +0100
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Mar 12 17:25:28 2014 +0100
1.3 @@ -1002,7 +1002,7 @@
1.4        with "1.hyps" H have "wf_bs bs x"
1.5          by blast
1.6      }
1.7 -    ultimately  show "wf_bs bs x"
1.8 +    ultimately show "wf_bs bs x"
1.9        by blast
1.10    qed
1.11  qed simp_all
1.12 @@ -1063,10 +1063,7 @@
1.13    done
1.14
1.15  lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)"
1.16 -  unfolding wf_bs_def
1.17 -  apply (induct p q rule: polyadd.induct)
1.18 -  apply (auto simp add: Let_def)
1.19 -  done
1.20 +  unfolding wf_bs_def by (induct p q rule: polyadd.induct) (auto simp add: Let_def)
1.21
1.22  lemma wf_bs_polyul: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p *\<^sub>p q)"
1.23    unfolding wf_bs_def
1.24 @@ -1425,12 +1422,14 @@
1.25    {
1.26      assume nn': "n = n'"
1.27      have "n = 0 \<or> n > 0" by arith
1.28 -    moreover {
1.29 +    moreover
1.30 +    {
1.31        assume nz: "n = 0"
1.32        then have ?case using 4 nn'
1.33          by (auto simp add: Let_def degcmc')
1.34      }
1.35 -    moreover {
1.36 +    moreover
1.37 +    {
1.38        assume nz: "n > 0"
1.39        with nn' H(3) have  cc': "c = c'" and pp': "p = p'"
1.40          by (cases n, auto)+
1.41 @@ -1486,10 +1485,13 @@
1.42    then show ?case by auto
1.43  next
1.44    case (Suc k n0 p)
1.45 -  then have "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
1.46 +  then have "isnpolyh (shift1 p) 0"
1.47 +    by (simp add: shift1_isnpolyh)
1.48    with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
1.50 -  then show ?case by (simp add: funpow_swap1)
1.51 +    and "head (shift1 p) = head p"
1.53 +  then show ?case
1.54 +    by (simp add: funpow_swap1)
1.55  qed
1.56
1.57  lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
1.58 @@ -1534,7 +1536,7 @@
1.59
1.61    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
1.62 -  shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
1.63 +  shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> q \<noteq> 0\<^sub>p \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
1.64  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
1.65    case (2 c c' n' p' n0 n1)
1.66    then have "isnpolyh (head (CN c' n' p')) n1" "isnormNum c"
1.67 @@ -1545,11 +1547,11 @@
1.68    case (3 c n p c' n0 n1)
1.69    then have "isnpolyh (head (CN c n p)) n0" "isnormNum c'"
1.71 -  then show ?case using 3
1.72 -    by (cases n) auto
1.73 +  then show ?case
1.74 +    using 3 by (cases n) auto
1.75  next
1.76    case (4 c n p c' n' p' n0 n1)
1.77 -  hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
1.78 +  then have norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
1.79      "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'"
1.80      by simp_all
1.81    have "n < n' \<or> n' < n \<or> n = n'" by arith
1.82 @@ -1576,7 +1578,8 @@
1.83        apply auto
1.84        done
1.85    }
1.86 -  moreover {
1.87 +  moreover
1.88 +  {
1.89      assume nn': "n' = n"
1.90      from nn' polymul_normh[OF norm(5,4)]
1.91      have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)
1.92 @@ -1599,13 +1602,17 @@
1.93        from polymul_degreen[OF norm(5,4), where m="0"]
1.94          polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
1.95        norm(5,6) degree_npolyhCN[OF norm(6)]
1.96 -    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.97 -    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.98 +    have dth: "degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))"
1.99 +      by simp
1.100 +    then have dth': "degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))"
1.101 +      by simp
1.102      from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
1.103 -    have ?case   using norm "4.hyps"(6)[OF norm(5,3)]
1.104 -        "4.hyps"(5)[OF norm(5,4)] nn' nz by simp
1.105 +    have ?case
1.106 +      using norm "4.hyps"(6)[OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] nn' nz
1.107 +      by simp
1.108      }
1.109 -    ultimately have ?case by (cases n) auto
1.110 +    ultimately have ?case
1.111 +      by (cases n) auto
1.112    }
1.113    ultimately show ?case by blast
1.114  qed simp_all
1.115 @@ -1618,11 +1625,12 @@
1.116
1.117  lemma degree_CN: "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<le> 1 + degree p"
1.118    by (cases n) simp_all
1.119 +
1.120  lemma degree_CN': "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<ge>  degree p"
1.121    by (cases n) simp_all
1.122
1.124 -  "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degree p \<noteq> degree q\<rbrakk> \<Longrightarrow>
1.125 +  "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> degree p \<noteq> degree q \<Longrightarrow>
1.126      degree (polyadd p q) = max (degree p) (degree q)"
1.127    using polyadd_different_degreen degree_eq_degreen0 by simp
1.128
1.129 @@ -1651,14 +1659,14 @@
1.130      and ns: "isnpolyh s n1"
1.131      and ap: "head p = a"
1.132      and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
1.133 -  shows "(polydivide_aux a n p k s = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p)
1.134 -          \<and> (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
1.135 +  shows "polydivide_aux a n p k s = (k',r) \<longrightarrow> k' \<ge> k \<and> (degree r = 0 \<or> degree r < degree p) \<and>
1.136 +    (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> (polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
1.137    using ns
1.138  proof (induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
1.139    case less
1.140    let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
1.141 -  let ?ths = "polydivide_aux a n p k s = (k', r) \<longrightarrow>  k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p)
1.142 -    \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1.143 +  let ?ths = "polydivide_aux a n p k s = (k', r) \<longrightarrow>  k \<le> k' \<and>
1.144 +    (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1.145    let ?b = "head s"
1.146    let ?p' = "funpow (degree s - n) shift1 p"
1.147    let ?xdn = "funpow (degree s - n) shift1 (1)\<^sub>p"
1.148 @@ -1675,46 +1683,62 @@
1.149      by (simp add: isnpoly_def)
1.150    from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap
1.151    have nakk':"isnpolyh ?akk' 0" by blast
1.152 -  { assume sz: "s = 0\<^sub>p"
1.153 -    hence ?ths using np polydivide_aux.simps
1.154 +  {
1.155 +    assume sz: "s = 0\<^sub>p"
1.156 +    then have ?ths
1.157 +      using np polydivide_aux.simps
1.158        apply clarsimp
1.159        apply (rule exI[where x="0\<^sub>p"])
1.160        apply simp
1.161 -      done }
1.162 +      done
1.163 +  }
1.164    moreover
1.165 -  { assume sz: "s \<noteq> 0\<^sub>p"
1.166 -    { assume dn: "degree s < n"
1.167 -      hence "?ths" using ns ndp np polydivide_aux.simps
1.168 +  {
1.169 +    assume sz: "s \<noteq> 0\<^sub>p"
1.170 +    {
1.171 +      assume dn: "degree s < n"
1.172 +      then have "?ths"
1.173 +        using ns ndp np polydivide_aux.simps
1.174          apply auto
1.175          apply (rule exI[where x="0\<^sub>p"])
1.176          apply simp
1.177 -        done }
1.178 +        done
1.179 +    }
1.180      moreover
1.181 -    { assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> n" by arith
1.182 +    {
1.183 +      assume dn': "\<not> degree s < n"
1.184 +      then have dn: "degree s \<ge> n"
1.185 +        by arith
1.186        have degsp': "degree s = degree ?p'"
1.187 -        using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] by simp
1.188 -      { assume ba: "?b = a"
1.190 +        using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"]
1.191 +        by simp
1.192 +      {
1.193 +        assume ba: "?b = a"
1.194 +        then have headsp': "head s = head ?p'"
1.195            using ap headp' by simp
1.196          have nr: "isnpolyh (s -\<^sub>p ?p') 0"
1.197            using polysub_normh[OF ns np'] by simp
1.198          from degree_polysub_samehead[OF ns np' headsp' degsp']
1.199          have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
1.200          moreover
1.201 -        { assume deglt:"degree (s -\<^sub>p ?p') < degree s"
1.202 +        {
1.203 +          assume deglt:"degree (s -\<^sub>p ?p') < degree s"
1.204            from polydivide_aux.simps sz dn' ba
1.205            have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
1.206              by (simp add: Let_def)
1.207 -          { assume h1: "polydivide_aux a n p k s = (k', r)"
1.208 +          {
1.209 +            assume h1: "polydivide_aux a n p k s = (k', r)"
1.210              from less(1)[OF deglt nr, of k k' r] trans[OF eq[symmetric] h1]
1.211              have kk': "k \<le> k'"
1.212 -              and nr:"\<exists>nr. isnpolyh r nr"
1.213 +              and nr: "\<exists>nr. isnpolyh r nr"
1.214                and dr: "degree r = 0 \<or> degree r < degree p"
1.215 -              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)"
1.216 +              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"
1.217                by auto
1.218              from q1 obtain q n1 where nq: "isnpolyh q n1"
1.219 -              and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r" by blast
1.220 -            from nr obtain nr where nr': "isnpolyh r nr" by blast
1.221 +              and asp: "a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"
1.222 +              by blast
1.223 +            from nr obtain nr where nr': "isnpolyh r nr"
1.224 +              by blast
1.225              from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0"
1.226                by simp
1.227              from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
1.228 @@ -1723,56 +1747,66 @@
1.229                polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
1.230              have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0"
1.231                by simp
1.232 -            from asp have "\<forall> (bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) =
1.233 -              Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
1.234 -            hence " \<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
1.235 +            from asp have "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
1.236 +              Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)"
1.237 +              by simp
1.238 +            then have "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
1.239 +              Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
1.240                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.241                by (simp add: field_simps)
1.242 -            hence " \<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.243 +            then have "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
1.244 +              Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.245                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) +
1.246                Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.247                by (auto simp only: funpow_shift1_1)
1.248 -            hence "\<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.249 +            then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list.
1.250 +              Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.251                Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) +
1.252                Ipoly bs q) + Ipoly bs r"
1.253                by (simp add: field_simps)
1.254 -            hence "\<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.255 +            then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list.
1.256 +              Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.257                Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r)"
1.258                by simp
1.259              with isnpolyh_unique[OF nakks' nqr']
1.260              have "a ^\<^sub>p (k' - k) *\<^sub>p s =
1.261                p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r"
1.262                by blast
1.263 -            hence ?qths using nq'
1.264 +            then have ?qths using nq'
1.265                apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q" in exI)
1.266                apply (rule_tac x="0" in exI)
1.267                apply simp
1.268                done
1.269 -            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.270 +            with kk' nr dr have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and>
1.271 +              (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1.272                by blast
1.273            }
1.274 -          hence ?ths by blast
1.275 +          then have ?ths by blast
1.276          }
1.277          moreover
1.278 -        { assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
1.279 +        {
1.280 +          assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
1.281            from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field_inverse_zero}"]
1.282 -          have " \<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'"
1.283 +          have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs ?p'"
1.284              by simp
1.285 -          hence "\<forall>(bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
1.286 +          then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
1.287              using np nxdn
1.288              apply simp
1.289              apply (simp only: funpow_shift1_1)
1.290              apply simp
1.291              done
1.292 -          hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
1.293 +          then have sp': "s = ?xdn *\<^sub>p p"
1.294 +            using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
1.295              by blast
1.296 -          { assume h1: "polydivide_aux a n p k s = (k',r)"
1.297 +          {
1.298 +            assume h1: "polydivide_aux a n p k s = (k',r)"
1.299              from polydivide_aux.simps sz dn' ba
1.300              have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
1.301                by (simp add: Let_def)
1.302              also have "\<dots> = (k,0\<^sub>p)"
1.303                using polydivide_aux.simps spz by simp
1.304 -            finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
1.305 +            finally have "(k', r) = (k, 0\<^sub>p)"
1.306 +              using h1 by simp
1.307              with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
1.308                polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?ths
1.309                apply auto
1.310 @@ -1784,7 +1818,8 @@
1.311          ultimately have ?ths by blast
1.312        }
1.313        moreover
1.314 -      { assume ba: "?b \<noteq> a"
1.315 +      {
1.316 +        assume ba: "?b \<noteq> a"
1.317          from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns]
1.318            polymul_normh[OF head_isnpolyh[OF ns] np']]
1.319          have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0"
1.320 @@ -1807,12 +1842,14 @@
1.321            ndp dn
1.322          have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p')"
1.323            by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
1.324 -        { assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s"
1.325 +        {
1.326 +          assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s"
1.327            from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.328              polymul_normh[OF head_isnpolyh[OF ns]np']] ap
1.329            have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0"
1.330              by simp
1.331 -          { assume h1:"polydivide_aux a n p k s = (k', r)"
1.332 +          {
1.333 +            assume h1:"polydivide_aux a n p k s = (k', r)"
1.334              from h1 polydivide_aux.simps sz dn' ba
1.335              have eq:"polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
1.336                by (simp add: Let_def)
1.337 @@ -1823,23 +1860,25 @@
1.338                and dr: "degree r = 0 \<or> degree r < degree p"
1.339                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"
1.340                by auto
1.341 -            from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
1.342 +            from kk' have kk'': "Suc (k' - Suc k) = k' - k"
1.343 +              by arith
1.344              {
1.345 -              fix bs:: "'a::{field_char_0,field_inverse_zero} list"
1.346 +              fix bs :: "'a::{field_char_0,field_inverse_zero} list"
1.347                from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
1.348                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)"
1.349                  by simp
1.350 -              hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s =
1.351 +              then have "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s =
1.352                  Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r"
1.353                  by (simp add: field_simps)
1.354 -              hence "Ipoly bs a ^ (k' - k)  * Ipoly bs s =
1.355 +              then have "Ipoly bs a ^ (k' - k)  * Ipoly bs s =
1.356                  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.357                  by (simp add: kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
1.358 -              hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.359 +              then have "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.360                  Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
1.361                  by (simp add: field_simps)
1.362              }
1.363 -            hence ieq:"\<forall>(bs :: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.364 +            then have ieq:"\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
1.365 +              Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.366                Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
1.367                by auto
1.368              let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
1.369 @@ -1857,29 +1896,33 @@
1.370                apply (rule exI[where x="0"], simp)
1.371                done
1.372            }
1.373 -          hence ?ths by blast
1.374 +          then have ?ths by blast
1.375          }
1.376          moreover
1.377 -        { assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
1.378 +        {
1.379 +          assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
1.380            {
1.381              fix bs :: "'a::{field_char_0,field_inverse_zero} list"
1.382              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
1.383              have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'"
1.384                by simp
1.385 -            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p"
1.386 +            then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p"
1.387                by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
1.388 -            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
1.389 +            then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
1.390                by simp
1.391            }
1.392 -          hence hth: "\<forall> (bs:: 'a::{field_char_0,field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) =
1.393 -            Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
1.394 +          then have hth: "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
1.395 +            Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
1.396            from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
1.397              using isnpolyh_unique[where ?'a = "'a::{field_char_0,field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.398                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
1.399 -              simplified ap] by simp
1.400 -          { assume h1: "polydivide_aux a n p k s = (k', r)"
1.401 +              simplified ap]
1.402 +            by simp
1.403 +          {
1.404 +            assume h1: "polydivide_aux a n p k s = (k', r)"
1.405              from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps
1.406 -            have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
1.407 +            have "(k', r) = (Suc k, 0\<^sub>p)"
1.408 +              by (simp add: Let_def)
1.409              with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
1.410                polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
1.411              have ?ths
1.412 @@ -1889,12 +1932,12 @@
1.413                apply (rule exI[where x="0"], simp)
1.414                done
1.415            }
1.416 -          hence ?ths by blast
1.417 +          then have ?ths by blast
1.418          }
1.419          ultimately have ?ths
1.420 -          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.421 +          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.422              head_nz[OF np] pnz sz ap[symmetric]
1.423 -          by (simp add: degree_eq_degreen0[symmetric]) blast
1.424 +          by (auto simp add: degree_eq_degreen0[symmetric])
1.425        }
1.426        ultimately have ?ths by blast
1.427      }
1.428 @@ -1905,10 +1948,12 @@
1.429
1.430  lemma polydivide_properties:
1.431    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
1.432 -    and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \<noteq> 0\<^sub>p"
1.433 -  shows "\<exists>k r. polydivide s p = (k,r) \<and>
1.434 +    and np: "isnpolyh p n0"
1.435 +    and ns: "isnpolyh s n1"
1.436 +    and pnz: "p \<noteq> 0\<^sub>p"
1.437 +  shows "\<exists>k r. polydivide s p = (k, r) \<and>
1.438      (\<exists>nr. isnpolyh r nr) \<and> (degree r = 0 \<or> degree r < degree p) \<and>
1.439 -    (\<exists>q n1. isnpolyh q n1 \<and> ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r))"
1.440 +    (\<exists>q n1. isnpolyh q n1 \<and> polypow k (head p) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
1.441  proof -
1.442    have trv: "head p = head p" "degree p = degree p"
1.443      by simp_all
1.444 @@ -1930,7 +1975,7 @@
1.445  qed
1.446
1.447
1.448 -subsection{* More about polypoly and pnormal etc *}
1.449 +subsection {* More about polypoly and pnormal etc *}
1.450
1.451  definition "isnonconstant p \<longleftrightarrow> \<not> isconstant p"
1.452
1.453 @@ -1940,19 +1985,23 @@
1.454  proof
1.455    let ?p = "polypoly bs p"
1.456    assume H: "pnormal ?p"
1.457 -  have csz: "coefficients p \<noteq> []" using nc by (cases p) auto
1.458 -
1.459 -  from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"]
1.460 -    pnormal_last_nonzero[OF H]
1.461 -  show "Ipoly bs (head p) \<noteq> 0" by (simp add: polypoly_def)
1.462 +  have csz: "coefficients p \<noteq> []"
1.463 +    using nc by (cases p) auto
1.464 +  from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] pnormal_last_nonzero[OF H]
1.465 +  show "Ipoly bs (head p) \<noteq> 0"
1.466 +    by (simp add: polypoly_def)
1.467  next
1.468    assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.469    let ?p = "polypoly bs p"
1.470 -  have csz: "coefficients p \<noteq> []" using nc by (cases p) auto
1.471 -  hence pz: "?p \<noteq> []" by (simp add: polypoly_def)
1.472 -  hence lg: "length ?p > 0" by simp
1.473 +  have csz: "coefficients p \<noteq> []"
1.474 +    using nc by (cases p) auto
1.475 +  then have pz: "?p \<noteq> []"
1.476 +    by (simp add: polypoly_def)
1.477 +  then have lg: "length ?p > 0"
1.478 +    by simp
1.479    from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"]
1.480 -  have lz: "last ?p \<noteq> 0" by (simp add: polypoly_def)
1.481 +  have lz: "last ?p \<noteq> 0"
1.482 +    by (simp add: polypoly_def)
1.483    from pnormal_last_length[OF lg lz] show "pnormal ?p" .
1.484  qed
1.485
1.486 @@ -1971,12 +2020,14 @@
1.487    let ?p = "polypoly bs p"
1.488    assume nc: "nonconstant ?p"
1.489    from isnonconstant_pnormal_iff[OF inc, of bs] nc
1.490 -  show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" unfolding nonconstant_def by blast
1.491 +  show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.492 +    unfolding nonconstant_def by blast
1.493  next
1.494    let ?p = "polypoly bs p"
1.495    assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.496    from isnonconstant_pnormal_iff[OF inc, of bs] h
1.497 -  have pn: "pnormal ?p" by blast
1.498 +  have pn: "pnormal ?p"
1.499 +    by blast
1.500    {
1.501      fix x
1.502      assume H: "?p = [x]"
1.503 @@ -1989,7 +2040,7 @@
1.504      using pn unfolding nonconstant_def by blast
1.505  qed
1.506
1.507 -lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
1.508 +lemma pnormal_length: "p \<noteq> [] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
1.509    apply (induct p)
1.510    apply (simp_all add: pnormal_def)
1.511    apply (case_tac "p = []")
1.512 @@ -2005,15 +2056,17 @@
1.513    from isnonconstant_coefficients_length[OF inc] have pz: "?p \<noteq> []"
1.514      unfolding polypoly_def by auto
1.515    from H degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
1.516 -  have lg:"length (pnormalize ?p) = length ?p"
1.517 +  have lg: "length (pnormalize ?p) = length ?p"
1.518      unfolding Polynomial_List.degree_def polypoly_def by simp
1.519 -  hence "pnormal ?p" using pnormal_length[OF pz] by blast
1.520 -  with isnonconstant_pnormal_iff[OF inc]
1.521 -  show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" by blast
1.522 +  then have "pnormal ?p"
1.523 +    using pnormal_length[OF pz] by blast
1.524 +  with isnonconstant_pnormal_iff[OF inc] show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.525 +    by blast
1.526  next
1.527 -  let  ?p = "polypoly bs p"
1.528 +  let ?p = "polypoly bs p"
1.529    assume H: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.530 -  with isnonconstant_pnormal_iff[OF inc] have "pnormal ?p" by blast
1.531 +  with isnonconstant_pnormal_iff[OF inc] have "pnormal ?p"
1.532 +    by blast
1.533    with degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
1.534    show "degree p = Polynomial_List.degree ?p"
1.535      unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto
1.536 @@ -2022,7 +2075,8 @@
1.537
1.538  section {* Swaps ; Division by a certain variable *}
1.539
1.540 -primrec swap :: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" where
1.541 +primrec swap :: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly"
1.542 +where
1.543    "swap n m (C x) = C x"
1.544  | "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
1.545  | "swap n m (Neg t) = Neg (swap n m t)"
1.546 @@ -2030,19 +2084,20 @@
1.547  | "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
1.548  | "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
1.549  | "swap n m (Pw t k) = Pw (swap n m t) k"
1.550 -| "swap n m (CN c k p) =
1.551 -    CN (swap n m c) (if k = n then m else if k=m then n else k) (swap n m p)"
1.552 +| "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k) (swap n m p)"
1.553
1.554  lemma swap:
1.555 -  assumes nbs: "n < length bs"
1.556 -    and mbs: "m < length bs"
1.557 +  assumes "n < length bs"
1.558 +    and "m < length bs"
1.559    shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
1.560  proof (induct t)
1.561    case (Bound k)
1.562 -  then show ?case using nbs mbs by simp
1.563 +  then show ?case
1.564 +    using assms by simp
1.565  next
1.566    case (CN c k p)
1.567 -  then show ?case using nbs mbs by simp
1.568 +  then show ?case
1.569 +    using assms by simp
1.570  qed simp_all
1.571
1.572  lemma swap_swap_id [simp]: "swap n m (swap m n t) = t"
```