src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 56207 52d5067ca06a
parent 56198 21dd034523e5
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Mar 18 16:44:51 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Mar 18 16:45:14 2014 +0100
     1.3 @@ -68,43 +68,43 @@
     1.4  
     1.5  subsection{* Degrees and heads and coefficients *}
     1.6  
     1.7 -fun degree:: "poly \<Rightarrow> nat"
     1.8 +fun degree :: "poly \<Rightarrow> nat"
     1.9  where
    1.10    "degree (CN c 0 p) = 1 + degree p"
    1.11  | "degree p = 0"
    1.12  
    1.13 -fun head:: "poly \<Rightarrow> poly"
    1.14 +fun head :: "poly \<Rightarrow> poly"
    1.15  where
    1.16    "head (CN c 0 p) = head p"
    1.17  | "head p = p"
    1.18  
    1.19  (* More general notions of degree and head *)
    1.20 -fun degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat"
    1.21 +fun degreen :: "poly \<Rightarrow> nat \<Rightarrow> nat"
    1.22  where
    1.23    "degreen (CN c n p) = (\<lambda>m. if n = m then 1 + degreen p n else 0)"
    1.24  | "degreen p = (\<lambda>m. 0)"
    1.25  
    1.26 -fun headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"
    1.27 +fun headn :: "poly \<Rightarrow> nat \<Rightarrow> poly"
    1.28  where
    1.29    "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"
    1.30  | "headn p = (\<lambda>m. p)"
    1.31  
    1.32 -fun coefficients:: "poly \<Rightarrow> poly list"
    1.33 +fun coefficients :: "poly \<Rightarrow> poly list"
    1.34  where
    1.35    "coefficients (CN c 0 p) = c # coefficients p"
    1.36  | "coefficients p = [p]"
    1.37  
    1.38 -fun isconstant:: "poly \<Rightarrow> bool"
    1.39 +fun isconstant :: "poly \<Rightarrow> bool"
    1.40  where
    1.41    "isconstant (CN c 0 p) = False"
    1.42  | "isconstant p = True"
    1.43  
    1.44 -fun behead:: "poly \<Rightarrow> poly"
    1.45 +fun behead :: "poly \<Rightarrow> poly"
    1.46  where
    1.47    "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
    1.48  | "behead p = 0\<^sub>p"
    1.49  
    1.50 -fun headconst:: "poly \<Rightarrow> Num"
    1.51 +fun headconst :: "poly \<Rightarrow> Num"
    1.52  where
    1.53    "headconst (CN c n p) = headconst p"
    1.54  | "headconst (C n) = n"
    1.55 @@ -679,11 +679,11 @@
    1.56    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p"
    1.57    using polymul_properties(2) by blast
    1.58  
    1.59 -lemma polymul_degreen:  (* FIXME duplicate? *)
    1.60 +lemma polymul_degreen:
    1.61    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    1.62    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow>
    1.63      degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \<or> q = 0\<^sub>p then 0 else degreen p m + degreen q m)"
    1.64 -  using polymul_properties(3) by blast
    1.65 +  by (fact polymul_properties(3))
    1.66  
    1.67  lemma polymul_norm:
    1.68    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    1.69 @@ -852,10 +852,10 @@
    1.70    by (simp add: shift1_def)
    1.71  
    1.72  lemma shift1_isnpoly:
    1.73 -  assumes pn: "isnpoly p"
    1.74 -    and pnz: "p \<noteq> 0\<^sub>p"
    1.75 +  assumes "isnpoly p"
    1.76 +    and "p \<noteq> 0\<^sub>p"
    1.77    shows "isnpoly (shift1 p) "
    1.78 -  using pn pnz by (simp add: shift1_def isnpoly_def)
    1.79 +  using assms by (simp add: shift1_def isnpoly_def)
    1.80  
    1.81  lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p"
    1.82    by (simp add: shift1_def)
    1.83 @@ -864,10 +864,10 @@
    1.84    by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
    1.85  
    1.86  lemma funpow_isnpolyh:
    1.87 -  assumes f: "\<And>p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
    1.88 -    and np: "isnpolyh p n"
    1.89 +  assumes "\<And>p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
    1.90 +    and "isnpolyh p n"
    1.91    shows "isnpolyh (funpow k f p) n"
    1.92 -  using f np by (induct k arbitrary: p) auto
    1.93 +  using assms by (induct k arbitrary: p) auto
    1.94  
    1.95  lemma funpow_shift1:
    1.96    "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
    1.97 @@ -886,10 +886,10 @@
    1.98    by (induct p rule: poly_cmul.induct) (auto simp add: field_simps)
    1.99  
   1.100  lemma behead:
   1.101 -  assumes np: "isnpolyh p n"
   1.102 +  assumes "isnpolyh p n"
   1.103    shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
   1.104      (Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})"
   1.105 -  using np
   1.106 +  using assms
   1.107  proof (induct p arbitrary: n rule: behead.induct)
   1.108    case (1 c p n)
   1.109    then have pn: "isnpolyh p n" by simp
   1.110 @@ -902,12 +902,12 @@
   1.111  qed (auto simp add: Let_def)
   1.112  
   1.113  lemma behead_isnpolyh:
   1.114 -  assumes np: "isnpolyh p n"
   1.115 +  assumes "isnpolyh p n"
   1.116    shows "isnpolyh (behead p) n"
   1.117 -  using np by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)
   1.118 +  using assms by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)
   1.119  
   1.120  
   1.121 -subsection{* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
   1.122 +subsection {* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
   1.123  
   1.124  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
   1.125  proof (induct p arbitrary: n rule: poly.induct, auto)
   1.126 @@ -938,28 +938,27 @@
   1.127    by (induct p  arbitrary: n0 rule: head.induct) (auto intro: isnpolyh_polybound0)
   1.128  
   1.129  lemma polybound0_I:
   1.130 -  assumes nb: "polybound0 a"
   1.131 +  assumes "polybound0 a"
   1.132    shows "Ipoly (b # bs) a = Ipoly (b' # bs) a"
   1.133 -  using nb
   1.134 -  by (induct a rule: poly.induct) auto
   1.135 +  using assms by (induct a rule: poly.induct) auto
   1.136  
   1.137  lemma polysubst0_I: "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b # bs) a) # bs) t"
   1.138    by (induct t) simp_all
   1.139  
   1.140  lemma polysubst0_I':
   1.141 -  assumes nb: "polybound0 a"
   1.142 +  assumes "polybound0 a"
   1.143    shows "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b' # bs) a) # bs) t"
   1.144 -  by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"])
   1.145 +  by (induct t) (simp_all add: polybound0_I[OF assms, where b="b" and b'="b'"])
   1.146  
   1.147  lemma decrpoly:
   1.148 -  assumes nb: "polybound0 t"
   1.149 +  assumes "polybound0 t"
   1.150    shows "Ipoly (x # bs) t = Ipoly bs (decrpoly t)"
   1.151 -  using nb by (induct t rule: decrpoly.induct) simp_all
   1.152 +  using assms by (induct t rule: decrpoly.induct) simp_all
   1.153  
   1.154  lemma polysubst0_polybound0:
   1.155 -  assumes nb: "polybound0 t"
   1.156 +  assumes "polybound0 t"
   1.157    shows "polybound0 (polysubst0 t a)"
   1.158 -  using nb by (induct a rule: poly.induct) auto
   1.159 +  using assms by (induct a rule: poly.induct) auto
   1.160  
   1.161  lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
   1.162    by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0)
   1.163 @@ -1034,10 +1033,10 @@
   1.164  lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
   1.165    unfolding wf_bs_def by simp
   1.166  
   1.167 -lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p"
   1.168 +lemma wf_bs_insensitive': "wf_bs (x # bs) p = wf_bs (y # bs) p"
   1.169    unfolding wf_bs_def by simp
   1.170  
   1.171 -lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"
   1.172 +lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x # bs) p"
   1.173    by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def)
   1.174  
   1.175  lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"
   1.176 @@ -1046,11 +1045,11 @@
   1.177  lemma coefficients_head: "last (coefficients p) = head p"
   1.178    by (induct p rule: coefficients.induct) auto
   1.179  
   1.180 -lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p"
   1.181 +lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x # bs) p"
   1.182    unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto
   1.183  
   1.184  lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists>ys. length (xs @ ys) = n"
   1.185 -  apply (rule exI[where x="replicate (n - length xs) z"])
   1.186 +  apply (rule exI[where x="replicate (n - length xs) z" for z])
   1.187    apply simp
   1.188    done
   1.189  
   1.190 @@ -1646,7 +1645,7 @@
   1.191  lemma polyneg_degree: "isnpolyh p n \<Longrightarrow> degree (polyneg p) = degree p"
   1.192    by (induct p arbitrary: n rule: degree.induct) auto
   1.193  
   1.194 -lemma polyneg_head: "isnpolyh p n \<Longrightarrow> head(polyneg p) = polyneg (head p)"
   1.195 +lemma polyneg_head: "isnpolyh p n \<Longrightarrow> head (polyneg p) = polyneg (head p)"
   1.196    by (induct p arbitrary: n rule: degree.induct) auto
   1.197  
   1.198  
   1.199 @@ -1719,7 +1718,8 @@
   1.200          have nr: "isnpolyh (s -\<^sub>p ?p') 0"
   1.201            using polysub_normh[OF ns np'] by simp
   1.202          from degree_polysub_samehead[OF ns np' headsp' degsp']
   1.203 -        have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
   1.204 +        have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p"
   1.205 +          by simp
   1.206          moreover
   1.207          {
   1.208            assume deglt:"degree (s -\<^sub>p ?p') < degree s"
   1.209 @@ -1799,7 +1799,7 @@
   1.210              using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
   1.211              by blast
   1.212            {
   1.213 -            assume h1: "polydivide_aux a n p k s = (k',r)"
   1.214 +            assume h1: "polydivide_aux a n p k s = (k', r)"
   1.215              from polydivide_aux.simps sz dn' ba
   1.216              have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
   1.217                by (simp add: Let_def)
   1.218 @@ -1878,11 +1878,11 @@
   1.219                  by (simp add: field_simps)
   1.220              }
   1.221              then have ieq:"\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
   1.222 -              Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.223 -              Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
   1.224 +                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.225 +                Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
   1.226                by auto
   1.227              let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
   1.228 -            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.229 +            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.230              have nqw: "isnpolyh ?q 0"
   1.231                by simp
   1.232              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.233 @@ -2048,26 +2048,26 @@
   1.234    done
   1.235  
   1.236  lemma degree_degree:
   1.237 -  assumes inc: "isnonconstant p"
   1.238 +  assumes "isnonconstant p"
   1.239    shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
   1.240  proof
   1.241    let ?p = "polypoly bs p"
   1.242    assume H: "degree p = Polynomial_List.degree ?p"
   1.243 -  from isnonconstant_coefficients_length[OF inc] have pz: "?p \<noteq> []"
   1.244 +  from isnonconstant_coefficients_length[OF assms] have pz: "?p \<noteq> []"
   1.245      unfolding polypoly_def by auto
   1.246 -  from H degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
   1.247 +  from H degree_coefficients[of p] isnonconstant_coefficients_length[OF assms]
   1.248    have lg: "length (pnormalize ?p) = length ?p"
   1.249      unfolding Polynomial_List.degree_def polypoly_def by simp
   1.250    then have "pnormal ?p"
   1.251      using pnormal_length[OF pz] by blast
   1.252 -  with isnonconstant_pnormal_iff[OF inc] show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
   1.253 +  with isnonconstant_pnormal_iff[OF assms] show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
   1.254      by blast
   1.255  next
   1.256    let ?p = "polypoly bs p"
   1.257    assume H: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
   1.258 -  with isnonconstant_pnormal_iff[OF inc] have "pnormal ?p"
   1.259 +  with isnonconstant_pnormal_iff[OF assms] have "pnormal ?p"
   1.260      by blast
   1.261 -  with degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
   1.262 +  with degree_coefficients[of p] isnonconstant_coefficients_length[OF assms]
   1.263    show "degree p = Polynomial_List.degree ?p"
   1.264      unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto
   1.265  qed