Theory First_Order_Terms.Fun_More
subsection ‹Results on Bijections›
theory Fun_More 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
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
end