# Structure dirGraphTheory

Source File Identifier index Theory binding index

```signature dirGraphTheory =
sig
type thm = Thm.thm

(*  Definitions  *)
val EXCLUDE_def : thm
val Parents_def : thm
val REACH_LIST_def : thm
val REACH_def : thm

(*  Theorems  *)
val EXCLUDE_LEM : thm
val REACH_EXCLUDE : thm
val REACH_LEM1 : thm
val REACH_LEM2 : thm

val dirGraph_grammars : type_grammar.grammar * term_grammar.grammar
(*
[indexedLists] Parent theory of "dirGraph"

[patternMatches] Parent theory of "dirGraph"

[EXCLUDE_def]  Definition

⊢ ∀G ex node. EXCLUDE G ex node = if node ∈ ex then [] else G node

[Parents_def]  Definition

⊢ ∀G. Parents G = {x | G x ≠ []}

[REACH_LIST_def]  Definition

⊢ ∀G nodes y. REACH_LIST G nodes y ⇔ ∃x. MEM x nodes ∧ y ∈ REACH G x

[REACH_def]  Definition

⊢ ∀G. REACH G = (λx y. MEM y (G x))꙳

[EXCLUDE_LEM]  Theorem

⊢ ∀G x l. EXCLUDE G (x INSERT l) = EXCLUDE (EXCLUDE G l) {x}

[REACH_EXCLUDE]  Theorem

⊢ ∀G x. REACH (EXCLUDE G x) = (λx' y. x' ∉ x ∧ MEM y (G x'))꙳

[REACH_LEM1]  Theorem

⊢ ∀p G seen.
p ∉ seen ⇒
REACH (EXCLUDE G seen) p =
p INSERT REACH_LIST (EXCLUDE G (p INSERT seen)) (G p)

[REACH_LEM2]  Theorem

⊢ ∀G x y. REACH G x y ⇒ ∀z. ¬REACH G z y ⇒ REACH (EXCLUDE G {z}) x y

*)
end

```

Source File Identifier index Theory binding index

HOL 4, Trindemossen-1