Theory Completeness

(*  Author: Tobias Nipkow  *)

section ‹Combining Computations With All Completeness Proofs›

theory Completeness
imports ArchComp "Flyspeck-Tame.Relative_Completeness"
begin

global_interpretation relative?: archive_by_computation
by standard (fact pre_iso_test3 pre_iso_test4 pre_iso_test5 pre_iso_test6
  same3 same4 same5 same6)+

theorem TameEnum_Archive:  "fgraph ` TameEnum ⊆⇩≃ Archive"
by (fact TameEnum_Archive)

lemma TameEnum_comp:
assumes "Seed⇘p⇙ [next_plane⇘p⇙]→* g" and "final g" and "tame g"
shows "Seed⇘p⇙ [next_tame⇘p⇙]→* g"
using assms by (fact TameEnum_comp)

lemma tame5:
assumes g: "Seed⇘p⇙ [next_plane0⇘p⇙]→* g" and "final g" and "tame g"
shows "p ≤ 3"
using assms by (fact tame5)

theorem completeness:
assumes "g ∈ PlaneGraphs" and "tame g" shows "fgraph g ∈⇩≃ Archive"
using assms by (fact completeness)

end