Theory Weighted_Path_Order.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