Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
authorpaulson <lp15@cam.ac.uk>
Fri Feb 07 17:43:47 2014 +0000 (2014-02-07)
changeset 5535885d81bc281d0
parent 55357 1dd39517e1ce
child 55360 8cd866874590
Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
src/HOL/Library/Fundamental_Theorem_Algebra.thy
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Feb 07 14:18:31 2014 +0100
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Feb 07 17:43:47 2014 +0000
     1.3 @@ -60,10 +60,6 @@
     1.4  lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
     1.5    by (rule of_real_power [symmetric])
     1.6  
     1.7 -lemma real_down2: "(0::real) < d1 \<Longrightarrow> 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
     1.8 -  apply (rule exI[where x = "min d1 d2 / 2"])
     1.9 -  by (simp add: field_simps min_def)
    1.10 -
    1.11  text{* The triangle inequality for cmod *}
    1.12  lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
    1.13    using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
    1.14 @@ -246,7 +242,7 @@
    1.15    shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
    1.16  proof-
    1.17    from seq_monosub[of "Re o s"]
    1.18 -  obtain f g where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
    1.19 +  obtain f where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
    1.20      unfolding o_def by blast
    1.21    from seq_monosub[of "Im o s o f"]
    1.22    obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s(f(g n))))" unfolding o_def by blast
    1.23 @@ -260,8 +256,7 @@
    1.24    have conv1: "convergent (\<lambda>n. Re (s ( f n)))"
    1.25      apply (rule Bseq_monoseq_convergent)
    1.26      apply (simp add: Bseq_def)
    1.27 -    apply (rule exI[where x= "r + 1"])
    1.28 -    using th rp apply simp
    1.29 +    apply (metis gt_ex le_less_linear less_trans order.trans th)
    1.30      using f(2) .
    1.31    have th:"\<forall>n. r + 1 \<ge> \<bar> Im (s n)\<bar>"
    1.32    proof
    1.33 @@ -272,8 +267,7 @@
    1.34    have conv2: "convergent (\<lambda>n. Im (s (f (g n))))"
    1.35      apply (rule Bseq_monoseq_convergent)
    1.36      apply (simp add: Bseq_def)
    1.37 -    apply (rule exI[where x= "r + 1"])
    1.38 -    using th rp apply simp
    1.39 +    apply (metis gt_ex le_less_linear less_trans order.trans th)
    1.40      using g(2) .
    1.41  
    1.42    from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
    1.43 @@ -347,14 +341,8 @@
    1.44  lemma  poly_minimum_modulus_disc:
    1.45    "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
    1.46  proof-
    1.47 -  {assume "\<not> r \<ge> 0" hence ?thesis unfolding linorder_not_le
    1.48 -      apply -
    1.49 -      apply (rule exI[where x=0])
    1.50 -      apply auto
    1.51 -      apply (subgoal_tac "cmod w < 0")
    1.52 -      apply simp
    1.53 -      apply arith
    1.54 -      done }
    1.55 +  {assume "\<not> r \<ge> 0" hence ?thesis
    1.56 +    by (metis norm_ge_zero order.trans)}
    1.57    moreover
    1.58    {assume rp: "r \<ge> 0"
    1.59      from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))" by simp
    1.60 @@ -558,11 +546,9 @@
    1.61        by (auto)}
    1.62    moreover
    1.63    {assume c0: "c\<noteq>0"
    1.64 -    hence ?case apply-
    1.65 +    have ?case 
    1.66        apply (rule exI[where x=0])
    1.67 -      apply (rule exI[where x=c], clarsimp)
    1.68 -      apply (rule exI[where x=cs])
    1.69 -      apply auto
    1.70 +      apply (rule exI[where x=c], auto simp add: c0)
    1.71        done}
    1.72    ultimately show ?case by blast
    1.73  qed
    1.74 @@ -682,7 +668,7 @@
    1.75        have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
    1.76          using norm_ge_zero[of w] w0 m(1)
    1.77            by (simp add: inverse_eq_divide zero_less_mult_iff)
    1.78 -      with real_down2[OF zero_less_one] obtain t where
    1.79 +      with real_lbound_gt_zero[OF zero_less_one] obtain t where
    1.80          t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
    1.81        let ?ct = "complex_of_real t"
    1.82        let ?w = "?ct * w"
    1.83 @@ -690,10 +676,7 @@
    1.84        also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
    1.85          unfolding wm1 by (simp)
    1.86        finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) = cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)"
    1.87 -        apply -
    1.88 -        apply (rule cong[OF refl[of cmod]])
    1.89 -        apply assumption
    1.90 -        done
    1.91 +        by metis
    1.92        with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
    1.93        have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)" unfolding norm_of_real by simp
    1.94        have ath: "\<And>x (t::real). 0\<le> x \<Longrightarrow> x < t \<Longrightarrow> t\<le>1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1" by arith
    1.95 @@ -703,14 +686,12 @@
    1.96          by (simp add: inverse_eq_divide field_simps)
    1.97        with zero_less_power[OF t(1), of k]
    1.98        have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
    1.99 -        apply - apply (rule mult_strict_left_mono) by simp_all
   1.100 +        by (metis comm_mult_strict_left_mono)
   1.101        have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))"  using w0 t(1)
   1.102          by (simp add: algebra_simps power_mult_distrib norm_power norm_mult)
   1.103        then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
   1.104          using t(1,2) m(2)[rule_format, OF tw] w0
   1.105 -        apply (simp only: )
   1.106 -        apply auto
   1.107 -        done
   1.108 +        by auto
   1.109        with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp
   1.110        from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
   1.111          by auto
   1.112 @@ -750,7 +731,7 @@
   1.113              from poly_bound_exists[of 1 ds] obtain m where
   1.114                m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
   1.115              have dm: "cmod d / m > 0" using d0 m(1) by (simp add: field_simps)
   1.116 -            from real_down2[OF dm zero_less_one] obtain x where
   1.117 +            from real_lbound_gt_zero[OF dm zero_less_one] obtain x where
   1.118                x: "x > 0" "x < cmod d / m" "x < 1" by blast
   1.119              let ?x = "complex_of_real x"
   1.120              from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
   1.121 @@ -810,9 +791,9 @@
   1.122              by (cases s) (auto split: if_splits)
   1.123            from sne kpn have k: "k \<noteq> 0" by simp
   1.124            let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
   1.125 -          from k oop [of a] have "q ^ n = p * ?w"
   1.126 -            apply -
   1.127 +          have "q ^ n = p * ?w"
   1.128              apply (subst r, subst s, subst kpn)
   1.129 +            using k oop [of a] 
   1.130              apply (subst power_mult_distrib, simp)
   1.131              apply (subst power_add [symmetric], simp)
   1.132              done
   1.133 @@ -925,9 +906,7 @@
   1.134  
   1.135  lemma divides_degree: assumes pq: "p dvd (q:: complex poly)"
   1.136    shows "degree p \<le> degree q \<or> q = 0"
   1.137 -apply (cases "q = 0", simp_all)
   1.138 -apply (erule dvd_imp_degree_le [OF pq])
   1.139 -done
   1.140 +by (metis dvd_imp_degree_le pq)
   1.141  
   1.142  (* Arithmetic operations on multivariate polynomials.                        *)
   1.143  
   1.144 @@ -946,8 +925,6 @@
   1.145  lemma poly_cancel_eq_conv: "p = (0::complex) \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (q = 0) \<equiv> (a * q - b * p = 0)" apply (atomize (full)) by auto
   1.146  
   1.147  lemma resolve_eq_raw:  "poly 0 x \<equiv> 0" "poly [:c:] x \<equiv> (c::complex)" by auto
   1.148 -lemma  resolve_eq_then: "(P \<Longrightarrow> (Q \<equiv> Q1)) \<Longrightarrow> (\<not>P \<Longrightarrow> (Q \<equiv> Q2))
   1.149 -  \<Longrightarrow> Q \<equiv> P \<and> Q1 \<or> \<not>P\<and> Q2" apply (atomize (full)) by blast
   1.150  
   1.151  lemma poly_divides_pad_rule:
   1.152    fixes p q :: "complex poly"
   1.153 @@ -1014,15 +991,15 @@
   1.154  qed
   1.155  
   1.156  lemma basic_cqe_conv1:
   1.157 -  "(\<exists>x. poly p x = 0 \<and> poly 0 x \<noteq> 0) \<equiv> False"
   1.158 -  "(\<exists>x. poly 0 x \<noteq> 0) \<equiv> False"
   1.159 -  "(\<exists>x. poly [:c:] x \<noteq> 0) \<equiv> c\<noteq>0"
   1.160 -  "(\<exists>x. poly 0 x = 0) \<equiv> True"
   1.161 -  "(\<exists>x. poly [:c:] x = 0) \<equiv> c = 0" by simp_all
   1.162 +  "(\<exists>x. poly p x = 0 \<and> poly 0 x \<noteq> 0) \<longleftrightarrow> False"
   1.163 +  "(\<exists>x. poly 0 x \<noteq> 0) \<longleftrightarrow> False"
   1.164 +  "(\<exists>x. poly [:c:] x \<noteq> 0) \<longleftrightarrow> c\<noteq>0"
   1.165 +  "(\<exists>x. poly 0 x = 0) \<longleftrightarrow> True"
   1.166 +  "(\<exists>x. poly [:c:] x = 0) \<longleftrightarrow> c = 0" by simp_all
   1.167  
   1.168  lemma basic_cqe_conv2:
   1.169    assumes l:"p \<noteq> 0"
   1.170 -  shows "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True"
   1.171 +  shows "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex))"
   1.172  proof-
   1.173    {fix h t
   1.174      assume h: "h\<noteq>0" "t=0"  "pCons a (pCons b p) = pCons h t"
   1.175 @@ -1030,58 +1007,35 @@
   1.176    hence th: "\<not> (\<exists> h t. h\<noteq>0 \<and> t=0 \<and> pCons a (pCons b p) = pCons h t)"
   1.177      by blast
   1.178    from fundamental_theorem_of_algebra_alt[OF th]
   1.179 -  show "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True" by auto
   1.180 +  show ?thesis by auto
   1.181  qed
   1.182  
   1.183 -lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> (p \<noteq> 0)"
   1.184 -proof-
   1.185 -  have "p = 0 \<longleftrightarrow> poly p = poly 0"
   1.186 -    by (simp add: poly_eq_poly_eq_iff)
   1.187 -  also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by auto
   1.188 -  finally show "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> p \<noteq> 0"
   1.189 -    by - (atomize (full), blast)
   1.190 -qed
   1.191 +lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<longleftrightarrow> (p \<noteq> 0)"
   1.192 +by (metis poly_all_0_iff_0)
   1.193  
   1.194  lemma basic_cqe_conv3:
   1.195    fixes p q :: "complex poly"
   1.196    assumes l: "p \<noteq> 0"
   1.197 -  shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
   1.198 -proof-
   1.199 +  shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<longleftrightarrow> \<not> ((pCons a p) dvd (q ^ (psize p)))"
   1.200 +proof -
   1.201    from l have dp:"degree (pCons a p) = psize p" by (simp add: psize_def)
   1.202    from nullstellensatz_univariate[of "pCons a p" q] l
   1.203 -  show "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
   1.204 -    unfolding dp
   1.205 -    by - (atomize (full), auto)
   1.206 +  show ?thesis
   1.207 +    by (metis dp pCons_eq_0_iff)
   1.208  qed
   1.209  
   1.210  lemma basic_cqe_conv4:
   1.211    fixes p q :: "complex poly"
   1.212 -  assumes h: "\<And>x. poly (q ^ n) x \<equiv> poly r x"
   1.213 -  shows "p dvd (q ^ n) \<equiv> p dvd r"
   1.214 +  assumes h: "\<And>x. poly (q ^ n) x = poly r x"
   1.215 +  shows "p dvd (q ^ n) \<longleftrightarrow> p dvd r"
   1.216  proof-
   1.217    from h have "poly (q ^ n) = poly r" by auto
   1.218    then have "(q ^ n) = r" by (simp add: poly_eq_poly_eq_iff)
   1.219 -  thus "p dvd (q ^ n) \<equiv> p dvd r" by simp
   1.220 +  thus "p dvd (q ^ n) \<longleftrightarrow> p dvd r" by simp
   1.221  qed
   1.222  
   1.223 -lemma pmult_Cons_Cons: "(pCons (a::complex) (pCons b p) * q = (smult a q) + (pCons 0 (pCons b p * q)))"
   1.224 -  by simp
   1.225 -
   1.226 -lemma elim_neg_conv: "- z \<equiv> (-1) * (z::complex)" by simp
   1.227 -lemma eqT_intr: "PROP P \<Longrightarrow> (True \<Longrightarrow> PROP P )" "PROP P \<Longrightarrow> True" by blast+
   1.228 -lemma negate_negate_rule: "Trueprop P \<equiv> (\<not> P \<equiv> False)" by (atomize (full), auto)
   1.229 -
   1.230  lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
   1.231 -lemma resolve_eq_ne: "(P \<equiv> True) \<equiv> (\<not>P \<equiv> False)" "(P \<equiv> False) \<equiv> (\<not>P \<equiv> True)"
   1.232 -  by (atomize (full)) simp_all
   1.233 -lemma cqe_conv1: "poly 0 x = 0 \<longleftrightarrow> True"  by simp
   1.234 -lemma cqe_conv2: "(p \<Longrightarrow> (q \<equiv> r)) \<equiv> ((p \<and> q) \<equiv> (p \<and> r))"  (is "?l \<equiv> ?r")
   1.235 -proof
   1.236 -  assume "p \<Longrightarrow> q \<equiv> r" thus "p \<and> q \<equiv> p \<and> r" apply - apply (atomize (full)) by blast
   1.237 -next
   1.238 -  assume "p \<and> q \<equiv> p \<and> r" "p"
   1.239 -  thus "q \<equiv> r" apply - apply (atomize (full)) apply blast done
   1.240 -qed
   1.241 +
   1.242  lemma poly_const_conv: "poly [:c:] (x::complex) = y \<longleftrightarrow> c = y" by simp
   1.243  
   1.244  end