Theory VeriComp.Inf

section ‹Infinitely Transitive Closure›

theory Inf
  imports Well_founded
begin

coinductive inf :: "('a  'a  bool)  'a  bool" for r where
  inf_step: "r x y  inf r y  inf r x"

coinductive inf_wf :: "('a  'a  bool)  ('b  'b  bool)  'b  'a  bool" for r order where
  inf_wf: "order n m  inf_wf r order n x  inf_wf r order m x" |
  inf_wf_step: "r++ x y  inf_wf r order n y  inf_wf r order m x"

lemma inf_wf_to_step_inf_wf:
  assumes "well_founded order"
  shows "inf_wf r order n x  y m. r x y  inf_wf r order m y"
proof (induction n arbitrary: x rule: well_founded.induct[OF assms(1)])
  case (1 n)
  from "1.prems"(1) show ?case
  proof (induction rule: inf_wf.cases)
    case (inf_wf m n' x')
    then show ?case using "1.IH" by simp
  next
    case (inf_wf_step x' y m n')
    then show ?case
      by (metis converse_tranclpE inf_wf.inf_wf_step)
  qed
qed

lemma inf_wf_to_inf:
  assumes "well_founded order"
  shows "inf_wf r order n x  inf r x"
proof (coinduction arbitrary: x n rule: inf.coinduct)
  case (inf x n)
  then obtain y m where "r x y" and "inf_wf r order m y"
    using inf_wf_to_step_inf_wf[OF assms(1) inf(1)] by metis
  thus ?case by auto
qed

lemma step_inf:
  assumes "right_unique r"
  shows "r x y  inf r x  inf r y"
  using right_uniqueD[OF right_unique r]
  by (metis inf.cases)

lemma star_inf:
  assumes "right_unique r"
  shows "r** x y  inf r x  inf r y"
proof (induction y rule: rtranclp_induct)
  case base
  then show ?case by assumption
next
  case (step y z)
  then show ?case
    using step_inf[OF right_unique r] by metis
qed

end