summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 13 Jun 2015 19:53:53 +0200 | |

changeset 60457 | f31f7599ef55 |

parent 60456 | 323b15b5af73 |

child 60458 | 0d10ae17e3ee |

tuned proofs;

--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sat Jun 13 19:38:26 2015 +0200 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sat Jun 13 19:53:53 2015 +0200 @@ -159,8 +159,9 @@ assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)" assume n: "n \<noteq> 0" let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1" - { - assume e: "even n" + show "\<exists>z. ?P z n" + proof cases + assume "even n" then have "\<exists>m. n = 2 * m" by presburger then obtain m where m: "n = 2 * m" @@ -170,19 +171,17 @@ with IH[rule_format, of m] obtain z where z: "?P z m" by blast from z have "?P (csqrt z) n" - by (simp add: m power_mult power2_csqrt) - then have "\<exists>z. ?P z n" .. - } - moreover - { - assume o: "odd n" - have th0: "cmod (complex_of_real (cmod b) / b) = 1" - using b by (simp add: norm_divide) - from o have "\<exists>m. n = Suc (2 * m)" + by (simp add: m power_mult) + then show ?thesis .. + next + assume "odd n" + then have "\<exists>m. n = Suc (2 * m)" by presburger+ then obtain m where m: "n = Suc (2 * m)" by blast - from unimodular_reduce_norm[OF th0] o + have th0: "cmod (complex_of_real (cmod b) / b) = 1" + using b by (simp add: norm_divide) + from unimodular_reduce_norm[OF th0] \<open>odd n\<close> have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1" apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1") apply (rule_tac x="1" in exI) @@ -206,7 +205,7 @@ then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast let ?w = "v / complex_of_real (root n (cmod b))" - from odd_real_root_pow[OF o, of "cmod b"] + from odd_real_root_pow[OF \<open>odd n\<close>, of "cmod b"] have th1: "?w ^ n = v^n / complex_of_real (cmod b)" by (simp add: power_divide of_real_power[symmetric]) have th2:"cmod (complex_of_real (cmod b) / b) = 1" @@ -222,9 +221,8 @@ done from mult_left_less_imp_less[OF th4 th3] have "?P ?w n" unfolding th1 . - then have "\<exists>z. ?P z n" .. - } - ultimately show "\<exists>z. ?P z n" by blast + then show ?thesis .. + qed qed text \<open>Bolzano-Weierstrass type property for closed disc in complex plane.\<close> @@ -1020,51 +1018,44 @@ "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)" proof - - show ?thesis - proof (cases "p = 0") - case True + consider "p = 0" | "p \<noteq> 0" "degree p = 0" | n where "p \<noteq> 0" "degree p = Suc n" + by (cases "degree p") auto + then show ?thesis + proof cases + case 1 then have eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0" by (auto simp add: poly_all_0_iff_0) { assume "p dvd (q ^ (degree p))" then obtain r where r: "q ^ (degree p) = p * r" .. - from r True have False by simp + from r 1 have False by simp } - with eq True show ?thesis by blast + with eq 1 show ?thesis by blast next - case False - show ?thesis - proof (cases "degree p = 0") - case True - with \<open>p \<noteq> 0\<close> obtain k where k: "p = [:k:]" "k \<noteq> 0" - by (cases p) (simp split: if_splits) - then have th1: "\<forall>x. poly p x \<noteq> 0" + case 2 + then obtain k where k: "p = [:k:]" "k \<noteq> 0" + by (cases p) (simp split: if_splits) + then have th1: "\<forall>x. poly p x \<noteq> 0" + by simp + from k 2(2) have "q ^ (degree p) = p * [:1/k:]" + by (simp add: one_poly_def) + then have th2: "p dvd (q ^ (degree p))" .. + from 2(1) th1 th2 show ?thesis + by blast + next + case 3 + { + assume "p dvd (q ^ (Suc n))" + then obtain u where u: "q ^ (Suc n) = p * u" .. + fix x + assume h: "poly p x = 0" "poly q x \<noteq> 0" + then have "poly (q ^ (Suc n)) x \<noteq> 0" by simp - from k True have "q ^ (degree p) = p * [:1/k:]" - by (simp add: one_poly_def) - then have th2: "p dvd (q ^ (degree p))" .. - from False th1 th2 show ?thesis - by blast - next - case False - assume dp: "degree p \<noteq> 0" - then obtain n where n: "degree p = Suc n " - by (cases "degree p") auto - { - assume "p dvd (q ^ (Suc n))" - then obtain u where u: "q ^ (Suc n) = p * u" .. - { - fix x - assume h: "poly p x = 0" "poly q x \<noteq> 0" - then have "poly (q ^ (Suc n)) x \<noteq> 0" - by simp - then have False using u h(1) - by (simp only: poly_mult) simp - } - } - with n nullstellensatz_lemma[of p q "degree p"] dp - show ?thesis by auto - qed + then have False using u h(1) + by (simp only: poly_mult) simp + } + with 3 nullstellensatz_lemma[of p q "degree p"] + show ?thesis by auto qed qed