Theory Completeness

(*  Author: Tobias Nipkow  *)

header {* Combining All Completeness Proofs *}

theory Completeness
imports ArchCompProps ArchComp
begin

definition Archive :: "vertex fgraph set" where
"Archive ≡ set(Tri @ Quad @ Pent @ Hex)"

theorem TameEnum_Archive:  "fgraph ` TameEnum ⊆⇣\<simeq> Archive"
using combine_evals_filter[OF pre_iso_test3 same3]
      combine_evals_filter[OF pre_iso_test4 same4]
      combine_evals_filter[OF pre_iso_test5 same5]
      combine_evals_filter[OF pre_iso_test6 same6]
by(fastforce simp:TameEnum_def Archive_def image_def qle_gr.defs
       eval_nat_numeral le_Suc_eq)


lemma TameEnum_comp:
assumes "Seed⇘p⇙ [next_plane⇘p⇙]->* g" and "final g" and "tame g"
shows "Seed⇘p⇙ [next_tame⇘p⇙]->* g"
proof -
  from assms have "Seed⇘p⇙ [next_tame0 p]->* g" by(rule next_tame0_comp)
  with assms show "Seed⇘p⇙ [next_tame⇘p⇙]->* g" by(blast intro: next_tame_comp)
qed

(* final not necessary but slightly simpler because of lemmas *)
lemma tame5:
assumes g: "Seed⇘p⇙ [next_plane0⇘p⇙]->* g" and "final g" and "tame g"
shows "p ≤ 3"
proof -
  from `tame g` have bound: "∀f ∈ \<F> g. |vertices f| ≤ 6"
    by (simp add: tame_def tame9a_def)
  show "p ≤ 3"
  proof (rule ccontr)
    assume 6: "¬ p ≤ 3"
    obtain f where "f ∈ set (finals g) & |vertices f| = p+3"
      using max_face_ex[OF g] by auto
    also from `final g` have "set (finals g) = set (faces g)" by simp
    finally have "f ∈ \<F> g & 6 < |vertices f|" using 6 by arith
    with bound show False by auto
  qed
qed


theorem completeness:
assumes "g ∈ PlaneGraphs" and "tame g" shows "fgraph g ∈⇣\<simeq> Archive"
proof -
  from `g ∈ PlaneGraphs` obtain p where g1: "Seed⇘p⇙ [next_plane⇘p⇙]->* g"
    and "final g"
    by(auto simp:PlaneGraphs_def PlaneGraphsP_def)
  have "Seed⇘p⇙ [next_plane0⇘p⇙]->* g"
    by(rule RTranCl_subset2[OF g1])
      (blast intro:inv_mgp inv_Seed mgp_next_plane0_if_next_plane
        dest:RTranCl_inv[OF inv_inv_next_plane])
  with `tame g` `final g` have "p ≤ 3" by(blast intro:tame5)
  with g1 `tame g` `final g` show ?thesis using TameEnum_Archive
    by(simp add: qle_gr.defs TameEnum_def TameEnumP_def)
      (blast intro: TameEnum_comp)
qed

end