Theory Binary_Relations_Agree

✐‹creator "Kevin Kappelmann"›
subsection ‹Agreement›
theory Binary_Relations_Agree
  imports
    Functions_Monotone
begin

consts rel_agree_on :: "'a  'b  bool"

overloading
  rel_agree_on_pred  "rel_agree_on :: ('a  bool)  (('a  'b  bool)  bool)  bool"
begin
  definition "rel_agree_on_pred (P :: 'a  bool) ( :: ('a  'b  bool)  bool) 
    R R' : . RP= R'P⇙"
end

lemma rel_agree_onI [intro]:
  assumes "R R' x y.  R   R'  P x  R x y  R' x y"
  shows "rel_agree_on P "
  using assms unfolding rel_agree_on_pred_def by blast

lemma rel_agree_onE:
  assumes "rel_agree_on P "
  obtains "R R'.  R   R'  RP= R'P⇙"
  using assms unfolding rel_agree_on_pred_def by blast

lemma rel_restrict_left_eq_if_rel_agree_onI:
  assumes "rel_agree_on P "
  and " R" " R'"
  shows "RP= R'P⇙"
  using assms by (blast elim: rel_agree_onE)

lemma rel_agree_onD:
  assumes "rel_agree_on P "
  and " R" " R'"
  and "P x"
  and "R x y"
  shows "R' x y"
  using assms by (blast elim: rel_agree_onE dest: fun_cong)

lemma antimono_rel_agree_on:
  "((≤)  (≤)  (≥)) (rel_agree_on :: ('a  bool)  (('a  'b  bool)  bool)  bool)"
  by (intro mono_wrt_relI Fun_Rel_relI) (fastforce dest: rel_agree_onD)

lemma le_if_in_dom_le_if_rel_agree_onI:
  assumes "rel_agree_on A "
  and " R" " R'"
  and "in_dom R  A"
  shows "R  R'"
  using assms by (auto dest: rel_agree_onD[where ?R="R"])

lemma eq_if_in_dom_le_if_rel_agree_onI:
  assumes "rel_agree_on A "
  and " R" " R'"
  and "in_dom R  A" "in_dom R'  A"
  shows "R = R'"
  using assms le_if_in_dom_le_if_rel_agree_onI by blast

end