Theory Twelvefold_Way.Twelvefold_Way_Core
section ‹Main Observations on Operations and Permutations›
theory Twelvefold_Way_Core
imports Preliminaries
begin
subsection ‹Range Multiset›
subsubsection ‹Existence of a Suitable Finite Function›
lemma obtain_function:
assumes "finite A"
assumes "size M = card A"
shows "∃f. image_mset f (mset_set A) = M"
using assms
proof (induct arbitrary: M rule: finite_induct)
case empty
from this show ?case by simp
next
case (insert x A)
from insert(1,2,4) have "size M > 0"
by (simp add: card_gt_0_iff)
from this obtain y where "y ∈# M"
using gr0_implies_Suc size_eq_Suc_imp_elem by blast
from insert(1,2,4) this have "size (M - {#y#}) = card A"
by (simp add: Diff_insert_absorb card_Diff_singleton_if insertI1 size_Diff_submset)
from insert.hyps this obtain f' where "image_mset f' (mset_set A) = M - {#y#}" by blast
from this have "image_mset (f'(x := y)) (mset_set (insert x A)) = M"
using ‹finite A› ‹x ∉ A› ‹y ∈# M› by (simp add: image_mset_fun_upd)
from this show ?case by blast
qed
lemma obtain_function_on_ext_funcset:
assumes "finite A"
assumes "size M = card A"
shows "∃f ∈ A →⇩E set_mset M. image_mset f (mset_set A) = M"
proof -
obtain f where range_eq_M: "image_mset f (mset_set A) = M"
using obtain_function ‹finite A› ‹size M = card A› by blast
let ?f = "λx. if x ∈ A then f x else undefined"
have "?f ∈ A →⇩E set_mset M"
using range_eq_M ‹finite A› by auto
moreover have "image_mset ?f (mset_set A) = M"
using range_eq_M ‹finite A› by (auto intro: multiset.map_cong0)
ultimately show ?thesis by auto
qed
subsubsection ‹Existence of Permutation›
lemma image_mset_eq_implies_bij_betw:
fixes f :: "'a1 ⇒ 'b" and f' :: "'a2 ⇒ 'b"
assumes "finite A" "finite A'"
assumes mset_eq: "image_mset f (mset_set A) = image_mset f' (mset_set A')"
obtains bij where "bij_betw bij A A'" and "∀x∈A. f x = f' (bij x)"
proof -
from ‹finite A› have [simp]: "finite {a ∈ A. f a = (b::'b)}" for b by auto
from ‹finite A'› have [simp]: "finite {a ∈ A'. f' a = (b::'b)}" for b by auto
have "f ` A = f' ` A'"
proof -
have "f ` A = f ` (set_mset (mset_set A))" using ‹finite A› by simp
also have "… = f' ` (set_mset (mset_set A'))"
by (metis mset_eq multiset.set_map)
also have "… = f' ` A'" using ‹finite A'› by simp
finally show ?thesis .
qed
have "∀b∈(f ` A). ∃bij. bij_betw bij {a ∈ A. f a = b} {a ∈ A'. f' a = b}"
proof
fix b
from mset_eq have
"count (image_mset f (mset_set A)) b = count (image_mset f' (mset_set A')) b" by simp
from this have "card {a ∈ A. f a = b} = card {a ∈ A'. f' a = b}"
using ‹finite A› ‹finite A'›
by (simp add: count_image_mset_eq_card_vimage)
from this show "∃bij. bij_betw bij {a ∈ A. f a = b} {a ∈ A'. f' a = b}"
by (intro finite_same_card_bij) simp_all
qed
from bchoice [OF this]
obtain bij where bij: "∀b∈f ` A. bij_betw (bij b) {a ∈ A. f a = b} {a ∈ A'. f' a = b}"
by auto
define bij' where "bij' = (λa. bij (f a) a)"
have "bij_betw bij' A A'"
proof -
have "disjoint_family_on (λi. {a ∈ A'. f' a = i}) (f ` A)"
unfolding disjoint_family_on_def by auto
moreover have "bij_betw (λa. bij (f a) a) {a ∈ A. f a = b} {a ∈ A'. f' a = b}" if b: "b ∈ f ` A" for b
using bij b by (subst bij_betw_cong[where g="bij b"]) auto
ultimately have "bij_betw (λa. bij (f a) a) (⋃b∈f ` A. {a ∈ A. f a = b}) (⋃b∈f ` A. {a ∈ A'. f' a = b})"
by (rule bij_betw_UNION_disjoint)
moreover have "(⋃b∈f ` A. {a ∈ A. f a = b}) = A" by auto
moreover have "(⋃b∈f ` A. {a ∈ A'. f' a = b}) = A'" using ‹f ` A = f' ` A'› by auto
ultimately show "bij_betw bij' A A'"
unfolding bij'_def by (subst bij_betw_cong[where g="(λa. bij (f a) a)"]) auto
qed
moreover from bij have "∀x∈A. f x = f' (bij' x)"
unfolding bij'_def using bij_betwE by fastforce
ultimately show ?thesis by (rule that)
qed
lemma image_mset_eq_implies_permutes:
fixes f :: "'a ⇒ 'b"
assumes "finite A"
assumes mset_eq: "image_mset f (mset_set A) = image_mset f' (mset_set A)"
obtains p where "p permutes A" and "∀x∈A. f x = f' (p x)"
proof -
from assms obtain b where "bij_betw b A A" and "∀x∈A. f x = f' (b x)"
using image_mset_eq_implies_bij_betw by blast
define p where "p = (λa. if a ∈ A then b a else a)"
have "p permutes A"
proof (rule bij_imp_permutes)
show "bij_betw p A A"
unfolding p_def by (simp add: ‹bij_betw b A A› bij_betw_cong)
next
fix x
assume "x ∉ A"
from this show "p x = x"
unfolding p_def by simp
qed
moreover from ‹∀x∈A. f x = f' (b x)› have "∀x∈A. f x = f' (p x)"
unfolding p_def by simp
ultimately show ?thesis by (rule that)
qed
subsection ‹Domain Partition›
subsubsection ‹Existence of a Suitable Finite Function›
lemma obtain_function_with_partition:
assumes "finite A" "finite B"
assumes "partition_on A P"
assumes "card P ≤ card B"
shows "∃f ∈ A →⇩E B. (λb. {x ∈ A. f x = b}) ` B - {{}} = P"
proof -
obtain g' where "bij_betw g' P (g' ` P)" and "g' ` P ⊆ B"
by (meson assms card_le_inj finite_elements inj_on_imp_bij_betw)
define f where "⋀a. f a = (if a ∈ A then g' (THE X. a ∈ X ∧ X ∈ P) else undefined)"
have "f ∈ A →⇩E B"
unfolding f_def
using ‹g' ` P ⊆ B› assms(3) partition_on_the_part_mem by fastforce
moreover have "(λb. {x ∈ A. f x = b}) ` B - {{}} = P"
proof
show "(λb. {x ∈ A. f x = b}) ` B - {{}} ⊆ P"
proof
fix X
assume X:"X ∈ (λb. {x ∈ A. f x = b}) ` B - {{}}"
from this obtain b where "b ∈ B" and "X = {x' ∈ A. f x' = b}" by auto
from this X obtain a where "a ∈ A" and "a ∈ X" and "f a = b" by blast
have "(THE X. a ∈ X ∧ X ∈ P) ∈ P"
using ‹a ∈ A› ‹partition_on A P› by (simp add: partition_on_the_part_mem)
from ‹X = {x' ∈ A. f x' = b}› have X_eq1: "X = {x' ∈ A. g' (THE X. x' ∈ X ∧ X ∈ P) = b}"
unfolding f_def by auto
also have "… = {x' ∈ A. (THE X. x' ∈ X ∧ X ∈ P) = inv_into P g' b}"
proof -
{
fix x'
assume "x' ∈ A"
have "(THE X. x' ∈ X ∧ X ∈ P) ∈ P"
using ‹partition_on A P› ‹x' ∈ A› by (simp add: partition_on_the_part_mem)
from X_eq1 ‹a ∈ X› have "g' (THE X. a ∈ X ∧ X ∈ P) = b"
unfolding f_def by auto
from this ‹(THE X. a ∈ X ∧ X ∈ P) ∈ P› have "b ∈ g' ` P" by auto
have "(g' (THE X. x' ∈ X ∧ X ∈ P) = b) ⟷ ((THE X. x' ∈ X ∧ X ∈ P) = inv_into P g' b)"
proof -
from ‹(THE X. x' ∈ X ∧ X ∈ P) ∈ P›
have "(g' (THE X. x' ∈ X ∧ X ∈ P) = b) ⟷ (inv_into P g' (g' (THE X. x' ∈ X ∧ X ∈ P)) = inv_into P g' b)"
using ‹b ∈ g' ` P› by (auto intro: inv_into_injective)
moreover have "inv_into P g' (g' (THE X. x' ∈ X ∧ X ∈ P)) = (THE X. x' ∈ X ∧ X ∈ P)"
using ‹bij_betw g' P (g' ` P)› ‹(THE X. x' ∈ X ∧ X ∈ P) ∈ P›
by (simp add: bij_betw_inv_into_left)
ultimately show ?thesis by simp
qed
}
from this show ?thesis by auto
qed
finally have X_eq: "X = {x' ∈ A. (THE X. x' ∈ X ∧ X ∈ P) = inv_into P g' b}" .
moreover have "inv_into P g' b ∈ P"
proof -
from X_eq have eq: "inv_into P g' b = (THE X. a ∈ X ∧ X ∈ P)"
using ‹a ∈ X› ‹a ∈ A› by auto
from this show ?thesis
using ‹(THE X. a ∈ X ∧ X ∈ P) ∈ P› by simp
qed
ultimately have "X = inv_into P g' b"
using partition_on_all_in_part_eq_part[OF ‹partition_on A P›] by blast
from this ‹inv_into P g' b ∈ P› show "X ∈ P" by blast
qed
next
show "P ⊆ (λb. {x ∈ A. f x = b}) ` B - {{}}"
proof
fix X
assume "X ∈ P"
from assms(3) this have "X ≠ {}"
by (auto elim: partition_onE)
moreover have "X ∈ (λb. {x ∈ A. f x = b}) ` B"
proof
show "g' X ∈ B"
using ‹X ∈ P› ‹g' ` P ⊆ B› by blast
show "X = {x ∈ A. f x = g' X}"
proof
show "X ⊆ {x ∈ A. f x = g' X}"
proof
fix x
assume "x ∈ X"
from this have "x ∈ A"
using ‹X ∈ P› assms(3) by (fastforce elim: partition_onE)
have "(THE X. x ∈ X ∧ X ∈ P) = X"
using ‹X ∈ P› ‹x ∈ X› assms(3) partition_on_the_part_eq by fastforce
from this ‹x ∈ A› have "f x = g' X"
unfolding f_def by auto
from this ‹x ∈ A› show "x ∈ {x ∈ A. f x = g' X}" by auto
qed
next
show "{x ∈ A. f x = g' X} ⊆ X"
proof
fix x
assume "x ∈ {x ∈ A. f x = g' X}"
from this have "x ∈ A" and g_eq: "g' (THE X. x ∈ X ∧ X ∈ P) = g' X"
unfolding f_def by auto
from ‹x ∈ A› have "(THE X. x ∈ X ∧ X ∈ P) ∈ P"
using assms(3) by (simp add: partition_on_the_part_mem)
from this g_eq have "(THE X. x ∈ X ∧ X ∈ P) = X"
using ‹X ∈ P› ‹bij_betw g' P (g' ` P)›
by (metis bij_betw_inv_into_left)
from this ‹x ∈ A› assms(3) show "x ∈ X"
using partition_on_in_the_unique_part by fastforce
qed
qed
qed
ultimately show "X ∈ (λb. {x ∈ A. f x = b}) ` B - {{}}"
by auto
qed
qed
ultimately show ?thesis by blast
qed
subsubsection ‹Equality under Permutation Application›
lemma permutes_implies_inv_image_on_eq:
assumes "p permutes B"
shows "(λb. {x ∈ A. p (f x) = b}) ` B = (λb. {x ∈ A. f x = b}) ` B"
proof -
have "∀b ∈ B. ∀x ∈ A. p (f x) = b ⟷ f x = inv p b"
using ‹p permutes B› by (auto simp add: permutes_inverses)
from this have "(λb. {x ∈ A. p (f x) = b}) ` B = (λb. {x ∈ A. f x = inv p b}) ` B"
using image_cong by blast
also have "… = (λb. {x ∈ A. f x = b}) ` inv p ` B"
by (auto simp add: image_comp)
also have "… = (λb. {x ∈ A. f x = b}) ` B"
by (simp add: ‹p permutes B› permutes_inv permutes_image)
finally show ?thesis .
qed
subsubsection ‹Existence of Permutation›
lemma the_elem:
assumes "f ∈ A →⇩E B" "f' ∈ A →⇩E B"
assumes partitions_eq: "(λb. {x ∈ A. f x = b}) ` B - {{}} = (λb. {x ∈ A. f' x = b}) ` B - {{}}"
assumes "x ∈ A"
shows "the_elem (f ` {xa ∈ A. f' xa = f' x}) = f x"
proof -
from ‹x ∈ A› have x: "x ∈ {x' ∈ A. f' x' = f' x}" by blast
have "f' x ∈ B"
using ‹x ∈ A› ‹f' ∈ A →⇩E B› by blast
from this have "{x' ∈ A. f' x' = f' x} ∈ (λb. {x ∈ A. f' x = b}) ` B - {{}}"
using ‹x ∈ A› by blast
from this have "{x' ∈ A. f' x' = f' x} ∈ (λb. {x ∈ A. f x = b}) ` B - {{}}"
using partitions_eq by blast
from this obtain b where eq: "{x' ∈ A. f' x' = f' x} = {x' ∈ A. f x' = b}" by blast
also from x this show "the_elem (f ` {x' ∈ A. f' x' = f' x}) = f x"
by (metis (mono_tags, lifting) empty_iff mem_Collect_eq the_elem_image_unique)
qed
lemma the_elem_eq:
assumes "f ∈ A →⇩E B"
assumes "b ∈ f ` A"
shows "the_elem (f ` {x' ∈ A. f x' = b}) = b"
proof -
from ‹b ∈ f ` A› obtain a where "a ∈ A" and "b = f a" by blast
from this show "the_elem (f ` {x' ∈ A. f x' = b}) = b"
using the_elem[OF ‹f ∈ A →⇩E B› ‹f ∈ A →⇩E B›] by simp
qed
lemma partitions_eq_implies:
assumes "f ∈ A →⇩E B" "f' ∈ A →⇩E B"
assumes partitions_eq: "(λb. {x ∈ A. f x = b}) ` B - {{}} = (λb. {x ∈ A. f' x = b}) ` B - {{}}"
assumes "x ∈ A" "x' ∈ A"
assumes "f x = f x'"
shows "f' x = f' x'"
proof -
have "f x ∈ B" and "x ∈ {a ∈ A. f a = f x}" and "x' ∈ {a ∈ A. f a = f x}"
using ‹f ∈ A →⇩E B› ‹x ∈ A› ‹x' ∈ A› ‹f x = f x'› by auto
moreover have "{a ∈ A. f a = f x} ∈ (λb. {x ∈ A. f x = b}) ` B - {{}}"
using ‹f x ∈ B› ‹x ∈ {a ∈ A. f a = f x}› by auto
ultimately obtain b where "x ∈ {a ∈ A. f' a = b}" and "x' ∈ {a ∈ A. f' a = b}"
using partitions_eq by (metis (no_types, lifting) Diff_iff imageE)
from this show "f' x = f' x'" by auto
qed
lemma card_domain_partitions:
assumes "f ∈ A →⇩E B"
assumes "finite B"
shows "card ((λb. {x ∈ A. f x = b}) ` B - {{}}) = card (f ` A)"
proof -
note [simp] = the_elem_eq[OF ‹f ∈ A →⇩E B›]
have "bij_betw (λX. the_elem (f ` X)) ((λb. {x ∈ A. f x = b}) ` B - {{}}) (f ` A)"
proof (rule bij_betw_imageI)
show "inj_on (λX. the_elem (f ` X)) ((λb. {x ∈ A. f x = b}) ` B - {{}})"
proof (rule inj_onI)
fix X X'
assume X: "X ∈ (λb. {x ∈ A. f x = b}) ` B - {{}}"
assume X': "X' ∈ (λb. {x ∈ A. f x = b}) ` B - {{}}"
assume eq: "the_elem (f ` X) = the_elem (f ` X')"
from X obtain b where "b ∈ B" and X_eq: "X = {x ∈ A. f x = b}" by blast
from X this have "b ∈ f ` A"
using Collect_empty_eq Diff_iff image_iff insertCI by auto
from X' obtain b' where "b' ∈ B" and X'_eq: "X' = {x ∈ A. f x = b'}" by blast
from X' this have "b' ∈ f ` A"
using Collect_empty_eq Diff_iff image_iff insertCI by auto
from X_eq X'_eq eq ‹⋀b. b ∈ f ` A ⟹ the_elem (f ` {x' ∈ A. f x' = b}) = b› ‹b ∈ f ` A› ‹b' ∈ f ` A›
have "b = b'" by auto
from this show "X = X'"
using X_eq X'_eq by simp
qed
show "(λX. the_elem (f ` X)) ` ((λb. {x ∈ A. f x = b}) ` B - {{}}) = f ` A"
proof
show "(λX. the_elem (f ` X)) ` ((λb. {x ∈ A. f x = b}) ` B - {{}}) ⊆ f ` A"
using ‹⋀b. b ∈ f ` A ⟹ the_elem (f ` {x' ∈ A. f x' = b}) = b› by auto
next
show "f ` A ⊆ (λX. the_elem (f ` X)) ` ((λb. {x ∈ A. f x = b}) ` B - {{}})"
proof
fix b
assume "b ∈ f ` A"
from this have "b = the_elem (f ` {x ∈ A. f x = b})"
using ‹⋀b. b ∈ f ` A ⟹ the_elem (f ` {x' ∈ A. f x' = b}) = b› by auto
moreover from ‹b ∈ f ` A› have " {x ∈ A. f x = b} ∈ (λb. {x ∈ A. f x = b}) ` B - {{}}"
using ‹f ∈ A →⇩E B› by auto
ultimately show "b ∈ (λX. the_elem (f ` X)) ` ((λb. {x ∈ A. f x = b}) ` B - {{}})" ..
qed
qed
qed
from this show ?thesis by (rule bij_betw_same_card)
qed
lemma partitions_eq_implies_permutes:
assumes "f ∈ A →⇩E B" "f' ∈ A →⇩E B"
assumes "finite B"
assumes partitions_eq: "(λb. {x ∈ A. f x = b}) ` B - {{}} = (λb. {x ∈ A. f' x = b}) ` B - {{}}"
shows "∃p. p permutes B ∧ (∀x∈A. f x = p (f' x))"
proof -
have card_eq: "card (f' ` A) = card (f ` A)"
using card_domain_partitions[OF ‹f ∈ A →⇩E B› ‹finite B›]
using card_domain_partitions[OF ‹f' ∈ A →⇩E B› ‹finite B›]
using partitions_eq by simp
have "f' ` A ⊆ B" "f ` A ⊆ B"
using ‹f ∈ A →⇩E B› ‹f' ∈ A →⇩E B› by auto
from this card_eq have "card (B - f' ` A) = card (B - f ` A)"
using ‹finite B› by (auto simp add: card_Diff_subset finite_subset)
from this obtain p' where "bij_betw p' (B - f' ` A) (B - f ` A)"
using ‹finite B› by (metis finite_same_card_bij finite_Diff)
from this have "p' ` (B - f' ` A) = (B - f ` A)"
by (simp add: bij_betw_imp_surj_on)
define p where "⋀b. p b = (if b ∈ B then
(if b ∈ f' ` A then the_elem (f ` {x ∈ A. f' x = b}) else p' b) else b)"
have "∀x∈A. f x = p (f' x)"
proof
fix x
assume "x ∈ A"
from this partitions_eq have "the_elem (f ` {xa ∈ A. f' xa = f' x}) = f x"
using the_elem[OF ‹f ∈ A →⇩E B› ‹f' ∈ A →⇩E B›] by auto
from this show "f x = p (f' x)"
using ‹x ∈ A› p_def ‹f' ∈ A →⇩E B› by auto
qed
moreover have "p permutes B"
proof (rule bij_imp_permutes)
let ?invp = "λb. if b ∈ f ` A then the_elem (f' ` {x ∈ A. f x = b}) else b"
note [simp] = the_elem[OF ‹f ∈ A →⇩E B› ‹f' ∈ A →⇩E B› partitions_eq]
show "bij_betw p B B"
proof (rule bij_betw_imageI)
show "p ` B = B"
proof
have "(λb. the_elem (f ` {x ∈ A. f' x = b})) ` (f' ` A) ⊆ B"
using ‹f ∈ A →⇩E B› by auto
from ‹p' ` (B - f' ` A) = (B - f ` A)› this show "p ` B ⊆ B"
unfolding p_def ‹f ∈ A →⇩E B› by force
next
show "B ⊆ p ` B"
proof
fix b
assume "b ∈ B"
show "b ∈ p ` B"
proof (cases "b ∈ f ` A")
assume "b ∉ f ` A"
note ‹p' ` (B - f' ` A) = (B - f ` A)›
from this ‹b ∈ B› ‹b ∉ f ` A› show ?thesis
unfolding p_def by auto
next
assume "b ∈ f ` A"
from this ‹∀x∈A. f x = p (f' x)› ‹b ∈ B› show ?thesis
using ‹f' ∈ A →⇩E B› by auto
qed
qed
qed
next
show "inj_on p B"
proof (rule inj_onI)
fix b b'
assume "b ∈ B" "b' ∈ B" "p b = p b'"
have "b ∈ f' ` A ⟷ b' ∈ f' ` A"
proof -
have "b ∈ f' ` A ⟷ p b ∈ f ` A"
unfolding p_def using ‹b ∈ B› ‹p' ` (B - f' ` A) = B - f ` A› by auto
also have "p b ∈ f ` A ⟷ p b' ∈ f ` A"
using ‹p b = p b'› by simp
also have "p b' ∈ f ` A ⟷ b' ∈ f' ` A"
unfolding p_def using ‹b' ∈ B› ‹p' ` (B - f' ` A) = B - f ` A› by auto
finally show ?thesis .
qed
from this have "(b ∈ f' ` A ∧ b' ∈ f' ` A) ∨ (b ∉ f' ` A ∧ b' ∉ f' ` A)" by blast
from this show "b = b'"
proof
assume "b ∈ f' ` A ∧ b' ∈ f' ` A"
from this obtain a a' where "a ∈ A" "b = f' a" and "a' ∈ A" "b' = f' a'" by auto
from this ‹b ∈ B› ‹b' ∈ B› have "p b = f a" "p b' = f a'"
unfolding p_def by auto
from this ‹p b = p b'› have "f a = f a'" by simp
from this have "f' a = f' a'"
using partitions_eq_implies[OF ‹f ∈ A →⇩E B› ‹f' ∈ A →⇩E B› partitions_eq]
using ‹a ∈ A› ‹a' ∈ A› by blast
from this show "b = b'"
using ‹b' = f' a'› ‹b = f' a› by simp
next
assume "b ∉ f' ` A ∧ b' ∉ f' ` A"
from this ‹b ∈ B› ‹b' ∈ B› have "p b' = p' b'" "p b = p' b"
unfolding p_def by auto
from this ‹p b = p b'› have "p' b = p' b'" by simp
moreover have "b ∈ B - f' ` A" "b' ∈ B - f' ` A"
using ‹b ∈ B› ‹b' ∈ B› ‹b ∉ f' ` A ∧ b' ∉ f' ` A› by auto
ultimately show "b = b'"
using ‹bij_betw p' _ _› by (metis bij_betw_inv_into_left)
qed
qed
qed
next
fix x
assume "x ∉ B"
from this show "p x = x"
using ‹f' ∈ A →⇩E B› p_def by auto
qed
ultimately show ?thesis by blast
qed
subsection ‹Number Partition of Range›
subsubsection ‹Existence of a Suitable Finite Function›
lemma obtain_partition:
assumes "finite A"
assumes "number_partition (card A) N"
shows "∃P. partition_on A P ∧ image_mset card (mset_set P) = N"
using assms
proof (induct N arbitrary: A)
case empty
from this have "A = {}"
unfolding number_partition_def by auto
from this have "partition_on A {}" by (simp add: partition_on_empty)
moreover have "image_mset card (mset_set {}) = {#}" by simp
ultimately show ?case by blast
next
case (add x N)
from add.prems(2) have "0 ∉# add_mset x N" and "sum_mset (add_mset x N) = card A"
unfolding number_partition_def by auto
from this have "x ≤ card A" by auto
from this obtain X where "X ⊆ A" and "card X = x"
using subset_with_given_card_exists by auto
from this have "X ≠ {}"
using ‹0 ∉# add_mset x N› ‹finite A› by auto
have "sum_mset N = card (A - X)"
using ‹sum_mset (add_mset x N) = card A› ‹card X = x› ‹X ⊆ A›
by (metis add.commute add.prems(1) add_diff_cancel_right' card_Diff_subset infinite_super sum_mset.add_mset)
from this ‹0 ∉# add_mset x N› have "number_partition (card (A - X)) N"
unfolding number_partition_def by auto
from this obtain P where "partition_on (A - X) P" and eq_N: "image_mset card (mset_set P) = N"
using add.hyps ‹finite A› by auto
from ‹partition_on (A - X) P› have "finite P"
using ‹finite A› finite_elements by blast
from ‹partition_on (A - X) P› have "X ∉ P"
using ‹X ≠ {}› partition_onD1 by fastforce
have "partition_on A (insert X P)"
using ‹partition_on (A - X) P› ‹X ⊆ A› ‹X ≠ {}›
by (rule partition_on_insert')
moreover have "image_mset card (mset_set (insert X P)) = add_mset x N"
using eq_N ‹card X = x› ‹finite P› ‹X ∉ P› by simp
ultimately show ?case by blast
qed
lemma obtain_extensional_function_from_number_partition:
assumes "finite A" "finite B"
assumes "number_partition (card A) N"
assumes "size N ≤ card B"
shows "∃f∈A →⇩E B. image_mset (λX. card X) (mset_set (((λb. {x ∈ A. f x = b})) ` B - {{}})) = N"
proof -
obtain P where "partition_on A P" and eq_N: "image_mset card (mset_set P) = N"
using assms obtain_partition by blast
from eq_N[symmetric] ‹size N ≤ card B› have "card P ≤ card B" by simp
from ‹partition_on A P› this obtain f where "f ∈ A →⇩E B"
and eq_P: "(λb. {x ∈ A. f x = b}) ` B - {{}} = P"
using obtain_function_with_partition[OF ‹finite A› ‹finite B›] by blast
have "image_mset (λX. card X) (mset_set (((λb. {x ∈ A. f x = b})) ` B - {{}})) = N"
using eq_P eq_N by simp
from this ‹f ∈ A →⇩E B› show ?thesis by auto
qed
subsubsection ‹Equality under Permutation Application›
lemma permutes_implies_multiset_of_partition_cards_eq:
assumes "p⇩A permutes A" "p⇩B permutes B"
shows "image_mset card (mset_set ((λb. {x ∈ A. p⇩B (f' (p⇩A x)) = b}) ` B - {{}})) = image_mset card (mset_set ((λb. {x ∈ A. f' x = b}) ` B - {{}}))"
proof -
have "inj_on ((`) (inv p⇩A)) ((λb. {x ∈ A. f' x = b}) ` B - {{}})"
by (meson ‹p⇩A permutes A› inj_image_eq_iff inj_onI permutes_surj surj_imp_inj_inv)
have "image_mset card (mset_set ((λb. {x ∈ A. p⇩B (f' (p⇩A x)) = b}) ` B - {{}})) =
image_mset card (mset_set ((λX. inv p⇩A ` X) ` ((λb. {x ∈ A. f' x = b}) ` B - {{}})))"
proof -
have "(λb. {x ∈ A. p⇩B (f' (p⇩A x)) = b}) ` B - {{}} = (λb. {x ∈ A. f' (p⇩A x) = b}) ` B - {{}}"
using permutes_implies_inv_image_on_eq[OF ‹p⇩B permutes B›] by metis
also have "… = (λb. inv p⇩A ` {x ∈ A. f' x = b}) ` B - {{}}"
proof -
have "{x ∈ A. f' (p⇩A x) = b} = inv p⇩A ` {x ∈ A. f' x = b}" for b
proof
show "{x ∈ A. f' (p⇩A x) = b} ⊆ inv p⇩A ` {x ∈ A. f' x = b}"
proof
fix x
assume "x ∈ {x ∈ A. f' (p⇩A x) = b}"
from this have "x ∈ A" "f' (p⇩A x) = b" by auto
moreover from this ‹p⇩A permutes A› have "p⇩A x ∈ A" by (simp add: permutes_in_image)
moreover from ‹p⇩A permutes A› have "x = inv p⇩A (p⇩A x)"
using permutes_inverses(2) by fastforce
ultimately show "x ∈ inv p⇩A ` {x ∈ A. f' x = b}" by auto
qed
next
show "inv p⇩A ` {x ∈ A. f' x = b} ⊆ {x ∈ A. f' (p⇩A x) = b}"
proof
fix x
assume "x ∈ inv p⇩A ` {x ∈ A. f' x = b}"
from this obtain x' where x: "x = inv p⇩A x'" "x' ∈ A" "f' x' = b" by auto
from this ‹p⇩A permutes A› have "x ∈ A" by (simp add: permutes_in_image permutes_inv)
from ‹x = inv p⇩A x'› ‹f' x' = b› have "f' (p⇩A x) = b"
using ‹p⇩A permutes A› permutes_inverses(1) by fastforce
from this ‹x ∈ A› show "x ∈ {x ∈ A. f' (p⇩A x) = b}" by auto
qed
qed
from this show ?thesis by blast
qed
also have "… = (λX. inv p⇩A ` X) ` ((λb. {x ∈ A. f' x = b}) ` B - {{}})" by auto
finally show ?thesis by simp
qed
also have "… = image_mset (λX. card (inv p⇩A ` X)) (mset_set ((λb. {x ∈ A. f' x = b}) ` B - {{}}))"
using ‹inj_on ((`) (inv p⇩A)) ((λb. {x ∈ A. f' x = b}) ` B - {{}})›
by (simp only: image_mset_mset_set[symmetric] image_mset.compositionality) (meson comp_apply)
also have "… = image_mset card (mset_set ((λb. {x ∈ A. f' x = b}) ` B - {{}}))"
using ‹p⇩A permutes A› by (simp add: card_image inj_on_inv_into permutes_surj)
finally show ?thesis .
qed
subsubsection ‹Existence of Permutation›
lemma partition_implies_permutes:
assumes "finite A"
assumes "partition_on A P" "partition_on A P'"
assumes "image_mset card (mset_set P') = image_mset card (mset_set P)"
obtains p where "p permutes A" "P' = (λX. p ` X) ` P"
proof -
from ‹partition_on A P› ‹partition_on A P'› have "finite P" "finite P'"
using ‹finite A› finite_elements by blast+
from this ‹image_mset card (mset_set P') = image_mset card (mset_set P)›
obtain bij where "bij_betw bij P P'" and "∀X∈P. card X = card (bij X)"
using image_mset_eq_implies_bij_betw by metis
have "∀X∈P. ∃p'. bij_betw p' X (bij X)"
proof
fix X
assume "X ∈ P"
from this have "X ⊆ A"
using ‹partition_on A P› partition_onD1 by fastforce
from this have "finite X"
using ‹finite A› rev_finite_subset by blast
from ‹X ∈ P› have "bij X ∈ P'"
using ‹bij_betw bij P P'› bij_betwE by blast
from this have "bij X ⊆ A"
using ‹partition_on A P'› partition_onD1 by fastforce
from this have "finite (bij X)"
using ‹finite A› rev_finite_subset by blast
from ‹X ∈ P› have "card X = card (bij X)"
using ‹∀X∈P. card X = card (bij X)› by blast
from this show "∃p'. bij_betw p' X (bij X)"
using ‹finite (bij X)› ‹finite X› finite_same_card_bij by blast
qed
from this have "∃p'. ∀X∈P. bij_betw (p' X) X (bij X)" by metis
from this obtain p' where p': "∀X∈P. bij_betw (p' X) X (bij X)" ..
define p where "⋀a. p a = (if a ∈ A then p' (THE X. a ∈ X ∧ X ∈ P) a else a)"
have "p permutes A"
proof -
have "bij_betw p A A"
proof -
have "disjoint_family_on bij P"
proof
fix X X'
assume XX': "X ∈ P" "X' ∈ P" "X ≠ X'"
from this have "bij X ∈ P'" "bij X' ∈ P'"
using ‹bij_betw bij P P'› bij_betwE by blast+
moreover from XX' have "bij X ≠ bij X'"
using ‹bij_betw bij P P'› by (metis bij_betw_inv_into_left)
ultimately show "bij X ∩ bij X' = {}"
using ‹partition_on A P'› by (meson partition_onE)
qed
moreover have "bij_betw (λa. p' (THE X. a ∈ X ∧ X ∈ P) a) X (bij X)" if "X ∈ P" for X
proof -
from ‹X ∈ P› have "bij_betw (p' X) X (bij X)"
using ‹∀X∈P. bij_betw (p' X) X (bij X)› by blast
moreover from ‹X ∈ P› have "∀a∈X. (THE X. a ∈ X ∧ X ∈ P) = X"
using ‹partition_on A P› partition_on_the_part_eq by fastforce
ultimately show ?thesis by (auto intro: bij_betw_congI)
qed
ultimately have "bij_betw (λa. p' (THE X. a ∈ X ∧ X ∈ P) a) (⋃X∈P. X) (⋃X∈P. bij X)"
by (rule bij_betw_UNION_disjoint)
moreover have "(⋃X∈P. X) = A" "(⋃X∈P'. X) = A"
using ‹partition_on A P› ‹partition_on A P'› partition_onD1 by auto
moreover have "(⋃X∈P. bij X) = (⋃X∈P'. X)"
using ‹bij_betw bij P P'› bij_betw_imp_surj_on by force
ultimately have "bij_betw (λa. p' (THE X. a ∈ X ∧ X ∈ P) a) A A" by simp
moreover have "∀a ∈ A. p' (THE X. a ∈ X ∧ X ∈ P) a = p a"
unfolding p_def by auto
ultimately show ?thesis by (rule bij_betw_congI)
qed
moreover have "p x = x" if "x ∉ A" for x
using ‹x ∉ A› p_def by auto
ultimately show ?thesis by (rule bij_imp_permutes)
qed
moreover have "P' = (λX. p ` X) ` P"
proof
show "P' ⊆ (λX. p ` X) ` P"
proof
fix X
assume "X ∈ P'"
have in_P: "the_inv_into P bij X ∈ P"
using ‹X ∈ P'› ‹bij_betw bij P P'› bij_betwE bij_betw_the_inv_into by blast
have eq_X: "bij (the_inv_into P bij X) = X"
using ‹X ∈ P'› ‹bij_betw bij P P'›
by (meson f_the_inv_into_f_bij_betw)
have "X = p ` (the_inv_into P bij X)"
proof
from in_P have "the_inv_into P bij X ⊆ A"
using ‹partition_on A P› partition_onD1 by fastforce
have "(λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` the_inv_into P bij X = X"
proof
show "(λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` the_inv_into P bij X ⊆ X"
proof
fix x
assume "x ∈ (λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` the_inv_into P bij X"
from this obtain a where a_in: "a ∈ the_inv_into P bij X"
and x_eq: "x = p' (THE X. a ∈ X ∧ X ∈ P) a" by blast
have "(THE X. a ∈ X ∧ X ∈ P) = the_inv_into P bij X"
using a_in in_P ‹partition_on A P› partition_on_the_part_eq
by fastforce
from this x_eq have x_eq: "x = p' (the_inv_into P bij X) a"
by auto
from this have "x ∈ bij (the_inv_into P bij X)"
using a_in in_P bij_betwE p' by blast
from this eq_X show "x ∈ X" by blast
qed
next
show "X ⊆ (λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` the_inv_into P bij X"
proof
fix x
assume "x ∈ X"
let ?X' = "the_inv_into P bij X"
define x' where "x' = the_inv_into ?X' (p' ?X') x"
from in_P p' eq_X have bij_betw: "bij_betw (p' ?X') ?X' X" by auto
from bij_betw ‹x ∈ X› have "x' ∈ ?X'"
unfolding x'_def
using bij_betwE bij_betw_the_inv_into by blast
from this in_P have "(THE X. x' ∈ X ∧ X ∈ P) = ?X'"
using ‹partition_on A P› partition_on_the_part_eq by fastforce
from this ‹x ∈ X› have "x = p' (THE X. x' ∈ X ∧ X ∈ P) x'"
unfolding x'_def
using bij_betw f_the_inv_into_f_bij_betw by fastforce
from this ‹x' ∈ ?X'› show "x ∈ (λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` the_inv_into P bij X" ..
qed
qed
from this ‹the_inv_into P bij X ⊆ A› show "X ⊆ p ` the_inv_into P bij X"
unfolding p_def by auto
next
show "p ` the_inv_into P bij X ⊆ X"
proof
fix x
assume "x ∈ p ` the_inv_into P bij X"
from this obtain x' where "x = p x'" and "x' ∈ the_inv_into P bij X"
by auto
have "x' ∈ A"
using ‹x' ∈ the_inv_into P bij X› assms(2) in_P partition_onD1 by fastforce
have eq: "(THE X. x' ∈ X ∧ X ∈ P) = the_inv_into P bij X"
using ‹x' ∈ the_inv_into P bij X› assms(2) in_P partition_on_the_part_eq by fastforce
have p': "p' (the_inv_into P bij X) x' ∈ X"
using ‹x' ∈ the_inv_into P bij X› bij_betwE eq_X in_P p' by blast
from ‹x = p x'› ‹x' ∈ A› eq p' show "x ∈ X"
unfolding p_def by auto
qed
qed
moreover from ‹X ∈ P'› ‹bij_betw bij P P'› have "the_inv_into P bij X ∈ P"
using bij_betwE bij_betw_the_inv_into by blast
ultimately show "X ∈ (λX. p ` X) ` P" ..
qed
next
show "(λX. p ` X) ` P ⊆ P'"
proof
fix X'
assume "X' ∈ (λX. p ` X) ` P"
from this obtain X where X'_eq: "X' = p ` X" and "X ∈ P" ..
from ‹X ∈ P› have "X ⊆ A"
using assms(2) partition_onD1 by force
from ‹X ∈ P› p' have bij: "bij_betw (p' X) X (bij X)" by auto
have "p ` X ∈ P'"
proof -
from ‹X ∈ P› ‹bij_betw bij P P'› have "bij X ∈ P'"
using bij_betwE by blast
moreover have "(λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` X = bij X"
proof
show "(λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` X ⊆ bij X"
proof
fix x'
assume "x' ∈ (λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` X"
from this obtain x where "x ∈ X" and x'_eq: "x' = p' (THE X. x ∈ X ∧ X ∈ P) x" ..
from ‹X ∈ P› ‹x ∈ X› have eq_X: "(THE X. x ∈ X ∧ X ∈ P) = X"
using assms(2) partition_on_the_part_eq by fastforce
from bij ‹x ∈ X› x'_eq eq_X show "x' ∈ bij X"
using bij_betwE by blast
qed
next
show "bij X ⊆ (λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` X"
proof
fix x'
assume "x' ∈ bij X"
let ?x = "inv_into X (p' X) x'"
from ‹x' ∈ bij X› bij have "?x ∈ X"
by (metis bij_betw_imp_surj_on inv_into_into)
from this ‹X ∈ P› have "(THE X. ?x ∈ X ∧ X ∈ P) = X"
using assms(2) partition_on_the_part_eq by fastforce
from this ‹x' ∈ bij X› bij have "x' = p' (THE X. ?x ∈ X ∧ X ∈ P) ?x"
using bij_betw_inv_into_right by fastforce
moreover from ‹x' ∈ bij X› bij have "?x ∈ X"
by (metis bij_betw_imp_surj_on inv_into_into)
ultimately show "x' ∈ (λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` X" ..
qed
qed
ultimately have "(λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` X ∈ P'" by simp
have "(λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` X = (λa. if a ∈ A then p' (THE X. a ∈ X ∧ X ∈ P) a else a) ` X "
using ‹X ⊆ A› by (auto intro: image_cong)
from this show ?thesis
using ‹(λa. p' (THE X. a ∈ X ∧ X ∈ P) a) ` X ∈ P'› unfolding p_def by auto
qed
from this X'_eq show "X' ∈ P'" by simp
qed
qed
ultimately show thesis using that by blast
qed
lemma permutes_domain_partition_eq:
assumes "f ∈ A → B"
assumes "p⇩A permutes A"
assumes "b ∈ B"
shows "p⇩A ` {x ∈ A. f x = b} = {x ∈ A. f (inv p⇩A x) = b}"
proof
show "p⇩A ` {x ∈ A. f x = b} ⊆ {x ∈ A. f (inv p⇩A x) = b}"
using ‹p⇩A permutes A› permutes_in_image permutes_inverses(2) by fastforce
next
show "{x ∈ A. f (inv p⇩A x) = b} ⊆ p⇩A ` {x ∈ A. f x = b}"
proof
fix x
assume "x ∈ {x ∈ A. f (inv p⇩A x) = b}"
from this have "x ∈ A" "f (inv p⇩A x) = b" by auto
from ‹x ∈ A› have "x = p⇩A (inv p⇩A x)"
using ‹p⇩A permutes A› permutes_inverses(1) by fastforce
moreover from ‹f (inv p⇩A x) = b› ‹x ∈ A› have "inv p⇩A x ∈ {x ∈ A. f x = b}"
by (simp add: ‹p⇩A permutes A› permutes_in_image permutes_inv)
ultimately show "x ∈ p⇩A ` {x ∈ A. f x = b}" ..
qed
qed
lemma image_domain_partition_eq:
assumes "f ∈ A →⇩E B"
assumes "p⇩A permutes A"
shows "(λX. p⇩A ` X) ` ((λb. {x ∈ A. f x = b}) ` B) = (λb. {x ∈ A. f (inv p⇩A x) = b}) ` B"
proof
from ‹f ∈ A →⇩E B› have "f ∈ A → B" by auto
note eq = permutes_domain_partition_eq[OF ‹f ∈ A → B› ‹p⇩A permutes A›]
show "(λX. p⇩A ` X) ` (λb. {x ∈ A. f x = b}) ` B ⊆ (λb. {x ∈ A. f (inv p⇩A x) = b}) ` B"
proof
fix X
assume "X ∈ (λX. p⇩A ` X) ` (λb. {x ∈ A. f x = b}) ` B"
from this obtain b where "b ∈ B" and X_eq: "X = p⇩A ` {x ∈ A. f x = b}" by auto
from this eq have "X = {x ∈ A. f (inv p⇩A x) = b}" by simp
from this ‹b ∈ B› show "X ∈ (λb. {x ∈ A. f (inv p⇩A x) = b}) ` B" ..
qed
next
from ‹f ∈ A →⇩E B› have "f ∈ A → B" by auto
note eq = permutes_domain_partition_eq[OF ‹f ∈ A → B› ‹p⇩A permutes A›, symmetric]
show "(λb. {x ∈ A. f (inv p⇩A x) = b}) ` B ⊆ (λX. p⇩A ` X) ` (λb. {x ∈ A. f x = b}) ` B"
proof
fix X
assume "X ∈ (λb. {x ∈ A. f (inv p⇩A x) = b}) ` B"
from this obtain b where "b ∈ B" and X_eq: "X = {x ∈ A. f (inv p⇩A x) = b}" by auto
from this eq have "X = p⇩A ` {x ∈ A. f x = b}" by simp
from this ‹b ∈ B› show "X ∈ (λX. p⇩A ` X) ` (λb. {x ∈ A. f x = b}) ` B" by auto
qed
qed
lemma multiset_of_partition_cards_eq_implies_permutes:
assumes "finite A" "finite B" "f ∈ A →⇩E B" "f' ∈ A →⇩E B"
assumes eq: "image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}})) = image_mset card (mset_set ((λb. {x ∈ A. f' x = b}) ` B - {{}}))"
obtains p⇩A p⇩B where "p⇩A permutes A" "p⇩B permutes B" "∀x∈A. f x = p⇩B (f' (p⇩A x))"
proof -
have "partition_on A ((λb. {x ∈ A. f x = b}) ` B - {{}})"
using ‹f ∈ A →⇩E B› by (auto intro!: partition_onI)
moreover have "partition_on A ((λb. {x ∈ A. f' x = b}) ` B - {{}})"
using ‹f' ∈ A →⇩E B› by (auto intro!: partition_onI)
moreover note partition_implies_permutes[OF ‹finite A› _ _ eq]
ultimately obtain p⇩A where "p⇩A permutes A" and
inv_image_eq: "(λb. {x ∈ A. f x = b}) ` B - {{}} =
(`) p⇩A ` ((λb. {x ∈ A. f' x = b}) ` B - {{}})" by blast
from ‹p⇩A permutes A› have "inj ((`) p⇩A)"
by (meson injI inj_image_eq_iff permutes_inj)
have inv_image_eq': "(λb. {x ∈ A. f x = b}) ` B - {{}} = (λb. {x ∈ A. f' (inv p⇩A x) = b}) ` B - {{}}"
proof -
note inv_image_eq
also have "(λX. p⇩A ` X) ` ((λb. {x ∈ A. f' x = b}) ` B - {{}}) = (λb. {x ∈ A. f' (inv p⇩A x) = b}) ` B - {{}}"
using image_domain_partition_eq[OF ‹f' ∈ A →⇩E B› ‹p⇩A permutes A›]
by (simp add: image_set_diff[OF ‹inj ((`) p⇩A)›])
finally show ?thesis .
qed
from ‹p⇩A permutes A› have "inv p⇩A permutes A"
using permutes_inv by blast
have "(λx. f' (inv p⇩A x)) ∈ A →⇩E B"
using ‹f' ∈ A →⇩E B› ‹inv p⇩A permutes A› permutes_in_image by fastforce
from ‹f ∈ A →⇩E B› this ‹finite B› obtain p⇩B
where "p⇩B permutes B" and eq'': "∀x∈A. f x = p⇩B (f' (inv p⇩A x))"
using partitions_eq_implies_permutes[OF _ _ _ inv_image_eq'] by blast
from ‹inv p⇩A permutes A› ‹p⇩B permutes B› eq'' that show thesis by blast
qed
subsection ‹Bijections on Same Domain and Range›
subsubsection ‹Existence of Domain Permutation›
lemma obtain_domain_permutation_for_two_bijections:
assumes "bij_betw f A B" "bij_betw f' A B"
obtains p where "p permutes A" and "∀a∈A. f a = f' (p a)"
proof -
let ?p = "λa. if a ∈ A then the_inv_into A f' (f a) else a"
have "?p permutes A"
proof (rule bij_imp_permutes)
show "bij_betw ?p A A"
proof (rule bij_betw_imageI)
show "inj_on ?p A"
proof (rule inj_onI)
fix a a'
assume "a ∈ A" "a' ∈ A" "?p a = ?p a'"
from this have "the_inv_into A f' (f a) = the_inv_into A f' (f a')"
using ‹a ∈ A› ‹a' ∈ A› by simp
from this have "f a = f a'"
using ‹a ∈ A› ‹a' ∈ A› assms
by (metis bij_betwE f_the_inv_into_f_bij_betw)
from this show "a = a'"
using ‹a ∈ A› ‹a' ∈ A› assms
by (metis bij_betw_inv_into_left)
qed
next
show "?p ` A = A"
proof
show "?p ` A ⊆ A"
proof
fix a
assume "a ∈ ?p ` A"
from this obtain a' where "a' ∈ A" and "a = the_inv_into A f' (f a')" by auto
from this assms show "a ∈ A"
by (metis bij_betwE bij_betw_imp_inj_on bij_betw_imp_surj_on subset_iff the_inv_into_into)
qed
next
show "A ⊆ ?p ` A"
proof
fix a
assume "a ∈ A"
from this assms have "the_inv_into A f (f' a) ∈ A"
by (meson bij_betwE bij_betw_the_inv_into)
moreover from ‹a ∈ A› assms have "a = the_inv_into A f' (f (the_inv_into A f (f' a)))"
by (metis bij_betwE bij_betw_imp_inj_on f_the_inv_into_f_bij_betw the_inv_into_f_eq)
ultimately show "a ∈ ?p ` A" by auto
qed
qed
qed
next
fix a
assume "a ∉ A"
from this show "?p a = a" by auto
qed
moreover have "∀a∈A. f a = f' (?p a)"
using ‹bij_betw f A B› ‹bij_betw f' A B›
using bij_betwE f_the_inv_into_f_bij_betw by fastforce
moreover note that
ultimately show thesis by auto
qed
subsubsection ‹Existence of Range Permutation›
lemma obtain_range_permutation_for_two_bijections:
assumes "bij_betw f A B" "bij_betw f' A B"
obtains p where "p permutes B" and "∀a∈A. f a = p (f' a)"
proof -
let ?p = "λb. if b ∈ B then f (inv_into A f' b) else b"
have "?p permutes B"
proof (rule bij_imp_permutes)
show "bij_betw ?p B B"
proof (rule bij_betw_imageI)
show "inj_on ?p B"
proof (rule inj_onI)
fix b b'
assume "b ∈ B" "b' ∈ B" "?p b = ?p b'"
from this have "f (inv_into A f' b) = f (inv_into A f' b')"
using ‹b ∈ B› ‹b' ∈ B› by simp
from this have "inv_into A f' b = inv_into A f' b'"
using ‹b ∈ B› ‹b' ∈ B› assms
by (metis bij_betw_imp_surj_on bij_betw_inv_into_left inv_into_into)
from this show "b = b'"
using ‹b ∈ B› ‹b' ∈ B› assms(2)
by (metis bij_betw_inv_into_right)
qed
next
show "?p ` B = B"
proof
from assms show "?p ` B ⊆ B"
by (auto simp add: bij_betwE bij_betw_def inv_into_into)
next
show "B ⊆ ?p ` B"
proof
fix b
assume "b ∈ B"
from this assms have "f' (inv_into A f b) ∈ B"
by (metis bij_betwE bij_betw_imp_surj_on inv_into_into)
moreover have "b = ?p (f' (inv_into A f b))"
using assms ‹f' (inv_into A f b) ∈ B› ‹b ∈ B›
by (auto simp add: bij_betw_imp_surj_on bij_betw_inv_into_left bij_betw_inv_into_right inv_into_into)
ultimately show "b ∈ ?p ` B" by auto
qed
qed
qed
next
fix b
assume "b ∉ B"
from this show "?p b = b" by auto
qed
moreover have "∀a∈A. f a = ?p (f' a)"
using ‹bij_betw f' A B› bij_betw_inv_into_left bij_betwE by fastforce
moreover note that
ultimately show thesis by auto
qed
end