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 ≡ ⋃p≤3. TameEnum⇘p⇙"

end