(* Author: Christian Sternagel <c.sternagel@gmail.com> Author: René Thiemann <rene.thiemann@uibk.ac.at> License: LGPL *) 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› (* Copied and canonized from IsaFoR's Term theory and Polynomial Factorization in the AFP. *) 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