Theory Fun_More2
subsection ‹Results on Bijections›
theory Fun_More2 imports Main begin
lemma finite_card_eq_imp_bij_betw:
assumes "finite A"
and "card (f ` A) = card A"
shows "bij_betw f A (f ` A)"
using ‹card (f ` A) = card A›
unfolding inj_on_iff_eq_card [OF ‹finite A›, symmetric]
by (rule inj_on_imp_bij_betw)
text ‹Every bijective function between two subsets of a set can be turned
into a compatible renaming (with finite domain) on the full set.›
lemma bij_betw_extend:
assumes *: "bij_betw f A B"
and "A ⊆ V"
and "B ⊆ V"
and "finite A"
shows "∃g. finite {x. g x ≠ x} ∧
(∀x∈UNIV - (A ∪ B). g x = x) ∧
(∀x∈A. g x = f x) ∧
bij_betw g V V"
proof -
have "finite B" using assms by (metis bij_betw_finite)
have [simp]: "card A = card B" by (metis * bij_betw_same_card)
have "card (A - B) = card (B - A)"
proof -
have "card (A - B) = card A - card (A ∩ B)"
by (metis ‹finite A› card_Diff_subset_Int finite_Int)
moreover have "card (B - A) = card B - card (A ∩ B)"
by (metis ‹finite A› card_Diff_subset_Int finite_Int inf_commute)
ultimately show ?thesis by simp
qed
then obtain g where **: "bij_betw g (B - A) (A - B)"
by (metis ‹finite A› ‹finite B› bij_betw_iff_card finite_Diff)
define h where "h = (λx. if x ∈ A then f x else if x ∈ B - A then g x else x)"
have "bij_betw h A B"
by (metis (full_types) * bij_betw_cong h_def)
moreover have "bij_betw h (V - (A ∪ B)) (V - (A ∪ B))"
by (auto simp: bij_betw_def h_def inj_on_def)
moreover have "B ∩ (V - (A ∪ B)) = {}" by blast
ultimately have "bij_betw h (A ∪ (V - (A ∪ B))) (B ∪ (V - (A ∪ B)))"
by (rule bij_betw_combine)
moreover have "A ∪ (V - (A ∪ B)) = V - (B - A)"
and "B ∪ (V - (A ∪ B)) = V - (A - B)"
using ‹A ⊆ V› and ‹B ⊆ V› by blast+
ultimately have "bij_betw h (V - (B - A)) (V - (A - B))" by simp
moreover have "bij_betw h (B - A) (A - B)"
using ** by (auto simp: bij_betw_def h_def inj_on_def)
moreover have "(V - (A - B)) ∩ (A - B) = {}" by blast
ultimately have "bij_betw h ((V - (B - A)) ∪ (B - A)) ((V - (A - B)) ∪ (A - B))"
by (rule bij_betw_combine)
moreover have "(V - (B - A)) ∪ (B - A) = V"
and "(V - (A - B)) ∪ (A - B) = V"
using ‹A ⊆ V› and ‹B ⊆ V› by auto
ultimately have "bij_betw h V V" by simp
moreover have "∀x∈A. h x = f x" by (auto simp: h_def)
moreover have "finite {x. h x ≠ x}"
proof -
have "finite (A ∪ (B - A))" using ‹finite A› and ‹finite B› by auto
moreover have "{x. h x ≠ x} ⊆ (A ∪ (B - A))" by (auto simp: h_def)
ultimately show ?thesis by (metis finite_subset)
qed
moreover have "∀x∈UNIV - (A ∪ B). h x = x" by (simp add: h_def)
ultimately show ?thesis by blast
qed
lemma bij_betw_to_bij: assumes "bij_betw f A B"
and "finite A"
shows "∃ r. bij r ∧ (∀ x ∈ A. f x = r x) ∧ (∀ x. x ∉ A ∪ B ⟶ r x = x)"
proof -
define S where "S = A ∪ B"
have "A ⊆ S" "B ⊆ S" by (auto simp: S_def)
from bij_betw_extend[OF assms(1) this assms(2), folded S_def]
obtain g where g: "(∀x∈UNIV - S. g x = x)" "(∀x∈A. g x = f x)" "bij_betw g S S"
by blast
show ?thesis
proof (rule exI[of _ g], intro conjI)
show "∀x. x ∉ A ∪ B ⟶ g x = x" using g S_def by auto
show "∀x∈A. f x = g x" using g by auto
have "bij_betw g (UNIV - S) (UNIV - S)" using g(1)
unfolding bij_betw_def by (auto simp: inj_on_def)
from bij_betw_combine[OF this g(3)]
show "bij g" by auto
qed
qed
subsection ‹Merging Functions›
definition fun_merge :: "('a ⇒ 'b)list ⇒ 'a set list ⇒ 'a ⇒ 'b"
where
"fun_merge fs as a = (fs ! (LEAST i. i < length as ∧ a ∈ as ! i)) a"
lemma fun_merge_eq_nth:
assumes i: "i < length as"
and a: "a ∈ as ! i"
and ident: "⋀ i j a. i < length as ⟹ j < length as ⟹ a ∈ as ! i ⟹ a ∈ as ! j ⟹ (fs ! i) a = (fs ! j) a"
shows "fun_merge fs as a = (fs ! i) a"
proof -
let ?p = "λ i. i < length as ∧ a ∈ as ! i"
let ?l = "LEAST i. ?p i"
have p: "?p ?l"
by (rule LeastI, insert i a, auto)
show ?thesis unfolding fun_merge_def
by (rule ident[OF _ i _ a], insert p, auto)
qed
lemma fun_merge_part:
assumes "∀i<length as.∀j<length as. i ≠ j ⟶ as ! i ∩ as ! j = {}"
and "i < length as"
and "a ∈ as ! i"
shows "fun_merge fs as a = (fs ! i) a"
proof(rule fun_merge_eq_nth [OF assms(2, 3)])
fix i j a
assume "i < length as" and "j < length as" and "a ∈ as ! i" and "a ∈ as ! j"
then have "i = j" using assms by (cases "i = j") auto
then show "(fs ! i) a = (fs ! j) a" by simp
qed
lemma fun_merge:
assumes part: "∀i<length Xs.∀j<length Xs. i ≠ j ⟶ Xs ! i ∩ Xs ! j = {}"
shows "∃σ. ∀i<length Xs. ∀x∈ Xs ! i. σ x = τ i x"
proof -
let ?τ = "map τ [0 ..< length Xs]"
let ?σ = "fun_merge ?τ Xs"
show ?thesis
by (rule exI[of _ ?σ], intro allI impI ballI,
insert fun_merge_part[OF part, of _ _ ?τ], auto)
qed
lemma dependent_nat_choice_start:
assumes 1: "P 0 x0"
and 2: "⋀x n. P n x ⟹ ∃y. P (Suc n) y ∧ Q n x y"
shows "∃f. f 0 = x0 ∧ (∀n. P n (f n) ∧ Q n (f n) (f (Suc n)))"
proof (intro exI allI conjI)
fix n
define f where "f = rec_nat x0 (λn x. SOME y. P (Suc n) y ∧ Q n x y)"
then have "P 0 (f 0)" "⋀n. P n (f n) ⟹ P (Suc n) (f (Suc n)) ∧ Q n (f n) (f (Suc n))"
using 1 someI_ex[OF 2] by simp_all
then show "P n (f n)" "Q n (f n) (f (Suc n))"
by (induct n) auto
qed auto
lemma dependent_nat_choice2_start:
assumes 1: "P 0 x0 y0"
and 2: "⋀x y n. P n x y ⟹ ∃x' y'. P (Suc n) x' y' ∧ Q n x y x' y'"
shows "∃ x y. x 0 = x0 ∧ y 0 = y0 ∧ (∀n. P n (x n) (y n) ∧ Q n (x n) (y n) (x (Suc n)) (y (Suc n)))"
proof -
have "∃f. f 0 = (x0, y0) ∧
(∀n. P n (fst (f n)) (snd (f n)) ∧
Q n (fst (f n)) (snd (f n)) (fst (f (Suc n))) (snd (f (Suc n))))" (is "∃ f. ?Prop f")
by (rule dependent_nat_choice_start[of "λ i xy. P i (fst xy) (snd xy)" "(x0,y0)"
"λ i xy xy'. Q i (fst xy) (snd xy) (fst xy') (snd xy')"], insert 1 2, auto)
then obtain f where f: "?Prop f" by blast
show ?thesis by (rule exI[of _ "λ i. fst (f i)"], rule exI[of _ "λ i. snd (f i)"], insert f, auto)
qed
end