# HG changeset patch # User Manuel Eberl # Date 1744796318 -7200 # Node ID 2886a76359f3af38543855ea74b7bb429e450056 # Parent da14e77a48b2c385b4e7bb415939045454399df6 removed duplicate lemmas diff -r da14e77a48b2 -r 2886a76359f3 src/HOL/Analysis/Gamma_Function.thy --- a/src/HOL/Analysis/Gamma_Function.thy Tue Apr 15 17:38:20 2025 +0200 +++ b/src/HOL/Analysis/Gamma_Function.thy Wed Apr 16 11:38:38 2025 +0200 @@ -2096,7 +2096,7 @@ } note lim = this from assms double_in_nonpos_Ints_imp[of z] have z': "2 * z \ \\<^sub>\\<^sub>0" by auto - from fraction_not_in_ints[of 2 1] have "(1/2 :: 'a) \ \\<^sub>\\<^sub>0" + from fraction_not_in_Ints[of 2 1] have "(1/2 :: 'a) \ \\<^sub>\\<^sub>0" by (intro not_in_Ints_imp_not_in_nonpos_Ints) simp_all with lim[of "1/2 :: 'a"] have "?h \ 2 * Gamma (1/2 :: 'a)" by (simp add: exp_of_real) from LIMSEQ_unique[OF this lim[OF assms]] z' show ?thesis @@ -2388,9 +2388,9 @@ case True with that have "z = 0 \ z = 1" by (force elim!: Ints_cases) moreover have "g 0 * g (1/2) = Gamma (1/2)^2 * g 0" - using fraction_not_in_ints[where 'a = complex, of 2 1] by (simp add: g_def power2_eq_square) + using fraction_not_in_Ints[where 'a = complex, of 2 1] by (simp add: g_def power2_eq_square) moreover have "g (1/2) * g 1 = Gamma (1/2)^2 * g 1" - using fraction_not_in_ints[where 'a = complex, of 2 1] + using fraction_not_in_Ints[where 'a = complex, of 2 1] by (simp add: g_def power2_eq_square Beta_def algebra_simps) ultimately show ?thesis by force next @@ -2457,7 +2457,7 @@ by (subst (1 2) g_eq[symmetric]) simp from DERIV_cmult[OF this, of "inverse ((Gamma (1/2))^2)"] have "(g has_field_derivative (g z * ((h (z/2) + h ((z+1)/2))/2))) (at z)" - using fraction_not_in_ints[where 'a = complex, of 2 1] + using fraction_not_in_Ints[where 'a = complex, of 2 1] by (simp add: divide_simps Gamma_eq_zero_iff not_in_Ints_imp_not_in_nonpos_Ints) moreover have "(g has_field_derivative (g z * h z)) (at z)" using g_g'[of z] by (simp add: ac_simps) @@ -2596,7 +2596,7 @@ lemma Gamma_one_half_real: "Gamma (1/2 :: real) = sqrt pi" proof - - from Gamma_reflection_complex[of "1/2"] fraction_not_in_ints[where 'a = complex, of 2 1] + from Gamma_reflection_complex[of "1/2"] fraction_not_in_Ints[where 'a = complex, of 2 1] have "Gamma (1/2 :: complex)^2 = of_real pi" by (simp add: power2_eq_square) hence "of_real pi = Gamma (complex_of_real (1/2))^2" by simp also have "\ = of_real ((Gamma (1/2))^2)" by (subst Gamma_complex_of_real) simp_all diff -r da14e77a48b2 -r 2886a76359f3 src/HOL/Library/Nonpos_Ints.thy --- a/src/HOL/Library/Nonpos_Ints.thy Tue Apr 15 17:38:20 2025 +0200 +++ b/src/HOL/Library/Nonpos_Ints.thy Wed Apr 16 11:38:38 2025 +0200 @@ -329,19 +329,7 @@ finally show ?thesis . qed -lemma fraction_not_in_ints: - assumes "\(n dvd m)" "n \ 0" - shows "of_int m / of_int n \ (\ :: 'a :: {division_ring,ring_char_0} set)" -proof - assume "of_int m / (of_int n :: 'a) \ \" - then obtain k where "of_int m / of_int n = (of_int k :: 'a)" by (elim Ints_cases) - with assms have "of_int m = (of_int (k * n) :: 'a)" by (auto simp add: field_split_simps) - hence "m = k * n" by (subst (asm) of_int_eq_iff) - hence "n dvd m" by simp - with assms(1) show False by contradiction -qed - -lemma fraction_not_in_nats: +lemma fraction_not_in_Nats: assumes "\n dvd m" "n \ 0" shows "of_int m / of_int n \ (\ :: 'a :: {division_ring,ring_char_0} set)" proof @@ -349,7 +337,7 @@ also note Nats_subset_Ints finally have "of_int m / of_int n \ (\ :: 'a set)" . moreover have "of_int m / of_int n \ (\ :: 'a set)" - using assms by (intro fraction_not_in_ints) + using assms by (intro fraction_not_in_Ints) ultimately show False by contradiction qed @@ -369,7 +357,7 @@ \ (numeral b :: int) dvd numeral a" (is "?L=?R") proof show "?L \ ?R" - by (metis fraction_not_in_ints of_int_numeral zero_neq_numeral) + by (metis fraction_not_in_Ints of_int_numeral zero_neq_numeral) assume ?R then obtain k::int where "numeral a = numeral b * (of_int k :: 'a)" unfolding dvd_def by (metis of_int_mult of_int_numeral)