Theory HOL_Alignment_Binary_Relations

✐‹creator "Kevin Kappelmann"›
subsection ‹Alignment With Binary Relation Definitions from HOL.Main›
theory HOL_Alignment_Binary_Relations
  imports
    Main
    HOL_Mem_Of
    HOL_Syntax_Bundles_Relations
    LBinary_Relations
begin

unbundle no_HOL_relation_syntax

named_theorems HOL_bin_rel_alignment

paragraph ‹Properties›
subparagraph ‹Antisymmetric›

overloading
  antisymmetric_on_set ≡ "antisymmetric_on :: 'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "antisymmetric_on_set (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ _ ≡
    antisymmetric_on (mem_of S)"
end

lemma antisymmetric_on_set_eq_antisymmetric_on_pred [simp]:
  "(antisymmetric_on (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ bool) = antisymmetric_on (mem_of S)"
  unfolding antisymmetric_on_set_def by simp

lemma antisymmetric_on_set_eq_antisymmetric_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "antisymmetric_on (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ bool ≡ antisymmetric_on P"
  using assms by simp

lemma antisymmetric_on_set_iff_antisymmetric_on_pred [iff]:
  "antisymmetric_on (S :: 'a set) (R :: 'a ⇒ 'a ⇒ bool) ⟷ antisymmetric_on (mem_of S) R"
  by simp

lemma antisymp_eq_antisymmetric [HOL_bin_rel_alignment]:
  "antisymp = antisymmetric"
  by (intro ext) (auto intro: antisympI dest: antisymmetricD antisympD)

subparagraph ‹Injective›

overloading
  rel_injective_on_set ≡ "rel_injective_on :: 'a set ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool"
  rel_injective_at_set ≡ "rel_injective_at :: 'a set ⇒ ('b ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "rel_injective_on_set (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ _ ≡
    rel_injective_on (mem_of S)"
  definition "rel_injective_at_set (S :: 'a set) :: ('b ⇒ 'a ⇒ bool) ⇒ _ ≡
    rel_injective_at (mem_of S)"
end

lemma rel_injective_on_set_eq_rel_injective_on_pred [simp]:
  "(rel_injective_on (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ bool) =
    rel_injective_on (mem_of S)"
  unfolding rel_injective_on_set_def by simp

lemma rel_injective_on_set_eq_rel_injective_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "rel_injective_on (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ bool ≡ rel_injective_on P"
  using assms by simp

lemma rel_injective_on_set_iff_rel_injective_on_pred [iff]:
  "rel_injective_on (S :: 'a set) (R :: 'a ⇒ 'b ⇒ bool) ⟷ rel_injective_on (mem_of S) R"
  by simp

lemma rel_injective_at_set_eq_rel_injective_at_pred [simp]:
  "(rel_injective_at (S :: 'a set) :: ('b ⇒ 'a ⇒ bool) ⇒ bool) =
    rel_injective_at (mem_of S)"
  unfolding rel_injective_at_set_def by simp

lemma rel_injective_at_set_eq_rel_injective_at_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "rel_injective_at (S :: 'a set) :: ('b ⇒ 'a ⇒ bool) ⇒ bool ≡ rel_injective_at P"
  using assms by simp

lemma rel_injective_at_set_iff_rel_injective_at_pred [iff]:
  "rel_injective_at (S :: 'a set) (R :: 'b ⇒ 'a ⇒ bool) ⟷ rel_injective_at (mem_of S) R"
  by simp

lemma left_unique_eq_rel_injective [HOL_bin_rel_alignment]:
  "left_unique = rel_injective"
  by (intro ext) (blast intro: left_uniqueI dest: rel_injectiveD left_uniqueD)

subparagraph ‹Irreflexive›

overloading
  irreflexive_on_set ≡ "irreflexive_on :: 'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "irreflexive_on_set (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ bool ≡
    irreflexive_on (mem_of S)"
end

lemma irreflexive_on_set_eq_irreflexive_on_pred [simp]:
  "(irreflexive_on (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ bool) =
    irreflexive_on (mem_of S)"
  unfolding irreflexive_on_set_def by simp

lemma irreflexive_on_set_eq_irreflexive_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "irreflexive_on (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ bool ≡ irreflexive_on P"
  using assms by simp

lemma irreflexive_on_set_iff_irreflexive_on_pred [iff]:
  "irreflexive_on (S :: 'a set) (R :: 'a ⇒ 'a ⇒ bool) ⟷ irreflexive_on (mem_of S) R"
  by simp

lemma irreflp_on_eq_irreflexive_on [HOL_bin_rel_alignment]: "irreflp_on = irreflexive_on"
  by (intro ext) (blast intro: irreflp_onI dest: irreflp_onD)

lemma irreflp_eq_irreflexive [HOL_bin_rel_alignment]: "irreflp = irreflexive"
  by (intro ext) (blast intro: irreflpI dest: irreflexiveD irreflpD)

subparagraph ‹Left-Total›

overloading
  left_total_on_set ≡ "left_total_on :: 'a set ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool"
begin
  definition "left_total_on_set (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ _ ≡
    left_total_on (mem_of S)"
end

lemma left_total_on_set_eq_left_total_on_pred [simp]:
  "(left_total_on (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ bool) =
    left_total_on (mem_of S)"
  unfolding left_total_on_set_def by simp

lemma left_total_on_set_eq_left_total_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "left_total_on (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ bool ≡ left_total_on P"
  using assms by simp

lemma left_total_on_set_iff_left_total_on_pred [iff]:
  "left_total_on (S :: 'a set) (R :: 'a ⇒ 'b ⇒ bool) ⟷ left_total_on (mem_of S) R"
  by simp

lemma Transfer_left_total_eq_left_total [HOL_bin_rel_alignment]:
  "Transfer.left_total = Binary_Relations_Left_Total.left_total"
  by (intro ext) (fast intro: Transfer.left_totalI
    elim: Transfer.left_totalE Binary_Relations_Left_Total.left_totalE)


subparagraph ‹Reflexive›

overloading
  reflexive_on_set ≡ "reflexive_on :: 'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "reflexive_on_set (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ _ ≡
    reflexive_on (mem_of S)"
end

lemma reflexive_on_set_eq_reflexive_on_pred [simp]:
  "(reflexive_on (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ bool) = reflexive_on (mem_of S)"
  unfolding reflexive_on_set_def by simp

lemma reflexive_on_set_eq_reflexive_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "reflexive_on (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ bool ≡ reflexive_on P"
  using assms by simp

lemma reflexive_on_set_iff_reflexive_on_pred [iff]:
  "reflexive_on (S :: 'a set) (R :: 'a ⇒ 'a ⇒ bool) ⟷ reflexive_on (mem_of S) R"
  by simp

lemma reflp_on_eq_reflexive_on [HOL_bin_rel_alignment]:
  "reflp_on = reflexive_on"
  by (intro ext) (blast intro: reflp_onI dest: reflp_onD)

lemma reflp_eq_reflexive [HOL_bin_rel_alignment]: "reflp = reflexive"
  by (intro ext) (blast intro: reflpI dest: reflexiveD reflpD)


subparagraph ‹Right-Unique›

overloading
  right_unique_on_set ≡ "right_unique_on :: 'a set ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool"
  right_unique_at_set ≡ "right_unique_at :: 'a set ⇒ ('b ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "right_unique_on_set (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ _ ≡
    right_unique_on (mem_of S)"
  definition "right_unique_at_set (S :: 'a set) :: ('b ⇒ 'a ⇒ bool) ⇒ _ ≡
    right_unique_at (mem_of S)"
end

lemma right_unique_on_set_eq_right_unique_on_pred [simp]:
  "(right_unique_on (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ bool) = right_unique_on (mem_of S)"
  unfolding right_unique_on_set_def by simp

lemma right_unique_on_set_eq_right_unique_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "right_unique_on (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ bool ≡ right_unique_on P"
  using assms by simp

lemma right_unique_on_set_iff_right_unique_on_pred [iff]:
  "right_unique_on (S :: 'a set) (R :: 'a ⇒ 'b ⇒ bool) ⟷ right_unique_on (mem_of S) R"
  by simp

lemma right_unique_at_set_eq_right_unique_at_pred [simp]:
  "(right_unique_at (S :: 'a set) :: ('b ⇒ 'a ⇒ bool) ⇒ bool) =
    right_unique_at (mem_of S)"
  unfolding right_unique_at_set_def by simp

lemma right_unique_at_set_iff_right_unique_at_pred [iff]:
  "right_unique_at (S :: 'a set) (R :: 'b ⇒ 'a ⇒ bool) ⟷ right_unique_at (mem_of S) R"
  by simp

lemma Transfer_right_unique_eq_right_unique [HOL_bin_rel_alignment]:
  "Transfer.right_unique = Binary_Relations_Right_Unique.right_unique"
  by (intro ext) (blast intro: Transfer.right_uniqueI
    dest: Transfer.right_uniqueD Binary_Relations_Right_Unique.right_uniqueD)


subparagraph ‹Surjective›

overloading
  rel_surjective_at_set ≡ "rel_surjective_at :: 'a set ⇒ ('b ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "rel_surjective_at_set (S :: 'a set) :: ('b ⇒ 'a ⇒ bool) ⇒ _ ≡
    rel_surjective_at (mem_of S)"
end

lemma rel_surjective_at_set_eq_rel_surjective_at_pred [simp]:
  "(rel_surjective_at (S :: 'a set) :: ('b ⇒ 'a ⇒ bool) ⇒ bool) = rel_surjective_at (mem_of S)"
  unfolding rel_surjective_at_set_def by simp

lemma rel_surjective_at_set_eq_rel_surjective_at_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "rel_surjective_at (S :: 'a set) :: ('b ⇒ 'a ⇒ bool) ⇒ bool ≡ rel_surjective_at P"
  using assms by simp

lemma rel_surjective_at_set_iff_rel_surjective_at_pred [iff]:
  "rel_surjective_at (S :: 'a set) (R :: 'b ⇒ 'a ⇒ bool) ⟷ rel_surjective_at (mem_of S) R"
  by simp

lemma Transfer_right_total_eq_rel_surjective [HOL_bin_rel_alignment]:
  "Transfer.right_total = rel_surjective"
  by (intro ext) (fast intro: Transfer.right_totalI rel_surjectiveI
    elim: Transfer.right_totalE rel_surjectiveE)


subparagraph ‹Symmetric›

overloading
  symmetric_on_set ≡ "symmetric_on :: 'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "symmetric_on_set (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ _ ≡
    symmetric_on (mem_of S)"
end

lemma symmetric_on_set_eq_symmetric_on_pred [simp]:
  "(symmetric_on (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ bool) = symmetric_on (mem_of S)"
  unfolding symmetric_on_set_def by simp

lemma symmetric_on_set_eq_symmetric_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "symmetric_on (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ bool ≡ symmetric_on P"
  using assms by simp

lemma symmetric_on_set_iff_symmetric_on_pred [iff]:
  "symmetric_on (S :: 'a set) (R :: 'a ⇒ 'a ⇒ bool) ⟷ symmetric_on (mem_of S) R"
  by simp

lemma symp_eq_symmetric [HOL_bin_rel_alignment]: "symp = symmetric"
  by (intro ext) (blast intro: sympI dest: symmetricD sympD)


subparagraph ‹Transitive›

overloading
  transitive_on_set ≡ "transitive_on :: 'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "transitive_on_set (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ _ ≡
    transitive_on (mem_of S)"
end

lemma transitive_on_set_eq_transitive_on_pred [simp]:
  "(transitive_on (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ bool) = transitive_on (mem_of S)"
  unfolding transitive_on_set_def by simp

lemma transitive_on_set_eq_transitive_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "transitive_on (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ bool ≡ transitive_on P"
  using assms by simp

lemma transitive_on_set_iff_transitive_on_pred [iff]:
  "transitive_on (S :: 'a set) (R :: 'a ⇒ 'a ⇒ bool) ⟷ transitive_on (mem_of S) R"
  by simp

lemma transp_eq_transitive [HOL_bin_rel_alignment]: "transp = transitive"
  by (intro ext) (blast intro: transpI dest: transpD)


subparagraph ‹Bi-Total›

lemma bi_total_on_set_eq_bi_total_on_pred [simp]:
  "(bi_total_on (S :: 'a set) (T :: 'b set) :: ('a ⇒ 'b ⇒ bool) ⇒ bool) =
    bi_total_on (mem_of S) (mem_of T)"
  by auto

lemma bi_total_on_set_eq_bi_total_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  and "Q ≡ mem_of T"
  shows "bi_total_on (S :: 'a set) (T :: 'b set) :: ('a ⇒ 'b ⇒ bool) ⇒ bool ≡ bi_total_on P Q"
  using assms by simp

lemma bi_total_on_set_iff_bi_total_on_pred [iff]:
  "bi_total_on (S :: 'a set) (T :: 'b set) (R :: 'a ⇒ 'b ⇒ bool) ⟷
    bi_total_on (mem_of S) (mem_of T) R"
  by simp

lemma Transfer_bi_total_eq_bi_total [HOL_bin_rel_alignment]:
  "Transfer.bi_total = Binary_Relations_Bi_Total.bi_total"
  unfolding bi_total_alt_def by (auto simp add: HOL_bin_rel_alignment)

subparagraph ‹Bi-Unique›

lemma bi_unique_on_set_eq_bi_unique_on_pred [simp]:
  "(bi_unique_on (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ bool) = bi_unique_on (mem_of S)"
  by auto

lemma bi_unique_on_set_eq_bi_unique_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "bi_unique_on (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ bool ≡ bi_unique_on P"
  using assms by simp

lemma bi_unique_on_set_iff_bi_unique_on_pred [iff]:
  "bi_unique_on (S :: 'a set) (R :: 'a ⇒ 'b ⇒ bool) ⟷ bi_unique_on (mem_of S) R"
  by simp

lemma Transfer_bi_unique_eq_bi_unique [HOL_bin_rel_alignment]:
  "Transfer.bi_unique = Binary_Relations_Bi_Unique.bi_unique"
  unfolding bi_unique_alt_def by (auto simp add: HOL_bin_rel_alignment)


paragraph ‹Functions›

lemma Domainp_eq_in_dom [HOL_bin_rel_alignment]: "Domainp = in_dom"
  by (intro ext) auto

lemma Rangep_eq_in_codom [HOL_bin_rel_alignment]: "Rangep = in_codom"
   by (intro ext) auto

lemma relcompp_eq_rel_comp [HOL_bin_rel_alignment]: "relcompp = rel_comp"
  by (intro ext) auto

lemma conversep_eq_rel_inv [HOL_bin_rel_alignment]: "conversep = rel_inv"
  by (intro ext) auto

lemma eq_onp_eq_eq_restrict [HOL_bin_rel_alignment]: "eq_onp = rel_restrict_left (=)"
  unfolding eq_onp_def by (intro ext) auto

definition "rel_restrict_left_set (R :: 'a ⇒ 'b ⇒ bool) (S :: 'a set) ≡ R↾⇘mem_of S⇙"
adhoc_overloading rel_restrict_left rel_restrict_left_set

definition "rel_restrict_right_set (R :: 'a ⇒ 'b ⇒ bool) (S :: 'b set) ≡ R↿⇘mem_of S⇙"
adhoc_overloading rel_restrict_right rel_restrict_right_set

lemma rel_restrict_left_set_eq_restrict_left_pred [simp]:
  "R↾⇘S⇙ = R↾⇘mem_of S⇙"
  unfolding rel_restrict_left_set_def by simp

lemma rel_restrict_left_set_eq_restrict_left_pred_uhint [uhint]:
  assumes "R ≡ R'"
  and "P ≡ mem_of S"
  shows "R↾⇘S⇙ ≡ R'↾⇘P⇙"
  using assms by simp

lemma restrict_left_set_iff_restrict_left_pred [iff]: "R↾⇘S⇙ x y ⟷ R↾⇘mem_of S⇙ x y"
  by simp

lemma rel_restrict_right_set_eq_restrict_right_pred [simp]:
  "R↿⇘S⇙ = R↿⇘mem_of S⇙"
  unfolding rel_restrict_right_set_def by simp

lemma rel_restrict_right_set_eq_restrict_right_pred_uhint [uhint]:
  assumes "R ≡ R'"
  and "P ≡ mem_of S"
  shows "R↿⇘S⇙ ≡ R'↿⇘P⇙"
  using assms by simp

lemma restrict_right_set_iff_restrict_right_pred [iff]: "R↿⇘S⇙ x y ⟷ R↿⇘mem_of S⇙ x y"
  by simp

end