Theory Binary_Relations_Transitive

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Transitive›
theory Binary_Relations_Transitive
  imports
    Functions_Monotone
begin

consts transitive_on :: "'a ⇒ 'b ⇒ bool"

overloading
  transitive_on_pred ≡ "transitive_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "transitive_on_pred P R ≡ ∀x y z : P. R x y ∧ R y z ⟶ R x z"
end

lemma transitive_onI [intro]:
  assumes "⋀x y z. P x ⟹ P y ⟹ P z ⟹ R x y ⟹ R y z ⟹ R x z"
  shows "transitive_on P R"
  unfolding transitive_on_pred_def using assms by blast

lemma transitive_onD:
  assumes "transitive_on P R"
  and "P x" "P y" "P z"
  and "R x y" "R y z"
  shows "R x z"
  using assms unfolding transitive_on_pred_def by blast

lemma transitive_on_if_rel_comp_self_imp:
  assumes "⋀x y. P x ⟹ P y ⟹ (R ∘∘ R) x y ⟹ R x y"
  shows "transitive_on P R"
proof (rule transitive_onI)
  fix x y z assume "R x y" "R y z"
  then have "(R ∘∘ R) x z" by (intro rel_compI)
  moreover assume "P x" "P y" "P z"
  ultimately show "R x z" by (simp only: assms)
qed

lemma transitive_on_rel_inv_iff_transitive_on [iff]:
  "transitive_on P R¯ ⟷ transitive_on (P :: 'a ⇒ bool) (R :: 'a ⇒ 'a ⇒ bool)"
  by (auto intro!: transitive_onI dest: transitive_onD)

lemma antimono_transitive_on: "antimono (transitive_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool)"
  by (intro antimonoI) (auto dest: transitive_onD)

consts transitive :: "'a ⇒ bool"

overloading
  transitive ≡ "transitive :: ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "(transitive :: ('a ⇒ 'a ⇒ bool) ⇒ bool) ≡ transitive_on (⊤ :: 'a ⇒ bool)"
end

lemma transitive_eq_transitive_on:
  "(transitive :: ('a ⇒ 'a ⇒ bool) ⇒ _) = transitive_on (⊤ :: 'a ⇒ bool)"
  unfolding transitive_def ..

lemma transitive_eq_transitive_on_uhint [uhint]:
  "P ≡ (⊤ :: 'a ⇒ bool) ⟹ (transitive :: ('a ⇒ 'a ⇒ bool) ⇒ _) ≡ transitive_on P"
  by (simp add: transitive_eq_transitive_on)

lemma transitiveI [intro]:
  assumes "⋀x y z. R x y ⟹ R y z ⟹ R x z"
  shows "transitive R"
  using assms by (urule transitive_onI)

lemma transitiveD [dest]:
  assumes "transitive R"
  and "R x y" "R y z"
  shows "R x z"
  using assms by (urule (d) transitive_onD where chained = insert) simp_all

lemma transitive_on_if_transitive:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "transitive R"
  shows "transitive_on P R"
  using assms by (intro transitive_onI) blast

lemma transitive_if_rel_comp_le_self:
  assumes "R ∘∘ R ≤ R"
  shows "transitive R"
  by (urule transitive_on_if_rel_comp_self_imp) (use assms in auto)

lemma rel_comp_le_self_if_transitive:
  assumes "transitive R"
  shows "R ∘∘ R ≤ R"
  using assms by blast

corollary transitive_iff_rel_comp_le_self: "transitive R ⟷ R ∘∘ R ≤ R"
  using transitive_if_rel_comp_le_self rel_comp_le_self_if_transitive by blast

lemma transitive_if_transitive_on_in_field:
  assumes "transitive_on (in_field R) R"
  shows "transitive R"
  using assms by (intro transitiveI) (blast dest: transitive_onD)

corollary transitive_on_in_field_iff_transitive [iff]:
  "transitive_on (in_field R) R ⟷ transitive R"
  using transitive_if_transitive_on_in_field transitive_on_if_transitive
  by blast

lemma transitive_rel_inv_iff_transitive [iff]: "transitive R¯ ⟷ transitive (R :: 'a ⇒ 'a ⇒ bool)"
  by fast

paragraph ‹Instantiations›

lemma transitive_eq: "transitive (=)"
  by (rule transitiveI) (rule trans)

lemma transitive_top: "transitive (⊤ :: 'a ⇒ 'a ⇒ bool)"
  by (rule transitiveI) auto


end