Theory TameEnumProps

(*  ID:         $Id: TameEnumProps.thy,v 1.3 2006/01/11 19:40:46 nipkow Exp $
    Author:     Gertrud Bauer, Tobias Nipkow
*)

header "Properties of Tame Graph Enumeration (2)"

theory TameEnumProps
imports GeneratorProps
begin


text{* Completeness of filter for final graphs. *}

(*
lemma tame2_is_tame2: "tame2 g ==> is_tame2 g"
apply(auto simp: is_tame2_def tame2_def ok3_def)
apply(fastsimp simp:nat_number length_Suc_conv
  intro!:norm_eq_if_face_cong[OF congs_sym, THEN sym])
done
*)

lemma help: "(EX x. (EX y:A. x = f y) & P x) = (EX y:A. P(f y))"
by blast

lemma tame3_is_tame3: "tame3 g ==> is_tame3 g"
apply(clarsimp simp: tame3_def is_tame3_def nat_number length_Suc_conv)
apply((erule allE)+, erule impE, blast)
apply(simp add: ok4_def ok42_def tame_quad_def norm_subset_def
  pr_iso_subseteq_def pr_iso_in_def image_def
  ex_disj_distrib bex_disj_distrib help conj_disj_distribL)
apply(erule disjE, rule disjI1)
apply(fastsimp intro!:norm_eq_if_face_cong simp:tameConf1_def)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf2_def intro!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf2_def dest!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf3_def intro!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf3_def intro!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf3_def intro!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf3_def intro!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf4_def intro!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp intro!:norm_eq_if_face_cong simp:tameConf1_def)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf2_def intro!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf2_def dest!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf3_def intro!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf3_def intro!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf3_def intro!:norm_eq_if_face_cong)
apply(rule disjI2, erule disjE, rule disjI1)
apply(fastsimp simp: tameConf3_def intro!:norm_eq_if_face_cong)
apply(rule disjI2)
apply(fastsimp simp: tameConf4_def intro!:norm_eq_if_face_cong)
done


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 "tame45 g" using tame by(auto simp:tame_def)
next
  show "tame6 g" using tame by(auto simp:tame_def)
next
  show "tame8 g" using tame by(auto simp:tame_def)
next
  show "is_tame3 g" using tame by(simp add:tame_def tame3_is_tame3)
next
  from tame obtain w where "admissible w g"
    and "∑f ∈ faces g w f < squanderTarget" by(auto simp:tame_def tame7_def)
  moreover have "squanderLowerBound g ≤  ∑f ∈ faces g w f"
    by (rule total_weight_lowerbound)
  ultimately show "is_tame7 g" by(auto simp:is_tame7_def)
qed


lemma next_tame_comp:
 "[| tame g; final g; Seedp [next_tame1 p]->* g |]
 ==> Seedp [next_tamep]->* g"
apply (unfold next_tame_def)
apply(rule filter_tame_succs[OF inv_inv_next_tame1])
     apply(simp add:next_tame1_def 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