Theory Binary_Relation_Functions

✐‹creator "Kevin Kappelmann"›
section ‹Binary Relations›
subsection ‹Basic Functions›
theory Binary_Relation_Functions
  imports
    Bounded_Quantifiers
    ML_Unification.Unify_Resolve_Tactics
begin

paragraph ‹Summary›
text ‹Basic functions on binary relations.›

subsubsection ‹Domain, Codomain, and Field›

definition "in_dom R x ≡ ∃y. R x y"

lemma in_domI [intro]:
  assumes "R x y"
  shows "in_dom R x"
  using assms unfolding in_dom_def by blast

lemma in_domE [elim]:
  assumes "in_dom R x"
  obtains y where "R x y"
  using assms unfolding in_dom_def by blast

lemma in_dom_bottom_eq_bottom [simp]: "in_dom ⊥ = ⊥" by fastforce
lemma in_dom_top_eq_top [simp]: "in_dom ⊤ = ⊤" by fastforce

lemma in_dom_sup_eq_in_dom_sup_in_dom [simp]: "in_dom (R ⊔ S) = in_dom R ⊔ in_dom S" by fastforce

consts in_codom_on :: "'a ⇒ 'b ⇒ 'c ⇒ bool"

definition "in_codom_on_pred (P :: 'a ⇒ bool) R y ≡ ∃x : P. R x y"
adhoc_overloading in_codom_on in_codom_on_pred

lemma in_codom_onI [intro]:
  assumes "R x y"
  and "P x"
  shows "in_codom_on P R y"
  using assms unfolding in_codom_on_pred_def by blast

lemma in_codom_onE [elim]:
  assumes "in_codom_on P R y"
  obtains x where "P x" "R x y"
  using assms unfolding in_codom_on_pred_def by blast

lemma in_codom_on_pred_iff_bex_rel: "in_codom_on P R y ⟷ (∃x : P. R x y)" by blast

lemma in_codom_bottom_pred_eq_bottom [simp]: "in_codom_on ⊥ = ⊥" by fastforce
lemma in_codom_bottom_rel_eq_bottom [simp]: "in_codom_on P ⊥ = ⊥" by fastforce
lemma in_codom_top_top_eq [simp]: "in_codom_on ⊤ ⊤ = ⊤" by fastforce

lemma in_codom_on_eq_pred_eq [simp]: "in_codom_on ((=) P) R = R P"
  by auto

lemma in_codom_on_sup_pred_eq_in_codom_on_sup_in_codom_on [simp]:
  "in_codom_on (P ⊔ Q) = in_codom_on P ⊔ in_codom_on Q"
  by fastforce

lemma in_codom_on_sup_rel_eq_in_codom_on_sup_in_codom_on [simp]:
  "in_codom_on P (R ⊔ S) = in_codom_on P R ⊔ in_codom_on P S"
  by fastforce

definition "in_codom ≡ in_codom_on (⊤ :: 'a ⇒ bool)"

lemma in_codom_eq_in_codom_on_top: "in_codom = in_codom_on ⊤" unfolding in_codom_def by auto

lemma in_codom_eq_in_codom_on_top_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  shows "in_codom ≡ in_codom_on P"
  using assms by (simp add: in_codom_eq_in_codom_on_top)

lemma in_codomI [intro]:
  assumes "R x y"
  shows "in_codom R y"
  using assms by (urule in_codom_onI) simp

lemma in_codomE [elim]:
  assumes "in_codom R y"
  obtains x where "R x y"
  using assms by (urule (e) in_codom_onE)

definition "in_field R x ≡ in_dom R x ∨ in_codom R x"

lemma in_field_if_in_dom:
  assumes "in_dom R x"
  shows "in_field R x"
  unfolding in_field_def using assms by blast

lemma in_field_if_in_codom:
  assumes "in_codom R x"
  shows "in_field R x"
  unfolding in_field_def using assms by blast

lemma in_fieldE [elim]:
  assumes "in_field R x"
  obtains (in_dom) x' where "R x x'" | (in_codom) x' where "R x' x"
  using assms unfolding in_field_def by blast

lemma in_fieldE':
  assumes "in_field R x"
  obtains (in_dom) "in_dom R x" | (in_codom) "in_codom R x"
  using assms by blast

lemma in_fieldI [intro]:
  assumes "R x y"
  shows "in_field R x" "in_field R y"
  using assms by (auto intro: in_field_if_in_dom in_field_if_in_codom)

lemma in_field_iff_in_dom_or_in_codom:
  "in_field R x ⟷ in_dom R x ∨ in_codom R x"
  by blast

lemma in_field_eq_in_dom_if_in_codom_eq_in_dom:
  assumes "in_codom R = in_dom R"
  shows "in_field R = in_dom R"
  using assms by (intro ext) (auto elim: in_fieldE')

lemma in_field_bottom_eq_bottom [simp]: "in_field ⊥ = ⊥" by fastforce
lemma in_field_top_eq_top [simp]: "in_field ⊤ = ⊤" by fastforce

lemma in_field_sup_eq_in_field_sup_in_field [simp]: "in_field (R ⊔ S) = in_field R ⊔ in_field S"
  by fastforce

subsubsection ‹Composition›

consts rel_comp :: "'a ⇒ 'b ⇒ 'c"

open_bundle rel_comp_syntax
begin
notation rel_comp (infixl ‹∘∘› 55)
end

definition "rel_comp_rel R S x y ≡ ∃z. R x z ∧ S z y"
adhoc_overloading rel_comp rel_comp_rel

lemma rel_compI [intro]:
  assumes "R x y"
  and "S y z"
  shows "(R ∘∘ S) x z"
  using assms unfolding rel_comp_rel_def by blast

lemma rel_compE [elim]:
  assumes "(R ∘∘ S) x y"
  obtains z where "R x z" "S z y"
  using assms unfolding rel_comp_rel_def by blast

lemma rel_comp_assoc: "R ∘∘ (S ∘∘ T) = (R ∘∘ S) ∘∘ T"
  by (intro ext) blast

lemma in_dom_if_in_dom_rel_comp:
  assumes "in_dom (R ∘∘ S) x"
  shows "in_dom R x"
  using assms by blast

lemma in_codom_if_in_codom_rel_comp:
  assumes "in_codom (R ∘∘ S) y"
  shows "in_codom S y"
  using assms by blast

lemma in_field_compE [elim]:
  assumes "in_field (R ∘∘ S) x"
  obtains (in_dom) "in_dom R x" | (in_codom) "in_codom S x"
  using assms by blast


subsubsection ‹Inverse›

consts rel_inv :: "'a ⇒ 'b"

open_bundle rel_inv_syntax
begin
notation rel_inv (‹(_¯)› [1000])
end

definition rel_inv_rel :: "('a ⇒ 'b ⇒ bool) ⇒ 'b ⇒ 'a ⇒ bool"
  where "rel_inv_rel R x y ≡ R y x"
adhoc_overloading rel_inv rel_inv_rel

lemma rel_invI [intro]:
  assumes "R x y"
  shows "R¯ y x"
  using assms unfolding rel_inv_rel_def .

lemma rel_invD [dest]:
  assumes "R¯ x y"
  shows "R y x"
  using assms unfolding rel_inv_rel_def .

lemma rel_inv_iff_rel [simp]: "R¯ x y ⟷ R y x"
  by blast

lemma in_dom_rel_inv_eq_in_codom [simp]: "in_dom R¯ = in_codom R"
  by (intro ext) blast

lemma in_codom_rel_inv_eq_in_dom [simp]: "in_codom R¯ = in_dom R"
  by (intro ext) blast

lemma in_field_rel_inv_eq_in_field [simp]: "in_field R¯ = in_field R"
  by (intro ext) auto

lemma rel_inv_comp_eq [simp]: "(R ∘∘ S)¯ = S¯ ∘∘ R¯"
  by (intro ext) blast

lemma rel_inv_inv_eq_self [simp]: "R¯¯ = R"
  by blast

lemma rel_inv_eq_iff_eq [iff]: "R¯ = S¯ ⟷ R = S"
  by (blast dest: fun_cong)

lemma rel_inv_le_rel_inv_iff [iff]: "R¯ ≤ S¯ ⟷ R ≤ S"
  by (blast intro: predicate2I dest: predicate2D)

lemma rel_inv_top_eq [simp]: "⊤¯ = ⊤" by fastforce
lemma rel_inv_bottom_eq [simp]: "⊥¯ = ⊥" by fastforce

subsubsection ‹Restrictions›

consts rel_if :: "bool ⇒ 'a ⇒ 'a"

open_bundle rel_if_syntax
begin
notation (output) rel_if (infixl ‹⟶› 50)
end

definition "rel_if_rel B R x y ≡ B ⟶ R x y"
adhoc_overloading rel_if rel_if_rel

lemma rel_if_eq_rel_if_pred [simp]:
  assumes "B"
  shows "(rel_if B R) = R"
  unfolding rel_if_rel_def using assms by blast

lemma rel_if_eq_top_if_not_pred [simp]:
  assumes "¬B"
  shows "(rel_if B R) = (λ_ _. True)"
  unfolding rel_if_rel_def using assms by blast

lemma rel_if_if_impI [intro]:
  assumes "B ⟹ R x y"
  shows "(rel_if B R) x y"
  unfolding rel_if_rel_def using assms by blast

lemma rel_ifE [elim]:
  assumes "(rel_if B R) x y"
  obtains "¬B" | "B" "R x y"
  using assms unfolding rel_if_rel_def by blast

lemma rel_ifD:
  assumes "(rel_if B R) x y"
  and "B"
  shows "R x y"
  using assms by blast

consts rel_restrict_left :: "'a ⇒ 'b ⇒ 'a"
consts rel_restrict_right :: "'a ⇒ 'b ⇒ 'a"
consts rel_restrict :: "'a ⇒ 'b ⇒ 'a"

open_bundle rel_restrict_syntax
begin
notation rel_restrict_left (‹(_)↾(⇘_⇙)› [1000])
notation rel_restrict_right (‹(_)↿(⇘_⇙)› [1000])
notation rel_restrict (‹(_)↑(⇘_⇙)› [1000])
end

definition "rel_restrict_left_pred R P x y ≡ P x ∧ R x y"
adhoc_overloading rel_restrict_left rel_restrict_left_pred
definition "rel_restrict_right_pred R P x y ≡ P y ∧ R x y"
adhoc_overloading rel_restrict_right rel_restrict_right_pred
definition "rel_restrict_pred R P ≡ R↾⇘P⇙↿⇘P⇙"
adhoc_overloading rel_restrict rel_restrict_pred

lemma rel_restrict_leftI [intro]:
  assumes "R x y"
  and "P x"
  shows "R↾⇘P⇙ x y"
  using assms unfolding rel_restrict_left_pred_def by blast

lemma rel_restrict_leftE [elim]:
  assumes "R↾⇘P⇙ x y"
  obtains "P x" "R x y"
  using assms unfolding rel_restrict_left_pred_def by blast

lemma rel_restrict_left_cong:
  assumes "⋀x. P x ⟷ P' x"
  and "⋀x y. P' x ⟹ R x y ⟷ R' x y"
  shows "R↾⇘P⇙ = R'↾⇘P'⇙"
  using assms by (intro ext iffI) blast+

lemma rel_restrict_left_restrict_left_eq_restrict_left [simp]: "R↾⇘P⇙↾⇘P⇙ = R↾⇘P⇙"
  by blast

lemma rel_restrict_left_top_eq [simp]: "(R :: 'a ⇒ 'b ⇒ bool)↾⇘⊤ :: 'a ⇒ bool⇙ = R"
  by (intro ext rel_restrict_leftI) auto

lemma rel_restrict_left_top_eq_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  shows "(R :: 'a ⇒ 'b ⇒ bool)↾⇘P⇙ ≡ R"
  using assms by simp

lemma rel_restrict_left_bottom_eq [simp]: "(R :: 'a ⇒ 'b ⇒ bool)↾⇘⊥ :: 'a ⇒ bool⇙ = ⊥"
  by (intro ext rel_restrict_leftI) auto

lemma bottom_restrict_left_eq [simp]: "⊥↾⇘P :: 'a ⇒ bool⇙ = ⊥"
  by fastforce

lemma rel_restrict_left_le_self: "(R :: 'a ⇒ 'b ⇒ bool)↾⇘(P :: 'a ⇒ bool)⇙ ≤ R"
  by (blast intro: predicate2I dest: predicate2D)

lemma le_rel_restrict_left_self_if_in_dom_le:
  assumes "in_dom R ≤ P"
  shows "R ≤ (R :: 'a ⇒ 'b ⇒ bool)↾⇘(P :: 'a ⇒ bool)⇙"
  using assms by (blast intro: predicate2I dest: predicate2D predicate1D)

corollary rel_restrict_left_eq_self_if_in_dom_le [simp]:
  assumes "in_dom R ≤ P"
  shows "R↾⇘P⇙ = R"
  using assms rel_restrict_left_le_self le_rel_restrict_left_self_if_in_dom_le by (intro antisym)

lemma ex_rel_restrict_left_iff_in_codom_on [iff]: "(∃x. R↾⇘P⇙ x y) ⟷ (in_codom_on P R y)" by blast

lemma in_dom_rel_restrict_leftI [intro]:
  assumes "R x y"
  and "P x"
  shows "in_dom R↾⇘P⇙ x"
  using assms by blast

lemma in_codom_rel_restrict_leftI [intro]:
  assumes "R x y"
  and "P x"
  shows "in_codom R↾⇘P⇙ y"
  using assms by blast


lemma rel_restrict_rightI [intro]:
  assumes "R x y"
  and "P y"
  shows "R↿⇘P⇙ x y"
  using assms unfolding rel_restrict_right_pred_def by blast

lemma rel_restrict_rightE [elim]:
  assumes "R↿⇘P⇙ x y"
  obtains "P y" "R x y"
  using assms unfolding rel_restrict_right_pred_def by blast

lemma rel_restrict_right_cong:
  assumes "⋀y. P y ⟷ P' y"
  and "⋀x y. P' y ⟹ R x y ⟷ R' x y"
  shows "R↿⇘P⇙ = R'↿⇘P'⇙"
  using assms by (intro ext iffI) blast+

lemma rel_restrict_right_restrict_right_eq_restrict_right [simp]: "R↿⇘P⇙↿⇘P⇙ = R↿⇘P⇙"
  by blast

lemma rel_restrict_right_top_eq [simp]: "(R :: 'a ⇒ 'b ⇒ bool)↿⇘⊤ ::'b ⇒ bool⇙ = R"
  by (intro ext rel_restrict_rightI) auto

lemma rel_restrict_right_top_eq_uhint [uhint]:
  assumes "P ≡ (⊤ ::'b ⇒ bool)"
  shows "(R :: 'a ⇒ 'b ⇒ bool)↿⇘P⇙ ≡ R"
  using assms by simp

lemma rel_restrict_right_bottom_eq [simp]: "(R :: 'a ⇒ 'b ⇒ bool)↿⇘⊥ :: 'b ⇒ bool⇙ = ⊥"
  by (intro ext rel_restrict_rightI) auto

lemma bottom_restrict_right_eq [simp]: "⊥↿⇘P :: 'b ⇒ bool⇙ = ⊥"
  by fastforce

lemma rel_restrict_right_le_self: "(R :: 'a ⇒ 'b ⇒ bool)↿⇘(P :: 'b ⇒ bool)⇙ ≤ R"
  by (blast intro: predicate2I dest: predicate2D)

lemma le_rel_restrict_right_self_if_in_codom_le:
  assumes "in_codom R ≤ P"
  shows "R ≤ (R :: 'a ⇒ 'b ⇒ bool)↿⇘(P :: 'b ⇒ bool)⇙"
  using assms by (blast intro: predicate2I dest: predicate2D predicate1D)

corollary rel_restrict_right_eq_self_if_in_codom_le [simp]:
  assumes "in_codom R ≤ P"
  shows "R↿⇘P⇙ = R"
  using assms rel_restrict_right_le_self le_rel_restrict_right_self_if_in_codom_le
  by (intro antisym)

context
  fixes R :: "'a ⇒ 'b ⇒ bool"
begin

lemma rel_restrict_right_eq: "R↿⇘P :: 'b ⇒ bool⇙ = ((R¯)↾⇘P⇙)¯"
  by blast

lemma rel_inv_restrict_right_rel_inv_eq_restrict_left [simp]: "((R¯)↿⇘P :: 'a ⇒ bool⇙)¯ = R↾⇘P⇙"
  by blast

lemma rel_restrict_right_iff_restrict_left: "R↿⇘P :: 'b ⇒ bool⇙ x y ⟷ (R¯)↾⇘P⇙ y x"
  unfolding rel_restrict_right_eq by simp

end

lemma rel_inv_rel_restrict_left_inv_rel_restrict_left_eq:
  fixes R :: "'a ⇒ 'b ⇒ bool" and P :: "'a ⇒ bool" and Q :: "'b ⇒ bool"
  shows "(((R↾⇘P⇙)¯)↾⇘Q⇙)¯ = (((R¯)↾⇘Q⇙)¯)↾⇘P⇙"
  by (intro ext iffI rel_restrict_leftI rel_invI) auto

lemma rel_restrict_left_right_eq_restrict_right_left:
  fixes R :: "'a ⇒ 'b ⇒ bool" and P :: "'a ⇒ bool" and Q :: "'b ⇒ bool"
  shows "R↾⇘P⇙↿⇘Q⇙ = R↿⇘Q⇙↾⇘P⇙"
  unfolding rel_restrict_right_eq
  by (fact rel_inv_rel_restrict_left_inv_rel_restrict_left_eq)

lemma rel_restrictI [intro]:
  assumes "R↾⇘P⇙↿⇘P⇙ x y"
  shows "R↑⇘P⇙ x y"
  using assms unfolding rel_restrict_pred_def by blast

lemma rel_restrictD [dest!]:
  assumes "R↑⇘P⇙ x y"
  shows "R↾⇘P⇙↿⇘P⇙ x y"
  using assms unfolding rel_restrict_pred_def by blast

lemma rel_restrict_eq_restrict_left_right [simp]: "R↑⇘P⇙ = R↾⇘P⇙↿⇘P⇙"
  by (intro ext) auto

lemma rel_restrict_cong:
  assumes "⋀y. P y ⟷ P' y"
  and "⋀x y. P' x ⟹ P' y ⟹ R x y ⟷ R' x y"
  shows "R↑⇘P⇙ = R'↑⇘P'⇙"
  using assms by (intro ext) fast

lemma rel_restrict_restrict_eq_restrict [simp]: "R↑⇘P⇙↑⇘P⇙ = R↑⇘P⇙"
  by blast

lemma rel_restrict_top_eq [simp]: "(R :: 'a ⇒ 'a ⇒ bool)↑⇘⊤ :: 'a ⇒ bool⇙ = R"
  by (intro ext rel_restrictI) auto

lemma rel_restrict_top_eq_uhint [uhint]:
  assumes "P ≡ (⊤ ::'a ⇒ bool)"
  shows "(R :: 'a ⇒ 'a ⇒ bool)↑⇘P⇙ ≡ R"
  using assms by simp

lemma rel_restrict_bottom_eq [simp]: "(R :: 'a ⇒ 'a ⇒ bool)↑⇘⊥ :: 'a ⇒ bool⇙ = ⊥"
  by (intro ext rel_restrictI) auto

lemma bottom_restrict_eq [simp]: "⊥↑⇘P :: 'a ⇒ bool⇙ = ⊥"
  by fastforce

lemma rel_restrict_le_self: "(R :: 'a ⇒ 'a ⇒ bool)↑⇘(P :: 'a ⇒ bool)⇙ ≤ R"
  by (auto intro: predicate2I dest: predicate2D)

lemma le_rel_restrict_self_if_in_field_le:
  assumes "in_field R ≤ P"
  shows "R ≤ (R :: 'a ⇒ 'a ⇒ bool)↑⇘(P :: 'a ⇒ bool)⇙"
  using assms by (blast intro: predicate2I dest: predicate2D predicate1D)

corollary rel_restrict_eq_self_if_in_field_le [simp]:
  assumes "in_field R ≤ P"
  shows "R↑⇘P⇙ = R"
  using assms rel_restrict_le_self le_rel_restrict_self_if_in_field_le
  by (intro antisym)


subsubsection ‹Mappers›

definition "rel_bimap f g (R :: 'a ⇒ 'b ⇒ bool) x y ≡ R (f x) (g y)"

lemma rel_bimap_eq [simp]: "rel_bimap f g R x y = R (f x) (g y)"
  unfolding rel_bimap_def by simp

definition "rel_map f R ≡ rel_bimap f f R"

lemma rel_bimap_self_eq_rel_map [simp]: "rel_bimap f f R = rel_map f R"
  unfolding rel_map_def by simp

lemma rel_map_eq [simp]: "rel_map f R x y = R (f x) (f y)"
  by (simp only: rel_bimap_self_eq_rel_map[symmetric] rel_bimap_eq)

end