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.62  
    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
   1.145