Theory LowerBound

(*  Author:  Gertrud Bauer  *)

section ‹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: ac_simps)
(*>*)

(* FIXME in Tame: admissibility should be expressed via sum!
   → convert a lot of listsum to sum
*)

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) ⟹ 𝖽 |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 ‹faceSquanderLowerBound›.›

  also have "faceSquanderLowerBound g = (∑⇘f ∈ faces g⇙ 𝖽 |vertices f| )" (*<*)
    by (simp add: faceSquanderLowerBound_def final) (*>*)

  txt ‹We expand the definition of ‹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:  "separated 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
  define V1 where "V1 = [v ← V. except g v = 0]"
  define V2 where "V2 = [v ← V. except g v ≠ 0]"  (*<*)
  have s: "set V1 ⊆ set V" by (auto simp add: V1_def)
  with pS obtain pSV1: "separated g (set V1)"
    by (auto dest: separated_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_subset_simp: "⋀v. v: set V ⟹ v : 𝒱 g"
    using V_subset by fast

  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 ‹V2› in two disjoint subsets,
  $V4$ contains all exceptional vertices of degree $\neq 5$
  $V3$ contains all exceptional vertices of degree $5$.
›

  also
  define V4 where "V4 = [v ← V2. vertextype g v ≠ (5,0,1)]"
  define V3 where "V3 = [v ← V2. vertextype g v = (5,0,1)]"

(*<*)
  with pS V2_def have V3: "separated g (set V3)"
    by (rule_tac separated_subset) auto
  have "distinct V3" by(simp add:V3_def V2_def ‹distinct V›)
(*
  with V3_def V2_def obtain V3: "separated g (set V3)"
    by (simp add: vertextype_def separated_def preSeparated_def separated⇩1_def
      separated⇩4_def)
*)
  from V_subset obtain V3_subset: "set V3 ⊆ 𝒱 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  ‹faces g› in two disjoint subsets:
  $F1$ contains all faces that contain a vertex of $V1$,
  $F2$ the remaining faces.›

  also
  define F1 where "F1 = [f ← faces g . ∃ v ∈ set V1. f ∈ set (facesAt g v)]"
  define F2 where "F2 = [f ← faces g . ¬(∃ v ∈ set V1. f ∈ set (facesAt g v))]"

  have "(∑⇘f ∈ faces g⇙ 𝖽 |vertices f| )
      = (∑⇘f ∈ F1⇙ 𝖽 |vertices f| ) + (∑⇘ f ∈ F2⇙ 𝖽 |vertices f| )" (*<*)
    by (simp only: ListSum_compl F1_def F2_def) (*>*) (* *)

  txt ‹We split up ‹F2› in two disjoint subsets:›

  also
  define F3 where "F3 = [f←F2. ∃v ∈ set V3. f ∈ set (facesAt g v)]"
  define F4 where "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: separated_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: separated_def separated⇩3_def)
       ultimately show False by auto
    qed
  qed simp

  have "(∑⇘f∈F2⇙ 𝖽 |vertices f| )
   = (∑⇘f∈F3⇙ 𝖽 |vertices f| ) + (∑⇘f∈F4⇙ 𝖽 |vertices f| )" (*<*)
    by (simp only: F3_def F4_def ListSum_compl) (*>*) (* *)

  text_raw ‹\newpage›
  txt ‹($E_1$) From the definition of ‹ExcessAt› we have›

  also have "(∑⇘v ∈ V1⇙ ExcessAt g v) + (∑⇘ f ∈ F1⇙ 𝖽 |vertices f| )
      = (∑⇘v ∈ V1⇙ 𝖻 (tri g v) (quad g v))"
  proof -
    from noExV1 V_subset have "(∑⇘ f ∈ F1⇙ 𝖽 |vertices f| )
      = (∑⇘v ∈ V1⇙ (tri g v *  𝖽 3 + quad g v * 𝖽 4))"
    apply (unfold F1_def)
    apply (rule_tac squanderFace_distr2)
    apply (rule pl)
    apply (rule final)
    apply (rule noExV1)
    apply (rule pSV1)
    apply (rule V1_distinct)
    apply (unfold V1_def)
    apply auto
    done

    also have "(∑⇘v ∈ V1⇙ ExcessAt g v)
      + (∑⇘v ∈ V1⇙ (tri g v * 𝖽 3 + quad g v * 𝖽 4))
      = (∑⇘v ∈ V1⇙ (ExcessAt g v
      + tri g v * 𝖽 3 + quad g v * 𝖽 4))" (*<*)
      by (simp add: ListSum_add ac_simps) (*>*) (* FIXME  also takes too long *)
    also from pl final tame have "… = (∑⇘v ∈ V1⇙ 𝖻 (tri g v) (quad g v))"
      by (rule_tac ListSum_eq)
         (fastforce 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$
  ‹excess› returns ‹a (tri g v)›.›

  also (trans1)
    from pl final V_subset have
    "(∑⇘v ∈ V3⇙ ExcessAt g v) = (∑⇘v ∈ V3⇙ 𝖺)" (*<*)
     apply (rule_tac ListSum_eq)
     apply (simp add: V3_def V2_def excessAtType_def ExcessAt_def degree_eq vertextype_def)
     by(blast intro: finalVertexI)
(*     apply force by(blast intro: finalVertexI)*) (*>*) (* *)

  txt ‹($E_3$) For all exceptional vertices of degree $\neq 5$
  ‹ExcessAt› returns 0.›

  also from pl final tame have "(∑⇘v ∈ V4⇙ ExcessAt g v) = (∑⇘v ∈ V4⇙ 0)" (*<*)
    by (rule_tac ListSum_eq)
       (auto simp: V2_def V4_def excessAtType_def ExcessAt_def degree_eq V_subset_simp tame_def tame12o_def) (*>*) (* *)

  also have "… = 0" (*<*) by simp   (*>*) (* *)

  txt ‹($A_1$) We use property ‹admissible⇩2›.›

  also(trans6) have
  "(∑⇘v ∈ V1⇙ 𝖻 (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 "𝖻 (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 ScoreProps.separated_disj_Union2)
    apply (rule pl)
    apply (rule final)
    apply (rule noExV1)
    apply (rule pSV1)
    apply (rule V1_distinct)
    apply (unfold V1_def)
    apply auto
    done

  txt ‹($A_2$) We use property ‹admissible⇩4›.›

  also have "(∑⇘v∈V3⇙ 𝖺) + (∑⇘f∈F3⇙ 𝖽 |vertices f| ) ≤ (∑⇘f ∈ F3 ⇙w f)" (*<*)
  proof-
    define T where "T = [f←F3. triangle f]"
    define E where "E = [f←F3. ¬ triangle f]"
    have "(∑⇘f∈F3⇙ 𝖽 |vertices f| ) =
      (∑⇘f∈T⇙ 𝖽 |vertices f| ) + (∑⇘f∈E⇙ 𝖽 |vertices f| )"
      by(simp only: T_def E_def ListSum_compl2)
    also have "(∑⇘f∈T⇙ 𝖽 |vertices f| ) =
          (∑⇘f ∈ [f←faces g . ∃v ∈ set V3. f ∈ set (facesAt g v) ∩ Collect triangle]⇙ 𝖽 |vertices f| )"
      by(rule listsum_cong[OF _ HOL.refl])
        (simp add:T_def F3 Int_def)
    also have "… = (∑⇘v ∈ V3⇙ ∑⇘f ∈ filter triangle (facesAt g v)⇙ 𝖽 |vertices f| )"
      by(rule ListSum_V_F_eq_ListSum_F[symmetric, OF ‹inv g› V3 ‹distinct V3› ‹set V3 ⊆ 𝒱 g›])
        (simp add:Ball_def)
    also have "… = 0" by (simp add: squanderFace_def)
    finally have "(∑⇘v∈V3⇙ 𝖺) + (∑⇘f∈F3⇙ 𝖽 |vertices f| ) =
      (∑⇘v∈V3⇙ 𝖺) + (∑⇘f∈E⇙ 𝖽 |vertices f| )" by simp
    also have "(∑⇘f∈E⇙ 𝖽 |vertices f| ) ≤ (∑⇘f∈E⇙ w f )"
      using ‹admissible w g›
      by(rule_tac ListSum_le)
        (simp add: admissible_def admissible⇩1_def E_def F3_def F2_def)
    also have "(∑⇘v∈V3⇙ 𝖺) ≤ (∑⇘v∈V3⇙ ∑⇘f∈filter triangle (facesAt g v)⇙ w(f))"
      using ‹admissible w g›
      by(rule_tac ListSum_le)
        (simp add: admissible_def admissible⇩3_def V3_def V2_def V_subset_simp)
    also have "… = (∑⇘f ∈ [f←faces g . ∃v ∈ set V3. f ∈ set (facesAt g v) ∩ Collect triangle]⇙ w f)"
      by(rule ListSum_V_F_eq_ListSum_F[OF ‹inv g› V3 ‹distinct V3› ‹set V3 ⊆ 𝒱 g›])
        (simp add:Ball_def)
    also have "… = (∑⇘f∈T⇙ w f)"
      by(simp add: T_def F3 Int_def)
    also have "ListSum T w + ListSum E w = ListSum F3 w"
      by(simp add: T_def E_def ListSum_compl2)
    finally show ?thesis by simp
  qed

  text_raw ‹\newpage›
  txt ‹($A_3$) We use property ‹admissible⇩1›.›

  also(trans3) have "(∑⇘ f ∈ F4⇙ 𝖽 |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 "𝖽 |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