src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 52380 3cc46b8cca5e
parent 51541 e7b6b61b7be2
child 53077 a1b3784f8129
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jun 15 17:19:23 2013 +0200
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jun 15 17:19:23 2013 +0200
     1.3 @@ -93,16 +93,17 @@
     1.4  
     1.5  text{* Offsetting the variable in a polynomial gives another of same degree *}
     1.6  
     1.7 -definition
     1.8 -  "offset_poly p h = poly_rec 0 (\<lambda>a p q. smult h q + pCons a q) p"
     1.9 +definition offset_poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
    1.10 +where
    1.11 +  "offset_poly p h = fold_coeffs (\<lambda>a q. smult h q + pCons a q) p 0"
    1.12  
    1.13  lemma offset_poly_0: "offset_poly 0 h = 0"
    1.14 -  unfolding offset_poly_def by (simp add: poly_rec_0)
    1.15 +  by (simp add: offset_poly_def)
    1.16  
    1.17  lemma offset_poly_pCons:
    1.18    "offset_poly (pCons a p) h =
    1.19      smult h (offset_poly p h) + pCons a (offset_poly p h)"
    1.20 -  unfolding offset_poly_def by (simp add: poly_rec_pCons)
    1.21 +  by (cases "p = 0 \<and> a = 0") (auto simp add: offset_poly_def)
    1.22  
    1.23  lemma offset_poly_single: "offset_poly [:a:] h = [:a:]"
    1.24  by (simp add: offset_poly_pCons offset_poly_0)
    1.25 @@ -644,7 +645,7 @@
    1.26      let ?r = "smult (inverse ?a0) q"
    1.27      have lgqr: "psize q = psize ?r"
    1.28        using a00 unfolding psize_def degree_def
    1.29 -      by (simp add: expand_poly_eq)
    1.30 +      by (simp add: poly_eq_iff)
    1.31      {assume h: "\<And>x y. poly ?r x = poly ?r y"
    1.32        {fix x y
    1.33          from qr[rule_format, of x]
    1.34 @@ -887,9 +888,7 @@
    1.35  proof-
    1.36    {assume pe: "p = 0"
    1.37      hence eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
    1.38 -      apply auto
    1.39 -      apply (rule poly_zero [THEN iffD1])
    1.40 -      by (rule ext, simp)
    1.41 +      by (auto simp add: poly_all_0_iff_0)
    1.42      {assume "p dvd (q ^ (degree p))"
    1.43        then obtain r where r: "q ^ (degree p) = p * r" ..
    1.44        from r pe have False by simp}
    1.45 @@ -927,7 +926,7 @@
    1.46    assume l: ?lhs
    1.47    from l[unfolded constant_def, rule_format, of _ "0"]
    1.48    have th: "poly p = poly [:poly p 0:]" apply - by (rule ext, simp)
    1.49 -  then have "p = [:poly p 0:]" by (simp add: poly_eq_iff)
    1.50 +  then have "p = [:poly p 0:]" by (simp add: poly_eq_poly_eq_iff)
    1.51    then have "degree p = degree [:poly p 0:]" by simp
    1.52    then show ?rhs by simp
    1.53  next
    1.54 @@ -1050,7 +1049,7 @@
    1.55  lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> (p \<noteq> 0)"
    1.56  proof-
    1.57    have "p = 0 \<longleftrightarrow> poly p = poly 0"
    1.58 -    by (simp add: poly_zero)
    1.59 +    by (simp add: poly_eq_poly_eq_iff)
    1.60    also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by auto
    1.61    finally show "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> p \<noteq> 0"
    1.62      by - (atomize (full), blast)
    1.63 @@ -1074,7 +1073,7 @@
    1.64    shows "p dvd (q ^ n) \<equiv> p dvd r"
    1.65  proof-
    1.66    from h have "poly (q ^ n) = poly r" by auto
    1.67 -  then have "(q ^ n) = r" by (simp add: poly_eq_iff)
    1.68 +  then have "(q ^ n) = r" by (simp add: poly_eq_poly_eq_iff)
    1.69    thus "p dvd (q ^ n) \<equiv> p dvd r" by simp
    1.70  qed
    1.71