Up to index of Isabelle/HOL/Tame
theory LowerBound(* ID: $Id: LowerBound.thy,v 1.2 2006/01/11 19:40:45 nipkow Exp $
Author: Gertrud Bauer
*)
header {* Correctness of Lower Bound for Final Graphs *}
theory LowerBound
imports PlaneProps ScoreProps
begin
(*<*)
lemma trans1:
"(l::nat) = a1 + a2 + (a3 + a4) ==> a1 + a3 = r ==> l = r + a2 + a4"
by simp
lemma trans2: "(l::nat) = a1 + a2 + a3 ==> a1 ≤ r ==> l ≤ r + a2 + a3"
by simp
lemma trans3:
"(l::nat) ≤ a1 + a2 + (a3 + a4) ==> a2 + a3 ≤ r ==> l ≤ a1 + r + a4"
by simp
lemma trans4: "(l::nat) ≤ a1 + a2 + a3 ==> a3 ≤ r ==> l ≤ a1 + a2 + r"
by simp
lemma trans5: "(l::nat) ≤ a1 + a2 + a3 ==> a2 + a3 = r ==> l ≤ a1 + r"
by simp
lemma trans6: "(a::nat) = b1 + (b2 + b3) + b4 ==> b3 = 0 ==>
a = b1 + b2 + b4" by (simp add: add_ac)
(*>*)
theorem total_weight_lowerbound:
"inv g ==> final g ==> tame g ==> admissible w g ==>
∑f ∈ faces g w f < squanderTarget ==>
squanderLowerBound g ≤ ∑f ∈ faces g w f"
proof -
assume final: "final g" and tame: "tame g" and pl: "inv g"
assume admissible: "admissible w g"
assume w: "∑f ∈ faces g w f < squanderTarget"
(*<*)
from admissible have admissible1:
"!!f. f ∈ set (faces g) ==> \<d> |vertices f| ≤ w f"
by (simp add: admissible_def admissible1_def)
(*>*) (* *)
have "squanderLowerBound g
= ExcessNotAt g None + faceSquanderLowerBound g"
by (simp add: squanderLowerBound_def)
txt {* We expand the definition of @{text "faceSquanderLowerBound"}. *}
also have "faceSquanderLowerBound g = ∑f ∈ faces g \<d> |vertices f|" (*<*)
by (simp add: faceSquanderLowerBound_def final) (*>*)
txt {* We expand the definition of @{text "ExcessNotAt"}. *}
also from ExcessNotAt_eq[OF pl[THEN inv_mgp] final] obtain V
where eq: "ExcessNotAt g None = ∑v ∈ V ExcessAt g v"
and pS: "preSeparated g (set V)"
and V_subset: "set V ⊆ set(vertices g)"
and V_distinct: "distinct V" (*<*)
by (blast) note eq
txt {* We partition V in two disjoint subsets $V1, V2$,
where $V2$ contains all exceptional vertices, $V1$ all
not exceptional vertices. *}
also def V1 ≡ "[v ∈ V. except g v = 0]"
def V2 ≡ "[v ∈ V. except g v ≠ 0]" (*<*)
have s: "set V1 ⊆ set V" by (auto simp add: V1_def)
with pS obtain pSV1: "preSeparated g (set V1)"
by (auto dest: preSeparated_subset)
from V_distinct obtain V1_distinct: "distinct V1"
by (unfold V1_def) (auto dest: distinct_filter)
obtain noExV1: "noExceptionals g (set V1)"
by (auto simp add: V1_def noExceptionals_def
exceptionalVertex_def)
(*>*) (* *)
have "(∑v ∈ V ExcessAt g v)
= (∑v ∈ V1 ExcessAt g v) + (∑v ∈ V2 ExcessAt g v)" (*<*)
by (simp only: V1_def V2_def ListSum_compl) (*>*)
txt {* We partition @{text "V2"} in two disjoint subsets,
$V4$ contains all exceptional vertices of degree $\neq 5$
$V3$ contains all exceptional vertices of degree $5$.
*}
also def V4 ≡ "[v ∈ V2. degree g v ≠ 5]"
def V3 ≡ "[v ∈ V2. degree g v = 5]"
(*<*)
with pS V2_def have "preSeparated g (set V3)"
by (rule_tac preSeparated_subset) auto
with V3_def V2_def obtain V3: "separated g (set V3)"
by (simp add: separated_def preSeparated_def separated1_def
separated4_def)
from V_subset obtain V3_subset: "set V3 ⊆ set (vertices g)"
by (auto simp add: V3_def V2_def)
(*>*)
have "(∑v ∈ V2 ExcessAt g v)
= (∑v ∈ V3 ExcessAt g v) + ∑v ∈ V4 ExcessAt g v" (*<*)
by (simp add: V4_def V3_def ListSum_compl) (*>*) (* *)
txt {* We partition @{text "faces g"} in two disjoint subsets:
$F1$ contains all faces that contain a vertex of $V1$,
$F2$ the remaining faces. *}
also def F1 ≡ "[f∈faces g . ∃ v ∈ set V1. f ∈ set (facesAt g v)]"
def F2 ≡ "[f∈faces g . ¬(∃ v ∈ set V1. f ∈ set (facesAt g v))]"
have "∑f ∈ faces g \<d> |vertices f|
= (∑f ∈ F1 \<d> |vertices f| ) + ∑ f ∈ F2 \<d> |vertices f|" (*<*)
by (simp only: ListSum_compl F1_def F2_def) (*>*) (* *)
txt {* We split up @{text "F2"} in two disjoint subsets: *}
also def F3 ≡ "[f ∈ F2. ∃v ∈ set V3. f ∈ set (facesAt g v)]"
def F4 ≡ "[f ∈ F2. ¬ (∃v ∈ set V3. f ∈ set (facesAt g v))]"
have F3: "F3 = [f∈faces g . ∃v ∈ set V3. f ∈ set (facesAt g v)]"
proof(simp add: F3_def F2_def, intro filter_eqI iffI conjI)
fix f assume "f ∈ set (faces g)"
with final have fin: "final f" by (rule finalGraph_face)
assume "∃v3∈set V3. f ∈ set (facesAt g v3)"
then obtain v3 where v3: "v3 ∈ set V3" "f ∈ set (facesAt g v3)"
by auto
show "(∀v1∈set V1. f ∉ set (facesAt g v1))"
proof (intro ballI notI)
fix v1 assume v1: "v1 ∈ set V1"
with v3 have "v1 ≠ v3"
by (auto simp add: V3_def V2_def V1_def)
moreover assume f: "f ∈ set (facesAt g v1)"
with v1 fin have c: "|vertices f| ≤ 4"
by (auto simp add: V1_def except_def)
from v1 have "v1 ∈ set V" by (simp add: V1_def)
with f pS c have "set (vertices f) ∩ set V = {v1}"
by (simp add: preSeparated_def separated3_def)
moreover from v3 have "v3 ∈ set V"
by (simp add: V3_def V2_def)
with v3 pS c have "set (vertices f) ∩ set V = {v3}"
by (simp add: preSeparated_def separated3_def)
ultimately show False by auto
qed
qed simp
have "(∑f∈F2 \<d> |vertices f| )
= (∑f∈F3 \<d> |vertices f| ) + ∑f∈F4 \<d> |vertices f|" (*<*)
by (simp only: F3_def F4_def ListSum_compl) (*>*) (* *)
txt_raw {* \newpage *}
txt {* ($E_1$) From the definition of @{text "ExcessAt"} we have *}
also have "(∑v ∈ V1 ExcessAt g v) + ∑ f ∈ F1 \<d> |vertices f|
= ∑v ∈ V1 \<b> (tri g v) (quad g v)"
proof -
from noExV1 V_subset have "∑ f ∈ F1 \<d> |vertices f|
= ∑v ∈ V1 (tri g v * \<d> 3 + quad g v * \<d> 4)"
apply (unfold F1_def) apply (rule_tac squanderFace_distr2) apply assumption+
apply (unfold V1_def) by auto
also have "(∑v ∈ V1 ExcessAt g v)
+ ∑v ∈ V1 (tri g v * \<d> 3 + quad g v * \<d> 4)
= ∑v ∈ V1 (ExcessAt g v
+ tri g v * \<d> 3 + quad g v * \<d> 4)" (*<*)
by (simp add: ListSum_add add_ac) (*>*) (* FIXME also takes too long *)
also from pl final tame have "… = ∑v ∈ V1 \<b> (tri g v) (quad g v)"
by (rule_tac ListSum_eq)
(fastsimp simp add: V1_def V_subset[THEN subsetD] intro: excess_eq1)
finally show ?thesis .
qed
txt {* ($E_2$) For all exceptional vertices of degree $5$
@{text "excess"} returns @{text "a (tri g v)"}. *}
also (trans1)
from pl final V_subset have
"(∑v ∈ V3 ExcessAt g v) = ∑v ∈ V3 \<a> (tri g v)" (*<*)
apply (rule_tac ListSum_eq)
apply (simp add: V3_def V2_def excessAtType_def ExcessAt_def degree_eq)
apply (subgoal_tac "finalVertex g v")
apply force by(blast intro: finalVertexI) (*>*) (* *)
txt {* ($E_3$) For all exceptional vertices of degree $\neq 5$
@{text "ExcessAt"} returns 0. *}
also from pl final have "(∑v ∈ V4 ExcessAt g v) = ∑v ∈ V4 0" (*<*) apply (rule_tac ListSum_eq)
by (auto simp add: V2_def V4_def excessAtType_def ExcessAt_def degree_eq) (*>*) (* *)
also have "… = 0" (*<*) by simp (*>*) (* *)
txt {* ($A_1$) We use property @{text "admissible2"}. *}
also(trans6) have
"∑v ∈ V1 \<b> (tri g v) (quad g v) ≤ (∑v ∈ V1 ∑f ∈ facesAt g v w f)"
proof (rule_tac ListSum_le)
fix v assume "v ∈ set V1"
with V1_def V_subset have "v ∈ set (vertices g)" (*<*) by auto (*>*) (* *)
with admissible show "\<b> (tri g v) (quad g v) ≤ ∑f ∈ facesAt g v w f"
using `v ∈ set V1` by (auto simp add:admissible_def admissible2_def V1_def)
qed
also(trans2) from pSV1 V1_distinct V_subset have "… = ∑f ∈ F1 w f"
apply (unfold F1_def) apply (rule_tac preSeparated_disj_Union2)
apply assumption+
apply (unfold V1_def) by auto
txt {* ($A_2$) We use property @{text "admissible4"}. *}
also from admissible V3 V3_subset have
"(∑v∈V3 \<a> (tri g v)) + (∑f∈F3 \<d> |vertices f| ) ≤ ∑f ∈ F3 w f" (*<*)
by (simp add: admissible_def admissible3_def F3) (*>*) (* *)
txt_raw {* \newpage *}
txt {* ($A_3$) We use property @{text "admissible1"}. *}
also(trans3) have "∑ f ∈ F4 \<d> |vertices f| ≤ ∑f ∈ F4 w f"
proof (rule ListSum_le)
fix f assume "f ∈ set F4"
then have f: "f ∈ set (faces g)" (*<*) by (simp add: F4_def F2_def)(*>*) (* *)
with admissible1 f show "\<d> |vertices f| ≤ w f" by (simp)
qed
txt {* We reunite $F3$ and $F4$. *}
also(trans4) have "(∑ f ∈ F3 w f) + (∑ f ∈ F4 w f) = (∑ f ∈ F2 w f)" (*<*)
by (simp only: F3_def F4_def ListSum_compl) (*>*) (* *)
txt {* We reunite $F1$ and $F2$. *}
also(trans5) have "(∑ f ∈ F1 w f) + (∑ f ∈ F2 w f) = ∑f ∈ faces g w f" (*<*)
by (simp only: F1_def F2_def ListSum_compl) (*>*) (* *)
finally show "squanderLowerBound g ≤ ∑f ∈ faces g w f" .
qed
end
lemma trans1:
[| l = a1.0 + a2.0 + (a3.0 + a4.0); a1.0 + a3.0 = r |] ==> l = r + a2.0 + a4.0
lemma trans2:
[| l = a1.0 + a2.0 + a3.0; a1.0 ≤ r |] ==> l ≤ r + a2.0 + a3.0
lemma trans3:
[| l ≤ a1.0 + a2.0 + (a3.0 + a4.0); a2.0 + a3.0 ≤ r |] ==> l ≤ a1.0 + r + a4.0
lemma trans4:
[| l ≤ a1.0 + a2.0 + a3.0; a3.0 ≤ r |] ==> l ≤ a1.0 + a2.0 + r
lemma trans5:
[| l ≤ a1.0 + a2.0 + a3.0; a2.0 + a3.0 = r |] ==> l ≤ a1.0 + r
lemma trans6:
[| a = b1.0 + (b2.0 + b3.0) + b4.0; b3.0 = 0 |] ==> a = b1.0 + b2.0 + b4.0
theorem total_weight_lowerbound:
[| Invariants.inv g; final g; tame g; admissible w g; ListSum (faces g) w < squanderTarget |] ==> squanderLowerBound g ≤ ListSum (faces g) w