Theory Binary_Relations_Lattice

✐‹creator "Kevin Kappelmann"›
subsection ‹Lattice›
theory Binary_Relations_Lattice
  imports
    Binary_Relations_Order_Base
    HOL.Boolean_Algebras
begin

paragraph ‹Summary›
text ‹Basic results about the lattice structure on binary relations.›

lemma rel_infI [intro]:
  assumes "R x y"
  and "S x y"
  shows "(R ⊓ S) x y"
  using assms by (rule inf2I)

lemma rel_infE [elim]:
  assumes "(R ⊓ S) x y"
  obtains "R x y" "S x y"
  using assms by (rule inf2E)

lemma rel_infD:
  assumes "(R ⊓ S) x y"
  shows "R x y" and "S x y"
  using assms by auto

lemma in_dom_rel_infI [intro]:
  assumes "R x y"
  and "S x y"
  shows "in_dom (R ⊓ S) x"
  using assms by blast

lemma in_dom_rel_infE [elim]:
  assumes "in_dom (R ⊓ S) x"
  obtains y where "R x y" "S x y"
  using assms by blast

lemma in_codom_rel_infI [intro]:
  assumes "R x y"
  and "S x y"
  shows "in_codom (R ⊓ S) y"
  using assms by blast

lemma in_codom_rel_infE [elim]:
  assumes "in_codom (R ⊓ S) y"
  obtains x where "R x y" "S x y"
  using assms by blast

lemma in_field_eq_in_dom_sup_in_codom: "in_field L = (in_dom L ⊔ in_codom L)"
  by (intro ext) (simp add: in_field_iff_in_dom_or_in_codom)

lemma in_dom_rel_restrict_left_eq [simp]: "in_dom R↾⇘P⇙ = (in_dom R ⊓ P)"
  by (intro ext) auto

lemma in_codom_rel_restrict_left_eq [simp]: "in_codom R↿⇘P⇙ = (in_codom R ⊓ P)"
  by (intro ext) auto

lemma rel_restrict_left_restrict_left_eq [simp]:
  fixes R :: "'a ⇒ 'b ⇒ bool" and P Q :: "'a ⇒ bool"
  shows "R↾⇘P⇙↾⇘Q⇙ = R↾⇘P⇙ ⊓ R↾⇘Q⇙"
  by (intro ext iffI rel_restrict_leftI) auto

lemma rel_restrict_left_restrict_right_eq [simp]:
  fixes R :: "'a ⇒ 'b ⇒ bool" and P :: "'a ⇒ bool" and Q :: "'b ⇒ bool"
  shows "R↾⇘P⇙↿⇘Q⇙ = R↾⇘P⇙ ⊓ R↿⇘Q⇙"
  by (intro ext iffI rel_restrict_leftI rel_restrict_rightI) auto

lemma rel_restrict_right_restrict_left_eq [simp]:
  fixes R :: "'a ⇒ 'b ⇒ bool" and P :: "'b ⇒ bool" and Q :: "'a ⇒ bool"
  shows "R↿⇘P⇙↾⇘Q⇙ = R↿⇘P⇙ ⊓ R↾⇘Q⇙"
  by (intro ext iffI rel_restrict_leftI rel_restrict_rightI) auto

lemma rel_restrict_right_restrict_right_eq [simp]:
  fixes R :: "'a ⇒ 'b ⇒ bool" and P Q :: "'b ⇒ bool"
  shows "R↿⇘P⇙↿⇘Q⇙ = R↿⇘P⇙ ⊓ R↿⇘Q⇙"
  by (intro ext iffI) auto

lemma rel_restrict_left_sup_eq [simp]:
  "(R :: 'a ⇒ 'b ⇒ bool)↾⇘((P :: 'a ⇒ bool) ⊔ Q)⇙ = R↾⇘P⇙ ⊔ R↾⇘Q⇙ "
  by (intro antisym le_relI) (auto elim!: rel_restrict_leftE)

lemma rel_restrict_left_inf_eq [simp]:
  "(R :: 'a ⇒ 'b ⇒ bool)↾⇘((P :: 'a ⇒ bool) ⊓ Q)⇙ = R↾⇘P⇙ ⊓ R↾⇘Q⇙ "
  by (intro antisym le_relI) (auto elim!: rel_restrict_leftE)

lemma inf_rel_bimap_and_eq_restrict_left_restrict_right:
  "R ⊓ (rel_bimap P Q (∧)) = R↾⇘P⇙↿⇘Q⇙"
  by (intro ext) auto


end