# Theory LowerBound

Up to index of Isabelle/HOL/Tame

theory LowerBound
imports PlaneProps ScoreProps
begin

```(*  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 ==>
(*>*)

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 w: "∑f ∈ faces g w f < squanderTarget"
(*<*)
"!!f. f ∈ set (faces g) ==> \<d> |vertices f| ≤ w f"
(*>*) (* *)

have "squanderLowerBound g
= ExcessNotAt g None + faceSquanderLowerBound g"

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}"

moreover from v3 have "v3 ∈ set V"
with v3 pS c have "set (vertices f) ∩ set V = {v3}"
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)" (*<*)
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"
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" (*<*)

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```