src/HOL/Library/Fundamental_Theorem_Algebra.thy
 changeset 60457 f31f7599ef55 parent 60449 229bad93377e child 60557 5854821993d2
1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jun 13 19:38:26 2015 +0200
1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jun 13 19:53:53 2015 +0200
1.3 @@ -159,8 +159,9 @@
1.4    assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)"
1.5    assume n: "n \<noteq> 0"
1.6    let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1"
1.7 -  {
1.8 -    assume e: "even n"
1.9 +  show "\<exists>z. ?P z n"
1.10 +  proof cases
1.11 +    assume "even n"
1.12      then have "\<exists>m. n = 2 * m"
1.13        by presburger
1.14      then obtain m where m: "n = 2 * m"
1.15 @@ -170,19 +171,17 @@
1.16      with IH[rule_format, of m] obtain z where z: "?P z m"
1.17        by blast
1.18      from z have "?P (csqrt z) n"
1.19 -      by (simp add: m power_mult power2_csqrt)
1.20 -    then have "\<exists>z. ?P z n" ..
1.21 -  }
1.22 -  moreover
1.23 -  {
1.24 -    assume o: "odd n"
1.25 -    have th0: "cmod (complex_of_real (cmod b) / b) = 1"
1.26 -      using b by (simp add: norm_divide)
1.27 -    from o have "\<exists>m. n = Suc (2 * m)"
1.28 +      by (simp add: m power_mult)
1.29 +    then show ?thesis ..
1.30 +  next
1.31 +    assume "odd n"
1.32 +    then have "\<exists>m. n = Suc (2 * m)"
1.33        by presburger+
1.34      then obtain m where m: "n = Suc (2 * m)"
1.35        by blast
1.36 -    from unimodular_reduce_norm[OF th0] o
1.37 +    have th0: "cmod (complex_of_real (cmod b) / b) = 1"
1.38 +      using b by (simp add: norm_divide)
1.39 +    from unimodular_reduce_norm[OF th0] \<open>odd n\<close>
1.40      have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
1.41        apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1")
1.42        apply (rule_tac x="1" in exI)
1.43 @@ -206,7 +205,7 @@
1.44      then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1"
1.45        by blast
1.46      let ?w = "v / complex_of_real (root n (cmod b))"
1.47 -    from odd_real_root_pow[OF o, of "cmod b"]
1.48 +    from odd_real_root_pow[OF \<open>odd n\<close>, of "cmod b"]
1.49      have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
1.50        by (simp add: power_divide of_real_power[symmetric])
1.51      have th2:"cmod (complex_of_real (cmod b) / b) = 1"
1.52 @@ -222,9 +221,8 @@
1.53        done
1.54      from mult_left_less_imp_less[OF th4 th3]
1.55      have "?P ?w n" unfolding th1 .
1.56 -    then have "\<exists>z. ?P z n" ..
1.57 -  }
1.58 -  ultimately show "\<exists>z. ?P z n" by blast
1.59 +    then show ?thesis ..
1.60 +  qed
1.61  qed
1.63  text \<open>Bolzano-Weierstrass type property for closed disc in complex plane.\<close>
1.64 @@ -1020,51 +1018,44 @@
1.65    "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
1.66      p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
1.67  proof -
1.68 -  show ?thesis
1.69 -  proof (cases "p = 0")
1.70 -    case True
1.71 +  consider "p = 0" | "p \<noteq> 0" "degree p = 0" | n where "p \<noteq> 0" "degree p = Suc n"
1.72 +    by (cases "degree p") auto
1.73 +  then show ?thesis
1.74 +  proof cases
1.75 +    case 1
1.76      then have eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
1.77        by (auto simp add: poly_all_0_iff_0)
1.78      {
1.79        assume "p dvd (q ^ (degree p))"
1.80        then obtain r where r: "q ^ (degree p) = p * r" ..
1.81 -      from r True have False by simp
1.82 +      from r 1 have False by simp
1.83      }
1.84 -    with eq True show ?thesis by blast
1.85 +    with eq 1 show ?thesis by blast
1.86    next
1.87 -    case False
1.88 -    show ?thesis
1.89 -    proof (cases "degree p = 0")
1.90 -      case True
1.91 -      with \<open>p \<noteq> 0\<close> obtain k where k: "p = [:k:]" "k \<noteq> 0"
1.92 -        by (cases p) (simp split: if_splits)
1.93 -      then have th1: "\<forall>x. poly p x \<noteq> 0"
1.94 +    case 2
1.95 +    then obtain k where k: "p = [:k:]" "k \<noteq> 0"
1.96 +      by (cases p) (simp split: if_splits)
1.97 +    then have th1: "\<forall>x. poly p x \<noteq> 0"
1.98 +      by simp
1.99 +    from k 2(2) have "q ^ (degree p) = p * [:1/k:]"
1.100 +      by (simp add: one_poly_def)
1.101 +    then have th2: "p dvd (q ^ (degree p))" ..
1.102 +    from 2(1) th1 th2 show ?thesis
1.103 +      by blast
1.104 +  next
1.105 +    case 3
1.106 +    {
1.107 +      assume "p dvd (q ^ (Suc n))"
1.108 +      then obtain u where u: "q ^ (Suc n) = p * u" ..
1.109 +      fix x
1.110 +      assume h: "poly p x = 0" "poly q x \<noteq> 0"
1.111 +      then have "poly (q ^ (Suc n)) x \<noteq> 0"
1.112          by simp
1.113 -      from k True have "q ^ (degree p) = p * [:1/k:]"
1.114 -        by (simp add: one_poly_def)
1.115 -      then have th2: "p dvd (q ^ (degree p))" ..
1.116 -      from False th1 th2 show ?thesis
1.117 -        by blast
1.118 -    next
1.119 -      case False
1.120 -      assume dp: "degree p \<noteq> 0"
1.121 -      then obtain n where n: "degree p = Suc n "
1.122 -        by (cases "degree p") auto
1.123 -      {
1.124 -        assume "p dvd (q ^ (Suc n))"
1.125 -        then obtain u where u: "q ^ (Suc n) = p * u" ..
1.126 -        {
1.127 -          fix x
1.128 -          assume h: "poly p x = 0" "poly q x \<noteq> 0"
1.129 -          then have "poly (q ^ (Suc n)) x \<noteq> 0"
1.130 -            by simp
1.131 -          then have False using u h(1)
1.132 -            by (simp only: poly_mult) simp
1.133 -        }
1.134 -      }
1.135 -      with n nullstellensatz_lemma[of p q "degree p"] dp
1.136 -      show ?thesis by auto
1.137 -    qed
1.138 +      then have False using u h(1)
1.139 +        by (simp only: poly_mult) simp
1.140 +    }
1.141 +    with 3 nullstellensatz_lemma[of p q "degree p"]
1.142 +    show ?thesis by auto
1.143    qed
1.144  qed