diff --git a/src/HOL/Analysis/Ball_Volume.thy b/src/HOL/Analysis/Ball_Volume.thy --- a/src/HOL/Analysis/Ball_Volume.thy +++ b/src/HOL/Analysis/Ball_Volume.thy @@ -1,333 +1,330 @@ -(* +(* File: HOL/Analysis/Ball_Volume.thy Author: Manuel Eberl, TU München *) section \The Volume of an \n\-Dimensional Ball\ theory Ball_Volume imports Gamma_Function Lebesgue_Integral_Substitution begin text \ We define the volume of the unit ball in terms of the Gamma function. Note that the dimension need not be an integer; we also allow fractional dimensions, although we do not use this case or prove anything about it for now. \ definition\<^marker>\tag important\ unit_ball_vol :: "real \ real" where "unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)" lemma unit_ball_vol_pos [simp]: "n \ 0 \ unit_ball_vol n > 0" by (force simp: unit_ball_vol_def intro: divide_nonneg_pos) lemma unit_ball_vol_nonneg [simp]: "n \ 0 \ unit_ball_vol n \ 0" by (simp add: dual_order.strict_implies_order) text \ We first need the value of the following integral, which is at the core of - computing the measure of an \n + 1\-dimensional ball in terms of the measure of an + computing the measure of an \n + 1\-dimensional ball in terms of the measure of an \n\-dimensional one. \ lemma emeasure_cball_aux_integral: - "(\\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \lborel) = + "(\\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \lborel) = ennreal (Beta (1 / 2) (real n / 2 + 1))" proof - have "((\t. t powr (-1 / 2) * (1 - t) powr (real n / 2)) has_integral Beta (1 / 2) (real n / 2 + 1)) {0..1}" using has_integral_Beta_real[of "1/2" "n / 2 + 1"] by simp from nn_integral_has_integral_lebesgue[OF _ this] have "ennreal (Beta (1 / 2) (real n / 2 + 1)) = - nn_integral lborel (\t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) * + nn_integral lborel (\t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) * indicator {0^2..1^2} t))" by (simp add: mult_ac ennreal_mult' ennreal_indicator) also have "\ = (\\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) * indicator {0..1} x) \lborel)" by (subst nn_integral_substitution[where g = "\x. x ^ 2" and g' = "\x. 2 * x"]) (auto intro!: derivative_eq_intros continuous_intros simp: set_borel_measurable_def) also have "\ = (\\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \lborel)" - by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) + by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) (auto simp: indicator_def powr_minus powr_half_sqrt field_split_simps ennreal_mult') also have "\ = (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \lborel) + (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \lborel)" (is "_ = ?I + _") by (simp add: mult_2 nn_integral_add) also have "?I = (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..0} x) \lborel)" by (subst nn_integral_real_affine[of _ "-1" 0]) (auto simp: indicator_def intro!: nn_integral_cong) hence "?I + ?I = \ + ?I" by simp - also have "\ = (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * + also have "\ = (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * (indicator {-1..0} x + indicator{0..1} x)) \lborel)" by (subst nn_integral_add [symmetric]) (auto simp: algebra_simps) also have "\ = (\\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..1} x) \lborel)" by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) (auto simp: indicator_def) also have "\ = (\\<^sup>+ x. ennreal (indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n) \lborel)" by (intro nn_integral_cong_AE AE_I[of _ _ "{1, -1}"]) (auto simp: powr_half_sqrt [symmetric] indicator_def abs_square_le_1 abs_square_eq_1 powr_def exp_of_nat_mult [symmetric] emeasure_lborel_countable) finally show ?thesis .. qed lemma real_sqrt_le_iff': "x \ 0 \ y \ 0 \ sqrt x \ y \ x \ y ^ 2" using real_le_lsqrt sqrt_le_D by blast -lemma power2_le_iff_abs_le: "y \ 0 \ (x::real) ^ 2 \ y ^ 2 \ abs x \ y" - by (subst real_sqrt_le_iff' [symmetric]) auto - text \ - Isabelle's type system makes it very difficult to do an induction over the dimension - of a Euclidean space type, because the type would change in the inductive step. To avoid - this problem, we instead formulate the problem in a more concrete way by unfolding the + Isabelle's type system makes it very difficult to do an induction over the dimension + of a Euclidean space type, because the type would change in the inductive step. To avoid + this problem, we instead formulate the problem in a more concrete way by unfolding the definition of the Euclidean norm. \ lemma emeasure_cball_aux: assumes "finite A" "r > 0" shows "emeasure (Pi\<^sub>M A (\_. lborel)) ({f. sqrt (\i\A. (f i)\<^sup>2) \ r} \ space (Pi\<^sub>M A (\_. lborel))) = ennreal (unit_ball_vol (real (card A)) * r ^ card A)" using assms proof (induction arbitrary: r) case (empty r) thus ?case by (simp add: unit_ball_vol_def space_PiM) next case (insert i A r) interpret product_sigma_finite "\_. lborel" by standard - have "emeasure (Pi\<^sub>M (insert i A) (\_. lborel)) + have "emeasure (Pi\<^sub>M (insert i A) (\_. lborel)) ({f. sqrt (\i\insert i A. (f i)\<^sup>2) \ r} \ space (Pi\<^sub>M (insert i A) (\_. lborel))) = nn_integral (Pi\<^sub>M (insert i A) (\_. lborel)) (indicator ({f. sqrt (\i\insert i A. (f i)\<^sup>2) \ r} \ space (Pi\<^sub>M (insert i A) (\_. lborel))))" by (subst nn_integral_indicator) auto - also have "\ = (\\<^sup>+ y. \\<^sup>+ x. indicator ({f. sqrt ((f i)\<^sup>2 + (\i\A. (f i)\<^sup>2)) \ r} \ - space (Pi\<^sub>M (insert i A) (\_. lborel))) (x(i := y)) + also have "\ = (\\<^sup>+ y. \\<^sup>+ x. indicator ({f. sqrt ((f i)\<^sup>2 + (\i\A. (f i)\<^sup>2)) \ r} \ + space (Pi\<^sub>M (insert i A) (\_. lborel))) (x(i := y)) \Pi\<^sub>M A (\_. lborel) \lborel)" using insert.prems insert.hyps by (subst product_nn_integral_insert_rev) auto - also have "\ = (\\<^sup>+ (y::real). \\<^sup>+ x. indicator {-r..r} y * indicator ({f. sqrt ((\i\A. (f i)\<^sup>2)) \ + also have "\ = (\\<^sup>+ (y::real). \\<^sup>+ x. indicator {-r..r} y * indicator ({f. sqrt ((\i\A. (f i)\<^sup>2)) \ sqrt (r ^ 2 - y ^ 2)} \ space (Pi\<^sub>M A (\_. lborel))) x \Pi\<^sub>M A (\_. lborel) \lborel)" proof (intro nn_integral_cong, goal_cases) case (1 y f) have *: "y \ {-r..r}" if "y ^ 2 + c \ r ^ 2" "c \ 0" for c proof - have "y ^ 2 \ y ^ 2 + c" using that by simp also have "\ \ r ^ 2" by fact finally show ?thesis using \r > 0\ by (simp add: power2_le_iff_abs_le abs_if split: if_splits) qed have "(\x\A. (if x = i then y else f x)\<^sup>2) = (\x\A. (f x)\<^sup>2)" using insert.hyps by (intro sum.cong) auto thus ?case using 1 \r > 0\ by (auto simp: sum_nonneg real_sqrt_le_iff' indicator_def PiE_def space_PiM dest!: *) qed - also have "\ = (\\<^sup>+ (y::real). indicator {-r..r} y * (\\<^sup>+ x. indicator ({f. sqrt ((\i\A. (f i)\<^sup>2)) + also have "\ = (\\<^sup>+ (y::real). indicator {-r..r} y * (\\<^sup>+ x. indicator ({f. sqrt ((\i\A. (f i)\<^sup>2)) \ sqrt (r ^ 2 - y ^ 2)} \ space (Pi\<^sub>M A (\_. lborel))) x \Pi\<^sub>M A (\_. lborel)) \lborel)" by (subst nn_integral_cmult) auto - also have "\ = (\\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\_. lborel)) + also have "\ = (\\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\_. lborel)) ({f. sqrt ((\i\A. (f i)\<^sup>2)) \ sqrt (r ^ 2 - y ^ 2)} \ space (Pi\<^sub>M A (\_. lborel))) \lborel)" using \finite A\ by (intro nn_integral_cong, subst nn_integral_indicator) auto - also have "\ = (\\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) * + also have "\ = (\\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) * (sqrt (r ^ 2 - y ^ 2)) ^ card A) \lborel)" proof (intro nn_integral_cong_AE, goal_cases) case 1 have "AE y in lborel. y \ {-r,r}" by (intro AE_not_in countable_imp_null_set_lborel) auto thus ?case proof eventually_elim case (elim y) show ?case proof (cases "y \ {-r<..2 < r\<^sup>2" by (subst real_sqrt_less_iff [symmetric]) auto thus ?thesis by (subst insert.IH) (auto) qed (insert elim, auto) qed qed - also have "\ = ennreal (unit_ball_vol (real (card A))) * + also have "\ = ennreal (unit_ball_vol (real (card A))) * (\\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \lborel)" by (subst nn_integral_cmult [symmetric]) (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong) also have "(\\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \lborel) = - (\\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A + (\\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A \(distr lborel borel ((*) (1/r))))" using \r > 0\ by (subst nn_integral_distr) (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong) - also have "\ = (\\<^sup>+ x. ennreal (r ^ Suc (card A)) * + also have "\ = (\\<^sup>+ x. ennreal (r ^ Suc (card A)) * (indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \lborel)" using \r > 0\ by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac) - also have "\ = ennreal (r ^ Suc (card A)) * (\\<^sup>+ x. indicator {- 1..1} x * + also have "\ = ennreal (r ^ Suc (card A)) * (\\<^sup>+ x. indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A \lborel)" by (subst nn_integral_cmult) auto also note emeasure_cball_aux_integral also have "ennreal (unit_ball_vol (real (card A))) * (ennreal (r ^ Suc (card A)) * - ennreal (Beta (1/2) (card A / 2 + 1))) = + ennreal (Beta (1/2) (card A / 2 + 1))) = ennreal (unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) * r ^ Suc (card A))" using \r > 0\ by (simp add: ennreal_mult' [symmetric] mult_ac) also have "unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) = unit_ball_vol (Suc (card A))" - by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps + by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps Gamma_one_half_real powr_half_sqrt [symmetric] powr_add [symmetric]) also have "Suc (card A) = card (insert i A)" using insert.hyps by simp finally show ?case . qed text \ We now get the main theorem very easily by just applying the above lemma. \ context fixes c :: "'a :: euclidean_space" and r :: real assumes r: "r \ 0" begin theorem\<^marker>\tag unimportant\ emeasure_cball: "emeasure lborel (cball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))" proof (cases "r = 0") case False with r have r: "r > 0" by simp - have "(lborel :: 'a measure) = + have "(lborel :: 'a measure) = distr (Pi\<^sub>M Basis (\_. lborel)) borel (\f. \b\Basis. f b *\<^sub>R b)" by (rule lborel_eq) - also have "emeasure \ (cball 0 r) = - emeasure (Pi\<^sub>M Basis (\_. lborel)) + also have "emeasure \ (cball 0 r) = + emeasure (Pi\<^sub>M Basis (\_. lborel)) ({y. dist 0 (\b\Basis. y b *\<^sub>R b :: 'a) \ r} \ space (Pi\<^sub>M Basis (\_. lborel)))" by (subst emeasure_distr) (auto simp: cball_def) also have "{f. dist 0 (\b\Basis. f b *\<^sub>R b :: 'a) \ r} = {f. sqrt (\i\Basis. (f i)\<^sup>2) \ r}" by (subst euclidean_dist_l2) (auto simp: L2_set_def) also have "emeasure (Pi\<^sub>M Basis (\_. lborel)) (\ \ space (Pi\<^sub>M Basis (\_. lborel))) = ennreal (unit_ball_vol (real DIM('a)) * r ^ DIM('a))" using r by (subst emeasure_cball_aux) simp_all also have "emeasure lborel (cball 0 r :: 'a set) = emeasure (distr lborel borel (\x. c + x)) (cball c r)" by (subst emeasure_distr) (auto simp: cball_def dist_norm norm_minus_commute) also have "distr lborel borel (\x. c + x) = lborel" using lborel_affine[of 1 c] by (simp add: density_1) finally show ?thesis . qed auto corollary\<^marker>\tag unimportant\ content_cball: "content (cball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)" by (simp add: measure_def emeasure_cball r) corollary\<^marker>\tag unimportant\ emeasure_ball: "emeasure lborel (ball c r) = ennreal (unit_ball_vol (DIM('a)) * r ^ DIM('a))" proof - from negligible_sphere[of c r] have "sphere c r \ null_sets lborel" by (auto simp: null_sets_completion_iff negligible_iff_null_sets negligible_convex_frontier) hence "emeasure lborel (ball c r \ sphere c r :: 'a set) = emeasure lborel (ball c r :: 'a set)" by (intro emeasure_Un_null_set) auto also have "ball c r \ sphere c r = (cball c r :: 'a set)" by auto also have "emeasure lborel \ = ennreal (unit_ball_vol (real DIM('a)) * r ^ DIM('a))" by (rule emeasure_cball) finally show ?thesis .. qed corollary\<^marker>\tag important\ content_ball: "content (ball c r) = unit_ball_vol (DIM('a)) * r ^ DIM('a)" by (simp add: measure_def r emeasure_ball) end text \ - Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in + Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in the cases of even and odd integer dimensions. \ lemma unit_ball_vol_even: "unit_ball_vol (real (2 * n)) = pi ^ n / fact n" by (simp add: unit_ball_vol_def add_ac powr_realpow Gamma_fact) lemma unit_ball_vol_odd': "unit_ball_vol (real (2 * n + 1)) = pi ^ n / pochhammer (1 / 2) (Suc n)" and unit_ball_vol_odd: "unit_ball_vol (real (2 * n + 1)) = (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n" proof - - have "unit_ball_vol (real (2 * n + 1)) = + have "unit_ball_vol (real (2 * n + 1)) = pi powr (real n + 1 / 2) / Gamma (1 / 2 + real (Suc n))" by (simp add: unit_ball_vol_def field_simps) also have "pochhammer (1 / 2) (Suc n) = Gamma (1 / 2 + real (Suc n)) / Gamma (1 / 2)" by (intro pochhammer_Gamma) auto hence "Gamma (1 / 2 + real (Suc n)) = sqrt pi * pochhammer (1 / 2) (Suc n)" by (simp add: Gamma_one_half_real) also have "pi powr (real n + 1 / 2) / \ = pi ^ n / pochhammer (1 / 2) (Suc n)" by (simp add: powr_add powr_half_sqrt powr_realpow) finally show "unit_ball_vol (real (2 * n + 1)) = \" . - also have "pochhammer (1 / 2 :: real) (Suc n) = + also have "pochhammer (1 / 2 :: real) (Suc n) = fact (2 * Suc n) / (2 ^ (2 * Suc n) * fact (Suc n))" using fact_double[of "Suc n", where ?'a = real] by (simp add: divide_simps mult_ac) also have "pi ^n / \ = (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n" by simp finally show "unit_ball_vol (real (2 * n + 1)) = \" . qed lemma unit_ball_vol_numeral: "unit_ball_vol (numeral (Num.Bit0 n)) = pi ^ numeral n / fact (numeral n)" (is ?th1) "unit_ball_vol (numeral (Num.Bit1 n)) = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) / fact (2 * Suc (numeral n)) * pi ^ numeral n" (is ?th2) proof - - have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)" + have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)" by (simp only: numeral_Bit0 mult_2 ring_distribs) also have "unit_ball_vol \ = pi ^ numeral n / fact (numeral n)" by (rule unit_ball_vol_even) finally show ?th1 by simp next have "numeral (Num.Bit1 n) = (2 * numeral n + 1 :: nat)" by (simp only: numeral_Bit1 mult_2) also have "unit_ball_vol \ = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) / fact (2 * Suc (numeral n)) * pi ^ numeral n" by (rule unit_ball_vol_odd) finally show ?th2 by simp qed lemmas eval_unit_ball_vol = unit_ball_vol_numeral fact_numeral text \ Just for fun, we compute the volume of unit balls for a few dimensions. \ lemma unit_ball_vol_0 [simp]: "unit_ball_vol 0 = 1" using unit_ball_vol_even[of 0] by simp lemma unit_ball_vol_1 [simp]: "unit_ball_vol 1 = 2" using unit_ball_vol_odd[of 0] by simp corollary\<^marker>\tag unimportant\ unit_ball_vol_2: "unit_ball_vol 2 = pi" and unit_ball_vol_3: "unit_ball_vol 3 = 4 / 3 * pi" and unit_ball_vol_4: "unit_ball_vol 4 = pi\<^sup>2 / 2" and unit_ball_vol_5: "unit_ball_vol 5 = 8 / 15 * pi\<^sup>2" by (simp_all add: eval_unit_ball_vol) corollary\<^marker>\tag unimportant\ circle_area: "r \ 0 \ content (ball c r :: (real ^ 2) set) = r ^ 2 * pi" by (simp add: content_ball unit_ball_vol_2) corollary\<^marker>\tag unimportant\ sphere_volume: "r \ 0 \ content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi" by (simp add: content_ball unit_ball_vol_3) text \ Useful equivalent forms \ corollary\<^marker>\tag unimportant\ content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \ r \ 0" proof - have "r > 0 \ content (ball c r) > 0" by (simp add: content_ball unit_ball_vol_def) then show ?thesis by (fastforce simp: ball_empty) qed corollary\<^marker>\tag unimportant\ content_ball_gt_0_iff [simp]: "0 < content (ball z r) \ 0 < r" by (auto simp: zero_less_measure_iff) corollary\<^marker>\tag unimportant\ content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \ r \ 0" proof (cases "r = 0") case False moreover have "r > 0 \ content (cball c r) > 0" by (simp add: content_cball unit_ball_vol_def) ultimately show ?thesis by fastforce qed auto corollary\<^marker>\tag unimportant\ content_cball_gt_0_iff [simp]: "0 < content (cball z r) \ 0 < r" by (auto simp: zero_less_measure_iff) end diff --git a/src/HOL/Finite_Set.thy b/src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy +++ b/src/HOL/Finite_Set.thy @@ -1,2538 +1,2549 @@ (* Title: HOL/Finite_Set.thy Author: Tobias Nipkow Author: Lawrence C Paulson Author: Markus Wenzel Author: Jeremy Avigad Author: Andrei Popescu *) section \Finite sets\ theory Finite_Set imports Product_Type Sum_Type Fields begin subsection \Predicate for finite sets\ context notes [[inductive_internals]] begin inductive finite :: "'a set \ bool" where emptyI [simp, intro!]: "finite {}" | insertI [simp, intro!]: "finite A \ finite (insert a A)" end simproc_setup finite_Collect ("finite (Collect P)") = \K Set_Comprehension_Pointfree.simproc\ declare [[simproc del: finite_Collect]] lemma finite_induct [case_names empty insert, induct set: finite]: \ \Discharging \x \ F\ entails extra work.\ assumes "finite F" assumes "P {}" and insert: "\x F. finite F \ x \ F \ P F \ P (insert x F)" shows "P F" using \finite F\ proof induct show "P {}" by fact next fix x F assume F: "finite F" and P: "P F" show "P (insert x F)" proof cases assume "x \ F" then have "insert x F = F" by (rule insert_absorb) with P show ?thesis by (simp only:) next assume "x \ F" from F this P show ?thesis by (rule insert) qed qed lemma infinite_finite_induct [case_names infinite empty insert]: assumes infinite: "\A. \ finite A \ P A" and empty: "P {}" and insert: "\x F. finite F \ x \ F \ P F \ P (insert x F)" shows "P A" proof (cases "finite A") case False with infinite show ?thesis . next case True then show ?thesis by (induct A) (fact empty insert)+ qed subsubsection \Choice principles\ lemma ex_new_if_finite: \ \does not depend on def of finite at all\ assumes "\ finite (UNIV :: 'a set)" and "finite A" shows "\a::'a. a \ A" proof - from assms have "A \ UNIV" by blast then show ?thesis by blast qed text \A finite choice principle. Does not need the SOME choice operator.\ lemma finite_set_choice: "finite A \ \x\A. \y. P x y \ \f. \x\A. P x (f x)" proof (induct rule: finite_induct) case empty then show ?case by simp next case (insert a A) then obtain f b where f: "\x\A. P x (f x)" and ab: "P a b" by auto show ?case (is "\f. ?P f") proof show "?P (\x. if x = a then b else f x)" using f ab by auto qed qed subsubsection \Finite sets are the images of initial segments of natural numbers\ lemma finite_imp_nat_seg_image_inj_on: assumes "finite A" shows "\(n::nat) f. A = f ` {i. i < n} \ inj_on f {i. i < n}" using assms proof induct case empty show ?case proof show "\f. {} = f ` {i::nat. i < 0} \ inj_on f {i. i < 0}" by simp qed next case (insert a A) have notinA: "a \ A" by fact from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast then have "insert a A = f(n:=a) ` {i. i < Suc n}" and "inj_on (f(n:=a)) {i. i < Suc n}" using notinA by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq) then show ?case by blast qed lemma nat_seg_image_imp_finite: "A = f ` {i::nat. i < n} \ finite A" proof (induct n arbitrary: A) case 0 then show ?case by simp next case (Suc n) let ?B = "f ` {i. i < n}" have finB: "finite ?B" by (rule Suc.hyps[OF refl]) show ?case proof (cases "\k (\n f. A = f ` {i::nat. i < n})" by (blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on) lemma finite_imp_inj_to_nat_seg: assumes "finite A" shows "\f n. f ` A = {i::nat. i < n} \ inj_on f A" proof - from finite_imp_nat_seg_image_inj_on [OF \finite A\] obtain f and n :: nat where bij: "bij_betw f {i. i ?f ` A = {i. i k}" by (simp add: le_eq_less_or_eq Collect_disj_eq) subsection \Finiteness and common set operations\ lemma rev_finite_subset: "finite B \ A \ B \ finite A" proof (induct arbitrary: A rule: finite_induct) case empty then show ?case by simp next case (insert x F A) have A: "A \ insert x F" and r: "A - {x} \ F \ finite (A - {x})" by fact+ show "finite A" proof cases assume x: "x \ A" with A have "A - {x} \ F" by (simp add: subset_insert_iff) with r have "finite (A - {x})" . then have "finite (insert x (A - {x}))" .. also have "insert x (A - {x}) = A" using x by (rule insert_Diff) finally show ?thesis . next show ?thesis when "A \ F" using that by fact assume "x \ A" with A show "A \ F" by (simp add: subset_insert_iff) qed qed lemma finite_subset: "A \ B \ finite B \ finite A" by (rule rev_finite_subset) lemma finite_UnI: assumes "finite F" and "finite G" shows "finite (F \ G)" using assms by induct simp_all lemma finite_Un [iff]: "finite (F \ G) \ finite F \ finite G" by (blast intro: finite_UnI finite_subset [of _ "F \ G"]) lemma finite_insert [simp]: "finite (insert a A) \ finite A" proof - have "finite {a} \ finite A \ finite A" by simp then have "finite ({a} \ A) \ finite A" by (simp only: finite_Un) then show ?thesis by simp qed lemma finite_Int [simp, intro]: "finite F \ finite G \ finite (F \ G)" by (blast intro: finite_subset) lemma finite_Collect_conjI [simp, intro]: "finite {x. P x} \ finite {x. Q x} \ finite {x. P x \ Q x}" by (simp add: Collect_conj_eq) lemma finite_Collect_disjI [simp]: "finite {x. P x \ Q x} \ finite {x. P x} \ finite {x. Q x}" by (simp add: Collect_disj_eq) lemma finite_Diff [simp, intro]: "finite A \ finite (A - B)" by (rule finite_subset, rule Diff_subset) lemma finite_Diff2 [simp]: assumes "finite B" shows "finite (A - B) \ finite A" proof - have "finite A \ finite ((A - B) \ (A \ B))" by (simp add: Un_Diff_Int) also have "\ \ finite (A - B)" using \finite B\ by simp finally show ?thesis .. qed lemma finite_Diff_insert [iff]: "finite (A - insert a B) \ finite (A - B)" proof - have "finite (A - B) \ finite (A - B - {a})" by simp moreover have "A - insert a B = A - B - {a}" by auto ultimately show ?thesis by simp qed lemma finite_compl [simp]: "finite (A :: 'a set) \ finite (- A) \ finite (UNIV :: 'a set)" by (simp add: Compl_eq_Diff_UNIV) lemma finite_Collect_not [simp]: "finite {x :: 'a. P x} \ finite {x. \ P x} \ finite (UNIV :: 'a set)" by (simp add: Collect_neg_eq) lemma finite_Union [simp, intro]: "finite A \ (\M. M \ A \ finite M) \ finite (\A)" by (induct rule: finite_induct) simp_all lemma finite_UN_I [intro]: "finite A \ (\a. a \ A \ finite (B a)) \ finite (\a\A. B a)" by (induct rule: finite_induct) simp_all lemma finite_UN [simp]: "finite A \ finite (\(B ` A)) \ (\x\A. finite (B x))" by (blast intro: finite_subset) lemma finite_Inter [intro]: "\A\M. finite A \ finite (\M)" by (blast intro: Inter_lower finite_subset) lemma finite_INT [intro]: "\x\I. finite (A x) \ finite (\x\I. A x)" by (blast intro: INT_lower finite_subset) lemma finite_imageI [simp, intro]: "finite F \ finite (h ` F)" by (induct rule: finite_induct) simp_all lemma finite_image_set [simp]: "finite {x. P x} \ finite {f x |x. P x}" by (simp add: image_Collect [symmetric]) lemma finite_image_set2: "finite {x. P x} \ finite {y. Q y} \ finite {f x y |x y. P x \ Q y}" by (rule finite_subset [where B = "\x \ {x. P x}. \y \ {y. Q y}. {f x y}"]) auto lemma finite_imageD: assumes "finite (f ` A)" and "inj_on f A" shows "finite A" using assms proof (induct "f ` A" arbitrary: A) case empty then show ?case by simp next case (insert x B) then have B_A: "insert x B = f ` A" by simp then obtain y where "x = f y" and "y \ A" by blast from B_A \x \ B\ have "B = f ` A - {x}" by blast with B_A \x \ B\ \x = f y\ \inj_on f A\ \y \ A\ have "B = f ` (A - {y})" by (simp add: inj_on_image_set_diff) moreover from \inj_on f A\ have "inj_on f (A - {y})" by (rule inj_on_diff) ultimately have "finite (A - {y})" by (rule insert.hyps) then show "finite A" by simp qed lemma finite_image_iff: "inj_on f A \ finite (f ` A) \ finite A" using finite_imageD by blast lemma finite_surj: "finite A \ B \ f ` A \ finite B" by (erule finite_subset) (rule finite_imageI) lemma finite_range_imageI: "finite (range g) \ finite (range (\x. f (g x)))" by (drule finite_imageI) (simp add: range_composition) lemma finite_subset_image: assumes "finite B" shows "B \ f ` A \ \C\A. finite C \ B = f ` C" using assms proof induct case empty then show ?case by simp next case insert then show ?case by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast qed lemma all_subset_image: "(\B. B \ f ` A \ P B) \ (\B. B \ A \ P(f ` B))" by (safe elim!: subset_imageE) (use image_mono in \blast+\) (* slow *) lemma all_finite_subset_image: "(\B. finite B \ B \ f ` A \ P B) \ (\B. finite B \ B \ A \ P (f ` B))" proof safe fix B :: "'a set" assume B: "finite B" "B \ f ` A" and P: "\B. finite B \ B \ A \ P (f ` B)" show "P B" using finite_subset_image [OF B] P by blast qed blast lemma ex_finite_subset_image: "(\B. finite B \ B \ f ` A \ P B) \ (\B. finite B \ B \ A \ P (f ` B))" proof safe fix B :: "'a set" assume B: "finite B" "B \ f ` A" and "P B" show "\B. finite B \ B \ A \ P (f ` B)" using finite_subset_image [OF B] \P B\ by blast qed blast lemma finite_vimage_IntI: "finite F \ inj_on h A \ finite (h -` F \ A)" proof (induct rule: finite_induct) case (insert x F) then show ?case by (simp add: vimage_insert [of h x F] finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2) qed simp lemma finite_finite_vimage_IntI: assumes "finite F" and "\y. y \ F \ finite ((h -` {y}) \ A)" shows "finite (h -` F \ A)" proof - have *: "h -` F \ A = (\ y\F. (h -` {y}) \ A)" by blast show ?thesis by (simp only: * assms finite_UN_I) qed lemma finite_vimageI: "finite F \ inj h \ finite (h -` F)" using finite_vimage_IntI[of F h UNIV] by auto lemma finite_vimageD': "finite (f -` A) \ A \ range f \ finite A" by (auto simp add: subset_image_iff intro: finite_subset[rotated]) lemma finite_vimageD: "finite (h -` F) \ surj h \ finite F" by (auto dest: finite_vimageD') lemma finite_vimage_iff: "bij h \ finite (h -` F) \ finite F" unfolding bij_def by (auto elim: finite_vimageD finite_vimageI) +lemma finite_inverse_image_gen: + assumes "finite A" "inj_on f D" + shows "finite {j\D. f j \ A}" + using finite_vimage_IntI [OF assms] + by (simp add: Collect_conj_eq inf_commute vimage_def) + +lemma finite_inverse_image: + assumes "finite A" "inj f" + shows "finite {j. f j \ A}" + using finite_inverse_image_gen [OF assms] by simp + lemma finite_Collect_bex [simp]: assumes "finite A" shows "finite {x. \y\A. Q x y} \ (\y\A. finite {x. Q x y})" proof - have "{x. \y\A. Q x y} = (\y\A. {x. Q x y})" by auto with assms show ?thesis by simp qed lemma finite_Collect_bounded_ex [simp]: assumes "finite {y. P y}" shows "finite {x. \y. P y \ Q x y} \ (\y. P y \ finite {x. Q x y})" proof - have "{x. \y. P y \ Q x y} = (\y\{y. P y}. {x. Q x y})" by auto with assms show ?thesis by simp qed lemma finite_Plus: "finite A \ finite B \ finite (A <+> B)" by (simp add: Plus_def) lemma finite_PlusD: fixes A :: "'a set" and B :: "'b set" assumes fin: "finite (A <+> B)" shows "finite A" "finite B" proof - have "Inl ` A \ A <+> B" by auto then have "finite (Inl ` A :: ('a + 'b) set)" using fin by (rule finite_subset) then show "finite A" by (rule finite_imageD) (auto intro: inj_onI) next have "Inr ` B \ A <+> B" by auto then have "finite (Inr ` B :: ('a + 'b) set)" using fin by (rule finite_subset) then show "finite B" by (rule finite_imageD) (auto intro: inj_onI) qed lemma finite_Plus_iff [simp]: "finite (A <+> B) \ finite A \ finite B" by (auto intro: finite_PlusD finite_Plus) lemma finite_Plus_UNIV_iff [simp]: "finite (UNIV :: ('a + 'b) set) \ finite (UNIV :: 'a set) \ finite (UNIV :: 'b set)" by (subst UNIV_Plus_UNIV [symmetric]) (rule finite_Plus_iff) lemma finite_SigmaI [simp, intro]: "finite A \ (\a. a\A \ finite (B a)) \ finite (SIGMA a:A. B a)" unfolding Sigma_def by blast lemma finite_SigmaI2: assumes "finite {x\A. B x \ {}}" and "\a. a \ A \ finite (B a)" shows "finite (Sigma A B)" proof - from assms have "finite (Sigma {x\A. B x \ {}} B)" by auto also have "Sigma {x:A. B x \ {}} B = Sigma A B" by auto finally show ?thesis . qed lemma finite_cartesian_product: "finite A \ finite B \ finite (A \ B)" by (rule finite_SigmaI) lemma finite_Prod_UNIV: "finite (UNIV :: 'a set) \ finite (UNIV :: 'b set) \ finite (UNIV :: ('a \ 'b) set)" by (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product) lemma finite_cartesian_productD1: assumes "finite (A \ B)" and "B \ {}" shows "finite A" proof - from assms obtain n f where "A \ B = f ` {i::nat. i < n}" by (auto simp add: finite_conv_nat_seg_image) then have "fst ` (A \ B) = fst ` f ` {i::nat. i < n}" by simp with \B \ {}\ have "A = (fst \ f) ` {i::nat. i < n}" by (simp add: image_comp) then have "\n f. A = f ` {i::nat. i < n}" by blast then show ?thesis by (auto simp add: finite_conv_nat_seg_image) qed lemma finite_cartesian_productD2: assumes "finite (A \ B)" and "A \ {}" shows "finite B" proof - from assms obtain n f where "A \ B = f ` {i::nat. i < n}" by (auto simp add: finite_conv_nat_seg_image) then have "snd ` (A \ B) = snd ` f ` {i::nat. i < n}" by simp with \A \ {}\ have "B = (snd \ f) ` {i::nat. i < n}" by (simp add: image_comp) then have "\n f. B = f ` {i::nat. i < n}" by blast then show ?thesis by (auto simp add: finite_conv_nat_seg_image) qed lemma finite_cartesian_product_iff: "finite (A \ B) \ (A = {} \ B = {} \ (finite A \ finite B))" by (auto dest: finite_cartesian_productD1 finite_cartesian_productD2 finite_cartesian_product) lemma finite_prod: "finite (UNIV :: ('a \ 'b) set) \ finite (UNIV :: 'a set) \ finite (UNIV :: 'b set)" using finite_cartesian_product_iff[of UNIV UNIV] by simp lemma finite_Pow_iff [iff]: "finite (Pow A) \ finite A" proof assume "finite (Pow A)" then have "finite ((\x. {x}) ` A)" by (blast intro: finite_subset) (* somewhat slow *) then show "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp next assume "finite A" then show "finite (Pow A)" by induct (simp_all add: Pow_insert) qed corollary finite_Collect_subsets [simp, intro]: "finite A \ finite {B. B \ A}" by (simp add: Pow_def [symmetric]) lemma finite_set: "finite (UNIV :: 'a set set) \ finite (UNIV :: 'a set)" by (simp only: finite_Pow_iff Pow_UNIV[symmetric]) lemma finite_UnionD: "finite (\A) \ finite A" by (blast intro: finite_subset [OF subset_Pow_Union]) lemma finite_bind: assumes "finite S" assumes "\x \ S. finite (f x)" shows "finite (Set.bind S f)" using assms by (simp add: bind_UNION) lemma finite_filter [simp]: "finite S \ finite (Set.filter P S)" unfolding Set.filter_def by simp lemma finite_set_of_finite_funs: assumes "finite A" "finite B" shows "finite {f. \x. (x \ A \ f x \ B) \ (x \ A \ f x = d)}" (is "finite ?S") proof - let ?F = "\f. {(a,b). a \ A \ b = f a}" have "?F ` ?S \ Pow(A \ B)" by auto from finite_subset[OF this] assms have 1: "finite (?F ` ?S)" by simp have 2: "inj_on ?F ?S" by (fastforce simp add: inj_on_def set_eq_iff fun_eq_iff) (* somewhat slow *) show ?thesis by (rule finite_imageD [OF 1 2]) qed lemma not_finite_existsD: assumes "\ finite {a. P a}" shows "\a. P a" proof (rule classical) assume "\ ?thesis" with assms show ?thesis by auto qed subsection \Further induction rules on finite sets\ lemma finite_ne_induct [case_names singleton insert, consumes 2]: assumes "finite F" and "F \ {}" assumes "\x. P {x}" and "\x F. finite F \ F \ {} \ x \ F \ P F \ P (insert x F)" shows "P F" using assms proof induct case empty then show ?case by simp next case (insert x F) then show ?case by cases auto qed lemma finite_subset_induct [consumes 2, case_names empty insert]: assumes "finite F" and "F \ A" and empty: "P {}" and insert: "\a F. finite F \ a \ A \ a \ F \ P F \ P (insert a F)" shows "P F" using \finite F\ \F \ A\ proof induct show "P {}" by fact next fix x F assume "finite F" and "x \ F" and P: "F \ A \ P F" and i: "insert x F \ A" show "P (insert x F)" proof (rule insert) from i show "x \ A" by blast from i have "F \ A" by blast with P show "P F" . show "finite F" by fact show "x \ F" by fact qed qed lemma finite_empty_induct: assumes "finite A" and "P A" and remove: "\a A. finite A \ a \ A \ P A \ P (A - {a})" shows "P {}" proof - have "P (A - B)" if "B \ A" for B :: "'a set" proof - from \finite A\ that have "finite B" by (rule rev_finite_subset) from this \B \ A\ show "P (A - B)" proof induct case empty from \P A\ show ?case by simp next case (insert b B) have "P (A - B - {b})" proof (rule remove) from \finite A\ show "finite (A - B)" by induct auto from insert show "b \ A - B" by simp from insert show "P (A - B)" by simp qed also have "A - B - {b} = A - insert b B" by (rule Diff_insert [symmetric]) finally show ?case . qed qed then have "P (A - A)" by blast then show ?thesis by simp qed lemma finite_update_induct [consumes 1, case_names const update]: assumes finite: "finite {a. f a \ c}" and const: "P (\a. c)" and update: "\a b f. finite {a. f a \ c} \ f a = c \ b \ c \ P f \ P (f(a := b))" shows "P f" using finite proof (induct "{a. f a \ c}" arbitrary: f) case empty with const show ?case by simp next case (insert a A) then have "A = {a'. (f(a := c)) a' \ c}" and "f a \ c" by auto with \finite A\ have "finite {a'. (f(a := c)) a' \ c}" by simp have "(f(a := c)) a = c" by simp from insert \A = {a'. (f(a := c)) a' \ c}\ have "P (f(a := c))" by simp with \finite {a'. (f(a := c)) a' \ c}\ \(f(a := c)) a = c\ \f a \ c\ have "P ((f(a := c))(a := f a))" by (rule update) then show ?case by simp qed lemma finite_subset_induct' [consumes 2, case_names empty insert]: assumes "finite F" and "F \ A" and empty: "P {}" and insert: "\a F. \finite F; a \ A; F \ A; a \ F; P F \ \ P (insert a F)" shows "P F" using assms(1,2) proof induct show "P {}" by fact next fix x F assume "finite F" and "x \ F" and P: "F \ A \ P F" and i: "insert x F \ A" show "P (insert x F)" proof (rule insert) from i show "x \ A" by blast from i have "F \ A" by blast with P show "P F" . show "finite F" by fact show "x \ F" by fact show "F \ A" by fact qed qed subsection \Class \finite\\ class finite = assumes finite_UNIV: "finite (UNIV :: 'a set)" begin lemma finite [simp]: "finite (A :: 'a set)" by (rule subset_UNIV finite_UNIV finite_subset)+ lemma finite_code [code]: "finite (A :: 'a set) \ True" by simp end instance prod :: (finite, finite) finite by standard (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) lemma inj_graph: "inj (\f. {(x, y). y = f x})" by (rule inj_onI) (auto simp add: set_eq_iff fun_eq_iff) instance "fun" :: (finite, finite) finite proof show "finite (UNIV :: ('a \ 'b) set)" proof (rule finite_imageD) let ?graph = "\f::'a \ 'b. {(x, y). y = f x}" have "range ?graph \ Pow UNIV" by simp moreover have "finite (Pow (UNIV :: ('a * 'b) set))" by (simp only: finite_Pow_iff finite) ultimately show "finite (range ?graph)" by (rule finite_subset) show "inj ?graph" by (rule inj_graph) qed qed instance bool :: finite by standard (simp add: UNIV_bool) instance set :: (finite) finite by standard (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite) instance unit :: finite by standard (simp add: UNIV_unit) instance sum :: (finite, finite) finite by standard (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) subsection \A basic fold functional for finite sets\ text \ The intended behaviour is \fold f z {x\<^sub>1, \, x\<^sub>n} = f x\<^sub>1 (\ (f x\<^sub>n z)\)\ if \f\ is ``left-commutative''. The commutativity requirement is relativised to the carrier set \S\: \ locale comp_fun_commute_on = fixes S :: "'a set" fixes f :: "'a \ 'b \ 'b" assumes comp_fun_commute_on: "x \ S \ y \ S \ f y \ f x = f x \ f y" begin lemma fun_left_comm: "x \ S \ y \ S \ f y (f x z) = f x (f y z)" using comp_fun_commute_on by (simp add: fun_eq_iff) lemma commute_left_comp: "x \ S \ y \ S \ f y \ (f x \ g) = f x \ (f y \ g)" by (simp add: o_assoc comp_fun_commute_on) end inductive fold_graph :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b \ bool" for f :: "'a \ 'b \ 'b" and z :: 'b where emptyI [intro]: "fold_graph f z {} z" | insertI [intro]: "x \ A \ fold_graph f z A y \ fold_graph f z (insert x A) (f x y)" inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x" lemma fold_graph_closed_lemma: "fold_graph f z A x \ x \ B" if "fold_graph g z A x" "\a b. a \ A \ b \ B \ f a b = g a b" "\a b. a \ A \ b \ B \ g a b \ B" "z \ B" using that(1-3) proof (induction rule: fold_graph.induct) case (insertI x A y) have "fold_graph f z A y" "y \ B" unfolding atomize_conj by (rule insertI.IH) (auto intro: insertI.prems) then have "g x y \ B" and f_eq: "f x y = g x y" by (auto simp: insertI.prems) moreover have "fold_graph f z (insert x A) (f x y)" by (rule fold_graph.insertI; fact) ultimately show ?case by (simp add: f_eq) qed (auto intro!: that) lemma fold_graph_closed_eq: "fold_graph f z A = fold_graph g z A" if "\a b. a \ A \ b \ B \ f a b = g a b" "\a b. a \ A \ b \ B \ g a b \ B" "z \ B" using fold_graph_closed_lemma[of f z A _ B g] fold_graph_closed_lemma[of g z A _ B f] that by auto definition fold :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b" where "fold f z A = (if finite A then (THE y. fold_graph f z A y) else z)" lemma fold_closed_eq: "fold f z A = fold g z A" if "\a b. a \ A \ b \ B \ f a b = g a b" "\a b. a \ A \ b \ B \ g a b \ B" "z \ B" unfolding Finite_Set.fold_def by (subst fold_graph_closed_eq[where B=B and g=g]) (auto simp: that) text \ A tempting alternative for the definition is \<^term>\if finite A then THE y. fold_graph f z A y else e\. It allows the removal of finiteness assumptions from the theorems \fold_comm\, \fold_reindex\ and \fold_distrib\. The proofs become ugly. It is not worth the effort. (???) \ lemma finite_imp_fold_graph: "finite A \ \x. fold_graph f z A x" by (induct rule: finite_induct) auto subsubsection \From \<^const>\fold_graph\ to \<^term>\fold\\ context comp_fun_commute_on begin lemma fold_graph_finite: assumes "fold_graph f z A y" shows "finite A" using assms by induct simp_all lemma fold_graph_insertE_aux: assumes "A \ S" assumes "fold_graph f z A y" "a \ A" shows "\y'. y = f a y' \ fold_graph f z (A - {a}) y'" using assms(2-,1) proof (induct set: fold_graph) case emptyI then show ?case by simp next case (insertI x A y) show ?case proof (cases "x = a") case True with insertI show ?thesis by auto next case False then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'" using insertI by auto from insertI have "x \ S" "a \ S" by auto then have "f x y = f a (f x y')" unfolding y by (intro fun_left_comm; simp) moreover have "fold_graph f z (insert x A - {a}) (f x y')" using y' and \x \ a\ and \x \ A\ by (simp add: insert_Diff_if fold_graph.insertI) ultimately show ?thesis by fast qed qed lemma fold_graph_insertE: assumes "insert x A \ S" assumes "fold_graph f z (insert x A) v" and "x \ A" obtains y where "v = f x y" and "fold_graph f z A y" using assms by (auto dest: fold_graph_insertE_aux[OF \insert x A \ S\ _ insertI1]) lemma fold_graph_determ: assumes "A \ S" assumes "fold_graph f z A x" "fold_graph f z A y" shows "y = x" using assms(2-,1) proof (induct arbitrary: y set: fold_graph) case emptyI then show ?case by fast next case (insertI x A y v) from \insert x A \ S\ and \fold_graph f z (insert x A) v\ and \x \ A\ obtain y' where "v = f x y'" and "fold_graph f z A y'" by (rule fold_graph_insertE) from \fold_graph f z A y'\ insertI have "y' = y" by simp with \v = f x y'\ show "v = f x y" by simp qed lemma fold_equality: "A \ S \ fold_graph f z A y \ fold f z A = y" by (cases "finite A") (auto simp add: fold_def intro: fold_graph_determ dest: fold_graph_finite) lemma fold_graph_fold: assumes "A \ S" assumes "finite A" shows "fold_graph f z A (fold f z A)" proof - from \finite A\ have "\x. fold_graph f z A x" by (rule finite_imp_fold_graph) moreover note fold_graph_determ[OF \A \ S\] ultimately have "\!x. fold_graph f z A x" by (rule ex_ex1I) then have "fold_graph f z A (The (fold_graph f z A))" by (rule theI') with assms show ?thesis by (simp add: fold_def) qed text \The base case for \fold\:\ lemma (in -) fold_infinite [simp]: "\ finite A \ fold f z A = z" by (auto simp: fold_def) lemma (in -) fold_empty [simp]: "fold f z {} = z" by (auto simp: fold_def) text \The various recursion equations for \<^const>\fold\:\ lemma fold_insert [simp]: assumes "insert x A \ S" assumes "finite A" and "x \ A" shows "fold f z (insert x A) = f x (fold f z A)" proof (rule fold_equality[OF \insert x A \ S\]) fix z from \insert x A \ S\ \finite A\ have "fold_graph f z A (fold f z A)" by (blast intro: fold_graph_fold) with \x \ A\ have "fold_graph f z (insert x A) (f x (fold f z A))" by (rule fold_graph.insertI) then show "fold_graph f z (insert x A) (f x (fold f z A))" by simp qed declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del] \ \No more proofs involve these.\ lemma fold_fun_left_comm: assumes "insert x A \ S" "finite A" shows "f x (fold f z A) = fold f (f x z) A" using assms(2,1) proof (induct rule: finite_induct) case empty then show ?case by simp next case (insert y F) then have "fold f (f x z) (insert y F) = f y (fold f (f x z) F)" by simp also have "\ = f x (f y (fold f z F))" using insert by (simp add: fun_left_comm[where ?y=x]) also have "\ = f x (fold f z (insert y F))" proof - from insert have "insert y F \ S" by simp from fold_insert[OF this] insert show ?thesis by simp qed finally show ?case .. qed lemma fold_insert2: "insert x A \ S \ finite A \ x \ A \ fold f z (insert x A) = fold f (f x z) A" by (simp add: fold_fun_left_comm) lemma fold_rec: assumes "A \ S" assumes "finite A" and "x \ A" shows "fold f z A = f x (fold f z (A - {x}))" proof - have A: "A = insert x (A - {x})" using \x \ A\ by blast then have "fold f z A = fold f z (insert x (A - {x}))" by simp also have "\ = f x (fold f z (A - {x}))" by (rule fold_insert) (use assms in \auto\) finally show ?thesis . qed lemma fold_insert_remove: assumes "insert x A \ S" assumes "finite A" shows "fold f z (insert x A) = f x (fold f z (A - {x}))" proof - from \finite A\ have "finite (insert x A)" by auto moreover have "x \ insert x A" by auto ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))" using \insert x A \ S\ by (blast intro: fold_rec) then show ?thesis by simp qed lemma fold_set_union_disj: assumes "A \ S" "B \ S" assumes "finite A" "finite B" "A \ B = {}" shows "Finite_Set.fold f z (A \ B) = Finite_Set.fold f (Finite_Set.fold f z A) B" using \finite B\ assms(1,2,3,5) proof induct case (insert x F) have "fold f z (A \ insert x F) = f x (fold f (fold f z A) F)" using insert by auto also have "\ = fold f (fold f z A) (insert x F)" using insert by (blast intro: fold_insert[symmetric]) finally show ?case . qed simp end text \Other properties of \<^const>\fold\:\ lemma fold_graph_image: assumes "inj_on g A" shows "fold_graph f z (g ` A) = fold_graph (f \ g) z A" proof fix w show "fold_graph f z (g ` A) w = fold_graph (f o g) z A w" proof assume "fold_graph f z (g ` A) w" then show "fold_graph (f \ g) z A w" using assms proof (induct "g ` A" w arbitrary: A) case emptyI then show ?case by (auto intro: fold_graph.emptyI) next case (insertI x A r B) from \inj_on g B\ \x \ A\ \insert x A = image g B\ obtain x' A' where "x' \ A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'" by (rule inj_img_insertE) from insertI.prems have "fold_graph (f \ g) z A' r" by (auto intro: insertI.hyps) with \x' \ A'\ have "fold_graph (f \ g) z (insert x' A') ((f \ g) x' r)" by (rule fold_graph.insertI) then show ?case by simp qed next assume "fold_graph (f \ g) z A w" then show "fold_graph f z (g ` A) w" using assms proof induct case emptyI then show ?case by (auto intro: fold_graph.emptyI) next case (insertI x A r) from \x \ A\ insertI.prems have "g x \ g ` A" by auto moreover from insertI have "fold_graph f z (g ` A) r" by simp ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)" by (rule fold_graph.insertI) then show ?case by simp qed qed qed lemma fold_image: assumes "inj_on g A" shows "fold f z (g ` A) = fold (f \ g) z A" proof (cases "finite A") case False with assms show ?thesis by (auto dest: finite_imageD simp add: fold_def) next case True then show ?thesis by (auto simp add: fold_def fold_graph_image[OF assms]) qed lemma fold_cong: assumes "comp_fun_commute_on S f" "comp_fun_commute_on S g" and "A \ S" "finite A" and cong: "\x. x \ A \ f x = g x" and "s = t" and "A = B" shows "fold f s A = fold g t B" proof - have "fold f s A = fold g s A" using \finite A\ \A \ S\ cong proof (induct A) case empty then show ?case by simp next case insert interpret f: comp_fun_commute_on S f by (fact \comp_fun_commute_on S f\) interpret g: comp_fun_commute_on S g by (fact \comp_fun_commute_on S g\) from insert show ?case by simp qed with assms show ?thesis by simp qed text \A simplified version for idempotent functions:\ locale comp_fun_idem_on = comp_fun_commute_on + assumes comp_fun_idem_on: "x \ S \ f x \ f x = f x" begin lemma fun_left_idem: "x \ S \ f x (f x z) = f x z" using comp_fun_idem_on by (simp add: fun_eq_iff) lemma fold_insert_idem: assumes "insert x A \ S" assumes fin: "finite A" shows "fold f z (insert x A) = f x (fold f z A)" proof cases assume "x \ A" then obtain B where "A = insert x B" and "x \ B" by (rule set_insert) then show ?thesis using assms by (simp add: comp_fun_idem_on fun_left_idem) next assume "x \ A" then show ?thesis using assms by auto qed declare fold_insert [simp del] fold_insert_idem [simp] lemma fold_insert_idem2: "insert x A \ S \ finite A \ fold f z (insert x A) = fold f (f x z) A" by (simp add: fold_fun_left_comm) end subsubsection \Liftings to \comp_fun_commute_on\ etc.\ lemma (in comp_fun_commute_on) comp_comp_fun_commute_on: "range g \ S \ comp_fun_commute_on R (f \ g)" by standard (force intro: comp_fun_commute_on) lemma (in comp_fun_idem_on) comp_comp_fun_idem_on: assumes "range g \ S" shows "comp_fun_idem_on R (f \ g)" proof interpret f_g: comp_fun_commute_on R "f o g" by (fact comp_comp_fun_commute_on[OF \range g \ S\]) show "x \ R \ y \ R \ (f \ g) y \ (f \ g) x = (f \ g) x \ (f \ g) y" for x y by (fact f_g.comp_fun_commute_on) qed (use \range g \ S\ in \force intro: comp_fun_idem_on\) lemma (in comp_fun_commute_on) comp_fun_commute_on_funpow: "comp_fun_commute_on S (\x. f x ^^ g x)" proof fix x y assume "x \ S" "y \ S" show "f y ^^ g y \ f x ^^ g x = f x ^^ g x \ f y ^^ g y" proof (cases "x = y") case True then show ?thesis by simp next case False show ?thesis proof (induct "g x" arbitrary: g) case 0 then show ?case by simp next case (Suc n g) have hyp1: "f y ^^ g y \ f x = f x \ f y ^^ g y" proof (induct "g y" arbitrary: g) case 0 then show ?case by simp next case (Suc n g) define h where "h z = g z - 1" for z with Suc have "n = h y" by simp with Suc have hyp: "f y ^^ h y \ f x = f x \ f y ^^ h y" by auto from Suc h_def have "g y = Suc (h y)" by simp with \x \ S\ \y \ S\ show ?case by (simp add: comp_assoc hyp) (simp add: o_assoc comp_fun_commute_on) qed define h where "h z = (if z = x then g x - 1 else g z)" for z with Suc have "n = h x" by simp with Suc have "f y ^^ h y \ f x ^^ h x = f x ^^ h x \ f y ^^ h y" by auto with False h_def have hyp2: "f y ^^ g y \ f x ^^ h x = f x ^^ h x \ f y ^^ g y" by simp from Suc h_def have "g x = Suc (h x)" by simp then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2) (simp add: comp_assoc hyp1) qed qed qed subsubsection \\<^term>\UNIV\ as carrier set\ locale comp_fun_commute = fixes f :: "'a \ 'b \ 'b" assumes comp_fun_commute: "f y \ f x = f x \ f y" begin lemma (in -) comp_fun_commute_def': "comp_fun_commute f = comp_fun_commute_on UNIV f" unfolding comp_fun_commute_def comp_fun_commute_on_def by blast text \ We abuse the \rewrites\ functionality of locales to remove trivial assumptions that result from instantiating the carrier set to \<^term>\UNIV\. \ sublocale comp_fun_commute_on UNIV f rewrites "\X. (X \ UNIV) \ True" and "\x. x \ UNIV \ True" and "\P. (True \ P) \ Trueprop P" and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)" proof - show "comp_fun_commute_on UNIV f" by standard (simp add: comp_fun_commute) qed simp_all end lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f o g)" unfolding comp_fun_commute_def' by (fact comp_comp_fun_commute_on) lemma (in comp_fun_commute) comp_fun_commute_funpow: "comp_fun_commute (\x. f x ^^ g x)" unfolding comp_fun_commute_def' by (fact comp_fun_commute_on_funpow) locale comp_fun_idem = comp_fun_commute + assumes comp_fun_idem: "f x o f x = f x" begin lemma (in -) comp_fun_idem_def': "comp_fun_idem f = comp_fun_idem_on UNIV f" unfolding comp_fun_idem_on_def comp_fun_idem_def comp_fun_commute_def' unfolding comp_fun_idem_axioms_def comp_fun_idem_on_axioms_def by blast text \ Again, we abuse the \rewrites\ functionality of locales to remove trivial assumptions that result from instantiating the carrier set to \<^term>\UNIV\. \ sublocale comp_fun_idem_on UNIV f rewrites "\X. (X \ UNIV) \ True" and "\x. x \ UNIV \ True" and "\P. (True \ P) \ Trueprop P" and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)" proof - show "comp_fun_idem_on UNIV f" by standard (simp_all add: comp_fun_idem comp_fun_commute) qed simp_all end lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f o g)" unfolding comp_fun_idem_def' by (fact comp_comp_fun_idem_on) subsubsection \Expressing set operations via \<^const>\fold\\ lemma comp_fun_commute_const: "comp_fun_commute (\_. f)" by standard rule lemma comp_fun_idem_insert: "comp_fun_idem insert" by standard auto lemma comp_fun_idem_remove: "comp_fun_idem Set.remove" by standard auto lemma (in semilattice_inf) comp_fun_idem_inf: "comp_fun_idem inf" by standard (auto simp add: inf_left_commute) lemma (in semilattice_sup) comp_fun_idem_sup: "comp_fun_idem sup" by standard (auto simp add: sup_left_commute) lemma union_fold_insert: assumes "finite A" shows "A \ B = fold insert B A" proof - interpret comp_fun_idem insert by (fact comp_fun_idem_insert) from \finite A\ show ?thesis by (induct A arbitrary: B) simp_all qed lemma minus_fold_remove: assumes "finite A" shows "B - A = fold Set.remove B A" proof - interpret comp_fun_idem Set.remove by (fact comp_fun_idem_remove) from \finite A\ have "fold Set.remove B A = B - A" by (induct A arbitrary: B) auto (* slow *) then show ?thesis .. qed lemma comp_fun_commute_filter_fold: "comp_fun_commute (\x A'. if P x then Set.insert x A' else A')" proof - interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert) show ?thesis by standard (auto simp: fun_eq_iff) qed lemma Set_filter_fold: assumes "finite A" shows "Set.filter P A = fold (\x A'. if P x then Set.insert x A' else A') {} A" using assms proof - interpret commute_insert: comp_fun_commute "(\x A'. if P x then Set.insert x A' else A')" by (fact comp_fun_commute_filter_fold) from \finite A\ show ?thesis by induct (auto simp add: Set.filter_def) qed lemma inter_Set_filter: assumes "finite B" shows "A \ B = Set.filter (\x. x \ A) B" using assms by induct (auto simp: Set.filter_def) lemma image_fold_insert: assumes "finite A" shows "image f A = fold (\k A. Set.insert (f k) A) {} A" proof - interpret comp_fun_commute "\k A. Set.insert (f k) A" by standard auto show ?thesis using assms by (induct A) auto qed lemma Ball_fold: assumes "finite A" shows "Ball A P = fold (\k s. s \ P k) True A" proof - interpret comp_fun_commute "\k s. s \ P k" by standard auto show ?thesis using assms by (induct A) auto qed lemma Bex_fold: assumes "finite A" shows "Bex A P = fold (\k s. s \ P k) False A" proof - interpret comp_fun_commute "\k s. s \ P k" by standard auto show ?thesis using assms by (induct A) auto qed lemma comp_fun_commute_Pow_fold: "comp_fun_commute (\x A. A \ Set.insert x ` A)" by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast lemma Pow_fold: assumes "finite A" shows "Pow A = fold (\x A. A \ Set.insert x ` A) {{}} A" proof - interpret comp_fun_commute "\x A. A \ Set.insert x ` A" by (rule comp_fun_commute_Pow_fold) show ?thesis using assms by (induct A) (auto simp: Pow_insert) qed lemma fold_union_pair: assumes "finite B" shows "(\y\B. {(x, y)}) \ A = fold (\y. Set.insert (x, y)) A B" proof - interpret comp_fun_commute "\y. Set.insert (x, y)" by standard auto show ?thesis using assms by (induct arbitrary: A) simp_all qed lemma comp_fun_commute_product_fold: "finite B \ comp_fun_commute (\x z. fold (\y. Set.insert (x, y)) z B)" by standard (auto simp: fold_union_pair [symmetric]) lemma product_fold: assumes "finite A" "finite B" shows "A \ B = fold (\x z. fold (\y. Set.insert (x, y)) z B) {} A" proof - interpret commute_product: comp_fun_commute "(\x z. fold (\y. Set.insert (x, y)) z B)" by (fact comp_fun_commute_product_fold[OF \finite B\]) from assms show ?thesis unfolding Sigma_def by (induct A) (simp_all add: fold_union_pair) qed context complete_lattice begin lemma inf_Inf_fold_inf: assumes "finite A" shows "inf (Inf A) B = fold inf B A" proof - interpret comp_fun_idem inf by (fact comp_fun_idem_inf) from \finite A\ fold_fun_left_comm show ?thesis by (induct A arbitrary: B) (simp_all add: inf_commute fun_eq_iff) qed lemma sup_Sup_fold_sup: assumes "finite A" shows "sup (Sup A) B = fold sup B A" proof - interpret comp_fun_idem sup by (fact comp_fun_idem_sup) from \finite A\ fold_fun_left_comm show ?thesis by (induct A arbitrary: B) (simp_all add: sup_commute fun_eq_iff) qed lemma Inf_fold_inf: "finite A \ Inf A = fold inf top A" using inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2) lemma Sup_fold_sup: "finite A \ Sup A = fold sup bot A" using sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2) lemma inf_INF_fold_inf: assumes "finite A" shows "inf B (\(f ` A)) = fold (inf \ f) B A" (is "?inf = ?fold") proof - interpret comp_fun_idem inf by (fact comp_fun_idem_inf) interpret comp_fun_idem "inf \ f" by (fact comp_comp_fun_idem) from \finite A\ have "?fold = ?inf" by (induct A arbitrary: B) (simp_all add: inf_left_commute) then show ?thesis .. qed lemma sup_SUP_fold_sup: assumes "finite A" shows "sup B (\(f ` A)) = fold (sup \ f) B A" (is "?sup = ?fold") proof - interpret comp_fun_idem sup by (fact comp_fun_idem_sup) interpret comp_fun_idem "sup \ f" by (fact comp_comp_fun_idem) from \finite A\ have "?fold = ?sup" by (induct A arbitrary: B) (simp_all add: sup_left_commute) then show ?thesis .. qed lemma INF_fold_inf: "finite A \ \(f ` A) = fold (inf \ f) top A" using inf_INF_fold_inf [of A top] by simp lemma SUP_fold_sup: "finite A \ \(f ` A) = fold (sup \ f) bot A" using sup_SUP_fold_sup [of A bot] by simp lemma finite_Inf_in: assumes "finite A" "A\{}" and inf: "\x y. \x \ A; y \ A\ \ inf x y \ A" shows "Inf A \ A" proof - have "Inf B \ A" if "B \ A" "B\{}" for B using finite_subset [OF \B \ A\ \finite A\] that by (induction B) (use inf in \force+\) then show ?thesis by (simp add: assms) qed lemma finite_Sup_in: assumes "finite A" "A\{}" and sup: "\x y. \x \ A; y \ A\ \ sup x y \ A" shows "Sup A \ A" proof - have "Sup B \ A" if "B \ A" "B\{}" for B using finite_subset [OF \B \ A\ \finite A\] that by (induction B) (use sup in \force+\) then show ?thesis by (simp add: assms) qed end subsection \Locales as mini-packages for fold operations\ subsubsection \The natural case\ locale folding_on = fixes S :: "'a set" fixes f :: "'a \ 'b \ 'b" and z :: "'b" assumes comp_fun_commute_on: "x \ S \ y \ S \ f y o f x = f x o f y" begin interpretation fold?: comp_fun_commute_on S f by standard (simp add: comp_fun_commute_on) definition F :: "'a set \ 'b" where eq_fold: "F A = Finite_Set.fold f z A" lemma empty [simp]: "F {} = z" by (simp add: eq_fold) lemma infinite [simp]: "\ finite A \ F A = z" by (simp add: eq_fold) lemma insert [simp]: assumes "insert x A \ S" and "finite A" and "x \ A" shows "F (insert x A) = f x (F A)" proof - from fold_insert assms have "Finite_Set.fold f z (insert x A) = f x (Finite_Set.fold f z A)" by simp with \finite A\ show ?thesis by (simp add: eq_fold fun_eq_iff) qed lemma remove: assumes "A \ S" and "finite A" and "x \ A" shows "F A = f x (F (A - {x}))" proof - from \x \ A\ obtain B where A: "A = insert x B" and "x \ B" by (auto dest: mk_disjoint_insert) moreover from \finite A\ A have "finite B" by simp ultimately show ?thesis using \A \ S\ by auto qed lemma insert_remove: assumes "insert x A \ S" and "finite A" shows "F (insert x A) = f x (F (A - {x}))" using assms by (cases "x \ A") (simp_all add: remove insert_absorb) end subsubsection \With idempotency\ locale folding_idem_on = folding_on + assumes comp_fun_idem_on: "x \ S \ y \ S \ f x \ f x = f x" begin declare insert [simp del] interpretation fold?: comp_fun_idem_on S f by standard (simp_all add: comp_fun_commute_on comp_fun_idem_on) lemma insert_idem [simp]: assumes "insert x A \ S" and "finite A" shows "F (insert x A) = f x (F A)" proof - from fold_insert_idem assms have "fold f z (insert x A) = f x (fold f z A)" by simp with \finite A\ show ?thesis by (simp add: eq_fold fun_eq_iff) qed end subsubsection \\<^term>\UNIV\ as the carrier set\ locale folding = fixes f :: "'a \ 'b \ 'b" and z :: "'b" assumes comp_fun_commute: "f y \ f x = f x \ f y" begin lemma (in -) folding_def': "folding f = folding_on UNIV f" unfolding folding_def folding_on_def by blast text \ Again, we abuse the \rewrites\ functionality of locales to remove trivial assumptions that result from instantiating the carrier set to \<^term>\UNIV\. \ sublocale folding_on UNIV f rewrites "\X. (X \ UNIV) \ True" and "\x. x \ UNIV \ True" and "\P. (True \ P) \ Trueprop P" and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)" proof - show "folding_on UNIV f" by standard (simp add: comp_fun_commute) qed simp_all end locale folding_idem = folding + assumes comp_fun_idem: "f x \ f x = f x" begin lemma (in -) folding_idem_def': "folding_idem f = folding_idem_on UNIV f" unfolding folding_idem_def folding_def' folding_idem_on_def unfolding folding_idem_axioms_def folding_idem_on_axioms_def by blast text \ Again, we abuse the \rewrites\ functionality of locales to remove trivial assumptions that result from instantiating the carrier set to \<^term>\UNIV\. \ sublocale folding_idem_on UNIV f rewrites "\X. (X \ UNIV) \ True" and "\x. x \ UNIV \ True" and "\P. (True \ P) \ Trueprop P" and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)" proof - show "folding_idem_on UNIV f" by standard (simp add: comp_fun_idem) qed simp_all end subsection \Finite cardinality\ text \ The traditional definition \<^prop>\card A \ LEAST n. \f. A = {f i |i. i < n}\ is ugly to work with. But now that we have \<^const>\fold\ things are easy: \ global_interpretation card: folding "\_. Suc" 0 defines card = "folding_on.F (\_. Suc) 0" by standard rule lemma card_insert_disjoint: "finite A \ x \ A \ card (insert x A) = Suc (card A)" by (fact card.insert) lemma card_insert_if: "finite A \ card (insert x A) = (if x \ A then card A else Suc (card A))" by auto (simp add: card.insert_remove card.remove) lemma card_ge_0_finite: "card A > 0 \ finite A" by (rule ccontr) simp lemma card_0_eq [simp]: "finite A \ card A = 0 \ A = {}" by (auto dest: mk_disjoint_insert) lemma finite_UNIV_card_ge_0: "finite (UNIV :: 'a set) \ card (UNIV :: 'a set) > 0" by (rule ccontr) simp lemma card_eq_0_iff: "card A = 0 \ A = {} \ \ finite A" by auto lemma card_range_greater_zero: "finite (range f) \ card (range f) > 0" by (rule ccontr) (simp add: card_eq_0_iff) lemma card_gt_0_iff: "0 < card A \ A \ {} \ finite A" by (simp add: neq0_conv [symmetric] card_eq_0_iff) lemma card_Suc_Diff1: assumes "finite A" "x \ A" shows "Suc (card (A - {x})) = card A" proof - have "Suc (card (A - {x})) = card (insert x (A - {x}))" using assms by (simp add: card.insert_remove) also have "... = card A" using assms by (simp add: card_insert_if) finally show ?thesis . qed lemma card_insert_le_m1: assumes "n > 0" "card y \ n - 1" shows "card (insert x y) \ n" using assms by (cases "finite y") (auto simp: card_insert_if) lemma card_Diff_singleton: assumes "x \ A" shows "card (A - {x}) = card A - 1" proof (cases "finite A") case True with assms show ?thesis by (simp add: card_Suc_Diff1 [symmetric]) qed auto lemma card_Diff_singleton_if: "card (A - {x}) = (if x \ A then card A - 1 else card A)" by (simp add: card_Diff_singleton) lemma card_Diff_insert[simp]: assumes "a \ A" and "a \ B" shows "card (A - insert a B) = card (A - B) - 1" proof - have "A - insert a B = (A - B) - {a}" using assms by blast then show ?thesis using assms by (simp add: card_Diff_singleton) qed lemma card_insert_le: "card A \ card (insert x A)" proof (cases "finite A") case True then show ?thesis by (simp add: card_insert_if) qed auto lemma card_Collect_less_nat[simp]: "card {i::nat. i < n} = n" by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq) lemma card_Collect_le_nat[simp]: "card {i::nat. i \ n} = Suc n" using card_Collect_less_nat[of "Suc n"] by (simp add: less_Suc_eq_le) lemma card_mono: assumes "finite B" and "A \ B" shows "card A \ card B" proof - from assms have "finite A" by (auto intro: finite_subset) then show ?thesis using assms proof (induct A arbitrary: B) case empty then show ?case by simp next case (insert x A) then have "x \ B" by simp from insert have "A \ B - {x}" and "finite (B - {x})" by auto with insert.hyps have "card A \ card (B - {x})" by auto with \finite A\ \x \ A\ \finite B\ \x \ B\ show ?case by simp (simp only: card.remove) qed qed lemma card_seteq: assumes "finite B" and A: "A \ B" "card B \ card A" shows "A = B" using assms proof (induction arbitrary: A rule: finite_induct) case (insert b B) then have A: "finite A" "A - {b} \ B" by force+ then have "card B \ card (A - {b})" using insert by (auto simp add: card_Diff_singleton_if) then have "A - {b} = B" using A insert.IH by auto then show ?case using insert.hyps insert.prems by auto qed auto lemma psubset_card_mono: "finite B \ A < B \ card A < card B" using card_seteq [of B A] by (auto simp add: psubset_eq) lemma card_Un_Int: assumes "finite A" "finite B" shows "card A + card B = card (A \ B) + card (A \ B)" using assms proof (induct A) case empty then show ?case by simp next case insert then show ?case by (auto simp add: insert_absorb Int_insert_left) qed lemma card_Un_disjoint: "finite A \ finite B \ A \ B = {} \ card (A \ B) = card A + card B" using card_Un_Int [of A B] by simp lemma card_Un_disjnt: "\finite A; finite B; disjnt A B\ \ card (A \ B) = card A + card B" by (simp add: card_Un_disjoint disjnt_def) lemma card_Un_le: "card (A \ B) \ card A + card B" proof (cases "finite A \ finite B") case True then show ?thesis using le_iff_add card_Un_Int [of A B] by auto qed auto lemma card_Diff_subset: assumes "finite B" and "B \ A" shows "card (A - B) = card A - card B" using assms proof (cases "finite A") case False with assms show ?thesis by simp next case True with assms show ?thesis by (induct B arbitrary: A) simp_all qed lemma card_Diff_subset_Int: assumes "finite (A \ B)" shows "card (A - B) = card A - card (A \ B)" proof - have "A - B = A - A \ B" by auto with assms show ?thesis by (simp add: card_Diff_subset) qed lemma diff_card_le_card_Diff: assumes "finite B" shows "card A - card B \ card (A - B)" proof - have "card A - card B \ card A - card (A \ B)" using card_mono[OF assms Int_lower2, of A] by arith also have "\ = card (A - B)" using assms by (simp add: card_Diff_subset_Int) finally show ?thesis . qed lemma card_le_sym_Diff: assumes "finite A" "finite B" "card A \ card B" shows "card(A - B) \ card(B - A)" proof - have "card(A - B) = card A - card (A \ B)" using assms(1,2) by(simp add: card_Diff_subset_Int) also have "\ \ card B - card (A \ B)" using assms(3) by linarith also have "\ = card(B - A)" using assms(1,2) by(simp add: card_Diff_subset_Int Int_commute) finally show ?thesis . qed lemma card_less_sym_Diff: assumes "finite A" "finite B" "card A < card B" shows "card(A - B) < card(B - A)" proof - have "card(A - B) = card A - card (A \ B)" using assms(1,2) by(simp add: card_Diff_subset_Int) also have "\ < card B - card (A \ B)" using assms(1,3) by (simp add: card_mono diff_less_mono) also have "\ = card(B - A)" using assms(1,2) by(simp add: card_Diff_subset_Int Int_commute) finally show ?thesis . qed lemma card_Diff1_less_iff: "card (A - {x}) < card A \ finite A \ x \ A" proof (cases "finite A \ x \ A") case True then show ?thesis by (auto simp: card_gt_0_iff intro: diff_less) qed auto lemma card_Diff1_less: "finite A \ x \ A \ card (A - {x}) < card A" unfolding card_Diff1_less_iff by auto lemma card_Diff2_less: assumes "finite A" "x \ A" "y \ A" shows "card (A - {x} - {y}) < card A" proof (cases "x = y") case True with assms show ?thesis by (simp add: card_Diff1_less del: card_Diff_insert) next case False then have "card (A - {x} - {y}) < card (A - {x})" "card (A - {x}) < card A" using assms by (intro card_Diff1_less; simp)+ then show ?thesis by (blast intro: less_trans) qed lemma card_Diff1_le: "card (A - {x}) \ card A" proof (cases "finite A") case True then show ?thesis by (cases "x \ A") (simp_all add: card_Diff1_less less_imp_le) qed auto lemma card_psubset: "finite B \ A \ B \ card A < card B \ A < B" by (erule psubsetI) blast lemma card_le_inj: assumes fA: "finite A" and fB: "finite B" and c: "card A \ card B" shows "\f. f ` A \ B \ inj_on f A" using fA fB c proof (induct arbitrary: B rule: finite_induct) case empty then show ?case by simp next case (insert x s t) then show ?case proof (induct rule: finite_induct [OF insert.prems(1)]) case 1 then show ?case by simp next case (2 y t) from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \ card t" by simp from "2.prems"(3) [OF "2.hyps"(1) cst] obtain f where "f ` s \ t" "inj_on f s" by blast with "2.prems"(2) "2.hyps"(2) show ?case unfolding inj_on_def by (rule_tac x = "\z. if z = x then y else f z" in exI) auto qed qed lemma card_subset_eq: assumes fB: "finite B" and AB: "A \ B" and c: "card A = card B" shows "A = B" proof - from fB AB have fA: "finite A" by (auto intro: finite_subset) from fA fB have fBA: "finite (B - A)" by auto have e: "A \ (B - A) = {}" by blast have eq: "A \ (B - A) = B" using AB by blast from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0" by arith then have "B - A = {}" unfolding card_eq_0_iff using fA fB by simp with AB show "A = B" by blast qed lemma insert_partition: "x \ F \ \c1 \ insert x F. \c2 \ insert x F. c1 \ c2 \ c1 \ c2 = {} \ x \ \F = {}" by auto lemma finite_psubset_induct [consumes 1, case_names psubset]: assumes finite: "finite A" and major: "\A. finite A \ (\B. B \ A \ P B) \ P A" shows "P A" using finite proof (induct A taking: card rule: measure_induct_rule) case (less A) have fin: "finite A" by fact have ih: "card B < card A \ finite B \ P B" for B by fact have "P B" if "B \ A" for B proof - from that have "card B < card A" using psubset_card_mono fin by blast moreover from that have "B \ A" by auto then have "finite B" using fin finite_subset by blast ultimately show ?thesis using ih by simp qed with fin show "P A" using major by blast qed lemma finite_induct_select [consumes 1, case_names empty select]: assumes "finite S" and "P {}" and select: "\T. T \ S \ P T \ \s\S - T. P (insert s T)" shows "P S" proof - have "0 \ card S" by simp then have "\T \ S. card T = card S \ P T" proof (induct rule: dec_induct) case base with \P {}\ show ?case by (intro exI[of _ "{}"]) auto next case (step n) then obtain T where T: "T \ S" "card T = n" "P T" by auto with \n < card S\ have "T \ S" "P T" by auto with select[of T] obtain s where "s \ S" "s \ T" "P (insert s T)" by auto with step(2) T \finite S\ show ?case by (intro exI[of _ "insert s T"]) (auto dest: finite_subset) qed with \finite S\ show "P S" by (auto dest: card_subset_eq) qed lemma remove_induct [case_names empty infinite remove]: assumes empty: "P ({} :: 'a set)" and infinite: "\ finite B \ P B" and remove: "\A. finite A \ A \ {} \ A \ B \ (\x. x \ A \ P (A - {x})) \ P A" shows "P B" proof (cases "finite B") case False then show ?thesis by (rule infinite) next case True define A where "A = B" with True have "finite A" "A \ B" by simp_all then show "P A" proof (induct "card A" arbitrary: A) case 0 then have "A = {}" by auto with empty show ?case by simp next case (Suc n A) from \A \ B\ and \finite B\ have "finite A" by (rule finite_subset) moreover from Suc.hyps have "A \ {}" by auto moreover note \A \ B\ moreover have "P (A - {x})" if x: "x \ A" for x using x Suc.prems \Suc n = card A\ by (intro Suc) auto ultimately show ?case by (rule remove) qed qed lemma finite_remove_induct [consumes 1, case_names empty remove]: fixes P :: "'a set \ bool" assumes "finite B" and "P {}" and "\A. finite A \ A \ {} \ A \ B \ (\x. x \ A \ P (A - {x})) \ P A" defines "B' \ B" shows "P B'" by (induct B' rule: remove_induct) (simp_all add: assms) text \Main cardinality theorem.\ lemma card_partition [rule_format]: "finite C \ finite (\C) \ (\c\C. card c = k) \ (\c1 \ C. \c2 \ C. c1 \ c2 \ c1 \ c2 = {}) \ k * card C = card (\C)" proof (induct rule: finite_induct) case empty then show ?case by simp next case (insert x F) then show ?case by (simp add: card_Un_disjoint insert_partition finite_subset [of _ "\(insert _ _)"]) qed lemma card_eq_UNIV_imp_eq_UNIV: assumes fin: "finite (UNIV :: 'a set)" and card: "card A = card (UNIV :: 'a set)" shows "A = (UNIV :: 'a set)" proof show "A \ UNIV" by simp show "UNIV \ A" proof show "x \ A" for x proof (rule ccontr) assume "x \ A" then have "A \ UNIV" by auto with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono) with card show False by simp qed qed qed text \The form of a finite set of given cardinality\ lemma card_eq_SucD: assumes "card A = Suc k" shows "\b B. A = insert b B \ b \ B \ card B = k \ (k = 0 \ B = {})" proof - have fin: "finite A" using assms by (auto intro: ccontr) moreover have "card A \ 0" using assms by auto ultimately obtain b where b: "b \ A" by auto show ?thesis proof (intro exI conjI) show "A = insert b (A - {b})" using b by blast show "b \ A - {b}" by blast show "card (A - {b}) = k" and "k = 0 \ A - {b} = {}" using assms b fin by (fastforce dest: mk_disjoint_insert)+ qed qed lemma card_Suc_eq: "card A = Suc k \ (\b B. A = insert b B \ b \ B \ card B = k \ (k = 0 \ B = {}))" by (auto simp: card_insert_if card_gt_0_iff elim!: card_eq_SucD) lemma card_Suc_eq_finite: "card A = Suc k \ (\b B. A = insert b B \ b \ B \ card B = k \ finite B)" unfolding card_Suc_eq using card_gt_0_iff by fastforce lemma card_1_singletonE: assumes "card A = 1" obtains x where "A = {x}" using assms by (auto simp: card_Suc_eq) lemma is_singleton_altdef: "is_singleton A \ card A = 1" unfolding is_singleton_def by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def) lemma card_1_singleton_iff: "card A = Suc 0 \ (\x. A = {x})" by (simp add: card_Suc_eq) lemma card_le_Suc0_iff_eq: assumes "finite A" shows "card A \ Suc 0 \ (\a1 \ A. \a2 \ A. a1 = a2)" (is "?C = ?A") proof assume ?C thus ?A using assms by (auto simp: le_Suc_eq dest: card_eq_SucD) next assume ?A show ?C proof cases assume "A = {}" thus ?C using \?A\ by simp next assume "A \ {}" then obtain a where "A = {a}" using \?A\ by blast thus ?C by simp qed qed lemma card_le_Suc_iff: "Suc n \ card A = (\a B. A = insert a B \ a \ B \ n \ card B \ finite B)" proof (cases "finite A") case True then show ?thesis by (fastforce simp: card_Suc_eq less_eq_nat.simps split: nat.splits) qed auto lemma finite_fun_UNIVD2: assumes fin: "finite (UNIV :: ('a \ 'b) set)" shows "finite (UNIV :: 'b set)" proof - from fin have "finite (range (\f :: 'a \ 'b. f arbitrary))" for arbitrary by (rule finite_imageI) moreover have "UNIV = range (\f :: 'a \ 'b. f arbitrary)" for arbitrary by (rule UNIV_eq_I) auto ultimately show "finite (UNIV :: 'b set)" by simp qed lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1" unfolding UNIV_unit by simp lemma infinite_arbitrarily_large: assumes "\ finite A" shows "\B. finite B \ card B = n \ B \ A" proof (induction n) case 0 show ?case by (intro exI[of _ "{}"]) auto next case (Suc n) then obtain B where B: "finite B \ card B = n \ B \ A" .. with \\ finite A\ have "A \ B" by auto with B have "B \ A" by auto then have "\x. x \ A - B" by (elim psubset_imp_ex_mem) then obtain x where x: "x \ A - B" .. with B have "finite (insert x B) \ card (insert x B) = Suc n \ insert x B \ A" by auto then show "\B. finite B \ card B = Suc n \ B \ A" .. qed text \Sometimes, to prove that a set is finite, it is convenient to work with finite subsets and to show that their cardinalities are uniformly bounded. This possibility is formalized in the next criterion.\ lemma finite_if_finite_subsets_card_bdd: assumes "\G. G \ F \ finite G \ card G \ C" shows "finite F \ card F \ C" proof (cases "finite F") case False obtain n::nat where n: "n > max C 0" by auto obtain G where G: "G \ F" "card G = n" using infinite_arbitrarily_large[OF False] by auto hence "finite G" using \n > max C 0\ using card.infinite gr_implies_not0 by blast hence False using assms G n not_less by auto thus ?thesis .. next case True thus ?thesis using assms[of F] by auto qed subsubsection \Cardinality of image\ lemma card_image_le: "finite A \ card (f ` A) \ card A" by (induct rule: finite_induct) (simp_all add: le_SucI card_insert_if) lemma card_image: "inj_on f A \ card (f ` A) = card A" proof (induct A rule: infinite_finite_induct) case (infinite A) then have "\ finite (f ` A)" by (auto dest: finite_imageD) with infinite show ?case by simp qed simp_all lemma bij_betw_same_card: "bij_betw f A B \ card A = card B" by (auto simp: card_image bij_betw_def) lemma endo_inj_surj: "finite A \ f ` A \ A \ inj_on f A \ f ` A = A" by (simp add: card_seteq card_image) lemma eq_card_imp_inj_on: assumes "finite A" "card(f ` A) = card A" shows "inj_on f A" using assms proof (induct rule:finite_induct) case empty show ?case by simp next case (insert x A) then show ?case using card_image_le [of A f] by (simp add: card_insert_if split: if_splits) qed lemma inj_on_iff_eq_card: "finite A \ inj_on f A \ card (f ` A) = card A" by (blast intro: card_image eq_card_imp_inj_on) lemma card_inj_on_le: assumes "inj_on f A" "f ` A \ B" "finite B" shows "card A \ card B" proof - have "finite A" using assms by (blast intro: finite_imageD dest: finite_subset) then show ?thesis using assms by (force intro: card_mono simp: card_image [symmetric]) qed lemma inj_on_iff_card_le: "\ finite A; finite B \ \ (\f. inj_on f A \ f ` A \ B) = (card A \ card B)" using card_inj_on_le[of _ A B] card_le_inj[of A B] by blast lemma surj_card_le: "finite A \ B \ f ` A \ card B \ card A" by (blast intro: card_image_le card_mono le_trans) lemma card_bij_eq: "inj_on f A \ f ` A \ B \ inj_on g B \ g ` B \ A \ finite A \ finite B \ card A = card B" by (auto intro: le_antisym card_inj_on_le) lemma bij_betw_finite: "bij_betw f A B \ finite A \ finite B" unfolding bij_betw_def using finite_imageD [of f A] by auto lemma inj_on_finite: "inj_on f A \ f ` A \ B \ finite B \ finite A" using finite_imageD finite_subset by blast lemma card_vimage_inj: "inj f \ A \ range f \ card (f -` A) = card A" by (auto 4 3 simp: subset_image_iff inj_vimage_image_eq intro: card_image[symmetric, OF subset_inj_on]) subsubsection \Pigeonhole Principles\ lemma pigeonhole: "card A > card (f ` A) \ \ inj_on f A " by (auto dest: card_image less_irrefl_nat) lemma pigeonhole_infinite: assumes "\ finite A" and "finite (f`A)" shows "\a0\A. \ finite {a\A. f a = f a0}" using assms(2,1) proof (induct "f`A" arbitrary: A rule: finite_induct) case empty then show ?case by simp next case (insert b F) show ?case proof (cases "finite {a\A. f a = b}") case True with \\ finite A\ have "\ finite (A - {a\A. f a = b})" by simp also have "A - {a\A. f a = b} = {a\A. f a \ b}" by blast finally have "\ finite {a\A. f a \ b}" . from insert(3)[OF _ this] insert(2,4) show ?thesis by simp (blast intro: rev_finite_subset) next case False then have "{a \ A. f a = b} \ {}" by force with False show ?thesis by blast qed qed lemma pigeonhole_infinite_rel: assumes "\ finite A" and "finite B" and "\a\A. \b\B. R a b" shows "\b\B. \ finite {a:A. R a b}" proof - let ?F = "\a. {b\B. R a b}" from finite_Pow_iff[THEN iffD2, OF \finite B\] have "finite (?F ` A)" by (blast intro: rev_finite_subset) from pigeonhole_infinite [where f = ?F, OF assms(1) this] obtain a0 where "a0 \ A" and infinite: "\ finite {a\A. ?F a = ?F a0}" .. obtain b0 where "b0 \ B" and "R a0 b0" using \a0 \ A\ assms(3) by blast have "finite {a\A. ?F a = ?F a0}" if "finite {a\A. R a b0}" using \b0 \ B\ \R a0 b0\ that by (blast intro: rev_finite_subset) with infinite \b0 \ B\ show ?thesis by blast qed subsubsection \Cardinality of sums\ lemma card_Plus: assumes "finite A" "finite B" shows "card (A <+> B) = card A + card B" proof - have "Inl`A \ Inr`B = {}" by fast with assms show ?thesis by (simp add: Plus_def card_Un_disjoint card_image) qed lemma card_Plus_conv_if: "card (A <+> B) = (if finite A \ finite B then card A + card B else 0)" by (auto simp add: card_Plus) text \Relates to equivalence classes. Based on a theorem of F. Kammüller.\ lemma dvd_partition: assumes f: "finite (\C)" and "\c\C. k dvd card c" "\c1\C. \c2\C. c1 \ c2 \ c1 \ c2 = {}" shows "k dvd card (\C)" proof - have "finite C" by (rule finite_UnionD [OF f]) then show ?thesis using assms proof (induct rule: finite_induct) case empty show ?case by simp next case (insert c C) then have "c \ \C = {}" by auto with insert show ?case by (simp add: card_Un_disjoint) qed qed subsubsection \Finite orders\ context order begin lemma finite_has_maximal: "\ finite A; A \ {} \ \ \ m \ A. \ b \ A. m \ b \ m = b" proof (induction rule: finite_psubset_induct) case (psubset A) from \A \ {}\ obtain a where "a \ A" by auto let ?B = "{b \ A. a < b}" show ?case proof cases assume "?B = {}" hence "\ b \ A. a \ b \ a = b" using le_neq_trans by blast thus ?thesis using \a \ A\ by blast next assume "?B \ {}" have "a \ ?B" by auto hence "?B \ A" using \a \ A\ by blast from psubset.IH[OF this \?B \ {}\] show ?thesis using order.strict_trans2 by blast qed qed lemma finite_has_maximal2: "\ finite A; a \ A \ \ \ m \ A. a \ m \ (\ b \ A. m \ b \ m = b)" using finite_has_maximal[of "{b \ A. a \ b}"] by fastforce lemma finite_has_minimal: "\ finite A; A \ {} \ \ \ m \ A. \ b \ A. b \ m \ m = b" proof (induction rule: finite_psubset_induct) case (psubset A) from \A \ {}\ obtain a where "a \ A" by auto let ?B = "{b \ A. b < a}" show ?case proof cases assume "?B = {}" hence "\ b \ A. b \ a \ a = b" using le_neq_trans by blast thus ?thesis using \a \ A\ by blast next assume "?B \ {}" have "a \ ?B" by auto hence "?B \ A" using \a \ A\ by blast from psubset.IH[OF this \?B \ {}\] show ?thesis using order.strict_trans1 by blast qed qed lemma finite_has_minimal2: "\ finite A; a \ A \ \ \ m \ A. m \ a \ (\ b \ A. b \ m \ m = b)" using finite_has_minimal[of "{b \ A. b \ a}"] by fastforce end subsubsection \Relating injectivity and surjectivity\ lemma finite_surj_inj: assumes "finite A" "A \ f ` A" shows "inj_on f A" proof - have "f ` A = A" by (rule card_seteq [THEN sym]) (auto simp add: assms card_image_le) then show ?thesis using assms by (simp add: eq_card_imp_inj_on) qed lemma finite_UNIV_surj_inj: "finite(UNIV:: 'a set) \ surj f \ inj f" for f :: "'a \ 'a" by (blast intro: finite_surj_inj subset_UNIV) lemma finite_UNIV_inj_surj: "finite(UNIV:: 'a set) \ inj f \ surj f" for f :: "'a \ 'a" by (fastforce simp:surj_def dest!: endo_inj_surj) lemma surjective_iff_injective_gen: assumes fS: "finite S" and fT: "finite T" and c: "card S = card T" and ST: "f ` S \ T" shows "(\y \ T. \x \ S. f x = y) \ inj_on f S" (is "?lhs \ ?rhs") proof assume h: "?lhs" { fix x y assume x: "x \ S" assume y: "y \ S" assume f: "f x = f y" from x fS have S0: "card S \ 0" by auto have "x = y" proof (rule ccontr) assume xy: "\ ?thesis" have th: "card S \ card (f ` (S - {y}))" unfolding c proof (rule card_mono) show "finite (f ` (S - {y}))" by (simp add: fS) have "\x \ y; x \ S; z \ S; f x = f y\ \ \x \ S. x \ y \ f z = f x" for z by (case_tac "z = y \ z = x") auto then show "T \ f ` (S - {y})" using h xy x y f by fastforce qed also have " \ \ card (S - {y})" by (simp add: card_image_le fS) also have "\ \ card S - 1" using y fS by simp finally show False using S0 by arith qed } then show ?rhs unfolding inj_on_def by blast next assume h: ?rhs have "f ` S = T" by (simp add: ST c card_image card_subset_eq fT h) then show ?lhs by blast qed hide_const (open) Finite_Set.fold subsection \Infinite Sets\ text \ Some elementary facts about infinite sets, mostly by Stephan Merz. Beware! Because "infinite" merely abbreviates a negation, these lemmas may not work well with \blast\. \ abbreviation infinite :: "'a set \ bool" where "infinite S \ \ finite S" text \ Infinite sets are non-empty, and if we remove some elements from an infinite set, the result is still infinite. \ lemma infinite_UNIV_nat [iff]: "infinite (UNIV :: nat set)" proof assume "finite (UNIV :: nat set)" with finite_UNIV_inj_surj [of Suc] show False by simp (blast dest: Suc_neq_Zero surjD) qed lemma infinite_UNIV_char_0: "infinite (UNIV :: 'a::semiring_char_0 set)" proof assume "finite (UNIV :: 'a set)" with subset_UNIV have "finite (range of_nat :: 'a set)" by (rule finite_subset) moreover have "inj (of_nat :: nat \ 'a)" by (simp add: inj_on_def) ultimately have "finite (UNIV :: nat set)" by (rule finite_imageD) then show False by simp qed lemma infinite_imp_nonempty: "infinite S \ S \ {}" by auto lemma infinite_remove: "infinite S \ infinite (S - {a})" by simp lemma Diff_infinite_finite: assumes "finite T" "infinite S" shows "infinite (S - T)" using \finite T\ proof induct from \infinite S\ show "infinite (S - {})" by auto next fix T x assume ih: "infinite (S - T)" have "S - (insert x T) = (S - T) - {x}" by (rule Diff_insert) with ih show "infinite (S - (insert x T))" by (simp add: infinite_remove) qed lemma Un_infinite: "infinite S \ infinite (S \ T)" by simp lemma infinite_Un: "infinite (S \ T) \ infinite S \ infinite T" by simp lemma infinite_super: assumes "S \ T" and "infinite S" shows "infinite T" proof assume "finite T" with \S \ T\ have "finite S" by (simp add: finite_subset) with \infinite S\ show False by simp qed proposition infinite_coinduct [consumes 1, case_names infinite]: assumes "X A" and step: "\A. X A \ \x\A. X (A - {x}) \ infinite (A - {x})" shows "infinite A" proof assume "finite A" then show False using \X A\ proof (induction rule: finite_psubset_induct) case (psubset A) then obtain x where "x \ A" "X (A - {x}) \ infinite (A - {x})" using local.step psubset.prems by blast then have "X (A - {x})" using psubset.hyps by blast show False proof (rule psubset.IH [where B = "A - {x}"]) show "A - {x} \ A" using \x \ A\ by blast qed fact qed qed text \ For any function with infinite domain and finite range there is some element that is the image of infinitely many domain elements. In particular, any infinite sequence of elements from a finite set contains some element that occurs infinitely often. \ lemma inf_img_fin_dom': assumes img: "finite (f ` A)" and dom: "infinite A" shows "\y \ f ` A. infinite (f -` {y} \ A)" proof (rule ccontr) have "A \ (\y\f ` A. f -` {y} \ A)" by auto moreover assume "\ ?thesis" with img have "finite (\y\f ` A. f -` {y} \ A)" by blast ultimately have "finite A" by (rule finite_subset) with dom show False by contradiction qed lemma inf_img_fin_domE': assumes "finite (f ` A)" and "infinite A" obtains y where "y \ f`A" and "infinite (f -` {y} \ A)" using assms by (blast dest: inf_img_fin_dom') lemma inf_img_fin_dom: assumes img: "finite (f`A)" and dom: "infinite A" shows "\y \ f`A. infinite (f -` {y})" using inf_img_fin_dom'[OF assms] by auto lemma inf_img_fin_domE: assumes "finite (f`A)" and "infinite A" obtains y where "y \ f`A" and "infinite (f -` {y})" using assms by (blast dest: inf_img_fin_dom) proposition finite_image_absD: "finite (abs ` S) \ finite S" for S :: "'a::linordered_ring set" by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom) subsection \The finite powerset operator\ definition Fpow :: "'a set \ 'a set set" where "Fpow A \ {X. X \ A \ finite X}" lemma Fpow_mono: "A \ B \ Fpow A \ Fpow B" unfolding Fpow_def by auto lemma empty_in_Fpow: "{} \ Fpow A" unfolding Fpow_def by auto lemma Fpow_not_empty: "Fpow A \ {}" using empty_in_Fpow by blast lemma Fpow_subset_Pow: "Fpow A \ Pow A" unfolding Fpow_def by auto lemma Fpow_Pow_finite: "Fpow A = Pow A Int {A. finite A}" unfolding Fpow_def Pow_def by blast lemma inj_on_image_Fpow: assumes "inj_on f A" shows "inj_on (image f) (Fpow A)" using assms Fpow_subset_Pow[of A] subset_inj_on[of "image f" "Pow A"] inj_on_image_Pow by blast lemma image_Fpow_mono: assumes "f ` A \ B" shows "(image f) ` (Fpow A) \ Fpow B" using assms by(unfold Fpow_def, auto) end diff --git a/src/HOL/Groups_Big.thy b/src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy +++ b/src/HOL/Groups_Big.thy @@ -1,1673 +1,1687 @@ (* Title: HOL/Groups_Big.thy Author: Tobias Nipkow Author: Lawrence C Paulson Author: Markus Wenzel Author: Jeremy Avigad *) section \Big sum and product over finite (non-empty) sets\ theory Groups_Big imports Power begin subsection \Generic monoid operation over a set\ locale comm_monoid_set = comm_monoid begin subsubsection \Standard sum or product indexed by a finite set\ interpretation comp_fun_commute f by standard (simp add: fun_eq_iff left_commute) interpretation comp?: comp_fun_commute "f \ g" by (fact comp_comp_fun_commute) definition F :: "('b \ 'a) \ 'b set \ 'a" where eq_fold: "F g A = Finite_Set.fold (f \ g) \<^bold>1 A" lemma infinite [simp]: "\ finite A \ F g A = \<^bold>1" by (simp add: eq_fold) lemma empty [simp]: "F g {} = \<^bold>1" by (simp add: eq_fold) lemma insert [simp]: "finite A \ x \ A \ F g (insert x A) = g x \<^bold>* F g A" by (simp add: eq_fold) lemma remove: assumes "finite A" and "x \ A" shows "F g A = g x \<^bold>* F g (A - {x})" proof - from \x \ A\ obtain B where B: "A = insert x B" and "x \ B" by (auto dest: mk_disjoint_insert) moreover from \finite A\ B have "finite B" by simp ultimately show ?thesis by simp qed lemma insert_remove: "finite A \ F g (insert x A) = g x \<^bold>* F g (A - {x})" by (cases "x \ A") (simp_all add: remove insert_absorb) lemma insert_if: "finite A \ F g (insert x A) = (if x \ A then F g A else g x \<^bold>* F g A)" by (cases "x \ A") (simp_all add: insert_absorb) lemma neutral: "\x\A. g x = \<^bold>1 \ F g A = \<^bold>1" by (induct A rule: infinite_finite_induct) simp_all lemma neutral_const [simp]: "F (\_. \<^bold>1) A = \<^bold>1" by (simp add: neutral) lemma union_inter: assumes "finite A" and "finite B" shows "F g (A \ B) \<^bold>* F g (A \ B) = F g A \<^bold>* F g B" \ \The reversed orientation looks more natural, but LOOPS as a simprule!\ using assms proof (induct A) case empty then show ?case by simp next case (insert x A) then show ?case by (auto simp: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute) qed corollary union_inter_neutral: assumes "finite A" and "finite B" and "\x \ A \ B. g x = \<^bold>1" shows "F g (A \ B) = F g A \<^bold>* F g B" using assms by (simp add: union_inter [symmetric] neutral) corollary union_disjoint: assumes "finite A" and "finite B" assumes "A \ B = {}" shows "F g (A \ B) = F g A \<^bold>* F g B" using assms by (simp add: union_inter_neutral) lemma union_diff2: assumes "finite A" and "finite B" shows "F g (A \ B) = F g (A - B) \<^bold>* F g (B - A) \<^bold>* F g (A \ B)" proof - have "A \ B = A - B \ (B - A) \ A \ B" by auto with assms show ?thesis by simp (subst union_disjoint, auto)+ qed lemma subset_diff: assumes "B \ A" and "finite A" shows "F g A = F g (A - B) \<^bold>* F g B" proof - from assms have "finite (A - B)" by auto moreover from assms have "finite B" by (rule finite_subset) moreover from assms have "(A - B) \ B = {}" by auto ultimately have "F g (A - B \ B) = F g (A - B) \<^bold>* F g B" by (rule union_disjoint) moreover from assms have "A \ B = A" by auto ultimately show ?thesis by simp qed lemma Int_Diff: assumes "finite A" shows "F g A = F g (A \ B) \<^bold>* F g (A - B)" by (subst subset_diff [where B = "A - B"]) (auto simp: Diff_Diff_Int assms) lemma setdiff_irrelevant: assumes "finite A" shows "F g (A - {x. g x = z}) = F g A" using assms by (induct A) (simp_all add: insert_Diff_if) lemma not_neutral_contains_not_neutral: assumes "F g A \ \<^bold>1" obtains a where "a \ A" and "g a \ \<^bold>1" proof - from assms have "\a\A. g a \ \<^bold>1" proof (induct A rule: infinite_finite_induct) case infinite then show ?case by simp next case empty then show ?case by simp next case (insert a A) then show ?case by fastforce qed with that show thesis by blast qed lemma reindex: assumes "inj_on h A" shows "F g (h ` A) = F (g \ h) A" proof (cases "finite A") case True with assms show ?thesis by (simp add: eq_fold fold_image comp_assoc) next case False with assms have "\ finite (h ` A)" by (blast dest: finite_imageD) with False show ?thesis by simp qed lemma cong [fundef_cong]: assumes "A = B" assumes g_h: "\x. x \ B \ g x = h x" shows "F g A = F h B" using g_h unfolding \A = B\ by (induct B rule: infinite_finite_induct) auto lemma cong_simp [cong]: "\ A = B; \x. x \ B =simp=> g x = h x \ \ F (\x. g x) A = F (\x. h x) B" by (rule cong) (simp_all add: simp_implies_def) lemma reindex_cong: assumes "inj_on l B" assumes "A = l ` B" assumes "\x. x \ B \ g (l x) = h x" shows "F g A = F h B" using assms by (simp add: reindex) lemma image_eq: assumes "inj_on g A" shows "F (\x. x) (g ` A) = F g A" using assms reindex_cong by fastforce lemma UNION_disjoint: assumes "finite I" and "\i\I. finite (A i)" and "\i\I. \j\I. i \ j \ A i \ A j = {}" shows "F g (\(A ` I)) = F (\x. F g (A x)) I" using assms proof (induction rule: finite_induct) case (insert i I) then have "\j\I. j \ i" by blast with insert.prems have "A i \ \(A ` I) = {}" by blast with insert show ?case by (simp add: union_disjoint) qed auto lemma Union_disjoint: assumes "\A\C. finite A" "\A\C. \B\C. A \ B \ A \ B = {}" shows "F g (\C) = (F \ F) g C" proof (cases "finite C") case True from UNION_disjoint [OF this assms] show ?thesis by simp next case False then show ?thesis by (auto dest: finite_UnionD intro: infinite) qed lemma distrib: "F (\x. g x \<^bold>* h x) A = F g A \<^bold>* F h A" by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute) lemma Sigma: assumes "finite A" "\x\A. finite (B x)" shows "F (\x. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)" unfolding Sigma_def proof (subst UNION_disjoint) show "F (\x. F (g x) (B x)) A = F (\x. F (\(x, y). g x y) (\y\B x. {(x, y)})) A" proof (rule cong [OF refl]) show "F (g x) (B x) = F (\(x, y). g x y) (\y\B x. {(x, y)})" if "x \ A" for x using that assms by (simp add: UNION_disjoint) qed qed (use assms in auto) lemma related: assumes Re: "R \<^bold>1 \<^bold>1" and Rop: "\x1 y1 x2 y2. R x1 x2 \ R y1 y2 \ R (x1 \<^bold>* y1) (x2 \<^bold>* y2)" and fin: "finite S" and R_h_g: "\x\S. R (h x) (g x)" shows "R (F h S) (F g S)" using fin by (rule finite_subset_induct) (use assms in auto) lemma mono_neutral_cong_left: assumes "finite T" and "S \ T" and "\i \ T - S. h i = \<^bold>1" and "\x. x \ S \ g x = h x" shows "F g S = F h T" proof- have eq: "T = S \ (T - S)" using \S \ T\ by blast have d: "S \ (T - S) = {}" using \S \ T\ by blast from \finite T\ \S \ T\ have f: "finite S" "finite (T - S)" by (auto intro: finite_subset) show ?thesis using assms(4) by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)]) qed lemma mono_neutral_cong_right: "finite T \ S \ T \ \i \ T - S. g i = \<^bold>1 \ (\x. x \ S \ g x = h x) \ F g T = F h S" by (auto intro!: mono_neutral_cong_left [symmetric]) lemma mono_neutral_left: "finite T \ S \ T \ \i \ T - S. g i = \<^bold>1 \ F g S = F g T" by (blast intro: mono_neutral_cong_left) lemma mono_neutral_right: "finite T \ S \ T \ \i \ T - S. g i = \<^bold>1 \ F g T = F g S" by (blast intro!: mono_neutral_left [symmetric]) lemma mono_neutral_cong: assumes [simp]: "finite T" "finite S" and *: "\i. i \ T - S \ h i = \<^bold>1" "\i. i \ S - T \ g i = \<^bold>1" and gh: "\x. x \ S \ T \ g x = h x" shows "F g S = F h T" proof- have "F g S = F g (S \ T)" by(rule mono_neutral_right)(auto intro: *) also have "\ = F h (S \ T)" using refl gh by(rule cong) also have "\ = F h T" by(rule mono_neutral_left)(auto intro: *) finally show ?thesis . qed lemma reindex_bij_betw: "bij_betw h S T \ F (\x. g (h x)) S = F g T" by (auto simp: bij_betw_def reindex) lemma reindex_bij_witness: assumes witness: "\a. a \ S \ i (j a) = a" "\a. a \ S \ j a \ T" "\b. b \ T \ j (i b) = b" "\b. b \ T \ i b \ S" assumes eq: "\a. a \ S \ h (j a) = g a" shows "F g S = F h T" proof - have "bij_betw j S T" using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto moreover have "F g S = F (\x. h (j x)) S" by (intro cong) (auto simp: eq) ultimately show ?thesis by (simp add: reindex_bij_betw) qed lemma reindex_bij_betw_not_neutral: assumes fin: "finite S'" "finite T'" assumes bij: "bij_betw h (S - S') (T - T')" assumes nn: "\a. a \ S' \ g (h a) = z" "\b. b \ T' \ g b = z" shows "F (\x. g (h x)) S = F g T" proof - have [simp]: "finite S \ finite T" using bij_betw_finite[OF bij] fin by auto show ?thesis proof (cases "finite S") case True with nn have "F (\x. g (h x)) S = F (\x. g (h x)) (S - S')" by (intro mono_neutral_cong_right) auto also have "\ = F g (T - T')" using bij by (rule reindex_bij_betw) also have "\ = F g T" using nn \finite S\ by (intro mono_neutral_cong_left) auto finally show ?thesis . next case False then show ?thesis by simp qed qed lemma reindex_nontrivial: assumes "finite A" and nz: "\x y. x \ A \ y \ A \ x \ y \ h x = h y \ g (h x) = \<^bold>1" shows "F g (h ` A) = F (g \ h) A" proof (subst reindex_bij_betw_not_neutral [symmetric]) show "bij_betw h (A - {x \ A. (g \ h) x = \<^bold>1}) (h ` A - h ` {x \ A. (g \ h) x = \<^bold>1})" using nz by (auto intro!: inj_onI simp: bij_betw_def) qed (use \finite A\ in auto) lemma reindex_bij_witness_not_neutral: assumes fin: "finite S'" "finite T'" assumes witness: "\a. a \ S - S' \ i (j a) = a" "\a. a \ S - S' \ j a \ T - T'" "\b. b \ T - T' \ j (i b) = b" "\b. b \ T - T' \ i b \ S - S'" assumes nn: "\a. a \ S' \ g a = z" "\b. b \ T' \ h b = z" assumes eq: "\a. a \ S \ h (j a) = g a" shows "F g S = F h T" proof - have bij: "bij_betw j (S - (S' \ S)) (T - (T' \ T))" using witness by (intro bij_betw_byWitness[where f'=i]) auto have F_eq: "F g S = F (\x. h (j x)) S" by (intro cong) (auto simp: eq) show ?thesis unfolding F_eq using fin nn eq by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto qed lemma delta_remove: assumes fS: "finite S" shows "F (\k. if k = a then b k else c k) S = (if a \ S then b a \<^bold>* F c (S-{a}) else F c (S-{a}))" proof - let ?f = "(\k. if k = a then b k else c k)" show ?thesis proof (cases "a \ S") case False then have "\k\S. ?f k = c k" by simp with False show ?thesis by simp next case True let ?A = "S - {a}" let ?B = "{a}" from True have eq: "S = ?A \ ?B" by blast have dj: "?A \ ?B = {}" by simp from fS have fAB: "finite ?A" "finite ?B" by auto have "F ?f S = F ?f ?A \<^bold>* F ?f ?B" using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp with True show ?thesis using comm_monoid_set.remove comm_monoid_set_axioms fS by fastforce qed qed lemma delta [simp]: assumes fS: "finite S" shows "F (\k. if k = a then b k else \<^bold>1) S = (if a \ S then b a else \<^bold>1)" by (simp add: delta_remove [OF assms]) lemma delta' [simp]: assumes fin: "finite S" shows "F (\k. if a = k then b k else \<^bold>1) S = (if a \ S then b a else \<^bold>1)" using delta [OF fin, of a b, symmetric] by (auto intro: cong) lemma If_cases: fixes P :: "'b \ bool" and g h :: "'b \ 'a" assumes fin: "finite A" shows "F (\x. if P x then h x else g x) A = F h (A \ {x. P x}) \<^bold>* F g (A \ - {x. P x})" proof - have a: "A = A \ {x. P x} \ A \ -{x. P x}" "(A \ {x. P x}) \ (A \ -{x. P x}) = {}" by blast+ from fin have f: "finite (A \ {x. P x})" "finite (A \ -{x. P x})" by auto let ?g = "\x. if P x then h x else g x" from union_disjoint [OF f a(2), of ?g] a(1) show ?thesis by (subst (1 2) cong) simp_all qed lemma cartesian_product: "F (\x. F (g x) B) A = F (case_prod g) (A \ B)" proof (cases "A = {} \ B = {}") case True then show ?thesis by auto next case False then have "A \ {}" "B \ {}" by auto show ?thesis proof (cases "finite A \ finite B") case True then show ?thesis by (simp add: Sigma) next case False then consider "infinite A" | "infinite B" by auto then have "infinite (A \ B)" by cases (use \A \ {}\ \B \ {}\ in \auto dest: finite_cartesian_productD1 finite_cartesian_productD2\) then show ?thesis using False by auto qed qed lemma inter_restrict: assumes "finite A" shows "F g (A \ B) = F (\x. if x \ B then g x else \<^bold>1) A" proof - let ?g = "\x. if x \ A \ B then g x else \<^bold>1" have "\i\A - A \ B. (if i \ A \ B then g i else \<^bold>1) = \<^bold>1" by simp moreover have "A \ B \ A" by blast ultimately have "F ?g (A \ B) = F ?g A" using \finite A\ by (intro mono_neutral_left) auto then show ?thesis by simp qed lemma inter_filter: "finite A \ F g {x \ A. P x} = F (\x. if P x then g x else \<^bold>1) A" by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def) lemma Union_comp: assumes "\A \ B. finite A" and "\A1 A2 x. A1 \ B \ A2 \ B \ A1 \ A2 \ x \ A1 \ x \ A2 \ g x = \<^bold>1" shows "F g (\B) = (F \ F) g B" using assms proof (induct B rule: infinite_finite_induct) case (infinite A) then have "\ finite (\A)" by (blast dest: finite_UnionD) with infinite show ?case by simp next case empty then show ?case by simp next case (insert A B) then have "finite A" "finite B" "finite (\B)" "A \ B" and "\x\A \ \B. g x = \<^bold>1" and H: "F g (\B) = (F \ F) g B" by auto then have "F g (A \ \B) = F g A \<^bold>* F g (\B)" by (simp add: union_inter_neutral) with \finite B\ \A \ B\ show ?case by (simp add: H) qed lemma swap: "F (\i. F (g i) B) A = F (\j. F (\i. g i j) A) B" unfolding cartesian_product by (rule reindex_bij_witness [where i = "\(i, j). (j, i)" and j = "\(i, j). (j, i)"]) auto lemma swap_restrict: "finite A \ finite B \ F (\x. F (g x) {y. y \ B \ R x y}) A = F (\y. F (\x. g x y) {x. x \ A \ R x y}) B" by (simp add: inter_filter) (rule swap) lemma image_gen: assumes fin: "finite S" shows "F h S = F (\y. F h {x. x \ S \ g x = y}) (g ` S)" proof - have "{y. y\ g`S \ g x = y} = {g x}" if "x \ S" for x using that by auto then have "F h S = F (\x. F (\y. h x) {y. y\ g`S \ g x = y}) S" by simp also have "\ = F (\y. F h {x. x \ S \ g x = y}) (g ` S)" by (rule swap_restrict [OF fin finite_imageI [OF fin]]) finally show ?thesis . qed lemma group: assumes fS: "finite S" and fT: "finite T" and fST: "g ` S \ T" shows "F (\y. F h {x. x \ S \ g x = y}) T = F h S" unfolding image_gen[OF fS, of h g] by (auto intro: neutral mono_neutral_right[OF fT fST]) lemma Plus: fixes A :: "'b set" and B :: "'c set" assumes fin: "finite A" "finite B" shows "F g (A <+> B) = F (g \ Inl) A \<^bold>* F (g \ Inr) B" proof - have "A <+> B = Inl ` A \ Inr ` B" by auto moreover from fin have "finite (Inl ` A)" "finite (Inr ` B)" by auto moreover have "Inl ` A \ Inr ` B = {}" by auto moreover have "inj_on Inl A" "inj_on Inr B" by (auto intro: inj_onI) ultimately show ?thesis using fin by (simp add: union_disjoint reindex) qed lemma same_carrier: assumes "finite C" assumes subset: "A \ C" "B \ C" assumes trivial: "\a. a \ C - A \ g a = \<^bold>1" "\b. b \ C - B \ h b = \<^bold>1" shows "F g A = F h B \ F g C = F h C" proof - have "finite A" and "finite B" and "finite (C - A)" and "finite (C - B)" using \finite C\ subset by (auto elim: finite_subset) from subset have [simp]: "A - (C - A) = A" by auto from subset have [simp]: "B - (C - B) = B" by auto from subset have "C = A \ (C - A)" by auto then have "F g C = F g (A \ (C - A))" by simp also have "\ = F g (A - (C - A)) \<^bold>* F g (C - A - A) \<^bold>* F g (A \ (C - A))" using \finite A\ \finite (C - A)\ by (simp only: union_diff2) finally have *: "F g C = F g A" using trivial by simp from subset have "C = B \ (C - B)" by auto then have "F h C = F h (B \ (C - B))" by simp also have "\ = F h (B - (C - B)) \<^bold>* F h (C - B - B) \<^bold>* F h (B \ (C - B))" using \finite B\ \finite (C - B)\ by (simp only: union_diff2) finally have "F h C = F h B" using trivial by simp with * show ?thesis by simp qed lemma same_carrierI: assumes "finite C" assumes subset: "A \ C" "B \ C" assumes trivial: "\a. a \ C - A \ g a = \<^bold>1" "\b. b \ C - B \ h b = \<^bold>1" assumes "F g C = F h C" shows "F g A = F h B" using assms same_carrier [of C A B] by simp lemma eq_general: assumes B: "\y. y \ B \ \!x. x \ A \ h x = y" and A: "\x. x \ A \ h x \ B \ \(h x) = \ x" shows "F \ A = F \ B" proof - have eq: "B = h ` A" by (auto dest: assms) have h: "inj_on h A" using assms by (blast intro: inj_onI) have "F \ A = F (\ \ h) A" using A by auto also have "\ = F \ B" by (simp add: eq reindex h) finally show ?thesis . qed lemma eq_general_inverses: assumes B: "\y. y \ B \ k y \ A \ h(k y) = y" and A: "\x. x \ A \ h x \ B \ k(h x) = x \ \(h x) = \ x" shows "F \ A = F \ B" by (rule eq_general [where h=h]) (force intro: dest: A B)+ subsubsection \HOL Light variant: sum/product indexed by the non-neutral subset\ text \NB only a subset of the properties above are proved\ definition G :: "['b \ 'a,'b set] \ 'a" where "G p I \ if finite {x \ I. p x \ \<^bold>1} then F p {x \ I. p x \ \<^bold>1} else \<^bold>1" lemma finite_Collect_op: shows "\finite {i \ I. x i \ \<^bold>1}; finite {i \ I. y i \ \<^bold>1}\ \ finite {i \ I. x i \<^bold>* y i \ \<^bold>1}" apply (rule finite_subset [where B = "{i \ I. x i \ \<^bold>1} \ {i \ I. y i \ \<^bold>1}"]) using left_neutral by force+ lemma empty' [simp]: "G p {} = \<^bold>1" by (auto simp: G_def) lemma eq_sum [simp]: "finite I \ G p I = F p I" by (auto simp: G_def intro: mono_neutral_cong_left) lemma insert' [simp]: assumes "finite {x \ I. p x \ \<^bold>1}" shows "G p (insert i I) = (if i \ I then G p I else p i \<^bold>* G p I)" proof - have "{x. x = i \ p x \ \<^bold>1 \ x \ I \ p x \ \<^bold>1} = (if p i = \<^bold>1 then {x \ I. p x \ \<^bold>1} else insert i {x \ I. p x \ \<^bold>1})" by auto then show ?thesis using assms by (simp add: G_def conj_disj_distribR insert_absorb) qed lemma distrib_triv': assumes "finite I" shows "G (\i. g i \<^bold>* h i) I = G g I \<^bold>* G h I" by (simp add: assms local.distrib) lemma non_neutral': "G g {x \ I. g x \ \<^bold>1} = G g I" by (simp add: G_def) lemma distrib': assumes "finite {x \ I. g x \ \<^bold>1}" "finite {x \ I. h x \ \<^bold>1}" shows "G (\i. g i \<^bold>* h i) I = G g I \<^bold>* G h I" proof - have "a \<^bold>* a \ a \ a \ \<^bold>1" for a by auto then have "G (\i. g i \<^bold>* h i) I = G (\i. g i \<^bold>* h i) ({i \ I. g i \ \<^bold>1} \ {i \ I. h i \ \<^bold>1})" using assms by (force simp: G_def finite_Collect_op intro!: mono_neutral_cong) also have "\ = G g I \<^bold>* G h I" proof - have "F g ({i \ I. g i \ \<^bold>1} \ {i \ I. h i \ \<^bold>1}) = G g I" "F h ({i \ I. g i \ \<^bold>1} \ {i \ I. h i \ \<^bold>1}) = G h I" by (auto simp: G_def assms intro: mono_neutral_right) then show ?thesis using assms by (simp add: distrib) qed finally show ?thesis . qed lemma cong': assumes "A = B" assumes g_h: "\x. x \ B \ g x = h x" shows "G g A = G h B" using assms by (auto simp: G_def cong: conj_cong intro: cong) lemma mono_neutral_cong_left': assumes "S \ T" and "\i. i \ T - S \ h i = \<^bold>1" and "\x. x \ S \ g x = h x" shows "G g S = G h T" proof - have *: "{x \ S. g x \ \<^bold>1} = {x \ T. h x \ \<^bold>1}" using assms by (metis DiffI subset_eq) then have "finite {x \ S. g x \ \<^bold>1} = finite {x \ T. h x \ \<^bold>1}" by simp then show ?thesis using assms by (auto simp add: G_def * intro: cong) qed lemma mono_neutral_cong_right': "S \ T \ \i \ T - S. g i = \<^bold>1 \ (\x. x \ S \ g x = h x) \ G g T = G h S" by (auto intro!: mono_neutral_cong_left' [symmetric]) lemma mono_neutral_left': "S \ T \ \i \ T - S. g i = \<^bold>1 \ G g S = G g T" by (blast intro: mono_neutral_cong_left') lemma mono_neutral_right': "S \ T \ \i \ T - S. g i = \<^bold>1 \ G g T = G g S" by (blast intro!: mono_neutral_left' [symmetric]) end subsection \Generalized summation over a set\ context comm_monoid_add begin sublocale sum: comm_monoid_set plus 0 defines sum = sum.F and sum' = sum.G .. abbreviation Sum ("\") where "\ \ sum (\x. x)" end text \Now: lots of fancy syntax. First, \<^term>\sum (\x. e) A\ is written \\x\A. e\.\ syntax (ASCII) "_sum" :: "pttrn \ 'a set \ 'b \ 'b::comm_monoid_add" ("(3SUM (_/:_)./ _)" [0, 51, 10] 10) syntax "_sum" :: "pttrn \ 'a set \ 'b \ 'b::comm_monoid_add" ("(2\(_/\_)./ _)" [0, 51, 10] 10) translations \ \Beware of argument permutation!\ "\i\A. b" \ "CONST sum (\i. b) A" text \Instead of \<^term>\\x\{x. P}. e\ we introduce the shorter \\x|P. e\.\ syntax (ASCII) "_qsum" :: "pttrn \ bool \ 'a \ 'a" ("(3SUM _ |/ _./ _)" [0, 0, 10] 10) syntax "_qsum" :: "pttrn \ bool \ 'a \ 'a" ("(2\_ | (_)./ _)" [0, 0, 10] 10) translations "\x|P. t" => "CONST sum (\x. t) {x. P}" print_translation \ let fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\Collect\, _) $ Abs (y, Ty, P)] = if x <> y then raise Match else let val x' = Syntax_Trans.mark_bound_body (x, Tx); val t' = subst_bound (x', t); val P' = subst_bound (x', P); in Syntax.const \<^syntax_const>\_qsum\ $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' end | sum_tr' _ = raise Match; in [(\<^const_syntax>\sum\, K sum_tr')] end \ subsubsection \Properties in more restricted classes of structures\ lemma sum_Un: "finite A \ finite B \ sum f (A \ B) = sum f A + sum f B - sum f (A \ B)" for f :: "'b \ 'a::ab_group_add" by (subst sum.union_inter [symmetric]) (auto simp add: algebra_simps) lemma sum_Un2: assumes "finite (A \ B)" shows "sum f (A \ B) = sum f (A - B) + sum f (B - A) + sum f (A \ B)" proof - have "A \ B = A - B \ (B - A) \ A \ B" by auto with assms show ?thesis by simp (subst sum.union_disjoint, auto)+ qed lemma sum_diff1: fixes f :: "'b \ 'a::ab_group_add" assumes "finite A" shows "sum f (A - {a}) = (if a \ A then sum f A - f a else sum f A)" using assms by induct (auto simp: insert_Diff_if) lemma sum_diff: fixes f :: "'b \ 'a::ab_group_add" assumes "finite A" "B \ A" shows "sum f (A - B) = sum f A - sum f B" proof - from assms(2,1) have "finite B" by (rule finite_subset) from this \B \ A\ show ?thesis proof induct case empty thus ?case by simp next case (insert x F) with \finite A\ \finite B\ show ?case by (simp add: Diff_insert[where a=x and B=F] sum_diff1 insert_absorb) qed qed lemma sum_diff1'_aux: fixes f :: "'a \ 'b::ab_group_add" assumes "finite F" "{i \ I. f i \ 0} \ F" shows "sum' f (I - {i}) = (if i \ I then sum' f I - f i else sum' f I)" using assms proof induct case (insert x F) have 1: "finite {x \ I. f x \ 0} \ finite {x \ I. x \ i \ f x \ 0}" by (erule rev_finite_subset) auto have 2: "finite {x \ I. x \ i \ f x \ 0} \ finite {x \ I. f x \ 0}" apply (drule finite_insert [THEN iffD2]) by (erule rev_finite_subset) auto have 3: "finite {i \ I. f i \ 0}" using finite_subset insert by blast show ?case using insert sum_diff1 [of "{i \ I. f i \ 0}" f i] by (auto simp: sum.G_def 1 2 3 set_diff_eq conj_ac) qed (simp add: sum.G_def) lemma sum_diff1': fixes f :: "'a \ 'b::ab_group_add" assumes "finite {i \ I. f i \ 0}" shows "sum' f (I - {i}) = (if i \ I then sum' f I - f i else sum' f I)" by (rule sum_diff1'_aux [OF assms order_refl]) lemma (in ordered_comm_monoid_add) sum_mono: "(\i. i\K \ f i \ g i) \ (\i\K. f i) \ (\i\K. g i)" by (induct K rule: infinite_finite_induct) (use add_mono in auto) lemma (in strict_ordered_comm_monoid_add) sum_strict_mono: assumes "finite A" "A \ {}" and "\x. x \ A \ f x < g x" shows "sum f A < sum g A" using assms proof (induct rule: finite_ne_induct) case singleton then show ?case by simp next case insert then show ?case by (auto simp: add_strict_mono) qed lemma sum_strict_mono_ex1: fixes f g :: "'i \ 'a::ordered_cancel_comm_monoid_add" assumes "finite A" and "\x\A. f x \ g x" and "\a\A. f a < g a" shows "sum f A < sum g A" proof- from assms(3) obtain a where a: "a \ A" "f a < g a" by blast have "sum f A = sum f ((A - {a}) \ {a})" by(simp add: insert_absorb[OF \a \ A\]) also have "\ = sum f (A - {a}) + sum f {a}" using \finite A\ by(subst sum.union_disjoint) auto also have "sum f (A - {a}) \ sum g (A - {a})" by (rule sum_mono) (simp add: assms(2)) also from a have "sum f {a} < sum g {a}" by simp also have "sum g (A - {a}) + sum g {a} = sum g((A - {a}) \ {a})" using \finite A\ by (subst sum.union_disjoint[symmetric]) auto also have "\ = sum g A" by (simp add: insert_absorb[OF \a \ A\]) finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono) qed lemma sum_mono_inv: fixes f g :: "'i \ 'a :: ordered_cancel_comm_monoid_add" assumes eq: "sum f I = sum g I" assumes le: "\i. i \ I \ f i \ g i" assumes i: "i \ I" assumes I: "finite I" shows "f i = g i" proof (rule ccontr) assume "\ ?thesis" with le[OF i] have "f i < g i" by simp with i have "\i\I. f i < g i" .. from sum_strict_mono_ex1[OF I _ this] le have "sum f I < sum g I" by blast with eq show False by simp qed lemma member_le_sum: fixes f :: "_ \ 'b::{semiring_1, ordered_comm_monoid_add}" assumes "i \ A" and le: "\x. x \ A - {i} \ 0 \ f x" and "finite A" shows "f i \ sum f A" proof - have "f i \ sum f (A \ {i})" by (simp add: assms) also have "... = (\x\A. if x \ {i} then f x else 0)" using assms sum.inter_restrict by blast also have "... \ sum f A" apply (rule sum_mono) apply (auto simp: le) done finally show ?thesis . qed lemma sum_negf: "(\x\A. - f x) = - (\x\A. f x)" for f :: "'b \ 'a::ab_group_add" by (induct A rule: infinite_finite_induct) auto lemma sum_subtractf: "(\x\A. f x - g x) = (\x\A. f x) - (\x\A. g x)" for f g :: "'b \'a::ab_group_add" using sum.distrib [of f "- g" A] by (simp add: sum_negf) lemma sum_subtractf_nat: "(\x. x \ A \ g x \ f x) \ (\x\A. f x - g x) = (\x\A. f x) - (\x\A. g x)" for f g :: "'a \ nat" by (induct A rule: infinite_finite_induct) (auto simp: sum_mono) context ordered_comm_monoid_add begin lemma sum_nonneg: "(\x. x \ A \ 0 \ f x) \ 0 \ sum f A" proof (induct A rule: infinite_finite_induct) case infinite then show ?case by simp next case empty then show ?case by simp next case (insert x F) then have "0 + 0 \ f x + sum f F" by (blast intro: add_mono) with insert show ?case by simp qed lemma sum_nonpos: "(\x. x \ A \ f x \ 0) \ sum f A \ 0" proof (induct A rule: infinite_finite_induct) case infinite then show ?case by simp next case empty then show ?case by simp next case (insert x F) then have "f x + sum f F \ 0 + 0" by (blast intro: add_mono) with insert show ?case by simp qed lemma sum_nonneg_eq_0_iff: "finite A \ (\x. x \ A \ 0 \ f x) \ sum f A = 0 \ (\x\A. f x = 0)" by (induct set: finite) (simp_all add: add_nonneg_eq_0_iff sum_nonneg) lemma sum_nonneg_0: "finite s \ (\i. i \ s \ f i \ 0) \ (\ i \ s. f i) = 0 \ i \ s \ f i = 0" by (simp add: sum_nonneg_eq_0_iff) lemma sum_nonneg_leq_bound: assumes "finite s" "\i. i \ s \ f i \ 0" "(\i \ s. f i) = B" "i \ s" shows "f i \ B" proof - from assms have "f i \ f i + (\i \ s - {i}. f i)" by (intro add_increasing2 sum_nonneg) auto also have "\ = B" using sum.remove[of s i f] assms by simp finally show ?thesis by auto qed lemma sum_mono2: assumes fin: "finite B" and sub: "A \ B" and nn: "\b. b \ B-A \ 0 \ f b" shows "sum f A \ sum f B" proof - have "sum f A \ sum f A + sum f (B-A)" by (auto intro: add_increasing2 [OF sum_nonneg] nn) also from fin finite_subset[OF sub fin] have "\ = sum f (A \ (B-A))" by (simp add: sum.union_disjoint del: Un_Diff_cancel) also from sub have "A \ (B-A) = B" by blast finally show ?thesis . qed lemma sum_le_included: assumes "finite s" "finite t" and "\y\t. 0 \ g y" "(\x\s. \y\t. i y = x \ f x \ g y)" shows "sum f s \ sum g t" proof - have "sum f s \ sum (\y. sum g {x. x\t \ i x = y}) s" proof (rule sum_mono) fix y assume "y \ s" with assms obtain z where z: "z \ t" "y = i z" "f y \ g z" by auto with assms show "f y \ sum g {x \ t. i x = y}" (is "?A y \ ?B y") using order_trans[of "?A (i z)" "sum g {z}" "?B (i z)", intro] by (auto intro!: sum_mono2) qed also have "\ \ sum (\y. sum g {x. x\t \ i x = y}) (i ` t)" using assms(2-4) by (auto intro!: sum_mono2 sum_nonneg) also have "\ \ sum g t" using assms by (auto simp: sum.image_gen[symmetric]) finally show ?thesis . qed end lemma (in canonically_ordered_monoid_add) sum_eq_0_iff [simp]: "finite F \ (sum f F = 0) = (\a\F. f a = 0)" by (intro ballI sum_nonneg_eq_0_iff zero_le) context semiring_0 begin lemma sum_distrib_left: "r * sum f A = (\n\A. r * f n)" by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps) lemma sum_distrib_right: "sum f A * r = (\n\A. f n * r)" by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps) end lemma sum_divide_distrib: "sum f A / r = (\n\A. f n / r)" for r :: "'a::field" proof (induct A rule: infinite_finite_induct) case infinite then show ?case by simp next case empty then show ?case by simp next case insert then show ?case by (simp add: add_divide_distrib) qed lemma sum_abs[iff]: "\sum f A\ \ sum (\i. \f i\) A" for f :: "'a \ 'b::ordered_ab_group_add_abs" proof (induct A rule: infinite_finite_induct) case infinite then show ?case by simp next case empty then show ?case by simp next case insert then show ?case by (auto intro: abs_triangle_ineq order_trans) qed lemma sum_abs_ge_zero[iff]: "0 \ sum (\i. \f i\) A" for f :: "'a \ 'b::ordered_ab_group_add_abs" by (simp add: sum_nonneg) lemma abs_sum_abs[simp]: "\\a\A. \f a\\ = (\a\A. \f a\)" for f :: "'a \ 'b::ordered_ab_group_add_abs" proof (induct A rule: infinite_finite_induct) case infinite then show ?case by simp next case empty then show ?case by simp next case (insert a A) then have "\\a\insert a A. \f a\\ = \\f a\ + (\a\A. \f a\)\" by simp also from insert have "\ = \\f a\ + \\a\A. \f a\\\" by simp also have "\ = \f a\ + \\a\A. \f a\\" by (simp del: abs_of_nonneg) also from insert have "\ = (\a\insert a A. \f a\)" by simp finally show ?case . qed lemma sum_product: fixes f :: "'a \ 'b::semiring_0" shows "sum f A * sum g B = (\i\A. \j\B. f i * g j)" by (simp add: sum_distrib_left sum_distrib_right) (rule sum.swap) lemma sum_mult_sum_if_inj: fixes f :: "'a \ 'b::semiring_0" shows "inj_on (\(a, b). f a * g b) (A \ B) \ sum f A * sum g B = sum id {f a * g b |a b. a \ A \ b \ B}" by(auto simp: sum_product sum.cartesian_product intro!: sum.reindex_cong[symmetric]) lemma sum_SucD: "sum f A = Suc n \ \a\A. 0 < f a" by (induct A rule: infinite_finite_induct) auto lemma sum_eq_Suc0_iff: "finite A \ sum f A = Suc 0 \ (\a\A. f a = Suc 0 \ (\b\A. a \ b \ f b = 0))" by (induct A rule: finite_induct) (auto simp add: add_is_1) lemmas sum_eq_1_iff = sum_eq_Suc0_iff[simplified One_nat_def[symmetric]] lemma sum_Un_nat: "finite A \ finite B \ sum f (A \ B) = sum f A + sum f B - sum f (A \ B)" for f :: "'a \ nat" \ \For the natural numbers, we have subtraction.\ by (subst sum.union_inter [symmetric]) (auto simp: algebra_simps) lemma sum_diff1_nat: "sum f (A - {a}) = (if a \ A then sum f A - f a else sum f A)" for f :: "'a \ nat" proof (induct A rule: infinite_finite_induct) case infinite then show ?case by simp next case empty then show ?case by simp next case insert then show ?case apply (auto simp: insert_Diff_if) apply (drule mk_disjoint_insert) apply auto done qed lemma sum_diff_nat: fixes f :: "'a \ nat" assumes "finite B" and "B \ A" shows "sum f (A - B) = sum f A - sum f B" using assms proof induct case empty then show ?case by simp next case (insert x F) note IH = \F \ A \ sum f (A - F) = sum f A - sum f F\ from \x \ F\ \insert x F \ A\ have "x \ A - F" by simp then have A: "sum f ((A - F) - {x}) = sum f (A - F) - f x" by (simp add: sum_diff1_nat) from \insert x F \ A\ have "F \ A" by simp with IH have "sum f (A - F) = sum f A - sum f F" by simp with A have B: "sum f ((A - F) - {x}) = sum f A - sum f F - f x" by simp from \x \ F\ have "A - insert x F = (A - F) - {x}" by auto with B have C: "sum f (A - insert x F) = sum f A - sum f F - f x" by simp from \finite F\ \x \ F\ have "sum f (insert x F) = sum f F + f x" by simp with C have "sum f (A - insert x F) = sum f A - sum f (insert x F)" by simp then show ?case by simp qed lemma sum_comp_morphism: "h 0 = 0 \ (\x y. h (x + y) = h x + h y) \ sum (h \ g) A = h (sum g A)" by (induct A rule: infinite_finite_induct) simp_all lemma (in comm_semiring_1) dvd_sum: "(\a. a \ A \ d dvd f a) \ d dvd sum f A" by (induct A rule: infinite_finite_induct) simp_all lemma (in ordered_comm_monoid_add) sum_pos: "finite I \ I \ {} \ (\i. i \ I \ 0 < f i) \ 0 < sum f I" by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos) lemma (in ordered_comm_monoid_add) sum_pos2: assumes I: "finite I" "i \ I" "0 < f i" "\i. i \ I \ 0 \ f i" shows "0 < sum f I" proof - have "0 < f i + sum f (I - {i})" using assms by (intro add_pos_nonneg sum_nonneg) auto also have "\ = sum f I" using assms by (simp add: sum.remove) finally show ?thesis . qed lemma sum_strict_mono2: fixes f :: "'a \ 'b::ordered_cancel_comm_monoid_add" assumes "finite B" "A \ B" "b \ B-A" "f b > 0" and "\x. x \ B \ f x \ 0" shows "sum f A < sum f B" proof - have "B - A \ {}" using assms(3) by blast have "sum f (B-A) > 0" by (rule sum_pos2) (use assms in auto) moreover have "sum f B = sum f (B-A) + sum f A" by (rule sum.subset_diff) (use assms in auto) ultimately show ?thesis using add_strict_increasing by auto qed lemma sum_cong_Suc: assumes "0 \ A" "\x. Suc x \ A \ f (Suc x) = g (Suc x)" shows "sum f A = sum g A" proof (rule sum.cong) fix x assume "x \ A" with assms(1) show "f x = g x" by (cases x) (auto intro!: assms(2)) qed simp_all subsubsection \Cardinality as special case of \<^const>\sum\\ lemma card_eq_sum: "card A = sum (\x. 1) A" proof - have "plus \ (\_. Suc 0) = (\_. Suc)" by (simp add: fun_eq_iff) then have "Finite_Set.fold (plus \ (\_. Suc 0)) = Finite_Set.fold (\_. Suc)" by (rule arg_cong) then have "Finite_Set.fold (plus \ (\_. Suc 0)) 0 A = Finite_Set.fold (\_. Suc) 0 A" by (blast intro: fun_cong) then show ?thesis by (simp add: card.eq_fold sum.eq_fold) qed context semiring_1 begin lemma sum_constant [simp]: "(\x \ A. y) = of_nat (card A) * y" by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps) context fixes A assumes \finite A\ begin lemma sum_of_bool_eq [simp]: \(\x \ A. of_bool (P x)) = of_nat (card (A \ {x. P x}))\ if \finite A\ using \finite A\ by induction simp_all lemma sum_mult_of_bool_eq [simp]: \(\x \ A. f x * of_bool (P x)) = (\x \ (A \ {x. P x}). f x)\ by (rule sum.mono_neutral_cong) (use \finite A\ in auto) lemma sum_of_bool_mult_eq [simp]: \(\x \ A. of_bool (P x) * f x) = (\x \ (A \ {x. P x}). f x)\ by (rule sum.mono_neutral_cong) (use \finite A\ in auto) end end lemma sum_Suc: "sum (\x. Suc(f x)) A = sum f A + card A" using sum.distrib[of f "\_. 1" A] by simp lemma sum_bounded_above: fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}" assumes le: "\i. i\A \ f i \ K" shows "sum f A \ of_nat (card A) * K" proof (cases "finite A") case True then show ?thesis using le sum_mono[where K=A and g = "\x. K"] by simp next case False then show ?thesis by simp qed lemma sum_bounded_above_divide: fixes K :: "'a::linordered_field" assumes le: "\i. i\A \ f i \ K / of_nat (card A)" and fin: "finite A" "A \ {}" shows "sum f A \ K" using sum_bounded_above [of A f "K / of_nat (card A)", OF le] fin by simp lemma sum_bounded_above_strict: fixes K :: "'a::{ordered_cancel_comm_monoid_add,semiring_1}" assumes "\i. i\A \ f i < K" "card A > 0" shows "sum f A < of_nat (card A) * K" using assms sum_strict_mono[where A=A and g = "\x. K"] by (simp add: card_gt_0_iff) lemma sum_bounded_below: fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}" assumes le: "\i. i\A \ K \ f i" shows "of_nat (card A) * K \ sum f A" proof (cases "finite A") case True then show ?thesis using le sum_mono[where K=A and f = "\x. K"] by simp next case False then show ?thesis by simp qed lemma convex_sum_bound_le: fixes x :: "'a \ 'b::linordered_idom" assumes 0: "\i. i \ I \ 0 \ x i" and 1: "sum x I = 1" and \: "\i. i \ I \ \a i - b\ \ \" shows "\(\i\I. a i * x i) - b\ \ \" proof - have [simp]: "(\i\I. c * x i) = c" for c by (simp flip: sum_distrib_left 1) then have "\(\i\I. a i * x i) - b\ = \\i\I. (a i - b) * x i\" by (simp add: sum_subtractf left_diff_distrib) also have "\ \ (\i\I. \(a i - b) * x i\)" using abs_abs abs_of_nonneg by blast also have "\ \ (\i\I. \(a i - b)\ * x i)" by (simp add: abs_mult 0) also have "\ \ (\i\I. \ * x i)" by (rule sum_mono) (use \ "0" mult_right_mono in blast) also have "\ = \" by simp finally show ?thesis . qed lemma card_UN_disjoint: assumes "finite I" and "\i\I. finite (A i)" and "\i\I. \j\I. i \ j \ A i \ A j = {}" shows "card (\(A ` I)) = (\i\I. card(A i))" proof - have "(\i\I. card (A i)) = (\i\I. \x\A i. 1)" by simp with assms show ?thesis by (simp add: card_eq_sum sum.UNION_disjoint del: sum_constant) qed lemma card_Union_disjoint: assumes "pairwise disjnt C" and fin: "\A. A \ C \ finite A" shows "card (\C) = sum card C" proof (cases "finite C") case True then show ?thesis using card_UN_disjoint [OF True, of "\x. x"] assms by (simp add: disjnt_def fin pairwise_def) next case False then show ?thesis using assms card_eq_0_iff finite_UnionD by fastforce qed lemma card_Union_le_sum_card: fixes U :: "'a set set" assumes "\u \ U. finite u" shows "card (\U) \ sum card U" proof (cases "finite U") case False then show "card (\U) \ sum card U" using card_eq_0_iff finite_UnionD by auto next case True then show "card (\U) \ sum card U" proof (induct U rule: finite_induct) case empty then show ?case by auto next case (insert x F) then have "card(\(insert x F)) \ card(x) + card (\F)" using card_Un_le by auto also have "... \ card(x) + sum card F" using insert.hyps by auto also have "... = sum card (insert x F)" using sum.insert_if and insert.hyps by auto finally show ?case . qed qed lemma card_UN_le: assumes "finite I" shows "card(\i\I. A i) \ (\i\I. card(A i))" using assms proof induction case (insert i I) then show ?case using card_Un_le nat_add_left_cancel_le by (force intro: order_trans) qed auto lemma sum_multicount_gen: assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)" shows "sum (\i. (card {j\t. R i j})) s = sum k t" (is "?l = ?r") proof- have "?l = sum (\i. sum (\x.1) {j\t. R i j}) s" by auto also have "\ = ?r" unfolding sum.swap_restrict [OF assms(1-2)] using assms(3) by auto finally show ?thesis . qed lemma sum_multicount: assumes "finite S" "finite T" "\j\T. (card {i\S. R i j} = k)" shows "sum (\i. card {j\T. R i j}) S = k * card T" (is "?l = ?r") proof- have "?l = sum (\i. k) T" by (rule sum_multicount_gen) (auto simp: assms) also have "\ = ?r" by (simp add: mult.commute) finally show ?thesis by auto qed lemma sum_card_image: assumes "finite A" assumes "pairwise (\s t. disjnt (f s) (f t)) A" shows "sum card (f ` A) = sum (\a. card (f a)) A" using assms proof (induct A) case (insert a A) show ?case proof cases assume "f a = {}" with insert show ?case by (subst sum.mono_neutral_right[where S="f ` A"]) (auto simp: pairwise_insert) next assume "f a \ {}" then have "sum card (insert (f a) (f ` A)) = card (f a) + sum card (f ` A)" using insert by (subst sum.insert) (auto simp: pairwise_insert) with insert show ?case by (simp add: pairwise_insert) qed qed simp subsubsection \Cardinality of products\ lemma card_SigmaI [simp]: "finite A \ \a\A. finite (B a) \ card (SIGMA x: A. B x) = (\a\A. card (B a))" by (simp add: card_eq_sum sum.Sigma del: sum_constant) (* lemma SigmaI_insert: "y \ A ==> (SIGMA x:(insert y A). B x) = (({y} \ (B y)) \ (SIGMA x: A. B x))" by auto *) lemma card_cartesian_product: "card (A \ B) = card A * card B" by (cases "finite A \ finite B") (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2) lemma card_cartesian_product_singleton: "card ({x} \ A) = card A" by (simp add: card_cartesian_product) subsection \Generalized product over a set\ context comm_monoid_mult begin sublocale prod: comm_monoid_set times 1 defines prod = prod.F and prod' = prod.G .. abbreviation Prod ("\_" [1000] 999) where "\A \ prod (\x. x) A" end syntax (ASCII) "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD (_/:_)./ _)" [0, 51, 10] 10) syntax "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\(_/\_)./ _)" [0, 51, 10] 10) translations \ \Beware of argument permutation!\ "\i\A. b" == "CONST prod (\i. b) A" text \Instead of \<^term>\\x\{x. P}. e\ we introduce the shorter \\x|P. e\.\ syntax (ASCII) "_qprod" :: "pttrn \ bool \ 'a \ 'a" ("(4PROD _ |/ _./ _)" [0, 0, 10] 10) syntax "_qprod" :: "pttrn \ bool \ 'a \ 'a" ("(2\_ | (_)./ _)" [0, 0, 10] 10) translations "\x|P. t" => "CONST prod (\x. t) {x. P}" context comm_monoid_mult begin lemma prod_dvd_prod: "(\a. a \ A \ f a dvd g a) \ prod f A dvd prod g A" proof (induct A rule: infinite_finite_induct) case infinite then show ?case by (auto intro: dvdI) next case empty then show ?case by (auto intro: dvdI) next case (insert a A) then have "f a dvd g a" and "prod f A dvd prod g A" by simp_all then obtain r s where "g a = f a * r" and "prod g A = prod f A * s" by (auto elim!: dvdE) then have "g a * prod g A = f a * prod f A * (r * s)" by (simp add: ac_simps) with insert.hyps show ?case by (auto intro: dvdI) qed lemma prod_dvd_prod_subset: "finite B \ A \ B \ prod f A dvd prod f B" by (auto simp add: prod.subset_diff ac_simps intro: dvdI) end subsubsection \Properties in more restricted classes of structures\ context linordered_nonzero_semiring begin lemma prod_ge_1: "(\x. x \ A \ 1 \ f x) \ 1 \ prod f A" proof (induct A rule: infinite_finite_induct) case infinite then show ?case by simp next case empty then show ?case by simp next case (insert x F) have "1 * 1 \ f x * prod f F" by (rule mult_mono') (use insert in auto) with insert show ?case by simp qed lemma prod_le_1: fixes f :: "'b \ 'a" assumes "\x. x \ A \ 0 \ f x \ f x \ 1" shows "prod f A \ 1" using assms proof (induct A rule: infinite_finite_induct) case infinite then show ?case by simp next case empty then show ?case by simp next case (insert x F) then show ?case by (force simp: mult.commute intro: dest: mult_le_one) qed end context comm_semiring_1 begin lemma dvd_prod_eqI [intro]: assumes "finite A" and "a \ A" and "b = f a" shows "b dvd prod f A" proof - from \finite A\ have "prod f (insert a (A - {a})) = f a * prod f (A - {a})" by (intro prod.insert) auto also from \a \ A\ have "insert a (A - {a}) = A" by blast finally have "prod f A = f a * prod f (A - {a})" . with \b = f a\ show ?thesis by simp qed lemma dvd_prodI [intro]: "finite A \ a \ A \ f a dvd prod f A" by auto lemma prod_zero: assumes "finite A" and "\a\A. f a = 0" shows "prod f A = 0" using assms proof (induct A) case empty then show ?case by simp next case (insert a A) then have "f a = 0 \ (\a\A. f a = 0)" by simp then have "f a * prod f A = 0" by rule (simp_all add: insert) with insert show ?case by simp qed lemma prod_dvd_prod_subset2: assumes "finite B" and "A \ B" and "\a. a \ A \ f a dvd g a" shows "prod f A dvd prod g B" proof - from assms have "prod f A dvd prod g A" by (auto intro: prod_dvd_prod) moreover from assms have "prod g A dvd prod g B" by (auto intro: prod_dvd_prod_subset) ultimately show ?thesis by (rule dvd_trans) qed end lemma (in semidom) prod_zero_iff [simp]: fixes f :: "'b \ 'a" assumes "finite A" shows "prod f A = 0 \ (\a\A. f a = 0)" using assms by (induct A) (auto simp: no_zero_divisors) lemma (in semidom_divide) prod_diff1: assumes "finite A" and "f a \ 0" shows "prod f (A - {a}) = (if a \ A then prod f A div f a else prod f A)" proof (cases "a \ A") case True then show ?thesis by simp next case False with assms show ?thesis proof induct case empty then show ?case by simp next case (insert b B) then show ?case proof (cases "a = b") case True with insert show ?thesis by simp next case False with insert have "a \ B" by simp define C where "C = B - {a}" with \finite B\ \a \ B\ have "B = insert a C" "finite C" "a \ C" by auto with insert show ?thesis by (auto simp add: insert_commute ac_simps) qed qed qed lemma sum_zero_power [simp]: "(\i\A. c i * 0^i) = (if finite A \ 0 \ A then c 0 else 0)" for c :: "nat \ 'a::division_ring" by (induct A rule: infinite_finite_induct) auto lemma sum_zero_power' [simp]: "(\i\A. c i * 0^i / d i) = (if finite A \ 0 \ A then c 0 / d 0 else 0)" for c :: "nat \ 'a::field" using sum_zero_power [of "\i. c i / d i" A] by auto lemma (in field) prod_inversef: "prod (inverse \ f) A = inverse (prod f A)" proof (cases "finite A") case True then show ?thesis by (induct A rule: finite_induct) simp_all next case False then show ?thesis by auto qed lemma (in field) prod_dividef: "(\x\A. f x / g x) = prod f A / prod g A" using prod_inversef [of g A] by (simp add: divide_inverse prod.distrib) lemma prod_Un: fixes f :: "'b \ 'a :: field" assumes "finite A" and "finite B" and "\x\A \ B. f x \ 0" shows "prod f (A \ B) = prod f A * prod f B / prod f (A \ B)" proof - from assms have "prod f A * prod f B = prod f (A \ B) * prod f (A \ B)" by (simp add: prod.union_inter [symmetric, of A B]) with assms show ?thesis by simp qed context linordered_semidom begin lemma prod_nonneg: "(\a\A. 0 \ f a) \ 0 \ prod f A" by (induct A rule: infinite_finite_induct) simp_all lemma prod_pos: "(\a\A. 0 < f a) \ 0 < prod f A" by (induct A rule: infinite_finite_induct) simp_all lemma prod_mono: "(\i. i \ A \ 0 \ f i \ f i \ g i) \ prod f A \ prod g A" by (induct A rule: infinite_finite_induct) (force intro!: prod_nonneg mult_mono)+ lemma prod_mono_strict: assumes "finite A" "\i. i \ A \ 0 \ f i \ f i < g i" "A \ {}" shows "prod f A < prod g A" using assms proof (induct A rule: finite_induct) case empty then show ?case by simp next case insert then show ?case by (force intro: mult_strict_mono' prod_nonneg) qed +lemma prod_le_power: + assumes A: "\i. i \ A \ 0 \ f i \ f i \ n" "card A \ k" and "n \ 1" + shows "prod f A \ n ^ k" + using A +proof (induction A arbitrary: k rule: infinite_finite_induct) + case (insert i A) + then obtain k' where k': "card A \ k'" "k = Suc k'" + using Suc_le_D by force + have "f i * prod f A \ n * n ^ k'" + using insert \n \ 1\ k' by (intro prod_nonneg mult_mono; force) + then show ?case + by (auto simp: \k = Suc k'\ insert.hyps) +qed (use \n \ 1\ in auto) + end lemma prod_mono2: fixes f :: "'a \ 'b :: linordered_idom" assumes fin: "finite B" and sub: "A \ B" and nn: "\b. b \ B-A \ 1 \ f b" and A: "\a. a \ A \ 0 \ f a" shows "prod f A \ prod f B" proof - have "prod f A \ prod f A * prod f (B-A)" by (metis prod_ge_1 A mult_le_cancel_left1 nn not_less prod_nonneg) also from fin finite_subset[OF sub fin] have "\ = prod f (A \ (B-A))" by (simp add: prod.union_disjoint del: Un_Diff_cancel) also from sub have "A \ (B-A) = B" by blast finally show ?thesis . qed lemma less_1_prod: fixes f :: "'a \ 'b::linordered_idom" shows "finite I \ I \ {} \ (\i. i \ I \ 1 < f i) \ 1 < prod f I" by (induct I rule: finite_ne_induct) (auto intro: less_1_mult) lemma less_1_prod2: fixes f :: "'a \ 'b::linordered_idom" assumes I: "finite I" "i \ I" "1 < f i" "\i. i \ I \ 1 \ f i" shows "1 < prod f I" proof - have "1 < f i * prod f (I - {i})" using assms by (meson DiffD1 leI less_1_mult less_le_trans mult_le_cancel_left1 prod_ge_1) also have "\ = prod f I" using assms by (simp add: prod.remove) finally show ?thesis . qed lemma (in linordered_field) abs_prod: "\prod f A\ = (\x\A. \f x\)" by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult) lemma prod_eq_1_iff [simp]: "finite A \ prod f A = 1 \ (\a\A. f a = 1)" for f :: "'a \ nat" by (induct A rule: finite_induct) simp_all lemma prod_pos_nat_iff [simp]: "finite A \ prod f A > 0 \ (\a\A. f a > 0)" for f :: "'a \ nat" using prod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero) lemma prod_constant [simp]: "(\x\ A. y) = y ^ card A" for y :: "'a::comm_monoid_mult" by (induct A rule: infinite_finite_induct) simp_all lemma prod_power_distrib: "prod f A ^ n = prod (\x. (f x) ^ n) A" for f :: "'a \ 'b::comm_semiring_1" by (induct A rule: infinite_finite_induct) (auto simp add: power_mult_distrib) lemma power_sum: "c ^ (\a\A. f a) = (\a\A. c ^ f a)" by (induct A rule: infinite_finite_induct) (simp_all add: power_add) lemma prod_gen_delta: fixes b :: "'b \ 'a::comm_monoid_mult" assumes fin: "finite S" shows "prod (\k. if k = a then b k else c) S = (if a \ S then b a * c ^ (card S - 1) else c ^ card S)" proof - let ?f = "(\k. if k=a then b k else c)" show ?thesis proof (cases "a \ S") case False then have "\ k\ S. ?f k = c" by simp with False show ?thesis by (simp add: prod_constant) next case True let ?A = "S - {a}" let ?B = "{a}" from True have eq: "S = ?A \ ?B" by blast have disjoint: "?A \ ?B = {}" by simp from fin have fin': "finite ?A" "finite ?B" by auto have f_A0: "prod ?f ?A = prod (\i. c) ?A" by (rule prod.cong) auto from fin True have card_A: "card ?A = card S - 1" by auto have f_A1: "prod ?f ?A = c ^ card ?A" unfolding f_A0 by (rule prod_constant) have "prod ?f ?A * prod ?f ?B = prod ?f S" using prod.union_disjoint[OF fin' disjoint, of ?f, unfolded eq[symmetric]] by simp with True card_A show ?thesis by (simp add: f_A1 field_simps cong add: prod.cong cong del: if_weak_cong) qed qed lemma sum_image_le: fixes g :: "'a \ 'b::ordered_comm_monoid_add" assumes "finite I" "\i. i \ I \ 0 \ g(f i)" shows "sum g (f ` I) \ sum (g \ f) I" using assms proof induction case empty then show ?case by auto next case (insert x F) from insertI1 have "0 \ g (f x)" by (rule insert) hence 1: "sum g (f ` F) \ g (f x) + sum g (f ` F)" using add_increasing by blast have 2: "sum g (f ` F) \ sum (g \ f) F" using insert by blast have "sum g (f ` insert x F) = sum g (insert (f x) (f ` F))" by simp also have "\ \ g (f x) + sum g (f ` F)" by (simp add: 1 insert sum.insert_if) also from 2 have "\ \ g (f x) + sum (g \ f) F" by (rule add_left_mono) also from insert(1, 2) have "\ = sum (g \ f) (insert x F)" by (simp add: sum.insert_if) finally show ?case . qed end diff --git a/src/HOL/Library/Countable_Set.thy b/src/HOL/Library/Countable_Set.thy --- a/src/HOL/Library/Countable_Set.thy +++ b/src/HOL/Library/Countable_Set.thy @@ -1,451 +1,470 @@ (* Title: HOL/Library/Countable_Set.thy Author: Johannes Hölzl Author: Andrei Popescu *) section \Countable sets\ theory Countable_Set imports Countable Infinite_Set begin subsection \Predicate for countable sets\ definition countable :: "'a set \ bool" where "countable S \ (\f::'a \ nat. inj_on f S)" lemma countableE: assumes S: "countable S" obtains f :: "'a \ nat" where "inj_on f S" using S by (auto simp: countable_def) lemma countableI: "inj_on (f::'a \ nat) S \ countable S" by (auto simp: countable_def) lemma countableI': "inj_on (f::'a \ 'b::countable) S \ countable S" using comp_inj_on[of f S to_nat] by (auto intro: countableI) lemma countableE_bij: assumes S: "countable S" obtains f :: "nat \ 'a" and C :: "nat set" where "bij_betw f C S" using S by (blast elim: countableE dest: inj_on_imp_bij_betw bij_betw_inv) lemma countableI_bij: "bij_betw f (C::nat set) S \ countable S" by (blast intro: countableI bij_betw_inv_into bij_betw_imp_inj_on) lemma countable_finite: "finite S \ countable S" by (blast dest: finite_imp_inj_to_nat_seg countableI) lemma countableI_bij1: "bij_betw f A B \ countable A \ countable B" by (blast elim: countableE_bij intro: bij_betw_trans countableI_bij) lemma countableI_bij2: "bij_betw f B A \ countable A \ countable B" by (blast elim: countableE_bij intro: bij_betw_trans bij_betw_inv_into countableI_bij) lemma countable_iff_bij[simp]: "bij_betw f A B \ countable A \ countable B" by (blast intro: countableI_bij1 countableI_bij2) lemma countable_subset: "A \ B \ countable B \ countable A" by (auto simp: countable_def intro: subset_inj_on) lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)" using countableI[of to_nat A] by auto subsection \Enumerate a countable set\ lemma countableE_infinite: assumes "countable S" "infinite S" obtains e :: "'a \ nat" where "bij_betw e S UNIV" proof - obtain f :: "'a \ nat" where "inj_on f S" using \countable S\ by (rule countableE) then have "bij_betw f S (f`S)" unfolding bij_betw_def by simp moreover from \inj_on f S\ \infinite S\ have inf_fS: "infinite (f`S)" by (auto dest: finite_imageD) then have "bij_betw (the_inv_into UNIV (enumerate (f`S))) (f`S) UNIV" by (intro bij_betw_the_inv_into bij_enumerate) ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) \ f) S UNIV" by (rule bij_betw_trans) then show thesis .. qed lemma countable_infiniteE': assumes "countable A" "infinite A" obtains g where "bij_betw g (UNIV :: nat set) A" using bij_betw_inv[OF countableE_infinite[OF assms]] that by blast lemma countable_enum_cases: assumes "countable S" obtains (finite) f :: "'a \ nat" where "finite S" "bij_betw f S {.. nat" where "infinite S" "bij_betw f S UNIV" using ex_bij_betw_finite_nat[of S] countableE_infinite \countable S\ by (cases "finite S") (auto simp add: atLeast0LessThan) definition to_nat_on :: "'a set \ 'a \ nat" where "to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)" definition from_nat_into :: "'a set \ nat \ 'a" where "from_nat_into S n = (if n \ to_nat_on S ` S then inv_into S (to_nat_on S) n else SOME s. s\S)" lemma to_nat_on_finite: "finite S \ bij_betw (to_nat_on S) S {..< card S}" using ex_bij_betw_finite_nat unfolding to_nat_on_def by (intro someI2_ex[where Q="\f. bij_betw f S {.. infinite S \ bij_betw (to_nat_on S) S UNIV" using countableE_infinite unfolding to_nat_on_def by (intro someI2_ex[where Q="\f. bij_betw f S UNIV"]) auto lemma bij_betw_from_nat_into_finite: "finite S \ bij_betw (from_nat_into S) {..< card S} S" unfolding from_nat_into_def[abs_def] using to_nat_on_finite[of S] apply (subst bij_betw_cong) apply (split if_split) apply (simp add: bij_betw_def) apply (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_finite) done lemma bij_betw_from_nat_into: "countable S \ infinite S \ bij_betw (from_nat_into S) UNIV S" unfolding from_nat_into_def[abs_def] using to_nat_on_infinite[of S, unfolded bij_betw_def] by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite) +text \ + The sum/product over the enumeration of a finite set equals simply the sum/product over the set +\ +context comm_monoid_set +begin + +lemma card_from_nat_into: + "F (\i. h (from_nat_into A i)) {..i. h (from_nat_into A i)) {.. 'a" where "A = range f" "inj f" by (metis bij_betw_def bij_betw_from_nat_into [OF assms]) lemma inj_on_to_nat_on[intro]: "countable A \ inj_on (to_nat_on A) A" using to_nat_on_infinite[of A] to_nat_on_finite[of A] by (cases "finite A") (auto simp: bij_betw_def) lemma to_nat_on_inj[simp]: "countable A \ a \ A \ b \ A \ to_nat_on A a = to_nat_on A b \ a = b" using inj_on_to_nat_on[of A] by (auto dest: inj_onD) lemma from_nat_into_to_nat_on[simp]: "countable A \ a \ A \ from_nat_into A (to_nat_on A a) = a" by (auto simp: from_nat_into_def intro!: inv_into_f_f) lemma subset_range_from_nat_into: "countable A \ A \ range (from_nat_into A)" by (auto intro: from_nat_into_to_nat_on[symmetric]) lemma from_nat_into: "A \ {} \ from_nat_into A n \ A" unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex) lemma range_from_nat_into_subset: "A \ {} \ range (from_nat_into A) \ A" using from_nat_into[of A] by auto lemma range_from_nat_into[simp]: "A \ {} \ countable A \ range (from_nat_into A) = A" by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into) lemma image_to_nat_on: "countable A \ infinite A \ to_nat_on A ` A = UNIV" using to_nat_on_infinite[of A] by (simp add: bij_betw_def) lemma to_nat_on_surj: "countable A \ infinite A \ \a\A. to_nat_on A a = n" by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on) lemma to_nat_on_from_nat_into[simp]: "n \ to_nat_on A ` A \ to_nat_on A (from_nat_into A n) = n" by (simp add: f_inv_into_f from_nat_into_def) lemma to_nat_on_from_nat_into_infinite[simp]: "countable A \ infinite A \ to_nat_on A (from_nat_into A n) = n" by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into) lemma from_nat_into_inj: "countable A \ m \ to_nat_on A ` A \ n \ to_nat_on A ` A \ from_nat_into A m = from_nat_into A n \ m = n" by (subst to_nat_on_inj[symmetric, of A]) auto lemma from_nat_into_inj_infinite[simp]: "countable A \ infinite A \ from_nat_into A m = from_nat_into A n \ m = n" using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp lemma eq_from_nat_into_iff: "countable A \ x \ A \ i \ to_nat_on A ` A \ x = from_nat_into A i \ i = to_nat_on A x" by auto lemma from_nat_into_surj: "countable A \ a \ A \ \n. from_nat_into A n = a" by (rule exI[of _ "to_nat_on A a"]) simp lemma from_nat_into_inject[simp]: "A \ {} \ countable A \ B \ {} \ countable B \ from_nat_into A = from_nat_into B \ A = B" by (metis range_from_nat_into) lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \ {} \ countable A})" unfolding inj_on_def by auto subsection \Closure properties of countability\ lemma countable_SIGMA[intro, simp]: "countable I \ (\i. i \ I \ countable (A i)) \ countable (SIGMA i : I. A i)" by (intro countableI'[of "\(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def) lemma countable_image[intro, simp]: assumes "countable A" shows "countable (f`A)" proof - obtain g :: "'a \ nat" where "inj_on g A" using assms by (rule countableE) moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \ A" by (auto intro: inj_on_inv_into inv_into_into) ultimately show ?thesis by (blast dest: comp_inj_on subset_inj_on intro: countableI) qed lemma countable_image_inj_on: "countable (f ` A) \ inj_on f A \ countable A" by (metis countable_image the_inv_into_onto) lemma countable_image_inj_Int_vimage: "\inj_on f S; countable A\ \ countable (S \ f -` A)" by (meson countable_image_inj_on countable_subset image_subset_iff_subset_vimage inf_le2 inj_on_Int) lemma countable_image_inj_gen: "\inj_on f S; countable A\ \ countable {x \ S. f x \ A}" using countable_image_inj_Int_vimage by (auto simp: vimage_def Collect_conj_eq) lemma countable_image_inj_eq: "inj_on f S \ countable(f ` S) \ countable S" using countable_image_inj_on by blast lemma countable_image_inj: "\countable A; inj f\ \ countable {x. f x \ A}" by (metis (mono_tags, lifting) countable_image_inj_eq countable_subset image_Collect_subsetI inj_on_inverseI the_inv_f_f) lemma countable_UN[intro, simp]: fixes I :: "'i set" and A :: "'i => 'a set" assumes I: "countable I" assumes A: "\i. i \ I \ countable (A i)" shows "countable (\i\I. A i)" proof - have "(\i\I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff) then show ?thesis by (simp add: assms) qed lemma countable_Un[intro]: "countable A \ countable B \ countable (A \ B)" by (rule countable_UN[of "{True, False}" "\True \ A | False \ B", simplified]) (simp split: bool.split) lemma countable_Un_iff[simp]: "countable (A \ B) \ countable A \ countable B" by (metis countable_Un countable_subset inf_sup_ord(3,4)) lemma countable_Plus[intro, simp]: "countable A \ countable B \ countable (A <+> B)" by (simp add: Plus_def) lemma countable_empty[intro, simp]: "countable {}" by (blast intro: countable_finite) lemma countable_insert[intro, simp]: "countable A \ countable (insert a A)" using countable_Un[of "{a}" A] by (auto simp: countable_finite) lemma countable_Int1[intro, simp]: "countable A \ countable (A \ B)" by (force intro: countable_subset) lemma countable_Int2[intro, simp]: "countable B \ countable (A \ B)" by (blast intro: countable_subset) lemma countable_INT[intro, simp]: "i \ I \ countable (A i) \ countable (\i\I. A i)" by (blast intro: countable_subset) lemma countable_Diff[intro, simp]: "countable A \ countable (A - B)" by (blast intro: countable_subset) lemma countable_insert_eq [simp]: "countable (insert x A) = countable A" by auto (metis Diff_insert_absorb countable_Diff insert_absorb) lemma countable_vimage: "B \ range f \ countable (f -` B) \ countable B" by (metis Int_absorb2 countable_image image_vimage_eq) lemma surj_countable_vimage: "surj f \ countable (f -` B) \ countable B" by (metis countable_vimage top_greatest) lemma countable_Collect[simp]: "countable A \ countable {a \ A. \ a}" by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1) lemma countable_Image: assumes "\y. y \ Y \ countable (X `` {y})" assumes "countable Y" shows "countable (X `` Y)" proof - have "countable (X `` (\y\Y. {y}))" unfolding Image_UN by (intro countable_UN assms) then show ?thesis by simp qed lemma countable_relpow: fixes X :: "'a rel" assumes Image_X: "\Y. countable Y \ countable (X `` Y)" assumes Y: "countable Y" shows "countable ((X ^^ i) `` Y)" using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X) lemma countable_funpow: fixes f :: "'a set \ 'a set" assumes "\A. countable A \ countable (f A)" and "countable A" shows "countable ((f ^^ n) A)" by(induction n)(simp_all add: assms) lemma countable_rtrancl: "(\Y. countable Y \ countable (X `` Y)) \ countable Y \ countable (X\<^sup>* `` Y)" unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow) lemma countable_lists[intro, simp]: assumes A: "countable A" shows "countable (lists A)" proof - have "countable (lists (range (from_nat_into A)))" by (auto simp: lists_image) with A show ?thesis by (auto dest: subset_range_from_nat_into countable_subset lists_mono) qed lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV" using finite_list by auto lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\bool))" by (simp add: Collect_finite_eq_lists) lemma countable_int: "countable \" unfolding Ints_def by auto lemma countable_rat: "countable \" unfolding Rats_def by auto lemma Collect_finite_subset_eq_lists: "{A. finite A \ A \ T} = set ` lists T" using finite_list by (auto simp: lists_eq_set) lemma countable_Collect_finite_subset: "countable T \ countable {A. finite A \ A \ T}" unfolding Collect_finite_subset_eq_lists by auto lemma countable_Fpow: "countable S \ countable (Fpow S)" using countable_Collect_finite_subset by (force simp add: Fpow_def conj_commute) lemma countable_set_option [simp]: "countable (set_option x)" by (cases x) auto subsection \Misc lemmas\ lemma countable_subset_image: "countable B \ B \ (f ` A) \ (\A'. countable A' \ A' \ A \ (B = f ` A'))" (is "?lhs = ?rhs") proof assume ?lhs show ?rhs by (rule exI [where x="inv_into A f ` B"]) (use \?lhs\ in \auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into\) next assume ?rhs then show ?lhs by force qed lemma ex_subset_image_inj: "(\T. T \ f ` S \ P T) \ (\T. T \ S \ inj_on f T \ P (f ` T))" by (auto simp: subset_image_inj) lemma all_subset_image_inj: "(\T. T \ f ` S \ P T) \ (\T. T \ S \ inj_on f T \ P(f ` T))" by (metis subset_image_inj) lemma ex_countable_subset_image_inj: "(\T. countable T \ T \ f ` S \ P T) \ (\T. countable T \ T \ S \ inj_on f T \ P (f ` T))" by (metis countable_image_inj_eq subset_image_inj) lemma all_countable_subset_image_inj: "(\T. countable T \ T \ f ` S \ P T) \ (\T. countable T \ T \ S \ inj_on f T \P(f ` T))" by (metis countable_image_inj_eq subset_image_inj) lemma ex_countable_subset_image: "(\T. countable T \ T \ f ` S \ P T) \ (\T. countable T \ T \ S \ P (f ` T))" by (metis countable_subset_image) lemma all_countable_subset_image: "(\T. countable T \ T \ f ` S \ P T) \ (\T. countable T \ T \ S \ P(f ` T))" by (metis countable_subset_image) lemma countable_image_eq: "countable(f ` S) \ (\T. countable T \ T \ S \ f ` S = f ` T)" by (metis countable_image countable_image_inj_eq order_refl subset_image_inj) lemma countable_image_eq_inj: "countable(f ` S) \ (\T. countable T \ T \ S \ f ` S = f ` T \ inj_on f T)" by (metis countable_image_inj_eq order_refl subset_image_inj) lemma infinite_countable_subset': assumes X: "infinite X" shows "\C\X. countable C \ infinite C" proof - obtain f :: "nat \ 'a" where "inj f" "range f \ X" using infinite_countable_subset [OF X] by blast then show ?thesis by (intro exI[of _ "range f"]) (auto simp: range_inj_infinite) qed lemma countable_all: assumes S: "countable S" shows "(\s\S. P s) \ (\n::nat. from_nat_into S n \ S \ P (from_nat_into S n))" using S[THEN subset_range_from_nat_into] by auto lemma finite_sequence_to_countable_set: assumes "countable X" obtains F where "\i. F i \ X" "\i. F i \ F (Suc i)" "\i. finite (F i)" "(\i. F i) = X" proof - show thesis apply (rule that[of "\i. if X = {} then {} else from_nat_into X ` {..i}"]) apply (auto simp add: image_iff intro: from_nat_into split: if_splits) using assms from_nat_into_surj by (fastforce cong: image_cong) qed lemma transfer_countable[transfer_rule]: "bi_unique R \ rel_fun (rel_set R) (=) countable countable" by (rule rel_funI, erule (1) bi_unique_rel_set_lemma) (auto dest: countable_image_inj_on) subsection \Uncountable\ abbreviation uncountable where "uncountable A \ \ countable A" lemma uncountable_def: "uncountable A \ A \ {} \ \ (\f::(nat \ 'a). range f = A)" by (auto intro: inj_on_inv_into simp: countable_def) (metis all_not_in_conv inj_on_iff_surj subset_UNIV) lemma uncountable_bij_betw: "bij_betw f A B \ uncountable B \ uncountable A" unfolding bij_betw_def by (metis countable_image) lemma uncountable_infinite: "uncountable A \ infinite A" by (metis countable_finite) lemma uncountable_minus_countable: "uncountable A \ countable B \ uncountable (A - B)" using countable_Un[of B "A - B"] by auto lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A" by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable) text \Every infinite set can be covered by a pairwise disjoint family of infinite sets. This version doesn't achieve equality, as it only covers a countable subset\ lemma infinite_infinite_partition: assumes "infinite A" obtains C :: "nat \ 'a set" where "pairwise (\i j. disjnt (C i) (C j)) UNIV" "(\i. C i) \ A" "\i. infinite (C i)" proof - obtain f :: "nat\'a" where "range f \ A" "inj f" using assms infinite_countable_subset by blast let ?C = "\i. range (\j. f (prod_encode (i,j)))" show thesis proof show "pairwise (\i j. disjnt (?C i) (?C j)) UNIV" by (auto simp: pairwise_def disjnt_def inj_on_eq_iff [OF \inj f\] inj_on_eq_iff [OF inj_prod_encode, of _ UNIV]) show "(\i. ?C i) \ A" using \range f \ A\ by blast have "infinite (range (\j. f (prod_encode (i, j))))" for i by (rule range_inj_infinite) (meson Pair_inject \inj f\ inj_def prod_encode_eq) then show "\i. infinite (?C i)" using that by auto qed qed end diff --git a/src/HOL/Library/Disjoint_Sets.thy b/src/HOL/Library/Disjoint_Sets.thy --- a/src/HOL/Library/Disjoint_Sets.thy +++ b/src/HOL/Library/Disjoint_Sets.thy @@ -1,415 +1,453 @@ (* Author: Johannes Hölzl, TU München *) section \Partitions and Disjoint Sets\ theory Disjoint_Sets imports Main begin lemma range_subsetD: "range f \ B \ f i \ B" by blast lemma Int_Diff_disjoint: "A \ B \ (A - B) = {}" by blast lemma Int_Diff_Un: "A \ B \ (A - B) = A" by blast lemma mono_Un: "mono A \ (\i\n. A i) = A n" unfolding mono_def by auto lemma disjnt_equiv_class: "equiv A r \ disjnt (r``{a}) (r``{b}) \ (a, b) \ r" by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def) subsection \Set of Disjoint Sets\ abbreviation disjoint :: "'a set set \ bool" where "disjoint \ pairwise disjnt" lemma disjoint_def: "disjoint A \ (\a\A. \b\A. a \ b \ a \ b = {})" unfolding pairwise_def disjnt_def by auto lemma disjointI: "(\a b. a \ A \ b \ A \ a \ b \ a \ b = {}) \ disjoint A" unfolding disjoint_def by auto lemma disjointD: "disjoint A \ a \ A \ b \ A \ a \ b \ a \ b = {}" unfolding disjoint_def by auto lemma disjoint_image: "inj_on f (\A) \ disjoint A \ disjoint ((`) f ` A)" unfolding inj_on_def disjoint_def by blast lemma assumes "disjoint (A \ B)" shows disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B" using assms by (simp_all add: disjoint_def) lemma disjoint_INT: assumes *: "\i. i \ I \ disjoint (F i)" shows "disjoint {\i\I. X i | X. \i\I. X i \ F i}" proof (safe intro!: disjointI del: equalityI) fix A B :: "'a \ 'b set" assume "(\i\I. A i) \ (\i\I. B i)" then obtain i where "A i \ B i" "i \ I" by auto moreover assume "\i\I. A i \ F i" "\i\I. B i \ F i" ultimately show "(\i\I. A i) \ (\i\I. B i) = {}" using *[OF \i\I\, THEN disjointD, of "A i" "B i"] by (auto simp flip: INT_Int_distrib) qed lemma diff_Union_pairwise_disjoint: assumes "pairwise disjnt \" "\ \ \" shows "\\ - \\ = \(\ - \)" proof - have "False" if x: "x \ A" "x \ B" and AB: "A \ \" "A \ \" "B \ \" for x A B proof - have "A \ B = {}" using assms disjointD AB by blast with x show ?thesis by blast qed then show ?thesis by auto qed lemma Int_Union_pairwise_disjoint: assumes "pairwise disjnt (\ \ \)" shows "\\ \ \\ = \(\ \ \)" proof - have "False" if x: "x \ A" "x \ B" and AB: "A \ \" "A \ \" "B \ \" for x A B proof - have "A \ B = {}" using assms disjointD AB by blast with x show ?thesis by blast qed then show ?thesis by auto qed lemma psubset_Union_pairwise_disjoint: assumes \: "pairwise disjnt \" and "\ \ \ - {{}}" shows "\\ \ \\" unfolding psubset_eq proof show "\\ \ \\" using assms by blast have "\ \ \" "\(\ - \ \ (\ - {{}})) \ {}" using assms by blast+ then show "\\ \ \\" using diff_Union_pairwise_disjoint [OF \] by blast qed subsubsection "Family of Disjoint Sets" definition disjoint_family_on :: "('i \ 'a set) \ 'i set \ bool" where "disjoint_family_on A S \ (\m\S. \n\S. m \ n \ A m \ A n = {})" abbreviation "disjoint_family A \ disjoint_family_on A UNIV" lemma disjoint_family_elem_disjnt: assumes "infinite A" "finite C" and df: "disjoint_family_on B A" obtains x where "x \ A" "disjnt C (B x)" proof - have "False" if *: "\x \ A. \y. y \ C \ y \ B x" proof - obtain g where g: "\x \ A. g x \ C \ g x \ B x" using * by metis with df have "inj_on g A" by (fastforce simp add: inj_on_def disjoint_family_on_def) then have "infinite (g ` A)" using \infinite A\ finite_image_iff by blast then show False by (meson \finite C\ finite_subset g image_subset_iff) qed then show ?thesis by (force simp: disjnt_iff intro: that) qed lemma disjoint_family_onD: "disjoint_family_on A I \ i \ I \ j \ I \ i \ j \ A i \ A j = {}" by (auto simp: disjoint_family_on_def) lemma disjoint_family_subset: "disjoint_family A \ (\x. B x \ A x) \ disjoint_family B" by (force simp add: disjoint_family_on_def) lemma disjoint_family_on_bisimulation: assumes "disjoint_family_on f S" and "\n m. n \ S \ m \ S \ n \ m \ f n \ f m = {} \ g n \ g m = {}" shows "disjoint_family_on g S" using assms unfolding disjoint_family_on_def by auto lemma disjoint_family_on_mono: "A \ B \ disjoint_family_on f B \ disjoint_family_on f A" unfolding disjoint_family_on_def by auto lemma disjoint_family_Suc: "(\n. A n \ A (Suc n)) \ disjoint_family (\i. A (Suc i) - A i)" using lift_Suc_mono_le[of A] by (auto simp add: disjoint_family_on_def) (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le) lemma disjoint_family_on_disjoint_image: "disjoint_family_on A I \ disjoint (A ` I)" unfolding disjoint_family_on_def disjoint_def by force lemma disjoint_family_on_vimageI: "disjoint_family_on F I \ disjoint_family_on (\i. f -` F i) I" by (auto simp: disjoint_family_on_def) lemma disjoint_image_disjoint_family_on: assumes d: "disjoint (A ` I)" and i: "inj_on A I" shows "disjoint_family_on A I" unfolding disjoint_family_on_def proof (intro ballI impI) fix n m assume nm: "m \ I" "n \ I" and "n \ m" with i[THEN inj_onD, of n m] show "A n \ A m = {}" by (intro disjointD[OF d]) auto qed +lemma disjoint_family_on_iff_disjoint_image: + assumes "\i. i \ I \ A i \ {}" + shows "disjoint_family_on A I \ disjoint (A ` I) \ inj_on A I" +proof + assume "disjoint_family_on A I" + then show "disjoint (A ` I) \ inj_on A I" + by (metis (mono_tags, lifting) assms disjoint_family_onD disjoint_family_on_disjoint_image inf.idem inj_onI) +qed (use disjoint_image_disjoint_family_on in metis) + +lemma card_UN_disjoint': + assumes "disjoint_family_on A I" "\i. i \ I \ finite (A i)" "finite I" + shows "card (\i\I. A i) = (\i\I. card (A i))" + using assms by (simp add: card_UN_disjoint disjoint_family_on_def) + lemma disjoint_UN: assumes F: "\i. i \ I \ disjoint (F i)" and *: "disjoint_family_on (\i. \(F i)) I" shows "disjoint (\i\I. F i)" proof (safe intro!: disjointI del: equalityI) fix A B i j assume "A \ B" "A \ F i" "i \ I" "B \ F j" "j \ I" show "A \ B = {}" proof cases assume "i = j" with F[of i] \i \ I\ \A \ F i\ \B \ F j\ \A \ B\ show "A \ B = {}" by (auto dest: disjointD) next assume "i \ j" with * \i\I\ \j\I\ have "(\(F i)) \ (\(F j)) = {}" by (rule disjoint_family_onD) with \A\F i\ \i\I\ \B\F j\ \j\I\ show "A \ B = {}" by auto qed qed lemma distinct_list_bind: assumes "distinct xs" "\x. x \ set xs \ distinct (f x)" "disjoint_family_on (set \ f) (set xs)" shows "distinct (List.bind xs f)" using assms by (induction xs) (auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind) lemma bij_betw_UNION_disjoint: assumes disj: "disjoint_family_on A' I" assumes bij: "\i. i \ I \ bij_betw f (A i) (A' i)" shows "bij_betw f (\i\I. A i) (\i\I. A' i)" unfolding bij_betw_def proof from bij show eq: "f ` \(A ` I) = \(A' ` I)" by (auto simp: bij_betw_def image_UN) show "inj_on f (\(A ` I))" proof (rule inj_onI, clarify) fix i j x y assume A: "i \ I" "j \ I" "x \ A i" "y \ A j" and B: "f x = f y" from A bij[of i] bij[of j] have "f x \ A' i" "f y \ A' j" by (auto simp: bij_betw_def) with B have "A' i \ A' j \ {}" by auto with disj A have "i = j" unfolding disjoint_family_on_def by blast with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD) qed qed lemma disjoint_union: "disjoint C \ disjoint B \ \C \ \B = {} \ disjoint (C \ B)" using disjoint_UN[of "{C, B}" "\x. x"] by (auto simp add: disjoint_family_on_def) text \ + Sum/product of the union of a finite disjoint family +\ +context comm_monoid_set +begin + +lemma UNION_disjoint_family: + assumes "finite I" and "\i\I. finite (A i)" + and "disjoint_family_on A I" + shows "F g (\(A ` I)) = F (\x. F g (A x)) I" + using assms unfolding disjoint_family_on_def by (rule UNION_disjoint) + +lemma Union_disjoint_sets: + assumes "\A\C. finite A" and "disjoint C" + shows "F g (\C) = (F \ F) g C" + using assms unfolding disjoint_def by (rule Union_disjoint) + +end + +text \ The union of an infinite disjoint family of non-empty sets is infinite. \ lemma infinite_disjoint_family_imp_infinite_UNION: assumes "\finite A" "\x. x \ A \ f x \ {}" "disjoint_family_on f A" shows "\finite (\(f ` A))" proof - define g where "g x = (SOME y. y \ f x)" for x have g: "g x \ f x" if "x \ A" for x unfolding g_def by (rule someI_ex, insert assms(2) that) blast have inj_on_g: "inj_on g A" proof (rule inj_onI, rule ccontr) fix x y assume A: "x \ A" "y \ A" "g x = g y" "x \ y" with g[of x] g[of y] have "g x \ f x" "g x \ f y" by auto with A \x \ y\ assms show False by (auto simp: disjoint_family_on_def inj_on_def) qed from g have "g ` A \ \(f ` A)" by blast moreover from inj_on_g \\finite A\ have "\finite (g ` A)" using finite_imageD by blast ultimately show ?thesis using finite_subset by blast qed subsection \Construct Disjoint Sequences\ definition disjointed :: "(nat \ 'a set) \ nat \ 'a set" where "disjointed A n = A n - (\i\{0..i\{0..i\{0..i. disjointed A i) = (\i. A i)" by (rule UN_finite2_eq [where k=0]) (simp add: finite_UN_disjointed_eq) lemma less_disjoint_disjointed: "m < n \ disjointed A m \ disjointed A n = {}" by (auto simp add: disjointed_def) lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" by (simp add: disjoint_family_on_def) (metis neq_iff Int_commute less_disjoint_disjointed) lemma disjointed_subset: "disjointed A n \ A n" by (auto simp add: disjointed_def) lemma disjointed_0[simp]: "disjointed A 0 = A 0" by (simp add: disjointed_def) lemma disjointed_mono: "mono A \ disjointed A (Suc n) = A (Suc n) - A n" using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost) subsection \Partitions\ text \ Partitions \<^term>\P\ of a set \<^term>\A\. We explicitly disallow empty sets. \ definition partition_on :: "'a set \ 'a set set \ bool" where "partition_on A P \ \P = A \ disjoint P \ {} \ P" lemma partition_onI: "\P = A \ (\p q. p \ P \ q \ P \ p \ q \ disjnt p q) \ {} \ P \ partition_on A P" by (auto simp: partition_on_def pairwise_def) lemma partition_onD1: "partition_on A P \ A = \P" by (auto simp: partition_on_def) lemma partition_onD2: "partition_on A P \ disjoint P" by (auto simp: partition_on_def) lemma partition_onD3: "partition_on A P \ {} \ P" by (auto simp: partition_on_def) subsection \Constructions of partitions\ lemma partition_on_empty: "partition_on {} P \ P = {}" unfolding partition_on_def by fastforce lemma partition_on_space: "A \ {} \ partition_on A {A}" by (auto simp: partition_on_def disjoint_def) lemma partition_on_singletons: "partition_on A ((\x. {x}) ` A)" by (auto simp: partition_on_def disjoint_def) lemma partition_on_transform: assumes P: "partition_on A P" assumes F_UN: "\(F ` P) = F (\P)" and F_disjnt: "\p q. p \ P \ q \ P \ disjnt p q \ disjnt (F p) (F q)" shows "partition_on (F A) (F ` P - {{}})" proof - have "\(F ` P - {{}}) = F A" unfolding P[THEN partition_onD1] F_UN[symmetric] by auto with P show ?thesis by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt) qed lemma partition_on_restrict: "partition_on A P \ partition_on (B \ A) ((\) B ` P - {{}})" by (intro partition_on_transform) (auto simp: disjnt_def) lemma partition_on_vimage: "partition_on A P \ partition_on (f -` A) ((-`) f ` P - {{}})" by (intro partition_on_transform) (auto simp: disjnt_def) lemma partition_on_inj_image: assumes P: "partition_on A P" and f: "inj_on f A" shows "partition_on (f ` A) ((`) f ` P - {{}})" proof (rule partition_on_transform[OF P]) show "p \ P \ q \ P \ disjnt p q \ disjnt (f ` p) (f ` q)" for p q using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def) qed auto lemma partition_on_insert: assumes "disjnt p (\P)" shows "partition_on A (insert p P) \ partition_on (A-p) P \ p \ A \ p \ {}" using assms by (auto simp: partition_on_def disjnt_iff pairwise_insert) subsection \Finiteness of partitions\ lemma finitely_many_partition_on: assumes "finite A" shows "finite {P. partition_on A P}" proof (rule finite_subset) show "{P. partition_on A P} \ Pow (Pow A)" unfolding partition_on_def by auto show "finite (Pow (Pow A))" using assms by simp qed lemma finite_elements: "finite A \ partition_on A P \ finite P" using partition_onD1[of A P] by (simp add: finite_UnionD) +lemma product_partition: + assumes "partition_on A P" and "\p. p \ P \ finite p" + shows "card A = (\p\P. card p)" + using assms unfolding partition_on_def by (meson card_Union_disjoint) + subsection \Equivalence of partitions and equivalence classes\ lemma partition_on_quotient: assumes r: "equiv A r" shows "partition_on A (A // r)" proof (rule partition_onI) from r have "refl_on A r" by (auto elim: equivE) then show "\(A // r) = A" "{} \ A // r" by (auto simp: refl_on_def quotient_def) fix p q assume "p \ A // r" "q \ A // r" "p \ q" then obtain x y where "x \ A" "y \ A" "p = r `` {x}" "q = r `` {y}" by (auto simp: quotient_def) with r equiv_class_eq_iff[OF r, of x y] \p \ q\ show "disjnt p q" by (auto simp: disjnt_equiv_class) qed lemma equiv_partition_on: assumes P: "partition_on A P" shows "equiv A {(x, y). \p \ P. x \ p \ y \ p}" proof (rule equivI) have "A = \P" "disjoint P" "{} \ P" using P by (auto simp: partition_on_def) then show "refl_on A {(x, y). \p\P. x \ p \ y \ p}" unfolding refl_on_def by auto show "trans {(x, y). \p\P. x \ p \ y \ p}" using \disjoint P\ by (auto simp: trans_def disjoint_def) qed (auto simp: sym_def) lemma partition_on_eq_quotient: assumes P: "partition_on A P" shows "A // {(x, y). \p \ P. x \ p \ y \ p} = P" unfolding quotient_def proof safe fix x assume "x \ A" then obtain p where "p \ P" "x \ p" "\q. q \ P \ x \ q \ p = q" using P by (auto simp: partition_on_def disjoint_def) then have "{y. \p\P. x \ p \ y \ p} = p" by (safe intro!: bexI[of _ p]) simp then show "{(x, y). \p\P. x \ p \ y \ p} `` {x} \ P" by (simp add: \p \ P\) next fix p assume "p \ P" then have "p \ {}" using P by (auto simp: partition_on_def) then obtain x where "x \ p" by auto then have "x \ A" "\q. q \ P \ x \ q \ p = q" using P \p \ P\ by (auto simp: partition_on_def disjoint_def) with \p\P\ \x \ p\ have "{y. \p\P. x \ p \ y \ p} = p" by (safe intro!: bexI[of _ p]) simp then show "p \ (\x\A. {{(x, y). \p\P. x \ p \ y \ p} `` {x}})" by (auto intro: \x \ A\) qed lemma partition_on_alt: "partition_on A P \ (\r. equiv A r \ P = A // r)" by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on) end diff --git a/src/HOL/Power.thy b/src/HOL/Power.thy --- a/src/HOL/Power.thy +++ b/src/HOL/Power.thy @@ -1,1021 +1,1025 @@ (* Title: HOL/Power.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge *) section \Exponentiation\ theory Power imports Num begin subsection \Powers for Arbitrary Monoids\ class power = one + times begin primrec power :: "'a \ nat \ 'a" (infixr "^" 80) where power_0: "a ^ 0 = 1" | power_Suc: "a ^ Suc n = a * a ^ n" notation (latex output) power ("(_\<^bsup>_\<^esup>)" [1000] 1000) text \Special syntax for squares.\ abbreviation power2 :: "'a \ 'a" ("(_\<^sup>2)" [1000] 999) where "x\<^sup>2 \ x ^ 2" end context includes lifting_syntax begin lemma power_transfer [transfer_rule]: \(R ===> (=) ===> R) (^) (^)\ if [transfer_rule]: \R 1 1\ \(R ===> R ===> R) (*) (*)\ for R :: \'a::power \ 'b::power \ bool\ by (simp only: power_def [abs_def]) transfer_prover end context monoid_mult begin subclass power . lemma power_one [simp]: "1 ^ n = 1" by (induct n) simp_all lemma power_one_right [simp]: "a ^ 1 = a" by simp lemma power_Suc0_right [simp]: "a ^ Suc 0 = a" by simp lemma power_commutes: "a ^ n * a = a * a ^ n" by (induct n) (simp_all add: mult.assoc) lemma power_Suc2: "a ^ Suc n = a ^ n * a" by (simp add: power_commutes) lemma power_add: "a ^ (m + n) = a ^ m * a ^ n" by (induct m) (simp_all add: algebra_simps) lemma power_mult: "a ^ (m * n) = (a ^ m) ^ n" by (induct n) (simp_all add: power_add) lemma power_even_eq: "a ^ (2 * n) = (a ^ n)\<^sup>2" by (subst mult.commute) (simp add: power_mult) lemma power_odd_eq: "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2" by (simp add: power_even_eq) lemma power_numeral_even: "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)" by (simp only: numeral_Bit0 power_add Let_def) lemma power_numeral_odd: "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)" by (simp only: numeral_Bit1 One_nat_def add_Suc_right add_0_right power_Suc power_add Let_def mult.assoc) lemma power2_eq_square: "a\<^sup>2 = a * a" by (simp add: numeral_2_eq_2) lemma power3_eq_cube: "a ^ 3 = a * a * a" by (simp add: numeral_3_eq_3 mult.assoc) lemma power4_eq_xxxx: "x^4 = x * x * x * x" by (simp add: mult.assoc power_numeral_even) lemma funpow_times_power: "(times x ^^ f x) = times (x ^ f x)" proof (induct "f x" arbitrary: f) case 0 then show ?case by (simp add: fun_eq_iff) next case (Suc n) define g where "g x = f x - 1" for x with Suc have "n = g x" by simp with Suc have "times x ^^ g x = times (x ^ g x)" by simp moreover from Suc g_def have "f x = g x + 1" by simp ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc) qed lemma power_commuting_commutes: assumes "x * y = y * x" shows "x ^ n * y = y * x ^n" proof (induct n) case 0 then show ?case by simp next case (Suc n) have "x ^ Suc n * y = x ^ n * y * x" by (subst power_Suc2) (simp add: assms ac_simps) also have "\ = y * x ^ Suc n" by (simp only: Suc power_Suc2) (simp add: ac_simps) finally show ?case . qed lemma power_minus_mult: "0 < n \ a ^ (n - 1) * a = a ^ n" by (simp add: power_commutes split: nat_diff_split) lemma left_right_inverse_power: assumes "x * y = 1" shows "x ^ n * y ^ n = 1" proof (induct n) case (Suc n) moreover have "x ^ Suc n * y ^ Suc n = x^n * (x * y) * y^n" by (simp add: power_Suc2[symmetric] mult.assoc[symmetric]) ultimately show ?case by (simp add: assms) qed simp end context comm_monoid_mult begin lemma power_mult_distrib [algebra_simps, algebra_split_simps, field_simps, field_split_simps, divide_simps]: "(a * b) ^ n = (a ^ n) * (b ^ n)" by (induction n) (simp_all add: ac_simps) end text \Extract constant factors from powers.\ declare power_mult_distrib [where a = "numeral w" for w, simp] declare power_mult_distrib [where b = "numeral w" for w, simp] lemma power_add_numeral [simp]: "a^numeral m * a^numeral n = a^numeral (m + n)" for a :: "'a::monoid_mult" by (simp add: power_add [symmetric]) lemma power_add_numeral2 [simp]: "a^numeral m * (a^numeral n * b) = a^numeral (m + n) * b" for a :: "'a::monoid_mult" by (simp add: mult.assoc [symmetric]) lemma power_mult_numeral [simp]: "(a^numeral m)^numeral n = a^numeral (m * n)" for a :: "'a::monoid_mult" by (simp only: numeral_mult power_mult) context semiring_numeral begin lemma numeral_sqr: "numeral (Num.sqr k) = numeral k * numeral k" by (simp only: sqr_conv_mult numeral_mult) lemma numeral_pow: "numeral (Num.pow k l) = numeral k ^ numeral l" by (induct l) (simp_all only: numeral_class.numeral.simps pow.simps numeral_sqr numeral_mult power_add power_one_right) lemma power_numeral [simp]: "numeral k ^ numeral l = numeral (Num.pow k l)" by (rule numeral_pow [symmetric]) end context semiring_1 begin lemma of_nat_power [simp]: "of_nat (m ^ n) = of_nat m ^ n" by (induct n) simp_all lemma zero_power: "0 < n \ 0 ^ n = 0" by (cases n) simp_all lemma power_zero_numeral [simp]: "0 ^ numeral k = 0" by (simp add: numeral_eq_Suc) lemma zero_power2: "0\<^sup>2 = 0" (* delete? *) by (rule power_zero_numeral) lemma one_power2: "1\<^sup>2 = 1" (* delete? *) by (rule power_one) lemma power_0_Suc [simp]: "0 ^ Suc n = 0" by simp text \It looks plausible as a simprule, but its effect can be strange.\ lemma power_0_left: "0 ^ n = (if n = 0 then 1 else 0)" by (cases n) simp_all end context semiring_char_0 begin lemma numeral_power_eq_of_nat_cancel_iff [simp]: "numeral x ^ n = of_nat y \ numeral x ^ n = y" using of_nat_eq_iff by fastforce lemma real_of_nat_eq_numeral_power_cancel_iff [simp]: "of_nat y = numeral x ^ n \ y = numeral x ^ n" using numeral_power_eq_of_nat_cancel_iff [of x n y] by (metis (mono_tags)) lemma of_nat_eq_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w = of_nat x \ b ^ w = x" by (metis of_nat_power of_nat_eq_iff) lemma of_nat_power_eq_of_nat_cancel_iff[simp]: "of_nat x = (of_nat b) ^ w \ x = b ^ w" by (metis of_nat_eq_of_nat_power_cancel_iff) end context comm_semiring_1 begin text \The divides relation.\ lemma le_imp_power_dvd: assumes "m \ n" shows "a ^ m dvd a ^ n" proof from assms have "a ^ n = a ^ (m + (n - m))" by simp also have "\ = a ^ m * a ^ (n - m)" by (rule power_add) finally show "a ^ n = a ^ m * a ^ (n - m)" . qed lemma power_le_dvd: "a ^ n dvd b \ m \ n \ a ^ m dvd b" by (rule dvd_trans [OF le_imp_power_dvd]) lemma dvd_power_same: "x dvd y \ x ^ n dvd y ^ n" by (induct n) (auto simp add: mult_dvd_mono) lemma dvd_power_le: "x dvd y \ m \ n \ x ^ n dvd y ^ m" by (rule power_le_dvd [OF dvd_power_same]) lemma dvd_power [simp]: fixes n :: nat assumes "n > 0 \ x = 1" shows "x dvd (x ^ n)" using assms proof assume "0 < n" then have "x ^ n = x ^ Suc (n - 1)" by simp then show "x dvd (x ^ n)" by simp next assume "x = 1" then show "x dvd (x ^ n)" by simp qed end context semiring_1_no_zero_divisors begin subclass power . lemma power_eq_0_iff [simp]: "a ^ n = 0 \ a = 0 \ n > 0" by (induct n) auto lemma power_not_zero: "a \ 0 \ a ^ n \ 0" by (induct n) auto lemma zero_eq_power2 [simp]: "a\<^sup>2 = 0 \ a = 0" unfolding power2_eq_square by simp end context ring_1 begin lemma power_minus: "(- a) ^ n = (- 1) ^ n * a ^ n" proof (induct n) case 0 show ?case by simp next case (Suc n) then show ?case by (simp del: power_Suc add: power_Suc2 mult.assoc) qed lemma power_minus': "NO_MATCH 1 x \ (-x) ^ n = (-1)^n * x ^ n" by (rule power_minus) lemma power_minus_Bit0: "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)" by (induct k, simp_all only: numeral_class.numeral.simps power_add power_one_right mult_minus_left mult_minus_right minus_minus) lemma power_minus_Bit1: "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))" by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left) lemma power2_minus [simp]: "(- a)\<^sup>2 = a\<^sup>2" by (fact power_minus_Bit0) lemma power_minus1_even [simp]: "(- 1) ^ (2*n) = 1" proof (induct n) case 0 show ?case by simp next case (Suc n) then show ?case by (simp add: power_add power2_eq_square) qed lemma power_minus1_odd: "(- 1) ^ Suc (2*n) = -1" by simp lemma power_minus_even [simp]: "(-a) ^ (2*n) = a ^ (2*n)" by (simp add: power_minus [of a]) end context ring_1_no_zero_divisors begin lemma power2_eq_1_iff: "a\<^sup>2 = 1 \ a = 1 \ a = - 1" using square_eq_1_iff [of a] by (simp add: power2_eq_square) end context idom begin lemma power2_eq_iff: "x\<^sup>2 = y\<^sup>2 \ x = y \ x = - y" unfolding power2_eq_square by (rule square_eq_iff) end context semidom_divide begin lemma power_diff: "a ^ (m - n) = (a ^ m) div (a ^ n)" if "a \ 0" and "n \ m" proof - define q where "q = m - n" with \n \ m\ have "m = q + n" by simp with \a \ 0\ q_def show ?thesis by (simp add: power_add) qed end context algebraic_semidom begin lemma div_power: "b dvd a \ (a div b) ^ n = a ^ n div b ^ n" by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same) lemma is_unit_power_iff: "is_unit (a ^ n) \ is_unit a \ n = 0" by (induct n) (auto simp add: is_unit_mult_iff) lemma dvd_power_iff: assumes "x \ 0" shows "x ^ m dvd x ^ n \ is_unit x \ m \ n" proof assume *: "x ^ m dvd x ^ n" { assume "m > n" note * also have "x ^ n = x ^ n * 1" by simp also from \m > n\ have "m = n + (m - n)" by simp also have "x ^ \ = x ^ n * x ^ (m - n)" by (rule power_add) finally have "x ^ (m - n) dvd 1" by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all) with \m > n\ have "is_unit x" by (simp add: is_unit_power_iff) } thus "is_unit x \ m \ n" by force qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd) end context normalization_semidom_multiplicative begin lemma normalize_power: "normalize (a ^ n) = normalize a ^ n" by (induct n) (simp_all add: normalize_mult) lemma unit_factor_power: "unit_factor (a ^ n) = unit_factor a ^ n" by (induct n) (simp_all add: unit_factor_mult) end context division_ring begin text \Perhaps these should be simprules.\ lemma power_inverse [field_simps, field_split_simps, divide_simps]: "inverse a ^ n = inverse (a ^ n)" proof (cases "a = 0") case True then show ?thesis by (simp add: power_0_left) next case False then have "inverse (a ^ n) = inverse a ^ n" by (induct n) (simp_all add: nonzero_inverse_mult_distrib power_commutes) then show ?thesis by simp qed lemma power_one_over [field_simps, field_split_simps, divide_simps]: "(1 / a) ^ n = 1 / a ^ n" using power_inverse [of a] by (simp add: divide_inverse) end context field begin lemma power_divide [field_simps, field_split_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n" by (induct n) simp_all end subsection \Exponentiation on ordered types\ context linordered_semidom begin lemma zero_less_power [simp]: "0 < a \ 0 < a ^ n" by (induct n) simp_all lemma zero_le_power [simp]: "0 \ a \ 0 \ a ^ n" by (induct n) simp_all lemma power_mono: "a \ b \ 0 \ a \ a ^ n \ b ^ n" by (induct n) (auto intro: mult_mono order_trans [of 0 a b]) lemma one_le_power [simp]: "1 \ a \ 1 \ a ^ n" using power_mono [of 1 a n] by simp lemma power_le_one: "0 \ a \ a \ 1 \ a ^ n \ 1" using power_mono [of a 1 n] by simp lemma power_gt1_lemma: assumes gt1: "1 < a" shows "1 < a * a ^ n" proof - from gt1 have "0 \ a" by (fact order_trans [OF zero_le_one less_imp_le]) from gt1 have "1 * 1 < a * 1" by simp also from gt1 have "\ \ a * a ^ n" by (simp only: mult_mono \0 \ a\ one_le_power order_less_imp_le zero_le_one order_refl) finally show ?thesis by simp qed lemma power_gt1: "1 < a \ 1 < a ^ Suc n" by (simp add: power_gt1_lemma) lemma one_less_power [simp]: "1 < a \ 0 < n \ 1 < a ^ n" by (cases n) (simp_all add: power_gt1_lemma) lemma power_le_imp_le_exp: assumes gt1: "1 < a" shows "a ^ m \ a ^ n \ m \ n" proof (induct m arbitrary: n) case 0 show ?case by simp next case (Suc m) show ?case proof (cases n) case 0 with Suc have "a * a ^ m \ 1" by simp with gt1 show ?thesis by (force simp only: power_gt1_lemma not_less [symmetric]) next case (Suc n) with Suc.prems Suc.hyps show ?thesis by (force dest: mult_left_le_imp_le simp add: less_trans [OF zero_less_one gt1]) qed qed lemma of_nat_zero_less_power_iff [simp]: "of_nat x ^ n > 0 \ x > 0 \ n = 0" by (induct n) auto text \Surely we can strengthen this? It holds for \0 too.\ lemma power_inject_exp [simp]: \a ^ m = a ^ n \ m = n\ if \1 < a\ using that by (force simp add: order_class.order.antisym power_le_imp_le_exp) text \ Can relax the first premise to \<^term>\0 in the case of the natural numbers. \ lemma power_less_imp_less_exp: "1 < a \ a ^ m < a ^ n \ m < n" by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] power_le_imp_le_exp) lemma power_strict_mono [rule_format]: "a < b \ 0 \ a \ 0 < n \ a ^ n < b ^ n" by (induct n) (auto simp: mult_strict_mono le_less_trans [of 0 a b]) lemma power_mono_iff [simp]: shows "\a \ 0; b \ 0; n>0\ \ a ^ n \ b ^ n \ a \ b" using power_mono [of a b] power_strict_mono [of b a] not_le by auto text\Lemma for \power_strict_decreasing\\ lemma power_Suc_less: "0 < a \ a < 1 \ a * a ^ n < a ^ n" by (induct n) (auto simp: mult_strict_left_mono) lemma power_strict_decreasing [rule_format]: "n < N \ 0 < a \ a < 1 \ a ^ N < a ^ n" proof (induct N) case 0 then show ?case by simp next case (Suc N) then show ?case apply (auto simp add: power_Suc_less less_Suc_eq) apply (subgoal_tac "a * a^N < 1 * a^n") apply simp apply (rule mult_strict_mono) apply auto done qed text \Proof resembles that of \power_strict_decreasing\.\ lemma power_decreasing: "n \ N \ 0 \ a \ a \ 1 \ a ^ N \ a ^ n" proof (induct N) case 0 then show ?case by simp next case (Suc N) then show ?case apply (auto simp add: le_Suc_eq) apply (subgoal_tac "a * a^N \ 1 * a^n") apply simp apply (rule mult_mono) apply auto done qed lemma power_decreasing_iff [simp]: "\0 < b; b < 1\ \ b ^ m \ b ^ n \ n \ m" using power_strict_decreasing [of m n b] by (auto intro: power_decreasing ccontr) lemma power_strict_decreasing_iff [simp]: "\0 < b; b < 1\ \ b ^ m < b ^ n \ n < m" using power_decreasing_iff [of b m n] unfolding le_less by (auto dest: power_strict_decreasing le_neq_implies_less) lemma power_Suc_less_one: "0 < a \ a < 1 \ a ^ Suc n < 1" using power_strict_decreasing [of 0 "Suc n" a] by simp text \Proof again resembles that of \power_strict_decreasing\.\ lemma power_increasing: "n \ N \ 1 \ a \ a ^ n \ a ^ N" proof (induct N) case 0 then show ?case by simp next case (Suc N) then show ?case apply (auto simp add: le_Suc_eq) apply (subgoal_tac "1 * a^n \ a * a^N") apply simp apply (rule mult_mono) apply (auto simp add: order_trans [OF zero_le_one]) done qed text \Lemma for \power_strict_increasing\.\ lemma power_less_power_Suc: "1 < a \ a ^ n < a * a ^ n" by (induct n) (auto simp: mult_strict_left_mono less_trans [OF zero_less_one]) lemma power_strict_increasing: "n < N \ 1 < a \ a ^ n < a ^ N" proof (induct N) case 0 then show ?case by simp next case (Suc N) then show ?case apply (auto simp add: power_less_power_Suc less_Suc_eq) apply (subgoal_tac "1 * a^n < a * a^N") apply simp apply (rule mult_strict_mono) apply (auto simp add: less_trans [OF zero_less_one] less_imp_le) done qed lemma power_increasing_iff [simp]: "1 < b \ b ^ x \ b ^ y \ x \ y" by (blast intro: power_le_imp_le_exp power_increasing less_imp_le) lemma power_strict_increasing_iff [simp]: "1 < b \ b ^ x < b ^ y \ x < y" by (blast intro: power_less_imp_less_exp power_strict_increasing) lemma power_le_imp_le_base: assumes le: "a ^ Suc n \ b ^ Suc n" and "0 \ b" shows "a \ b" proof (rule ccontr) assume "\ ?thesis" then have "b < a" by (simp only: linorder_not_le) then have "b ^ Suc n < a ^ Suc n" by (simp only: assms(2) power_strict_mono) with le show False by (simp add: linorder_not_less [symmetric]) qed lemma power_less_imp_less_base: assumes less: "a ^ n < b ^ n" assumes nonneg: "0 \ b" shows "a < b" proof (rule contrapos_pp [OF less]) assume "\ ?thesis" then have "b \ a" by (simp only: linorder_not_less) from this nonneg have "b ^ n \ a ^ n" by (rule power_mono) then show "\ a ^ n < b ^ n" by (simp only: linorder_not_less) qed lemma power_inject_base: "a ^ Suc n = b ^ Suc n \ 0 \ a \ 0 \ b \ a = b" by (blast intro: power_le_imp_le_base order.antisym eq_refl sym) lemma power_eq_imp_eq_base: "a ^ n = b ^ n \ 0 \ a \ 0 \ b \ 0 < n \ a = b" by (cases n) (simp_all del: power_Suc, rule power_inject_base) lemma power_eq_iff_eq_base: "0 < n \ 0 \ a \ 0 \ b \ a ^ n = b ^ n \ a = b" using power_eq_imp_eq_base [of a n b] by auto lemma power2_le_imp_le: "x\<^sup>2 \ y\<^sup>2 \ 0 \ y \ x \ y" unfolding numeral_2_eq_2 by (rule power_le_imp_le_base) lemma power2_less_imp_less: "x\<^sup>2 < y\<^sup>2 \ 0 \ y \ x < y" by (rule power_less_imp_less_base) lemma power2_eq_imp_eq: "x\<^sup>2 = y\<^sup>2 \ 0 \ x \ 0 \ y \ x = y" unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp lemma power_Suc_le_self: "0 \ a \ a \ 1 \ a ^ Suc n \ a" using power_decreasing [of 1 "Suc n" a] by simp lemma power2_eq_iff_nonneg [simp]: assumes "0 \ x" "0 \ y" shows "(x ^ 2 = y ^ 2) \ x = y" using assms power2_eq_imp_eq by blast lemma of_nat_less_numeral_power_cancel_iff[simp]: "of_nat x < numeral i ^ n \ x < numeral i ^ n" using of_nat_less_iff[of x "numeral i ^ n", unfolded of_nat_numeral of_nat_power] . lemma of_nat_le_numeral_power_cancel_iff[simp]: "of_nat x \ numeral i ^ n \ x \ numeral i ^ n" using of_nat_le_iff[of x "numeral i ^ n", unfolded of_nat_numeral of_nat_power] . lemma numeral_power_less_of_nat_cancel_iff[simp]: "numeral i ^ n < of_nat x \ numeral i ^ n < x" using of_nat_less_iff[of "numeral i ^ n" x, unfolded of_nat_numeral of_nat_power] . lemma numeral_power_le_of_nat_cancel_iff[simp]: "numeral i ^ n \ of_nat x \ numeral i ^ n \ x" using of_nat_le_iff[of "numeral i ^ n" x, unfolded of_nat_numeral of_nat_power] . lemma of_nat_le_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w \ of_nat x \ b ^ w \ x" by (metis of_nat_le_iff of_nat_power) lemma of_nat_power_le_of_nat_cancel_iff[simp]: "of_nat x \ (of_nat b) ^ w \ x \ b ^ w" by (metis of_nat_le_iff of_nat_power) lemma of_nat_less_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w < of_nat x \ b ^ w < x" by (metis of_nat_less_iff of_nat_power) lemma of_nat_power_less_of_nat_cancel_iff[simp]: "of_nat x < (of_nat b) ^ w \ x < b ^ w" by (metis of_nat_less_iff of_nat_power) end text \Some @{typ nat}-specific lemmas:\ lemma mono_ge2_power_minus_self: assumes "k \ 2" shows "mono (\m. k ^ m - m)" unfolding mono_iff_le_Suc proof fix n have "k ^ n < k ^ Suc n" using power_strict_increasing_iff[of k "n" "Suc n"] assms by linarith thus "k ^ n - n \ k ^ Suc n - Suc n" by linarith qed lemma self_le_ge2_pow[simp]: assumes "k \ 2" shows "m \ k ^ m" proof (induction m) case 0 show ?case by simp next case (Suc m) hence "Suc m \ Suc (k ^ m)" by simp also have "... \ k^m + k^m" using one_le_power[of k m] assms by linarith also have "... \ k * k^m" by (metis mult_2 mult_le_mono1[OF assms]) finally show ?case by simp qed lemma diff_le_diff_pow[simp]: assumes "k \ 2" shows "m - n \ k ^ m - k ^ n" proof (cases "n \ m") case True thus ?thesis using monoD[OF mono_ge2_power_minus_self[OF assms] True] self_le_ge2_pow[OF assms, of m] by (simp add: le_diff_conv le_diff_conv2) qed auto context linordered_ring_strict begin lemma sum_squares_eq_zero_iff: "x * x + y * y = 0 \ x = 0 \ y = 0" by (simp add: add_nonneg_eq_0_iff) lemma sum_squares_le_zero_iff: "x * x + y * y \ 0 \ x = 0 \ y = 0" by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff) lemma sum_squares_gt_zero_iff: "0 < x * x + y * y \ x \ 0 \ y \ 0" by (simp add: not_le [symmetric] sum_squares_le_zero_iff) end context linordered_idom begin lemma zero_le_power2 [simp]: "0 \ a\<^sup>2" by (simp add: power2_eq_square) lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \ a \ 0" by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) lemma power2_less_0 [simp]: "\ a\<^sup>2 < 0" by (force simp add: power2_eq_square mult_less_0_iff) lemma power_abs: "\a ^ n\ = \a\ ^ n" \ \FIXME simp?\ by (induct n) (simp_all add: abs_mult) lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n" by (induct n) (simp_all add: sgn_mult) lemma abs_power_minus [simp]: "\(- a) ^ n\ = \a ^ n\" by (simp add: power_abs) lemma zero_less_power_abs_iff [simp]: "0 < \a\ ^ n \ a \ 0 \ n = 0" proof (induct n) case 0 show ?case by simp next case Suc then show ?case by (auto simp: zero_less_mult_iff) qed lemma zero_le_power_abs [simp]: "0 \ \a\ ^ n" by (rule zero_le_power [OF abs_ge_zero]) lemma power2_less_eq_zero_iff [simp]: "a\<^sup>2 \ 0 \ a = 0" by (simp add: le_less) lemma abs_power2 [simp]: "\a\<^sup>2\ = a\<^sup>2" by (simp add: power2_eq_square) lemma power2_abs [simp]: "\a\\<^sup>2 = a\<^sup>2" by (simp add: power2_eq_square) lemma odd_power_less_zero: "a < 0 \ a ^ Suc (2 * n) < 0" proof (induct n) case 0 then show ?case by simp next case (Suc n) have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" by (simp add: ac_simps power_add power2_eq_square) then show ?case by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg) qed lemma odd_0_le_power_imp_0_le: "0 \ a ^ Suc (2 * n) \ 0 \ a" using odd_power_less_zero [of a n] by (force simp add: linorder_not_less [symmetric]) lemma zero_le_even_power'[simp]: "0 \ a ^ (2 * n)" proof (induct n) case 0 show ?case by simp next case (Suc n) have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" by (simp add: ac_simps power_add power2_eq_square) then show ?case by (simp add: Suc zero_le_mult_iff) qed lemma sum_power2_ge_zero: "0 \ x\<^sup>2 + y\<^sup>2" by (intro add_nonneg_nonneg zero_le_power2) lemma not_sum_power2_lt_zero: "\ x\<^sup>2 + y\<^sup>2 < 0" unfolding not_less by (rule sum_power2_ge_zero) lemma sum_power2_eq_zero_iff: "x\<^sup>2 + y\<^sup>2 = 0 \ x = 0 \ y = 0" unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff) lemma sum_power2_le_zero_iff: "x\<^sup>2 + y\<^sup>2 \ 0 \ x = 0 \ y = 0" by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero) lemma sum_power2_gt_zero_iff: "0 < x\<^sup>2 + y\<^sup>2 \ x \ 0 \ y \ 0" unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) lemma abs_le_square_iff: "\x\ \ \y\ \ x\<^sup>2 \ y\<^sup>2" (is "?lhs \ ?rhs") proof assume ?lhs then have "\x\\<^sup>2 \ \y\\<^sup>2" by (rule power_mono) simp then show ?rhs by simp next assume ?rhs then show ?lhs by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero]) qed +lemma power2_le_iff_abs_le: + "y \ 0 \ x\<^sup>2 \ y\<^sup>2 \ \x\ \ y" + by (metis abs_le_square_iff abs_of_nonneg) + lemma abs_square_le_1:"x\<^sup>2 \ 1 \ \x\ \ 1" using abs_le_square_iff [of x 1] by simp lemma abs_square_eq_1: "x\<^sup>2 = 1 \ \x\ = 1" by (auto simp add: abs_if power2_eq_1_iff) lemma abs_square_less_1: "x\<^sup>2 < 1 \ \x\ < 1" using abs_square_eq_1 [of x] abs_square_le_1 [of x] by (auto simp add: le_less) lemma square_le_1: assumes "- 1 \ x" "x \ 1" shows "x\<^sup>2 \ 1" using assms by (metis add.inverse_inverse linear mult_le_one neg_equal_0_iff_equal neg_le_iff_le power2_eq_square power_minus_Bit0) end subsection \Miscellaneous rules\ lemma (in linordered_semidom) self_le_power: "1 \ a \ 0 < n \ a \ a ^ n" using power_increasing [of 1 n a] power_one_right [of a] by auto lemma (in power) power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))" unfolding One_nat_def by (cases m) simp_all lemma (in comm_semiring_1) power2_sum: "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y" by (simp add: algebra_simps power2_eq_square mult_2_right) context comm_ring_1 begin lemma power2_diff: "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y" by (simp add: algebra_simps power2_eq_square mult_2_right) lemma power2_commute: "(x - y)\<^sup>2 = (y - x)\<^sup>2" by (simp add: algebra_simps power2_eq_square) lemma minus_power_mult_self: "(- a) ^ n * (- a) ^ n = a ^ (2 * n)" by (simp add: power_mult_distrib [symmetric]) (simp add: power2_eq_square [symmetric] power_mult [symmetric]) lemma minus_one_mult_self [simp]: "(- 1) ^ n * (- 1) ^ n = 1" using minus_power_mult_self [of 1 n] by simp lemma left_minus_one_mult_self [simp]: "(- 1) ^ n * ((- 1) ^ n * a) = a" by (simp add: mult.assoc [symmetric]) end text \Simprules for comparisons where common factors can be cancelled.\ lemmas zero_compare_simps = add_strict_increasing add_strict_increasing2 add_increasing zero_le_mult_iff zero_le_divide_iff zero_less_mult_iff zero_less_divide_iff mult_le_0_iff divide_le_0_iff mult_less_0_iff divide_less_0_iff zero_le_power2 power2_less_0 subsection \Exponentiation for the Natural Numbers\ lemma nat_one_le_power [simp]: "Suc 0 \ i \ Suc 0 \ i ^ n" by (rule one_le_power [of i n, unfolded One_nat_def]) lemma nat_zero_less_power_iff [simp]: "x ^ n > 0 \ x > 0 \ n = 0" for x :: nat by (induct n) auto lemma nat_power_eq_Suc_0_iff [simp]: "x ^ m = Suc 0 \ m = 0 \ x = Suc 0" by (induct m) auto lemma power_Suc_0 [simp]: "Suc 0 ^ n = Suc 0" by simp text \ Valid for the naturals, but what if \0 < i < 1\? Premises cannot be weakened: consider the case where \i = 0\, \m = 1\ and \n = 0\. \ lemma nat_power_less_imp_less: fixes i :: nat assumes nonneg: "0 < i" assumes less: "i ^ m < i ^ n" shows "m < n" proof (cases "i = 1") case True with less power_one [where 'a = nat] show ?thesis by simp next case False with nonneg have "1 < i" by auto from power_strict_increasing_iff [OF this] less show ?thesis .. qed lemma power_gt_expt: "n > Suc 0 \ n^k > k" by (induction k) (auto simp: less_trans_Suc n_less_m_mult_n) lemma less_exp [simp]: \n < 2 ^ n\ by (simp add: power_gt_expt) lemma power_dvd_imp_le: fixes i :: nat assumes "i ^ m dvd i ^ n" "1 < i" shows "m \ n" using assms by (auto intro: power_le_imp_le_exp [OF \1 < i\ dvd_imp_le]) lemma dvd_power_iff_le: fixes k::nat shows "2 \ k \ ((k ^ m) dvd (k ^ n) \ m \ n)" using le_imp_power_dvd power_dvd_imp_le by force lemma power2_nat_le_eq_le: "m\<^sup>2 \ n\<^sup>2 \ m \ n" for m n :: nat by (auto intro: power2_le_imp_le power_mono) lemma power2_nat_le_imp_le: fixes m n :: nat assumes "m\<^sup>2 \ n" shows "m \ n" proof (cases m) case 0 then show ?thesis by simp next case (Suc k) show ?thesis proof (rule ccontr) assume "\ ?thesis" then have "n < m" by simp with assms Suc show False by (simp add: power2_eq_square) qed qed lemma ex_power_ivl1: fixes b k :: nat assumes "b \ 2" shows "k \ 1 \ \n. b^n \ k \ k < b^(n+1)" (is "_ \ \n. ?P k n") proof(induction k) case 0 thus ?case by simp next case (Suc k) show ?case proof cases assume "k=0" hence "?P (Suc k) 0" using assms by simp thus ?case .. next assume "k\0" with Suc obtain n where IH: "?P k n" by auto show ?case proof (cases "k = b^(n+1) - 1") case True hence "?P (Suc k) (n+1)" using assms by (simp add: power_less_power_Suc) thus ?thesis .. next case False hence "?P (Suc k) n" using IH by auto thus ?thesis .. qed qed qed lemma ex_power_ivl2: fixes b k :: nat assumes "b \ 2" "k \ 2" shows "\n. b^n < k \ k \ b^(n+1)" proof - have "1 \ k - 1" using assms(2) by arith from ex_power_ivl1[OF assms(1) this] obtain n where "b ^ n \ k - 1 \ k - 1 < b ^ (n + 1)" .. hence "b^n < k \ k \ b^(n+1)" using assms by auto thus ?thesis .. qed subsubsection \Cardinality of the Powerset\ lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2" unfolding UNIV_bool by simp lemma card_Pow: "finite A \ card (Pow A) = 2 ^ card A" proof (induct rule: finite_induct) case empty show ?case by simp next case (insert x A) from \x \ A\ have disjoint: "Pow A \ insert x ` Pow A = {}" by blast from \x \ A\ have inj_on: "inj_on (insert x) (Pow A)" unfolding inj_on_def by auto have "card (Pow (insert x A)) = card (Pow A \ insert x ` Pow A)" by (simp only: Pow_insert) also have "\ = card (Pow A) + card (insert x ` Pow A)" by (rule card_Un_disjoint) (use \finite A\ disjoint in simp_all) also from inj_on have "card (insert x ` Pow A) = card (Pow A)" by (rule card_image) also have "\ + \ = 2 * \" by (simp add: mult_2) also from insert(3) have "\ = 2 ^ Suc (card A)" by simp also from insert(1,2) have "Suc (card A) = card (insert x A)" by (rule card_insert_disjoint [symmetric]) finally show ?case . qed subsection \Code generator tweak\ code_identifier code_module Power \ (SML) Arith and (OCaml) Arith and (Haskell) Arith end