Theory Completeness

(*  ID:         $Id: Completeness.thy,v 1.2 2006/01/13 19:18:49 nipkow Exp $
    Author:     Tobias Nipkow
*)

header {* Combining All Completeness Proofs *}

theory Completeness
imports ArchCompProps
begin

constdefs
 Archive :: "vertex fgraph set"
"Archive ≡
 set(Tri @ Quad @ Pent @ Hex @ Hept @ Oct)"

theorem TameEnum_Archive:  "fgraph ` TameEnum ⊆\<simeq> Archive"
using combine_evals[OF pre_iso_test3 same3]
      combine_evals[OF pre_iso_test4 same4]
      combine_evals[OF pre_iso_test5 same5]
      combine_evals[OF pre_iso_test6 same6]
      combine_evals[OF pre_iso_test7 same7]
      combine_evals[OF pre_iso_test8 same8]
apply(clarsimp simp:TameEnum_def Archive_def image_def iso_subseteq_def
               iso_in_def nat_number le_Suc_eq)
apply fast
done


lemma TameEnum_comp:
assumes pg: "Seedp [next_planep]->* g" and "final g" and "tame g"
shows "Seedp [next_tamep]->* g"
proof -
  from prems have "Seedp [next_tame0 p]->* g" by(rule next_tame0_comp)
  with prems have "Seedp [next_tame1 p]->* g" by(blast intro: next_tame1_comp)
  with prems show "Seedp [next_tamep]->* g" by(blast intro: next_tame_comp)
qed

lemma Seed_max_final_ex:
 "∃f∈set (finals (Seed p)). |vertices f| = maxGon p"
  by (simp add: Seed_def graph_max_final_ex)

lemma max_face_ex: assumes a: "Seedp [next_plane0p]->* g"
shows "∃f ∈ set (finals g). |vertices f| = maxGon p"
proof -
  show ?thesis
  using a
  proof (induct rule: RTranCl_induct)
    case refl then show ?case using Seed_max_final_ex by simp
  next
    case (succs g g')
    then obtain f where "f∈set (finals g)" and "|vertices f| = maxGon p"
      by auto
    moreover have "f∈set (finals g')" by (rule next_plane0_finals_incr)
    ultimately show ?case by auto
  qed
qed

(* final not necessary but slightly simpler because of lemmas *)
lemma tame5:
assumes g: "Seedp [next_plane0p]->* g" and "final g" and "tame g"
shows "p ≤ 5"
proof -
  from `tame g` have bound: "∀f ∈ \<F> g. |vertices f| ≤ 8"
   by (simp add: tame_def tame1_def)
  show "p ≤ 5"
  proof (rule ccontr)
    assume 6: "¬ p ≤ 5"
    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 & 8 < |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: "Seedp [next_planep]->* g"
    and "final g"
    by(auto simp:PlaneGraphs_def PlaneGraphsP_def)
  have "Seedp [next_plane0p]->* 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 ≤ 5" by(blast intro:tame5)
  with g1 `tame g` `final g` show ?thesis using TameEnum_Archive
    by(simp add: iso_subseteq_def TameEnum_def TameEnumP_def)
      (blast intro: TameEnum_comp)
qed


end