Structure dirGraphTheory

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

HOL 4, Kananaskis-13