diff --git a/src/HOL/Analysis/Brouwer_Fixpoint.thy b/src/HOL/Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy @@ -1,2605 +1,2602 @@ (* Author: John Harrison Author: Robert Himmelmann, TU Muenchen (Translation from HOL light) and LCP *) (* At the moment this is just Brouwer's fixpoint theorem. The proof is from *) (* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518 *) (* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf". *) (* *) (* The script below is quite messy, but at least we avoid formalizing any *) (* topological machinery; we don't even use barycentric subdivision; this is *) (* the big advantage of Kuhn's proof over the usual Sperner's lemma one. *) (* *) (* (c) Copyright, John Harrison 1998-2008 *) section \Brouwer's Fixed Point Theorem\ theory Brouwer_Fixpoint imports Homeomorphism Derivative begin subsection \Retractions\ lemma retract_of_contractible: assumes "contractible T" "S retract_of T" shows "contractible S" using assms apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with) apply (rule_tac x="r a" in exI) apply (rule_tac x="r \ h" in exI) apply (intro conjI continuous_intros continuous_on_compose) apply (erule continuous_on_subset | force)+ done lemma retract_of_path_connected: "\path_connected T; S retract_of T\ \ path_connected S" by (metis path_connected_continuous_image retract_of_def retraction) lemma retract_of_simply_connected: "\simply_connected T; S retract_of T\ \ simply_connected S" apply (simp add: retract_of_def retraction_def, clarify) apply (rule simply_connected_retraction_gen) apply (force elim!: continuous_on_subset)+ done lemma retract_of_homotopically_trivial: assumes ts: "T retract_of S" and hom: "\f g. \continuous_on U f; f ` U \ S; continuous_on U g; g ` U \ S\ \ homotopic_with_canon (\x. True) U S f g" and "continuous_on U f" "f ` U \ T" and "continuous_on U g" "g ` U \ T" shows "homotopic_with_canon (\x. True) U T f g" proof - obtain r where "r ` S \ S" "continuous_on S r" "\x\S. r (r x) = r x" "T = r ` S" using ts by (auto simp: retract_of_def retraction) then obtain k where "Retracts S r T k" unfolding Retracts_def by (metis continuous_on_subset dual_order.trans image_iff image_mono) then show ?thesis apply (rule Retracts.homotopically_trivial_retraction_gen) using assms apply (force simp: hom)+ done qed lemma retract_of_homotopically_trivial_null: assumes ts: "T retract_of S" and hom: "\f. \continuous_on U f; f ` U \ S\ \ \c. homotopic_with_canon (\x. True) U S f (\x. c)" and "continuous_on U f" "f ` U \ T" obtains c where "homotopic_with_canon (\x. True) U T f (\x. c)" proof - obtain r where "r ` S \ S" "continuous_on S r" "\x\S. r (r x) = r x" "T = r ` S" using ts by (auto simp: retract_of_def retraction) then obtain k where "Retracts S r T k" unfolding Retracts_def by (metis continuous_on_subset dual_order.trans image_iff image_mono) then show ?thesis apply (rule Retracts.homotopically_trivial_retraction_null_gen) apply (rule TrueI refl assms that | assumption)+ done qed lemma retraction_openin_vimage_iff: "openin (top_of_set S) (S \ r -` U) \ openin (top_of_set T) U" if retraction: "retraction S T r" and "U \ T" using retraction apply (rule retractionE) apply (rule continuous_right_inverse_imp_quotient_map [where g=r]) using \U \ T\ apply (auto elim: continuous_on_subset) done lemma retract_of_locally_compact: fixes S :: "'a :: {heine_borel,real_normed_vector} set" shows "\ locally compact S; T retract_of S\ \ locally compact T" by (metis locally_compact_closedin closedin_retract) lemma homotopic_into_retract: "\f ` S \ T; g ` S \ T; T retract_of U; homotopic_with_canon (\x. True) S U f g\ \ homotopic_with_canon (\x. True) S T f g" apply (subst (asm) homotopic_with_def) apply (simp add: homotopic_with retract_of_def retraction_def, clarify) apply (rule_tac x="r \ h" in exI) apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+ done lemma retract_of_locally_connected: assumes "locally connected T" "S retract_of T" shows "locally connected S" using assms by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_connected_quotient_image retract_ofE) lemma retract_of_locally_path_connected: assumes "locally path_connected T" "S retract_of T" shows "locally path_connected S" using assms by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_path_connected_quotient_image retract_ofE) text \A few simple lemmas about deformation retracts\ lemma deformation_retract_imp_homotopy_eqv: fixes S :: "'a::euclidean_space set" assumes "homotopic_with_canon (\x. True) S S id r" and r: "retraction S T r" shows "S homotopy_eqv T" proof - have "homotopic_with_canon (\x. True) S S (id \ r) id" by (simp add: assms(1) homotopic_with_symD) moreover have "homotopic_with_canon (\x. True) T T (r \ id) id" using r unfolding retraction_def by (metis eq_id_iff homotopic_with_id2 topspace_euclidean_subtopology) ultimately show ?thesis unfolding homotopy_equivalent_space_def by (metis (no_types, lifting) continuous_map_subtopology_eu continuous_on_id' id_def image_id r retraction_def) qed lemma deformation_retract: fixes S :: "'a::euclidean_space set" shows "(\r. homotopic_with_canon (\x. True) S S id r \ retraction S T r) \ T retract_of S \ (\f. homotopic_with_canon (\x. True) S S id f \ f ` S \ T)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (auto simp: retract_of_def retraction_def) next assume ?rhs then show ?lhs apply (clarsimp simp add: retract_of_def retraction_def) apply (rule_tac x=r in exI, simp) apply (rule homotopic_with_trans, assumption) apply (rule_tac f = "r \ f" and g="r \ id" in homotopic_with_eq) apply (rule_tac Y=S in homotopic_compose_continuous_left) apply (auto simp: homotopic_with_sym) done qed lemma deformation_retract_of_contractible_sing: fixes S :: "'a::euclidean_space set" assumes "contractible S" "a \ S" obtains r where "homotopic_with_canon (\x. True) S S id r" "retraction S {a} r" proof - have "{a} retract_of S" by (simp add: \a \ S\) moreover have "homotopic_with_canon (\x. True) S S id (\x. a)" using assms by (auto simp: contractible_def homotopic_into_contractible image_subset_iff) moreover have "(\x. a) ` S \ {a}" by (simp add: image_subsetI) ultimately show ?thesis using that deformation_retract by metis qed lemma continuous_on_compact_surface_projection_aux: fixes S :: "'a::t2_space set" assumes "compact S" "S \ T" "image q T \ S" and contp: "continuous_on T p" and "\x. x \ S \ q x = x" and [simp]: "\x. x \ T \ q(p x) = q x" and "\x. x \ T \ p(q x) = p x" shows "continuous_on T q" proof - have *: "image p T = image p S" using assms by auto (metis imageI subset_iff) have contp': "continuous_on S p" by (rule continuous_on_subset [OF contp \S \ T\]) have "continuous_on (p ` T) q" by (simp add: "*" assms(1) assms(2) assms(5) continuous_on_inv contp' rev_subsetD) then have "continuous_on T (q \ p)" by (rule continuous_on_compose [OF contp]) then show ?thesis by (rule continuous_on_eq [of _ "q \ p"]) (simp add: o_def) qed lemma continuous_on_compact_surface_projection: fixes S :: "'a::real_normed_vector set" assumes "compact S" and S: "S \ V - {0}" and "cone V" and iff: "\x k. x \ V - {0} \ 0 < k \ (k *\<^sub>R x) \ S \ d x = k" shows "continuous_on (V - {0}) (\x. d x *\<^sub>R x)" proof (rule continuous_on_compact_surface_projection_aux [OF \compact S\ S]) show "(\x. d x *\<^sub>R x) ` (V - {0}) \ S" using iff by auto show "continuous_on (V - {0}) (\x. inverse(norm x) *\<^sub>R x)" by (intro continuous_intros) force show "\x. x \ S \ d x *\<^sub>R x = x" by (metis S zero_less_one local.iff scaleR_one subset_eq) show "d (x /\<^sub>R norm x) *\<^sub>R (x /\<^sub>R norm x) = d x *\<^sub>R x" if "x \ V - {0}" for x using iff [of "inverse(norm x) *\<^sub>R x" "norm x * d x", symmetric] iff that \cone V\ by (simp add: field_simps cone_def zero_less_mult_iff) show "d x *\<^sub>R x /\<^sub>R norm (d x *\<^sub>R x) = x /\<^sub>R norm x" if "x \ V - {0}" for x proof - have "0 < d x" using local.iff that by blast then show ?thesis by simp qed qed subsection \Kuhn Simplices\ lemma bij_betw_singleton_eq: assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a \ A" assumes eq: "(\x. x \ A \ x \ a \ f x = g x)" shows "f a = g a" proof - have "f ` (A - {a}) = g ` (A - {a})" by (intro image_cong) (simp_all add: eq) then have "B - {f a} = B - {g a}" using f g a by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff) moreover have "f a \ B" "g a \ B" using f g a by (auto simp: bij_betw_def) ultimately show ?thesis by auto qed lemma swap_image: "Fun.swap i j f ` A = (if i \ A then (if j \ A then f ` A else f ` ((A - {i}) \ {j})) else (if j \ A then f ` ((A - {j}) \ {i}) else f ` A))" by (auto simp: swap_def cong: image_cong_simp) lemmas swap_apply1 = swap_apply(1) lemmas swap_apply2 = swap_apply(2) lemma pointwise_minimal_pointwise_maximal: fixes s :: "(nat \ nat) set" assumes "finite s" and "s \ {}" and "\x\s. \y\s. x \ y \ y \ x" shows "\a\s. \x\s. a \ x" and "\a\s. \x\s. x \ a" using assms proof (induct s rule: finite_ne_induct) case (insert b s) assume *: "\x\insert b s. \y\insert b s. x \ y \ y \ x" then obtain u l where "l \ s" "\b\s. l \ b" "u \ s" "\b\s. b \ u" using insert by auto with * show "\a\insert b s. \x\insert b s. a \ x" "\a\insert b s. \x\insert b s. x \ a" using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+ qed auto lemma kuhn_labelling_lemma: fixes P Q :: "'a::euclidean_space \ bool" assumes "\x. P x \ P (f x)" and "\x. P x \ (\i\Basis. Q i \ 0 \ x\i \ x\i \ 1)" shows "\l. (\x.\i\Basis. l x i \ (1::nat)) \ (\x.\i\Basis. P x \ Q i \ (x\i = 0) \ (l x i = 0)) \ (\x.\i\Basis. P x \ Q i \ (x\i = 1) \ (l x i = 1)) \ (\x.\i\Basis. P x \ Q i \ (l x i = 0) \ x\i \ f x\i) \ (\x.\i\Basis. P x \ Q i \ (l x i = 1) \ f x\i \ x\i)" proof - { fix x i let ?R = "\y. (P x \ Q i \ x \ i = 0 \ y = (0::nat)) \ (P x \ Q i \ x \ i = 1 \ y = 1) \ (P x \ Q i \ y = 0 \ x \ i \ f x \ i) \ (P x \ Q i \ y = 1 \ f x \ i \ x \ i)" { assume "P x" "Q i" "i \ Basis" with assms have "0 \ f x \ i \ f x \ i \ 1" by auto } then have "i \ Basis \ ?R 0 \ ?R 1" by auto } then show ?thesis unfolding all_conj_distrib[symmetric] Ball_def (* FIXME: shouldn't this work by metis? *) by (subst choice_iff[symmetric])+ blast qed subsubsection \The key "counting" observation, somewhat abstracted\ lemma kuhn_counting_lemma: fixes bnd compo compo' face S F defines "nF s == card {f\F. face f s \ compo' f}" assumes [simp, intro]: "finite F" \ \faces\ and [simp, intro]: "finite S" \ \simplices\ and "\f. f \ F \ bnd f \ card {s\S. face f s} = 1" and "\f. f \ F \ \ bnd f \ card {s\S. face f s} = 2" and "\s. s \ S \ compo s \ nF s = 1" and "\s. s \ S \ \ compo s \ nF s = 0 \ nF s = 2" and "odd (card {f\F. compo' f \ bnd f})" shows "odd (card {s\S. compo s})" proof - have "(\s | s \ S \ \ compo s. nF s) + (\s | s \ S \ compo s. nF s) = (\s\S. nF s)" by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong) also have "\ = (\s\S. card {f \ {f\F. compo' f \ bnd f}. face f s}) + (\s\S. card {f \ {f\F. compo' f \ \ bnd f}. face f s})" unfolding sum.distrib[symmetric] by (subst card_Un_disjoint[symmetric]) (auto simp: nF_def intro!: sum.cong arg_cong[where f=card]) also have "\ = 1 * card {f\F. compo' f \ bnd f} + 2 * card {f\F. compo' f \ \ bnd f}" using assms(4,5) by (fastforce intro!: arg_cong2[where f="(+)"] sum_multicount) finally have "odd ((\s | s \ S \ \ compo s. nF s) + card {s\S. compo s})" using assms(6,8) by simp moreover have "(\s | s \ S \ \ compo s. nF s) = (\s | s \ S \ \ compo s \ nF s = 0. nF s) + (\s | s \ S \ \ compo s \ nF s = 2. nF s)" using assms(7) by (subst sum.union_disjoint[symmetric]) (fastforce intro!: sum.cong)+ ultimately show ?thesis by auto qed subsubsection \The odd/even result for faces of complete vertices, generalized\ lemma kuhn_complete_lemma: assumes [simp]: "finite simplices" and face: "\f s. face f s \ (\a\s. f = s - {a})" and card_s[simp]: "\s. s \ simplices \ card s = n + 2" and rl_bd: "\s. s \ simplices \ rl ` s \ {..Suc n}" and bnd: "\f s. s \ simplices \ face f s \ bnd f \ card {s\simplices. face f s} = 1" and nbnd: "\f s. s \ simplices \ face f s \ \ bnd f \ card {s\simplices. face f s} = 2" and odd_card: "odd (card {f. (\s\simplices. face f s) \ rl ` f = {..n} \ bnd f})" shows "odd (card {s\simplices. (rl ` s = {..Suc n})})" proof (rule kuhn_counting_lemma) have finite_s[simp]: "\s. s \ simplices \ finite s" by (metis add_is_0 zero_neq_numeral card_infinite assms(3)) let ?F = "{f. \s\simplices. face f s}" have F_eq: "?F = (\s\simplices. \a\s. {s - {a}})" by (auto simp: face) show "finite ?F" using \finite simplices\ unfolding F_eq by auto show "card {s \ simplices. face f s} = 1" if "f \ ?F" "bnd f" for f using bnd that by auto show "card {s \ simplices. face f s} = 2" if "f \ ?F" "\ bnd f" for f using nbnd that by auto show "odd (card {f \ {f. \s\simplices. face f s}. rl ` f = {..n} \ bnd f})" using odd_card by simp fix s assume s[simp]: "s \ simplices" let ?S = "{f \ {f. \s\simplices. face f s}. face f s \ rl ` f = {..n}}" have "?S = (\a. s - {a}) ` {a\s. rl ` (s - {a}) = {..n}}" using s by (fastforce simp: face) then have card_S: "card ?S = card {a\s. rl ` (s - {a}) = {..n}}" by (auto intro!: card_image inj_onI) { assume rl: "rl ` s = {..Suc n}" then have inj_rl: "inj_on rl s" by (intro eq_card_imp_inj_on) auto moreover obtain a where "rl a = Suc n" "a \ s" by (metis atMost_iff image_iff le_Suc_eq rl) ultimately have n: "{..n} = rl ` (s - {a})" by (auto simp: inj_on_image_set_diff rl) have "{a\s. rl ` (s - {a}) = {..n}} = {a}" using inj_rl \a \ s\ by (auto simp: n inj_on_image_eq_iff[OF inj_rl]) then show "card ?S = 1" unfolding card_S by simp } { assume rl: "rl ` s \ {..Suc n}" show "card ?S = 0 \ card ?S = 2" proof cases assume *: "{..n} \ rl ` s" with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}" by (auto simp: atMost_Suc subset_insert_iff split: if_split_asm) then have "\ inj_on rl s" by (intro pigeonhole) simp then obtain a b where ab: "a \ s" "b \ s" "rl a = rl b" "a \ b" by (auto simp: inj_on_def) then have eq: "rl ` (s - {a}) = rl ` s" by auto with ab have inj: "inj_on rl (s - {a})" by (intro eq_card_imp_inj_on) (auto simp: rl_s card_Diff_singleton_if) { fix x assume "x \ s" "x \ {a, b}" then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})" by (auto simp: eq inj_on_image_set_diff[OF inj]) also have "\ = rl ` (s - {x})" using ab \x \ {a, b}\ by auto also assume "\ = rl ` s" finally have False using \x\s\ by auto } moreover { fix x assume "x \ {a, b}" with ab have "x \ s \ rl ` (s - {x}) = rl ` s" by (simp add: set_eq_iff image_iff Bex_def) metis } ultimately have "{a\s. rl ` (s - {a}) = {..n}} = {a, b}" unfolding rl_s[symmetric] by fastforce with \a \ b\ show "card ?S = 0 \ card ?S = 2" unfolding card_S by simp next assume "\ {..n} \ rl ` s" then have "\x. rl ` (s - {x}) \ {..n}" by auto then show "card ?S = 0 \ card ?S = 2" unfolding card_S by simp qed } qed fact locale kuhn_simplex = fixes p n and base upd and s :: "(nat \ nat) set" assumes base: "base \ {..< n} \ {..< p}" assumes base_out: "\i. n \ i \ base i = p" assumes upd: "bij_betw upd {..< n} {..< n}" assumes s_pre: "s = (\i j. if j \ upd`{..< i} then Suc (base j) else base j) ` {.. n}" begin definition "enum i j = (if j \ upd`{..< i} then Suc (base j) else base j)" lemma s_eq: "s = enum ` {.. n}" unfolding s_pre enum_def[abs_def] .. lemma upd_space: "i < n \ upd i < n" using upd by (auto dest!: bij_betwE) lemma s_space: "s \ {..< n} \ {.. p}" proof - { fix i assume "i \ n" then have "enum i \ {..< n} \ {.. p}" proof (induct i) case 0 then show ?case using base by (auto simp: Pi_iff less_imp_le enum_def) next case (Suc i) with base show ?case by (auto simp: Pi_iff Suc_le_eq less_imp_le enum_def intro: upd_space) qed } then show ?thesis by (auto simp: s_eq) qed lemma inj_upd: "inj_on upd {..< n}" using upd by (simp add: bij_betw_def) lemma inj_enum: "inj_on enum {.. n}" proof - { fix x y :: nat assume "x \ y" "x \ n" "y \ n" with upd have "upd ` {..< x} \ upd ` {..< y}" by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def) then have "enum x \ enum y" by (auto simp: enum_def fun_eq_iff) } then show ?thesis by (auto simp: inj_on_def) qed lemma enum_0: "enum 0 = base" by (simp add: enum_def[abs_def]) lemma base_in_s: "base \ s" unfolding s_eq by (subst enum_0[symmetric]) auto lemma enum_in: "i \ n \ enum i \ s" unfolding s_eq by auto lemma one_step: assumes a: "a \ s" "j < n" assumes *: "\a'. a' \ s \ a' \ a \ a' j = p'" shows "a j \ p'" proof assume "a j = p'" with * a have "\a'. a' \ s \ a' j = p'" by auto then have "\i. i \ n \ enum i j = p'" unfolding s_eq by auto from this[of 0] this[of n] have "j \ upd ` {..< n}" by (auto simp: enum_def fun_eq_iff split: if_split_asm) with upd \j < n\ show False by (auto simp: bij_betw_def) qed lemma upd_inj: "i < n \ j < n \ upd i = upd j \ i = j" using upd by (auto simp: bij_betw_def inj_on_eq_iff) lemma upd_surj: "upd ` {..< n} = {..< n}" using upd by (auto simp: bij_betw_def) lemma in_upd_image: "A \ {..< n} \ i < n \ upd i \ upd ` A \ i \ A" using inj_on_image_mem_iff[of upd "{..< n}"] upd by (auto simp: bij_betw_def) lemma enum_inj: "i \ n \ j \ n \ enum i = enum j \ i = j" using inj_enum by (auto simp: inj_on_eq_iff) lemma in_enum_image: "A \ {.. n} \ i \ n \ enum i \ enum ` A \ i \ A" using inj_on_image_mem_iff[OF inj_enum] by auto lemma enum_mono: "i \ n \ j \ n \ enum i \ enum j \ i \ j" by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric]) lemma enum_strict_mono: "i \ n \ j \ n \ enum i < enum j \ i < j" using enum_mono[of i j] enum_inj[of i j] by (auto simp: le_less) lemma chain: "a \ s \ b \ s \ a \ b \ b \ a" by (auto simp: s_eq enum_mono) lemma less: "a \ s \ b \ s \ a i < b i \ a < b" using chain[of a b] by (auto simp: less_fun_def le_fun_def not_le[symmetric]) lemma enum_0_bot: "a \ s \ a = enum 0 \ (\a'\s. a \ a')" unfolding s_eq by (auto simp: enum_mono Ball_def) lemma enum_n_top: "a \ s \ a = enum n \ (\a'\s. a' \ a)" unfolding s_eq by (auto simp: enum_mono Ball_def) lemma enum_Suc: "i < n \ enum (Suc i) = (enum i)(upd i := Suc (enum i (upd i)))" by (auto simp: fun_eq_iff enum_def upd_inj) lemma enum_eq_p: "i \ n \ n \ j \ enum i j = p" by (induct i) (auto simp: enum_Suc enum_0 base_out upd_space not_less[symmetric]) lemma out_eq_p: "a \ s \ n \ j \ a j = p" unfolding s_eq by (auto simp: enum_eq_p) lemma s_le_p: "a \ s \ a j \ p" using out_eq_p[of a j] s_space by (cases "j < n") auto lemma le_Suc_base: "a \ s \ a j \ Suc (base j)" unfolding s_eq by (auto simp: enum_def) lemma base_le: "a \ s \ base j \ a j" unfolding s_eq by (auto simp: enum_def) lemma enum_le_p: "i \ n \ j < n \ enum i j \ p" using enum_in[of i] s_space by auto lemma enum_less: "a \ s \ i < n \ enum i < a \ enum (Suc i) \ a" unfolding s_eq by (auto simp: enum_strict_mono enum_mono) lemma ksimplex_0: "n = 0 \ s = {(\x. p)}" using s_eq enum_def base_out by auto lemma replace_0: assumes "j < n" "a \ s" and p: "\x\s - {a}. x j = 0" and "x \ s" shows "x \ a" proof cases assume "x \ a" have "a j \ 0" using assms by (intro one_step[where a=a]) auto with less[OF \x\s\ \a\s\, of j] p[rule_format, of x] \x \ s\ \x \ a\ show ?thesis by auto qed simp lemma replace_1: assumes "j < n" "a \ s" and p: "\x\s - {a}. x j = p" and "x \ s" shows "a \ x" proof cases assume "x \ a" have "a j \ p" using assms by (intro one_step[where a=a]) auto with enum_le_p[of _ j] \j < n\ \a\s\ have "a j < p" by (auto simp: less_le s_eq) with less[OF \a\s\ \x\s\, of j] p[rule_format, of x] \x \ s\ \x \ a\ show ?thesis by auto qed simp end locale kuhn_simplex_pair = s: kuhn_simplex p n b_s u_s s + t: kuhn_simplex p n b_t u_t t for p n b_s u_s s b_t u_t t begin lemma enum_eq: assumes l: "i \ l" "l \ j" and "j + d \ n" assumes eq: "s.enum ` {i .. j} = t.enum ` {i + d .. j + d}" shows "s.enum l = t.enum (l + d)" using l proof (induct l rule: dec_induct) case base then have s: "s.enum i \ t.enum ` {i + d .. j + d}" and t: "t.enum (i + d) \ s.enum ` {i .. j}" using eq by auto from t \i \ j\ \j + d \ n\ have "s.enum i \ t.enum (i + d)" by (auto simp: s.enum_mono) moreover from s \i \ j\ \j + d \ n\ have "t.enum (i + d) \ s.enum i" by (auto simp: t.enum_mono) ultimately show ?case by auto next case (step l) moreover from step.prems \j + d \ n\ have "s.enum l < s.enum (Suc l)" "t.enum (l + d) < t.enum (Suc l + d)" by (simp_all add: s.enum_strict_mono t.enum_strict_mono) moreover have "s.enum (Suc l) \ t.enum ` {i + d .. j + d}" "t.enum (Suc l + d) \ s.enum ` {i .. j}" using step \j + d \ n\ eq by (auto simp: s.enum_inj t.enum_inj) ultimately have "s.enum (Suc l) = t.enum (Suc (l + d))" using \j + d \ n\ by (intro antisym s.enum_less[THEN iffD1] t.enum_less[THEN iffD1]) (auto intro!: s.enum_in t.enum_in) then show ?case by simp qed lemma ksimplex_eq_bot: assumes a: "a \ s" "\a'. a' \ s \ a \ a'" assumes b: "b \ t" "\b'. b' \ t \ b \ b'" assumes eq: "s - {a} = t - {b}" shows "s = t" proof cases assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp next assume "n \ 0" have "s.enum 0 = (s.enum (Suc 0)) (u_s 0 := s.enum (Suc 0) (u_s 0) - 1)" "t.enum 0 = (t.enum (Suc 0)) (u_t 0 := t.enum (Suc 0) (u_t 0) - 1)" using \n \ 0\ by (simp_all add: s.enum_Suc t.enum_Suc) moreover have e0: "a = s.enum 0" "b = t.enum 0" using a b by (simp_all add: s.enum_0_bot t.enum_0_bot) moreover { fix j assume "0 < j" "j \ n" moreover have "s - {a} = s.enum ` {Suc 0 .. n}" "t - {b} = t.enum ` {Suc 0 .. n}" unfolding s.s_eq t.s_eq e0 by (auto simp: s.enum_inj t.enum_inj) ultimately have "s.enum j = t.enum j" using enum_eq[of "1" j n 0] eq by auto } note enum_eq = this then have "s.enum (Suc 0) = t.enum (Suc 0)" using \n \ 0\ by auto moreover { fix j assume "Suc j < n" with enum_eq[of "Suc j"] enum_eq[of "Suc (Suc j)"] have "u_s (Suc j) = u_t (Suc j)" using s.enum_Suc[of "Suc j"] t.enum_Suc[of "Suc j"] by (auto simp: fun_eq_iff split: if_split_asm) } then have "\j. 0 < j \ j < n \ u_s j = u_t j" by (auto simp: gr0_conv_Suc) with \n \ 0\ have "u_t 0 = u_s 0" by (intro bij_betw_singleton_eq[OF t.upd s.upd, of 0]) auto ultimately have "a = b" by simp with assms show "s = t" by auto qed lemma ksimplex_eq_top: assumes a: "a \ s" "\a'. a' \ s \ a' \ a" assumes b: "b \ t" "\b'. b' \ t \ b' \ b" assumes eq: "s - {a} = t - {b}" shows "s = t" proof (cases n) assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp next case (Suc n') have "s.enum n = (s.enum n') (u_s n' := Suc (s.enum n' (u_s n')))" "t.enum n = (t.enum n') (u_t n' := Suc (t.enum n' (u_t n')))" using Suc by (simp_all add: s.enum_Suc t.enum_Suc) moreover have en: "a = s.enum n" "b = t.enum n" using a b by (simp_all add: s.enum_n_top t.enum_n_top) moreover { fix j assume "j < n" moreover have "s - {a} = s.enum ` {0 .. n'}" "t - {b} = t.enum ` {0 .. n'}" unfolding s.s_eq t.s_eq en by (auto simp: s.enum_inj t.enum_inj Suc) ultimately have "s.enum j = t.enum j" using enum_eq[of "0" j n' 0] eq Suc by auto } note enum_eq = this then have "s.enum n' = t.enum n'" using Suc by auto moreover { fix j assume "j < n'" with enum_eq[of j] enum_eq[of "Suc j"] have "u_s j = u_t j" using s.enum_Suc[of j] t.enum_Suc[of j] by (auto simp: Suc fun_eq_iff split: if_split_asm) } then have "\j. j < n' \ u_s j = u_t j" by (auto simp: gr0_conv_Suc) then have "u_t n' = u_s n'" by (intro bij_betw_singleton_eq[OF t.upd s.upd, of n']) (auto simp: Suc) ultimately have "a = b" by simp with assms show "s = t" by auto qed end inductive ksimplex for p n :: nat where ksimplex: "kuhn_simplex p n base upd s \ ksimplex p n s" lemma finite_ksimplexes: "finite {s. ksimplex p n s}" proof (rule finite_subset) { fix a s assume "ksimplex p n s" "a \ s" then obtain b u where "kuhn_simplex p n b u s" by (auto elim: ksimplex.cases) then interpret kuhn_simplex p n b u s . from s_space \a \ s\ out_eq_p[OF \a \ s\] have "a \ (\f x. if n \ x then p else f x) ` ({..< n} \\<^sub>E {.. p})" by (auto simp: image_iff subset_eq Pi_iff split: if_split_asm intro!: bexI[of _ "restrict a {..< n}"]) } then show "{s. ksimplex p n s} \ Pow ((\f x. if n \ x then p else f x) ` ({..< n} \\<^sub>E {.. p}))" by auto qed (simp add: finite_PiE) lemma ksimplex_card: assumes "ksimplex p n s" shows "card s = Suc n" using assms proof cases case (ksimplex u b) then interpret kuhn_simplex p n u b s . show ?thesis by (simp add: card_image s_eq inj_enum) qed lemma simplex_top_face: assumes "0 < p" "\x\s'. x n = p" shows "ksimplex p n s' \ (\s a. ksimplex p (Suc n) s \ a \ s \ s' = s - {a})" using assms proof safe fix s a assume "ksimplex p (Suc n) s" and a: "a \ s" and na: "\x\s - {a}. x n = p" then show "ksimplex p n (s - {a})" proof cases case (ksimplex base upd) then interpret kuhn_simplex p "Suc n" base upd "s" . have "a n < p" using one_step[of a n p] na \a\s\ s_space by (auto simp: less_le) then have "a = enum 0" using \a \ s\ na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n]) then have s_eq: "s - {a} = enum ` Suc ` {.. n}" using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident in_enum_image subset_eq) then have "enum 1 \ s - {a}" by auto then have "upd 0 = n" using \a n < p\ \a = enum 0\ na[rule_format, of "enum 1"] by (auto simp: fun_eq_iff enum_Suc split: if_split_asm) then have "bij_betw upd (Suc ` {..< n}) {..< n}" using upd by (subst notIn_Un_bij_betw3[where b=0]) (auto simp: lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0) then have "bij_betw (upd\Suc) {..enum 1 \ s - {a}\] \a = enum 0\ by (auto simp: \upd 0 = n\) show ?thesis proof (rule ksimplex.intros, standard) show "bij_betw (upd\Suc) {..< n} {..< n}" by fact show "base(n := p) \ {.. {..i. n\i \ (base(n := p)) i = p" using base base_out by (auto simp: Pi_iff) have "\i. Suc ` {..< i} = {..< Suc i} - {0}" by (auto simp: image_iff Ball_def) arith then have upd_Suc: "\i. i \ n \ (upd\Suc) ` {..< i} = upd ` {..< Suc i} - {n}" using \upd 0 = n\ upd_inj by (auto simp add: image_iff less_Suc_eq_0_disj) have n_in_upd: "\i. n \ upd ` {..< Suc i}" using \upd 0 = n\ by auto define f' where "f' i j = (if j \ (upd\Suc)`{..< i} then Suc ((base(n := p)) j) else (base(n := p)) j)" for i j { fix x i assume i [arith]: "i \ n" with upd_Suc have "(upd \ Suc) ` {..a n < p\ \a = enum 0\ \upd 0 = n\ \a n = p - 1\ have "enum (Suc i) x = f' i x" by (auto simp add: f'_def enum_def) } then show "s - {a} = f' ` {.. n}" unfolding s_eq image_comp by (intro image_cong) auto qed qed next assume "ksimplex p n s'" and *: "\x\s'. x n = p" then show "\s a. ksimplex p (Suc n) s \ a \ s \ s' = s - {a}" proof cases case (ksimplex base upd) then interpret kuhn_simplex p n base upd s' . define b where "b = base (n := p - 1)" define u where "u i = (case i of 0 \ n | Suc i \ upd i)" for i have "ksimplex p (Suc n) (s' \ {b})" proof (rule ksimplex.intros, standard) show "b \ {.. {..0 < p\ unfolding lessThan_Suc b_def by (auto simp: PiE_iff) show "\i. Suc n \ i \ b i = p" using base_out by (auto simp: b_def) have "bij_betw u (Suc ` {..< n} \ {0}) ({.. {u 0})" using upd by (intro notIn_Un_bij_betw) (auto simp: u_def bij_betw_def image_comp comp_def inj_on_def) then show "bij_betw u {.. u`{..< i} then Suc (b j) else b j)" for i j have u_eq: "\i. i \ n \ u ` {..< Suc i} = upd ` {..< i} \ { n }" by (auto simp: u_def image_iff upd_inj Ball_def split: nat.split) arith { fix x have "x \ n \ n \ upd ` {.. {0})" unfolding atMost_Suc_eq_insert_0 by simp also have "\ = (f' \ Suc) ` {.. n} \ {b}" by (auto simp: f'_def) also have "(f' \ Suc) ` {.. n} = s'" using \0 < p\ base_out[of n] unfolding s_eq enum_def[abs_def] f'_def[abs_def] upd_space by (intro image_cong) (simp_all add: u_eq b_def fun_eq_iff n_not_upd) finally show "s' \ {b} = f' ` {.. Suc n}" .. qed moreover have "b \ s'" using * \0 < p\ by (auto simp: b_def) ultimately show ?thesis by auto qed qed lemma ksimplex_replace_0: assumes s: "ksimplex p n s" and a: "a \ s" assumes j: "j < n" and p: "\x\s - {a}. x j = 0" shows "card {s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = 1" using s proof cases case (ksimplex b_s u_s) { fix t b assume "ksimplex p n t" then obtain b_t u_t where "kuhn_simplex p n b_t u_t t" by (auto elim: ksimplex.cases) interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t by intro_locales fact+ assume b: "b \ t" "t - {b} = s - {a}" with a j p s.replace_0[of _ a] t.replace_0[of _ b] have "s = t" by (intro ksimplex_eq_top[of a b]) auto } then have "{s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = {s}" using s \a \ s\ by auto then show ?thesis by simp qed lemma ksimplex_replace_1: assumes s: "ksimplex p n s" and a: "a \ s" assumes j: "j < n" and p: "\x\s - {a}. x j = p" shows "card {s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = 1" using s proof cases case (ksimplex b_s u_s) { fix t b assume "ksimplex p n t" then obtain b_t u_t where "kuhn_simplex p n b_t u_t t" by (auto elim: ksimplex.cases) interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t by intro_locales fact+ assume b: "b \ t" "t - {b} = s - {a}" with a j p s.replace_1[of _ a] t.replace_1[of _ b] have "s = t" by (intro ksimplex_eq_bot[of a b]) auto } then have "{s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = {s}" using s \a \ s\ by auto then show ?thesis by simp qed -lemma card_2_exists: "card s = 2 \ (\x\s. \y\s. x \ y \ (\z\s. z = x \ z = y))" - by (auto simp: card_Suc_eq eval_nat_numeral) - lemma ksimplex_replace_2: assumes s: "ksimplex p n s" and "a \ s" and "n \ 0" and lb: "\jx\s - {a}. x j \ 0" and ub: "\jx\s - {a}. x j \ p" shows "card {s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = 2" using s proof cases case (ksimplex base upd) then interpret kuhn_simplex p n base upd s . from \a \ s\ obtain i where "i \ n" "a = enum i" unfolding s_eq by auto from \i \ n\ have "i = 0 \ i = n \ (0 < i \ i < n)" by linarith then have "\!s'. s' \ s \ ksimplex p n s' \ (\b\s'. s - {a} = s'- {b})" proof (elim disjE conjE) assume "i = 0" define rot where [abs_def]: "rot i = (if i + 1 = n then 0 else i + 1)" for i let ?upd = "upd \ rot" have rot: "bij_betw rot {..< n} {..< n}" by (auto simp: bij_betw_def inj_on_def image_iff Ball_def rot_def) arith+ from rot upd have "bij_betw ?upd {.. ?upd`{..< i} then Suc (enum (Suc 0) j) else enum (Suc 0) j)" for i j interpret b: kuhn_simplex p n "enum (Suc 0)" "upd \ rot" "f' ` {.. n}" proof from \a = enum i\ ub \n \ 0\ \i = 0\ obtain i' where "i' \ n" "enum i' \ enum 0" "enum i' (upd 0) \ p" unfolding s_eq by (auto intro: upd_space simp: enum_inj) then have "enum 1 \ enum i'" "enum i' (upd 0) < p" using enum_le_p[of i' "upd 0"] by (auto simp: enum_inj enum_mono upd_space) then have "enum 1 (upd 0) < p" by (auto simp: le_fun_def intro: le_less_trans) then show "enum (Suc 0) \ {.. {..n \ 0\ by (auto simp: enum_0 enum_Suc PiE_iff extensional_def upd_space) { fix i assume "n \ i" then show "enum (Suc 0) i = p" using \n \ 0\ by (auto simp: enum_eq_p) } show "bij_betw ?upd {..n \ 0\ show ?thesis by (simp only: f'_def enum_def fun_eq_iff image_comp [symmetric]) (auto simp add: upd_inj) qed then have "enum ` Suc ` {..< n} = f' ` {..< n}" by (force simp: enum_inj) also have "Suc ` {..< n} = {.. n} - {0}" by (auto simp: image_iff Ball_def) arith also have "{..< n} = {.. n} - {n}" by auto finally have eq: "s - {a} = f' ` {.. n} - {f' n}" unfolding s_eq \a = enum i\ \i = 0\ by (simp add: inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f']) have "enum 0 < f' 0" using \n \ 0\ by (simp add: enum_strict_mono f'_eq_enum) also have "\ < f' n" using \n \ 0\ b.enum_strict_mono[of 0 n] unfolding b_enum by simp finally have "a \ f' n" using \a = enum i\ \i = 0\ by auto { fix t c assume "ksimplex p n t" "c \ t" and eq_sma: "s - {a} = t - {c}" obtain b u where "kuhn_simplex p n b u t" using \ksimplex p n t\ by (auto elim: ksimplex.cases) then interpret t: kuhn_simplex p n b u t . { fix x assume "x \ s" "x \ a" then have "x (upd 0) = enum (Suc 0) (upd 0)" by (auto simp: \a = enum i\ \i = 0\ s_eq enum_def enum_inj) } then have eq_upd0: "\x\t-{c}. x (upd 0) = enum (Suc 0) (upd 0)" unfolding eq_sma[symmetric] by auto then have "c (upd 0) \ enum (Suc 0) (upd 0)" using \n \ 0\ by (intro t.one_step[OF \c\t\ ]) (auto simp: upd_space) then have "c (upd 0) < enum (Suc 0) (upd 0) \ c (upd 0) > enum (Suc 0) (upd 0)" by auto then have "t = s \ t = f' ` {..n}" proof (elim disjE conjE) assume *: "c (upd 0) < enum (Suc 0) (upd 0)" interpret st: kuhn_simplex_pair p n base upd s b u t .. { fix x assume "x \ t" with * \c\t\ eq_upd0[rule_format, of x] have "c \ x" by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) } note top = this have "s = t" using \a = enum i\ \i = 0\ \c \ t\ by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq_sma]) (auto simp: s_eq enum_mono t.s_eq t.enum_mono top) then show ?thesis by simp next assume *: "c (upd 0) > enum (Suc 0) (upd 0)" interpret st: kuhn_simplex_pair p n "enum (Suc 0)" "upd \ rot" "f' ` {.. n}" b u t .. have eq: "f' ` {..n} - {f' n} = t - {c}" using eq_sma eq by simp { fix x assume "x \ t" with * \c\t\ eq_upd0[rule_format, of x] have "x \ c" by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) } note top = this have "f' ` {..n} = t" using \a = enum i\ \i = 0\ \c \ t\ by (intro st.ksimplex_eq_top[OF _ _ _ _ eq]) (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono b_enum[symmetric] top) then show ?thesis by simp qed } with ks_f' eq \a \ f' n\ \n \ 0\ show ?thesis apply (intro ex1I[of _ "f' ` {.. n}"]) apply auto [] apply metis done next assume "i = n" from \n \ 0\ obtain n' where n': "n = Suc n'" by (cases n) auto define rot where "rot i = (case i of 0 \ n' | Suc i \ i)" for i let ?upd = "upd \ rot" have rot: "bij_betw rot {..< n} {..< n}" by (auto simp: bij_betw_def inj_on_def image_iff Bex_def rot_def n' split: nat.splits) arith from rot upd have "bij_betw ?upd {.. ?upd`{..< i} then Suc (b j) else b j)" for i j interpret b: kuhn_simplex p n b "upd \ rot" "f' ` {.. n}" proof { fix i assume "n \ i" then show "b i = p" using base_out[of i] upd_space[of n'] by (auto simp: b_def n') } show "b \ {.. {..n \ 0\ upd_space[of n'] by (auto simp: b_def PiE_def Pi_iff Ball_def upd_space extensional_def n') show "bij_betw ?upd {..n \ 0\ by auto { from \a = enum i\ \n \ 0\ \i = n\ lb upd_space[of n'] obtain i' where "i' \ n" "enum i' \ enum n" "0 < enum i' (upd n')" unfolding s_eq by (auto simp: enum_inj n') moreover have "enum i' (upd n') = base (upd n')" unfolding enum_def using \i' \ n\ \enum i' \ enum n\ by (auto simp: n' upd_inj enum_inj) ultimately have "0 < base (upd n')" by auto } then have benum1: "b.enum (Suc 0) = base" unfolding b.enum_Suc[OF \0] b.enum_0 by (auto simp: b_def rot_def) have [simp]: "\j. Suc j < n \ rot ` {..< Suc j} = {n'} \ {..< j}" by (auto simp: rot_def image_iff Ball_def split: nat.splits) have rot_simps: "\j. rot (Suc j) = j" "rot 0 = n'" by (simp_all add: rot_def) { fix j assume j: "Suc j \ n" then have "b.enum (Suc j) = enum j" by (induct j) (auto simp: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) } note b_enum_eq_enum = this then have "enum ` {..< n} = b.enum ` Suc ` {..< n}" by (auto simp: image_comp intro!: image_cong) also have "Suc ` {..< n} = {.. n} - {0}" by (auto simp: image_iff Ball_def) arith also have "{..< n} = {.. n} - {n}" by auto finally have eq: "s - {a} = b.enum ` {.. n} - {b.enum 0}" unfolding s_eq \a = enum i\ \i = n\ using inj_on_image_set_diff[OF inj_enum Diff_subset, of "{n}"] inj_on_image_set_diff[OF b.inj_enum Diff_subset, of "{0}"] by (simp add: comp_def) have "b.enum 0 \ b.enum n" by (simp add: b.enum_mono) also have "b.enum n < enum n" using \n \ 0\ by (simp add: enum_strict_mono b_enum_eq_enum n') finally have "a \ b.enum 0" using \a = enum i\ \i = n\ by auto { fix t c assume "ksimplex p n t" "c \ t" and eq_sma: "s - {a} = t - {c}" obtain b' u where "kuhn_simplex p n b' u t" using \ksimplex p n t\ by (auto elim: ksimplex.cases) then interpret t: kuhn_simplex p n b' u t . { fix x assume "x \ s" "x \ a" then have "x (upd n') = enum n' (upd n')" by (auto simp: \a = enum i\ n' \i = n\ s_eq enum_def enum_inj in_upd_image) } then have eq_upd0: "\x\t-{c}. x (upd n') = enum n' (upd n')" unfolding eq_sma[symmetric] by auto then have "c (upd n') \ enum n' (upd n')" using \n \ 0\ by (intro t.one_step[OF \c\t\ ]) (auto simp: n' upd_space[unfolded n']) then have "c (upd n') < enum n' (upd n') \ c (upd n') > enum n' (upd n')" by auto then have "t = s \ t = b.enum ` {..n}" proof (elim disjE conjE) assume *: "c (upd n') > enum n' (upd n')" interpret st: kuhn_simplex_pair p n base upd s b' u t .. { fix x assume "x \ t" with * \c\t\ eq_upd0[rule_format, of x] have "x \ c" by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) } note top = this have "s = t" using \a = enum i\ \i = n\ \c \ t\ by (intro st.ksimplex_eq_top[OF _ _ _ _ eq_sma]) (auto simp: s_eq enum_mono t.s_eq t.enum_mono top) then show ?thesis by simp next assume *: "c (upd n') < enum n' (upd n')" interpret st: kuhn_simplex_pair p n b "upd \ rot" "f' ` {.. n}" b' u t .. have eq: "f' ` {..n} - {b.enum 0} = t - {c}" using eq_sma eq f' by simp { fix x assume "x \ t" with * \c\t\ eq_upd0[rule_format, of x] have "c \ x" by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) } note bot = this have "f' ` {..n} = t" using \a = enum i\ \i = n\ \c \ t\ by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq]) (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono bot) with f' show ?thesis by simp qed } with ks_f' eq \a \ b.enum 0\ \n \ 0\ show ?thesis apply (intro ex1I[of _ "b.enum ` {.. n}"]) apply auto [] apply metis done next assume i: "0 < i" "i < n" define i' where "i' = i - 1" with i have "Suc i' < n" by simp with i have Suc_i': "Suc i' = i" by (simp add: i'_def) let ?upd = "Fun.swap i' i upd" from i upd have "bij_betw ?upd {..< n} {..< n}" by (subst bij_betw_swap_iff) (auto simp: i'_def) define f' where [abs_def]: "f' i j = (if j \ ?upd`{..< i} then Suc (base j) else base j)" for i j interpret b: kuhn_simplex p n base ?upd "f' ` {.. n}" proof show "base \ {.. {.. i" then show "base i = p" by (rule base_out) } show "bij_betw ?upd {.. {..n}" using i by auto { fix j assume "j \ n" moreover have "j < i \ i = j \ i < j" by arith moreover note i ultimately have "enum j = b.enum j \ j \ i" unfolding enum_def[abs_def] b.enum_def[abs_def] by (auto simp: fun_eq_iff swap_image i'_def in_upd_image inj_on_image_set_diff[OF inj_upd]) } note enum_eq_benum = this then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})" by (intro image_cong) auto then have eq: "s - {a} = b.enum ` {.. n} - {b.enum i}" unfolding s_eq \a = enum i\ using inj_on_image_set_diff[OF inj_enum Diff_subset \{i} \ {..n}\] inj_on_image_set_diff[OF b.inj_enum Diff_subset \{i} \ {..n}\] by (simp add: comp_def) have "a \ b.enum i" using \a = enum i\ enum_eq_benum i by auto { fix t c assume "ksimplex p n t" "c \ t" and eq_sma: "s - {a} = t - {c}" obtain b' u where "kuhn_simplex p n b' u t" using \ksimplex p n t\ by (auto elim: ksimplex.cases) then interpret t: kuhn_simplex p n b' u t . have "enum i' \ s - {a}" "enum (i + 1) \ s - {a}" using \a = enum i\ i enum_in by (auto simp: enum_inj i'_def) then obtain l k where l: "t.enum l = enum i'" "l \ n" "t.enum l \ c" and k: "t.enum k = enum (i + 1)" "k \ n" "t.enum k \ c" unfolding eq_sma by (auto simp: t.s_eq) with i have "t.enum l < t.enum k" by (simp add: enum_strict_mono i'_def) with \l \ n\ \k \ n\ have "l < k" by (simp add: t.enum_strict_mono) { assume "Suc l = k" have "enum (Suc (Suc i')) = t.enum (Suc l)" using i by (simp add: k \Suc l = k\ i'_def) then have False using \l < k\ \k \ n\ \Suc i' < n\ by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: if_split_asm) (metis Suc_lessD n_not_Suc_n upd_inj) } with \l < k\ have "Suc l < k" by arith have c_eq: "c = t.enum (Suc l)" proof (rule ccontr) assume "c \ t.enum (Suc l)" then have "t.enum (Suc l) \ s - {a}" using \l < k\ \k \ n\ by (simp add: t.s_eq eq_sma) then obtain j where "t.enum (Suc l) = enum j" "j \ n" "enum j \ enum i" unfolding s_eq \a = enum i\ by auto with i have "t.enum (Suc l) \ t.enum l \ t.enum k \ t.enum (Suc l)" by (auto simp: i'_def enum_mono enum_inj l k) with \Suc l < k\ \k \ n\ show False by (simp add: t.enum_mono) qed { have "t.enum (Suc (Suc l)) \ s - {a}" unfolding eq_sma c_eq t.s_eq using \Suc l < k\ \k \ n\ by (auto simp: t.enum_inj) then obtain j where eq: "t.enum (Suc (Suc l)) = enum j" and "j \ n" "j \ i" by (auto simp: s_eq \a = enum i\) moreover have "enum i' < t.enum (Suc (Suc l))" unfolding l(1)[symmetric] using \Suc l < k\ \k \ n\ by (auto simp: t.enum_strict_mono) ultimately have "i' < j" using i by (simp add: enum_strict_mono i'_def) with \j \ i\ \j \ n\ have "t.enum k \ t.enum (Suc (Suc l))" unfolding i'_def by (simp add: enum_mono k eq) then have "k \ Suc (Suc l)" using \k \ n\ \Suc l < k\ by (simp add: t.enum_mono) } with \Suc l < k\ have "Suc (Suc l) = k" by simp then have "enum (Suc (Suc i')) = t.enum (Suc (Suc l))" using i by (simp add: k i'_def) also have "\ = (enum i') (u l := Suc (enum i' (u l)), u (Suc l) := Suc (enum i' (u (Suc l))))" using \Suc l < k\ \k \ n\ by (simp add: t.enum_Suc l t.upd_inj) finally have "(u l = upd i' \ u (Suc l) = upd (Suc i')) \ (u l = upd (Suc i') \ u (Suc l) = upd i')" using \Suc i' < n\ by (auto simp: enum_Suc fun_eq_iff split: if_split_asm) then have "t = s \ t = b.enum ` {..n}" proof (elim disjE conjE) assume u: "u l = upd i'" have "c = t.enum (Suc l)" unfolding c_eq .. also have "t.enum (Suc l) = enum (Suc i')" using u \l < k\ \k \ n\ \Suc i' < n\ by (simp add: enum_Suc t.enum_Suc l) also have "\ = a" using \a = enum i\ i by (simp add: i'_def) finally show ?thesis using eq_sma \a \ s\ \c \ t\ by auto next assume u: "u l = upd (Suc i')" define B where "B = b.enum ` {..n}" have "b.enum i' = enum i'" using enum_eq_benum[of i'] i by (auto simp: i'_def gr0_conv_Suc) have "c = t.enum (Suc l)" unfolding c_eq .. also have "t.enum (Suc l) = b.enum (Suc i')" using u \l < k\ \k \ n\ \Suc i' < n\ by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \b.enum i' = enum i'\) (simp add: Suc_i') also have "\ = b.enum i" using i by (simp add: i'_def) finally have "c = b.enum i" . then have "t - {c} = B - {c}" "c \ B" unfolding eq_sma[symmetric] eq B_def using i by auto with \c \ t\ have "t = B" by auto then show ?thesis by (simp add: B_def) qed } with ks_f' eq \a \ b.enum i\ \n \ 0\ \i \ n\ show ?thesis apply (intro ex1I[of _ "b.enum ` {.. n}"]) apply auto [] apply metis done qed then show ?thesis - using s \a \ s\ by (simp add: card_2_exists Ex1_def) metis + using s \a \ s\ by (simp add: card_2_iff' Ex1_def) metis qed text \Hence another step towards concreteness.\ lemma kuhn_simplex_lemma: assumes "\s. ksimplex p (Suc n) s \ rl ` s \ {.. Suc n}" and "odd (card {f. \s a. ksimplex p (Suc n) s \ a \ s \ (f = s - {a}) \ rl ` f = {..n} \ ((\j\n. \x\f. x j = 0) \ (\j\n. \x\f. x j = p))})" shows "odd (card {s. ksimplex p (Suc n) s \ rl ` s = {..Suc n}})" proof (rule kuhn_complete_lemma[OF finite_ksimplexes refl, unfolded mem_Collect_eq, where bnd="\f. (\j\{..n}. \x\f. x j = 0) \ (\j\{..n}. \x\f. x j = p)"], safe del: notI) have *: "\x y. x = y \ odd (card x) \ odd (card y)" by auto show "odd (card {f. (\s\{s. ksimplex p (Suc n) s}. \a\s. f = s - {a}) \ rl ` f = {..n} \ ((\j\{..n}. \x\f. x j = 0) \ (\j\{..n}. \x\f. x j = p))})" apply (rule *[OF _ assms(2)]) apply (auto simp: atLeast0AtMost) done next fix s assume s: "ksimplex p (Suc n) s" then show "card s = n + 2" by (simp add: ksimplex_card) fix a assume a: "a \ s" then show "rl a \ Suc n" using assms(1) s by (auto simp: subset_eq) let ?S = "{t. ksimplex p (Suc n) t \ (\b\t. s - {a} = t - {b})}" { fix j assume j: "j \ n" "\x\s - {a}. x j = 0" with s a show "card ?S = 1" using ksimplex_replace_0[of p "n + 1" s a j] by (subst eq_commute) simp } { fix j assume j: "j \ n" "\x\s - {a}. x j = p" with s a show "card ?S = 1" using ksimplex_replace_1[of p "n + 1" s a j] by (subst eq_commute) simp } { assume "card ?S \ 2" "\ (\j\{..n}. \x\s - {a}. x j = p)" with s a show "\j\{..n}. \x\s - {a}. x j = 0" using ksimplex_replace_2[of p "n + 1" s a] by (subst (asm) eq_commute) auto } qed subsubsection \Reduced labelling\ definition reduced :: "nat \ (nat \ nat) \ nat" where "reduced n x = (LEAST k. k = n \ x k \ 0)" lemma reduced_labelling: shows "reduced n x \ n" and "\i x (reduced n x) \ 0" proof - show "reduced n x \ n" unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) auto show "\i x (reduced n x) \ 0" unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+ qed lemma reduced_labelling_unique: "r \ n \ \i r = n \ x r \ 0 \ reduced n x = r" unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) (metis le_less not_le)+ lemma reduced_labelling_zero: "j < n \ x j = 0 \ reduced n x \ j" using reduced_labelling[of n x] by auto lemma reduce_labelling_zero[simp]: "reduced 0 x = 0" by (rule reduced_labelling_unique) auto lemma reduced_labelling_nonzero: "j < n \ x j \ 0 \ reduced n x \ j" using reduced_labelling[of n x] by (elim allE[where x=j]) auto lemma reduced_labelling_Suc: "reduced (Suc n) x \ Suc n \ reduced (Suc n) x = reduced n x" using reduced_labelling[of "Suc n" x] by (intro reduced_labelling_unique[symmetric]) auto lemma complete_face_top: assumes "\x\f. \j\n. x j = 0 \ lab x j = 0" and "\x\f. \j\n. x j = p \ lab x j = 1" and eq: "(reduced (Suc n) \ lab) ` f = {..n}" shows "((\j\n. \x\f. x j = 0) \ (\j\n. \x\f. x j = p)) \ (\x\f. x n = p)" proof (safe del: disjCI) fix x j assume j: "j \ n" "\x\f. x j = 0" { fix x assume "x \ f" with assms j have "reduced (Suc n) (lab x) \ j" by (intro reduced_labelling_zero) auto } moreover have "j \ (reduced (Suc n) \ lab) ` f" using j eq by auto ultimately show "x n = p" by force next fix x j assume j: "j \ n" "\x\f. x j = p" and x: "x \ f" have "j = n" proof (rule ccontr) assume "\ ?thesis" { fix x assume "x \ f" with assms j have "reduced (Suc n) (lab x) \ j" by (intro reduced_labelling_nonzero) auto then have "reduced (Suc n) (lab x) \ n" using \j \ n\ \j \ n\ by simp } moreover have "n \ (reduced (Suc n) \ lab) ` f" using eq by auto ultimately show False by force qed moreover have "j \ (reduced (Suc n) \ lab) ` f" using j eq by auto ultimately show "x n = p" using j x by auto qed auto text \Hence we get just about the nice induction.\ lemma kuhn_induction: assumes "0 < p" and lab_0: "\x. \j\n. (\j. x j \ p) \ x j = 0 \ lab x j = 0" and lab_1: "\x. \j\n. (\j. x j \ p) \ x j = p \ lab x j = 1" and odd: "odd (card {s. ksimplex p n s \ (reduced n\lab) ` s = {..n}})" shows "odd (card {s. ksimplex p (Suc n) s \ (reduced (Suc n)\lab) ` s = {..Suc n}})" proof - let ?rl = "reduced (Suc n) \ lab" and ?ext = "\f v. \j\n. \x\f. x j = v" let ?ext = "\s. (\j\n. \x\s. x j = 0) \ (\j\n. \x\s. x j = p)" have "\s. ksimplex p (Suc n) s \ ?rl ` s \ {..Suc n}" by (simp add: reduced_labelling subset_eq) moreover have "{s. ksimplex p n s \ (reduced n \ lab) ` s = {..n}} = {f. \s a. ksimplex p (Suc n) s \ a \ s \ f = s - {a} \ ?rl ` f = {..n} \ ?ext f}" proof (intro set_eqI, safe del: disjCI equalityI disjE) fix s assume s: "ksimplex p n s" and rl: "(reduced n \ lab) ` s = {..n}" from s obtain u b where "kuhn_simplex p n u b s" by (auto elim: ksimplex.cases) then interpret kuhn_simplex p n u b s . have all_eq_p: "\x\s. x n = p" by (auto simp: out_eq_p) moreover { fix x assume "x \ s" with lab_1[rule_format, of n x] all_eq_p s_le_p[of x] have "?rl x \ n" by (auto intro!: reduced_labelling_nonzero) then have "?rl x = reduced n (lab x)" by (auto intro!: reduced_labelling_Suc) } then have "?rl ` s = {..n}" using rl by (simp cong: image_cong) moreover obtain t a where "ksimplex p (Suc n) t" "a \ t" "s = t - {a}" using s unfolding simplex_top_face[OF \0 < p\ all_eq_p] by auto ultimately show "\t a. ksimplex p (Suc n) t \ a \ t \ s = t - {a} \ ?rl ` s = {..n} \ ?ext s" by auto next fix x s a assume s: "ksimplex p (Suc n) s" and rl: "?rl ` (s - {a}) = {.. n}" and a: "a \ s" and "?ext (s - {a})" from s obtain u b where "kuhn_simplex p (Suc n) u b s" by (auto elim: ksimplex.cases) then interpret kuhn_simplex p "Suc n" u b s . have all_eq_p: "\x\s. x (Suc n) = p" by (auto simp: out_eq_p) { fix x assume "x \ s - {a}" then have "?rl x \ ?rl ` (s - {a})" by auto then have "?rl x \ n" unfolding rl by auto then have "?rl x = reduced n (lab x)" by (auto intro!: reduced_labelling_Suc) } then show rl': "(reduced n\lab) ` (s - {a}) = {..n}" unfolding rl[symmetric] by (intro image_cong) auto from \?ext (s - {a})\ have all_eq_p: "\x\s - {a}. x n = p" proof (elim disjE exE conjE) fix j assume "j \ n" "\x\s - {a}. x j = 0" with lab_0[rule_format, of j] all_eq_p s_le_p have "\x. x \ s - {a} \ reduced (Suc n) (lab x) \ j" by (intro reduced_labelling_zero) auto moreover have "j \ ?rl ` (s - {a})" using \j \ n\ unfolding rl by auto ultimately show ?thesis by force next fix j assume "j \ n" and eq_p: "\x\s - {a}. x j = p" show ?thesis proof cases assume "j = n" with eq_p show ?thesis by simp next assume "j \ n" { fix x assume x: "x \ s - {a}" have "reduced n (lab x) \ j" proof (rule reduced_labelling_nonzero) show "lab x j \ 0" using lab_1[rule_format, of j x] x s_le_p[of x] eq_p \j \ n\ by auto show "j < n" using \j \ n\ \j \ n\ by simp qed then have "reduced n (lab x) \ n" using \j \ n\ \j \ n\ by simp } moreover have "n \ (reduced n\lab) ` (s - {a})" unfolding rl' by auto ultimately show ?thesis by force qed qed show "ksimplex p n (s - {a})" unfolding simplex_top_face[OF \0 < p\ all_eq_p] using s a by auto qed ultimately show ?thesis using assms by (intro kuhn_simplex_lemma) auto qed text \And so we get the final combinatorial result.\ lemma ksimplex_0: "ksimplex p 0 s \ s = {(\x. p)}" proof assume "ksimplex p 0 s" then show "s = {(\x. p)}" by (blast dest: kuhn_simplex.ksimplex_0 elim: ksimplex.cases) next assume s: "s = {(\x. p)}" show "ksimplex p 0 s" proof (intro ksimplex, unfold_locales) show "(\_. p) \ {..<0::nat} \ {..x j. (\j. x j \ p) \ j < n \ x j = 0 \ lab x j = 0" and "\x j. (\j. x j \ p) \ j < n \ x j = p \ lab x j = 1" shows "odd (card {s. ksimplex p n s \ (reduced n\lab) ` s = {..n}})" (is "odd (card (?M n))") using assms proof (induct n) case 0 then show ?case by (simp add: ksimplex_0 cong: conj_cong) next case (Suc n) then have "odd (card (?M n))" by force with Suc show ?case using kuhn_induction[of p n] by (auto simp: comp_def) qed lemma kuhn_lemma: fixes n p :: nat assumes "0 < p" and "\x. (\i p) \ (\i label x i = 1)" and "\x. (\i p) \ (\i label x i = 0)" and "\x. (\i p) \ (\i label x i = 1)" obtains q where "\iir s. (\j r j \ r j \ q j + 1) \ (\j s j \ s j \ q j + 1) \ label r i \ label s i" proof - let ?rl = "reduced n \ label" let ?A = "{s. ksimplex p n s \ ?rl ` s = {..n}}" have "odd (card ?A)" using assms by (intro kuhn_combinatorial[of p n label]) auto then have "?A \ {}" by (rule odd_card_imp_not_empty) then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}" by (auto elim: ksimplex.cases) interpret kuhn_simplex p n b u s by fact show ?thesis proof (intro that[of b] allI impI) fix i assume "i < n" then show "b i < p" using base by auto next fix i assume "i < n" then have "i \ {.. n}" "Suc i \ {.. n}" by auto then obtain u v where u: "u \ s" "Suc i = ?rl u" and v: "v \ s" "i = ?rl v" unfolding rl[symmetric] by blast have "label u i \ label v i" using reduced_labelling [of n "label u"] reduced_labelling [of n "label v"] u(2)[symmetric] v(2)[symmetric] \i < n\ by auto moreover have "b j \ u j" "u j \ b j + 1" "b j \ v j" "v j \ b j + 1" if "j < n" for j using that base_le[OF \u\s\] le_Suc_base[OF \u\s\] base_le[OF \v\s\] le_Suc_base[OF \v\s\] by auto ultimately show "\r s. (\j r j \ r j \ b j + 1) \ (\j s j \ s j \ b j + 1) \ label r i \ label s i" by blast qed qed subsubsection \Main result for the unit cube\ lemma kuhn_labelling_lemma': assumes "(\x::nat\real. P x \ P (f x))" and "\x. P x \ (\i::nat. Q i \ 0 \ x i \ x i \ 1)" shows "\l. (\x i. l x i \ (1::nat)) \ (\x i. P x \ Q i \ x i = 0 \ l x i = 0) \ (\x i. P x \ Q i \ x i = 1 \ l x i = 1) \ (\x i. P x \ Q i \ l x i = 0 \ x i \ f x i) \ (\x i. P x \ Q i \ l x i = 1 \ f x i \ x i)" proof - have and_forall_thm: "\P Q. (\x. P x) \ (\x. Q x) \ (\x. P x \ Q x)" by auto have *: "\x y::real. 0 \ x \ x \ 1 \ 0 \ y \ y \ 1 \ x \ 1 \ x \ y \ x \ 0 \ y \ x" by auto show ?thesis unfolding and_forall_thm apply (subst choice_iff[symmetric])+ apply rule apply rule proof - fix x x' let ?R = "\y::nat. (P x \ Q x' \ x x' = 0 \ y = 0) \ (P x \ Q x' \ x x' = 1 \ y = 1) \ (P x \ Q x' \ y = 0 \ x x' \ (f x) x') \ (P x \ Q x' \ y = 1 \ (f x) x' \ x x')" have "0 \ f x x' \ f x x' \ 1" if "P x" "Q x'" using assms(2)[rule_format,of "f x" x'] that apply (drule_tac assms(1)[rule_format]) apply auto done then have "?R 0 \ ?R 1" by auto then show "\y\1. ?R y" by auto qed qed subsection \Brouwer's fixed point theorem\ text \We start proving Brouwer's fixed point theorem for the unit cube = \cbox 0 One\.\ lemma brouwer_cube: fixes f :: "'a::euclidean_space \ 'a" assumes "continuous_on (cbox 0 One) f" and "f ` cbox 0 One \ cbox 0 One" shows "\x\cbox 0 One. f x = x" proof (rule ccontr) define n where "n = DIM('a)" have n: "1 \ n" "0 < n" "n \ 0" unfolding n_def by (auto simp: Suc_le_eq) assume "\ ?thesis" then have *: "\ (\x\cbox 0 One. f x - x = 0)" by auto obtain d where d: "d > 0" "\x. x \ cbox 0 One \ d \ norm (f x - x)" apply (rule brouwer_compactness_lemma[OF compact_cbox _ *]) apply (rule continuous_intros assms)+ apply blast done have *: "\x. x \ cbox 0 One \ f x \ cbox 0 One" "\x. x \ (cbox 0 One::'a set) \ (\i\Basis. True \ 0 \ x \ i \ x \ i \ 1)" using assms(2)[unfolded image_subset_iff Ball_def] unfolding cbox_def by auto obtain label :: "'a \ 'a \ nat" where label [rule_format]: "\x. \i\Basis. label x i \ 1" "\x. \i\Basis. x \ cbox 0 One \ x \ i = 0 \ label x i = 0" "\x. \i\Basis. x \ cbox 0 One \ x \ i = 1 \ label x i = 1" "\x. \i\Basis. x \ cbox 0 One \ label x i = 0 \ x \ i \ f x \ i" "\x. \i\Basis. x \ cbox 0 One \ label x i = 1 \ f x \ i \ x \ i" using kuhn_labelling_lemma[OF *] by auto note label = this [rule_format] have lem1: "\x\cbox 0 One. \y\cbox 0 One. \i\Basis. label x i \ label y i \ \f x \ i - x \ i\ \ norm (f y - f x) + norm (y - x)" proof safe fix x y :: 'a assume x: "x \ cbox 0 One" and y: "y \ cbox 0 One" fix i assume i: "label x i \ label y i" "i \ Basis" have *: "\x y fx fy :: real. x \ fx \ fy \ y \ fx \ x \ y \ fy \ \fx - x\ \ \fy - fx\ + \y - x\" by auto have "\(f x - x) \ i\ \ \(f y - f x)\i\ + \(y - x)\i\" proof (cases "label x i = 0") case True then have fxy: "\ f y \ i \ y \ i \ f x \ i \ x \ i" by (metis True i label(1) label(5) le_antisym less_one not_le_imp_less y) show ?thesis unfolding inner_simps by (rule *) (auto simp: True i label x y fxy) next case False then show ?thesis using label [OF \i \ Basis\] i(1) x y apply (auto simp: inner_diff_left le_Suc_eq) by (metis "*") qed also have "\ \ norm (f y - f x) + norm (y - x)" by (simp add: add_mono i(2) norm_bound_Basis_le) finally show "\f x \ i - x \ i\ \ norm (f y - f x) + norm (y - x)" unfolding inner_simps . qed have "\e>0. \x\cbox 0 One. \y\cbox 0 One. \z\cbox 0 One. \i\Basis. norm (x - z) < e \ norm (y - z) < e \ label x i \ label y i \ \(f(z) - z)\i\ < d / (real n)" proof - have d': "d / real n / 8 > 0" using d(1) by (simp add: n_def) have *: "uniformly_continuous_on (cbox 0 One) f" by (rule compact_uniformly_continuous[OF assms(1) compact_cbox]) obtain e where e: "e > 0" "\x x'. x \ cbox 0 One \ x' \ cbox 0 One \ norm (x' - x) < e \ norm (f x' - f x) < d / real n / 8" using *[unfolded uniformly_continuous_on_def,rule_format,OF d'] unfolding dist_norm by blast show ?thesis proof (intro exI conjI ballI impI) show "0 < min (e / 2) (d / real n / 8)" using d' e by auto fix x y z i assume as: "x \ cbox 0 One" "y \ cbox 0 One" "z \ cbox 0 One" "norm (x - z) < min (e / 2) (d / real n / 8)" "norm (y - z) < min (e / 2) (d / real n / 8)" "label x i \ label y i" assume i: "i \ Basis" have *: "\z fz x fx n1 n2 n3 n4 d4 d :: real. \fx - x\ \ n1 + n2 \ \fx - fz\ \ n3 \ \x - z\ \ n4 \ n1 < d4 \ n2 < 2 * d4 \ n3 < d4 \ n4 < d4 \ (8 * d4 = d) \ \fz - z\ < d" by auto show "\(f z - z) \ i\ < d / real n" unfolding inner_simps proof (rule *) show "\f x \ i - x \ i\ \ norm (f y -f x) + norm (y - x)" using as(1) as(2) as(6) i lem1 by blast show "norm (f x - f z) < d / real n / 8" using d' e as by auto show "\f x \ i - f z \ i\ \ norm (f x - f z)" "\x \ i - z \ i\ \ norm (x - z)" unfolding inner_diff_left[symmetric] by (rule Basis_le_norm[OF i])+ have tria: "norm (y - x) \ norm (y - z) + norm (x - z)" using dist_triangle[of y x z, unfolded dist_norm] unfolding norm_minus_commute by auto also have "\ < e / 2 + e / 2" using as(4) as(5) by auto finally show "norm (f y - f x) < d / real n / 8" using as(1) as(2) e(2) by auto have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8" using as(4) as(5) by auto with tria show "norm (y - x) < 2 * (d / real n / 8)" by auto qed (use as in auto) qed qed then obtain e where e: "e > 0" "\x y z i. x \ cbox 0 One \ y \ cbox 0 One \ z \ cbox 0 One \ i \ Basis \ norm (x - z) < e \ norm (y - z) < e \ label x i \ label y i \ \(f z - z) \ i\ < d / real n" by blast obtain p :: nat where p: "1 + real n / e \ real p" using real_arch_simple .. have "1 + real n / e > 0" using e(1) n by (simp add: add_pos_pos) then have "p > 0" using p by auto obtain b :: "nat \ 'a" where b: "bij_betw b {..< n} Basis" by atomize_elim (auto simp: n_def intro!: finite_same_card_bij) define b' where "b' = inv_into {..< n} b" then have b': "bij_betw b' Basis {..< n}" using bij_betw_inv_into[OF b] by auto then have b'_Basis: "\i. i \ Basis \ b' i \ {..< n}" unfolding bij_betw_def by (auto simp: set_eq_iff) have bb'[simp]:"\i. i \ Basis \ b (b' i) = i" unfolding b'_def using b by (auto simp: f_inv_into_f bij_betw_def) have b'b[simp]:"\i. i < n \ b' (b i) = i" unfolding b'_def using b by (auto simp: inv_into_f_eq bij_betw_def) have *: "\x :: nat. x = 0 \ x = 1 \ x \ 1" by auto have b'': "\j. j < n \ b j \ Basis" using b unfolding bij_betw_def by auto have q1: "0 < p" "\x. (\i p) \ (\ii\Basis. (real (x (b' i)) / real p) *\<^sub>R i) \ b) i = 0 \ (label (\i\Basis. (real (x (b' i)) / real p) *\<^sub>R i) \ b) i = 1)" unfolding * using \p > 0\ \n > 0\ using label(1)[OF b''] by auto { fix x :: "nat \ nat" and i assume "\i p" "i < n" "x i = p \ x i = 0" then have "(\i\Basis. (real (x (b' i)) / real p) *\<^sub>R i) \ (cbox 0 One::'a set)" using b'_Basis by (auto simp: cbox_def bij_betw_def zero_le_divide_iff divide_le_eq_1) } note cube = this have q2: "\x. (\i p) \ (\i (label (\i\Basis. (real (x (b' i)) / real p) *\<^sub>R i) \ b) i = 0)" unfolding o_def using cube \p > 0\ by (intro allI impI label(2)) (auto simp: b'') have q3: "\x. (\i p) \ (\i (label (\i\Basis. (real (x (b' i)) / real p) *\<^sub>R i) \ b) i = 1)" using cube \p > 0\ unfolding o_def by (intro allI impI label(3)) (auto simp: b'') obtain q where q: "\iir s. (\j r j \ r j \ q j + 1) \ (\j s j \ s j \ q j + 1) \ (label (\i\Basis. (real (r (b' i)) / real p) *\<^sub>R i) \ b) i \ (label (\i\Basis. (real (s (b' i)) / real p) *\<^sub>R i) \ b) i" by (rule kuhn_lemma[OF q1 q2 q3]) define z :: 'a where "z = (\i\Basis. (real (q (b' i)) / real p) *\<^sub>R i)" have "\i\Basis. d / real n \ \(f z - z)\i\" proof (rule ccontr) have "\i\Basis. q (b' i) \ {0..p}" using q(1) b' by (auto intro: less_imp_le simp: bij_betw_def) then have "z \ cbox 0 One" unfolding z_def cbox_def using b'_Basis by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1) then have d_fz_z: "d \ norm (f z - z)" by (rule d) assume "\ ?thesis" then have as: "\i\Basis. \f z \ i - z \ i\ < d / real n" using \n > 0\ by (auto simp: not_le inner_diff) have "norm (f z - z) \ (\i\Basis. \f z \ i - z \ i\)" unfolding inner_diff_left[symmetric] by (rule norm_le_l1) also have "\ < (\(i::'a) \ Basis. d / real n)" by (meson as finite_Basis nonempty_Basis sum_strict_mono) also have "\ = d" using DIM_positive[where 'a='a] by (auto simp: n_def) finally show False using d_fz_z by auto qed then obtain i where i: "i \ Basis" "d / real n \ \(f z - z) \ i\" .. have *: "b' i < n" using i and b'[unfolded bij_betw_def] by auto obtain r s where rs: "\j. j < n \ q j \ r j \ r j \ q j + 1" "\j. j < n \ q j \ s j \ s j \ q j + 1" "(label (\i\Basis. (real (r (b' i)) / real p) *\<^sub>R i) \ b) (b' i) \ (label (\i\Basis. (real (s (b' i)) / real p) *\<^sub>R i) \ b) (b' i)" using q(2)[rule_format,OF *] by blast have b'_im: "\i. i \ Basis \ b' i < n" using b' unfolding bij_betw_def by auto define r' ::'a where "r' = (\i\Basis. (real (r (b' i)) / real p) *\<^sub>R i)" have "\i. i \ Basis \ r (b' i) \ p" apply (rule order_trans) apply (rule rs(1)[OF b'_im,THEN conjunct2]) using q(1)[rule_format,OF b'_im] apply (auto simp: Suc_le_eq) done then have "r' \ cbox 0 One" unfolding r'_def cbox_def using b'_Basis by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1) define s' :: 'a where "s' = (\i\Basis. (real (s (b' i)) / real p) *\<^sub>R i)" have "\i. i \ Basis \ s (b' i) \ p" using b'_im q(1) rs(2) by fastforce then have "s' \ cbox 0 One" unfolding s'_def cbox_def using b'_Basis by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1) have "z \ cbox 0 One" unfolding z_def cbox_def using b'_Basis q(1)[rule_format,OF b'_im] \p > 0\ by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le) { have "(\i\Basis. \real (r (b' i)) - real (q (b' i))\) \ (\(i::'a)\Basis. 1)" by (rule sum_mono) (use rs(1)[OF b'_im] in force) also have "\ < e * real p" using p \e > 0\ \p > 0\ by (auto simp: field_simps n_def) finally have "(\i\Basis. \real (r (b' i)) - real (q (b' i))\) < e * real p" . } moreover { have "(\i\Basis. \real (s (b' i)) - real (q (b' i))\) \ (\(i::'a)\Basis. 1)" by (rule sum_mono) (use rs(2)[OF b'_im] in force) also have "\ < e * real p" using p \e > 0\ \p > 0\ by (auto simp: field_simps n_def) finally have "(\i\Basis. \real (s (b' i)) - real (q (b' i))\) < e * real p" . } ultimately have "norm (r' - z) < e" and "norm (s' - z) < e" unfolding r'_def s'_def z_def using \p > 0\ apply (rule_tac[!] le_less_trans[OF norm_le_l1]) apply (auto simp: field_simps sum_divide_distrib[symmetric] inner_diff_left) done then have "\(f z - z) \ i\ < d / real n" using rs(3) i unfolding r'_def[symmetric] s'_def[symmetric] o_def bb' by (intro e(2)[OF \r'\cbox 0 One\ \s'\cbox 0 One\ \z\cbox 0 One\]) auto then show False using i by auto qed text \Next step is to prove it for nonempty interiors.\ lemma brouwer_weak: fixes f :: "'a::euclidean_space \ 'a" assumes "compact S" and "convex S" and "interior S \ {}" and "continuous_on S f" and "f ` S \ S" obtains x where "x \ S" and "f x = x" proof - let ?U = "cbox 0 One :: 'a set" have "\Basis /\<^sub>R 2 \ interior ?U" proof (rule interiorI) let ?I = "(\i\Basis. {x::'a. 0 < x \ i} \ {x. x \ i < 1})" show "open ?I" by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner) show "\Basis /\<^sub>R 2 \ ?I" by simp show "?I \ cbox 0 One" unfolding cbox_def by force qed then have *: "interior ?U \ {}" by fast have *: "?U homeomorphic S" using homeomorphic_convex_compact[OF convex_box(1) compact_cbox * assms(2,1,3)] . have "\f. continuous_on ?U f \ f ` ?U \ ?U \ (\x\?U. f x = x)" using brouwer_cube by auto then show ?thesis unfolding homeomorphic_fixpoint_property[OF *] using assms by (auto intro: that) qed text \Then the particular case for closed balls.\ lemma brouwer_ball: fixes f :: "'a::euclidean_space \ 'a" assumes "e > 0" and "continuous_on (cball a e) f" and "f ` cball a e \ cball a e" obtains x where "x \ cball a e" and "f x = x" using brouwer_weak[OF compact_cball convex_cball, of a e f] unfolding interior_cball ball_eq_empty using assms by auto text \And finally we prove Brouwer's fixed point theorem in its general version.\ theorem brouwer: fixes f :: "'a::euclidean_space \ 'a" assumes S: "compact S" "convex S" "S \ {}" and contf: "continuous_on S f" and fim: "f ` S \ S" obtains x where "x \ S" and "f x = x" proof - have "\e>0. S \ cball 0 e" using compact_imp_bounded[OF \compact S\] unfolding bounded_pos by auto then obtain e where e: "e > 0" "S \ cball 0 e" by blast have "\x\ cball 0 e. (f \ closest_point S) x = x" proof (rule_tac brouwer_ball[OF e(1)]) show "continuous_on (cball 0 e) (f \ closest_point S)" apply (rule continuous_on_compose) using S compact_eq_bounded_closed continuous_on_closest_point apply blast by (meson S contf closest_point_in_set compact_imp_closed continuous_on_subset image_subsetI) show "(f \ closest_point S) ` cball 0 e \ cball 0 e" by clarsimp (metis S fim closest_point_exists(1) compact_eq_bounded_closed e(2) image_subset_iff mem_cball_0 subsetCE) qed (use assms in auto) then obtain x where x: "x \ cball 0 e" "(f \ closest_point S) x = x" .. have "x \ S" by (metis closest_point_in_set comp_apply compact_imp_closed fim image_eqI S(1) S(3) subset_iff x(2)) then have *: "closest_point S x = x" by (rule closest_point_self) show thesis proof show "closest_point S x \ S" by (simp add: "*" \x \ S\) show "f (closest_point S x) = closest_point S x" using "*" x(2) by auto qed qed subsection \Applications\ text \So we get the no-retraction theorem.\ corollary no_retraction_cball: fixes a :: "'a::euclidean_space" assumes "e > 0" shows "\ (frontier (cball a e) retract_of (cball a e))" proof assume *: "frontier (cball a e) retract_of (cball a e)" have **: "\xa. a - (2 *\<^sub>R a - xa) = - (a - xa)" using scaleR_left_distrib[of 1 1 a] by auto obtain x where x: "x \ {x. norm (a - x) = e}" "2 *\<^sub>R a - x = x" proof (rule retract_fixpoint_property[OF *, of "\x. scaleR 2 a - x"]) show "continuous_on (frontier (cball a e)) ((-) (2 *\<^sub>R a))" by (intro continuous_intros) show "(-) (2 *\<^sub>R a) ` frontier (cball a e) \ frontier (cball a e)" by clarsimp (metis "**" dist_norm norm_minus_cancel) qed (auto simp: dist_norm intro: brouwer_ball[OF assms]) then have "scaleR 2 a = scaleR 1 x + scaleR 1 x" by (auto simp: algebra_simps) then have "a = x" unfolding scaleR_left_distrib[symmetric] by auto then show False using x assms by auto qed corollary contractible_sphere: fixes a :: "'a::euclidean_space" shows "contractible(sphere a r) \ r \ 0" proof (cases "0 < r") case True then show ?thesis unfolding contractible_def nullhomotopic_from_sphere_extension using no_retraction_cball [OF True, of a] by (auto simp: retract_of_def retraction_def) next case False then show ?thesis unfolding contractible_def nullhomotopic_from_sphere_extension using less_eq_real_def by auto qed corollary connected_sphere_eq: fixes a :: "'a :: euclidean_space" shows "connected(sphere a r) \ 2 \ DIM('a) \ r \ 0" (is "?lhs = ?rhs") proof (cases r "0::real" rule: linorder_cases) case less then show ?thesis by auto next case equal then show ?thesis by auto next case greater show ?thesis proof assume L: ?lhs have "False" if 1: "DIM('a) = 1" proof - obtain x y where xy: "sphere a r = {x,y}" "x \ y" using sphere_1D_doubleton [OF 1 greater] by (metis dist_self greater insertI1 less_add_same_cancel1 mem_sphere mult_2 not_le zero_le_dist) then have "finite (sphere a r)" by auto with L \r > 0\ xy show "False" using connected_finite_iff_sing by auto qed with greater show ?rhs by (metis DIM_ge_Suc0 One_nat_def Suc_1 le_antisym not_less_eq_eq) next assume ?rhs then show ?lhs using connected_sphere greater by auto qed qed corollary path_connected_sphere_eq: fixes a :: "'a :: euclidean_space" shows "path_connected(sphere a r) \ 2 \ DIM('a) \ r \ 0" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs using connected_sphere_eq path_connected_imp_connected by blast next assume R: ?rhs then show ?lhs by (auto simp: contractible_imp_path_connected contractible_sphere path_connected_sphere) qed proposition frontier_subset_retraction: fixes S :: "'a::euclidean_space set" assumes "bounded S" and fros: "frontier S \ T" and contf: "continuous_on (closure S) f" and fim: "f ` S \ T" and fid: "\x. x \ T \ f x = x" shows "S \ T" proof (rule ccontr) assume "\ S \ T" then obtain a where "a \ S" "a \ T" by blast define g where "g \ \z. if z \ closure S then f z else z" have "continuous_on (closure S \ closure(-S)) g" unfolding g_def apply (rule continuous_on_cases) using fros fid frontier_closures by (auto simp: contf) moreover have "closure S \ closure(- S) = UNIV" using closure_Un by fastforce ultimately have contg: "continuous_on UNIV g" by metis obtain B where "0 < B" and B: "closure S \ ball a B" using \bounded S\ bounded_subset_ballD by blast have notga: "g x \ a" for x unfolding g_def using fros fim \a \ T\ apply (auto simp: frontier_def) using fid interior_subset apply fastforce by (simp add: \a \ S\ closure_def) define h where "h \ (\y. a + (B / norm(y - a)) *\<^sub>R (y - a)) \ g" have "\ (frontier (cball a B) retract_of (cball a B))" by (metis no_retraction_cball \0 < B\) then have "\k. \ retraction (cball a B) (frontier (cball a B)) k" by (simp add: retract_of_def) moreover have "retraction (cball a B) (frontier (cball a B)) h" unfolding retraction_def proof (intro conjI ballI) show "frontier (cball a B) \ cball a B" by force show "continuous_on (cball a B) h" unfolding h_def by (intro continuous_intros) (use contg continuous_on_subset notga in auto) show "h ` cball a B \ frontier (cball a B)" using \0 < B\ by (auto simp: h_def notga dist_norm) show "\x. x \ frontier (cball a B) \ h x = x" apply (auto simp: h_def algebra_simps) apply (simp add: vector_add_divide_simps notga) by (metis (no_types, hide_lams) B add.commute dist_commute dist_norm g_def mem_ball not_less_iff_gr_or_eq subset_eq) qed ultimately show False by simp qed subsubsection \Punctured affine hulls, etc\ lemma rel_frontier_deformation_retract_of_punctured_convex: fixes S :: "'a::euclidean_space set" assumes "convex S" "convex T" "bounded S" and arelS: "a \ rel_interior S" and relS: "rel_frontier S \ T" and affS: "T \ affine hull S" obtains r where "homotopic_with_canon (\x. True) (T - {a}) (T - {a}) id r" "retraction (T - {a}) (rel_frontier S) r" proof - have "\d. 0 < d \ (a + d *\<^sub>R l) \ rel_frontier S \ (\e. 0 \ e \ e < d \ (a + e *\<^sub>R l) \ rel_interior S)" if "(a + l) \ affine hull S" "l \ 0" for l apply (rule ray_to_rel_frontier [OF \bounded S\ arelS]) apply (rule that)+ by metis then obtain dd where dd1: "\l. \(a + l) \ affine hull S; l \ 0\ \ 0 < dd l \ (a + dd l *\<^sub>R l) \ rel_frontier S" and dd2: "\l e. \(a + l) \ affine hull S; e < dd l; 0 \ e; l \ 0\ \ (a + e *\<^sub>R l) \ rel_interior S" by metis+ have aaffS: "a \ affine hull S" by (meson arelS subsetD hull_inc rel_interior_subset) have "((\z. z - a) ` (affine hull S - {a})) = ((\z. z - a) ` (affine hull S)) - {0}" by auto moreover have "continuous_on (((\z. z - a) ` (affine hull S)) - {0}) (\x. dd x *\<^sub>R x)" proof (rule continuous_on_compact_surface_projection) show "compact (rel_frontier ((\z. z - a) ` S))" by (simp add: \bounded S\ bounded_translation_minus compact_rel_frontier_bounded) have releq: "rel_frontier ((\z. z - a) ` S) = (\z. z - a) ` rel_frontier S" using rel_frontier_translation [of "-a"] add.commute by simp also have "\ \ (\z. z - a) ` (affine hull S) - {0}" using rel_frontier_affine_hull arelS rel_frontier_def by fastforce finally show "rel_frontier ((\z. z - a) ` S) \ (\z. z - a) ` (affine hull S) - {0}" . show "cone ((\z. z - a) ` (affine hull S))" by (rule subspace_imp_cone) (use aaffS in \simp add: subspace_affine image_comp o_def affine_translation_aux [of a]\) show "(0 < k \ k *\<^sub>R x \ rel_frontier ((\z. z - a) ` S)) \ (dd x = k)" if x: "x \ (\z. z - a) ` (affine hull S) - {0}" for k x proof show "dd x = k \ 0 < k \ k *\<^sub>R x \ rel_frontier ((\z. z - a) ` S)" using dd1 [of x] that image_iff by (fastforce simp add: releq) next assume k: "0 < k \ k *\<^sub>R x \ rel_frontier ((\z. z - a) ` S)" have False if "dd x < k" proof - have "k \ 0" "a + k *\<^sub>R x \ closure S" using k closure_translation [of "-a"] by (auto simp: rel_frontier_def cong: image_cong_simp) then have segsub: "open_segment a (a + k *\<^sub>R x) \ rel_interior S" by (metis rel_interior_closure_convex_segment [OF \convex S\ arelS]) have "x \ 0" and xaffS: "a + x \ affine hull S" using x by auto then have "0 < dd x" and inS: "a + dd x *\<^sub>R x \ rel_frontier S" using dd1 by auto moreover have "a + dd x *\<^sub>R x \ open_segment a (a + k *\<^sub>R x)" using k \x \ 0\ \0 < dd x\ apply (simp add: in_segment) apply (rule_tac x = "dd x / k" in exI) apply (simp add: field_simps that) apply (simp add: vector_add_divide_simps algebra_simps) done ultimately show ?thesis using segsub by (auto simp: rel_frontier_def) qed moreover have False if "k < dd x" using x k that rel_frontier_def by (fastforce simp: algebra_simps releq dest!: dd2) ultimately show "dd x = k" by fastforce qed qed ultimately have *: "continuous_on ((\z. z - a) ` (affine hull S - {a})) (\x. dd x *\<^sub>R x)" by auto have "continuous_on (affine hull S - {a}) ((\x. a + dd x *\<^sub>R x) \ (\z. z - a))" by (intro * continuous_intros continuous_on_compose) with affS have contdd: "continuous_on (T - {a}) ((\x. a + dd x *\<^sub>R x) \ (\z. z - a))" by (blast intro: continuous_on_subset) show ?thesis proof show "homotopic_with_canon (\x. True) (T - {a}) (T - {a}) id (\x. a + dd (x - a) *\<^sub>R (x - a))" proof (rule homotopic_with_linear) show "continuous_on (T - {a}) id" by (intro continuous_intros continuous_on_compose) show "continuous_on (T - {a}) (\x. a + dd (x - a) *\<^sub>R (x - a))" using contdd by (simp add: o_def) show "closed_segment (id x) (a + dd (x - a) *\<^sub>R (x - a)) \ T - {a}" if "x \ T - {a}" for x proof (clarsimp simp: in_segment, intro conjI) fix u::real assume u: "0 \ u" "u \ 1" have "a + dd (x - a) *\<^sub>R (x - a) \ T" by (metis DiffD1 DiffD2 add.commute add.right_neutral affS dd1 diff_add_cancel relS singletonI subsetCE that) then show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \ T" using convexD [OF \convex T\] that u by simp have iff: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + d *\<^sub>R (x - a)) = a \ (1 - u + u * d) *\<^sub>R (x - a) = 0" for d by (auto simp: algebra_simps) have "x \ T" "x \ a" using that by auto then have axa: "a + (x - a) \ affine hull S" by (metis (no_types) add.commute affS diff_add_cancel rev_subsetD) then have "\ dd (x - a) \ 0 \ a + dd (x - a) *\<^sub>R (x - a) \ rel_frontier S" using \x \ a\ dd1 by fastforce with \x \ a\ show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \ a" apply (auto simp: iff) using less_eq_real_def mult_le_0_iff not_less u by fastforce qed qed show "retraction (T - {a}) (rel_frontier S) (\x. a + dd (x - a) *\<^sub>R (x - a))" proof (simp add: retraction_def, intro conjI ballI) show "rel_frontier S \ T - {a}" using arelS relS rel_frontier_def by fastforce show "continuous_on (T - {a}) (\x. a + dd (x - a) *\<^sub>R (x - a))" using contdd by (simp add: o_def) show "(\x. a + dd (x - a) *\<^sub>R (x - a)) ` (T - {a}) \ rel_frontier S" apply (auto simp: rel_frontier_def) apply (metis Diff_subset add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def subset_iff) by (metis DiffE add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def rev_subsetD) show "a + dd (x - a) *\<^sub>R (x - a) = x" if x: "x \ rel_frontier S" for x proof - have "x \ a" using that arelS by (auto simp: rel_frontier_def) have False if "dd (x - a) < 1" proof - have "x \ closure S" using x by (auto simp: rel_frontier_def) then have segsub: "open_segment a x \ rel_interior S" by (metis rel_interior_closure_convex_segment [OF \convex S\ arelS]) have xaffS: "x \ affine hull S" using affS relS x by auto then have "0 < dd (x - a)" and inS: "a + dd (x - a) *\<^sub>R (x - a) \ rel_frontier S" using dd1 by (auto simp: \x \ a\) moreover have "a + dd (x - a) *\<^sub>R (x - a) \ open_segment a x" using \x \ a\ \0 < dd (x - a)\ apply (simp add: in_segment) apply (rule_tac x = "dd (x - a)" in exI) apply (simp add: algebra_simps that) done ultimately show ?thesis using segsub by (auto simp: rel_frontier_def) qed moreover have False if "1 < dd (x - a)" using x that dd2 [of "x - a" 1] \x \ a\ closure_affine_hull by (auto simp: rel_frontier_def) ultimately have "dd (x - a) = 1" \ \similar to another proof above\ by fastforce with that show ?thesis by (simp add: rel_frontier_def) qed qed qed qed corollary rel_frontier_retract_of_punctured_affine_hull: fixes S :: "'a::euclidean_space set" assumes "bounded S" "convex S" "a \ rel_interior S" shows "rel_frontier S retract_of (affine hull S - {a})" apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S "affine hull S" a]) apply (auto simp: affine_imp_convex rel_frontier_affine_hull retract_of_def assms) done corollary rel_boundary_retract_of_punctured_affine_hull: fixes S :: "'a::euclidean_space set" assumes "compact S" "convex S" "a \ rel_interior S" shows "(S - rel_interior S) retract_of (affine hull S - {a})" by (metis assms closure_closed compact_eq_bounded_closed rel_frontier_def rel_frontier_retract_of_punctured_affine_hull) lemma homotopy_eqv_rel_frontier_punctured_convex: fixes S :: "'a::euclidean_space set" assumes "convex S" "bounded S" "a \ rel_interior S" "convex T" "rel_frontier S \ T" "T \ affine hull S" shows "(rel_frontier S) homotopy_eqv (T - {a})" apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S T]) using assms apply auto using deformation_retract_imp_homotopy_eqv homotopy_equivalent_space_sym by blast lemma homotopy_eqv_rel_frontier_punctured_affine_hull: fixes S :: "'a::euclidean_space set" assumes "convex S" "bounded S" "a \ rel_interior S" shows "(rel_frontier S) homotopy_eqv (affine hull S - {a})" apply (rule homotopy_eqv_rel_frontier_punctured_convex) using assms rel_frontier_affine_hull by force+ lemma path_connected_sphere_gen: assumes "convex S" "bounded S" "aff_dim S \ 1" shows "path_connected(rel_frontier S)" proof (cases "rel_interior S = {}") case True then show ?thesis by (simp add: \convex S\ convex_imp_path_connected rel_frontier_def) next case False then show ?thesis by (metis aff_dim_affine_hull affine_affine_hull affine_imp_convex all_not_in_conv assms path_connected_punctured_convex rel_frontier_retract_of_punctured_affine_hull retract_of_path_connected) qed lemma connected_sphere_gen: assumes "convex S" "bounded S" "aff_dim S \ 1" shows "connected(rel_frontier S)" by (simp add: assms path_connected_imp_connected path_connected_sphere_gen) subsubsection\Borsuk-style characterization of separation\ lemma continuous_on_Borsuk_map: "a \ s \ continuous_on s (\x. inverse(norm (x - a)) *\<^sub>R (x - a))" by (rule continuous_intros | force)+ lemma Borsuk_map_into_sphere: "(\x. inverse(norm (x - a)) *\<^sub>R (x - a)) ` s \ sphere 0 1 \ (a \ s)" by auto (metis eq_iff_diff_eq_0 left_inverse norm_eq_zero) lemma Borsuk_maps_homotopic_in_path_component: assumes "path_component (- s) a b" shows "homotopic_with_canon (\x. True) s (sphere 0 1) (\x. inverse(norm(x - a)) *\<^sub>R (x - a)) (\x. inverse(norm(x - b)) *\<^sub>R (x - b))" proof - obtain g where "path g" "path_image g \ -s" "pathstart g = a" "pathfinish g = b" using assms by (auto simp: path_component_def) then show ?thesis apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def) apply (rule_tac x = "\z. inverse(norm(snd z - (g \ fst)z)) *\<^sub>R (snd z - (g \ fst)z)" in exI) apply (intro conjI continuous_intros) apply (rule continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+ done qed lemma non_extensible_Borsuk_map: fixes a :: "'a :: euclidean_space" assumes "compact s" and cin: "c \ components(- s)" and boc: "bounded c" and "a \ c" shows "\ (\g. continuous_on (s \ c) g \ g ` (s \ c) \ sphere 0 1 \ (\x \ s. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))" proof - have "closed s" using assms by (simp add: compact_imp_closed) have "c \ -s" using assms by (simp add: in_components_subset) with \a \ c\ have "a \ s" by blast then have ceq: "c = connected_component_set (- s) a" by (metis \a \ c\ cin components_iff connected_component_eq) then have "bounded (s \ connected_component_set (- s) a)" using \compact s\ boc compact_imp_bounded by auto with bounded_subset_ballD obtain r where "0 < r" and r: "(s \ connected_component_set (- s) a) \ ball a r" by blast { fix g assume "continuous_on (s \ c) g" "g ` (s \ c) \ sphere 0 1" and [simp]: "\x. x \ s \ g x = (x - a) /\<^sub>R norm (x - a)" then have [simp]: "\x. x \ s \ c \ norm (g x) = 1" by force have cb_eq: "cball a r = (s \ connected_component_set (- s) a) \ (cball a r - connected_component_set (- s) a)" using ball_subset_cball [of a r] r by auto have cont1: "continuous_on (s \ connected_component_set (- s) a) (\x. a + r *\<^sub>R g x)" apply (rule continuous_intros)+ using \continuous_on (s \ c) g\ ceq by blast have cont2: "continuous_on (cball a r - connected_component_set (- s) a) (\x. a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))" by (rule continuous_intros | force simp: \a \ s\)+ have 1: "continuous_on (cball a r) (\x. if connected_component (- s) a x then a + r *\<^sub>R g x else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))" apply (subst cb_eq) apply (rule continuous_on_cases [OF _ _ cont1 cont2]) using ceq cin apply (auto intro: closed_Un_complement_component simp: \closed s\ open_Compl open_connected_component) done have 2: "(\x. a + r *\<^sub>R g x) ` (cball a r \ connected_component_set (- s) a) \ sphere a r " using \0 < r\ by (force simp: dist_norm ceq) have "retraction (cball a r) (sphere a r) (\x. if x \ connected_component_set (- s) a then a + r *\<^sub>R g x else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))" using \0 < r\ apply (simp add: retraction_def dist_norm 1 2, safe) apply (force simp: dist_norm abs_if mult_less_0_iff divide_simps \a \ s\) using r by (auto simp: dist_norm norm_minus_commute) then have False using no_retraction_cball [OF \0 < r\, of a, unfolded retract_of_def, simplified, rule_format, of "\x. if x \ connected_component_set (- s) a then a + r *\<^sub>R g x else a + r *\<^sub>R inverse(norm(x - a)) *\<^sub>R (x - a)"] by blast } then show ?thesis by blast qed subsubsection \Proving surjectivity via Brouwer fixpoint theorem\ lemma brouwer_surjective: fixes f :: "'n::euclidean_space \ 'n" assumes "compact T" and "convex T" and "T \ {}" and "continuous_on T f" and "\x y. \x\S; y\T\ \ x + (y - f y) \ T" and "x \ S" shows "\y\T. f y = x" proof - have *: "\x y. f y = x \ x + (y - f y) = y" by (auto simp add: algebra_simps) show ?thesis unfolding * apply (rule brouwer[OF assms(1-3), of "\y. x + (y - f y)"]) apply (intro continuous_intros) using assms apply auto done qed lemma brouwer_surjective_cball: fixes f :: "'n::euclidean_space \ 'n" assumes "continuous_on (cball a e) f" and "e > 0" and "x \ S" and "\x y. \x\S; y\cball a e\ \ x + (y - f y) \ cball a e" shows "\y\cball a e. f y = x" apply (rule brouwer_surjective) apply (rule compact_cball convex_cball)+ unfolding cball_eq_empty using assms apply auto done subsubsection \Inverse function theorem\ text \See Sussmann: "Multidifferential calculus", Theorem 2.1.1\ lemma sussmann_open_mapping: fixes f :: "'a::real_normed_vector \ 'b::euclidean_space" assumes "open S" and contf: "continuous_on S f" and "x \ S" and derf: "(f has_derivative f') (at x)" and "bounded_linear g'" "f' \ g' = id" and "T \ S" and x: "x \ interior T" shows "f x \ interior (f ` T)" proof - interpret f': bounded_linear f' using assms unfolding has_derivative_def by auto interpret g': bounded_linear g' using assms by auto obtain B where B: "0 < B" "\x. norm (g' x) \ norm x * B" using bounded_linear.pos_bounded[OF assms(5)] by blast hence *: "1 / (2 * B) > 0" by auto obtain e0 where e0: "0 < e0" "\y. norm (y - x) < e0 \ norm (f y - f x - f' (y - x)) \ 1 / (2 * B) * norm (y - x)" using derf unfolding has_derivative_at_alt using * by blast obtain e1 where e1: "0 < e1" "cball x e1 \ T" using mem_interior_cball x by blast have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B" using field_lbound_gt_zero[OF *] by blast have lem: "\y\cball (f x) e. f (x + g' (y - f x)) = z" if "z\cball (f x) (e / 2)" for z proof (rule brouwer_surjective_cball) have z: "z \ S" if as: "y \cball (f x) e" "z = x + (g' y - g' (f x))" for y z proof- have "dist x z = norm (g' (f x) - g' y)" unfolding as(2) and dist_norm by auto also have "\ \ norm (f x - y) * B" by (metis B(2) g'.diff) also have "\ \ e * B" by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1)) also have "\ \ e1" using B(1) e(3) pos_less_divide_eq by fastforce finally have "z \ cball x e1" by force then show "z \ S" using e1 assms(7) by auto qed show "continuous_on (cball (f x) e) (\y. f (x + g' (y - f x)))" unfolding g'.diff proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f]) show "continuous_on ((\y. x + (g' y - g' (f x))) ` cball (f x) e) f" by (rule continuous_on_subset[OF contf]) (use z in blast) show "continuous_on (cball (f x) e) (\y. x + (g' y - g' (f x)))" by (intro continuous_intros linear_continuous_on[OF \bounded_linear g'\]) qed next fix y z assume y: "y \ cball (f x) (e / 2)" and z: "z \ cball (f x) e" have "norm (g' (z - f x)) \ norm (z - f x) * B" using B by auto also have "\ \ e * B" by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1) also have "\ < e0" using B(1) e(2) pos_less_divide_eq by blast finally have *: "norm (x + g' (z - f x) - x) < e0" by auto have **: "f x + f' (x + g' (z - f x) - x) = z" using assms(6)[unfolded o_def id_def,THEN cong] by auto have "norm (f x - (y + (z - f (x + g' (z - f x))))) \ norm (f (x + g' (z - f x)) - z) + norm (f x - y)" using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"] by (auto simp add: algebra_simps) also have "\ \ 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)" using e0(2)[rule_format, OF *] by (simp only: algebra_simps **) auto also have "\ \ 1 / (B * 2) * norm (g' (z - f x)) + e/2" using y by (auto simp: dist_norm) also have "\ \ 1 / (B * 2) * B * norm (z - f x) + e/2" using * B by (auto simp add: field_simps) also have "\ \ 1 / 2 * norm (z - f x) + e/2" by auto also have "\ \ e/2 + e/2" using B(1) \norm (z - f x) * B \ e * B\ by auto finally show "y + (z - f (x + g' (z - f x))) \ cball (f x) e" by (auto simp: dist_norm) qed (use e that in auto) show ?thesis unfolding mem_interior proof (intro exI conjI subsetI) fix y assume "y \ ball (f x) (e / 2)" then have *: "y \ cball (f x) (e / 2)" by auto obtain z where z: "z \ cball (f x) e" "f (x + g' (z - f x)) = y" using lem * by blast then have "norm (g' (z - f x)) \ norm (z - f x) * B" using B by (auto simp add: field_simps) also have "\ \ e * B" by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1)) also have "\ \ e1" using e B unfolding less_divide_eq by auto finally have "x + g'(z - f x) \ T" by (metis add_diff_cancel diff_diff_add dist_norm e1(2) mem_cball norm_minus_commute subset_eq) then show "y \ f ` T" using z by auto qed (use e in auto) qed text \Hence the following eccentric variant of the inverse function theorem. This has no continuity assumptions, but we do need the inverse function. We could put \f' \ g = I\ but this happens to fit with the minimal linear algebra theory I've set up so far.\ lemma has_derivative_inverse_strong: fixes f :: "'n::euclidean_space \ 'n" assumes "open S" and "x \ S" and contf: "continuous_on S f" and gf: "\x. x \ S \ g (f x) = x" and derf: "(f has_derivative f') (at x)" and id: "f' \ g' = id" shows "(g has_derivative g') (at (f x))" proof - have linf: "bounded_linear f'" using derf unfolding has_derivative_def by auto then have ling: "bounded_linear g'" unfolding linear_conv_bounded_linear[symmetric] using id right_inverse_linear by blast moreover have "g' \ f' = id" using id linf ling unfolding linear_conv_bounded_linear[symmetric] using linear_inverse_left by auto moreover have *: "\T. \T \ S; x \ interior T\ \ f x \ interior (f ` T)" apply (rule sussmann_open_mapping) apply (rule assms ling)+ apply auto done have "continuous (at (f x)) g" unfolding continuous_at Lim_at proof (rule, rule) fix e :: real assume "e > 0" then have "f x \ interior (f ` (ball x e \ S))" using *[rule_format,of "ball x e \ S"] \x \ S\ by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)]) then obtain d where d: "0 < d" "ball (f x) d \ f ` (ball x e \ S)" unfolding mem_interior by blast show "\d>0. \y. 0 < dist y (f x) \ dist y (f x) < d \ dist (g y) (g (f x)) < e" proof (intro exI allI impI conjI) fix y assume "0 < dist y (f x) \ dist y (f x) < d" then have "g y \ g ` f ` (ball x e \ S)" by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff) then show "dist (g y) (g (f x)) < e" using gf[OF \x \ S\] by (simp add: assms(4) dist_commute image_iff) qed (use d in auto) qed moreover have "f x \ interior (f ` S)" apply (rule sussmann_open_mapping) apply (rule assms ling)+ using interior_open[OF assms(1)] and \x \ S\ apply auto done moreover have "f (g y) = y" if "y \ interior (f ` S)" for y by (metis gf imageE interiorE subsetD that) ultimately show ?thesis using assms by (metis has_derivative_inverse_basic_x open_interior) qed text \A rewrite based on the other domain.\ lemma has_derivative_inverse_strong_x: fixes f :: "'a::euclidean_space \ 'a" assumes "open S" and "g y \ S" and "continuous_on S f" and "\x. x \ S \ g (f x) = x" and "(f has_derivative f') (at (g y))" and "f' \ g' = id" and "f (g y) = y" shows "(g has_derivative g') (at y)" using has_derivative_inverse_strong[OF assms(1-6)] unfolding assms(7) by simp text \On a region.\ theorem has_derivative_inverse_on: fixes f :: "'n::euclidean_space \ 'n" assumes "open S" and derf: "\x. x \ S \ (f has_derivative f'(x)) (at x)" and "\x. x \ S \ g (f x) = x" and "f' x \ g' x = id" and "x \ S" shows "(g has_derivative g'(x)) (at (f x))" proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f]) show "continuous_on S f" unfolding continuous_on_eq_continuous_at[OF \open S\] using derf has_derivative_continuous by blast qed (use assms in auto) 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,2268 +1,2263 @@ (* 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_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'': \ locale comp_fun_commute = fixes f :: "'a \ 'b \ 'b" assumes comp_fun_commute: "f y \ f x = f x \ f y" begin lemma fun_left_comm: "f y (f x z) = f x (f y z)" using comp_fun_commute by (simp add: fun_eq_iff) lemma commute_left_comp: "f y \ (f x \ g) = f x \ (f y \ g)" by (simp add: o_assoc comp_fun_commute) 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 definiens 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 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: "fold_graph f z A y \ a \ A \ \y'. y = f a y' \ fold_graph f z (A - {a}) y'" 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 have "f x y = f a (f x y')" unfolding y by (rule fun_left_comm) 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 "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 _ insertI1]) lemma fold_graph_determ: "fold_graph f z A x \ fold_graph f z A y \ y = x" proof (induct arbitrary: y set: fold_graph) case emptyI then show ?case by fast next case (insertI x A y v) from \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'\ have "y' = y" by (rule insertI) with \v = f x y'\ show "v = f x y" by simp qed lemma fold_equality: "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 "finite A" shows "fold_graph f z A (fold f z A)" proof - from assms have "\x. fold_graph f z A x" by (rule finite_imp_fold_graph) moreover note fold_graph_determ 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 "finite A" and "x \ A" shows "fold f z (insert x A) = f x (fold f z A)" proof (rule fold_equality) fix z from \finite A\ have "fold_graph f z A (fold f z A)" by (rule 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: "finite A \ f x (fold f z A) = fold f (f x z) A" proof (induct rule: finite_induct) case empty then show ?case by simp next case insert then show ?case by (simp add: fun_left_comm [of x]) qed lemma fold_insert2: "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 "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) (simp add: \finite A\)+ finally show ?thesis . qed lemma fold_insert_remove: 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}))" by (rule fold_rec) then show ?thesis by simp qed lemma fold_set_union_disj: 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 assms(2,1,3) by induct simp_all end text \Other properties of \<^const>\fold\:\ 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 have "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 \ g) z A w" (is "?P \ ?Q") proof assume ?P then show ?Q 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 ?Q then show ?P 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 with True assms show ?thesis by (auto simp add: fold_def) qed lemma fold_cong: assumes "comp_fun_commute f" "comp_fun_commute g" and "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\ cong proof (induct A) case empty then show ?case by simp next case insert interpret f: comp_fun_commute f by (fact \comp_fun_commute f\) interpret g: comp_fun_commute g by (fact \comp_fun_commute 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 = comp_fun_commute + assumes comp_fun_idem: "f x \ f x = f x" begin lemma fun_left_idem: "f x (f x z) = f x z" using comp_fun_idem by (simp add: fun_eq_iff) lemma fold_insert_idem: 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 fun_left_idem) next assume "x \ A" then show ?thesis using assms by simp qed declare fold_insert [simp del] fold_insert_idem [simp] lemma fold_insert_idem2: "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\ etc.\ lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f \ g)" by standard (simp_all add: comp_fun_commute) lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f \ g)" by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales) (simp_all add: comp_fun_idem) lemma (in comp_fun_commute) comp_fun_commute_funpow: "comp_fun_commute (\x. f x ^^ g x)" proof show "f y ^^ g y \ f x ^^ g x = f x ^^ g x \ f y ^^ g y" for x 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 then show ?case by (simp add: comp_assoc hyp) (simp add: o_assoc comp_fun_commute) 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 \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 by induct (auto simp add: Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold]) 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 (* somewhat slow *) 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" using assms unfolding Sigma_def by (induct A) (simp_all add: comp_fun_commute.fold_insert[OF comp_fun_commute_product_fold] fold_union_pair) 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 end subsection \Locales as mini-packages for fold operations\ subsubsection \The natural case\ locale folding = fixes f :: "'a \ 'b \ 'b" and z :: "'b" assumes comp_fun_commute: "f y \ f x = f x \ f y" begin interpretation fold?: comp_fun_commute f by standard (use comp_fun_commute in \simp add: fun_eq_iff\) definition F :: "'a set \ 'b" where eq_fold: "F A = 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 "finite A" and "x \ A" shows "F (insert x A) = f x (F A)" proof - from fold_insert 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 lemma remove: assumes "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 by simp qed lemma insert_remove: "finite A \ F (insert x A) = f x (F (A - {x}))" by (cases "x \ A") (simp_all add: remove insert_absorb) end subsubsection \With idempotency\ locale folding_idem = folding + assumes comp_fun_idem: "f x \ f x = f x" begin declare insert [simp del] interpretation fold?: comp_fun_idem f by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff) lemma insert_idem [simp]: assumes "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 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.F (\_. Suc) 0" by standard rule lemma card_infinite: "\ finite A \ card A = 0" by (fact card.infinite) lemma card_empty: "card {} = 0" by (fact card.empty) 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: "finite A \ x \ A \ Suc (card (A - {x})) = card A" apply (rule insert_Diff [THEN subst, where t = A]) apply assumption apply (simp del: insert_Diff_single) done lemma card_insert_le_m1: "n > 0 \ card y \ n - 1 \ card (insert x y) \ n" apply (cases "finite y") apply (cases "x \ y") apply (auto simp: insert_absorb) done lemma card_Diff_singleton: "finite A \ x \ A \ card (A - {x}) = card A - 1" by (simp add: card_Suc_Diff1 [symmetric]) lemma card_Diff_singleton_if: "finite A \ 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 "finite A" and "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: "finite A \ card (insert x A) = Suc (card (A - {x}))" by (fact card.insert_remove) lemma card_insert_le: "finite A \ card A \ card (insert x A)" by (simp add: card_insert_if) 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: "finite B \ (\A. A \ B \ card B \ card A \ A = B)" apply (induct rule: finite_induct) apply simp apply clarify apply (subgoal_tac "finite A \ A - {x} \ F") prefer 2 apply (blast intro: finite_subset, atomize) apply (drule_tac x = "A - {x}" in spec) apply (simp add: card_Diff_singleton_if split: if_split_asm) apply (case_tac "card A", auto) done lemma psubset_card_mono: "finite B \ A < B \ card A < card B" apply (simp add: psubset_eq linorder_not_le [symmetric]) apply (blast dest: card_seteq) done 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_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: "finite A \ x \ A \ card (A - {x}) < card A" by (rule Suc_less_SucD) (simp add: card_Suc_Diff1 del: card_Diff_insert) lemma card_Diff2_less: "finite A \ x \ A \ y \ A \ card (A - {x} - {y}) < card A" apply (cases "x = y") apply (simp add: card_Diff1_less del:card_Diff_insert) apply (rule less_trans) prefer 2 apply (auto intro!: card_Diff1_less simp del: card_Diff_insert) done lemma card_Diff1_le: "finite A \ card (A - {x}) \ card A" by (cases "x \ A") (simp_all add: card_Diff1_less less_imp_le) 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 apply - apply (rule exI[where x = "\z. if z = x then y else f z"]) apply (auto simp add: inj_on_def) done 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 (* somewhat slow *) 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 = {}))" apply (auto elim!: card_eq_SucD) apply (subst card.insert) apply (auto simp add: intro:ccontr) done lemma card_1_singletonE: assumes "card A = 1" obtains x where "A = {x}" using assms by (auto simp: card_Suc_eq) -lemma card_2_doubletonE: - assumes "card A = Suc (Suc 0)" - obtains x y where "A = {x,y}" "x\y" - using assms by (blast dest: card_eq_SucD) - 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)" apply(cases "finite A") apply (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff dest: subset_singletonD split: nat.splits if_splits) by 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 then show ?case apply simp apply (subst card_Un_disjoint) apply (auto simp add: disjoint_eq_subset_Compl) done qed qed 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 apply (rule psubset.IH [where B = "A - {x}"]) apply (use \x \ A\ in blast) apply (simp add: \X (A - {x})\) done 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/Library/Ramsey.thy b/src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy +++ b/src/HOL/Library/Ramsey.thy @@ -1,879 +1,878 @@ (* Title: HOL/Library/Ramsey.thy Author: Tom Ridge. Full finite version by L C Paulson. *) section \Ramsey's Theorem\ theory Ramsey imports Infinite_Set FuncSet begin subsection \Preliminary definitions\ subsubsection \The $n$-element subsets of a set $A$\ definition nsets :: "['a set, nat] \ 'a set set" ("([_]\<^bsup>_\<^esup>)" [0,999] 999) where "nsets A n \ {N. N \ A \ finite N \ card N = n}" lemma nsets_mono: "A \ B \ nsets A n \ nsets B n" by (auto simp: nsets_def) lemma nsets_2_eq: "nsets A 2 = (\x\A. \y\A - {x}. {{x, y}})" - unfolding numeral_2_eq_2 - by (auto simp: nsets_def elim!: card_2_doubletonE) +by (auto simp: nsets_def card_2_iff) lemma binomial_eq_nsets: "n choose k = card (nsets {0.. finite A \ card A < r" unfolding nsets_def proof (intro iffI conjI) assume that: "{N. N \ A \ finite N \ card N = r} = {}" show "finite A" using infinite_arbitrarily_large that by auto then have "\ r \ card A" using that by (simp add: set_eq_iff) (metis finite_subset get_smaller_card [of A r]) then show "card A < r" using not_less by blast next show "{N. N \ A \ finite N \ card N = r} = {}" if "finite A \ card A < r" using that card_mono leD by auto qed lemma nsets_eq_empty: "n < r \ nsets {..x. {x}) ` A" using card_eq_SucD by (force simp: nsets_def) lemma inj_on_nsets: assumes "inj_on f A" shows "inj_on (\X. f ` X) ([A]\<^bsup>n\<^esup>)" using assms unfolding nsets_def by (metis (no_types, lifting) inj_on_inverseI inv_into_image_cancel mem_Collect_eq) lemma bij_betw_nsets: assumes "bij_betw f A B" shows "bij_betw (\X. f ` X) ([A]\<^bsup>n\<^esup>) ([B]\<^bsup>n\<^esup>)" proof - have "(`) f ` [A]\<^bsup>n\<^esup> = [f ` A]\<^bsup>n\<^esup>" using assms apply (auto simp: nsets_def bij_betw_def image_iff card_image inj_on_subset) by (metis card_image inj_on_finite order_refl subset_image_inj) with assms show ?thesis by (auto simp: bij_betw_def inj_on_nsets) qed subsubsection \Partition predicates\ definition partn :: "'a set \ nat \ nat \ 'b set \ bool" where "partn \ \ \ \ \ \f \ nsets \ \ \ \. \H \ nsets \ \. \\\\. f ` (nsets H \) \ {\}" definition partn_lst :: "'a set \ nat list \ nat \ bool" where "partn_lst \ \ \ \ \f \ nsets \ \ \ {..}. \i < length \. \H \ nsets \ (\!i). f ` (nsets H \) \ {i}" lemma partn_lst_greater_resource: fixes M::nat assumes M: "partn_lst {.. \" and "M \ N" shows "partn_lst {.. \" proof (clarsimp simp: partn_lst_def) fix f assume "f \ nsets {.. \ {..}" then have "f \ nsets {.. \ {..}" by (meson Pi_anti_mono \M \ N\ lessThan_subset_iff nsets_mono subsetD) then obtain i H where i: "i < length \" and H: "H \ nsets {.. ! i)" and subi: "f ` nsets H \ \ {i}" using M partn_lst_def by blast have "H \ nsets {.. ! i)" using \M \ N\ H by (auto simp: nsets_def subset_iff) then show "\i. \H\nsets {.. ! i). f ` nsets H \ \ {i}" using i subi by blast qed lemma partn_lst_fewer_colours: assumes major: "partn_lst \ (n#\) \" and "n \ \" shows "partn_lst \ \ \" proof (clarsimp simp: partn_lst_def) fix f :: "'a set \ nat" assume f: "f \ [\]\<^bsup>\\<^esup> \ {..}" then obtain i H where i: "i < Suc (length \)" and H: "H \ [\]\<^bsup>((n # \) ! i)\<^esup>" and hom: "\x\[H]\<^bsup>\\<^esup>. Suc (f x) = i" using \n \ \\ major [unfolded partn_lst_def, rule_format, of "Suc o f"] by (fastforce simp: image_subset_iff nsets_eq_empty_iff) show "\i. \H\nsets \ (\ ! i). f ` [H]\<^bsup>\\<^esup> \ {i}" proof (cases i) case 0 then have "[H]\<^bsup>\\<^esup> = {}" using hom by blast then show ?thesis using 0 H \n \ \\ by (simp add: nsets_eq_empty_iff) (simp add: nsets_def) next case (Suc i') then show ?thesis using i H hom by auto qed qed lemma partn_lst_eq_partn: "partn_lst {..Finite versions of Ramsey's theorem\ text \ To distinguish the finite and infinite ones, lower and upper case names are used. \ subsubsection \Trivial cases\ text \Vacuous, since we are dealing with 0-sets!\ lemma ramsey0: "\N::nat. partn_lst {..Just the pigeon hole principle, since we are dealing with 1-sets\ lemma ramsey1: "\N::nat. partn_lst {..iH\nsets {.. {i}" if "f \ nsets {.. {.. \i. {q. q \ q0+q1 \ f {q} = i}" have "A 0 \ A 1 = {..q0 + q1}" using that by (auto simp: A_def PiE_iff nsets_one lessThan_Suc_atMost le_Suc_eq) moreover have "A 0 \ A 1 = {}" by (auto simp: A_def) ultimately have "q0 + q1 \ card (A 0) + card (A 1)" by (metis card_Un_le card_atMost eq_imp_le le_SucI le_trans) then consider "card (A 0) \ q0" | "card (A 1) \ q1" by linarith then obtain i where "i < Suc (Suc 0)" "card (A i) \ [q0, q1] ! i" by (metis One_nat_def lessI nth_Cons_0 nth_Cons_Suc zero_less_Suc) then obtain B where "B \ A i" "card B = [q0, q1] ! i" "finite B" by (meson finite_subset get_smaller_card infinite_arbitrarily_large) then have "B \ nsets {.. f ` nsets B (Suc 0) \ {i}" by (auto simp: A_def nsets_def card_1_singleton_iff) then show ?thesis using \i < Suc (Suc 0)\ by auto qed then show ?thesis by (clarsimp simp: partn_lst_def) blast qed subsubsection \Ramsey's theorem with two colours and arbitrary exponents (hypergraph version)\ proposition ramsey2_full: "\N::nat. partn_lst {.. 0" by simp show ?thesis using Suc.prems proof (induct k \ "q1 + q2" arbitrary: q1 q2) case 0 show ?case proof show "partn_lst {..<1::nat} [q1, q2] (Suc r)" using nsets_empty_iff subset_insert 0 by (fastforce simp: partn_lst_def funcset_to_empty_iff nsets_eq_empty image_subset_iff) qed next case (Suc k) consider "q1 = 0 \ q2 = 0" | "q1 \ 0" "q2 \ 0" by auto then show ?case proof cases case 1 then have "partn_lst {..< Suc 0} [q1, q2] (Suc r)" unfolding partn_lst_def using \r > 0\ by (fastforce simp add: nsets_empty_iff nsets_singleton_iff lessThan_Suc) then show ?thesis by blast next case 2 with Suc have "k = (q1 - 1) + q2" "k = q1 + (q2 - 1)" by auto then obtain p1 p2::nat where p1: "partn_lst {..iH\nsets {..p} ([q1,q2] ! i). f ` nsets H (Suc r) \ {i}" if f: "f \ nsets {..p} (Suc r) \ {.. \R. f (insert p R)" have "f (insert p i) \ {.. nsets {.. nsets {.. {.. {i}" and U: "U \ nsets {.. {.. nsets {.. nsets {..p} n" if "X \ nsets {.. \R. f (u ` R)" have "h \ nsets {.. {.. {j}" and V: "V \ nsets {.. {.. u ` {.. nsets {.. nsets {.. nsets {..p} q1" unfolding nsets_def using \q1 \ 0\ card_insert_if by fastforce have invu_nsets: "inv_into {.. nsets V r" if "X \ nsets (u ` V) r" for X r proof - have "X \ u ` V \ finite X \ card X = r" using nsets_def that by auto then have [simp]: "card (inv_into {.. nsets ?W (Suc r)" for X proof (cases "p \ X") case True then have Xp: "X - {p} \ nsets (u ` V) r" using X by (auto simp: nsets_def) moreover have "u ` V \ U" using Vsub bij_betwE u by blast ultimately have "X - {p} \ nsets U r" by (meson in_mono nsets_mono) then have "g (X - {p}) = i" using gi by blast have "f X = i" using gi True \X - {p} \ nsets U r\ insert_Diff by (fastforce simp add: g_def image_subset_iff) then show ?thesis by (simp add: \f X = i\ \g (X - {p}) = i\) next case False then have Xim: "X \ nsets (u ` V) (Suc r)" using X by (auto simp: nsets_def subset_insert) then have "u ` inv_into {.. nsets {..p} q1" by (simp add: izero inq1) ultimately show ?thesis by (metis izero image_subsetI insertI1 nth_Cons_0 zero_less_Suc) next case jone then have "u ` V \ nsets {..p} q2" using V u_nsets by auto moreover have "f ` nsets (u ` V) (Suc r) \ {j}" using hj by (force simp add: h_def image_subset_iff nsets_def subset_image_inj card_image dest: finite_imageD) ultimately show ?thesis using jone not_less_eq by fastforce qed next case ione then have "U \ nsets {.. nsets {..p} n" if "X \ nsets {.. \R. f (u ` R)" have "h \ nsets {.. {.. {j}" and V: "V \ nsets {.. {.. u ` {.. nsets {.. nsets {.. nsets {..p} q2" unfolding nsets_def using \q2 \ 0\ card_insert_if by fastforce have invu_nsets: "inv_into {.. nsets V r" if "X \ nsets (u ` V) r" for X r proof - have "X \ u ` V \ finite X \ card X = r" using nsets_def that by auto then have [simp]: "card (inv_into {.. nsets ?W (Suc r)" for X proof (cases "p \ X") case True then have Xp: "X - {p} \ nsets (u ` V) r" using X by (auto simp: nsets_def) moreover have "u ` V \ U" using Vsub bij_betwE u by blast ultimately have "X - {p} \ nsets U r" by (meson in_mono nsets_mono) then have "g (X - {p}) = i" using gi by blast have "f X = i" using gi True \X - {p} \ nsets U r\ insert_Diff by (fastforce simp add: g_def image_subset_iff) then show ?thesis by (simp add: \f X = i\ \g (X - {p}) = i\) next case False then have Xim: "X \ nsets (u ` V) (Suc r)" using X by (auto simp: nsets_def subset_insert) then have "u ` inv_into {.. nsets {..p} q2" by (simp add: ione inq1) ultimately show ?thesis by (metis ione image_subsetI insertI1 lessI nth_Cons_0 nth_Cons_Suc) next case jzero then have "u ` V \ nsets {..p} q1" using V u_nsets by auto moreover have "f ` nsets (u ` V) (Suc r) \ {j}" using hj apply (clarsimp simp add: h_def image_subset_iff nsets_def) by (metis Zero_not_Suc card_eq_0_iff card_image subset_image_inj) ultimately show ?thesis using jzero not_less_eq by fastforce qed qed qed then show "partn_lst {..Full Ramsey's theorem with multiple colours and arbitrary exponents\ theorem ramsey_full: "\N::nat. partn_lst {.. "length qs" arbitrary: qs) case 0 then show ?case by (rule_tac x=" r" in exI) (simp add: partn_lst_def) next case (Suc k) note IH = this show ?case proof (cases k) case 0 with Suc obtain q where "qs = [q]" by (metis length_0_conv length_Suc_conv) then show ?thesis by (rule_tac x=q in exI) (auto simp: partn_lst_def funcset_to_empty_iff) next case (Suc k') then obtain q1 q2 l where qs: "qs = q1#q2#l" by (metis Suc.hyps(2) length_Suc_conv) then obtain q::nat where q: "partn_lst {..qs = q1 # q2 # l\ by fastforce have keq: "Suc (length l) = k" using IH qs by auto show ?thesis proof (intro exI conjI) show "partn_lst {.. nsets {.. {.. \X. if f X < Suc (Suc 0) then 0 else f X - Suc 0" have "g \ nsets {.. {.. {i}" and U: "U \ nsets {..iH\nsets {.. {i}" proof (cases "i = 0") case True then have "U \ nsets {.. {0, Suc 0}" using U gi unfolding g_def by (auto simp: image_subset_iff) then obtain u where u: "bij_betw u {.. {..U \ nsets {.. mem_Collect_eq nsets_def) have u_nsets: "u ` X \ nsets {.. nsets {.. \X. f (u ` X)" have "f (u ` X) < Suc (Suc 0)" if "X \ nsets {.. nsets U r" using u u_nsets that by (auto simp: nsets_def bij_betwE subset_eq) then show ?thesis using f01 by auto qed then have "h \ nsets {.. {.. {j}" and V: "V \ nsets {.. (\x. (u ` x)) ` nsets V r" apply (clarsimp simp add: nsets_def image_iff) by (metis card_eq_0_iff card_image image_is_empty subset_image_inj) then have "f ` nsets (u ` V) r \ h ` nsets V r" by (auto simp: h_def) then show "f ` nsets (u ` V) r \ {j}" using hj by auto show "(u ` V) \ nsets {.. {Suc i}" using i gi False apply (auto simp: g_def image_subset_iff) by (metis Suc_lessD Suc_pred g_def gi image_subset_iff not_less_eq singleton_iff) show "U \ nsets {..Simple graph version\ text \This is the most basic version in terms of cliques and independent sets, i.e. the version for graphs and 2 colours. \ definition "clique V E \ (\v\V. \w\V. v \ w \ {v, w} \ E)" definition "indep V E \ (\v\V. \w\V. v \ w \ {v, w} \ E)" lemma ramsey2: "\r\1. \(V::'a set) (E::'a set set). finite V \ card V \ r \ (\R \ V. card R = m \ clique R E \ card R = n \ indep R E)" proof - obtain N where "N \ Suc 0" and N: "partn_lst {..R\V. card R = m \ clique R E \ card R = n \ indep R E" if "finite V" "N \ card V" for V :: "'a set" and E :: "'a set set" proof - from that obtain v where u: "inj_on v {.. V" by (metis card_le_inj card_lessThan finite_lessThan) define f where "f \ \e. if v ` e \ E then 0 else Suc 0" have f: "f \ nsets {.. {.. {i}" and U: "U \ nsets {.. V" using U u by (auto simp: image_subset_iff nsets_def) show "card (v ` U) = m \ clique (v ` U) E \ card (v ` U) = n \ indep (v ` U) E" using i unfolding numeral_2_eq_2 using gi U u apply (simp add: image_subset_iff nsets_2_eq clique_def indep_def less_Suc_eq) apply (auto simp: f_def nsets_def card_image inj_on_subset split: if_split_asm) done qed qed then show ?thesis using \Suc 0 \ N\ by auto qed subsection \Preliminaries\ subsubsection \``Axiom'' of Dependent Choice\ primrec choice :: "('a \ bool) \ ('a \ 'a) set \ nat \ 'a" where \ \An integer-indexed chain of choices\ choice_0: "choice P r 0 = (SOME x. P x)" | choice_Suc: "choice P r (Suc n) = (SOME y. P y \ (choice P r n, y) \ r)" lemma choice_n: assumes P0: "P x0" and Pstep: "\x. P x \ \y. P y \ (x, y) \ r" shows "P (choice P r n)" proof (induct n) case 0 show ?case by (force intro: someI P0) next case Suc then show ?case by (auto intro: someI2_ex [OF Pstep]) qed lemma dependent_choice: assumes trans: "trans r" and P0: "P x0" and Pstep: "\x. P x \ \y. P y \ (x, y) \ r" obtains f :: "nat \ 'a" where "\n. P (f n)" and "\n m. n < m \ (f n, f m) \ r" proof fix n show "P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep]) next fix n m :: nat assume "n < m" from Pstep [OF choice_n [OF P0 Pstep]] have "(choice P r k, choice P r (Suc k)) \ r" for k by (auto intro: someI2_ex) then show "(choice P r n, choice P r m) \ r" by (auto intro: less_Suc_induct [OF \n < m\] transD [OF trans]) qed subsubsection \Partition functions\ definition part_fn :: "nat \ nat \ 'a set \ ('a set \ nat) \ bool" \ \the function \<^term>\f\ partitions the \<^term>\r\-subsets of the typically infinite set \<^term>\Y\ into \<^term>\s\ distinct categories.\ where "part_fn r s Y f \ (f \ nsets Y r \ {..For induction, we decrease the value of \<^term>\r\ in partitions.\ lemma part_fn_Suc_imp_part_fn: "\infinite Y; part_fn (Suc r) s Y f; y \ Y\ \ part_fn r s (Y - {y}) (\u. f (insert y u))" by (simp add: part_fn_def nsets_def Pi_def subset_Diff_insert) lemma part_fn_subset: "part_fn r s YY f \ Y \ YY \ part_fn r s Y f" unfolding part_fn_def nsets_def by blast subsection \Ramsey's Theorem: Infinitary Version\ lemma Ramsey_induction: fixes s r :: nat and YY :: "'a set" and f :: "'a set \ nat" assumes "infinite YY" "part_fn r s YY f" shows "\Y' t'. Y' \ YY \ infinite Y' \ t' < s \ (\X. X \ Y' \ finite X \ card X = r \ f X = t')" using assms proof (induct r arbitrary: YY f) case 0 then show ?case by (auto simp add: part_fn_def card_eq_0_iff cong: conj_cong) next case (Suc r) show ?case proof - from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \ YY" by blast let ?ramr = "{((y, Y, t), (y', Y', t')). y' \ Y \ Y' \ Y}" let ?propr = "\(y, Y, t). y \ YY \ y \ Y \ Y \ YY \ infinite Y \ t < s \ (\X. X\Y \ finite X \ card X = r \ (f \ insert y) X = t)" from Suc.prems have infYY': "infinite (YY - {yy})" by auto from Suc.prems have partf': "part_fn r s (YY - {yy}) (f \ insert yy)" by (simp add: o_def part_fn_Suc_imp_part_fn yy) have transr: "trans ?ramr" by (force simp add: trans_def) from Suc.hyps [OF infYY' partf'] obtain Y0 and t0 where "Y0 \ YY - {yy}" "infinite Y0" "t0 < s" "X \ Y0 \ finite X \ card X = r \ (f \ insert yy) X = t0" for X by blast with yy have propr0: "?propr(yy, Y0, t0)" by blast have proprstep: "\y. ?propr y \ (x, y) \ ?ramr" if x: "?propr x" for x proof (cases x) case (fields yx Yx tx) with x obtain yx' where yx': "yx' \ Yx" by (blast dest: infinite_imp_nonempty) from fields x have infYx': "infinite (Yx - {yx'})" by auto with fields x yx' Suc.prems have partfx': "part_fn r s (Yx - {yx'}) (f \ insert yx')" by (simp add: o_def part_fn_Suc_imp_part_fn part_fn_subset [where YY=YY and Y=Yx]) from Suc.hyps [OF infYx' partfx'] obtain Y' and t' where Y': "Y' \ Yx - {yx'}" "infinite Y'" "t' < s" "X \ Y' \ finite X \ card X = r \ (f \ insert yx') X = t'" for X by blast from fields x Y' yx' have "?propr (yx', Y', t') \ (x, (yx', Y', t')) \ ?ramr" by blast then show ?thesis .. qed from dependent_choice [OF transr propr0 proprstep] obtain g where pg: "?propr (g n)" and rg: "n < m \ (g n, g m) \ ?ramr" for n m :: nat by blast let ?gy = "fst \ g" let ?gt = "snd \ snd \ g" have rangeg: "\k. range ?gt \ {.. range ?gt" then obtain n where "x = ?gt n" .. with pg [of n] show "x \ {.. ?gy m'" by (cases "g m", cases "g m'") auto qed show ?thesis proof (intro exI conjI) from pg show "?gy ` {n. ?gt n = s'} \ YY" by (auto simp add: Let_def split_beta) from infeqs' show "infinite (?gy ` {n. ?gt n = s'})" by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD) show "s' < s" by (rule less') show "\X. X \ ?gy ` {n. ?gt n = s'} \ finite X \ card X = Suc r \ f X = s'" proof - have "f X = s'" if X: "X \ ?gy ` {n. ?gt n = s'}" and cardX: "finite X" "card X = Suc r" for X proof - from X obtain AA where AA: "AA \ {n. ?gt n = s'}" and Xeq: "X = ?gy`AA" by (auto simp add: subset_image_iff) with cardX have "AA \ {}" by auto then have AAleast: "(LEAST x. x \ AA) \ AA" by (auto intro: LeastI_ex) show ?thesis proof (cases "g (LEAST x. x \ AA)") case (fields ya Ya ta) with AAleast Xeq have ya: "ya \ X" by (force intro!: rev_image_eqI) then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb) also have "\ = ta" proof - have *: "X - {ya} \ Ya" proof fix x assume x: "x \ X - {ya}" then obtain a' where xeq: "x = ?gy a'" and a': "a' \ AA" by (auto simp add: Xeq) with fields x have "a' \ (LEAST x. x \ AA)" by auto with Least_le [of "\x. x \ AA", OF a'] have "(LEAST x. x \ AA) < a'" by arith from xeq fields rg [OF this] show "x \ Ya" by auto qed have "card (X - {ya}) = r" by (simp add: cardX ya) with pg [of "LEAST x. x \ AA"] fields cardX * show ?thesis by (auto simp del: insert_Diff_single) qed also from AA AAleast fields have "\ = s'" by auto finally show ?thesis . qed qed then show ?thesis by blast qed qed qed qed theorem Ramsey: fixes s r :: nat and Z :: "'a set" and f :: "'a set \ nat" shows "\infinite Z; \X. X \ Z \ finite X \ card X = r \ f X < s\ \ \Y t. Y \ Z \ infinite Y \ t < s \ (\X. X \ Y \ finite X \ card X = r \ f X = t)" by (blast intro: Ramsey_induction [unfolded part_fn_def nsets_def]) corollary Ramsey2: fixes s :: nat and Z :: "'a set" and f :: "'a set \ nat" assumes infZ: "infinite Z" and part: "\x\Z. \y\Z. x \ y \ f {x, y} < s" shows "\Y t. Y \ Z \ infinite Y \ t < s \ (\x\Y. \y\Y. x\y \ f {x, y} = t)" proof - from part have part2: "\X. X \ Z \ finite X \ card X = 2 \ f X < s" by (fastforce simp add: eval_nat_numeral card_Suc_eq) obtain Y t where *: "Y \ Z" "infinite Y" "t < s" "(\X. X \ Y \ finite X \ card X = 2 \ f X = t)" by (insert Ramsey [OF infZ part2]) auto then have "\x\Y. \y\Y. x \ y \ f {x, y} = t" by auto with * show ?thesis by iprover qed subsection \Disjunctive Well-Foundedness\ text \ An application of Ramsey's theorem to program termination. See @{cite "Podelski-Rybalchenko"}. \ definition disj_wf :: "('a \ 'a) set \ bool" where "disj_wf r \ (\T. \n::nat. (\i r = (\i 'a) \ (nat \ ('a \ 'a) set) \ nat set \ nat" where "transition_idx s T A = (LEAST k. \i j. A = {i, j} \ i < j \ (s j, s i) \ T k)" lemma transition_idx_less: assumes "i < j" "(s j, s i) \ T k" "k < n" shows "transition_idx s T {i, j} < n" proof - from assms(1,2) have "transition_idx s T {i, j} \ k" by (simp add: transition_idx_def, blast intro: Least_le) with assms(3) show ?thesis by simp qed lemma transition_idx_in: assumes "i < j" "(s j, s i) \ T k" shows "(s j, s i) \ T (transition_idx s T {i, j})" using assms by (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR cong: conj_cong) (erule LeastI) text \To be equal to the union of some well-founded relations is equivalent to being the subset of such a union.\ lemma disj_wf: "disj_wf r \ (\T. \n::nat. (\i r \ (\iT n. \\i \ (T ` {.. \ (\i r)) \ r = (\i r)" by (force simp add: wf_Int1) show ?thesis unfolding disj_wf_def by auto (metis "*") qed theorem trans_disj_wf_implies_wf: assumes "trans r" and "disj_wf r" shows "wf r" proof (simp only: wf_iff_no_infinite_down_chain, rule notI) assume "\s. \i. (s (Suc i), s i) \ r" then obtain s where sSuc: "\i. (s (Suc i), s i) \ r" .. from \disj_wf r\ obtain T and n :: nat where wfT: "\kkk. (s j, s i) \ T k \ ki < j\ have "(s j, s i) \ r" proof (induct rule: less_Suc_induct) case 1 then show ?case by (simp add: sSuc) next case 2 with \trans r\ show ?case unfolding trans_def by blast qed then show ?thesis by (auto simp add: r) qed have "i < j \ transition_idx s T {i, j} < n" for i j using s_in_T transition_idx_less by blast then have trless: "i \ j \ transition_idx s T {i, j} < n" for i j by (metis doubleton_eq_iff less_linear) have "\K k. K \ UNIV \ infinite K \ k < n \ (\i\K. \j\K. i \ j \ transition_idx s T {i, j} = k)" by (rule Ramsey2) (auto intro: trless infinite_UNIV_nat) then obtain K and k where infK: "infinite K" and "k < n" and allk: "\i\K. \j\K. i \ j \ transition_idx s T {i, j} = k" by auto have "(s (enumerate K (Suc m)), s (enumerate K m)) \ T k" for m :: nat proof - let ?j = "enumerate K (Suc m)" let ?i = "enumerate K m" have ij: "?i < ?j" by (simp add: enumerate_step infK) have "?j \ K" "?i \ K" by (simp_all add: enumerate_in_set infK) with ij have k: "k = transition_idx s T {?i, ?j}" by (simp add: allk) from s_in_T [OF ij] obtain k' where "(s ?j, s ?i) \ T k'" "k' T k" by (simp add: k transition_idx_in ij) qed then have "\ wf (T k)" by (meson wf_iff_no_infinite_down_chain) with wfT \k < n\ show False by blast qed end diff --git a/src/HOL/Set_Interval.thy b/src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy +++ b/src/HOL/Set_Interval.thy @@ -1,2509 +1,2516 @@ (* Title: HOL/Set_Interval.thy Author: Tobias Nipkow, Clemens Ballarin, Jeremy Avigad lessThan, greaterThan, atLeast, atMost and two-sided intervals Modern convention: Ixy stands for an interval where x and y describe the lower and upper bound and x,y : {c,o,i} where c = closed, o = open, i = infinite. Examples: Ico = {_ ..< _} and Ici = {_ ..} *) section \Set intervals\ theory Set_Interval imports Divides begin +(* Belongs in Finite_Set but 2 is not available there *) +lemma card_2_iff: "card S = 2 \ (\x y. S = {x,y} \ x \ y)" +by (auto simp: card_Suc_eq numeral_eq_Suc) + +lemma card_2_iff': "card S = 2 \ (\x\S. \y\S. x \ y \ (\z\S. z = x \ z = y))" +by (auto simp: card_Suc_eq numeral_eq_Suc) + context ord begin definition lessThan :: "'a => 'a set" ("(1{..<_})") where "{.. 'a set" ("(1{.._})") where "{..u} == {x. x \ u}" definition greaterThan :: "'a => 'a set" ("(1{_<..})") where "{l<..} == {x. l 'a set" ("(1{_..})") where "{l..} == {x. l\x}" definition greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where "{l<.. 'a => 'a set" ("(1{_..<_})") where "{l.. 'a => 'a set" ("(1{_<.._})") where "{l<..u} == {l<..} Int {..u}" definition atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where "{l..u} == {l..} Int {..u}" end text\A note of warning when using \<^term>\{.. on type \<^typ>\nat\: it is equivalent to \<^term>\{0::nat.. but some lemmas involving \<^term>\{m.. may not exist in \<^term>\{..-form as well.\ syntax (ASCII) "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10) "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10) "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10) "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10) syntax (latex output) "_UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ \ _)/ _)" [0, 0, 10] 10) "_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10) "_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ \ _)/ _)" [0, 0, 10] 10) "_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10) syntax "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10) "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\_<_./ _)" [0, 0, 10] 10) "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10) "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\_<_./ _)" [0, 0, 10] 10) translations "\i\n. A" \ "\i\{..n}. A" "\i "\i\{..i\n. A" \ "\i\{..n}. A" "\i "\i\{..Various equivalences\ lemma (in ord) lessThan_iff [iff]: "(i \ lessThan k) = (i greaterThan k) = (k atLeast k) = (k<=i)" by (simp add: atLeast_def) lemma Compl_atLeast [simp]: "!!k:: 'a::linorder. -atLeast k = lessThan k" by (auto simp add: lessThan_def atLeast_def) lemma (in ord) atMost_iff [iff]: "(i \ atMost k) = (i<=k)" by (simp add: atMost_def) lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" by (blast intro: order_antisym) lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \ { b <..} = { max a b <..}" by auto lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \ {..< b} = {..< min a b}" by auto subsection \Logical Equivalences for Set Inclusion and Equality\ lemma atLeast_empty_triv [simp]: "{{}..} = UNIV" by auto lemma atMost_UNIV_triv [simp]: "{..UNIV} = UNIV" by auto lemma atLeast_subset_iff [iff]: "(atLeast x \ atLeast y) = (y \ (x::'a::preorder))" by (blast intro: order_trans) lemma atLeast_eq_iff [iff]: "(atLeast x = atLeast y) = (x = (y::'a::order))" by (blast intro: order_antisym order_trans) lemma greaterThan_subset_iff [iff]: "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))" unfolding greaterThan_def by (auto simp: linorder_not_less [symmetric]) lemma greaterThan_eq_iff [iff]: "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" by (auto simp: elim!: equalityE) lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::preorder))" by (blast intro: order_trans) lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::order))" by (blast intro: order_antisym order_trans) lemma lessThan_subset_iff [iff]: "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))" unfolding lessThan_def by (auto simp: linorder_not_less [symmetric]) lemma lessThan_eq_iff [iff]: "(lessThan x = lessThan y) = (x = (y::'a::linorder))" by (auto simp: elim!: equalityE) lemma lessThan_strict_subset_iff: fixes m n :: "'a::linorder" shows "{.. m < n" by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq) lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \ {b <..} \ b < a" by auto lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \ {..< b} \ a < b" by auto lemma (in preorder) Ioi_le_Ico: "{a <..} \ {a ..}" by (auto intro: less_imp_le) subsection \Two-sided intervals\ context ord begin lemma greaterThanLessThan_iff [simp]: "(i \ {l<.. i < u)" by (simp add: greaterThanLessThan_def) lemma atLeastLessThan_iff [simp]: "(i \ {l.. i \ i < u)" by (simp add: atLeastLessThan_def) lemma greaterThanAtMost_iff [simp]: "(i \ {l<..u}) = (l < i \ i \ u)" by (simp add: greaterThanAtMost_def) lemma atLeastAtMost_iff [simp]: "(i \ {l..u}) = (l \ i \ i \ u)" by (simp add: atLeastAtMost_def) text \The above four lemmas could be declared as iffs. Unfortunately this breaks many proofs. Since it only helps blast, it is better to leave them alone.\ lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \ {..< b }" by auto lemma (in order) atLeastLessThan_eq_atLeastAtMost_diff: "{a..Emptyness, singletons, subset\ context preorder begin lemma atLeastatMost_empty_iff[simp]: "{a..b} = {} \ (\ a \ b)" by auto (blast intro: order_trans) lemma atLeastatMost_empty_iff2[simp]: "{} = {a..b} \ (\ a \ b)" by auto (blast intro: order_trans) lemma atLeastLessThan_empty_iff[simp]: "{a.. (\ a < b)" by auto (blast intro: le_less_trans) lemma atLeastLessThan_empty_iff2[simp]: "{} = {a.. (\ a < b)" by auto (blast intro: le_less_trans) lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ \ k < l" by auto (blast intro: less_le_trans) lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ \ k < l" by auto (blast intro: less_le_trans) lemma atLeastatMost_subset_iff[simp]: "{a..b} \ {c..d} \ (\ a \ b) \ c \ a \ b \ d" unfolding atLeastAtMost_def atLeast_def atMost_def by (blast intro: order_trans) lemma atLeastatMost_psubset_iff: "{a..b} < {c..d} \ ((\ a \ b) \ c \ a \ b \ d \ (c < a \ b < d)) \ c \ d" by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) lemma atLeastAtMost_subseteq_atLeastLessThan_iff: "{a..b} \ {c ..< d} \ (a \ b \ c \ a \ b < d)" by auto (blast intro: local.order_trans local.le_less_trans elim: )+ lemma Icc_subset_Ici_iff[simp]: "{l..h} \ {l'..} = (\ l\h \ l\l')" by(auto simp: subset_eq intro: order_trans) lemma Icc_subset_Iic_iff[simp]: "{l..h} \ {..h'} = (\ l\h \ h\h')" by(auto simp: subset_eq intro: order_trans) lemma not_Ici_eq_empty[simp]: "{l..} \ {}" by(auto simp: set_eq_iff) lemma not_Iic_eq_empty[simp]: "{..h} \ {}" by(auto simp: set_eq_iff) lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric] lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric] end context order begin lemma atLeastatMost_empty[simp]: "b < a \ {a..b} = {}" by(auto simp: atLeastAtMost_def atLeast_def atMost_def) lemma atLeastLessThan_empty[simp]: "b \ a \ {a.. k ==> {k<..l} = {}" by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp lemma Icc_eq_Icc[simp]: "{l..h} = {l'..h'} = (l=l' \ h=h' \ \ l\h \ \ l'\h')" by(simp add: order_class.eq_iff)(auto intro: order_trans) lemma atLeastAtMost_singleton_iff[simp]: "{a .. b} = {c} \ a = b \ b = c" proof assume "{a..b} = {c}" hence *: "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp with \{a..b} = {c}\ have "c \ a \ b \ c" by auto with * show "a = b \ b = c" by auto qed simp end context no_top begin (* also holds for no_bot but no_top should suffice *) lemma not_UNIV_le_Icc[simp]: "\ UNIV \ {l..h}" using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) lemma not_UNIV_le_Iic[simp]: "\ UNIV \ {..h}" using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) lemma not_Ici_le_Icc[simp]: "\ {l..} \ {l'..h'}" using gt_ex[of h'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) lemma not_Ici_le_Iic[simp]: "\ {l..} \ {..h'}" using gt_ex[of h'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) end context no_bot begin lemma not_UNIV_le_Ici[simp]: "\ UNIV \ {l..}" using lt_ex[of l] by(auto simp: subset_eq less_le_not_le) lemma not_Iic_le_Icc[simp]: "\ {..h} \ {l'..h'}" using lt_ex[of l'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) lemma not_Iic_le_Ici[simp]: "\ {..h} \ {l'..}" using lt_ex[of l'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) end context no_top begin (* also holds for no_bot but no_top should suffice *) lemma not_UNIV_eq_Icc[simp]: "\ UNIV = {l'..h'}" using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric] lemma not_UNIV_eq_Iic[simp]: "\ UNIV = {..h'}" using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric] lemma not_Icc_eq_Ici[simp]: "\ {l..h} = {l'..}" unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric] (* also holds for no_bot but no_top should suffice *) lemma not_Iic_eq_Ici[simp]: "\ {..h} = {l'..}" using not_Ici_le_Iic[of l' h] by blast lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric] end context no_bot begin lemma not_UNIV_eq_Ici[simp]: "\ UNIV = {l'..}" using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le) lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric] lemma not_Icc_eq_Iic[simp]: "\ {l..h} = {..h'}" unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric] end context dense_linorder begin lemma greaterThanLessThan_empty_iff[simp]: "{ a <..< b } = {} \ b \ a" using dense[of a b] by (cases "a < b") auto lemma greaterThanLessThan_empty_iff2[simp]: "{} = { a <..< b } \ b \ a" using dense[of a b] by (cases "a < b") auto lemma atLeastLessThan_subseteq_atLeastAtMost_iff: "{a ..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)" using dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: "{a <.. b} \ { c .. d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: "{a <..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_greaterThanLessThan: "{a <..< b} \ {c <..< d} \ (a < b \ a \ c \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: "{a <.. b} \ { c ..< d } \ (a < b \ c \ a \ b < d)" using dense[of "a" "min c b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: "{a <..< b} \ { c ..< d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff: "{a <..< b} \ { c <.. d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) end context no_top begin lemma greaterThan_non_empty[simp]: "{x <..} \ {}" using gt_ex[of x] by auto end context no_bot begin lemma lessThan_non_empty[simp]: "{..< x} \ {}" using lt_ex[of x] by auto end lemma (in linorder) atLeastLessThan_subset_iff: "{a.. {c.. b \ a \ c\a \ b\d" apply (auto simp:subset_eq Ball_def not_le) apply(frule_tac x=a in spec) apply(erule_tac x=d in allE) apply (auto simp: ) done lemma atLeastLessThan_inj: fixes a b c d :: "'a::linorder" assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d" shows "a = c" "b = d" using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le antisym_conv2 subset_refl)+ lemma atLeastLessThan_eq_iff: fixes a b c d :: "'a::linorder" assumes "a < b" "c < d" shows "{a ..< b} = {c ..< d} \ a = c \ b = d" using atLeastLessThan_inj assms by auto lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \ (b \ a \ d \ c) \ a = c \ b = d" by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le) lemma (in order) Iio_Int_singleton: "{.. {x} = (if x < k then {x} else {})" by auto lemma (in linorder) Ioc_subset_iff: "{a<..b} \ {c<..d} \ (b \ a \ c \ a \ b \ d)" by (auto simp: subset_eq Ball_def) (metis less_le not_less) lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot" by (auto simp: set_eq_iff intro: le_bot) lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \ x = top" by (auto simp: set_eq_iff intro: top_le) lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff: "{x..y} = UNIV \ (x = bot \ y = top)" by (auto simp: set_eq_iff intro: top_le le_bot) lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \ n = bot" by (auto simp: set_eq_iff not_less le_bot) lemma lessThan_empty_iff: "{..< n::nat} = {} \ n = 0" by (simp add: Iio_eq_empty_iff bot_nat_def) lemma mono_image_least: assumes f_mono: "mono f" and f_img: "f ` {m ..< n} = {m' ..< n'}" "m < n" shows "f m = m'" proof - from f_img have "{m' ..< n'} \ {}" by (metis atLeastLessThan_empty_iff image_is_empty) with f_img have "m' \ f ` {m ..< n}" by auto then obtain k where "f k = m'" "m \ k" by auto moreover have "m' \ f m" using f_img by auto ultimately show "f m = m'" using f_mono by (auto elim: monoE[where x=m and y=k]) qed subsection \Infinite intervals\ context dense_linorder begin lemma infinite_Ioo: assumes "a < b" shows "\ finite {a<.. {}" using \a < b\ by auto ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b" using Max_in[of "{a <..< b}"] by auto then obtain x where "Max {a <..< b} < x" "x < b" using dense[of "Max {a<.. {a <..< b}" using \a < Max {a <..< b}\ by auto then have "x \ Max {a <..< b}" using fin by auto with \Max {a <..< b} < x\ show False by auto qed lemma infinite_Icc: "a < b \ \ finite {a .. b}" using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b] by (auto dest: finite_subset) lemma infinite_Ico: "a < b \ \ finite {a ..< b}" using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b] by (auto dest: finite_subset) lemma infinite_Ioc: "a < b \ \ finite {a <.. b}" using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b] by (auto dest: finite_subset) lemma infinite_Ioo_iff [simp]: "infinite {a<.. a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioo) lemma infinite_Icc_iff [simp]: "infinite {a .. b} \ a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Icc) lemma infinite_Ico_iff [simp]: "infinite {a.. a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ico) lemma infinite_Ioc_iff [simp]: "infinite {a<..b} \ a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioc) end lemma infinite_Iio: "\ finite {..< a :: 'a :: {no_bot, linorder}}" proof assume "finite {..< a}" then have *: "\x. x < a \ Min {..< a} \ x" by auto obtain x where "x < a" using lt_ex by auto obtain y where "y < Min {..< a}" using lt_ex by auto also have "Min {..< a} \ x" using \x < a\ by fact also note \x < a\ finally have "Min {..< a} \ y" by fact with \y < Min {..< a}\ show False by auto qed lemma infinite_Iic: "\ finite {.. a :: 'a :: {no_bot, linorder}}" using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"] by (auto simp: subset_eq less_imp_le) lemma infinite_Ioi: "\ finite {a :: 'a :: {no_top, linorder} <..}" proof assume "finite {a <..}" then have *: "\x. a < x \ x \ Max {a <..}" by auto obtain y where "Max {a <..} < y" using gt_ex by auto obtain x where x: "a < x" using gt_ex by auto also from x have "x \ Max {a <..}" by fact also note \Max {a <..} < y\ finally have "y \ Max { a <..}" by fact with \Max {a <..} < y\ show False by auto qed lemma infinite_Ici: "\ finite {a :: 'a :: {no_top, linorder} ..}" using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"] by (auto simp: subset_eq less_imp_le) subsubsection \Intersection\ context linorder begin lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}" by auto lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}" by auto lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}" by auto lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}" by auto lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}" by auto lemma Int_atLeastLessThan[simp]: "{a.. {..b} = {.. min a b}" by (auto simp: min_def) lemma Ioc_disjoint: "{a<..b} \ {c<..d} = {} \ b \ a \ d \ c \ b \ c \ d \ a" by auto end context complete_lattice begin lemma shows Sup_atLeast[simp]: "Sup {x ..} = top" and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top" and Sup_atMost[simp]: "Sup {.. y} = y" and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y" and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y" by (auto intro!: Sup_eqI) lemma shows Inf_atMost[simp]: "Inf {.. x} = bot" and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot" and Inf_atLeast[simp]: "Inf {x ..} = x" and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x" and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x" by (auto intro!: Inf_eqI) end lemma fixes x y :: "'a :: {complete_lattice, dense_linorder}" shows Sup_lessThan[simp]: "Sup {..< y} = y" and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y" and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y" and Inf_greaterThan[simp]: "Inf {x <..} = x" and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x" and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x" by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded) subsection \Intervals of natural numbers\ subsubsection \The Constant \<^term>\lessThan\\ lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" by (simp add: lessThan_def) lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" by (simp add: lessThan_def less_Suc_eq, blast) text \The following proof is convenient in induction proofs where new elements get indices at the beginning. So it is used to transform \<^term>\{.. to \<^term>\0::nat\ and \<^term>\{..< n}\.\ lemma zero_notin_Suc_image [simp]: "0 \ Suc ` A" by auto lemma lessThan_Suc_eq_insert_0: "{..m::nat. lessThan m) = UNIV" by blast subsubsection \The Constant \<^term>\greaterThan\\ lemma greaterThan_0: "greaterThan 0 = range Suc" unfolding greaterThan_def by (blast dest: gr0_conv_Suc [THEN iffD1]) lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}" unfolding greaterThan_def by (auto elim: linorder_neqE) lemma INT_greaterThan_UNIV: "(\m::nat. greaterThan m) = {}" by blast subsubsection \The Constant \<^term>\atLeast\\ lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" by (unfold atLeast_def UNIV_def, simp) lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}" unfolding atLeast_def by (auto simp: order_le_less Suc_le_eq) lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k" by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) lemma UN_atLeast_UNIV: "(\m::nat. atLeast m) = UNIV" by blast subsubsection \The Constant \<^term>\atMost\\ lemma atMost_0 [simp]: "atMost (0::nat) = {0}" by (simp add: atMost_def) lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" unfolding atMost_def by (auto simp add: less_Suc_eq order_le_less) lemma UN_atMost_UNIV: "(\m::nat. atMost m) = UNIV" by blast subsubsection \The Constant \<^term>\atLeastLessThan\\ text\The orientation of the following 2 rules is tricky. The lhs is defined in terms of the rhs. Hence the chosen orientation makes sense in this theory --- the reverse orientation complicates proofs (eg nontermination). But outside, when the definition of the lhs is rarely used, the opposite orientation seems preferable because it reduces a specific concept to a more general one.\ lemma atLeast0LessThan [code_abbrev]: "{0::nat..The Constant \<^term>\atLeastAtMost\\ lemma Icc_eq_insert_lb_nat: "m \ n \ {m..n} = insert m {Suc m..n}" by auto lemma atLeast0_atMost_Suc: "{0..Suc n} = insert (Suc n) {0..n}" by (simp add: atLeast0AtMost atMost_Suc) lemma atLeast0_atMost_Suc_eq_insert_0: "{0..Suc n} = insert 0 (Suc ` {0..n})" by (simp add: atLeast0AtMost atMost_Suc_eq_insert_0) subsubsection \Intervals of nats with \<^term>\Suc\\ text\Not a simprule because the RHS is too messy.\ lemma atLeastLessThanSuc: "{m.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}" by (auto simp add: atLeastAtMost_def) lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}" by auto text \The analogous result is useful on \<^typ>\int\:\ (* here, because we don't have an own int section *) lemma atLeastAtMostPlus1_int_conv: "m \ 1+n \ {m..1+n} = insert (1+n) {m..n::int}" by (auto intro: set_eqI) lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j..Intervals and numerals\ lemma lessThan_nat_numeral: \ \Evaluation for specific numerals\ "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))" by (simp add: numeral_eq_Suc lessThan_Suc) lemma atMost_nat_numeral: \ \Evaluation for specific numerals\ "atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))" by (simp add: numeral_eq_Suc atMost_Suc) lemma atLeastLessThan_nat_numeral: \ \Evaluation for specific numerals\ "atLeastLessThan m (numeral k :: nat) = (if m \ (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k)) else {})" by (simp add: numeral_eq_Suc atLeastLessThanSuc) subsubsection \Image\ context linordered_semidom begin lemma image_add_atLeast[simp]: "plus k ` {i..} = {k + i..}" proof - have "n = k + (n - k)" if "i + k \ n" for n proof - have "n = (n - (k + i)) + (k + i)" using that by (metis add_commute le_add_diff_inverse) then show "n = k + (n - k)" by (metis local.add_diff_cancel_left' add_assoc add_commute) qed then show ?thesis by (fastforce simp: add_le_imp_le_diff add.commute) qed lemma image_add_atLeastAtMost [simp]: "plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B") proof show "?A \ ?B" by (auto simp add: ac_simps) next show "?B \ ?A" proof fix n assume "n \ ?B" then have "i \ n - k" by (simp add: add_le_imp_le_diff) have "n = n - k + k" proof - from \n \ ?B\ have "n = n - (i + k) + (i + k)" by simp also have "\ = n - k - i + i + k" by (simp add: algebra_simps) also have "\ = n - k + k" using \i \ n - k\ by simp finally show ?thesis . qed moreover have "n - k \ {i..j}" using \n \ ?B\ by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le) ultimately show "n \ ?A" by (simp add: ac_simps) qed qed lemma image_add_atLeastAtMost' [simp]: "(\n. n + k) ` {i..j} = {i + k..j + k}" by (simp add: add.commute [of _ k]) lemma image_add_atLeastLessThan [simp]: "plus k ` {i..n. n + k) ` {i.. uminus ` {x<..}" by (rule imageI) (simp add: *) thus "y \ uminus ` {x<..}" by simp next fix y assume "y \ -x" have "- (-y) \ uminus ` {x..}" by (rule imageI) (insert \y \ -x\[THEN le_imp_neg_le], simp) thus "y \ uminus ` {x..}" by simp qed simp_all lemma fixes x :: 'a shows image_uminus_lessThan[simp]: "uminus ` {.. = {c - b<..c - a}" by simp finally show ?thesis by simp qed lemma image_minus_const_greaterThanAtMost[simp]: fixes a b c::"'a::linordered_idom" shows "(-) c ` {a<..b} = {c - b.. = {c - b.. = {..c - a}" by simp finally show ?thesis by simp qed lemma image_minus_const_AtMost[simp]: fixes b c::"'a::linordered_idom" shows "(-) c ` {..b} = {c - b..}" proof - have "(-) c ` {..b} = (+) c ` uminus ` {..b}" unfolding image_image by simp also have "\ = {c - b..}" by simp finally show ?thesis by simp qed lemma image_minus_const_atLeastAtMost' [simp]: "(\t. t-d)`{a..b} = {a-d..b-d}" for d::"'a::linordered_idom" by (metis (no_types, lifting) diff_conv_add_uminus image_add_atLeastAtMost' image_cong) context linordered_field begin lemma image_mult_atLeastAtMost [simp]: "((*) d ` {a..b}) = {d*a..d*b}" if "d>0" using that by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x]) lemma image_divide_atLeastAtMost [simp]: "((\c. c / d) ` {a..b}) = {a/d..b/d}" if "d>0" proof - from that have "inverse d > 0" by simp with image_mult_atLeastAtMost [of "inverse d" a b] have "(*) (inverse d) ` {a..b} = {inverse d * a..inverse d * b}" by blast moreover have "(*) (inverse d) = (\c. c / d)" by (simp add: fun_eq_iff field_simps) ultimately show ?thesis by simp qed lemma image_mult_atLeastAtMost_if: "(*) c ` {x .. y} = (if c > 0 then {c * x .. c * y} else if x \ y then {c * y .. c * x} else {})" proof (cases "c = 0 \ x > y") case True then show ?thesis by auto next case False then have "x \ y" by auto from False consider "c < 0"| "c > 0" by (auto simp add: neq_iff) then show ?thesis proof cases case 1 have "(*) c ` {x..y} = {c * y..c * x}" proof (rule set_eqI) fix d from 1 have "inj (\z. z / c)" by (auto intro: injI) then have "d \ (*) c ` {x..y} \ d / c \ (\z. z div c) ` (*) c ` {x..y}" by (subst inj_image_mem_iff) simp_all also have "\ \ d / c \ {x..y}" using 1 by (simp add: image_image) also have "\ \ d \ {c * y..c * x}" by (auto simp add: field_simps 1) finally show "d \ (*) c ` {x..y} \ d \ {c * y..c * x}" . qed with \x \ y\ show ?thesis by auto qed (simp add: mult_left_mono_neg) qed lemma image_mult_atLeastAtMost_if': "(\x. x * c) ` {x..y} = (if x \ y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})" using image_mult_atLeastAtMost_if [of c x y] by (auto simp add: ac_simps) lemma image_affinity_atLeastAtMost: "((\x. m * x + c) ` {a..b}) = (if {a..b} = {} then {} else if 0 \ m then {m * a + c .. m * b + c} else {m * b + c .. m * a + c})" proof - have *: "(\x. m * x + c) = ((\x. x + c) \ (*) m)" by (simp add: fun_eq_iff) show ?thesis by (simp only: * image_comp [symmetric] image_mult_atLeastAtMost_if) (auto simp add: mult_le_cancel_left) qed lemma image_affinity_atLeastAtMost_diff: "((\x. m*x - c) ` {a..b}) = (if {a..b}={} then {} else if 0 \ m then {m*a - c .. m*b - c} else {m*b - c .. m*a - c})" using image_affinity_atLeastAtMost [of m "-c" a b] by simp lemma image_affinity_atLeastAtMost_div: "((\x. x/m + c) ` {a..b}) = (if {a..b}={} then {} else if 0 \ m then {a/m + c .. b/m + c} else {b/m + c .. a/m + c})" using image_affinity_atLeastAtMost [of "inverse m" c a b] by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide) lemma image_affinity_atLeastAtMost_div_diff: "((\x. x/m - c) ` {a..b}) = (if {a..b}={} then {} else if 0 \ m then {a/m - c .. b/m - c} else {b/m - c .. a/m - c})" using image_affinity_atLeastAtMost_diff [of "inverse m" c a b] by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide) end lemma atLeast1_lessThan_eq_remove0: "{Suc 0..x. x + (l::int)) ` {0..i. i - c) ` {x ..< y} = (if c < y then {x - c ..< y - c} else if x < y then {0} else {})" (is "_ = ?right") proof safe fix a assume a: "a \ ?right" show "a \ (\i. i - c) ` {x ..< y}" proof cases assume "c < y" with a show ?thesis by (auto intro!: image_eqI[of _ _ "a + c"]) next assume "\ c < y" with a show ?thesis by (auto intro!: image_eqI[of _ _ x] split: if_split_asm) qed qed auto lemma image_int_atLeastLessThan: "int ` {a..Finiteness\ lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..A bounded set of natural numbers is finite.\ lemma bounded_nat_set_is_finite: "(\i\N. i < (n::nat)) \ finite N" by (rule finite_subset [OF _ finite_lessThan]) auto text \A set of natural numbers is finite iff it is bounded.\ lemma finite_nat_set_iff_bounded: "finite(N::nat set) = (\m. \n\N. n?F\, simplified less_Suc_eq_le[symmetric]] by blast next assume ?B show ?F using \?B\ by(blast intro:bounded_nat_set_is_finite) qed lemma finite_nat_set_iff_bounded_le: "finite(N::nat set) = (\m. \n\N. n\m)" unfolding finite_nat_set_iff_bounded by (blast dest:less_imp_le_nat le_imp_less_Suc) lemma finite_less_ub: "!!f::nat=>nat. (!!n. n \ f n) ==> finite {n. f n \ u}" by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) lemma bounded_Max_nat: fixes P :: "nat \ bool" assumes x: "P x" and M: "\x. P x \ x \ M" obtains m where "P m" "\x. P x \ x \ m" proof - have "finite {x. P x}" using M finite_nat_set_iff_bounded_le by auto then have "Max {x. P x} \ {x. P x}" using Max_in x by auto then show ?thesis by (simp add: \finite {x. P x}\ that) qed text\Any subset of an interval of natural numbers the size of the subset is exactly that interval.\ lemma subset_card_intvl_is_intvl: assumes "A \ {k.. A" by auto with insert have "A \ {k..Proving Inclusions and Equalities between Unions\ lemma UN_le_eq_Un0: "(\i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B") proof show "?A \ ?B" proof fix x assume "x \ ?A" then obtain i where i: "i\n" "x \ M i" by auto show "x \ ?B" proof(cases i) case 0 with i show ?thesis by simp next case (Suc j) with i show ?thesis by auto qed qed next show "?B \ ?A" by fastforce qed lemma UN_le_add_shift: "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B") proof show "?A \ ?B" by fastforce next show "?B \ ?A" proof fix x assume "x \ ?B" then obtain i where i: "i \ {k..n+k}" "x \ M(i)" by auto hence "i-k\n \ x \ M((i-k)+k)" by auto thus "x \ ?A" by blast qed qed lemma UN_le_add_shift_strict: "(\ii\{k.. ?A" proof fix x assume "x \ ?B" then obtain i where i: "i \ {k.. M(i)" by auto then have "i - k < n \ x \ M((i-k) + k)" by auto then show "x \ ?A" using UN_le_add_shift by blast qed qed (fastforce) lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)" by (auto simp add: atLeast0LessThan) lemma UN_finite_subset: "(\n::nat. (\i\{0.. C) \ (\n. A n) \ C" by (subst UN_UN_finite_eq [symmetric]) blast lemma UN_finite2_subset: assumes "\n::nat. (\i\{0.. (\i\{0..n. A n) \ (\n. B n)" proof (rule UN_finite_subset, rule) fix n and a from assms have "(\i\{0.. (\i\{0.. (\i\{0.. (\i\{0.. (\i. B i)" by (auto simp add: UN_UN_finite_eq) qed lemma UN_finite2_eq: "(\n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)" apply (rule subset_antisym [OF UN_finite_subset UN_finite2_subset]) apply auto apply (force simp add: atLeastLessThan_add_Un [of 0])+ done subsubsection \Cardinality\ lemma card_lessThan [simp]: "card {..x. x + l) ` {.. {0.. {0..n}" shows "finite N" using assms finite_atLeastAtMost by (rule finite_subset) lemma ex_bij_betw_nat_finite: "finite M \ \h. bij_betw h {0.. \h. bij_betw h M {0.. finite B \ card A = card B \ \h. bij_betw h A B" apply(drule ex_bij_betw_finite_nat) apply(drule ex_bij_betw_nat_finite) apply(auto intro!:bij_betw_trans) done lemma ex_bij_betw_nat_finite_1: "finite M \ \h. bij_betw h {1 .. card M} M" by (rule finite_same_card_bij) auto lemma bij_betw_iff_card: assumes "finite A" "finite B" shows "(\f. bij_betw f A B) \ (card A = card B)" proof assume "card A = card B" moreover obtain f where "bij_betw f A {0 ..< card A}" using assms ex_bij_betw_finite_nat by blast moreover obtain g where "bij_betw g {0 ..< card B} B" using assms ex_bij_betw_nat_finite by blast ultimately have "bij_betw (g \ f) A B" by (auto simp: bij_betw_trans) thus "(\f. bij_betw f A B)" by blast qed (auto simp: bij_betw_same_card) lemma subset_eq_atLeast0_lessThan_card: fixes n :: nat assumes "N \ {0.. n" proof - from assms finite_lessThan have "card N \ card {0..Relational version of @{thm [source] card_inj_on_le}:\ lemma card_le_if_inj_on_rel: assumes "finite B" "\a. a \ A \ \b. b\B \ r a b" "\a1 a2 b. \ a1 \ A; a2 \ A; b \ B; r a1 b; r a2 b \ \ a1 = a2" shows "card A \ card B" proof - let ?P = "\a b. b \ B \ r a b" let ?f = "\a. SOME b. ?P a b" have 1: "?f ` A \ B" by (auto intro: someI2_ex[OF assms(2)]) have "inj_on ?f A" proof (auto simp: inj_on_def) fix a1 a2 assume asms: "a1 \ A" "a2 \ A" "?f a1 = ?f a2" have 0: "?f a1 \ B" using "1" \a1 \ A\ by blast have 1: "r a1 (?f a1)" using someI_ex[OF assms(2)[OF \a1 \ A\]] by blast have 2: "r a2 (?f a1)" using someI_ex[OF assms(2)[OF \a2 \ A\]] asms(3) by auto show "a1 = a2" using assms(3)[OF asms(1,2) 0 1 2] . qed with 1 show ?thesis using card_inj_on_le[of ?f A B] assms(1) by simp qed subsection \Intervals of integers\ lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..Finiteness\ lemma image_atLeastZeroLessThan_int: "0 \ u ==> {(0::int).. u") case True then show ?thesis by (auto simp: image_atLeastZeroLessThan_int) qed auto lemma finite_atLeastLessThan_int [iff]: "finite {l..Cardinality\ lemma card_atLeastZeroLessThan_int: "card {(0::int).. u") case True then show ?thesis by (auto simp: image_atLeastZeroLessThan_int card_image inj_on_def) qed auto lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}" proof - have "{k. P k \ k < i} \ {.. M" shows "card {k \ M. k < Suc i} \ 0" proof - from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff) qed lemma card_less_Suc2: assumes "0 \ M" shows "card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}" proof - have *: "\j \ M; j < Suc i\ \ j - Suc 0 < i \ Suc (j - Suc 0) \ M \ Suc 0 \ j" for j by (cases j) (use assms in auto) show ?thesis proof (rule card_bij_eq) show "inj_on Suc {k. Suc k \ M \ k < i}" by force show "inj_on (\x. x - Suc 0) {k \ M. k < Suc i}" by (rule inj_on_diff_nat) (use * in blast) qed (use * in auto) qed lemma card_less_Suc: assumes "0 \ M" shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}" proof - have "Suc (card {k. Suc k \ M \ k < i}) = Suc (card {k. Suc k \ M - {0} \ k < i})" by simp also have "\ = Suc (card {k \ M - {0}. k < Suc i})" apply (subst card_less_Suc2) using assms by auto also have "\ = Suc (card ({k \ M. k < Suc i} - {0}))" by (force intro: arg_cong [where f=card]) also have "\ = card (insert 0 ({k \ M. k < Suc i} - {0}))" by (simp add: card_insert) also have "... = card {k \ M. k < Suc i}" using assms by (force simp add: intro: arg_cong [where f=card]) finally show ?thesis. qed subsection \Lemmas useful with the summation operator sum\ text \For examples, see Algebra/poly/UnivPoly2.thy\ subsubsection \Disjoint Unions\ text \Singletons and open intervals\ lemma ivl_disj_un_singleton: "{l::'a::linorder} Un {l<..} = {l..}" "{.. {l} Un {l<.. {l<.. u ==> {l} Un {l<..u} = {l..u}" "(l::'a::linorder) \ u ==> {l..One- and two-sided intervals\ lemma ivl_disj_un_one: "(l::'a::linorder) < u ==> {..l} Un {l<.. u ==> {.. u ==> {..l} Un {l<..u} = {..u}" "(l::'a::linorder) \ u ==> {.. u ==> {l<..u} Un {u<..} = {l<..}" "(l::'a::linorder) < u ==> {l<.. u ==> {l..u} Un {u<..} = {l..}" "(l::'a::linorder) \ u ==> {l..Two- and two-sided intervals\ lemma ivl_disj_un_two: "[| (l::'a::linorder) < m; m \ u |] ==> {l<.. m; m < u |] ==> {l<..m} Un {m<.. m; m \ u |] ==> {l.. m; m < u |] ==> {l..m} Un {m<.. u |] ==> {l<.. m; m \ u |] ==> {l<..m} Un {m<..u} = {l<..u}" "[| (l::'a::linorder) \ m; m \ u |] ==> {l.. m; m \ u |] ==> {l..m} Un {m<..u} = {l..u}" by auto lemma ivl_disj_un_two_touch: "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m.. m; m < u |] ==> {l..m} Un {m.. u |] ==> {l<..m} Un {m..u} = {l<..u}" "[| (l::'a::linorder) \ m; m \ u |] ==> {l..m} Un {m..u} = {l..u}" by auto lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch subsubsection \Disjoint Intersections\ text \One- and two-sided intervals\ lemma ivl_disj_int_one: "{..l::'a::order} Int {l<..Two- and two-sided intervals\ lemma ivl_disj_int_two: "{l::'a::order<..Some Differences\ lemma ivl_diff[simp]: "i \ n \ {i..Some Subset Conditions\ lemma ivl_subset [simp]: "({i.. {m.. i \ m \ i \ j \ (n::'a::linorder))" using linorder_class.le_less_linear[of i n] apply (auto simp: linorder_not_le) apply (force intro: leI)+ done lemma get_smaller_card: assumes "finite A" "k \ card A" obtains B where "B \ A" "card B = k" proof - obtain h where h: "bij_betw h {0..finite A\ ex_bij_betw_nat_finite by blast show thesis proof show "h ` {0.. A" by (metis \k \ card A\ bij_betw_def h image_mono ivl_subset zero_le) have "inj_on h {0..k \ card A\ bij_betw_def h inj_on_subset ivl_subset zero_le) then show "card (h ` {0..Generic big monoid operation over intervals\ context semiring_char_0 begin lemma inj_on_of_nat [simp]: "inj_on of_nat N" by rule simp lemma bij_betw_of_nat [simp]: "bij_betw of_nat N A \ of_nat ` N = A" by (simp add: bij_betw_def) end context comm_monoid_set begin lemma atLeastLessThan_reindex: "F g {h m.. h) {m.. h) {m..n}" if "bij_betw h {m..n} {h m..h n}" for m n ::nat proof - from that have "inj_on h {m..n}" and "h ` {m..n} = {h m..h n}" by (simp_all add: bij_betw_def) then show ?thesis using reindex [of h "{m..n}" g] by simp qed lemma atLeastLessThan_shift_bounds: "F g {m + k.. plus k) {m.. plus k) {m..n}" for m n k :: nat using atLeastAtMost_reindex [of "plus k" m n g] by (simp add: ac_simps) lemma atLeast_Suc_lessThan_Suc_shift: "F g {Suc m.. Suc) {m.. Suc) {m..n}" using atLeastAtMost_shift_bounds [of _ _ 1] by (simp add: plus_1_eq_Suc) lemma atLeast_int_lessThan_int_shift: "F g {int m.. int) {m.. int) {m..n}" by (rule atLeastAtMost_reindex) (simp add: image_int_atLeastAtMost) lemma atLeast0_lessThan_Suc: "F g {0..* g n" by (simp add: atLeast0_lessThan_Suc ac_simps) lemma atLeast0_atMost_Suc: "F g {0..Suc n} = F g {0..n} \<^bold>* g (Suc n)" by (simp add: atLeast0_atMost_Suc ac_simps) lemma atLeast0_lessThan_Suc_shift: "F g {0..* F (g \ Suc) {0..* F (g \ Suc) {0..n}" by (simp add: atLeast0_atMost_Suc_eq_insert_0 atLeast_Suc_atMost_Suc_shift) lemma atLeast_Suc_lessThan: "F g {m..* F g {Suc m..* F g {Suc m..n}" if "m \ n" proof - from that have "{m..n} = insert m {Suc m..n}" by auto then show ?thesis by simp qed lemma ivl_cong: "a = c \ b = d \ (\x. c \ x \ x < d \ g x = h x) \ F g {a.. plus m) {0.. n") simp_all lemma atLeastAtMost_shift_0: fixes m n p :: nat assumes "m \ n" shows "F g {m..n} = F (g \ plus m) {0..n - m}" using assms atLeastAtMost_shift_bounds [of g 0 m "n - m"] by simp lemma atLeastLessThan_concat: fixes m n p :: nat shows "m \ n \ n \ p \ F g {m..* F g {n..i. g (m + n - Suc i)) {n..i. g (m + n - i)) {n..m}" by (rule reindex_bij_witness [where i="\i. m + n - i" and j="\i. m + n - i"]) auto lemma atLeastLessThan_rev_at_least_Suc_atMost: "F g {n..i. g (m + n - i)) {Suc n..m}" unfolding atLeastLessThan_rev [of g n m] by (cases m) (simp_all add: atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost) end subsection \Summation indexed over intervals\ syntax (ASCII) "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10) "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10) syntax (latex_sum output) "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ = _\<^latex>\}^{\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ = _\<^latex>\}^{<\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ < _\<^latex>\}$\ _)" [0,0,10] 10) "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ \ _\<^latex>\}$\ _)" [0,0,10] 10) syntax "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) translations "\x=a..b. t" == "CONST sum (\x. t) {a..b}" "\x=a..x. t) {a..i\n. t" == "CONST sum (\i. t) {..n}" "\ii. t) {..The above introduces some pretty alternative syntaxes for summation over intervals: \begin{center} \begin{tabular}{lll} Old & New & \LaTeX\\ @{term[source]"\x\{a..b}. e"} & \<^term>\\x=a..b. e\ & @{term[mode=latex_sum]"\x=a..b. e"}\\ @{term[source]"\x\{a..\\x=a.. & @{term[mode=latex_sum]"\x=a..x\{..b}. e"} & \<^term>\\x\b. e\ & @{term[mode=latex_sum]"\x\b. e"}\\ @{term[source]"\x\{..\\x & @{term[mode=latex_sum]"\xlatex_sum\ (e.g.\ via \mode = latex_sum\ in antiquotations). It is not the default \LaTeX\ output because it only works well with italic-style formulae, not tt-style. Note that for uniformity on \<^typ>\nat\ it is better to use \<^term>\\x::nat=0.. rather than \\x: \sum\ may not provide all lemmas available for \<^term>\{m.. also in the special form for \<^term>\{...\ text\This congruence rule should be used for sums over intervals as the standard theorem @{text[source]sum.cong} does not work well with the simplifier who adds the unsimplified premise \<^term>\x\B\ to the context.\ context comm_monoid_set begin lemma zero_middle: assumes "1 \ p" "k \ p" shows "F (\j. if j < k then g j else if j = k then \<^bold>1 else h (j - Suc 0)) {..p} = F (\j. if j < k then g j else h j) {..p - Suc 0}" (is "?lhs = ?rhs") proof - have [simp]: "{..p - Suc 0} \ {j. j < k} = {.. - {j. j < k} = {k..p - Suc 0}" using assms by auto have "?lhs = F g {..* F (\j. if j = k then \<^bold>1 else h (j - Suc 0)) {k..p}" using union_disjoint [of "{.. = F g {..* F (\j. h (j - Suc 0)) {Suc k..p}" by (simp add: atLeast_Suc_atMost [of k p] assms) also have "\ = F g {..* F h {k .. p - Suc 0}" using reindex [of Suc "{k..p - Suc 0}"] assms by simp also have "\ = ?rhs" by (simp add: If_cases) finally show ?thesis . qed lemma atMost_Suc [simp]: "F g {..Suc n} = F g {..n} \<^bold>* g (Suc n)" by (simp add: atMost_Suc ac_simps) lemma lessThan_Suc [simp]: "F g {..* g n" by (simp add: lessThan_Suc ac_simps) lemma cl_ivl_Suc [simp]: "F g {m..Suc n} = (if Suc n < m then \<^bold>1 else F g {m..n} \<^bold>* g(Suc n))" by (auto simp: ac_simps atLeastAtMostSuc_conv) lemma op_ivl_Suc [simp]: "F g {m..1 else F g {m..* g(n))" by (auto simp: ac_simps atLeastLessThanSuc) lemma head: fixes n :: nat assumes mn: "m \ n" shows "F g {m..n} = g m \<^bold>* F g {m<..n}" (is "?lhs = ?rhs") proof - from mn have "{m..n} = {m} \ {m<..n}" by (auto intro: ivl_disj_un_singleton) hence "?lhs = F g ({m} \ {m<..n})" by (simp add: atLeast0LessThan) also have "\ = ?rhs" by simp finally show ?thesis . qed lemma ub_add_nat: assumes "(m::nat) \ n + 1" shows "F g {m..n + p} = F g {m..n} \<^bold>* F g {n + 1..n + p}" proof- have "{m .. n+p} = {m..n} \ {n+1..n+p}" using \m \ n+1\ by auto thus ?thesis by (auto simp: ivl_disj_int union_disjoint atLeastSucAtMost_greaterThanAtMost) qed lemma nat_group: fixes k::nat shows "F (\m. F g {m * k ..< m*k + k}) {.. 0" by auto then show ?thesis by (induct n) (simp_all add: atLeastLessThan_concat add.commute atLeast0LessThan[symmetric]) qed auto lemma triangle_reindex: fixes n :: nat shows "F (\(i,j). g i j) {(i,j). i+j < n} = F (\k. F (\i. g i (k - i)) {..k}) {..(i,j). g i j) {(i,j). i+j \ n} = F (\k. F (\i. g i (k - i)) {..k}) {..n}" using triangle_reindex [of g "Suc n"] by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost) lemma nat_diff_reindex: "F (\i. g (n - Suc i)) {..i. g(i + k)){m..i. g(i + k)){m..n::nat}" by (rule reindex_bij_witness[where i="\i. i + k" and j="\i. i - k"]) auto corollary shift_bounds_cl_Suc_ivl: "F g {Suc m..Suc n} = F (\i. g(Suc i)){m..n}" by (simp add: shift_bounds_cl_nat_ivl[where k="Suc 0", simplified]) corollary Suc_reindex_ivl: "m \ n \ F g {m..n} \<^bold>* g (Suc n) = g m \<^bold>* F (\i. g (Suc i)) {m..n}" by (simp add: assoc atLeast_Suc_atMost flip: shift_bounds_cl_Suc_ivl) corollary shift_bounds_Suc_ivl: "F g {Suc m..i. g(Suc i)){m..* F (\i. g (Suc i)) {..n}" proof (induct n) case 0 show ?case by simp next case (Suc n) note IH = this have "F g {..Suc (Suc n)} = F g {..Suc n} \<^bold>* g (Suc (Suc n))" by (rule atMost_Suc) also have "F g {..Suc n} = g 0 \<^bold>* F (\i. g (Suc i)) {..n}" by (rule IH) also have "g 0 \<^bold>* F (\i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)) = g 0 \<^bold>* (F (\i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)))" by (rule assoc) also have "F (\i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)) = F (\i. g (Suc i)) {..Suc n}" by (rule atMost_Suc [symmetric]) finally show ?case . qed lemma lessThan_Suc_shift: "F g {..* F (\i. g (Suc i)) {..* F (\i. g (Suc i)) {.. n \ F g {m..n} = g n \<^bold>* F g {m..i. F (\j. a i j) {0..j. F (\i. a i j) {Suc j..n}) {0..i. F (\j. a i j) {..j. F (\i. a i j) {Suc j..n}) {..k. g (Suc k)) {.. = F (\k. g (Suc k)) {.. b \ F g {a..* g b" by (simp add: atLeastLessThanSuc commute) lemma nat_ivl_Suc': assumes "m \ Suc n" shows "F g {m..Suc n} = g (Suc n) \<^bold>* F g {m..n}" proof - from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto also have "F g \ = g (Suc n) \<^bold>* F g {m..n}" by simp finally show ?thesis . qed lemma in_pairs: "F g {2*m..Suc(2*n)} = F (\i. g(2*i) \<^bold>* g(Suc(2*i))) {m..n}" proof (induction n) case 0 show ?case by (cases "m=0") auto next case (Suc n) then show ?case by (auto simp: assoc split: if_split_asm) qed lemma in_pairs_0: "F g {..Suc(2*n)} = F (\i. g(2*i) \<^bold>* g(Suc(2*i))) {..n}" using in_pairs [of _ 0 n] by (simp add: atLeast0AtMost) end lemma sum_natinterval_diff: fixes f:: "nat \ ('a::ab_group_add)" shows "sum (\k. f k - f(k + 1)) {(m::nat) .. n} = (if m \ n then f m - f(n + 1) else 0)" by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) lemma sum_diff_nat_ivl: fixes f :: "nat \ 'a::ab_group_add" shows "\ m \ n; n \ p \ \ sum f {m..x. Q x \ P x \ (\xxxk = 0..k = 0..k = Suc 0..k = Suc 0..k = 0..Shifting bounds\ context comm_monoid_add begin context fixes f :: "nat \ 'a" assumes "f 0 = 0" begin lemma sum_shift_lb_Suc0_0_upt: "sum f {Suc 0..f 0 = 0\ by simp qed lemma sum_shift_lb_Suc0_0: "sum f {Suc 0..k} = sum f {0..k}" proof (cases k) case 0 with \f 0 = 0\ show ?thesis by simp next case (Suc k) moreover have "{0..Suc k} = insert 0 {Suc 0..Suc k}" by auto ultimately show ?thesis using \f 0 = 0\ by simp qed end end lemma sum_Suc_diff: fixes f :: "nat \ 'a::ab_group_add" assumes "m \ Suc n" shows "(\i = m..n. f(Suc i) - f i) = f (Suc n) - f m" using assms by (induct n) (auto simp: le_Suc_eq) lemma sum_Suc_diff': fixes f :: "nat \ 'a::ab_group_add" assumes "m \ n" shows "(\i = m..Telescoping\ lemma sum_telescope: fixes f::"nat \ 'a::ab_group_add" shows "sum (\i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)" by (induct i) simp_all lemma sum_telescope'': assumes "m \ n" shows "(\k\{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)" by (rule dec_induct[OF assms]) (simp_all add: algebra_simps) lemma sum_lessThan_telescope: "(\nnThe formula for geometric sums\ lemma sum_power2: "(\i=0.. 1" shows "(\i 0" by simp_all moreover have "(\iy \ 0\) ultimately show ?thesis by simp qed lemma diff_power_eq_sum: fixes y :: "'a::{comm_ring,monoid_mult}" shows "x ^ (Suc n) - y ^ (Suc n) = (x - y) * (\pppp \\COMPLEX_POLYFUN\ in HOL Light\ fixes x :: "'a::{comm_ring,monoid_mult}" shows "x^n - y^n = (x - y) * (\i 0 \ x^n - 1 = (x - 1) * (\i 0 \ 1 - x^n = (1 - x) * (\i 0 \ 1 - x^n = (1 - x) * (\ii\n. x^i) = 1 - x^Suc n" by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost) lemma sum_power_shift: fixes x :: "'a::{comm_ring,monoid_mult}" assumes "m \ n" shows "(\i=m..n. x^i) = x^m * (\i\n-m. x^i)" proof - have "(\i=m..n. x^i) = x^m * (\i=m..n. x^(i-m))" by (simp add: sum_distrib_left power_add [symmetric]) also have "(\i=m..n. x^(i-m)) = (\i\n-m. x^i)" using \m \ n\ by (intro sum.reindex_bij_witness[where j="\i. i - m" and i="\i. i + m"]) auto finally show ?thesis . qed lemma sum_gp_multiplied: fixes x :: "'a::{comm_ring,monoid_mult}" assumes "m \ n" shows "(1 - x) * (\i=m..n. x^i) = x^m - x^Suc n" proof - have "(1 - x) * (\i=m..n. x^i) = x^m * (1 - x) * (\i\n-m. x^i)" by (metis mult.assoc mult.commute assms sum_power_shift) also have "... =x^m * (1 - x^Suc(n-m))" by (metis mult.assoc sum_gp_basic) also have "... = x^m - x^Suc n" using assms by (simp add: algebra_simps) (metis le_add_diff_inverse power_add) finally show ?thesis . qed lemma sum_gp: fixes x :: "'a::{comm_ring,division_ring}" shows "(\i=m..n. x^i) = (if n < m then 0 else if x = 1 then of_nat((n + 1) - m) else (x^m - x^Suc n) / (1 - x))" using sum_gp_multiplied [of m n x] apply auto by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq) subsubsection\Geometric progressions\ lemma sum_gp0: fixes x :: "'a::{comm_ring,division_ring}" shows "(\i\n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))" using sum_gp_basic[of x n] by (simp add: mult.commute field_split_simps) lemma sum_power_add: fixes x :: "'a::{comm_ring,monoid_mult}" shows "(\i\I. x^(m+i)) = x^m * (\i\I. x^i)" by (simp add: sum_distrib_left power_add) lemma sum_gp_offset: fixes x :: "'a::{comm_ring,division_ring}" shows "(\i=m..m+n. x^i) = (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" using sum_gp [of x m "m+n"] by (auto simp: power_add algebra_simps) lemma sum_gp_strict: fixes x :: "'a::{comm_ring,division_ring}" shows "(\iThe formulae for arithmetic sums\ context comm_semiring_1 begin lemma double_gauss_sum: "2 * (\i = 0..n. of_nat i) = of_nat n * (of_nat n + 1)" by (induct n) (simp_all add: sum.atLeast0_atMost_Suc algebra_simps left_add_twice) lemma double_gauss_sum_from_Suc_0: "2 * (\i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1)" proof - have "sum of_nat {Suc 0..n} = sum of_nat (insert 0 {Suc 0..n})" by simp also have "\ = sum of_nat {0..n}" by (cases n) (simp_all add: atLeast0_atMost_Suc_eq_insert_0) finally show ?thesis by (simp add: double_gauss_sum) qed lemma double_arith_series: "2 * (\i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d)" proof - have "(\i = 0..n. a + of_nat i * d) = ((\i = 0..n. a) + (\i = 0..n. of_nat i * d))" by (rule sum.distrib) also have "\ = (of_nat (Suc n) * a + d * (\i = 0..n. of_nat i))" by (simp add: sum_distrib_left algebra_simps) finally show ?thesis by (simp add: algebra_simps double_gauss_sum left_add_twice) qed end context unique_euclidean_semiring_with_nat begin lemma gauss_sum: "(\i = 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2" using double_gauss_sum [of n, symmetric] by simp lemma gauss_sum_from_Suc_0: "(\i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2" using double_gauss_sum_from_Suc_0 [of n, symmetric] by simp lemma arith_series: "(\i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d) div 2" using double_arith_series [of a d n, symmetric] by simp end lemma gauss_sum_nat: "\{0..n} = (n * Suc n) div 2" using gauss_sum [of n, where ?'a = nat] by simp lemma arith_series_nat: "(\i = 0..n. a + i * d) = Suc n * (2 * a + n * d) div 2" using arith_series [of a d n] by simp lemma Sum_Icc_int: "\{m..n} = (n * (n + 1) - m * (m - 1)) div 2" if "m \ n" for m n :: int using that proof (induct i \ "nat (n - m)" arbitrary: m n) case 0 then have "m = n" by arith then show ?case by (simp add: algebra_simps mult_2 [symmetric]) next case (Suc i) have 0: "i = nat((n-1) - m)" "m \ n-1" using Suc(2,3) by arith+ have "\ {m..n} = \ {m..1+(n-1)}" by simp also have "\ = \ {m..n-1} + n" using \m \ n\ by(subst atLeastAtMostPlus1_int_conv) simp_all also have "\ = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" by(simp add: Suc(1)[OF 0]) also have "\ = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp also have "\ = (n*(n+1) - m*(m-1)) div 2" by (simp add: algebra_simps mult_2_right) finally show ?case . qed lemma Sum_Icc_nat: "\{m..n} = (n * (n + 1) - m * (m - 1)) div 2" for m n :: nat proof (cases "m \ n") case True then have *: "m * (m - 1) \ n * (n + 1)" by (meson diff_le_self order_trans le_add1 mult_le_mono) have "int (\{m..n}) = (\{int m..int n})" by (simp add: sum.atLeast_int_atMost_int_shift) also have "\ = (int n * (int n + 1) - int m * (int m - 1)) div 2" using \m \ n\ by (simp add: Sum_Icc_int) also have "\ = int ((n * (n + 1) - m * (m - 1)) div 2)" using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff) finally show ?thesis by (simp only: of_nat_eq_iff) next case False then show ?thesis by (auto dest: less_imp_Suc_add simp add: not_le algebra_simps) qed lemma Sum_Ico_nat: "\{m..Division remainder\ lemma range_mod: fixes n :: nat assumes "n > 0" shows "range (\m. m mod n) = {0.. ?A \ m \ ?B" proof assume "m \ ?A" with assms show "m \ ?B" by auto next assume "m \ ?B" moreover have "m mod n \ ?A" by (rule rangeI) ultimately show "m \ ?A" by simp qed qed subsection \Products indexed over intervals\ syntax (ASCII) "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10) "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10) "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10) "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10) syntax (latex_prod output) "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{<\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ < _\<^latex>\}$\ _)" [0,0,10] 10) "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ \ _\<^latex>\}$\ _)" [0,0,10] 10) syntax "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) translations "\x=a..b. t" \ "CONST prod (\x. t) {a..b}" "\x=a.. "CONST prod (\x. t) {a..i\n. t" \ "CONST prod (\i. t) {..n}" "\i "CONST prod (\i. t) {..{int i..int (i+j)}" by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv) lemma prod_int_eq: "prod int {i..j} = \{int i..int j}" proof (cases "i \ j") case True then show ?thesis by (metis le_iff_add prod_int_plus_eq) next case False then show ?thesis by auto qed subsection \Efficient folding over intervals\ function fold_atLeastAtMost_nat where [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc = (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))" by pat_completeness auto termination by (relation "measure (\(_,a,b,_). Suc b - a)") auto lemma fold_atLeastAtMost_nat: assumes "comp_fun_commute f" shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}" using assms proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases) case (1 f a b acc) interpret comp_fun_commute f by fact show ?case proof (cases "a > b") case True thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto next case False with 1 show ?thesis by (subst fold_atLeastAtMost_nat.simps) (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm) qed qed lemma sum_atLeastAtMost_code: "sum f {a..b} = fold_atLeastAtMost_nat (\a acc. f a + acc) a b 0" proof - have "comp_fun_commute (\a. (+) (f a))" by unfold_locales (auto simp: o_def add_ac) thus ?thesis by (simp add: sum.eq_fold fold_atLeastAtMost_nat o_def) qed lemma prod_atLeastAtMost_code: "prod f {a..b} = fold_atLeastAtMost_nat (\a acc. f a * acc) a b 1" proof - have "comp_fun_commute (\a. (*) (f a))" by unfold_locales (auto simp: o_def mult_ac) thus ?thesis by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def) qed (* TODO: Add support for folding over more kinds of intervals here *) end