diff --git a/src/HOL/Complex.thy b/src/HOL/Complex.thy --- a/src/HOL/Complex.thy +++ b/src/HOL/Complex.thy @@ -1,1335 +1,1315 @@ (* Title: HOL/Complex.thy Author: Jacques D. Fleuriot, 2001 University of Edinburgh Author: Lawrence C Paulson, 2003/4 *) section \Complex Numbers: Rectangular and Polar Representations\ theory Complex imports Transcendental begin text \ We use the \<^theory_text>\codatatype\ command to define the type of complex numbers. This allows us to use \<^theory_text>\primcorec\ to define complex functions by defining their real and imaginary result separately. \ codatatype complex = Complex (Re: real) (Im: real) lemma complex_surj: "Complex (Re z) (Im z) = z" by (rule complex.collapse) lemma complex_eqI [intro?]: "Re x = Re y \ Im x = Im y \ x = y" by (rule complex.expand) simp lemma complex_eq_iff: "x = y \ Re x = Re y \ Im x = Im y" by (auto intro: complex.expand) subsection \Addition and Subtraction\ instantiation complex :: ab_group_add begin primcorec zero_complex where "Re 0 = 0" | "Im 0 = 0" primcorec plus_complex where "Re (x + y) = Re x + Re y" | "Im (x + y) = Im x + Im y" primcorec uminus_complex where "Re (- x) = - Re x" | "Im (- x) = - Im x" primcorec minus_complex where "Re (x - y) = Re x - Re y" | "Im (x - y) = Im x - Im y" instance by standard (simp_all add: complex_eq_iff) end subsection \Multiplication and Division\ instantiation complex :: field begin primcorec one_complex where "Re 1 = 1" | "Im 1 = 0" primcorec times_complex where "Re (x * y) = Re x * Re y - Im x * Im y" | "Im (x * y) = Re x * Im y + Im x * Re y" primcorec inverse_complex where "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" definition "x div y = x * inverse y" for x y :: complex instance by standard (simp_all add: complex_eq_iff divide_complex_def distrib_left distrib_right right_diff_distrib left_diff_distrib power2_eq_square add_divide_distrib [symmetric]) end lemma Re_divide: "Re (x / y) = (Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)" by (simp add: divide_complex_def add_divide_distrib) lemma Im_divide: "Im (x / y) = (Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)" by (simp add: divide_complex_def diff_divide_distrib) lemma Complex_divide: "(x / y) = Complex ((Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)) ((Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2))" by (metis Im_divide Re_divide complex_surj) lemma Re_power2: "Re (x ^ 2) = (Re x)^2 - (Im x)^2" by (simp add: power2_eq_square) lemma Im_power2: "Im (x ^ 2) = 2 * Re x * Im x" by (simp add: power2_eq_square) lemma Re_power_real [simp]: "Im x = 0 \ Re (x ^ n) = Re x ^ n " by (induct n) simp_all lemma Im_power_real [simp]: "Im x = 0 \ Im (x ^ n) = 0" by (induct n) simp_all subsection \Scalar Multiplication\ instantiation complex :: real_field begin primcorec scaleR_complex where "Re (scaleR r x) = r * Re x" | "Im (scaleR r x) = r * Im x" instance proof fix a b :: real and x y :: complex show "scaleR a (x + y) = scaleR a x + scaleR a y" by (simp add: complex_eq_iff distrib_left) show "scaleR (a + b) x = scaleR a x + scaleR b x" by (simp add: complex_eq_iff distrib_right) show "scaleR a (scaleR b x) = scaleR (a * b) x" by (simp add: complex_eq_iff mult.assoc) show "scaleR 1 x = x" by (simp add: complex_eq_iff) show "scaleR a x * y = scaleR a (x * y)" by (simp add: complex_eq_iff algebra_simps) show "x * scaleR a y = scaleR a (x * y)" by (simp add: complex_eq_iff algebra_simps) qed end subsection \Numerals, Arithmetic, and Embedding from R\ abbreviation complex_of_real :: "real \ complex" where "complex_of_real \ of_real" declare [[coercion "of_real :: real \ complex"]] declare [[coercion "of_rat :: rat \ complex"]] declare [[coercion "of_int :: int \ complex"]] declare [[coercion "of_nat :: nat \ complex"]] lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n" by (induct n) simp_all lemma complex_Im_of_nat [simp]: "Im (of_nat n) = 0" by (induct n) simp_all lemma complex_Re_of_int [simp]: "Re (of_int z) = of_int z" by (cases z rule: int_diff_cases) simp lemma complex_Im_of_int [simp]: "Im (of_int z) = 0" by (cases z rule: int_diff_cases) simp lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v" using complex_Re_of_int [of "numeral v"] by simp lemma complex_Im_numeral [simp]: "Im (numeral v) = 0" using complex_Im_of_int [of "numeral v"] by simp lemma Re_complex_of_real [simp]: "Re (complex_of_real z) = z" by (simp add: of_real_def) lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0" by (simp add: of_real_def) lemma Re_divide_numeral [simp]: "Re (z / numeral w) = Re z / numeral w" by (simp add: Re_divide sqr_conv_mult) lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w" by (simp add: Im_divide sqr_conv_mult) lemma Re_divide_of_nat [simp]: "Re (z / of_nat n) = Re z / of_nat n" by (cases n) (simp_all add: Re_divide field_split_simps power2_eq_square del: of_nat_Suc) lemma Im_divide_of_nat [simp]: "Im (z / of_nat n) = Im z / of_nat n" by (cases n) (simp_all add: Im_divide field_split_simps power2_eq_square del: of_nat_Suc) lemma of_real_Re [simp]: "z \ \ \ of_real (Re z) = z" by (auto simp: Reals_def) lemma complex_Re_fact [simp]: "Re (fact n) = fact n" proof - have "(fact n :: complex) = of_real (fact n)" by simp also have "Re \ = fact n" by (subst Re_complex_of_real) simp_all finally show ?thesis . qed lemma complex_Im_fact [simp]: "Im (fact n) = 0" by (subst of_nat_fact [symmetric]) (simp only: complex_Im_of_nat) lemma Re_prod_Reals: "(\x. x \ A \ f x \ \) \ Re (prod f A) = prod (\x. Re (f x)) A" proof (induction A rule: infinite_finite_induct) case (insert x A) hence "Re (prod f (insert x A)) = Re (f x) * Re (prod f A) - Im (f x) * Im (prod f A)" by simp also from insert.prems have "f x \ \" by simp hence "Im (f x) = 0" by (auto elim!: Reals_cases) also have "Re (prod f A) = (\x\A. Re (f x))" by (intro insert.IH insert.prems) auto finally show ?case using insert.hyps by simp qed auto subsection \The Complex Number $i$\ primcorec imaginary_unit :: complex ("\") where "Re \ = 0" | "Im \ = 1" lemma Complex_eq: "Complex a b = a + \ * b" by (simp add: complex_eq_iff) lemma complex_eq: "a = Re a + \ * Im a" by (simp add: complex_eq_iff) lemma fun_complex_eq: "f = (\x. Re (f x) + \ * Im (f x))" by (simp add: fun_eq_iff complex_eq) lemma i_squared [simp]: "\ * \ = -1" by (simp add: complex_eq_iff) lemma power2_i [simp]: "\\<^sup>2 = -1" by (simp add: power2_eq_square) lemma inverse_i [simp]: "inverse \ = - \" by (rule inverse_unique) simp lemma divide_i [simp]: "x / \ = - \ * x" by (simp add: divide_complex_def) lemma complex_i_mult_minus [simp]: "\ * (\ * x) = - x" by (simp add: mult.assoc [symmetric]) lemma complex_i_not_zero [simp]: "\ \ 0" by (simp add: complex_eq_iff) lemma complex_i_not_one [simp]: "\ \ 1" by (simp add: complex_eq_iff) lemma complex_i_not_numeral [simp]: "\ \ numeral w" by (simp add: complex_eq_iff) lemma complex_i_not_neg_numeral [simp]: "\ \ - numeral w" by (simp add: complex_eq_iff) lemma complex_split_polar: "\r a. z = complex_of_real r * (cos a + \ * sin a)" by (simp add: complex_eq_iff polar_Ex) lemma i_even_power [simp]: "\ ^ (n * 2) = (-1) ^ n" by (metis mult.commute power2_i power_mult) lemma Re_i_times [simp]: "Re (\ * z) = - Im z" by simp lemma Im_i_times [simp]: "Im (\ * z) = Re z" by simp lemma i_times_eq_iff: "\ * w = z \ w = - (\ * z)" by auto lemma divide_numeral_i [simp]: "z / (numeral n * \) = - (\ * z) / numeral n" by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right) lemma imaginary_eq_real_iff [simp]: assumes "y \ Reals" "x \ Reals" shows "\ * y = x \ x=0 \ y=0" - using assms - unfolding Reals_def - apply clarify - apply (rule iffI) - apply (metis Im_complex_of_real Im_i_times Re_complex_of_real mult_eq_0_iff of_real_0) - by simp + by (metis Im_complex_of_real Im_i_times assms mult_zero_right of_real_0 of_real_Re) lemma real_eq_imaginary_iff [simp]: assumes "y \ Reals" "x \ Reals" shows "x = \ * y \ x=0 \ y=0" using assms imaginary_eq_real_iff by fastforce subsection \Vector Norm\ instantiation complex :: real_normed_field begin definition "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)" abbreviation cmod :: "complex \ real" where "cmod \ norm" definition complex_sgn_def: "sgn x = x /\<^sub>R cmod x" definition dist_complex_def: "dist x y = cmod (x - y)" definition uniformity_complex_def [code del]: "(uniformity :: (complex \ complex) filter) = (INF e\{0 <..}. principal {(x, y). dist x y < e})" definition open_complex_def [code del]: "open (U :: complex set) \ (\x\U. eventually (\(x', y). x' = x \ y \ U) uniformity)" instance proof fix r :: real and x y :: complex and S :: "complex set" show "(norm x = 0) = (x = 0)" by (simp add: norm_complex_def complex_eq_iff) show "norm (x + y) \ norm x + norm y" by (simp add: norm_complex_def complex_eq_iff real_sqrt_sum_squares_triangle_ineq) show "norm (scaleR r x) = \r\ * norm x" by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric] real_sqrt_mult) show "norm (x * y) = norm x * norm y" by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric] power2_eq_square algebra_simps) qed (rule complex_sgn_def dist_complex_def open_complex_def uniformity_complex_def)+ end declare uniformity_Abort[where 'a = complex, code] lemma norm_ii [simp]: "norm \ = 1" by (simp add: norm_complex_def) lemma cmod_unit_one: "cmod (cos a + \ * sin a) = 1" by (simp add: norm_complex_def) lemma cmod_complex_polar: "cmod (r * (cos a + \ * sin a)) = \r\" by (simp add: norm_mult cmod_unit_one) lemma complex_Re_le_cmod: "Re x \ cmod x" unfolding norm_complex_def by (rule real_sqrt_sum_squares_ge1) lemma complex_mod_minus_le_complex_mod: "- cmod x \ cmod x" by (rule order_trans [OF _ norm_ge_zero]) simp lemma complex_mod_triangle_ineq2: "cmod (b + a) - cmod b \ cmod a" by (rule ord_le_eq_trans [OF norm_triangle_ineq2]) simp lemma abs_Re_le_cmod: "\Re x\ \ cmod x" by (simp add: norm_complex_def) lemma abs_Im_le_cmod: "\Im x\ \ cmod x" by (simp add: norm_complex_def) lemma cmod_le: "cmod z \ \Re z\ + \Im z\" - apply (subst complex_eq) - apply (rule order_trans) - apply (rule norm_triangle_ineq) - apply (simp add: norm_mult) - done + using norm_complex_def sqrt_sum_squares_le_sum_abs by presburger lemma cmod_eq_Re: "Im z = 0 \ cmod z = \Re z\" by (simp add: norm_complex_def) lemma cmod_eq_Im: "Re z = 0 \ cmod z = \Im z\" by (simp add: norm_complex_def) lemma cmod_power2: "(cmod z)\<^sup>2 = (Re z)\<^sup>2 + (Im z)\<^sup>2" by (simp add: norm_complex_def) lemma cmod_plus_Re_le_0_iff: "cmod z + Re z \ 0 \ Re z = - cmod z" using abs_Re_le_cmod[of z] by auto lemma cmod_Re_le_iff: "Im x = Im y \ cmod x \ cmod y \ \Re x\ \ \Re y\" by (metis add.commute add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff) lemma cmod_Im_le_iff: "Re x = Re y \ cmod x \ cmod y \ \Im x\ \ \Im y\" by (metis add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff) lemma Im_eq_0: "\Re z\ = cmod z \ Im z = 0" by (subst (asm) power_eq_iff_eq_base[symmetric, where n=2]) (auto simp add: norm_complex_def) lemma abs_sqrt_wlog: "(\x. x \ 0 \ P x (x\<^sup>2)) \ P \x\ (x\<^sup>2)" for x::"'a::linordered_idom" by (metis abs_ge_zero power2_abs) lemma complex_abs_le_norm: "\Re z\ + \Im z\ \ sqrt 2 * norm z" unfolding norm_complex_def apply (rule abs_sqrt_wlog [where x="Re z"]) apply (rule abs_sqrt_wlog [where x="Im z"]) apply (rule power2_le_imp_le) apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric]) done lemma complex_unit_circle: "z \ 0 \ (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1" by (simp add: norm_complex_def complex_eq_iff power2_eq_square add_divide_distrib [symmetric]) text \Properties of complex signum.\ lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult.commute) lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z" by (simp add: complex_sgn_def divide_inverse) lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z" by (simp add: complex_sgn_def divide_inverse) subsection \Absolute value\ + instantiation complex :: field_abs_sgn begin definition abs_complex :: "complex \ complex" where "abs_complex = of_real \ norm" instance - apply standard - apply (auto simp add: abs_complex_def complex_sgn_def norm_mult) - apply (auto simp add: scaleR_conv_of_real field_simps) - done - + proof qed (auto simp add: abs_complex_def complex_sgn_def norm_divide norm_mult scaleR_conv_of_real field_simps) end subsection \Completeness of the Complexes\ lemma bounded_linear_Re: "bounded_linear Re" by (rule bounded_linear_intro [where K=1]) (simp_all add: norm_complex_def) lemma bounded_linear_Im: "bounded_linear Im" by (rule bounded_linear_intro [where K=1]) (simp_all add: norm_complex_def) lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re] lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im] lemmas tendsto_Re [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Re] lemmas tendsto_Im [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im] lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re] lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im] lemmas continuous_Re [simp] = bounded_linear.continuous [OF bounded_linear_Re] lemmas continuous_Im [simp] = bounded_linear.continuous [OF bounded_linear_Im] lemmas continuous_on_Re [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Re] lemmas continuous_on_Im [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im] lemmas has_derivative_Re [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Re] lemmas has_derivative_Im [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im] lemmas sums_Re = bounded_linear.sums [OF bounded_linear_Re] lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im] +lemmas Re_suminf = bounded_linear.suminf[OF bounded_linear_Re] +lemmas Im_suminf = bounded_linear.suminf[OF bounded_linear_Im] lemma tendsto_Complex [tendsto_intros]: "(f \ a) F \ (g \ b) F \ ((\x. Complex (f x) (g x)) \ Complex a b) F" unfolding Complex_eq by (auto intro!: tendsto_intros) lemma tendsto_complex_iff: "(f \ x) F \ (((\x. Re (f x)) \ Re x) F \ ((\x. Im (f x)) \ Im x) F)" proof safe assume "((\x. Re (f x)) \ Re x) F" "((\x. Im (f x)) \ Im x) F" from tendsto_Complex[OF this] show "(f \ x) F" unfolding complex.collapse . qed (auto intro: tendsto_intros) lemma continuous_complex_iff: "continuous F f \ continuous F (\x. Re (f x)) \ continuous F (\x. Im (f x))" by (simp only: continuous_def tendsto_complex_iff) lemma continuous_on_of_real_o_iff [simp]: "continuous_on S (\x. complex_of_real (g x)) = continuous_on S g" using continuous_on_Re continuous_on_of_real by fastforce lemma continuous_on_of_real_id [simp]: "continuous_on S (of_real :: real \ 'a::real_normed_algebra_1)" by (rule continuous_on_of_real [OF continuous_on_id]) lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \ ((\x. Re (f x)) has_field_derivative (Re x)) F \ ((\x. Im (f x)) has_field_derivative (Im x)) F" by (simp add: has_vector_derivative_def has_field_derivative_def has_derivative_def tendsto_complex_iff algebra_simps bounded_linear_scaleR_left bounded_linear_mult_right) lemma has_field_derivative_Re[derivative_intros]: "(f has_vector_derivative D) F \ ((\x. Re (f x)) has_field_derivative (Re D)) F" unfolding has_vector_derivative_complex_iff by safe lemma has_field_derivative_Im[derivative_intros]: "(f has_vector_derivative D) F \ ((\x. Im (f x)) has_field_derivative (Im D)) F" unfolding has_vector_derivative_complex_iff by safe instance complex :: banach proof fix X :: "nat \ complex" assume X: "Cauchy X" then have "(\n. Complex (Re (X n)) (Im (X n))) \ Complex (lim (\n. Re (X n))) (lim (\n. Im (X n)))" by (intro tendsto_Complex convergent_LIMSEQ_iff[THEN iffD1] Cauchy_convergent_iff[THEN iffD1] Cauchy_Re Cauchy_Im) then show "convergent X" unfolding complex.collapse by (rule convergentI) qed declare DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros] subsection \Complex Conjugation\ primcorec cnj :: "complex \ complex" where "Re (cnj z) = Re z" | "Im (cnj z) = - Im z" lemma complex_cnj_cancel_iff [simp]: "cnj x = cnj y \ x = y" by (simp add: complex_eq_iff) lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z" by (simp add: complex_eq_iff) lemma complex_cnj_zero [simp]: "cnj 0 = 0" by (simp add: complex_eq_iff) lemma complex_cnj_zero_iff [iff]: "cnj z = 0 \ z = 0" by (simp add: complex_eq_iff) lemma complex_cnj_one_iff [simp]: "cnj z = 1 \ z = 1" by (simp add: complex_eq_iff) lemma complex_cnj_add [simp]: "cnj (x + y) = cnj x + cnj y" by (simp add: complex_eq_iff) lemma cnj_sum [simp]: "cnj (sum f s) = (\x\s. cnj (f x))" by (induct s rule: infinite_finite_induct) auto lemma complex_cnj_diff [simp]: "cnj (x - y) = cnj x - cnj y" by (simp add: complex_eq_iff) lemma complex_cnj_minus [simp]: "cnj (- x) = - cnj x" by (simp add: complex_eq_iff) lemma complex_cnj_one [simp]: "cnj 1 = 1" by (simp add: complex_eq_iff) lemma complex_cnj_mult [simp]: "cnj (x * y) = cnj x * cnj y" by (simp add: complex_eq_iff) lemma cnj_prod [simp]: "cnj (prod f s) = (\x\s. cnj (f x))" by (induct s rule: infinite_finite_induct) auto lemma complex_cnj_inverse [simp]: "cnj (inverse x) = inverse (cnj x)" by (simp add: complex_eq_iff) lemma complex_cnj_divide [simp]: "cnj (x / y) = cnj x / cnj y" by (simp add: divide_complex_def) lemma complex_cnj_power [simp]: "cnj (x ^ n) = cnj x ^ n" by (induct n) simp_all lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n" by (simp add: complex_eq_iff) lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z" by (simp add: complex_eq_iff) lemma complex_cnj_numeral [simp]: "cnj (numeral w) = numeral w" by (simp add: complex_eq_iff) lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w" by (simp add: complex_eq_iff) lemma complex_cnj_scaleR [simp]: "cnj (scaleR r x) = scaleR r (cnj x)" by (simp add: complex_eq_iff) lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" by (simp add: norm_complex_def) lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x" by (simp add: complex_eq_iff) lemma complex_cnj_i [simp]: "cnj \ = - \" by (simp add: complex_eq_iff) lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)" by (simp add: complex_eq_iff) lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * \" by (simp add: complex_eq_iff) lemma Ints_cnj [intro]: "x \ \ \ cnj x \ \" by (auto elim!: Ints_cases) lemma cnj_in_Ints_iff [simp]: "cnj x \ \ \ x \ \" using Ints_cnj[of x] Ints_cnj[of "cnj x"] by auto lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<^sup>2 + (Im z)\<^sup>2)" by (simp add: complex_eq_iff power2_eq_square) lemma cnj_add_mult_eq_Re: "z * cnj w + cnj z * w = 2 * Re (z * cnj w)" by (rule complex_eqI) auto lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<^sup>2" by (simp add: norm_mult power2_eq_square) lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" by (simp add: norm_complex_def power2_eq_square) lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0" by simp lemma complex_cnj_fact [simp]: "cnj (fact n) = fact n" by (subst of_nat_fact [symmetric], subst complex_cnj_of_nat) simp lemma complex_cnj_pochhammer [simp]: "cnj (pochhammer z n) = pochhammer (cnj z) n" by (induct n arbitrary: z) (simp_all add: pochhammer_rec) lemma bounded_linear_cnj: "bounded_linear cnj" using complex_cnj_add complex_cnj_scaleR by (rule bounded_linear_intro [where K=1]) simp lemma linear_cnj: "linear cnj" using bounded_linear.linear[OF bounded_linear_cnj] . lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj] and isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj] and continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj] and continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj] and has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj] lemma lim_cnj: "((\x. cnj(f x)) \ cnj l) F \ (f \ l) F" by (simp add: tendsto_iff dist_complex_def complex_cnj_diff [symmetric] del: complex_cnj_diff) lemma sums_cnj: "((\x. cnj(f x)) sums cnj l) \ (f sums l)" by (simp add: sums_def lim_cnj cnj_sum [symmetric] del: cnj_sum) lemma differentiable_cnj_iff: "(\z. cnj (f z)) differentiable at x within A \ f differentiable at x within A" proof assume "(\z. cnj (f z)) differentiable at x within A" then obtain D where "((\z. cnj (f z)) has_derivative D) (at x within A)" by (auto simp: differentiable_def) from has_derivative_cnj[OF this] show "f differentiable at x within A" by (auto simp: differentiable_def) next assume "f differentiable at x within A" then obtain D where "(f has_derivative D) (at x within A)" by (auto simp: differentiable_def) from has_derivative_cnj[OF this] show "(\z. cnj (f z)) differentiable at x within A" by (auto simp: differentiable_def) qed lemma has_vector_derivative_cnj [derivative_intros]: assumes "(f has_vector_derivative f') (at z within A)" shows "((\z. cnj (f z)) has_vector_derivative cnj f') (at z within A)" using assms by (auto simp: has_vector_derivative_complex_iff intro: derivative_intros) subsection \Basic Lemmas\ lemma complex_of_real_code[code_unfold]: "of_real = (\x. Complex x 0)" by (intro ext, auto simp: complex_eq_iff) lemma complex_eq_0: "z=0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0" by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff) lemma complex_neq_0: "z\0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0" by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff) lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z" by (cases z) (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric] simp del: of_real_power) lemma complex_div_cnj: "a / b = (a * cnj b) / (norm b)\<^sup>2" using complex_norm_square by auto lemma Re_complex_div_eq_0: "Re (a / b) = 0 \ Re (a * cnj b) = 0" by (auto simp add: Re_divide) lemma Im_complex_div_eq_0: "Im (a / b) = 0 \ Im (a * cnj b) = 0" by (auto simp add: Im_divide) lemma complex_div_gt_0: "(Re (a / b) > 0 \ Re (a * cnj b) > 0) \ (Im (a / b) > 0 \ Im (a * cnj b) > 0)" proof (cases "b = 0") case True then show ?thesis by auto next case False then have "0 < (Re b)\<^sup>2 + (Im b)\<^sup>2" by (simp add: complex_eq_iff sum_power2_gt_zero_iff) then show ?thesis by (simp add: Re_divide Im_divide zero_less_divide_iff) qed lemma Re_complex_div_gt_0: "Re (a / b) > 0 \ Re (a * cnj b) > 0" and Im_complex_div_gt_0: "Im (a / b) > 0 \ Im (a * cnj b) > 0" using complex_div_gt_0 by auto lemma Re_complex_div_ge_0: "Re (a / b) \ 0 \ Re (a * cnj b) \ 0" by (metis le_less Re_complex_div_eq_0 Re_complex_div_gt_0) lemma Im_complex_div_ge_0: "Im (a / b) \ 0 \ Im (a * cnj b) \ 0" by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 le_less) lemma Re_complex_div_lt_0: "Re (a / b) < 0 \ Re (a * cnj b) < 0" by (metis less_asym neq_iff Re_complex_div_eq_0 Re_complex_div_gt_0) lemma Im_complex_div_lt_0: "Im (a / b) < 0 \ Im (a * cnj b) < 0" by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 less_asym neq_iff) lemma Re_complex_div_le_0: "Re (a / b) \ 0 \ Re (a * cnj b) \ 0" by (metis not_le Re_complex_div_gt_0) lemma Im_complex_div_le_0: "Im (a / b) \ 0 \ Im (a * cnj b) \ 0" by (metis Im_complex_div_gt_0 not_le) lemma Re_divide_of_real [simp]: "Re (z / of_real r) = Re z / r" by (simp add: Re_divide power2_eq_square) lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r" by (simp add: Im_divide power2_eq_square) lemma Re_divide_Reals [simp]: "r \ \ \ Re (z / r) = Re z / Re r" by (metis Re_divide_of_real of_real_Re) lemma Im_divide_Reals [simp]: "r \ \ \ Im (z / r) = Im z / Re r" by (metis Im_divide_of_real of_real_Re) lemma Re_sum[simp]: "Re (sum f s) = (\x\s. Re (f x))" by (induct s rule: infinite_finite_induct) auto lemma Im_sum[simp]: "Im (sum f s) = (\x\s. Im(f x))" by (induct s rule: infinite_finite_induct) auto lemma sum_Re_le_cmod: "(\i\I. Re (z i)) \ cmod (\i\I. z i)" by (metis Re_sum complex_Re_le_cmod) lemma sum_Im_le_cmod: "(\i\I. Im (z i)) \ cmod (\i\I. z i)" by (smt (verit, best) Im_sum abs_Im_le_cmod sum.cong) lemma sums_complex_iff: "f sums x \ ((\x. Re (f x)) sums Re x) \ ((\x. Im (f x)) sums Im x)" unfolding sums_def tendsto_complex_iff Im_sum Re_sum .. lemma summable_complex_iff: "summable f \ summable (\x. Re (f x)) \ summable (\x. Im (f x))" unfolding summable_def sums_complex_iff[abs_def] by (metis complex.sel) lemma summable_complex_of_real [simp]: "summable (\n. complex_of_real (f n)) \ summable f" unfolding summable_complex_iff by simp lemma summable_Re: "summable f \ summable (\x. Re (f x))" unfolding summable_complex_iff by blast lemma summable_Im: "summable f \ summable (\x. Im (f x))" unfolding summable_complex_iff by blast lemma complex_is_Nat_iff: "z \ \ \ Im z = 0 \ (\i. Re z = of_nat i)" by (auto simp: Nats_def complex_eq_iff) lemma complex_is_Int_iff: "z \ \ \ Im z = 0 \ (\i. Re z = of_int i)" by (auto simp: Ints_def complex_eq_iff) lemma complex_is_Real_iff: "z \ \ \ Im z = 0" by (auto simp: Reals_def complex_eq_iff) lemma Reals_cnj_iff: "z \ \ \ cnj z = z" by (auto simp: complex_is_Real_iff complex_eq_iff) lemma in_Reals_norm: "z \ \ \ norm z = \Re z\" by (simp add: complex_is_Real_iff norm_complex_def) lemma Re_Reals_divide: "r \ \ \ Re (r / z) = Re r * Re z / (norm z)\<^sup>2" by (simp add: Re_divide complex_is_Real_iff cmod_power2) lemma Im_Reals_divide: "r \ \ \ Im (r / z) = -Re r * Im z / (norm z)\<^sup>2" by (simp add: Im_divide complex_is_Real_iff cmod_power2) lemma series_comparison_complex: fixes f:: "nat \ 'a::banach" assumes sg: "summable g" and "\n. g n \ \" "\n. Re (g n) \ 0" and fg: "\n. n \ N \ norm(f n) \ norm(g n)" shows "summable f" proof - have g: "\n. cmod (g n) = Re (g n)" using assms by (metis abs_of_nonneg in_Reals_norm) show ?thesis - apply (rule summable_comparison_test' [where g = "\n. norm (g n)" and N=N]) - using sg - apply (auto simp: summable_def) - apply (rule_tac x = "Re s" in exI) - apply (auto simp: g sums_Re) - apply (metis fg g) - done + by (metis fg g sg summable_comparison_test summable_complex_iff) qed subsection \Polar Form for Complex Numbers\ lemma complex_unimodular_polar: assumes "norm z = 1" obtains t where "0 \ t" "t < 2 * pi" "z = Complex (cos t) (sin t)" by (metis cmod_power2 one_power2 complex_surj sincos_total_2pi [of "Re z" "Im z"] assms) subsubsection \$\cos \theta + i \sin \theta$\ primcorec cis :: "real \ complex" where "Re (cis a) = cos a" | "Im (cis a) = sin a" lemma cis_zero [simp]: "cis 0 = 1" by (simp add: complex_eq_iff) lemma norm_cis [simp]: "norm (cis a) = 1" by (simp add: norm_complex_def) lemma sgn_cis [simp]: "sgn (cis a) = cis a" by (simp add: sgn_div_norm) lemma cis_2pi [simp]: "cis (2 * pi) = 1" by (simp add: cis.ctr complex_eq_iff) lemma cis_neq_zero [simp]: "cis a \ 0" by (metis norm_cis norm_zero zero_neq_one) lemma cis_cnj: "cnj (cis t) = cis (-t)" by (simp add: complex_eq_iff) lemma cis_mult: "cis a * cis b = cis (a + b)" by (simp add: complex_eq_iff cos_add sin_add) lemma DeMoivre: "(cis a) ^ n = cis (real n * a)" by (induct n) (simp_all add: algebra_simps cis_mult) lemma cis_inverse [simp]: "inverse (cis a) = cis (- a)" by (simp add: complex_eq_iff) lemma cis_divide: "cis a / cis b = cis (a - b)" by (simp add: divide_complex_def cis_mult) lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re (cis a ^ n)" by (auto simp add: DeMoivre) lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im (cis a ^ n)" by (auto simp add: DeMoivre) lemma cis_pi [simp]: "cis pi = -1" by (simp add: complex_eq_iff) lemma cis_pi_half[simp]: "cis (pi / 2) = \" by (simp add: cis.ctr complex_eq_iff) lemma cis_minus_pi_half[simp]: "cis (-(pi / 2)) = -\" by (simp add: cis.ctr complex_eq_iff) lemma cis_multiple_2pi[simp]: "n \ \ \ cis (2 * pi * n) = 1" by (auto elim!: Ints_cases simp: cis.ctr one_complex.ctr) subsubsection \$r(\cos \theta + i \sin \theta)$\ definition rcis :: "real \ real \ complex" where "rcis r a = complex_of_real r * cis a" lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" by (simp add: rcis_def) lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a" by (simp add: rcis_def) lemma rcis_Ex: "\r a. z = rcis r a" by (simp add: complex_eq_iff polar_Ex) lemma complex_mod_rcis [simp]: "cmod (rcis r a) = \r\" by (simp add: rcis_def norm_mult) lemma cis_rcis_eq: "cis a = rcis 1 a" by (simp add: rcis_def) lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1 * r2) (a + b)" by (simp add: rcis_def cis_mult) lemma rcis_zero_mod [simp]: "rcis 0 a = 0" by (simp add: rcis_def) lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r" by (simp add: rcis_def) lemma rcis_eq_zero_iff [simp]: "rcis r a = 0 \ r = 0" by (simp add: rcis_def) lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)" by (simp add: rcis_def power_mult_distrib DeMoivre) lemma rcis_inverse: "inverse(rcis r a) = rcis (1 / r) (- a)" by (simp add: divide_inverse rcis_def) lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1 / r2) (a - b)" by (simp add: rcis_def cis_divide [symmetric]) subsubsection \Complex exponential\ lemma exp_Reals_eq: assumes "z \ \" shows "exp z = of_real (exp (Re z))" using assms by (auto elim!: Reals_cases simp: exp_of_real) lemma cis_conv_exp: "cis b = exp (\ * b)" proof - have "(\ * complex_of_real b) ^ n /\<^sub>R fact n = of_real (cos_coeff n * b^n) + \ * of_real (sin_coeff n * b^n)" for n :: nat proof - have "\ ^ n = fact n *\<^sub>R (cos_coeff n + \ * sin_coeff n)" by (induct n) (simp_all add: sin_coeff_Suc cos_coeff_Suc complex_eq_iff Re_divide Im_divide field_simps power2_eq_square add_nonneg_eq_0_iff) then show ?thesis by (simp add: field_simps) qed then show ?thesis using sin_converges [of b] cos_converges [of b] by (auto simp add: Complex_eq cis.ctr exp_def simp del: of_real_mult intro!: sums_unique sums_add sums_mult sums_of_real) qed lemma exp_eq_polar: "exp z = exp (Re z) * cis (Im z)" unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by (cases z) (simp add: Complex_eq) lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)" unfolding exp_eq_polar by simp lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)" unfolding exp_eq_polar by simp lemma norm_cos_sin [simp]: "norm (Complex (cos t) (sin t)) = 1" by (simp add: norm_complex_def) lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)" by (simp add: cis.code cmod_complex_polar exp_eq_polar Complex_eq) lemma complex_exp_exists: "\a r. z = complex_of_real r * exp a" - apply (insert rcis_Ex [of z]) - apply (auto simp add: exp_eq_polar rcis_def mult.assoc [symmetric]) - apply (rule_tac x = "\ * complex_of_real a" in exI) - apply auto - done + using cis_conv_exp rcis_Ex rcis_def by force lemma exp_pi_i [simp]: "exp (of_real pi * \) = -1" by (metis cis_conv_exp cis_pi mult.commute) lemma exp_pi_i' [simp]: "exp (\ * of_real pi) = -1" using cis_conv_exp cis_pi by auto lemma exp_two_pi_i [simp]: "exp (2 * of_real pi * \) = 1" by (simp add: exp_eq_polar complex_eq_iff) lemma exp_two_pi_i' [simp]: "exp (\ * (of_real pi * 2)) = 1" by (metis exp_two_pi_i mult.commute) lemma continuous_on_cis [continuous_intros]: "continuous_on A f \ continuous_on A (\x. cis (f x))" by (auto simp: cis_conv_exp intro!: continuous_intros) subsubsection \Complex argument\ definition Arg :: "complex \ real" where "Arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \ - pi < a \ a \ pi))" lemma Arg_zero: "Arg 0 = 0" by (simp add: Arg_def) lemma cis_Arg_unique: assumes "sgn z = cis x" and "-pi < x" and "x \ pi" shows "Arg z = x" proof - from assms have "z \ 0" by auto have "(SOME a. sgn z = cis a \ -pi < a \ a \ pi) = x" proof fix a define d where "d = a - x" assume a: "sgn z = cis a \ - pi < a \ a \ pi" from a assms have "- (2*pi) < d \ d < 2*pi" unfolding d_def by simp moreover from a assms have "cos a = cos x" and "sin a = sin x" by (simp_all add: complex_eq_iff) then have cos: "cos d = 1" by (simp add: d_def cos_diff) moreover from cos have "sin d = 0" by (rule cos_one_sin_zero) ultimately have "d = 0" by (auto simp: sin_zero_iff elim!: evenE dest!: less_2_cases) then show "a = x" by (simp add: d_def) qed (simp add: assms del: Re_sgn Im_sgn) with \z \ 0\ show "Arg z = x" by (simp add: Arg_def) qed lemma Arg_correct: assumes "z \ 0" shows "sgn z = cis (Arg z) \ -pi < Arg z \ Arg z \ pi" proof (simp add: Arg_def assms, rule someI_ex) obtain r a where z: "z = rcis r a" using rcis_Ex by fast with assms have "r \ 0" by auto define b where "b = (if 0 < r then a else a + pi)" have b: "sgn z = cis b" using \r \ 0\ by (simp add: z b_def rcis_def of_real_def sgn_scaleR sgn_if complex_eq_iff) have cis_2pi_nat: "cis (2 * pi * real_of_nat n) = 1" for n by (induct n) (simp_all add: distrib_left cis_mult [symmetric] complex_eq_iff) have cis_2pi_int: "cis (2 * pi * real_of_int x) = 1" for x by (cases x rule: int_diff_cases) (simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat) define c where "c = b - 2 * pi * of_int \(b - pi) / (2 * pi)\" have "sgn z = cis c" by (simp add: b c_def cis_divide [symmetric] cis_2pi_int) moreover have "- pi < c \ c \ pi" using ceiling_correct [of "(b - pi) / (2*pi)"] by (simp add: c_def less_divide_eq divide_le_eq algebra_simps del: le_of_int_ceiling) ultimately show "\a. sgn z = cis a \ -pi < a \ a \ pi" by fast qed lemma Arg_bounded: "- pi < Arg z \ Arg z \ pi" by (cases "z = 0") (simp_all add: Arg_zero Arg_correct) lemma cis_Arg: "z \ 0 \ cis (Arg z) = sgn z" by (simp add: Arg_correct) lemma rcis_cmod_Arg: "rcis (cmod z) (Arg z) = z" by (cases "z = 0") (simp_all add: rcis_def cis_Arg sgn_div_norm of_real_def) lemma rcis_cnj: shows "cnj a = rcis (cmod a) (- Arg a)" by (metis cis_cnj complex_cnj_complex_of_real complex_cnj_mult rcis_cmod_Arg rcis_def) lemma cos_Arg_i_mult_zero [simp]: "y \ 0 \ Re y = 0 \ cos (Arg y) = 0" using cis_Arg [of y] by (simp add: complex_eq_iff) lemma Arg_ii [simp]: "Arg \ = pi/2" by (rule cis_Arg_unique; simp add: sgn_eq) lemma Arg_minus_ii [simp]: "Arg (-\) = -pi/2" proof (rule cis_Arg_unique) show "sgn (- \) = cis (- pi / 2)" by (simp add: sgn_eq) show "- pi / 2 \ pi" using pi_not_less_zero by linarith qed auto subsection \Complex n-th roots\ lemma bij_betw_roots_unity: assumes "n > 0" shows "bij_betw (\k. cis (2 * pi * real k / real n)) {.. = cis (2*pi*(real k - real l)/n)" using assms by (simp add: field_simps cis_divide) finally have "cos (2*pi*(real k - real l) / n) = 1" by (simp add: complex_eq_iff) then obtain m :: int where "2 * pi * (real k - real l) / real n = real_of_int m * 2 * pi" by (subst (asm) cos_one_2pi_int) blast hence "real_of_int (int k - int l) = real_of_int (m * int n)" unfolding of_int_diff of_int_mult using assms by (simp add: nonzero_divide_eq_eq) also note of_int_eq_iff finally have *: "abs m * n = abs (int k - int l)" by (simp add: abs_mult) also have "\ < int n" using kl by linarith finally have "m = 0" using assms by simp with * show "k = l" by simp qed have subset: "?f ` {.. {z. z ^ n = 1}" proof safe fix k :: nat have "cis (2 * pi * real k / real n) ^ n = cis (2 * pi) ^ k" using assms by (simp add: DeMoivre mult_ac) also have "cis (2 * pi) = 1" by (simp add: complex_eq_iff) finally show "?f k ^ n = 1" by simp qed have "n = card {.. \ card {z::complex. z ^ n = 1}" by (intro card_inj_on_le[OF inj]) (auto simp: finite_roots_unity) finally have card: "card {z::complex. z ^ n = 1} = n" using assms by (intro antisym card_roots_unity) auto have "card (?f ` {.. 0" shows "card {z::complex. z ^ n = 1} = n" using bij_betw_same_card [OF bij_betw_roots_unity [OF assms]] by simp lemma bij_betw_nth_root_unity: fixes c :: complex and n :: nat assumes c: "c \ 0" and n: "n > 0" defines "c' \ root n (norm c) * cis (Arg c / n)" shows "bij_betw (\z. c' * z) {z. z ^ n = 1} {z. z ^ n = c}" proof - have "c' ^ n = of_real (root n (norm c) ^ n) * cis (Arg c)" unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre) also from n have "root n (norm c) ^ n = norm c" by simp also from c have "of_real \ * cis (Arg c) = c" by (simp add: cis_Arg Complex.sgn_eq) finally have [simp]: "c' ^ n = c" . show ?thesis unfolding bij_betw_def inj_on_def proof safe fix z :: complex assume "z ^ n = 1" hence "(c' * z) ^ n = c' ^ n" by (simp add: power_mult_distrib) also have "c' ^ n = of_real (root n (norm c) ^ n) * cis (Arg c)" unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre) also from n have "root n (norm c) ^ n = norm c" by simp also from c have "\ * cis (Arg c) = c" by (simp add: cis_Arg Complex.sgn_eq) finally show "(c' * z) ^ n = c" . next fix z assume z: "c = z ^ n" define z' where "z' = z / c'" from c and n have "c' \ 0" by (auto simp: c'_def) with n c have "z = c' * z'" and "z' ^ n = 1" by (auto simp: z'_def power_divide z) thus "z \ (\z. c' * z) ` {z. z ^ n = 1}" by blast qed (insert c n, auto simp: c'_def) qed lemma finite_nth_roots [intro]: assumes "n > 0" shows "finite {z::complex. z ^ n = c}" proof (cases "c = 0") case True with assms have "{z::complex. z ^ n = c} = {0}" by auto thus ?thesis by simp next case False from assms have "finite {z::complex. z ^ n = 1}" by (intro finite_roots_unity) simp_all also have "?this \ ?thesis" by (rule bij_betw_finite, rule bij_betw_nth_root_unity) fact+ finally show ?thesis . qed lemma card_nth_roots: assumes "c \ 0" "n > 0" shows "card {z::complex. z ^ n = c} = n" proof - have "card {z. z ^ n = c} = card {z::complex. z ^ n = 1}" by (rule sym, rule bij_betw_same_card, rule bij_betw_nth_root_unity) fact+ also have "\ = n" by (rule card_roots_unity_eq) fact+ finally show ?thesis . qed lemma sum_roots_unity: assumes "n > 1" shows "\{z::complex. z ^ n = 1} = 0" proof - define \ where "\ = cis (2 * pi / real n)" have [simp]: "\ \ 1" proof assume "\ = 1" with assms obtain k :: int where "2 * pi / real n = 2 * pi * of_int k" by (auto simp: \_def complex_eq_iff cos_one_2pi_int) with assms have "real n * of_int k = 1" by (simp add: field_simps) also have "real n * of_int k = of_int (int n * k)" by simp also have "1 = (of_int 1 :: real)" by simp also note of_int_eq_iff finally show False using assms by (auto simp: zmult_eq_1_iff) qed have "(\z | z ^ n = 1. z :: complex) = (\k = (\k ^ k)" by (intro sum.cong refl) (auto simp: \_def DeMoivre mult_ac) also have "\ = (\ ^ n - 1) / (\ - 1)" by (subst geometric_sum) auto also have "\ ^ n - 1 = cis (2 * pi) - 1" using assms by (auto simp: \_def DeMoivre) also have "\ = 0" by (simp add: complex_eq_iff) finally show ?thesis by simp qed lemma sum_nth_roots: assumes "n > 1" shows "\{z::complex. z ^ n = c} = 0" proof (cases "c = 0") case True with assms have "{z::complex. z ^ n = c} = {0}" by auto also have "\\ = 0" by simp finally show ?thesis . next case False define c' where "c' = root n (norm c) * cis (Arg c / n)" from False and assms have "(\{z. z ^ n = c}) = (\z | z ^ n = 1. c' * z)" by (subst sum.reindex_bij_betw [OF bij_betw_nth_root_unity, symmetric]) (auto simp: sum_distrib_left finite_roots_unity c'_def) also from assms have "\ = 0" by (simp add: sum_distrib_left [symmetric] sum_roots_unity) finally show ?thesis . qed subsection \Square root of complex numbers\ primcorec csqrt :: "complex \ complex" where "Re (csqrt z) = sqrt ((cmod z + Re z) / 2)" | "Im (csqrt z) = (if Im z = 0 then 1 else sgn (Im z)) * sqrt ((cmod z - Re z) / 2)" lemma csqrt_of_real_nonneg [simp]: "Im x = 0 \ Re x \ 0 \ csqrt x = sqrt (Re x)" by (simp add: complex_eq_iff norm_complex_def) lemma csqrt_of_real_nonpos [simp]: "Im x = 0 \ Re x \ 0 \ csqrt x = \ * sqrt \Re x\" by (simp add: complex_eq_iff norm_complex_def) lemma of_real_sqrt: "x \ 0 \ of_real (sqrt x) = csqrt (of_real x)" by (simp add: complex_eq_iff norm_complex_def) lemma csqrt_0 [simp]: "csqrt 0 = 0" by simp lemma csqrt_1 [simp]: "csqrt 1 = 1" by simp lemma csqrt_ii [simp]: "csqrt \ = (1 + \) / sqrt 2" by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt) lemma power2_csqrt[simp,algebra]: "(csqrt z)\<^sup>2 = z" proof (cases "Im z = 0") case True then show ?thesis using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"] by (cases "0::real" "Re z" rule: linorder_cases) (simp_all add: complex_eq_iff Re_power2 Im_power2 power2_eq_square cmod_eq_Re) next case False moreover have "cmod z * cmod z - Re z * Re z = Im z * Im z" by (simp add: norm_complex_def power2_eq_square) moreover have "\Re z\ \ cmod z" by (simp add: norm_complex_def) ultimately show ?thesis by (simp add: Re_power2 Im_power2 complex_eq_iff real_sgn_eq field_simps real_sqrt_mult[symmetric] real_sqrt_divide) qed lemma csqrt_eq_0 [simp]: "csqrt z = 0 \ z = 0" by auto (metis power2_csqrt power_eq_0_iff) lemma csqrt_eq_1 [simp]: "csqrt z = 1 \ z = 1" by auto (metis power2_csqrt power2_eq_1_iff) lemma csqrt_principal: "0 < Re (csqrt z) \ Re (csqrt z) = 0 \ 0 \ Im (csqrt z)" by (auto simp add: not_less cmod_plus_Re_le_0_iff Im_eq_0) lemma Re_csqrt: "0 \ Re (csqrt z)" by (metis csqrt_principal le_less) lemma csqrt_square: assumes "0 < Re b \ (Re b = 0 \ 0 \ Im b)" shows "csqrt (b^2) = b" proof - have "csqrt (b^2) = b \ csqrt (b^2) = - b" by (simp add: power2_eq_iff[symmetric]) moreover have "csqrt (b^2) \ -b \ b = 0" using csqrt_principal[of "b ^ 2"] assms by (intro disjCI notI) (auto simp: complex_eq_iff) ultimately show ?thesis by auto qed lemma csqrt_unique: "w\<^sup>2 = z \ 0 < Re w \ Re w = 0 \ 0 \ Im w \ csqrt z = w" by (auto simp: csqrt_square) lemma csqrt_minus [simp]: assumes "Im x < 0 \ (Im x = 0 \ 0 \ Re x)" shows "csqrt (- x) = \ * csqrt x" proof - have "csqrt ((\ * csqrt x)^2) = \ * csqrt x" proof (rule csqrt_square) have "Im (csqrt x) \ 0" using assms by (auto simp add: cmod_eq_Re mult_le_0_iff field_simps complex_Re_le_cmod) then show "0 < Re (\ * csqrt x) \ Re (\ * csqrt x) = 0 \ 0 \ Im (\ * csqrt x)" by (auto simp add: Re_csqrt simp del: csqrt.simps) qed also have "(\ * csqrt x)^2 = - x" by (simp add: power_mult_distrib) finally show ?thesis . qed text \Legacy theorem names\ lemmas cmod_def = norm_complex_def lemma legacy_Complex_simps: shows Complex_eq_0: "Complex a b = 0 \ a = 0 \ b = 0" and complex_add: "Complex a b + Complex c d = Complex (a + c) (b + d)" and complex_minus: "- (Complex a b) = Complex (- a) (- b)" and complex_diff: "Complex a b - Complex c d = Complex (a - c) (b - d)" and Complex_eq_1: "Complex a b = 1 \ a = 1 \ b = 0" and Complex_eq_neg_1: "Complex a b = - 1 \ a = - 1 \ b = 0" and complex_mult: "Complex a b * Complex c d = Complex (a * c - b * d) (a * d + b * c)" and complex_inverse: "inverse (Complex a b) = Complex (a / (a\<^sup>2 + b\<^sup>2)) (- b / (a\<^sup>2 + b\<^sup>2))" and Complex_eq_numeral: "Complex a b = numeral w \ a = numeral w \ b = 0" and Complex_eq_neg_numeral: "Complex a b = - numeral w \ a = - numeral w \ b = 0" and complex_scaleR: "scaleR r (Complex a b) = Complex (r * a) (r * b)" and Complex_eq_i: "Complex x y = \ \ x = 0 \ y = 1" and i_mult_Complex: "\ * Complex a b = Complex (- b) a" and Complex_mult_i: "Complex a b * \ = Complex (- b) a" and i_complex_of_real: "\ * complex_of_real r = Complex 0 r" and complex_of_real_i: "complex_of_real r * \ = Complex 0 r" and Complex_add_complex_of_real: "Complex x y + complex_of_real r = Complex (x+r) y" and complex_of_real_add_Complex: "complex_of_real r + Complex x y = Complex (r+x) y" and Complex_mult_complex_of_real: "Complex x y * complex_of_real r = Complex (x*r) (y*r)" and complex_of_real_mult_Complex: "complex_of_real r * Complex x y = Complex (r*x) (r*y)" and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa \ y = 0)" and complex_cnj: "cnj (Complex a b) = Complex a (- b)" and Complex_sum': "sum (\x. Complex (f x) 0) s = Complex (sum f s) 0" and Complex_sum: "Complex (sum f s) 0 = sum (\x. Complex (f x) 0) s" and complex_of_real_def: "complex_of_real r = Complex r 0" and complex_norm: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)" by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide) lemma Complex_in_Reals: "Complex x 0 \ \" by (metis Reals_of_real complex_of_real_def) end diff --git a/src/HOL/Real.thy b/src/HOL/Real.thy --- a/src/HOL/Real.thy +++ b/src/HOL/Real.thy @@ -1,1772 +1,1789 @@ (* Title: HOL/Real.thy Author: Jacques D. Fleuriot, University of Edinburgh, 1998 Author: Larry Paulson, University of Cambridge Author: Jeremy Avigad, Carnegie Mellon University Author: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 Construction of Cauchy Reals by Brian Huffman, 2010 *) section \Development of the Reals using Cauchy Sequences\ theory Real imports Rat begin text \ This theory contains a formalization of the real numbers as equivalence classes of Cauchy sequences of rationals. See the AFP entry @{text Dedekind_Real} for an alternative construction using Dedekind cuts. \ subsection \Preliminary lemmas\ text\Useful in convergence arguments\ lemma inverse_of_nat_le: fixes n::nat shows "\n \ m; n\0\ \ 1 / of_nat m \ (1::'a::linordered_field) / of_nat n" by (simp add: frac_le) lemma add_diff_add: "(a + c) - (b + d) = (a - b) + (c - d)" for a b c d :: "'a::ab_group_add" by simp lemma minus_diff_minus: "- a - - b = - (a - b)" for a b :: "'a::ab_group_add" by simp lemma mult_diff_mult: "(x * y - a * b) = x * (y - b) + (x - a) * b" for x y a b :: "'a::ring" by (simp add: algebra_simps) lemma inverse_diff_inverse: fixes a b :: "'a::division_ring" assumes "a \ 0" and "b \ 0" shows "inverse a - inverse b = - (inverse a * (a - b) * inverse b)" using assms by (simp add: algebra_simps) lemma obtain_pos_sum: fixes r :: rat assumes r: "0 < r" obtains s t where "0 < s" and "0 < t" and "r = s + t" proof from r show "0 < r/2" by simp from r show "0 < r/2" by simp show "r = r/2 + r/2" by simp qed subsection \Sequences that converge to zero\ definition vanishes :: "(nat \ rat) \ bool" where "vanishes X \ (\r>0. \k. \n\k. \X n\ < r)" lemma vanishesI: "(\r. 0 < r \ \k. \n\k. \X n\ < r) \ vanishes X" unfolding vanishes_def by simp lemma vanishesD: "vanishes X \ 0 < r \ \k. \n\k. \X n\ < r" unfolding vanishes_def by simp lemma vanishes_const [simp]: "vanishes (\n. c) \ c = 0" proof (cases "c = 0") case True then show ?thesis by (simp add: vanishesI) next case False then show ?thesis unfolding vanishes_def using zero_less_abs_iff by blast qed lemma vanishes_minus: "vanishes X \ vanishes (\n. - X n)" unfolding vanishes_def by simp lemma vanishes_add: assumes X: "vanishes X" and Y: "vanishes Y" shows "vanishes (\n. X n + Y n)" proof (rule vanishesI) fix r :: rat assume "0 < r" then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" by (rule obtain_pos_sum) obtain i where i: "\n\i. \X n\ < s" using vanishesD [OF X s] .. obtain j where j: "\n\j. \Y n\ < t" using vanishesD [OF Y t] .. have "\n\max i j. \X n + Y n\ < r" proof clarsimp fix n assume n: "i \ n" "j \ n" have "\X n + Y n\ \ \X n\ + \Y n\" by (rule abs_triangle_ineq) also have "\ < s + t" by (simp add: add_strict_mono i j n) finally show "\X n + Y n\ < r" by (simp only: r) qed then show "\k. \n\k. \X n + Y n\ < r" .. qed lemma vanishes_diff: assumes "vanishes X" "vanishes Y" shows "vanishes (\n. X n - Y n)" unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus assms) lemma vanishes_mult_bounded: assumes X: "\a>0. \n. \X n\ < a" assumes Y: "vanishes (\n. Y n)" shows "vanishes (\n. X n * Y n)" proof (rule vanishesI) fix r :: rat assume r: "0 < r" obtain a where a: "0 < a" "\n. \X n\ < a" using X by blast obtain b where b: "0 < b" "r = a * b" proof show "0 < r / a" using r a by simp show "r = a * (r / a)" using a by simp qed obtain k where k: "\n\k. \Y n\ < b" using vanishesD [OF Y b(1)] .. have "\n\k. \X n * Y n\ < r" by (simp add: b(2) abs_mult mult_strict_mono' a k) then show "\k. \n\k. \X n * Y n\ < r" .. qed subsection \Cauchy sequences\ definition cauchy :: "(nat \ rat) \ bool" where "cauchy X \ (\r>0. \k. \m\k. \n\k. \X m - X n\ < r)" lemma cauchyI: "(\r. 0 < r \ \k. \m\k. \n\k. \X m - X n\ < r) \ cauchy X" unfolding cauchy_def by simp lemma cauchyD: "cauchy X \ 0 < r \ \k. \m\k. \n\k. \X m - X n\ < r" unfolding cauchy_def by simp lemma cauchy_const [simp]: "cauchy (\n. x)" unfolding cauchy_def by simp lemma cauchy_add [simp]: assumes X: "cauchy X" and Y: "cauchy Y" shows "cauchy (\n. X n + Y n)" proof (rule cauchyI) fix r :: rat assume "0 < r" then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" by (rule obtain_pos_sum) obtain i where i: "\m\i. \n\i. \X m - X n\ < s" using cauchyD [OF X s] .. obtain j where j: "\m\j. \n\j. \Y m - Y n\ < t" using cauchyD [OF Y t] .. have "\m\max i j. \n\max i j. \(X m + Y m) - (X n + Y n)\ < r" proof clarsimp fix m n assume *: "i \ m" "j \ m" "i \ n" "j \ n" have "\(X m + Y m) - (X n + Y n)\ \ \X m - X n\ + \Y m - Y n\" unfolding add_diff_add by (rule abs_triangle_ineq) also have "\ < s + t" by (rule add_strict_mono) (simp_all add: i j *) finally show "\(X m + Y m) - (X n + Y n)\ < r" by (simp only: r) qed then show "\k. \m\k. \n\k. \(X m + Y m) - (X n + Y n)\ < r" .. qed lemma cauchy_minus [simp]: assumes X: "cauchy X" shows "cauchy (\n. - X n)" using assms unfolding cauchy_def unfolding minus_diff_minus abs_minus_cancel . lemma cauchy_diff [simp]: assumes "cauchy X" "cauchy Y" shows "cauchy (\n. X n - Y n)" using assms unfolding diff_conv_add_uminus by (simp del: add_uminus_conv_diff) lemma cauchy_imp_bounded: assumes "cauchy X" shows "\b>0. \n. \X n\ < b" proof - obtain k where k: "\m\k. \n\k. \X m - X n\ < 1" using cauchyD [OF assms zero_less_one] .. show "\b>0. \n. \X n\ < b" proof (intro exI conjI allI) have "0 \ \X 0\" by simp also have "\X 0\ \ Max (abs ` X ` {..k})" by simp finally have "0 \ Max (abs ` X ` {..k})" . then show "0 < Max (abs ` X ` {..k}) + 1" by simp next fix n :: nat show "\X n\ < Max (abs ` X ` {..k}) + 1" proof (rule linorder_le_cases) assume "n \ k" then have "\X n\ \ Max (abs ` X ` {..k})" by simp then show "\X n\ < Max (abs ` X ` {..k}) + 1" by simp next assume "k \ n" have "\X n\ = \X k + (X n - X k)\" by simp also have "\X k + (X n - X k)\ \ \X k\ + \X n - X k\" by (rule abs_triangle_ineq) also have "\ < Max (abs ` X ` {..k}) + 1" by (rule add_le_less_mono) (simp_all add: k \k \ n\) finally show "\X n\ < Max (abs ` X ` {..k}) + 1" . qed qed qed lemma cauchy_mult [simp]: assumes X: "cauchy X" and Y: "cauchy Y" shows "cauchy (\n. X n * Y n)" proof (rule cauchyI) fix r :: rat assume "0 < r" then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v" by (rule obtain_pos_sum) obtain a where a: "0 < a" "\n. \X n\ < a" using cauchy_imp_bounded [OF X] by blast obtain b where b: "0 < b" "\n. \Y n\ < b" using cauchy_imp_bounded [OF Y] by blast obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b" proof show "0 < v/b" using v b(1) by simp show "0 < u/a" using u a(1) by simp show "r = a * (u/a) + (v/b) * b" using a(1) b(1) \r = u + v\ by simp qed obtain i where i: "\m\i. \n\i. \X m - X n\ < s" using cauchyD [OF X s] .. obtain j where j: "\m\j. \n\j. \Y m - Y n\ < t" using cauchyD [OF Y t] .. have "\m\max i j. \n\max i j. \X m * Y m - X n * Y n\ < r" proof clarsimp fix m n assume *: "i \ m" "j \ m" "i \ n" "j \ n" have "\X m * Y m - X n * Y n\ = \X m * (Y m - Y n) + (X m - X n) * Y n\" unfolding mult_diff_mult .. also have "\ \ \X m * (Y m - Y n)\ + \(X m - X n) * Y n\" by (rule abs_triangle_ineq) also have "\ = \X m\ * \Y m - Y n\ + \X m - X n\ * \Y n\" unfolding abs_mult .. also have "\ < a * t + s * b" by (simp_all add: add_strict_mono mult_strict_mono' a b i j *) finally show "\X m * Y m - X n * Y n\ < r" by (simp only: r) qed then show "\k. \m\k. \n\k. \X m * Y m - X n * Y n\ < r" .. qed lemma cauchy_not_vanishes_cases: assumes X: "cauchy X" assumes nz: "\ vanishes X" shows "\b>0. \k. (\n\k. b < - X n) \ (\n\k. b < X n)" proof - obtain r where "0 < r" and r: "\k. \n\k. r \ \X n\" using nz unfolding vanishes_def by (auto simp add: not_less) obtain s t where s: "0 < s" and t: "0 < t" and "r = s + t" using \0 < r\ by (rule obtain_pos_sum) obtain i where i: "\m\i. \n\i. \X m - X n\ < s" using cauchyD [OF X s] .. obtain k where "i \ k" and "r \ \X k\" using r by blast have k: "\n\k. \X n - X k\ < s" using i \i \ k\ by auto have "X k \ - r \ r \ X k" using \r \ \X k\\ by auto then have "(\n\k. t < - X n) \ (\n\k. t < X n)" unfolding \r = s + t\ using k by auto then have "\k. (\n\k. t < - X n) \ (\n\k. t < X n)" .. then show "\t>0. \k. (\n\k. t < - X n) \ (\n\k. t < X n)" using t by auto qed lemma cauchy_not_vanishes: assumes X: "cauchy X" and nz: "\ vanishes X" shows "\b>0. \k. \n\k. b < \X n\" using cauchy_not_vanishes_cases [OF assms] by (elim ex_forward conj_forward asm_rl) auto lemma cauchy_inverse [simp]: assumes X: "cauchy X" and nz: "\ vanishes X" shows "cauchy (\n. inverse (X n))" proof (rule cauchyI) fix r :: rat assume "0 < r" obtain b i where b: "0 < b" and i: "\n\i. b < \X n\" using cauchy_not_vanishes [OF X nz] by blast from b i have nz: "\n\i. X n \ 0" by auto obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b" proof show "0 < b * r * b" by (simp add: \0 < r\ b) show "r = inverse b * (b * r * b) * inverse b" using b by simp qed obtain j where j: "\m\j. \n\j. \X m - X n\ < s" using cauchyD [OF X s] .. have "\m\max i j. \n\max i j. \inverse (X m) - inverse (X n)\ < r" proof clarsimp fix m n assume *: "i \ m" "j \ m" "i \ n" "j \ n" have "\inverse (X m) - inverse (X n)\ = inverse \X m\ * \X m - X n\ * inverse \X n\" by (simp add: inverse_diff_inverse nz * abs_mult) also have "\ < inverse b * s * inverse b" by (simp add: mult_strict_mono less_imp_inverse_less i j b * s) finally show "\inverse (X m) - inverse (X n)\ < r" by (simp only: r) qed then show "\k. \m\k. \n\k. \inverse (X m) - inverse (X n)\ < r" .. qed lemma vanishes_diff_inverse: assumes X: "cauchy X" "\ vanishes X" and Y: "cauchy Y" "\ vanishes Y" and XY: "vanishes (\n. X n - Y n)" shows "vanishes (\n. inverse (X n) - inverse (Y n))" proof (rule vanishesI) fix r :: rat assume r: "0 < r" obtain a i where a: "0 < a" and i: "\n\i. a < \X n\" using cauchy_not_vanishes [OF X] by blast obtain b j where b: "0 < b" and j: "\n\j. b < \Y n\" using cauchy_not_vanishes [OF Y] by blast obtain s where s: "0 < s" and "inverse a * s * inverse b = r" proof show "0 < a * r * b" using a r b by simp show "inverse a * (a * r * b) * inverse b = r" using a r b by simp qed obtain k where k: "\n\k. \X n - Y n\ < s" using vanishesD [OF XY s] .. have "\n\max (max i j) k. \inverse (X n) - inverse (Y n)\ < r" proof clarsimp fix n assume n: "i \ n" "j \ n" "k \ n" with i j a b have "X n \ 0" and "Y n \ 0" by auto then have "\inverse (X n) - inverse (Y n)\ = inverse \X n\ * \X n - Y n\ * inverse \Y n\" by (simp add: inverse_diff_inverse abs_mult) also have "\ < inverse a * s * inverse b" by (intro mult_strict_mono' less_imp_inverse_less) (simp_all add: a b i j k n) also note \inverse a * s * inverse b = r\ finally show "\inverse (X n) - inverse (Y n)\ < r" . qed then show "\k. \n\k. \inverse (X n) - inverse (Y n)\ < r" .. qed subsection \Equivalence relation on Cauchy sequences\ definition realrel :: "(nat \ rat) \ (nat \ rat) \ bool" where "realrel = (\X Y. cauchy X \ cauchy Y \ vanishes (\n. X n - Y n))" lemma realrelI [intro?]: "cauchy X \ cauchy Y \ vanishes (\n. X n - Y n) \ realrel X Y" by (simp add: realrel_def) lemma realrel_refl: "cauchy X \ realrel X X" by (simp add: realrel_def) lemma symp_realrel: "symp realrel" by (simp add: abs_minus_commute realrel_def symp_def vanishes_def) lemma transp_realrel: "transp realrel" unfolding realrel_def by (rule transpI) (force simp add: dest: vanishes_add) lemma part_equivp_realrel: "part_equivp realrel" by (blast intro: part_equivpI symp_realrel transp_realrel realrel_refl cauchy_const) subsection \The field of real numbers\ quotient_type real = "nat \ rat" / partial: realrel morphisms rep_real Real by (rule part_equivp_realrel) lemma cr_real_eq: "pcr_real = (\x y. cauchy x \ Real x = y)" unfolding real.pcr_cr_eq cr_real_def realrel_def by auto lemma Real_induct [induct type: real]: (* TODO: generate automatically *) assumes "\X. cauchy X \ P (Real X)" shows "P x" proof (induct x) case (1 X) then have "cauchy X" by (simp add: realrel_def) then show "P (Real X)" by (rule assms) qed lemma eq_Real: "cauchy X \ cauchy Y \ Real X = Real Y \ vanishes (\n. X n - Y n)" using real.rel_eq_transfer unfolding real.pcr_cr_eq cr_real_def rel_fun_def realrel_def by simp lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy" by (simp add: real.domain_eq realrel_def) instantiation real :: field begin lift_definition zero_real :: "real" is "\n. 0" by (simp add: realrel_refl) lift_definition one_real :: "real" is "\n. 1" by (simp add: realrel_refl) lift_definition plus_real :: "real \ real \ real" is "\X Y n. X n + Y n" unfolding realrel_def add_diff_add by (simp only: cauchy_add vanishes_add simp_thms) lift_definition uminus_real :: "real \ real" is "\X n. - X n" unfolding realrel_def minus_diff_minus by (simp only: cauchy_minus vanishes_minus simp_thms) lift_definition times_real :: "real \ real \ real" is "\X Y n. X n * Y n" proof - fix f1 f2 f3 f4 have "\cauchy f1; cauchy f4; vanishes (\n. f1 n - f2 n); vanishes (\n. f3 n - f4 n)\ \ vanishes (\n. f1 n * (f3 n - f4 n) + f4 n * (f1 n - f2 n))" by (simp add: vanishes_add vanishes_mult_bounded cauchy_imp_bounded) then show "\realrel f1 f2; realrel f3 f4\ \ realrel (\n. f1 n * f3 n) (\n. f2 n * f4 n)" by (simp add: mult.commute realrel_def mult_diff_mult) qed lift_definition inverse_real :: "real \ real" is "\X. if vanishes X then (\n. 0) else (\n. inverse (X n))" proof - fix X Y assume "realrel X Y" then have X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\n. X n - Y n)" by (simp_all add: realrel_def) have "vanishes X \ vanishes Y" proof assume "vanishes X" from vanishes_diff [OF this XY] show "vanishes Y" by simp next assume "vanishes Y" from vanishes_add [OF this XY] show "vanishes X" by simp qed then show "?thesis X Y" by (simp add: vanishes_diff_inverse X Y XY realrel_def) qed definition "x - y = x + - y" for x y :: real definition "x div y = x * inverse y" for x y :: real lemma add_Real: "cauchy X \ cauchy Y \ Real X + Real Y = Real (\n. X n + Y n)" using plus_real.transfer by (simp add: cr_real_eq rel_fun_def) lemma minus_Real: "cauchy X \ - Real X = Real (\n. - X n)" using uminus_real.transfer by (simp add: cr_real_eq rel_fun_def) lemma diff_Real: "cauchy X \ cauchy Y \ Real X - Real Y = Real (\n. X n - Y n)" by (simp add: minus_Real add_Real minus_real_def) lemma mult_Real: "cauchy X \ cauchy Y \ Real X * Real Y = Real (\n. X n * Y n)" using times_real.transfer by (simp add: cr_real_eq rel_fun_def) lemma inverse_Real: "cauchy X \ inverse (Real X) = (if vanishes X then 0 else Real (\n. inverse (X n)))" using inverse_real.transfer zero_real.transfer unfolding cr_real_eq rel_fun_def by (simp split: if_split_asm, metis) instance proof fix a b c :: real show "a + b = b + a" by transfer (simp add: ac_simps realrel_def) show "(a + b) + c = a + (b + c)" by transfer (simp add: ac_simps realrel_def) show "0 + a = a" by transfer (simp add: realrel_def) show "- a + a = 0" by transfer (simp add: realrel_def) show "a - b = a + - b" by (rule minus_real_def) show "(a * b) * c = a * (b * c)" by transfer (simp add: ac_simps realrel_def) show "a * b = b * a" by transfer (simp add: ac_simps realrel_def) show "1 * a = a" by transfer (simp add: ac_simps realrel_def) show "(a + b) * c = a * c + b * c" by transfer (simp add: distrib_right realrel_def) show "(0::real) \ (1::real)" by transfer (simp add: realrel_def) have "vanishes (\n. inverse (X n) * X n - 1)" if X: "cauchy X" "\ vanishes X" for X proof (rule vanishesI) fix r::rat assume "0 < r" obtain b k where "b>0" "\n\k. b < \X n\" using X cauchy_not_vanishes by blast then show "\k. \n\k. \inverse (X n) * X n - 1\ < r" using \0 < r\ by force qed then show "a \ 0 \ inverse a * a = 1" by transfer (simp add: realrel_def) show "a div b = a * inverse b" by (rule divide_real_def) show "inverse (0::real) = 0" by transfer (simp add: realrel_def) qed end subsection \Positive reals\ lift_definition positive :: "real \ bool" is "\X. \r>0. \k. \n\k. r < X n" proof - have 1: "\r>0. \k. \n\k. r < Y n" if *: "realrel X Y" and **: "\r>0. \k. \n\k. r < X n" for X Y proof - from * have XY: "vanishes (\n. X n - Y n)" by (simp_all add: realrel_def) from ** obtain r i where "0 < r" and i: "\n\i. r < X n" by blast obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" using \0 < r\ by (rule obtain_pos_sum) obtain j where j: "\n\j. \X n - Y n\ < s" using vanishesD [OF XY s] .. have "\n\max i j. t < Y n" proof clarsimp fix n assume n: "i \ n" "j \ n" have "\X n - Y n\ < s" and "r < X n" using i j n by simp_all then show "t < Y n" by (simp add: r) qed then show ?thesis using t by blast qed fix X Y assume "realrel X Y" then have "realrel X Y" and "realrel Y X" using symp_realrel by (auto simp: symp_def) then show "?thesis X Y" by (safe elim!: 1) qed lemma positive_Real: "cauchy X \ positive (Real X) \ (\r>0. \k. \n\k. r < X n)" using positive.transfer by (simp add: cr_real_eq rel_fun_def) lemma positive_zero: "\ positive 0" by transfer auto lemma positive_add: assumes "positive x" "positive y" shows "positive (x + y)" proof - have *: "\\n\i. a < x n; \n\j. b < y n; 0 < a; 0 < b; n \ max i j\ \ a+b < x n + y n" for x y and a b::rat and i j n::nat by (simp add: add_strict_mono) show ?thesis using assms by transfer (blast intro: * pos_add_strict) qed lemma positive_mult: assumes "positive x" "positive y" shows "positive (x * y)" proof - have *: "\\n\i. a < x n; \n\j. b < y n; 0 < a; 0 < b; n \ max i j\ \ a*b < x n * y n" for x y and a b::rat and i j n::nat by (simp add: mult_strict_mono') show ?thesis using assms by transfer (blast intro: * mult_pos_pos) qed lemma positive_minus: "\ positive x \ x \ 0 \ positive (- x)" apply transfer apply (simp add: realrel_def) apply (blast dest: cauchy_not_vanishes_cases) done instantiation real :: linordered_field begin definition "x < y \ positive (y - x)" definition "x \ y \ x < y \ x = y" for x y :: real definition "\a\ = (if a < 0 then - a else a)" for a :: real definition "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" for a :: real instance proof fix a b c :: real show "\a\ = (if a < 0 then - a else a)" by (rule abs_real_def) show "a < b \ a \ b \ \ b \ a" "a \ b \ b \ c \ a \ c" "a \ a" "a \ b \ b \ a \ a = b" "a \ b \ c + a \ c + b" unfolding less_eq_real_def less_real_def by (force simp add: positive_zero dest: positive_add)+ show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" by (rule sgn_real_def) show "a \ b \ b \ a" by (auto dest!: positive_minus simp: less_eq_real_def less_real_def) show "a < b \ 0 < c \ c * a < c * b" unfolding less_real_def by (force simp add: algebra_simps dest: positive_mult) qed end instantiation real :: distrib_lattice begin definition "(inf :: real \ real \ real) = min" definition "(sup :: real \ real \ real) = max" instance by standard (auto simp add: inf_real_def sup_real_def max_min_distrib2) end lemma of_nat_Real: "of_nat x = Real (\n. of_nat x)" by (induct x) (simp_all add: zero_real_def one_real_def add_Real) lemma of_int_Real: "of_int x = Real (\n. of_int x)" by (cases x rule: int_diff_cases) (simp add: of_nat_Real diff_Real) lemma of_rat_Real: "of_rat x = Real (\n. x)" proof (induct x) case (Fract a b) then show ?case apply (simp add: Fract_of_int_quotient of_rat_divide) apply (simp add: of_int_Real divide_inverse inverse_Real mult_Real) done qed instance real :: archimedean_field proof show "\z. x \ of_int z" for x :: real proof (induct x) case (1 X) then obtain b where "0 < b" and b: "\n. \X n\ < b" by (blast dest: cauchy_imp_bounded) then have "Real X < of_int (\b\ + 1)" using 1 apply (simp add: of_int_Real less_real_def diff_Real positive_Real) apply (rule_tac x=1 in exI) apply (simp add: algebra_simps) by (metis abs_ge_self le_less_trans le_of_int_ceiling less_le) then show ?case using less_eq_real_def by blast qed qed instantiation real :: floor_ceiling begin definition [code del]: "\x::real\ = (THE z. of_int z \ x \ x < of_int (z + 1))" instance proof show "of_int \x\ \ x \ x < of_int (\x\ + 1)" for x :: real unfolding floor_real_def using floor_exists1 by (rule theI') qed end subsection \Completeness\ lemma not_positive_Real: assumes "cauchy X" shows "\ positive (Real X) \ (\r>0. \k. \n\k. X n \ r)" (is "?lhs = ?rhs") unfolding positive_Real [OF assms] proof (intro iffI allI notI impI) show "\k. \n\k. X n \ r" if r: "\ (\r>0. \k. \n\k. r < X n)" and "0 < r" for r proof - obtain s t where "s > 0" "t > 0" "r = s+t" using \r > 0\ obtain_pos_sum by blast obtain k where k: "\m n. \m\k; n\k\ \ \X m - X n\ < t" using cauchyD [OF assms \t > 0\] by blast obtain n where "n \ k" "X n \ s" by (meson r \0 < s\ not_less) then have "X l \ r" if "l \ n" for l using k [OF \n \ k\, of l] that \r = s+t\ by linarith then show ?thesis by blast qed qed (meson le_cases not_le) lemma le_Real: assumes "cauchy X" "cauchy Y" shows "Real X \ Real Y = (\r>0. \k. \n\k. X n \ Y n + r)" unfolding not_less [symmetric, where 'a=real] less_real_def apply (simp add: diff_Real not_positive_Real assms) apply (simp add: diff_le_eq ac_simps) done lemma le_RealI: assumes Y: "cauchy Y" shows "\n. x \ of_rat (Y n) \ x \ Real Y" proof (induct x) fix X assume X: "cauchy X" and "\n. Real X \ of_rat (Y n)" then have le: "\m r. 0 < r \ \k. \n\k. X n \ Y m + r" by (simp add: of_rat_Real le_Real) then have "\k. \n\k. X n \ Y n + r" if "0 < r" for r :: rat proof - from that obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" by (rule obtain_pos_sum) obtain i where i: "\m\i. \n\i. \Y m - Y n\ < s" using cauchyD [OF Y s] .. obtain j where j: "\n\j. X n \ Y i + t" using le [OF t] .. have "\n\max i j. X n \ Y n + r" proof clarsimp fix n assume n: "i \ n" "j \ n" have "X n \ Y i + t" using n j by simp moreover have "\Y i - Y n\ < s" using n i by simp ultimately show "X n \ Y n + r" unfolding r by simp qed then show ?thesis .. qed then show "Real X \ Real Y" by (simp add: of_rat_Real le_Real X Y) qed lemma Real_leI: assumes X: "cauchy X" assumes le: "\n. of_rat (X n) \ y" shows "Real X \ y" proof - have "- y \ - Real X" by (simp add: minus_Real X le_RealI of_rat_minus le) then show ?thesis by simp qed lemma less_RealD: assumes "cauchy Y" shows "x < Real Y \ \n. x < of_rat (Y n)" apply (erule contrapos_pp) apply (simp add: not_less) apply (erule Real_leI [OF assms]) done lemma of_nat_less_two_power [simp]: "of_nat n < (2::'a::linordered_idom) ^ n" apply (induct n) apply simp apply (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc) done lemma complete_real: fixes S :: "real set" assumes "\x. x \ S" and "\z. \x\S. x \ z" shows "\y. (\x\S. x \ y) \ (\z. (\x\S. x \ z) \ y \ z)" proof - obtain x where x: "x \ S" using assms(1) .. obtain z where z: "\x\S. x \ z" using assms(2) .. define P where "P x \ (\y\S. y \ of_rat x)" for x obtain a where a: "\ P a" proof have "of_int \x - 1\ \ x - 1" by (rule of_int_floor_le) also have "x - 1 < x" by simp finally have "of_int \x - 1\ < x" . then have "\ x \ of_int \x - 1\" by (simp only: not_le) then show "\ P (of_int \x - 1\)" unfolding P_def of_rat_of_int_eq using x by blast qed obtain b where b: "P b" proof show "P (of_int \z\)" unfolding P_def of_rat_of_int_eq proof fix y assume "y \ S" then have "y \ z" using z by simp also have "z \ of_int \z\" by (rule le_of_int_ceiling) finally show "y \ of_int \z\" . qed qed define avg where "avg x y = x/2 + y/2" for x y :: rat define bisect where "bisect = (\(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y))" define A where "A n = fst ((bisect ^^ n) (a, b))" for n define B where "B n = snd ((bisect ^^ n) (a, b))" for n define C where "C n = avg (A n) (B n)" for n have A_0 [simp]: "A 0 = a" unfolding A_def by simp have B_0 [simp]: "B 0 = b" unfolding B_def by simp have A_Suc [simp]: "\n. A (Suc n) = (if P (C n) then A n else C n)" unfolding A_def B_def C_def bisect_def split_def by simp have B_Suc [simp]: "\n. B (Suc n) = (if P (C n) then C n else B n)" unfolding A_def B_def C_def bisect_def split_def by simp have width: "B n - A n = (b - a) / 2^n" for n proof (induct n) case (Suc n) then show ?case by (simp add: C_def eq_divide_eq avg_def algebra_simps) qed simp have twos: "\n. y / 2 ^ n < r" if "0 < r" for y r :: rat proof - obtain n where "y / r < rat_of_nat n" using \0 < r\ reals_Archimedean2 by blast then have "\n. y < r * 2 ^ n" by (metis divide_less_eq less_trans mult.commute of_nat_less_two_power that) then show ?thesis by (simp add: field_split_simps) qed have PA: "\ P (A n)" for n by (induct n) (simp_all add: a) have PB: "P (B n)" for n by (induct n) (simp_all add: b) have ab: "a < b" using a b unfolding P_def by (meson leI less_le_trans of_rat_less) have AB: "A n < B n" for n by (induct n) (simp_all add: ab C_def avg_def) have "A i \ A j \ B j \ B i" if "i < j" for i j using that proof (induction rule: less_Suc_induct) case (1 i) then show ?case apply (clarsimp simp add: C_def avg_def add_divide_distrib [symmetric]) apply (rule AB [THEN less_imp_le]) done qed simp then have A_mono: "A i \ A j" and B_mono: "B j \ B i" if "i \ j" for i j by (metis eq_refl le_neq_implies_less that)+ have cauchy_lemma: "cauchy X" if *: "\n i. i\n \ A n \ X i \ X i \ B n" for X proof (rule cauchyI) fix r::rat assume "0 < r" then obtain k where k: "(b - a) / 2 ^ k < r" using twos by blast have "\X m - X n\ < r" if "m\k" "n\k" for m n proof - have "\X m - X n\ \ B k - A k" by (simp add: * abs_rat_def diff_mono that) also have "... < r" by (simp add: k width) finally show ?thesis . qed then show "\k. \m\k. \n\k. \X m - X n\ < r" by blast qed have "cauchy A" by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order less_le_trans) have "cauchy B" by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order le_less_trans) have "\x\S. x \ Real B" proof fix x assume "x \ S" then show "x \ Real B" using PB [unfolded P_def] \cauchy B\ by (simp add: le_RealI) qed moreover have "\z. (\x\S. x \ z) \ Real A \ z" by (meson PA Real_leI P_def \cauchy A\ le_cases order.trans) moreover have "vanishes (\n. (b - a) / 2 ^ n)" proof (rule vanishesI) fix r :: rat assume "0 < r" then obtain k where k: "\b - a\ / 2 ^ k < r" using twos by blast have "\n\k. \(b - a) / 2 ^ n\ < r" proof clarify fix n assume n: "k \ n" have "\(b - a) / 2 ^ n\ = \b - a\ / 2 ^ n" by simp also have "\ \ \b - a\ / 2 ^ k" using n by (simp add: divide_left_mono) also note k finally show "\(b - a) / 2 ^ n\ < r" . qed then show "\k. \n\k. \(b - a) / 2 ^ n\ < r" .. qed then have "Real B = Real A" by (simp add: eq_Real \cauchy A\ \cauchy B\ width) ultimately show "\y. (\x\S. x \ y) \ (\z. (\x\S. x \ z) \ y \ z)" by force qed instantiation real :: linear_continuum begin subsection \Supremum of a set of reals\ definition "Sup X = (LEAST z::real. \x\X. x \ z)" definition "Inf X = - Sup (uminus ` X)" for X :: "real set" instance proof show Sup_upper: "x \ Sup X" if "x \ X" "bdd_above X" for x :: real and X :: "real set" proof - from that obtain s where s: "\y\X. y \ s" "\z. \y\X. y \ z \ s \ z" using complete_real[of X] unfolding bdd_above_def by blast then show ?thesis unfolding Sup_real_def by (rule LeastI2_order) (auto simp: that) qed show Sup_least: "Sup X \ z" if "X \ {}" and z: "\x. x \ X \ x \ z" for z :: real and X :: "real set" proof - from that obtain s where s: "\y\X. y \ s" "\z. \y\X. y \ z \ s \ z" using complete_real [of X] by blast then have "Sup X = s" unfolding Sup_real_def by (best intro: Least_equality) also from s z have "\ \ z" by blast finally show ?thesis . qed show "Inf X \ x" if "x \ X" "bdd_below X" for x :: real and X :: "real set" using Sup_upper [of "-x" "uminus ` X"] by (auto simp: Inf_real_def that) show "z \ Inf X" if "X \ {}" "\x. x \ X \ z \ x" for z :: real and X :: "real set" using Sup_least [of "uminus ` X" "- z"] by (force simp: Inf_real_def that) show "\a b::real. a \ b" using zero_neq_one by blast qed end subsection \Hiding implementation details\ hide_const (open) vanishes cauchy positive Real declare Real_induct [induct del] declare Abs_real_induct [induct del] declare Abs_real_cases [cases del] lifting_update real.lifting lifting_forget real.lifting subsection \Embedding numbers into the Reals\ abbreviation real_of_nat :: "nat \ real" where "real_of_nat \ of_nat" abbreviation real :: "nat \ real" where "real \ of_nat" abbreviation real_of_int :: "int \ real" where "real_of_int \ of_int" abbreviation real_of_rat :: "rat \ real" where "real_of_rat \ of_rat" declare [[coercion_enabled]] declare [[coercion "of_nat :: nat \ int"]] declare [[coercion "of_nat :: nat \ real"]] declare [[coercion "of_int :: int \ real"]] (* We do not add rat to the coerced types, this has often unpleasant side effects when writing inverse (Suc n) which sometimes gets two coercions: of_rat (inverse (of_nat (Suc n))) *) declare [[coercion_map map]] declare [[coercion_map "\f g h x. g (h (f x))"]] declare [[coercion_map "\f g (x,y). (f x, g y)"]] declare of_int_eq_0_iff [algebra, presburger] declare of_int_eq_1_iff [algebra, presburger] declare of_int_eq_iff [algebra, presburger] declare of_int_less_0_iff [algebra, presburger] declare of_int_less_1_iff [algebra, presburger] declare of_int_less_iff [algebra, presburger] declare of_int_le_0_iff [algebra, presburger] declare of_int_le_1_iff [algebra, presburger] declare of_int_le_iff [algebra, presburger] declare of_int_0_less_iff [algebra, presburger] declare of_int_0_le_iff [algebra, presburger] declare of_int_1_less_iff [algebra, presburger] declare of_int_1_le_iff [algebra, presburger] lemma int_less_real_le: "n < m \ real_of_int n + 1 \ real_of_int m" proof - have "(0::real) \ 1" by (metis less_eq_real_def zero_less_one) then show ?thesis by (metis floor_of_int less_floor_iff) qed lemma int_le_real_less: "n \ m \ real_of_int n < real_of_int m + 1" by (meson int_less_real_le not_le) lemma real_of_int_div_aux: "(real_of_int x) / (real_of_int d) = real_of_int (x div d) + (real_of_int (x mod d)) / (real_of_int d)" proof - have "x = (x div d) * d + x mod d" by auto then have "real_of_int x = real_of_int (x div d) * real_of_int d + real_of_int(x mod d)" by (metis of_int_add of_int_mult) then have "real_of_int x / real_of_int d = \ / real_of_int d" by simp then show ?thesis by (auto simp add: add_divide_distrib algebra_simps) qed lemma real_of_int_div: "d dvd n \ real_of_int (n div d) = real_of_int n / real_of_int d" for d n :: int by (simp add: real_of_int_div_aux) lemma real_of_int_div2: "0 \ real_of_int n / real_of_int x - real_of_int (n div x)" proof (cases "x = 0") case False then show ?thesis by (metis diff_ge_0_iff_ge floor_divide_of_int_eq of_int_floor_le) qed simp lemma real_of_int_div3: "real_of_int n / real_of_int x - real_of_int (n div x) \ 1" apply (simp add: algebra_simps) by (metis add.commute floor_correct floor_divide_of_int_eq less_eq_real_def of_int_1 of_int_add) lemma real_of_int_div4: "real_of_int (n div x) \ real_of_int n / real_of_int x" using real_of_int_div2 [of n x] by simp subsection \Embedding the Naturals into the Reals\ lemma real_of_card: "real (card A) = sum (\x. 1) A" by simp lemma nat_less_real_le: "n < m \ real n + 1 \ real m" by (metis discrete of_nat_1 of_nat_add of_nat_le_iff) lemma nat_le_real_less: "n \ m \ real n < real m + 1" for m n :: nat by (meson nat_less_real_le not_le) lemma real_of_nat_div_aux: "real x / real d = real (x div d) + real (x mod d) / real d" proof - have "x = (x div d) * d + x mod d" by auto then have "real x = real (x div d) * real d + real(x mod d)" by (metis of_nat_add of_nat_mult) then have "real x / real d = \ / real d" by simp then show ?thesis by (auto simp add: add_divide_distrib algebra_simps) qed lemma real_of_nat_div: "d dvd n \ real(n div d) = real n / real d" by (subst real_of_nat_div_aux) (auto simp add: dvd_eq_mod_eq_0 [symmetric]) lemma real_of_nat_div2: "0 \ real n / real x - real (n div x)" for n x :: nat apply (simp add: algebra_simps) by (metis floor_divide_of_nat_eq of_int_floor_le of_int_of_nat_eq) lemma real_of_nat_div3: "real n / real x - real (n div x) \ 1" for n x :: nat proof (cases "x = 0") case False then show ?thesis by (metis of_int_of_nat_eq real_of_int_div3 zdiv_int) qed auto lemma real_of_nat_div4: "real (n div x) \ real n / real x" for n x :: nat using real_of_nat_div2 [of n x] by simp subsection \The Archimedean Property of the Reals\ lemma real_arch_inverse: "0 < e \ (\n::nat. n \ 0 \ 0 < inverse (real n) \ inverse (real n) < e)" using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat] by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc) lemma reals_Archimedean3: "0 < x \ \y. \n. y < real n * x" by (auto intro: ex_less_of_nat_mult) lemma real_archimedian_rdiv_eq_0: assumes x0: "x \ 0" and c: "c \ 0" and xc: "\m::nat. m > 0 \ real m * x \ c" shows "x = 0" by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc) subsection \Rationals\ lemma Rats_abs_iff[simp]: "\(x::real)\ \ \ \ x \ \" by(simp add: abs_real_def split: if_splits) lemma Rats_eq_int_div_int: "\ = {real_of_int i / real_of_int j | i j. j \ 0}" (is "_ = ?S") proof show "\ \ ?S" proof fix x :: real assume "x \ \" then obtain r where "x = of_rat r" unfolding Rats_def .. have "of_rat r \ ?S" by (cases r) (auto simp add: of_rat_rat) then show "x \ ?S" using \x = of_rat r\ by simp qed next show "?S \ \" proof (auto simp: Rats_def) fix i j :: int assume "j \ 0" then have "real_of_int i / real_of_int j = of_rat (Fract i j)" by (simp add: of_rat_rat) then show "real_of_int i / real_of_int j \ range of_rat" by blast qed qed lemma Rats_eq_int_div_nat: "\ = { real_of_int i / real n | i n. n \ 0}" proof (auto simp: Rats_eq_int_div_int) fix i j :: int assume "j \ 0" show "\(i'::int) (n::nat). real_of_int i / real_of_int j = real_of_int i' / real n \ 0 < n" proof (cases "j > 0") case True then have "real_of_int i / real_of_int j = real_of_int i / real (nat j) \ 0 < nat j" by simp then show ?thesis by blast next case False with \j \ 0\ have "real_of_int i / real_of_int j = real_of_int (- i) / real (nat (- j)) \ 0 < nat (- j)" by simp then show ?thesis by blast qed next fix i :: int and n :: nat assume "0 < n" then have "real_of_int i / real n = real_of_int i / real_of_int(int n) \ int n \ 0" by simp then show "\i' j. real_of_int i / real n = real_of_int i' / real_of_int j \ j \ 0" by blast qed lemma Rats_abs_nat_div_natE: assumes "x \ \" obtains m n :: nat where "n \ 0" and "\x\ = real m / real n" and "coprime m n" proof - from \x \ \\ obtain i :: int and n :: nat where "n \ 0" and "x = real_of_int i / real n" by (auto simp add: Rats_eq_int_div_nat) then have "\x\ = real (nat \i\) / real n" by simp then obtain m :: nat where x_rat: "\x\ = real m / real n" by blast let ?gcd = "gcd m n" from \n \ 0\ have gcd: "?gcd \ 0" by simp let ?k = "m div ?gcd" let ?l = "n div ?gcd" let ?gcd' = "gcd ?k ?l" have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m" by (rule dvd_mult_div_cancel) have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n" by (rule dvd_mult_div_cancel) from \n \ 0\ and gcd_l have "?gcd * ?l \ 0" by simp then have "?l \ 0" by (blast dest!: mult_not_zero) moreover have "\x\ = real ?k / real ?l" proof - from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)" by (simp add: real_of_nat_div) also from gcd_k and gcd_l have "\ = real m / real n" by simp also from x_rat have "\ = \x\" .. finally show ?thesis .. qed moreover have "?gcd' = 1" proof - have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)" by (rule gcd_mult_distrib_nat) with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp with gcd show ?thesis by auto qed then have "coprime ?k ?l" by (simp only: coprime_iff_gcd_eq_1) ultimately show ?thesis .. qed subsection \Density of the Rational Reals in the Reals\ text \ This density proof is due to Stefan Richter and was ported by TN. The original source is \<^emph>\Real Analysis\ by H.L. Royden. It employs the Archimedean property of the reals.\ lemma Rats_dense_in_real: fixes x :: real assumes "x < y" shows "\r\\. x < r \ r < y" proof - from \x < y\ have "0 < y - x" by simp with reals_Archimedean obtain q :: nat where q: "inverse (real q) < y - x" and "0 < q" by blast define p where "p = \y * real q\ - 1" define r where "r = of_int p / real q" from q have "x < y - inverse (real q)" by simp also from \0 < q\ have "y - inverse (real q) \ r" by (simp add: r_def p_def le_divide_eq left_diff_distrib) finally have "x < r" . moreover from \0 < q\ have "r < y" by (simp add: r_def p_def divide_less_eq diff_less_eq less_ceiling_iff [symmetric]) moreover have "r \ \" by (simp add: r_def) ultimately show ?thesis by blast qed lemma of_rat_dense: fixes x y :: real assumes "x < y" shows "\q :: rat. x < of_rat q \ of_rat q < y" using Rats_dense_in_real [OF \x < y\] by (auto elim: Rats_cases) subsection \Numerals and Arithmetic\ declaration \ K (Lin_Arith.add_inj_const (\<^const_name>\of_nat\, \<^typ>\nat \ real\) #> Lin_Arith.add_inj_const (\<^const_name>\of_int\, \<^typ>\int \ real\)) \ subsection \Simprules combining \x + y\ and \0\\ (* FIXME ARE THEY NEEDED? *) lemma real_add_minus_iff [simp]: "x + - a = 0 \ x = a" for x a :: real by arith lemma real_add_less_0_iff: "x + y < 0 \ y < - x" for x y :: real by auto lemma real_0_less_add_iff: "0 < x + y \ - x < y" for x y :: real by auto lemma real_add_le_0_iff: "x + y \ 0 \ y \ - x" for x y :: real by auto lemma real_0_le_add_iff: "0 \ x + y \ - x \ y" for x y :: real by auto subsection \Lemmas about powers\ lemma two_realpow_ge_one: "(1::real) \ 2 ^ n" by simp (* FIXME: declare this [simp] for all types, or not at all *) declare sum_squares_eq_zero_iff [simp] sum_power2_eq_zero_iff [simp] lemma real_minus_mult_self_le [simp]: "- (u * u) \ x * x" for u x :: real by (rule order_trans [where y = 0]) auto lemma realpow_square_minus_le [simp]: "- u\<^sup>2 \ x\<^sup>2" for u x :: real by (auto simp add: power2_eq_square) subsection \Density of the Reals\ lemma field_lbound_gt_zero: "0 < d1 \ 0 < d2 \ \e. 0 < e \ e < d1 \ e < d2" for d1 d2 :: "'a::linordered_field" by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def) lemma field_less_half_sum: "x < y \ x < (x + y) / 2" for x y :: "'a::linordered_field" by auto lemma field_sum_of_halves: "x / 2 + x / 2 = x" for x :: "'a::linordered_field" by simp subsection \Archimedean properties and useful consequences\ text\Bernoulli's inequality\ proposition Bernoulli_inequality: fixes x :: real assumes "-1 \ x" shows "1 + n * x \ (1 + x) ^ n" proof (induct n) case 0 then show ?case by simp next case (Suc n) have "1 + Suc n * x \ 1 + (Suc n)*x + n * x^2" by (simp add: algebra_simps) also have "... = (1 + x) * (1 + n*x)" by (auto simp: power2_eq_square algebra_simps) also have "... \ (1 + x) ^ Suc n" using Suc.hyps assms mult_left_mono by fastforce finally show ?case . qed corollary Bernoulli_inequality_even: fixes x :: real assumes "even n" shows "1 + n * x \ (1 + x) ^ n" proof (cases "-1 \ x \ n=0") case True then show ?thesis by (auto simp: Bernoulli_inequality) next case False then have "real n \ 1" by simp with False have "n * x \ -1" by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one) then have "1 + n * x \ 0" by auto also have "... \ (1 + x) ^ n" using assms using zero_le_even_power by blast finally show ?thesis . qed corollary real_arch_pow: fixes x :: real assumes x: "1 < x" shows "\n. y < x^n" proof - from x have x0: "x - 1 > 0" by arith from reals_Archimedean3[OF x0, rule_format, of y] obtain n :: nat where n: "y < real n * (x - 1)" by metis from x0 have x00: "x- 1 \ -1" by arith from Bernoulli_inequality[OF x00, of n] n have "y < x^n" by auto then show ?thesis by metis qed corollary real_arch_pow_inv: fixes x y :: real assumes y: "y > 0" and x1: "x < 1" shows "\n. x^n < y" proof (cases "x > 0") case True with x1 have ix: "1 < 1/x" by (simp add: field_simps) from real_arch_pow[OF ix, of "1/y"] obtain n where n: "1/y < (1/x)^n" by blast then show ?thesis using y \x > 0\ by (auto simp add: field_simps) next case False with y x1 show ?thesis by (metis less_le_trans not_less power_one_right) qed lemma forall_pos_mono: "(\d e::real. d < e \ P d \ P e) \ (\n::nat. n \ 0 \ P (inverse (real n))) \ (\e. 0 < e \ P e)" by (metis real_arch_inverse) lemma forall_pos_mono_1: "(\d e::real. d < e \ P d \ P e) \ (\n. P (inverse (real (Suc n)))) \ 0 < e \ P e" apply (rule forall_pos_mono) apply auto apply (metis Suc_pred of_nat_Suc) done subsection \Floor and Ceiling Functions from the Reals to the Integers\ (* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *) lemma real_of_nat_less_numeral_iff [simp]: "real n < numeral w \ n < numeral w" for n :: nat by (metis of_nat_less_iff of_nat_numeral) lemma numeral_less_real_of_nat_iff [simp]: "numeral w < real n \ numeral w < n" for n :: nat by (metis of_nat_less_iff of_nat_numeral) lemma numeral_le_real_of_nat_iff [simp]: "numeral n \ real m \ numeral n \ m" for m :: nat by (metis not_le real_of_nat_less_numeral_iff) lemma of_int_floor_cancel [simp]: "of_int \x\ = x \ (\n::int. x = of_int n)" by (metis floor_of_int) +lemma of_int_floor [simp]: "a \ \ \ of_int (floor a) = a" + by (metis Ints_cases of_int_floor_cancel) + +lemma floor_frac [simp]: "\frac r\ = 0" + by (simp add: frac_def) + +lemma frac_1 [simp]: "frac 1 = 0" + by (simp add: frac_def) + +lemma frac_in_Rats_iff [simp]: + fixes r::"'a::{floor_ceiling,field_char_0}" + shows "frac r \ \ \ r \ \" + by (metis Rats_add Rats_diff Rats_of_int diff_add_cancel frac_def) + lemma floor_eq: "real_of_int n < x \ x < real_of_int n + 1 \ \x\ = n" by linarith lemma floor_eq2: "real_of_int n \ x \ x < real_of_int n + 1 \ \x\ = n" by (fact floor_unique) lemma floor_eq3: "real n < x \ x < real (Suc n) \ nat \x\ = n" by linarith lemma floor_eq4: "real n \ x \ x < real (Suc n) \ nat \x\ = n" by linarith lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \ real_of_int \r\" by linarith lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real_of_int \r\" by linarith lemma real_of_int_floor_add_one_ge [simp]: "r \ real_of_int \r\ + 1" by linarith lemma real_of_int_floor_add_one_gt [simp]: "r < real_of_int \r\ + 1" by linarith lemma floor_divide_real_eq_div: assumes "0 \ b" shows "\a / real_of_int b\ = \a\ div b" proof (cases "b = 0") case True then show ?thesis by simp next case False with assms have b: "b > 0" by simp have "j = i div b" if "real_of_int i \ a" "a < 1 + real_of_int i" "real_of_int j * real_of_int b \ a" "a < real_of_int b + real_of_int j * real_of_int b" for i j :: int proof - from that have "i < b + j * b" by (metis le_less_trans of_int_add of_int_less_iff of_int_mult) moreover have "j * b < 1 + i" proof - have "real_of_int (j * b) < real_of_int i + 1" using \a < 1 + real_of_int i\ \real_of_int j * real_of_int b \ a\ by force then show "j * b < 1 + i" by linarith qed ultimately have "(j - i div b) * b \ i mod b" "i mod b < ((j - i div b) + 1) * b" by (auto simp: field_simps) then have "(j - i div b) * b < 1 * b" "0 * b < ((j - i div b) + 1) * b" using pos_mod_bound [OF b, of i] pos_mod_sign [OF b, of i] by linarith+ then show ?thesis using b unfolding mult_less_cancel_right by auto qed with b show ?thesis by (auto split: floor_split simp: field_simps) qed lemma floor_one_divide_eq_div_numeral [simp]: "\1 / numeral b::real\ = 1 div numeral b" by (metis floor_divide_of_int_eq of_int_1 of_int_numeral) lemma floor_minus_one_divide_eq_div_numeral [simp]: "\- (1 / numeral b)::real\ = - 1 div numeral b" by (metis (mono_tags, opaque_lifting) div_minus_right minus_divide_right floor_divide_of_int_eq of_int_neg_numeral of_int_1) lemma floor_divide_eq_div_numeral [simp]: "\numeral a / numeral b::real\ = numeral a div numeral b" by (metis floor_divide_of_int_eq of_int_numeral) lemma floor_minus_divide_eq_div_numeral [simp]: "\- (numeral a / numeral b)::real\ = - numeral a div numeral b" by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral) lemma of_int_ceiling_cancel [simp]: "of_int \x\ = x \ (\n::int. x = of_int n)" using ceiling_of_int by metis +lemma of_int_ceiling [simp]: "a \ \ \ of_int (ceiling a) = a" + by (metis Ints_cases of_int_ceiling_cancel) + lemma ceiling_eq: "of_int n < x \ x \ of_int n + 1 \ \x\ = n + 1" by (simp add: ceiling_unique) lemma of_int_ceiling_diff_one_le [simp]: "of_int \r\ - 1 \ r" by linarith lemma of_int_ceiling_le_add_one [simp]: "of_int \r\ \ r + 1" by linarith lemma ceiling_le: "x \ of_int a \ \x\ \ a" by (simp add: ceiling_le_iff) lemma ceiling_divide_eq_div: "\of_int a / of_int b\ = - (- a div b)" by (metis ceiling_def floor_divide_of_int_eq minus_divide_left of_int_minus) lemma ceiling_divide_eq_div_numeral [simp]: "\numeral a / numeral b :: real\ = - (- numeral a div numeral b)" using ceiling_divide_eq_div[of "numeral a" "numeral b"] by simp lemma ceiling_minus_divide_eq_div_numeral [simp]: "\- (numeral a / numeral b :: real)\ = - (numeral a div numeral b)" using ceiling_divide_eq_div[of "- numeral a" "numeral b"] by simp text \ The following lemmas are remnants of the erstwhile functions natfloor and natceiling. \ lemma nat_floor_neg: "x \ 0 \ nat \x\ = 0" for x :: real by linarith lemma le_nat_floor: "real x \ a \ x \ nat \a\" by linarith lemma le_mult_nat_floor: "nat \a\ * nat \b\ \ nat \a * b\" by (cases "0 \ a \ 0 \ b") (auto simp add: nat_mult_distrib[symmetric] nat_mono le_mult_floor) lemma nat_ceiling_le_eq [simp]: "nat \x\ \ a \ x \ real a" by linarith lemma real_nat_ceiling_ge: "x \ real (nat \x\)" by linarith lemma Rats_no_top_le: "\q \ \. x \ q" for x :: real by (auto intro!: bexI[of _ "of_nat (nat \x\)"]) linarith lemma Rats_no_bot_less: "\q \ \. q < x" for x :: real by (auto intro!: bexI[of _ "of_int (\x\ - 1)"]) linarith subsection \Exponentiation with floor\ lemma floor_power: assumes "x = of_int \x\" shows "\x ^ n\ = \x\ ^ n" proof - have "x ^ n = of_int (\x\ ^ n)" using assms by (induct n arbitrary: x) simp_all then show ?thesis by (metis floor_of_int) qed lemma floor_numeral_power [simp]: "\numeral x ^ n\ = numeral x ^ n" by (metis floor_of_int of_int_numeral of_int_power) lemma ceiling_numeral_power [simp]: "\numeral x ^ n\ = numeral x ^ n" by (metis ceiling_of_int of_int_numeral of_int_power) subsection \Implementation of rational real numbers\ text \Formal constructor\ definition Ratreal :: "rat \ real" where [code_abbrev, simp]: "Ratreal = real_of_rat" code_datatype Ratreal text \Quasi-Numerals\ lemma [code_abbrev]: "real_of_rat (numeral k) = numeral k" "real_of_rat (- numeral k) = - numeral k" "real_of_rat (rat_of_int a) = real_of_int a" by simp_all lemma [code_post]: "real_of_rat 0 = 0" "real_of_rat 1 = 1" "real_of_rat (- 1) = - 1" "real_of_rat (1 / numeral k) = 1 / numeral k" "real_of_rat (numeral k / numeral l) = numeral k / numeral l" "real_of_rat (- (1 / numeral k)) = - (1 / numeral k)" "real_of_rat (- (numeral k / numeral l)) = - (numeral k / numeral l)" by (simp_all add: of_rat_divide of_rat_minus) text \Operations\ lemma zero_real_code [code]: "0 = Ratreal 0" by simp lemma one_real_code [code]: "1 = Ratreal 1" by simp instantiation real :: equal begin definition "HOL.equal x y \ x - y = 0" for x :: real instance by standard (simp add: equal_real_def) lemma real_equal_code [code]: "HOL.equal (Ratreal x) (Ratreal y) \ HOL.equal x y" by (simp add: equal_real_def equal) lemma [code nbe]: "HOL.equal x x \ True" for x :: real by (rule equal_refl) end lemma real_less_eq_code [code]: "Ratreal x \ Ratreal y \ x \ y" by (simp add: of_rat_less_eq) lemma real_less_code [code]: "Ratreal x < Ratreal y \ x < y" by (simp add: of_rat_less) lemma real_plus_code [code]: "Ratreal x + Ratreal y = Ratreal (x + y)" by (simp add: of_rat_add) lemma real_times_code [code]: "Ratreal x * Ratreal y = Ratreal (x * y)" by (simp add: of_rat_mult) lemma real_uminus_code [code]: "- Ratreal x = Ratreal (- x)" by (simp add: of_rat_minus) lemma real_minus_code [code]: "Ratreal x - Ratreal y = Ratreal (x - y)" by (simp add: of_rat_diff) lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)" by (simp add: of_rat_inverse) lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)" by (simp add: of_rat_divide) lemma real_floor_code [code]: "\Ratreal x\ = \x\" by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff of_int_floor_le of_rat_of_int_eq real_less_eq_code) text \Quickcheck\ context includes term_syntax begin definition valterm_ratreal :: "rat \ (unit \ Code_Evaluation.term) \ real \ (unit \ Code_Evaluation.term)" where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\} k" end instantiation real :: random begin context includes state_combinator_syntax begin definition "Quickcheck_Random.random i = Quickcheck_Random.random i \\ (\r. Pair (valterm_ratreal r))" instance .. end end instantiation real :: exhaustive begin definition "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (\r. f (Ratreal r)) d" instance .. end instantiation real :: full_exhaustive begin definition "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (\r. f (valterm_ratreal r)) d" instance .. end instantiation real :: narrowing begin definition "narrowing_real = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing" instance .. end subsection \Setup for Nitpick\ declaration \ Nitpick_HOL.register_frac_type \<^type_name>\real\ [(\<^const_name>\zero_real_inst.zero_real\, \<^const_name>\Nitpick.zero_frac\), (\<^const_name>\one_real_inst.one_real\, \<^const_name>\Nitpick.one_frac\), (\<^const_name>\plus_real_inst.plus_real\, \<^const_name>\Nitpick.plus_frac\), (\<^const_name>\times_real_inst.times_real\, \<^const_name>\Nitpick.times_frac\), (\<^const_name>\uminus_real_inst.uminus_real\, \<^const_name>\Nitpick.uminus_frac\), (\<^const_name>\inverse_real_inst.inverse_real\, \<^const_name>\Nitpick.inverse_frac\), (\<^const_name>\ord_real_inst.less_real\, \<^const_name>\Nitpick.less_frac\), (\<^const_name>\ord_real_inst.less_eq_real\, \<^const_name>\Nitpick.less_eq_frac\)] \ lemmas [nitpick_unfold] = inverse_real_inst.inverse_real one_real_inst.one_real ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real times_real_inst.times_real uminus_real_inst.uminus_real zero_real_inst.zero_real subsection \Setup for SMT\ ML_file \Tools/SMT/smt_real.ML\ ML_file \Tools/SMT/z3_real.ML\ lemma [z3_rule]: "0 + x = x" "x + 0 = x" "0 * x = 0" "1 * x = x" "-x = -1 * x" "x + y = y + x" for x y :: real by auto lemma [smt_arith_multiplication]: fixes A B :: real and p n :: real assumes "A \ B" "0 < n" "p > 0" shows "(A / n) * p \ (B / n) * p" using assms by (auto simp: field_simps) lemma [smt_arith_multiplication]: fixes A B :: real and p n :: real assumes "A < B" "0 < n" "p > 0" shows "(A / n) * p < (B / n) * p" using assms by (auto simp: field_simps) lemma [smt_arith_multiplication]: fixes A B :: real and p n :: int assumes "A \ B" "0 < n" "p > 0" shows "(A / n) * p \ (B / n) * p" using assms by (auto simp: field_simps) lemma [smt_arith_multiplication]: fixes A B :: real and p n :: int assumes "A < B" "0 < n" "p > 0" shows "(A / n) * p < (B / n) * p" using assms by (auto simp: field_simps) lemmas [smt_arith_multiplication] = verit_le_mono_div[THEN mult_left_mono, unfolded int_distrib, of _ _ \nat (floor (_ :: real))\ \nat (floor (_ :: real))\] div_le_mono[THEN mult_left_mono, unfolded int_distrib, of _ _ \nat (floor (_ :: real))\ \nat (floor (_ :: real))\] verit_le_mono_div_int[THEN mult_left_mono, unfolded int_distrib, of _ _ \floor (_ :: real)\ \floor (_ :: real)\] zdiv_mono1[THEN mult_left_mono, unfolded int_distrib, of _ _ \floor (_ :: real)\ \floor (_ :: real)\] arg_cong[of _ _ \\a :: real. a / real (n::nat) * real (p::nat)\ for n p :: nat, THEN sym] arg_cong[of _ _ \\a :: real. a / real_of_int n * real_of_int p\ for n p :: int, THEN sym] arg_cong[of _ _ \\a :: real. a / n * p\ for n p :: real, THEN sym] lemmas [smt_arith_simplify] = floor_one floor_numeral div_by_1 times_divide_eq_right nonzero_mult_div_cancel_left division_ring_divide_zero div_0 divide_minus_left zero_less_divide_iff subsection \Setup for Argo\ ML_file \Tools/Argo/argo_real.ML\ end diff --git a/src/HOL/Rings.thy b/src/HOL/Rings.thy --- a/src/HOL/Rings.thy +++ b/src/HOL/Rings.thy @@ -1,2750 +1,2753 @@ (* Title: HOL/Rings.thy Author: Gertrud Bauer Author: Steven Obua Author: Tobias Nipkow Author: Lawrence C Paulson Author: Markus Wenzel Author: Jeremy Avigad *) section \Rings\ theory Rings imports Groups Set Fun begin subsection \Semirings and rings\ class semiring = ab_semigroup_add + semigroup_mult + assumes distrib_right [algebra_simps, algebra_split_simps]: "(a + b) * c = a * c + b * c" assumes distrib_left [algebra_simps, algebra_split_simps]: "a * (b + c) = a * b + a * c" begin text \For the \combine_numerals\ simproc\ lemma combine_common_factor: "a * e + (b * e + c) = (a + b) * e + c" by (simp add: distrib_right ac_simps) end class mult_zero = times + zero + assumes mult_zero_left [simp]: "0 * a = 0" assumes mult_zero_right [simp]: "a * 0 = 0" begin lemma mult_not_zero: "a * b \ 0 \ a \ 0 \ b \ 0" by auto end class semiring_0 = semiring + comm_monoid_add + mult_zero class semiring_0_cancel = semiring + cancel_comm_monoid_add begin subclass semiring_0 proof fix a :: 'a have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric]) then show "0 * a = 0" by (simp only: add_left_cancel) have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric]) then show "a * 0 = 0" by (simp only: add_left_cancel) qed end class comm_semiring = ab_semigroup_add + ab_semigroup_mult + assumes distrib: "(a + b) * c = a * c + b * c" begin subclass semiring proof fix a b c :: 'a show "(a + b) * c = a * c + b * c" by (simp add: distrib) have "a * (b + c) = (b + c) * a" by (simp add: ac_simps) also have "\ = b * a + c * a" by (simp only: distrib) also have "\ = a * b + a * c" by (simp add: ac_simps) finally show "a * (b + c) = a * b + a * c" by blast qed end class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero begin subclass semiring_0 .. end class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add begin subclass semiring_0_cancel .. subclass comm_semiring_0 .. end class zero_neq_one = zero + one + assumes zero_neq_one [simp]: "0 \ 1" begin lemma one_neq_zero [simp]: "1 \ 0" by (rule not_sym) (rule zero_neq_one) definition of_bool :: "bool \ 'a" where "of_bool p = (if p then 1 else 0)" lemma of_bool_eq [simp, code]: "of_bool False = 0" "of_bool True = 1" by (simp_all add: of_bool_def) lemma of_bool_eq_iff: "of_bool p = of_bool q \ p = q" by (simp add: of_bool_def) lemma split_of_bool [split]: "P (of_bool p) \ (p \ P 1) \ (\ p \ P 0)" by (cases p) simp_all lemma split_of_bool_asm: "P (of_bool p) \ \ (p \ \ P 1 \ \ p \ \ P 0)" by (cases p) simp_all lemma of_bool_eq_0_iff [simp]: \of_bool P = 0 \ \ P\ by simp lemma of_bool_eq_1_iff [simp]: \of_bool P = 1 \ P\ by simp end class semiring_1 = zero_neq_one + semiring_0 + monoid_mult begin lemma of_bool_conj: "of_bool (P \ Q) = of_bool P * of_bool Q" by auto end lemma lambda_zero: "(\h::'a::mult_zero. 0) = (*) 0" by auto lemma lambda_one: "(\x::'a::monoid_mult. x) = (*) 1" by auto subsection \Abstract divisibility\ class dvd = times begin definition dvd :: "'a \ 'a \ bool" (infix "dvd" 50) where "b dvd a \ (\k. a = b * k)" lemma dvdI [intro?]: "a = b * k \ b dvd a" unfolding dvd_def .. lemma dvdE [elim]: "b dvd a \ (\k. a = b * k \ P) \ P" unfolding dvd_def by blast end context comm_monoid_mult begin subclass dvd . lemma dvd_refl [simp]: "a dvd a" proof show "a = a * 1" by simp qed lemma dvd_trans [trans]: assumes "a dvd b" and "b dvd c" shows "a dvd c" proof - from assms obtain v where "b = a * v" by auto moreover from assms obtain w where "c = b * w" by auto ultimately have "c = a * (v * w)" by (simp add: mult.assoc) then show ?thesis .. qed lemma subset_divisors_dvd: "{c. c dvd a} \ {c. c dvd b} \ a dvd b" by (auto simp add: subset_iff intro: dvd_trans) lemma strict_subset_divisors_dvd: "{c. c dvd a} \ {c. c dvd b} \ a dvd b \ \ b dvd a" by (auto simp add: subset_iff intro: dvd_trans) lemma one_dvd [simp]: "1 dvd a" by (auto intro: dvdI) lemma dvd_mult [simp]: "a dvd (b * c)" if "a dvd c" using that by rule (auto intro: mult.left_commute dvdI) lemma dvd_mult2 [simp]: "a dvd (b * c)" if "a dvd b" using that dvd_mult [of a b c] by (simp add: ac_simps) lemma dvd_triv_right [simp]: "a dvd b * a" by (rule dvd_mult) (rule dvd_refl) lemma dvd_triv_left [simp]: "a dvd a * b" by (rule dvd_mult2) (rule dvd_refl) lemma mult_dvd_mono: assumes "a dvd b" and "c dvd d" shows "a * c dvd b * d" proof - from \a dvd b\ obtain b' where "b = a * b'" .. moreover from \c dvd d\ obtain d' where "d = c * d'" .. ultimately have "b * d = (a * c) * (b' * d')" by (simp add: ac_simps) then show ?thesis .. qed lemma dvd_mult_left: "a * b dvd c \ a dvd c" by (simp add: dvd_def mult.assoc) blast lemma dvd_mult_right: "a * b dvd c \ b dvd c" using dvd_mult_left [of b a c] by (simp add: ac_simps) end class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult begin subclass semiring_1 .. lemma dvd_0_left_iff [simp]: "0 dvd a \ a = 0" by auto lemma dvd_0_right [iff]: "a dvd 0" proof show "0 = a * 0" by simp qed lemma dvd_0_left: "0 dvd a \ a = 0" by simp lemma dvd_add [simp]: assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)" proof - from \a dvd b\ obtain b' where "b = a * b'" .. moreover from \a dvd c\ obtain c' where "c = a * c'" .. ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left) then show ?thesis .. qed end class semiring_1_cancel = semiring + cancel_comm_monoid_add + zero_neq_one + monoid_mult begin subclass semiring_0_cancel .. subclass semiring_1 .. end class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add + zero_neq_one + comm_monoid_mult + assumes right_diff_distrib' [algebra_simps, algebra_split_simps]: "a * (b - c) = a * b - a * c" begin subclass semiring_1_cancel .. subclass comm_semiring_0_cancel .. subclass comm_semiring_1 .. lemma left_diff_distrib' [algebra_simps, algebra_split_simps]: "(b - c) * a = b * a - c * a" by (simp add: algebra_simps) lemma dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \ a dvd b" proof - have "a dvd a * c + b \ a dvd b" (is "?P \ ?Q") proof assume ?Q then show ?P by simp next assume ?P then obtain d where "a * c + b = a * d" .. then have "a * c + b - a * c = a * d - a * c" by simp then have "b = a * d - a * c" by simp then have "b = a * (d - c)" by (simp add: algebra_simps) then show ?Q .. qed then show "a dvd c * a + b \ a dvd b" by (simp add: ac_simps) qed lemma dvd_add_times_triv_right_iff [simp]: "a dvd b + c * a \ a dvd b" using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps) lemma dvd_add_triv_left_iff [simp]: "a dvd a + b \ a dvd b" using dvd_add_times_triv_left_iff [of a 1 b] by simp lemma dvd_add_triv_right_iff [simp]: "a dvd b + a \ a dvd b" using dvd_add_times_triv_right_iff [of a b 1] by simp lemma dvd_add_right_iff: assumes "a dvd b" shows "a dvd b + c \ a dvd c" (is "?P \ ?Q") proof assume ?P then obtain d where "b + c = a * d" .. moreover from \a dvd b\ obtain e where "b = a * e" .. ultimately have "a * e + c = a * d" by simp then have "a * e + c - a * e = a * d - a * e" by simp then have "c = a * d - a * e" by simp then have "c = a * (d - e)" by (simp add: algebra_simps) then show ?Q .. next assume ?Q with assms show ?P by simp qed lemma dvd_add_left_iff: "a dvd c \ a dvd b + c \ a dvd b" using dvd_add_right_iff [of a c b] by (simp add: ac_simps) end class ring = semiring + ab_group_add begin subclass semiring_0_cancel .. text \Distribution rules\ lemma minus_mult_left: "- (a * b) = - a * b" by (rule minus_unique) (simp add: distrib_right [symmetric]) lemma minus_mult_right: "- (a * b) = a * - b" by (rule minus_unique) (simp add: distrib_left [symmetric]) text \Extract signs from products\ lemmas mult_minus_left [simp] = minus_mult_left [symmetric] lemmas mult_minus_right [simp] = minus_mult_right [symmetric] lemma minus_mult_minus [simp]: "- a * - b = a * b" by simp lemma minus_mult_commute: "- a * b = a * - b" by simp lemma right_diff_distrib [algebra_simps, algebra_split_simps]: "a * (b - c) = a * b - a * c" using distrib_left [of a b "-c "] by simp lemma left_diff_distrib [algebra_simps, algebra_split_simps]: "(a - b) * c = a * c - b * c" using distrib_right [of a "- b" c] by simp lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib lemma eq_add_iff1: "a * e + c = b * e + d \ (a - b) * e + c = d" by (simp add: algebra_simps) lemma eq_add_iff2: "a * e + c = b * e + d \ c = (b - a) * e + d" by (simp add: algebra_simps) end lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib class comm_ring = comm_semiring + ab_group_add begin subclass ring .. subclass comm_semiring_0_cancel .. lemma square_diff_square_factored: "x * x - y * y = (x + y) * (x - y)" by (simp add: algebra_simps) end class ring_1 = ring + zero_neq_one + monoid_mult begin subclass semiring_1_cancel .. lemma of_bool_not_iff [simp]: \of_bool (\ P) = 1 - of_bool P\ by simp lemma square_diff_one_factored: "x * x - 1 = (x + 1) * (x - 1)" by (simp add: algebra_simps) end class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult begin subclass ring_1 .. subclass comm_semiring_1_cancel by standard (simp add: algebra_simps) lemma dvd_minus_iff [simp]: "x dvd - y \ x dvd y" proof assume "x dvd - y" then have "x dvd - 1 * - y" by (rule dvd_mult) then show "x dvd y" by simp next assume "x dvd y" then have "x dvd - 1 * y" by (rule dvd_mult) then show "x dvd - y" by simp qed lemma minus_dvd_iff [simp]: "- x dvd y \ x dvd y" proof assume "- x dvd y" then obtain k where "y = - x * k" .. then have "y = x * - k" by simp then show "x dvd y" .. next assume "x dvd y" then obtain k where "y = x * k" .. then have "y = - x * - k" by simp then show "- x dvd y" .. qed lemma dvd_diff [simp]: "x dvd y \ x dvd z \ x dvd (y - z)" using dvd_add [of x y "- z"] by simp end subsection \Towards integral domains\ class semiring_no_zero_divisors = semiring_0 + assumes no_zero_divisors: "a \ 0 \ b \ 0 \ a * b \ 0" begin lemma divisors_zero: assumes "a * b = 0" shows "a = 0 \ b = 0" proof (rule classical) assume "\ ?thesis" then have "a \ 0" and "b \ 0" by auto with no_zero_divisors have "a * b \ 0" by blast with assms show ?thesis by simp qed lemma mult_eq_0_iff [simp]: "a * b = 0 \ a = 0 \ b = 0" proof (cases "a = 0 \ b = 0") case False then have "a \ 0" and "b \ 0" by auto then show ?thesis using no_zero_divisors by simp next case True then show ?thesis by auto qed end class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors + assumes mult_cancel_right [simp]: "a * c = b * c \ c = 0 \ a = b" and mult_cancel_left [simp]: "c * a = c * b \ c = 0 \ a = b" begin lemma mult_left_cancel: "c \ 0 \ c * a = c * b \ a = b" by simp lemma mult_right_cancel: "c \ 0 \ a * c = b * c \ a = b" by simp end class ring_no_zero_divisors = ring + semiring_no_zero_divisors begin subclass semiring_no_zero_divisors_cancel proof fix a b c have "a * c = b * c \ (a - b) * c = 0" by (simp add: algebra_simps) also have "\ \ c = 0 \ a = b" by auto finally show "a * c = b * c \ c = 0 \ a = b" . have "c * a = c * b \ c * (a - b) = 0" by (simp add: algebra_simps) also have "\ \ c = 0 \ a = b" by auto finally show "c * a = c * b \ c = 0 \ a = b" . qed end class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors begin subclass semiring_1_no_zero_divisors .. lemma square_eq_1_iff: "x * x = 1 \ x = 1 \ x = - 1" proof - have "(x - 1) * (x + 1) = x * x - 1" by (simp add: algebra_simps) then have "x * x = 1 \ (x - 1) * (x + 1) = 0" by simp then show ?thesis by (simp add: eq_neg_iff_add_eq_0) qed lemma mult_cancel_right1 [simp]: "c = b * c \ c = 0 \ b = 1" using mult_cancel_right [of 1 c b] by auto lemma mult_cancel_right2 [simp]: "a * c = c \ c = 0 \ a = 1" using mult_cancel_right [of a c 1] by simp lemma mult_cancel_left1 [simp]: "c = c * b \ c = 0 \ b = 1" using mult_cancel_left [of c 1 b] by force lemma mult_cancel_left2 [simp]: "c * a = c \ c = 0 \ a = 1" using mult_cancel_left [of c a 1] by simp end class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors begin subclass semiring_1_no_zero_divisors .. end class idom = comm_ring_1 + semiring_no_zero_divisors begin subclass semidom .. subclass ring_1_no_zero_divisors .. lemma dvd_mult_cancel_right [simp]: "a * c dvd b * c \ c = 0 \ a dvd b" proof - have "a * c dvd b * c \ (\k. b * c = (a * k) * c)" by (auto simp add: ac_simps) also have "(\k. b * c = (a * k) * c) \ c = 0 \ a dvd b" by auto finally show ?thesis . qed lemma dvd_mult_cancel_left [simp]: "c * a dvd c * b \ c = 0 \ a dvd b" using dvd_mult_cancel_right [of a c b] by (simp add: ac_simps) lemma square_eq_iff: "a * a = b * b \ a = b \ a = - b" proof assume "a * a = b * b" then have "(a - b) * (a + b) = 0" by (simp add: algebra_simps) then show "a = b \ a = - b" by (simp add: eq_neg_iff_add_eq_0) next assume "a = b \ a = - b" then show "a * a = b * b" by auto qed end class idom_abs_sgn = idom + abs + sgn + assumes sgn_mult_abs: "sgn a * \a\ = a" and sgn_sgn [simp]: "sgn (sgn a) = sgn a" and abs_abs [simp]: "\\a\\ = \a\" and abs_0 [simp]: "\0\ = 0" and sgn_0 [simp]: "sgn 0 = 0" and sgn_1 [simp]: "sgn 1 = 1" and sgn_minus_1: "sgn (- 1) = - 1" and sgn_mult: "sgn (a * b) = sgn a * sgn b" begin lemma sgn_eq_0_iff: "sgn a = 0 \ a = 0" proof - { assume "sgn a = 0" then have "sgn a * \a\ = 0" by simp then have "a = 0" by (simp add: sgn_mult_abs) } then show ?thesis by auto qed lemma abs_eq_0_iff: "\a\ = 0 \ a = 0" proof - { assume "\a\ = 0" then have "sgn a * \a\ = 0" by simp then have "a = 0" by (simp add: sgn_mult_abs) } then show ?thesis by auto qed lemma abs_mult_sgn: "\a\ * sgn a = a" using sgn_mult_abs [of a] by (simp add: ac_simps) lemma abs_1 [simp]: "\1\ = 1" using sgn_mult_abs [of 1] by simp lemma sgn_abs [simp]: "\sgn a\ = of_bool (a \ 0)" using sgn_mult_abs [of "sgn a"] mult_cancel_left [of "sgn a" "\sgn a\" 1] by (auto simp add: sgn_eq_0_iff) lemma abs_sgn [simp]: "sgn \a\ = of_bool (a \ 0)" using sgn_mult_abs [of "\a\"] mult_cancel_right [of "sgn \a\" "\a\" 1] by (auto simp add: abs_eq_0_iff) lemma abs_mult: "\a * b\ = \a\ * \b\" proof (cases "a = 0 \ b = 0") case True then show ?thesis by auto next case False then have *: "sgn (a * b) \ 0" by (simp add: sgn_eq_0_iff) from abs_mult_sgn [of "a * b"] abs_mult_sgn [of a] abs_mult_sgn [of b] have "\a * b\ * sgn (a * b) = \a\ * sgn a * \b\ * sgn b" by (simp add: ac_simps) then have "\a * b\ * sgn (a * b) = \a\ * \b\ * sgn (a * b)" by (simp add: sgn_mult ac_simps) with * show ?thesis by simp qed lemma sgn_minus [simp]: "sgn (- a) = - sgn a" proof - from sgn_minus_1 have "sgn (- 1 * a) = - 1 * sgn a" by (simp only: sgn_mult) then show ?thesis by simp qed lemma abs_minus [simp]: "\- a\ = \a\" proof - have [simp]: "\- 1\ = 1" using sgn_mult_abs [of "- 1"] by simp then have "\- 1 * a\ = 1 * \a\" by (simp only: abs_mult) then show ?thesis by simp qed end subsection \(Partial) Division\ class divide = fixes divide :: "'a \ 'a \ 'a" (infixl "div" 70) setup \Sign.add_const_constraint (\<^const_name>\divide\, SOME \<^typ>\'a \ 'a \ 'a\)\ context semiring begin lemma [field_simps, field_split_simps]: shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \ a * (b + c) = a * b + a * c" and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \ (a + b) * c = a * c + b * c" by (rule distrib_left distrib_right)+ end context ring begin lemma [field_simps, field_split_simps]: shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \ (a - b) * c = a * c - b * c" and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \ a * (b - c) = a * b - a * c" by (rule left_diff_distrib right_diff_distrib)+ end setup \Sign.add_const_constraint (\<^const_name>\divide\, SOME \<^typ>\'a::divide \ 'a \ 'a\)\ text \Algebraic classes with division\ class semidom_divide = semidom + divide + assumes nonzero_mult_div_cancel_right [simp]: "b \ 0 \ (a * b) div b = a" assumes div_by_0 [simp]: "a div 0 = 0" begin lemma nonzero_mult_div_cancel_left [simp]: "a \ 0 \ (a * b) div a = b" using nonzero_mult_div_cancel_right [of a b] by (simp add: ac_simps) subclass semiring_no_zero_divisors_cancel proof show *: "a * c = b * c \ c = 0 \ a = b" for a b c proof (cases "c = 0") case True then show ?thesis by simp next case False have "a = b" if "a * c = b * c" proof - from that have "a * c div c = b * c div c" by simp with False show ?thesis by simp qed then show ?thesis by auto qed show "c * a = c * b \ c = 0 \ a = b" for a b c using * [of a c b] by (simp add: ac_simps) qed lemma div_self [simp]: "a \ 0 \ a div a = 1" using nonzero_mult_div_cancel_left [of a 1] by simp lemma div_0 [simp]: "0 div a = 0" proof (cases "a = 0") case True then show ?thesis by simp next case False then have "a * 0 div a = 0" by (rule nonzero_mult_div_cancel_left) then show ?thesis by simp qed lemma div_by_1 [simp]: "a div 1 = a" using nonzero_mult_div_cancel_left [of 1 a] by simp lemma dvd_div_eq_0_iff: assumes "b dvd a" shows "a div b = 0 \ a = 0" using assms by (elim dvdE, cases "b = 0") simp_all lemma dvd_div_eq_cancel: "a div c = b div c \ c dvd a \ c dvd b \ a = b" by (elim dvdE, cases "c = 0") simp_all lemma dvd_div_eq_iff: "c dvd a \ c dvd b \ a div c = b div c \ a = b" by (elim dvdE, cases "c = 0") simp_all lemma inj_on_mult: "inj_on ((*) a) A" if "a \ 0" proof (rule inj_onI) fix b c assume "a * b = a * c" then have "a * b div a = a * c div a" by (simp only:) with that show "b = c" by simp qed end class idom_divide = idom + semidom_divide begin lemma dvd_neg_div: assumes "b dvd a" shows "- a div b = - (a div b)" proof (cases "b = 0") case True then show ?thesis by simp next case False from assms obtain c where "a = b * c" .. then have "- a div b = (b * - c) div b" by simp from False also have "\ = - c" by (rule nonzero_mult_div_cancel_left) with False \a = b * c\ show ?thesis by simp qed lemma dvd_div_neg: assumes "b dvd a" shows "a div - b = - (a div b)" proof (cases "b = 0") case True then show ?thesis by simp next case False then have "- b \ 0" by simp from assms obtain c where "a = b * c" .. then have "a div - b = (- b * - c) div - b" by simp from \- b \ 0\ also have "\ = - c" by (rule nonzero_mult_div_cancel_left) with False \a = b * c\ show ?thesis by simp qed end class algebraic_semidom = semidom_divide begin text \ Class \<^class>\algebraic_semidom\ enriches a integral domain by notions from algebra, like units in a ring. It is a separate class to avoid spoiling fields with notions which are degenerated there. \ lemma dvd_times_left_cancel_iff [simp]: assumes "a \ 0" shows "a * b dvd a * c \ b dvd c" (is "?lhs \ ?rhs") proof assume ?lhs then obtain d where "a * c = a * b * d" .. with assms have "c = b * d" by (simp add: ac_simps) then show ?rhs .. next assume ?rhs then obtain d where "c = b * d" .. then have "a * c = a * b * d" by (simp add: ac_simps) then show ?lhs .. qed lemma dvd_times_right_cancel_iff [simp]: assumes "a \ 0" shows "b * a dvd c * a \ b dvd c" using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps) lemma div_dvd_iff_mult: assumes "b \ 0" and "b dvd a" shows "a div b dvd c \ a dvd c * b" proof - from \b dvd a\ obtain d where "a = b * d" .. with \b \ 0\ show ?thesis by (simp add: ac_simps) qed lemma dvd_div_iff_mult: assumes "c \ 0" and "c dvd b" shows "a dvd b div c \ a * c dvd b" proof - from \c dvd b\ obtain d where "b = c * d" .. with \c \ 0\ show ?thesis by (simp add: mult.commute [of a]) qed lemma div_dvd_div [simp]: assumes "a dvd b" and "a dvd c" shows "b div a dvd c div a \ b dvd c" proof (cases "a = 0") case True with assms show ?thesis by simp next case False moreover from assms obtain k l where "b = a * k" and "c = a * l" by blast ultimately show ?thesis by simp qed lemma div_add [simp]: assumes "c dvd a" and "c dvd b" shows "(a + b) div c = a div c + b div c" proof (cases "c = 0") case True then show ?thesis by simp next case False moreover from assms obtain k l where "a = c * k" and "b = c * l" by blast moreover have "c * k + c * l = c * (k + l)" by (simp add: algebra_simps) ultimately show ?thesis by simp qed lemma div_mult_div_if_dvd: assumes "b dvd a" and "d dvd c" shows "(a div b) * (c div d) = (a * c) div (b * d)" proof (cases "b = 0 \ c = 0") case True with assms show ?thesis by auto next case False moreover from assms obtain k l where "a = b * k" and "c = d * l" by blast moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)" by (simp add: ac_simps) ultimately show ?thesis by simp qed lemma dvd_div_eq_mult: assumes "a \ 0" and "a dvd b" shows "b div a = c \ b = c * a" (is "?lhs \ ?rhs") proof assume ?rhs then show ?lhs by (simp add: assms) next assume ?lhs then have "b div a * a = c * a" by simp moreover from assms have "b div a * a = b" by (auto simp add: ac_simps) ultimately show ?rhs by simp qed lemma dvd_div_mult_self [simp]: "a dvd b \ b div a * a = b" by (cases "a = 0") (auto simp add: ac_simps) lemma dvd_mult_div_cancel [simp]: "a dvd b \ a * (b div a) = b" using dvd_div_mult_self [of a b] by (simp add: ac_simps) lemma div_mult_swap: assumes "c dvd b" shows "a * (b div c) = (a * b) div c" proof (cases "c = 0") case True then show ?thesis by simp next case False from assms obtain d where "b = c * d" .. moreover from False have "a * divide (d * c) c = ((a * d) * c) div c" by simp ultimately show ?thesis by (simp add: ac_simps) qed lemma dvd_div_mult: "c dvd b \ b div c * a = (b * a) div c" using div_mult_swap [of c b a] by (simp add: ac_simps) lemma dvd_div_mult2_eq: assumes "b * c dvd a" shows "a div (b * c) = a div b div c" proof - from assms obtain k where "a = b * c * k" .. then show ?thesis by (cases "b = 0 \ c = 0") (auto, simp add: ac_simps) qed lemma dvd_div_div_eq_mult: assumes "a \ 0" "c \ 0" and "a dvd b" "c dvd d" shows "b div a = d div c \ b * c = a * d" (is "?lhs \ ?rhs") proof - from assms have "a * c \ 0" by simp then have "?lhs \ b div a * (a * c) = d div c * (a * c)" by simp also have "\ \ (a * (b div a)) * c = (c * (d div c)) * a" by (simp add: ac_simps) also have "\ \ (a * b div a) * c = (c * d div c) * a" using assms by (simp add: div_mult_swap) also have "\ \ ?rhs" using assms by (simp add: ac_simps) finally show ?thesis . qed lemma dvd_mult_imp_div: assumes "a * c dvd b" shows "a dvd b div c" proof (cases "c = 0") case True then show ?thesis by simp next case False from \a * c dvd b\ obtain d where "b = a * c * d" .. with False show ?thesis by (simp add: mult.commute [of a] mult.assoc) qed lemma div_div_eq_right: assumes "c dvd b" "b dvd a" shows "a div (b div c) = a div b * c" proof (cases "c = 0 \ b = 0") case True then show ?thesis by auto next case False from assms obtain r s where "b = c * r" and "a = c * r * s" by blast moreover with False have "r \ 0" by auto ultimately show ?thesis using False by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c]) qed lemma div_div_div_same: assumes "d dvd b" "b dvd a" shows "(a div d) div (b div d) = a div b" proof (cases "b = 0 \ d = 0") case True with assms show ?thesis by auto next case False from assms obtain r s where "a = d * r * s" and "b = d * r" by blast with False show ?thesis by simp (simp add: ac_simps) qed text \Units: invertible elements in a ring\ abbreviation is_unit :: "'a \ bool" where "is_unit a \ a dvd 1" lemma not_is_unit_0 [simp]: "\ is_unit 0" by simp lemma unit_imp_dvd [dest]: "is_unit b \ b dvd a" by (rule dvd_trans [of _ 1]) simp_all lemma unit_dvdE: assumes "is_unit a" obtains c where "a \ 0" and "b = a * c" proof - from assms have "a dvd b" by auto then obtain c where "b = a * c" .. moreover from assms have "a \ 0" by auto ultimately show thesis using that by blast qed lemma dvd_unit_imp_unit: "a dvd b \ is_unit b \ is_unit a" by (rule dvd_trans) lemma unit_div_1_unit [simp, intro]: assumes "is_unit a" shows "is_unit (1 div a)" proof - from assms have "1 = 1 div a * a" by simp then show "is_unit (1 div a)" by (rule dvdI) qed lemma is_unitE [elim?]: assumes "is_unit a" obtains b where "a \ 0" and "b \ 0" and "is_unit b" and "1 div a = b" and "1 div b = a" and "a * b = 1" and "c div a = c * b" proof (rule that) define b where "b = 1 div a" then show "1 div a = b" by simp from assms b_def show "is_unit b" by simp with assms show "a \ 0" and "b \ 0" by auto from assms b_def show "a * b = 1" by simp then have "1 = a * b" .. with b_def \b \ 0\ show "1 div b = a" by simp from assms have "a dvd c" .. then obtain d where "c = a * d" .. with \a \ 0\ \a * b = 1\ show "c div a = c * b" by (simp add: mult.assoc mult.left_commute [of a]) qed lemma unit_prod [intro]: "is_unit a \ is_unit b \ is_unit (a * b)" by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) lemma is_unit_mult_iff: "is_unit (a * b) \ is_unit a \ is_unit b" by (auto dest: dvd_mult_left dvd_mult_right) lemma unit_div [intro]: "is_unit a \ is_unit b \ is_unit (a div b)" by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod) lemma mult_unit_dvd_iff: assumes "is_unit b" shows "a * b dvd c \ a dvd c" proof assume "a * b dvd c" with assms show "a dvd c" by (simp add: dvd_mult_left) next assume "a dvd c" then obtain k where "c = a * k" .. with assms have "c = (a * b) * (1 div b * k)" by (simp add: mult_ac) then show "a * b dvd c" by (rule dvdI) qed lemma mult_unit_dvd_iff': "is_unit a \ (a * b) dvd c \ b dvd c" using mult_unit_dvd_iff [of a b c] by (simp add: ac_simps) lemma dvd_mult_unit_iff: assumes "is_unit b" shows "a dvd c * b \ a dvd c" proof assume "a dvd c * b" with assms have "c * b dvd c * (b * (1 div b))" by (subst mult_assoc [symmetric]) simp also from assms have "b * (1 div b) = 1" by (rule is_unitE) simp finally have "c * b dvd c" by simp with \a dvd c * b\ show "a dvd c" by (rule dvd_trans) next assume "a dvd c" then show "a dvd c * b" by simp qed lemma dvd_mult_unit_iff': "is_unit b \ a dvd b * c \ a dvd c" using dvd_mult_unit_iff [of b a c] by (simp add: ac_simps) lemma div_unit_dvd_iff: "is_unit b \ a div b dvd c \ a dvd c" by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff) lemma dvd_div_unit_iff: "is_unit b \ a dvd c div b \ a dvd c" by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff) lemmas unit_dvd_iff = mult_unit_dvd_iff mult_unit_dvd_iff' dvd_mult_unit_iff dvd_mult_unit_iff' div_unit_dvd_iff dvd_div_unit_iff (* FIXME consider named_theorems *) lemma unit_mult_div_div [simp]: "is_unit a \ b * (1 div a) = b div a" by (erule is_unitE [of _ b]) simp lemma unit_div_mult_self [simp]: "is_unit a \ b div a * a = b" by (rule dvd_div_mult_self) auto lemma unit_div_1_div_1 [simp]: "is_unit a \ 1 div (1 div a) = a" by (erule is_unitE) simp lemma unit_div_mult_swap: "is_unit c \ a * (b div c) = (a * b) div c" by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c]) lemma unit_div_commute: "is_unit b \ (a div b) * c = (a * c) div b" using unit_div_mult_swap [of b c a] by (simp add: ac_simps) lemma unit_eq_div1: "is_unit b \ a div b = c \ a = c * b" by (auto elim: is_unitE) lemma unit_eq_div2: "is_unit b \ a = c div b \ a * b = c" using unit_eq_div1 [of b c a] by auto lemma unit_mult_left_cancel: "is_unit a \ a * b = a * c \ b = c" using mult_cancel_left [of a b c] by auto lemma unit_mult_right_cancel: "is_unit a \ b * a = c * a \ b = c" using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps) lemma unit_div_cancel: assumes "is_unit a" shows "b div a = c div a \ b = c" proof - from assms have "is_unit (1 div a)" by simp then have "b * (1 div a) = c * (1 div a) \ b = c" by (rule unit_mult_right_cancel) with assms show ?thesis by simp qed lemma is_unit_div_mult2_eq: assumes "is_unit b" and "is_unit c" shows "a div (b * c) = a div b div c" proof - from assms have "is_unit (b * c)" by (simp add: unit_prod) then have "b * c dvd a" by (rule unit_imp_dvd) then show ?thesis by (rule dvd_div_mult2_eq) qed lemma is_unit_div_mult_cancel_left: assumes "a \ 0" and "is_unit b" shows "a div (a * b) = 1 div b" proof - from assms have "a div (a * b) = a div a div b" by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq) with assms show ?thesis by simp qed lemma is_unit_div_mult_cancel_right: assumes "a \ 0" and "is_unit b" shows "a div (b * a) = 1 div b" using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps) lemma unit_div_eq_0_iff: assumes "is_unit b" shows "a div b = 0 \ a = 0" by (rule dvd_div_eq_0_iff) (insert assms, auto) lemma div_mult_unit2: "is_unit c \ b dvd a \ a div (b * c) = a div b div c" by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff) text \Coprimality\ definition coprime :: "'a \ 'a \ bool" where "coprime a b \ (\c. c dvd a \ c dvd b \ is_unit c)" lemma coprimeI: assumes "\c. c dvd a \ c dvd b \ is_unit c" shows "coprime a b" using assms by (auto simp: coprime_def) lemma not_coprimeI: assumes "c dvd a" and "c dvd b" and "\ is_unit c" shows "\ coprime a b" using assms by (auto simp: coprime_def) lemma coprime_common_divisor: "is_unit c" if "coprime a b" and "c dvd a" and "c dvd b" using that by (auto simp: coprime_def) lemma not_coprimeE: assumes "\ coprime a b" obtains c where "c dvd a" and "c dvd b" and "\ is_unit c" using assms by (auto simp: coprime_def) lemma coprime_imp_coprime: "coprime a b" if "coprime c d" and "\e. \ is_unit e \ e dvd a \ e dvd b \ e dvd c" and "\e. \ is_unit e \ e dvd a \ e dvd b \ e dvd d" proof (rule coprimeI) fix e assume "e dvd a" and "e dvd b" with that have "e dvd c" and "e dvd d" by (auto intro: dvd_trans) with \coprime c d\ show "is_unit e" by (rule coprime_common_divisor) qed lemma coprime_divisors: "coprime a b" if "a dvd c" "b dvd d" and "coprime c d" using \coprime c d\ proof (rule coprime_imp_coprime) fix e assume "e dvd a" then show "e dvd c" using \a dvd c\ by (rule dvd_trans) assume "e dvd b" then show "e dvd d" using \b dvd d\ by (rule dvd_trans) qed lemma coprime_self [simp]: "coprime a a \ is_unit a" (is "?P \ ?Q") proof assume ?P then show ?Q by (rule coprime_common_divisor) simp_all next assume ?Q show ?P by (rule coprimeI) (erule dvd_unit_imp_unit, rule \?Q\) qed lemma coprime_commute [ac_simps]: "coprime b a \ coprime a b" unfolding coprime_def by auto lemma is_unit_left_imp_coprime: "coprime a b" if "is_unit a" proof (rule coprimeI) fix c assume "c dvd a" with that show "is_unit c" by (auto intro: dvd_unit_imp_unit) qed lemma is_unit_right_imp_coprime: "coprime a b" if "is_unit b" using that is_unit_left_imp_coprime [of b a] by (simp add: ac_simps) lemma coprime_1_left [simp]: "coprime 1 a" by (rule coprimeI) lemma coprime_1_right [simp]: "coprime a 1" by (rule coprimeI) lemma coprime_0_left_iff [simp]: "coprime 0 a \ is_unit a" by (auto intro: coprimeI dvd_unit_imp_unit coprime_common_divisor [of 0 a a]) lemma coprime_0_right_iff [simp]: "coprime a 0 \ is_unit a" using coprime_0_left_iff [of a] by (simp add: ac_simps) lemma coprime_mult_self_left_iff [simp]: "coprime (c * a) (c * b) \ is_unit c \ coprime a b" by (auto intro: coprime_common_divisor) (rule coprimeI, auto intro: coprime_common_divisor simp add: dvd_mult_unit_iff')+ lemma coprime_mult_self_right_iff [simp]: "coprime (a * c) (b * c) \ is_unit c \ coprime a b" using coprime_mult_self_left_iff [of c a b] by (simp add: ac_simps) lemma coprime_absorb_left: assumes "x dvd y" shows "coprime x y \ is_unit x" using assms coprime_common_divisor is_unit_left_imp_coprime by auto lemma coprime_absorb_right: assumes "y dvd x" shows "coprime x y \ is_unit y" using assms coprime_common_divisor is_unit_right_imp_coprime by auto end class unit_factor = fixes unit_factor :: "'a \ 'a" class semidom_divide_unit_factor = semidom_divide + unit_factor + assumes unit_factor_0 [simp]: "unit_factor 0 = 0" and is_unit_unit_factor: "a dvd 1 \ unit_factor a = a" and unit_factor_is_unit: "a \ 0 \ unit_factor a dvd 1" and unit_factor_mult_unit_left: "a dvd 1 \ unit_factor (a * b) = a * unit_factor b" \ \This fine-grained hierarchy will later on allow lean normalization of polynomials\ begin lemma unit_factor_mult_unit_right: "a dvd 1 \ unit_factor (b * a) = unit_factor b * a" using unit_factor_mult_unit_left[of a b] by (simp add: mult_ac) lemmas [simp] = unit_factor_mult_unit_left unit_factor_mult_unit_right end class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor + fixes normalize :: "'a \ 'a" assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a" and normalize_0 [simp]: "normalize 0 = 0" begin text \ Class \<^class>\normalization_semidom\ cultivates the idea that each integral domain can be split into equivalence classes whose representants are associated, i.e. divide each other. \<^const>\normalize\ specifies a canonical representant for each equivalence class. The rationale behind this is that it is easier to reason about equality than equivalences, hence we prefer to think about equality of normalized values rather than associated elements. \ declare unit_factor_is_unit [iff] lemma unit_factor_dvd [simp]: "a \ 0 \ unit_factor a dvd b" by (rule unit_imp_dvd) simp lemma unit_factor_self [simp]: "unit_factor a dvd a" by (cases "a = 0") simp_all lemma normalize_mult_unit_factor [simp]: "normalize a * unit_factor a = a" using unit_factor_mult_normalize [of a] by (simp add: ac_simps) lemma normalize_eq_0_iff [simp]: "normalize a = 0 \ a = 0" (is "?lhs \ ?rhs") proof assume ?lhs moreover have "unit_factor a * normalize a = a" by simp ultimately show ?rhs by simp next assume ?rhs then show ?lhs by simp qed lemma unit_factor_eq_0_iff [simp]: "unit_factor a = 0 \ a = 0" (is "?lhs \ ?rhs") proof assume ?lhs moreover have "unit_factor a * normalize a = a" by simp ultimately show ?rhs by simp next assume ?rhs then show ?lhs by simp qed lemma div_unit_factor [simp]: "a div unit_factor a = normalize a" proof (cases "a = 0") case True then show ?thesis by simp next case False then have "unit_factor a \ 0" by simp with nonzero_mult_div_cancel_left have "unit_factor a * normalize a div unit_factor a = normalize a" by blast then show ?thesis by simp qed lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a" proof (cases "a = 0") case True then show ?thesis by simp next case False have "normalize a div a = normalize a div (unit_factor a * normalize a)" by simp also have "\ = 1 div unit_factor a" using False by (subst is_unit_div_mult_cancel_right) simp_all finally show ?thesis . qed lemma is_unit_normalize: assumes "is_unit a" shows "normalize a = 1" proof - from assms have "unit_factor a = a" by (rule is_unit_unit_factor) moreover from assms have "a \ 0" by auto moreover have "normalize a = a div unit_factor a" by simp ultimately show ?thesis by simp qed lemma unit_factor_1 [simp]: "unit_factor 1 = 1" by (rule is_unit_unit_factor) simp lemma normalize_1 [simp]: "normalize 1 = 1" by (rule is_unit_normalize) simp lemma normalize_1_iff: "normalize a = 1 \ is_unit a" (is "?lhs \ ?rhs") proof assume ?rhs then show ?lhs by (rule is_unit_normalize) next assume ?lhs then have "unit_factor a * normalize a = unit_factor a * 1" by simp then have "unit_factor a = a" by simp moreover from \?lhs\ have "a \ 0" by auto then have "is_unit (unit_factor a)" by simp ultimately show ?rhs by simp qed lemma div_normalize [simp]: "a div normalize a = unit_factor a" proof (cases "a = 0") case True then show ?thesis by simp next case False then have "normalize a \ 0" by simp with nonzero_mult_div_cancel_right have "unit_factor a * normalize a div normalize a = unit_factor a" by blast then show ?thesis by simp qed lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b" by (cases "b = 0") simp_all lemma inv_unit_factor_eq_0_iff [simp]: "1 div unit_factor a = 0 \ a = 0" (is "?lhs \ ?rhs") proof assume ?lhs then have "a * (1 div unit_factor a) = a * 0" by simp then show ?rhs by simp next assume ?rhs then show ?lhs by simp qed lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a" by (cases "a = 0") (auto intro: is_unit_unit_factor) lemma normalize_unit_factor [simp]: "a \ 0 \ normalize (unit_factor a) = 1" by (rule is_unit_normalize) simp lemma normalize_mult_unit_left [simp]: assumes "a dvd 1" shows "normalize (a * b) = normalize b" proof (cases "b = 0") case False have "a * unit_factor b * normalize (a * b) = unit_factor (a * b) * normalize (a * b)" using assms by (subst unit_factor_mult_unit_left) auto also have "\ = a * b" by simp also have "b = unit_factor b * normalize b" by simp hence "a * b = a * unit_factor b * normalize b" by (simp only: mult_ac) finally show ?thesis using assms False by auto qed auto lemma normalize_mult_unit_right [simp]: assumes "b dvd 1" shows "normalize (a * b) = normalize a" using assms by (subst mult.commute) auto lemma normalize_idem [simp]: "normalize (normalize a) = normalize a" proof (cases "a = 0") case False have "normalize a = normalize (unit_factor a * normalize a)" by simp also from False have "\ = normalize (normalize a)" by (subst normalize_mult_unit_left) auto finally show ?thesis .. qed auto lemma unit_factor_normalize [simp]: assumes "a \ 0" shows "unit_factor (normalize a) = 1" proof - from assms have *: "normalize a \ 0" by simp have "unit_factor (normalize a) * normalize (normalize a) = normalize a" by (simp only: unit_factor_mult_normalize) then have "unit_factor (normalize a) * normalize a = normalize a" by simp with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a" by simp with * show ?thesis by simp qed lemma normalize_dvd_iff [simp]: "normalize a dvd b \ a dvd b" proof - have "normalize a dvd b \ unit_factor a * normalize a dvd b" using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b] by (cases "a = 0") simp_all then show ?thesis by simp qed lemma dvd_normalize_iff [simp]: "a dvd normalize b \ a dvd b" proof - have "a dvd normalize b \ a dvd normalize b * unit_factor b" using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"] by (cases "b = 0") simp_all then show ?thesis by simp qed lemma normalize_idem_imp_unit_factor_eq: assumes "normalize a = a" shows "unit_factor a = of_bool (a \ 0)" proof (cases "a = 0") case True then show ?thesis by simp next case False then show ?thesis using assms unit_factor_normalize [of a] by simp qed lemma normalize_idem_imp_is_unit_iff: assumes "normalize a = a" shows "is_unit a \ a = 1" using assms by (cases "a = 0") (auto dest: is_unit_normalize) lemma coprime_normalize_left_iff [simp]: "coprime (normalize a) b \ coprime a b" by (rule; rule coprimeI) (auto intro: coprime_common_divisor) lemma coprime_normalize_right_iff [simp]: "coprime a (normalize b) \ coprime a b" using coprime_normalize_left_iff [of b a] by (simp add: ac_simps) text \ We avoid an explicit definition of associated elements but prefer explicit normalisation instead. In theory we could define an abbreviation like \<^prop>\associated a b \ normalize a = normalize b\ but this is counterproductive without suggestive infix syntax, which we do not want to sacrifice for this purpose here. \ lemma associatedI: assumes "a dvd b" and "b dvd a" shows "normalize a = normalize b" proof (cases "a = 0 \ b = 0") case True with assms show ?thesis by auto next case False from \a dvd b\ obtain c where b: "b = a * c" .. moreover from \b dvd a\ obtain d where a: "a = b * d" .. ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps) with False have "1 = c * d" unfolding mult_cancel_left by simp then have "is_unit c" and "is_unit d" by auto with a b show ?thesis by (simp add: is_unit_normalize) qed lemma associatedD1: "normalize a = normalize b \ a dvd b" using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric] by simp lemma associatedD2: "normalize a = normalize b \ b dvd a" using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric] by simp lemma associated_unit: "normalize a = normalize b \ is_unit a \ is_unit b" using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2) lemma associated_iff_dvd: "normalize a = normalize b \ a dvd b \ b dvd a" (is "?lhs \ ?rhs") proof assume ?rhs then show ?lhs by (auto intro!: associatedI) next assume ?lhs then have "unit_factor a * normalize a = unit_factor a * normalize b" by simp then have *: "normalize b * unit_factor a = a" by (simp add: ac_simps) show ?rhs proof (cases "a = 0 \ b = 0") case True with \?lhs\ show ?thesis by auto next case False then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b" by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff) with * show ?thesis by simp qed qed lemma associated_eqI: assumes "a dvd b" and "b dvd a" assumes "normalize a = a" and "normalize b = b" shows "a = b" proof - from assms have "normalize a = normalize b" unfolding associated_iff_dvd by simp with \normalize a = a\ have "a = normalize b" by simp with \normalize b = b\ show "a = b" by simp qed lemma normalize_unit_factor_eqI: assumes "normalize a = normalize b" and "unit_factor a = unit_factor b" shows "a = b" proof - from assms have "unit_factor a * normalize a = unit_factor b * normalize b" by simp then show ?thesis by simp qed lemma normalize_mult_normalize_left [simp]: "normalize (normalize a * b) = normalize (a * b)" by (rule associated_eqI) (auto intro!: mult_dvd_mono) lemma normalize_mult_normalize_right [simp]: "normalize (a * normalize b) = normalize (a * b)" by (rule associated_eqI) (auto intro!: mult_dvd_mono) end class normalization_semidom_multiplicative = normalization_semidom + assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" begin lemma normalize_mult: "normalize (a * b) = normalize a * normalize b" proof (cases "a = 0 \ b = 0") case True then show ?thesis by auto next case False have "unit_factor (a * b) * normalize (a * b) = a * b" by (rule unit_factor_mult_normalize) then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp also have "\ = a * b div unit_factor (b * a)" by (simp add: ac_simps) also have "\ = a * b div unit_factor b div unit_factor a" using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric]) also have "\ = a * (b div unit_factor b) div unit_factor a" using False by (subst unit_div_mult_swap) simp_all also have "\ = normalize a * normalize b" using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric]) finally show ?thesis . qed lemma dvd_unit_factor_div: assumes "b dvd a" shows "unit_factor (a div b) = unit_factor a div unit_factor b" proof - from assms have "a = a div b * b" by simp then have "unit_factor a = unit_factor (a div b * b)" by simp then show ?thesis by (cases "b = 0") (simp_all add: unit_factor_mult) qed lemma dvd_normalize_div: assumes "b dvd a" shows "normalize (a div b) = normalize a div normalize b" proof - from assms have "a = a div b * b" by simp then have "normalize a = normalize (a div b * b)" by simp then show ?thesis by (cases "b = 0") (simp_all add: normalize_mult) qed end text \Syntactic division remainder operator\ class modulo = dvd + divide + fixes modulo :: "'a \ 'a \ 'a" (infixl "mod" 70) text \Arbitrary quotient and remainder partitions\ class semiring_modulo = comm_semiring_1_cancel + divide + modulo + assumes div_mult_mod_eq: "a div b * b + a mod b = a" begin lemma mod_div_decomp: fixes a b obtains q r where "q = a div b" and "r = a mod b" and "a = q * b + r" proof - from div_mult_mod_eq have "a = a div b * b + a mod b" by simp moreover have "a div b = a div b" .. moreover have "a mod b = a mod b" .. note that ultimately show thesis by blast qed lemma mult_div_mod_eq: "b * (a div b) + a mod b = a" using div_mult_mod_eq [of a b] by (simp add: ac_simps) lemma mod_div_mult_eq: "a mod b + a div b * b = a" using div_mult_mod_eq [of a b] by (simp add: ac_simps) lemma mod_mult_div_eq: "a mod b + b * (a div b) = a" using div_mult_mod_eq [of a b] by (simp add: ac_simps) lemma minus_div_mult_eq_mod: "a - a div b * b = a mod b" by (rule add_implies_diff [symmetric]) (fact mod_div_mult_eq) lemma minus_mult_div_eq_mod: "a - b * (a div b) = a mod b" by (rule add_implies_diff [symmetric]) (fact mod_mult_div_eq) lemma minus_mod_eq_div_mult: "a - a mod b = a div b * b" by (rule add_implies_diff [symmetric]) (fact div_mult_mod_eq) lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)" by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq) lemma mod_0_imp_dvd [dest!]: "b dvd a" if "a mod b = 0" proof - have "b dvd (a div b) * b" by simp also have "(a div b) * b = a" using div_mult_mod_eq [of a b] by (simp add: that) finally show ?thesis . qed lemma [nitpick_unfold]: "a mod b = a - a div b * b" by (fact minus_div_mult_eq_mod [symmetric]) end subsection \Quotient and remainder in integral domains\ class semidom_modulo = algebraic_semidom + semiring_modulo begin lemma mod_0 [simp]: "0 mod a = 0" using div_mult_mod_eq [of 0 a] by simp lemma mod_by_0 [simp]: "a mod 0 = a" using div_mult_mod_eq [of a 0] by simp lemma mod_by_1 [simp]: "a mod 1 = 0" proof - from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp then have "a + a mod 1 = a + 0" by simp then show ?thesis by (rule add_left_imp_eq) qed lemma mod_self [simp]: "a mod a = 0" using div_mult_mod_eq [of a a] by simp lemma dvd_imp_mod_0 [simp]: "b mod a = 0" if "a dvd b" using that minus_div_mult_eq_mod [of b a] by simp lemma mod_eq_0_iff_dvd: "a mod b = 0 \ b dvd a" by (auto intro: mod_0_imp_dvd) lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]: "a dvd b \ b mod a = 0" by (simp add: mod_eq_0_iff_dvd) lemma dvd_mod_iff: assumes "c dvd b" shows "c dvd a mod b \ c dvd a" proof - from assms have "(c dvd a mod b) \ (c dvd ((a div b) * b + a mod b))" by (simp add: dvd_add_right_iff) also have "(a div b) * b + a mod b = a" using div_mult_mod_eq [of a b] by simp finally show ?thesis . qed lemma dvd_mod_imp_dvd: assumes "c dvd a mod b" and "c dvd b" shows "c dvd a" using assms dvd_mod_iff [of c b a] by simp lemma dvd_minus_mod [simp]: "b dvd a - a mod b" by (simp add: minus_mod_eq_div_mult) lemma cancel_div_mod_rules: "((a div b) * b + a mod b) + c = a + c" "(b * (a div b) + a mod b) + c = a + c" by (simp_all add: div_mult_mod_eq mult_div_mod_eq) end class idom_modulo = idom + semidom_modulo begin subclass idom_divide .. lemma div_diff [simp]: "c dvd a \ c dvd b \ (a - b) div c = a div c - b div c" using div_add [of _ _ "- b"] by (simp add: dvd_neg_div) end subsection \Interlude: basic tool support for algebraic and arithmetic calculations\ named_theorems arith "arith facts -- only ground formulas" ML_file \Tools/arith_data.ML\ ML_file \~~/src/Provers/Arith/cancel_div_mod.ML\ ML \ structure Cancel_Div_Mod_Ring = Cancel_Div_Mod ( val div_name = \<^const_name>\divide\; val mod_name = \<^const_name>\modulo\; val mk_binop = HOLogic.mk_binop; val mk_sum = Arith_Data.mk_sum; val dest_sum = Arith_Data.dest_sum; val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules}; val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps}) ) \ simproc_setup cancel_div_mod_int ("(a::'a::semidom_modulo) + b") = \K Cancel_Div_Mod_Ring.proc\ subsection \Ordered semirings and rings\ text \ The theory of partially ordered rings is taken from the books: \<^item> \<^emph>\Lattice Theory\ by Garret Birkhoff, American Mathematical Society, 1979 \<^item> \<^emph>\Partially Ordered Algebraic Systems\, Pergamon Press, 1963 Most of the used notions can also be looked up in \<^item> \<^url>\http://www.mathworld.com\ by Eric Weisstein et. al. \<^item> \<^emph>\Algebra I\ by van der Waerden, Springer \ class ordered_semiring = semiring + ordered_comm_monoid_add + assumes mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b" assumes mult_right_mono: "a \ b \ 0 \ c \ a * c \ b * c" begin lemma mult_mono: "a \ b \ c \ d \ 0 \ b \ 0 \ c \ a * c \ b * d" apply (erule (1) mult_right_mono [THEN order_trans]) apply (erule (1) mult_left_mono) done lemma mult_mono': "a \ b \ c \ d \ 0 \ a \ 0 \ c \ a * c \ b * d" by (rule mult_mono) (fast intro: order_trans)+ end lemma mono_mult: fixes a :: "'a::ordered_semiring" shows "a \ 0 \ mono ((*) a)" by (simp add: mono_def mult_left_mono) class ordered_semiring_0 = semiring_0 + ordered_semiring begin lemma mult_nonneg_nonneg [simp]: "0 \ a \ 0 \ b \ 0 \ a * b" using mult_left_mono [of 0 b a] by simp lemma mult_nonneg_nonpos: "0 \ a \ b \ 0 \ a * b \ 0" using mult_left_mono [of b 0 a] by simp lemma mult_nonpos_nonneg: "a \ 0 \ 0 \ b \ a * b \ 0" using mult_right_mono [of a 0 b] by simp text \Legacy -- use @{thm [source] mult_nonpos_nonneg}.\ lemma mult_nonneg_nonpos2: "0 \ a \ b \ 0 \ b * a \ 0" by (drule mult_right_mono [of b 0]) auto lemma split_mult_neg_le: "(0 \ a \ b \ 0) \ (a \ 0 \ 0 \ b) \ a * b \ 0" by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) end class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add begin subclass semiring_0_cancel .. subclass ordered_semiring_0 .. end class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add begin subclass ordered_cancel_semiring .. subclass ordered_cancel_comm_monoid_add .. subclass ordered_ab_semigroup_monoid_add_imp_le .. lemma mult_left_less_imp_less: "c * a < c * b \ 0 \ c \ a < b" by (force simp add: mult_left_mono not_le [symmetric]) lemma mult_right_less_imp_less: "a * c < b * c \ 0 \ c \ a < b" by (force simp add: mult_right_mono not_le [symmetric]) end class zero_less_one = order + zero + one + assumes zero_less_one [simp]: "0 < 1" begin subclass zero_neq_one by standard (simp add: less_imp_neq) lemma zero_le_one [simp]: \0 \ 1\ by (rule less_imp_le) simp end class linordered_semiring_1 = linordered_semiring + semiring_1 + zero_less_one begin lemma convex_bound_le: assumes "x \ a" "y \ a" "0 \ u" "0 \ v" "u + v = 1" shows "u * x + v * y \ a" proof- from assms have "u * x + v * y \ u * a + v * a" by (simp add: add_mono mult_left_mono) with assms show ?thesis unfolding distrib_right[symmetric] by simp qed end class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + assumes mult_strict_left_mono: "a < b \ 0 < c \ c * a < c * b" assumes mult_strict_right_mono: "a < b \ 0 < c \ a * c < b * c" begin subclass semiring_0_cancel .. subclass linordered_semiring proof fix a b c :: 'a assume *: "a \ b" "0 \ c" then show "c * a \ c * b" unfolding le_less using mult_strict_left_mono by (cases "c = 0") auto from * show "a * c \ b * c" unfolding le_less using mult_strict_right_mono by (cases "c = 0") auto qed lemma mult_left_le_imp_le: "c * a \ c * b \ 0 < c \ a \ b" by (auto simp add: mult_strict_left_mono _not_less [symmetric]) lemma mult_right_le_imp_le: "a * c \ b * c \ 0 < c \ a \ b" by (auto simp add: mult_strict_right_mono not_less [symmetric]) lemma mult_pos_pos[simp]: "0 < a \ 0 < b \ 0 < a * b" using mult_strict_left_mono [of 0 b a] by simp lemma mult_pos_neg: "0 < a \ b < 0 \ a * b < 0" using mult_strict_left_mono [of b 0 a] by simp lemma mult_neg_pos: "a < 0 \ 0 < b \ a * b < 0" using mult_strict_right_mono [of a 0 b] by simp text \Legacy -- use @{thm [source] mult_neg_pos}.\ lemma mult_pos_neg2: "0 < a \ b < 0 \ b * a < 0" by (drule mult_strict_right_mono [of b 0]) auto lemma zero_less_mult_pos: assumes "0 < a * b" "0 < a" shows "0 < b" proof (cases "b \ 0") case True then show ?thesis using assms by (auto simp: le_less dest: less_not_sym mult_pos_neg [of a b]) qed (auto simp add: le_less not_less) lemma zero_less_mult_pos2: assumes "0 < b * a" "0 < a" shows "0 < b" proof (cases "b \ 0") case True then show ?thesis using assms by (auto simp: le_less dest: less_not_sym mult_pos_neg2 [of a b]) qed (auto simp add: le_less not_less) text \Strict monotonicity in both arguments\ lemma mult_strict_mono: assumes "a < b" "c < d" "0 < b" "0 \ c" shows "a * c < b * d" proof (cases "c = 0") case True with assms show ?thesis by simp next case False with assms have "a*c < b*c" by (simp add: mult_strict_right_mono [OF \a < b\]) also have "\ < b*d" by (simp add: assms mult_strict_left_mono) finally show ?thesis . qed text \This weaker variant has more natural premises\ lemma mult_strict_mono': assumes "a < b" and "c < d" and "0 \ a" and "0 \ c" shows "a * c < b * d" by (rule mult_strict_mono) (insert assms, auto) lemma mult_less_le_imp_less: assumes "a < b" and "c \ d" and "0 \ a" and "0 < c" shows "a * c < b * d" proof - have "a * c < b * c" by (simp add: assms mult_strict_right_mono) also have "... \ b * d" by (intro mult_left_mono) (use assms in auto) finally show ?thesis . qed lemma mult_le_less_imp_less: assumes "a \ b" and "c < d" and "0 < a" and "0 \ c" shows "a * c < b * d" proof - have "a * c \ b * c" by (simp add: assms mult_right_mono) also have "... < b * d" by (intro mult_strict_left_mono) (use assms in auto) finally show ?thesis . qed end class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1 + zero_less_one begin subclass linordered_semiring_1 .. lemma convex_bound_lt: assumes "x < a" "y < a" "0 \ u" "0 \ v" "u + v = 1" shows "u * x + v * y < a" proof - from assms have "u * x + v * y < u * a + v * a" by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono) with assms show ?thesis unfolding distrib_right[symmetric] by simp qed end class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + assumes comm_mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b" begin subclass ordered_semiring proof fix a b c :: 'a assume "a \ b" "0 \ c" then show "c * a \ c * b" by (rule comm_mult_left_mono) then show "a * c \ b * c" by (simp only: mult.commute) qed end class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add begin subclass comm_semiring_0_cancel .. subclass ordered_comm_semiring .. subclass ordered_cancel_semiring .. end class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add + assumes comm_mult_strict_left_mono: "a < b \ 0 < c \ c * a < c * b" begin subclass linordered_semiring_strict proof fix a b c :: 'a assume "a < b" "0 < c" then show "c * a < c * b" by (rule comm_mult_strict_left_mono) then show "a * c < b * c" by (simp only: mult.commute) qed subclass ordered_cancel_comm_semiring proof fix a b c :: 'a assume "a \ b" "0 \ c" then show "c * a \ c * b" unfolding le_less using mult_strict_left_mono by (cases "c = 0") auto qed end class ordered_ring = ring + ordered_cancel_semiring begin subclass ordered_ab_group_add .. lemma less_add_iff1: "a * e + c < b * e + d \ (a - b) * e + c < d" by (simp add: algebra_simps) lemma less_add_iff2: "a * e + c < b * e + d \ c < (b - a) * e + d" by (simp add: algebra_simps) lemma le_add_iff1: "a * e + c \ b * e + d \ (a - b) * e + c \ d" by (simp add: algebra_simps) lemma le_add_iff2: "a * e + c \ b * e + d \ c \ (b - a) * e + d" by (simp add: algebra_simps) lemma mult_left_mono_neg: "b \ a \ c \ 0 \ c * a \ c * b" by (auto dest: mult_left_mono [of _ _ "- c"]) lemma mult_right_mono_neg: "b \ a \ c \ 0 \ a * c \ b * c" by (auto dest: mult_right_mono [of _ _ "- c"]) lemma mult_nonpos_nonpos: "a \ 0 \ b \ 0 \ 0 \ a * b" using mult_right_mono_neg [of a 0 b] by simp lemma split_mult_pos_le: "(0 \ a \ 0 \ b) \ (a \ 0 \ b \ 0) \ 0 \ a * b" by (auto simp add: mult_nonpos_nonpos) end class abs_if = minus + uminus + ord + zero + abs + assumes abs_if: "\a\ = (if a < 0 then - a else a)" class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if begin subclass ordered_ring .. subclass ordered_ab_group_add_abs proof fix a b show "\a + b\ \ \a\ + \b\" by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg) qed (auto simp: abs_if) lemma zero_le_square [simp]: "0 \ a * a" using linear [of 0 a] by (auto simp add: mult_nonpos_nonpos) lemma not_square_less_zero [simp]: "\ (a * a < 0)" by (simp add: not_less) proposition abs_eq_iff: "\x\ = \y\ \ x = y \ x = -y" by (auto simp add: abs_if split: if_split_asm) lemma abs_eq_iff': "\a\ = b \ b \ 0 \ (a = b \ a = - b)" by (cases "a \ 0") auto lemma eq_abs_iff': "a = \b\ \ a \ 0 \ (b = a \ b = - a)" using abs_eq_iff' [of b a] by auto lemma sum_squares_ge_zero: "0 \ x * x + y * y" by (intro add_nonneg_nonneg zero_le_square) lemma not_sum_squares_lt_zero: "\ x * x + y * y < 0" by (simp add: not_less sum_squares_ge_zero) end class linordered_ring_strict = ring + linordered_semiring_strict + ordered_ab_group_add + abs_if begin subclass linordered_ring .. lemma mult_strict_left_mono_neg: "b < a \ c < 0 \ c * a < c * b" using mult_strict_left_mono [of b a "- c"] by simp lemma mult_strict_right_mono_neg: "b < a \ c < 0 \ a * c < b * c" using mult_strict_right_mono [of b a "- c"] by simp lemma mult_neg_neg: "a < 0 \ b < 0 \ 0 < a * b" using mult_strict_right_mono_neg [of a 0 b] by simp subclass ring_no_zero_divisors proof fix a b assume "a \ 0" then have a: "a < 0 \ 0 < a" by (simp add: neq_iff) assume "b \ 0" then have b: "b < 0 \ 0 < b" by (simp add: neq_iff) have "a * b < 0 \ 0 < a * b" proof (cases "a < 0") case True show ?thesis proof (cases "b < 0") case True with \a < 0\ show ?thesis by (auto dest: mult_neg_neg) next case False with b have "0 < b" by auto with \a < 0\ show ?thesis by (auto dest: mult_strict_right_mono) qed next case False with a have "0 < a" by auto show ?thesis proof (cases "b < 0") case True with \0 < a\ show ?thesis by (auto dest: mult_strict_right_mono_neg) next case False with b have "0 < b" by auto with \0 < a\ show ?thesis by auto qed qed then show "a * b \ 0" by (simp add: neq_iff) qed lemma zero_less_mult_iff [algebra_split_simps, field_split_simps]: "0 < a * b \ 0 < a \ 0 < b \ a < 0 \ b < 0" by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases]) (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2) lemma zero_le_mult_iff [algebra_split_simps, field_split_simps]: "0 \ a * b \ 0 \ a \ 0 \ b \ a \ 0 \ b \ 0" by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff) lemma mult_less_0_iff [algebra_split_simps, field_split_simps]: "a * b < 0 \ 0 < a \ b < 0 \ a < 0 \ 0 < b" using zero_less_mult_iff [of "- a" b] by auto lemma mult_le_0_iff [algebra_split_simps, field_split_simps]: "a * b \ 0 \ 0 \ a \ b \ 0 \ a \ 0 \ 0 \ b" using zero_le_mult_iff [of "- a" b] by auto text \ Cancellation laws for \<^term>\c * a < c * b\ and \<^term>\a * c < b * c\, also with the relations \\\ and equality. \ text \ These ``disjunction'' versions produce two cases when the comparison is an assumption, but effectively four when the comparison is a goal. \ lemma mult_less_cancel_right_disj: "a * c < b * c \ 0 < c \ a < b \ c < 0 \ b < a" proof (cases "c = 0") case False show ?thesis (is "?lhs \ ?rhs") proof assume ?lhs then have "c < 0 \ b < a" "c > 0 \ b > a" by (auto simp flip: not_le intro: mult_right_mono mult_right_mono_neg) with False show ?rhs by (auto simp add: neq_iff) next assume ?rhs with False show ?lhs by (auto simp add: mult_strict_right_mono mult_strict_right_mono_neg) qed qed auto lemma mult_less_cancel_left_disj: "c * a < c * b \ 0 < c \ a < b \ c < 0 \ b < a" proof (cases "c = 0") case False show ?thesis (is "?lhs \ ?rhs") proof assume ?lhs then have "c < 0 \ b < a" "c > 0 \ b > a" by (auto simp flip: not_le intro: mult_left_mono mult_left_mono_neg) with False show ?rhs by (auto simp add: neq_iff) next assume ?rhs with False show ?lhs by (auto simp add: mult_strict_left_mono mult_strict_left_mono_neg) qed qed auto text \ The ``conjunction of implication'' lemmas produce two cases when the comparison is a goal, but give four when the comparison is an assumption. \ lemma mult_less_cancel_right: "a * c < b * c \ (0 \ c \ a < b) \ (c \ 0 \ b < a)" using mult_less_cancel_right_disj [of a c b] by auto lemma mult_less_cancel_left: "c * a < c * b \ (0 \ c \ a < b) \ (c \ 0 \ b < a)" using mult_less_cancel_left_disj [of c a b] by auto lemma mult_le_cancel_right: "a * c \ b * c \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" by (simp add: not_less [symmetric] mult_less_cancel_right_disj) lemma mult_le_cancel_left: "c * a \ c * b \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" by (simp add: not_less [symmetric] mult_less_cancel_left_disj) lemma mult_le_cancel_left_pos: "0 < c \ c * a \ c * b \ a \ b" by (auto simp: mult_le_cancel_left) lemma mult_le_cancel_left_neg: "c < 0 \ c * a \ c * b \ b \ a" by (auto simp: mult_le_cancel_left) lemma mult_less_cancel_left_pos: "0 < c \ c * a < c * b \ a < b" by (auto simp: mult_less_cancel_left) lemma mult_less_cancel_left_neg: "c < 0 \ c * a < c * b \ b < a" by (auto simp: mult_less_cancel_left) end lemmas mult_sign_intros = mult_nonneg_nonneg mult_nonneg_nonpos mult_nonpos_nonneg mult_nonpos_nonpos mult_pos_pos mult_pos_neg mult_neg_pos mult_neg_neg class ordered_comm_ring = comm_ring + ordered_comm_semiring begin subclass ordered_ring .. subclass ordered_cancel_comm_semiring .. end class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one + assumes add_mono1: "a < b \ a + 1 < b + 1" begin subclass zero_neq_one by standard (insert zero_less_one, blast) subclass comm_semiring_1 by standard (rule mult_1_left) lemma zero_le_one [simp]: "0 \ 1" by (rule zero_less_one [THEN less_imp_le]) lemma not_one_le_zero [simp]: "\ 1 \ 0" by (simp add: not_le) lemma not_one_less_zero [simp]: "\ 1 < 0" by (simp add: not_less) lemma of_bool_less_eq_iff [simp]: \of_bool P \ of_bool Q \ (P \ Q)\ by auto lemma of_bool_less_iff [simp]: \of_bool P < of_bool Q \ \ P \ Q\ by auto lemma mult_left_le: "c \ 1 \ 0 \ a \ a * c \ a" using mult_left_mono[of c 1 a] by simp lemma mult_le_one: "a \ 1 \ 0 \ b \ b \ 1 \ a * b \ 1" using mult_mono[of a 1 b 1] by simp lemma zero_less_two: "0 < 1 + 1" using add_pos_pos[OF zero_less_one zero_less_one] . end class linordered_semidom = semidom + linordered_comm_semiring_strict + zero_less_one + assumes le_add_diff_inverse2 [simp]: "b \ a \ a - b + b = a" begin subclass linordered_nonzero_semiring proof show "a + 1 < b + 1" if "a < b" for a b proof (rule ccontr, simp add: not_less) assume "b \ a" with that show False by simp qed qed lemma zero_less_eq_of_bool [simp]: \0 \ of_bool P\ by simp lemma zero_less_of_bool_iff [simp]: \0 < of_bool P \ P\ by simp lemma of_bool_less_eq_one [simp]: \of_bool P \ 1\ by simp lemma of_bool_less_one_iff [simp]: \of_bool P < 1 \ \ P\ by simp lemma of_bool_or_iff [simp]: \of_bool (P \ Q) = max (of_bool P) (of_bool Q)\ by (simp add: max_def) text \Addition is the inverse of subtraction.\ lemma le_add_diff_inverse [simp]: "b \ a \ b + (a - b) = a" by (frule le_add_diff_inverse2) (simp add: add.commute) lemma add_diff_inverse: "\ a < b \ b + (a - b) = a" by simp lemma add_le_imp_le_diff: assumes "i + k \ n" shows "i \ n - k" proof - have "n - (i + k) + i + k = n" by (simp add: assms add.assoc) with assms add_implies_diff have "i + k \ n - k + k" by fastforce then show ?thesis by simp qed lemma add_le_add_imp_diff_le: assumes 1: "i + k \ n" and 2: "n \ j + k" shows "i + k \ n \ n \ j + k \ n - k \ j" proof - have "n - (i + k) + i + k = n" using 1 by (simp add: add.assoc) moreover have "n - k = n - k - i + i" using 1 by (simp add: add_le_imp_le_diff) ultimately show ?thesis using 2 add_le_imp_le_diff [of "n-k" k "j + k"] by (simp add: add.commute diff_diff_add) qed lemma less_1_mult: "1 < m \ 1 < n \ 1 < m * n" using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one]) end class linordered_idom = comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn + assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)" begin subclass linordered_ring_strict .. subclass linordered_semiring_1_strict proof have "0 \ 1 * 1" by (fact zero_le_square) then show "0 < 1" by (simp add: le_less) qed subclass ordered_comm_ring .. subclass idom .. subclass linordered_semidom by standard simp subclass idom_abs_sgn by standard (auto simp add: sgn_if abs_if zero_less_mult_iff) lemma abs_bool_eq [simp]: \\of_bool P\ = of_bool P\ by simp lemma linorder_neqE_linordered_idom: assumes "x \ y" obtains "x < y" | "y < x" using assms by (rule neqE) text \These cancellation simp rules also produce two cases when the comparison is a goal.\ lemma mult_le_cancel_right1: "c \ b * c \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)" using mult_le_cancel_right [of 1 c b] by simp lemma mult_le_cancel_right2: "a * c \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)" using mult_le_cancel_right [of a c 1] by simp lemma mult_le_cancel_left1: "c \ c * b \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)" using mult_le_cancel_left [of c 1 b] by simp lemma mult_le_cancel_left2: "c * a \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)" using mult_le_cancel_left [of c a 1] by simp lemma mult_less_cancel_right1: "c < b * c \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)" using mult_less_cancel_right [of 1 c b] by simp lemma mult_less_cancel_right2: "a * c < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)" using mult_less_cancel_right [of a c 1] by simp lemma mult_less_cancel_left1: "c < c * b \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)" using mult_less_cancel_left [of c 1 b] by simp lemma mult_less_cancel_left2: "c * a < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)" using mult_less_cancel_left [of c a 1] by simp lemma sgn_0_0: "sgn a = 0 \ a = 0" by (fact sgn_eq_0_iff) lemma sgn_1_pos: "sgn a = 1 \ a > 0" unfolding sgn_if by simp lemma sgn_1_neg: "sgn a = - 1 \ a < 0" unfolding sgn_if by auto lemma sgn_pos [simp]: "0 < a \ sgn a = 1" by (simp only: sgn_1_pos) lemma sgn_neg [simp]: "a < 0 \ sgn a = - 1" by (simp only: sgn_1_neg) lemma abs_sgn: "\k\ = k * sgn k" unfolding sgn_if abs_if by auto lemma sgn_greater [simp]: "0 < sgn a \ 0 < a" unfolding sgn_if by auto lemma sgn_less [simp]: "sgn a < 0 \ a < 0" unfolding sgn_if by auto lemma abs_sgn_eq_1 [simp]: "a \ 0 \ \sgn a\ = 1" by simp lemma abs_sgn_eq: "\sgn a\ = (if a = 0 then 0 else 1)" by (simp add: sgn_if) lemma sgn_mult_self_eq [simp]: "sgn a * sgn a = of_bool (a \ 0)" by (cases "a > 0") simp_all lemma abs_mult_self_eq [simp]: "\a\ * \a\ = a * a" by (cases "a > 0") simp_all lemma same_sgn_sgn_add: "sgn (a + b) = sgn a" if "sgn b = sgn a" proof (cases a 0 rule: linorder_cases) case equal with that show ?thesis by simp next case less with that have "b < 0" by (simp add: sgn_1_neg) with \a < 0\ have "a + b < 0" by (rule add_neg_neg) with \a < 0\ show ?thesis by simp next case greater with that have "b > 0" by (simp add: sgn_1_pos) with \a > 0\ have "a + b > 0" by (rule add_pos_pos) with \a > 0\ show ?thesis by simp qed lemma same_sgn_abs_add: "\a + b\ = \a\ + \b\" if "sgn b = sgn a" proof - have "a + b = sgn a * \a\ + sgn b * \b\" by (simp add: sgn_mult_abs) also have "\ = sgn a * (\a\ + \b\)" using that by (simp add: algebra_simps) finally show ?thesis by (auto simp add: abs_mult) qed lemma sgn_not_eq_imp: "sgn a = - sgn b" if "sgn b \ sgn a" and "sgn a \ 0" and "sgn b \ 0" using that by (cases "a < 0") (auto simp add: sgn_0_0 sgn_1_pos sgn_1_neg) lemma abs_dvd_iff [simp]: "\m\ dvd k \ m dvd k" by (simp add: abs_if) lemma dvd_abs_iff [simp]: "m dvd \k\ \ m dvd k" by (simp add: abs_if) lemma dvd_if_abs_eq: "\l\ = \k\ \ l dvd k" by (subst abs_dvd_iff [symmetric]) simp text \ The following lemmas can be proven in more general structures, but are dangerous as simp rules in absence of @{thm neg_equal_zero}, @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. \ lemma equation_minus_iff_1 [simp, no_atp]: "1 = - a \ a = - 1" by (fact equation_minus_iff) lemma minus_equation_iff_1 [simp, no_atp]: "- a = 1 \ a = - 1" by (subst minus_equation_iff, auto) lemma le_minus_iff_1 [simp, no_atp]: "1 \ - b \ b \ - 1" by (fact le_minus_iff) lemma minus_le_iff_1 [simp, no_atp]: "- a \ 1 \ - 1 \ a" by (fact minus_le_iff) lemma less_minus_iff_1 [simp, no_atp]: "1 < - b \ b < - 1" by (fact less_minus_iff) lemma minus_less_iff_1 [simp, no_atp]: "- a < 1 \ - 1 < a" by (fact minus_less_iff) lemma add_less_zeroD: shows "x+y < 0 \ x<0 \ y<0" by (auto simp: not_less intro: le_less_trans [of _ "x+y"]) end text \Reasoning about inequalities with division\ context linordered_semidom begin lemma less_add_one: "a < a + 1" proof - have "a + 0 < a + 1" by (blast intro: zero_less_one add_strict_left_mono) then show ?thesis by simp qed end context linordered_idom begin lemma mult_right_le_one_le: "0 \ x \ 0 \ y \ y \ 1 \ x * y \ x" by (rule mult_left_le) lemma mult_left_le_one_le: "0 \ x \ 0 \ y \ y \ 1 \ y * x \ x" by (auto simp add: mult_le_cancel_right2) end text \Absolute Value\ context linordered_idom begin lemma mult_sgn_abs: "sgn x * \x\ = x" by (fact sgn_mult_abs) lemma abs_one: "\1\ = 1" by (fact abs_1) end class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs + assumes abs_eq_mult: "(0 \ a \ a \ 0) \ (0 \ b \ b \ 0) \ \a * b\ = \a\ * \b\" context linordered_idom begin subclass ordered_ring_abs by standard (auto simp: abs_if not_less mult_less_0_iff) lemma abs_mult_self: "\a\ * \a\ = a * a" by (fact abs_mult_self_eq) lemma abs_mult_less: assumes ac: "\a\ < c" and bd: "\b\ < d" shows "\a\ * \b\ < c * d" proof - from ac have "0 < c" by (blast intro: le_less_trans abs_ge_zero) with bd show ?thesis by (simp add: ac mult_strict_mono) qed lemma abs_less_iff: "\a\ < b \ a < b \ - a < b" by (simp add: less_le abs_le_iff) (auto simp add: abs_if) lemma abs_mult_pos: "0 \ x \ \y\ * x = \y * x\" by (simp add: abs_mult) +lemma abs_mult_pos': "0 \ x \ x * \y\ = \x * y\" + by (simp add: abs_mult) + lemma abs_diff_less_iff: "\x - a\ < r \ a - r < x \ x < a + r" by (auto simp add: diff_less_eq ac_simps abs_less_iff) lemma abs_diff_le_iff: "\x - a\ \ r \ a - r \ x \ x \ a + r" by (auto simp add: diff_le_eq ac_simps abs_le_iff) lemma abs_add_one_gt_zero: "0 < 1 + \x\" by (auto simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans) end subsection \Dioids\ text \ Dioids are the alternative extensions of semirings, a semiring can either be a ring or a dioid but never both. \ class dioid = semiring_1 + canonically_ordered_monoid_add begin subclass ordered_semiring by standard (auto simp: le_iff_add distrib_left distrib_right) end hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib code_identifier code_module Rings \ (SML) Arith and (OCaml) Arith and (Haskell) Arith end diff --git a/src/HOL/Set_Interval.thy b/src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy +++ b/src/HOL/Set_Interval.thy @@ -1,2578 +1,2580 @@ (* Title: HOL/Set_Interval.thy Author: Tobias Nipkow, Clemens Ballarin, Jeremy Avigad lessThan, greaterThan, atLeast, atMost and two-sided intervals Modern convention: Ixy stands for an interval where x and y describe the lower and upper bound and x,y : {c,o,i} where c = closed, o = open, i = infinite. Examples: Ico = {_ ..< _} and Ici = {_ ..} *) section \Set intervals\ theory Set_Interval imports Divides begin (* Belongs in Finite_Set but 2 is not available there *) lemma card_2_iff: "card S = 2 \ (\x y. S = {x,y} \ x \ y)" by (auto simp: card_Suc_eq numeral_eq_Suc) lemma card_2_iff': "card S = 2 \ (\x\S. \y\S. x \ y \ (\z\S. z = x \ z = y))" by (auto simp: card_Suc_eq numeral_eq_Suc) lemma card_3_iff: "card S = 3 \ (\x y z. S = {x,y,z} \ x \ y \ y \ z \ x \ z)" by (fastforce simp: card_Suc_eq numeral_eq_Suc) context ord begin definition lessThan :: "'a => 'a set" ("(1{..<_})") where "{.. 'a set" ("(1{.._})") where "{..u} == {x. x \ u}" definition greaterThan :: "'a => 'a set" ("(1{_<..})") where "{l<..} == {x. l 'a set" ("(1{_..})") where "{l..} == {x. l\x}" definition greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where "{l<.. 'a => 'a set" ("(1{_..<_})") where "{l.. 'a => 'a set" ("(1{_<.._})") where "{l<..u} == {l<..} Int {..u}" definition atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where "{l..u} == {l..} Int {..u}" end text\A note of warning when using \<^term>\{.. on type \<^typ>\nat\: it is equivalent to \<^term>\{0::nat.. but some lemmas involving \<^term>\{m.. may not exist in \<^term>\{..-form as well.\ syntax (ASCII) "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10) "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10) "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10) "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10) syntax (latex output) "_UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ \ _)/ _)" [0, 0, 10] 10) "_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10) "_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ \ _)/ _)" [0, 0, 10] 10) "_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10) syntax "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10) "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\_<_./ _)" [0, 0, 10] 10) "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10) "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\_<_./ _)" [0, 0, 10] 10) translations "\i\n. A" \ "\i\{..n}. A" "\i "\i\{..i\n. A" \ "\i\{..n}. A" "\i "\i\{..Various equivalences\ lemma (in ord) lessThan_iff [iff]: "(i \ lessThan k) = (i greaterThan k) = (k atLeast k) = (k<=i)" -by (simp add: atLeast_def) + by (simp add: atLeast_def) lemma Compl_atLeast [simp]: "!!k:: 'a::linorder. -atLeast k = lessThan k" by (auto simp add: lessThan_def atLeast_def) lemma (in ord) atMost_iff [iff]: "(i \ atMost k) = (i<=k)" by (simp add: atMost_def) lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" by (blast intro: order_antisym) lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \ { b <..} = { max a b <..}" by auto lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \ {..< b} = {..< min a b}" by auto subsection \Logical Equivalences for Set Inclusion and Equality\ lemma atLeast_empty_triv [simp]: "{{}..} = UNIV" by auto lemma atMost_UNIV_triv [simp]: "{..UNIV} = UNIV" by auto lemma atLeast_subset_iff [iff]: - "(atLeast x \ atLeast y) = (y \ (x::'a::preorder))" -by (blast intro: order_trans) + "(atLeast x \ atLeast y) = (y \ (x::'a::preorder))" + by (blast intro: order_trans) lemma atLeast_eq_iff [iff]: - "(atLeast x = atLeast y) = (x = (y::'a::order))" -by (blast intro: order_antisym order_trans) + "(atLeast x = atLeast y) = (x = (y::'a::order))" + by (blast intro: order_antisym order_trans) lemma greaterThan_subset_iff [iff]: - "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))" + "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))" unfolding greaterThan_def by (auto simp: linorder_not_less [symmetric]) lemma greaterThan_eq_iff [iff]: "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" by (auto simp: elim!: equalityE) lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::preorder))" by (blast intro: order_trans) lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::order))" by (blast intro: order_antisym order_trans) lemma lessThan_subset_iff [iff]: "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))" unfolding lessThan_def by (auto simp: linorder_not_less [symmetric]) lemma lessThan_eq_iff [iff]: "(lessThan x = lessThan y) = (x = (y::'a::linorder))" by (auto simp: elim!: equalityE) lemma lessThan_strict_subset_iff: fixes m n :: "'a::linorder" shows "{.. m < n" by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq) lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \ {b <..} \ b < a" by auto lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \ {..< b} \ a < b" by auto lemma (in preorder) Ioi_le_Ico: "{a <..} \ {a ..}" by (auto intro: less_imp_le) subsection \Two-sided intervals\ context ord begin lemma greaterThanLessThan_iff [simp]: "(i \ {l<.. i < u)" by (simp add: greaterThanLessThan_def) lemma atLeastLessThan_iff [simp]: "(i \ {l.. i \ i < u)" by (simp add: atLeastLessThan_def) lemma greaterThanAtMost_iff [simp]: "(i \ {l<..u}) = (l < i \ i \ u)" by (simp add: greaterThanAtMost_def) lemma atLeastAtMost_iff [simp]: "(i \ {l..u}) = (l \ i \ i \ u)" by (simp add: atLeastAtMost_def) text \The above four lemmas could be declared as iffs. Unfortunately this breaks many proofs. Since it only helps blast, it is better to leave them alone.\ lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \ {..< b }" by auto lemma (in order) atLeastLessThan_eq_atLeastAtMost_diff: "{a..Emptyness, singletons, subset\ context preorder begin lemma atLeastatMost_empty_iff[simp]: "{a..b} = {} \ (\ a \ b)" by auto (blast intro: order_trans) lemma atLeastatMost_empty_iff2[simp]: "{} = {a..b} \ (\ a \ b)" by auto (blast intro: order_trans) lemma atLeastLessThan_empty_iff[simp]: "{a.. (\ a < b)" by auto (blast intro: le_less_trans) lemma atLeastLessThan_empty_iff2[simp]: "{} = {a.. (\ a < b)" by auto (blast intro: le_less_trans) lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ \ k < l" by auto (blast intro: less_le_trans) lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ \ k < l" by auto (blast intro: less_le_trans) lemma atLeastatMost_subset_iff[simp]: "{a..b} \ {c..d} \ (\ a \ b) \ c \ a \ b \ d" unfolding atLeastAtMost_def atLeast_def atMost_def by (blast intro: order_trans) lemma atLeastatMost_psubset_iff: "{a..b} < {c..d} \ ((\ a \ b) \ c \ a \ b \ d \ (c < a \ b < d)) \ c \ d" by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) lemma atLeastAtMost_subseteq_atLeastLessThan_iff: "{a..b} \ {c ..< d} \ (a \ b \ c \ a \ b < d)" by auto (blast intro: local.order_trans local.le_less_trans elim: )+ lemma Icc_subset_Ici_iff[simp]: "{l..h} \ {l'..} = (\ l\h \ l\l')" by(auto simp: subset_eq intro: order_trans) lemma Icc_subset_Iic_iff[simp]: "{l..h} \ {..h'} = (\ l\h \ h\h')" by(auto simp: subset_eq intro: order_trans) lemma not_Ici_eq_empty[simp]: "{l..} \ {}" by(auto simp: set_eq_iff) lemma not_Iic_eq_empty[simp]: "{..h} \ {}" by(auto simp: set_eq_iff) lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric] lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric] end context order begin lemma atLeastatMost_empty[simp]: "b < a \ {a..b} = {}" by(auto simp: atLeastAtMost_def atLeast_def atMost_def) lemma atLeastLessThan_empty[simp]: "b \ a \ {a.. k ==> {k<..l} = {}" by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp lemma Icc_eq_Icc[simp]: "{l..h} = {l'..h'} = (l=l' \ h=h' \ \ l\h \ \ l'\h')" by (simp add: order_class.order.eq_iff) (auto intro: order_trans) +lemma (in linorder) Ico_eq_Ico: + "{l.. h=h' \ \ l \ l' a = b \ b = c" proof assume "{a..b} = {c}" hence *: "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp with \{a..b} = {c}\ have "c \ a \ b \ c" by auto with * show "a = b \ b = c" by auto qed simp end context no_top begin (* also holds for no_bot but no_top should suffice *) lemma not_UNIV_le_Icc[simp]: "\ UNIV \ {l..h}" using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) lemma not_UNIV_le_Iic[simp]: "\ UNIV \ {..h}" using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) lemma not_Ici_le_Icc[simp]: "\ {l..} \ {l'..h'}" using gt_ex[of h'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) lemma not_Ici_le_Iic[simp]: "\ {l..} \ {..h'}" using gt_ex[of h'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) end context no_bot begin lemma not_UNIV_le_Ici[simp]: "\ UNIV \ {l..}" using lt_ex[of l] by(auto simp: subset_eq less_le_not_le) lemma not_Iic_le_Icc[simp]: "\ {..h} \ {l'..h'}" using lt_ex[of l'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) lemma not_Iic_le_Ici[simp]: "\ {..h} \ {l'..}" using lt_ex[of l'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) end context no_top begin (* also holds for no_bot but no_top should suffice *) lemma not_UNIV_eq_Icc[simp]: "\ UNIV = {l'..h'}" using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric] lemma not_UNIV_eq_Iic[simp]: "\ UNIV = {..h'}" using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric] lemma not_Icc_eq_Ici[simp]: "\ {l..h} = {l'..}" unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric] (* also holds for no_bot but no_top should suffice *) lemma not_Iic_eq_Ici[simp]: "\ {..h} = {l'..}" using not_Ici_le_Iic[of l' h] by blast lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric] end context no_bot begin lemma not_UNIV_eq_Ici[simp]: "\ UNIV = {l'..}" using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le) lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric] lemma not_Icc_eq_Iic[simp]: "\ {l..h} = {..h'}" unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric] end context dense_linorder begin lemma greaterThanLessThan_empty_iff[simp]: "{ a <..< b } = {} \ b \ a" using dense[of a b] by (cases "a < b") auto lemma greaterThanLessThan_empty_iff2[simp]: "{} = { a <..< b } \ b \ a" using dense[of a b] by (cases "a < b") auto lemma atLeastLessThan_subseteq_atLeastAtMost_iff: "{a ..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)" using dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: "{a <.. b} \ { c .. d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: "{a <..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_greaterThanLessThan: "{a <..< b} \ {c <..< d} \ (a < b \ a \ c \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: "{a <.. b} \ { c ..< d } \ (a < b \ c \ a \ b < d)" using dense[of "a" "min c b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: "{a <..< b} \ { c ..< d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff: "{a <..< b} \ { c <.. d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) end context no_top begin lemma greaterThan_non_empty[simp]: "{x <..} \ {}" using gt_ex[of x] by auto end context no_bot begin lemma lessThan_non_empty[simp]: "{..< x} \ {}" using lt_ex[of x] by auto end lemma (in linorder) atLeastLessThan_subset_iff: "{a.. {c.. b \ a \ c\a \ b\d" apply (auto simp:subset_eq Ball_def not_le) apply(frule_tac x=a in spec) apply(erule_tac x=d in allE) apply auto done lemma atLeastLessThan_inj: fixes a b c d :: "'a::linorder" assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d" shows "a = c" "b = d" using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le antisym_conv2 subset_refl)+ lemma atLeastLessThan_eq_iff: fixes a b c d :: "'a::linorder" assumes "a < b" "c < d" shows "{a ..< b} = {c ..< d} \ a = c \ b = d" using atLeastLessThan_inj assms by auto lemma (in linorder) Ioc_inj: \{a <.. b} = {c <.. d} \ (b \ a \ d \ c) \ a = c \ b = d\ (is \?P \ ?Q\) proof assume ?Q then show ?P by auto next assume ?P then have \a < x \ x \ b \ c < x \ x \ d\ for x by (simp add: set_eq_iff) from this [of a] this [of b] this [of c] this [of d] show ?Q by auto qed lemma (in order) Iio_Int_singleton: "{.. {x} = (if x < k then {x} else {})" by auto lemma (in linorder) Ioc_subset_iff: "{a<..b} \ {c<..d} \ (b \ a \ c \ a \ b \ d)" by (auto simp: subset_eq Ball_def) (metis less_le not_less) lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot" by (auto simp: set_eq_iff intro: le_bot) lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \ x = top" by (auto simp: set_eq_iff intro: top_le) lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff: "{x..y} = UNIV \ (x = bot \ y = top)" by (auto simp: set_eq_iff intro: top_le le_bot) lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \ n = bot" by (auto simp: set_eq_iff not_less le_bot) lemma lessThan_empty_iff: "{..< n::nat} = {} \ n = 0" by (simp add: Iio_eq_empty_iff bot_nat_def) lemma mono_image_least: assumes f_mono: "mono f" and f_img: "f ` {m ..< n} = {m' ..< n'}" "m < n" shows "f m = m'" proof - from f_img have "{m' ..< n'} \ {}" by (metis atLeastLessThan_empty_iff image_is_empty) with f_img have "m' \ f ` {m ..< n}" by auto then obtain k where "f k = m'" "m \ k" by auto moreover have "m' \ f m" using f_img by auto ultimately show "f m = m'" using f_mono by (auto elim: monoE[where x=m and y=k]) qed subsection \Infinite intervals\ context dense_linorder begin lemma infinite_Ioo: assumes "a < b" shows "\ finite {a<.. {}" using \a < b\ by auto ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b" using Max_in[of "{a <..< b}"] by auto then obtain x where "Max {a <..< b} < x" "x < b" using dense[of "Max {a<.. {a <..< b}" using \a < Max {a <..< b}\ by auto then have "x \ Max {a <..< b}" using fin by auto with \Max {a <..< b} < x\ show False by auto qed lemma infinite_Icc: "a < b \ \ finite {a .. b}" using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b] by (auto dest: finite_subset) lemma infinite_Ico: "a < b \ \ finite {a ..< b}" using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b] by (auto dest: finite_subset) lemma infinite_Ioc: "a < b \ \ finite {a <.. b}" using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b] by (auto dest: finite_subset) lemma infinite_Ioo_iff [simp]: "infinite {a<.. a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioo) lemma infinite_Icc_iff [simp]: "infinite {a .. b} \ a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Icc) lemma infinite_Ico_iff [simp]: "infinite {a.. a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ico) lemma infinite_Ioc_iff [simp]: "infinite {a<..b} \ a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioc) end lemma infinite_Iio: "\ finite {..< a :: 'a :: {no_bot, linorder}}" proof assume "finite {..< a}" then have *: "\x. x < a \ Min {..< a} \ x" by auto obtain x where "x < a" using lt_ex by auto obtain y where "y < Min {..< a}" using lt_ex by auto also have "Min {..< a} \ x" using \x < a\ by fact also note \x < a\ finally have "Min {..< a} \ y" by fact with \y < Min {..< a}\ show False by auto qed lemma infinite_Iic: "\ finite {.. a :: 'a :: {no_bot, linorder}}" using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"] by (auto simp: subset_eq less_imp_le) lemma infinite_Ioi: "\ finite {a :: 'a :: {no_top, linorder} <..}" proof assume "finite {a <..}" then have *: "\x. a < x \ x \ Max {a <..}" by auto obtain y where "Max {a <..} < y" using gt_ex by auto obtain x where x: "a < x" using gt_ex by auto also from x have "x \ Max {a <..}" by fact also note \Max {a <..} < y\ finally have "y \ Max { a <..}" by fact with \Max {a <..} < y\ show False by auto qed lemma infinite_Ici: "\ finite {a :: 'a :: {no_top, linorder} ..}" using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"] by (auto simp: subset_eq less_imp_le) subsubsection \Intersection\ context linorder begin lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}" by auto lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}" by auto lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}" by auto lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}" by auto lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}" by auto lemma Int_atLeastLessThan[simp]: "{a.. {..b} = {.. min a b}" by (auto simp: min_def) lemma Ioc_disjoint: "{a<..b} \ {c<..d} = {} \ b \ a \ d \ c \ b \ c \ d \ a" by auto end context complete_lattice begin lemma shows Sup_atLeast[simp]: "Sup {x ..} = top" and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top" and Sup_atMost[simp]: "Sup {.. y} = y" and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y" and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y" by (auto intro!: Sup_eqI) lemma shows Inf_atMost[simp]: "Inf {.. x} = bot" and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot" and Inf_atLeast[simp]: "Inf {x ..} = x" and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x" and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x" by (auto intro!: Inf_eqI) end lemma fixes x y :: "'a :: {complete_lattice, dense_linorder}" shows Sup_lessThan[simp]: "Sup {..< y} = y" and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y" and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y" and Inf_greaterThan[simp]: "Inf {x <..} = x" and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x" and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x" by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded) subsection \Intervals of natural numbers\ subsubsection \The Constant \<^term>\lessThan\\ lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" by (simp add: lessThan_def) lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" by (simp add: lessThan_def less_Suc_eq, blast) text \The following proof is convenient in induction proofs where new elements get indices at the beginning. So it is used to transform \<^term>\{.. to \<^term>\0::nat\ and \<^term>\{..< n}\.\ lemma zero_notin_Suc_image [simp]: "0 \ Suc ` A" by auto lemma lessThan_Suc_eq_insert_0: "{..m::nat. lessThan m) = UNIV" by blast subsubsection \The Constant \<^term>\greaterThan\\ lemma greaterThan_0: "greaterThan 0 = range Suc" unfolding greaterThan_def by (blast dest: gr0_conv_Suc [THEN iffD1]) lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}" unfolding greaterThan_def by (auto elim: linorder_neqE) lemma INT_greaterThan_UNIV: "(\m::nat. greaterThan m) = {}" by blast subsubsection \The Constant \<^term>\atLeast\\ lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" by (unfold atLeast_def UNIV_def, simp) lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}" unfolding atLeast_def by (auto simp: order_le_less Suc_le_eq) lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k" by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) lemma UN_atLeast_UNIV: "(\m::nat. atLeast m) = UNIV" by blast subsubsection \The Constant \<^term>\atMost\\ lemma atMost_0 [simp]: "atMost (0::nat) = {0}" by (simp add: atMost_def) lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" unfolding atMost_def by (auto simp add: less_Suc_eq order_le_less) lemma UN_atMost_UNIV: "(\m::nat. atMost m) = UNIV" by blast subsubsection \The Constant \<^term>\atLeastLessThan\\ text\The orientation of the following 2 rules is tricky. The lhs is defined in terms of the rhs. Hence the chosen orientation makes sense in this theory --- the reverse orientation complicates proofs (eg nontermination). But outside, when the definition of the lhs is rarely used, the opposite orientation seems preferable because it reduces a specific concept to a more general one.\ lemma atLeast0LessThan [code_abbrev]: "{0::nat..The Constant \<^term>\atLeastAtMost\\ lemma Icc_eq_insert_lb_nat: "m \ n \ {m..n} = insert m {Suc m..n}" by auto lemma atLeast0_atMost_Suc: "{0..Suc n} = insert (Suc n) {0..n}" by (simp add: atLeast0AtMost atMost_Suc) lemma atLeast0_atMost_Suc_eq_insert_0: "{0..Suc n} = insert 0 (Suc ` {0..n})" by (simp add: atLeast0AtMost atMost_Suc_eq_insert_0) subsubsection \Intervals of nats with \<^term>\Suc\\ text\Not a simprule because the RHS is too messy.\ lemma atLeastLessThanSuc: "{m.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}" by auto lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}" by auto text \The analogous result is useful on \<^typ>\int\:\ (* here, because we don't have an own int section *) lemma atLeastAtMostPlus1_int_conv: "m \ 1+n \ {m..1+n} = insert (1+n) {m..n::int}" by (auto intro: set_eqI) lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j..Intervals and numerals\ lemma lessThan_nat_numeral: \ \Evaluation for specific numerals\ "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))" by (simp add: numeral_eq_Suc lessThan_Suc) lemma atMost_nat_numeral: \ \Evaluation for specific numerals\ "atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))" by (simp add: numeral_eq_Suc atMost_Suc) lemma atLeastLessThan_nat_numeral: \ \Evaluation for specific numerals\ "atLeastLessThan m (numeral k :: nat) = (if m \ (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k)) else {})" by (simp add: numeral_eq_Suc atLeastLessThanSuc) subsubsection \Image\ context linordered_semidom begin lemma image_add_atLeast[simp]: "plus k ` {i..} = {k + i..}" proof - have "n = k + (n - k)" if "i + k \ n" for n proof - have "n = (n - (k + i)) + (k + i)" using that by (metis add_commute le_add_diff_inverse) then show "n = k + (n - k)" by (metis local.add_diff_cancel_left' add_assoc add_commute) qed then show ?thesis by (fastforce simp: add_le_imp_le_diff add.commute) qed lemma image_add_atLeastAtMost [simp]: "plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B") proof show "?A \ ?B" by (auto simp add: ac_simps) next show "?B \ ?A" proof fix n assume "n \ ?B" then have "i \ n - k" by (simp add: add_le_imp_le_diff) have "n = n - k + k" proof - from \n \ ?B\ have "n = n - (i + k) + (i + k)" by simp also have "\ = n - k - i + i + k" by (simp add: algebra_simps) also have "\ = n - k + k" using \i \ n - k\ by simp finally show ?thesis . qed moreover have "n - k \ {i..j}" using \n \ ?B\ by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le) ultimately show "n \ ?A" by (simp add: ac_simps) qed qed lemma image_add_atLeastAtMost' [simp]: "(\n. n + k) ` {i..j} = {i + k..j + k}" by (simp add: add.commute [of _ k]) lemma image_add_atLeastLessThan [simp]: "plus k ` {i..n. n + k) ` {i.. uminus ` {x<..}" by (rule imageI) (simp add: *) thus "y \ uminus ` {x<..}" by simp next fix y assume "y \ -x" have "- (-y) \ uminus ` {x..}" by (rule imageI) (insert \y \ -x\[THEN le_imp_neg_le], simp) thus "y \ uminus ` {x..}" by simp qed simp_all lemma fixes x :: 'a shows image_uminus_lessThan[simp]: "uminus ` {.. = {c - b<..c - a}" by simp finally show ?thesis by simp qed lemma image_minus_const_greaterThanAtMost[simp]: fixes a b c::"'a::linordered_idom" shows "(-) c ` {a<..b} = {c - b.. = {c - b.. = {..c - a}" by simp finally show ?thesis by simp qed lemma image_minus_const_AtMost[simp]: fixes b c::"'a::linordered_idom" shows "(-) c ` {..b} = {c - b..}" proof - have "(-) c ` {..b} = (+) c ` uminus ` {..b}" unfolding image_image by simp also have "\ = {c - b..}" by simp finally show ?thesis by simp qed lemma image_minus_const_atLeastAtMost' [simp]: "(\t. t-d)`{a..b} = {a-d..b-d}" for d::"'a::linordered_idom" by (metis (no_types, lifting) diff_conv_add_uminus image_add_atLeastAtMost' image_cong) context linordered_field begin lemma image_mult_atLeastAtMost [simp]: "((*) d ` {a..b}) = {d*a..d*b}" if "d>0" using that by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x]) lemma image_divide_atLeastAtMost [simp]: "((\c. c / d) ` {a..b}) = {a/d..b/d}" if "d>0" proof - from that have "inverse d > 0" by simp with image_mult_atLeastAtMost [of "inverse d" a b] have "(*) (inverse d) ` {a..b} = {inverse d * a..inverse d * b}" by blast moreover have "(*) (inverse d) = (\c. c / d)" by (simp add: fun_eq_iff field_simps) ultimately show ?thesis by simp qed lemma image_mult_atLeastAtMost_if: "(*) c ` {x .. y} = (if c > 0 then {c * x .. c * y} else if x \ y then {c * y .. c * x} else {})" proof (cases "c = 0 \ x > y") case True then show ?thesis by auto next case False then have "x \ y" by auto from False consider "c < 0"| "c > 0" by (auto simp add: neq_iff) then show ?thesis proof cases case 1 have "(*) c ` {x..y} = {c * y..c * x}" proof (rule set_eqI) fix d from 1 have "inj (\z. z / c)" by (auto intro: injI) then have "d \ (*) c ` {x..y} \ d / c \ (\z. z div c) ` (*) c ` {x..y}" by (subst inj_image_mem_iff) simp_all also have "\ \ d / c \ {x..y}" using 1 by (simp add: image_image) also have "\ \ d \ {c * y..c * x}" by (auto simp add: field_simps 1) finally show "d \ (*) c ` {x..y} \ d \ {c * y..c * x}" . qed with \x \ y\ show ?thesis by auto qed (simp add: mult_left_mono_neg) qed lemma image_mult_atLeastAtMost_if': "(\x. x * c) ` {x..y} = (if x \ y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})" using image_mult_atLeastAtMost_if [of c x y] by (auto simp add: ac_simps) lemma image_affinity_atLeastAtMost: "((\x. m * x + c) ` {a..b}) = (if {a..b} = {} then {} else if 0 \ m then {m * a + c .. m * b + c} else {m * b + c .. m * a + c})" proof - have *: "(\x. m * x + c) = ((\x. x + c) \ (*) m)" by (simp add: fun_eq_iff) show ?thesis by (simp only: * image_comp [symmetric] image_mult_atLeastAtMost_if) (auto simp add: mult_le_cancel_left) qed lemma image_affinity_atLeastAtMost_diff: "((\x. m*x - c) ` {a..b}) = (if {a..b}={} then {} else if 0 \ m then {m*a - c .. m*b - c} else {m*b - c .. m*a - c})" using image_affinity_atLeastAtMost [of m "-c" a b] by simp lemma image_affinity_atLeastAtMost_div: "((\x. x/m + c) ` {a..b}) = (if {a..b}={} then {} else if 0 \ m then {a/m + c .. b/m + c} else {b/m + c .. a/m + c})" using image_affinity_atLeastAtMost [of "inverse m" c a b] by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide) lemma image_affinity_atLeastAtMost_div_diff: "((\x. x/m - c) ` {a..b}) = (if {a..b}={} then {} else if 0 \ m then {a/m - c .. b/m - c} else {b/m - c .. a/m - c})" using image_affinity_atLeastAtMost_diff [of "inverse m" c a b] by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide) end lemma atLeast1_lessThan_eq_remove0: "{Suc 0..x. x + (l::int)) ` {0..i. i - c) ` {x ..< y} = (if c < y then {x - c ..< y - c} else if x < y then {0} else {})" (is "_ = ?right") proof safe fix a assume a: "a \ ?right" show "a \ (\i. i - c) ` {x ..< y}" proof cases assume "c < y" with a show ?thesis by (auto intro!: image_eqI[of _ _ "a + c"]) next assume "\ c < y" with a show ?thesis by (auto intro!: image_eqI[of _ _ x] split: if_split_asm) qed qed auto lemma image_int_atLeastLessThan: "int ` {a..Finiteness\ lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..A bounded set of natural numbers is finite.\ lemma bounded_nat_set_is_finite: "(\i\N. i < (n::nat)) \ finite N" by (rule finite_subset [OF _ finite_lessThan]) auto text \A set of natural numbers is finite iff it is bounded.\ lemma finite_nat_set_iff_bounded: "finite(N::nat set) = (\m. \n\N. n?F\, simplified less_Suc_eq_le[symmetric]] by blast next assume ?B show ?F using \?B\ by(blast intro:bounded_nat_set_is_finite) qed lemma finite_nat_set_iff_bounded_le: "finite(N::nat set) = (\m. \n\N. n\m)" unfolding finite_nat_set_iff_bounded by (blast dest:less_imp_le_nat le_imp_less_Suc) lemma finite_less_ub: "!!f::nat=>nat. (!!n. n \ f n) ==> finite {n. f n \ u}" by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) lemma bounded_Max_nat: fixes P :: "nat \ bool" assumes x: "P x" and M: "\x. P x \ x \ M" obtains m where "P m" "\x. P x \ x \ m" proof - have "finite {x. P x}" using M finite_nat_set_iff_bounded_le by auto then have "Max {x. P x} \ {x. P x}" using Max_in x by auto then show ?thesis by (simp add: \finite {x. P x}\ that) qed text\Any subset of an interval of natural numbers the size of the subset is exactly that interval.\ lemma subset_card_intvl_is_intvl: assumes "A \ {k.. A" by auto with insert have "A \ {k..Proving Inclusions and Equalities between Unions\ lemma UN_le_eq_Un0: "(\i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B") proof show "?A \ ?B" proof fix x assume "x \ ?A" then obtain i where i: "i\n" "x \ M i" by auto show "x \ ?B" proof(cases i) case 0 with i show ?thesis by simp next case (Suc j) with i show ?thesis by auto qed qed next show "?B \ ?A" by fastforce qed lemma UN_le_add_shift: "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B") proof show "?A \ ?B" by fastforce next show "?B \ ?A" proof fix x assume "x \ ?B" then obtain i where i: "i \ {k..n+k}" "x \ M(i)" by auto hence "i-k\n \ x \ M((i-k)+k)" by auto thus "x \ ?A" by blast qed qed lemma UN_le_add_shift_strict: "(\ii\{k.. ?A" proof fix x assume "x \ ?B" then obtain i where i: "i \ {k.. M(i)" by auto then have "i - k < n \ x \ M((i-k) + k)" by auto then show "x \ ?A" using UN_le_add_shift by blast qed qed (fastforce) lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)" by (auto simp add: atLeast0LessThan) lemma UN_finite_subset: "(\n::nat. (\i\{0.. C) \ (\n. A n) \ C" by (subst UN_UN_finite_eq [symmetric]) blast lemma UN_finite2_subset: assumes "\n::nat. (\i\{0.. (\i\{0..n. A n) \ (\n. B n)" proof (rule UN_finite_subset, rule) fix n and a from assms have "(\i\{0.. (\i\{0.. (\i\{0.. (\i\{0.. (\i. B i)" by (auto simp add: UN_UN_finite_eq) qed lemma UN_finite2_eq: "(\n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)" apply (rule subset_antisym [OF UN_finite_subset UN_finite2_subset]) apply auto apply (force simp add: atLeastLessThan_add_Un [of 0])+ done subsubsection \Cardinality\ lemma card_lessThan [simp]: "card {..x. x + l) ` {.. {0.. {0..n}" shows "finite N" using assms finite_atLeastAtMost by (rule finite_subset) lemma ex_bij_betw_nat_finite: "finite M \ \h. bij_betw h {0.. \h. bij_betw h M {0.. finite B \ card A = card B \ \h. bij_betw h A B" apply(drule ex_bij_betw_finite_nat) apply(drule ex_bij_betw_nat_finite) apply(auto intro!:bij_betw_trans) done lemma ex_bij_betw_nat_finite_1: "finite M \ \h. bij_betw h {1 .. card M} M" by (rule finite_same_card_bij) auto lemma bij_betw_iff_card: assumes "finite A" "finite B" shows "(\f. bij_betw f A B) \ (card A = card B)" proof assume "card A = card B" moreover obtain f where "bij_betw f A {0 ..< card A}" using assms ex_bij_betw_finite_nat by blast moreover obtain g where "bij_betw g {0 ..< card B} B" using assms ex_bij_betw_nat_finite by blast ultimately have "bij_betw (g \ f) A B" by (auto simp: bij_betw_trans) thus "(\f. bij_betw f A B)" by blast qed (auto simp: bij_betw_same_card) lemma subset_eq_atLeast0_lessThan_card: fixes n :: nat assumes "N \ {0.. n" proof - from assms finite_lessThan have "card N \ card {0..Relational version of @{thm [source] card_inj_on_le}:\ lemma card_le_if_inj_on_rel: assumes "finite B" "\a. a \ A \ \b. b\B \ r a b" "\a1 a2 b. \ a1 \ A; a2 \ A; b \ B; r a1 b; r a2 b \ \ a1 = a2" shows "card A \ card B" proof - let ?P = "\a b. b \ B \ r a b" let ?f = "\a. SOME b. ?P a b" have 1: "?f ` A \ B" by (auto intro: someI2_ex[OF assms(2)]) have "inj_on ?f A" proof (auto simp: inj_on_def) fix a1 a2 assume asms: "a1 \ A" "a2 \ A" "?f a1 = ?f a2" have 0: "?f a1 \ B" using "1" \a1 \ A\ by blast have 1: "r a1 (?f a1)" using someI_ex[OF assms(2)[OF \a1 \ A\]] by blast have 2: "r a2 (?f a1)" using someI_ex[OF assms(2)[OF \a2 \ A\]] asms(3) by auto show "a1 = a2" using assms(3)[OF asms(1,2) 0 1 2] . qed with 1 show ?thesis using card_inj_on_le[of ?f A B] assms(1) by simp qed lemma inj_on_funpow_least: \<^marker>\contributor \Lars Noschinski\\ \inj_on (\k. (f ^^ k) s) {0.. if \(f ^^ n) s = s\ \\m. 0 < m \ m < n \ (f ^^ m) s \ s\ proof - { fix k l assume A: "k < n" "l < n" "k \ l" "(f ^^ k) s = (f ^^ l) s" define k' l' where "k' = min k l" and "l' = max k l" with A have A': "k' < l'" "(f ^^ k') s = (f ^^ l') s" "l' < n" by (auto simp: min_def max_def) have "s = (f ^^ ((n - l') + l')) s" using that \l' < n\ by simp also have "\ = (f ^^ (n - l')) ((f ^^ l') s)" by (simp add: funpow_add) also have "(f ^^ l') s = (f ^^ k') s" by (simp add: A') also have "(f ^^ (n - l')) \ = (f ^^ (n - l' + k')) s" by (simp add: funpow_add) finally have "(f ^^ (n - l' + k')) s = s" by simp moreover have "n - l' + k' < n" "0 < n - l' + k'"using A' by linarith+ ultimately have False using that(2) by auto } then show ?thesis by (intro inj_onI) auto qed subsection \Intervals of integers\ lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..Finiteness\ lemma image_atLeastZeroLessThan_int: "0 \ u ==> {(0::int).. u") case True then show ?thesis by (auto simp: image_atLeastZeroLessThan_int) qed auto lemma finite_atLeastLessThan_int [iff]: "finite {l..Cardinality\ lemma card_atLeastZeroLessThan_int: "card {(0::int).. u") case True then show ?thesis by (auto simp: image_atLeastZeroLessThan_int card_image inj_on_def) qed auto lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}" proof - have "{k. P k \ k < i} \ {.. M" shows "card {k \ M. k < Suc i} \ 0" proof - from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff) qed lemma card_less_Suc2: assumes "0 \ M" shows "card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}" proof - have *: "\j \ M; j < Suc i\ \ j - Suc 0 < i \ Suc (j - Suc 0) \ M \ Suc 0 \ j" for j by (cases j) (use assms in auto) show ?thesis proof (rule card_bij_eq) show "inj_on Suc {k. Suc k \ M \ k < i}" by force show "inj_on (\x. x - Suc 0) {k \ M. k < Suc i}" by (rule inj_on_diff_nat) (use * in blast) qed (use * in auto) qed lemma card_less_Suc: assumes "0 \ M" shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}" proof - have "Suc (card {k. Suc k \ M \ k < i}) = Suc (card {k. Suc k \ M - {0} \ k < i})" by simp also have "\ = Suc (card {k \ M - {0}. k < Suc i})" apply (subst card_less_Suc2) using assms by auto also have "\ = Suc (card ({k \ M. k < Suc i} - {0}))" by (force intro: arg_cong [where f=card]) also have "\ = card (insert 0 ({k \ M. k < Suc i} - {0}))" by (simp add: card.insert_remove) also have "... = card {k \ M. k < Suc i}" using assms by (force simp add: intro: arg_cong [where f=card]) finally show ?thesis. qed lemma card_le_Suc_Max: "finite S \ card S \ Suc (Max S)" proof (rule classical) assume "finite S" and "\ Suc (Max S) \ card S" then have "Suc (Max S) < card S" by simp with \finite S\ have "S \ {0..Max S}" by auto hence "card S \ card {0..Max S}" by (intro card_mono; auto) thus "card S \ Suc (Max S)" by simp qed subsection \Lemmas useful with the summation operator sum\ text \For examples, see Algebra/poly/UnivPoly2.thy\ subsubsection \Disjoint Unions\ text \Singletons and open intervals\ lemma ivl_disj_un_singleton: "{l::'a::linorder} Un {l<..} = {l..}" "{.. {l} Un {l<.. {l<.. u ==> {l} Un {l<..u} = {l..u}" "(l::'a::linorder) \ u ==> {l..One- and two-sided intervals\ lemma ivl_disj_un_one: "(l::'a::linorder) < u ==> {..l} Un {l<.. u ==> {.. u ==> {..l} Un {l<..u} = {..u}" "(l::'a::linorder) \ u ==> {.. u ==> {l<..u} Un {u<..} = {l<..}" "(l::'a::linorder) < u ==> {l<.. u ==> {l..u} Un {u<..} = {l..}" "(l::'a::linorder) \ u ==> {l..Two- and two-sided intervals\ lemma ivl_disj_un_two: "[| (l::'a::linorder) < m; m \ u |] ==> {l<.. m; m < u |] ==> {l<..m} Un {m<.. m; m \ u |] ==> {l.. m; m < u |] ==> {l..m} Un {m<.. u |] ==> {l<.. m; m \ u |] ==> {l<..m} Un {m<..u} = {l<..u}" "[| (l::'a::linorder) \ m; m \ u |] ==> {l.. m; m \ u |] ==> {l..m} Un {m<..u} = {l..u}" by auto lemma ivl_disj_un_two_touch: "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m.. m; m < u |] ==> {l..m} Un {m.. u |] ==> {l<..m} Un {m..u} = {l<..u}" "[| (l::'a::linorder) \ m; m \ u |] ==> {l..m} Un {m..u} = {l..u}" by auto lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch subsubsection \Disjoint Intersections\ text \One- and two-sided intervals\ lemma ivl_disj_int_one: "{..l::'a::order} Int {l<..Two- and two-sided intervals\ lemma ivl_disj_int_two: "{l::'a::order<..Some Differences\ lemma ivl_diff[simp]: "i \ n \ {i..Some Subset Conditions\ lemma ivl_subset [simp]: "({i.. {m.. i \ m \ i \ j \ (n::'a::linorder))" using linorder_class.le_less_linear[of i n] apply (auto simp: linorder_not_le) apply (force intro: leI)+ done lemma obtain_subset_with_card_n: assumes "n \ card S" obtains T where "T \ S" "card T = n" "finite T" proof - obtain n' where "card S = n + n'" by (metis assms le_add_diff_inverse) with that show thesis proof (induct n' arbitrary: S) case 0 then show ?case by (cases "finite S") auto next case Suc then show ?case by (simp add: card_Suc_eq) (metis subset_insertI2) qed qed subsection \Generic big monoid operation over intervals\ context semiring_char_0 begin lemma inj_on_of_nat [simp]: "inj_on of_nat N" by rule simp lemma bij_betw_of_nat [simp]: "bij_betw of_nat N A \ of_nat ` N = A" by (simp add: bij_betw_def) lemma Nats_infinite: "infinite (\ :: 'a set)" by (metis Nats_def finite_imageD infinite_UNIV_char_0 inj_on_of_nat) end context comm_monoid_set begin lemma atLeastLessThan_reindex: "F g {h m.. h) {m.. h) {m..n}" if "bij_betw h {m..n} {h m..h n}" for m n ::nat proof - from that have "inj_on h {m..n}" and "h ` {m..n} = {h m..h n}" by (simp_all add: bij_betw_def) then show ?thesis using reindex [of h "{m..n}" g] by simp qed lemma atLeastLessThan_shift_bounds: "F g {m + k.. plus k) {m.. plus k) {m..n}" for m n k :: nat using atLeastAtMost_reindex [of "plus k" m n g] by (simp add: ac_simps) lemma atLeast_Suc_lessThan_Suc_shift: "F g {Suc m.. Suc) {m.. Suc) {m..n}" using atLeastAtMost_shift_bounds [of _ _ 1] by (simp add: plus_1_eq_Suc) lemma atLeast_atMost_pred_shift: "F (g \ (\n. n - Suc 0)) {Suc m..Suc n} = F g {m..n}" unfolding atLeast_Suc_atMost_Suc_shift by simp lemma atLeast_lessThan_pred_shift: "F (g \ (\n. n - Suc 0)) {Suc m.. int) {m.. int) {m..n}" by (rule atLeastAtMost_reindex) (simp add: image_int_atLeastAtMost) lemma atLeast0_lessThan_Suc: "F g {0..* g n" by (simp add: atLeast0_lessThan_Suc ac_simps) lemma atLeast0_atMost_Suc: "F g {0..Suc n} = F g {0..n} \<^bold>* g (Suc n)" by (simp add: atLeast0_atMost_Suc ac_simps) lemma atLeast0_lessThan_Suc_shift: "F g {0..* F (g \ Suc) {0..* F (g \ Suc) {0..n}" by (simp add: atLeast0_atMost_Suc_eq_insert_0 atLeast_Suc_atMost_Suc_shift) lemma atLeast_Suc_lessThan: "F g {m..* F g {Suc m..* F g {Suc m..n}" if "m \ n" proof - from that have "{m..n} = insert m {Suc m..n}" by auto then show ?thesis by simp qed lemma ivl_cong: "a = c \ b = d \ (\x. c \ x \ x < d \ g x = h x) \ F g {a.. plus m) {0.. n") simp_all lemma atLeastAtMost_shift_0: fixes m n p :: nat assumes "m \ n" shows "F g {m..n} = F (g \ plus m) {0..n - m}" using assms atLeastAtMost_shift_bounds [of g 0 m "n - m"] by simp lemma atLeastLessThan_concat: fixes m n p :: nat shows "m \ n \ n \ p \ F g {m..* F g {n..i. g (m + n - Suc i)) {n..i. g (m + n - i)) {n..m}" by (rule reindex_bij_witness [where i="\i. m + n - i" and j="\i. m + n - i"]) auto lemma atLeastLessThan_rev_at_least_Suc_atMost: "F g {n..i. g (m + n - i)) {Suc n..m}" unfolding atLeastLessThan_rev [of g n m] by (cases m) (simp_all add: atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost) end subsection \Summation indexed over intervals\ syntax (ASCII) "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10) "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10) syntax (latex_sum output) "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ = _\<^latex>\}^{\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ = _\<^latex>\}^{<\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ < _\<^latex>\}$\ _)" [0,0,10] 10) "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ \ _\<^latex>\}$\ _)" [0,0,10] 10) syntax "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) translations "\x=a..b. t" == "CONST sum (\x. t) {a..b}" "\x=a..x. t) {a..i\n. t" == "CONST sum (\i. t) {..n}" "\ii. t) {..The above introduces some pretty alternative syntaxes for summation over intervals: \begin{center} \begin{tabular}{lll} Old & New & \LaTeX\\ @{term[source]"\x\{a..b}. e"} & \<^term>\\x=a..b. e\ & @{term[mode=latex_sum]"\x=a..b. e"}\\ @{term[source]"\x\{a..\\x=a.. & @{term[mode=latex_sum]"\x=a..x\{..b}. e"} & \<^term>\\x\b. e\ & @{term[mode=latex_sum]"\x\b. e"}\\ @{term[source]"\x\{..\\x & @{term[mode=latex_sum]"\xlatex_sum\ (e.g.\ via \mode = latex_sum\ in antiquotations). It is not the default \LaTeX\ output because it only works well with italic-style formulae, not tt-style. Note that for uniformity on \<^typ>\nat\ it is better to use \<^term>\\x::nat=0.. rather than \\x: \sum\ may not provide all lemmas available for \<^term>\{m.. also in the special form for \<^term>\{...\ text\This congruence rule should be used for sums over intervals as the standard theorem @{text[source]sum.cong} does not work well with the simplifier who adds the unsimplified premise \<^term>\x\B\ to the context.\ context comm_monoid_set begin lemma zero_middle: assumes "1 \ p" "k \ p" shows "F (\j. if j < k then g j else if j = k then \<^bold>1 else h (j - Suc 0)) {..p} = F (\j. if j < k then g j else h j) {..p - Suc 0}" (is "?lhs = ?rhs") proof - have [simp]: "{..p - Suc 0} \ {j. j < k} = {.. - {j. j < k} = {k..p - Suc 0}" using assms by auto have "?lhs = F g {..* F (\j. if j = k then \<^bold>1 else h (j - Suc 0)) {k..p}" using union_disjoint [of "{.. = F g {..* F (\j. h (j - Suc 0)) {Suc k..p}" by (simp add: atLeast_Suc_atMost [of k p] assms) also have "\ = F g {..* F h {k .. p - Suc 0}" using reindex [of Suc "{k..p - Suc 0}"] assms by simp also have "\ = ?rhs" by (simp add: If_cases) finally show ?thesis . qed lemma atMost_Suc [simp]: "F g {..Suc n} = F g {..n} \<^bold>* g (Suc n)" by (simp add: atMost_Suc ac_simps) lemma lessThan_Suc [simp]: "F g {..* g n" by (simp add: lessThan_Suc ac_simps) lemma cl_ivl_Suc [simp]: "F g {m..Suc n} = (if Suc n < m then \<^bold>1 else F g {m..n} \<^bold>* g(Suc n))" by (auto simp: ac_simps atLeastAtMostSuc_conv) lemma op_ivl_Suc [simp]: "F g {m..1 else F g {m..* g(n))" by (auto simp: ac_simps atLeastLessThanSuc) lemma head: fixes n :: nat assumes mn: "m \ n" shows "F g {m..n} = g m \<^bold>* F g {m<..n}" (is "?lhs = ?rhs") proof - from mn have "{m..n} = {m} \ {m<..n}" by (auto intro: ivl_disj_un_singleton) hence "?lhs = F g ({m} \ {m<..n})" by (simp add: atLeast0LessThan) also have "\ = ?rhs" by simp finally show ?thesis . qed lemma last_plus: fixes n::nat shows "m \ n \ F g {m..n} = g n \<^bold>* F g {m..1 else F g {m..* g(n))" by (simp add: commute last_plus) lemma ub_add_nat: assumes "(m::nat) \ n + 1" shows "F g {m..n + p} = F g {m..n} \<^bold>* F g {n + 1..n + p}" proof- have "{m .. n+p} = {m..n} \ {n+1..n+p}" using \m \ n+1\ by auto thus ?thesis by (auto simp: ivl_disj_int union_disjoint atLeastSucAtMost_greaterThanAtMost) qed lemma nat_group: fixes k::nat shows "F (\m. F g {m * k ..< m*k + k}) {.. 0" by auto then show ?thesis by (induct n) (simp_all add: atLeastLessThan_concat add.commute atLeast0LessThan[symmetric]) qed auto lemma triangle_reindex: fixes n :: nat shows "F (\(i,j). g i j) {(i,j). i+j < n} = F (\k. F (\i. g i (k - i)) {..k}) {..(i,j). g i j) {(i,j). i+j \ n} = F (\k. F (\i. g i (k - i)) {..k}) {..n}" using triangle_reindex [of g "Suc n"] by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost) lemma nat_diff_reindex: "F (\i. g (n - Suc i)) {..i. g(i + k)){m..i. g(i + k)){m..n::nat}" by (rule reindex_bij_witness[where i="\i. i + k" and j="\i. i - k"]) auto corollary shift_bounds_cl_Suc_ivl: "F g {Suc m..Suc n} = F (\i. g(Suc i)){m..n}" by (simp add: shift_bounds_cl_nat_ivl[where k="Suc 0", simplified]) corollary Suc_reindex_ivl: "m \ n \ F g {m..n} \<^bold>* g (Suc n) = g m \<^bold>* F (\i. g (Suc i)) {m..n}" by (simp add: assoc atLeast_Suc_atMost flip: shift_bounds_cl_Suc_ivl) corollary shift_bounds_Suc_ivl: "F g {Suc m..i. g(Suc i)){m..* F (\i. g (Suc i)) {..n}" proof (induct n) case 0 show ?case by simp next case (Suc n) note IH = this have "F g {..Suc (Suc n)} = F g {..Suc n} \<^bold>* g (Suc (Suc n))" by (rule atMost_Suc) also have "F g {..Suc n} = g 0 \<^bold>* F (\i. g (Suc i)) {..n}" by (rule IH) also have "g 0 \<^bold>* F (\i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)) = g 0 \<^bold>* (F (\i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)))" by (rule assoc) also have "F (\i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)) = F (\i. g (Suc i)) {..Suc n}" by (rule atMost_Suc [symmetric]) finally show ?case . qed lemma lessThan_Suc_shift: "F g {..* F (\i. g (Suc i)) {..* F (\i. g (Suc i)) {..i. F (\j. a i j) {0..j. F (\i. a i j) {Suc j..n}) {0..i. F (\j. a i j) {..j. F (\i. a i j) {Suc j..n}) {..k. g (Suc k)) {.. = F (\k. g (Suc k)) {.. b \ F g {a..* g b" by (simp add: atLeastLessThanSuc commute) lemma nat_ivl_Suc': assumes "m \ Suc n" shows "F g {m..Suc n} = g (Suc n) \<^bold>* F g {m..n}" proof - from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto also have "F g \ = g (Suc n) \<^bold>* F g {m..n}" by simp finally show ?thesis . qed lemma in_pairs: "F g {2*m..Suc(2*n)} = F (\i. g(2*i) \<^bold>* g(Suc(2*i))) {m..n}" proof (induction n) case 0 show ?case by (cases "m=0") auto next case (Suc n) then show ?case by (auto simp: assoc split: if_split_asm) qed lemma in_pairs_0: "F g {..Suc(2*n)} = F (\i. g(2*i) \<^bold>* g(Suc(2*i))) {..n}" using in_pairs [of _ 0 n] by (simp add: atLeast0AtMost) end lemma card_sum_le_nat_sum: "\ {0.. \ S" proof (cases "finite S") case True then show ?thesis proof (induction "card S" arbitrary: S) case (Suc x) then have "Max S \ x" using card_le_Suc_Max by fastforce let ?S' = "S - {Max S}" from Suc have "Max S \ S" by (auto intro: Max_in) hence cards: "card S = Suc (card ?S')" using \finite S\ by (intro card.remove; auto) hence "\ {0.. \ ?S'" using Suc by (intro Suc; auto) hence "\ {0.. \ ?S' + Max S" using \Max S \ x\ by simp also have "... = \ S" using sum.remove[OF \finite S\ \Max S \ S\, where g="\x. x"] by simp finally show ?case using cards Suc by auto qed simp qed simp lemma sum_natinterval_diff: fixes f:: "nat \ ('a::ab_group_add)" shows "sum (\k. f k - f(k + 1)) {(m::nat) .. n} = (if m \ n then f m - f(n + 1) else 0)" by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) lemma sum_diff_nat_ivl: fixes f :: "nat \ 'a::ab_group_add" shows "\ m \ n; n \ p \ \ sum f {m..x. Q x \ P x \ (\xxxShifting bounds\ context comm_monoid_add begin context fixes f :: "nat \ 'a" assumes "f 0 = 0" begin lemma sum_shift_lb_Suc0_0_upt: "sum f {Suc 0..f 0 = 0\ by simp qed lemma sum_shift_lb_Suc0_0: "sum f {Suc 0..k} = sum f {0..k}" proof (cases k) case 0 with \f 0 = 0\ show ?thesis by simp next case (Suc k) moreover have "{0..Suc k} = insert 0 {Suc 0..Suc k}" by auto ultimately show ?thesis using \f 0 = 0\ by simp qed end end lemma sum_Suc_diff: fixes f :: "nat \ 'a::ab_group_add" assumes "m \ Suc n" shows "(\i = m..n. f(Suc i) - f i) = f (Suc n) - f m" using assms by (induct n) (auto simp: le_Suc_eq) lemma sum_Suc_diff': fixes f :: "nat \ 'a::ab_group_add" assumes "m \ n" shows "(\i = m..Telescoping\ lemma sum_telescope: fixes f::"nat \ 'a::ab_group_add" shows "sum (\i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)" by (induct i) simp_all lemma sum_telescope'': assumes "m \ n" shows "(\k\{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)" by (rule dec_induct[OF assms]) (simp_all add: algebra_simps) lemma sum_lessThan_telescope: "(\nnThe formula for geometric sums\ lemma sum_power2: "(\i=0.. 1" shows "(\i 0" by simp_all moreover have "(\iy \ 0\) ultimately show ?thesis by simp qed lemma diff_power_eq_sum: fixes y :: "'a::{comm_ring,monoid_mult}" shows "x ^ (Suc n) - y ^ (Suc n) = (x - y) * (\pppp \\COMPLEX_POLYFUN\ in HOL Light\ fixes x :: "'a::{comm_ring,monoid_mult}" shows "x^n - y^n = (x - y) * (\iiiii\n. x^i) = 1 - x^Suc n" by (simp only: one_diff_power_eq lessThan_Suc_atMost) lemma sum_power_shift: fixes x :: "'a::{comm_ring,monoid_mult}" assumes "m \ n" shows "(\i=m..n. x^i) = x^m * (\i\n-m. x^i)" proof - have "(\i=m..n. x^i) = x^m * (\i=m..n. x^(i-m))" by (simp add: sum_distrib_left power_add [symmetric]) also have "(\i=m..n. x^(i-m)) = (\i\n-m. x^i)" using \m \ n\ by (intro sum.reindex_bij_witness[where j="\i. i - m" and i="\i. i + m"]) auto finally show ?thesis . qed lemma sum_gp_multiplied: fixes x :: "'a::{comm_ring,monoid_mult}" assumes "m \ n" shows "(1 - x) * (\i=m..n. x^i) = x^m - x^Suc n" proof - have "(1 - x) * (\i=m..n. x^i) = x^m * (1 - x) * (\i\n-m. x^i)" by (metis mult.assoc mult.commute assms sum_power_shift) also have "... =x^m * (1 - x^Suc(n-m))" by (metis mult.assoc sum_gp_basic) also have "... = x^m - x^Suc n" using assms by (simp add: algebra_simps) (metis le_add_diff_inverse power_add) finally show ?thesis . qed lemma sum_gp: fixes x :: "'a::{comm_ring,division_ring}" shows "(\i=m..n. x^i) = (if n < m then 0 else if x = 1 then of_nat((n + 1) - m) else (x^m - x^Suc n) / (1 - x))" using sum_gp_multiplied [of m n x] apply auto by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq) subsubsection\Geometric progressions\ lemma sum_gp0: fixes x :: "'a::{comm_ring,division_ring}" shows "(\i\n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))" using sum_gp_basic[of x n] by (simp add: mult.commute field_split_simps) lemma sum_power_add: fixes x :: "'a::{comm_ring,monoid_mult}" shows "(\i\I. x^(m+i)) = x^m * (\i\I. x^i)" by (simp add: sum_distrib_left power_add) lemma sum_gp_offset: fixes x :: "'a::{comm_ring,division_ring}" shows "(\i=m..m+n. x^i) = (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" using sum_gp [of x m "m+n"] by (auto simp: power_add algebra_simps) lemma sum_gp_strict: fixes x :: "'a::{comm_ring,division_ring}" shows "(\iThe formulae for arithmetic sums\ context comm_semiring_1 begin lemma double_gauss_sum: "2 * (\i = 0..n. of_nat i) = of_nat n * (of_nat n + 1)" by (induct n) (simp_all add: sum.atLeast0_atMost_Suc algebra_simps left_add_twice) lemma double_gauss_sum_from_Suc_0: "2 * (\i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1)" proof - have "sum of_nat {Suc 0..n} = sum of_nat (insert 0 {Suc 0..n})" by simp also have "\ = sum of_nat {0..n}" by (cases n) (simp_all add: atLeast0_atMost_Suc_eq_insert_0) finally show ?thesis by (simp add: double_gauss_sum) qed lemma double_arith_series: "2 * (\i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d)" proof - have "(\i = 0..n. a + of_nat i * d) = ((\i = 0..n. a) + (\i = 0..n. of_nat i * d))" by (rule sum.distrib) also have "\ = (of_nat (Suc n) * a + d * (\i = 0..n. of_nat i))" by (simp add: sum_distrib_left algebra_simps) finally show ?thesis by (simp add: algebra_simps double_gauss_sum left_add_twice) qed end context unique_euclidean_semiring_with_nat begin lemma gauss_sum: "(\i = 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2" using double_gauss_sum [of n, symmetric] by simp lemma gauss_sum_from_Suc_0: "(\i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2" using double_gauss_sum_from_Suc_0 [of n, symmetric] by simp lemma arith_series: "(\i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d) div 2" using double_arith_series [of a d n, symmetric] by simp end lemma gauss_sum_nat: "\{0..n} = (n * Suc n) div 2" using gauss_sum [of n, where ?'a = nat] by simp lemma arith_series_nat: "(\i = 0..n. a + i * d) = Suc n * (2 * a + n * d) div 2" using arith_series [of a d n] by simp lemma Sum_Icc_int: "\{m..n} = (n * (n + 1) - m * (m - 1)) div 2" if "m \ n" for m n :: int using that proof (induct i \ "nat (n - m)" arbitrary: m n) case 0 then have "m = n" by arith then show ?case by (simp add: algebra_simps mult_2 [symmetric]) next case (Suc i) have 0: "i = nat((n-1) - m)" "m \ n-1" using Suc(2,3) by arith+ have "\ {m..n} = \ {m..1+(n-1)}" by simp also have "\ = \ {m..n-1} + n" using \m \ n\ by(subst atLeastAtMostPlus1_int_conv) simp_all also have "\ = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" by(simp add: Suc(1)[OF 0]) also have "\ = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp also have "\ = (n*(n+1) - m*(m-1)) div 2" by (simp add: algebra_simps mult_2_right) finally show ?case . qed lemma Sum_Icc_nat: "\{m..n} = (n * (n + 1) - m * (m - 1)) div 2" for m n :: nat proof (cases "m \ n") case True then have *: "m * (m - 1) \ n * (n + 1)" by (meson diff_le_self order_trans le_add1 mult_le_mono) have "int (\{m..n}) = (\{int m..int n})" by (simp add: sum.atLeast_int_atMost_int_shift) also have "\ = (int n * (int n + 1) - int m * (int m - 1)) div 2" using \m \ n\ by (simp add: Sum_Icc_int) also have "\ = int ((n * (n + 1) - m * (m - 1)) div 2)" using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff) finally show ?thesis by (simp only: of_nat_eq_iff) next case False then show ?thesis by (auto dest: less_imp_Suc_add simp add: not_le algebra_simps) qed lemma Sum_Ico_nat: "\{m..Division remainder\ lemma range_mod: fixes n :: nat assumes "n > 0" shows "range (\m. m mod n) = {0.. ?A \ m \ ?B" proof assume "m \ ?A" with assms show "m \ ?B" by auto next assume "m \ ?B" moreover have "m mod n \ ?A" by (rule rangeI) ultimately show "m \ ?A" by simp qed qed subsection \Products indexed over intervals\ syntax (ASCII) "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10) "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10) "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10) "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10) syntax (latex_prod output) "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{<\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ < _\<^latex>\}$\ _)" [0,0,10] 10) "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ \ _\<^latex>\}$\ _)" [0,0,10] 10) syntax "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) translations "\x=a..b. t" \ "CONST prod (\x. t) {a..b}" "\x=a.. "CONST prod (\x. t) {a..i\n. t" \ "CONST prod (\i. t) {..n}" "\i "CONST prod (\i. t) {..{int i..int (i+j)}" by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv) lemma prod_int_eq: "prod int {i..j} = \{int i..int j}" proof (cases "i \ j") case True then show ?thesis by (metis le_iff_add prod_int_plus_eq) next case False then show ?thesis by auto qed subsection \Efficient folding over intervals\ function fold_atLeastAtMost_nat where [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc = (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))" by pat_completeness auto termination by (relation "measure (\(_,a,b,_). Suc b - a)") auto lemma fold_atLeastAtMost_nat: assumes "comp_fun_commute f" shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}" using assms proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases) case (1 f a b acc) interpret comp_fun_commute f by fact show ?case proof (cases "a > b") case True thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto next case False with 1 show ?thesis by (subst fold_atLeastAtMost_nat.simps) (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm) qed qed lemma sum_atLeastAtMost_code: "sum f {a..b} = fold_atLeastAtMost_nat (\a acc. f a + acc) a b 0" proof - have "comp_fun_commute (\a. (+) (f a))" by unfold_locales (auto simp: o_def add_ac) thus ?thesis by (simp add: sum.eq_fold fold_atLeastAtMost_nat o_def) qed lemma prod_atLeastAtMost_code: "prod f {a..b} = fold_atLeastAtMost_nat (\a acc. f a * acc) a b 1" proof - have "comp_fun_commute (\a. (*) (f a))" by unfold_locales (auto simp: o_def mult_ac) thus ?thesis by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def) qed (* TODO: Add support for folding over more kinds of intervals here *) end