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  bool"
consts bin_rel :: "'a  'b  'c  bool"

bundle bin_rel_syntax
begin
syntax "_dep_bin_rel" :: idt  'a  'b  'c  'd ("{∑}_ : _./ _" [41, 41, 40] 51)
notation bin_rel (infixl "{×}" 51)
end
bundle no_bin_rel_syntax
begin
no_syntax "_dep_bin_rel" :: idt  'a  'b  'c  'd ("{∑}_ : _./ _" [41, 41, 40] 51)
no_notation bin_rel (infixl "{×}" 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 "B'  (λ_. B)"
  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: "((≤) m (≤)  (≥)  (≤)) dep_bin_rel"
  by (intro mono_wrt_relI Fun_Rel_relI dep_bin_relI) force

lemma mono_bin_rel: "((≤) m (≤)  (≥)  (≤)) ({×})"
  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 "RA= 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_rel_comp:
  "(A {×} B m ({∑}x : B. C x) m A {×} in_codom_on B C) (∘∘)"
  by fastforce

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

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

lemma mono_dep_bin_rel_top_dep_bin_rel_inf_rel_restrict_left:
  "(({∑}x : A. B x) m (P : ) m ({∑}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) m (P : ) m ({∑}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