theory Relations
imports
"~~/src/HOL/Library/Multiset"
"$AFP/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‹Local splitting›
definition locally_splittable :: "'a rel ⇒ 'a rel ⇒ 'a rel ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
"locally_splittable R1 R2 R3 A B ≡ (∀t u. t ∈# A ⟶ u ∈# B ⟶
(t,u) ∈ R1 ⟶ (t,u) ∈ R2 ∨ (t,u) ∈ R3)"
text‹included + compatible ⇒ 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
}
thus ?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
}
thus ?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 lsp_trans_l:
assumes "locally_splittable R1 R2 R3 (A + B) (C + D)"
shows "locally_splittable R1 R2 R3 A C"
using assms unfolding locally_splittable_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 lsp_trans_r:
assumes "locally_splittable R1 R2 R3 (A + B) (C + D)"
shows "locally_splittable R1 R2 R3 B D"
using assms unfolding locally_splittable_def by auto
lemma lr_minus:
assumes "locally_refl R A"
shows "locally_refl R (A - B)"
using assms unfolding locally_refl_def
by auto
lemma li_minus:
assumes "locally_irrefl R A"
shows "locally_irrefl R (A - B)"
using assms unfolding locally_irrefl_def
by auto
lemma ls_minus:
assumes "locally_sym R A"
shows "locally_sym R (A - B)"
using assms unfolding locally_sym_def
by auto
lemma las_minus:
assumes "locally_antisym R A"
shows "locally_antisym R (A - B)"
using assms unfolding locally_antisym_def
by auto
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 force
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 auto
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 force
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 force
lemma lsp_minus:
assumes "locally_splittable R1 R2 R3 A C"
shows "locally_splittable R1 R2 R3 (A - B) (C - D)"
using assms unfolding locally_splittable_def by auto
end