Theory TameEnumProps

(*  Author:  Gertrud Bauer, Tobias Nipkow  *)

section "Properties of Tame Graph Enumeration (2)"

theory TameEnumProps
imports GeneratorProps
begin


text‹Completeness of filter for final graphs.›

lemma untame_negFin:
assumes pl: "inv g" and fin: "final g" and tame: "tame g"
shows "is_tame g"
proof (unfold is_tame_def, intro conjI)
  show "tame10 g" using tame by(auto simp:tame_def)
next
  show "tame11a g" using tame by(auto simp:tame_def)
next
  show "tame12o g" using tame by(auto simp:tame_def)
next
next
  from tame obtain w where adm: "admissible w g"
    and sqn: "(∑⇘f ∈ faces g⇙ w f) < squanderTarget" by(auto simp:tame_def tame13a_def)
  moreover have "squanderLowerBound g ≤  (∑⇘f ∈ faces g⇙ w f)"
    using pl fin tame adm sqn by (rule total_weight_lowerbound)
  ultimately show "is_tame13a g" by(auto simp:is_tame13a_def)
qed


lemma next_tame_comp:
 "⟦ tame g; final g; Seed⇘p⇙ [next_tame0 p]→* g ⟧
 ⟹ Seed⇘p⇙ [next_tame⇘p⇙]→* g"
apply (unfold next_tame_def)
apply(rule filter_tame_succs[OF inv_inv_next_tame0])
     apply(simp add:next_tame0_def finalGraph_def)
    apply(rule context_conjI)
     apply(simp)
    apply(blast dest:untame_negFin)
   apply assumption
  apply(rule inv_Seed)
 apply assumption+
done


end