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
```