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_def0 : thm
    val BFT_ind : thm
    val BFT_ind0 : 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_def0]  Theorem
      
      ⊢ ∀seen fringe f acc G.
          BFT G f seen fringe acc =
          if FINITE (Parents G) then
            case fringe of
              [] => acc
            | h::t =>
              if MEM h seen then BFT G f seen t acc
              else BFT G f (h::seen) (t ⧺ G h) (f h acc)
          else ARB
   
   [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
   
   [BFT_ind0]  Theorem
      
      ⊢ ∀P. (∀G f seen fringe acc.
               (∀h t.
                  FINITE (Parents G) ∧ fringe = h::t ∧ ¬MEM h seen ⇒
                  P G f (h::seen) (t ⧺ G h) (f h acc)) ∧
               (∀h t.
                  FINITE (Parents G) ∧ fringe = h::t ∧ MEM h seen ⇒
                  P G f seen t acc) ⇒
               P G f seen fringe acc) ⇒
            ∀v v1 v2 v3 v4. P v v1 v2 v3 v4
   
   
*)
end

HOL 4, Trindemossen-1