(* ID: $Id: TameEnum.thy,v 1.2 2006/01/11 19:40:46 nipkow Exp $
Author: Gertrud Bauer, Tobias Nipkow
*)
header {* Neglectable Final Graphs *}
theory TameEnum
imports Generator Plane4
begin
constdefs
is_tame :: "graph => bool"
"is_tame g ≡ tame45 g ∧ tame6 g ∧ tame8 g ∧ is_tame7 g ∧ is_tame3 g"
constdefs
next_tame :: "nat => graph => graph list" ("next'_tame_")
"next_tamep ≡ filter (λg. ¬ final g ∨ is_tame g) o next_tame1p"
constdefs
TameEnumP :: "nat => graph set" ("TameEnum_")
"TameEnump ≡ {g. Seedp [next_tamep]->* g ∧ final g}"
TameEnum :: "graph set"
"TameEnum ≡ \<Union>p≤5. TameEnump"
end