# Structure dftTheory

Source File Identifier index Theory binding index

```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

```

Source File Identifier index Theory binding index