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