Theory Reachablen

section ‹$n$-step reachability›

theory Reachablen
imports
  Graph_Theory.Graph_Theory
begin

inductive
  ntrancl_onp :: "'a set ⇒ 'a rel ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool"
  for F :: "'a set" and r :: "'a rel"
where
    ntrancl_on_0: "a = b ⟹ a ∈ F ⟹ ntrancl_onp F r 0 a b"
  | ntrancl_on_Suc: "(a,b) ∈ r ⟹ ntrancl_onp F r n b c ⟹ a ∈ F ⟹ ntrancl_onp F r (Suc n) a c"

lemma ntrancl_onpD_rtrancl_on:
  assumes "ntrancl_onp F r n a b" shows "(a,b) ∈ rtrancl_on F r"
  using assms by induct (auto intro: converse_rtrancl_on_into_rtrancl_on)

lemma rtrancl_onE_ntrancl_onp:
  assumes "(a,b) ∈ rtrancl_on F r" obtains n where "ntrancl_onp F r n a b"
proof atomize_elim
  from assms show "∃n. ntrancl_onp F r n a b"
  proof induct
    case base
    then have "ntrancl_onp F r 0 b b" by (auto intro: ntrancl_onp.intros)
    then show ?case ..
  next
    case (step a c)
    from ‹∃n. _› obtain n where "ntrancl_onp F r n c b" ..
    with ‹(a,c) ∈ r› have "ntrancl_onp F r (Suc n) a b" using  ‹a ∈ F› by (rule ntrancl_onp.intros)
    then show ?case ..
  qed
qed

lemma rtrancl_on_conv_ntrancl_onp: "(a,b) ∈ rtrancl_on F r ⟷ (∃n. ntrancl_onp F r n a b)"
  by (metis ntrancl_onpD_rtrancl_on rtrancl_onE_ntrancl_onp)


definition nreachable :: "('a,'b) pre_digraph ⇒ 'a ⇒ nat ⇒ 'a ⇒ bool" (‹_ →⇗_⇖ı _› [100,100] 40) where
  "nreachable G u n v ≡ ntrancl_onp (verts G) (arcs_ends G) n u v"

context wf_digraph begin

lemma reachableE_nreachable:
  assumes "u →⇧* v" obtains n where "u →⇗n⇖ v"
  using assms by (auto simp: reachable_def nreachable_def elim: rtrancl_onE_ntrancl_onp)

lemma converse_nreachable_cases[cases pred: nreachable]:
  assumes "u →⇗n⇖ v"
  obtains (ntrancl_on_0) "u = v" "n = 0" "u ∈ verts G"
    | (ntrancl_on_Suc) w m where "u → w" "n = Suc m" "w →⇗m⇖ v"
  using assms unfolding nreachable_def by cases auto

lemma converse_nreachable_induct[consumes 1, case_names base step, induct pred: reachable]:
  assumes major: "u →⇗n⇖⇘G⇙ v"
    and cases: "v ∈ verts G ⟹ P 0 v"
       "⋀n x y. ⟦x →⇘G⇙ y; y →⇗n⇖⇘G⇙ v; P n y⟧ ⟹ P (Suc n) x"
  shows "P n u"
  using assms unfolding nreachable_def by induct auto

lemma converse_nreachable_induct_less[consumes 1, case_names base step, induct pred: reachable]:
  assumes major: "u →⇗n⇖⇘G⇙ v"
    and cases: "v ∈ verts G ⟹ P 0 v"
       "⋀n x y. ⟦x →⇘G⇙ y; y →⇗n⇖⇘G⇙ v; ⋀z m. m ≤ n ⟹ (z →⇗m⇖⇘G⇙ v) ⟹ P m z⟧ ⟹ P (Suc n) x"
  shows "P n u"
proof -
  have "⋀q u. q ≤ n ⟹ (u →⇗q⇖⇘G⇙ v) ⟹ P q u"
  proof (induction n arbitrary: u rule: less_induct)
    case (less n)
    show ?case
    proof (cases q)
      case 0 with less show ?thesis by (auto intro: cases elim: converse_nreachable_cases)
    next
      case (Suc q')
      with ‹u →⇗q⇖ v› obtain w where "u → w" "w →⇗q'⇖ v" by (auto elim: converse_nreachable_cases)
      then show ?thesis
        unfolding ‹q = _› using Suc less by (auto intro!: less.IH cases)
    qed
  qed
  with major show ?thesis by auto
qed

end

end