Theory TameEnum

(*  Author:     Gertrud Bauer, Tobias Nipkow
*)

section ‹Neglectable Final Graphs›

theory TameEnum
imports Generator
begin

definition is_tame :: "graph  bool" where
"is_tame g    tame10 g  tame11a g  tame12o g  is_tame13a g"

definition next_tame :: "nat  graph  graph list" ("next'_tame⇘_") where
"next_tame⇘p filter (λg. ¬ final g  is_tame g)  next_tame0⇘p⇙"

definition TameEnumP :: "nat  graph set" ("TameEnum⇘_") where
"TameEnum⇘p {g. Seed⇘p[next_tame⇘p]→* g  final g}"

definition TameEnum :: "graph set" where
"TameEnum  p3. TameEnum⇘p⇙"

end