Theory HOL_Alignment_Functions

✐‹creator "Kevin Kappelmann"›
subsection ‹Alignment With Function Definitions from HOL.Main›
theory HOL_Alignment_Functions
  imports
    HOL_Alignment_Binary_Relations
    HOL_Syntax_Bundles_Functions
    LFunctions
begin

unbundle no_HOL_function_syntax

named_theorems HOL_fun_alignment

paragraph ‹Functions›

subparagraph ‹Bijection›

definition "bijection_on_set (S :: 'a set) (S' :: 'b set) :: ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool ≡
  bijection_on (mem_of S) (mem_of S')"
adhoc_overloading bijection_on bijection_on_set

lemma bijection_on_set_eq_bijection_on_pred [simp]:
  "bijection_on (S :: 'a set) (S' :: 'b set) = bijection_on (mem_of S) (mem_of S')"
  unfolding bijection_on_set_def by simp

lemma bijection_on_set_eq_bijection_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  and "Q ≡ mem_of S'"
  shows "bijection_on S S' ≡ bijection_on P Q"
  using assms by simp

lemma bijection_on_set_iff_bijection_on_pred [iff]:
  "bijection_on (S :: 'a set) (S' :: 'b set) (f :: 'a ⇒ 'b) (g :: 'b ⇒ 'a) ⟷
    bijection_on (mem_of S) (mem_of S') f g"
  by simp

lemma bij_betw_bijection_onE:
  assumes "bij_betw (f :: 'a ⇒ 'b) S S'"
  obtains g :: "'b ⇒ 'a" where "bijection_on S S' f g"
proof
  let ?g = "the_inv_into S f"
  from assms bij_betw_the_inv_into have "bij_betw ?g S' S" by blast
  with assms show "bijection_on S S' f ?g"
    by (auto intro!: bijection_onI
      dest: bij_betw_apply bij_betw_imp_inj_on the_inv_into_f_f
      simp: f_the_inv_into_f_bij_betw)
qed

lemma bij_betw_if_bijection_on:
  assumes "bijection_on S S' (f :: 'a ⇒ 'b) (g :: 'b ⇒ 'a)"
  shows "bij_betw f S S'"
  using assms by (intro bij_betw_byWitness[where ?f'=g])
  (auto elim: bijection_onE dest: inverse_onD)

corollary bij_betw_iff_ex_bijection_on [HOL_fun_alignment]:
  "bij_betw (f :: 'a ⇒ 'b) S S' ⟷ (∃(g :: 'b ⇒ 'a). bijection_on S S' f g)"
  by (intro iffI) (auto elim!: bij_betw_bijection_onE intro: bij_betw_if_bijection_on)


subparagraph ‹Injective›

overloading
  injective_on_set ≡ "injective_on :: 'a set ⇒ ('a ⇒ 'b) ⇒ bool"
begin
  definition "injective_on_set (S :: 'a set) :: ('a ⇒ 'b) ⇒ bool ≡
    injective_on (mem_of S)"
end

lemma injective_on_set_eq_injective_on_pred [simp]:
  "(injective_on (S :: 'a set) :: ('a ⇒ 'b) ⇒ _) = injective_on (mem_of S)"
  unfolding injective_on_set_def by simp

lemma injective_on_set_eq_injective_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "injective_on (S :: 'a set) :: ('a ⇒ 'b) ⇒ _ ≡ injective_on P"
  using assms by simp

lemma injective_on_set_iff_injective_on_pred [iff]:
  "injective_on (S :: 'a set) (f :: 'a ⇒ 'b) ⟷ injective_on (mem_of S) f"
  by simp

lemma inj_on_iff_injective_on [HOL_fun_alignment]: "inj_on f P ⟷ injective_on P f"
  by (auto intro: inj_onI dest: inj_onD injective_onD)

lemma inj_eq_injective [HOL_fun_alignment]: "inj = injective"
  by (auto intro: injI dest: injD injectiveD)


subparagraph ‹Inverse›

overloading
  inverse_on_set ≡ "inverse_on :: 'a set ⇒ ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool"
begin
  definition "inverse_on_set (S :: 'a set) :: ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool ≡
    inverse_on (mem_of S)"
end

lemma inverse_on_set_eq_inverse_on_pred [simp]:
  "(inverse_on (S :: 'a set) :: ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ _) = inverse_on (mem_of S)"
  unfolding inverse_on_set_def by simp

lemma inverse_on_set_eq_inverse_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "inverse_on (S :: 'a set) :: ('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ _ ≡ inverse_on P"
  using assms by simp

lemma inverse_on_set_iff_inverse_on_pred [iff]:
  "inverse_on (S :: 'a set) (f :: 'a ⇒ 'b) (g :: 'b ⇒ 'a) ⟷ inverse_on (mem_of S) f g"
  by simp


subparagraph ‹Monotone›

lemma monotone_on_eq_mono_wrt_rel_restrict_left_right [HOL_fun_alignment]:
  "monotone_on S R = mono_wrt_rel R↾⇘S⇙↿⇘S⇙"
  by (intro ext) (auto intro!: monotone_onI dest: monotone_onD)

lemma monotone_eq_mono_wrt_rel [HOL_fun_alignment]: "monotone = mono_wrt_rel"
  by (intro ext) (auto intro: monotoneI dest: monotoneD)

lemma pred_fun_eq_mono_wrt_pred [HOL_fun_alignment]: "pred_fun = mono_wrt_pred"
  by (intro ext) auto

lemma Fun_mono_eq_mono [HOL_fun_alignment]: "Fun.mono = mono"
  by (intro ext) (auto intro: Fun.mono_onI dest: Fun.monoD)

lemma Fun_antimono_eq_antimono [HOL_fun_alignment]: "Fun.antimono = antimono"
  by (intro ext) (auto intro: monotoneI dest: monotoneD)


subparagraph ‹Surjective›

overloading
  surjective_at_set ≡ "surjective_at :: 'a set ⇒ ('b ⇒ 'a) ⇒ bool"
begin
  definition "surjective_at_set (S :: 'a set) :: ('b ⇒ 'a) ⇒ bool ≡
    surjective_at (mem_of S)"
end

lemma surjective_at_set_eq_surjective_at_pred [simp]:
  "(surjective_at (S :: 'a set) :: ('b ⇒ 'a) ⇒ _) = surjective_at (mem_of S)"
  unfolding surjective_at_set_def by simp

lemma surjective_at_set_eq_surjective_at_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "surjective_at (S :: 'a set) :: ('b ⇒ 'a) ⇒ _ ≡ surjective_at P"
  using assms by simp

lemma surjective_at_set_iff_surjective_at_pred [iff]:
  "surjective_at (S :: 'a set) (f :: 'b ⇒ 'a) ⟷ surjective_at (mem_of S) f"
  by simp

lemma surj_eq_surjective [HOL_fun_alignment]: "surj = surjective"
  by (intro ext) (fast intro: surjI dest: surjD elim: surjectiveE)


paragraph ‹Functions›

lemma Fun_id_eq_id [HOL_fun_alignment]: "Fun.id = Functions_Base.id"
  by (intro ext) simp

lemma Fun_comp_eq_comp [HOL_fun_alignment]: "Fun.comp = Functions_Base.comp"
  by (intro ext) simp

lemma map_fun_eq_fun_map [HOL_fun_alignment]: "map_fun = fun_map"
  by (intro ext) simp


paragraph ‹Relators›

lemma rel_fun_eq_Fun_Rel_rel [HOL_fun_alignment]: "BNF_Def.rel_fun = Fun_Rel"
  by (intro ext) (auto dest: rel_funD)


end