Theory Dependent_Binary_Relations

✐‹creator "Kevin Kappelmann"›
subsection ‹Dependent Binary Relations›
theory Dependent_Binary_Relations
  imports
    Binary_Relations_Agree
begin

consts dep_bin_rel :: "'a ⇒ ('b ⇒ 'c) ⇒ 'd"
consts bin_rel :: "'a ⇒ 'b ⇒ 'c"

bundle bin_rel_syntax
begin
syntax "_dep_bin_rel" :: ‹idt ⇒ 'a ⇒ 'b ⇒ 'c› ("{∑}_ : _./ _" [51, 50, 50] 51)
notation bin_rel (infixr "{×}" 51)
end
bundle no_bin_rel_syntax
begin
no_syntax "_dep_bin_rel" :: ‹idt ⇒ 'a ⇒ 'b ⇒ 'c› ("{∑}_ : _./ _" [51, 50, 50] 51)
no_notation bin_rel (infixr "{×}" 51)
end
unbundle bin_rel_syntax
translations
  "{∑}x : A. B" ⇌ "CONST dep_bin_rel A (λx. B)"

definition "dep_bin_rel_pred (A :: 'a ⇒ bool) (B :: 'a ⇒ 'b ⇒ bool) (R :: 'a ⇒ 'b ⇒ bool) ≡
  ∀x y. R x y ⟶ A x ∧ B x y"
adhoc_overloading dep_bin_rel dep_bin_rel_pred

definition "bin_rel_pred (A :: 'a ⇒ bool) (B :: 'b ⇒ bool) :: ('a ⇒ 'b ⇒ bool) ⇒ bool ≡
  {∑}(_ :: 'a) : A. B"
adhoc_overloading bin_rel bin_rel_pred

lemma bin_rel_pred_eq_dep_bin_rel_pred: "A {×} B = {∑}_ : A. B"
  unfolding bin_rel_pred_def by auto

lemma bin_rel_pred_eq_dep_bin_rel_pred_uhint [uhint]:
  assumes "A ≡ A'"
  and "⋀x. B ≡ B' x"
  shows "A {×} B ≡ {∑}x : A'. B' x"
  using assms by (simp add: bin_rel_pred_eq_dep_bin_rel_pred)

lemma bin_rel_pred_iff_dep_bin_rel_pred: "(A {×} B) R ⟷ ({∑}_ : A. B) R"
  unfolding bin_rel_pred_eq_dep_bin_rel_pred by auto

lemma dep_bin_relI [intro]:
  assumes "⋀x y. R x y ⟹ A x"
  and "⋀x y. R x y ⟹ A x ⟹ B x y"
  shows "({∑}x : A. B x) R"
  using assms unfolding dep_bin_rel_pred_def by auto

lemma dep_bin_rel_if_bin_rel_and:
  assumes "⋀x y. R x y ⟹ A x ∧ B x y"
  shows "({∑}x : A. B x) R"
  using assms by auto

lemma dep_bin_relE [elim]:
  assumes "({∑}x : A. B x) R"
  and "R x y"
  obtains "A x" "B x y"
  using assms unfolding dep_bin_rel_pred_def by auto

lemma dep_bin_relE':
  assumes "({∑}x : A. B x) R"
  obtains "⋀x y. R x y ⟹ A x ∧ B x y"
  using assms by auto

lemma bin_relI [intro]:
  assumes "⋀x y. R x y ⟹ A x"
  and "⋀x y. R x y ⟹ A x ⟹ B y"
  shows "(A {×} B) R"
  using assms by (urule dep_bin_relI where chained = fact)

lemma bin_rel_if_bin_rel_and:
  assumes "⋀x y. R x y ⟹ A x ∧ B y"
  shows "(A {×} B) R"
  using assms by (urule dep_bin_rel_if_bin_rel_and)

lemma bin_relE [elim]:
  assumes "(A {×} B) R"
  and "R x y"
  obtains "A x" "B y"
  using assms by (urule (e) dep_bin_relE)

lemma bin_relE':
  assumes "(A {×} B) R"
  obtains "⋀x y. R x y ⟹ A x ∧ B y"
  using assms by (urule (e) dep_bin_relE')

lemma dep_bin_rel_cong [cong]:
  "⟦A = A'; ⋀x. A' x ⟹ B x = B' x⟧ ⟹ ({∑}x : A. B x) = {∑}x : A'. B' x"
  by (intro ext iffI dep_bin_relI) fastforce+

lemma le_dep_bin_rel_if_le_dom:
  assumes "A ≤ A'"
  shows "({∑}x : A. B x) ≤ ({∑}x : A'. B x)"
  using assms by (intro le_predI dep_bin_relI) auto

lemma dep_bin_rel_covariant_codom:
  assumes "({∑}x : A. B x) R"
  and "⋀x y. R x y ⟹ A x ⟹ B x y ⟹ B' x y"
  shows "({∑}x : A. B' x) R"
  using assms by (intro dep_bin_relI) auto

lemma mono_dep_bin_rel: "((≤) ⇒ (≤) ⇛ (≥) ⇛ (≤)) dep_bin_rel"
  by (intro mono_wrt_relI Fun_Rel_relI dep_bin_relI) force

lemma mono_bin_rel: "((≤) ⇒ (≤) ⇛ (≥) ⇛ (≤)) ({×})"
  by (intro mono_wrt_relI Fun_Rel_relI) auto

lemma in_dom_le_if_dep_bin_rel:
  assumes "({∑}x : A. B x) R"
  shows "in_dom R ≤ A"
  using assms by auto

lemma in_codom_le_in_codom_on_if_dep_bin_rel:
  assumes "({∑}x : A. B x) R"
  shows "in_codom R ≤ in_codom_on A B"
  using assms by fast

lemma rel_restrict_left_eq_self_if_dep_bin_rel [simp]:
  assumes "({∑}x : A. B x) R"
  shows "R↾⇘A⇙ = R"
  using assms rel_restrict_left_eq_self_if_in_dom_le by auto

lemma dep_bin_rel_bottom_dom_iff_eq_bottom [iff]: "({∑}x : ⊥. B x) R ⟷ R = ⊥"
  by fastforce

lemma dep_bin_rel_bottom_codom_iff_eq_bottom [iff]: "({∑}x : A. ⊥) R ⟷ R = ⊥"
  by fastforce

lemma mono_bin_rel_dep_bin_rel_bin_rel_in_codom_on_rel_comp:
  "(A {×} B ⇒ ({∑}x : B. C x) ⇒ A {×} in_codom_on B C) (∘∘)"
  by fastforce

lemma mono_bin_rel_bin_rel_bin_rel_rel_comp: "(A {×} B ⇒ B {×} C ⇒ A {×} C) (∘∘)"
  by fast

lemma mono_dep_bin_rel_bin_rel_rel_inv: "(({∑}x : A. B x) ⇒ in_codom_on A B {×} A) rel_inv"
  by force

lemma mono_bin_rel_rel_inv: "(A {×} B ⇒ B {×} A) rel_inv"
  by auto

lemma mono_dep_bin_rel_top_dep_bin_rel_inf_rel_restrict_left:
  "(({∑}x : A. B x) ⇒ (P : ⊤) ⇒ ({∑}x : A ⊓ P. B x)) rel_restrict_left"
  by fast

lemma mono_dep_bin_rel_top_dep_bin_rel_inf_rel_restrict_right:
  "(({∑}x : A. B x) ⇒ (P : ⊤) ⇒ ({∑}x : A. B x ⊓ P)) rel_restrict_right"
  by fast

lemma le_if_rel_agree_on_if_dep_bin_relI:
  assumes "({∑}x : A. B x) R"
  and "rel_agree_on A ℛ"
  and "ℛ R" "ℛ R'"
  shows "R ≤ R'"
  using assms by (intro le_if_in_dom_le_if_rel_agree_onI in_dom_le_if_dep_bin_rel)

lemma eq_if_rel_agree_on_if_dep_bin_relI:
  assumes "({∑}x : A. B x) R" "({∑}x : A. B' x) R'"
  and "rel_agree_on A ℛ"
  and "ℛ R" "ℛ R'"
  shows "R = R'"
  using assms by (intro eq_if_in_dom_le_if_rel_agree_onI in_dom_le_if_dep_bin_rel)


end