Up to index of Isabelle/HOL/Tame
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
lemma help:
(∃x. (∃y∈A. x = f y) ∧ P x) = (∃y∈A. P (f y))
lemma tame3_is_tame3:
tame3 g ==> is_tame3 g
lemma untame_negFin:
[| Invariants.inv g; final g; tame g |] ==> is_tame g
lemma next_tame_comp:
[| tame g; final g; Seedp [next_tame1p]->* g |] ==> Seedp [next_tamep]->* g