(* Title: HOL/Cardinals/Fun_More.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 More on injections, bijections and inverses. *) section ‹More on Injections, Bijections and Inverses› theory Fun_More imports Main begin subsection ‹Purely functional properties› (* unused *) (*1*)lemma notIn_Un_bij_betw2: assumes NIN: "b ∉ A" and NIN': "b' ∉ A'" and BIJ: "bij_betw f A A'" shows "bij_betw f (A ∪ {b}) (A' ∪ {b'}) = (f b = b')" proof assume "f b = b'" thus "bij_betw f (A ∪ {b}) (A' ∪ {b'})" using assms notIn_Un_bij_betw[of b A f A'] by auto next assume *: "bij_betw f (A ∪ {b}) (A' ∪ {b'})" hence "f b ∈ A' ∪ {b'}" unfolding bij_betw_def by auto moreover {assume "f b ∈ A'" then obtain b1 where 1: "b1 ∈ A" and 2: "f b1 = f b" using BIJ by (auto simp add: bij_betw_def) hence "b = b1" using * by (auto simp add: bij_betw_def inj_on_def) with 1 NIN have False by auto } ultimately show "f b = b'" by blast qed (* unused *) (*1*)lemma bij_betw_ball: assumes BIJ: "bij_betw f A B" shows "(∀b ∈ B. phi b) = (∀a ∈ A. phi(f a))" using assms unfolding bij_betw_def inj_on_def by blast (* unused *) (*1*)lemma bij_betw_diff_singl: assumes BIJ: "bij_betw f A A'" and IN: "a ∈ A" shows "bij_betw f (A - {a}) (A' - {f a})" proof- let ?B = "A - {a}" let ?B' = "A' - {f a}" have "f a ∈ A'" using IN BIJ unfolding bij_betw_def by blast hence "a ∉ ?B ∧ f a ∉ ?B' ∧ A = ?B ∪ {a} ∧ A' = ?B' ∪ {f a}" using IN by blast thus ?thesis using notIn_Un_bij_betw3[of a ?B f ?B'] BIJ by simp qed subsection ‹Properties involving finite and infinite sets› (*3*)lemma inj_on_image_Pow: assumes "inj_on f A" shows "inj_on (image f) (Pow A)" unfolding Pow_def inj_on_def proof(clarsimp) fix X Y assume *: "X ≤ A" and **: "Y ≤ A" and ***: "f ` X = f ` Y" show "X = Y" proof(auto) fix x assume ****: "x ∈ X" with *** obtain y where "y ∈ Y ∧ f x = f y" by blast with **** * ** assms show "x ∈ Y" unfolding inj_on_def by auto next fix y assume ****: "y ∈ Y" with *** obtain x where "x ∈ X ∧ f x = f y" by atomize_elim force with **** * ** assms show "y ∈ X" unfolding inj_on_def by auto qed qed (*2*)lemma bij_betw_image_Pow: assumes "bij_betw f A B" shows "bij_betw (image f) (Pow A) (Pow B)" using assms unfolding bij_betw_def by (auto simp add: inj_on_image_Pow image_Pow_surj) (* unused *) (*1*)lemma bij_betw_inv_into_RIGHT: assumes BIJ: "bij_betw f A A'" and SUB: "B' ≤ A'" shows "f `((inv_into A f)`B') = B'" using assms proof(auto simp add: bij_betw_inv_into_right) let ?f' = "(inv_into A f)" fix a' assume *: "a' ∈ B'" hence "a' ∈ A'" using SUB by auto hence "a' = f (?f' a')" using BIJ by (auto simp add: bij_betw_inv_into_right) thus "a' ∈ f ` (?f' ` B')" using * by blast qed (* unused *) (*1*)lemma bij_betw_inv_into_RIGHT_LEFT: assumes BIJ: "bij_betw f A A'" and SUB: "B' ≤ A'" and IM: "(inv_into A f) ` B' = B" shows "f ` B = B'" proof- have "f`((inv_into A f)` B') = B'" using assms bij_betw_inv_into_RIGHT[of f A A' B'] by auto thus ?thesis using IM by auto qed (* unused *) (*2*)lemma bij_betw_inv_into_twice: assumes "bij_betw f A A'" shows "∀a ∈ A. inv_into A' (inv_into A f) a = f a" proof let ?f' = "inv_into A f" let ?f'' = "inv_into A' ?f'" have 1: "bij_betw ?f' A' A" using assms by (auto simp add: bij_betw_inv_into) fix a assume *: "a ∈ A" then obtain a' where 2: "a' ∈ A'" and 3: "?f' a' = a" using 1 unfolding bij_betw_def by force hence "?f'' a = a'" using * 1 3 by (auto simp add: bij_betw_inv_into_left) moreover have "f a = a'" using assms 2 3 by (auto simp add: bij_betw_inv_into_right) ultimately show "?f'' a = f a" by simp qed subsection ‹Properties involving Hilbert choice› (*1*)lemma bij_betw_inv_into_LEFT: assumes BIJ: "bij_betw f A A'" and SUB: "B ≤ A" shows "(inv_into A f)`(f ` B) = B" using assms unfolding bij_betw_def using inv_into_image_cancel by force (*1*)lemma bij_betw_inv_into_LEFT_RIGHT: assumes BIJ: "bij_betw f A A'" and SUB: "B ≤ A" and IM: "f ` B = B'" shows "(inv_into A f) ` B' = B" using assms bij_betw_inv_into_LEFT[of f A A' B] by fast subsection ‹Other facts› (*3*)lemma atLeastLessThan_injective: assumes "{0 ..< m::nat} = {0 ..< n}" shows "m = n" proof- {assume "m < n" hence "m ∈ {0 ..< n}" by auto hence "{0 ..< m} < {0 ..< n}" by auto hence False using assms by blast } moreover {assume "n < m" hence "n ∈ {0 ..< m}" by auto hence "{0 ..< n} < {0 ..< m}" by auto hence False using assms by blast } ultimately show ?thesis by force qed (*2*)lemma atLeastLessThan_injective2: "bij_betw f {0 ..< m::nat} {0 ..< n} ⟹ m = n" using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n] card_atLeastLessThan[of m] card_atLeastLessThan[of n] bij_betw_iff_card[of "{0 ..< m}" "{0 ..< n}"] by auto (*2*)lemma atLeastLessThan_less_eq: "({0..<m} ≤ {0..<n}) = ((m::nat) ≤ n)" unfolding ivl_subset by arith (*2*)lemma atLeastLessThan_less_eq2: assumes "inj_on f {0..<(m::nat)} ∧ f ` {0..<m} ≤ {0..<n}" shows "m ≤ n" using assms using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n] card_atLeastLessThan[of m] card_atLeastLessThan[of n] card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce (* unused *) (*2*)lemma atLeastLessThan_less_eq3: "(∃f. inj_on f {0..<(m::nat)} ∧ f ` {0..<m} ≤ {0..<n}) = (m ≤ n)" using atLeastLessThan_less_eq2 proof(auto) assume "m ≤ n" hence "inj_on id {0..<m} ∧ id ` {0..<m} ⊆ {0..<n}" unfolding inj_on_def by force thus "∃f. inj_on f {0..<m} ∧ f ` {0..<m} ⊆ {0..<n}" by blast qed (* unused *) (*3*)lemma atLeastLessThan_less: "({0..<m} < {0..<n}) = ((m::nat) < n)" proof- have "({0..<m} < {0..<n}) = ({0..<m} ≤ {0..<n} ∧ {0..<m} ~= {0..<n})" using subset_iff_psubset_eq by blast also have "… = (m ≤ n ∧ m ~= n)" using atLeastLessThan_less_eq atLeastLessThan_injective by blast also have "… = (m < n)" by auto finally show ?thesis . qed end