Theory Fun_More

(*
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} 
    (xUNIV - (A  B). g x = x) 
    (xA. 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 "xA. 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 "xUNIV - (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