Theory GeneratorProps

(*  Author:  Tobias Nipkow  *)

section "Properties of Tame Graph Enumeration (1)"

theory GeneratorProps
imports Plane1Props Generator TameProps LowerBound
begin

lemma genPolyTame_spec:
 "generatePolygonTame n v f g = [g' ← generatePolygon n v f g . ¬ notame g']"
by(simp add:generatePolygonTame_def generatePolygon_def enum_enumerator)

lemma genPolyTame_subset_genPoly:
 "g' ∈ set(generatePolygonTame i v f g) ⟹
  g' ∈ set(generatePolygon i v f g)"
by(auto simp add:generatePolygon_def generatePolygonTame_def enum_enumerator)


lemma next_tame0_subset_plane:
 "set(next_tame0 p g) ⊆ set(next_plane p g)"
by(auto simp add:next_tame0_def next_plane_def polysizes_def
           elim!:genPolyTame_subset_genPoly simp del:upt_Suc)


lemma genPoly_new_face:
 "⟦g' ∈ set (generatePolygon n v f g); minGraphProps g; f ∈ set (nonFinals g);
   v ∈ 𝒱 f; n ≥ 3 ⟧ ⟹
  ∃f ∈ set(finals g') - set(finals g). |vertices f| = n"
apply(auto simp add:generatePolygon_def image_def)
apply(rename_tac "is")
apply(frule enumerator_length2)
 apply arith
apply(frule (4) pre_subdivFace_indexToVertexList)
 apply(arith)
apply(subgoal_tac "indexToVertexList f v is ≠ []")
 prefer 2 apply(subst length_0_conv[symmetric]) apply simp
apply(simp add: subdivFace_subdivFace'_eq)
apply(clarsimp simp:neq_Nil_conv)
apply(rename_tac "ovs")
apply(subgoal_tac "|indexToVertexList f v is| = |ovs| + 1")
 prefer 2 apply(simp)
apply(drule (1) pre_subdivFace_pre_subdivFace')
apply(drule (1) final_subdivFace')
  apply(simp add:nonFinals_def)
 apply(simp add:pre_subdivFace'_def)
apply (simp (no_asm_use))
apply(simp)
apply blast
done


(* Could prove = instead of ≥, but who needs it? *)
lemma genPoly_incr_facesquander_lb:
assumes "g' ∈ set (generatePolygon n v f g)" "inv g"
        "f ∈ set(nonFinals g)" "v ∈ 𝒱 f" "3 ≤ n"
shows "faceSquanderLowerBound g' ≥ faceSquanderLowerBound g + 𝖽 n"
proof -
  from genPoly_new_face[OF assms(1) inv_mgp[OF assms(2)] assms(3-5)] obtain f
    where f: "f ∈ set (finals g') - set(finals g)"
    and size: "|vertices f| = n" by auto
  have g': "g' ∈ set(next_plane0 (n - 3) g)" using assms(5)
    by(rule_tac in_next_plane0I[OF assms(1,3-5)]) simp
  note dist = minGraphProps11'[OF inv_mgp[OF assms(2)]]
  note inv' = invariantE[OF inv_inv_next_plane0, OF g' assms(2)]
  note dist' = minGraphProps11'[OF inv_mgp[OF inv']]
  note subset = next_plane0_finals_subset[OF g']
  have "faceSquanderLowerBound g' ≥
        faceSquanderLowerBound g + 𝖽 |vertices f|"
  proof(unfold faceSquanderLowerBound_def)
    have "(∑⇘f∈finals g⇙ 𝖽 |vertices f| ) + 𝖽 |vertices f| =
          (∑f∈set(finals g). 𝖽 |vertices f| ) + 𝖽 |vertices f|"
      using dist by(simp add:finals_def ListSum_conv_sum)
    also have "… = (∑f∈set(finals g) ∪ {f}. 𝖽 |vertices f| )"
      using f by simp
    also have "… ≤ (∑f∈set(finals g'). 𝖽 |vertices f| )"
      using f subset by(fastforce intro!: sum_mono2)
    also have "… = (∑⇘f∈finals g'⇙ 𝖽 |vertices f| )"
      using dist' by(simp add:finals_def ListSum_conv_sum)
    finally show "(∑⇘f∈finals g⇙ 𝖽 |vertices f| ) + 𝖽 |vertices f|
          ≤ (∑⇘f∈finals g'⇙ 𝖽 |vertices f| )" .
  qed
  with size show ?thesis by blast
qed


definition close :: "graph ⇒ vertex ⇒ vertex ⇒ bool" where
"close g u v ≡
 ∃f ∈ set(facesAt g u). if |vertices f| = 4 then v = f ∙ u ∨ v = f ∙ (f ∙ u)
                        else v = f ∙ u"

(* FIXME This should be the def of delAround *)
lemma delAround_def: "deleteAround g u ps = [p ← ps. ¬ close g u (fst p)]"
by (induct ps) (auto simp: deleteAroundCons close_def)


lemma close_sym: assumes mgp: "minGraphProps g" and ug: "u : 𝒱 g" and cl: "close g u v"
shows "close g v u"
proof -
  obtain f where f: "f ∈ set(facesAt g u)" and
    "if": "if |vertices f| = 4 then v = f ∙ u ∨ v = f ∙ (f ∙ u) else v = f ∙ u"
    using cl by (unfold close_def) blast
  note uf = minGraphProps6[OF mgp ug f]
  note distf = minGraphProps3[OF mgp minGraphProps5[OF mgp ug f]]
  show ?thesis
  proof cases
    assume 4: "|vertices f| = 4"
    hence "v = f ∙ u ∨ v = f ∙ (f ∙ u)" using "if" by simp
    thus ?thesis
    proof
      assume "v = f ∙ u"
      then obtain f' where "f' ∈ set(facesAt g v)" "f' ∙ v = u"
        using mgp_nextVertex_face_ex2[OF mgp ug f] by blast
      thus ?thesis by(auto simp:close_def)
    next
      assume v: "v = f ∙ (f ∙ u)"
      hence "f ∙ (f ∙ v) = u" using quad_next4_id[OF 4 distf uf] by simp
      moreover have "f ∈ set(facesAt g v)" using v uf
        by(simp add: minGraphProps7[OF mgp minGraphProps5[OF mgp ug f]])
      ultimately show ?thesis using 4 by(auto simp:close_def)
    qed
  next
    assume "|vertices f| ≠ 4"
    hence "v = f ∙ u" using "if" by simp
    then obtain f' where "f' ∈ set(facesAt g v)" "f' ∙ v = u"
      using mgp_nextVertex_face_ex2[OF mgp ug f] by blast
    thus ?thesis by(auto simp:close_def)
  qed
qed


lemma sep_conv:
assumes mgp: "minGraphProps g" and "V ⊆ 𝒱 g"
shows "separated g V = (∀u∈V.∀v∈V. u ≠ v ⟶ ¬ close g u v)" (is "?P = ?Q")
proof
  assume sep: ?P
  show ?Q
  proof(clarify)
    fix u v assume uv: "u ∈ V" "v ∈ V" "u ≠ v" and cl: "close g u v"
    from cl obtain f where f: "f ∈ set(facesAt g u)" and
      "if": "if |vertices f| = 4 then (v = f ∙ u) ∨ (v = f ∙ (f ∙ u))
                               else (v = f ∙ u)"
      by (unfold close_def) blast
    have "u : 𝒱 g" using ‹u : V› ‹V ⊆ 𝒱 g› by blast
    note uf = minGraphProps6[OF mgp ‹u : 𝒱 g› f]
    show False
    proof cases
      assume 4: "|vertices f| = 4"
      hence "v = f ∙ u ∨ v = f ∙ (f ∙ u)" using "if" by simp
      thus False
      proof
        assume "v = f ∙ u"
        thus False using sep f uv
          by(simp add:separated_def separated⇩2_def separated⇩3_def)
      next
        assume "v = f ∙ (f ∙ u)"
        moreover hence "v ∈ 𝒱 f" using ‹u ∈ 𝒱 f› by simp
        moreover have "|vertices f| ≤ 4" using 4 by arith
        ultimately show False using sep f uv ‹u ∈ 𝒱 f›
          apply(unfold separated_def separated⇩2_def separated⇩3_def)
(* why does blast get stuck? *)
          apply(subgoal_tac "f ∙ (f ∙ u) ∈ 𝒱 f ∩ V")
          prefer 2 apply blast
          by simp
      qed
    next
      assume 4: "|vertices f| ≠ 4"
      hence "v = f ∙ u" using "if" by simp
      thus False using sep f uv
        by(simp add:separated_def separated⇩2_def separated⇩3_def)
    qed
  qed
next
  assume not_cl: ?Q
  show ?P
  proof(simp add:separated_def, rule conjI)
    show "separated⇩2 g V"
    proof (clarsimp simp:separated⇩2_def)
      fix v f assume a: "v ∈ V" "f ∈ set (facesAt g v)" "f ∙ v ∈ V"
      have "v : 𝒱 g" using a(1) ‹V ⊆ 𝒱 g› by blast
      show False using a not_cl mgp_facesAt_no_loop[OF mgp ‹v : 𝒱 g› a(2)]
        by(fastforce simp: close_def split:if_split_asm)
    qed
    show "separated⇩3 g V"
    proof (clarsimp simp:separated⇩3_def)
      fix v f
      assume "v ∈ V" and f: "f ∈ set (facesAt g v)" and len: "|vertices f| ≤ 4"
      have vg: "v : 𝒱 g" using ‹v : V› ‹V ⊆ 𝒱 g› by blast
      note distf = minGraphProps3[OF mgp minGraphProps5[OF mgp vg f]]
      note vf = minGraphProps6[OF mgp vg f]
      { fix u assume "u ∈ 𝒱 f" and "u ∈ V"
        have "u = v"
        proof cases
          assume 3: "|vertices f| = 3"
          hence "𝒱 f = {v, f ∙ v, f ∙ (f ∙ v)}"
            using vertices_triangle[OF _ vf distf] by simp
          moreover
          { assume "u = f ∙ v"
            hence "u = v"
              using not_cl f ‹u ∈ V› ‹v ∈ V› 3
              by(force simp:close_def split:if_split_asm)
          }
          moreover
          { assume "u = f ∙ (f ∙ v)"
            hence fu: "f ∙ u = v"
              by(simp add: tri_next3_id[OF 3 distf ‹v ∈ 𝒱 f›])
            hence "(u,v) ∈ ℰ f" using nextVertex_in_edges[OF ‹u ∈ 𝒱 f›]
              by(simp add:fu)
            then obtain f' where "f' ∈ set(facesAt g v)" "(v,u) ∈  ℰ f'"
              using mgp_edge_face_ex[OF mgp vg f] by blast
            hence "u = v" using not_cl ‹u ∈ V› ‹v ∈ V› 3
              by(force simp:close_def edges_face_eq split:if_split_asm)
          }
          ultimately show "u=v" using ‹u ∈ 𝒱 f› by blast
        next
          assume 3: "|vertices f| ≠ 3"
          hence 4: "|vertices f| = 4"
            using len mgp_vertices3[OF mgp minGraphProps5[OF mgp vg f]] by arith
          hence "𝒱 f = {v, f ∙ v, f ∙ (f ∙ v), f ∙ (f ∙ (f ∙ v))}"
            using vertices_quad[OF _ vf distf] by simp
          moreover
          { assume "u = f ∙ v"
            hence "u = v"
              using not_cl f ‹u ∈ V› ‹v ∈ V› 4
              by(force simp:close_def split:if_split_asm)
          }
          moreover
          { assume "u = f ∙ (f ∙ v)"
            hence "u = v"
              using not_cl f ‹u ∈ V› ‹v ∈ V› 4
              by(force simp:close_def split:if_split_asm)
          }
          moreover
          { assume "u = f ∙ (f ∙ (f ∙ v))"
            hence fu: "f ∙ u = v"
              by(simp add: quad_next4_id[OF 4 distf ‹v ∈ 𝒱 f›])
            hence "(u,v) ∈ ℰ f" using nextVertex_in_edges[OF ‹u ∈ 𝒱 f›]
              by(simp add:fu)
            then obtain f' where "f' ∈ set(facesAt g v)" "(v,u) ∈  ℰ f'"
              using mgp_edge_face_ex[OF mgp vg f] by blast
            hence "u = v" using not_cl ‹u ∈ V› ‹v ∈ V› 4
              by(force simp:close_def edges_face_eq split:if_split_asm)
          }
          ultimately show "u=v" using ‹u ∈ 𝒱 f› by blast
        qed
      }
      thus "𝒱 f ∩ V = {v}" using ‹v ∈ V› vf by blast
    qed
  qed
qed

lemma sep_ne: "∃P ⊆ M. separated g (fst ` P)"
by(unfold separated_def separated⇩2_def separated⇩3_def) blast

lemma ExcessNotAtRec_conv_Max:
assumes mgp: "minGraphProps g"
shows "set(map fst ps) ⊆ 𝒱 g ⟹ distinct(map fst ps) ⟹
  ExcessNotAtRec ps g =
  Max{ ∑p∈P. snd p |P. P ⊆ set ps ∧ separated g (fst ` P)}"
  (is "_ ⟹ _ ⟹ _ = Max(?M ps)" is "_ ⟹ _ ⟹ _ = Max{_ |P. ?S ps P}")
proof(induct ps rule: length_induct)
  case (1 ps0)
  note IH = 1(1) and subset = 1(2) and dist = 1(3)
  show ?case
  proof (cases ps0)
    case Nil thus ?thesis by simp
  next
    case (Cons p ps)
    let ?ps = "deleteAround g (fst p) ps"
    have le: "|?ps| ≤ |ps|" by(simp add:delAround_def)
    have dist': "distinct(map fst ?ps)" using dist Cons
      apply (clarsimp simp:delAround_def)
      apply(drule distinct_filter[where P = "Not ∘ close g (fst p)"])
      apply(simp add: filter_map o_def)
      done
    have "fst p : 𝒱 g" and "fst ` set ps ⊆ 𝒱 g"
      using subset Cons by auto
    have sub1: "⋀P Q. P ⊆ {x : set ps. Q x} ⟹ fst ` P ⊆ 𝒱 g"
      using subset Cons by auto
    have sub2: "⋀P Q. P ⊆ insert p {x : set ps. Q x} ⟹ fst ` P ⊆ 𝒱 g"
      using subset Cons by auto
    have sub3: "⋀P. P ⊆ insert p (set ps) ⟹ fst ` P ⊆ 𝒱 g"
      using subset Cons by auto
    have "⋀a. set (map fst (deleteAround g a ps)) ⊆ 𝒱 g"
      using deleteAround_subset[of g _ ps] subset Cons
      by auto
    hence "ExcessNotAtRec ps0 g = max (Max(?M ps)) (Max(?M ?ps) + snd p)"
      using Cons IH subset le dist dist' by (cases p) simp
    also have "Max (?M ?ps) + snd p =
      Max {(∑p∈P. snd p) + snd p | P. ?S ?ps P}"
      by (auto simp add:setcompr_eq_image Max_add_commute[symmetric] sep_ne intro!: arg_cong [where f=Max])
    also have "{(∑p∈P. snd p) + snd p |P. ?S ?ps P} =
      {sum snd (insert p P) |P. ?S ?ps P}"
      using dist Cons
      apply (auto simp:delAround_def)
      apply(rule_tac x=P in exI)
      apply(fastforce intro!: sum.insert[THEN trans,symmetric] elim: finite_subset)
      apply(rule_tac x=P in exI)
      apply(fastforce intro!: sum.insert[THEN trans] elim: finite_subset)
      done
    also have "… = {sum snd P |P.
            P ⊆ insert p (set ?ps) ∧ p ∈ P ∧ separated g (fst ` P)}"
      apply(auto simp add:sep_conv[OF mgp] sub1 sub2 delAround_def cong: conj_cong)
      apply(rule_tac x = "insert p P" in exI)
      apply simp
      apply(rule conjI) apply blast
      using ‹image fst (set ps) ⊆ 𝒱 g› ‹fst p : 𝒱 g›
      apply (blast intro:close_sym[OF mgp])
      apply(rule_tac x = "P-{p}" in exI)
      apply (simp add:insert_absorb)
      apply blast
      done
    also have "… = {sum snd P |P.
            P ⊆ insert p (set ps) ∧ p ∈ P ∧ separated g (fst ` P)}"
      using Cons dist
      apply(auto simp add:sep_conv[OF mgp] sub2 sub3 delAround_def cong: conj_cong)
      apply(rule_tac x = "P" in exI)
      apply simp
      apply auto
      done
    also have "max (Max(?M ps)) (Max …) = Max(?M ps ∪ {sum snd P |P.
            P ⊆ insert p (set ps) ∧ p ∈ P ∧ separated g (fst ` P)})"
      (is "_ = Max ?U")
    proof -
      have "{sum snd P |P.
            P ⊆ insert p (set ps) ∧ p ∈ P ∧ separated g (fst ` P)} ≠ {}"
        apply simp
        apply(rule_tac x="{p}" in exI)
        using ‹fst p : 𝒱 g› by(simp add:sep_conv[OF mgp])
      thus ?thesis by(simp add: Max_Un sep_ne)
    qed
    also have "?U = ?M ps0" using Cons by simp blast
    finally show ?thesis .
  qed
qed


lemma dist_ExcessTab: "distinct (map fst (ExcessTable g (vertices g)))"
by(simp add:ExcessTable_def vertices_graph o_def)



lemma mono_ExcessTab: "⟦g' ∈ set (next_plane0⇘p⇙ g); inv g ⟧ ⟹
  set(ExcessTable g (vertices g)) ⊆ set(ExcessTable g' (vertices g'))"
apply(clarsimp simp:ExcessTable_def image_def)
apply(rule conjI)
 apply(blast dest:next_plane0_vertices_subset inv_mgp)
apply (clarsimp simp:ExcessAt_def split:if_split_asm)
apply(frule (3) next_plane0_finalVertex_mono)
apply(simp add: next_plane0_len_filter_eq tri_def quad_def except_def)
done


lemma close_antimono:
 "⟦g' ∈ set (next_plane0⇘p⇙ g); inv g; u ∈ 𝒱 g; finalVertex g u ⟧ ⟹
  close g' u v ⟹ close g u v"
by(simp add:close_def next_plane0_finalVertex_facesAt_eq)

lemma ExcessTab_final:
 "p ∈ set(ExcessTable g (vertices g)) ⟹ finalVertex g (fst p)"
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:if_split_asm)

lemma ExcessTab_vertex:
 "p ∈ set(ExcessTable g (vertices g)) ⟹ fst p ∈ 𝒱 g"
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:if_split_asm)

lemma fst_set_ExcessTable_subset:
 "fst ` set (ExcessTable g (vertices g)) ⊆ 𝒱 g"
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:if_split_asm)

lemma next_plane0_incr_ExcessNotAt:
 "⟦g' ∈ set (next_plane0⇘p⇙ g); inv g ⟧ ⟹
  ExcessNotAt g None ≤ ExcessNotAt g' None"
apply(frule (1) invariantE[OF inv_inv_next_plane0])
apply(frule (1) mono_ExcessTab)
apply(simp add: ExcessNotAt_def ExcessNotAtRec_conv_Max[OF _ _ dist_ExcessTab]
  fst_set_ExcessTable_subset)
apply(rule Max_mono)
  prefer 2 apply (simp add: sep_ne)
 prefer 2 apply (simp)
apply auto
apply(rule_tac x=P in exI)
apply auto
apply(subgoal_tac "fst ` P ⊆ 𝒱 g'")
 prefer 2 apply (blast dest: ExcessTab_vertex)
apply(subgoal_tac "fst ` P ⊆ 𝒱 g")
 prefer 2 apply (blast dest: ExcessTab_vertex)
apply(simp add:sep_conv)
apply (blast intro:close_antimono ExcessTab_final ExcessTab_vertex)
done
(* close -> in neibhood ?? *)


lemma next_plane0_incr_squander_lb:
 "⟦g' ∈ set (next_plane0⇘p⇙ g); inv g ⟧ ⟹
  squanderLowerBound g ≤ squanderLowerBound g'"
apply(simp add:squanderLowerBound_def)
apply(frule (1) next_plane0_incr_ExcessNotAt)
apply(clarsimp simp add:next_plane0_def split:if_split_asm)
apply(drule (4) genPoly_incr_facesquander_lb)
apply arith
done

lemma inv_notame:
 "⟦g' ∈ set (next_plane0⇘p⇙ g); inv g; notame7 g⟧
  ⟹ notame7 g'"
apply(simp add:notame_def notame7_def tame11b_def is_tame13a_def tame10ub_def del:disj_not1)
apply(frule inv_mgp)
apply(frule (1) next_plane0_vertices_subset)
apply(erule disjE)
 apply(simp add:vertices_graph)
apply(rule disjI2)
apply(erule disjE)
 apply clarify
 apply(frule (2) next_plane0_incr_degree)
 apply(frule (2) next_plane0_incr_except)
 apply (force split:if_split_asm)
apply(frule (1) next_plane0_incr_squander_lb)
apply(arith)
done


lemma inv_inv_notame:
 "invariant(λg. inv g ∧ notame7 g) next_plane⇘p⇙"
apply(simp add:invariant_def)
apply(blast intro: inv_notame mgp_next_plane0_if_next_plane[OF inv_mgp]
       invariantE[OF inv_inv_next_plane])
done


lemma untame_notame:
 "untame (λg. inv g ∧ notame7 g)"
proof(clarsimp simp add: notame_def notame7_def untame_def tame11b_def is_tame13a_def tame10ub_def
                         linorder_not_le linorder_not_less)
  fix g assume "final g" "inv g" "tame g"
    and cases: "15 < countVertices g ∨
                (∃v∈𝒱 g. (except g v = 0 ⟶ 7 < degree g v) ∧
                            (0 < except g v ⟶ 6 < degree g v))
                ∨ squanderTarget ≤ squanderLowerBound g"
                (is "?A ∨ ?B ∨ ?C" is "_ ∨ (∃v∈𝒱 g. ?B' v) ∨ _")
  from cases show False
  proof(elim disjE)
    assume ?B
    then obtain v where v: "v ∈𝒱 g" "?B' v" by auto
    show False
    proof cases
      assume "except g v = 0"
      thus False using ‹tame g› v by(auto simp: tame_def tame11b_def)
    next
      assume "except g v ≠ 0"
      thus False using ‹tame g› v
        by(auto simp: except_def filter_empty_conv tame_def tame11b_def
          minGraphProps_facesAt_eq[OF inv_mgp[OF ‹inv g›]] split:if_split_asm)
    qed
  next
    assume ?A
    thus False using ‹tame g›  by(simp add:tame_def tame10_def)
  next
    assume ?C
    thus False using total_weight_lowerbound[OF ‹inv g› ‹final g› ‹tame g›]
      ‹tame g›  by(force simp add:tame_def tame13a_def)
  qed
qed


lemma polysizes_tame:
 "⟦ g' ∈ set (generatePolygon n v f g); inv g; f ∈ set(nonFinals g);
   v ∈ 𝒱 f; 3 ≤ n; n < 4+p; n ∉ set(polysizes p g) ⟧
 ⟹ notame7 g'"
apply(frule (4) in_next_plane0I)
apply(frule (4) genPoly_incr_facesquander_lb)
apply(frule (1) next_plane0_incr_ExcessNotAt)
apply(simp add: notame_def notame7_def is_tame13a_def faceSquanderLowerBound_def
           polysizes_def squanderLowerBound_def)
done

lemma genPolyTame_notame:
 "⟦ g' ∈ set (generatePolygon n v f g); g' ∉ set (generatePolygonTame n v f g);
    inv g; 3 ≤ n ⟧
  ⟹ notame7 g'"
by(fastforce simp:generatePolygon_def generatePolygonTame_def enum_enumerator
                 notame_def notame7_def)

declare upt_Suc[simp del] (* FIXME global? *)
lemma excess_notame:
 "⟦ inv g; g' ∈ set (next_plane⇘p⇙ g); g' ∉ set (next_tame0 p g) ⟧
       ⟹ notame7 g'"
apply(frule (1) mgp_next_plane0_if_next_plane[OF inv_mgp])
apply(auto simp add:next_tame0_def next_plane_def split:if_split_asm)
apply(rename_tac n)
apply(case_tac "n ∈ set(polysizes p g)")
 apply(drule bspec) apply assumption
 apply(simp add:genPolyTame_notame)
apply(subgoal_tac "minimalFace (nonFinals g) ∈ set(nonFinals g)")
 prefer 2 apply(simp add:minimalFace_def)
apply(subgoal_tac "minimalVertex g (minimalFace (nonFinals g)) ∈ 𝒱(minimalFace (nonFinals g))")
 apply(blast intro:polysizes_tame)
apply(simp add:minimalVertex_def)
apply(rule minimal_in_set)
apply(erule mgp_vertices_nonempty[OF inv_mgp])
apply(simp add:nonFinals_def)
done
declare upt_Suc[simp]


lemma next_tame0_comp: "⟦ Seed⇘p⇙ [next_plane p]→* g; final g; tame g ⟧
 ⟹ Seed⇘p⇙ [next_tame0 p]→* g"
apply(rule filterout_untame_succs[OF inv_inv_next_plane inv_inv_notame
  untame_notame])
    apply(blast intro:excess_notame)
   apply assumption
  apply(rule inv_Seed)
 apply assumption
apply assumption
done

lemma inv_inv_next_tame0: "invariant inv (next_tame0 p)"
by(rule inv_subset[OF inv_inv_next_plane next_tame0_subset_plane])

lemma inv_inv_next_tame: "invariant inv next_tame⇘p⇙"
apply(simp add:next_tame_def)
apply(rule inv_subset[OF inv_inv_next_tame0])
apply auto
done

lemma mgp_TameEnum: "g ∈ TameEnum⇘p⇙ ⟹ minGraphProps g"
by (unfold TameEnumP_def)
   (blast intro: RTranCl_inv[OF inv_inv_next_tame] inv_Seed inv_mgp)


end