# Theory Relations

```subsection ‹Local versions of relations›

theory Relations
imports
"HOL-Library.Multiset"
"Abstract-Rewriting.Abstract_Rewriting"
begin

text‹Common predicates on relations›

definition compatible_l :: "'a rel ⇒ 'a rel ⇒ bool" where
"compatible_l R1 R2 ≡ R1 O R2 ⊆ R2"

definition compatible_r :: "'a rel ⇒ 'a rel ⇒ bool" where
"compatible_r R1 R2 ≡ R2 O R1 ⊆ R2"

text‹Local reflexivity›

definition locally_refl :: "'a rel ⇒ 'a multiset ⇒ bool" where
"locally_refl R A ≡ (∀ a. a ∈# A ⟶ (a,a) ∈ R)"

definition locally_irrefl :: "'a rel ⇒ 'a multiset ⇒ bool" where
"locally_irrefl R A ≡ (∀t. t ∈# A ⟶ (t,t) ∉ R)"

text‹Local symmetry›

definition locally_sym :: "'a rel ⇒ 'a multiset ⇒ bool" where
"locally_sym R A ≡ (∀t u. t ∈# A ⟶ u ∈# A ⟶
(t,u) ∈ R ⟶ (u,t) ∈ R)"

definition locally_antisym :: "'a rel ⇒ 'a multiset ⇒ bool" where
"locally_antisym R A ≡ (∀t u. t ∈# A ⟶ u ∈# A ⟶
(t,u) ∈ R ⟶ (u,t) ∈ R ⟶ t = u)"

text‹Local transitivity›

definition locally_trans :: "'a rel ⇒ 'a multiset ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
"locally_trans R A B C ≡ (∀t u v.
t ∈# A ⟶ u ∈# B ⟶ v ∈# C ⟶
(t,u) ∈ R ⟶ (u,v) ∈ R ⟶ (t,v) ∈ R)"

text‹Local inclusion›

definition locally_included :: "'a rel ⇒ 'a rel ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
"locally_included R1 R2 A B ≡ (∀t u. t ∈# A ⟶ u ∈# B ⟶
(t,u) ∈ R1 ⟶  (t,u) ∈ R2)"

text‹Local transitivity compatibility›

definition locally_compatible_l :: "'a rel ⇒ 'a rel ⇒ 'a multiset ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
"locally_compatible_l R1 R2 A B C ≡ (∀t u v. t ∈# A ⟶ u ∈# B ⟶ v ∈# C ⟶
(t,u) ∈ R1 ⟶ (u,v) ∈ R2 ⟶ (t,v) ∈ R2)"

definition locally_compatible_r :: "'a rel ⇒ 'a rel ⇒ 'a multiset ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
"locally_compatible_r R1 R2 A B C ≡ (∀t u v. t ∈# A ⟶ u ∈# B ⟶ v ∈# C ⟶
(t,u) ∈ R2 ⟶ (u,v) ∈ R1 ⟶ (t,v) ∈ R2)"

text‹included + compatible \$\longrightarrow\$  transitive›

lemma in_cl_tr:
assumes "R1 ⊆ R2"
and "compatible_l R2 R1"
shows "trans R1"
proof-
{
fix x y z
assume s_x_y: "(x,y) ∈ R1" and s_y_z: "(y,z) ∈ R1"
from assms s_x_y have "(x,y) ∈ R2" by auto
with s_y_z assms(2)[unfolded compatible_l_def]  have "(x,z) ∈ R1" by blast
}
then show ?thesis unfolding trans_def by fast
qed

lemma in_cr_tr:
assumes "R1 ⊆ R2"
and "compatible_r R2 R1"
shows "trans R1"
proof-
{
fix x y z
assume s_x_y: "(x,y) ∈ R1" and s_y_z: "(y,z) ∈ R1"
with assms have "(y,z) ∈ R2" by auto
with s_x_y assms(2)[unfolded compatible_r_def] have "(x,z) ∈ R1" by blast
}
then show ?thesis unfolding trans_def by fast
qed

text‹If a property holds globally, it also holds locally. Obviously.›

lemma r_lr:
assumes "refl R"
shows "locally_refl R A"
using assms unfolding refl_on_def locally_refl_def by blast

lemma tr_ltr:
assumes "trans R"
shows "locally_trans R A B C"
using assms unfolding trans_def and locally_trans_def by fast

lemma in_lin:
assumes "R1 ⊆ R2"
shows "locally_included R1 R2 A B"
using assms unfolding locally_included_def by auto

lemma cl_lcl:
assumes "compatible_l R1 R2"
shows "locally_compatible_l R1 R2 A B C"
using assms unfolding compatible_l_def and locally_compatible_l_def by auto

lemma cr_lcr:
assumes "compatible_r R1 R2"
shows "locally_compatible_r R1 R2 A B C"
using assms unfolding compatible_r_def and locally_compatible_r_def by auto

text‹If a predicate holds on a set then it holds on
all the subsets:›

lemma lr_trans_l:
assumes "locally_refl R (A + B)"
shows "locally_refl R A"
using assms unfolding locally_refl_def
by auto

lemma li_trans_l:
assumes "locally_irrefl R (A + B)"
shows "locally_irrefl R A"
using assms unfolding locally_irrefl_def
by auto

lemma ls_trans_l:
assumes "locally_sym R (A + B)"
shows "locally_sym R A"
using assms unfolding locally_sym_def
by auto

lemma las_trans_l:
assumes "locally_antisym R (A + B)"
shows "locally_antisym R A"
using assms unfolding locally_antisym_def
by auto

lemma lt_trans_l:
assumes "locally_trans R (A + B) (C + D) (E + F)"
shows "locally_trans R A C E"
using assms[unfolded locally_trans_def, rule_format]
unfolding locally_trans_def by auto

lemma lin_trans_l:
assumes "locally_included R1 R2 (A + B) (C + D)"
shows "locally_included R1 R2 A C"
using assms unfolding locally_included_def by auto

lemma lcl_trans_l:
assumes "locally_compatible_l R1 R2 (A + B) (C + D) (E + F)"
shows "locally_compatible_l R1 R2 A C E"
using assms[unfolded locally_compatible_l_def, rule_format]
unfolding locally_compatible_l_def by auto

lemma lcr_trans_l:
assumes "locally_compatible_r R1 R2 (A + B) (C + D) (E + F)"
shows "locally_compatible_r R1 R2 A C E"
using assms[unfolded locally_compatible_r_def, rule_format]
unfolding locally_compatible_r_def by auto

lemma lr_trans_r:
assumes "locally_refl R (A + B)"
shows "locally_refl R B"
using assms unfolding locally_refl_def
by auto

lemma li_trans_r:
assumes "locally_irrefl R (A + B)"
shows "locally_irrefl R B"
using assms unfolding locally_irrefl_def
by auto

lemma ls_trans_r:
assumes "locally_sym R (A + B)"
shows "locally_sym R B"
using assms unfolding locally_sym_def
by auto

lemma las_trans_r:
assumes "locally_antisym R (A + B)"
shows "locally_antisym R B"
using assms unfolding locally_antisym_def
by auto

lemma lt_trans_r:
assumes "locally_trans R (A + B) (C + D) (E + F)"
shows "locally_trans R B D F"
using assms[unfolded locally_trans_def, rule_format]
unfolding locally_trans_def
by auto

lemma lin_trans_r:
assumes "locally_included R1 R2 (A + B) (C + D)"
shows "locally_included R1 R2 B D"
using assms unfolding locally_included_def by auto

lemma lcl_trans_r:
assumes "locally_compatible_l R1 R2 (A + B) (C + D) (E + F)"
shows "locally_compatible_l R1 R2 B D F"
using assms[unfolded locally_compatible_l_def, rule_format]
unfolding locally_compatible_l_def by auto

lemma lcr_trans_r:
assumes "locally_compatible_r R1 R2 (A + B) (C + D) (E + F)"
shows "locally_compatible_r R1 R2 B D F"
using assms[unfolded locally_compatible_r_def, rule_format]
unfolding locally_compatible_r_def by auto

lemma lr_minus:
assumes "locally_refl R A"
shows "locally_refl R (A - B)"
using assms unfolding locally_refl_def by (meson in_diffD)

lemma li_minus:
assumes "locally_irrefl R A"
shows "locally_irrefl R (A - B)"
using assms unfolding locally_irrefl_def by (meson in_diffD)

lemma ls_minus:
assumes "locally_sym R A"
shows "locally_sym R (A - B)"
using assms unfolding locally_sym_def by (meson in_diffD)

lemma las_minus:
assumes "locally_antisym R A"
shows "locally_antisym R (A - B)"
using assms unfolding locally_antisym_def by (meson in_diffD)

lemma lt_minus:
assumes "locally_trans R A C E"
shows "locally_trans R (A - B) (C - D) (E - F)"
using assms[unfolded locally_trans_def, rule_format]
unfolding locally_trans_def by (meson in_diffD)

lemma lin_minus:
assumes "locally_included R1 R2 A C"
shows "locally_included R1 R2 (A - B) (C - D)"
using assms unfolding locally_included_def by (meson in_diffD)

lemma lcl_minus:
assumes "locally_compatible_l R1 R2 A C E"
shows "locally_compatible_l R1 R2 (A - B) (C - D) (E - F)"
using assms[unfolded locally_compatible_l_def, rule_format]
unfolding locally_compatible_l_def by (meson in_diffD)

lemma lcr_minus:
assumes "locally_compatible_r R1 R2 A C E"
shows "locally_compatible_r R1 R2 (A - B) (C - D) (E - F)"
using assms[unfolded locally_compatible_r_def, rule_format]
unfolding locally_compatible_r_def by (meson in_diffD)

text ‹Notations›

notation restrict (infixl "↾" 80)

lemma mem_restrictI[intro!]: assumes "x ∈ X" "y ∈ X" "(x,y) ∈ R" shows "(x,y) ∈ R ↾ X"
using assms unfolding restrict_def by auto

lemma mem_restrictD[dest]: assumes "(x,y) ∈ R ↾ X" shows "x ∈ X" "y ∈ X" "(x,y) ∈ R"
using assms unfolding restrict_def by auto

end
```