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.5  text{* Offsetting the variable in a polynomial gives another of same degree *}
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.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.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.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