\<^sub>N y) = INum x / (INum y ::'a :: {ring_char_0, division_by_zero,field})" by (simp add: Ndiv_def) +lemma Ndiv[simp]: "INum (x \

\<^sub>N y) = INum x / (INum y ::'a :: {ring_char_0, division_ring_inverse_zero,field})" by (simp add: Ndiv_def) lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field})< 0) = 0>\<^sub>N x " + shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})< 0) = 0>\<^sub>N x " proof- have " \ a b. x = (a,b)" by simp then obtain a b where x[simp]:"x = (a,b)" by blast @@ -345,7 +345,7 @@ qed lemma Nle0_iff[simp]:assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) \ 0) = 0\\<^sub>N x" + shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \ 0) = 0\\<^sub>N x" proof- have " \ a b. x = (a,b)" by simp then obtain a b where x[simp]:"x = (a,b)" by blast @@ -357,7 +357,7 @@ ultimately show ?thesis by blast qed -lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field})> 0) = 0<\<^sub>N x" +lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})> 0) = 0<\<^sub>N x" proof- have " \ a b. x = (a,b)" by simp then obtain a b where x[simp]:"x = (a,b)" by blast @@ -369,7 +369,7 @@ ultimately show ?thesis by blast qed lemma Nge0_iff[simp]:assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) \ 0) = 0\\<^sub>N x" + shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \ 0) = 0\\<^sub>N x" proof- have " \ a b. x = (a,b)" by simp then obtain a b where x[simp]:"x = (a,b)" by blast @@ -382,7 +382,7 @@ qed lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" - shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) < INum y) = (x <\<^sub>N y)" + shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) < INum y) = (x <\<^sub>N y)" proof- let ?z = "0::'a" have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp @@ -391,7 +391,7 @@ qed lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" - shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field})\ INum y) = (x \\<^sub>N y)" + shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})\ INum y) = (x \\<^sub>N y)" proof- have "((INum x ::'a) \ INum y) = (INum (x -\<^sub>N y) \ (0::'a))" using nx ny by simp also have "\ = (0\\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp @@ -399,7 +399,7 @@ qed lemma Nadd_commute: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "x +\<^sub>N y = y +\<^sub>N x" proof- have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all @@ -408,7 +408,7 @@ qed lemma [simp]: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "(0, b) +\<^sub>N y = normNum y" and "(a, 0) +\<^sub>N y = normNum y" and "x +\<^sub>N (0, b) = normNum x" @@ -420,7 +420,7 @@ done lemma normNum_nilpotent_aux[simp]: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" assumes nx: "isnormNum x" shows "normNum x = x" proof- @@ -432,7 +432,7 @@ qed lemma normNum_nilpotent[simp]: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "normNum (normNum x) = normNum x" by simp @@ -440,11 +440,11 @@ by (simp_all add: normNum_def) lemma normNum_Nadd: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp lemma Nadd_normNum1[simp]: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "normNum x +\<^sub>N y = x +\<^sub>N y" proof- have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all @@ -454,7 +454,7 @@ qed lemma Nadd_normNum2[simp]: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "x +\<^sub>N normNum y = x +\<^sub>N y" proof- have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all @@ -464,7 +464,7 @@ qed lemma Nadd_assoc: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" proof- have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all @@ -476,7 +476,7 @@ by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute) lemma Nmul_assoc: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z" shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)" proof- @@ -487,7 +487,7 @@ qed lemma Nsub0: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)" proof- { fix h :: 'a @@ -502,7 +502,7 @@ by (simp_all add: Nmul_def Let_def split_def) lemma Nmul_eq0[simp]: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" assumes nx:"isnormNum x" and ny: "isnormNum y" shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \ y = 0\<^sub>N)" proof- diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Library/Binomial.thy --- a/src/HOL/Library/Binomial.thy Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Library/Binomial.thy Mon Apr 26 13:43:31 2010 +0200 @@ -236,10 +236,10 @@ have th1: "(\n\{1\nat..n}. a + of_nat n) = (\n\{0\nat..n - 1}. a + 1 + of_nat n)" apply (rule setprod_reindex_cong[where f = "Suc"]) - using n0 by (auto simp add: expand_fun_eq ring_simps) + using n0 by (auto simp add: expand_fun_eq field_simps) have ?thesis apply (simp add: pochhammer_def) unfolding setprod_insert[OF th0, unfolded eq] - using th1 by (simp add: ring_simps)} + using th1 by (simp add: field_simps)} ultimately show ?thesis by blast qed @@ -378,10 +378,10 @@ by simp from n h th0 have "fact k * fact (n - k) * (n choose k) = k * (fact h * fact (m - h) * (m choose h)) + (m - h) * (fact k * fact (m - k) * (m choose k))" - by (simp add: ring_simps) + by (simp add: field_simps) also have "\ = (k + (m - h)) * fact m" using H[rule_format, OF mn hm'] H[rule_format, OF mn km] - by (simp add: ring_simps) + by (simp add: field_simps) finally have ?ths using h n km by simp} moreover have "n=0 \ k = 0 \ k = n \ (EX m h. n=Suc m \ k = Suc h \ h < m)" using kn by presburger ultimately show ?ths by blast @@ -391,13 +391,13 @@ assumes kn: "k \ n" shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))" using binomial_fact_lemma[OF kn] - by (simp add: field_eq_simps of_nat_mult [symmetric]) + by (simp add: field_simps of_nat_mult [symmetric]) lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k" proof- {assume kn: "k > n" from kn binomial_eq_0[OF kn] have ?thesis - by (simp add: gbinomial_pochhammer field_eq_simps + by (simp add: gbinomial_pochhammer field_simps pochhammer_of_nat_eq_0_iff)} moreover {assume "k=0" then have ?thesis by simp} @@ -414,13 +414,13 @@ apply clarsimp apply (presburger) apply presburger - by (simp add: expand_fun_eq ring_simps of_nat_add[symmetric] del: of_nat_add) + by (simp add: expand_fun_eq field_simps of_nat_add[symmetric] del: of_nat_add) have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" "{1..n - Suc h} \ {n - h .. n} = {}" and eq3: "{1..n - Suc h} \ {n - h .. n} = {1..n}" using h kn by auto from eq[symmetric] have ?thesis using kn apply (simp add: binomial_fact[OF kn, where ?'a = 'a] - gbinomial_pochhammer field_eq_simps pochhammer_Suc_setprod) + gbinomial_pochhammer field_simps pochhammer_Suc_setprod) apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc) unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \ 'a"] eq[unfolded h] unfolding mult_assoc[symmetric] @@ -449,9 +449,9 @@ have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))" unfolding gbinomial_pochhammer pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc - by (simp add: field_eq_simps del: of_nat_Suc) + by (simp add: field_simps del: of_nat_Suc) also have "\ = ?l" unfolding gbinomial_pochhammer - by (simp add: ring_simps) + by (simp add: field_simps) finally show ?thesis .. qed @@ -482,17 +482,17 @@ have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\i\{0\nat..Suc h}. a - of_nat i)" unfolding h - apply (simp add: ring_simps del: fact_Suc) + apply (simp add: field_simps del: fact_Suc) unfolding gbinomial_mult_fact' apply (subst fact_Suc) unfolding of_nat_mult apply (subst mult_commute) unfolding mult_assoc unfolding gbinomial_mult_fact - by (simp add: ring_simps) + by (simp add: field_simps) also have "\ = (\i\{0..h}. a - of_nat i) * (a + 1)" unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc - by (simp add: ring_simps h) + by (simp add: field_simps h) also have "\ = (\i\{0..k}. (a + 1) - of_nat i)" using eq0 unfolding h setprod_nat_ivl_1_Suc diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Library/Bit.thy --- a/src/HOL/Library/Bit.thy Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Library/Bit.thy Mon Apr 26 13:43:31 2010 +0200 @@ -49,7 +49,7 @@ subsection {* Type @{typ bit} forms a field *} -instantiation bit :: "{field, division_by_zero}" +instantiation bit :: "{field, division_ring_inverse_zero}" begin definition plus_bit_def: diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Mon Apr 26 13:43:31 2010 +0200 @@ -588,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_simps field_eq_simps del:minus_divide_left[symmetric]) + by (simp add: minus_divide_left field_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) @@ -596,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_simps field_eq_simps nonzero_power_divide) + by (simp add: field_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) @@ -693,7 +693,7 @@ from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]] have th1: "setsum (\i. f$i * natfun_inverse f (n - i)) {1..n} = - (f$0) * (inverse f)$n" - by (simp add: ring_simps) + by (simp add: field_simps) have "(f * inverse f) $ n = (\i = 0..n. f $i * natfun_inverse f (n - i))" unfolding fps_mult_nth ifn .. also have "\ = f$0 * natfun_inverse f n @@ -766,7 +766,7 @@ lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n+1)" by (simp add: fps_deriv_def) lemma fps_deriv_linear[simp]: "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = fps_const a * fps_deriv f + fps_const b * fps_deriv g" - unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: ring_simps) + unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: field_simps) lemma fps_deriv_mult[simp]: fixes f :: "('a :: comm_ring_1) fps" @@ -817,7 +817,7 @@ unfolding s0 s1 unfolding setsum_addf[symmetric] setsum_right_distrib apply (rule setsum_cong2) - by (auto simp add: of_nat_diff ring_simps) + by (auto simp add: of_nat_diff field_simps) finally have "(f * ?D g + ?D f * g) $ n = ?D (f*g) $ n" .} then show ?thesis unfolding fps_eq_iff by auto qed @@ -878,7 +878,7 @@ proof- have "fps_deriv f = fps_deriv g \ fps_deriv (f - g) = 0" by simp also have "\ \ f - g = fps_const ((f-g)$0)" unfolding fps_deriv_eq_0_iff .. - finally show ?thesis by (simp add: ring_simps) + finally show ?thesis by (simp add: field_simps) qed lemma fps_deriv_eq_iff_ex: "(fps_deriv f = fps_deriv g) \ (\(c::'a::{idom,semiring_char_0}). f = fps_const c + g)" @@ -929,7 +929,7 @@ qed lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)" - by (induct k arbitrary: f) (auto simp add: ring_simps of_nat_mult) + by (induct k arbitrary: f) (auto simp add: field_simps of_nat_mult) subsection {* Powers*} @@ -943,7 +943,7 @@ case (Suc n) note h = Suc.hyps[OF `a$0 = 1`] show ?case unfolding power_Suc fps_mult_nth - using h `a$0 = 1` fps_power_zeroth_eq_one[OF `a$0=1`] by (simp add: ring_simps) + using h `a$0 = 1` fps_power_zeroth_eq_one[OF `a$0=1`] by (simp add: field_simps) qed lemma startsby_one_power:"a $ 0 = (1::'a::comm_ring_1) \ a^n $ 0 = 1" @@ -1005,7 +1005,7 @@ case 0 thus ?case by (simp add: power_0) next case (Suc n) - have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)" by (simp add: ring_simps power_Suc) + have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)" by (simp add: field_simps power_Suc) also have "\ = setsum (\i. a^n$i * a $ (Suc n - i)) {0.. Suc n}" by (simp add: fps_mult_nth) also have "\ = setsum (\i. a^n$i * a $ (Suc n - i)) {n .. Suc n}" apply (rule setsum_mono_zero_right) @@ -1045,8 +1045,8 @@ qed lemma fps_deriv_power: "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)" - apply (induct n, auto simp add: power_Suc ring_simps fps_const_add[symmetric] simp del: fps_const_add) - by (case_tac n, auto simp add: power_Suc ring_simps) + apply (induct n, auto simp add: power_Suc field_simps fps_const_add[symmetric] simp del: fps_const_add) + by (case_tac n, auto simp add: power_Suc field_simps) lemma fps_inverse_deriv: fixes a:: "('a :: field) fps" @@ -1060,11 +1060,11 @@ with inverse_mult_eq_1[OF a0] have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) = 0" unfolding power2_eq_square - apply (simp add: ring_simps) + apply (simp add: field_simps) by (simp add: mult_assoc[symmetric]) hence "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * inverse a ^ 2 = 0 - fps_deriv a * inverse a ^ 2" by simp - then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2" by (simp add: ring_simps) + then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2" by (simp add: field_simps) qed lemma fps_inverse_mult: @@ -1084,7 +1084,7 @@ from inverse_mult_eq_1[OF ab0] have "inverse (a*b) * (a*b) * inverse a * inverse b = 1 * inverse a * inverse b" by simp then have "inverse (a*b) * (inverse a * a) * (inverse b * b) = inverse a * inverse b" - by (simp add: ring_simps) + by (simp add: field_simps) then have ?thesis using inverse_mult_eq_1[OF a0] inverse_mult_eq_1[OF b0] by simp} ultimately show ?thesis by blast qed @@ -1105,7 +1105,7 @@ assumes a0: "b$0 \ 0" shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b ^ 2" using fps_inverse_deriv[OF a0] - by (simp add: fps_divide_def ring_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0]) + by (simp add: fps_divide_def field_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0]) lemma fps_inverse_gp': "inverse (Abs_fps(\n. (1::'a::field))) @@ -1121,7 +1121,7 @@ proof- have eq: "(1 + X) * ?r = 1" unfolding minus_one_power_iff - by (auto simp add: ring_simps fps_eq_iff) + by (auto simp add: field_simps fps_eq_iff) show ?thesis by (auto simp add: eq intro: fps_inverse_unique) qed @@ -1185,7 +1185,7 @@ next case (Suc k) note th = Suc.hyps[symmetric] - have "(Abs_fps a - setsum (\i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n = (Abs_fps a - setsum (\i. fps_const (a i :: 'a) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) $ n" by (simp add: ring_simps) + have "(Abs_fps a - setsum (\i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n = (Abs_fps a - setsum (\i. fps_const (a i :: 'a) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) $ n" by (simp add: field_simps) also have "\ = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)$n" using th unfolding fps_sub_nth by simp @@ -1209,10 +1209,10 @@ definition "XD = op * X o fps_deriv" lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: ('a::comm_ring_1) fps)" - by (simp add: XD_def ring_simps) + by (simp add: XD_def field_simps) lemma XD_mult_const[simp]:"XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * XD a" - by (simp add: XD_def ring_simps) + by (simp add: XD_def field_simps) lemma XD_linear[simp]: "XD (fps_const c * a + fps_const d * b) = fps_const c * XD a + fps_const d * XD (b :: ('a::comm_ring_1) fps)" by simp @@ -1226,7 +1226,7 @@ lemma fps_mult_XD_shift: "(XD ^^ k) (a:: ('a::{comm_ring_1}) fps) = Abs_fps (\n. (of_nat n ^ k) * a$n)" - by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def) + by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff field_simps del: One_nat_def) subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*} subsubsection{* Rule 5 --- summation and "division" by (1 - X)*} @@ -1688,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_eq_simps fps_radical_def del: of_nat_Suc) + unfolding n1 using r00 a0 by (simp add: field_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] .. @@ -1764,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_eq_simps divide_inverse) + hence "a * (inverse c * c) = b/c" by (simp only: field_simps divide_inverse) then show "a = b/c" unfolding field_inverse[OF c0] by simp qed @@ -1837,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_eq_simps del: of_nat_Suc) + by (simp add: field_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 @@ -1854,7 +1854,7 @@ then have "a$n = ?r $n" apply (simp del: of_nat_Suc) unfolding fps_radical_def n1 - by (simp add: field_eq_simps n1 th00 del: of_nat_Suc)} + by (simp add: field_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)} @@ -2018,11 +2018,11 @@ proof- {fix n have "(fps_deriv (a oo b))$n = setsum (\i. a $ i * (fps_deriv (b^i))$n) {0.. Suc n}" - by (simp add: fps_compose_def ring_simps setsum_right_distrib del: of_nat_Suc) + by (simp add: fps_compose_def field_simps setsum_right_distrib del: of_nat_Suc) also have "\ = setsum (\i. a$i * ((fps_const (of_nat i)) * (fps_deriv b * (b^(i - 1))))$n) {0.. Suc n}" - by (simp add: ring_simps fps_deriv_power del: fps_mult_left_const_nth of_nat_Suc) + by (simp add: field_simps fps_deriv_power del: fps_mult_left_const_nth of_nat_Suc) also have "\ = setsum (\i. of_nat i * a$i * (((b^(i - 1)) * fps_deriv b))$n) {0.. Suc n}" - unfolding fps_mult_left_const_nth by (simp add: ring_simps) + unfolding fps_mult_left_const_nth by (simp add: field_simps) also have "\ = setsum (\i. of_nat i * a$i * (setsum (\j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {0.. Suc n}" unfolding fps_mult_nth .. also have "\ = setsum (\i. of_nat i * a$i * (setsum (\j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {1.. Suc n}" @@ -2170,7 +2170,7 @@ by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum_0') lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)" - by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_addf) + by (simp add: fps_eq_iff fps_compose_nth field_simps setsum_addf) lemma fps_compose_setsum_distrib: "(setsum f S) oo a = setsum (\i. f i oo a) S" proof- @@ -2212,7 +2212,7 @@ apply (simp add: fps_mult_nth setsum_right_distrib) apply (subst setsum_commute) apply (rule setsum_cong2) - by (auto simp add: ring_simps) + by (auto simp add: field_simps) also have "\ = ?l" apply (simp add: fps_mult_nth fps_compose_nth setsum_product) apply (rule setsum_cong2) @@ -2312,7 +2312,7 @@ qed lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)" - by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_negf[symmetric]) + by (simp add: fps_eq_iff fps_compose_nth field_simps setsum_negf[symmetric]) lemma fps_compose_sub_distrib: shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)" @@ -2469,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_eq_simps) + from a1 have ra1: "?r a $ 1 \ 0" by (simp add: fps_inv_def field_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 @@ -2486,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_eq_simps) + from a1 c1 have rca1: "?r c a $ 1 \ 0" by (simp add: fps_ginv_def field_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 @@ -2534,8 +2534,8 @@ proof- {fix n have "?l$n = ?r $ n" - 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)} + apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc) + by (simp add: of_nat_mult field_simps)} then show ?thesis by (simp add: fps_eq_iff) qed @@ -2545,15 +2545,15 @@ 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_eq_simps del: of_nat_Suc) + by (simp add: fps_deriv_def fps_eq_iff field_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_eq_simps del: of_nat_Suc fact_Suc) + apply (simp add: field_simps del: of_nat_Suc fact_Suc) apply (drule sym) - by (simp add: ring_simps of_nat_mult power_Suc)} + by (simp add: field_simps of_nat_mult power_Suc)} note th' = this have ?rhs by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro : th')} @@ -2570,7 +2570,7 @@ lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r") proof- have "fps_deriv (?r) = fps_const (a+b) * ?r" - by (simp add: fps_const_add[symmetric] ring_simps del: fps_const_add) + by (simp add: fps_const_add[symmetric] field_simps del: fps_const_add) then have "?r = ?l" apply (simp only: E_unique_ODE) by (simp add: fps_mult_nth E_def) then show ?thesis .. @@ -2618,13 +2618,13 @@ (is "inverse ?l = ?r") proof- have th: "?l * ?r = 1" - by (auto simp add: ring_simps fps_eq_iff minus_one_power_iff) + by (auto simp add: field_simps fps_eq_iff minus_one_power_iff) have th': "?l $ 0 \ 0" by (simp add: ) from fps_inverse_unique[OF th' th] show ?thesis . qed lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)" - by (induct n, auto simp add: ring_simps E_add_mult power_Suc) + by (induct n, auto simp add: field_simps E_add_mult power_Suc) lemma radical_E: assumes r: "r (Suc k) 1 = 1" @@ -2649,18 +2649,18 @@ text{* The generalized binomial theorem as a consequence of @{thm E_add_mult} *} lemma gbinomial_theorem: - "((a::'a::{field_char_0, division_by_zero})+b) ^ n = (\k=0..n. of_nat (n choose k) * a^k * b^(n-k))" + "((a::'a::{field_char_0, division_ring_inverse_zero})+b) ^ n = (\k=0..n. of_nat (n choose k) * a^k * b^(n-k))" proof- 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_eq_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib) + by (simp add: field_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_eq_simps of_nat_mult) + by (simp add: field_simps of_nat_mult) qed text{* And the nat-form -- also available from Binomial.thy *} @@ -2683,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_eq_simps) + by (simp add: L_def field_simps) lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def) lemma L_E_inv: @@ -2694,9 +2694,9 @@ have b0: "?b $ 0 = 0" by simp have b1: "?b $ 1 \ 0" by (simp add: a) have "fps_deriv (E a - 1) oo fps_inv (E a - 1) = (fps_const a * (E a - 1) + fps_const a) oo fps_inv (E a - 1)" - by (simp add: ring_simps) + by (simp add: field_simps) also have "\ = fps_const a * (X + 1)" apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1]) - by (simp add: ring_simps) + by (simp add: field_simps) finally have eq: "fps_deriv (E a - 1) oo fps_inv (E a - 1) = fps_const a * (X + 1)" . from fps_inv_deriv[OF b0 b1, unfolded eq] have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)" @@ -2713,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_eq_simps) + from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_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" @@ -2743,7 +2743,7 @@ have "?l = ?r \ inverse ?x1 * ?l = inverse ?x1 * ?r" by simp also have "\ \ ?da = (fps_const c * a) / ?x1" apply (simp only: fps_divide_def mult_assoc[symmetric] inverse_mult_eq_1[OF x10]) - by (simp add: ring_simps) + by (simp add: field_simps) finally have eq: "?l = ?r \ ?lhs" by simp moreover {assume h: "?l = ?r" @@ -2752,8 +2752,8 @@ 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_eq_simps del: of_nat_Suc) + apply (simp add: field_simps del: of_nat_Suc) + by (cases n, simp_all add: field_simps del: of_nat_Suc) } note th0 = this {fix n have "a$n = (c gchoose n) * a$0" @@ -2762,24 +2762,24 @@ next case (Suc m) thus ?case unfolding th0 - apply (simp add: field_eq_simps del: of_nat_Suc) + apply (simp add: field_simps del: of_nat_Suc) unfolding mult_assoc[symmetric] gbinomial_mult_1 - by (simp add: ring_simps) + by (simp add: field_simps) qed} note th1 = this have ?rhs apply (simp add: fps_eq_iff) apply (subst th1) - by (simp add: ring_simps)} + by (simp add: field_simps)} moreover {assume h: ?rhs have th00:"\x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute) have "?l = ?r" apply (subst h) apply (subst (2) h) - apply (clarsimp simp add: fps_eq_iff ring_simps) + apply (clarsimp simp add: fps_eq_iff field_simps) unfolding mult_assoc[symmetric] th00 gbinomial_mult_1 - by (simp add: ring_simps gbinomial_mult_1)} + by (simp add: field_simps gbinomial_mult_1)} ultimately show ?thesis by blast qed @@ -2798,9 +2798,9 @@ have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)" by simp also have "\ = inverse (1 + X) * (fps_const c * ?b c * ?b d + fps_const d * ?b c * ?b d - fps_const (c+d) * ?b (c + d))" unfolding fps_binomial_deriv - by (simp add: fps_divide_def ring_simps) + by (simp add: fps_divide_def field_simps) also have "\ = (fps_const (c + d)/ (1 + X)) * ?P" - by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add) + by (simp add: field_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add) finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)" by (simp add: fps_divide_def) have "?P = fps_const (?P$0) * ?b (c + d)" @@ -2880,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_eq_simps power_add[symmetric])} + by (simp add: field_simps power_add[symmetric])} moreover {assume nk: "k \ n" have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" @@ -2905,7 +2905,7 @@ unfolding m1nk unfolding m h pochhammer_Suc_setprod - apply (simp add: field_eq_simps del: fact_Suc id_def) + apply (simp add: field_simps del: fact_Suc id_def) unfolding fact_altdef_nat id_def unfolding of_nat_setprod unfolding setprod_timesf[symmetric] @@ -2942,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_eq_simps) + using nz' by (simp add: field_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_eq_simps) + by (simp add: field_simps) also have "\ = b gchoose (n - k)" unfolding th1 th2 using kn' by (simp add: gbinomial_def) @@ -2959,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_eq_simps) + using bn0 by (auto simp add: field_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_eq_simps) + using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_simps) apply (rule setsum_cong2) apply (drule th00(2)) - by (simp add: field_eq_simps power_add[symmetric]) + by (simp add: field_simps power_add[symmetric]) finally show ?thesis by simp qed @@ -2992,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_eq_simps setsum_right_distrib) + show ?thesis using nz by (simp add: field_simps setsum_right_distrib) qed subsubsection{* Formal trigonometric functions *} @@ -3014,11 +3014,11 @@ 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_eq_simps del: of_nat_add of_nat_Suc) + by (simp add: field_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_eq_simps del: of_nat_add of_nat_Suc) + by (simp add: field_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 )} + by (simp add: fps_cos_def field_simps power_Suc )} then show "?lhs $ n = ?rhs $ n" by (cases "even n", simp_all add: fps_deriv_def fps_sin_def fps_cos_def) qed @@ -3038,13 +3038,13 @@ 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_eq_simps del: of_nat_add of_nat_Suc) + by (simp add: field_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_eq_simps del: of_nat_add of_nat_Suc) + by (simp add: field_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 - by (simp add: fps_sin_def ring_simps power_Suc)} + by (simp add: fps_sin_def field_simps power_Suc)} then show "?lhs $ n = ?rhs $ n" by (cases "even n", simp_all add: fps_deriv_def fps_sin_def fps_cos_def) @@ -3055,7 +3055,7 @@ proof- have "fps_deriv ?lhs = 0" apply (simp add: fps_deriv_power fps_sin_deriv fps_cos_deriv power_Suc) - by (simp add: ring_simps fps_const_neg[symmetric] del: fps_const_neg) + by (simp add: field_simps fps_const_neg[symmetric] del: fps_const_neg) then have "?lhs = fps_const (?lhs $ 0)" unfolding fps_deriv_eq_0_iff . also have "\ = 1" @@ -3177,7 +3177,7 @@ have th0: "fps_cos c $ 0 \ 0" by (simp add: fps_cos_def) show ?thesis using fps_sin_cos_sum_of_squares[of c] - apply (simp add: fps_tan_def fps_divide_deriv[OF th0] fps_sin_deriv fps_cos_deriv add: fps_const_neg[symmetric] ring_simps power2_eq_square del: fps_const_neg) + apply (simp add: fps_tan_def fps_divide_deriv[OF th0] fps_sin_deriv fps_cos_deriv add: fps_const_neg[symmetric] field_simps power2_eq_square del: fps_const_neg) unfolding right_distrib[symmetric] by simp qed @@ -3252,7 +3252,7 @@ subsection {* Hypergeometric series *} -definition "F as bs (c::'a::{field_char_0, division_by_zero}) = Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))" +definition "F as bs (c::'a::{field_char_0, division_ring_inverse_zero}) = Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))" lemma F_nth[simp]: "F as bs c $ n = (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n))" by (simp add: F_def) @@ -3321,9 +3321,9 @@ by (simp add: fps_eq_iff fps_integral_def) lemma F_minus_nat: - "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, division_by_zero}) $ k = (if k <= n then pochhammer (- of_nat n) k * c ^ k / + "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, division_ring_inverse_zero}) $ k = (if k <= n then pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k)) else 0)" - "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, division_by_zero}) $ k = (if k <= m then pochhammer (- of_nat m) k * c ^ k / + "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, division_ring_inverse_zero}) $ k = (if k <= m then pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k)) else 0)" by (auto simp add: pochhammer_eq_0_iff) diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Library/Fraction_Field.thy --- a/src/HOL/Library/Fraction_Field.thy Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Library/Fraction_Field.thy Mon Apr 26 13:43:31 2010 +0200 @@ -267,7 +267,7 @@ end -instance fract :: (idom) division_by_zero +instance fract :: (idom) division_ring_inverse_zero proof show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand) (simp add: fract_collapse) @@ -450,7 +450,7 @@ by simp with F have "(a * d) * (b * d) * ?F * ?F \ (c * b) * (b * d) * ?F * ?F" by (simp add: mult_le_cancel_right) - with neq show ?thesis by (simp add: ring_simps) + with neq show ?thesis by (simp add: field_simps) qed qed show "q < r ==> 0 < s ==> s * q < s * r" diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Library/Numeral_Type.thy Mon Apr 26 13:43:31 2010 +0200 @@ -213,7 +213,7 @@ lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)" apply (intro_classes, unfold definitions) -apply (simp_all add: Rep_simps zmod_simps ring_simps) +apply (simp_all add: Rep_simps zmod_simps field_simps) done end diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Library/Polynomial.thy Mon Apr 26 13:43:31 2010 +0200 @@ -1093,10 +1093,10 @@ apply (cases "r = 0") apply (cases "r' = 0") apply (simp add: pdivmod_rel_def) -apply (simp add: pdivmod_rel_def ring_simps degree_mult_eq) +apply (simp add: pdivmod_rel_def field_simps degree_mult_eq) apply (cases "r' = 0") apply (simp add: pdivmod_rel_def degree_mult_eq) -apply (simp add: pdivmod_rel_def ring_simps) +apply (simp add: pdivmod_rel_def field_simps) apply (simp add: degree_mult_eq degree_add_less) done diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Mon Apr 26 13:43:31 2010 +0200 @@ -1282,9 +1282,9 @@ fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS val concl = Thm.dest_arg o cprop_of val shuffle1 = - fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" by (atomize (full)) (simp add: ring_simps) }) + fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" by (atomize (full)) (simp add: field_simps) }) val shuffle2 = - fconv_rule (rewr_conv @{lemma "(x + a == y) == (x == y - (a::real))" by (atomize (full)) (simp add: ring_simps)}) + fconv_rule (rewr_conv @{lemma "(x + a == y) == (x == y - (a::real))" by (atomize (full)) (simp add: field_simps)}) fun substitutable_monomial fvs tm = case term_of tm of Free(_,@{typ real}) => if not (member (op aconvc) fvs tm) then (Rat.one,tm) else raise Failure "substitutable_monomial" diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Apr 26 13:43:31 2010 +0200 @@ -1383,7 +1383,7 @@ apply(rule_tac x=x in bexI) apply assumption+ apply(rule continuous_on_intros)+ unfolding frontier_cball subset_eq Ball_def image_iff apply(rule,rule,erule bexE) unfolding vector_dist_norm apply(simp add: * norm_minus_commute) . note x = this - hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by(auto simp add:group_simps) + hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by(auto simp add:algebra_simps) hence "a = x" unfolding scaleR_left_distrib[THEN sym] by auto thus False using x using assms by auto qed @@ -1396,7 +1396,7 @@ "interval_bij (a,b) (u,v) = (\x. (\ i. (v$i - u$i) / (b$i - a$i) * x$i) + (\ i. u$i - (v$i - u$i) / (b$i - a$i) * a$i))" apply rule unfolding Cart_eq interval_bij_def vector_component_simps - by(auto simp add:group_simps field_simps add_divide_distrib[THEN sym]) + by(auto simp add: field_simps add_divide_distrib[THEN sym]) lemma continuous_interval_bij: "continuous (at x) (interval_bij (a,b::real^'n) (u,v))" diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Apr 26 13:43:31 2010 +0200 @@ -646,7 +646,7 @@ using assms(1)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]] using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]] apply - apply(rule add_mono) by auto - hence "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \ u * (f x + g x) + v * (f y + g y)" by (simp add: ring_simps) } + hence "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \ u * (f x + g x) + v * (f y + g y)" by (simp add: field_simps) } thus ?thesis unfolding convex_on_def by auto qed @@ -654,7 +654,7 @@ assumes "0 \ (c::real)" "convex_on s f" shows "convex_on s (\x. c * f x)" proof- - have *:"\u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: ring_simps) + have *:"\u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps) show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto qed @@ -1060,7 +1060,7 @@ proof- have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto have *:"\x y z ::real. x + y + z = 1 \ x = 1 - y - z" - "\x y z ::real^_. x + y + z = 1 \ x = 1 - y - z" by (auto simp add: ring_simps) + "\x y z ::real^_. x + y + z = 1 \ x = 1 - y - z" by (auto simp add: field_simps) show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and * unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp @@ -2310,7 +2310,7 @@ } moreover { fix a b assume "\ u * a + v * b \ a" hence "v * b > (1 - u) * a" unfolding not_le using as(4) by(auto simp add: field_simps) - hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: ring_simps) + hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: field_simps) hence "u * a + v * b \ b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) } ultimately show "u *\<^sub>R x + v *\<^sub>R y \ s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)]) using as(3-) dimindex_ge_1 apply- by(auto simp add: vector_component) qed diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Apr 26 13:43:31 2010 +0200 @@ -1,11 +1,12 @@ -(* Title: HOL/Library/Convex_Euclidean_Space.thy - Author: John Harrison - Translation from HOL light: Robert Himmelmann, TU Muenchen *) +(* Title: HOL/Multivariate_Analysis/Derivative.thy + Author: John Harrison + Translation from HOL Light: Robert Himmelmann, TU Muenchen +*) header {* Multivariate calculus in Euclidean space. *} theory Derivative - imports Brouwer_Fixpoint RealVector +imports Brouwer_Fixpoint RealVector begin @@ -40,7 +41,7 @@ show ?l unfolding deriv_def LIM_def apply safe apply(drule as,safe) apply(rule_tac x=d in exI,safe) apply(erule_tac x="xa + x" in allE) unfolding vector_dist_norm diff_0_right norm_scaleR - unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:group_simps *) qed + unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:algebra_simps *) qed lemma FDERIV_conv_has_derivative:"FDERIV f (x::'a::{real_normed_vector,perfect_space}) :> f' = (f has_derivative f') (at x)" (is "?l = ?r") proof assume ?l note as = this[unfolded fderiv_def] @@ -50,14 +51,14 @@ thus "\d>0. \xa. 0 < dist xa x \ dist xa x < d \ dist ((1 / norm (xa - netlimit (at x))) *\<^sub>R (f xa - (f (netlimit (at x)) + f' (xa - netlimit (at x))))) (0) < e" apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa - x" in allE) - unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:group_simps) qed next + unfolding vector_dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq) qed next assume ?r note as = this[unfolded has_derivative_def] show ?l unfolding fderiv_def LIM_def apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule) fix e::real assume "e>0" guess d using as[THEN conjunct2,unfolded Lim_at,rule_format,OF`e>0`] .. thus "\s>0. \xa. xa \ 0 \ dist xa 0 < s \ dist (norm (f (x + xa) - f x - f' xa) / norm xa) 0 < e" apply- apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa + x" in allE) - unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:group_simps) qed qed + unfolding vector_dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq add.commute) qed qed subsection {* These are the only cases we'll care about, probably. *} @@ -76,7 +77,7 @@ (\e>0. \d>0. \x'\s. 0 < norm(x' - x) \ norm(x' - x) < d \ norm(f x' - f x - f'(x' - x)) / norm(x' - x) < e)" unfolding has_derivative_within Lim_within vector_dist_norm - unfolding diff_0_right norm_mul by(simp add: group_simps) + unfolding diff_0_right norm_mul by (simp add: diff_diff_eq) lemma has_derivative_at': "(f has_derivative f') (at x) \ bounded_linear f' \ @@ -186,14 +187,14 @@ note as = assms[unfolded has_derivative_def] show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add) using Lim_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as - by(auto simp add:group_simps scaleR_right_diff_distrib scaleR_right_distrib) qed + by (auto simp add:algebra_simps scaleR_right_diff_distrib scaleR_right_distrib) qed lemma has_derivative_add_const:"(f has_derivative f') net \ ((\x. f x + c) has_derivative f') net" apply(drule has_derivative_add) apply(rule has_derivative_const) by auto lemma has_derivative_sub: "(f has_derivative f') net \ (g has_derivative g') net \ ((\x. f(x) - g(x)) has_derivative (\h. f'(h) - g'(h))) net" - apply(drule has_derivative_add) apply(drule has_derivative_neg,assumption) by(simp add:group_simps) + apply(drule has_derivative_add) apply(drule has_derivative_neg,assumption) by(simp add:algebra_simps) lemma has_derivative_setsum: assumes "finite s" "\a\s. ((f a) has_derivative (f' a)) net" shows "((\x. setsum (\a. f a x) s) has_derivative (\h. setsum (\a. f' a h) s)) net" @@ -391,8 +392,8 @@ case False hence "norm (f y - (f x + f' (y - x))) < e * norm (y - x)" using as(4)[rule_format, OF `y\s`] unfolding vector_dist_norm diff_0_right norm_mul using as(3) using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded vector_dist_norm] - by(auto simp add:linear_0 linear_sub group_simps) - thus ?thesis by(auto simp add:group_simps) qed qed next + by (auto simp add: linear_0 linear_sub) + thus ?thesis by(auto simp add:algebra_simps) qed qed next assume ?rhs thus ?lhs unfolding has_derivative_within Lim_within apply-apply(erule conjE,rule,assumption) apply(rule,erule_tac x="e/2" in allE,rule,erule impE) defer apply(erule exE,rule_tac x=d in exI) apply(erule conjE,rule,assumption,rule,rule) unfolding vector_dist_norm diff_0_right norm_scaleR @@ -400,7 +401,7 @@ fix e d y assume "bounded_linear f'" "0 < e" "0 < d" "y \ s" "0 < norm (y - x) \ norm (y - x) < d" "norm (f y - f x - f' (y - x)) \ e / 2 * norm (y - x)" thus "\1 / norm (y - x)\ * norm (f y - (f x + f' (y - x))) < e" - apply(rule_tac le_less_trans[of _ "e/2"]) by(auto intro!:mult_imp_div_pos_le simp add:group_simps) qed auto qed + apply(rule_tac le_less_trans[of _ "e/2"]) by(auto intro!:mult_imp_div_pos_le simp add:algebra_simps) qed auto qed lemma has_derivative_at_alt: "(f has_derivative f') (at x) \ bounded_linear f' \ @@ -435,8 +436,8 @@ hence 1:"norm (f y - f x - f' (y - x)) \ min (norm (y - x)) (e / 2 / B2 * norm (y - x))" using d1 d2 d by auto have "norm (f y - f x) \ norm (f y - f x - f' (y - x)) + norm (f' (y - x))" - using norm_triangle_sub[of "f y - f x" "f' (y - x)"] by(auto simp add:group_simps) - also have "\ \ norm (f y - f x - f' (y - x)) + B1 * norm (y - x)" apply(rule add_left_mono) using B1 by(auto simp add:group_simps) + using norm_triangle_sub[of "f y - f x" "f' (y - x)"] by(auto simp add:algebra_simps) + also have "\ \ norm (f y - f x - f' (y - x)) + B1 * norm (y - x)" apply(rule add_left_mono) using B1 by(auto simp add:algebra_simps) also have "\ \ min (norm (y - x)) (e / 2 / B2 * norm (y - x)) + B1 * norm (y - x)" apply(rule add_right_mono) using d1 d2 d as by auto also have "\ \ norm (y - x) + B1 * norm (y - x)" by auto also have "\ = norm (y - x) * (1 + B1)" by(auto simp add:field_simps) @@ -453,8 +454,8 @@ interpret g': bounded_linear g' using assms(2) by auto interpret f': bounded_linear f' using assms(1) by auto have "norm (- g' (f' (y - x)) + g' (f y - f x)) = norm (g' (f y - f x - f' (y - x)))" - by(auto simp add:group_simps f'.diff g'.diff g'.add) - also have "\ \ B2 * norm (f y - f x - f' (y - x))" using B2 by(auto simp add:group_simps) + by(auto simp add:algebra_simps f'.diff g'.diff g'.add) + also have "\ \ B2 * norm (f y - f x - f' (y - x))" using B2 by(auto simp add:algebra_simps) also have "\ \ B2 * (e / 2 / B2 * norm (y - x))" apply(rule mult_left_mono) using as d1 d2 d B2 by auto also have "\ \ e / 2 * norm (y - x)" using B2 by auto finally have 5:"norm (- g' (f' (y - x)) + g' (f y - f x)) \ e / 2 * norm (y - x)" by auto @@ -535,7 +536,7 @@ unfolding scaleR_right_distrib by auto also have "\ = norm ((1 / abs c) *\<^sub>R (c *\<^sub>R (- (f' (basis i)) + f'' (basis i))))" unfolding f'.scaleR f''.scaleR unfolding scaleR_right_distrib scaleR_minus_right by auto - also have "\ = e" unfolding e_def norm_mul using c[THEN conjunct1] using norm_minus_cancel[of "f' (basis i) - f'' (basis i)"] by(auto simp add:group_simps) + also have "\ = e" unfolding e_def norm_mul using c[THEN conjunct1] using norm_minus_cancel[of "f' (basis i) - f'' (basis i)"] by (auto simp add: add.commute ab_diff_minus) finally show False using c using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R basis i"] using norm_basis[of i] unfolding vector_dist_norm unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib by auto qed qed @@ -623,7 +624,7 @@ have ***:"\y y1 y2 d dx::real. (y1\y\y2\y) \ (y\y1\y\y2) \ d < abs dx \ abs(y1 - y - - dx) \ d \ (abs (y2 - y - dx) \ d) \ False" by arith show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\D $ k $ j\ / 2 * \d\"]) using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left - unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding group_simps by (auto intro: mult_pos_pos) + unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos) qed subsection {* In particular if we have a mapping into @{typ "real^1"}. *} @@ -727,7 +728,7 @@ shows "norm(f x - f y) \ B * norm(x - y)" proof- let ?p = "\u. x + u *\<^sub>R (y - x)" have *:"\u. u\{0..1} \ x + u *\<^sub>R (y - x) \ s" - using assms(1)[unfolded convex_alt,rule_format,OF x y] unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib by(auto simp add:group_simps) + using assms(1)[unfolded convex_alt,rule_format,OF x y] unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib by(auto simp add:algebra_simps) hence 1:"continuous_on {0..1} (f \ ?p)" apply- apply(rule continuous_on_intros continuous_on_vmul)+ unfolding continuous_on_eq_continuous_within apply(rule,rule differentiable_imp_continuous_within) unfolding differentiable_def apply(rule_tac x="f' xa" in exI) @@ -862,7 +863,7 @@ assumes "compact t" "convex t" "t \ {}" "continuous_on t f" "\x\s. \y\t. x + (y - f y) \ t" "x\s" shows "\y\t. f y = x" proof- - have *:"\x y. f y = x \ x + (y - f y) = y" by(auto simp add:group_simps) + have *:"\x y. f y = x \ x + (y - f y) = y" by(auto simp add:algebra_simps) show ?thesis unfolding * apply(rule brouwer[OF assms(1-3), of "\y. x + (y - f y)"]) apply(rule continuous_on_intros assms)+ using assms(4-6) by auto qed @@ -907,8 +908,8 @@ finally have *:"norm (x + g' (z - f x) - x) < e0" by auto have **:"f x + f' (x + g' (z - f x) - x) = z" using assms(6)[unfolded o_def id_def,THEN cong] by auto have "norm (f x - (y + (z - f (x + g' (z - f x))))) \ norm (f (x + g' (z - f x)) - z) + norm (f x - y)" - using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"] by(auto simp add:group_simps) - also have "\ \ 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)" using e0[THEN conjunct2,rule_format,OF *] unfolding group_simps ** by auto + using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"] by(auto simp add:algebra_simps) + also have "\ \ 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)" using e0[THEN conjunct2,rule_format,OF *] unfolding algebra_simps ** by auto also have "\ \ 1 / (B * 2) * norm (g' (z - f x)) + e/2" using as(1)[unfolded mem_cball vector_dist_norm] by auto also have "\ \ 1 / (B * 2) * B * norm (z - f x) + e/2" using * and B by(auto simp add:field_simps) also have "\ \ 1 / 2 * norm (z - f x) + e/2" by auto @@ -983,7 +984,7 @@ (* we know for some other reason that the inverse function exists, it's OK. *} lemma bounded_linear_sub: "bounded_linear f \ bounded_linear g ==> bounded_linear (\x. f x - g x)" - using bounded_linear_add[of f "\x. - g x"] bounded_linear_minus[of g] by(auto simp add:group_simps) + using bounded_linear_add[of f "\x. - g x"] bounded_linear_minus[of g] by(auto simp add:algebra_simps) lemma has_derivative_locally_injective: fixes f::"real^'n \ real^'m" assumes "a \ s" "open s" "bounded_linear g'" "g' o f'(a) = id" @@ -1004,7 +1005,7 @@ show "\x\ball a d. \x'\ball a d. f x' = f x \ x' = x" proof(intro strip) fix x y assume as:"x\ball a d" "y\ball a d" "f x = f y" def ph \ "\w. w - g'(f w - f x)" have ph':"ph = g' \ (\w. f' a w - (f w - f x))" - unfolding ph_def o_def unfolding diff using f'g' by(auto simp add:group_simps) + unfolding ph_def o_def unfolding diff using f'g' by(auto simp add:algebra_simps) have "norm (ph x - ph y) \ (1/2) * norm (x - y)" apply(rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\x v. v - g'(f' x v)"]) apply(rule_tac[!] ballI) proof- fix u assume u:"u \ ball a d" hence "u\s" using d d2 by auto @@ -1020,7 +1021,7 @@ unfolding linear_conv_bounded_linear by(rule assms(3) **)+ also have "\ \ onorm g' * k" apply(rule mult_left_mono) using d1[THEN conjunct2,rule_format,of u] using onorm_neg[OF **(1)[unfolded linear_linear]] - using d and u and onorm_pos_le[OF assms(3)[unfolded linear_linear]] by(auto simp add:group_simps) + using d and u and onorm_pos_le[OF assms(3)[unfolded linear_linear]] by(auto simp add:algebra_simps) also have "\ \ 1/2" unfolding k_def by auto finally show "onorm (\v. v - g' (f' u v)) \ 1 / 2" by assumption qed moreover have "norm (ph y - ph x) = norm (y - x)" apply(rule arg_cong[where f=norm]) @@ -1039,7 +1040,7 @@ fix x assume "x\s" show "((\a. f m a - f n a) has_derivative (\h. f' m x h - f' n x h)) (at x within s)" by(rule has_derivative_intros assms(2)[rule_format] `x\s`)+ { fix h have "norm (f' m x h - f' n x h) \ norm (f' m x h - g' x h) + norm (f' n x h - g' x h)" - using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"] unfolding norm_minus_commute by(auto simp add:group_simps) + using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"] unfolding norm_minus_commute by(auto simp add:algebra_simps) also have "\ \ e * norm h+ e * norm h" using assms(3)[rule_format,OF `N\m` `x\s`, of h] assms(3)[rule_format,OF `N\n` `x\s`, of h] by(auto simp add:field_simps) finally have "norm (f' m x h - f' n x h) \ 2 * e * norm h" by auto } @@ -1083,7 +1084,7 @@ have "eventually (\xa. norm (f n x - f n y - (f xa x - f xa y)) \ e * norm (x - y)) sequentially" unfolding eventually_sequentially apply(rule_tac x=N in exI) proof(rule,rule) fix m assume "N\m" thus "norm (f n x - f n y - (f m x - f m y)) \ e * norm (x - y)" - using N[rule_format, of n m x y] and as by(auto simp add:group_simps) qed + using N[rule_format, of n m x y] and as by(auto simp add:algebra_simps) qed thus "norm (f n x - f n y - (g x - g y)) \ e * norm (x - y)" apply- apply(rule Lim_norm_ubound[OF trivial_limit_sequentially, where f="\m. (f n x - f n y) - (f m x - f m y)"]) apply(rule Lim_sub Lim_const g[rule_format] as)+ by assumption qed qed @@ -1120,10 +1121,10 @@ have "norm (f ?N y - f ?N x - f' ?N x (y - x)) \ e / 3 * norm (y - x)" using d1 and as by auto ultimately have "norm (g y - g x - f' ?N x (y - x)) \ 2 * e / 3 * norm (y - x)" using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"] - by (auto simp add:group_simps) moreover + by (auto simp add:algebra_simps) moreover have " norm (f' ?N x (y - x) - g' x (y - x)) \ e / 3 * norm (y - x)" using N1 `x\s` by auto ultimately show "norm (g y - g x - g' x (y - x)) \ e * norm (y - x)" - using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"] by(auto simp add:group_simps) + using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"] by(auto simp add:algebra_simps) qed qed qed qed subsection {* Can choose to line up antiderivatives if we want. *} @@ -1274,7 +1275,7 @@ unfolding has_vector_derivative_def using has_derivative_id by auto lemma has_vector_derivative_cmul: "(f has_vector_derivative f') net \ ((\x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net" - unfolding has_vector_derivative_def apply(drule has_derivative_cmul) by(auto simp add:group_simps) + unfolding has_vector_derivative_def apply(drule has_derivative_cmul) by(auto simp add:algebra_simps) lemma has_vector_derivative_cmul_eq: assumes "c \ 0" shows "(((\x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \ (f has_vector_derivative f') net)" diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Mon Apr 26 13:43:31 2010 +0200 @@ -55,7 +55,7 @@ done (* FIXME: In Finite_Set there is a useless further assumption *) -lemma setprod_inversef: "finite A ==> setprod (inverse \ f) A = (inverse (setprod f A) :: 'a:: {division_by_zero, field})" +lemma setprod_inversef: "finite A ==> setprod (inverse \ f) A = (inverse (setprod f A) :: 'a:: {division_ring_inverse_zero, field})" apply (erule finite_induct) apply (simp) apply simp @@ -352,13 +352,13 @@ apply (rule setprod_insert) apply simp by blast - also have "\ = (a k $ p k * setprod (\i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\i. ?f i $ p i) ?Uk)" by (simp add: ring_simps) + also have "\ = (a k $ p k * setprod (\i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\i. ?f i $ p i) ?Uk)" by (simp add: field_simps) also have "\ = (a k $ p k * setprod (\i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\i. ?h i $ p i) ?Uk)" by (metis th1 th2) also have "\ = setprod (\i. ?g i $ p i) (insert k ?Uk) + setprod (\i. ?h i $ p i) (insert k ?Uk)" unfolding setprod_insert[OF th3] by simp finally have "setprod (\i. ?f i $ p i) ?U = setprod (\i. ?g i $ p i) ?U + setprod (\i. ?h i $ p i) ?U" unfolding kU[symmetric] . then show "of_int (sign p) * setprod (\i. ?f i $ p i) ?U = of_int (sign p) * setprod (\i. ?g i $ p i) ?U + of_int (sign p) * setprod (\i. ?h i $ p i) ?U" - by (simp add: ring_simps) + by (simp add: field_simps) qed lemma det_row_mul: @@ -389,14 +389,14 @@ apply (rule setprod_insert) apply simp by blast - also have "\ = (c*s a k) $ p k * setprod (\i. ?f i $ p i) ?Uk" by (simp add: ring_simps) + also have "\ = (c*s a k) $ p k * setprod (\i. ?f i $ p i) ?Uk" by (simp add: field_simps) also have "\ = c* (a k $ p k * setprod (\i. ?g i $ p i) ?Uk)" unfolding th1 by (simp add: mult_ac) also have "\ = c* (setprod (\i. ?g i $ p i) (insert k ?Uk))" unfolding setprod_insert[OF th3] by simp finally have "setprod (\i. ?f i $ p i) ?U = c* (setprod (\i. ?g i $ p i) ?U)" unfolding kU[symmetric] . then show "of_int (sign p) * setprod (\i. ?f i $ p i) ?U = c * (of_int (sign p) * setprod (\i. ?g i $ p i) ?U)" - by (simp add: ring_simps) + by (simp add: field_simps) qed lemma det_row_0: @@ -604,7 +604,7 @@ have "setprod (\i. c i * a i $ p i) ?U = setprod c ?U * setprod (\i. a i $ p i) ?U" unfolding setprod_timesf .. then show "?s * (\xa\?U. c xa * a xa $ p xa) = - setprod c ?U * (?s* (\xa\?U. a xa $ p xa))" by (simp add: ring_simps) + setprod c ?U * (?s* (\xa\?U. a xa $ p xa))" by (simp add: field_simps) qed lemma det_mul: @@ -681,7 +681,7 @@ using permutes_in_image[OF q] by vector show "?s q * setprod (\i. (((\ i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U = ?s p * (setprod (\i. A$i$p i) ?U) * (?s (q o inv p) * setprod (\i. B$i$(q o inv p) i) ?U)" using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp] - by (simp add: sign_nz th00 ring_simps sign_idempotent sign_compose) + by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose) qed } then have th2: "setsum (\f. det (\ i. A$i$f i *s B$f i)) ?PU = det A * det B" @@ -772,7 +772,7 @@ have fUk: "finite ?Uk" by simp have kUk: "k \ ?Uk" by simp have th00: "\k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s" - by (vector ring_simps) + by (vector field_simps) have th001: "\f k . (\x. if x = k then f k else f x) = f" by (auto intro: ext) have "(\ i. row i A) = A" by (vector row_def) then have thd1: "det (\ i. row i A) = det A" by simp @@ -793,7 +793,7 @@ unfolding thd0 unfolding det_row_mul unfolding th001[of k "\i. row i A"] - unfolding thd1 by (simp add: ring_simps) + unfolding thd1 by (simp add: field_simps) qed lemma cramer_lemma: @@ -901,7 +901,7 @@ have th: "\x::'a. x = 1 \ x = - 1 \ x*x = 1" (is "\x::'a. ?ths x") proof- fix x:: 'a - have th0: "x*x - 1 = (x - 1)*(x + 1)" by (simp add: ring_simps) + have th0: "x*x - 1 = (x - 1)*(x + 1)" by (simp add: field_simps) have th1: "\(x::'a) y. x = - y \ x + y = 0" apply (subst eq_iff_diff_eq_0) by simp have "x*x = 1 \ x*x - 1 = 0" by simp @@ -929,7 +929,7 @@ unfolding dot_norm_neg dist_norm[symmetric] unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} note fc = this - show ?thesis unfolding linear_def vector_eq smult_conv_scaleR by (simp add: inner_simps fc ring_simps) + show ?thesis unfolding linear_def vector_eq smult_conv_scaleR by (simp add: inner_simps fc field_simps) qed lemma isometry_linear: @@ -980,7 +980,7 @@ using H(5-9) apply (simp add: norm_eq norm_eq_1) apply (simp add: inner_simps smult_conv_scaleR) unfolding * - by (simp add: ring_simps) } + by (simp add: field_simps) } note th0 = this let ?g = "\x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)" {fix x:: "real ^'n" assume nx: "norm x = 1" @@ -1079,7 +1079,7 @@ unfolding permutes_sing apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq) apply (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31)) - by (simp add: ring_simps) + by (simp add: field_simps) qed end diff -r 3cbce59ed78d -r 85ee44388f7b src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Apr 26 11:20:18 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Apr 26 13:43:31 2010 +0200 @@ -257,14 +257,14 @@ | "vector_power x (Suc n) = x * vector_power x n" instance cart :: (semiring,finite) semiring - apply (intro_classes) by (vector ring_simps)+ + apply (intro_classes) by (vector field_simps)+ instance cart :: (semiring_0,finite) semiring_0 - apply (intro_classes) by (vector ring_simps)+ + apply (intro_classes) by (vector field_simps)+ instance cart :: (semiring_1,finite) semiring_1 apply (intro_classes) by vector instance cart :: (comm_semiring,finite) comm_semiring - apply (intro_classes) by (vector ring_simps)+ + apply (intro_classes) by (vector field_simps)+ instance cart :: (comm_semiring_0,finite) comm_semiring_0 by (intro_classes) instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. @@ -278,7 +278,7 @@ instance cart :: (real_algebra,finite) real_algebra apply intro_classes - apply (simp_all add: vector_scaleR_def ring_simps) + apply (simp_all add: vector_scaleR_def field_simps) apply vector apply vector done @@ -318,19 +318,19 @@ lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x" by (vector mult_assoc) lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x" - by (vector ring_simps) + by (vector field_simps) lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y" - by (vector ring_simps) + by (vector field_simps) lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y" - by (vector ring_simps) + by (vector field_simps) lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector lemma vector_sneg_minus1: "-x = (- (1::'a::ring_1)) *s x" by vector lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x" - by (vector ring_simps) + by (vector field_simps) lemma vec_eq[simp]: "(vec m = vec n) \ (m = n)" by (simp add: Cart_eq) @@ -752,7 +752,7 @@ lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)" proof- have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith - thus ?thesis by (simp add: ring_simps power2_eq_square) + thus ?thesis by (simp add: field_simps power2_eq_square) qed lemma square_continuous: "0 < (e::real) ==> \d. 0 < d \ (\y. abs(y - x) < d \ abs(y * y - x * x) < e)" @@ -828,7 +828,7 @@ lemma norm_triangle_sub: fixes x y :: "'a::real_normed_vector" shows "norm x \ norm y + norm (x - y)" - using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps) + using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps) lemma component_le_norm: "\x$i\ <= norm x" apply (simp add: norm_vector_def) @@ -867,7 +867,7 @@ lemma real_abs_le_square_iff: "\x\ \ \y\ \ (x::real)^2 \ y^2" proof- - have "x^2 \ y^2 \ (x -y) * (y + x) \ 0" by (simp add: ring_simps power2_eq_square) + have "x^2 \ y^2 \ (x -y) * (y + x) \ 0" by (simp add: field_simps power2_eq_square) also have "\ \ \x\ \ \y\" apply (simp add: zero_compare_simps real_abs_def not_less) by arith finally show ?thesis .. qed @@ -898,7 +898,7 @@ unfolding power2_norm_eq_inner inner_simps inner_commute by auto lemma dot_norm_neg: "x \ y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2" - unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:group_simps) + unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:algebra_simps) text{* Equality of vectors in terms of @{term "op \"} products. *} @@ -909,7 +909,7 @@ assume ?rhs then have "x \ x - x \ y = 0 \ x \ y - y \ y = 0" by simp hence "x \ (x - y) = 0 \ y \ (x - y) = 0" by (simp add: inner_simps inner_commute) - then have "(x - y) \