diff --git a/src/HOL/Analysis/Affine.thy b/src/HOL/Analysis/Affine.thy --- a/src/HOL/Analysis/Affine.thy +++ b/src/HOL/Analysis/Affine.thy @@ -1,1641 +1,1639 @@ section "Affine Sets" theory Affine imports Linear_Algebra begin lemma if_smult: "(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" by (fact if_distrib) lemma sum_delta_notmem: assumes "x \ s" shows "sum (\y. if (y = x) then P x else Q y) s = sum Q s" and "sum (\y. if (x = y) then P x else Q y) s = sum Q s" and "sum (\y. if (y = x) then P y else Q y) s = sum Q s" and "sum (\y. if (x = y) then P y else Q y) s = sum Q s" apply (rule_tac [!] sum.cong) using assms apply auto done lemmas independent_finite = independent_imp_finite lemma span_substd_basis: assumes d: "d \ Basis" shows "span d = {x. \i\Basis. i \ d \ x\i = 0}" (is "_ = ?B") proof - have "d \ ?B" using d by (auto simp: inner_Basis) moreover have s: "subspace ?B" using subspace_substandard[of "\i. i \ d"] . ultimately have "span d \ ?B" using span_mono[of d "?B"] span_eq_iff[of "?B"] by blast moreover have *: "card d \ dim (span d)" using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms] span_superset[of d] by auto moreover from * have "dim ?B \ dim (span d)" using dim_substandard[OF assms] by auto ultimately show ?thesis using s subspace_dim_equal[of "span d" "?B"] subspace_span[of d] by auto qed lemma basis_to_substdbasis_subspace_isomorphism: fixes B :: "'a::euclidean_space set" assumes "independent B" shows "\f d::'a set. card d = card B \ linear f \ f ` B = d \ f ` span B = {x. \i\Basis. i \ d \ x \ i = 0} \ inj_on f (span B) \ d \ Basis" proof - have B: "card B = dim B" using dim_unique[of B B "card B"] assms span_superset[of B] by auto have "dim B \ card (Basis :: 'a set)" using dim_subset_UNIV[of B] by simp from ex_card[OF this] obtain d :: "'a set" where d: "d \ Basis" and t: "card d = dim B" by auto let ?t = "{x::'a::euclidean_space. \i\Basis. i \ d \ x\i = 0}" have "\f. linear f \ f ` B = d \ f ` span B = ?t \ inj_on f (span B)" proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_superset) show "d \ {x. \i\Basis. i \ d \ x \ i = 0}" using d inner_not_same_Basis by blast qed (auto simp: span_substd_basis independent_substdbasis dim_substandard d t B assms) with t \card B = dim B\ d show ?thesis by auto qed subsection \Affine set and affine hull\ definition\<^marker>\tag important\ affine :: "'a::real_vector set \ bool" where "affine s \ (\x\s. \y\s. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s)" lemma affine_alt: "affine s \ (\x\s. \y\s. \u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \ s)" unfolding affine_def by (metis eq_diff_eq') lemma affine_empty [iff]: "affine {}" unfolding affine_def by auto lemma affine_sing [iff]: "affine {x}" unfolding affine_alt by (auto simp: scaleR_left_distrib [symmetric]) lemma affine_UNIV [iff]: "affine UNIV" unfolding affine_def by auto lemma affine_Inter [intro]: "(\s. s\f \ affine s) \ affine (\f)" unfolding affine_def by auto lemma affine_Int[intro]: "affine s \ affine t \ affine (s \ t)" unfolding affine_def by auto lemma affine_scaling: "affine s \ affine (image (\x. c *\<^sub>R x) s)" apply (clarsimp simp add: affine_def) apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI) apply (auto simp: algebra_simps) done lemma affine_affine_hull [simp]: "affine(affine hull s)" unfolding hull_def using affine_Inter[of "{t. affine t \ s \ t}"] by auto lemma affine_hull_eq[simp]: "(affine hull s = s) \ affine s" by (metis affine_affine_hull hull_same) lemma affine_hyperplane: "affine {x. a \ x = b}" by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral) subsubsection\<^marker>\tag unimportant\ \Some explicit formulations\ text "Formalized by Lars Schewe." lemma affine: fixes V::"'a::real_vector set" shows "affine V \ (\S u. finite S \ S \ {} \ S \ V \ sum u S = 1 \ (\x\S. u x *\<^sub>R x) \ V)" proof - have "u *\<^sub>R x + v *\<^sub>R y \ V" if "x \ V" "y \ V" "u + v = (1::real)" and *: "\S u. \finite S; S \ {}; S \ V; sum u S = 1\ \ (\x\S. u x *\<^sub>R x) \ V" for x y u v proof (cases "x = y") case True then show ?thesis using that by (metis scaleR_add_left scaleR_one) next case False then show ?thesis using that *[of "{x,y}" "\w. if w = x then u else v"] by auto qed moreover have "(\x\S. u x *\<^sub>R x) \ V" if *: "\x y u v. \x\V; y\V; u + v = 1\ \ u *\<^sub>R x + v *\<^sub>R y \ V" and "finite S" "S \ {}" "S \ V" "sum u S = 1" for S u proof - define n where "n = card S" consider "card S = 0" | "card S = 1" | "card S = 2" | "card S > 2" by linarith then show "(\x\S. u x *\<^sub>R x) \ V" proof cases assume "card S = 1" then obtain a where "S={a}" by (auto simp: card_Suc_eq) then show ?thesis using that by simp next assume "card S = 2" then obtain a b where "S = {a, b}" by (metis Suc_1 card_1_singletonE card_Suc_eq) then show ?thesis using *[of a b] that by (auto simp: sum_clauses(2)) next assume "card S > 2" then show ?thesis using that n_def proof (induct n arbitrary: u S) case 0 then show ?case by auto next case (Suc n u S) have "sum u S = card S" if "\ (\x\S. u x \ 1)" using that unfolding card_eq_sum by auto with Suc.prems obtain x where "x \ S" and x: "u x \ 1" by force have c: "card (S - {x}) = card S - 1" by (simp add: Suc.prems(3) \x \ S\) have "sum u (S - {x}) = 1 - u x" by (simp add: Suc.prems sum_diff1 \x \ S\) with x have eq1: "inverse (1 - u x) * sum u (S - {x}) = 1" by auto have inV: "(\y\S - {x}. (inverse (1 - u x) * u y) *\<^sub>R y) \ V" proof (cases "card (S - {x}) > 2") case True then have S: "S - {x} \ {}" "card (S - {x}) = n" using Suc.prems c by force+ show ?thesis proof (rule Suc.hyps) show "(\a\S - {x}. inverse (1 - u x) * u a) = 1" by (auto simp: eq1 sum_distrib_left[symmetric]) qed (use S Suc.prems True in auto) next case False then have "card (S - {x}) = Suc (Suc 0)" using Suc.prems c by auto then obtain a b where ab: "(S - {x}) = {a, b}" "a\b" unfolding card_Suc_eq by auto then show ?thesis using eq1 \S \ V\ by (auto simp: sum_distrib_left distrib_left intro!: Suc.prems(2)[of a b]) qed have "u x + (1 - u x) = 1 \ u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\y\S - {x}. u y *\<^sub>R y) /\<^sub>R (1 - u x)) \ V" by (rule Suc.prems) (use \x \ S\ Suc.prems inV in \auto simp: scaleR_right.sum\) moreover have "(\a\S. u a *\<^sub>R a) = u x *\<^sub>R x + (\a\S - {x}. u a *\<^sub>R a)" by (meson Suc.prems(3) sum.remove \x \ S\) ultimately show "(\x\S. u x *\<^sub>R x) \ V" by (simp add: x) qed qed (use \S\{}\ \finite S\ in auto) qed ultimately show ?thesis unfolding affine_def by meson qed lemma affine_hull_explicit: "affine hull p = {y. \S u. finite S \ S \ {} \ S \ p \ sum u S = 1 \ sum (\v. u v *\<^sub>R v) S = y}" (is "_ = ?rhs") proof (rule hull_unique) show "p \ ?rhs" proof (intro subsetI CollectI exI conjI) show "\x. sum (\z. 1) {x} = 1" by auto qed auto show "?rhs \ T" if "p \ T" "affine T" for T using that unfolding affine by blast show "affine ?rhs" unfolding affine_def proof clarify fix u v :: real and sx ux sy uy assume uv: "u + v = 1" and x: "finite sx" "sx \ {}" "sx \ p" "sum ux sx = (1::real)" and y: "finite sy" "sy \ {}" "sy \ p" "sum uy sy = (1::real)" have **: "(sx \ sy) \ sx = sx" "(sx \ sy) \ sy = sy" by auto show "\S w. finite S \ S \ {} \ S \ p \ sum w S = 1 \ (\v\S. w v *\<^sub>R v) = u *\<^sub>R (\v\sx. ux v *\<^sub>R v) + v *\<^sub>R (\v\sy. uy v *\<^sub>R v)" proof (intro exI conjI) show "finite (sx \ sy)" using x y by auto show "sum (\i. (if i\sx then u * ux i else 0) + (if i\sy then v * uy i else 0)) (sx \ sy) = 1" using x y uv by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] sum_distrib_left [symmetric] **) have "(\i\sx \ sy. ((if i \ sx then u * ux i else 0) + (if i \ sy then v * uy i else 0)) *\<^sub>R i) = (\i\sx. (u * ux i) *\<^sub>R i) + (\i\sy. (v * uy i) *\<^sub>R i)" using x y unfolding scaleR_left_distrib scaleR_zero_left if_smult by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] **) also have "\ = u *\<^sub>R (\v\sx. ux v *\<^sub>R v) + v *\<^sub>R (\v\sy. uy v *\<^sub>R v)" unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] by blast finally show "(\i\sx \ sy. ((if i \ sx then u * ux i else 0) + (if i \ sy then v * uy i else 0)) *\<^sub>R i) = u *\<^sub>R (\v\sx. ux v *\<^sub>R v) + v *\<^sub>R (\v\sy. uy v *\<^sub>R v)" . qed (use x y in auto) qed qed lemma affine_hull_finite: assumes "finite S" shows "affine hull S = {y. \u. sum u S = 1 \ sum (\v. u v *\<^sub>R v) S = y}" proof - have *: "\h. sum h S = 1 \ (\v\S. h v *\<^sub>R v) = x" if "F \ S" "finite F" "F \ {}" and sum: "sum u F = 1" and x: "(\v\F. u v *\<^sub>R v) = x" for x F u proof - have "S \ F = F" using that by auto show ?thesis proof (intro exI conjI) show "(\x\S. if x \ F then u x else 0) = 1" by (metis (mono_tags, lifting) \S \ F = F\ assms sum.inter_restrict sum) show "(\v\S. (if v \ F then u v else 0) *\<^sub>R v) = x" by (simp add: if_smult cong: if_cong) (metis (no_types) \S \ F = F\ assms sum.inter_restrict x) qed qed show ?thesis unfolding affine_hull_explicit using assms by (fastforce dest: *) qed subsubsection\<^marker>\tag unimportant\ \Stepping theorems and hence small special cases\ lemma affine_hull_empty[simp]: "affine hull {} = {}" by simp lemma affine_hull_finite_step: fixes y :: "'a::real_vector" shows "finite S \ (\u. sum u (insert a S) = w \ sum (\x. u x *\<^sub>R x) (insert a S) = y) \ (\v u. sum u S = w - v \ sum (\x. u x *\<^sub>R x) S = y - v *\<^sub>R a)" (is "_ \ ?lhs = ?rhs") proof - assume fin: "finite S" show "?lhs = ?rhs" proof assume ?lhs then obtain u where u: "sum u (insert a S) = w \ (\x\insert a S. u x *\<^sub>R x) = y" by auto show ?rhs proof (cases "a \ S") case True then show ?thesis using u by (simp add: insert_absorb) (metis diff_zero real_vector.scale_zero_left) next case False show ?thesis by (rule exI [where x="u a"]) (use u fin False in auto) qed next assume ?rhs then obtain v u where vu: "sum u S = w - v" "(\x\S. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto have *: "\x M. (if x = a then v else M) *\<^sub>R x = (if x = a then v *\<^sub>R x else M *\<^sub>R x)" by auto show ?lhs proof (cases "a \ S") case True show ?thesis by (rule exI [where x="\x. (if x=a then v else 0) + u x"]) (simp add: True scaleR_left_distrib sum.distrib sum_clauses fin vu * cong: if_cong) next case False then show ?thesis apply (rule_tac x="\x. if x=a then v else u x" in exI) apply (simp add: vu sum_clauses(2)[OF fin] *) by (simp add: sum_delta_notmem(3) vu) qed qed qed lemma affine_hull_2: fixes a b :: "'a::real_vector" shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs") proof - have *: "\x y z. z = x - y \ y + z = (x::real)" "\x y z. z = x - y \ y + z = (x::'a)" by auto have "?lhs = {y. \u. sum u {a, b} = 1 \ (\v\{a, b}. u v *\<^sub>R v) = y}" using affine_hull_finite[of "{a,b}"] by auto also have "\ = {y. \v u. u b = 1 - v \ u b *\<^sub>R b = y - v *\<^sub>R a}" by (simp add: affine_hull_finite_step[of "{b}" a]) also have "\ = ?rhs" unfolding * by auto finally show ?thesis by auto qed lemma affine_hull_3: fixes a b c :: "'a::real_vector" shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" proof - have *: "\x y z. z = x - y \ y + z = (x::real)" "\x y z. z = x - y \ y + z = (x::'a)" by auto show ?thesis apply (simp add: affine_hull_finite affine_hull_finite_step) unfolding * apply safe apply (metis add.assoc) apply (rule_tac x=u in exI, force) done qed lemma mem_affine: assumes "affine S" "x \ S" "y \ S" "u + v = 1" shows "u *\<^sub>R x + v *\<^sub>R y \ S" using assms affine_def[of S] by auto lemma mem_affine_3: assumes "affine S" "x \ S" "y \ S" "z \ S" "u + v + w = 1" shows "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \ S" proof - have "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \ affine hull {x, y, z}" using affine_hull_3[of x y z] assms by auto moreover have "affine hull {x, y, z} \ affine hull S" using hull_mono[of "{x, y, z}" "S"] assms by auto moreover have "affine hull S = S" using assms affine_hull_eq[of S] by auto ultimately show ?thesis by auto qed lemma mem_affine_3_minus: assumes "affine S" "x \ S" "y \ S" "z \ S" shows "x + v *\<^sub>R (y-z) \ S" using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps) corollary%unimportant mem_affine_3_minus2: "\affine S; x \ S; y \ S; z \ S\ \ x - v *\<^sub>R (y-z) \ S" by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left) subsubsection\<^marker>\tag unimportant\ \Some relations between affine hull and subspaces\ lemma affine_hull_insert_subset_span: "affine hull (insert a S) \ {a + v| v . v \ span {x - a | x . x \ S}}" proof - have "\v T u. x = a + v \ (finite T \ T \ {x - a |x. x \ S} \ (\v\T. u v *\<^sub>R v) = v)" if "finite F" "F \ {}" "F \ insert a S" "sum u F = 1" "(\v\F. u v *\<^sub>R v) = x" for x F u proof - have *: "(\x. x - a) ` (F - {a}) \ {x - a |x. x \ S}" using that by auto show ?thesis proof (intro exI conjI) show "finite ((\x. x - a) ` (F - {a}))" by (simp add: that(1)) show "(\v\(\x. x - a) ` (F - {a}). u(v+a) *\<^sub>R v) = x-a" by (simp add: sum.reindex[unfolded inj_on_def] algebra_simps sum_subtractf scaleR_left.sum[symmetric] sum_diff1 that) qed (use \F \ insert a S\ in auto) qed then show ?thesis unfolding affine_hull_explicit span_explicit by fast qed lemma affine_hull_insert_span: assumes "a \ S" shows "affine hull (insert a S) = {a + v | v . v \ span {x - a | x. x \ S}}" proof - have *: "\G u. finite G \ G \ {} \ G \ insert a S \ sum u G = 1 \ (\v\G. u v *\<^sub>R v) = y" if "v \ span {x - a |x. x \ S}" "y = a + v" for y v proof - from that obtain T u where u: "finite T" "T \ {x - a |x. x \ S}" "a + (\v\T. u v *\<^sub>R v) = y" unfolding span_explicit by auto define F where "F = (\x. x + a) ` T" have F: "finite F" "F \ S" "(\v\F. u (v - a) *\<^sub>R (v - a)) = y - a" unfolding F_def using u by (auto simp: sum.reindex[unfolded inj_on_def]) have *: "F \ {a} = {}" "F \ - {a} = F" using F assms by auto show "\G u. finite G \ G \ {} \ G \ insert a S \ sum u G = 1 \ (\v\G. u v *\<^sub>R v) = y" apply (rule_tac x = "insert a F" in exI) apply (rule_tac x = "\x. if x=a then 1 - sum (\x. u (x - a)) F else u (x - a)" in exI) using assms F apply (auto simp: sum_clauses sum.If_cases if_smult sum_subtractf scaleR_left.sum algebra_simps *) done qed show ?thesis by (intro subset_antisym affine_hull_insert_subset_span) (auto simp: affine_hull_explicit dest!: *) qed lemma affine_hull_span: assumes "a \ S" shows "affine hull S = {a + v | v. v \ span {x - a | x. x \ S - {a}}}" using affine_hull_insert_span[of a "S - {a}", unfolded insert_Diff[OF assms]] by auto subsubsection\<^marker>\tag unimportant\ \Parallel affine sets\ definition affine_parallel :: "'a::real_vector set \ 'a::real_vector set \ bool" where "affine_parallel S T \ (\a. T = (\x. a + x) ` S)" lemma affine_parallel_expl_aux: fixes S T :: "'a::real_vector set" assumes "\x. x \ S \ a + x \ T" shows "T = (\x. a + x) ` S" proof - have "x \ ((\x. a + x) ` S)" if "x \ T" for x using that by (simp add: image_iff) (metis add.commute diff_add_cancel assms) moreover have "T \ (\x. a + x) ` S" using assms by auto ultimately show ?thesis by auto qed lemma affine_parallel_expl: "affine_parallel S T \ (\a. \x. x \ S \ a + x \ T)" by (auto simp add: affine_parallel_def) (use affine_parallel_expl_aux [of S _ T] in blast) lemma affine_parallel_reflex: "affine_parallel S S" unfolding affine_parallel_def using image_add_0 by blast lemma affine_parallel_commut: assumes "affine_parallel A B" shows "affine_parallel B A" proof - from assms obtain a where B: "B = (\x. a + x) ` A" unfolding affine_parallel_def by auto have [simp]: "(\x. x - a) = plus (- a)" by (simp add: fun_eq_iff) from B show ?thesis using translation_galois [of B a A] unfolding affine_parallel_def by blast qed lemma affine_parallel_assoc: assumes "affine_parallel A B" and "affine_parallel B C" shows "affine_parallel A C" proof - from assms obtain ab where "B = (\x. ab + x) ` A" unfolding affine_parallel_def by auto moreover from assms obtain bc where "C = (\x. bc + x) ` B" unfolding affine_parallel_def by auto ultimately show ?thesis using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto qed lemma affine_translation_aux: fixes a :: "'a::real_vector" assumes "affine ((\x. a + x) ` S)" shows "affine S" proof - { fix x y u v assume xy: "x \ S" "y \ S" "(u :: real) + v = 1" then have "(a + x) \ ((\x. a + x) ` S)" "(a + y) \ ((\x. a + x) ` S)" by auto then have h1: "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) \ (\x. a + x) ` S" using xy assms unfolding affine_def by auto have "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) = (u + v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)" by (simp add: algebra_simps) also have "\ = a + (u *\<^sub>R x + v *\<^sub>R y)" using \u + v = 1\ by auto ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) \ (\x. a + x) ` S" using h1 by auto then have "u *\<^sub>R x + v *\<^sub>R y \ S" by auto } then show ?thesis unfolding affine_def by auto qed lemma affine_translation: "affine S \ affine ((+) a ` S)" for a :: "'a::real_vector" proof show "affine ((+) a ` S)" if "affine S" using that translation_assoc [of "- a" a S] by (auto intro: affine_translation_aux [of "- a" "((+) a ` S)"]) show "affine S" if "affine ((+) a ` S)" using that by (rule affine_translation_aux) qed lemma parallel_is_affine: fixes S T :: "'a::real_vector set" assumes "affine S" "affine_parallel S T" shows "affine T" proof - from assms obtain a where "T = (\x. a + x) ` S" unfolding affine_parallel_def by auto then show ?thesis using affine_translation assms by auto qed lemma subspace_imp_affine: "subspace s \ affine s" unfolding subspace_def affine_def by auto lemma affine_hull_subset_span: "(affine hull s) \ (span s)" by (metis hull_minimal span_superset subspace_imp_affine subspace_span) subsubsection\<^marker>\tag unimportant\ \Subspace parallel to an affine set\ lemma subspace_affine: "subspace S \ affine S \ 0 \ S" proof - have h0: "subspace S \ affine S \ 0 \ S" using subspace_imp_affine[of S] subspace_0 by auto { assume assm: "affine S \ 0 \ S" { fix c :: real fix x assume x: "x \ S" have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto moreover have "(1 - c) *\<^sub>R 0 + c *\<^sub>R x \ S" using affine_alt[of S] assm x by auto ultimately have "c *\<^sub>R x \ S" by auto } then have h1: "\c. \x \ S. c *\<^sub>R x \ S" by auto { fix x y assume xy: "x \ S" "y \ S" define u where "u = (1 :: real)/2" have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" by auto moreover have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y" by (simp add: algebra_simps) moreover have "(1 - u) *\<^sub>R x + u *\<^sub>R y \ S" using affine_alt[of S] assm xy by auto ultimately have "(1/2) *\<^sub>R (x+y) \ S" using u_def by auto moreover have "x + y = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" by auto ultimately have "x + y \ S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto } then have "\x \ S. \y \ S. x + y \ S" by auto then have "subspace S" using h1 assm unfolding subspace_def by auto } then show ?thesis using h0 by metis qed lemma affine_diffs_subspace: assumes "affine S" "a \ S" shows "subspace ((\x. (-a)+x) ` S)" proof - have [simp]: "(\x. x - a) = plus (- a)" by (simp add: fun_eq_iff) have "affine ((\x. (-a)+x) ` S)" using affine_translation assms by blast moreover have "0 \ ((\x. (-a)+x) ` S)" using assms exI[of "(\x. x\S \ -a+x = 0)" a] by auto ultimately show ?thesis using subspace_affine by auto qed lemma affine_diffs_subspace_subtract: "subspace ((\x. x - a) ` S)" if "affine S" "a \ S" using that affine_diffs_subspace [of _ a] by simp lemma parallel_subspace_explicit: assumes "affine S" and "a \ S" assumes "L \ {y. \x \ S. (-a) + x = y}" shows "subspace L \ affine_parallel S L" proof - from assms have "L = plus (- a) ` S" by auto then have par: "affine_parallel S L" unfolding affine_parallel_def .. then have "affine L" using assms parallel_is_affine by auto moreover have "0 \ L" using assms by auto ultimately show ?thesis using subspace_affine par by auto qed lemma parallel_subspace_aux: assumes "subspace A" and "subspace B" and "affine_parallel A B" shows "A \ B" proof - from assms obtain a where a: "\x. x \ A \ a + x \ B" using affine_parallel_expl[of A B] by auto then have "-a \ A" using assms subspace_0[of B] by auto then have "a \ A" using assms subspace_neg[of A "-a"] by auto then show ?thesis using assms a unfolding subspace_def by auto qed lemma parallel_subspace: assumes "subspace A" and "subspace B" and "affine_parallel A B" shows "A = B" proof show "A \ B" using assms parallel_subspace_aux by auto show "A \ B" using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto qed lemma affine_parallel_subspace: assumes "affine S" "S \ {}" shows "\!L. subspace L \ affine_parallel S L" proof - have ex: "\L. subspace L \ affine_parallel S L" using assms parallel_subspace_explicit by auto { fix L1 L2 assume ass: "subspace L1 \ affine_parallel S L1" "subspace L2 \ affine_parallel S L2" then have "affine_parallel L1 L2" using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto then have "L1 = L2" using ass parallel_subspace by auto } then show ?thesis using ex by auto qed subsection \Affine Dependence\ text "Formalized by Lars Schewe." definition\<^marker>\tag important\ affine_dependent :: "'a::real_vector set \ bool" where "affine_dependent s \ (\x\s. x \ affine hull (s - {x}))" lemma affine_dependent_imp_dependent: "affine_dependent s \ dependent s" unfolding affine_dependent_def dependent_def using affine_hull_subset_span by auto lemma affine_dependent_subset: "\affine_dependent s; s \ t\ \ affine_dependent t" apply (simp add: affine_dependent_def Bex_def) apply (blast dest: hull_mono [OF Diff_mono [OF _ subset_refl]]) done lemma affine_independent_subset: shows "\\ affine_dependent t; s \ t\ \ \ affine_dependent s" by (metis affine_dependent_subset) lemma affine_independent_Diff: "\ affine_dependent s \ \ affine_dependent(s - t)" by (meson Diff_subset affine_dependent_subset) proposition affine_dependent_explicit: "affine_dependent p \ (\S u. finite S \ S \ p \ sum u S = 0 \ (\v\S. u v \ 0) \ sum (\v. u v *\<^sub>R v) S = 0)" proof - have "\S u. finite S \ S \ p \ sum u S = 0 \ (\v\S. u v \ 0) \ (\w\S. u w *\<^sub>R w) = 0" if "(\w\S. u w *\<^sub>R w) = x" "x \ p" "finite S" "S \ {}" "S \ p - {x}" "sum u S = 1" for x S u proof (intro exI conjI) have "x \ S" using that by auto then show "(\v \ insert x S. if v = x then - 1 else u v) = 0" using that by (simp add: sum_delta_notmem) show "(\w \ insert x S. (if w = x then - 1 else u w) *\<^sub>R w) = 0" using that \x \ S\ by (simp add: if_smult sum_delta_notmem cong: if_cong) qed (use that in auto) moreover have "\x\p. \S u. finite S \ S \ {} \ S \ p - {x} \ sum u S = 1 \ (\v\S. u v *\<^sub>R v) = x" if "(\v\S. u v *\<^sub>R v) = 0" "finite S" "S \ p" "sum u S = 0" "v \ S" "u v \ 0" for S u v proof (intro bexI exI conjI) have "S \ {v}" using that by auto then show "S - {v} \ {}" using that by auto show "(\x \ S - {v}. - (1 / u v) * u x) = 1" unfolding sum_distrib_left[symmetric] sum_diff1[OF \finite S\] by (simp add: that) show "(\x\S - {v}. (- (1 / u v) * u x) *\<^sub>R x) = v" unfolding sum_distrib_left [symmetric] scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] sum_diff1[OF \finite S\] using that by auto show "S - {v} \ p - {v}" using that by auto qed (use that in auto) ultimately show ?thesis unfolding affine_dependent_def affine_hull_explicit by auto qed lemma affine_dependent_explicit_finite: fixes S :: "'a::real_vector set" assumes "finite S" shows "affine_dependent S \ (\u. sum u S = 0 \ (\v\S. u v \ 0) \ sum (\v. u v *\<^sub>R v) S = 0)" (is "?lhs = ?rhs") proof have *: "\vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else 0::'a)" by auto assume ?lhs then obtain t u v where "finite t" "t \ S" "sum u t = 0" "v\t" "u v \ 0" "(\v\t. u v *\<^sub>R v) = 0" unfolding affine_dependent_explicit by auto then show ?rhs apply (rule_tac x="\x. if x\t then u x else 0" in exI) apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF \t\S\]) done next assume ?rhs then obtain u v where "sum u S = 0" "v\S" "u v \ 0" "(\v\S. u v *\<^sub>R v) = 0" by auto then show ?lhs unfolding affine_dependent_explicit using assms by auto qed lemma dependent_imp_affine_dependent: assumes "dependent {x - a| x . x \ s}" and "a \ s" shows "affine_dependent (insert a s)" proof - from assms(1)[unfolded dependent_explicit] obtain S u v where obt: "finite S" "S \ {x - a |x. x \ s}" "v\S" "u v \ 0" "(\v\S. u v *\<^sub>R v) = 0" by auto define t where "t = (\x. x + a) ` S" have inj: "inj_on (\x. x + a) S" unfolding inj_on_def by auto have "0 \ S" using obt(2) assms(2) unfolding subset_eq by auto have fin: "finite t" and "t \ s" unfolding t_def using obt(1,2) by auto then have "finite (insert a t)" and "insert a t \ insert a s" by auto moreover have *: "\P Q. (\x\t. (if x = a then P x else Q x)) = (\x\t. Q x)" apply (rule sum.cong) using \a\s\ \t\s\ apply auto done have "(\x\insert a t. if x = a then - (\x\t. u (x - a)) else u (x - a)) = 0" unfolding sum_clauses(2)[OF fin] * using \a\s\ \t\s\ by auto moreover have "\v\insert a t. (if v = a then - (\x\t. u (x - a)) else u (v - a)) \ 0" using obt(3,4) \0\S\ by (rule_tac x="v + a" in bexI) (auto simp: t_def) moreover have *: "\P Q. (\x\t. (if x = a then P x else Q x) *\<^sub>R x) = (\x\t. Q x *\<^sub>R x)" using \a\s\ \t\s\ by (auto intro!: sum.cong) have "(\x\t. u (x - a)) *\<^sub>R a = (\v\t. u (v - a) *\<^sub>R v)" unfolding scaleR_left.sum unfolding t_def and sum.reindex[OF inj] and o_def using obt(5) by (auto simp: sum.distrib scaleR_right_distrib) then have "(\v\insert a t. (if v = a then - (\x\t. u (x - a)) else u (v - a)) *\<^sub>R v) = 0" unfolding sum_clauses(2)[OF fin] using \a\s\ \t\s\ by (auto simp: *) ultimately show ?thesis unfolding affine_dependent_explicit apply (rule_tac x="insert a t" in exI, auto) done qed lemma affine_dependent_biggerset: fixes s :: "'a::euclidean_space set" assumes "finite s" "card s \ DIM('a) + 2" shows "affine_dependent s" proof - have "s \ {}" using assms by auto then obtain a where "a\s" by auto have *: "{x - a |x. x \ s - {a}} = (\x. x - a) ` (s - {a})" by auto have "card {x - a |x. x \ s - {a}} = card (s - {a})" unfolding * by (simp add: card_image inj_on_def) also have "\ > DIM('a)" using assms(2) - unfolding card_Diff_singleton[OF assms(1) \a\s\] by auto + unfolding card_Diff_singleton[OF \a\s\] by auto finally show ?thesis apply (subst insert_Diff[OF \a\s\, symmetric]) apply (rule dependent_imp_affine_dependent) apply (rule dependent_biggerset, auto) done qed lemma affine_dependent_biggerset_general: assumes "finite (S :: 'a::euclidean_space set)" and "card S \ dim S + 2" shows "affine_dependent S" proof - from assms(2) have "S \ {}" by auto then obtain a where "a\S" by auto have *: "{x - a |x. x \ S - {a}} = (\x. x - a) ` (S - {a})" by auto have **: "card {x - a |x. x \ S - {a}} = card (S - {a})" by (metis (no_types, lifting) "*" card_image diff_add_cancel inj_on_def) have "dim {x - a |x. x \ S - {a}} \ dim S" using \a\S\ by (auto simp: span_base span_diff intro: subset_le_dim) also have "\ < dim S + 1" by auto also have "\ \ card (S - {a})" - using assms - using card_Diff_singleton[OF assms(1) \a\S\] - by auto + using assms card_Diff_singleton[OF \a\S\] by auto finally show ?thesis apply (subst insert_Diff[OF \a\S\, symmetric]) apply (rule dependent_imp_affine_dependent) apply (rule dependent_biggerset_general) unfolding ** apply auto done qed subsection\<^marker>\tag unimportant\ \Some Properties of Affine Dependent Sets\ lemma affine_independent_0 [simp]: "\ affine_dependent {}" by (simp add: affine_dependent_def) lemma affine_independent_1 [simp]: "\ affine_dependent {a}" by (simp add: affine_dependent_def) lemma affine_independent_2 [simp]: "\ affine_dependent {a,b}" by (simp add: affine_dependent_def insert_Diff_if hull_same) lemma affine_hull_translation: "affine hull ((\x. a + x) ` S) = (\x. a + x) ` (affine hull S)" proof - have "affine ((\x. a + x) ` (affine hull S))" using affine_translation affine_affine_hull by blast moreover have "(\x. a + x) ` S \ (\x. a + x) ` (affine hull S)" using hull_subset[of S] by auto ultimately have h1: "affine hull ((\x. a + x) ` S) \ (\x. a + x) ` (affine hull S)" by (metis hull_minimal) have "affine((\x. -a + x) ` (affine hull ((\x. a + x) ` S)))" using affine_translation affine_affine_hull by blast moreover have "(\x. -a + x) ` (\x. a + x) ` S \ (\x. -a + x) ` (affine hull ((\x. a + x) ` S))" using hull_subset[of "(\x. a + x) ` S"] by auto moreover have "S = (\x. -a + x) ` (\x. a + x) ` S" using translation_assoc[of "-a" a] by auto ultimately have "(\x. -a + x) ` (affine hull ((\x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal) then have "affine hull ((\x. a + x) ` S) >= (\x. a + x) ` (affine hull S)" by auto then show ?thesis using h1 by auto qed lemma affine_dependent_translation: assumes "affine_dependent S" shows "affine_dependent ((\x. a + x) ` S)" proof - obtain x where x: "x \ S \ x \ affine hull (S - {x})" using assms affine_dependent_def by auto have "(+) a ` (S - {x}) = (+) a ` S - {a + x}" by auto then have "a + x \ affine hull ((\x. a + x) ` S - {a + x})" using affine_hull_translation[of a "S - {x}"] x by auto moreover have "a + x \ (\x. a + x) ` S" using x by auto ultimately show ?thesis unfolding affine_dependent_def by auto qed lemma affine_dependent_translation_eq: "affine_dependent S \ affine_dependent ((\x. a + x) ` S)" proof - { assume "affine_dependent ((\x. a + x) ` S)" then have "affine_dependent S" using affine_dependent_translation[of "((\x. a + x) ` S)" "-a"] translation_assoc[of "-a" a] by auto } then show ?thesis using affine_dependent_translation by auto qed lemma affine_hull_0_dependent: assumes "0 \ affine hull S" shows "dependent S" proof - obtain s u where s_u: "finite s \ s \ {} \ s \ S \ sum u s = 1 \ (\v\s. u v *\<^sub>R v) = 0" using assms affine_hull_explicit[of S] by auto then have "\v\s. u v \ 0" by auto then have "finite s \ s \ S \ (\v\s. u v \ 0 \ (\v\s. u v *\<^sub>R v) = 0)" using s_u by auto then show ?thesis unfolding dependent_explicit[of S] by auto qed lemma affine_dependent_imp_dependent2: assumes "affine_dependent (insert 0 S)" shows "dependent S" proof - obtain x where x: "x \ insert 0 S \ x \ affine hull (insert 0 S - {x})" using affine_dependent_def[of "(insert 0 S)"] assms by blast then have "x \ span (insert 0 S - {x})" using affine_hull_subset_span by auto moreover have "span (insert 0 S - {x}) = span (S - {x})" using insert_Diff_if[of "0" S "{x}"] span_insert_0[of "S-{x}"] by auto ultimately have "x \ span (S - {x})" by auto then have "x \ 0 \ dependent S" using x dependent_def by auto moreover { assume "x = 0" then have "0 \ affine hull S" using x hull_mono[of "S - {0}" S] by auto then have "dependent S" using affine_hull_0_dependent by auto } ultimately show ?thesis by auto qed lemma affine_dependent_iff_dependent: assumes "a \ S" shows "affine_dependent (insert a S) \ dependent ((\x. -a + x) ` S)" proof - have "((+) (- a) ` S) = {x - a| x . x \ S}" by auto then show ?thesis using affine_dependent_translation_eq[of "(insert a S)" "-a"] affine_dependent_imp_dependent2 assms dependent_imp_affine_dependent[of a S] by (auto simp del: uminus_add_conv_diff) qed lemma affine_dependent_iff_dependent2: assumes "a \ S" shows "affine_dependent S \ dependent ((\x. -a + x) ` (S-{a}))" proof - have "insert a (S - {a}) = S" using assms by auto then show ?thesis using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto qed lemma affine_hull_insert_span_gen: "affine hull (insert a s) = (\x. a + x) ` span ((\x. - a + x) ` s)" proof - have h1: "{x - a |x. x \ s} = ((\x. -a+x) ` s)" by auto { assume "a \ s" then have ?thesis using affine_hull_insert_span[of a s] h1 by auto } moreover { assume a1: "a \ s" have "\x. x \ s \ -a+x=0" apply (rule exI[of _ a]) using a1 apply auto done then have "insert 0 ((\x. -a+x) ` (s - {a})) = (\x. -a+x) ` s" by auto then have "span ((\x. -a+x) ` (s - {a}))=span ((\x. -a+x) ` s)" using span_insert_0[of "(+) (- a) ` (s - {a})"] by (auto simp del: uminus_add_conv_diff) moreover have "{x - a |x. x \ (s - {a})} = ((\x. -a+x) ` (s - {a}))" by auto moreover have "insert a (s - {a}) = insert a s" by auto ultimately have ?thesis using affine_hull_insert_span[of "a" "s-{a}"] by auto } ultimately show ?thesis by auto qed lemma affine_hull_span2: assumes "a \ s" shows "affine hull s = (\x. a+x) ` span ((\x. -a+x) ` (s-{a}))" using affine_hull_insert_span_gen[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto lemma affine_hull_span_gen: assumes "a \ affine hull s" shows "affine hull s = (\x. a+x) ` span ((\x. -a+x) ` s)" proof - have "affine hull (insert a s) = affine hull s" using hull_redundant[of a affine s] assms by auto then show ?thesis using affine_hull_insert_span_gen[of a "s"] by auto qed lemma affine_hull_span_0: assumes "0 \ affine hull S" shows "affine hull S = span S" using affine_hull_span_gen[of "0" S] assms by auto lemma extend_to_affine_basis_nonempty: fixes S V :: "'n::real_vector set" assumes "\ affine_dependent S" "S \ V" "S \ {}" shows "\T. \ affine_dependent T \ S \ T \ T \ V \ affine hull T = affine hull V" proof - obtain a where a: "a \ S" using assms by auto then have h0: "independent ((\x. -a + x) ` (S-{a}))" using affine_dependent_iff_dependent2 assms by auto obtain B where B: "(\x. -a+x) ` (S - {a}) \ B \ B \ (\x. -a+x) ` V \ independent B \ (\x. -a+x) ` V \ span B" using assms by (blast intro: maximal_independent_subset_extend[OF _ h0, of "(\x. -a + x) ` V"]) define T where "T = (\x. a+x) ` insert 0 B" then have "T = insert a ((\x. a+x) ` B)" by auto then have "affine hull T = (\x. a+x) ` span B" using affine_hull_insert_span_gen[of a "((\x. a+x) ` B)"] translation_assoc[of "-a" a B] by auto then have "V \ affine hull T" using B assms translation_inverse_subset[of a V "span B"] by auto moreover have "T \ V" using T_def B a assms by auto ultimately have "affine hull T = affine hull V" by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono) moreover have "S \ T" using T_def B translation_inverse_subset[of a "S-{a}" B] by auto moreover have "\ affine_dependent T" using T_def affine_dependent_translation_eq[of "insert 0 B"] affine_dependent_imp_dependent2 B by auto ultimately show ?thesis using \T \ V\ by auto qed lemma affine_basis_exists: fixes V :: "'n::real_vector set" shows "\B. B \ V \ \ affine_dependent B \ affine hull V = affine hull B" proof (cases "V = {}") case True then show ?thesis using affine_independent_0 by auto next case False then obtain x where "x \ V" by auto then show ?thesis using affine_dependent_def[of "{x}"] extend_to_affine_basis_nonempty[of "{x}" V] by auto qed proposition extend_to_affine_basis: fixes S V :: "'n::real_vector set" assumes "\ affine_dependent S" "S \ V" obtains T where "\ affine_dependent T" "S \ T" "T \ V" "affine hull T = affine hull V" proof (cases "S = {}") case True then show ?thesis using affine_basis_exists by (metis empty_subsetI that) next case False then show ?thesis by (metis assms extend_to_affine_basis_nonempty that) qed subsection \Affine Dimension of a Set\ definition\<^marker>\tag important\ aff_dim :: "('a::euclidean_space) set \ int" where "aff_dim V = (SOME d :: int. \B. affine hull B = affine hull V \ \ affine_dependent B \ of_nat (card B) = d + 1)" lemma aff_dim_basis_exists: fixes V :: "('n::euclidean_space) set" shows "\B. affine hull B = affine hull V \ \ affine_dependent B \ of_nat (card B) = aff_dim V + 1" proof - obtain B where "\ affine_dependent B \ affine hull B = affine hull V" using affine_basis_exists[of V] by auto then show ?thesis unfolding aff_dim_def some_eq_ex[of "\d. \B. affine hull B = affine hull V \ \ affine_dependent B \ of_nat (card B) = d + 1"] apply auto apply (rule exI[of _ "int (card B) - (1 :: int)"]) apply (rule exI[of _ "B"], auto) done qed lemma affine_hull_eq_empty [simp]: "affine hull S = {} \ S = {}" by (metis affine_empty subset_empty subset_hull) lemma empty_eq_affine_hull[simp]: "{} = affine hull S \ S = {}" by (metis affine_hull_eq_empty) lemma aff_dim_parallel_subspace_aux: fixes B :: "'n::euclidean_space set" assumes "\ affine_dependent B" "a \ B" shows "finite B \ ((card B) - 1 = dim (span ((\x. -a+x) ` (B-{a}))))" proof - have "independent ((\x. -a + x) ` (B-{a}))" using affine_dependent_iff_dependent2 assms by auto then have fin: "dim (span ((\x. -a+x) ` (B-{a}))) = card ((\x. -a + x) ` (B-{a}))" "finite ((\x. -a + x) ` (B - {a}))" using indep_card_eq_dim_span[of "(\x. -a+x) ` (B-{a})"] by auto show ?thesis proof (cases "(\x. -a + x) ` (B - {a}) = {}") case True have "B = insert a ((\x. a + x) ` (\x. -a + x) ` (B - {a}))" using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto then have "B = {a}" using True by auto then show ?thesis using assms fin by auto next case False then have "card ((\x. -a + x) ` (B - {a})) > 0" using fin by auto moreover have h1: "card ((\x. -a + x) ` (B-{a})) = card (B-{a})" by (rule card_image) (use translate_inj_on in blast) ultimately have "card (B-{a}) > 0" by auto then have *: "finite (B - {a})" using card_gt_0_iff[of "(B - {a})"] by auto then have "card (B - {a}) = card B - 1" using card_Diff_singleton assms by auto with * show ?thesis using fin h1 by auto qed qed lemma aff_dim_parallel_subspace: fixes V L :: "'n::euclidean_space set" assumes "V \ {}" and "subspace L" and "affine_parallel (affine hull V) L" shows "aff_dim V = int (dim L)" proof - obtain B where B: "affine hull B = affine hull V \ \ affine_dependent B \ int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto then have "B \ {}" using assms B by auto then obtain a where a: "a \ B" by auto define Lb where "Lb = span ((\x. -a+x) ` (B-{a}))" moreover have "affine_parallel (affine hull B) Lb" using Lb_def B assms affine_hull_span2[of a B] a affine_parallel_commut[of "Lb" "(affine hull B)"] unfolding affine_parallel_def by auto moreover have "subspace Lb" using Lb_def subspace_span by auto moreover have "affine hull B \ {}" using assms B by auto ultimately have "L = Lb" using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B by auto then have "dim L = dim Lb" by auto moreover have "card B - 1 = dim Lb" and "finite B" using Lb_def aff_dim_parallel_subspace_aux a B by auto ultimately show ?thesis using B \B \ {}\ card_gt_0_iff[of B] by auto qed lemma aff_independent_finite: fixes B :: "'n::euclidean_space set" assumes "\ affine_dependent B" shows "finite B" proof - { assume "B \ {}" then obtain a where "a \ B" by auto then have ?thesis using aff_dim_parallel_subspace_aux assms by auto } then show ?thesis by auto qed lemma aff_dim_empty: fixes S :: "'n::euclidean_space set" shows "S = {} \ aff_dim S = -1" proof - obtain B where *: "affine hull B = affine hull S" and "\ affine_dependent B" and "int (card B) = aff_dim S + 1" using aff_dim_basis_exists by auto moreover from * have "S = {} \ B = {}" by auto ultimately show ?thesis using aff_independent_finite[of B] card_gt_0_iff[of B] by auto qed lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1" by (simp add: aff_dim_empty [symmetric]) lemma aff_dim_affine_hull [simp]: "aff_dim (affine hull S) = aff_dim S" unfolding aff_dim_def using hull_hull[of _ S] by auto lemma aff_dim_affine_hull2: assumes "affine hull S = affine hull T" shows "aff_dim S = aff_dim T" unfolding aff_dim_def using assms by auto lemma aff_dim_unique: fixes B V :: "'n::euclidean_space set" assumes "affine hull B = affine hull V \ \ affine_dependent B" shows "of_nat (card B) = aff_dim V + 1" proof (cases "B = {}") case True then have "V = {}" using assms by auto then have "aff_dim V = (-1::int)" using aff_dim_empty by auto then show ?thesis using \B = {}\ by auto next case False then obtain a where a: "a \ B" by auto define Lb where "Lb = span ((\x. -a+x) ` (B-{a}))" have "affine_parallel (affine hull B) Lb" using Lb_def affine_hull_span2[of a B] a affine_parallel_commut[of "Lb" "(affine hull B)"] unfolding affine_parallel_def by auto moreover have "subspace Lb" using Lb_def subspace_span by auto ultimately have "aff_dim B = int(dim Lb)" using aff_dim_parallel_subspace[of B Lb] \B \ {}\ by auto moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a assms by auto ultimately have "of_nat (card B) = aff_dim B + 1" using \B \ {}\ card_gt_0_iff[of B] by auto then show ?thesis using aff_dim_affine_hull2 assms by auto qed lemma aff_dim_affine_independent: fixes B :: "'n::euclidean_space set" assumes "\ affine_dependent B" shows "of_nat (card B) = aff_dim B + 1" using aff_dim_unique[of B B] assms by auto lemma affine_independent_iff_card: fixes s :: "'a::euclidean_space set" shows "\ affine_dependent s \ finite s \ aff_dim s = int(card s) - 1" apply (rule iffI) apply (simp add: aff_dim_affine_independent aff_independent_finite) by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff) lemma aff_dim_sing [simp]: fixes a :: "'n::euclidean_space" shows "aff_dim {a} = 0" using aff_dim_affine_independent[of "{a}"] affine_independent_1 by auto lemma aff_dim_2 [simp]: fixes a :: "'n::euclidean_space" shows "aff_dim {a,b} = (if a = b then 0 else 1)" proof (clarsimp) assume "a \ b" then have "aff_dim{a,b} = card{a,b} - 1" using affine_independent_2 [of a b] aff_dim_affine_independent by fastforce also have "\ = 1" using \a \ b\ by simp finally show "aff_dim {a, b} = 1" . qed lemma aff_dim_inner_basis_exists: fixes V :: "('n::euclidean_space) set" shows "\B. B \ V \ affine hull B = affine hull V \ \ affine_dependent B \ of_nat (card B) = aff_dim V + 1" proof - obtain B where B: "\ affine_dependent B" "B \ V" "affine hull B = affine hull V" using affine_basis_exists[of V] by auto then have "of_nat(card B) = aff_dim V+1" using aff_dim_unique by auto with B show ?thesis by auto qed lemma aff_dim_le_card: fixes V :: "'n::euclidean_space set" assumes "finite V" shows "aff_dim V \ of_nat (card V) - 1" proof - obtain B where B: "B \ V" "of_nat (card B) = aff_dim V + 1" using aff_dim_inner_basis_exists[of V] by auto then have "card B \ card V" using assms card_mono by auto with B show ?thesis by auto qed lemma aff_dim_parallel_eq: fixes S T :: "'n::euclidean_space set" assumes "affine_parallel (affine hull S) (affine hull T)" shows "aff_dim S = aff_dim T" proof - { assume "T \ {}" "S \ {}" then obtain L where L: "subspace L \ affine_parallel (affine hull T) L" using affine_parallel_subspace[of "affine hull T"] affine_affine_hull[of T] by auto then have "aff_dim T = int (dim L)" using aff_dim_parallel_subspace \T \ {}\ by auto moreover have *: "subspace L \ affine_parallel (affine hull S) L" using L affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto moreover from * have "aff_dim S = int (dim L)" using aff_dim_parallel_subspace \S \ {}\ by auto ultimately have ?thesis by auto } moreover { assume "S = {}" then have "S = {}" and "T = {}" using assms unfolding affine_parallel_def by auto then have ?thesis using aff_dim_empty by auto } moreover { assume "T = {}" then have "S = {}" and "T = {}" using assms unfolding affine_parallel_def by auto then have ?thesis using aff_dim_empty by auto } ultimately show ?thesis by blast qed lemma aff_dim_translation_eq: "aff_dim ((+) a ` S) = aff_dim S" for a :: "'n::euclidean_space" proof - have "affine_parallel (affine hull S) (affine hull ((\x. a + x) ` S))" unfolding affine_parallel_def apply (rule exI[of _ "a"]) using affine_hull_translation[of a S] apply auto done then show ?thesis using aff_dim_parallel_eq[of S "(\x. a + x) ` S"] by auto qed lemma aff_dim_translation_eq_subtract: "aff_dim ((\x. x - a) ` S) = aff_dim S" for a :: "'n::euclidean_space" using aff_dim_translation_eq [of "- a"] by (simp cong: image_cong_simp) lemma aff_dim_affine: fixes S L :: "'n::euclidean_space set" assumes "S \ {}" and "affine S" and "subspace L" and "affine_parallel S L" shows "aff_dim S = int (dim L)" proof - have *: "affine hull S = S" using assms affine_hull_eq[of S] by auto then have "affine_parallel (affine hull S) L" using assms by (simp add: *) then show ?thesis using assms aff_dim_parallel_subspace[of S L] by blast qed lemma dim_affine_hull: fixes S :: "'n::euclidean_space set" shows "dim (affine hull S) = dim S" proof - have "dim (affine hull S) \ dim S" using dim_subset by auto moreover have "dim (span S) \ dim (affine hull S)" using dim_subset affine_hull_subset_span by blast moreover have "dim (span S) = dim S" using dim_span by auto ultimately show ?thesis by auto qed lemma aff_dim_subspace: fixes S :: "'n::euclidean_space set" assumes "subspace S" shows "aff_dim S = int (dim S)" proof (cases "S={}") case True with assms show ?thesis by (simp add: subspace_affine) next case False with aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] subspace_affine show ?thesis by auto qed lemma aff_dim_zero: fixes S :: "'n::euclidean_space set" assumes "0 \ affine hull S" shows "aff_dim S = int (dim S)" proof - have "subspace (affine hull S)" using subspace_affine[of "affine hull S"] affine_affine_hull assms by auto then have "aff_dim (affine hull S) = int (dim (affine hull S))" using assms aff_dim_subspace[of "affine hull S"] by auto then show ?thesis using aff_dim_affine_hull[of S] dim_affine_hull[of S] by auto qed lemma aff_dim_eq_dim: "aff_dim S = int (dim ((+) (- a) ` S))" if "a \ affine hull S" for S :: "'n::euclidean_space set" proof - have "0 \ affine hull (+) (- a) ` S" unfolding affine_hull_translation using that by (simp add: ac_simps) with aff_dim_zero show ?thesis by (metis aff_dim_translation_eq) qed lemma aff_dim_eq_dim_subtract: "aff_dim S = int (dim ((\x. x - a) ` S))" if "a \ affine hull S" for S :: "'n::euclidean_space set" using aff_dim_eq_dim [of a] that by (simp cong: image_cong_simp) lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))" using aff_dim_subspace[of "(UNIV :: 'n::euclidean_space set)"] dim_UNIV[where 'a="'n::euclidean_space"] by auto lemma aff_dim_geq: fixes V :: "'n::euclidean_space set" shows "aff_dim V \ -1" proof - obtain B where "affine hull B = affine hull V" and "\ affine_dependent B" and "int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto then show ?thesis by auto qed lemma aff_dim_negative_iff [simp]: fixes S :: "'n::euclidean_space set" shows "aff_dim S < 0 \S = {}" by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq) lemma aff_lowdim_subset_hyperplane: fixes S :: "'a::euclidean_space set" assumes "aff_dim S < DIM('a)" obtains a b where "a \ 0" "S \ {x. a \ x = b}" proof (cases "S={}") case True moreover have "(SOME b. b \ Basis) \ 0" by (metis norm_some_Basis norm_zero zero_neq_one) ultimately show ?thesis using that by blast next case False then obtain c S' where "c \ S'" "S = insert c S'" by (meson equals0I mk_disjoint_insert) have "dim ((+) (-c) ` S) < DIM('a)" by (metis \S = insert c S'\ aff_dim_eq_dim assms hull_inc insertI1 of_nat_less_imp_less) then obtain a where "a \ 0" "span ((+) (-c) ` S) \ {x. a \ x = 0}" using lowdim_subset_hyperplane by blast moreover have "a \ w = a \ c" if "span ((+) (- c) ` S) \ {x. a \ x = 0}" "w \ S" for w proof - have "w-c \ span ((+) (- c) ` S)" by (simp add: span_base \w \ S\) with that have "w-c \ {x. a \ x = 0}" by blast then show ?thesis by (auto simp: algebra_simps) qed ultimately have "S \ {x. a \ x = a \ c}" by blast then show ?thesis by (rule that[OF \a \ 0\]) qed lemma affine_independent_card_dim_diffs: fixes S :: "'a :: euclidean_space set" assumes "\ affine_dependent S" "a \ S" shows "card S = dim ((\x. x - a) ` S) + 1" proof - have non: "\ affine_dependent (insert a S)" by (simp add: assms insert_absorb) have "finite S" by (meson assms aff_independent_finite) with \a \ S\ have "card S \ 0" by auto moreover have "dim ((\x. x - a) ` S) = card S - 1" using aff_dim_eq_dim_subtract aff_dim_unique \a \ S\ hull_inc insert_absorb non by fastforce ultimately show ?thesis by auto qed lemma independent_card_le_aff_dim: fixes B :: "'n::euclidean_space set" assumes "B \ V" assumes "\ affine_dependent B" shows "int (card B) \ aff_dim V + 1" proof - obtain T where T: "\ affine_dependent T \ B \ T \ T \ V \ affine hull T = affine hull V" by (metis assms extend_to_affine_basis[of B V]) then have "of_nat (card T) = aff_dim V + 1" using aff_dim_unique by auto then show ?thesis using T card_mono[of T B] aff_independent_finite[of T] by auto qed lemma aff_dim_subset: fixes S T :: "'n::euclidean_space set" assumes "S \ T" shows "aff_dim S \ aff_dim T" proof - obtain B where B: "\ affine_dependent B" "B \ S" "affine hull B = affine hull S" "of_nat (card B) = aff_dim S + 1" using aff_dim_inner_basis_exists[of S] by auto then have "int (card B) \ aff_dim T + 1" using assms independent_card_le_aff_dim[of B T] by auto with B show ?thesis by auto qed lemma aff_dim_le_DIM: fixes S :: "'n::euclidean_space set" shows "aff_dim S \ int (DIM('n))" proof - have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))" using aff_dim_UNIV by auto then show "aff_dim (S:: 'n::euclidean_space set) \ int(DIM('n))" using aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto qed lemma affine_dim_equal: fixes S :: "'n::euclidean_space set" assumes "affine S" "affine T" "S \ {}" "S \ T" "aff_dim S = aff_dim T" shows "S = T" proof - obtain a where "a \ S" using assms by auto then have "a \ T" using assms by auto define LS where "LS = {y. \x \ S. (-a) + x = y}" then have ls: "subspace LS" "affine_parallel S LS" using assms parallel_subspace_explicit[of S a LS] \a \ S\ by auto then have h1: "int(dim LS) = aff_dim S" using assms aff_dim_affine[of S LS] by auto have "T \ {}" using assms by auto define LT where "LT = {y. \x \ T. (-a) + x = y}" then have lt: "subspace LT \ affine_parallel T LT" using assms parallel_subspace_explicit[of T a LT] \a \ T\ by auto then have "int(dim LT) = aff_dim T" using assms aff_dim_affine[of T LT] \T \ {}\ by auto then have "dim LS = dim LT" using h1 assms by auto moreover have "LS \ LT" using LS_def LT_def assms by auto ultimately have "LS = LT" using subspace_dim_equal[of LS LT] ls lt by auto moreover have "S = {x. \y \ LS. a+y=x}" using LS_def by auto moreover have "T = {x. \y \ LT. a+y=x}" using LT_def by auto ultimately show ?thesis by auto qed lemma aff_dim_eq_0: fixes S :: "'a::euclidean_space set" shows "aff_dim S = 0 \ (\a. S = {a})" proof (cases "S = {}") case True then show ?thesis by auto next case False then obtain a where "a \ S" by auto show ?thesis proof safe assume 0: "aff_dim S = 0" have "\ {a,b} \ S" if "b \ a" for b by (metis "0" aff_dim_2 aff_dim_subset not_one_le_zero that) then show "\a. S = {a}" using \a \ S\ by blast qed auto qed lemma affine_hull_UNIV: fixes S :: "'n::euclidean_space set" assumes "aff_dim S = int(DIM('n))" shows "affine hull S = (UNIV :: ('n::euclidean_space) set)" proof - have "S \ {}" using assms aff_dim_empty[of S] by auto have h0: "S \ affine hull S" using hull_subset[of S _] by auto have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S" using aff_dim_UNIV assms by auto then have h2: "aff_dim (affine hull S) \ aff_dim (UNIV :: ('n::euclidean_space) set)" using aff_dim_le_DIM[of "affine hull S"] assms h0 by auto have h3: "aff_dim S \ aff_dim (affine hull S)" using h0 aff_dim_subset[of S "affine hull S"] assms by auto then have h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)" using h0 h1 h2 by auto then show ?thesis using affine_dim_equal[of "affine hull S" "(UNIV :: ('n::euclidean_space) set)"] affine_affine_hull[of S] affine_UNIV assms h4 h0 \S \ {}\ by auto qed lemma disjoint_affine_hull: fixes s :: "'n::euclidean_space set" assumes "\ affine_dependent s" "t \ s" "u \ s" "t \ u = {}" shows "(affine hull t) \ (affine hull u) = {}" proof - from assms(1) have "finite s" by (simp add: aff_independent_finite) with assms(2,3) have "finite t" "finite u" by (blast intro: finite_subset)+ have False if "y \ affine hull t" and "y \ affine hull u" for y proof - from that obtain a b where a1 [simp]: "sum a t = 1" and [simp]: "sum (\v. a v *\<^sub>R v) t = y" and [simp]: "sum b u = 1" "sum (\v. b v *\<^sub>R v) u = y" by (auto simp: affine_hull_finite \finite t\ \finite u\) define c where "c x = (if x \ t then a x else if x \ u then -(b x) else 0)" for x from assms(2,3,4) have [simp]: "s \ t = t" "s \ - t \ u = u" by auto have "sum c s = 0" by (simp add: c_def comm_monoid_add_class.sum.If_cases \finite s\ sum_negf) moreover have "\ (\v\s. c v = 0)" by (metis (no_types) IntD1 \s \ t = t\ a1 c_def sum.neutral zero_neq_one) moreover have "(\v\s. c v *\<^sub>R v) = 0" by (simp add: c_def if_smult sum_negf comm_monoid_add_class.sum.If_cases \finite s\) ultimately show ?thesis using assms(1) \finite s\ by (auto simp: affine_dependent_explicit) qed then show ?thesis by blast qed end \ No newline at end of file diff --git a/src/HOL/Complex.thy b/src/HOL/Complex.thy --- a/src/HOL/Complex.thy +++ b/src/HOL/Complex.thy @@ -1,1327 +1,1331 @@ (* Title: HOL/Complex.thy Author: Jacques D. Fleuriot, 2001 University of Edinburgh Author: Lawrence C Paulson, 2003/4 *) section \Complex Numbers: Rectangular and Polar Representations\ theory Complex imports Transcendental begin text \ We use the \<^theory_text>\codatatype\ command to define the type of complex numbers. This allows us to use \<^theory_text>\primcorec\ to define complex functions by defining their real and imaginary result separately. \ codatatype complex = Complex (Re: real) (Im: real) lemma complex_surj: "Complex (Re z) (Im z) = z" by (rule complex.collapse) lemma complex_eqI [intro?]: "Re x = Re y \ Im x = Im y \ x = y" by (rule complex.expand) simp lemma complex_eq_iff: "x = y \ Re x = Re y \ Im x = Im y" by (auto intro: complex.expand) + subsection \Addition and Subtraction\ instantiation complex :: ab_group_add begin primcorec zero_complex where "Re 0 = 0" | "Im 0 = 0" primcorec plus_complex where "Re (x + y) = Re x + Re y" | "Im (x + y) = Im x + Im y" primcorec uminus_complex where "Re (- x) = - Re x" | "Im (- x) = - Im x" primcorec minus_complex where "Re (x - y) = Re x - Re y" | "Im (x - y) = Im x - Im y" instance by standard (simp_all add: complex_eq_iff) end subsection \Multiplication and Division\ instantiation complex :: field begin primcorec one_complex where "Re 1 = 1" | "Im 1 = 0" primcorec times_complex where "Re (x * y) = Re x * Re y - Im x * Im y" | "Im (x * y) = Re x * Im y + Im x * Re y" primcorec inverse_complex where "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" definition "x div y = x * inverse y" for x y :: complex instance by standard (simp_all add: complex_eq_iff divide_complex_def distrib_left distrib_right right_diff_distrib left_diff_distrib power2_eq_square add_divide_distrib [symmetric]) end lemma Re_divide: "Re (x / y) = (Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)" by (simp add: divide_complex_def add_divide_distrib) lemma Im_divide: "Im (x / y) = (Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)" by (simp add: divide_complex_def diff_divide_distrib) lemma Complex_divide: "(x / y) = Complex ((Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)) ((Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2))" by (metis Im_divide Re_divide complex_surj) lemma Re_power2: "Re (x ^ 2) = (Re x)^2 - (Im x)^2" by (simp add: power2_eq_square) lemma Im_power2: "Im (x ^ 2) = 2 * Re x * Im x" by (simp add: power2_eq_square) lemma Re_power_real [simp]: "Im x = 0 \ Re (x ^ n) = Re x ^ n " by (induct n) simp_all lemma Im_power_real [simp]: "Im x = 0 \ Im (x ^ n) = 0" by (induct n) simp_all subsection \Scalar Multiplication\ instantiation complex :: real_field begin primcorec scaleR_complex where "Re (scaleR r x) = r * Re x" | "Im (scaleR r x) = r * Im x" instance proof fix a b :: real and x y :: complex show "scaleR a (x + y) = scaleR a x + scaleR a y" by (simp add: complex_eq_iff distrib_left) show "scaleR (a + b) x = scaleR a x + scaleR b x" by (simp add: complex_eq_iff distrib_right) show "scaleR a (scaleR b x) = scaleR (a * b) x" by (simp add: complex_eq_iff mult.assoc) show "scaleR 1 x = x" by (simp add: complex_eq_iff) show "scaleR a x * y = scaleR a (x * y)" by (simp add: complex_eq_iff algebra_simps) show "x * scaleR a y = scaleR a (x * y)" by (simp add: complex_eq_iff algebra_simps) qed end subsection \Numerals, Arithmetic, and Embedding from R\ abbreviation complex_of_real :: "real \ complex" where "complex_of_real \ of_real" declare [[coercion "of_real :: real \ complex"]] declare [[coercion "of_rat :: rat \ complex"]] declare [[coercion "of_int :: int \ complex"]] declare [[coercion "of_nat :: nat \ complex"]] lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n" by (induct n) simp_all lemma complex_Im_of_nat [simp]: "Im (of_nat n) = 0" by (induct n) simp_all lemma complex_Re_of_int [simp]: "Re (of_int z) = of_int z" by (cases z rule: int_diff_cases) simp lemma complex_Im_of_int [simp]: "Im (of_int z) = 0" by (cases z rule: int_diff_cases) simp lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v" using complex_Re_of_int [of "numeral v"] by simp lemma complex_Im_numeral [simp]: "Im (numeral v) = 0" using complex_Im_of_int [of "numeral v"] by simp lemma Re_complex_of_real [simp]: "Re (complex_of_real z) = z" by (simp add: of_real_def) lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0" by (simp add: of_real_def) lemma Re_divide_numeral [simp]: "Re (z / numeral w) = Re z / numeral w" by (simp add: Re_divide sqr_conv_mult) lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w" by (simp add: Im_divide sqr_conv_mult) lemma Re_divide_of_nat [simp]: "Re (z / of_nat n) = Re z / of_nat n" by (cases n) (simp_all add: Re_divide field_split_simps power2_eq_square del: of_nat_Suc) lemma Im_divide_of_nat [simp]: "Im (z / of_nat n) = Im z / of_nat n" by (cases n) (simp_all add: Im_divide field_split_simps power2_eq_square del: of_nat_Suc) lemma of_real_Re [simp]: "z \ \ \ of_real (Re z) = z" by (auto simp: Reals_def) lemma complex_Re_fact [simp]: "Re (fact n) = fact n" proof - have "(fact n :: complex) = of_real (fact n)" by simp also have "Re \ = fact n" by (subst Re_complex_of_real) simp_all finally show ?thesis . qed lemma complex_Im_fact [simp]: "Im (fact n) = 0" by (subst of_nat_fact [symmetric]) (simp only: complex_Im_of_nat) lemma Re_prod_Reals: "(\x. x \ A \ f x \ \) \ Re (prod f A) = prod (\x. Re (f x)) A" proof (induction A rule: infinite_finite_induct) case (insert x A) hence "Re (prod f (insert x A)) = Re (f x) * Re (prod f A) - Im (f x) * Im (prod f A)" by simp also from insert.prems have "f x \ \" by simp hence "Im (f x) = 0" by (auto elim!: Reals_cases) also have "Re (prod f A) = (\x\A. Re (f x))" by (intro insert.IH insert.prems) auto finally show ?case using insert.hyps by simp qed auto subsection \The Complex Number $i$\ primcorec imaginary_unit :: complex ("\") where "Re \ = 0" | "Im \ = 1" lemma Complex_eq: "Complex a b = a + \ * b" by (simp add: complex_eq_iff) lemma complex_eq: "a = Re a + \ * Im a" by (simp add: complex_eq_iff) lemma fun_complex_eq: "f = (\x. Re (f x) + \ * Im (f x))" by (simp add: fun_eq_iff complex_eq) lemma i_squared [simp]: "\ * \ = -1" by (simp add: complex_eq_iff) lemma power2_i [simp]: "\\<^sup>2 = -1" by (simp add: power2_eq_square) lemma inverse_i [simp]: "inverse \ = - \" by (rule inverse_unique) simp lemma divide_i [simp]: "x / \ = - \ * x" by (simp add: divide_complex_def) lemma complex_i_mult_minus [simp]: "\ * (\ * x) = - x" by (simp add: mult.assoc [symmetric]) lemma complex_i_not_zero [simp]: "\ \ 0" by (simp add: complex_eq_iff) lemma complex_i_not_one [simp]: "\ \ 1" by (simp add: complex_eq_iff) lemma complex_i_not_numeral [simp]: "\ \ numeral w" by (simp add: complex_eq_iff) lemma complex_i_not_neg_numeral [simp]: "\ \ - numeral w" by (simp add: complex_eq_iff) lemma complex_split_polar: "\r a. z = complex_of_real r * (cos a + \ * sin a)" by (simp add: complex_eq_iff polar_Ex) lemma i_even_power [simp]: "\ ^ (n * 2) = (-1) ^ n" by (metis mult.commute power2_i power_mult) lemma Re_i_times [simp]: "Re (\ * z) = - Im z" by simp lemma Im_i_times [simp]: "Im (\ * z) = Re z" by simp lemma i_times_eq_iff: "\ * w = z \ w = - (\ * z)" by auto lemma divide_numeral_i [simp]: "z / (numeral n * \) = - (\ * z) / numeral n" by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right) lemma imaginary_eq_real_iff [simp]: assumes "y \ Reals" "x \ Reals" shows "\ * y = x \ x=0 \ y=0" using assms unfolding Reals_def apply clarify apply (rule iffI) apply (metis Im_complex_of_real Im_i_times Re_complex_of_real mult_eq_0_iff of_real_0) by simp lemma real_eq_imaginary_iff [simp]: assumes "y \ Reals" "x \ Reals" shows "x = \ * y \ x=0 \ y=0" using assms imaginary_eq_real_iff by fastforce subsection \Vector Norm\ instantiation complex :: real_normed_field begin definition "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)" abbreviation cmod :: "complex \ real" where "cmod \ norm" definition complex_sgn_def: "sgn x = x /\<^sub>R cmod x" definition dist_complex_def: "dist x y = cmod (x - y)" definition uniformity_complex_def [code del]: "(uniformity :: (complex \ complex) filter) = (INF e\{0 <..}. principal {(x, y). dist x y < e})" definition open_complex_def [code del]: "open (U :: complex set) \ (\x\U. eventually (\(x', y). x' = x \ y \ U) uniformity)" instance proof fix r :: real and x y :: complex and S :: "complex set" show "(norm x = 0) = (x = 0)" by (simp add: norm_complex_def complex_eq_iff) show "norm (x + y) \ norm x + norm y" by (simp add: norm_complex_def complex_eq_iff real_sqrt_sum_squares_triangle_ineq) show "norm (scaleR r x) = \r\ * norm x" by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric] real_sqrt_mult) show "norm (x * y) = norm x * norm y" by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric] power2_eq_square algebra_simps) qed (rule complex_sgn_def dist_complex_def open_complex_def uniformity_complex_def)+ end declare uniformity_Abort[where 'a = complex, code] lemma norm_ii [simp]: "norm \ = 1" by (simp add: norm_complex_def) lemma cmod_unit_one: "cmod (cos a + \ * sin a) = 1" by (simp add: norm_complex_def) lemma cmod_complex_polar: "cmod (r * (cos a + \ * sin a)) = \r\" by (simp add: norm_mult cmod_unit_one) lemma complex_Re_le_cmod: "Re x \ cmod x" unfolding norm_complex_def by (rule real_sqrt_sum_squares_ge1) lemma complex_mod_minus_le_complex_mod: "- cmod x \ cmod x" by (rule order_trans [OF _ norm_ge_zero]) simp lemma complex_mod_triangle_ineq2: "cmod (b + a) - cmod b \ cmod a" by (rule ord_le_eq_trans [OF norm_triangle_ineq2]) simp lemma abs_Re_le_cmod: "\Re x\ \ cmod x" by (simp add: norm_complex_def) lemma abs_Im_le_cmod: "\Im x\ \ cmod x" by (simp add: norm_complex_def) lemma cmod_le: "cmod z \ \Re z\ + \Im z\" apply (subst complex_eq) apply (rule order_trans) apply (rule norm_triangle_ineq) apply (simp add: norm_mult) done lemma cmod_eq_Re: "Im z = 0 \ cmod z = \Re z\" by (simp add: norm_complex_def) lemma cmod_eq_Im: "Re z = 0 \ cmod z = \Im z\" by (simp add: norm_complex_def) lemma cmod_power2: "(cmod z)\<^sup>2 = (Re z)\<^sup>2 + (Im z)\<^sup>2" by (simp add: norm_complex_def) lemma cmod_plus_Re_le_0_iff: "cmod z + Re z \ 0 \ Re z = - cmod z" using abs_Re_le_cmod[of z] by auto lemma cmod_Re_le_iff: "Im x = Im y \ cmod x \ cmod y \ \Re x\ \ \Re y\" by (metis add.commute add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff) lemma cmod_Im_le_iff: "Re x = Re y \ cmod x \ cmod y \ \Im x\ \ \Im y\" by (metis add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff) lemma Im_eq_0: "\Re z\ = cmod z \ Im z = 0" by (subst (asm) power_eq_iff_eq_base[symmetric, where n=2]) (auto simp add: norm_complex_def) lemma abs_sqrt_wlog: "(\x. x \ 0 \ P x (x\<^sup>2)) \ P \x\ (x\<^sup>2)" for x::"'a::linordered_idom" by (metis abs_ge_zero power2_abs) lemma complex_abs_le_norm: "\Re z\ + \Im z\ \ sqrt 2 * norm z" unfolding norm_complex_def apply (rule abs_sqrt_wlog [where x="Re z"]) apply (rule abs_sqrt_wlog [where x="Im z"]) apply (rule power2_le_imp_le) apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric]) done lemma complex_unit_circle: "z \ 0 \ (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1" by (simp add: norm_complex_def complex_eq_iff power2_eq_square add_divide_distrib [symmetric]) text \Properties of complex signum.\ lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult.commute) lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z" by (simp add: complex_sgn_def divide_inverse) lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z" by (simp add: complex_sgn_def divide_inverse) subsection \Absolute value\ instantiation complex :: field_abs_sgn begin definition abs_complex :: "complex \ complex" where "abs_complex = of_real \ norm" instance apply standard apply (auto simp add: abs_complex_def complex_sgn_def norm_mult) apply (auto simp add: scaleR_conv_of_real field_simps) done end subsection \Completeness of the Complexes\ lemma bounded_linear_Re: "bounded_linear Re" by (rule bounded_linear_intro [where K=1]) (simp_all add: norm_complex_def) lemma bounded_linear_Im: "bounded_linear Im" by (rule bounded_linear_intro [where K=1]) (simp_all add: norm_complex_def) lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re] lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im] lemmas tendsto_Re [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Re] lemmas tendsto_Im [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im] lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re] lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im] lemmas continuous_Re [simp] = bounded_linear.continuous [OF bounded_linear_Re] lemmas continuous_Im [simp] = bounded_linear.continuous [OF bounded_linear_Im] lemmas continuous_on_Re [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Re] lemmas continuous_on_Im [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im] lemmas has_derivative_Re [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Re] lemmas has_derivative_Im [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im] lemmas sums_Re = bounded_linear.sums [OF bounded_linear_Re] lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im] lemma tendsto_Complex [tendsto_intros]: "(f \ a) F \ (g \ b) F \ ((\x. Complex (f x) (g x)) \ Complex a b) F" unfolding Complex_eq by (auto intro!: tendsto_intros) lemma tendsto_complex_iff: "(f \ x) F \ (((\x. Re (f x)) \ Re x) F \ ((\x. Im (f x)) \ Im x) F)" proof safe assume "((\x. Re (f x)) \ Re x) F" "((\x. Im (f x)) \ Im x) F" from tendsto_Complex[OF this] show "(f \ x) F" unfolding complex.collapse . qed (auto intro: tendsto_intros) lemma continuous_complex_iff: "continuous F f \ continuous F (\x. Re (f x)) \ continuous F (\x. Im (f x))" by (simp only: continuous_def tendsto_complex_iff) lemma continuous_on_of_real_o_iff [simp]: "continuous_on S (\x. complex_of_real (g x)) = continuous_on S g" using continuous_on_Re continuous_on_of_real by fastforce lemma continuous_on_of_real_id [simp]: "continuous_on S (of_real :: real \ 'a::real_normed_algebra_1)" by (rule continuous_on_of_real [OF continuous_on_id]) lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \ ((\x. Re (f x)) has_field_derivative (Re x)) F \ ((\x. Im (f x)) has_field_derivative (Im x)) F" by (simp add: has_vector_derivative_def has_field_derivative_def has_derivative_def tendsto_complex_iff algebra_simps bounded_linear_scaleR_left bounded_linear_mult_right) lemma has_field_derivative_Re[derivative_intros]: "(f has_vector_derivative D) F \ ((\x. Re (f x)) has_field_derivative (Re D)) F" unfolding has_vector_derivative_complex_iff by safe lemma has_field_derivative_Im[derivative_intros]: "(f has_vector_derivative D) F \ ((\x. Im (f x)) has_field_derivative (Im D)) F" unfolding has_vector_derivative_complex_iff by safe instance complex :: banach proof fix X :: "nat \ complex" assume X: "Cauchy X" then have "(\n. Complex (Re (X n)) (Im (X n))) \ Complex (lim (\n. Re (X n))) (lim (\n. Im (X n)))" by (intro tendsto_Complex convergent_LIMSEQ_iff[THEN iffD1] Cauchy_convergent_iff[THEN iffD1] Cauchy_Re Cauchy_Im) then show "convergent X" unfolding complex.collapse by (rule convergentI) qed declare DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros] subsection \Complex Conjugation\ primcorec cnj :: "complex \ complex" where "Re (cnj z) = Re z" | "Im (cnj z) = - Im z" lemma complex_cnj_cancel_iff [simp]: "cnj x = cnj y \ x = y" by (simp add: complex_eq_iff) lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z" by (simp add: complex_eq_iff) lemma complex_cnj_zero [simp]: "cnj 0 = 0" by (simp add: complex_eq_iff) lemma complex_cnj_zero_iff [iff]: "cnj z = 0 \ z = 0" by (simp add: complex_eq_iff) lemma complex_cnj_one_iff [simp]: "cnj z = 1 \ z = 1" by (simp add: complex_eq_iff) lemma complex_cnj_add [simp]: "cnj (x + y) = cnj x + cnj y" by (simp add: complex_eq_iff) lemma cnj_sum [simp]: "cnj (sum f s) = (\x\s. cnj (f x))" by (induct s rule: infinite_finite_induct) auto lemma complex_cnj_diff [simp]: "cnj (x - y) = cnj x - cnj y" by (simp add: complex_eq_iff) lemma complex_cnj_minus [simp]: "cnj (- x) = - cnj x" by (simp add: complex_eq_iff) lemma complex_cnj_one [simp]: "cnj 1 = 1" by (simp add: complex_eq_iff) lemma complex_cnj_mult [simp]: "cnj (x * y) = cnj x * cnj y" by (simp add: complex_eq_iff) lemma cnj_prod [simp]: "cnj (prod f s) = (\x\s. cnj (f x))" by (induct s rule: infinite_finite_induct) auto lemma complex_cnj_inverse [simp]: "cnj (inverse x) = inverse (cnj x)" by (simp add: complex_eq_iff) lemma complex_cnj_divide [simp]: "cnj (x / y) = cnj x / cnj y" by (simp add: divide_complex_def) lemma complex_cnj_power [simp]: "cnj (x ^ n) = cnj x ^ n" by (induct n) simp_all lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n" by (simp add: complex_eq_iff) lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z" by (simp add: complex_eq_iff) lemma complex_cnj_numeral [simp]: "cnj (numeral w) = numeral w" by (simp add: complex_eq_iff) lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w" by (simp add: complex_eq_iff) lemma complex_cnj_scaleR [simp]: "cnj (scaleR r x) = scaleR r (cnj x)" by (simp add: complex_eq_iff) lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" by (simp add: norm_complex_def) lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x" by (simp add: complex_eq_iff) lemma complex_cnj_i [simp]: "cnj \ = - \" by (simp add: complex_eq_iff) lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)" by (simp add: complex_eq_iff) lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * \" by (simp add: complex_eq_iff) lemma Ints_cnj [intro]: "x \ \ \ cnj x \ \" by (auto elim!: Ints_cases) lemma cnj_in_Ints_iff [simp]: "cnj x \ \ \ x \ \" using Ints_cnj[of x] Ints_cnj[of "cnj x"] by auto lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<^sup>2 + (Im z)\<^sup>2)" by (simp add: complex_eq_iff power2_eq_square) lemma cnj_add_mult_eq_Re: "z * cnj w + cnj z * w = 2 * Re (z * cnj w)" by (rule complex_eqI) auto lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<^sup>2" by (simp add: norm_mult power2_eq_square) lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" by (simp add: norm_complex_def power2_eq_square) lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0" by simp lemma complex_cnj_fact [simp]: "cnj (fact n) = fact n" by (subst of_nat_fact [symmetric], subst complex_cnj_of_nat) simp lemma complex_cnj_pochhammer [simp]: "cnj (pochhammer z n) = pochhammer (cnj z) n" by (induct n arbitrary: z) (simp_all add: pochhammer_rec) lemma bounded_linear_cnj: "bounded_linear cnj" using complex_cnj_add complex_cnj_scaleR by (rule bounded_linear_intro [where K=1]) simp lemma linear_cnj: "linear cnj" using bounded_linear.linear[OF bounded_linear_cnj] . lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj] and isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj] and continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj] and continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj] and has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj] lemma lim_cnj: "((\x. cnj(f x)) \ cnj l) F \ (f \ l) F" by (simp add: tendsto_iff dist_complex_def complex_cnj_diff [symmetric] del: complex_cnj_diff) lemma sums_cnj: "((\x. cnj(f x)) sums cnj l) \ (f sums l)" by (simp add: sums_def lim_cnj cnj_sum [symmetric] del: cnj_sum) lemma differentiable_cnj_iff: "(\z. cnj (f z)) differentiable at x within A \ f differentiable at x within A" proof assume "(\z. cnj (f z)) differentiable at x within A" then obtain D where "((\z. cnj (f z)) has_derivative D) (at x within A)" by (auto simp: differentiable_def) from has_derivative_cnj[OF this] show "f differentiable at x within A" by (auto simp: differentiable_def) next assume "f differentiable at x within A" then obtain D where "(f has_derivative D) (at x within A)" by (auto simp: differentiable_def) from has_derivative_cnj[OF this] show "(\z. cnj (f z)) differentiable at x within A" by (auto simp: differentiable_def) qed lemma has_vector_derivative_cnj [derivative_intros]: assumes "(f has_vector_derivative f') (at z within A)" shows "((\z. cnj (f z)) has_vector_derivative cnj f') (at z within A)" using assms by (auto simp: has_vector_derivative_complex_iff intro: derivative_intros) subsection \Basic Lemmas\ +lemma complex_of_real_code[code_unfold]: "of_real = (\x. Complex x 0)" + by (intro ext, auto simp: complex_eq_iff) + lemma complex_eq_0: "z=0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0" by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff) lemma complex_neq_0: "z\0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0" by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff) lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z" by (cases z) (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric] simp del: of_real_power) lemma complex_div_cnj: "a / b = (a * cnj b) / (norm b)\<^sup>2" using complex_norm_square by auto lemma Re_complex_div_eq_0: "Re (a / b) = 0 \ Re (a * cnj b) = 0" by (auto simp add: Re_divide) lemma Im_complex_div_eq_0: "Im (a / b) = 0 \ Im (a * cnj b) = 0" by (auto simp add: Im_divide) lemma complex_div_gt_0: "(Re (a / b) > 0 \ Re (a * cnj b) > 0) \ (Im (a / b) > 0 \ Im (a * cnj b) > 0)" proof (cases "b = 0") case True then show ?thesis by auto next case False then have "0 < (Re b)\<^sup>2 + (Im b)\<^sup>2" by (simp add: complex_eq_iff sum_power2_gt_zero_iff) then show ?thesis by (simp add: Re_divide Im_divide zero_less_divide_iff) qed lemma Re_complex_div_gt_0: "Re (a / b) > 0 \ Re (a * cnj b) > 0" and Im_complex_div_gt_0: "Im (a / b) > 0 \ Im (a * cnj b) > 0" using complex_div_gt_0 by auto lemma Re_complex_div_ge_0: "Re (a / b) \ 0 \ Re (a * cnj b) \ 0" by (metis le_less Re_complex_div_eq_0 Re_complex_div_gt_0) lemma Im_complex_div_ge_0: "Im (a / b) \ 0 \ Im (a * cnj b) \ 0" by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 le_less) lemma Re_complex_div_lt_0: "Re (a / b) < 0 \ Re (a * cnj b) < 0" by (metis less_asym neq_iff Re_complex_div_eq_0 Re_complex_div_gt_0) lemma Im_complex_div_lt_0: "Im (a / b) < 0 \ Im (a * cnj b) < 0" by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 less_asym neq_iff) lemma Re_complex_div_le_0: "Re (a / b) \ 0 \ Re (a * cnj b) \ 0" by (metis not_le Re_complex_div_gt_0) lemma Im_complex_div_le_0: "Im (a / b) \ 0 \ Im (a * cnj b) \ 0" by (metis Im_complex_div_gt_0 not_le) lemma Re_divide_of_real [simp]: "Re (z / of_real r) = Re z / r" by (simp add: Re_divide power2_eq_square) lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r" by (simp add: Im_divide power2_eq_square) lemma Re_divide_Reals [simp]: "r \ \ \ Re (z / r) = Re z / Re r" by (metis Re_divide_of_real of_real_Re) lemma Im_divide_Reals [simp]: "r \ \ \ Im (z / r) = Im z / Re r" by (metis Im_divide_of_real of_real_Re) lemma Re_sum[simp]: "Re (sum f s) = (\x\s. Re (f x))" by (induct s rule: infinite_finite_induct) auto lemma Im_sum[simp]: "Im (sum f s) = (\x\s. Im(f x))" by (induct s rule: infinite_finite_induct) auto lemma sums_complex_iff: "f sums x \ ((\x. Re (f x)) sums Re x) \ ((\x. Im (f x)) sums Im x)" unfolding sums_def tendsto_complex_iff Im_sum Re_sum .. lemma summable_complex_iff: "summable f \ summable (\x. Re (f x)) \ summable (\x. Im (f x))" unfolding summable_def sums_complex_iff[abs_def] by (metis complex.sel) lemma summable_complex_of_real [simp]: "summable (\n. complex_of_real (f n)) \ summable f" unfolding summable_complex_iff by simp lemma summable_Re: "summable f \ summable (\x. Re (f x))" unfolding summable_complex_iff by blast lemma summable_Im: "summable f \ summable (\x. Im (f x))" unfolding summable_complex_iff by blast lemma complex_is_Nat_iff: "z \ \ \ Im z = 0 \ (\i. Re z = of_nat i)" by (auto simp: Nats_def complex_eq_iff) lemma complex_is_Int_iff: "z \ \ \ Im z = 0 \ (\i. Re z = of_int i)" by (auto simp: Ints_def complex_eq_iff) lemma complex_is_Real_iff: "z \ \ \ Im z = 0" by (auto simp: Reals_def complex_eq_iff) lemma Reals_cnj_iff: "z \ \ \ cnj z = z" by (auto simp: complex_is_Real_iff complex_eq_iff) lemma in_Reals_norm: "z \ \ \ norm z = \Re z\" by (simp add: complex_is_Real_iff norm_complex_def) lemma Re_Reals_divide: "r \ \ \ Re (r / z) = Re r * Re z / (norm z)\<^sup>2" by (simp add: Re_divide complex_is_Real_iff cmod_power2) lemma Im_Reals_divide: "r \ \ \ Im (r / z) = -Re r * Im z / (norm z)\<^sup>2" by (simp add: Im_divide complex_is_Real_iff cmod_power2) lemma series_comparison_complex: fixes f:: "nat \ 'a::banach" assumes sg: "summable g" and "\n. g n \ \" "\n. Re (g n) \ 0" and fg: "\n. n \ N \ norm(f n) \ norm(g n)" shows "summable f" proof - have g: "\n. cmod (g n) = Re (g n)" using assms by (metis abs_of_nonneg in_Reals_norm) show ?thesis apply (rule summable_comparison_test' [where g = "\n. norm (g n)" and N=N]) using sg apply (auto simp: summable_def) apply (rule_tac x = "Re s" in exI) apply (auto simp: g sums_Re) apply (metis fg g) done qed subsection \Polar Form for Complex Numbers\ lemma complex_unimodular_polar: assumes "norm z = 1" obtains t where "0 \ t" "t < 2 * pi" "z = Complex (cos t) (sin t)" by (metis cmod_power2 one_power2 complex_surj sincos_total_2pi [of "Re z" "Im z"] assms) subsubsection \$\cos \theta + i \sin \theta$\ primcorec cis :: "real \ complex" where "Re (cis a) = cos a" | "Im (cis a) = sin a" lemma cis_zero [simp]: "cis 0 = 1" by (simp add: complex_eq_iff) lemma norm_cis [simp]: "norm (cis a) = 1" by (simp add: norm_complex_def) lemma sgn_cis [simp]: "sgn (cis a) = cis a" by (simp add: sgn_div_norm) lemma cis_2pi [simp]: "cis (2 * pi) = 1" by (simp add: cis.ctr complex_eq_iff) lemma cis_neq_zero [simp]: "cis a \ 0" by (metis norm_cis norm_zero zero_neq_one) lemma cis_cnj: "cnj (cis t) = cis (-t)" by (simp add: complex_eq_iff) lemma cis_mult: "cis a * cis b = cis (a + b)" by (simp add: complex_eq_iff cos_add sin_add) lemma DeMoivre: "(cis a) ^ n = cis (real n * a)" by (induct n) (simp_all add: algebra_simps cis_mult) lemma cis_inverse [simp]: "inverse (cis a) = cis (- a)" by (simp add: complex_eq_iff) lemma cis_divide: "cis a / cis b = cis (a - b)" by (simp add: divide_complex_def cis_mult) lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re (cis a ^ n)" by (auto simp add: DeMoivre) lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im (cis a ^ n)" by (auto simp add: DeMoivre) lemma cis_pi [simp]: "cis pi = -1" by (simp add: complex_eq_iff) lemma cis_pi_half[simp]: "cis (pi / 2) = \" by (simp add: cis.ctr complex_eq_iff) lemma cis_minus_pi_half[simp]: "cis (-(pi / 2)) = -\" by (simp add: cis.ctr complex_eq_iff) lemma cis_multiple_2pi[simp]: "n \ \ \ cis (2 * pi * n) = 1" by (auto elim!: Ints_cases simp: cis.ctr one_complex.ctr) subsubsection \$r(\cos \theta + i \sin \theta)$\ definition rcis :: "real \ real \ complex" where "rcis r a = complex_of_real r * cis a" lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" by (simp add: rcis_def) lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a" by (simp add: rcis_def) lemma rcis_Ex: "\r a. z = rcis r a" by (simp add: complex_eq_iff polar_Ex) lemma complex_mod_rcis [simp]: "cmod (rcis r a) = \r\" by (simp add: rcis_def norm_mult) lemma cis_rcis_eq: "cis a = rcis 1 a" by (simp add: rcis_def) lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1 * r2) (a + b)" by (simp add: rcis_def cis_mult) lemma rcis_zero_mod [simp]: "rcis 0 a = 0" by (simp add: rcis_def) lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r" by (simp add: rcis_def) lemma rcis_eq_zero_iff [simp]: "rcis r a = 0 \ r = 0" by (simp add: rcis_def) lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)" by (simp add: rcis_def power_mult_distrib DeMoivre) lemma rcis_inverse: "inverse(rcis r a) = rcis (1 / r) (- a)" by (simp add: divide_inverse rcis_def) lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1 / r2) (a - b)" by (simp add: rcis_def cis_divide [symmetric]) subsubsection \Complex exponential\ lemma exp_Reals_eq: assumes "z \ \" shows "exp z = of_real (exp (Re z))" using assms by (auto elim!: Reals_cases simp: exp_of_real) lemma cis_conv_exp: "cis b = exp (\ * b)" proof - have "(\ * complex_of_real b) ^ n /\<^sub>R fact n = of_real (cos_coeff n * b^n) + \ * of_real (sin_coeff n * b^n)" for n :: nat proof - have "\ ^ n = fact n *\<^sub>R (cos_coeff n + \ * sin_coeff n)" by (induct n) (simp_all add: sin_coeff_Suc cos_coeff_Suc complex_eq_iff Re_divide Im_divide field_simps power2_eq_square add_nonneg_eq_0_iff) then show ?thesis by (simp add: field_simps) qed then show ?thesis using sin_converges [of b] cos_converges [of b] by (auto simp add: Complex_eq cis.ctr exp_def simp del: of_real_mult intro!: sums_unique sums_add sums_mult sums_of_real) qed lemma exp_eq_polar: "exp z = exp (Re z) * cis (Im z)" unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by (cases z) (simp add: Complex_eq) lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)" unfolding exp_eq_polar by simp lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)" unfolding exp_eq_polar by simp lemma norm_cos_sin [simp]: "norm (Complex (cos t) (sin t)) = 1" by (simp add: norm_complex_def) lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)" by (simp add: cis.code cmod_complex_polar exp_eq_polar Complex_eq) lemma complex_exp_exists: "\a r. z = complex_of_real r * exp a" apply (insert rcis_Ex [of z]) apply (auto simp add: exp_eq_polar rcis_def mult.assoc [symmetric]) apply (rule_tac x = "\ * complex_of_real a" in exI) apply auto done lemma exp_pi_i [simp]: "exp (of_real pi * \) = -1" by (metis cis_conv_exp cis_pi mult.commute) lemma exp_pi_i' [simp]: "exp (\ * of_real pi) = -1" using cis_conv_exp cis_pi by auto lemma exp_two_pi_i [simp]: "exp (2 * of_real pi * \) = 1" by (simp add: exp_eq_polar complex_eq_iff) lemma exp_two_pi_i' [simp]: "exp (\ * (of_real pi * 2)) = 1" by (metis exp_two_pi_i mult.commute) lemma continuous_on_cis [continuous_intros]: "continuous_on A f \ continuous_on A (\x. cis (f x))" by (auto simp: cis_conv_exp intro!: continuous_intros) subsubsection \Complex argument\ definition Arg :: "complex \ real" where "Arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \ - pi < a \ a \ pi))" lemma Arg_zero: "Arg 0 = 0" by (simp add: Arg_def) lemma cis_Arg_unique: assumes "sgn z = cis x" and "-pi < x" and "x \ pi" shows "Arg z = x" proof - from assms have "z \ 0" by auto have "(SOME a. sgn z = cis a \ -pi < a \ a \ pi) = x" proof fix a define d where "d = a - x" assume a: "sgn z = cis a \ - pi < a \ a \ pi" from a assms have "- (2*pi) < d \ d < 2*pi" unfolding d_def by simp moreover from a assms have "cos a = cos x" and "sin a = sin x" by (simp_all add: complex_eq_iff) then have cos: "cos d = 1" by (simp add: d_def cos_diff) moreover from cos have "sin d = 0" by (rule cos_one_sin_zero) ultimately have "d = 0" by (auto simp: sin_zero_iff elim!: evenE dest!: less_2_cases) then show "a = x" by (simp add: d_def) qed (simp add: assms del: Re_sgn Im_sgn) with \z \ 0\ show "Arg z = x" by (simp add: Arg_def) qed lemma Arg_correct: assumes "z \ 0" shows "sgn z = cis (Arg z) \ -pi < Arg z \ Arg z \ pi" proof (simp add: Arg_def assms, rule someI_ex) obtain r a where z: "z = rcis r a" using rcis_Ex by fast with assms have "r \ 0" by auto define b where "b = (if 0 < r then a else a + pi)" have b: "sgn z = cis b" using \r \ 0\ by (simp add: z b_def rcis_def of_real_def sgn_scaleR sgn_if complex_eq_iff) have cis_2pi_nat: "cis (2 * pi * real_of_nat n) = 1" for n by (induct n) (simp_all add: distrib_left cis_mult [symmetric] complex_eq_iff) have cis_2pi_int: "cis (2 * pi * real_of_int x) = 1" for x by (cases x rule: int_diff_cases) (simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat) define c where "c = b - 2 * pi * of_int \(b - pi) / (2 * pi)\" have "sgn z = cis c" by (simp add: b c_def cis_divide [symmetric] cis_2pi_int) moreover have "- pi < c \ c \ pi" using ceiling_correct [of "(b - pi) / (2*pi)"] by (simp add: c_def less_divide_eq divide_le_eq algebra_simps del: le_of_int_ceiling) ultimately show "\a. sgn z = cis a \ -pi < a \ a \ pi" by fast qed lemma Arg_bounded: "- pi < Arg z \ Arg z \ pi" by (cases "z = 0") (simp_all add: Arg_zero Arg_correct) lemma cis_Arg: "z \ 0 \ cis (Arg z) = sgn z" by (simp add: Arg_correct) lemma rcis_cmod_Arg: "rcis (cmod z) (Arg z) = z" by (cases "z = 0") (simp_all add: rcis_def cis_Arg sgn_div_norm of_real_def) lemma rcis_cnj: shows "cnj a = rcis (cmod a) (- Arg a)" by (metis cis_cnj complex_cnj_complex_of_real complex_cnj_mult rcis_cmod_Arg rcis_def) lemma cos_Arg_i_mult_zero [simp]: "y \ 0 \ Re y = 0 \ cos (Arg y) = 0" using cis_Arg [of y] by (simp add: complex_eq_iff) lemma Arg_ii [simp]: "Arg \ = pi/2" by (rule cis_Arg_unique; simp add: sgn_eq) lemma Arg_minus_ii [simp]: "Arg (-\) = -pi/2" proof (rule cis_Arg_unique) show "sgn (- \) = cis (- pi / 2)" by (simp add: sgn_eq) show "- pi / 2 \ pi" using pi_not_less_zero by linarith qed auto subsection \Complex n-th roots\ lemma bij_betw_roots_unity: assumes "n > 0" shows "bij_betw (\k. cis (2 * pi * real k / real n)) {.. = cis (2*pi*(real k - real l)/n)" using assms by (simp add: field_simps cis_divide) finally have "cos (2*pi*(real k - real l) / n) = 1" by (simp add: complex_eq_iff) then obtain m :: int where "2 * pi * (real k - real l) / real n = real_of_int m * 2 * pi" by (subst (asm) cos_one_2pi_int) blast hence "real_of_int (int k - int l) = real_of_int (m * int n)" unfolding of_int_diff of_int_mult using assms by (simp add: nonzero_divide_eq_eq) also note of_int_eq_iff finally have *: "abs m * n = abs (int k - int l)" by (simp add: abs_mult) also have "\ < int n" using kl by linarith finally have "m = 0" using assms by simp with * show "k = l" by simp qed have subset: "?f ` {.. {z. z ^ n = 1}" proof safe fix k :: nat have "cis (2 * pi * real k / real n) ^ n = cis (2 * pi) ^ k" using assms by (simp add: DeMoivre mult_ac) also have "cis (2 * pi) = 1" by (simp add: complex_eq_iff) finally show "?f k ^ n = 1" by simp qed have "n = card {.. \ card {z::complex. z ^ n = 1}" by (intro card_inj_on_le[OF inj]) (auto simp: finite_roots_unity) finally have card: "card {z::complex. z ^ n = 1} = n" using assms by (intro antisym card_roots_unity) auto have "card (?f ` {.. 0" shows "card {z::complex. z ^ n = 1} = n" using bij_betw_same_card [OF bij_betw_roots_unity [OF assms]] by simp lemma bij_betw_nth_root_unity: fixes c :: complex and n :: nat assumes c: "c \ 0" and n: "n > 0" defines "c' \ root n (norm c) * cis (Arg c / n)" shows "bij_betw (\z. c' * z) {z. z ^ n = 1} {z. z ^ n = c}" proof - have "c' ^ n = of_real (root n (norm c) ^ n) * cis (Arg c)" unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre) also from n have "root n (norm c) ^ n = norm c" by simp also from c have "of_real \ * cis (Arg c) = c" by (simp add: cis_Arg Complex.sgn_eq) finally have [simp]: "c' ^ n = c" . show ?thesis unfolding bij_betw_def inj_on_def proof safe fix z :: complex assume "z ^ n = 1" hence "(c' * z) ^ n = c' ^ n" by (simp add: power_mult_distrib) also have "c' ^ n = of_real (root n (norm c) ^ n) * cis (Arg c)" unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre) also from n have "root n (norm c) ^ n = norm c" by simp also from c have "\ * cis (Arg c) = c" by (simp add: cis_Arg Complex.sgn_eq) finally show "(c' * z) ^ n = c" . next fix z assume z: "c = z ^ n" define z' where "z' = z / c'" from c and n have "c' \ 0" by (auto simp: c'_def) with n c have "z = c' * z'" and "z' ^ n = 1" by (auto simp: z'_def power_divide z) thus "z \ (\z. c' * z) ` {z. z ^ n = 1}" by blast qed (insert c n, auto simp: c'_def) qed lemma finite_nth_roots [intro]: assumes "n > 0" shows "finite {z::complex. z ^ n = c}" proof (cases "c = 0") case True with assms have "{z::complex. z ^ n = c} = {0}" by auto thus ?thesis by simp next case False from assms have "finite {z::complex. z ^ n = 1}" by (intro finite_roots_unity) simp_all also have "?this \ ?thesis" by (rule bij_betw_finite, rule bij_betw_nth_root_unity) fact+ finally show ?thesis . qed lemma card_nth_roots: assumes "c \ 0" "n > 0" shows "card {z::complex. z ^ n = c} = n" proof - have "card {z. z ^ n = c} = card {z::complex. z ^ n = 1}" by (rule sym, rule bij_betw_same_card, rule bij_betw_nth_root_unity) fact+ also have "\ = n" by (rule card_roots_unity_eq) fact+ finally show ?thesis . qed lemma sum_roots_unity: assumes "n > 1" shows "\{z::complex. z ^ n = 1} = 0" proof - define \ where "\ = cis (2 * pi / real n)" have [simp]: "\ \ 1" proof assume "\ = 1" with assms obtain k :: int where "2 * pi / real n = 2 * pi * of_int k" by (auto simp: \_def complex_eq_iff cos_one_2pi_int) with assms have "real n * of_int k = 1" by (simp add: field_simps) also have "real n * of_int k = of_int (int n * k)" by simp also have "1 = (of_int 1 :: real)" by simp also note of_int_eq_iff finally show False using assms by (auto simp: zmult_eq_1_iff) qed have "(\z | z ^ n = 1. z :: complex) = (\k = (\k ^ k)" by (intro sum.cong refl) (auto simp: \_def DeMoivre mult_ac) also have "\ = (\ ^ n - 1) / (\ - 1)" by (subst geometric_sum) auto also have "\ ^ n - 1 = cis (2 * pi) - 1" using assms by (auto simp: \_def DeMoivre) also have "\ = 0" by (simp add: complex_eq_iff) finally show ?thesis by simp qed lemma sum_nth_roots: assumes "n > 1" shows "\{z::complex. z ^ n = c} = 0" proof (cases "c = 0") case True with assms have "{z::complex. z ^ n = c} = {0}" by auto also have "\\ = 0" by simp finally show ?thesis . next case False define c' where "c' = root n (norm c) * cis (Arg c / n)" from False and assms have "(\{z. z ^ n = c}) = (\z | z ^ n = 1. c' * z)" by (subst sum.reindex_bij_betw [OF bij_betw_nth_root_unity, symmetric]) (auto simp: sum_distrib_left finite_roots_unity c'_def) also from assms have "\ = 0" by (simp add: sum_distrib_left [symmetric] sum_roots_unity) finally show ?thesis . qed subsection \Square root of complex numbers\ primcorec csqrt :: "complex \ complex" where "Re (csqrt z) = sqrt ((cmod z + Re z) / 2)" | "Im (csqrt z) = (if Im z = 0 then 1 else sgn (Im z)) * sqrt ((cmod z - Re z) / 2)" lemma csqrt_of_real_nonneg [simp]: "Im x = 0 \ Re x \ 0 \ csqrt x = sqrt (Re x)" by (simp add: complex_eq_iff norm_complex_def) lemma csqrt_of_real_nonpos [simp]: "Im x = 0 \ Re x \ 0 \ csqrt x = \ * sqrt \Re x\" by (simp add: complex_eq_iff norm_complex_def) lemma of_real_sqrt: "x \ 0 \ of_real (sqrt x) = csqrt (of_real x)" by (simp add: complex_eq_iff norm_complex_def) lemma csqrt_0 [simp]: "csqrt 0 = 0" by simp lemma csqrt_1 [simp]: "csqrt 1 = 1" by simp lemma csqrt_ii [simp]: "csqrt \ = (1 + \) / sqrt 2" by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt) lemma power2_csqrt[simp,algebra]: "(csqrt z)\<^sup>2 = z" proof (cases "Im z = 0") case True then show ?thesis using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"] by (cases "0::real" "Re z" rule: linorder_cases) (simp_all add: complex_eq_iff Re_power2 Im_power2 power2_eq_square cmod_eq_Re) next case False moreover have "cmod z * cmod z - Re z * Re z = Im z * Im z" by (simp add: norm_complex_def power2_eq_square) moreover have "\Re z\ \ cmod z" by (simp add: norm_complex_def) ultimately show ?thesis by (simp add: Re_power2 Im_power2 complex_eq_iff real_sgn_eq field_simps real_sqrt_mult[symmetric] real_sqrt_divide) qed lemma csqrt_eq_0 [simp]: "csqrt z = 0 \ z = 0" by auto (metis power2_csqrt power_eq_0_iff) lemma csqrt_eq_1 [simp]: "csqrt z = 1 \ z = 1" by auto (metis power2_csqrt power2_eq_1_iff) lemma csqrt_principal: "0 < Re (csqrt z) \ Re (csqrt z) = 0 \ 0 \ Im (csqrt z)" by (auto simp add: not_less cmod_plus_Re_le_0_iff Im_eq_0) lemma Re_csqrt: "0 \ Re (csqrt z)" by (metis csqrt_principal le_less) lemma csqrt_square: assumes "0 < Re b \ (Re b = 0 \ 0 \ Im b)" shows "csqrt (b^2) = b" proof - have "csqrt (b^2) = b \ csqrt (b^2) = - b" by (simp add: power2_eq_iff[symmetric]) moreover have "csqrt (b^2) \ -b \ b = 0" using csqrt_principal[of "b ^ 2"] assms by (intro disjCI notI) (auto simp: complex_eq_iff) ultimately show ?thesis by auto qed lemma csqrt_unique: "w\<^sup>2 = z \ 0 < Re w \ Re w = 0 \ 0 \ Im w \ csqrt z = w" by (auto simp: csqrt_square) lemma csqrt_minus [simp]: assumes "Im x < 0 \ (Im x = 0 \ 0 \ Re x)" shows "csqrt (- x) = \ * csqrt x" proof - have "csqrt ((\ * csqrt x)^2) = \ * csqrt x" proof (rule csqrt_square) have "Im (csqrt x) \ 0" using assms by (auto simp add: cmod_eq_Re mult_le_0_iff field_simps complex_Re_le_cmod) then show "0 < Re (\ * csqrt x) \ Re (\ * csqrt x) = 0 \ 0 \ Im (\ * csqrt x)" by (auto simp add: Re_csqrt simp del: csqrt.simps) qed also have "(\ * csqrt x)^2 = - x" by (simp add: power_mult_distrib) finally show ?thesis . qed text \Legacy theorem names\ lemmas cmod_def = norm_complex_def lemma legacy_Complex_simps: shows Complex_eq_0: "Complex a b = 0 \ a = 0 \ b = 0" and complex_add: "Complex a b + Complex c d = Complex (a + c) (b + d)" and complex_minus: "- (Complex a b) = Complex (- a) (- b)" and complex_diff: "Complex a b - Complex c d = Complex (a - c) (b - d)" and Complex_eq_1: "Complex a b = 1 \ a = 1 \ b = 0" and Complex_eq_neg_1: "Complex a b = - 1 \ a = - 1 \ b = 0" and complex_mult: "Complex a b * Complex c d = Complex (a * c - b * d) (a * d + b * c)" and complex_inverse: "inverse (Complex a b) = Complex (a / (a\<^sup>2 + b\<^sup>2)) (- b / (a\<^sup>2 + b\<^sup>2))" and Complex_eq_numeral: "Complex a b = numeral w \ a = numeral w \ b = 0" and Complex_eq_neg_numeral: "Complex a b = - numeral w \ a = - numeral w \ b = 0" and complex_scaleR: "scaleR r (Complex a b) = Complex (r * a) (r * b)" and Complex_eq_i: "Complex x y = \ \ x = 0 \ y = 1" and i_mult_Complex: "\ * Complex a b = Complex (- b) a" and Complex_mult_i: "Complex a b * \ = Complex (- b) a" and i_complex_of_real: "\ * complex_of_real r = Complex 0 r" and complex_of_real_i: "complex_of_real r * \ = Complex 0 r" and Complex_add_complex_of_real: "Complex x y + complex_of_real r = Complex (x+r) y" and complex_of_real_add_Complex: "complex_of_real r + Complex x y = Complex (r+x) y" and Complex_mult_complex_of_real: "Complex x y * complex_of_real r = Complex (x*r) (y*r)" and complex_of_real_mult_Complex: "complex_of_real r * Complex x y = Complex (r*x) (r*y)" and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa \ y = 0)" and complex_cnj: "cnj (Complex a b) = Complex a (- b)" and Complex_sum': "sum (\x. Complex (f x) 0) s = Complex (sum f s) 0" and Complex_sum: "Complex (sum f s) 0 = sum (\x. Complex (f x) 0) s" and complex_of_real_def: "complex_of_real r = Complex r 0" and complex_norm: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)" by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide) lemma Complex_in_Reals: "Complex x 0 \ \" by (metis Reals_of_real complex_of_real_def) end diff --git a/src/HOL/Finite_Set.thy b/src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy +++ b/src/HOL/Finite_Set.thy @@ -1,2526 +1,2538 @@ (* 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''. The commutativity requirement is relativised to the carrier set \S\: \ locale comp_fun_commute_on = fixes S :: "'a set" fixes f :: "'a \ 'b \ 'b" assumes comp_fun_commute_on: "x \ S \ y \ S \ f y \ f x = f x \ f y" begin lemma fun_left_comm: "x \ S \ y \ S \ f y (f x z) = f x (f y z)" using comp_fun_commute_on by (simp add: fun_eq_iff) lemma commute_left_comp: "x \ S \ y \ S \ f y \ (f x \ g) = f x \ (f y \ g)" by (simp add: o_assoc comp_fun_commute_on) end inductive fold_graph :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b \ bool" for f :: "'a \ 'b \ 'b" and z :: 'b where emptyI [intro]: "fold_graph f z {} z" | insertI [intro]: "x \ A \ fold_graph f z A y \ fold_graph f z (insert x A) (f x y)" inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x" lemma fold_graph_closed_lemma: "fold_graph f z A x \ x \ B" if "fold_graph g z A x" "\a b. a \ A \ b \ B \ f a b = g a b" "\a b. a \ A \ b \ B \ g a b \ B" "z \ B" using that(1-3) proof (induction rule: fold_graph.induct) case (insertI x A y) have "fold_graph f z A y" "y \ B" unfolding atomize_conj by (rule insertI.IH) (auto intro: insertI.prems) then have "g x y \ B" and f_eq: "f x y = g x y" by (auto simp: insertI.prems) moreover have "fold_graph f z (insert x A) (f x y)" by (rule fold_graph.insertI; fact) ultimately show ?case by (simp add: f_eq) qed (auto intro!: that) lemma fold_graph_closed_eq: "fold_graph f z A = fold_graph g z A" if "\a b. a \ A \ b \ B \ f a b = g a b" "\a b. a \ A \ b \ B \ g a b \ B" "z \ B" using fold_graph_closed_lemma[of f z A _ B g] fold_graph_closed_lemma[of g z A _ B f] that by auto definition fold :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b" where "fold f z A = (if finite A then (THE y. fold_graph f z A y) else z)" lemma fold_closed_eq: "fold f z A = fold g z A" if "\a b. a \ A \ b \ B \ f a b = g a b" "\a b. a \ A \ b \ B \ g a b \ B" "z \ B" unfolding Finite_Set.fold_def by (subst fold_graph_closed_eq[where B=B and g=g]) (auto simp: that) text \ A tempting alternative for the definition is \<^term>\if finite A then THE y. fold_graph f z A y else e\. It allows the removal of finiteness assumptions from the theorems \fold_comm\, \fold_reindex\ and \fold_distrib\. The proofs become ugly. It is not worth the effort. (???) \ lemma finite_imp_fold_graph: "finite A \ \x. fold_graph f z A x" by (induct rule: finite_induct) auto subsubsection \From \<^const>\fold_graph\ to \<^term>\fold\\ context comp_fun_commute_on begin lemma fold_graph_finite: assumes "fold_graph f z A y" shows "finite A" using assms by induct simp_all lemma fold_graph_insertE_aux: assumes "A \ S" assumes "fold_graph f z A y" "a \ A" shows "\y'. y = f a y' \ fold_graph f z (A - {a}) y'" using assms(2-,1) proof (induct set: fold_graph) case emptyI then show ?case by simp next case (insertI x A y) show ?case proof (cases "x = a") case True with insertI show ?thesis by auto next case False then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'" using insertI by auto from insertI have "x \ S" "a \ S" by auto then have "f x y = f a (f x y')" unfolding y by (intro fun_left_comm; simp) moreover have "fold_graph f z (insert x A - {a}) (f x y')" using y' and \x \ a\ and \x \ A\ by (simp add: insert_Diff_if fold_graph.insertI) ultimately show ?thesis by fast qed qed lemma fold_graph_insertE: assumes "insert x A \ S" assumes "fold_graph f z (insert x A) v" and "x \ A" obtains y where "v = f x y" and "fold_graph f z A y" using assms by (auto dest: fold_graph_insertE_aux[OF \insert x A \ S\ _ insertI1]) lemma fold_graph_determ: assumes "A \ S" assumes "fold_graph f z A x" "fold_graph f z A y" shows "y = x" using assms(2-,1) proof (induct arbitrary: y set: fold_graph) case emptyI then show ?case by fast next case (insertI x A y v) from \insert x A \ S\ and \fold_graph f z (insert x A) v\ and \x \ A\ obtain y' where "v = f x y'" and "fold_graph f z A y'" by (rule fold_graph_insertE) from \fold_graph f z A y'\ insertI have "y' = y" by simp with \v = f x y'\ show "v = f x y" by simp qed lemma fold_equality: "A \ S \ fold_graph f z A y \ fold f z A = y" by (cases "finite A") (auto simp add: fold_def intro: fold_graph_determ dest: fold_graph_finite) lemma fold_graph_fold: assumes "A \ S" assumes "finite A" shows "fold_graph f z A (fold f z A)" proof - from \finite A\ have "\x. fold_graph f z A x" by (rule finite_imp_fold_graph) moreover note fold_graph_determ[OF \A \ S\] ultimately have "\!x. fold_graph f z A x" by (rule ex_ex1I) then have "fold_graph f z A (The (fold_graph f z A))" by (rule theI') with assms show ?thesis by (simp add: fold_def) qed text \The base case for \fold\:\ lemma (in -) fold_infinite [simp]: "\ finite A \ fold f z A = z" by (auto simp: fold_def) lemma (in -) fold_empty [simp]: "fold f z {} = z" by (auto simp: fold_def) text \The various recursion equations for \<^const>\fold\:\ lemma fold_insert [simp]: assumes "insert x A \ S" assumes "finite A" and "x \ A" shows "fold f z (insert x A) = f x (fold f z A)" proof (rule fold_equality[OF \insert x A \ S\]) fix z from \insert x A \ S\ \finite A\ have "fold_graph f z A (fold f z A)" by (blast intro: fold_graph_fold) with \x \ A\ have "fold_graph f z (insert x A) (f x (fold f z A))" by (rule fold_graph.insertI) then show "fold_graph f z (insert x A) (f x (fold f z A))" by simp qed declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del] \ \No more proofs involve these.\ lemma fold_fun_left_comm: assumes "insert x A \ S" "finite A" shows "f x (fold f z A) = fold f (f x z) A" using assms(2,1) proof (induct rule: finite_induct) case empty then show ?case by simp next case (insert y F) then have "fold f (f x z) (insert y F) = f y (fold f (f x z) F)" by simp also have "\ = f x (f y (fold f z F))" using insert by (simp add: fun_left_comm[where ?y=x]) also have "\ = f x (fold f z (insert y F))" proof - from insert have "insert y F \ S" by simp from fold_insert[OF this] insert show ?thesis by simp qed finally show ?case .. qed lemma fold_insert2: "insert x A \ S \ finite A \ x \ A \ fold f z (insert x A) = fold f (f x z) A" by (simp add: fold_fun_left_comm) lemma fold_rec: assumes "A \ S" assumes "finite A" and "x \ A" shows "fold f z A = f x (fold f z (A - {x}))" proof - have A: "A = insert x (A - {x})" using \x \ A\ by blast then have "fold f z A = fold f z (insert x (A - {x}))" by simp also have "\ = f x (fold f z (A - {x}))" by (rule fold_insert) (use assms in \auto\) finally show ?thesis . qed lemma fold_insert_remove: assumes "insert x A \ S" assumes "finite A" shows "fold f z (insert x A) = f x (fold f z (A - {x}))" proof - from \finite A\ have "finite (insert x A)" by auto moreover have "x \ insert x A" by auto ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))" using \insert x A \ S\ by (blast intro: fold_rec) then show ?thesis by simp qed lemma fold_set_union_disj: assumes "A \ S" "B \ S" assumes "finite A" "finite B" "A \ B = {}" shows "Finite_Set.fold f z (A \ B) = Finite_Set.fold f (Finite_Set.fold f z A) B" using \finite B\ assms(1,2,3,5) proof induct case (insert x F) have "fold f z (A \ insert x F) = f x (fold f (fold f z A) F)" using insert by auto also have "\ = fold f (fold f z A) (insert x F)" using insert by (blast intro: fold_insert[symmetric]) finally show ?case . qed simp end text \Other properties of \<^const>\fold\:\ lemma fold_graph_image: assumes "inj_on g A" shows "fold_graph f z (g ` A) = fold_graph (f \ g) z A" proof fix w show "fold_graph f z (g ` A) w = fold_graph (f o g) z A w" proof assume "fold_graph f z (g ` A) w" then show "fold_graph (f \ g) z A w" using assms proof (induct "g ` A" w arbitrary: A) case emptyI then show ?case by (auto intro: fold_graph.emptyI) next case (insertI x A r B) from \inj_on g B\ \x \ A\ \insert x A = image g B\ obtain x' A' where "x' \ A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'" by (rule inj_img_insertE) from insertI.prems have "fold_graph (f \ g) z A' r" by (auto intro: insertI.hyps) with \x' \ A'\ have "fold_graph (f \ g) z (insert x' A') ((f \ g) x' r)" by (rule fold_graph.insertI) then show ?case by simp qed next assume "fold_graph (f \ g) z A w" then show "fold_graph f z (g ` A) w" using assms proof induct case emptyI then show ?case by (auto intro: fold_graph.emptyI) next case (insertI x A r) from \x \ A\ insertI.prems have "g x \ g ` A" by auto moreover from insertI have "fold_graph f z (g ` A) r" by simp ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)" by (rule fold_graph.insertI) then show ?case by simp qed qed qed lemma fold_image: assumes "inj_on g A" shows "fold f z (g ` A) = fold (f \ g) z A" proof (cases "finite A") case False with assms show ?thesis by (auto dest: finite_imageD simp add: fold_def) next case True then show ?thesis by (auto simp add: fold_def fold_graph_image[OF assms]) qed lemma fold_cong: assumes "comp_fun_commute_on S f" "comp_fun_commute_on S g" and "A \ S" "finite A" and cong: "\x. x \ A \ f x = g x" and "s = t" and "A = B" shows "fold f s A = fold g t B" proof - have "fold f s A = fold g s A" using \finite A\ \A \ S\ cong proof (induct A) case empty then show ?case by simp next case insert interpret f: comp_fun_commute_on S f by (fact \comp_fun_commute_on S f\) interpret g: comp_fun_commute_on S g by (fact \comp_fun_commute_on S g\) from insert show ?case by simp qed with assms show ?thesis by simp qed text \A simplified version for idempotent functions:\ locale comp_fun_idem_on = comp_fun_commute_on + assumes comp_fun_idem_on: "x \ S \ f x \ f x = f x" begin lemma fun_left_idem: "x \ S \ f x (f x z) = f x z" using comp_fun_idem_on by (simp add: fun_eq_iff) lemma fold_insert_idem: assumes "insert x A \ S" assumes fin: "finite A" shows "fold f z (insert x A) = f x (fold f z A)" proof cases assume "x \ A" then obtain B where "A = insert x B" and "x \ B" by (rule set_insert) then show ?thesis using assms by (simp add: comp_fun_idem_on fun_left_idem) next assume "x \ A" then show ?thesis using assms by auto qed declare fold_insert [simp del] fold_insert_idem [simp] lemma fold_insert_idem2: "insert x A \ S \ finite A \ fold f z (insert x A) = fold f (f x z) A" by (simp add: fold_fun_left_comm) end subsubsection \Liftings to \comp_fun_commute_on\ etc.\ lemma (in comp_fun_commute_on) comp_comp_fun_commute_on: "range g \ S \ comp_fun_commute_on R (f \ g)" by standard (force intro: comp_fun_commute_on) lemma (in comp_fun_idem_on) comp_comp_fun_idem_on: assumes "range g \ S" shows "comp_fun_idem_on R (f \ g)" proof interpret f_g: comp_fun_commute_on R "f o g" by (fact comp_comp_fun_commute_on[OF \range g \ S\]) show "x \ R \ y \ R \ (f \ g) y \ (f \ g) x = (f \ g) x \ (f \ g) y" for x y by (fact f_g.comp_fun_commute_on) qed (use \range g \ S\ in \force intro: comp_fun_idem_on\) lemma (in comp_fun_commute_on) comp_fun_commute_on_funpow: "comp_fun_commute_on S (\x. f x ^^ g x)" proof fix x y assume "x \ S" "y \ S" show "f y ^^ g y \ f x ^^ g x = f x ^^ g x \ f y ^^ g y" proof (cases "x = y") case True then show ?thesis by simp next case False show ?thesis proof (induct "g x" arbitrary: g) case 0 then show ?case by simp next case (Suc n g) have hyp1: "f y ^^ g y \ f x = f x \ f y ^^ g y" proof (induct "g y" arbitrary: g) case 0 then show ?case by simp next case (Suc n g) define h where "h z = g z - 1" for z with Suc have "n = h y" by simp with Suc have hyp: "f y ^^ h y \ f x = f x \ f y ^^ h y" by auto from Suc h_def have "g y = Suc (h y)" by simp with \x \ S\ \y \ S\ show ?case by (simp add: comp_assoc hyp) (simp add: o_assoc comp_fun_commute_on) qed define h where "h z = (if z = x then g x - 1 else g z)" for z with Suc have "n = h x" by simp with Suc have "f y ^^ h y \ f x ^^ h x = f x ^^ h x \ f y ^^ h y" by auto with False h_def have hyp2: "f y ^^ g y \ f x ^^ h x = f x ^^ h x \ f y ^^ g y" by simp from Suc h_def have "g x = Suc (h x)" by simp then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2) (simp add: comp_assoc hyp1) qed qed qed subsubsection \\<^term>\UNIV\ as carrier set\ locale comp_fun_commute = fixes f :: "'a \ 'b \ 'b" assumes comp_fun_commute: "f y \ f x = f x \ f y" begin lemma (in -) comp_fun_commute_def': "comp_fun_commute f = comp_fun_commute_on UNIV f" unfolding comp_fun_commute_def comp_fun_commute_on_def by blast text \ We abuse the \rewrites\ functionality of locales to remove trivial assumptions that result from instantiating the carrier set to \<^term>\UNIV\. \ sublocale comp_fun_commute_on UNIV f rewrites "\X. (X \ UNIV) \ True" and "\x. x \ UNIV \ True" and "\P. (True \ P) \ Trueprop P" and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)" proof - show "comp_fun_commute_on UNIV f" by standard (simp add: comp_fun_commute) qed simp_all end lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f o g)" unfolding comp_fun_commute_def' by (fact comp_comp_fun_commute_on) lemma (in comp_fun_commute) comp_fun_commute_funpow: "comp_fun_commute (\x. f x ^^ g x)" unfolding comp_fun_commute_def' by (fact comp_fun_commute_on_funpow) locale comp_fun_idem = comp_fun_commute + assumes comp_fun_idem: "f x o f x = f x" begin lemma (in -) comp_fun_idem_def': "comp_fun_idem f = comp_fun_idem_on UNIV f" unfolding comp_fun_idem_on_def comp_fun_idem_def comp_fun_commute_def' unfolding comp_fun_idem_axioms_def comp_fun_idem_on_axioms_def by blast text \ Again, we abuse the \rewrites\ functionality of locales to remove trivial assumptions that result from instantiating the carrier set to \<^term>\UNIV\. \ sublocale comp_fun_idem_on UNIV f rewrites "\X. (X \ UNIV) \ True" and "\x. x \ UNIV \ True" and "\P. (True \ P) \ Trueprop P" and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)" proof - show "comp_fun_idem_on UNIV f" by standard (simp_all add: comp_fun_idem comp_fun_commute) qed simp_all end lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f o g)" unfolding comp_fun_idem_def' by (fact comp_comp_fun_idem_on) subsubsection \Expressing set operations via \<^const>\fold\\ lemma comp_fun_commute_const: "comp_fun_commute (\_. f)" by standard rule lemma comp_fun_idem_insert: "comp_fun_idem insert" by standard auto lemma comp_fun_idem_remove: "comp_fun_idem Set.remove" by standard auto lemma (in semilattice_inf) comp_fun_idem_inf: "comp_fun_idem inf" by standard (auto simp add: inf_left_commute) lemma (in semilattice_sup) comp_fun_idem_sup: "comp_fun_idem sup" by standard (auto simp add: sup_left_commute) lemma union_fold_insert: assumes "finite A" shows "A \ B = fold insert B A" proof - interpret comp_fun_idem insert by (fact comp_fun_idem_insert) from \finite A\ show ?thesis by (induct A arbitrary: B) simp_all qed lemma minus_fold_remove: assumes "finite A" shows "B - A = fold Set.remove B A" proof - interpret comp_fun_idem Set.remove by (fact comp_fun_idem_remove) from \finite A\ have "fold Set.remove B A = B - A" by (induct A arbitrary: B) auto (* slow *) then show ?thesis .. qed lemma comp_fun_commute_filter_fold: "comp_fun_commute (\x A'. if P x then Set.insert x A' else A')" proof - interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert) show ?thesis by standard (auto simp: fun_eq_iff) qed lemma Set_filter_fold: assumes "finite A" shows "Set.filter P A = fold (\x A'. if P x then Set.insert x A' else A') {} A" using assms proof - interpret commute_insert: comp_fun_commute "(\x A'. if P x then Set.insert x A' else A')" by (fact comp_fun_commute_filter_fold) from \finite A\ show ?thesis by induct (auto simp add: Set.filter_def) qed lemma inter_Set_filter: assumes "finite B" shows "A \ B = Set.filter (\x. x \ A) B" using assms by induct (auto simp: Set.filter_def) lemma image_fold_insert: assumes "finite A" shows "image f A = fold (\k A. Set.insert (f k) A) {} A" proof - interpret comp_fun_commute "\k A. Set.insert (f k) A" by standard auto show ?thesis using assms by (induct A) auto qed lemma Ball_fold: assumes "finite A" shows "Ball A P = fold (\k s. s \ P k) True A" proof - interpret comp_fun_commute "\k s. s \ P k" by standard auto show ?thesis using assms by (induct A) auto qed lemma Bex_fold: assumes "finite A" shows "Bex A P = fold (\k s. s \ P k) False A" proof - interpret comp_fun_commute "\k s. s \ P k" by standard auto show ?thesis using assms by (induct A) auto qed lemma comp_fun_commute_Pow_fold: "comp_fun_commute (\x A. A \ Set.insert x ` A)" by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast lemma Pow_fold: assumes "finite A" shows "Pow A = fold (\x A. A \ Set.insert x ` A) {{}} A" proof - interpret comp_fun_commute "\x A. A \ Set.insert x ` A" by (rule comp_fun_commute_Pow_fold) show ?thesis using assms by (induct A) (auto simp: Pow_insert) qed lemma fold_union_pair: assumes "finite B" shows "(\y\B. {(x, y)}) \ A = fold (\y. Set.insert (x, y)) A B" proof - interpret comp_fun_commute "\y. Set.insert (x, y)" by standard auto show ?thesis using assms by (induct arbitrary: A) simp_all qed lemma comp_fun_commute_product_fold: "finite B \ comp_fun_commute (\x z. fold (\y. Set.insert (x, y)) z B)" by standard (auto simp: fold_union_pair [symmetric]) lemma product_fold: assumes "finite A" "finite B" shows "A \ B = fold (\x z. fold (\y. Set.insert (x, y)) z B) {} A" proof - interpret commute_product: comp_fun_commute "(\x z. fold (\y. Set.insert (x, y)) z B)" by (fact comp_fun_commute_product_fold[OF \finite B\]) from assms show ?thesis unfolding Sigma_def by (induct A) (simp_all add: fold_union_pair) qed context complete_lattice begin lemma inf_Inf_fold_inf: assumes "finite A" shows "inf (Inf A) B = fold inf B A" proof - interpret comp_fun_idem inf by (fact comp_fun_idem_inf) from \finite A\ fold_fun_left_comm show ?thesis by (induct A arbitrary: B) (simp_all add: inf_commute fun_eq_iff) qed lemma sup_Sup_fold_sup: assumes "finite A" shows "sup (Sup A) B = fold sup B A" proof - interpret comp_fun_idem sup by (fact comp_fun_idem_sup) from \finite A\ fold_fun_left_comm show ?thesis by (induct A arbitrary: B) (simp_all add: sup_commute fun_eq_iff) qed lemma Inf_fold_inf: "finite A \ Inf A = fold inf top A" using inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2) lemma Sup_fold_sup: "finite A \ Sup A = fold sup bot A" using sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2) lemma inf_INF_fold_inf: assumes "finite A" shows "inf B (\(f ` A)) = fold (inf \ f) B A" (is "?inf = ?fold") proof - interpret comp_fun_idem inf by (fact comp_fun_idem_inf) interpret comp_fun_idem "inf \ f" by (fact comp_comp_fun_idem) from \finite A\ have "?fold = ?inf" by (induct A arbitrary: B) (simp_all add: inf_left_commute) then show ?thesis .. qed lemma sup_SUP_fold_sup: assumes "finite A" shows "sup B (\(f ` A)) = fold (sup \ f) B A" (is "?sup = ?fold") proof - interpret comp_fun_idem sup by (fact comp_fun_idem_sup) interpret comp_fun_idem "sup \ f" by (fact comp_comp_fun_idem) from \finite A\ have "?fold = ?sup" by (induct A arbitrary: B) (simp_all add: sup_left_commute) then show ?thesis .. qed lemma INF_fold_inf: "finite A \ \(f ` A) = fold (inf \ f) top A" using inf_INF_fold_inf [of A top] by simp lemma SUP_fold_sup: "finite A \ \(f ` A) = fold (sup \ f) bot A" using sup_SUP_fold_sup [of A bot] by simp lemma finite_Inf_in: assumes "finite A" "A\{}" and inf: "\x y. \x \ A; y \ A\ \ inf x y \ A" shows "Inf A \ A" proof - have "Inf B \ A" if "B \ A" "B\{}" for B using finite_subset [OF \B \ A\ \finite A\] that by (induction B) (use inf in \force+\) then show ?thesis by (simp add: assms) qed lemma finite_Sup_in: assumes "finite A" "A\{}" and sup: "\x y. \x \ A; y \ A\ \ sup x y \ A" shows "Sup A \ A" proof - have "Sup B \ A" if "B \ A" "B\{}" for B using finite_subset [OF \B \ A\ \finite A\] that by (induction B) (use sup in \force+\) then show ?thesis by (simp add: assms) qed end subsection \Locales as mini-packages for fold operations\ subsubsection \The natural case\ locale folding_on = fixes S :: "'a set" fixes f :: "'a \ 'b \ 'b" and z :: "'b" assumes comp_fun_commute_on: "x \ S \ y \ S \ f y o f x = f x o f y" begin interpretation fold?: comp_fun_commute_on S f by standard (simp add: comp_fun_commute_on) definition F :: "'a set \ 'b" where eq_fold: "F A = Finite_Set.fold f z A" lemma empty [simp]: "F {} = z" by (simp add: eq_fold) lemma infinite [simp]: "\ finite A \ F A = z" by (simp add: eq_fold) lemma insert [simp]: assumes "insert x A \ S" and "finite A" and "x \ A" shows "F (insert x A) = f x (F A)" proof - from fold_insert assms have "Finite_Set.fold f z (insert x A) = f x (Finite_Set.fold f z A)" by simp with \finite A\ show ?thesis by (simp add: eq_fold fun_eq_iff) qed lemma remove: assumes "A \ S" and "finite A" and "x \ A" shows "F A = f x (F (A - {x}))" proof - from \x \ A\ obtain B where A: "A = insert x B" and "x \ B" by (auto dest: mk_disjoint_insert) moreover from \finite A\ A have "finite B" by simp ultimately show ?thesis using \A \ S\ by auto qed lemma insert_remove: assumes "insert x A \ S" and "finite A" shows "F (insert x A) = f x (F (A - {x}))" using assms by (cases "x \ A") (simp_all add: remove insert_absorb) end subsubsection \With idempotency\ locale folding_idem_on = folding_on + assumes comp_fun_idem_on: "x \ S \ y \ S \ f x \ f x = f x" begin declare insert [simp del] interpretation fold?: comp_fun_idem_on S f by standard (simp_all add: comp_fun_commute_on comp_fun_idem_on) lemma insert_idem [simp]: assumes "insert x A \ S" and "finite A" shows "F (insert x A) = f x (F A)" proof - from fold_insert_idem assms have "fold f z (insert x A) = f x (fold f z A)" by simp with \finite A\ show ?thesis by (simp add: eq_fold fun_eq_iff) qed end subsubsection \\<^term>\UNIV\ as the carrier set\ locale folding = fixes f :: "'a \ 'b \ 'b" and z :: "'b" assumes comp_fun_commute: "f y \ f x = f x \ f y" begin lemma (in -) folding_def': "folding f = folding_on UNIV f" unfolding folding_def folding_on_def by blast text \ Again, we abuse the \rewrites\ functionality of locales to remove trivial assumptions that result from instantiating the carrier set to \<^term>\UNIV\. \ sublocale folding_on UNIV f rewrites "\X. (X \ UNIV) \ True" and "\x. x \ UNIV \ True" and "\P. (True \ P) \ Trueprop P" and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)" proof - show "folding_on UNIV f" by standard (simp add: comp_fun_commute) qed simp_all end locale folding_idem = folding + assumes comp_fun_idem: "f x \ f x = f x" begin lemma (in -) folding_idem_def': "folding_idem f = folding_idem_on UNIV f" unfolding folding_idem_def folding_def' folding_idem_on_def unfolding folding_idem_axioms_def folding_idem_on_axioms_def by blast text \ Again, we abuse the \rewrites\ functionality of locales to remove trivial assumptions that result from instantiating the carrier set to \<^term>\UNIV\. \ sublocale folding_idem_on UNIV f rewrites "\X. (X \ UNIV) \ True" and "\x. x \ UNIV \ True" and "\P. (True \ P) \ Trueprop P" and "\P Q. (True \ PROP P \ PROP Q) \ (PROP P \ True \ PROP Q)" proof - show "folding_idem_on UNIV f" by standard (simp add: comp_fun_idem) qed simp_all end subsection \Finite cardinality\ text \ The traditional definition \<^prop>\card A \ LEAST n. \f. A = {f i |i. i < n}\ is ugly to work with. But now that we have \<^const>\fold\ things are easy: \ global_interpretation card: folding "\_. Suc" 0 defines card = "folding_on.F (\_. Suc) 0" by standard rule lemma card_insert_disjoint: "finite A \ x \ A \ card (insert x A) = Suc (card A)" by (fact card.insert) lemma card_insert_if: "finite A \ card (insert x A) = (if x \ A then card A else Suc (card A))" by auto (simp add: card.insert_remove card.remove) lemma card_ge_0_finite: "card A > 0 \ finite A" by (rule ccontr) simp lemma card_0_eq [simp]: "finite A \ card A = 0 \ A = {}" by (auto dest: mk_disjoint_insert) lemma finite_UNIV_card_ge_0: "finite (UNIV :: 'a set) \ card (UNIV :: 'a set) > 0" by (rule ccontr) simp lemma card_eq_0_iff: "card A = 0 \ A = {} \ \ finite A" by auto lemma card_range_greater_zero: "finite (range f) \ card (range f) > 0" by (rule ccontr) (simp add: card_eq_0_iff) lemma card_gt_0_iff: "0 < card A \ A \ {} \ finite A" by (simp add: neq0_conv [symmetric] card_eq_0_iff) lemma card_Suc_Diff1: assumes "finite A" "x \ A" shows "Suc (card (A - {x})) = card A" proof - have "Suc (card (A - {x})) = card (insert x (A - {x}))" using assms by (simp add: card.insert_remove) also have "... = card A" using assms by (simp add: card_insert_if) finally show ?thesis . qed lemma card_insert_le_m1: assumes "n > 0" "card y \ n - 1" shows "card (insert x y) \ n" using assms by (cases "finite y") (auto simp: card_insert_if) -lemma card_Diff_singleton: "finite A \ x \ A \ card (A - {x}) = card A - 1" - by (simp add: card_Suc_Diff1 [symmetric]) +lemma card_Diff_singleton: + assumes "x \ A" shows "card (A - {x}) = card A - 1" +proof (cases "finite A") + case True + with assms show ?thesis + by (simp add: card_Suc_Diff1 [symmetric]) +qed auto lemma card_Diff_singleton_if: - "finite A \ card (A - {x}) = (if x \ A then card A - 1 else card 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" + assumes "a \ A" and "a \ B" shows "card (A - insert a B) = card (A - B) - 1" proof - have "A - insert a B = (A - B) - {a}" using assms by blast then show ?thesis using assms by (simp add: card_Diff_singleton) qed -lemma card_insert_le: "finite A \ card A \ card (insert x A)" - by (simp add: card_insert_if) +lemma card_insert_le: "card A \ card (insert x A)" +proof (cases "finite A") + case True + then show ?thesis by (simp add: card_insert_if) +qed auto lemma card_Collect_less_nat[simp]: "card {i::nat. i < n} = n" by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq) lemma card_Collect_le_nat[simp]: "card {i::nat. i \ n} = Suc n" using card_Collect_less_nat[of "Suc n"] by (simp add: less_Suc_eq_le) lemma card_mono: assumes "finite B" and "A \ B" shows "card A \ card B" proof - from assms have "finite A" by (auto intro: finite_subset) then show ?thesis using assms proof (induct A arbitrary: B) case empty then show ?case by simp next case (insert x A) then have "x \ B" by simp from insert have "A \ B - {x}" and "finite (B - {x})" by auto with insert.hyps have "card A \ card (B - {x})" by auto with \finite A\ \x \ A\ \finite B\ \x \ B\ show ?case by simp (simp only: card.remove) qed qed lemma card_seteq: assumes "finite B" and A: "A \ B" "card B \ card A" shows "A = B" using assms proof (induction arbitrary: A rule: finite_induct) case (insert b B) then have A: "finite A" "A - {b} \ B" by force+ then have "card B \ card (A - {b})" using insert by (auto simp add: card_Diff_singleton_if) then have "A - {b} = B" using A insert.IH by auto then show ?case using insert.hyps insert.prems by auto qed auto lemma psubset_card_mono: "finite B \ A < B \ card A < card B" using card_seteq [of B A] by (auto simp add: psubset_eq) lemma card_Un_Int: assumes "finite A" "finite B" shows "card A + card B = card (A \ B) + card (A \ B)" using assms proof (induct A) case empty then show ?case by simp next case insert then show ?case by (auto simp add: insert_absorb Int_insert_left) qed lemma card_Un_disjoint: "finite A \ finite B \ A \ B = {} \ card (A \ B) = card A + card B" using card_Un_Int [of A B] by simp lemma card_Un_disjnt: "\finite A; finite B; disjnt A B\ \ card (A \ B) = card A + card B" by (simp add: card_Un_disjoint disjnt_def) lemma card_Un_le: "card (A \ B) \ card A + card B" proof (cases "finite A \ finite B") case True then show ?thesis using le_iff_add card_Un_Int [of A B] by auto qed auto lemma card_Diff_subset: assumes "finite B" and "B \ A" shows "card (A - B) = card A - card B" using assms proof (cases "finite A") case False with assms show ?thesis by simp next case True with assms show ?thesis by (induct B arbitrary: A) simp_all qed lemma card_Diff_subset_Int: assumes "finite (A \ B)" shows "card (A - B) = card A - card (A \ B)" proof - have "A - B = A - A \ B" by auto with assms show ?thesis by (simp add: card_Diff_subset) qed lemma diff_card_le_card_Diff: assumes "finite B" shows "card A - card B \ card (A - B)" proof - have "card A - card B \ card A - card (A \ B)" using card_mono[OF assms Int_lower2, of A] by arith also have "\ = card (A - B)" using assms by (simp add: card_Diff_subset_Int) finally show ?thesis . qed lemma card_le_sym_Diff: assumes "finite A" "finite B" "card A \ card B" shows "card(A - B) \ card(B - A)" proof - have "card(A - B) = card A - card (A \ B)" using assms(1,2) by(simp add: card_Diff_subset_Int) also have "\ \ card B - card (A \ B)" using assms(3) by linarith also have "\ = card(B - A)" using assms(1,2) by(simp add: card_Diff_subset_Int Int_commute) finally show ?thesis . qed lemma card_less_sym_Diff: assumes "finite A" "finite B" "card A < card B" shows "card(A - B) < card(B - A)" proof - have "card(A - B) = card A - card (A \ B)" using assms(1,2) by(simp add: card_Diff_subset_Int) also have "\ < card B - card (A \ B)" using assms(1,3) by (simp add: card_mono diff_less_mono) also have "\ = card(B - A)" using assms(1,2) by(simp add: card_Diff_subset_Int Int_commute) finally show ?thesis . qed lemma card_Diff1_less_iff: "card (A - {x}) < card A \ finite A \ x \ A" proof (cases "finite A \ x \ A") case True then show ?thesis by (auto simp: card_gt_0_iff intro: diff_less) qed auto lemma card_Diff1_less: "finite A \ x \ A \ card (A - {x}) < card A" unfolding card_Diff1_less_iff by auto lemma card_Diff2_less: assumes "finite A" "x \ A" "y \ A" shows "card (A - {x} - {y}) < card A" proof (cases "x = y") case True with assms show ?thesis by (simp add: card_Diff1_less del: card_Diff_insert) next case False then have "card (A - {x} - {y}) < card (A - {x})" "card (A - {x}) < card A" using assms by (intro card_Diff1_less; simp)+ then show ?thesis by (blast intro: less_trans) qed -lemma card_Diff1_le: "finite A \ card (A - {x}) \ card A" - by (cases "x \ A") (simp_all add: card_Diff1_less less_imp_le) +lemma card_Diff1_le: "card (A - {x}) \ card A" +proof (cases "finite A") + case True + then show ?thesis + by (cases "x \ A") (simp_all add: card_Diff1_less less_imp_le) +qed auto lemma card_psubset: "finite B \ A \ B \ card A < card B \ A < B" by (erule psubsetI) blast lemma card_le_inj: assumes fA: "finite A" and fB: "finite B" and c: "card A \ card B" shows "\f. f ` A \ B \ inj_on f A" using fA fB c proof (induct arbitrary: B rule: finite_induct) case empty then show ?case by simp next case (insert x s t) then show ?case proof (induct rule: finite_induct [OF insert.prems(1)]) case 1 then show ?case by simp next case (2 y t) from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \ card t" by simp from "2.prems"(3) [OF "2.hyps"(1) cst] obtain f where "f ` s \ t" "inj_on f s" by blast with "2.prems"(2) "2.hyps"(2) show ?case unfolding inj_on_def by (rule_tac x = "\z. if z = x then y else f z" in exI) auto qed qed lemma card_subset_eq: assumes fB: "finite B" and AB: "A \ B" and c: "card A = card B" shows "A = B" proof - from fB AB have fA: "finite A" by (auto intro: finite_subset) from fA fB have fBA: "finite (B - A)" by auto have e: "A \ (B - A) = {}" by blast have eq: "A \ (B - A) = B" using AB by blast from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0" by arith then have "B - A = {}" unfolding card_eq_0_iff using fA fB by simp with AB show "A = B" by blast qed lemma insert_partition: "x \ F \ \c1 \ insert x F. \c2 \ insert x F. c1 \ c2 \ c1 \ c2 = {} \ x \ \F = {}" - by auto (* somewhat slow *) + by auto lemma finite_psubset_induct [consumes 1, case_names psubset]: assumes finite: "finite A" and major: "\A. finite A \ (\B. B \ A \ P B) \ P A" shows "P A" using finite proof (induct A taking: card rule: measure_induct_rule) case (less A) have fin: "finite A" by fact have ih: "card B < card A \ finite B \ P B" for B by fact have "P B" if "B \ A" for B proof - from that have "card B < card A" using psubset_card_mono fin by blast moreover from that have "B \ A" by auto then have "finite B" using fin finite_subset by blast ultimately show ?thesis using ih by simp qed with fin show "P A" using major by blast qed lemma finite_induct_select [consumes 1, case_names empty select]: assumes "finite S" and "P {}" and select: "\T. T \ S \ P T \ \s\S - T. P (insert s T)" shows "P S" proof - have "0 \ card S" by simp then have "\T \ S. card T = card S \ P T" proof (induct rule: dec_induct) case base with \P {}\ show ?case by (intro exI[of _ "{}"]) auto next case (step n) then obtain T where T: "T \ S" "card T = n" "P T" by auto with \n < card S\ have "T \ S" "P T" by auto with select[of T] obtain s where "s \ S" "s \ T" "P (insert s T)" by auto with step(2) T \finite S\ show ?case by (intro exI[of _ "insert s T"]) (auto dest: finite_subset) qed with \finite S\ show "P S" by (auto dest: card_subset_eq) qed lemma remove_induct [case_names empty infinite remove]: assumes empty: "P ({} :: 'a set)" and infinite: "\ finite B \ P B" and remove: "\A. finite A \ A \ {} \ A \ B \ (\x. x \ A \ P (A - {x})) \ P A" shows "P B" proof (cases "finite B") case False then show ?thesis by (rule infinite) next case True define A where "A = B" with True have "finite A" "A \ B" by simp_all then show "P A" proof (induct "card A" arbitrary: A) case 0 then have "A = {}" by auto with empty show ?case by simp next case (Suc n A) from \A \ B\ and \finite B\ have "finite A" by (rule finite_subset) moreover from Suc.hyps have "A \ {}" by auto moreover note \A \ B\ moreover have "P (A - {x})" if x: "x \ A" for x using x Suc.prems \Suc n = card A\ by (intro Suc) auto ultimately show ?case by (rule remove) qed qed lemma finite_remove_induct [consumes 1, case_names empty remove]: fixes P :: "'a set \ bool" assumes "finite B" and "P {}" and "\A. finite A \ A \ {} \ A \ B \ (\x. x \ A \ P (A - {x})) \ P A" defines "B' \ B" shows "P B'" by (induct B' rule: remove_induct) (simp_all add: assms) text \Main cardinality theorem.\ lemma card_partition [rule_format]: "finite C \ finite (\C) \ (\c\C. card c = k) \ (\c1 \ C. \c2 \ C. c1 \ c2 \ c1 \ c2 = {}) \ k * card C = card (\C)" proof (induct rule: finite_induct) case empty then show ?case by simp next case (insert x F) then show ?case by (simp add: card_Un_disjoint insert_partition finite_subset [of _ "\(insert _ _)"]) qed lemma card_eq_UNIV_imp_eq_UNIV: assumes fin: "finite (UNIV :: 'a set)" and card: "card A = card (UNIV :: 'a set)" shows "A = (UNIV :: 'a set)" proof show "A \ UNIV" by simp show "UNIV \ A" proof show "x \ A" for x proof (rule ccontr) assume "x \ A" then have "A \ UNIV" by auto with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono) with card show False by simp qed qed qed text \The form of a finite set of given cardinality\ lemma card_eq_SucD: assumes "card A = Suc k" shows "\b B. A = insert b B \ b \ B \ card B = k \ (k = 0 \ B = {})" proof - have fin: "finite A" using assms by (auto intro: ccontr) moreover have "card A \ 0" using assms by auto ultimately obtain b where b: "b \ A" by auto show ?thesis proof (intro exI conjI) show "A = insert b (A - {b})" using b by blast show "b \ A - {b}" by blast show "card (A - {b}) = k" and "k = 0 \ A - {b} = {}" using assms b fin by (fastforce dest: mk_disjoint_insert)+ qed qed lemma card_Suc_eq: "card A = Suc k \ (\b B. A = insert b B \ b \ B \ card B = k \ (k = 0 \ B = {}))" by (auto simp: card_insert_if card_gt_0_iff elim!: card_eq_SucD) lemma card_Suc_eq_finite: "card A = Suc k \ (\b B. A = insert b B \ b \ B \ card B = k \ finite B)" unfolding card_Suc_eq using card_gt_0_iff by fastforce lemma card_1_singletonE: assumes "card A = 1" obtains x where "A = {x}" using assms by (auto simp: card_Suc_eq) lemma is_singleton_altdef: "is_singleton A \ card A = 1" unfolding is_singleton_def by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def) lemma card_1_singleton_iff: "card A = Suc 0 \ (\x. A = {x})" by (simp add: card_Suc_eq) lemma card_le_Suc0_iff_eq: assumes "finite A" shows "card A \ Suc 0 \ (\a1 \ A. \a2 \ A. a1 = a2)" (is "?C = ?A") proof assume ?C thus ?A using assms by (auto simp: le_Suc_eq dest: card_eq_SucD) next assume ?A show ?C proof cases assume "A = {}" thus ?C using \?A\ by simp next assume "A \ {}" then obtain a where "A = {a}" using \?A\ by blast thus ?C by simp qed qed lemma card_le_Suc_iff: "Suc n \ card A = (\a B. A = insert a B \ a \ B \ n \ card B \ finite B)" proof (cases "finite A") case True then show ?thesis by (fastforce simp: card_Suc_eq less_eq_nat.simps split: nat.splits) qed auto lemma finite_fun_UNIVD2: assumes fin: "finite (UNIV :: ('a \ 'b) set)" shows "finite (UNIV :: 'b set)" proof - from fin have "finite (range (\f :: 'a \ 'b. f arbitrary))" for arbitrary by (rule finite_imageI) moreover have "UNIV = range (\f :: 'a \ 'b. f arbitrary)" for arbitrary by (rule UNIV_eq_I) auto ultimately show "finite (UNIV :: 'b set)" by simp qed lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1" unfolding UNIV_unit by simp lemma infinite_arbitrarily_large: assumes "\ finite A" shows "\B. finite B \ card B = n \ B \ A" proof (induction n) case 0 show ?case by (intro exI[of _ "{}"]) auto next case (Suc n) then obtain B where B: "finite B \ card B = n \ B \ A" .. with \\ finite A\ have "A \ B" by auto with B have "B \ A" by auto then have "\x. x \ A - B" by (elim psubset_imp_ex_mem) then obtain x where x: "x \ A - B" .. with B have "finite (insert x B) \ card (insert x B) = Suc n \ insert x B \ A" by auto then show "\B. finite B \ card B = Suc n \ B \ A" .. qed text \Sometimes, to prove that a set is finite, it is convenient to work with finite subsets and to show that their cardinalities are uniformly bounded. This possibility is formalized in the next criterion.\ lemma finite_if_finite_subsets_card_bdd: assumes "\G. G \ F \ finite G \ card G \ C" shows "finite F \ card F \ C" proof (cases "finite F") case False obtain n::nat where n: "n > max C 0" by auto obtain G where G: "G \ F" "card G = n" using infinite_arbitrarily_large[OF False] by auto hence "finite G" using \n > max C 0\ using card.infinite gr_implies_not0 by blast hence False using assms G n not_less by auto thus ?thesis .. next case True thus ?thesis using assms[of F] by auto qed subsubsection \Cardinality of image\ lemma card_image_le: "finite A \ card (f ` A) \ card A" by (induct rule: finite_induct) (simp_all add: le_SucI card_insert_if) lemma card_image: "inj_on f A \ card (f ` A) = card A" proof (induct A rule: infinite_finite_induct) case (infinite A) then have "\ finite (f ` A)" by (auto dest: finite_imageD) with infinite show ?case by simp qed simp_all lemma bij_betw_same_card: "bij_betw f A B \ card A = card B" by (auto simp: card_image bij_betw_def) lemma endo_inj_surj: "finite A \ f ` A \ A \ inj_on f A \ f ` A = A" by (simp add: card_seteq card_image) lemma eq_card_imp_inj_on: assumes "finite A" "card(f ` A) = card A" shows "inj_on f A" using assms proof (induct rule:finite_induct) case empty show ?case by simp next case (insert x A) then show ?case using card_image_le [of A f] by (simp add: card_insert_if split: if_splits) qed lemma inj_on_iff_eq_card: "finite A \ inj_on f A \ card (f ` A) = card A" by (blast intro: card_image eq_card_imp_inj_on) lemma card_inj_on_le: assumes "inj_on f A" "f ` A \ B" "finite B" shows "card A \ card B" proof - have "finite A" using assms by (blast intro: finite_imageD dest: finite_subset) then show ?thesis using assms by (force intro: card_mono simp: card_image [symmetric]) qed lemma inj_on_iff_card_le: "\ finite A; finite B \ \ (\f. inj_on f A \ f ` A \ B) = (card A \ card B)" using card_inj_on_le[of _ A B] card_le_inj[of A B] by blast lemma surj_card_le: "finite A \ B \ f ` A \ card B \ card A" by (blast intro: card_image_le card_mono le_trans) lemma card_bij_eq: "inj_on f A \ f ` A \ B \ inj_on g B \ g ` B \ A \ finite A \ finite B \ card A = card B" by (auto intro: le_antisym card_inj_on_le) lemma bij_betw_finite: "bij_betw f A B \ finite A \ finite B" unfolding bij_betw_def using finite_imageD [of f A] by auto lemma inj_on_finite: "inj_on f A \ f ` A \ B \ finite B \ finite A" using finite_imageD finite_subset by blast lemma card_vimage_inj: "inj f \ A \ range f \ card (f -` A) = card A" by (auto 4 3 simp: subset_image_iff inj_vimage_image_eq intro: card_image[symmetric, OF subset_inj_on]) subsubsection \Pigeonhole Principles\ lemma pigeonhole: "card A > card (f ` A) \ \ inj_on f A " by (auto dest: card_image less_irrefl_nat) lemma pigeonhole_infinite: assumes "\ finite A" and "finite (f`A)" shows "\a0\A. \ finite {a\A. f a = f a0}" using assms(2,1) proof (induct "f`A" arbitrary: A rule: finite_induct) case empty then show ?case by simp next case (insert b F) show ?case proof (cases "finite {a\A. f a = b}") case True with \\ finite A\ have "\ finite (A - {a\A. f a = b})" by simp also have "A - {a\A. f a = b} = {a\A. f a \ b}" by blast finally have "\ finite {a\A. f a \ b}" . from insert(3)[OF _ this] insert(2,4) show ?thesis by simp (blast intro: rev_finite_subset) next case False then have "{a \ A. f a = b} \ {}" by force with False show ?thesis by blast qed qed lemma pigeonhole_infinite_rel: assumes "\ finite A" and "finite B" and "\a\A. \b\B. R a b" shows "\b\B. \ finite {a:A. R a b}" proof - let ?F = "\a. {b\B. R a b}" from finite_Pow_iff[THEN iffD2, OF \finite B\] have "finite (?F ` A)" by (blast intro: rev_finite_subset) from pigeonhole_infinite [where f = ?F, OF assms(1) this] obtain a0 where "a0 \ A" and infinite: "\ finite {a\A. ?F a = ?F a0}" .. obtain b0 where "b0 \ B" and "R a0 b0" using \a0 \ A\ assms(3) by blast have "finite {a\A. ?F a = ?F a0}" if "finite {a\A. R a b0}" using \b0 \ B\ \R a0 b0\ that by (blast intro: rev_finite_subset) with infinite \b0 \ B\ show ?thesis by blast qed subsubsection \Cardinality of sums\ lemma card_Plus: assumes "finite A" "finite B" shows "card (A <+> B) = card A + card B" proof - have "Inl`A \ Inr`B = {}" by fast with assms show ?thesis by (simp add: Plus_def card_Un_disjoint card_image) qed lemma card_Plus_conv_if: "card (A <+> B) = (if finite A \ finite B then card A + card B else 0)" by (auto simp add: card_Plus) text \Relates to equivalence classes. Based on a theorem of F. Kammüller.\ lemma dvd_partition: assumes f: "finite (\C)" and "\c\C. k dvd card c" "\c1\C. \c2\C. c1 \ c2 \ c1 \ c2 = {}" shows "k dvd card (\C)" proof - have "finite C" by (rule finite_UnionD [OF f]) then show ?thesis using assms proof (induct rule: finite_induct) case empty show ?case by simp next case (insert c C) then have "c \ \C = {}" by auto with insert show ?case by (simp add: card_Un_disjoint) qed qed subsubsection \Finite orders\ context order begin lemma finite_has_maximal: "\ finite A; A \ {} \ \ \ m \ A. \ b \ A. m \ b \ m = b" proof (induction rule: finite_psubset_induct) case (psubset A) from \A \ {}\ obtain a where "a \ A" by auto let ?B = "{b \ A. a < b}" show ?case proof cases assume "?B = {}" hence "\ b \ A. a \ b \ a = b" using le_neq_trans by blast thus ?thesis using \a \ A\ by blast next assume "?B \ {}" have "a \ ?B" by auto hence "?B \ A" using \a \ A\ by blast from psubset.IH[OF this \?B \ {}\] show ?thesis using order.strict_trans2 by blast qed qed lemma finite_has_maximal2: "\ finite A; a \ A \ \ \ m \ A. a \ m \ (\ b \ A. m \ b \ m = b)" using finite_has_maximal[of "{b \ A. a \ b}"] by fastforce lemma finite_has_minimal: "\ finite A; A \ {} \ \ \ m \ A. \ b \ A. b \ m \ m = b" proof (induction rule: finite_psubset_induct) case (psubset A) from \A \ {}\ obtain a where "a \ A" by auto let ?B = "{b \ A. b < a}" show ?case proof cases assume "?B = {}" hence "\ b \ A. b \ a \ a = b" using le_neq_trans by blast thus ?thesis using \a \ A\ by blast next assume "?B \ {}" have "a \ ?B" by auto hence "?B \ A" using \a \ A\ by blast from psubset.IH[OF this \?B \ {}\] show ?thesis using order.strict_trans1 by blast qed qed lemma finite_has_minimal2: "\ finite A; a \ A \ \ \ m \ A. m \ a \ (\ b \ A. b \ m \ m = b)" using finite_has_minimal[of "{b \ A. b \ a}"] by fastforce end subsubsection \Relating injectivity and surjectivity\ lemma finite_surj_inj: assumes "finite A" "A \ f ` A" shows "inj_on f A" proof - have "f ` A = A" by (rule card_seteq [THEN sym]) (auto simp add: assms card_image_le) then show ?thesis using assms by (simp add: eq_card_imp_inj_on) qed lemma finite_UNIV_surj_inj: "finite(UNIV:: 'a set) \ surj f \ inj f" for f :: "'a \ 'a" by (blast intro: finite_surj_inj subset_UNIV) lemma finite_UNIV_inj_surj: "finite(UNIV:: 'a set) \ inj f \ surj f" for f :: "'a \ 'a" by (fastforce simp:surj_def dest!: endo_inj_surj) lemma surjective_iff_injective_gen: assumes fS: "finite S" and fT: "finite T" and c: "card S = card T" and ST: "f ` S \ T" shows "(\y \ T. \x \ S. f x = y) \ inj_on f S" (is "?lhs \ ?rhs") proof assume h: "?lhs" { fix x y assume x: "x \ S" assume y: "y \ S" assume f: "f x = f y" from x fS have S0: "card S \ 0" by auto have "x = y" proof (rule ccontr) assume xy: "\ ?thesis" have th: "card S \ card (f ` (S - {y}))" unfolding c proof (rule card_mono) show "finite (f ` (S - {y}))" by (simp add: fS) have "\x \ y; x \ S; z \ S; f x = f y\ \ \x \ S. x \ y \ f z = f x" for z by (case_tac "z = y \ z = x") auto then show "T \ f ` (S - {y})" using h xy x y f by fastforce qed also have " \ \ card (S - {y})" by (simp add: card_image_le fS) also have "\ \ card S - 1" using y fS by simp finally show False using S0 by arith qed } then show ?rhs unfolding inj_on_def by blast next assume h: ?rhs have "f ` S = T" by (simp add: ST c card_image card_subset_eq fT h) then show ?lhs by blast qed hide_const (open) Finite_Set.fold subsection \Infinite Sets\ text \ Some elementary facts about infinite sets, mostly by Stephan Merz. Beware! Because "infinite" merely abbreviates a negation, these lemmas may not work well with \blast\. \ abbreviation infinite :: "'a set \ bool" where "infinite S \ \ finite S" text \ Infinite sets are non-empty, and if we remove some elements from an infinite set, the result is still infinite. \ lemma infinite_UNIV_nat [iff]: "infinite (UNIV :: nat set)" proof assume "finite (UNIV :: nat set)" with finite_UNIV_inj_surj [of Suc] show False by simp (blast dest: Suc_neq_Zero surjD) qed lemma infinite_UNIV_char_0: "infinite (UNIV :: 'a::semiring_char_0 set)" proof assume "finite (UNIV :: 'a set)" with subset_UNIV have "finite (range of_nat :: 'a set)" by (rule finite_subset) moreover have "inj (of_nat :: nat \ 'a)" by (simp add: inj_on_def) ultimately have "finite (UNIV :: nat set)" by (rule finite_imageD) then show False by simp qed lemma infinite_imp_nonempty: "infinite S \ S \ {}" by auto lemma infinite_remove: "infinite S \ infinite (S - {a})" by simp lemma Diff_infinite_finite: assumes "finite T" "infinite S" shows "infinite (S - T)" using \finite T\ proof induct from \infinite S\ show "infinite (S - {})" by auto next fix T x assume ih: "infinite (S - T)" have "S - (insert x T) = (S - T) - {x}" by (rule Diff_insert) with ih show "infinite (S - (insert x T))" by (simp add: infinite_remove) qed lemma Un_infinite: "infinite S \ infinite (S \ T)" by simp lemma infinite_Un: "infinite (S \ T) \ infinite S \ infinite T" by simp lemma infinite_super: assumes "S \ T" and "infinite S" shows "infinite T" proof assume "finite T" with \S \ T\ have "finite S" by (simp add: finite_subset) with \infinite S\ show False by simp qed proposition infinite_coinduct [consumes 1, case_names infinite]: assumes "X A" and step: "\A. X A \ \x\A. X (A - {x}) \ infinite (A - {x})" shows "infinite A" proof assume "finite A" then show False using \X A\ proof (induction rule: finite_psubset_induct) case (psubset A) then obtain x where "x \ A" "X (A - {x}) \ infinite (A - {x})" using local.step psubset.prems by blast then have "X (A - {x})" using psubset.hyps by blast show False proof (rule psubset.IH [where B = "A - {x}"]) show "A - {x} \ A" using \x \ A\ by blast qed fact qed qed text \ For any function with infinite domain and finite range there is some element that is the image of infinitely many domain elements. In particular, any infinite sequence of elements from a finite set contains some element that occurs infinitely often. \ lemma inf_img_fin_dom': assumes img: "finite (f ` A)" and dom: "infinite A" shows "\y \ f ` A. infinite (f -` {y} \ A)" proof (rule ccontr) have "A \ (\y\f ` A. f -` {y} \ A)" by auto moreover assume "\ ?thesis" with img have "finite (\y\f ` A. f -` {y} \ A)" by blast ultimately have "finite A" by (rule finite_subset) with dom show False by contradiction qed lemma inf_img_fin_domE': assumes "finite (f ` A)" and "infinite A" obtains y where "y \ f`A" and "infinite (f -` {y} \ A)" using assms by (blast dest: inf_img_fin_dom') lemma inf_img_fin_dom: assumes img: "finite (f`A)" and dom: "infinite A" shows "\y \ f`A. infinite (f -` {y})" using inf_img_fin_dom'[OF assms] by auto lemma inf_img_fin_domE: assumes "finite (f`A)" and "infinite A" obtains y where "y \ f`A" and "infinite (f -` {y})" using assms by (blast dest: inf_img_fin_dom) proposition finite_image_absD: "finite (abs ` S) \ finite S" for S :: "'a::linordered_ring set" by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom) subsection \The finite powerset operator\ definition Fpow :: "'a set \ 'a set set" where "Fpow A \ {X. X \ A \ finite X}" lemma Fpow_mono: "A \ B \ Fpow A \ Fpow B" unfolding Fpow_def by auto lemma empty_in_Fpow: "{} \ Fpow A" unfolding Fpow_def by auto lemma Fpow_not_empty: "Fpow A \ {}" using empty_in_Fpow by blast lemma Fpow_subset_Pow: "Fpow A \ Pow A" unfolding Fpow_def by auto lemma Fpow_Pow_finite: "Fpow A = Pow A Int {A. finite A}" unfolding Fpow_def Pow_def by blast lemma inj_on_image_Fpow: assumes "inj_on f A" shows "inj_on (image f) (Fpow A)" using assms Fpow_subset_Pow[of A] subset_inj_on[of "image f" "Pow A"] inj_on_image_Pow by blast lemma image_Fpow_mono: assumes "f ` A \ B" shows "(image f) ` (Fpow A) \ Fpow B" using assms by(unfold Fpow_def, auto) end diff --git a/src/HOL/Library/Disjoint_Sets.thy b/src/HOL/Library/Disjoint_Sets.thy --- a/src/HOL/Library/Disjoint_Sets.thy +++ b/src/HOL/Library/Disjoint_Sets.thy @@ -1,409 +1,415 @@ (* Author: Johannes Hölzl, TU München *) section \Partitions and Disjoint Sets\ theory Disjoint_Sets imports Main begin lemma range_subsetD: "range f \ B \ f i \ B" by blast lemma Int_Diff_disjoint: "A \ B \ (A - B) = {}" by blast lemma Int_Diff_Un: "A \ B \ (A - B) = A" by blast lemma mono_Un: "mono A \ (\i\n. A i) = A n" unfolding mono_def by auto lemma disjnt_equiv_class: "equiv A r \ disjnt (r``{a}) (r``{b}) \ (a, b) \ r" by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def) subsection \Set of Disjoint Sets\ abbreviation disjoint :: "'a set set \ bool" where "disjoint \ pairwise disjnt" lemma disjoint_def: "disjoint A \ (\a\A. \b\A. a \ b \ a \ b = {})" unfolding pairwise_def disjnt_def by auto lemma disjointI: "(\a b. a \ A \ b \ A \ a \ b \ a \ b = {}) \ disjoint A" unfolding disjoint_def by auto lemma disjointD: "disjoint A \ a \ A \ b \ A \ a \ b \ a \ b = {}" unfolding disjoint_def by auto lemma disjoint_image: "inj_on f (\A) \ disjoint A \ disjoint ((`) f ` A)" unfolding inj_on_def disjoint_def by blast lemma assumes "disjoint (A \ B)" shows disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B" using assms by (simp_all add: disjoint_def) lemma disjoint_INT: assumes *: "\i. i \ I \ disjoint (F i)" shows "disjoint {\i\I. X i | X. \i\I. X i \ F i}" proof (safe intro!: disjointI del: equalityI) fix A B :: "'a \ 'b set" assume "(\i\I. A i) \ (\i\I. B i)" then obtain i where "A i \ B i" "i \ I" by auto moreover assume "\i\I. A i \ F i" "\i\I. B i \ F i" ultimately show "(\i\I. A i) \ (\i\I. B i) = {}" using *[OF \i\I\, THEN disjointD, of "A i" "B i"] by (auto simp flip: INT_Int_distrib) qed lemma diff_Union_pairwise_disjoint: assumes "pairwise disjnt \" "\ \ \" shows "\\ - \\ = \(\ - \)" proof - have "False" if x: "x \ A" "x \ B" and AB: "A \ \" "A \ \" "B \ \" for x A B proof - have "A \ B = {}" using assms disjointD AB by blast with x show ?thesis by blast qed then show ?thesis by auto qed lemma Int_Union_pairwise_disjoint: assumes "pairwise disjnt (\ \ \)" shows "\\ \ \\ = \(\ \ \)" proof - have "False" if x: "x \ A" "x \ B" and AB: "A \ \" "A \ \" "B \ \" for x A B proof - have "A \ B = {}" using assms disjointD AB by blast with x show ?thesis by blast qed then show ?thesis by auto qed lemma psubset_Union_pairwise_disjoint: assumes \: "pairwise disjnt \" and "\ \ \ - {{}}" shows "\\ \ \\" unfolding psubset_eq proof show "\\ \ \\" using assms by blast have "\ \ \" "\(\ - \ \ (\ - {{}})) \ {}" using assms by blast+ then show "\\ \ \\" using diff_Union_pairwise_disjoint [OF \] by blast qed subsubsection "Family of Disjoint Sets" definition disjoint_family_on :: "('i \ 'a set) \ 'i set \ bool" where "disjoint_family_on A S \ (\m\S. \n\S. m \ n \ A m \ A n = {})" abbreviation "disjoint_family A \ disjoint_family_on A UNIV" lemma disjoint_family_elem_disjnt: assumes "infinite A" "finite C" and df: "disjoint_family_on B A" obtains x where "x \ A" "disjnt C (B x)" proof - have "False" if *: "\x \ A. \y. y \ C \ y \ B x" proof - obtain g where g: "\x \ A. g x \ C \ g x \ B x" using * by metis with df have "inj_on g A" by (fastforce simp add: inj_on_def disjoint_family_on_def) then have "infinite (g ` A)" using \infinite A\ finite_image_iff by blast then show False by (meson \finite C\ finite_subset g image_subset_iff) qed then show ?thesis by (force simp: disjnt_iff intro: that) qed lemma disjoint_family_onD: "disjoint_family_on A I \ i \ I \ j \ I \ i \ j \ A i \ A j = {}" by (auto simp: disjoint_family_on_def) lemma disjoint_family_subset: "disjoint_family A \ (\x. B x \ A x) \ disjoint_family B" by (force simp add: disjoint_family_on_def) lemma disjoint_family_on_bisimulation: assumes "disjoint_family_on f S" and "\n m. n \ S \ m \ S \ n \ m \ f n \ f m = {} \ g n \ g m = {}" shows "disjoint_family_on g S" using assms unfolding disjoint_family_on_def by auto lemma disjoint_family_on_mono: "A \ B \ disjoint_family_on f B \ disjoint_family_on f A" unfolding disjoint_family_on_def by auto lemma disjoint_family_Suc: "(\n. A n \ A (Suc n)) \ disjoint_family (\i. A (Suc i) - A i)" using lift_Suc_mono_le[of A] by (auto simp add: disjoint_family_on_def) (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le) lemma disjoint_family_on_disjoint_image: "disjoint_family_on A I \ disjoint (A ` I)" unfolding disjoint_family_on_def disjoint_def by force lemma disjoint_family_on_vimageI: "disjoint_family_on F I \ disjoint_family_on (\i. f -` F i) I" by (auto simp: disjoint_family_on_def) lemma disjoint_image_disjoint_family_on: assumes d: "disjoint (A ` I)" and i: "inj_on A I" shows "disjoint_family_on A I" unfolding disjoint_family_on_def proof (intro ballI impI) fix n m assume nm: "m \ I" "n \ I" and "n \ m" with i[THEN inj_onD, of n m] show "A n \ A m = {}" by (intro disjointD[OF d]) auto qed lemma disjoint_UN: assumes F: "\i. i \ I \ disjoint (F i)" and *: "disjoint_family_on (\i. \(F i)) I" shows "disjoint (\i\I. F i)" proof (safe intro!: disjointI del: equalityI) fix A B i j assume "A \ B" "A \ F i" "i \ I" "B \ F j" "j \ I" show "A \ B = {}" proof cases assume "i = j" with F[of i] \i \ I\ \A \ F i\ \B \ F j\ \A \ B\ show "A \ B = {}" by (auto dest: disjointD) next assume "i \ j" with * \i\I\ \j\I\ have "(\(F i)) \ (\(F j)) = {}" by (rule disjoint_family_onD) with \A\F i\ \i\I\ \B\F j\ \j\I\ show "A \ B = {}" by auto qed qed lemma distinct_list_bind: assumes "distinct xs" "\x. x \ set xs \ distinct (f x)" "disjoint_family_on (set \ f) (set xs)" shows "distinct (List.bind xs f)" using assms by (induction xs) (auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind) lemma bij_betw_UNION_disjoint: assumes disj: "disjoint_family_on A' I" assumes bij: "\i. i \ I \ bij_betw f (A i) (A' i)" shows "bij_betw f (\i\I. A i) (\i\I. A' i)" unfolding bij_betw_def proof from bij show eq: "f ` \(A ` I) = \(A' ` I)" by (auto simp: bij_betw_def image_UN) show "inj_on f (\(A ` I))" proof (rule inj_onI, clarify) fix i j x y assume A: "i \ I" "j \ I" "x \ A i" "y \ A j" and B: "f x = f y" from A bij[of i] bij[of j] have "f x \ A' i" "f y \ A' j" by (auto simp: bij_betw_def) with B have "A' i \ A' j \ {}" by auto with disj A have "i = j" unfolding disjoint_family_on_def by blast with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD) qed qed lemma disjoint_union: "disjoint C \ disjoint B \ \C \ \B = {} \ disjoint (C \ B)" using disjoint_UN[of "{C, B}" "\x. x"] by (auto simp add: disjoint_family_on_def) text \ The union of an infinite disjoint family of non-empty sets is infinite. \ lemma infinite_disjoint_family_imp_infinite_UNION: assumes "\finite A" "\x. x \ A \ f x \ {}" "disjoint_family_on f A" shows "\finite (\(f ` A))" proof - define g where "g x = (SOME y. y \ f x)" for x have g: "g x \ f x" if "x \ A" for x unfolding g_def by (rule someI_ex, insert assms(2) that) blast have inj_on_g: "inj_on g A" proof (rule inj_onI, rule ccontr) fix x y assume A: "x \ A" "y \ A" "g x = g y" "x \ y" with g[of x] g[of y] have "g x \ f x" "g x \ f y" by auto with A \x \ y\ assms show False by (auto simp: disjoint_family_on_def inj_on_def) qed from g have "g ` A \ \(f ` A)" by blast moreover from inj_on_g \\finite A\ have "\finite (g ` A)" using finite_imageD by blast ultimately show ?thesis using finite_subset by blast qed subsection \Construct Disjoint Sequences\ definition disjointed :: "(nat \ 'a set) \ nat \ 'a set" where "disjointed A n = A n - (\i\{0..i\{0..i\{0..i. disjointed A i) = (\i. A i)" by (rule UN_finite2_eq [where k=0]) (simp add: finite_UN_disjointed_eq) lemma less_disjoint_disjointed: "m < n \ disjointed A m \ disjointed A n = {}" by (auto simp add: disjointed_def) lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" by (simp add: disjoint_family_on_def) (metis neq_iff Int_commute less_disjoint_disjointed) lemma disjointed_subset: "disjointed A n \ A n" by (auto simp add: disjointed_def) lemma disjointed_0[simp]: "disjointed A 0 = A 0" by (simp add: disjointed_def) lemma disjointed_mono: "mono A \ disjointed A (Suc n) = A (Suc n) - A n" using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost) subsection \Partitions\ text \ Partitions \<^term>\P\ of a set \<^term>\A\. We explicitly disallow empty sets. \ definition partition_on :: "'a set \ 'a set set \ bool" where "partition_on A P \ \P = A \ disjoint P \ {} \ P" lemma partition_onI: "\P = A \ (\p q. p \ P \ q \ P \ p \ q \ disjnt p q) \ {} \ P \ partition_on A P" by (auto simp: partition_on_def pairwise_def) lemma partition_onD1: "partition_on A P \ A = \P" by (auto simp: partition_on_def) lemma partition_onD2: "partition_on A P \ disjoint P" by (auto simp: partition_on_def) lemma partition_onD3: "partition_on A P \ {} \ P" by (auto simp: partition_on_def) subsection \Constructions of partitions\ lemma partition_on_empty: "partition_on {} P \ P = {}" unfolding partition_on_def by fastforce lemma partition_on_space: "A \ {} \ partition_on A {A}" by (auto simp: partition_on_def disjoint_def) lemma partition_on_singletons: "partition_on A ((\x. {x}) ` A)" by (auto simp: partition_on_def disjoint_def) lemma partition_on_transform: assumes P: "partition_on A P" assumes F_UN: "\(F ` P) = F (\P)" and F_disjnt: "\p q. p \ P \ q \ P \ disjnt p q \ disjnt (F p) (F q)" shows "partition_on (F A) (F ` P - {{}})" proof - have "\(F ` P - {{}}) = F A" unfolding P[THEN partition_onD1] F_UN[symmetric] by auto with P show ?thesis by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt) qed lemma partition_on_restrict: "partition_on A P \ partition_on (B \ A) ((\) B ` P - {{}})" by (intro partition_on_transform) (auto simp: disjnt_def) lemma partition_on_vimage: "partition_on A P \ partition_on (f -` A) ((-`) f ` P - {{}})" by (intro partition_on_transform) (auto simp: disjnt_def) lemma partition_on_inj_image: assumes P: "partition_on A P" and f: "inj_on f A" shows "partition_on (f ` A) ((`) f ` P - {{}})" proof (rule partition_on_transform[OF P]) show "p \ P \ q \ P \ disjnt p q \ disjnt (f ` p) (f ` q)" for p q using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def) qed auto +lemma partition_on_insert: + assumes "disjnt p (\P)" + shows "partition_on A (insert p P) \ partition_on (A-p) P \ p \ A \ p \ {}" + using assms + by (auto simp: partition_on_def disjnt_iff pairwise_insert) + subsection \Finiteness of partitions\ lemma finitely_many_partition_on: assumes "finite A" shows "finite {P. partition_on A P}" proof (rule finite_subset) show "{P. partition_on A P} \ Pow (Pow A)" unfolding partition_on_def by auto show "finite (Pow (Pow A))" using assms by simp qed lemma finite_elements: "finite A \ partition_on A P \ finite P" using partition_onD1[of A P] by (simp add: finite_UnionD) subsection \Equivalence of partitions and equivalence classes\ lemma partition_on_quotient: assumes r: "equiv A r" shows "partition_on A (A // r)" proof (rule partition_onI) from r have "refl_on A r" by (auto elim: equivE) then show "\(A // r) = A" "{} \ A // r" by (auto simp: refl_on_def quotient_def) fix p q assume "p \ A // r" "q \ A // r" "p \ q" then obtain x y where "x \ A" "y \ A" "p = r `` {x}" "q = r `` {y}" by (auto simp: quotient_def) with r equiv_class_eq_iff[OF r, of x y] \p \ q\ show "disjnt p q" by (auto simp: disjnt_equiv_class) qed lemma equiv_partition_on: assumes P: "partition_on A P" shows "equiv A {(x, y). \p \ P. x \ p \ y \ p}" proof (rule equivI) have "A = \P" "disjoint P" "{} \ P" using P by (auto simp: partition_on_def) then show "refl_on A {(x, y). \p\P. x \ p \ y \ p}" unfolding refl_on_def by auto show "trans {(x, y). \p\P. x \ p \ y \ p}" using \disjoint P\ by (auto simp: trans_def disjoint_def) qed (auto simp: sym_def) lemma partition_on_eq_quotient: assumes P: "partition_on A P" shows "A // {(x, y). \p \ P. x \ p \ y \ p} = P" unfolding quotient_def proof safe fix x assume "x \ A" then obtain p where "p \ P" "x \ p" "\q. q \ P \ x \ q \ p = q" using P by (auto simp: partition_on_def disjoint_def) then have "{y. \p\P. x \ p \ y \ p} = p" by (safe intro!: bexI[of _ p]) simp then show "{(x, y). \p\P. x \ p \ y \ p} `` {x} \ P" by (simp add: \p \ P\) next fix p assume "p \ P" then have "p \ {}" using P by (auto simp: partition_on_def) then obtain x where "x \ p" by auto then have "x \ A" "\q. q \ P \ x \ q \ p = q" using P \p \ P\ by (auto simp: partition_on_def disjoint_def) with \p\P\ \x \ p\ have "{y. \p\P. x \ p \ y \ p} = p" by (safe intro!: bexI[of _ p]) simp then show "p \ (\x\A. {{(x, y). \p\P. x \ p \ y \ p} `` {x}})" by (auto intro: \x \ A\) qed lemma partition_on_alt: "partition_on A P \ (\r. equiv A r \ P = A // r)" by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on) end diff --git a/src/HOL/Quotient_Examples/Quotient_FSet.thy b/src/HOL/Quotient_Examples/Quotient_FSet.thy --- a/src/HOL/Quotient_Examples/Quotient_FSet.thy +++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy @@ -1,1163 +1,1158 @@ (* Title: HOL/Quotient_Examples/Quotient_FSet.thy Author: Cezary Kaliszyk, TU Munich Author: Christian Urban, TU Munich Type of finite sets. *) (******************************************************************** WARNING: There is a formalization of 'a fset as a subtype of sets in HOL/Library/FSet.thy using Lifting/Transfer. The user should use that file rather than this file unless there are some very specific reasons. *********************************************************************) theory Quotient_FSet imports "HOL-Library.Multiset" "HOL-Library.Quotient_List" begin text \ The type of finite sets is created by a quotient construction over lists. The definition of the equivalence: \ definition list_eq :: "'a list \ 'a list \ bool" (infix "\" 50) where [simp]: "xs \ ys \ set xs = set ys" lemma list_eq_reflp: "reflp list_eq" by (auto intro: reflpI) lemma list_eq_symp: "symp list_eq" by (auto intro: sympI) lemma list_eq_transp: "transp list_eq" by (auto intro: transpI) lemma list_eq_equivp: "equivp list_eq" by (auto intro: equivpI list_eq_reflp list_eq_symp list_eq_transp) text \The \fset\ type\ quotient_type 'a fset = "'a list" / "list_eq" by (rule list_eq_equivp) text \ Definitions for sublist, cardinality, intersection, difference and respectful fold over lists. \ declare List.member_def [simp] definition sub_list :: "'a list \ 'a list \ bool" where [simp]: "sub_list xs ys \ set xs \ set ys" definition card_list :: "'a list \ nat" where [simp]: "card_list xs = card (set xs)" definition inter_list :: "'a list \ 'a list \ 'a list" where [simp]: "inter_list xs ys = [x \ xs. x \ set xs \ x \ set ys]" definition diff_list :: "'a list \ 'a list \ 'a list" where [simp]: "diff_list xs ys = [x \ xs. x \ set ys]" definition rsp_fold :: "('a \ 'b \ 'b) \ bool" where "rsp_fold f \ (\u v. f u \ f v = f v \ f u)" lemma rsp_foldI: "(\u v. f u \ f v = f v \ f u) \ rsp_fold f" by (simp add: rsp_fold_def) lemma rsp_foldE: assumes "rsp_fold f" obtains "f u \ f v = f v \ f u" using assms by (simp add: rsp_fold_def) definition fold_once :: "('a \ 'b \ 'b) \ 'a list \ 'b \ 'b" where "fold_once f xs = (if rsp_fold f then fold f (remdups xs) else id)" lemma fold_once_default [simp]: "\ rsp_fold f \ fold_once f xs = id" by (simp add: fold_once_def) lemma fold_once_fold_remdups: "rsp_fold f \ fold_once f xs = fold f (remdups xs)" by (simp add: fold_once_def) section \Quotient composition lemmas\ lemma list_all2_refl': assumes q: "equivp R" shows "(list_all2 R) r r" by (rule list_all2_refl) (metis equivp_def q) lemma compose_list_refl: assumes q: "equivp R" shows "(list_all2 R OOO (\)) r r" proof have *: "r \ r" by (rule equivp_reflp[OF fset_equivp]) show "list_all2 R r r" by (rule list_all2_refl'[OF q]) with * show "((\) OO list_all2 R) r r" .. qed lemma map_list_eq_cong: "b \ ba \ map f b \ map f ba" by (simp only: list_eq_def set_map) lemma quotient_compose_list_g: assumes q: "Quotient3 R Abs Rep" and e: "equivp R" shows "Quotient3 ((list_all2 R) OOO (\)) (abs_fset \ (map Abs)) ((map Rep) \ rep_fset)" unfolding Quotient3_def comp_def proof (intro conjI allI) fix a r s show "abs_fset (map Abs (map Rep (rep_fset a))) = a" by (simp add: abs_o_rep[OF q] Quotient3_abs_rep[OF Quotient3_fset] List.map.id) have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))" by (rule list_all2_refl'[OF e]) have c: "((\) OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))" by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) show "(list_all2 R OOO (\)) (map Rep (rep_fset a)) (map Rep (rep_fset a))" by (rule, rule list_all2_refl'[OF e]) (rule c) show "(list_all2 R OOO (\)) r s = ((list_all2 R OOO (\)) r r \ (list_all2 R OOO (\)) s s \ abs_fset (map Abs r) = abs_fset (map Abs s))" proof (intro iffI conjI) show "(list_all2 R OOO (\)) r r" by (rule compose_list_refl[OF e]) show "(list_all2 R OOO (\)) s s" by (rule compose_list_refl[OF e]) next assume a: "(list_all2 R OOO (\)) r s" then have b: "map Abs r \ map Abs s" proof (elim relcomppE) fix b ba assume c: "list_all2 R r b" assume d: "b \ ba" assume e: "list_all2 R ba s" have f: "map Abs r = map Abs b" using Quotient3_rel[OF list_quotient3[OF q]] c by blast have "map Abs ba = map Abs s" using Quotient3_rel[OF list_quotient3[OF q]] e by blast then have g: "map Abs s = map Abs ba" by simp then show "map Abs r \ map Abs s" using d f map_list_eq_cong by simp qed then show "abs_fset (map Abs r) = abs_fset (map Abs s)" using Quotient3_rel[OF Quotient3_fset] by blast next assume a: "(list_all2 R OOO (\)) r r \ (list_all2 R OOO (\)) s s \ abs_fset (map Abs r) = abs_fset (map Abs s)" then have s: "(list_all2 R OOO (\)) s s" by simp have d: "map Abs r \ map Abs s" by (subst Quotient3_rel [OF Quotient3_fset, symmetric]) (simp add: a) have b: "map Rep (map Abs r) \ map Rep (map Abs s)" by (rule map_list_eq_cong[OF d]) have y: "list_all2 R (map Rep (map Abs s)) s" by (fact rep_abs_rsp_left[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of s]]) have c: "((\) OO list_all2 R) (map Rep (map Abs r)) s" by (rule relcomppI) (rule b, rule y) have z: "list_all2 R r (map Rep (map Abs r))" by (fact rep_abs_rsp[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of r]]) then show "(list_all2 R OOO (\)) r s" using a c relcomppI by simp qed qed lemma quotient_compose_list[quot_thm]: shows "Quotient3 ((list_all2 (\)) OOO (\)) (abs_fset \ (map abs_fset)) ((map rep_fset) \ rep_fset)" by (rule quotient_compose_list_g, rule Quotient3_fset, rule list_eq_equivp) section \Quotient definitions for fsets\ subsection \Finite sets are a bounded, distributive lattice with minus\ instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" begin quotient_definition "bot :: 'a fset" is "Nil :: 'a list" done abbreviation empty_fset ("{||}") where "{||} \ bot :: 'a fset" quotient_definition "less_eq_fset :: ('a fset \ 'a fset \ bool)" is "sub_list :: ('a list \ 'a list \ bool)" by simp abbreviation subset_fset :: "'a fset \ 'a fset \ bool" (infix "|\|" 50) where "xs |\| ys \ xs \ ys" definition less_fset :: "'a fset \ 'a fset \ bool" where "xs < ys \ xs \ ys \ xs \ (ys::'a fset)" abbreviation psubset_fset :: "'a fset \ 'a fset \ bool" (infix "|\|" 50) where "xs |\| ys \ xs < ys" quotient_definition "sup :: 'a fset \ 'a fset \ 'a fset" is "append :: 'a list \ 'a list \ 'a list" by simp abbreviation union_fset (infixl "|\|" 65) where "xs |\| ys \ sup xs (ys::'a fset)" quotient_definition "inf :: 'a fset \ 'a fset \ 'a fset" is "inter_list :: 'a list \ 'a list \ 'a list" by simp abbreviation inter_fset (infixl "|\|" 65) where "xs |\| ys \ inf xs (ys::'a fset)" quotient_definition "minus :: 'a fset \ 'a fset \ 'a fset" is "diff_list :: 'a list \ 'a list \ 'a list" by fastforce instance proof fix x y z :: "'a fset" show "x |\| y \ x |\| y \ \ y |\| x" by (unfold less_fset_def, descending) auto show "x |\| x" by (descending) (simp) show "{||} |\| x" by (descending) (simp) show "x |\| x |\| y" by (descending) (simp) show "y |\| x |\| y" by (descending) (simp) show "x |\| y |\| x" by (descending) (auto) show "x |\| y |\| y" by (descending) (auto) show "x |\| (y |\| z) = x |\| y |\| (x |\| z)" by (descending) (auto) next fix x y z :: "'a fset" assume a: "x |\| y" assume b: "y |\| z" show "x |\| z" using a b by (descending) (simp) next fix x y :: "'a fset" assume a: "x |\| y" assume b: "y |\| x" show "x = y" using a b by (descending) (auto) next fix x y z :: "'a fset" assume a: "y |\| x" assume b: "z |\| x" show "y |\| z |\| x" using a b by (descending) (simp) next fix x y z :: "'a fset" assume a: "x |\| y" assume b: "x |\| z" show "x |\| y |\| z" using a b by (descending) (auto) qed end subsection \Other constants for fsets\ quotient_definition "insert_fset :: 'a \ 'a fset \ 'a fset" is "Cons" by auto syntax "_insert_fset" :: "args => 'a fset" ("{|(_)|}") translations "{|x, xs|}" == "CONST insert_fset x {|xs|}" "{|x|}" == "CONST insert_fset x {||}" quotient_definition fset_member where "fset_member :: 'a fset \ 'a \ bool" is "List.member" by fastforce abbreviation in_fset :: "'a \ 'a fset \ bool" (infix "|\|" 50) where "x |\| S \ fset_member S x" abbreviation notin_fset :: "'a \ 'a fset \ bool" (infix "|\|" 50) where "x |\| S \ \ (x |\| S)" subsection \Other constants on the Quotient Type\ quotient_definition "card_fset :: 'a fset \ nat" is card_list by simp quotient_definition "map_fset :: ('a \ 'b) \ 'a fset \ 'b fset" is map by simp quotient_definition "remove_fset :: 'a \ 'a fset \ 'a fset" is removeAll by simp quotient_definition "fset :: 'a fset \ 'a set" is "set" by simp lemma fold_once_set_equiv: assumes "xs \ ys" shows "fold_once f xs = fold_once f ys" proof (cases "rsp_fold f") case False then show ?thesis by simp next case True then have "\x y. x \ set (remdups xs) \ y \ set (remdups xs) \ f x \ f y = f y \ f x" by (rule rsp_foldE) moreover from assms have "mset (remdups xs) = mset (remdups ys)" by (simp add: set_eq_iff_mset_remdups_eq) ultimately have "fold f (remdups xs) = fold f (remdups ys)" by (rule fold_multiset_equiv) with True show ?thesis by (simp add: fold_once_fold_remdups) qed quotient_definition "fold_fset :: ('a \ 'b \ 'b) \ 'a fset \ 'b \ 'b" is fold_once by (rule fold_once_set_equiv) lemma concat_rsp_pre: assumes a: "list_all2 (\) x x'" and b: "x' \ y'" and c: "list_all2 (\) y' y" and d: "\x\set x. xa \ set x" shows "\x\set y. xa \ set x" proof - obtain xb where e: "xb \ set x" and f: "xa \ set xb" using d by auto have "\y. y \ set x' \ xb \ y" by (rule list_all2_find_element[OF e a]) then obtain ya where h: "ya \ set x'" and i: "xb \ ya" by auto have "ya \ set y'" using b h by simp then have "\yb. yb \ set y \ ya \ yb" using c by (rule list_all2_find_element) then show ?thesis using f i by auto qed quotient_definition "concat_fset :: ('a fset) fset \ 'a fset" is concat proof (elim relcomppE) fix a b ba bb assume a: "list_all2 (\) a ba" with list_symp [OF list_eq_symp] have a': "list_all2 (\) ba a" by (rule sympE) assume b: "ba \ bb" with list_eq_symp have b': "bb \ ba" by (rule sympE) assume c: "list_all2 (\) bb b" with list_symp [OF list_eq_symp] have c': "list_all2 (\) b bb" by (rule sympE) have "\x. (\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof fix x show "(\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof assume d: "\xa\set a. x \ set xa" show "\xa\set b. x \ set xa" by (rule concat_rsp_pre[OF a b c d]) next assume e: "\xa\set b. x \ set xa" show "\xa\set a. x \ set xa" by (rule concat_rsp_pre[OF c' b' a' e]) qed qed then show "concat a \ concat b" by auto qed quotient_definition "filter_fset :: ('a \ bool) \ 'a fset \ 'a fset" is filter by force subsection \Compositional respectfulness and preservation lemmas\ lemma Nil_rsp2 [quot_respect]: shows "(list_all2 (\) OOO (\)) Nil Nil" by (rule compose_list_refl, rule list_eq_equivp) lemma Cons_rsp2 [quot_respect]: shows "((\) ===> list_all2 (\) OOO (\) ===> list_all2 (\) OOO (\)) Cons Cons" apply (auto intro!: rel_funI) apply (rule_tac b="x # b" in relcomppI) apply auto apply (rule_tac b="x # ba" in relcomppI) apply auto done lemma Nil_prs2 [quot_preserve]: assumes "Quotient3 R Abs Rep" shows "(Abs \ map f) [] = Abs []" by simp lemma Cons_prs2 [quot_preserve]: assumes q: "Quotient3 R1 Abs1 Rep1" and r: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> (map Rep1 \ Rep2) ---> (Abs2 \ map Abs1)) (#) = (id ---> Rep2 ---> Abs2) (#)" by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q]) lemma append_prs2 [quot_preserve]: assumes q: "Quotient3 R1 Abs1 Rep1" and r: "Quotient3 R2 Abs2 Rep2" shows "((map Rep1 \ Rep2) ---> (map Rep1 \ Rep2) ---> (Abs2 \ map Abs1)) (@) = (Rep2 ---> Rep2 ---> Abs2) (@)" by (simp add: fun_eq_iff abs_o_rep[OF q] List.map.id) lemma list_all2_app_l: assumes a: "reflp R" and b: "list_all2 R l r" shows "list_all2 R (z @ l) (z @ r)" using a b by (induct z) (auto elim: reflpE) lemma append_rsp2_pre0: assumes a:"list_all2 (\) x x'" shows "list_all2 (\) (x @ z) (x' @ z)" using a apply (induct x x' rule: list_induct2') by simp_all (rule list_all2_refl'[OF list_eq_equivp]) lemma append_rsp2_pre1: assumes a:"list_all2 (\) x x'" shows "list_all2 (\) (z @ x) (z @ x')" using a apply (induct x x' arbitrary: z rule: list_induct2') apply (rule list_all2_refl'[OF list_eq_equivp]) apply (simp_all del: list_eq_def) apply (rule list_all2_app_l) apply (simp_all add: reflpI) done lemma append_rsp2_pre: assumes "list_all2 (\) x x'" and "list_all2 (\) z z'" shows "list_all2 (\) (x @ z) (x' @ z')" using assms by (rule list_all2_appendI) lemma compositional_rsp3: assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C" shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C" by (auto intro!: rel_funI) (metis (full_types) assms rel_funE relcomppI) lemma append_rsp2 [quot_respect]: "(list_all2 (\) OOO (\) ===> list_all2 (\) OOO (\) ===> list_all2 (\) OOO (\)) append append" by (intro compositional_rsp3) (auto intro!: rel_funI simp add: append_rsp2_pre) lemma map_rsp2 [quot_respect]: "(((\) ===> (\)) ===> list_all2 (\) OOO (\) ===> list_all2 (\) OOO (\)) map map" proof (auto intro!: rel_funI) fix f f' :: "'a list \ 'b list" fix xa ya x y :: "'a list list" assume fs: "((\) ===> (\)) f f'" and x: "list_all2 (\) xa x" and xy: "set x = set y" and y: "list_all2 (\) y ya" have a: "(list_all2 (\)) (map f xa) (map f x)" using x by (induct xa x rule: list_induct2') (simp_all, metis fs rel_funE list_eq_def) have b: "set (map f x) = set (map f y)" using xy fs by (induct x y rule: list_induct2') (simp_all, metis image_insert) have c: "(list_all2 (\)) (map f y) (map f' ya)" using y fs by (induct y ya rule: list_induct2') (simp_all, metis apply_rsp' list_eq_def) show "(list_all2 (\) OOO (\)) (map f xa) (map f' ya)" by (metis a b c list_eq_def relcomppI) qed lemma map_prs2 [quot_preserve]: shows "((abs_fset ---> rep_fset) ---> (map rep_fset \ rep_fset) ---> abs_fset \ map abs_fset) map = (id ---> rep_fset ---> abs_fset) map" by (auto simp add: fun_eq_iff) (simp only: map_map[symmetric] map_prs_aux[OF Quotient3_fset Quotient3_fset]) section \Lifted theorems\ subsection \fset\ lemma fset_simps [simp]: shows "fset {||} = {}" and "fset (insert_fset x S) = insert x (fset S)" by (descending, simp)+ lemma finite_fset [simp]: shows "finite (fset S)" by (descending) (simp) lemma fset_cong: shows "fset S = fset T \ S = T" by (descending) (simp) lemma filter_fset [simp]: shows "fset (filter_fset P xs) = Collect P \ fset xs" by (descending) (auto) lemma remove_fset [simp]: shows "fset (remove_fset x xs) = fset xs - {x}" by (descending) (simp) lemma inter_fset [simp]: shows "fset (xs |\| ys) = fset xs \ fset ys" by (descending) (auto) lemma union_fset [simp]: shows "fset (xs |\| ys) = fset xs \ fset ys" by (lifting set_append) lemma minus_fset [simp]: shows "fset (xs - ys) = fset xs - fset ys" by (descending) (auto) subsection \in_fset\ lemma in_fset: shows "x |\| S \ x \ fset S" by descending simp lemma notin_fset: shows "x |\| S \ x \ fset S" by (simp add: in_fset) lemma notin_empty_fset: shows "x |\| {||}" by (simp add: in_fset) lemma fset_eq_iff: shows "S = T \ (\x. (x |\| S) = (x |\| T))" by descending auto lemma none_in_empty_fset: shows "(\x. x |\| S) \ S = {||}" by descending simp subsection \insert_fset\ lemma in_insert_fset_iff [simp]: shows "x |\| insert_fset y S \ x = y \ x |\| S" by descending simp lemma shows insert_fsetI1: "x |\| insert_fset x S" and insert_fsetI2: "x |\| S \ x |\| insert_fset y S" by simp_all lemma insert_absorb_fset [simp]: shows "x |\| S \ insert_fset x S = S" by (descending) (auto) lemma empty_not_insert_fset[simp]: shows "{||} \ insert_fset x S" and "insert_fset x S \ {||}" by (descending, simp)+ lemma insert_fset_left_comm: shows "insert_fset x (insert_fset y S) = insert_fset y (insert_fset x S)" by (descending) (auto) lemma insert_fset_left_idem: shows "insert_fset x (insert_fset x S) = insert_fset x S" by (descending) (auto) lemma singleton_fset_eq[simp]: shows "{|x|} = {|y|} \ x = y" by (descending) (auto) lemma in_fset_mdef: shows "x |\| F \ x |\| (F - {|x|}) \ F = insert_fset x (F - {|x|})" by (descending) (auto) subsection \union_fset\ lemmas [simp] = sup_bot_left[where 'a="'a fset"] sup_bot_right[where 'a="'a fset"] lemma union_insert_fset [simp]: shows "insert_fset x S |\| T = insert_fset x (S |\| T)" by (lifting append.simps(2)) lemma singleton_union_fset_left: shows "{|a|} |\| S = insert_fset a S" by simp lemma singleton_union_fset_right: shows "S |\| {|a|} = insert_fset a S" by (subst sup.commute) simp lemma in_union_fset: shows "x |\| S |\| T \ x |\| S \ x |\| T" by (descending) (simp) subsection \minus_fset\ lemma minus_in_fset: shows "x |\| (xs - ys) \ x |\| xs \ x |\| ys" by (descending) (simp) lemma minus_insert_fset: shows "insert_fset x xs - ys = (if x |\| ys then xs - ys else insert_fset x (xs - ys))" by (descending) (auto) lemma minus_insert_in_fset[simp]: shows "x |\| ys \ insert_fset x xs - ys = xs - ys" by (simp add: minus_insert_fset) lemma minus_insert_notin_fset[simp]: shows "x |\| ys \ insert_fset x xs - ys = insert_fset x (xs - ys)" by (simp add: minus_insert_fset) lemma in_minus_fset: shows "x |\| F - S \ x |\| S" unfolding in_fset minus_fset by blast lemma notin_minus_fset: shows "x |\| S \ x |\| F - S" unfolding in_fset minus_fset by blast subsection \remove_fset\ lemma in_remove_fset: shows "x |\| remove_fset y S \ x |\| S \ x \ y" by (descending) (simp) lemma notin_remove_fset: shows "x |\| remove_fset x S" by (descending) (simp) lemma notin_remove_ident_fset: shows "x |\| S \ remove_fset x S = S" by (descending) (simp) lemma remove_fset_cases: shows "S = {||} \ (\x. x |\| S \ S = insert_fset x (remove_fset x S))" by (descending) (auto simp add: insert_absorb) subsection \inter_fset\ lemma inter_empty_fset_l: shows "{||} |\| S = {||}" by simp lemma inter_empty_fset_r: shows "S |\| {||} = {||}" by simp lemma inter_insert_fset: shows "insert_fset x S |\| T = (if x |\| T then insert_fset x (S |\| T) else S |\| T)" by (descending) (auto) lemma in_inter_fset: shows "x |\| (S |\| T) \ x |\| S \ x |\| T" by (descending) (simp) subsection \subset_fset and psubset_fset\ lemma subset_fset: shows "xs |\| ys \ fset xs \ fset ys" by (descending) (simp) lemma psubset_fset: shows "xs |\| ys \ fset xs \ fset ys" unfolding less_fset_def by (descending) (auto) lemma subset_insert_fset: shows "(insert_fset x xs) |\| ys \ x |\| ys \ xs |\| ys" by (descending) (simp) lemma subset_in_fset: shows "xs |\| ys = (\x. x |\| xs \ x |\| ys)" by (descending) (auto) lemma subset_empty_fset: shows "xs |\| {||} \ xs = {||}" by (descending) (simp) lemma not_psubset_empty_fset: shows "\ xs |\| {||}" by (metis fset_simps(1) psubset_fset not_psubset_empty) subsection \map_fset\ lemma map_fset_simps [simp]: shows "map_fset f {||} = {||}" and "map_fset f (insert_fset x S) = insert_fset (f x) (map_fset f S)" by (descending, simp)+ lemma map_fset_image [simp]: shows "fset (map_fset f S) = f ` (fset S)" by (descending) (simp) lemma inj_map_fset_cong: shows "inj f \ map_fset f S = map_fset f T \ S = T" by (descending) (metis inj_vimage_image_eq list_eq_def set_map) lemma map_union_fset: shows "map_fset f (S |\| T) = map_fset f S |\| map_fset f T" by (descending) (simp) lemma in_fset_map_fset[simp]: "a |\| map_fset f X = (\b. b |\| X \ a = f b)" by descending auto subsection \card_fset\ lemma card_fset: shows "card_fset xs = card (fset xs)" by (descending) (simp) lemma card_insert_fset_iff [simp]: shows "card_fset (insert_fset x S) = (if x |\| S then card_fset S else Suc (card_fset S))" by (descending) (simp add: insert_absorb) lemma card_fset_0[simp]: shows "card_fset S = 0 \ S = {||}" by (descending) (simp) lemma card_empty_fset[simp]: shows "card_fset {||} = 0" by (simp add: card_fset) lemma card_fset_1: shows "card_fset S = 1 \ (\x. S = {|x|})" by (descending) (auto simp add: card_Suc_eq) lemma card_fset_gt_0: shows "x \ fset S \ 0 < card_fset S" by (descending) (auto simp add: card_gt_0_iff) lemma card_notin_fset: shows "(x |\| S) = (card_fset (insert_fset x S) = Suc (card_fset S))" by simp lemma card_fset_Suc: shows "card_fset S = Suc n \ \x T. x |\| T \ S = insert_fset x T \ card_fset T = n" apply(descending) apply(auto dest!: card_eq_SucD) by (metis Diff_insert_absorb set_removeAll) lemma card_remove_fset_iff [simp]: shows "card_fset (remove_fset y S) = (if y |\| S then card_fset S - 1 else card_fset S)" by (descending) (simp) lemma card_Suc_exists_in_fset: shows "card_fset S = Suc n \ \a. a |\| S" by (drule card_fset_Suc) (auto) lemma in_card_fset_not_0: shows "a |\| A \ card_fset A \ 0" by (descending) (auto) lemma card_fset_mono: shows "xs |\| ys \ card_fset xs \ card_fset ys" unfolding card_fset psubset_fset by (simp add: card_mono subset_fset) lemma card_subset_fset_eq: shows "xs |\| ys \ card_fset ys \ card_fset xs \ xs = ys" unfolding card_fset subset_fset by (auto dest: card_seteq[OF finite_fset] simp add: fset_cong) lemma psubset_card_fset_mono: shows "xs |\| ys \ card_fset xs < card_fset ys" unfolding card_fset subset_fset by (metis finite_fset psubset_fset psubset_card_mono) lemma card_union_inter_fset: shows "card_fset xs + card_fset ys = card_fset (xs |\| ys) + card_fset (xs |\| ys)" unfolding card_fset union_fset inter_fset by (rule card_Un_Int[OF finite_fset finite_fset]) lemma card_union_disjoint_fset: shows "xs |\| ys = {||} \ card_fset (xs |\| ys) = card_fset xs + card_fset ys" unfolding card_fset union_fset apply (rule card_Un_disjoint[OF finite_fset finite_fset]) by (metis inter_fset fset_simps(1)) lemma card_remove_fset_less1: shows "x |\| xs \ card_fset (remove_fset x xs) < card_fset xs" unfolding card_fset in_fset remove_fset by (rule card_Diff1_less[OF finite_fset]) lemma card_remove_fset_less2: shows "x |\| xs \ y |\| xs \ card_fset (remove_fset y (remove_fset x xs)) < card_fset xs" unfolding card_fset remove_fset in_fset by (rule card_Diff2_less[OF finite_fset]) lemma card_remove_fset_le1: shows "card_fset (remove_fset x xs) \ card_fset xs" - unfolding remove_fset card_fset - by (rule card_Diff1_le[OF finite_fset]) + by simp lemma card_psubset_fset: shows "ys |\| xs \ card_fset ys < card_fset xs \ ys |\| xs" unfolding card_fset psubset_fset subset_fset by (rule card_psubset[OF finite_fset]) lemma card_map_fset_le: shows "card_fset (map_fset f xs) \ card_fset xs" unfolding card_fset map_fset_image by (rule card_image_le[OF finite_fset]) lemma card_minus_insert_fset[simp]: assumes "a |\| A" and "a |\| B" shows "card_fset (A - insert_fset a B) = card_fset (A - B) - 1" - using assms - unfolding in_fset card_fset minus_fset - by (simp add: card_Diff_insert[OF finite_fset]) + using assms by (simp add: in_fset card_fset) lemma card_minus_subset_fset: assumes "B |\| A" shows "card_fset (A - B) = card_fset A - card_fset B" using assms - unfolding subset_fset card_fset minus_fset - by (rule card_Diff_subset[OF finite_fset]) + by (simp add: subset_fset card_fset card_Diff_subset) lemma card_minus_fset: shows "card_fset (A - B) = card_fset A - card_fset (A |\| B)" - unfolding inter_fset card_fset minus_fset - by (rule card_Diff_subset_Int) (simp) + by (simp add: card_fset card_Diff_subset_Int) subsection \concat_fset\ lemma concat_empty_fset [simp]: shows "concat_fset {||} = {||}" by descending simp lemma concat_insert_fset [simp]: shows "concat_fset (insert_fset x S) = x |\| concat_fset S" by descending simp lemma concat_union_fset [simp]: shows "concat_fset (xs |\| ys) = concat_fset xs |\| concat_fset ys" by descending simp lemma map_concat_fset: shows "map_fset f (concat_fset xs) = concat_fset (map_fset (map_fset f) xs)" by (lifting map_concat) subsection \filter_fset\ lemma subset_filter_fset: "filter_fset P xs |\| filter_fset Q xs = (\ x. x |\| xs \ P x \ Q x)" by descending auto lemma eq_filter_fset: "(filter_fset P xs = filter_fset Q xs) = (\x. x |\| xs \ P x = Q x)" by descending auto lemma psubset_filter_fset: "(\x. x |\| xs \ P x \ Q x) \ (x |\| xs & \ P x & Q x) \ filter_fset P xs |\| filter_fset Q xs" unfolding less_fset_def by (auto simp add: subset_filter_fset eq_filter_fset) subsection \fold_fset\ lemma fold_empty_fset: "fold_fset f {||} = id" by descending (simp add: fold_once_def) lemma fold_insert_fset: "fold_fset f (insert_fset a A) = (if rsp_fold f then if a |\| A then fold_fset f A else fold_fset f A \ f a else id)" by descending (simp add: fold_once_fold_remdups) lemma remdups_removeAll: "remdups (removeAll x xs) = remove1 x (remdups xs)" by (induct xs) auto lemma member_commute_fold_once: assumes "rsp_fold f" and "x \ set xs" shows "fold_once f xs = fold_once f (removeAll x xs) \ f x" proof - from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \ f x" by (auto intro!: fold_remove1_split elim: rsp_foldE) then show ?thesis using \rsp_fold f\ by (simp add: fold_once_fold_remdups remdups_removeAll) qed lemma in_commute_fold_fset: "rsp_fold f \ h |\| b \ fold_fset f b = fold_fset f (remove_fset h b) \ f h" by descending (simp add: member_commute_fold_once) subsection \Choice in fsets\ lemma fset_choice: assumes a: "\x. x |\| A \ (\y. P x y)" shows "\f. \x. x |\| A \ P x (f x)" using a apply(descending) using finite_set_choice by (auto simp add: Ball_def) section \Induction and Cases rules for fsets\ lemma fset_exhaust [case_names empty insert, cases type: fset]: assumes empty_fset_case: "S = {||} \ P" and insert_fset_case: "\x S'. S = insert_fset x S' \ P" shows "P" using assms by (lifting list.exhaust) lemma fset_induct [case_names empty insert]: assumes empty_fset_case: "P {||}" and insert_fset_case: "\x S. P S \ P (insert_fset x S)" shows "P S" using assms by (descending) (blast intro: list.induct) lemma fset_induct_stronger [case_names empty insert, induct type: fset]: assumes empty_fset_case: "P {||}" and insert_fset_case: "\x S. \x |\| S; P S\ \ P (insert_fset x S)" shows "P S" proof(induct S rule: fset_induct) case empty show "P {||}" using empty_fset_case by simp next case (insert x S) have "P S" by fact then show "P (insert_fset x S)" using insert_fset_case by (cases "x |\| S") (simp_all) qed lemma fset_card_induct: assumes empty_fset_case: "P {||}" and card_fset_Suc_case: "\S T. Suc (card_fset S) = (card_fset T) \ P S \ P T" shows "P S" proof (induct S) case empty show "P {||}" by (rule empty_fset_case) next case (insert x S) have h: "P S" by fact have "x |\| S" by fact then have "Suc (card_fset S) = card_fset (insert_fset x S)" using card_fset_Suc by auto then show "P (insert_fset x S)" using h card_fset_Suc_case by simp qed lemma fset_raw_strong_cases: obtains "xs = []" | ys x where "\ List.member ys x" and "xs \ x # ys" proof (induct xs) case Nil then show thesis by simp next case (Cons a xs) have a: "\xs = [] \ thesis; \x ys. \\ List.member ys x; xs \ x # ys\ \ thesis\ \ thesis" by (rule Cons(1)) have b: "\x' ys'. \\ List.member ys' x'; a # xs \ x' # ys'\ \ thesis" by fact have c: "xs = [] \ thesis" using b apply(simp) by (metis list.set(1) emptyE empty_subsetI) have "\x ys. \\ List.member ys x; xs \ x # ys\ \ thesis" proof - fix x :: 'a fix ys :: "'a list" assume d:"\ List.member ys x" assume e:"xs \ x # ys" show thesis proof (cases "x = a") assume h: "x = a" then have f: "\ List.member ys a" using d by simp have g: "a # xs \ a # ys" using e h by auto show thesis using b f g by simp next assume h: "x \ a" then have f: "\ List.member (a # ys) x" using d by auto have g: "a # xs \ x # (a # ys)" using e h by auto show thesis using b f g by (simp del: List.member_def) qed qed then show thesis using a c by blast qed lemma fset_strong_cases: obtains "xs = {||}" | ys x where "x |\| ys" and "xs = insert_fset x ys" by (lifting fset_raw_strong_cases) lemma fset_induct2: "P {||} {||} \ (\x xs. x |\| xs \ P (insert_fset x xs) {||}) \ (\y ys. y |\| ys \ P {||} (insert_fset y ys)) \ (\x xs y ys. \P xs ys; x |\| xs; y |\| ys\ \ P (insert_fset x xs) (insert_fset y ys)) \ P xsa ysa" apply (induct xsa arbitrary: ysa) apply (induct_tac x rule: fset_induct_stronger) apply simp_all apply (induct_tac xa rule: fset_induct_stronger) apply simp_all done text \Extensionality\ lemma fset_eqI: assumes "\x. x \ fset A \ x \ fset B" shows "A = B" using assms proof (induct A arbitrary: B) case empty then show ?case by (auto simp add: in_fset none_in_empty_fset [symmetric] sym) next case (insert x A) from insert.prems insert.hyps(1) have "\z. z \ fset A \ z \ fset (B - {|x|})" by (auto simp add: in_fset) then have A: "A = B - {|x|}" by (rule insert.hyps(2)) with insert.prems [symmetric, of x] have "x |\| B" by (simp add: in_fset) with A show ?case by (metis in_fset_mdef) qed subsection \alternate formulation with a different decomposition principle and a proof of equivalence\ inductive list_eq2 :: "'a list \ 'a list \ bool" ("_ \2 _") where "(a # b # xs) \2 (b # a # xs)" | "[] \2 []" | "xs \2 ys \ ys \2 xs" | "(a # a # xs) \2 (a # xs)" | "xs \2 ys \ (a # xs) \2 (a # ys)" | "xs1 \2 xs2 \ xs2 \2 xs3 \ xs1 \2 xs3" lemma list_eq2_refl: shows "xs \2 xs" by (induct xs) (auto intro: list_eq2.intros) lemma cons_delete_list_eq2: shows "(a # (removeAll a A)) \2 (if List.member A a then A else a # A)" apply (induct A) apply (simp add: list_eq2_refl) apply (case_tac "List.member (aa # A) a") apply (simp_all) apply (case_tac [!] "a = aa") apply (simp_all) apply (case_tac "List.member A a") apply (auto)[2] apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6)) apply (auto simp add: list_eq2_refl) done lemma member_delete_list_eq2: assumes a: "List.member r e" shows "(e # removeAll e r) \2 r" using a cons_delete_list_eq2[of e r] by simp lemma list_eq2_equiv: "(l \ r) \ (list_eq2 l r)" proof show "list_eq2 l r \ l \ r" by (induct rule: list_eq2.induct) auto next { fix n assume a: "card_list l = n" and b: "l \ r" have "l \2 r" using a b proof (induct n arbitrary: l r) case 0 have "card_list l = 0" by fact then have "\x. \ List.member l x" by auto then have z: "l = []" by auto then have "r = []" using \l \ r\ by simp then show ?case using z list_eq2_refl by simp next case (Suc m) have b: "l \ r" by fact have d: "card_list l = Suc m" by fact then have "\a. List.member l a" apply(simp) apply(drule card_eq_SucD) apply(blast) done then obtain a where e: "List.member l a" by auto then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b by auto have f: "card_list (removeAll a l) = m" using e d by (simp) have g: "removeAll a l \ removeAll a r" using remove_fset.rsp b by simp have "(removeAll a l) \2 (removeAll a r)" by (rule Suc.hyps[OF f g]) then have h: "(a # removeAll a l) \2 (a # removeAll a r)" by (rule list_eq2.intros(5)) have i: "l \2 (a # removeAll a l)" by (rule list_eq2.intros(3)[OF member_delete_list_eq2[OF e]]) have "l \2 (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h]) then show ?case using list_eq2.intros(6)[OF _ member_delete_list_eq2[OF e']] by simp qed } then show "l \ r \ l \2 r" by blast qed (* We cannot write it as "assumes .. shows" since Isabelle changes the quantifiers to schematic variables and reintroduces them in a different order *) lemma fset_eq_cases: "\a1 = a2; \a b xs. \a1 = insert_fset a (insert_fset b xs); a2 = insert_fset b (insert_fset a xs)\ \ P; \a1 = {||}; a2 = {||}\ \ P; \xs ys. \a1 = ys; a2 = xs; xs = ys\ \ P; \a xs. \a1 = insert_fset a (insert_fset a xs); a2 = insert_fset a xs\ \ P; \xs ys a. \a1 = insert_fset a xs; a2 = insert_fset a ys; xs = ys\ \ P; \xs1 xs2 xs3. \a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\ \ P\ \ P" by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]]) lemma fset_eq_induct: assumes "x1 = x2" and "\a b xs. P (insert_fset a (insert_fset b xs)) (insert_fset b (insert_fset a xs))" and "P {||} {||}" and "\xs ys. \xs = ys; P xs ys\ \ P ys xs" and "\a xs. P (insert_fset a (insert_fset a xs)) (insert_fset a xs)" and "\xs ys a. \xs = ys; P xs ys\ \ P (insert_fset a xs) (insert_fset a ys)" and "\xs1 xs2 xs3. \xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\ \ P xs1 xs3" shows "P x1 x2" using assms by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) ML \ fun dest_fsetT (Type (\<^type_name>\fset\, [T])) = T | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); \ no_notation list_eq (infix "\" 50) and list_eq2 (infix "\2" 50) end