Up to index of Isabelle/HOL/Tame

theory LowerBoundimports 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 ==> 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 admissible_{1}: "!!f. f ∈ set (faces g) ==> \<d> |vertices f| ≤ w f" by (simp add: admissible_def admissible_{1}_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 separated_{1}_def separated_{4}_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 separated_{3}_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 separated_{3}_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 "admissible_{2}"}. *} 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 admissible_{2}_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 "admissible_{4}"}. *} 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 admissible_{3}_def F3) (*>*) (* *) txt_raw {* \newpage *} txt {* ($A_3$) We use property @{text "admissible_{1}"}. *} 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 admissible_{1}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