Theory Partial_Order_Reduction.Relation_Extensions

section ‹Relations›

theory Relation_Extensions
imports
  Basic_Extensions
begin

  abbreviation rev_lex_prod (infixr "<*rlex*>" 80)
    where "r1 <*rlex*> r2  inv_image (r2 <*lex*> r1) 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