Theory HOL-Cardinals.Fun_More

(*  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

subsection ‹Purely functional properties›

(* 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})"
  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

subsection ‹Properties involving finite and infinite sets›

(* 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'"
  by (metis BIJ SUB bij_betw_imp_surj_on image_inv_into_cancel)

(* 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'"
  by (metis BIJ IM SUB bij_betw_inv_into_RIGHT)

(* 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"
  by (simp add: assms inv_into_inv_into_eq)

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"
  using assms atLeast0LessThan by force

(*2*)lemma atLeastLessThan_injective2:
  "bij_betw f {0 ..< m::nat} {0 ..< n}  m = n"
  using bij_betw_same_card by fastforce

(*2*)lemma atLeastLessThan_less_eq:
  "({0..<m}  {0..<n}) = ((m::nat)  n)"
  by auto

(*2*)lemma atLeastLessThan_less_eq2:
  assumes "inj_on f {0..<(m::nat)}" "f ` {0..<m}  {0..<n}"
  shows "m  n"
  by (metis assms card_inj_on_le card_lessThan finite_lessThan lessThan_atLeast0)

(* unused *)
(*3*)lemma atLeastLessThan_less:
  "({0..<m} < {0..<n}) = ((m::nat) < n)"
  by auto