Structure bftTheory

signature bftTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val Rel_def : thm
  
  (*  Theorems  *)
    val BFT_ALL_DISTINCT : thm
    val BFT_CONS : thm
    val BFT_FOLD : thm
    val BFT_REACH_1 : thm
    val BFT_REACH_2 : thm
    val BFT_REACH_THM : thm
    val BFT_def : thm
    val BFT_ind : thm
  
  val bft_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [dirGraph] Parent theory of "bft"
   
   [Rel_def]  Definition
      
      ⊢ ∀G f seen fringe acc.
            Rel (G,f,seen,fringe,acc) =
            (CARD (Parents G DIFF set seen),LENGTH fringe)
   
   [BFT_ALL_DISTINCT]  Theorem
      
      ⊢ ∀G seen fringe.
            FINITE (Parents G) ⇒ ALL_DISTINCT (BFT G CONS seen fringe [])
   
   [BFT_CONS]  Theorem
      
      ⊢ ∀G f seen fringe acc a b.
            FINITE (Parents G) ∧ f = CONS ∧ acc = a ⧺ b ⇒
            BFT G f seen fringe acc = BFT G f seen fringe a ⧺ b
   
   [BFT_FOLD]  Theorem
      
      ⊢ ∀G f seen fringe acc.
            FINITE (Parents G) ⇒
            BFT G f seen fringe acc =
            FOLDR f acc (BFT G CONS seen fringe [])
   
   [BFT_REACH_1]  Theorem
      
      ⊢ ∀G f seen fringe acc.
            FINITE (Parents G) ∧ f = CONS ⇒
            ∀x.
                MEM x (BFT G f seen fringe acc) ⇒
                x ∈ REACH_LIST G fringe ∨ MEM x acc
   
   [BFT_REACH_2]  Theorem
      
      ⊢ ∀G f seen fringe acc x.
            FINITE (Parents G) ∧ f = CONS ∧
            x ∈ REACH_LIST (EXCLUDE G (set seen)) fringe ∧ ¬MEM x seen ⇒
            MEM x (BFT G f seen fringe acc)
   
   [BFT_REACH_THM]  Theorem
      
      ⊢ ∀G fringe.
            FINITE (Parents G) ⇒
            ∀x. x ∈ REACH_LIST G fringe ⇔ MEM x (BFT G CONS [] fringe [])
   
   [BFT_def]  Theorem
      
      ⊢ FINITE (Parents G) ⇒
        BFT G f seen [] acc = acc ∧
        BFT G f seen (h::t) acc =
        if MEM h seen then BFT G f seen t acc
        else BFT G f (h::seen) (t ⧺ G h) (f h acc)
   
   [BFT_ind]  Theorem
      
      ⊢ ∀P.
            (∀G f seen h t acc.
                 P G f seen [] acc ∧
                 ((FINITE (Parents G) ∧ ¬MEM h seen ⇒
                   P G f (h::seen) (t ⧺ G h) (f h acc)) ∧
                  (FINITE (Parents G) ∧ MEM h seen ⇒ P G f seen t acc) ⇒
                  P G f seen (h::t) acc)) ⇒
            ∀v v1 v2 v3 v4. P v v1 v2 v3 v4
   
   
*)
end

HOL 4, Kananaskis-13