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.49 -    and "head (shift1 p) = head p" by (simp_all add: shift1_head)
    1.50 -  then show ?case by (simp add: funpow_swap1)
    1.51 +    and "head (shift1 p) = head p"
    1.52 +    by (simp_all add: shift1_head)
    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.60  lemma polymul_head_polyeq:
    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.70      by (simp_all add: head_isnpolyh)
    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.123  lemma polyadd_different_degree:
   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.189 -        hence headsp': "head s = head ?p'"
   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"