Structure dftTheory

signature dftTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val Rel_def : thm
  
  (*  Theorems  *)
    val DFT_ALL_DISTINCT : thm
    val DFT_CONS : thm
    val DFT_FOLD : thm
    val DFT_REACH_1 : thm
    val DFT_REACH_2 : thm
    val DFT_REACH_THM : thm
    val DFT_def : thm
    val DFT_ind : thm
  
  val dft_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [dirGraph] Parent theory of "dft"
   
   [Rel_def]  Definition
      
      ⊢ ∀G f seen to_visit acc.
            Rel (G,f,seen,to_visit,acc) =
            (CARD (Parents G DIFF set seen),LENGTH to_visit)
   
   [DFT_ALL_DISTINCT]  Theorem
      
      ⊢ ∀G seen to_visit.
            FINITE (Parents G) ⇒ ALL_DISTINCT (DFT G CONS seen to_visit [])
   
   [DFT_CONS]  Theorem
      
      ⊢ ∀G f seen to_visit acc a b.
            FINITE (Parents G) ∧ f = CONS ∧ acc = a ⧺ b ⇒
            DFT G f seen to_visit acc = DFT G f seen to_visit a ⧺ b
   
   [DFT_FOLD]  Theorem
      
      ⊢ ∀G f seen to_visit acc.
            FINITE (Parents G) ⇒
            DFT G f seen to_visit acc =
            FOLDR f acc (DFT G CONS seen to_visit [])
   
   [DFT_REACH_1]  Theorem
      
      ⊢ ∀G f seen to_visit acc.
            FINITE (Parents G) ∧ f = CONS ⇒
            ∀x.
                MEM x (DFT G f seen to_visit acc) ⇒
                x ∈ REACH_LIST G to_visit ∨ MEM x acc
   
   [DFT_REACH_2]  Theorem
      
      ⊢ ∀G f seen to_visit acc x.
            FINITE (Parents G) ∧ f = CONS ∧
            x ∈ REACH_LIST (EXCLUDE G (set seen)) to_visit ∧ ¬MEM x seen ⇒
            MEM x (DFT G f seen to_visit acc)
   
   [DFT_REACH_THM]  Theorem
      
      ⊢ ∀G to_visit.
            FINITE (Parents G) ⇒
            ∀x.
                x ∈ REACH_LIST G to_visit ⇔
                MEM x (DFT G CONS [] to_visit [])
   
   [DFT_def]  Theorem
      
      ⊢ FINITE (Parents G) ⇒
        DFT G f seen [] acc = acc ∧
        DFT G f seen (visit_now::visit_later) acc =
        if MEM visit_now seen then DFT G f seen visit_later acc
        else
          DFT G f (visit_now::seen) (G visit_now ⧺ visit_later)
            (f visit_now acc)
   
   [DFT_ind]  Theorem
      
      ⊢ ∀P.
            (∀G f seen visit_now visit_later acc.
                 P G f seen [] acc ∧
                 ((FINITE (Parents G) ∧ ¬MEM visit_now seen ⇒
                   P G f (visit_now::seen) (G visit_now ⧺ visit_later)
                     (f visit_now acc)) ∧
                  (FINITE (Parents G) ∧ MEM visit_now seen ⇒
                   P G f seen visit_later acc) ⇒
                  P G f seen (visit_now::visit_later) acc)) ⇒
            ∀v v1 v2 v3 v4. P v v1 v2 v3 v4
   
   
*)
end

HOL 4, Kananaskis-13