Theory VeriComp.Transfer_Extras

theory Transfer_Extras
  imports Main
begin

lemma rtranclp_complete_run_right_unique:
  fixes R :: "'a ⇒ 'a ⇒ bool" and x y z :: 'a
  assumes "right_unique R"
  shows "R⇧*⇧* x y ⟹ (∄w. R y w) ⟹ R⇧*⇧* x z ⟹ (∄w. R z w) ⟹ y = z"
proof (induction x arbitrary: z rule: converse_rtranclp_induct)
  case base
  then show ?case
    by (auto elim: converse_rtranclpE)
next
  case (step x w)
  hence "R⇧*⇧* w z"
    using right_uniqueD[OF ‹right_unique R›]
    by (metis converse_rtranclpE)
  with step show ?case
    by simp
qed

lemma tranclp_complete_run_right_unique:
  fixes R :: "'a ⇒ 'a ⇒ bool" and x y z :: 'a
  assumes "right_unique R"
  shows "R⇧+⇧+ x y ⟹ (∄w. R y w) ⟹ R⇧+⇧+ x z ⟹ (∄w. R z w) ⟹ y = z"
  using right_uniqueD[OF ‹right_unique R›, of x]
  by (auto dest!: tranclpD intro!: rtranclp_complete_run_right_unique[OF ‹right_unique R›, of _ y z])

end