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' : ℛ. R↾⇘P⇙ = 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' ⟹ R↾⇘P⇙ = 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 "R↾⇘P⇙ = 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