Cleaned up some messy proofs
authorpaulson <lp15@cam.ac.uk>
Thu Apr 03 17:26:04 2014 +0100 (2014-04-03)
changeset 563838e7052e9fda4
parent 56381 0556204bc230
child 56384 5fdcfffcc72e
Cleaned up some messy proofs
src/HOL/Library/Poly_Deriv.thy
src/HOL/Library/Polynomial.thy
     1.1 --- a/src/HOL/Library/Poly_Deriv.thy	Thu Apr 03 17:56:08 2014 +0200
     1.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Thu Apr 03 17:26:04 2014 +0100
     1.3 @@ -28,9 +28,8 @@
     1.4    by (simp add: pderiv.simps)
     1.5  
     1.6  lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
     1.7 -  apply (induct p arbitrary: n, simp)
     1.8 -  apply (simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
     1.9 -  done
    1.10 +  by (induct p arbitrary: n) 
    1.11 +     (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
    1.12  
    1.13  primrec pderiv_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list"
    1.14  where
    1.15 @@ -54,8 +53,7 @@
    1.16    apply (cases "degree p", simp)
    1.17    apply (rule le_degree)
    1.18    apply (simp add: coeff_pderiv del: of_nat_Suc)
    1.19 -  apply (rule subst, assumption)
    1.20 -  apply (rule leading_coeff_neq_0, clarsimp)
    1.21 +  apply (metis degree_0 leading_coeff_0_iff nat.distinct(1))
    1.22    done
    1.23  
    1.24  lemma pderiv_singleton [simp]: "pderiv [:a:] = 0"
    1.25 @@ -74,10 +72,7 @@
    1.26  by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
    1.27  
    1.28  lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p"
    1.29 -apply (induct p)
    1.30 -apply simp
    1.31 -apply (simp add: pderiv_add pderiv_smult pderiv_pCons algebra_simps)
    1.32 -done
    1.33 +by (induct p) (auto simp: pderiv_add pderiv_smult pderiv_pCons algebra_simps)
    1.34  
    1.35  lemma pderiv_power_Suc:
    1.36    "pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p"
    1.37 @@ -87,13 +82,9 @@
    1.38  apply (subst pderiv_mult)
    1.39  apply (erule ssubst)
    1.40  apply (simp only: of_nat_Suc smult_add_left smult_1_left)
    1.41 -apply (simp add: algebra_simps) (* FIXME *)
    1.42 +apply (simp add: algebra_simps)
    1.43  done
    1.44  
    1.45 -
    1.46 -lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"
    1.47 -by (simp add: DERIV_cmult mult_commute [of _ c])
    1.48 -
    1.49  lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
    1.50  by (rule DERIV_cong, rule DERIV_pow, simp)
    1.51  declare DERIV_pow2 [simp] DERIV_pow [simp]
    1.52 @@ -116,9 +107,8 @@
    1.53  
    1.54  lemma poly_IVT_pos: "[| a < b; poly p (a::real) < 0; 0 < poly p b |]
    1.55        ==> \<exists>x. a < x & x < b & (poly p x = 0)"
    1.56 -apply (cut_tac f = "%x. poly p x" and a = a and b = b and y = 0 in IVT_objl)
    1.57 -apply (auto simp add: order_le_less)
    1.58 -done
    1.59 +using IVT_objl [of "poly p" a 0 b]
    1.60 +by (auto simp add: order_le_less)
    1.61  
    1.62  lemma poly_IVT_neg: "[| (a::real) < b; 0 < poly p a; poly p b < 0 |]
    1.63        ==> \<exists>x. a < x & x < b & (poly p x = 0)"
    1.64 @@ -126,7 +116,8 @@
    1.65  
    1.66  lemma poly_MVT: "(a::real) < b ==>
    1.67       \<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
    1.68 -apply (drule_tac f = "poly p" in MVT, auto)
    1.69 +using MVT [of a b "poly p"]
    1.70 +apply auto
    1.71  apply (rule_tac x = z in exI)
    1.72  apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
    1.73  done
    1.74 @@ -135,16 +126,12 @@
    1.75  
    1.76  lemma order_unique_lemma:
    1.77    fixes p :: "'a::idom poly"
    1.78 -  assumes "[:-a, 1:] ^ n dvd p \<and> \<not> [:-a, 1:] ^ Suc n dvd p"
    1.79 +  assumes "[:-a, 1:] ^ n dvd p" "\<not> [:-a, 1:] ^ Suc n dvd p"
    1.80    shows "n = order a p"
    1.81  unfolding Polynomial.order_def
    1.82  apply (rule Least_equality [symmetric])
    1.83 -apply (rule assms [THEN conjunct2])
    1.84 -apply (erule contrapos_np)
    1.85 -apply (rule power_le_dvd)
    1.86 -apply (rule assms [THEN conjunct1])
    1.87 -apply simp
    1.88 -done
    1.89 +apply (rule assms)
    1.90 +by (metis assms not_less_eq_eq power_le_dvd)
    1.91  
    1.92  lemma lemma_order_pderiv1:
    1.93    "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
    1.94 @@ -158,45 +145,43 @@
    1.95    shows "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c"
    1.96    by (drule (1) Rings.dvd_diff, simp)
    1.97  
    1.98 -lemma lemma_order_pderiv [rule_format]:
    1.99 -     "\<forall>p q a. 0 < n &
   1.100 -       pderiv p \<noteq> 0 &
   1.101 -       p = [:- a, 1:] ^ n * q & ~ [:- a, 1:] dvd q
   1.102 -       --> n = Suc (order a (pderiv p))"
   1.103 - apply (cases "n", safe, rename_tac n p q a)
   1.104 - apply (rule order_unique_lemma)
   1.105 - apply (rule conjI)
   1.106 -  apply (subst lemma_order_pderiv1)
   1.107 -  apply (rule dvd_add)
   1.108 -   apply (rule dvd_mult2)
   1.109 -   apply (rule le_imp_power_dvd, simp)
   1.110 -  apply (rule dvd_smult)
   1.111 -  apply (rule dvd_mult)
   1.112 -  apply (rule dvd_refl)
   1.113 - apply (subst lemma_order_pderiv1)
   1.114 - apply (erule contrapos_nn) back
   1.115 - apply (subgoal_tac "[:- a, 1:] ^ Suc n dvd q * [:- a, 1:] ^ n")
   1.116 -  apply (simp del: mult_pCons_left)
   1.117 - apply (drule dvd_add_cancel1)
   1.118 -  apply (simp del: mult_pCons_left)
   1.119 - apply (drule dvd_smult_cancel, simp del: of_nat_Suc)
   1.120 - apply assumption
   1.121 -done
   1.122 +lemma lemma_order_pderiv:
   1.123 +  assumes n: "0 < n" 
   1.124 +      and pd: "pderiv p \<noteq> 0" 
   1.125 +      and pe: "p = [:- a, 1:] ^ n * q" 
   1.126 +      and nd: "~ [:- a, 1:] dvd q"
   1.127 +    shows "n = Suc (order a (pderiv p))"
   1.128 +using n 
   1.129 +proof -
   1.130 +  have "pderiv ([:- a, 1:] ^ n * q) \<noteq> 0"
   1.131 +    using assms by auto
   1.132 +  obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \<noteq> 0"
   1.133 +    using assms by (cases n) auto
   1.134 +  then have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l"
   1.135 +    by (metis dvd_add_cancel1 dvd_smult_iff dvd_triv_left of_nat_eq_0_iff old.nat.distinct(2))
   1.136 +  have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))" 
   1.137 +  proof (rule order_unique_lemma)
   1.138 +    show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
   1.139 +      apply (subst lemma_order_pderiv1)
   1.140 +      apply (rule dvd_add)
   1.141 +      apply (metis dvdI dvd_mult2 power_Suc2)
   1.142 +      apply (metis dvd_smult dvd_triv_right)
   1.143 +      done
   1.144 +  next
   1.145 +    show "\<not> [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
   1.146 +     apply (subst lemma_order_pderiv1)
   1.147 +     by (metis * nd dvd_mult_cancel_right field_power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
   1.148 +  qed
   1.149 +  then show ?thesis
   1.150 +    by (metis `n = Suc n'` pe)
   1.151 +qed
   1.152  
   1.153  lemma order_decomp:
   1.154       "p \<noteq> 0
   1.155        ==> \<exists>q. p = [:-a, 1:] ^ (order a p) * q &
   1.156                  ~([:-a, 1:] dvd q)"
   1.157  apply (drule order [where a=a])
   1.158 -apply (erule conjE)
   1.159 -apply (erule dvdE)
   1.160 -apply (rule exI)
   1.161 -apply (rule conjI, assumption)
   1.162 -apply (erule contrapos_nn)
   1.163 -apply (erule ssubst) back
   1.164 -apply (subst power_Suc2)
   1.165 -apply (erule mult_dvd_mono [OF dvd_refl])
   1.166 -done
   1.167 +by (metis dvdE dvd_mult_cancel_left power_Suc2)
   1.168  
   1.169  lemma order_pderiv: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
   1.170        ==> (order a p = Suc (order a (pderiv p)))"
   1.171 @@ -219,9 +204,9 @@
   1.172      apply (drule order [where a=a and p=p, folded i_def t_def])
   1.173      apply (drule order [where a=a and p=q, folded j_def t_def])
   1.174      apply clarify
   1.175 +    apply (erule dvdE)+
   1.176      apply (rule order_unique_lemma [symmetric], fold t_def)
   1.177 -    apply (erule dvdE)+
   1.178 -    apply (simp add: power_add t_dvd_iff)
   1.179 +    apply (simp_all add: power_add t_dvd_iff)
   1.180      done
   1.181  qed
   1.182  
   1.183 @@ -230,9 +215,7 @@
   1.184  lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
   1.185  apply (cases "p = 0", auto)
   1.186  apply (drule order_2 [where a=a and p=p])
   1.187 -apply (erule contrapos_np)
   1.188 -apply (erule power_le_dvd)
   1.189 -apply simp
   1.190 +apply (metis not_less_eq_eq power_le_dvd)
   1.191  apply (erule power_le_dvd [OF order_1])
   1.192  done
   1.193  
   1.194 @@ -277,13 +260,11 @@
   1.195           pderiv p = e * d;
   1.196           d = r * p + s * pderiv p
   1.197        |] ==> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
   1.198 -apply (blast intro: poly_squarefree_decomp_order)
   1.199 -done
   1.200 +by (blast intro: poly_squarefree_decomp_order)
   1.201  
   1.202  lemma order_pderiv2: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
   1.203        ==> (order a (pderiv p) = n) = (order a p = Suc n)"
   1.204 -apply (auto dest: order_pderiv)
   1.205 -done
   1.206 +by (auto dest: order_pderiv)
   1.207  
   1.208  definition
   1.209    rsquarefree :: "'a::idom poly => bool" where
   1.210 @@ -300,13 +281,9 @@
   1.211  apply (case_tac "p = 0", simp, simp)
   1.212  apply (case_tac "pderiv p = 0")
   1.213  apply simp
   1.214 -apply (drule pderiv_iszero, clarify)
   1.215 -apply simp
   1.216 -apply (rule allI)
   1.217 -apply (cut_tac p = "[:h:]" and a = a in order_root)
   1.218 -apply simp
   1.219 -apply (auto simp add: order_root order_pderiv2)
   1.220 -apply (erule_tac x="a" in allE, simp)
   1.221 +apply (drule pderiv_iszero, clarsimp)
   1.222 +apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree)
   1.223 +apply (force simp add: order_root order_pderiv2)
   1.224  done
   1.225  
   1.226  lemma poly_squarefree_decomp:
     2.1 --- a/src/HOL/Library/Polynomial.thy	Thu Apr 03 17:56:08 2014 +0200
     2.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Apr 03 17:26:04 2014 +0100
     2.3 @@ -1747,12 +1747,9 @@
     2.4  lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
     2.5  apply (cases "p = 0", simp_all)
     2.6  apply (rule iffI)
     2.7 -apply (rule ccontr, simp)
     2.8 -apply (frule order_2 [where a=a], simp)
     2.9 -apply (simp add: poly_eq_0_iff_dvd)
    2.10 -apply (simp add: poly_eq_0_iff_dvd)
    2.11 -apply (simp only: order_def)
    2.12 -apply (drule not_less_Least, simp)
    2.13 +apply (metis order_2 not_gr0 poly_eq_0_iff_dvd power_0 power_Suc_0 power_one_right)
    2.14 +unfolding poly_eq_0_iff_dvd
    2.15 +apply (metis dvd_power dvd_trans order_1)
    2.16  done
    2.17  
    2.18