Theory GeneratorProps

(*  Author:  Tobias Nipkow  *)

header "Properties of Tame Graph Enumeration (1)"

theory GeneratorProps
imports Plane1Props Generator TameProps LowerBound
begin

lemma genPolyTame_spec:
 "generatePolygonTame n v f g = [g' \<leftarrow> 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 ∈ \<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 ∈ \<V> f" "3 ≤ n"
shows "faceSquanderLowerBound g' ≥ faceSquanderLowerBound g + \<d> 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 + \<d> |vertices f|"
  proof(unfold faceSquanderLowerBound_def)
    have "(∑⇘f∈finals g⇙ \<d> |vertices f| ) + \<d> |vertices f| =
          (∑f∈set(finals g). \<d> |vertices f| ) + \<d> |vertices f|"
      using dist by(simp add:finals_def ListSum_conv_setsum)
    also have "… = (∑f∈set(finals g) ∪ {f}. \<d> |vertices f| )"
      using f by simp
    also have "… ≤ (∑f∈set(finals g'). \<d> |vertices f| )"
      using f subset by(fastforce intro!: setsum_mono3)
    also have "… = (∑⇘f∈finals g'⇙ \<d> |vertices f| )"
      using dist' by(simp add:finals_def ListSum_conv_setsum)
    finally show "(∑⇘f∈finals g⇙ \<d> |vertices f| ) + \<d> |vertices f|
          ≤ (∑⇘f∈finals g'⇙ \<d> |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 \<leftarrow> ps. ¬ close g u (fst p)]"
by (induct ps) (auto simp: deleteAroundCons close_def)


lemma close_sym: assumes mgp: "minGraphProps g" and ug: "u : \<V> 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 <= \<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 : \<V> g" using `u : V` `V <= \<V> g` by blast
    note uf = minGraphProps6[OF mgp `u : \<V> 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 ∈ \<V> f" using `u ∈ \<V> f` by simp
        moreover have "|vertices f| ≤ 4" using 4 by arith
        ultimately show False using sep f uv `u ∈ \<V> f`
          apply(unfold separated_def separated⇣2_def separated⇣3_def)
(* why does blast get stuck? *)
          apply(subgoal_tac "f • (f • u) ∈ \<V> 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 : \<V> g" using a(1) `V <= \<V> g` by blast
      show False using a not_cl mgp_facesAt_no_loop[OF mgp `v : \<V> g` a(2)]
        by(fastforce simp: close_def split:split_if_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 : \<V> g" using `v : 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 ∈ \<V> f" and "u ∈ V"
        have "u = v"
        proof cases
          assume 3: "|vertices f| = 3"
          hence "\<V> 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:split_if_asm)
          }
          moreover
          { assume "u = f • (f • v)"
            hence fu: "f • u = v"
              by(simp add: tri_next3_id[OF 3 distf `v ∈ \<V> f`])
            hence "(u,v) ∈ \<E> f" using nextVertex_in_edges[OF `u ∈ \<V> f`]
              by(simp add:fu)
            then obtain f' where "f' ∈ set(facesAt g v)" "(v,u) ∈  \<E> 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:split_if_asm)
          }
          ultimately show "u=v" using `u ∈ \<V> 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 "\<V> 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:split_if_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:split_if_asm)
          }
          moreover
          { assume "u = f • (f • (f • v))"
            hence fu: "f • u = v"
              by(simp add: quad_next4_id[OF 4 distf `v ∈ \<V> f`])
            hence "(u,v) ∈ \<E> f" using nextVertex_in_edges[OF `u ∈ \<V> f`]
              by(simp add:fu)
            then obtain f' where "f' ∈ set(facesAt g v)" "(v,u) ∈  \<E> 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:split_if_asm)
          }
          ultimately show "u=v" using `u ∈ \<V> f` by blast
        qed
      }
      thus "\<V> f ∩ V = {v}" using `v ∈ V` vf by blast
    qed
  qed
qed


lemma fin_aux: "finite B ==> finite{f A|A. A ⊆ B ∧ P A}"
apply(rule finite_subset[where B = "f ` Pow B"])
 apply blast
apply simp
done

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) <= \<V> 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 add:Max_def)
  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 o close g (fst p)"])
      apply(simp add: filter_map o_def)
      done
    have "fst p : \<V> g" and "fst ` set ps <= \<V> g"
      using subset Cons by auto
    have sub1: "!!P Q. P <= {x : set ps. Q x} ==> fst ` P <= \<V> g"
      using subset Cons by auto
    have sub2: "!!P Q. P <= insert p {x : set ps. Q x} ==> fst ` P <= \<V> g"
      using subset Cons by auto
    have sub3: "!!P. P <= insert p (set ps) ==> fst ` P <= \<V> g"
      using subset Cons by auto
    have "!!a. set (map fst (deleteAround g a ps)) ⊆ \<V> g"
      using deleteAround_subset[of g _ ps] subset Cons
      by auto
    hence "ExcessNotAtRec ps0 g = max (Max(?M ps)) (snd p + Max(?M ?ps))"
      using Cons IH subset le dist dist' by (cases p) simp
    also have "snd p + Max (?M ?ps) =
      Max {snd p + (∑p∈P. snd p) | P. ?S ?ps P}"
      by (auto simp add:add_Max_commute fin_aux sep_ne intro!: arg_cong [where f=Max])
    also have "{snd p + (∑p∈P. snd p) |P. ?S ?ps P} =
      {setsum 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!: setsum_insert[THEN trans,symmetric] elim: finite_subset)
      apply(rule_tac x=P in exI)
      apply(fastforce intro!: setsum_insert[THEN trans] elim: finite_subset)
      done
    also have "… = {setsum 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) <= \<V> g` `fst p : \<V> 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 "… = {setsum 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 ∪ {setsum snd P |P.
            P ⊆ insert p (set ps) ∧ p ∈ P ∧ separated g (fst ` P)})"
      (is "_ = Max ?U")
    proof -
      have "{setsum 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 : \<V> g` by(simp add:sep_conv[OF mgp])
      thus ?thesis by(simp add: Max_Un fin_aux 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:split_if_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 ∈ \<V> 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:split_if_asm)

lemma ExcessTab_vertex:
 "p ∈ set(ExcessTable g (vertices g)) ==> fst p ∈ \<V> g"
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:split_if_asm)

lemma fst_set_ExcessTable_subset:
 "fst ` set (ExcessTable g (vertices g)) ⊆ \<V> g"
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:split_if_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 add: fin_aux)
apply auto
apply(rule_tac x=P in exI)
apply auto
apply(subgoal_tac "fst ` P <= \<V> g'")
 prefer 2 apply (blast dest: ExcessTab_vertex)
apply(subgoal_tac "fst ` P <= \<V> 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:split_if_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:split_if_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∈\<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∈\<V> g. ?B' v) ∨ _")
  from cases show False
  proof(elim disjE)
    assume ?B
    then obtain v where v: "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:split_if_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 ∈ \<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:split_if_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)) ∈ \<V>(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