# HG changeset patch # User paulson # Date 1675173916 0 # Node ID 9a60c17595437d39a706fd295440c611f468f8a7 # Parent da8a0e7bcac86ba18f43ec6fd607b52d6cb9ada8 Lots more new material thanks to Manuel Eberl diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Jan 31 14:05:16 2023 +0000 @@ -2193,6 +2193,12 @@ by (auto simp: Re_exp Im_exp) qed +lemma Arg_1 [simp]: "Arg 1 = 0" + by (rule Arg_unique[of 1]) auto + +lemma Arg_numeral [simp]: "Arg (numeral n) = 0" + by (rule Arg_unique[of "numeral n"]) auto + lemma Arg_times_of_real [simp]: assumes "0 < r" shows "Arg (of_real r * z) = Arg z" using Arg_def Ln_times_of_real assms by auto @@ -2207,6 +2213,10 @@ using Im_Ln_le_pi Im_Ln_pos_le by (simp add: Arg_def) +text \converse fails because the argument can equal $\pi$.\ +lemma Arg_uminus: "Arg z < 0 \ Arg (-z) > 0" + by (smt (verit) Arg_bounded Arg_minus Complex.Arg_def) + lemma Arg_eq_pi: "Arg z = pi \ Re z < 0 \ Im z = 0" by (auto simp: Arg_def Im_Ln_eq_pi) @@ -2261,7 +2271,13 @@ by (metis Arg_cnj_eq_inverse Arg_inverse Reals_0 complex_cnj_zero) lemma Arg_exp: "-pi < Im z \ Im z \ pi \ Arg(exp z) = Im z" - by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar) + by (simp add: Arg_eq_Im_Ln) + +lemma Arg_cis: "x \ {-pi<..pi} \ Arg (cis x) = x" + unfolding cis_conv_exp by (subst Arg_exp) auto + +lemma Arg_rcis: "x \ {-pi<..pi} \ r > 0 \ Arg (rcis r x) = x" + unfolding rcis_def by (subst Arg_times_of_real) (auto simp: Arg_cis) lemma Ln_Arg: "z\0 \ Ln(z) = ln(norm z) + \ * Arg(z)" by (metis Arg_def Re_Ln complex_eq) @@ -3093,6 +3109,33 @@ by simp qed +lemma csqrt_mult: + assumes "Arg z + Arg w \ {-pi<..pi}" + shows "csqrt (z * w) = csqrt z * csqrt w" +proof (cases "z = 0 \ w = 0") + case False + have "csqrt (z * w) = exp ((ln (z * w)) / 2)" + using False by (intro csqrt_exp_Ln) auto + also have "\ = exp ((Ln z + Ln w) / 2)" + using False assms by (subst Ln_times_simple) (auto simp: Arg_eq_Im_Ln) + also have "(Ln z + Ln w) / 2 = Ln z / 2 + Ln w / 2" + by (simp add: add_divide_distrib) + also have "exp \ = csqrt z * csqrt w" + using False by (simp add: exp_add csqrt_exp_Ln) + finally show ?thesis . +qed auto + +lemma Arg_csqrt [simp]: "Arg (csqrt z) = Arg z / 2" +proof (cases "z = 0") + case False + have "Im (Ln z) \ {-pi<..pi}" + by (simp add: False Im_Ln_le_pi mpi_less_Im_Ln) + also have "\ \ {-2*pi<..2*pi}" + by auto + finally show ?thesis + using False by (auto simp: csqrt_exp_Ln Arg_exp Arg_eq_Im_Ln) +qed (auto simp: Arg_zero) + lemma csqrt_inverse: "z \ \\<^sub>\\<^sub>0 \ csqrt (inverse z) = inverse (csqrt z)" by (metis Ln_inverse csqrt_eq_0 csqrt_exp_Ln divide_minus_left exp_minus diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Analysis/Derivative.thy Tue Jan 31 14:05:16 2023 +0000 @@ -313,9 +313,13 @@ lemma diff_chain_at[derivative_intros]: "(f has_derivative f') (at x) \ (g has_derivative g') (at (f x)) \ ((g \ f) has_derivative (g' \ f')) (at x)" - using has_derivative_compose[of f f' x UNIV g g'] - by (simp add: comp_def) - + by (meson diff_chain_within has_derivative_at_withinI) + +lemma has_vector_derivative_shift: "(f has_vector_derivative D x) (at x) + \ ((+) d \ f has_vector_derivative D x) (at x)" + using diff_chain_at [OF _ shift_has_derivative_id] + by (simp add: has_derivative_iff_Ex has_vector_derivative_def) + lemma has_vector_derivative_within_open: "a \ S \ open S \ (f has_vector_derivative f') (at a within S) \ (f has_vector_derivative f') (at a)" @@ -3311,7 +3315,16 @@ lemma C1_differentiable_on_of_real [derivative_intros]: "of_real C1_differentiable_on S" unfolding C1_differentiable_on_def - by (smt (verit, del_insts) DERIV_ident UNIV_I continuous_on_const has_vector_derivative_of_real has_vector_derivative_transform) + using vector_derivative_works by fastforce + +lemma C1_differentiable_on_translation: + "f C1_differentiable_on U - S \ (+) d \ f C1_differentiable_on U - S" + by (metis C1_differentiable_on_def has_vector_derivative_shift) + +lemma C1_differentiable_on_translation_eq: + fixes d :: "'a::real_normed_vector" + shows "(+) d \ f C1_differentiable_on i - S \ f C1_differentiable_on i - S" + by (force simp: o_def intro: C1_differentiable_on_translation dest: C1_differentiable_on_translation [of concl: "-d"]) definition\<^marker>\tag important\ piecewise_C1_differentiable_on @@ -3330,6 +3343,11 @@ C1_differentiable_on_def differentiable_def has_vector_derivative_def intro: has_derivative_at_withinI) +lemma piecewise_C1_differentiable_on_translation_eq: + "((+) d \ f piecewise_C1_differentiable_on i) \ (f piecewise_C1_differentiable_on i)" + unfolding piecewise_C1_differentiable_on_def continuous_on_translation_eq + by (metis C1_differentiable_on_translation_eq) + lemma piecewise_C1_differentiable_compose [derivative_intros]: assumes fg: "f piecewise_C1_differentiable_on S" "g piecewise_C1_differentiable_on (f ` S)" and fin: "\x. finite (S \ f-`{x})" shows "(g \ f) piecewise_C1_differentiable_on S" diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Analysis/Elementary_Metric_Spaces.thy --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Jan 31 14:05:16 2023 +0000 @@ -370,6 +370,20 @@ by (metis islimpt_approachable closed_limpt [where 'a='a]) qed +lemma discrete_imp_not_islimpt: + assumes e: "0 < e" + and d: "\x y. x \ S \ y \ S \ dist y x < e \ y = x" + shows "\ x islimpt S" +proof + assume "x islimpt S" + hence "x islimpt S - {x}" + by (meson islimpt_punctured) + moreover from assms have "closed (S - {x})" + by (intro discrete_imp_closed) auto + ultimately show False + unfolding closed_limpt by blast +qed + subsection \Interior\ diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Analysis/Elementary_Topology.thy --- a/src/HOL/Analysis/Elementary_Topology.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Analysis/Elementary_Topology.thy Tue Jan 31 14:05:16 2023 +0000 @@ -13,7 +13,6 @@ Product_Vector begin - section \Elementary Topology\ @@ -845,6 +844,22 @@ apply (auto simp: open_Int) done +lemma open_imp_islimpt: + fixes x::"'a:: perfect_space" + assumes "open S" "x\S" + shows "x islimpt S" + using assms interior_eq interior_limit_point by auto + +lemma islimpt_Int_eventually: + assumes "x islimpt A" "eventually (\y. y \ B) (at x)" + shows "x islimpt A \ B" + using assms unfolding islimpt_def eventually_at_filter eventually_nhds + by (metis Int_iff UNIV_I open_Int) + +lemma islimpt_conv_frequently_at: + "x islimpt A \ frequently (\y. y \ A) (at x)" + unfolding islimpt_def eventually_at_filter frequently_def eventually_nhds by blast + lemma interior_closed_Un_empty_interior: assumes cS: "closed S" and iT: "interior T = {}" @@ -2435,6 +2450,16 @@ lemma homeomorphism_sym: "homeomorphism S t f g = homeomorphism t S g f" by (force simp: homeomorphism_def) +lemma continuous_on_translation_eq: + fixes g :: "'a :: real_normed_vector \ 'b :: real_normed_vector" + shows "continuous_on A ((+) a \ g) = continuous_on A g" +proof - + have g: "g = (\x. -a + x) \ ((\x. a + x) \ g)" + by (rule ext) simp + show ?thesis + by (metis (no_types, opaque_lifting) g continuous_on_compose homeomorphism_def homeomorphism_translation) +qed + definition\<^marker>\tag important\ homeomorphic :: "'a::topological_space set \ 'b::topological_space set \ bool" (infixr "homeomorphic" 60) where "s homeomorphic t \ (\f g. homeomorphism s t f g)" diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Analysis/Line_Segment.thy --- a/src/HOL/Analysis/Line_Segment.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Analysis/Line_Segment.thy Tue Jan 31 14:05:16 2023 +0000 @@ -914,15 +914,21 @@ qed qed +lemma closed_segment_same_fst: + "fst a = fst b \ closed_segment a b = {fst a} \ closed_segment (snd a) (snd b)" + by (auto simp: closed_segment_def scaleR_prod_def) + +lemma closed_segment_same_snd: + "snd a = snd b \ closed_segment a b = closed_segment (fst a) (fst b) \ {snd a}" + by (auto simp: closed_segment_def scaleR_prod_def) + lemma subset_oc_segment: fixes a :: "'a::euclidean_space" shows "open_segment a b \ closed_segment c d \ a = b \ a \ closed_segment c d \ b \ closed_segment c d" -apply (simp add: subset_open_segment [symmetric]) -apply (rule iffI) - apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment) -apply (meson dual_order.trans segment_open_subset_closed) -done + apply (rule iffI) + apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment) + by (meson dual_order.trans segment_open_subset_closed subset_open_segment) lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Analysis/Smooth_Paths.thy --- a/src/HOL/Analysis/Smooth_Paths.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Analysis/Smooth_Paths.thy Tue Jan 31 14:05:16 2023 +0000 @@ -270,6 +270,9 @@ lemma closed_valid_path_image: "valid_path g \ closed(path_image g)" by (metis closed_path_image valid_path_imp_path) +lemma valid_path_translation_eq: "valid_path ((+)d \ p) \ valid_path p" + by (simp add: valid_path_def piecewise_C1_differentiable_on_translation_eq) + lemma valid_path_compose: assumes "valid_path g" and der: "\x. x \ path_image g \ f field_differentiable (at x)" @@ -312,9 +315,8 @@ ultimately have "f \ g C1_differentiable_on {0..1} - S" using C1_differentiable_on_eq by blast moreover have "path (f \ g)" - apply (rule path_continuous_image[OF valid_path_imp_path[OF \valid_path g\]]) using der - by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at) + by (simp add: path_continuous_image[OF valid_path_imp_path[OF \valid_path g\]] continuous_at_imp_continuous_on field_differentiable_imp_continuous_at) ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def using \finite S\ by auto qed diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/BNF_Cardinal_Order_Relation.thy --- a/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Tue Jan 31 14:05:16 2023 +0000 @@ -411,7 +411,7 @@ card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast lemma card_of_Pow: "|A| x. x \ A \ f x \ \) \ Re (prod f A) = prod (\x. Re (f x)) A" proof (induction A rule: infinite_finite_induct) @@ -279,6 +285,9 @@ lemma i_even_power [simp]: "\ ^ (n * 2) = (-1) ^ n" by (metis mult.commute power2_i power_mult) +lemma i_even_power' [simp]: "even n \ \ ^ n = (-1) ^ (n div 2)" + by (metis dvd_mult_div_cancel power2_i power_mult) + lemma Re_i_times [simp]: "Re (\ * z) = - Im z" by simp @@ -1065,6 +1074,12 @@ using pi_not_less_zero by linarith qed auto +lemma cos_Arg: "z \ 0 \ cos (Arg z) = Re z / norm z" + by (metis Re_sgn cis.sel(1) cis_Arg) + +lemma sin_Arg: "z \ 0 \ sin (Arg z) = Im z / norm z" + by (metis Im_sgn cis.sel(2) cis_Arg) + subsection \Complex n-th roots\ lemma bij_betw_roots_unity: diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Filter.thy --- a/src/HOL/Filter.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Filter.thy Tue Jan 31 14:05:16 2023 +0000 @@ -65,6 +65,9 @@ lemma eventuallyI: "(\x. P x) \ eventually P F" by (auto intro: always_eventually) +lemma filter_eqI: "(\P. eventually P F \ eventually P G) \ F = G" + by (auto simp: filter_eq_iff) + lemma eventually_mono: "\eventually P F; \x. P x \ Q x\ \ eventually Q F" unfolding eventually_def @@ -105,6 +108,11 @@ shows "eventually (\i. R i) F" using assms by (auto elim!: eventually_rev_mp) +lemma eventually_cong: + assumes "eventually P F" and "\x. P x \ Q x \ R x" + shows "eventually Q F \ eventually R F" + using assms eventually_elim2 by blast + lemma eventually_ball_finite_distrib: "finite A \ (eventually (\x. \y\A. P x y) net) \ (\y\A. eventually (\x. P x y) net)" by (induction A rule: finite_induct) (auto simp: eventually_conj_iff) @@ -209,6 +217,12 @@ "(\\<^sub>Fx in F. P x \ Q x) \ (eventually P F \ frequently Q F)" unfolding imp_conv_disj frequently_disj_iff not_eventually[symmetric] .. +lemma frequently_eventually_conj: + assumes "\\<^sub>Fx in F. P x" + assumes "\\<^sub>Fx in F. Q x" + shows "\\<^sub>Fx in F. Q x \ P x" + using assms eventually_elim2 by (force simp add: frequently_def) + lemma eventually_frequently_const_simps: "(\\<^sub>Fx in F. P x \ C) \ (\\<^sub>Fx in F. P x) \ C" "(\\<^sub>Fx in F. C \ P x) \ C \ (\\<^sub>Fx in F. P x)" @@ -557,6 +571,13 @@ apply (auto elim!: eventually_rev_mp) done +lemma eventually_comp_filtermap: + "eventually (P \ f) F \ eventually P (filtermap f F)" + unfolding comp_def using eventually_filtermap by auto + +lemma filtermap_compose: "filtermap (f \ g) F = filtermap f (filtermap g F)" + unfolding filter_eq_iff by (simp add: eventually_filtermap) + lemma filtermap_ident: "filtermap (\x. x) F = F" by (simp add: filter_eq_iff eventually_filtermap) @@ -585,6 +606,16 @@ lemma filtermap_INF: "filtermap f (\b\B. F b) \ (\b\B. filtermap f (F b))" by (rule INF_greatest, rule filtermap_mono, erule INF_lower) +lemma frequently_cong: + assumes ev: "eventually P F" and QR: "\x. P x \ Q x \ R x" + shows "frequently Q F \ frequently R F" + unfolding frequently_def + using QR by (auto intro!: eventually_cong [OF ev]) + +lemma frequently_filtermap: + "frequently P (filtermap f F) = frequently (\x. P (f x)) F" + by (simp add: frequently_def eventually_filtermap) + subsubsection \Contravariant map function for filters\ diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Library/Equipollence.thy --- a/src/HOL/Library/Equipollence.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Library/Equipollence.thy Tue Jan 31 14:05:16 2023 +0000 @@ -186,7 +186,7 @@ lemma lesspoll_Pow_self: "A \ Pow A" unfolding lesspoll_def bij_betw_def eqpoll_def - by (meson lepoll_Pow_self Cantors_paradox) + by (meson lepoll_Pow_self Cantors_theorem) lemma finite_lesspoll_infinite: assumes "infinite A" "finite B" shows "B \ A" diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Power.thy --- a/src/HOL/Power.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Power.thy Tue Jan 31 14:05:16 2023 +0000 @@ -89,6 +89,9 @@ lemma power4_eq_xxxx: "x^4 = x * x * x * x" by (simp add: mult.assoc power_numeral_even) +lemma power_numeral_reduce: "x ^ numeral n = x * x ^ pred_numeral n" + by (simp add: numeral_eq_Suc) + lemma funpow_times_power: "(times x ^^ f x) = times (x ^ f x)" proof (induct "f x" arbitrary: f) case 0 diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Set.thy --- a/src/HOL/Set.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Set.thy Tue Jan 31 14:05:16 2023 +0000 @@ -952,7 +952,7 @@ lemma image_add_0 [simp]: "(+) (0::'a::comm_monoid_add) ` S = S" by auto -theorem Cantors_paradox: "\f. f ` A = Pow A" +theorem Cantors_theorem: "\f. f ` A = Pow A" proof assume "\f. f ` A = Pow A" then obtain f where f: "f ` A = Pow A" .. @@ -1363,7 +1363,7 @@ lemma Diff_Int2: "A \ C - B \ C = A \ C - B" by blast -lemma subset_UnE: +lemma subset_UnE: assumes "C \ A \ B" obtains A' B' where "A' \ A" "B' \ B" "C = A' \ B'" proof diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Topological_Spaces.thy Tue Jan 31 14:05:16 2023 +0000 @@ -720,6 +720,24 @@ using linordered_field_no_lb[rule_format, of x] by (auto simp: eventually_at_left) +lemma filtermap_nhds_eq_imp_filtermap_at_eq: + assumes "filtermap f (nhds z) = nhds (f z)" + assumes "eventually (\x. f x = f z \ x = z) (at z)" + shows "filtermap f (at z) = at (f z)" +proof (rule filter_eqI) + fix P :: "'a \ bool" + have "eventually P (filtermap f (at z)) \ (\\<^sub>F x in nhds z. x \ z \ P (f x))" + by (simp add: eventually_filtermap eventually_at_filter) + also have "\ \ (\\<^sub>F x in nhds z. f x \ f z \ P (f x))" + by (rule eventually_cong [OF assms(2)[unfolded eventually_at_filter]]) auto + also have "\ \ (\\<^sub>F x in filtermap f (nhds z). x \ f z \ P x)" + by (simp add: eventually_filtermap) + also have "filtermap f (nhds z) = nhds (f z)" + by (rule assms) + also have "(\\<^sub>F x in nhds (f z). x \ f z \ P x) \ (\\<^sub>F x in at (f z). P x)" + by (simp add: eventually_at_filter) + finally show "eventually P (filtermap f (at z)) = eventually P (at (f z))" . +qed subsubsection \Tendsto\ @@ -1803,6 +1821,29 @@ by (metis (no_types) f filterlim_compose filterlim_filtermap g tendsto_at_iff_tendsto_nhds tendsto_compose_filtermap) qed +lemma tendsto_nhds_iff: "(f \ (c :: 'a :: t1_space)) (nhds x) \ f \x\ c \ f x = c" +proof safe + assume lim: "(f \ c) (nhds x)" + show "f x = c" + proof (rule ccontr) + assume "f x \ c" + hence "c \ f x" + by auto + then obtain A where A: "open A" "c \ A" "f x \ A" + by (subst (asm) separation_t1) auto + with lim obtain B where "open B" "x \ B" "\x. x \ B \ f x \ A" + unfolding tendsto_def eventually_nhds by metis + with \f x \ A\ show False + by blast + qed + show "(f \ c) (at x)" + using lim by (rule filterlim_mono) (auto simp: at_within_def) +next + assume "f \x\ f x" "c = f x" + thus "(f \ f x) (nhds x)" + unfolding tendsto_def eventually_at_filter by (fast elim: eventually_mono) +qed + subsubsection \Relation of \LIM\ and \LIMSEQ\\ @@ -2289,20 +2330,35 @@ "isCont g (f x) \ continuous (at x within s) f \ continuous (at x within s) (\x. g (f x))" using continuous_at_imp_continuous_at_within continuous_within_compose2 by blast -lemma filtermap_nhds_open_map: +lemma filtermap_nhds_open_map': assumes cont: "isCont f a" - and open_map: "\S. open S \ open (f`S)" + and "open A" "a \ A" + and open_map: "\S. open S \ S \ A \ open (f ` S)" shows "filtermap f (nhds a) = nhds (f a)" unfolding filter_eq_iff proof safe fix P assume "eventually P (filtermap f (nhds a))" - then obtain S where "open S" "a \ S" "\x\S. P (f x)" + then obtain S where S: "open S" "a \ S" "\x\S. P (f x)" by (auto simp: eventually_filtermap eventually_nhds) - then show "eventually P (nhds (f a))" - unfolding eventually_nhds by (intro exI[of _ "f`S"]) (auto intro!: open_map) + show "eventually P (nhds (f a))" + unfolding eventually_nhds + proof (rule exI [of _ "f ` (A \ S)"], safe) + show "open (f ` (A \ S))" + using S by (intro open_Int assms) auto + show "f a \ f ` (A \ S)" + using assms S by auto + show "P (f x)" if "x \ A" "x \ S" for x + using S that by auto + qed qed (metis filterlim_iff tendsto_at_iff_tendsto_nhds isCont_def eventually_filtermap cont) +lemma filtermap_nhds_open_map: + assumes cont: "isCont f a" + and open_map: "\S. open S \ open (f`S)" + shows "filtermap f (nhds a) = nhds (f a)" + using cont filtermap_nhds_open_map' open_map by blast + lemma continuous_at_split: "continuous (at x) f \ continuous (at_left x) f \ continuous (at_right x) f" for x :: "'a::linorder_topology" diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Mon Jan 30 15:24:25 2023 +0000 +++ b/src/HOL/Transcendental.thy Tue Jan 31 14:05:16 2023 +0000 @@ -1531,6 +1531,28 @@ qed qed simp +lemma exp_power_int: + fixes x :: "'a::{real_normed_field,banach}" + shows "exp x powi n = exp (of_int n * x)" +proof (cases "n \ 0") + case True + have "exp x powi n = exp x ^ nat n" + using True by (simp add: power_int_def) + thus ?thesis + using True by (subst (asm) exp_of_nat_mult [symmetric]) auto +next + case False + have "exp x powi n = inverse (exp x ^ nat (-n))" + using False by (simp add: power_int_def field_simps) + also have "exp x ^ nat (-n) = exp (of_nat (nat (-n)) * x)" + using False by (subst exp_of_nat_mult) auto + also have "inverse \ = exp (-(of_nat (nat (-n)) * x))" + by (subst exp_minus) (auto simp: field_simps) + also have "-(of_nat (nat (-n)) * x) = of_int n * x" + using False by simp + finally show ?thesis . +qed + subsubsection \Properties of the Exponential Function on Reals\ @@ -2493,6 +2515,9 @@ lemma powr_realpow: "0 < x \ x powr (real n) = x^n" by (induction n) (simp_all add: ac_simps powr_add) +lemma powr_realpow': "(z :: real) \ 0 \ n \ 0 \ z powr of_nat n = z ^ n" + by (cases "z = 0") (auto simp: powr_realpow) + lemma powr_real_of_int': assumes "x \ 0" "x \ 0 \ n > 0" shows "x powr real_of_int n = power_int x n"