src/HOL/Library/Fundamental_Theorem_Algebra.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63589 58aab4745e85
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29197
6d4cb27ed19c adapted HOL source structure to distribution layout
haftmann
parents: 28952
diff changeset
     1
(* Author: Amine Chaieb, TU Muenchen *)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
     2
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
     3
section \<open>Fundamental Theorem of Algebra\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
     4
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
     5
theory Fundamental_Theorem_Algebra
51537
abcd6d5f7508 more standard imports;
wenzelm
parents: 50636
diff changeset
     6
imports Polynomial Complex_Main
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
     7
begin
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
     8
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
     9
subsection \<open>More lemmas about module of complex numbers\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    10
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
    11
text \<open>The triangle inequality for cmod\<close>
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
    12
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    13
lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    14
  using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    15
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
    16
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
    17
subsection \<open>Basic lemmas about polynomials\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    18
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    19
lemma poly_bound_exists:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    20
  fixes p :: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    21
  shows "\<exists>m. m > 0 \<and> (\<forall>z. norm z \<le> r \<longrightarrow> norm (poly p z) \<le> m)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    22
proof (induct p)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    23
  case 0
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    24
  then show ?case by (rule exI[where x=1]) simp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    25
next
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    26
  case (pCons c cs)
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
    27
  from pCons.hyps obtain m where m: "\<forall>z. norm z \<le> r \<longrightarrow> norm (poly cs z) \<le> m"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    28
    by blast
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
    29
  let ?k = " 1 + norm c + \<bar>r * m\<bar>"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
    30
  have kp: "?k > 0"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
    31
    using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
    32
  have "norm (poly (pCons c cs) z) \<le> ?k" if H: "norm z \<le> r" for z
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
    33
  proof -
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    34
    from m H have th: "norm (poly cs z) \<le> m"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    35
      by blast
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
    36
    from H have rp: "r \<ge> 0"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
    37
      using norm_ge_zero[of z] by arith
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
    38
    have "norm (poly (pCons c cs) z) \<le> norm c + norm (z * poly cs z)"
27514
6fcf6864d703 remove redundant lemmas about cmod
huffman
parents: 27445
diff changeset
    39
      using norm_triangle_ineq[of c "z* poly cs z"] by simp
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    40
    also have "\<dots> \<le> norm c + r * m"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    41
      using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]]
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
    42
      by (simp add: norm_mult)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    43
    also have "\<dots> \<le> ?k"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    44
      by simp
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
    45
    finally show ?thesis .
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
    46
  qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    47
  with kp show ?case by blast
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    48
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    49
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    50
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
    51
text \<open>Offsetting the variable in a polynomial gives another of same degree\<close>
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    52
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 51541
diff changeset
    53
definition offset_poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    54
  where "offset_poly p h = fold_coeffs (\<lambda>a q. smult h q + pCons a q) p 0"
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    55
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    56
lemma offset_poly_0: "offset_poly 0 h = 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 51541
diff changeset
    57
  by (simp add: offset_poly_def)
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    58
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    59
lemma offset_poly_pCons:
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    60
  "offset_poly (pCons a p) h =
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    61
    smult h (offset_poly p h) + pCons a (offset_poly p h)"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 51541
diff changeset
    62
  by (cases "p = 0 \<and> a = 0") (auto simp add: offset_poly_def)
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    63
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    64
lemma offset_poly_single: "offset_poly [:a:] h = [:a:]"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    65
  by (simp add: offset_poly_pCons offset_poly_0)
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    66
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    67
lemma poly_offset_poly: "poly (offset_poly p h) x = poly p (h + x)"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    68
  apply (induct p)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    69
  apply (simp add: offset_poly_0)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    70
  apply (simp add: offset_poly_pCons algebra_simps)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    71
  done
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    72
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    73
lemma offset_poly_eq_0_lemma: "smult c p + pCons a p = 0 \<Longrightarrow> p = 0"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    74
  by (induct p arbitrary: a) (simp, force)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
    75
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    76
lemma offset_poly_eq_0_iff: "offset_poly p h = 0 \<longleftrightarrow> p = 0"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    77
  apply (safe intro!: offset_poly_0)
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
    78
  apply (induct p)
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
    79
  apply simp
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    80
  apply (simp add: offset_poly_pCons)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    81
  apply (frule offset_poly_eq_0_lemma, simp)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    82
  done
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    83
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    84
lemma degree_offset_poly: "degree (offset_poly p h) = degree p"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    85
  apply (induct p)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    86
  apply (simp add: offset_poly_0)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    87
  apply (case_tac "p = 0")
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    88
  apply (simp add: offset_poly_0 offset_poly_pCons)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    89
  apply (simp add: offset_poly_pCons)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    90
  apply (subst degree_add_eq_right)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    91
  apply (rule le_less_trans [OF degree_smult_le])
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    92
  apply (simp add: offset_poly_eq_0_iff)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    93
  apply (simp add: offset_poly_eq_0_iff)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    94
  done
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    95
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
    96
definition "psize p = (if p = 0 then 0 else Suc (degree p))"
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
    97
29538
5cc98af1398d rename plength to psize
huffman
parents: 29485
diff changeset
    98
lemma psize_eq_0_iff [simp]: "psize p = 0 \<longleftrightarrow> p = 0"
5cc98af1398d rename plength to psize
huffman
parents: 29485
diff changeset
    99
  unfolding psize_def by simp
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   100
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   101
lemma poly_offset:
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   102
  fixes p :: "'a::comm_ring_1 poly"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   103
  shows "\<exists>q. psize q = psize p \<and> (\<forall>x. poly q x = poly p (a + x))"
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   104
proof (intro exI conjI)
29538
5cc98af1398d rename plength to psize
huffman
parents: 29485
diff changeset
   105
  show "psize (offset_poly p a) = psize p"
5cc98af1398d rename plength to psize
huffman
parents: 29485
diff changeset
   106
    unfolding psize_def
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   107
    by (simp add: offset_poly_eq_0_iff degree_offset_poly)
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   108
  show "\<forall>x. poly (offset_poly p a) x = poly p (a + x)"
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   109
    by (simp add: poly_offset_poly)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   110
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   111
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   112
text \<open>An alternative useful formulation of completeness of the reals\<close>
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   113
lemma real_sup_exists:
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   114
  assumes ex: "\<exists>x. P x"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   115
    and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   116
  shows "\<exists>s::real. \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
54263
c4159fe6fa46 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents: 54230
diff changeset
   117
proof
c4159fe6fa46 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents: 54230
diff changeset
   118
  from bz have "bdd_above (Collect P)"
c4159fe6fa46 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents: 54230
diff changeset
   119
    by (force intro: less_imp_le)
c4159fe6fa46 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents: 54230
diff changeset
   120
  then show "\<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < Sup (Collect P)"
c4159fe6fa46 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents: 54230
diff changeset
   121
    using ex bz by (subst less_cSup_iff) auto
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   122
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   123
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   124
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   125
subsection \<open>Fundamental theorem of algebra\<close>
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   126
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   127
lemma unimodular_reduce_norm:
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   128
  assumes md: "cmod z = 1"
63589
58aab4745e85 more symbols;
wenzelm
parents: 63060
diff changeset
   129
  shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + \<i>) < 1 \<or> cmod (z - \<i>) < 1"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   130
proof -
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   131
  obtain x y where z: "z = Complex x y "
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   132
    by (cases z) auto
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   133
  from md z have xy: "x\<^sup>2 + y\<^sup>2 = 1"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   134
    by (simp add: cmod_def)
63589
58aab4745e85 more symbols;
wenzelm
parents: 63060
diff changeset
   135
  have False if "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + \<i>) \<ge> 1" "cmod (z - \<i>) \<ge> 1"
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   136
  proof -
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   137
    from that z xy have "2 * x \<le> 1" "2 * x \<ge> -1" "2 * y \<le> 1" "2 * y \<ge> -1"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29538
diff changeset
   138
      by (simp_all add: cmod_def power2_eq_square algebra_simps)
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61585
diff changeset
   139
    then have "\<bar>2 * x\<bar> \<le> 1" "\<bar>2 * y\<bar> \<le> 1"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   140
      by simp_all
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61585
diff changeset
   141
    then have "\<bar>2 * x\<bar>\<^sup>2 \<le> 1\<^sup>2" "\<bar>2 * y\<bar>\<^sup>2 \<le> 1\<^sup>2"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   142
      by - (rule power_mono, simp, simp)+
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   143
    then have th0: "4 * x\<^sup>2 \<le> 1" "4 * y\<^sup>2 \<le> 1"
51541
e7b6b61b7be2 tuned proofs;
wenzelm
parents: 51537
diff changeset
   144
      by (simp_all add: power_mult_distrib)
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   145
    from add_mono[OF th0] xy show ?thesis
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   146
      by simp
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   147
  qed
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   148
  then show ?thesis
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   149
    unfolding linorder_not_le[symmetric] by blast
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   150
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   151
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 60567
diff changeset
   152
text \<open>Hence we can always reduce modulus of \<open>1 + b z^n\<close> if nonzero\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   153
lemma reduce_poly_simple:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   154
  assumes b: "b \<noteq> 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   155
    and n: "n \<noteq> 0"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   156
  shows "\<exists>z. cmod (1 + b * z^n) < 1"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   157
  using n
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   158
proof (induct n rule: nat_less_induct)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   159
  fix n
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   160
  assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   161
  assume n: "n \<noteq> 0"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   162
  let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1"
60457
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   163
  show "\<exists>z. ?P z n"
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   164
  proof cases
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   165
    assume "even n"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   166
    then have "\<exists>m. n = 2 * m"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   167
      by presburger
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   168
    then obtain m where m: "n = 2 * m"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   169
      by blast
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   170
    from n m have "m \<noteq> 0" "m < n"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   171
      by presburger+
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   172
    with IH[rule_format, of m] obtain z where z: "?P z m"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   173
      by blast
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   174
    from z have "?P (csqrt z) n"
60457
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   175
      by (simp add: m power_mult)
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   176
    then show ?thesis ..
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   177
  next
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   178
    assume "odd n"
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   179
    then have "\<exists>m. n = Suc (2 * m)"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   180
      by presburger+
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   181
    then obtain m where m: "n = Suc (2 * m)"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   182
      by blast
60457
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   183
    have th0: "cmod (complex_of_real (cmod b) / b) = 1"
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   184
      using b by (simp add: norm_divide)
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   185
    from unimodular_reduce_norm[OF th0] \<open>odd n\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   186
    have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   187
      apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1")
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   188
      apply (rule_tac x="1" in exI)
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   189
      apply simp
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   190
      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1")
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   191
      apply (rule_tac x="-1" in exI)
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   192
      apply simp
63589
58aab4745e85 more symbols;
wenzelm
parents: 63060
diff changeset
   193
      apply (cases "cmod (complex_of_real (cmod b) / b + \<i>) < 1")
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   194
      apply (cases "even m")
63589
58aab4745e85 more symbols;
wenzelm
parents: 63060
diff changeset
   195
      apply (rule_tac x="\<i>" in exI)
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   196
      apply (simp add: m power_mult)
63589
58aab4745e85 more symbols;
wenzelm
parents: 63060
diff changeset
   197
      apply (rule_tac x="- \<i>" in exI)
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   198
      apply (simp add: m power_mult)
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   199
      apply (cases "even m")
63589
58aab4745e85 more symbols;
wenzelm
parents: 63060
diff changeset
   200
      apply (rule_tac x="- \<i>" in exI)
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   201
      apply (simp add: m power_mult)
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54263
diff changeset
   202
      apply (auto simp add: m power_mult)
63589
58aab4745e85 more symbols;
wenzelm
parents: 63060
diff changeset
   203
      apply (rule_tac x="\<i>" in exI)
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54263
diff changeset
   204
      apply (auto simp add: m power_mult)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   205
      done
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   206
    then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   207
      by blast
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   208
    let ?w = "v / complex_of_real (root n (cmod b))"
60457
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   209
    from odd_real_root_pow[OF \<open>odd n\<close>, of "cmod b"]
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   210
    have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56795
diff changeset
   211
      by (simp add: power_divide of_real_power[symmetric])
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   212
    have th2:"cmod (complex_of_real (cmod b) / b) = 1"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   213
      using b by (simp add: norm_divide)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   214
    then have th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   215
      by simp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   216
    have th4: "cmod (complex_of_real (cmod b) / b) *
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   217
        cmod (1 + b * (v ^ n / complex_of_real (cmod b))) <
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   218
        cmod (complex_of_real (cmod b) / b) * 1"
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 46240
diff changeset
   219
      apply (simp only: norm_mult[symmetric] distrib_left)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   220
      using b v
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   221
      apply (simp add: th2)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   222
      done
59555
05573e5504a9 eliminated fact duplicates
haftmann
parents: 58881
diff changeset
   223
    from mult_left_less_imp_less[OF th4 th3]
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   224
    have "?P ?w n" unfolding th1 .
60457
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   225
    then show ?thesis ..
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
   226
  qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   227
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   228
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   229
text \<open>Bolzano-Weierstrass type property for closed disc in complex plane.\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   230
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   231
lemma metric_bound_lemma: "cmod (x - y) \<le> \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   232
  using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y"]
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   233
  unfolding cmod_def by simp
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   234
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   235
lemma bolzano_weierstrass_complex_disc:
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   236
  assumes r: "\<forall>n. cmod (s n) \<le> r"
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   237
  shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   238
proof -
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   239
  from seq_monosub[of "Re \<circ> s"]
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   240
  obtain f where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   241
    unfolding o_def by blast
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   242
  from seq_monosub[of "Im \<circ> s \<circ> f"]
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   243
  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s (f (g n))))"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   244
    unfolding o_def by blast
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   245
  let ?h = "f \<circ> g"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   246
  from r[rule_format, of 0] have rp: "r \<ge> 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   247
    using norm_ge_zero[of "s 0"] by arith
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   248
  have th: "\<forall>n. r + 1 \<ge> \<bar>Re (s n)\<bar>"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   249
  proof
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   250
    fix n
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   251
    from abs_Re_le_cmod[of "s n"] r[rule_format, of n]
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   252
    show "\<bar>Re (s n)\<bar> \<le> r + 1" by arith
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   253
  qed
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   254
  have conv1: "convergent (\<lambda>n. Re (s (f n)))"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   255
    apply (rule Bseq_monoseq_convergent)
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   256
    apply (simp add: Bseq_def)
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   257
    apply (metis gt_ex le_less_linear less_trans order.trans th)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   258
    apply (rule f(2))
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   259
    done
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   260
  have th: "\<forall>n. r + 1 \<ge> \<bar>Im (s n)\<bar>"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   261
  proof
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   262
    fix n
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   263
    from abs_Im_le_cmod[of "s n"] r[rule_format, of n]
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   264
    show "\<bar>Im (s n)\<bar> \<le> r + 1"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   265
      by arith
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   266
  qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   267
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   268
  have conv2: "convergent (\<lambda>n. Im (s (f (g n))))"
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   269
    apply (rule Bseq_monoseq_convergent)
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   270
    apply (simp add: Bseq_def)
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   271
    apply (metis gt_ex le_less_linear less_trans order.trans th)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   272
    apply (rule g(2))
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   273
    done
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   274
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   275
  from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   276
    by blast
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   277
  then have x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar>Re (s (f n)) - x\<bar> < r"
31337
a9ed5fcc5e39 LIMSEQ_def -> LIMSEQ_iff
huffman
parents: 31021
diff changeset
   278
    unfolding LIMSEQ_iff real_norm_def .
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   279
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   280
  from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   281
    by blast
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   282
  then have y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar>Im (s (f (g n))) - y\<bar> < r"
31337
a9ed5fcc5e39 LIMSEQ_def -> LIMSEQ_iff
huffman
parents: 31021
diff changeset
   283
    unfolding LIMSEQ_iff real_norm_def .
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   284
  let ?w = "Complex x y"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   285
  from f(1) g(1) have hs: "subseq ?h"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   286
    unfolding subseq_def by auto
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   287
  have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" if "e > 0" for e
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   288
  proof -
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   289
    from that have e2: "e/2 > 0"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   290
      by simp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   291
    from x[rule_format, OF e2] y[rule_format, OF e2]
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   292
    obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   293
      and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   294
      by blast
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   295
    have "cmod (s (?h n) - ?w) < e" if "n \<ge> N1 + N2" for n
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   296
    proof -
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   297
      from that have nN1: "g n \<ge> N1" and nN2: "n \<ge> N2"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   298
        using seq_suble[OF g(1), of n] by arith+
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   299
      from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   300
      show ?thesis
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   301
        using metric_bound_lemma[of "s (f (g n))" ?w] by simp
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   302
    qed
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   303
    then show ?thesis by blast
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   304
  qed
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   305
  with hs show ?thesis by blast
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   306
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   307
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   308
text \<open>Polynomial is continuous.\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   309
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   310
lemma poly_cont:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   311
  fixes p :: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   312
  assumes ep: "e > 0"
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
   313
  shows "\<exists>d >0. \<forall>w. 0 < norm (w - z) \<and> norm (w - z) < d \<longrightarrow> norm (poly p w - poly p z) < e"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   314
proof -
63060
293ede07b775 some uses of 'obtain' with structure statement;
wenzelm
parents: 62128
diff changeset
   315
  obtain q where q: "degree q = degree p" "poly q x = poly p (z + x)" for x
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   316
  proof
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   317
    show "degree (offset_poly p z) = degree p"
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   318
      by (rule degree_offset_poly)
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   319
    show "\<And>x. poly (offset_poly p z) x = poly p (z + x)"
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   320
      by (rule poly_offset_poly)
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   321
  qed
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   322
  have th: "\<And>w. poly q (w - z) = poly p w"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   323
    using q(2)[of "w - z" for w] by simp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   324
  show ?thesis unfolding th[symmetric]
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   325
  proof (induct q)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   326
    case 0
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   327
    then show ?case
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   328
      using ep by auto
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   329
  next
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   330
    case (pCons c cs)
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   331
    from poly_bound_exists[of 1 "cs"]
63060
293ede07b775 some uses of 'obtain' with structure statement;
wenzelm
parents: 62128
diff changeset
   332
    obtain m where m: "m > 0" "norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m" for z
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   333
      by blast
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   334
    from ep m(1) have em0: "e/m > 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   335
      by (simp add: field_simps)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   336
    have one0: "1 > (0::real)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   337
      by arith
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   338
    from real_lbound_gt_zero[OF one0 em0]
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   339
    obtain d where d: "d > 0" "d < 1" "d < e / m"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   340
      by blast
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   341
    from d(1,3) m(1) have dm: "d * m > 0" "d * m < e"
56544
b60d5d119489 made mult_pos_pos a simp rule
nipkow
parents: 56403
diff changeset
   342
      by (simp_all add: field_simps)
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   343
    show ?case
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   344
    proof (rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   345
      fix d w
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   346
      assume H: "d > 0" "d < 1" "d < e/m" "w \<noteq> z" "norm (w - z) < d"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   347
      then have d1: "norm (w-z) \<le> 1" "d \<ge> 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   348
        by simp_all
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   349
      from H(3) m(1) have dme: "d*m < e"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   350
        by (simp add: field_simps)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   351
      from H have th: "norm (w - z) \<le> d"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   352
        by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   353
      from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   354
      show "norm (w - z) * norm (poly cs (w - z)) < e"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   355
        by simp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   356
    qed
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   357
  qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   358
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   359
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   360
text \<open>Hence a polynomial attains minimum on a closed disc
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   361
  in the complex plane.\<close>
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   362
lemma poly_minimum_modulus_disc: "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   363
proof -
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   364
  show ?thesis
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   365
  proof (cases "r \<ge> 0")
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   366
    case False
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   367
    then show ?thesis
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   368
      by (metis norm_ge_zero order.trans)
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   369
  next
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   370
    case True
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   371
    then have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   372
      by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   373
    then have mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   374
      by blast
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   375
    have False if "cmod z \<le> r" "cmod (poly p z) = - x" "\<not> x < 1" for x z
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   376
    proof -
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   377
      from that have "- x < 0 "
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   378
        by arith
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   379
      with that(2) norm_ge_zero[of "poly p z"] show ?thesis
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   380
        by simp
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   381
    qed
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   382
    then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   383
      by blast
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   384
    from real_sup_exists[OF mth1 mth2] obtain s where
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   385
      s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow> y < s"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   386
      by blast
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   387
    let ?m = "- s"
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   388
    have s1[unfolded minus_minus]:
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   389
      "(\<exists>z x. cmod z \<le> r \<and> - (- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y" for y
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   390
      using s[rule_format, of "-y"]
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   391
      unfolding minus_less_iff[of y] equation_minus_iff by blast
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   392
    from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   393
      by auto
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   394
    have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" for n
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   395
      using s1[rule_format, of "?m + 1/real (Suc n)"] by simp
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   396
    then have th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   397
    from choice[OF th] obtain g where
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   398
        g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m + 1 /real(Suc n)"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   399
      by blast
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   400
    from bolzano_weierstrass_complex_disc[OF g(1)]
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   401
    obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   402
      by blast
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   403
    {
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   404
      fix w
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   405
      assume wr: "cmod w \<le> r"
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   406
      let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   407
      {
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   408
        assume e: "?e > 0"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   409
        then have e2: "?e/2 > 0"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   410
          by simp
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   411
        from poly_cont[OF e2, of z p] obtain d where
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   412
            d: "d > 0" "\<forall>w. 0<cmod (w - z)\<and> cmod(w - z) < d \<longrightarrow> cmod(poly p w - poly p z) < ?e/2"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   413
          by blast
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   414
        have th1: "cmod(poly p w - poly p z) < ?e / 2" if w: "cmod (w - z) < d" for w
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   415
          using d(2)[rule_format, of w] w e by (cases "w = z") simp_all
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   416
        from fz(2) d(1) obtain N1 where N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   417
          by blast
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   418
        from reals_Archimedean2[of "2/?e"] obtain N2 :: nat where N2: "2/?e < real N2"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   419
          by blast
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   420
        have th2: "cmod (poly p (g (f (N1 + N2))) - poly p z) < ?e/2"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   421
          using N1[rule_format, of "N1 + N2"] th1 by simp
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   422
        have th0: "a < e2 \<Longrightarrow> \<bar>b - m\<bar> < e2 \<Longrightarrow> 2 * e2 \<le> \<bar>b - m\<bar> + a \<Longrightarrow> False"
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   423
          for a b e2 m :: real
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   424
          by arith
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   425
        have ath: "m \<le> x \<Longrightarrow> x < m + e \<Longrightarrow> \<bar>x - m\<bar> < e" for m x e :: real
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   426
          by arith
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   427
        from s1m[OF g(1)[rule_format]] have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   428
        from seq_suble[OF fz(1), of "N1 + N2"]
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   429
        have th00: "real (Suc (N1 + N2)) \<le> real (Suc (f (N1 + N2)))"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   430
          by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   431
        have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1 + N2)) > 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   432
          using N2 by auto
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   433
        from frac_le[OF th000 th00]
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   434
        have th00: "?m + 1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   435
          by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   436
        from g(2)[rule_format, of "f (N1 + N2)"]
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   437
        have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   438
        from order_less_le_trans[OF th01 th00]
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   439
        have th32: "cmod (poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   440
        from N2 have "2/?e < real (Suc (N1 + N2))"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   441
          by arith
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   442
        with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   443
        have "?e/2 > 1/ real (Suc (N1 + N2))"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   444
          by (simp add: inverse_eq_divide)
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   445
        with ath[OF th31 th32] have thc1: "\<bar>cmod (poly p (g (f (N1 + N2)))) - ?m\<bar> < ?e/2"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   446
          by arith
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   447
        have ath2: "\<bar>a - b\<bar> \<le> c \<Longrightarrow> \<bar>b - m\<bar> \<le> \<bar>a - m\<bar> + c" for a b c m :: real
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   448
          by arith
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   449
        have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar> \<le>
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   450
            cmod (poly p (g (f (N1 + N2))) - poly p z)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   451
          by (simp add: norm_triangle_ineq3)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   452
        from ath2[OF th22, of ?m]
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   453
        have thc2: "2 * (?e/2) \<le>
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   454
            \<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar> + cmod (poly p (g (f (N1 + N2))) - poly p z)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   455
          by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   456
        from th0[OF th2 thc1 thc2] have False .
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   457
      }
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   458
      then have "?e = 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   459
        by auto
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   460
      then have "cmod (poly p z) = ?m"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   461
        by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   462
      with s1m[OF wr] have "cmod (poly p z) \<le> cmod (poly p w)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   463
        by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   464
    }
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   465
    then show ?thesis by blast
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   466
  qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   467
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   468
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   469
text \<open>Nonzero polynomial in z goes to infinity as z does.\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   470
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   471
lemma poly_infinity:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   472
  fixes p:: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   473
  assumes ex: "p \<noteq> 0"
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
   474
  shows "\<exists>r. \<forall>z. r \<le> norm z \<longrightarrow> d \<le> norm (poly (pCons a p) z)"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   475
  using ex
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   476
proof (induct p arbitrary: a d)
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   477
  case 0
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   478
  then show ?case by simp
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   479
next
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   480
  case (pCons c cs a d)
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   481
  show ?case
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   482
  proof (cases "cs = 0")
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   483
    case False
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   484
    with pCons.hyps obtain r where r: "\<forall>z. r \<le> norm z \<longrightarrow> d + norm a \<le> norm (poly (pCons c cs) z)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   485
      by blast
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   486
    let ?r = "1 + \<bar>r\<bar>"
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   487
    have "d \<le> norm (poly (pCons a (pCons c cs)) z)" if "1 + \<bar>r\<bar> \<le> norm z" for z
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   488
    proof -
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   489
      have r0: "r \<le> norm z"
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   490
        using that by arith
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   491
      from r[rule_format, OF r0] have th0: "d + norm a \<le> 1 * norm(poly (pCons c cs) z)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   492
        by arith
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   493
      from that have z1: "norm z \<ge> 1"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   494
        by arith
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   495
      from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
   496
      have th1: "d \<le> norm(z * poly (pCons c cs) z) - norm a"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   497
        unfolding norm_mult by (simp add: algebra_simps)
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
   498
      from norm_diff_ineq[of "z * poly (pCons c cs) z" a]
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   499
      have th2: "norm (z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
51541
e7b6b61b7be2 tuned proofs;
wenzelm
parents: 51537
diff changeset
   500
        by (simp add: algebra_simps)
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   501
      from th1 th2 show ?thesis
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   502
        by arith
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   503
    qed
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   504
    then show ?thesis by blast
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   505
  next
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   506
    case True
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   507
    with pCons.prems have c0: "c \<noteq> 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   508
      by simp
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   509
    have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   510
      if h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z" for z :: 'a
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   511
    proof -
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   512
      from c0 have "norm c > 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   513
        by simp
56403
ae4f904c98b0 tuned spaces
blanchet
parents: 55735
diff changeset
   514
      from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z * c)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   515
        by (simp add: field_simps norm_mult)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   516
      have ath: "\<And>mzh mazh ma. mzh \<le> mazh + ma \<Longrightarrow> \<bar>d\<bar> + ma \<le> mzh \<Longrightarrow> d \<le> mazh"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   517
        by arith
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   518
      from norm_diff_ineq[of "z * c" a] have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   519
        by (simp add: algebra_simps)
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   520
      from ath[OF th1 th0] show ?thesis
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   521
        using True by simp
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   522
    qed
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   523
    then show ?thesis by blast
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   524
  qed
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   525
qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   526
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   527
text \<open>Hence polynomial's modulus attains its minimum somewhere.\<close>
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   528
lemma poly_minimum_modulus: "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   529
proof (induct p)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   530
  case 0
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   531
  then show ?case by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   532
next
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   533
  case (pCons c cs)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   534
  show ?case
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   535
  proof (cases "cs = 0")
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   536
    case False
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   537
    from poly_infinity[OF False, of "cmod (poly (pCons c cs) 0)" c]
63060
293ede07b775 some uses of 'obtain' with structure statement;
wenzelm
parents: 62128
diff changeset
   538
    obtain r where r: "cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
293ede07b775 some uses of 'obtain' with structure statement;
wenzelm
parents: 62128
diff changeset
   539
      if "r \<le> cmod z" for z
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   540
      by blast
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   541
    have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   542
      by arith
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   543
    from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
63060
293ede07b775 some uses of 'obtain' with structure statement;
wenzelm
parents: 62128
diff changeset
   544
    obtain v where v: "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
293ede07b775 some uses of 'obtain' with structure statement;
wenzelm
parents: 62128
diff changeset
   545
      if "cmod w \<le> \<bar>r\<bar>" for w
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   546
      by blast
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   547
    have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)" if z: "r \<le> cmod z" for z
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   548
      using v[of 0] r[OF z] by simp
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   549
    with v ath[of r] show ?thesis
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   550
      by blast
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   551
  next
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   552
    case True
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   553
    with pCons.hyps show ?thesis
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   554
      by simp
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   555
  qed
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   556
qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   557
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   558
text \<open>Constant function (non-syntactic characterization).\<close>
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   559
definition "constant f \<longleftrightarrow> (\<forall>x y. f x = f y)"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   560
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   561
lemma nonconstant_length: "\<not> constant (poly p) \<Longrightarrow> psize p \<ge> 2"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   562
  by (induct p) (auto simp: constant_def psize_def)
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   563
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   564
lemma poly_replicate_append: "poly (monom 1 n * p) (x::'a::comm_ring_1) = x^n * poly p x"
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   565
  by (simp add: poly_monom)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   566
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   567
text \<open>Decomposition of polynomial, skipping zero coefficients after the first.\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   568
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   569
lemma poly_decompose_lemma:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   570
  assumes nz: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly p z = (0::'a::idom))"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   571
  shows "\<exists>k a q. a \<noteq> 0 \<and> Suc (psize q + k) = psize p \<and> (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   572
  unfolding psize_def
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   573
  using nz
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   574
proof (induct p)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   575
  case 0
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   576
  then show ?case by simp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   577
next
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   578
  case (pCons c cs)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   579
  show ?case
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   580
  proof (cases "c = 0")
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   581
    case True
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   582
    from pCons.hyps pCons.prems True show ?thesis
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   583
      apply auto
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   584
      apply (rule_tac x="k+1" in exI)
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   585
      apply (rule_tac x="a" in exI)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   586
      apply clarsimp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   587
      apply (rule_tac x="q" in exI)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   588
      apply auto
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   589
      done
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   590
  next
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   591
    case False
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   592
    show ?thesis
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   593
      apply (rule exI[where x=0])
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   594
      apply (rule exI[where x=c])
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   595
      apply (auto simp: False)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   596
      done
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   597
  qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   598
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   599
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   600
lemma poly_decompose:
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   601
  assumes nc: "\<not> constant (poly p)"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   602
  shows "\<exists>k a q. a \<noteq> (0::'a::idom) \<and> k \<noteq> 0 \<and>
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   603
               psize q + k + 1 = psize p \<and>
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   604
              (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   605
  using nc
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   606
proof (induct p)
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   607
  case 0
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   608
  then show ?case
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   609
    by (simp add: constant_def)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   610
next
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   611
  case (pCons c cs)
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   612
  have "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   613
  proof
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   614
    assume "\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   615
    then have "poly (pCons c cs) x = poly (pCons c cs) y" for x y
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   616
      by (cases "x = 0") auto
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   617
    with pCons.prems show False
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   618
      by (auto simp add: constant_def)
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   619
  qed
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   620
  from poly_decompose_lemma[OF this]
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   621
  show ?case
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   622
    apply clarsimp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   623
    apply (rule_tac x="k+1" in exI)
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   624
    apply (rule_tac x="a" in exI)
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   625
    apply simp
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   626
    apply (rule_tac x="q" in exI)
29538
5cc98af1398d rename plength to psize
huffman
parents: 29485
diff changeset
   627
    apply (auto simp add: psize_def split: if_splits)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   628
    done
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   629
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   630
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   631
text \<open>Fundamental theorem of algebra\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   632
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   633
lemma fundamental_theorem_of_algebra:
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   634
  assumes nc: "\<not> constant (poly p)"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   635
  shows "\<exists>z::complex. poly p z = 0"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   636
  using nc
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   637
proof (induct "psize p" arbitrary: p rule: less_induct)
34915
7894c7dab132 Adapted to changes in induct method.
berghofe
parents: 32960
diff changeset
   638
  case less
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   639
  let ?p = "poly p"
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   640
  let ?ths = "\<exists>z. ?p z = 0"
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   641
34915
7894c7dab132 Adapted to changes in induct method.
berghofe
parents: 32960
diff changeset
   642
  from nonconstant_length[OF less(2)] have n2: "psize p \<ge> 2" .
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   643
  from poly_minimum_modulus obtain c where c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   644
    by blast
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   645
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   646
  show ?ths
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   647
  proof (cases "?p c = 0")
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   648
    case True
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   649
    then show ?thesis by blast
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   650
  next
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   651
    case False
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   652
    from poly_offset[of p c] obtain q where q: "psize q = psize p" "\<forall>x. poly q x = ?p (c + x)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   653
      by blast
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   654
    have False if h: "constant (poly q)"
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   655
    proof -
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   656
      from q(2) have th: "\<forall>x. poly q (x - c) = ?p x"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   657
        by auto
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   658
      have "?p x = ?p y" for x y
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   659
      proof -
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   660
        from th have "?p x = poly q (x - c)"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   661
          by auto
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   662
        also have "\<dots> = poly q (y - c)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   663
          using h unfolding constant_def by blast
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   664
        also have "\<dots> = ?p y"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   665
          using th by auto
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   666
        finally show ?thesis .
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   667
      qed
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   668
      with less(2) show ?thesis
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   669
        unfolding constant_def by blast
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   670
    qed
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   671
    then have qnc: "\<not> constant (poly q)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   672
      by blast
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   673
    from q(2) have pqc0: "?p c = poly q 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   674
      by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   675
    from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   676
      by simp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   677
    let ?a0 = "poly q 0"
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   678
    from False pqc0 have a00: "?a0 \<noteq> 0"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   679
      by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   680
    from a00 have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   681
      by simp
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   682
    let ?r = "smult (inverse ?a0) q"
29538
5cc98af1398d rename plength to psize
huffman
parents: 29485
diff changeset
   683
    have lgqr: "psize q = psize ?r"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   684
      using a00
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   685
      unfolding psize_def degree_def
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 51541
diff changeset
   686
      by (simp add: poly_eq_iff)
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   687
    have False if h: "\<And>x y. poly ?r x = poly ?r y"
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   688
    proof -
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   689
      have "poly q x = poly q y" for x y
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   690
      proof -
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   691
        from qr[rule_format, of x] have "poly q x = poly ?r x * ?a0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   692
          by auto
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   693
        also have "\<dots> = poly ?r y * ?a0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   694
          using h by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   695
        also have "\<dots> = poly q y"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   696
          using qr[rule_format, of y] by simp
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   697
        finally show ?thesis .
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   698
      qed
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   699
      with qnc show ?thesis
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   700
        unfolding constant_def by blast
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   701
    qed
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   702
    then have rnc: "\<not> constant (poly ?r)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   703
      unfolding constant_def by blast
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   704
    from qr[rule_format, of 0] a00 have r01: "poly ?r 0 = 1"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   705
      by auto
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   706
    have mrmq_eq: "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" for w
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   707
    proof -
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   708
      have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   709
        using qr[rule_format, of w] a00 by (simp add: divide_inverse ac_simps)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   710
      also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   711
        using a00 unfolding norm_divide by (simp add: field_simps)
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   712
      finally show ?thesis .
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   713
    qed
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   714
    from poly_decompose[OF rnc] obtain k a s where
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   715
      kas: "a \<noteq> 0" "k \<noteq> 0" "psize s + k + 1 = psize ?r"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   716
        "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   717
    have "\<exists>w. cmod (poly ?r w) < 1"
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   718
    proof (cases "psize p = k + 1")
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   719
      case True
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   720
      with kas(3) lgqr[symmetric] q(1) have s0: "s = 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   721
        by auto
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   722
      have hth[symmetric]: "cmod (poly ?r w) = cmod (1 + a * w ^ k)" for w
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   723
        using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   724
      from reduce_poly_simple[OF kas(1,2)] show ?thesis
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   725
        unfolding hth by blast
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   726
    next
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   727
      case False note kn = this
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   728
      from kn kas(3) q(1) lgqr have k1n: "k + 1 < psize p"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   729
        by simp
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   730
      have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   731
        unfolding constant_def poly_pCons poly_monom
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   732
        using kas(1)
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   733
        apply simp
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   734
        apply (rule exI[where x=0])
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   735
        apply (rule exI[where x=1])
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   736
        apply simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   737
        done
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   738
      from kas(1) kas(2) have th02: "k + 1 = psize (pCons 1 (monom a (k - 1)))"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   739
        by (simp add: psize_def degree_monom_eq)
34915
7894c7dab132 Adapted to changes in induct method.
berghofe
parents: 32960
diff changeset
   740
      from less(1) [OF k1n [simplified th02] th01]
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   741
      obtain w where w: "1 + w^k * a = 0"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   742
        unfolding poly_pCons poly_monom
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   743
        using kas(2) by (cases k) (auto simp add: algebra_simps)
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   744
      from poly_bound_exists[of "cmod w" s] obtain m where
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   745
        m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   746
      have w0: "w \<noteq> 0"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   747
        using kas(2) w by (auto simp add: power_0_left)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   748
      from w have "(1 + w ^ k * a) - 1 = 0 - 1"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   749
        by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   750
      then have wm1: "w^k * a = - 1"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   751
        by simp
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   752
      have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   753
        using norm_ge_zero[of w] w0 m(1)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   754
        by (simp add: inverse_eq_divide zero_less_mult_iff)
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   755
      with real_lbound_gt_zero[OF zero_less_one] obtain t where
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   756
        t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   757
      let ?ct = "complex_of_real t"
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   758
      let ?w = "?ct * w"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   759
      have "1 + ?w^k * (a + ?w * poly s ?w) = 1 + ?ct^k * (w^k * a) + ?w^k * ?w * poly s ?w"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   760
        using kas(1) by (simp add: algebra_simps power_mult_distrib)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   761
      also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   762
        unfolding wm1 by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   763
      finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) =
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   764
        cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)"
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   765
        by metis
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   766
      with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   767
      have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   768
        unfolding norm_of_real by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   769
      have ath: "\<And>x t::real. 0 \<le> x \<Longrightarrow> x < t \<Longrightarrow> t \<le> 1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   770
        by arith
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   771
      have "t * cmod w \<le> 1 * cmod w"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   772
        apply (rule mult_mono)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   773
        using t(1,2)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   774
        apply auto
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   775
        done
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   776
      then have tw: "cmod ?w \<le> cmod w"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   777
        using t(1) by (simp add: norm_mult)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   778
      from t inv0 have "t * (cmod w ^ (k + 1) * m) < 1"
57862
8f074e6e22fc tuned proofs;
wenzelm
parents: 57514
diff changeset
   779
        by (simp add: field_simps)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   780
      with zero_less_power[OF t(1), of k] have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
59557
ebd8ecacfba6 establish unique preferred fact names
haftmann
parents: 59555
diff changeset
   781
        by simp
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   782
      have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k + 1) * cmod (poly s ?w)))"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   783
        using w0 t(1)
51541
e7b6b61b7be2 tuned proofs;
wenzelm
parents: 51537
diff changeset
   784
        by (simp add: algebra_simps power_mult_distrib norm_power norm_mult)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   785
      then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   786
        using t(1,2) m(2)[rule_format, OF tw] w0
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   787
        by auto
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   788
      with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   789
        by simp
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   790
      from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   791
        by auto
27514
6fcf6864d703 remove redundant lemmas about cmod
huffman
parents: 27445
diff changeset
   792
      from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121]
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   793
      have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" .
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   794
      from th11 th12 have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   795
        by arith
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   796
      then have "cmod (poly ?r ?w) < 1"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   797
        unfolding kas(4)[rule_format, of ?w] r01 by simp
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   798
      then show ?thesis
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   799
        by blast
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   800
    qed
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   801
    with cq0 q(2) show ?thesis
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   802
      unfolding mrmq_eq not_less[symmetric] by auto
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   803
  qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   804
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   805
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   806
text \<open>Alternative version with a syntactic notion of constant polynomial.\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   807
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   808
lemma fundamental_theorem_of_algebra_alt:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   809
  assumes nc: "\<not> (\<exists>a l. a \<noteq> 0 \<and> l = 0 \<and> p = pCons a l)"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   810
  shows "\<exists>z. poly p z = (0::complex)"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   811
  using nc
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   812
proof (induct p)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   813
  case 0
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   814
  then show ?case by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   815
next
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   816
  case (pCons c cs)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   817
  show ?case
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   818
  proof (cases "c = 0")
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   819
    case True
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   820
    then show ?thesis by auto
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   821
  next
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   822
    case False
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   823
    have "\<not> constant (poly (pCons c cs))"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   824
    proof
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   825
      assume nc: "constant (poly (pCons c cs))"
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   826
      from nc[unfolded constant_def, rule_format, of 0]
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   827
      have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   828
      then have "cs = 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   829
      proof (induct cs)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   830
        case 0
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   831
        then show ?case by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   832
      next
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   833
        case (pCons d ds)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   834
        show ?case
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   835
        proof (cases "d = 0")
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   836
          case True
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   837
          then show ?thesis
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   838
            using pCons.prems pCons.hyps by simp
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   839
        next
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   840
          case False
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   841
          from poly_bound_exists[of 1 ds] obtain m where
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   842
            m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   843
          have dm: "cmod d / m > 0"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   844
            using False m(1) by (simp add: field_simps)
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   845
          from real_lbound_gt_zero[OF dm zero_less_one]
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   846
          obtain x where x: "x > 0" "x < cmod d / m" "x < 1"
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   847
            by blast
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   848
          let ?x = "complex_of_real x"
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   849
          from x have cx: "?x \<noteq> 0" "cmod ?x \<le> 1"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   850
            by simp_all
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   851
          from pCons.prems[rule_format, OF cx(1)]
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   852
          have cth: "cmod (?x*poly ds ?x) = cmod d"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   853
            by (simp add: eq_diff_eq[symmetric])
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   854
          from m(2)[rule_format, OF cx(2)] x(1)
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   855
          have th0: "cmod (?x*poly ds ?x) \<le> x*m"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   856
            by (simp add: norm_mult)
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   857
          from x(2) m(1) have "x * m < cmod d"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   858
            by (simp add: field_simps)
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   859
          with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   860
            by auto
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   861
          with cth show ?thesis
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   862
            by blast
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   863
        qed
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   864
      qed
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   865
      then show False
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   866
        using pCons.prems False by blast
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   867
    qed
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   868
    then show ?thesis
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   869
      by (rule fundamental_theorem_of_algebra)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   870
  qed
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   871
qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   872
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   873
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   874
subsection \<open>Nullstellensatz, degrees and divisibility of polynomials\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   875
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   876
lemma nullstellensatz_lemma:
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   877
  fixes p :: "complex poly"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   878
  assumes "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   879
    and "degree p = n"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   880
    and "n \<noteq> 0"
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   881
  shows "p dvd (q ^ n)"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   882
  using assms
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   883
proof (induct n arbitrary: p q rule: nat_less_induct)
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   884
  fix n :: nat
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
   885
  fix p q :: "complex poly"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   886
  assume IH: "\<forall>m<n. \<forall>p q.
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   887
                 (\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longrightarrow>
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   888
                 degree p = m \<longrightarrow> m \<noteq> 0 \<longrightarrow> p dvd (q ^ m)"
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
   889
    and pq0: "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   890
    and dpn: "degree p = n"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   891
    and n0: "n \<noteq> 0"
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   892
  from dpn n0 have pne: "p \<noteq> 0" by auto
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   893
  show "p dvd (q ^ n)"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   894
  proof (cases "\<exists>a. poly p a = 0")
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   895
    case True
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   896
    then obtain a where a: "poly p a = 0" ..
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   897
    have ?thesis if oa: "order a p \<noteq> 0"
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   898
    proof -
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
   899
      let ?op = "order a p"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   900
      from pne have ap: "([:- a, 1:] ^ ?op) dvd p" "\<not> [:- a, 1:] ^ (Suc ?op) dvd p"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   901
        using order by blast+
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   902
      note oop = order_degree[OF pne, unfolded dpn]
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   903
      show ?thesis
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   904
      proof (cases "q = 0")
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   905
        case True
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   906
        with n0 show ?thesis by (simp add: power_0_left)
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   907
      next
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   908
        case False
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   909
        from pq0[rule_format, OF a, unfolded poly_eq_0_iff_dvd]
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   910
        obtain r where r: "q = [:- a, 1:] * r" by (rule dvdE)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   911
        from ap(1) obtain s where s: "p = [:- a, 1:] ^ ?op * s"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   912
          by (rule dvdE)
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   913
        have sne: "s \<noteq> 0"
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   914
          using s pne by auto
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   915
        show ?thesis
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   916
        proof (cases "degree s = 0")
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   917
          case True
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   918
          then obtain k where kpn: "s = [:k:]"
51541
e7b6b61b7be2 tuned proofs;
wenzelm
parents: 51537
diff changeset
   919
            by (cases s) (auto split: if_splits)
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   920
          from sne kpn have k: "k \<noteq> 0" by simp
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32456
diff changeset
   921
          let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
   922
          have "q ^ n = p * ?w"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   923
            apply (subst r)
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   924
            apply (subst s)
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   925
            apply (subst kpn)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   926
            using k oop [of a]
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   927
            apply (subst power_mult_distrib)
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   928
            apply simp
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   929
            apply (subst power_add [symmetric])
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   930
            apply simp
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   931
            done
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   932
          then show ?thesis
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   933
            unfolding dvd_def by blast
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   934
        next
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   935
          case False
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   936
          with sne dpn s oa have dsn: "degree s < n"
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   937
            apply auto
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   938
            apply (erule ssubst)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   939
            apply (simp add: degree_mult_eq degree_linear_power)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   940
            done
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   941
          have "poly r x = 0" if h: "poly s x = 0" for x
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   942
          proof -
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   943
            have xa: "x \<noteq> a"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   944
            proof
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   945
              assume "x = a"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   946
              from h[unfolded this poly_eq_0_iff_dvd] obtain u where u: "s = [:- a, 1:] * u"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   947
                by (rule dvdE)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   948
              have "p = [:- a, 1:] ^ (Suc ?op) * u"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   949
                apply (subst s)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   950
                apply (subst u)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   951
                apply (simp only: power_Suc ac_simps)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   952
                done
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   953
              with ap(2)[unfolded dvd_def] show False
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   954
                by blast
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   955
            qed
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   956
            from h have "poly p x = 0"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   957
              by (subst s) simp
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   958
            with pq0 have "poly q x = 0"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
   959
              by blast
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   960
            with r xa show ?thesis
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   961
              by auto
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   962
          qed
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   963
          with IH[rule_format, OF dsn, of s r] False have "s dvd (r ^ (degree s))"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   964
            by blast
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   965
          then obtain u where u: "r ^ (degree s) = s * u" ..
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   966
          then have u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   967
            by (simp only: poly_mult[symmetric] poly_power[symmetric])
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   968
          let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   969
          from oop[of a] dsn have "q ^ n = p * ?w"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   970
            apply -
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   971
            apply (subst s)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   972
            apply (subst r)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   973
            apply (simp only: power_mult_distrib)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   974
            apply (subst mult.assoc [where b=s])
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   975
            apply (subst mult.assoc [where a=u])
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   976
            apply (subst mult.assoc [where b=u, symmetric])
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   977
            apply (subst u [symmetric])
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   978
            apply (simp add: ac_simps power_add [symmetric])
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   979
            done
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   980
          then show ?thesis
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   981
            unfolding dvd_def by blast
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   982
        qed
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   983
      qed
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
   984
    qed
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   985
    then show ?thesis
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   986
      using a order_root pne by blast
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   987
  next
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   988
    case False
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   989
    with fundamental_theorem_of_algebra_alt[of p]
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   990
    obtain c where ccs: "c \<noteq> 0" "p = pCons c 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   991
      by blast
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   992
    then have pp: "poly p x = c" for x
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   993
      by simp
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
   994
    let ?w = "[:1/c:] * (q ^ n)"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   995
    from ccs have "(q ^ n) = (p * ?w)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   996
      by simp
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   997
    then show ?thesis
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
   998
      unfolding dvd_def by blast
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
   999
  qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1000
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1001
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1002
lemma nullstellensatz_univariate:
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
  1003
  "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1004
    p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1005
proof -
60457
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1006
  consider "p = 0" | "p \<noteq> 0" "degree p = 0" | n where "p \<noteq> 0" "degree p = Suc n"
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1007
    by (cases "degree p") auto
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1008
  then show ?thesis
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1009
  proof cases
60567
19c277ea65ae tuned proofs -- less digits;
wenzelm
parents: 60557
diff changeset
  1010
    case p: 1
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1011
    then have eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
52380
3cc46b8cca5e lifting for primitive definitions;
haftmann
parents: 51541
diff changeset
  1012
      by (auto simp add: poly_all_0_iff_0)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1013
    {
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1014
      assume "p dvd (q ^ (degree p))"
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1015
      then obtain r where r: "q ^ (degree p) = p * r" ..
60567
19c277ea65ae tuned proofs -- less digits;
wenzelm
parents: 60557
diff changeset
  1016
      from r p have False by simp
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1017
    }
60567
19c277ea65ae tuned proofs -- less digits;
wenzelm
parents: 60557
diff changeset
  1018
    with eq p show ?thesis by blast
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
  1019
  next
60567
19c277ea65ae tuned proofs -- less digits;
wenzelm
parents: 60557
diff changeset
  1020
    case dp: 2
60457
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1021
    then obtain k where k: "p = [:k:]" "k \<noteq> 0"
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1022
      by (cases p) (simp split: if_splits)
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1023
    then have th1: "\<forall>x. poly p x \<noteq> 0"
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1024
      by simp
60567
19c277ea65ae tuned proofs -- less digits;
wenzelm
parents: 60557
diff changeset
  1025
    from k dp(2) have "q ^ (degree p) = p * [:1/k:]"
60457
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1026
      by (simp add: one_poly_def)
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1027
    then have th2: "p dvd (q ^ (degree p))" ..
60567
19c277ea65ae tuned proofs -- less digits;
wenzelm
parents: 60557
diff changeset
  1028
    from dp(1) th1 th2 show ?thesis
60457
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1029
      by blast
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1030
  next
60567
19c277ea65ae tuned proofs -- less digits;
wenzelm
parents: 60557
diff changeset
  1031
    case dp: 3
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1032
    have False if dvd: "p dvd (q ^ (Suc n))" and h: "poly p x = 0" "poly q x \<noteq> 0" for x
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1033
    proof -
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1034
      from dvd obtain u where u: "q ^ (Suc n) = p * u" ..
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1035
      from h have "poly (q ^ (Suc n)) x \<noteq> 0"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1036
        by simp
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1037
      with u h(1) show ?thesis
60457
f31f7599ef55 tuned proofs;
wenzelm
parents: 60449
diff changeset
  1038
        by (simp only: poly_mult) simp
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1039
    qed
60567
19c277ea65ae tuned proofs -- less digits;
wenzelm
parents: 60557
diff changeset
  1040
    with dp nullstellensatz_lemma[of p q "degree p"] show ?thesis
19c277ea65ae tuned proofs -- less digits;
wenzelm
parents: 60557
diff changeset
  1041
      by auto
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
  1042
  qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1043
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1044
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
  1045
text \<open>Useful lemma\<close>
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1046
lemma constant_degree:
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1047
  fixes p :: "'a::{idom,ring_char_0} poly"
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1048
  shows "constant (poly p) \<longleftrightarrow> degree p = 0" (is "?lhs = ?rhs")
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1049
proof
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1050
  show ?rhs if ?lhs
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1051
  proof -
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1052
    from that[unfolded constant_def, rule_format, of _ "0"]
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1053
    have th: "poly p = poly [:poly p 0:]"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1054
      by auto
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1055
    then have "p = [:poly p 0:]"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1056
      by (simp add: poly_eq_poly_eq_iff)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1057
    then have "degree p = degree [:poly p 0:]"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1058
      by simp
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1059
    then show ?thesis
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1060
      by simp
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1061
  qed
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1062
  show ?lhs if ?rhs
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1063
  proof -
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1064
    from that obtain k where "p = [:k:]"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1065
      by (cases p) (simp split: if_splits)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1066
    then show ?thesis
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1067
      unfolding constant_def by auto
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1068
  qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1069
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1070
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
  1071
text \<open>Arithmetic operations on multivariate polynomials.\<close>
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1072
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
  1073
lemma mpoly_base_conv:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1074
  fixes x :: "'a::comm_ring_1"
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
  1075
  shows "0 = poly 0 x" "c = poly [:c:] x" "x = poly [:0,1:] x"
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
  1076
  by simp_all
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1077
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
  1078
lemma mpoly_norm_conv:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1079
  fixes x :: "'a::comm_ring_1"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1080
  shows "poly [:0:] x = poly 0 x" "poly [:poly 0 y:] x = poly 0 x"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1081
  by simp_all
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1082
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
  1083
lemma mpoly_sub_conv:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1084
  fixes x :: "'a::comm_ring_1"
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
  1085
  shows "poly p x - poly q x = poly p x + -1 * poly q x"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53077
diff changeset
  1086
  by simp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1087
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1088
lemma poly_pad_rule: "poly p x = 0 \<Longrightarrow> poly (pCons 0 p) x = 0"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1089
  by simp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1090
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
  1091
lemma poly_cancel_eq_conv:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1092
  fixes x :: "'a::field"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
  1093
  shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> y = 0 \<longleftrightarrow> a * y - b * x = 0"
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
  1094
  by auto
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1095
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
  1096
lemma poly_divides_pad_rule:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1097
  fixes p:: "('a::comm_ring_1) poly"
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1098
  assumes pq: "p dvd q"
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1099
  shows "p dvd (pCons 0 q)"
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1100
proof -
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1101
  have "pCons 0 q = q * [:0,1:]" by simp
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1102
  then have "q dvd (pCons 0 q)" ..
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1103
  with pq show ?thesis by (rule dvd_trans)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1104
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1105
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
  1106
lemma poly_divides_conv0:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1107
  fixes p:: "'a::field poly"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1108
  assumes lgpq: "degree q < degree p"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1109
    and lq: "p \<noteq> 0"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1110
  shows "p dvd q \<longleftrightarrow> q = 0" (is "?lhs \<longleftrightarrow> ?rhs")
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1111
proof
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1112
  assume ?rhs
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1113
  then have "q = p * 0" by simp
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1114
  then show ?lhs ..
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1115
next
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1116
  assume l: ?lhs
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1117
  show ?rhs
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1118
  proof (cases "q = 0")
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1119
    case True
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1120
    then show ?thesis by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1121
  next
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1122
    assume q0: "q \<noteq> 0"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1123
    from l q0 have "degree p \<le> degree q"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1124
      by (rule dvd_imp_degree_le)
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1125
    with lgpq show ?thesis by simp
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1126
  qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1127
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1128
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
  1129
lemma poly_divides_conv1:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1130
  fixes p :: "'a::field poly"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1131
  assumes a0: "a \<noteq> 0"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1132
    and pp': "p dvd p'"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1133
    and qrp': "smult a q - p' = r"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1134
  shows "p dvd q \<longleftrightarrow> p dvd r" (is "?lhs \<longleftrightarrow> ?rhs")
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1135
proof
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1136
  from pp' obtain t where t: "p' = p * t" ..
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1137
  show ?rhs if ?lhs
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1138
  proof -
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1139
    from that obtain u where u: "q = p * u" ..
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1140
    have "r = p * (smult a u - t)"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1141
      using u qrp' [symmetric] t by (simp add: algebra_simps)
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1142
    then show ?thesis ..
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1143
  qed
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1144
  show ?lhs if ?rhs
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1145
  proof -
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1146
    from that obtain u where u: "r = p * u" ..
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1147
    from u [symmetric] t qrp' [symmetric] a0
60557
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1148
    have "q = p * smult (1/a) (u + t)"
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1149
      by (simp add: algebra_simps)
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1150
    then show ?thesis ..
5854821993d2 tuned proofs;
wenzelm
parents: 60457
diff changeset
  1151
  qed
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1152
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1153
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1154
lemma basic_cqe_conv1:
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
  1155
  "(\<exists>x. poly p x = 0 \<and> poly 0 x \<noteq> 0) \<longleftrightarrow> False"
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
  1156
  "(\<exists>x. poly 0 x \<noteq> 0) \<longleftrightarrow> False"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1157
  "(\<exists>x. poly [:c:] x \<noteq> 0) \<longleftrightarrow> c \<noteq> 0"
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
  1158
  "(\<exists>x. poly 0 x = 0) \<longleftrightarrow> True"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1159
  "(\<exists>x. poly [:c:] x = 0) \<longleftrightarrow> c = 0"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1160
  by simp_all
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1161
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
  1162
lemma basic_cqe_conv2:
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
  1163
  assumes l: "p \<noteq> 0"
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
  1164
  shows "\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1165
proof -
60424
c96fff9dcdbc misc tuning;
wenzelm
parents: 59557
diff changeset
  1166
  have False if "h \<noteq> 0" "t = 0" and "pCons a (pCons b p) = pCons h t" for h t
60449
229bad93377e renamed "prems" to "that";
wenzelm
parents: 60424
diff changeset
  1167
    using l that by simp
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1168
  then have th: "\<not> (\<exists> h t. h \<noteq> 0 \<and> t = 0 \<and> pCons a (pCons b p) = pCons h t)"
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1169
    by blast
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1170
  from fundamental_theorem_of_algebra_alt[OF th] show ?thesis
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1171
    by auto
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1172
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1173
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1174
lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<longleftrightarrow> p \<noteq> 0"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1175
  by (metis poly_all_0_iff_0)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1176
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1177
lemma basic_cqe_conv3:
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1178
  fixes p q :: "complex poly"
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30242
diff changeset
  1179
  assumes l: "p \<noteq> 0"
56795
e8cce2bd23e5 tuned proofs;
wenzelm
parents: 56778
diff changeset
  1180
  shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<longleftrightarrow> \<not> (pCons a p) dvd (q ^ psize p)"
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
  1181
proof -
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1182
  from l have dp: "degree (pCons a p) = psize p"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1183
    by (simp add: psize_def)
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1184
  from nullstellensatz_univariate[of "pCons a p" q] l
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
  1185
  show ?thesis
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
  1186
    by (metis dp pCons_eq_0_iff)
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1187
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1188
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1189
lemma basic_cqe_conv4:
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1190
  fixes p q :: "complex poly"
55358
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
  1191
  assumes h: "\<And>x. poly (q ^ n) x = poly r x"
85d81bc281d0 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
paulson <lp15@cam.ac.uk>
parents: 54489
diff changeset
  1192
  shows "p dvd (q ^ n) \<longleftrightarrow> p dvd r"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1193
proof -
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1194
  from h have "poly (q ^ n) = poly r"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1195
    by auto
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1196
  then have "(q ^ n) = r"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1197
    by (simp add: poly_eq_poly_eq_iff)
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1198
  then show "p dvd (q ^ n) \<longleftrightarrow> p dvd r"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1199
    by simp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1200
qed
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1201
55735
81ba62493610 generalised some results using type classes
paulson <lp15@cam.ac.uk>
parents: 55734
diff changeset
  1202
lemma poly_const_conv:
56778
cb0929421ca6 tuned proofs;
wenzelm
parents: 56776
diff changeset
  1203
  fixes x :: "'a::comm_ring_1"
56776
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1204
  shows "poly [:c:] x = y \<longleftrightarrow> c = y"
309e1a61ee7c tuned proofs;
wenzelm
parents: 56544
diff changeset
  1205
  by simp
26123
44384b5c4fc0 A proof a the fundamental theorem of algebra
chaieb
parents:
diff changeset
  1206
29464
c0d225a7f6ff convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman
parents: 29292
diff changeset
  1207
end