Theory HOL-Library.Transitive_Closure_Table

(*  Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen  *)

section ‹A table-based implementation of the reflexive transitive closure›

theory Transitive_Closure_Table
imports Main
begin

inductive rtrancl_path :: "('a  'a  bool)  'a  'a list  'a  bool"
  for r :: "'a  'a  bool"
where
  base: "rtrancl_path r x [] x"
| step: "r x y  rtrancl_path r y ys z  rtrancl_path r x (y # ys) z"

lemma rtranclp_eq_rtrancl_path: "r** x y  (xs. rtrancl_path r x xs y)"
proof
  show "xs. rtrancl_path r x xs y" if "r** x y"
    using that
  proof (induct rule: converse_rtranclp_induct)
    case base
    have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
    then show ?case ..
  next
    case (step x z)
    from xs. rtrancl_path r z xs y
    obtain xs where "rtrancl_path r z xs y" ..
    with r x z have "rtrancl_path r x (z # xs) y"
      by (rule rtrancl_path.step)
    then show ?case ..
  qed
  show "r** x y" if "xs. rtrancl_path r x xs y"
  proof -
    from that obtain xs where "rtrancl_path r x xs y" ..
    then show ?thesis
    proof induct
      case (base x)
      show ?case
        by (rule rtranclp.rtrancl_refl)
    next
      case (step x y ys z)
      from r x y r** y z show ?case
        by (rule converse_rtranclp_into_rtranclp)
    qed
  qed
qed

lemma rtrancl_path_trans:
  assumes xy: "rtrancl_path r x xs y"
    and yz: "rtrancl_path r y ys z"
  shows "rtrancl_path r x (xs @ ys) z" using xy yz
proof (induct arbitrary: z)
  case (base x)
  then show ?case by simp
next
  case (step x y xs)
  then have "rtrancl_path r y (xs @ ys) z"
    by simp
  with r x y have "rtrancl_path r x (y # (xs @ ys)) z"
    by (rule rtrancl_path.step)
  then show ?case by simp
qed

lemma rtrancl_path_appendE:
  assumes xz: "rtrancl_path r x (xs @ y # ys) z"
  obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z"
  using xz
proof (induct xs arbitrary: x)
  case Nil
  then have "rtrancl_path r x (y # ys) z" by simp
  then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"
    by cases auto
  from xy have "rtrancl_path r x [y] y"
    by (rule rtrancl_path.step [OF _ rtrancl_path.base])
  then have "rtrancl_path r x ([] @ [y]) y" by simp
  then show thesis using yz by (rule Nil)
next
  case (Cons a as)
  then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp
  then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"
    by cases auto
  show thesis
  proof (rule Cons(1) [OF _ az])
    assume "rtrancl_path r y ys z"
    assume "rtrancl_path r a (as @ [y]) y"
    with xa have "rtrancl_path r x (a # (as @ [y])) y"
      by (rule rtrancl_path.step)
    then have "rtrancl_path r x ((a # as) @ [y]) y"
      by simp
    then show thesis using rtrancl_path r y ys z
      by (rule Cons(2))
  qed
qed

lemma rtrancl_path_distinct:
  assumes xy: "rtrancl_path r x xs y"
  obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" and "set xs'  set xs"
  using xy
proof (induct xs rule: measure_induct_rule [of length])
  case (less xs)
  show ?case
  proof (cases "distinct (x # xs)")
    case True
    with rtrancl_path r x xs y show ?thesis by (rule less) simp
  next
    case False
    then have "as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
      by (rule not_distinct_decomp)
    then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"
      by iprover
    show ?thesis
    proof (cases as)
      case Nil
      with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
        by auto
      from x xs rtrancl_path r x xs y have cs: "rtrancl_path r x cs y" "set cs  set xs"
        by (auto elim: rtrancl_path_appendE)
      from xs have "length cs < length xs" by simp
      then show ?thesis
        by (rule less(1))(blast intro: cs less(2) order_trans del: subsetI)+
    next
      case (Cons d ds)
      with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
        by auto
      with rtrancl_path r x xs y obtain xa: "rtrancl_path r x (ds @ [a]) a"
        and ay: "rtrancl_path r a (bs @ a # cs) y"
        by (auto elim: rtrancl_path_appendE)
      from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
      with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
        by (rule rtrancl_path_trans)
      from xs have set: "set ((ds @ [a]) @ cs)  set xs" by auto
      from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
      then show ?thesis
        by (rule less(1))(blast intro: xy less(2) set[THEN subsetD])+
    qed
  qed
qed

inductive rtrancl_tab :: "('a  'a  bool)  'a list  'a  'a  bool"
  for r :: "'a  'a  bool"
where
  base: "rtrancl_tab r xs x x"
| step: "x  set xs  r x y  rtrancl_tab r (x # xs) y z  rtrancl_tab r xs x z"

lemma rtrancl_path_imp_rtrancl_tab:
  assumes path: "rtrancl_path r x xs y"
    and x: "distinct (x # xs)"
    and ys: "({x}  set xs)  set ys = {}"
  shows "rtrancl_tab r ys x y"
  using path x ys
proof (induct arbitrary: ys)
  case base
  show ?case
    by (rule rtrancl_tab.base)
next
  case (step x y zs z)
  then have "x  set ys"
    by auto
  from step have "distinct (y # zs)"
    by simp
  moreover from step have "({y}  set zs)  set (x # ys) = {}"
    by auto
  ultimately have "rtrancl_tab r (x # ys) y z"
    by (rule step)
  with x  set ys r x y show ?case
    by (rule rtrancl_tab.step)
qed

lemma rtrancl_tab_imp_rtrancl_path:
  assumes tab: "rtrancl_tab r ys x y"
  obtains xs where "rtrancl_path r x xs y"
  using tab
proof induct
  case base
  from rtrancl_path.base show ?case
    by (rule base)
next
  case step
  show ?case
    by (iprover intro: step rtrancl_path.step)
qed

lemma rtranclp_eq_rtrancl_tab_nil: "r** x y  rtrancl_tab r [] x y"
proof
  show "rtrancl_tab r [] x y" if "r** x y"
  proof -
    from that obtain xs where "rtrancl_path r x xs y"
      by (auto simp add: rtranclp_eq_rtrancl_path)
    then obtain xs' where xs': "rtrancl_path r x xs' y" and distinct: "distinct (x # xs')"
      by (rule rtrancl_path_distinct)
    have "({x}  set xs')  set [] = {}"
      by simp
    with xs' distinct show ?thesis
      by (rule rtrancl_path_imp_rtrancl_tab)
  qed
  show "r** x y" if "rtrancl_tab r [] x y"
  proof -
    from that obtain xs where "rtrancl_path r x xs y"
      by (rule rtrancl_tab_imp_rtrancl_path)
    then show ?thesis
      by (auto simp add: rtranclp_eq_rtrancl_path)
  qed
qed

declare rtranclp_rtrancl_eq [code del]
declare rtranclp_eq_rtrancl_tab_nil [THEN iffD2, code_pred_intro]

code_pred rtranclp
  using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce

lemma rtrancl_path_Range: " rtrancl_path R x xs y; z  set xs   Rangep R z"
by(induction rule: rtrancl_path.induct) auto

lemma rtrancl_path_Range_end: " rtrancl_path R x xs y; xs  []   Rangep R y"
by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)

lemma rtrancl_path_nth:
  " rtrancl_path R x xs y; i < length xs   R ((x # xs) ! i) (xs ! i)"
proof(induction arbitrary: i rule: rtrancl_path.induct)
  case step thus ?case by(cases i) simp_all
qed simp

lemma rtrancl_path_last: " rtrancl_path R x xs y; xs  []   last xs = y"
by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)

lemma rtrancl_path_mono:
  " rtrancl_path R x p y; x y. R x y  S x y   rtrancl_path S x p y"
by(induction rule: rtrancl_path.induct)(auto intro: rtrancl_path.intros)

end