# HG changeset patch
# User wenzelm
# Date 1395157514 -3600
# Node ID 52d5067ca06a1bdc68ca8da32997954a5bfdcf78
# Parent  7adec2a527f5315f1dad239bdb83dcc06ae1b9f6
tuned proofs;

diff -r 7adec2a527f5 -r 52d5067ca06a src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Mar 18 16:44:51 2014 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Mar 18 16:45:14 2014 +0100
@@ -68,43 +68,43 @@
 
 subsection{* Degrees and heads and coefficients *}
 
-fun degree:: "poly \<Rightarrow> nat"
+fun degree :: "poly \<Rightarrow> nat"
 where
   "degree (CN c 0 p) = 1 + degree p"
 | "degree p = 0"
 
-fun head:: "poly \<Rightarrow> poly"
+fun head :: "poly \<Rightarrow> poly"
 where
   "head (CN c 0 p) = head p"
 | "head p = p"
 
 (* More general notions of degree and head *)
-fun degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat"
+fun degreen :: "poly \<Rightarrow> nat \<Rightarrow> nat"
 where
   "degreen (CN c n p) = (\<lambda>m. if n = m then 1 + degreen p n else 0)"
 | "degreen p = (\<lambda>m. 0)"
 
-fun headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"
+fun headn :: "poly \<Rightarrow> nat \<Rightarrow> poly"
 where
   "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"
 | "headn p = (\<lambda>m. p)"
 
-fun coefficients:: "poly \<Rightarrow> poly list"
+fun coefficients :: "poly \<Rightarrow> poly list"
 where
   "coefficients (CN c 0 p) = c # coefficients p"
 | "coefficients p = [p]"
 
-fun isconstant:: "poly \<Rightarrow> bool"
+fun isconstant :: "poly \<Rightarrow> bool"
 where
   "isconstant (CN c 0 p) = False"
 | "isconstant p = True"
 
-fun behead:: "poly \<Rightarrow> poly"
+fun behead :: "poly \<Rightarrow> poly"
 where
   "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
 | "behead p = 0\<^sub>p"
 
-fun headconst:: "poly \<Rightarrow> Num"
+fun headconst :: "poly \<Rightarrow> Num"
 where
   "headconst (CN c n p) = headconst p"
 | "headconst (C n) = n"
@@ -679,11 +679,11 @@
   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"
   using polymul_properties(2) by blast
 
-lemma polymul_degreen:  (* FIXME duplicate? *)
+lemma polymul_degreen:
   assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow>
     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)"
-  using polymul_properties(3) by blast
+  by (fact polymul_properties(3))
 
 lemma polymul_norm:
   assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
@@ -852,10 +852,10 @@
   by (simp add: shift1_def)
 
 lemma shift1_isnpoly:
-  assumes pn: "isnpoly p"
-    and pnz: "p \<noteq> 0\<^sub>p"
+  assumes "isnpoly p"
+    and "p \<noteq> 0\<^sub>p"
   shows "isnpoly (shift1 p) "
-  using pn pnz by (simp add: shift1_def isnpoly_def)
+  using assms by (simp add: shift1_def isnpoly_def)
 
 lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p"
   by (simp add: shift1_def)
@@ -864,10 +864,10 @@
   by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
 
 lemma funpow_isnpolyh:
-  assumes f: "\<And>p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
-    and np: "isnpolyh p n"
+  assumes "\<And>p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
+    and "isnpolyh p n"
   shows "isnpolyh (funpow k f p) n"
-  using f np by (induct k arbitrary: p) auto
+  using assms by (induct k arbitrary: p) auto
 
 lemma funpow_shift1:
   "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
@@ -886,10 +886,10 @@
   by (induct p rule: poly_cmul.induct) (auto simp add: field_simps)
 
 lemma behead:
-  assumes np: "isnpolyh p n"
+  assumes "isnpolyh p n"
   shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
     (Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})"
-  using np
+  using assms
 proof (induct p arbitrary: n rule: behead.induct)
   case (1 c p n)
   then have pn: "isnpolyh p n" by simp
@@ -902,12 +902,12 @@
 qed (auto simp add: Let_def)
 
 lemma behead_isnpolyh:
-  assumes np: "isnpolyh p n"
+  assumes "isnpolyh p n"
   shows "isnpolyh (behead p) n"
-  using np by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)
+  using assms by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)
 
 
-subsection{* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
+subsection {* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
 
 lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
 proof (induct p arbitrary: n rule: poly.induct, auto)
@@ -938,28 +938,27 @@
   by (induct p  arbitrary: n0 rule: head.induct) (auto intro: isnpolyh_polybound0)
 
 lemma polybound0_I:
-  assumes nb: "polybound0 a"
+  assumes "polybound0 a"
   shows "Ipoly (b # bs) a = Ipoly (b' # bs) a"
-  using nb
-  by (induct a rule: poly.induct) auto
+  using assms by (induct a rule: poly.induct) auto
 
 lemma polysubst0_I: "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b # bs) a) # bs) t"
   by (induct t) simp_all
 
 lemma polysubst0_I':
-  assumes nb: "polybound0 a"
+  assumes "polybound0 a"
   shows "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b' # bs) a) # bs) t"
-  by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"])
+  by (induct t) (simp_all add: polybound0_I[OF assms, where b="b" and b'="b'"])
 
 lemma decrpoly:
-  assumes nb: "polybound0 t"
+  assumes "polybound0 t"
   shows "Ipoly (x # bs) t = Ipoly bs (decrpoly t)"
-  using nb by (induct t rule: decrpoly.induct) simp_all
+  using assms by (induct t rule: decrpoly.induct) simp_all
 
 lemma polysubst0_polybound0:
-  assumes nb: "polybound0 t"
+  assumes "polybound0 t"
   shows "polybound0 (polysubst0 t a)"
-  using nb by (induct a rule: poly.induct) auto
+  using assms by (induct a rule: poly.induct) auto
 
 lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
   by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0)
@@ -1034,10 +1033,10 @@
 lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
   unfolding wf_bs_def by simp
 
-lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p"
+lemma wf_bs_insensitive': "wf_bs (x # bs) p = wf_bs (y # bs) p"
   unfolding wf_bs_def by simp
 
-lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"
+lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x # bs) p"
   by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def)
 
 lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"
@@ -1046,11 +1045,11 @@
 lemma coefficients_head: "last (coefficients p) = head p"
   by (induct p rule: coefficients.induct) auto
 
-lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p"
+lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x # bs) p"
   unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto
 
 lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists>ys. length (xs @ ys) = n"
-  apply (rule exI[where x="replicate (n - length xs) z"])
+  apply (rule exI[where x="replicate (n - length xs) z" for z])
   apply simp
   done
 
@@ -1646,7 +1645,7 @@
 lemma polyneg_degree: "isnpolyh p n \<Longrightarrow> degree (polyneg p) = degree p"
   by (induct p arbitrary: n rule: degree.induct) auto
 
-lemma polyneg_head: "isnpolyh p n \<Longrightarrow> head(polyneg p) = polyneg (head p)"
+lemma polyneg_head: "isnpolyh p n \<Longrightarrow> head (polyneg p) = polyneg (head p)"
   by (induct p arbitrary: n rule: degree.induct) auto
 
 
@@ -1719,7 +1718,8 @@
         have nr: "isnpolyh (s -\<^sub>p ?p') 0"
           using polysub_normh[OF ns np'] by simp
         from degree_polysub_samehead[OF ns np' headsp' degsp']
-        have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
+        have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p"
+          by simp
         moreover
         {
           assume deglt:"degree (s -\<^sub>p ?p') < degree s"
@@ -1799,7 +1799,7 @@
             using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
             by blast
           {
-            assume h1: "polydivide_aux a n p k s = (k',r)"
+            assume h1: "polydivide_aux a n p k s = (k', r)"
             from polydivide_aux.simps sz dn' ba
             have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
               by (simp add: Let_def)
@@ -1878,11 +1878,11 @@
                 by (simp add: field_simps)
             }
             then have ieq:"\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
-              Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
-              Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
+                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
+                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
             let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
-            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]]
+            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]]
             have nqw: "isnpolyh ?q 0"
               by simp
             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]]
@@ -2048,26 +2048,26 @@
   done
 
 lemma degree_degree:
-  assumes inc: "isnonconstant p"
+  assumes "isnonconstant p"
   shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
 proof
   let ?p = "polypoly bs p"
   assume H: "degree p = Polynomial_List.degree ?p"
-  from isnonconstant_coefficients_length[OF inc] have pz: "?p \<noteq> []"
+  from isnonconstant_coefficients_length[OF assms] have pz: "?p \<noteq> []"
     unfolding polypoly_def by auto
-  from H degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
+  from H degree_coefficients[of p] isnonconstant_coefficients_length[OF assms]
   have lg: "length (pnormalize ?p) = length ?p"
     unfolding Polynomial_List.degree_def polypoly_def by simp
   then have "pnormal ?p"
     using pnormal_length[OF pz] by blast
-  with isnonconstant_pnormal_iff[OF inc] show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
+  with isnonconstant_pnormal_iff[OF assms] show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
     by blast
 next
   let ?p = "polypoly bs p"
   assume H: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
-  with isnonconstant_pnormal_iff[OF inc] have "pnormal ?p"
+  with isnonconstant_pnormal_iff[OF assms] have "pnormal ?p"
     by blast
-  with degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
+  with degree_coefficients[of p] isnonconstant_coefficients_length[OF assms]
   show "degree p = Polynomial_List.degree ?p"
     unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto
 qed