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)"
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"
{
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:]"
+    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:]"
-      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
```