Theory Relative_Completeness

(*  Author: Tobias Nipkow  *)

section ‹Completeness Proofs under hypothetical computations›

theory Relative_Completeness
imports ArchCompProps
begin

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

locale archive_by_computation =
  assumes pre_iso_test3: "∀g ∈ set Tri. pre_iso_test g"
  assumes pre_iso_test4: "∀g ∈ set Quad. pre_iso_test g"
  assumes pre_iso_test5: "∀g ∈ set Pent. pre_iso_test g"
  assumes pre_iso_test6: "∀g ∈ set Hex. pre_iso_test g"
  assumes same3: "samet (tameEnumFilter 0) Tri"
  assumes same4: "samet (tameEnumFilter 1) Quad"
  assumes same5: "samet (tameEnumFilter 2) Pent"
  assumes same6: "samet (tameEnumFilter 3) Hex"
begin

theorem TameEnum_Archive:  "fgraph ` TameEnum ⊆⇩≃ 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 ∈ ℱ 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 ∈ ℱ 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 ∈⇩≃ 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

end