Theory TameEnum

(*  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