# HG changeset patch # User wenzelm # Date 1398700139 -7200 # Node ID 309e1a61ee7c91928366dffb58a5278c6b604af5 # Parent 59f70b89e5fdb6d56deff13487af966c4cb39b45 tuned proofs; diff -r 59f70b89e5fd -r 309e1a61ee7c src/HOL/Library/Fundamental_Theorem_Algebra.thy --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Apr 28 16:17:07 2014 +0200 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Apr 28 17:48:59 2014 +0200 @@ -8,12 +8,13 @@ subsection {* Square root of complex numbers *} -definition csqrt :: "complex \ complex" where -"csqrt z = (if Im z = 0 then - if 0 \ Re z then Complex (sqrt(Re z)) 0 - else Complex 0 (sqrt(- Re z)) - else Complex (sqrt((cmod z + Re z) /2)) - ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))" +definition csqrt :: "complex \ complex" +where + "csqrt z = + (if Im z = 0 then + if 0 \ Re z then Complex (sqrt(Re z)) 0 + else Complex 0 (sqrt(- Re z)) + else Complex (sqrt((cmod z + Re z) /2)) ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))" lemma csqrt[algebra]: "(csqrt z)\<^sup>2 = z" proof- @@ -594,20 +595,27 @@ qed lemma poly_decompose: - assumes nc: "~constant(poly p)" - shows "\k a q. a\(0::'a::{idom}) \ k\0 \ + assumes nc: "\ constant (poly p)" + shows "\k a q. a \ (0::'a::{idom}) \ k \ 0 \ psize q + k + 1 = psize p \ (\z. poly p z = poly p 0 + z^k * poly (pCons a q) z)" -using nc -proof(induct p) - case 0 thus ?case by (simp add: constant_def) + using nc +proof (induct p) + case 0 + then show ?case + by (simp add: constant_def) next case (pCons c cs) - {assume C:"\z. z \ 0 \ poly cs z = 0" - {fix x y - from C have "poly (pCons c cs) x = poly (pCons c cs) y" by (cases "x=0", auto)} - with pCons.prems have False by (auto simp add: constant_def)} - hence th: "\ (\z. z \ 0 \ poly cs z = 0)" .. + { + assume C:"\z. z \ 0 \ poly cs z = 0" + { + fix x y + from C have "poly (pCons c cs) x = poly (pCons c cs) y" + by (cases "x = 0") auto + } + with pCons.prems have False by (auto simp add: constant_def) + } + then have th: "\ (\z. z \ 0 \ poly cs z = 0)" .. from poly_decompose_lemma[OF th] show ?case apply clarsimp @@ -622,17 +630,17 @@ text{* Fundamental theorem of algebra *} lemma fundamental_theorem_of_algebra: - assumes nc: "~constant(poly p)" + assumes nc: "\ constant (poly p)" shows "\z::complex. poly p z = 0" -using nc -proof(induct "psize p" arbitrary: p rule: less_induct) + using nc +proof (induct "psize p" arbitrary: p rule: less_induct) case less let ?p = "poly p" let ?ths = "\z. ?p z = 0" from nonconstant_length[OF less(2)] have n2: "psize p \ 2" . - from poly_minimum_modulus obtain c where - c: "\w. cmod (?p c) \ cmod (?p w)" by blast + from poly_minimum_modulus obtain c where c: "\w. cmod (?p c) \ cmod (?p w)" + by blast {assume pc: "?p c = 0" hence ?ths by blast} moreover {assume pc0: "?p c \ 0" @@ -797,11 +805,13 @@ lemma nullstellensatz_lemma: fixes p :: "complex poly" assumes "\x. poly p x = 0 \ poly q x = 0" - and "degree p = n" and "n \ 0" + and "degree p = n" + and "n \ 0" shows "p dvd (q ^ n)" -using assms -proof(induct n arbitrary: p q rule: nat_less_induct) - fix n::nat fix p q :: "complex poly" + using assms +proof (induct n arbitrary: p q rule: nat_less_induct) + fix n :: nat + fix p q :: "complex poly" assume IH: "\mp q. (\x. poly p x = (0::complex) \ poly q x = 0) \ degree p = m \ m \ 0 \ p dvd (q ^ m)" @@ -893,7 +903,7 @@ lemma nullstellensatz_univariate: "(\x. poly p x = (0::complex) \ poly q x = 0) \ p dvd (q ^ (degree p)) \ (p = 0 \ q = 0)" -proof- +proof - {assume pe: "p = 0" hence eq: "(\x. poly p x = (0::complex) \ poly q x = 0) \ q = 0" by (auto simp add: poly_all_0_iff_0) @@ -933,20 +943,26 @@ proof assume l: ?lhs from l[unfolded constant_def, rule_format, of _ "0"] - have th: "poly p = poly [:poly p 0:]" apply - by (rule ext, simp) - then have "p = [:poly p 0:]" by (simp add: poly_eq_poly_eq_iff) - then have "degree p = degree [:poly p 0:]" by simp - then show ?rhs by simp + have th: "poly p = poly [:poly p 0:]" + by auto + then have "p = [:poly p 0:]" + by (simp add: poly_eq_poly_eq_iff) + then have "degree p = degree [:poly p 0:]" + by simp + then show ?rhs + by simp next assume r: ?rhs then obtain k where "p = [:k:]" by (cases p) (simp split: if_splits) - then show ?lhs unfolding constant_def by auto + then show ?lhs + unfolding constant_def by auto qed -lemma divides_degree: assumes pq: "p dvd (q:: complex poly)" +lemma divides_degree: + assumes pq: "p dvd (q:: complex poly)" shows "degree p \ degree q \ q = 0" -by (metis dvd_imp_degree_le pq) + by (metis dvd_imp_degree_le pq) (* Arithmetic operations on multivariate polynomials. *) @@ -957,7 +973,8 @@ lemma mpoly_norm_conv: fixes x :: "'a::comm_ring_1" - shows "poly [:0:] x = poly 0 x" "poly [:poly 0 y:] x = poly 0 x" by simp_all + shows "poly [:0:] x = poly 0 x" "poly [:poly 0 y:] x = poly 0 x" + by simp_all lemma mpoly_sub_conv: fixes x :: "'a::comm_ring_1" @@ -982,78 +999,86 @@ qed lemma poly_divides_conv0: - fixes p:: "('a::field) poly" - assumes lgpq: "degree q < degree p" and lq:"p \ 0" - shows "p dvd q \ q = 0" (is "?lhs \ ?rhs") -proof- - {assume r: ?rhs - hence "q = p * 0" by simp - hence ?lhs ..} + fixes p:: "'a::field poly" + assumes lgpq: "degree q < degree p" + and lq: "p \ 0" + shows "p dvd q \ q = 0" (is "?lhs \ ?rhs") +proof + assume r: ?rhs + then have "q = p * 0" by simp + then show ?lhs .. +next + assume l: ?lhs + { + assume q0: "q = 0" + then have ?rhs by simp + } moreover - {assume l: ?lhs - {assume q0: "q = 0" - hence ?rhs by simp} - moreover - {assume q0: "q \ 0" - from l q0 have "degree p \ degree q" - by (rule dvd_imp_degree_le) - with lgpq have ?rhs by simp } - ultimately have ?rhs by blast } - ultimately show "?lhs \ ?rhs" by - (atomize (full), blast) + { + assume q0: "q \ 0" + from l q0 have "degree p \ degree q" + by (rule dvd_imp_degree_le) + with lgpq have ?rhs by simp + } + ultimately show ?rhs by blast qed lemma poly_divides_conv1: - fixes p:: "('a::field) poly" - assumes a0: "a\ 0" and pp': "p dvd p'" - and qrp': "smult a q - p' \ r" - shows "p dvd q \ p dvd r" (is "?lhs \ ?rhs") -proof- - { + fixes p :: "('a::field) poly" + assumes a0: "a \ 0" + and pp': "p dvd p'" + and qrp': "smult a q - p' = r" + shows "p dvd q \ p dvd r" (is "?lhs \ ?rhs") +proof from pp' obtain t where t: "p' = p * t" .. - {assume l: ?lhs + { + assume l: ?lhs then obtain u where u: "q = p * u" .. - have "r = p * (smult a u - t)" - using u qrp' [symmetric] t by (simp add: algebra_simps) - then have ?rhs ..} - moreover - {assume r: ?rhs + have "r = p * (smult a u - t)" + using u qrp' [symmetric] t by (simp add: algebra_simps) + then show ?rhs .. + next + assume r: ?rhs then obtain u where u: "r = p * u" .. from u [symmetric] t qrp' [symmetric] a0 have "q = p * smult (1/a) (u + t)" by (simp add: algebra_simps) - hence ?lhs ..} - ultimately have "?lhs = ?rhs" by blast } -thus "?lhs \ ?rhs" by - (atomize(full), blast) + then show ?lhs .. + } qed lemma basic_cqe_conv1: "(\x. poly p x = 0 \ poly 0 x \ 0) \ False" "(\x. poly 0 x \ 0) \ False" - "(\x. poly [:c:] x \ 0) \ c\0" + "(\x. poly [:c:] x \ 0) \ c \ 0" "(\x. poly 0 x = 0) \ True" - "(\x. poly [:c:] x = 0) \ c = 0" by simp_all + "(\x. poly [:c:] x = 0) \ c = 0" + by simp_all lemma basic_cqe_conv2: assumes l:"p \ 0" shows "(\x. poly (pCons a (pCons b p)) x = (0::complex))" -proof- - {fix h t - assume h: "h\0" "t=0" "pCons a (pCons b p) = pCons h t" - with l have False by simp} - hence th: "\ (\ h t. h\0 \ t=0 \ pCons a (pCons b p) = pCons h t)" +proof - + { + fix h t + assume h: "h \ 0" "t = 0" and "pCons a (pCons b p) = pCons h t" + with l have False by simp + } + then have th: "\ (\ h t. h \ 0 \ t = 0 \ pCons a (pCons b p) = pCons h t)" by blast - from fundamental_theorem_of_algebra_alt[OF th] - show ?thesis by auto + from fundamental_theorem_of_algebra_alt[OF th] show ?thesis + by auto qed -lemma basic_cqe_conv_2b: "(\x. poly p x \ (0::complex)) \ (p \ 0)" -by (metis poly_all_0_iff_0) +lemma basic_cqe_conv_2b: "(\x. poly p x \ (0::complex)) \ p \ 0" + by (metis poly_all_0_iff_0) lemma basic_cqe_conv3: fixes p q :: "complex poly" assumes l: "p \ 0" - shows "(\x. poly (pCons a p) x = 0 \ poly q x \ 0) \ \ ((pCons a p) dvd (q ^ (psize p)))" + shows "(\x. poly (pCons a p) x = 0 \ poly q x \ 0) \ \ ((pCons a p) dvd (q ^ psize p))" proof - - from l have dp:"degree (pCons a p) = psize p" by (simp add: psize_def) + from l have dp: "degree (pCons a p) = psize p" + by (simp add: psize_def) from nullstellensatz_univariate[of "pCons a p" q] l show ?thesis by (metis dp pCons_eq_0_iff) @@ -1063,14 +1088,18 @@ fixes p q :: "complex poly" assumes h: "\x. poly (q ^ n) x = poly r x" shows "p dvd (q ^ n) \ p dvd r" -proof- - from h have "poly (q ^ n) = poly r" by auto - then have "(q ^ n) = r" by (simp add: poly_eq_poly_eq_iff) - thus "p dvd (q ^ n) \ p dvd r" by simp +proof - + from h have "poly (q ^ n) = poly r" + by auto + then have "(q ^ n) = r" + by (simp add: poly_eq_poly_eq_iff) + then show "p dvd (q ^ n) \ p dvd r" + by simp qed lemma poly_const_conv: fixes x :: "'a::comm_ring_1" - shows "poly [:c:] x = y \ c = y" by simp + shows "poly [:c:] x = y \ c = y" + by simp end