Theory Functions_Bijection

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Bijections›
theory Functions_Bijection
  imports
    Functions_Inverse
    Functions_Monotone
begin

consts bijection_on :: "'a  'b  'c  'd  bool"

definition "bijection_on_pred (P :: 'a  bool) (Q :: 'b  bool) f g 
  (P m Q) f 
  (Q m P) g 
  inverse_on P f g 
  inverse_on Q g f"
adhoc_overloading bijection_on bijection_on_pred

context
  fixes P :: "'a  bool" and Q :: "'b  bool" and f :: "'a  'b" and g :: "'b  'a"
begin

lemma bijection_onI [intro]:
  assumes "(P m Q) f"
  and "(Q m P) g"
  and "inverse_on P f g"
  and "inverse_on Q g f"
  shows "bijection_on P Q f g"
  using assms unfolding bijection_on_pred_def by blast

lemma bijection_onE [elim]:
  assumes "bijection_on P Q f g"
  obtains "(P m Q) f" "(Q m P) g"
    "inverse_on P f g" "inverse_on Q g f"
  using assms unfolding bijection_on_pred_def by blast

lemma mono_wrt_pred_if_bijection_on_left:
  assumes "bijection_on P Q f g"
  shows "(P m Q) f"
  using assms by (elim bijection_onE)

lemma mono_wrt_pred_if_bijection_on_right:
  assumes "bijection_on P Q f g"
  shows "(Q m P) g"
  using assms by (elim bijection_onE)

lemma bijection_on_pred_right:
  assumes "bijection_on P Q f g"
  and "P x"
  shows "Q (f x)"
  using assms by blast

lemma bijection_on_pred_left:
  assumes "bijection_on P Q f g"
  and "Q y"
  shows "P (g y)"
  using assms by blast

lemma inverse_on_if_bijection_on_left_right:
  assumes "bijection_on P Q f g"
  shows "inverse_on P f g"
  using assms by (elim bijection_onE)

lemma inverse_on_if_bijection_on_right_left:
  assumes "bijection_on P Q f g"
  shows "inverse_on Q g f"
  using assms by (elim bijection_onE)

lemma bijection_on_left_right_eq_self:
  assumes "bijection_on P Q f g"
  and "P x"
  shows "g (f x) = x"
  using assms inverse_on_if_bijection_on_left_right
  by (intro inverse_onD)

lemma bijection_on_right_left_eq_self':
  assumes "bijection_on P Q f g"
  and "Q y"
  shows "f (g y) = y"
  using assms inverse_on_if_bijection_on_right_left by (intro inverse_onD)

end

context
  fixes P :: "'a  bool" and Q :: "'b  bool" and f :: "'a  'b" and g :: "'b  'a"
begin

lemma bijection_on_right_left_if_bijection_on_left_right:
  assumes "bijection_on P Q f g"
  shows "bijection_on Q P g f"
  using assms by auto

lemma injective_on_if_bijection_on_left:
  assumes "bijection_on P Q f g"
  shows "injective_on P f"
  using assms
  by (intro injective_on_if_inverse_on inverse_on_if_bijection_on_left_right)

lemma injective_on_if_bijection_on_right:
  assumes "bijection_on P Q f g"
  shows "injective_on Q g"
  by (intro injective_on_if_inverse_on)
  (fact inverse_on_if_bijection_on_right_left[OF assms])

end

lemma bijection_on_compI:
  fixes P :: "'a  bool" and P' :: "'b  bool" and Q :: "'c  bool"
  assumes "bijection_on P P' f g"
  and "bijection_on P' Q f' g'"
  shows "bijection_on P Q (f'  f) (g  g')"
  using assms by (intro bijection_onI)
  (auto intro: dep_mono_wrt_pred_comp_dep_mono_wrt_pred_compI' inverse_on_compI
    elim!: bijection_onE simp: mono_wrt_pred_eq_dep_mono_wrt_pred)


consts bijection :: "'a  'b  bool"

definition "(bijection_rel :: ('a  'b)  ('b  'a)  bool) 
  bijection_on ( :: 'a  bool) ( :: 'b  bool)"
adhoc_overloading bijection bijection_rel

lemma bijection_eq_bijection_on:
  "(bijection :: ('a  'b)  ('b  'a)  bool) = bijection_on ( :: 'a  bool) ( :: 'b  bool)"
  unfolding bijection_rel_def ..

lemma bijection_eq_bijection_on_uhint [uhint]:
  assumes "P  ( :: 'a  bool)"
  and "Q  ( :: 'b  bool)"
  shows "(bijection :: ('a  'b)  ('b  'a)  bool) = bijection_on P Q"
  using assms by (simp add: bijection_eq_bijection_on)

context
  fixes P :: "'a  bool" and Q :: "'b  bool" and f :: "'a  'b" and g :: "'b  'a"
begin

lemma bijectionI [intro]:
  assumes "inverse f g"
  and "inverse g f"
  shows "bijection f g"
  by (urule bijection_onI) (simp | urule assms)+

lemma bijectionE [elim]:
  assumes "bijection f g"
  obtains "inverse f g" "inverse g f"
  using assms by (urule (e) bijection_onE)

lemma inverse_if_bijection_left_right:
  assumes "bijection f g"
  shows "inverse f g"
  using assms by (elim bijectionE)

lemma inverse_if_bijection_right_left:
  assumes "bijection f g"
  shows "inverse g f"
  using assms by (elim bijectionE)

end

lemma bijection_right_left_if_bijection_left_right:
  fixes f :: "'a  'b" and g :: "'b  'a"
  assumes "bijection f g"
  shows "bijection g f"
  using assms by auto

paragraph ‹Instantiations›

lemma bijection_on_self_id: "bijection_on (P :: 'a  bool) P id id"
  by (intro bijection_onI inverse_onI mono_wrt_predI) simp_all


end