# HG changeset patch # User haftmann # Date 1272033531 -7200 # Node ID ed3a87a7f9773030f3be734f16e594c1f57c9468 # Parent e3d3b14b13cd955eb0c2b136218693555d9dea82 epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance diff -r e3d3b14b13cd -r ed3a87a7f977 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Fri Apr 23 16:17:25 2010 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Fri Apr 23 16:38:51 2010 +0200 @@ -388,6 +388,8 @@ then show "a*b \ 0" unfolding fps_nonzero_nth by blast qed +instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. + instance fps :: (idom) idom .. instantiation fps :: (comm_ring_1) number_ring @@ -586,7 +588,7 @@ from k have "real k > - log y x" by simp then have "ln y * real k > - ln x" unfolding log_def using ln_gt_zero_iff[OF yp] y1 - by (simp add: minus_divide_left field_eq_simps del:minus_divide_left[symmetric] ) + by (simp add: minus_divide_left field_simps field_eq_simps del:minus_divide_left[symmetric]) then have "ln y * real k + ln x > 0" by simp then have "exp (real k * ln y + ln x) > exp 0" by (simp add: mult_ac) @@ -594,7 +596,7 @@ unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln[OF xp] exp_ln[OF yp] by simp then have "x > (1/y)^k" using yp - by (simp add: field_eq_simps nonzero_power_divide ) + by (simp add: field_simps field_eq_simps nonzero_power_divide) then show ?thesis using kp by blast qed lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" by (simp add: X_def) @@ -649,8 +651,7 @@ declare setsum_cong[fundef_cong] - -instantiation fps :: ("{comm_monoid_add,inverse, times, uminus}") inverse +instantiation fps :: ("{comm_monoid_add, inverse, times, uminus}") inverse begin fun natfun_inverse:: "'a fps \ nat \ 'a" where @@ -658,9 +659,12 @@ | "natfun_inverse f n = - inverse (f$0) * setsum (\i. f$i * natfun_inverse f (n - i)) {1..n}" definition fps_inverse_def: - "inverse f = (if f$0 = 0 then 0 else Abs_fps (natfun_inverse f))" + "inverse f = (if f $ 0 = 0 then 0 else Abs_fps (natfun_inverse f))" + definition fps_divide_def: "divide = (\(f::'a fps) g. f * inverse g)" + instance .. + end lemma fps_inverse_zero[simp]: @@ -671,10 +675,7 @@ apply (auto simp add: expand_fps_eq fps_inverse_def) by (case_tac n, auto) -instance fps :: ("{comm_monoid_add,inverse, times, uminus}") division_by_zero - by default (rule fps_inverse_zero) - -lemma inverse_mult_eq_1[intro]: assumes f0: "f$0 \ (0::'a::field)" +lemma inverse_mult_eq_1 [intro]: assumes f0: "f$0 \ (0::'a::field)" shows "inverse f * f = 1" proof- have c: "inverse f * f = f * inverse f" by (simp add: mult_commute) @@ -1687,7 +1688,7 @@ then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k" by (simp add: natpermute_max_card[OF nz, simplified]) also have "\ = a$n - setsum ?f ?Pnknn" - unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc ) + unfolding n1 using r00 a0 by (simp add: field_eq_simps fps_radical_def del: of_nat_Suc) finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" . have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] .. @@ -1763,7 +1764,7 @@ shows "a = b / c" proof- from eq have "a * c * inverse c = b * inverse c" by simp - hence "a * (inverse c * c) = b/c" by (simp only: field_simps divide_inverse) + hence "a * (inverse c * c) = b/c" by (simp only: field_eq_simps divide_inverse) then show "a = b/c" unfolding field_inverse[OF c0] by simp qed @@ -1836,7 +1837,7 @@ show "a$(xs !i) = ?r$(xs!i)" . qed have th00: "\(x::'a). of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x" - by (simp add: field_simps del: of_nat_Suc) + by (simp add: field_eq_simps del: of_nat_Suc) from H have "b$n = a^Suc k $ n" by (simp add: fps_eq_iff) also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn" unfolding fps_power_nth_Suc @@ -1853,7 +1854,7 @@ then have "a$n = ?r $n" apply (simp del: of_nat_Suc) unfolding fps_radical_def n1 - by (simp add: field_simps n1 th00 del: of_nat_Suc)} + by (simp add: field_eq_simps n1 th00 del: of_nat_Suc)} ultimately show "a$n = ?r $ n" by (cases n, auto) qed} then have "a = ?r" by (simp add: fps_eq_iff)} @@ -2468,7 +2469,7 @@ proof- let ?r = "fps_inv" have ra0: "?r a $ 0 = 0" by (simp add: fps_inv_def) - from a1 have ra1: "?r a $ 1 \ 0" by (simp add: fps_inv_def field_simps) + from a1 have ra1: "?r a $ 1 \ 0" by (simp add: fps_inv_def field_eq_simps) have X0: "X$0 = 0" by simp from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" . then have "?r (?r a) oo ?r a oo a = X oo a" by simp @@ -2485,7 +2486,7 @@ proof- let ?r = "fps_ginv" from c0 have rca0: "?r c a $0 = 0" by (simp add: fps_ginv_def) - from a1 c1 have rca1: "?r c a $ 1 \ 0" by (simp add: fps_ginv_def field_simps) + from a1 c1 have rca1: "?r c a $ 1 \ 0" by (simp add: fps_ginv_def field_eq_simps) from fps_ginv[OF rca0 rca1] have "?r b (?r c a) oo ?r c a = b" . then have "?r b (?r c a) oo ?r c a oo a = b oo a" by simp @@ -2533,7 +2534,7 @@ proof- {fix n have "?l$n = ?r $ n" - apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc) + apply (auto simp add: E_def field_eq_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc) by (simp add: of_nat_mult ring_simps)} then show ?thesis by (simp add: fps_eq_iff) qed @@ -2544,13 +2545,13 @@ proof- {assume d: ?lhs from d have th: "\n. a $ Suc n = c * a$n / of_nat (Suc n)" - by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc) + by (simp add: fps_deriv_def fps_eq_iff field_eq_simps del: of_nat_Suc) {fix n have "a$n = a$0 * c ^ n/ (of_nat (fact n))" apply (induct n) apply simp unfolding th using fact_gt_zero_nat - apply (simp add: field_simps del: of_nat_Suc fact_Suc) + apply (simp add: field_eq_simps del: of_nat_Suc fact_Suc) apply (drule sym) by (simp add: ring_simps of_nat_mult power_Suc)} note th' = this @@ -2653,13 +2654,13 @@ from E_add_mult[of a b] have "(E (a + b)) $ n = (E a * E b)$n" by simp then have "(a + b) ^ n = (\i\nat = 0\nat..n. a ^ i * b ^ (n - i) * (of_nat (fact n) / of_nat (fact i * fact (n - i))))" - by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib) + by (simp add: field_eq_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib) then show ?thesis apply simp apply (rule setsum_cong2) apply simp apply (frule binomial_fact[where ?'a = 'a, symmetric]) - by (simp add: field_simps of_nat_mult) + by (simp add: field_eq_simps of_nat_mult) qed text{* And the nat-form -- also available from Binomial.thy *} @@ -2682,7 +2683,7 @@ by (simp add: L_def fps_eq_iff del: of_nat_Suc) lemma L_nth: "L c $ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))" - by (simp add: L_def field_simps) + by (simp add: L_def field_eq_simps) lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def) lemma L_E_inv: @@ -2712,7 +2713,7 @@ shows "L c + L d = fps_const (c+d) * L (c*d)" (is "?r = ?l") proof- - from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps) + from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_eq_simps) have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)" by (simp add: fps_deriv_L fps_const_add[symmetric] algebra_simps del: fps_const_add) also have "\ = fps_deriv ?l" @@ -2752,7 +2753,7 @@ from lrn have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" apply (simp add: ring_simps del: of_nat_Suc) - by (cases n, simp_all add: field_simps del: of_nat_Suc) + by (cases n, simp_all add: field_eq_simps del: of_nat_Suc) } note th0 = this {fix n have "a$n = (c gchoose n) * a$0" @@ -2761,7 +2762,7 @@ next case (Suc m) thus ?case unfolding th0 - apply (simp add: field_simps del: of_nat_Suc) + apply (simp add: field_eq_simps del: of_nat_Suc) unfolding mult_assoc[symmetric] gbinomial_mult_1 by (simp add: ring_simps) qed} @@ -2879,7 +2880,7 @@ using kn pochhammer_minus'[where k=k and n=n and b=b] apply (simp add: pochhammer_same) using bn0 - by (simp add: field_simps power_add[symmetric])} + by (simp add: field_eq_simps power_add[symmetric])} moreover {assume nk: "k \ n" have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" @@ -2904,7 +2905,7 @@ unfolding m1nk unfolding m h pochhammer_Suc_setprod - apply (simp add: field_simps del: fact_Suc id_def) + apply (simp add: field_eq_simps del: fact_Suc id_def) unfolding fact_altdef_nat id_def unfolding of_nat_setprod unfolding setprod_timesf[symmetric] @@ -2941,10 +2942,10 @@ apply auto done then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {0.. n - k - 1}" - using nz' by (simp add: field_simps) + using nz' by (simp add: field_eq_simps) have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) = ((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)" using bnz0 - by (simp add: field_simps) + by (simp add: field_eq_simps) also have "\ = b gchoose (n - k)" unfolding th1 th2 using kn' by (simp add: gbinomial_def) @@ -2958,15 +2959,15 @@ note th00 = this have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))" unfolding gbinomial_pochhammer - using bn0 by (auto simp add: field_simps) + using bn0 by (auto simp add: field_eq_simps) also have "\ = ?l" unfolding gbinomial_Vandermonde[symmetric] apply (simp add: th00) unfolding gbinomial_pochhammer - using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_simps) + using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_eq_simps) apply (rule setsum_cong2) apply (drule th00(2)) - by (simp add: field_simps power_add[symmetric]) + by (simp add: field_eq_simps power_add[symmetric]) finally show ?thesis by simp qed @@ -2991,7 +2992,7 @@ have nz: "pochhammer c n \ 0" using c by (simp add: pochhammer_eq_0_iff) from Vandermonde_pochhammer_lemma[where a = "?a" and b="?b" and n=n, OF h, unfolded th0 th1] - show ?thesis using nz by (simp add: field_simps setsum_right_distrib) + show ?thesis using nz by (simp add: field_eq_simps setsum_right_distrib) qed subsubsection{* Formal trigonometric functions *} @@ -3013,9 +3014,9 @@ using en by (simp add: fps_sin_def) also have "\ = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))" unfolding fact_Suc of_nat_mult - by (simp add: field_simps del: of_nat_add of_nat_Suc) + by (simp add: field_eq_simps del: of_nat_add of_nat_Suc) also have "\ = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)" - by (simp add: field_simps del: of_nat_add of_nat_Suc) + by (simp add: field_eq_simps del: of_nat_add of_nat_Suc) finally have "?lhs $n = ?rhs$n" using en by (simp add: fps_cos_def ring_simps power_Suc )} then show "?lhs $ n = ?rhs $ n" @@ -3037,9 +3038,9 @@ using en by (simp add: fps_cos_def) also have "\ = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))" unfolding fact_Suc of_nat_mult - by (simp add: field_simps del: of_nat_add of_nat_Suc) + by (simp add: field_eq_simps del: of_nat_add of_nat_Suc) also have "\ = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)" - by (simp add: field_simps del: of_nat_add of_nat_Suc) + by (simp add: field_eq_simps del: of_nat_add of_nat_Suc) also have "\ = (- ((- 1)^((n - 1) div 2))) * c^Suc n / of_nat (fact n)" unfolding th0 unfolding th1[OF en] by simp finally have "?lhs $n = ?rhs$n" using en @@ -3345,6 +3346,6 @@ shows "foldr (%c r. f c o r) cs (%c. g c a) c0 $ n = foldr (%c r. (k c + of_nat n) * r) cs (g c0 a $ n)" - by (induct cs arbitrary: c0, auto simp add: algebra_simps f ) + by (induct cs arbitrary: c0, auto simp add: algebra_simps f) end