Theory LowerBound (Isabelle repository version)

(*  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₁:
   "!!f. f ∈ set (faces g) ==> \<d> |vertices f| ≤ w f"
    by (simp add: admissible_def admissible₁_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₁_def
      separated₄_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₃_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₃_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₂"}. *}

  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₂_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₄"}. *}

  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₃_def F3) (*>*) (* *)

  txt_raw {* \newpage *}
  txt {* ($A_3$) We use property @{text "admissible₁"}. *}

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