# HG changeset patch # User wenzelm # Date 1373880559 -7200 # Node ID 1e7896c7f781f6649d7b44e0d30e5633e4a4dbb9 # Parent 42c14dba1daa4161aaf16ffef5973f10afbddf6c tuned specifications and proofs; diff -r 42c14dba1daa -r 1e7896c7f781 src/HOL/Decision_Procs/Commutative_Ring.thy --- a/src/HOL/Decision_Procs/Commutative_Ring.thy Mon Jul 15 10:42:12 2013 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Mon Jul 15 11:29:19 2013 +0200 @@ -271,7 +271,7 @@ with 1 have "\P. Ipol ls (pow l P) = Ipol ls P ^ l" by simp moreover note Suc `even l` even_nat_plus_one_div_two - ultimately show ?thesis by (auto simp add: mul_ci power_Suc even_pow) + ultimately show ?thesis by (auto simp add: mul_ci even_pow) next assume "odd l" { @@ -286,7 +286,7 @@ have two_times: "2 * (w div 2) = w" by (simp only: numerals even_nat_div_two_times_two [OF `even w`]) have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)" - by (simp add: power_Suc) + by simp then have "Ipol ls P * Ipol ls P = Ipol ls P ^ 2" by (simp add: numerals) with Suc show ?thesis diff -r 42c14dba1daa -r 1e7896c7f781 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Jul 15 10:42:12 2013 +0200 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Jul 15 11:29:19 2013 +0200 @@ -8,8 +8,6 @@ imports Complex_Main "~~/src/HOL/Library/Abstract_Rat" Polynomial_List begin - (* Implementation *) - subsection{* Datatype of polynomial expressions *} datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly @@ -18,8 +16,11 @@ abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \ C (0\<^sub>N)" abbreviation poly_p :: "int \ poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \ C (i)\<^sub>N" + subsection{* Boundedness, substitution and all that *} -primrec polysize:: "poly \ nat" where + +primrec polysize:: "poly \ nat" +where "polysize (C c) = 1" | "polysize (Bound n) = 1" | "polysize (Neg p) = 1 + polysize p" @@ -29,7 +30,8 @@ | "polysize (Pw p n) = 1 + polysize p" | "polysize (CN c n p) = 4 + polysize c + polysize p" -primrec polybound0:: "poly \ bool" (* a poly is INDEPENDENT of Bound 0 *) where +primrec polybound0:: "poly \ bool" -- {* a poly is INDEPENDENT of Bound 0 *} +where "polybound0 (C c) = True" | "polybound0 (Bound n) = (n>0)" | "polybound0 (Neg a) = polybound0 a" @@ -39,7 +41,8 @@ | "polybound0 (Pw p n) = (polybound0 p)" | "polybound0 (CN c n p) = (n \ 0 \ polybound0 c \ polybound0 p)" -primrec polysubst0:: "poly \ poly \ poly" (* substitute a poly into a poly for Bound 0 *) where +primrec polysubst0:: "poly \ poly \ poly" -- {* substitute a poly into a poly for Bound 0 *} +where "polysubst0 t (C c) = (C c)" | "polysubst0 t (Bound n) = (if n=0 then t else Bound n)" | "polysubst0 t (Neg a) = Neg (polysubst0 t a)" @@ -61,6 +64,7 @@ | "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)" | "decrpoly a = a" + subsection{* Degrees and heads and coefficients *} fun degree:: "poly \ nat" @@ -104,9 +108,9 @@ "headconst (CN c n p) = headconst p" | "headconst (C n) = n" + subsection{* Operations for normalization *} - declare if_cong[fundef_cong del] declare let_cong[fundef_cong del] @@ -131,8 +135,7 @@ | "polyneg a = Neg a" definition polysub :: "poly \ poly \ poly" (infixl "-\<^sub>p" 60) -where - "p -\<^sub>p q = polyadd p (polyneg q)" + where "p -\<^sub>p q = polyadd p (polyneg q)" fun polymul :: "poly \ poly \ poly" (infixl "*\<^sub>p" 60) where @@ -173,7 +176,8 @@ by pat_completeness auto termination by (relation "measure polysize") auto -fun poly_cmul :: "Num \ poly \ poly" where +fun poly_cmul :: "Num \ poly \ poly" +where "poly_cmul y (C x) = C (y *\<^sub>N x)" | "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)" | "poly_cmul y p = C y *\<^sub>p p" @@ -181,35 +185,39 @@ definition monic :: "poly \ (poly \ bool)" where "monic p \ (let h = headconst p in if h = 0\<^sub>N then (p,False) else ((C (Ninv h)) *\<^sub>p p, 0>\<^sub>N h))" + subsection{* Pseudo-division *} -definition shift1 :: "poly \ poly" where - "shift1 p \ CN 0\<^sub>p 0 p" +definition shift1 :: "poly \ poly" + where "shift1 p \ CN 0\<^sub>p 0 p" -abbreviation funpow :: "nat \ ('a \ 'a) \ ('a \ 'a)" where - "funpow \ compow" +abbreviation funpow :: "nat \ ('a \ 'a) \ ('a \ 'a)" + where "funpow \ compow" partial_function (tailrec) polydivide_aux :: "poly \ nat \ poly \ nat \ poly \ nat \ poly" - where +where "polydivide_aux a n p k s = - (if s = 0\<^sub>p then (k,s) - else (let b = head s; m = degree s in - (if m < n then (k,s) else - (let p'= funpow (m - n) shift1 p in - (if a = b then polydivide_aux a n p k (s -\<^sub>p p') - else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))" + (if s = 0\<^sub>p then (k,s) + else (let b = head s; m = degree s in + (if m < n then (k,s) else + (let p'= funpow (m - n) shift1 p in + (if a = b then polydivide_aux a n p k (s -\<^sub>p p') + else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))" -definition polydivide :: "poly \ poly \ (nat \ poly)" where - "polydivide s p \ polydivide_aux (head p) (degree p) p 0 s" +definition polydivide :: "poly \ poly \ (nat \ poly)" + where "polydivide s p \ polydivide_aux (head p) (degree p) p 0 s" -fun poly_deriv_aux :: "nat \ poly \ poly" where +fun poly_deriv_aux :: "nat \ poly \ poly" +where "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)" | "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p" -fun poly_deriv :: "poly \ poly" where +fun poly_deriv :: "poly \ poly" +where "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p" | "poly_deriv p = 0\<^sub>p" + subsection{* Semantics of the polynomial representation *} primrec Ipoly :: "'a list \ poly \ 'a::{field_char_0, field_inverse_zero, power}" where @@ -233,6 +241,7 @@ lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat + subsection {* Normal form and normalization *} fun isnpolyh:: "poly \ nat \ bool" @@ -242,10 +251,10 @@ | "isnpolyh p = (\k. False)" lemma isnpolyh_mono: "\n' \ n ; isnpolyh p n\ \ isnpolyh p n'" -by (induct p rule: isnpolyh.induct, auto) + by (induct p rule: isnpolyh.induct) auto -definition isnpoly :: "poly \ bool" where - "isnpoly p \ isnpolyh p 0" +definition isnpoly :: "poly \ bool" + where "isnpoly p \ isnpolyh p 0" text{* polyadd preserves normal forms *} @@ -304,7 +313,8 @@ qed auto lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q" -by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left) + by (induct p q rule: polyadd.induct) + (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left) lemma polyadd_norm: "\ isnpoly p ; isnpoly q\ \ isnpoly (polyadd p q)" using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp @@ -332,14 +342,14 @@ qed auto lemma headnz[simp]: "\isnpolyh p n ; p \ 0\<^sub>p\ \ headn p m \ 0\<^sub>p" - by (induct p arbitrary: n rule: headn.induct, auto) + by (induct p arbitrary: n rule: headn.induct) auto lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \ degree p = 0" - by (induct p arbitrary: n rule: degree.induct, auto) + by (induct p arbitrary: n rule: degree.induct) auto lemma degreen_0[simp]: "isnpolyh p n \ m < n \ degreen p m = 0" - by (induct p arbitrary: n rule: degreen.induct, auto) + by (induct p arbitrary: n rule: degreen.induct) auto lemma degree_isnpolyh_Suc': "n > 0 \ isnpolyh p n \ degree p = 0" - by (induct p arbitrary: n rule: degree.induct, auto) + by (induct p arbitrary: n rule: degree.induct) auto lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \ degree c = 0" using degree_isnpolyh_Suc by auto @@ -352,9 +362,9 @@ shows "degreen (p +\<^sub>p q) m \ max (degreen p m) (degreen q m)" using np nq m proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct) - case (2 c c' n' p' n0 n1) thus ?case by (cases n', simp_all) + case (2 c c' n' p' n0 n1) thus ?case by (cases n') simp_all next - case (3 c n p c' n0 n1) thus ?case by (cases n, auto) + case (3 c n p c' n0 n1) thus ?case by (cases n) auto next case (4 c n p c' n' p' n0 n1 m) have "n' = n \ n < n' \ n' < n" by arith @@ -377,7 +387,8 @@ moreover {assume eq: "n = n'" hence ?case using 4 apply (cases "p +\<^sub>p p' = 0\<^sub>p") apply (auto simp add: Let_def) - by blast + apply blast + done } ultimately have ?case by blast} ultimately show ?case by blast @@ -385,13 +396,14 @@ lemma polymul_properties: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \ min n0 n1" + and np: "isnpolyh p n0" + and nq: "isnpolyh q n1" + and m: "m \ min n0 n1" shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" - and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \ q = 0\<^sub>p)" - and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \ q = 0\<^sub>p) then 0 - else degreen p m + degreen q m)" + and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \ q = 0\<^sub>p)" + and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \ q = 0\<^sub>p) then 0 else degreen p m + degreen q m)" using np nq m -proof(induct p q arbitrary: n0 n1 m rule: polymul.induct) +proof (induct p q arbitrary: n0 n1 m rule: polymul.induct) case (2 c c' n' p') { case (1 n0 n1) with "2.hyps"(4-6)[of n' n' n'] @@ -430,7 +442,7 @@ with "4.hyps"(16-17)[OF cnp np', of "n'"] "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp' have ?case - by (cases "Suc n' = n", simp_all add: min_def) + by (cases "Suc n' = n") (simp_all add: min_def) } moreover { assume "n' = n" with "4.hyps"(16-17)[OF cnp np', of n] @@ -525,35 +537,41 @@ qed auto lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)" -by(induct p q rule: polymul.induct, auto simp add: field_simps) + by (induct p q rule: polymul.induct) (auto simp add: field_simps) lemma polymul_normh: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\isnpolyh p n0 ; isnpolyh q n1\ \ isnpolyh (p *\<^sub>p q) (min n0 n1)" using polymul_properties(1) by blast + lemma polymul_eq0_iff: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\ isnpolyh p n0 ; isnpolyh q n1\ \ (p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \ q = 0\<^sub>p) " using polymul_properties(2) by blast -lemma polymul_degreen: + +lemma polymul_degreen: (* FIXME duplicate? *) assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - shows "\ isnpolyh p n0 ; isnpolyh q n1 ; m \ min n0 n1\ \ degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \ q = 0\<^sub>p) then 0 else degreen p m + degreen q m)" + shows "\ isnpolyh p n0 ; isnpolyh q n1 ; m \ min n0 n1\ \ + degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \ q = 0\<^sub>p) then 0 else degreen p m + degreen q m)" using polymul_properties(3) by blast + lemma polymul_norm: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\ isnpoly p; isnpoly q\ \ isnpoly (polymul p q)" using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp lemma headconst_zero: "isnpolyh p n0 \ headconst p = 0\<^sub>N \ p = 0\<^sub>p" - by (induct p arbitrary: n0 rule: headconst.induct, auto) + by (induct p arbitrary: n0 rule: headconst.induct) auto lemma headconst_isnormNum: "isnpolyh p n0 \ isnormNum (headconst p)" - by (induct p arbitrary: n0, auto) + by (induct p arbitrary: n0) auto -lemma monic_eqI: assumes np: "isnpolyh p n0" - shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})" +lemma monic_eqI: + assumes np: "isnpolyh p n0" + shows "INum (headconst p) * Ipoly bs (fst (monic p)) = + (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})" unfolding monic_def Let_def -proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np]) +proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np]) let ?h = "headconst p" assume pz: "p \ 0\<^sub>p" {assume hz: "INum ?h = (0::'a)" @@ -567,14 +585,14 @@ text{* polyneg is a negation and preserves normal forms *} lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p" -by (induct p rule: polyneg.induct, auto) + by (induct p rule: polyneg.induct) auto lemma polyneg0: "isnpolyh p n \ ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)" - by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def) + by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: Nneg_def) lemma polyneg_polyneg: "isnpolyh p n0 \ ~\<^sub>p (~\<^sub>p p) = p" - by (induct p arbitrary: n0 rule: polyneg.induct, auto) + by (induct p arbitrary: n0 rule: polyneg.induct) auto lemma polyneg_normh: "\n. isnpolyh p n \ isnpolyh (polyneg p) n " -by (induct p rule: polyneg.induct, auto simp add: polyneg0) + by (induct p rule: polyneg.induct) (auto simp add: polyneg0) lemma polyneg_norm: "isnpoly p \ isnpoly (polyneg p)" using isnpoly_def polyneg_normh by simp @@ -583,29 +601,31 @@ text{* polysub is a substraction and preserves normal forms *} lemma polysub[simp]: "Ipoly bs (polysub p q) = (Ipoly bs p) - (Ipoly bs q)" -by (simp add: polysub_def polyneg polyadd) + by (simp add: polysub_def) lemma polysub_normh: "\ n0 n1. \ isnpolyh p n0 ; isnpolyh q n1\ \ isnpolyh (polysub p q) (min n0 n1)" -by (simp add: polysub_def polyneg_normh polyadd_normh) + by (simp add: polysub_def polyneg_normh polyadd_normh) lemma polysub_norm: "\ isnpoly p; isnpoly q\ \ isnpoly (polysub p q)" using polyadd_norm polyneg_norm by (simp add: polysub_def) -lemma polysub_same_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" +lemma polysub_same_0[simp]: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpolyh p n0 \ polysub p p = 0\<^sub>p" -unfolding polysub_def split_def fst_conv snd_conv -by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def]) + unfolding polysub_def split_def fst_conv snd_conv + by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def]) lemma polysub_0: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\ isnpolyh p n0 ; isnpolyh q n1\ \ (p -\<^sub>p q = 0\<^sub>p) = (p = q)" unfolding polysub_def split_def fst_conv snd_conv by (induct p q arbitrary: n0 n1 rule:polyadd.induct) - (auto simp: Nsub0[simplified Nsub_def] Let_def) + (auto simp: Nsub0[simplified Nsub_def] Let_def) text{* polypow is a power function and preserves normal forms *} lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n" -proof(induct n rule: polypow.induct) - case 1 thus ?case by simp +proof (induct n rule: polypow.induct) + case 1 + thus ?case by simp next case (2 n) let ?q = "polypow ((Suc n) div 2) p" @@ -613,19 +633,21 @@ have "odd (Suc n) \ even (Suc n)" by simp moreover {assume odd: "odd (Suc n)" - have th: "(Suc (Suc (Suc (0\nat)) * (Suc n div Suc (Suc (0\nat))))) = Suc n div 2 + Suc n div 2 + 1" by arith + have th: "(Suc (Suc (Suc (0\nat)) * (Suc n div Suc (Suc (0\nat))))) = Suc n div 2 + Suc n div 2 + 1" + by arith from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" by (simp add: Let_def) also have "\ = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)" using "2.hyps" by simp also have "\ = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)" - apply (simp only: power_add power_one_right) by simp + by (simp only: power_add power_one_right) simp also have "\ = (Ipoly bs p) ^ (Suc (Suc (Suc (0\nat)) * (Suc n div Suc (Suc (0\nat)))))" by (simp only: th) finally have ?case using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp } moreover {assume even: "even (Suc n)" - have th: "(Suc (Suc (0\nat))) * (Suc n div Suc (Suc (0\nat))) = Suc n div 2 + Suc n div 2" by arith + have th: "(Suc (Suc (0\nat))) * (Suc n div Suc (Suc (0\nat))) = Suc n div 2 + Suc n div 2" + by arith from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def) also have "\ = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)" using "2.hyps" apply (simp only: power_add) by simp @@ -634,7 +656,7 @@ qed lemma polypow_normh: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpolyh p n \ isnpolyh (polypow k p) n" proof (induct k arbitrary: n rule: polypow.induct) case (2 k n) @@ -653,23 +675,28 @@ text{* Finally the whole normalization *} -lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})" -by (induct p rule:polynate.induct, auto) +lemma polynate [simp]: + "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})" + by (induct p rule:polynate.induct) auto lemma polynate_norm[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpoly (polynate p)" - by (induct p rule: polynate.induct, simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm) (simp_all add: isnpoly_def) + by (induct p rule: polynate.induct) + (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm, + simp_all add: isnpoly_def) text{* shift1 *} lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)" -by (simp add: shift1_def polymul) + by (simp add: shift1_def) lemma shift1_isnpoly: - assumes pn: "isnpoly p" and pnz: "p \ 0\<^sub>p" shows "isnpoly (shift1 p) " - using pn pnz by (simp add: shift1_def isnpoly_def ) + assumes pn: "isnpoly p" + and pnz: "p \ 0\<^sub>p" + shows "isnpoly (shift1 p) " + using pn pnz by (simp add: shift1_def isnpoly_def) lemma shift1_nz[simp]:"shift1 p \ 0\<^sub>p" by (simp add: shift1_def) @@ -678,18 +705,22 @@ by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1) lemma funpow_isnpolyh: - assumes f: "\ p. isnpolyh p n \ isnpolyh (f p) n "and np: "isnpolyh p n" + assumes f: "\ p. isnpolyh p n \ isnpolyh (f p) n" + and np: "isnpolyh p n" shows "isnpolyh (funpow k f p) n" - using f np by (induct k arbitrary: p, auto) + using f np by (induct k arbitrary: p) auto -lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)" - by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc ) +lemma funpow_shift1: + "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = + Ipoly bs (Mul (Pw (Bound 0) n) p)" + by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1) lemma shift1_isnpolyh: "isnpolyh p n0 \ p\ 0\<^sub>p \ isnpolyh (shift1 p) 0" using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def) lemma funpow_shift1_1: - "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)" + "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = + Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)" by (simp add: funpow_shift1) lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)" @@ -697,23 +728,29 @@ lemma behead: assumes np: "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})" + 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 proof (induct p arbitrary: n rule: behead.induct) case (1 c p n) hence pn: "isnpolyh p n" by simp from 1(1)[OF pn] have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . - then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p") - by (simp_all add: th[symmetric] field_simps power_Suc) + then show ?case using "1.hyps" + apply (simp add: Let_def,cases "behead p = 0\<^sub>p") + apply (simp_all add: th[symmetric] field_simps) + done qed (auto simp add: Let_def) lemma behead_isnpolyh: - assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n" - using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono) + assumes np: "isnpolyh p n" + shows "isnpolyh (behead p) n" + using np by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono) + subsection{* Miscellaneous lemmas about indexes, decrementation, substitution etc ... *} + lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \ polybound0 p" -proof(induct p arbitrary: n rule: poly.induct, auto) +proof (induct p arbitrary: n rule: poly.induct, auto) case (goal1 c n p n') hence "n = Suc (n - 1)" by simp hence "isnpolyh p (Suc (n - 1))" using `isnpolyh p n` by simp @@ -721,27 +758,29 @@ qed lemma isconstant_polybound0: "isnpolyh p n0 \ isconstant p \ polybound0 p" -by (induct p arbitrary: n0 rule: isconstant.induct, auto simp add: isnpolyh_polybound0) + by (induct p arbitrary: n0 rule: isconstant.induct) (auto simp add: isnpolyh_polybound0) -lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \ p = 0\<^sub>p" by (induct p, auto) +lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \ p = 0\<^sub>p" + by (induct p) auto lemma decrpoly_normh: "isnpolyh p n0 \ polybound0 p \ isnpolyh (decrpoly p) (n0 - 1)" - apply (induct p arbitrary: n0, auto) + apply (induct p arbitrary: n0) + apply auto apply (atomize) apply (erule_tac x = "Suc nat" in allE) apply auto done lemma head_polybound0: "isnpolyh p n0 \ polybound0 (head p)" - by (induct p arbitrary: n0 rule: head.induct, auto intro: isnpolyh_polybound0) + by (induct p arbitrary: n0 rule: head.induct) (auto intro: isnpolyh_polybound0) lemma polybound0_I: assumes nb: "polybound0 a" shows "Ipoly (b#bs) a = Ipoly (b'#bs) a" -using nb -by (induct a rule: poly.induct) auto -lemma polysubst0_I: - shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t" + using nb + 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': @@ -749,16 +788,18 @@ 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'"]) -lemma decrpoly: assumes nb: "polybound0 t" +lemma decrpoly: + assumes nb: "polybound0 t" shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)" - using nb by (induct t rule: decrpoly.induct, simp_all) + using nb by (induct t rule: decrpoly.induct) simp_all -lemma polysubst0_polybound0: assumes nb: "polybound0 t" +lemma polysubst0_polybound0: + assumes nb: "polybound0 t" shows "polybound0 (polysubst0 t a)" -using nb by (induct a rule: poly.induct, auto) + using nb by (induct a rule: poly.induct) auto lemma degree0_polybound0: "isnpolyh p n \ degree p = 0 \ polybound0 p" - by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0) + by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0) primrec maxindex :: "poly \ nat" where "maxindex (Bound n) = n + 1" @@ -770,11 +811,11 @@ | "maxindex (Pw p n) = maxindex p" | "maxindex (C x) = 0" -definition wf_bs :: "'a list \ poly \ bool" where - "wf_bs bs p = (length bs \ maxindex p)" +definition wf_bs :: "'a list \ poly \ bool" + where "wf_bs bs p = (length bs \ maxindex p)" lemma wf_bs_coefficients: "wf_bs bs p \ \ c \ set (coefficients p). wf_bs bs c" -proof(induct p rule: coefficients.induct) +proof (induct p rule: coefficients.induct) case (1 c p) show ?case proof @@ -791,12 +832,13 @@ qed simp_all lemma maxindex_coefficients: " \c\ set (coefficients p). maxindex c \ maxindex p" -by (induct p rule: coefficients.induct, auto) + by (induct p rule: coefficients.induct) auto lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p" - unfolding wf_bs_def by (induct p, auto simp add: nth_append) + unfolding wf_bs_def by (induct p) (auto simp add: nth_append) -lemma take_maxindex_wf: assumes wf: "wf_bs bs p" +lemma take_maxindex_wf: + assumes wf: "wf_bs bs p" shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p" proof- let ?ip = "maxindex p" @@ -808,7 +850,7 @@ qed lemma decr_maxindex: "polybound0 p \ maxindex (decrpoly p) = maxindex p - 1" - by (induct p, auto) + by (induct p) auto lemma wf_bs_insensitive: "length bs = length bs' \ wf_bs bs p = wf_bs bs' p" unfolding wf_bs_def by simp @@ -819,22 +861,28 @@ lemma wf_bs_coefficients': "\c \ set (coefficients p). wf_bs bs c \ wf_bs (x#bs) p" -by(induct p rule: coefficients.induct, auto simp add: wf_bs_def) + by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def) lemma coefficients_Nil[simp]: "coefficients p \ []" - by (induct p rule: coefficients.induct, simp_all) + by (induct p rule: coefficients.induct) simp_all lemma coefficients_head: "last (coefficients p) = head p" - by (induct p rule: coefficients.induct, auto) + by (induct p rule: coefficients.induct) auto lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \ wf_bs (x#bs) p" - unfolding wf_bs_def by (induct p rule: decrpoly.induct, auto) + unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto lemma length_le_list_ex: "length xs \ n \ \ ys. length (xs @ ys) = n" apply (rule exI[where x="replicate (n - length xs) z"]) - by simp + apply simp + done + lemma isnpolyh_Suc_const:"isnpolyh p (Suc n) \ isconstant p" -by (cases p, auto) (case_tac "nat", simp_all) + apply (cases p) + apply auto + apply (case_tac "nat") + apply simp_all + done lemma wf_bs_polyadd: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p +\<^sub>p q)" unfolding wf_bs_def @@ -852,11 +900,12 @@ done lemma wf_bs_polyneg: "wf_bs bs p \ wf_bs bs (~\<^sub>p p)" - unfolding wf_bs_def by (induct p rule: polyneg.induct, auto) + unfolding wf_bs_def by (induct p rule: polyneg.induct) auto lemma wf_bs_polysub: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p -\<^sub>p q)" unfolding polysub_def split_def fst_conv snd_conv using wf_bs_polyadd wf_bs_polyneg by blast + subsection{* Canonicity of polynomial representation, see lemma isnpolyh_unique*} definition "polypoly bs p = map (Ipoly bs) (coefficients p)" @@ -874,8 +923,8 @@ lemma coefficients_isconst: "isnpolyh p n \ \q\set (coefficients p). isconstant q" - by (induct p arbitrary: n rule: coefficients.induct, - auto simp add: isnpolyh_Suc_const) + by (induct p arbitrary: n rule: coefficients.induct) + (auto simp add: isnpolyh_Suc_const) lemma polypoly_polypoly': assumes np: "isnpolyh p n0" @@ -896,12 +945,14 @@ qed lemma polypoly_poly: - assumes np: "isnpolyh p n0" shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x" + assumes np: "isnpolyh p n0" + shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x" using np -by (induct p arbitrary: n0 bs rule: coefficients.induct, auto simp add: polypoly_def) + by (induct p arbitrary: n0 bs rule: coefficients.induct) (auto simp add: polypoly_def) lemma polypoly'_poly: - assumes np: "isnpolyh p n0" shows "\p\\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x" + assumes np: "isnpolyh p n0" + shows "\p\\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x" using polypoly_poly[OF np, simplified polypoly_polypoly'[OF np]] . @@ -909,29 +960,34 @@ assumes np: "isnpolyh p n0" and nb: "polybound0 p" shows "polypoly bs p = [Ipoly bs p]" using np nb unfolding polypoly_def - by (cases p, auto, case_tac nat, auto) + apply (cases p) + apply auto + apply (case_tac nat) + apply auto + done lemma head_isnpolyh: "isnpolyh p n0 \ isnpolyh (head p) n0" - by (induct p rule: head.induct, auto) + by (induct p rule: head.induct) auto lemma headn_nz[simp]: "isnpolyh p n0 \ (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)" - by (cases p,auto) + by (cases p) auto lemma head_eq_headn0: "head p = headn p 0" - by (induct p rule: head.induct, simp_all) + by (induct p rule: head.induct) simp_all lemma head_nz[simp]: "isnpolyh p n0 \ (head p = 0\<^sub>p) = (p = 0\<^sub>p)" by (simp add: head_eq_headn0) lemma isnpolyh_zero_iff: - assumes nq: "isnpolyh p n0" and eq :"\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, field_inverse_zero, power})" + assumes nq: "isnpolyh p n0" + and eq :"\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, field_inverse_zero, power})" shows "p = 0\<^sub>p" -using nq eq + using nq eq proof (induct "maxindex p" arbitrary: p n0 rule: less_induct) case less note np = `isnpolyh p n0` and zp = `\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)` {assume nz: "maxindex p = 0" - then obtain c where "p = C c" using np by (cases p, auto) + then obtain c where "p = C c" using np by (cases p) auto with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp} moreover {assume nz: "maxindex p \ 0" @@ -958,7 +1014,7 @@ hence "\ x. Ipoly (x#(?ts @ xs)) p = 0" by simp with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a] have "\x. poly (polypoly' (?ts @ xs) p) x = poly [] x" by simp - hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) + hence "poly (polypoly' (?ts @ xs) p) = poly []" by auto hence "\ c \ set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0" using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff) with coefficients_head[of p, symmetric] @@ -975,7 +1031,8 @@ qed lemma isnpolyh_unique: - assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1" + assumes np:"isnpolyh p n0" + and nq: "isnpolyh q n1" shows "(\bs. \p\\<^sub>p\<^bsup>bs\<^esup> = (\q\\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0, field_inverse_zero, power})) \ p = q" proof(auto) assume H: "\bs. (\p\\<^sub>p\<^bsup>bs\<^esup> ::'a)= \q\\<^sub>p\<^bsup>bs\<^esup>" @@ -989,69 +1046,91 @@ text{* consequences of unicity on the algorithms for polynomial normalization *} -lemma polyadd_commute: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p" +lemma polyadd_commute: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + and np: "isnpolyh p n0" + and nq: "isnpolyh q n1" + shows "p +\<^sub>p q = q +\<^sub>p p" using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp lemma one_normh: "isnpolyh (1)\<^sub>p n" by simp + lemma polyadd_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p" + and np: "isnpolyh p n0" + shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p" using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all lemma polymul_1[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np: "isnpolyh p n0" shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + and np: "isnpolyh p n0" + shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p" using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all + lemma polymul_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np: "isnpolyh p n0" shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" and "0\<^sub>p *\<^sub>p p = 0\<^sub>p" + and np: "isnpolyh p n0" + shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" and "0\<^sub>p *\<^sub>p p = 0\<^sub>p" using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all lemma polymul_commute: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np:"isnpolyh p n0" and nq: "isnpolyh q n1" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + and np:"isnpolyh p n0" + and nq: "isnpolyh q n1" shows "p *\<^sub>p q = q *\<^sub>p p" -using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\{field_char_0, field_inverse_zero, power}"] by simp + using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\{field_char_0, field_inverse_zero, power}"] + by simp -declare polyneg_polyneg[simp] +declare polyneg_polyneg [simp] -lemma isnpolyh_polynate_id[simp]: +lemma isnpolyh_polynate_id [simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np:"isnpolyh p n0" shows "polynate p = p" - using isnpolyh_unique[where ?'a= "'a::{field_char_0, field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0, field_inverse_zero}"] by simp + and np:"isnpolyh p n0" + shows "polynate p = p" + using isnpolyh_unique[where ?'a= "'a::{field_char_0, field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0, field_inverse_zero}"] + by simp lemma polynate_idempotent[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "polynate (polynate p) = polynate p" using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] . lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)" unfolding poly_nate_def polypoly'_def .. -lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\x:: 'a ::{field_char_0, field_inverse_zero}. \p\\<^sub>p\<^bsup>x # bs\<^esup>)" + +lemma poly_nate_poly: + "poly (poly_nate bs p) = (\x:: 'a ::{field_char_0, field_inverse_zero}. \p\\<^sub>p\<^bsup>x # bs\<^esup>)" using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p] - unfolding poly_nate_polypoly' by (auto intro: ext) + unfolding poly_nate_polypoly' by auto + subsection{* heads, degrees and all that *} + lemma degree_eq_degreen0: "degree p = degreen p 0" - by (induct p rule: degree.induct, simp_all) + by (induct p rule: degree.induct) simp_all -lemma degree_polyneg: assumes n: "isnpolyh p n" +lemma degree_polyneg: + assumes n: "isnpolyh p n" shows "degree (polyneg p) = degree p" - using n - by (induct p arbitrary: n rule: polyneg.induct, simp_all) (case_tac na, auto) + apply (induct p arbitrary: n rule: polyneg.induct) + using n apply simp_all + apply (case_tac na) + apply auto + done lemma degree_polyadd: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "degree (p +\<^sub>p q) \ max (degree p) (degree q)" -using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp + using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp -lemma degree_polysub: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" +lemma degree_polysub: + assumes np: "isnpolyh p n0" + and nq: "isnpolyh q n1" shows "degree (p -\<^sub>p q) \ max (degree p) (degree q)" proof- from nq have nq': "isnpolyh (~\<^sub>p q) n1" using polyneg_normh by simp @@ -1060,24 +1139,25 @@ lemma degree_polysub_samehead: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" - and d: "degree p = degree q" + and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" + and d: "degree p = degree q" shows "degree (p -\<^sub>p q) < degree p \ (p -\<^sub>p q = 0\<^sub>p)" -unfolding polysub_def split_def fst_conv snd_conv -using np nq h d -proof(induct p q rule:polyadd.induct) - case (1 c c') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) + unfolding polysub_def split_def fst_conv snd_conv + using np nq h d +proof (induct p q rule: polyadd.induct) + case (1 c c') + thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) next case (2 c c' n' p') from 2 have "degree (C c) = degree (CN c' n' p')" by simp - hence nz:"n' > 0" by (cases n', auto) - hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto) + hence nz:"n' > 0" by (cases n') auto + hence "head (CN c' n' p') = CN c' n' p'" by (cases n') auto with 2 show ?case by simp next case (3 c n p c') hence "degree (C c') = degree (CN c n p)" by simp - hence nz:"n > 0" by (cases n, auto) - hence "head (CN c n p) = CN c n p" by (cases n, auto) + hence nz:"n > 0" by (cases n) auto + hence "head (CN c n p) = CN c n p" by (cases n) auto with 3 show ?case by simp next case (4 c n p c' n' p') @@ -1096,36 +1176,43 @@ moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')} moreover {assume nz: "n > 0" with nn' H(3) have cc':"c = c'" and pp': "p = p'" by (cases n, auto)+ - hence ?case using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] polysub_same_0[OF c'nh, simplified polysub_def] using nn' 4 by (simp add: Let_def)} + hence ?case + using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] polysub_same_0[OF c'nh, simplified polysub_def] + using nn' 4 by (simp add: Let_def)} ultimately have ?case by blast} moreover {assume nn': "n < n'" hence n'p: "n' > 0" by simp - hence headcnp':"head (CN c' n' p') = CN c' n' p'" by (cases n', simp_all) - have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" using 4 nn' by (cases n', simp_all) - hence "n > 0" by (cases n, simp_all) - hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto) + hence headcnp':"head (CN c' n' p') = CN c' n' p'" by (cases n') simp_all + have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" + using 4 nn' by (cases n', simp_all) + hence "n > 0" by (cases n) simp_all + hence headcnp: "head (CN c n p) = CN c n p" by (cases n) auto from H(3) headcnp headcnp' nn' have ?case by auto} moreover {assume nn': "n > n'" hence np: "n > 0" by simp - hence headcnp:"head (CN c n p) = CN c n p" by (cases n, simp_all) + hence headcnp:"head (CN c n p) = CN c n p" by (cases n) simp_all from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp - from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all) - with degcnpeq have "n' > 0" by (cases n', simp_all) - hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto) + from np have degcnp: "degree (CN c n p) = 0" by (cases n) simp_all + with degcnpeq have "n' > 0" by (cases n') simp_all + hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n') auto from H(3) headcnp headcnp' nn' have ?case by auto} ultimately show ?case by blast qed auto lemma shift1_head : "isnpolyh p n0 \ head (shift1 p) = head p" -by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def) + by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def) lemma funpow_shift1_head: "isnpolyh p n0 \ p\ 0\<^sub>p \ head (funpow k shift1 p) = head p" -proof(induct k arbitrary: n0 p) - case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh) +proof (induct k arbitrary: n0 p) + case 0 + thus ?case by auto +next + case (Suc k n0 p) + hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh) with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" and "head (shift1 p) = head p" by (simp_all add: shift1_head) thus ?case by (simp add: funpow_swap1) -qed auto +qed lemma shift1_degree: "degree (shift1 p) = 1 + degree p" by (simp add: shift1_def) @@ -1133,47 +1220,52 @@ by (induct k arbitrary: p) (auto simp add: shift1_degree) lemma funpow_shift1_nz: "p \ 0\<^sub>p \ funpow n shift1 p \ 0\<^sub>p" - by (induct n arbitrary: p) (simp_all add: funpow.simps) + by (induct n arbitrary: p) simp_all lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \ head p = p" - by (induct p arbitrary: n rule: degree.induct, auto) + by (induct p arbitrary: n rule: degree.induct) auto lemma headn_0[simp]: "isnpolyh p n \ m < n \ headn p m = p" - by (induct p arbitrary: n rule: degreen.induct, auto) + by (induct p arbitrary: n rule: degreen.induct) auto lemma head_isnpolyh_Suc': "n > 0 \ isnpolyh p n \ head p = p" - by (induct p arbitrary: n rule: degree.induct, auto) + by (induct p arbitrary: n rule: degree.induct) auto lemma head_head[simp]: "isnpolyh p n0 \ head (head p) = head p" - by (induct p rule: head.induct, auto) + by (induct p rule: head.induct) auto lemma polyadd_eq_const_degree: - "\ isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\ \ degree p = degree q" + "isnpolyh p n0 \ isnpolyh q n1 \ polyadd p q = C c \ degree p = degree q" using polyadd_eq_const_degreen degree_eq_degreen0 by simp -lemma polyadd_head: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" - and deg: "degree p \ degree q" +lemma polyadd_head: + assumes np: "isnpolyh p n0" + and nq: "isnpolyh q n1" + and deg: "degree p \ degree q" shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)" -using np nq deg -apply(induct p q arbitrary: n0 n1 rule: polyadd.induct,simp_all) -apply (case_tac n', simp, simp) -apply (case_tac n, simp, simp) -apply (case_tac n, case_tac n', simp add: Let_def) -apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p") -apply (auto simp add: polyadd_eq_const_degree) -apply (metis head_nz) -apply (metis head_nz) -apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq) -by (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans) + using np nq deg + apply (induct p q arbitrary: n0 n1 rule: polyadd.induct) + using np + apply simp_all + apply (case_tac n', simp, simp) + apply (case_tac n, simp, simp) + apply (case_tac n, case_tac n', simp add: Let_def) + apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p") + apply (auto simp add: polyadd_eq_const_degree) + apply (metis head_nz) + apply (metis head_nz) + apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq) + apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans) + done lemma polymul_head_polyeq: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\isnpolyh p n0; isnpolyh q n1 ; p \ 0\<^sub>p ; q \ 0\<^sub>p \ \ head (p *\<^sub>p q) = head p *\<^sub>p head q" proof (induct p q arbitrary: n0 n1 rule: polymul.induct) case (2 c c' n' p' n0 n1) hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum c" by (simp_all add: head_isnpolyh) - thus ?case using 2 by (cases n', auto) + thus ?case using 2 by (cases n') auto next case (3 c n p c' n0 n1) hence "isnpolyh (head (CN c n p)) n0" "isnormNum c'" by (simp_all add: head_isnpolyh) - thus ?case using 3 by (cases n, auto) + thus ?case using 3 by (cases n) auto next case (4 c n p c' n' p' n0 n1) hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')" @@ -1182,13 +1274,22 @@ have "n < n' \ n' < n \ n = n'" by arith moreover {assume nn': "n < n'" hence ?case - using norm - "4.hyps"(2)[OF norm(1,6)] - "4.hyps"(1)[OF norm(2,6)] by (simp, cases n, simp,cases n', simp_all)} + using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)] + apply simp + apply (cases n) + apply simp + apply (cases n') + apply simp_all + done } moreover {assume nn': "n'< n" - hence ?case using norm "4.hyps"(6) [OF norm(5,3)] - "4.hyps"(5)[OF norm(5,4)] - by (simp,cases n',simp,cases n,auto)} + hence ?case + using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] + apply simp + apply (cases n') + apply simp + apply (cases n) + apply auto + done } moreover {assume nn': "n' = n" from nn' polymul_normh[OF norm(5,4)] have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def) @@ -1218,44 +1319,50 @@ qed simp_all lemma degree_coefficients: "degree p = length (coefficients p) - 1" - by(induct p rule: degree.induct, auto) + by (induct p rule: degree.induct) auto lemma degree_head[simp]: "degree (head p) = 0" - by (induct p rule: head.induct, auto) + by (induct p rule: head.induct) auto lemma degree_CN: "isnpolyh p n \ degree (CN c n p) \ 1 + degree p" - by (cases n, simp_all) + by (cases n) simp_all lemma degree_CN': "isnpolyh p n \ degree (CN c n p) \ degree p" - by (cases n, simp_all) + by (cases n) simp_all -lemma polyadd_different_degree: "\isnpolyh p n0 ; isnpolyh q n1; degree p \ degree q\ \ degree (polyadd p q) = max (degree p) (degree q)" +lemma polyadd_different_degree: + "\isnpolyh p n0 ; isnpolyh q n1; degree p \ degree q\ \ + degree (polyadd p q) = max (degree p) (degree q)" using polyadd_different_degreen degree_eq_degreen0 by simp lemma degreen_polyneg: "isnpolyh p n0 \ degreen (~\<^sub>p p) m = degreen p m" - by (induct p arbitrary: n0 rule: polyneg.induct, auto) + by (induct p arbitrary: n0 rule: polyneg.induct) auto lemma degree_polymul: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np: "isnpolyh p n0" and nq: "isnpolyh q n1" + and np: "isnpolyh p n0" + and nq: "isnpolyh q n1" shows "degree (p *\<^sub>p q) \ degree p + degree q" using polymul_degreen[OF np nq, where m="0"] degree_eq_degreen0 by simp lemma polyneg_degree: "isnpolyh p n \ degree (polyneg p) = degree p" - by (induct p arbitrary: n rule: degree.induct, auto) + by (induct p arbitrary: n rule: degree.induct) auto lemma polyneg_head: "isnpolyh p n \ head(polyneg p) = polyneg (head p)" - by (induct p arbitrary: n rule: degree.induct, auto) + by (induct p arbitrary: n rule: degree.induct) auto + subsection {* Correctness of polynomial pseudo division *} lemma polydivide_aux_properties: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np: "isnpolyh p n0" and ns: "isnpolyh s n1" - and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \ 0\<^sub>p" + and np: "isnpolyh p n0" + and ns: "isnpolyh s n1" + and ap: "head p = a" + and ndp: "degree p = n" and pnz: "p \ 0\<^sub>p" shows "(polydivide_aux a n p k s = (k',r) \ (k' \ k) \ (degree r = 0 \ degree r < degree p) \ (\nr. isnpolyh r nr) \ (\q n1. isnpolyh q n1 \ ((polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))" using ns -proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct) +proof (induct "degree s" arbitrary: s k k' r n1 rule: less_induct) case less let ?qths = "\q n1. isnpolyh q n1 \ (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" let ?ths = "polydivide_aux a n p k s = (k', r) \ k \ k' \ (degree r = 0 \ degree r < degree p) @@ -1272,12 +1379,20 @@ from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def) from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap have nakk':"isnpolyh ?akk' 0" by blast - {assume sz: "s = 0\<^sub>p" - hence ?ths using np polydivide_aux.simps apply clarsimp by (rule exI[where x="0\<^sub>p"], simp) } + { assume sz: "s = 0\<^sub>p" + hence ?ths using np polydivide_aux.simps + apply clarsimp + apply (rule exI[where x="0\<^sub>p"]) + apply simp + done } moreover {assume sz: "s \ 0\<^sub>p" {assume dn: "degree s < n" - hence "?ths" using ns ndp np polydivide_aux.simps by auto (rule exI[where x="0\<^sub>p"],simp) } + hence "?ths" using ns ndp np polydivide_aux.simps + apply auto + apply (rule exI[where x="0\<^sub>p"]) + apply simp + done } moreover {assume dn': "\ degree s < n" hence dn: "degree s \ n" by arith have degsp': "degree s = degree ?p'" @@ -1332,9 +1447,14 @@ {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p" 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}"] have " \(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp - hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp - by (simp only: funpow_shift1_1) simp - hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast + hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" + using np nxdn + apply simp + apply (simp only: funpow_shift1_1) + apply simp + done + hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] + by blast {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')" @@ -1385,12 +1505,16 @@ {fix bs:: "'a::{field_char_0, field_inverse_zero} list" from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric] - 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)" by simp - hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r" - by (simp add: field_simps power_Suc) - hence "Ipoly bs a ^ (k' - k) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r" - by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"]) - hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" + 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)" + by simp + hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = + Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r" + by (simp add: field_simps) + hence "Ipoly bs a ^ (k' - k) * Ipoly bs s = + Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r" + by (simp add: kk'' funpow_shift1_1[where n="degree s - n" and p="p"]) + hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = + Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" by (simp add: field_simps)} hence ieq:"\(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)" by auto @@ -1415,7 +1539,8 @@ by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"]) hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp } - hence hth: "\ (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" .. + hence hth: "\ (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) = + Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" .. from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns] @@ -1426,17 +1551,20 @@ have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def) with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn] polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq - have ?ths apply (clarsimp simp add: Let_def) - apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp + have ?ths + apply (clarsimp simp add: Let_def) + apply (rule exI[where x="?b *\<^sub>p ?xdn"]) + apply simp apply (rule exI[where x="0"], simp) - done} - hence ?ths by blast} - ultimately have ?ths 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"] - head_nz[OF np] pnz sz ap[symmetric] + done } + hence ?ths by blast } + ultimately have ?ths + 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"] + head_nz[OF np] pnz sz ap[symmetric] by (simp add: degree_eq_degreen0[symmetric]) blast } ultimately have ?ths by blast } - ultimately have ?ths by blast} + ultimately have ?ths by blast } ultimately show ?ths by blast qed @@ -1462,16 +1590,18 @@ done qed + subsection{* More about polypoly and pnormal etc *} definition "isnonconstant p = (\ isconstant p)" -lemma isnonconstant_pnormal_iff: assumes nc: "isnonconstant p" +lemma isnonconstant_pnormal_iff: + assumes nc: "isnonconstant p" shows "pnormal (polypoly bs p) \ Ipoly bs (head p) \ 0" proof let ?p = "polypoly bs p" assume H: "pnormal ?p" - have csz: "coefficients p \ []" using nc by (cases p, auto) + have csz: "coefficients p \ []" using nc by (cases p) auto from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] pnormal_last_nonzero[OF H] @@ -1479,7 +1609,7 @@ next assume h: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" let ?p = "polypoly bs p" - have csz: "coefficients p \ []" using nc by (cases p, auto) + have csz: "coefficients p \ []" using nc by (cases p) auto hence pz: "?p \ []" by (simp add: polypoly_def) hence lg: "length ?p > 0" by simp from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] @@ -1489,10 +1619,14 @@ lemma isnonconstant_coefficients_length: "isnonconstant p \ length (coefficients p) > 1" unfolding isnonconstant_def - apply (cases p, simp_all) - apply (case_tac nat, auto) + apply (cases p) + apply simp_all + apply (case_tac nat) + apply auto done -lemma isnonconstant_nonconstant: assumes inc: "isnonconstant p" + +lemma isnonconstant_nonconstant: + assumes inc: "isnonconstant p" shows "nonconstant (polypoly bs p) \ Ipoly bs (head p) \ 0" proof let ?p = "polypoly bs p" @@ -1511,12 +1645,14 @@ qed lemma pnormal_length: "p\[] \ pnormal p \ length (pnormalize p) = length p" - unfolding pnormal_def - apply (induct p) - apply (simp_all, case_tac "p=[]", simp_all) - done + apply (induct p) + apply (simp_all add: pnormal_def) + apply (case_tac "p = []") + apply simp_all + done -lemma degree_degree: assumes inc: "isnonconstant p" +lemma degree_degree: + assumes inc: "isnonconstant p" shows "degree p = Polynomial_List.degree (polypoly bs p) \ \head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" proof let ?p = "polypoly bs p" @@ -1538,7 +1674,9 @@ unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto qed + section{* Swaps ; Division by a certain variable *} + primrec swap:: "nat \ nat \ poly \ poly" where "swap n m (C x) = C x" | "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)" @@ -1550,37 +1688,47 @@ | "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)" -lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs" +lemma swap: + assumes nbs: "n < length bs" + and mbs: "m < length bs" shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" proof (induct t) - case (Bound k) thus ?case using nbs mbs by simp + case (Bound k) + thus ?case using nbs mbs by simp next - case (CN c k p) thus ?case using nbs mbs by simp + case (CN c k p) + thus ?case using nbs mbs by simp qed simp_all -lemma swap_swap_id[simp]: "swap n m (swap m n t) = t" - by (induct t,simp_all) -lemma swap_commute: "swap n m p = swap m n p" by (induct p, simp_all) +lemma swap_swap_id [simp]: "swap n m (swap m n t) = t" + by (induct t) simp_all + +lemma swap_commute: "swap n m p = swap m n p" + by (induct p) simp_all lemma swap_same_id[simp]: "swap n n t = t" - by (induct t, simp_all) + by (induct t) simp_all definition "swapnorm n m t = polynate (swap n m t)" -lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs" - shows "((Ipoly bs (swapnorm n m t) :: 'a\{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" +lemma swapnorm: + assumes nbs: "n < length bs" + and mbs: "m < length bs" + shows "((Ipoly bs (swapnorm n m t) :: 'a\{field_char_0, field_inverse_zero})) = + Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" using swap[OF assms] swapnorm_def by simp -lemma swapnorm_isnpoly[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" +lemma swapnorm_isnpoly [simp]: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpoly (swapnorm n m p)" unfolding swapnorm_def by simp definition "polydivideby n s p = - (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp - in (k,swapnorm 0 n h,swapnorm 0 n r))" + (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp + in (k,swapnorm 0 n h,swapnorm 0 n r))" -lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)" by (induct p, simp_all) +lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)" + by (induct p) simp_all fun isweaknpoly :: "poly \ bool" where @@ -1589,9 +1737,9 @@ | "isweaknpoly p = False" lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \ isweaknpoly p" - by (induct p arbitrary: n0, auto) + by (induct p arbitrary: n0) auto lemma swap_isweanpoly: "isweaknpoly p \ isweaknpoly (swap n m p)" - by (induct p, auto) + by (induct p) auto end \ No newline at end of file