# Theory Completeness

Up to index of Isabelle/HOL/Tame

theory Completeness
imports ArchCompProps
begin

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

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"
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
(blast intro: TameEnum_comp)
qed

end
```

theorem TameEnum_Archive:

`  fgraph ` TameEnum ⊆\<simeq> Archive  [!]`

lemma TameEnum_comp:

`  [| Seedp [next_planep]->* g; final g; tame g |] ==> Seedp [next_tamep]->* g`

lemma Seed_max_final_ex:

`  ∃f∈set (finals Seedp). |vertices f| = maxGon p`

lemma max_face_ex:

`  Seedp [next_plane0p]->* g ==> ∃f∈set (finals g). |vertices f| = maxGon p`

lemma tame5:

`  [| Seedp [next_plane0p]->* g; final g; tame g |] ==> p ≤ 5`

theorem completeness:

`  [| g ∈ PlaneGraphs; tame g |] ==> fgraph g ∈\<simeq> Archive  [!]`