Theory Relation_Extensions

section ‹Relations›

theory Relation_Extensions
imports
  Basic_Extensions
begin

  abbreviation rev_lex_prod (infixr ‹<*rlex*>› 80)
    where "r⇩₁ <*rlex*> r⇩₂ ≡ inv_image (r⇩₂ <*lex*> r⇩₁) swap"

  lemmas sym_rtranclp[intro] = sym_rtrancl[to_pred]

  definition liftablep :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool"
    where "liftablep r f ≡ ∀ x y. r x y ⟶ r (f x) (f y)"

  lemma liftablepI[intro]:
    assumes "⋀ x y. r x y ⟹ r (f x) (f y)"
    shows "liftablep r f"
    using assms
    unfolding liftablep_def
    by simp
  lemma liftablepE[elim]:
    assumes "liftablep r f"
    assumes "r x y"
    obtains "r (f x) (f y)"
    using assms
    unfolding liftablep_def
    by simp

  lemma liftablep_rtranclp:
    assumes "liftablep r f"
    shows "liftablep r⇧^*⇧^* f"
  proof
    fix x y
    assume "r⇧^*⇧^* x y"
    thus "r⇧^*⇧^* (f x) (f y)"
      using assms
      by (induct rule: rtranclp_induct, force+)
  qed

  definition confluentp :: "('a ⇒ 'a ⇒ bool) ⇒ bool"
    where "confluentp r ≡ ∀ x y1 y2. r⇧^*⇧^* x y1 ⟶ r⇧^*⇧^* x y2 ⟶ (∃ z. r⇧^*⇧^* y1 z ∧ r⇧^*⇧^* y2 z)"

  lemma confluentpI[intro]:
    assumes "⋀ x y1 y2. r⇧^*⇧^* x y1 ⟹ r⇧^*⇧^* x y2 ⟹ ∃ z. r⇧^*⇧^* y1 z ∧ r⇧^*⇧^* y2 z"
    shows "confluentp r"
    using assms
    unfolding confluentp_def
    by simp

  lemma confluentpE[elim]:
    assumes "confluentp r"
    assumes "r⇧^*⇧^* x y1" "r⇧^*⇧^* x y2"
    obtains z
    where "r⇧^*⇧^* y1 z" "r⇧^*⇧^* y2 z"
    using assms
    unfolding confluentp_def
    by blast

  lemma confluentpI'[intro]:
    assumes "⋀ x y1 y2. r⇧^*⇧^* x y1 ⟹ r x y2 ⟹ ∃ z. r⇧^*⇧^* y1 z ∧ r⇧^*⇧^* y2 z"
    shows "confluentp r"
  proof
    fix x y1 y2
    assume "r⇧^*⇧^* x y1" "r⇧^*⇧^* x y2"
    thus "∃ z. r⇧^*⇧^* y1 z ∧ r⇧^*⇧^* y2 z" using assms by (induct rule: rtranclp_induct, force+)
  qed

  lemma transclp_eq_implies_confluent_imp:
    assumes "r1⇧^*⇧^* = r2⇧^*⇧^*"
    assumes "confluentp r1"
    shows "confluentp r2"
    using assms
    by force

  lemma transclp_eq_implies_confluent_eq:
    assumes "r1⇧^*⇧^* = r2⇧^*⇧^*"
    shows "confluentp r1 ⟷ confluentp r2"
    using assms transclp_eq_implies_confluent_imp
    by metis

  definition diamondp :: "('a ⇒ 'a ⇒ bool) ⇒ bool"
    where "diamondp r ≡ ∀ x y1 y2. r x y1 ⟶ r x y2 ⟶ (∃ z. r y1 z ∧ r y2 z)"

  lemma diamondpI[intro]:
    assumes "⋀ x y1 y2. r x y1 ⟹ r x y2 ⟹ ∃ z. r y1 z ∧ r y2 z"
    shows "diamondp r"
    using assms
    unfolding diamondp_def
    by simp

  lemma diamondpE[elim]:
    assumes "diamondp r"
    assumes "r x y1" "r x y2"
    obtains z
    where "r y1 z" "r y2 z"
    using assms
    unfolding diamondp_def
    by blast

  lemma diamondp_implies_confluentp:
    assumes "diamondp r"
    shows "confluentp r"
  proof (rule confluentpI')
    fix x y1 y2
    assume "r⇧^*⇧^* x y1" "r x y2"
    hence "∃ z. r y1 z ∧ r⇧^*⇧^* y2 z" using assms by (induct rule: rtranclp_induct, force+)
    thus "∃ z. r⇧^*⇧^* y1 z ∧ r⇧^*⇧^* y2 z" by blast
  qed

  locale wellfounded_relation =
    fixes R :: "'a ⇒ 'a ⇒ bool"
    assumes wellfounded: "wfP R"

end