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