Theory ScoreProps

Up to index of Isabelle/HOL/Tame

theory ScoreProps
imports ListSum TameEnum PlaneProps TameProps
begin

(*  ID:         $Id: ScoreProps.thy,v 1.1 2006/01/04 13:44:06 nipkow Exp $
    Author:     Gertrud Bauer, Tobias Nipkow
*)

header {* Properties of Lower Bound Machinery *}

theory ScoreProps
imports ListSum TameEnum PlaneProps TameProps
begin

lemma deleteAround_empty[simp]: "deleteAround g a [] = []"
  by (simp add: deleteAround_def)

lemma deleteAroundCons:
  "deleteAround g a (p#ps) =
    (if fst p ∈ {v. ∃f ∈ set (facesAt g a).
               length (vertices f) = 4
             ∧ v ∈ {f • a, f • (f • a)}
             ∨ length (vertices f) ≠  4 ∧ v = f • a}
     then deleteAround g a ps
     else p#deleteAround g a ps)"
apply (auto simp add: deleteAround_def)
    apply blast
   apply (fastsimp simp:nextV2)
  apply(drule_tac x = "[f • a, f2 • a]" in bspec)
   apply (fastsimp simp:image_def)
  apply (simp)
 apply(drule_tac x = "[f • a, f2 • a]" in bspec)
  apply (fastsimp simp:image_def)
 apply (simp add:nextV2)
apply(drule_tac x = "[f • a]" in bspec)
 apply (fastsimp simp:image_def)
apply (simp)
done

lemma deleteAround_subset: "set (deleteAround g a ps) ⊆ set ps"
by (simp add: deleteAround_def)

lemma distinct_deleteAround: "distinct (map fst ps) ==>
    distinct (map fst (deleteAround g (fst (a, b)) ps))"
proof (induct ps)
  case Nil then show ?case by simp
next
  case (Cons p ps)
  then have "fst p ∉ fst ` set ps" by simp
  moreover have "set (deleteAround g a ps) ⊆ set ps"
    by (rule deleteAround_subset)
  ultimately have "fst p ∉ fst ` set (deleteAround g a ps)" by auto

  moreover from Cons have "distinct (map fst ps)" by simp
  then have "distinct (map fst (deleteAround g (fst (a, b)) ps))"
    by (rule Cons)
  ultimately show ?case by (simp add: deleteAroundCons)
qed


constdefs
  deleteAround' :: "graph => vertex => (vertex × nat) list =>
    (vertex × nat) list"
  "deleteAround' g v ps ≡
      let fs = facesAt g v;
      vs = (λf. let n1 = f • v;
                n2 = f • n1 in
                if length (vertices f) = 4 then [n1, n2] else [n1]);
      ws = concat (map vs fs) in
      removeKeyList ws ps"


lemma deleteAround_eq: "deleteAround g v ps = deleteAround' g v ps"
apply (auto simp add: deleteAround_def deleteAround'_def split: split_if_asm)
apply (unfold nextV2[THEN eq_reflection], simp)
done

lemma deleteAround_nextVertex:
  "f ∈ set (facesAt g a) ==>
  (f • a, b) ∉ set (deleteAround g a ps)"
  by (auto simp add: deleteAround_eq deleteAround'_def removeKeyList_eq)

lemma deleteAround_nextVertex_nextVertex:
  "f ∈ set (facesAt g a) ==> |vertices f| = 4 ==>
  (f • (f • a), b) ∉ set (deleteAround g a ps)"
  by (auto simp add: deleteAround_eq deleteAround'_def removeKeyList_eq)


lemma deleteAround_prevVertex:
  "minGraphProps g ==> f ∈ set (facesAt g a) ==>
  (f-1 • a, b) ∉ set (deleteAround g a ps)"
proof -
  assume a: "minGraphProps g" "f ∈ set (facesAt g a)"
  have "(f-1 • a, a) ∈ \<E> f" using a
    by(blast intro:prevVertex_in_edges minGraphProps)
  then obtain f' where f': "f' ∈ set(facesAt g a)"
    and e: "(a, f-1 • a) ∈ \<E> f'"
    using a by(blast dest:mgp_edge_face_ex)
  have "(f' • a, b) ∉ set (deleteAround g a ps)" using f'
    by (auto simp add: deleteAround_eq deleteAround'_def removeKeyList_eq)
  moreover have "f' • a = f-1 • a"
    using e by (simp add:edges_face_eq)
  ultimately show ?thesis by simp
qed


lemma deleteAround_separated:
  "minGraphProps g ==> final g ==> |vertices f| ≤ 4 ==> f ∈ set(facesAt g a) ==>
  \<V> f ∩ set [fst p. p ∈ deleteAround g a ps] ⊆ {a}"
  (concl is "?A")
proof -
  assume fin: "final g" and mgp: "minGraphProps g" and 4: "|vertices f| ≤ 4"
  assume f: "f ∈ set (facesAt g a)"
  then have a: "a ∈ \<V> f" using mgp f by(blast intro:minGraphProps)
  have "2 < |vertices f|" using mgp f by(blast intro:minGraphProps)
  with 4 have "|vertices f| = 3 ∨ |vertices f| = 4" by arith
  then show "?A"
  proof
    assume 3: "|vertices f| = 3"
    show "?A"
    proof (rule ccontr)
      assume "¬ ?A"
      then obtain b where b1: "b ≠ a" "b ∈ \<V> f"
        "b ∈ set (map fst (deleteAround g a ps))" by auto
      from mgp f have d: "distinct (vertices f)"
        by(blast intro:minGraphProps)
      with a 3 have "\<V> f = {a, f • a, f • (f • a)}"
          by (rule_tac vertices_triangle)
      also from d a 3 have
        "f • (f • a) = f-1 • a"
        by (simp add: triangle_nextVertex_prevVertex)
      finally have
        "b ∈ {f • a, f-1 • a}"
        using b1 by simp
      with mgp f have "b ∉ set (map fst (deleteAround g a ps))"
      using deleteAround_nextVertex deleteAround_prevVertex by auto
      then show False by contradiction
    qed
  next
    assume 4: "|vertices f| = 4"
    show "?A"
    proof (rule ccontr)
      assume "¬ ?A"
      then obtain b where b1: "b ≠ a" "b ∈ \<V> f"
        "b ∈ set (map fst (deleteAround g a ps))" by auto
      from mgp f have d: "distinct (vertices f)" by(blast intro:minGraphProps)
      with a 4 have "\<V> f = {a, f • a, f • (f • a), f • (f • (f • a))}"
          by (rule_tac vertices_quad)
      also from d a 4 have "f • (f • (f • a)) = f-1 • a"
        by (simp add: quad_nextVertex_prevVertex)
      finally have "b ∈ {f • a, f • (f • a), f-1 • a}"
      using b1 by simp
      with f mgp 4 have "b ∉ set (map fst (deleteAround g a ps))"
      using deleteAround_nextVertex deleteAround_prevVertex
           deleteAround_nextVertex_nextVertex by auto
      then show False by contradiction
    qed
  qed
qed
(*
deleteAround g y loescht nextVertex f a,
nextVertex f (nextVertex f a),
prevVertex f a wird mit nachbarflaeche geloescht.
*)


lemma [iff]: "preSeparated g {}"
  by (simp add: preSeparated_def separated2_def separated3_def)

lemma preSeparated_insert:
assumes mgp: "minGraphProps g" and a: "a ∈ \<V> g"
  and ps: "preSeparated g V"
  and s2: "(!!f. f ∈ set (facesAt g a) ==> f • a ∉ V)"
  and s3: "(!!f. f ∈ set (facesAt g a) ==>
      |vertices f| ≤ 4 ==> \<V> f ∩ V ⊆ {a})"
  shows "preSeparated g (insert a V)"
proof (simp add: preSeparated_def separated2_def separated3_def,
 intro conjI ballI impI)
  fix f assume  "f ∈ set (facesAt g a)"
  then show "f • a ≠ a" by (rule mgp_facesAt_no_loop[OF mgp])
  show "f • a ∉ V" by (rule s2)
next
  fix f v assume v: "f ∈ set (facesAt g v)" and vV: "v ∈ V"
  show "f • v ≠ a"
  proof
    assume f: "f • v = a"
    then obtain f' where f': "f' ∈ set(facesAt g a)" and v: "f' • a = v"
      using mgp_nextVertex_face_ex2[OF mgp v] by blast
    have "f' • a ∈ V" using v by simp
    with f' s2 show False by blast
  qed
  from ps v vV show "f • v ∉ V"
    by (simp add: preSeparated_def separated2_def)
next
  fix f assume f:  "f ∈ set (facesAt g a)" "|vertices f| ≤ 4"
  have "\<V> f ∩ V ⊆ {a}" by (rule_tac s3)
  moreover from mgp f have "a ∈ \<V> f" by(blast intro:minGraphProps)
  ultimately show "\<V> f ∩ insert a V = {a}" by auto
next
  fix v f
  assume a: "v ∈ V" "f ∈ set (facesAt g v)"
    "|vertices f| ≤ 4"
  with ps have v: "\<V> f ∩ V = {v}"
    by (simp add: preSeparated_def separated3_def)
  show  "\<V> f ∩ insert a V = {v}"
  proof cases
    assume "a = v"
    with v mgp a show ?thesis by(blast intro:minGraphProps)
  next
    assume n: "a ≠ v"
    have  "a ∉ \<V> f"
    proof
      assume a2: "a ∈ \<V> f"
      with mgp a have "f ∈ \<F> g" by(blast intro:minGraphProps)
      with mgp a2 have "f ∈ set (facesAt g a)" by(blast intro:minGraphProps)
      with a have "\<V> f ∩ V ⊆ {a}" by (simp add: s3)
      with v have "a = v" by auto
      with n show False by auto
    qed
    with a  v show "\<V> f ∩ insert a V = {v}" by blast
  qed
qed



consts ExcessNotAtRecList :: "(vertex, nat) table => graph => vertex list"
recdef ExcessNotAtRecList "measure (λps. size ps)"
"ExcessNotAtRecList [] = (%g. [])"
"ExcessNotAtRecList (p#ps) = (%g.
  let l1 = ExcessNotAtRecList ps g;
  l2 = ExcessNotAtRecList (deleteAround g (fst p) ps) g in
  if ExcessNotAtRec ps g
   ≤ snd p + ExcessNotAtRec (deleteAround g (fst p) ps) g
  then fst p#l2 else l1)"
(hints recdef_simp: less_Suc_eq_le length_deleteAround)


lemma isTable_deleteAround:
  "isTable E vs ((a,b)#ps) ==> isTable E vs (deleteAround g a ps)"
  by (rule isTable_subset, rule deleteAround_subset,
    rule isTable_Cons)

lemma ListSum_ExcessNotAtRecList:
 "isTable E vs ps ==> ExcessNotAtRec ps g
  = ∑p ∈ ExcessNotAtRecList ps g E p" (is "?T ps ==> ?P ps")
proof (induct ps rule: ExcessNotAtRec.induct)
  show "?P []" by simp
next
  fix a b ps
  assume prem: "?T ((a,b)#ps)"
  then have E: "b = E a" by (simp add: isTable_eq)
  assume hyp1: "?T (deleteAround g (fst (a, b)) ps) ==>
   ?P (deleteAround g (fst (a, b)) ps)"
  assume hyp2:  "?T ps ==> ?P ps"
  have H1: "?P (deleteAround g (fst (a, b)) ps)"
    by (rule hyp1, rule isTable_deleteAround) simp
  have H2: "?P ps" by (rule hyp2, rule isTable_Cons)

  show "?P ((a,b)#ps)"
  proof cases
    assume
    "ExcessNotAtRec ps g
    ≤ b + ExcessNotAtRec (deleteAround g a ps) g"
    with H1 E show ?thesis
      by (simp add: max_def split: split_if_asm)
  next
    assume "¬ ExcessNotAtRec ps g
       ≤ b + ExcessNotAtRec (deleteAround g a ps) g"
    with H2 E show ?thesis
      by (simp add: max_def split: split_if_asm)
  qed
qed

lemma ExcessNotAtRecList_subset:
  "set (ExcessNotAtRecList ps g) ⊆ set [fst p. p ∈ ps]" (is "?P ps")
proof (induct ps rule: ExcessNotAtRecList.induct)
  show "?P []" by simp
next
  fix a b ps
  presume H1: "?P (deleteAround g a ps)"
  presume H2: "?P ps"
  show "?P ((a, b) # ps)"
  proof cases
    assume a: "ExcessNotAtRec ps g
      ≤ b + ExcessNotAtRec (deleteAround g a ps) g"
    have "set (deleteAround g a ps) ⊆ set ps"
      by (simp add: deleteAround_subset)
    then have
    "fst ` set (deleteAround g a ps) ⊆ insert a (fst ` set ps)"
      by blast
    with a H1 show ?thesis by (simp)
  next
    assume "¬ ExcessNotAtRec ps g
      ≤ b + ExcessNotAtRec (deleteAround g a ps) g"
    with H2 show ?thesis by (auto)
  qed
qed simp


lemma preSeparated_ExcessNotAtRecList:
 "minGraphProps g ==> final g ==> isTable E (vertices g) ps ==>
  preSeparated g (set (ExcessNotAtRecList ps g))"
proof -
  assume fin: "final g" and mgp: "minGraphProps g"
  show
   "isTable E (vertices g) ps ==> preSeparated g (set (ExcessNotAtRecList ps g))"
   (is "?T ps ==> ?P ps")
  proof (induct rule: ExcessNotAtRec.induct)
    show "?P []" by simp
  next
    fix a b ps
    assume prem: "?T ((a,b)#ps)"
    then have E: "b = E a" by (simp add: isTable_eq)
    assume hyp1: "?T (deleteAround g (fst (a, b)) ps) ==>
      ?P (deleteAround g (fst (a, b)) ps)"
    assume hyp2:  "?T ps ==> ?P ps"
    have H1: "?P (deleteAround g (fst (a, b)) ps)"
      by (rule hyp1, rule isTable_deleteAround) simp
    have H2: "?P ps" by (rule hyp2, rule isTable_Cons)

    show "?P ((a,b)#ps)"
    proof cases
      assume c: "ExcessNotAtRec ps g
        ≤ b + ExcessNotAtRec (deleteAround g a ps) g"
      have "preSeparated g
       (insert a (set (ExcessNotAtRecList (deleteAround g a ps) g)))"
      proof (rule preSeparated_insert)
        from prem show "a ∈ set (vertices g)" by (auto simp add: isTable_def)
        from H1
        show pS: "preSeparated g
            (set (ExcessNotAtRecList (deleteAround g a ps) g))"
          by simp

        fix f assume "f ∈ set (facesAt g a)"
        then have
        "f • a ∉ set [fst p. p ∈ deleteAround g a ps]"
          by (auto simp add: facesAt_def deleteAround_eq deleteAround'_def
            removeKeyList_eq split: split_if_asm)
        moreover
        have "set (ExcessNotAtRecList (deleteAround g a ps) g)
          ⊆ set [fst p. p ∈ deleteAround g a ps]"
          by (rule ExcessNotAtRecList_subset)
        ultimately
        show "f • a
          ∉ set (ExcessNotAtRecList (deleteAround g a ps) g)"
          by auto
        assume "|vertices f| ≤ 4"
        have "set (vertices f)
          ∩ set [fst p. p ∈ deleteAround g a ps] ⊆ {a}"
          by (rule_tac deleteAround_separated[OF mgp fin])
        moreover
        have "set (ExcessNotAtRecList (deleteAround g a ps) g)
          ⊆ set [fst p. p ∈ deleteAround g a ps]"
           by (rule ExcessNotAtRecList_subset)
        ultimately
        show "set (vertices f)
           ∩ set (ExcessNotAtRecList (deleteAround g a ps) g) ⊆ {a}"
          by blast
      qed
      with H1 E c show ?thesis by (simp)
    next
      assume "¬ ExcessNotAtRec ps g
        ≤ b + ExcessNotAtRec (deleteAround g a ps) g"
      with H2 E show ?thesis by simp
    qed
  qed
qed


lemma isTable_ExcessTable:
  "isTable (λv. ExcessAt g v) vs (ExcessTable g vs)"
  by  (auto simp add: isTable_def ExcessTable_def ExcessAt_def)

lemma ExcessTable_subset:
  "set (map fst (ExcessTable g vs)) ⊆ set vs"
  by (induct vs) (auto simp add: ExcessTable_def)

lemma distinct_ExcessNotAtRecList:
  "distinct (map fst ps) ==> distinct (ExcessNotAtRecList ps g)"
    (is "?T ps ==> ?P ps")
proof (induct rule: ExcessNotAtRec.induct)
  show "?P []" by simp
next
  fix a b ps
  assume prem: "?T ((a,b)#ps)"
  then have a: "a ∉ set (map fst ps)" by simp
  assume hyp1: "?T (deleteAround g (fst (a, b)) ps) ==>
    ?P (deleteAround g (fst (a, b)) ps)"
  assume hyp2:  "?T ps ==> ?P ps"
  from prems have "?T ps" by simp
  then have H1: "?P (deleteAround g (fst (a, b)) ps)"
   by (rule_tac hyp1) (rule distinct_deleteAround)
  from prem have H2: "?P ps"
    by (rule_tac hyp2) simp

  have "a ∉ set (ExcessNotAtRecList (deleteAround g a ps) g)"(* auto ?? *)
  proof
    assume "a ∈ set (ExcessNotAtRecList (deleteAround g a ps) g)"
    also have "set (ExcessNotAtRecList (deleteAround g a ps) g)
      ⊆ set [fst p. p ∈ deleteAround g a ps]"
     by (rule ExcessNotAtRecList_subset)
    also have "set (deleteAround g a ps) ⊆ set ps"
      by (rule deleteAround_subset)
    then have "set [fst p. p ∈ deleteAround g a ps]
      ⊆ set [fst p. p ∈ ps]" by auto
    finally have "a ∈ set (map fst ps)" .
    with a show False by contradiction
  qed
  with H1 H2 show "?P ((a,b)#ps)"
    by ( simp add: ExcessNotAtRecList_subset)
qed

(* alternative definition *)
consts ExcessTable_cont ::
  "(vertex => nat) => vertex list => (vertex × nat) list"
primrec
  "ExcessTable_cont ExcessAtPG [] = []"
  "ExcessTable_cont ExcessAtPG (v#vs) =
   (let vi = ExcessAtPG v in
     if 0 < vi
     then (v, vi)#ExcessTable_cont ExcessAtPG vs
     else ExcessTable_cont ExcessAtPG vs)"

constdefs
  ExcessTable' :: "graph => vertex list => (vertex × nat) list"
  "ExcessTable' g ≡ ExcessTable_cont (ExcessAt g)"



lemma distinct_ExcessTable_cont:
  "distinct vs ==>
  distinct (map fst (ExcessTable_cont (ExcessAt g) vs))"
proof (induct vs)
  case Nil then show ?case by (simp add: ExcessTable_def)
next
  case (Cons v vs)
  from Cons have v: "v ∉ set vs" by simp
  from Cons have "distinct vs" by simp
  with Cons have IH:
    "distinct (map fst (ExcessTable_cont (ExcessAt g) vs))"
    by simp
  moreover have
    "v ∉ fst ` set (ExcessTable_cont (ExcessAt g) vs)"
  proof
    assume "v ∈ fst ` set (ExcessTable_cont (ExcessAt g) vs)"
    also have "fst ` set (ExcessTable_cont (ExcessAt g) vs) ⊆ set vs"
      by (induct vs) auto
    finally have " v ∈ set vs" .
    with v show False by contradiction
  qed
  ultimately show ?case by (simp add: ExcessTable_def)
qed


lemma ExcessTable_cont_eq:
 "ExcessTable_cont E vs =
  [(v, E v). v ∈ [v∈vs . 0 < E v]]"
  by (induct vs) (simp_all)


lemma ExcessTable_eq: "ExcessTable = ExcessTable'"
proof (rule ext, rule ext)
  fix p g vs show "ExcessTable g vs = ExcessTable' g vs"
  by (simp add: ExcessTable_def ExcessTable'_def ExcessTable_cont_eq)
qed

lemma distinct_ExcessTable:
   "distinct vs ==> distinct [fst p. p ∈ ExcessTable g vs]"
  by (simp_all add: ExcessTable_eq ExcessTable'_def distinct_ExcessTable_cont)

lemma ExcessNotAt_eq:
  "minGraphProps g ==> final g ==>
  ∃V. ExcessNotAt g None
      = ∑v ∈ V ExcessAt g v
   ∧ preSeparated g (set V) ∧ set V ⊆ set (vertices g)
   ∧ distinct V"
proof (intro exI conjI)
  assume mgp: "minGraphProps g" and fin: "final g"
  let ?ps = "ExcessTable g (vertices g)"
  let ?V = "ExcessNotAtRecList ?ps g"
  let ?vs = "vertices g"
  let ?E = "λv. ExcessAt g v"
  have t: "isTable ?E ?vs ?ps" by (rule isTable_ExcessTable)
  with this show "ExcessNotAt g None = ∑v ∈ ?V ?E v"
    by (simp add: ListSum_ExcessNotAtRecList ExcessNotAt_def)

  show "preSeparated g (set ?V)"
    by(rule preSeparated_ExcessNotAtRecList[OF mgp fin t])

  have "set (ExcessNotAtRecList ?ps g) ⊆ set (map fst ?ps)"
    by (rule ExcessNotAtRecList_subset)
  also have "… ⊆ set (vertices g)" by (rule ExcessTable_subset)
  finally show "set ?V ⊆ set (vertices g)" .

  show "distinct ?V"
   by (simp add: distinct_ExcessNotAtRecList distinct_ExcessTable)
qed



lemma excess_eq:
  assumes 6: "t + q ≤ 6"
  shows "excessAtType t q 0 + t * \<d> 3 + q * \<d> 4 = \<b> t q"
proof -
  note simps = excessAtType_def squanderVertex_def squanderFace_def squanderTarget_def
  from 6 have "q=0 ∨ q=1 ∨ q=2 ∨ q=3 ∨ q=4 ∨ q=5 ∨ q=6" by arith
  then show ?thesis
  proof (elim disjE)
    assume q: "q = 0" (* 16 subgoals *)
    with prems show ?thesis by (simp add:simps)
  next
    assume q: "q = 1" (* 29 subgoals *)
    with prems show ?thesis by (simp add:simps)
  next
    assume q: "q = 2" (* 16 subgoals *)
    with prems show ?thesis by (simp add: simps)
  next
    assume q: "q = 3" (* 16 subgoals *)
    with prems show ?thesis  by (simp add: simps)
  next
    assume q: "q = 4" (* 6 subgoals *)
    with prems show ?thesis  by (simp add: simps)
  next
    assume q: "q = 5" (* 1 subgoal *)
    with prems show ?thesis  by (simp add: simps)
  next
    assume q: "q = 6" (* 1 subgoal *)
    with prems show ?thesis  by (simp add: simps)
  qed
qed

lemma excess_eq1:
  "[| inv g; final g; tame g; except g v = 0; v ∈ set(vertices g) |] ==>
   ExcessAt g v + (tri g v) * \<d> 3 + (quad g v) * \<d>  4
   = \<b> (tri g v) (quad g v)"
apply(subgoal_tac "finalVertex g v")
apply(simp add: ExcessAt_def excess_eq faceCountMax_bound)
apply(auto simp:finalVertex_def plane_final_facesAt)
done


text {* preSeparating *}

lemma preSeparated_separating:
assumes pl: "inv g" and fin: "final g" and ne: "noExceptionals g (set V)"
and pS: "preSeparated g (set V)"
shows "separating (set V) (λv. set (facesAt g v))"
proof -
  from pS have i: "∀v∈set V. ∀f∈set (facesAt g v).
    |vertices f| ≤ 4 --> set (vertices f) ∩ set V = {v}"
    by (simp add: preSeparated_def separated3_def)

  show "separating (set V) (λv. set (facesAt g v))"
  proof (simp add: separating_def, intro ballI impI)
    fix v1 v2 assume v: "v1 ∈ set V" "v2 ∈ set V" "v1 ≠ v2"
    show "set (facesAt g v1) ∩ set (facesAt g v2) = {}" (is "?P")
    proof (rule ccontr)
      assume "¬ ?P"
      then obtain f where f1: "f ∈ set (facesAt g v1)"
        and f2: "f ∈ set (facesAt g v2)" by auto
      from v ne have "¬ exceptionalVertex g v1"
        "¬ exceptionalVertex g v2"
        by (simp_all add: noExceptionals_def)
      with f1 pl fin have l: "|vertices f| ≤ 4"
        by (simp add: not_exceptional)
      from v f1 l i have "set (vertices f) ∩ set V = {v1}" by simp
      also from v f2 l i
      have "set (vertices f) ∩ set V = {v2}" by simp
      finally have "v1 = v2" by auto
      then show False by contradiction
    qed
  qed
qed

lemma preSeparated_disj_Union2:
assumes pl: "inv g" and fin: "final g" and ne: "noExceptionals g (set V)"
and pS: "preSeparated g (set V)" and dist: "distinct V"
and V_subset: "set V ⊆ set (vertices g)"
shows "(∑v ∈ Vf ∈ facesAt g v (w::face => nat) f)
       = ∑f ∈ [f∈faces g . ∃v ∈ set V. f ∈ set (facesAt g v)] w f"
proof -
  have s: "separating (set V) (λv. set (facesAt g v))"
    by (rule preSeparated_separating[OF pl fin ne pS])
  moreover note dist
  moreover from pl V_subset
  have v: "!!v. v ∈ set V ==> distinct (facesAt g v)"
    by(blast intro:mgp_dist_facesAt[OF inv_mgp])
  moreover
  have "distinct [f∈faces g . ∃v ∈ set V. f ∈ set (facesAt g v)]"
    by (intro distinct_filter minGraphProps11'[OF inv_mgp[OF pl]])
  moreover from pl have "{x. x ∈ set (faces g) ∧ (∃v ∈ set V. x ∈ set (facesAt g v))} =
      (\<Union>v∈set V. set (facesAt g v))"
    by (blast intro:minGraphProps inv_mgp)
  moreover from v have "(∑v∈set V. ListSum (facesAt g v) w) = (∑v∈set V. setsum w (set (facesAt g v)))"
    by (auto simp add: ListSum_conv_setsum)

  ultimately show ?thesis
    apply (simp add: ListSum_conv_setsum)
    apply (rule setsum_disj_Union) by simp+
qed

lemma squanderFace_distr2: "inv g ==> final g ==> noExceptionals g (set V) ==>
  preSeparated g (set V) ==> distinct V ==> set V ⊆ set (vertices g) ==>
     ∑f ∈ [f∈faces g. ∃v ∈ set V. f ∈ set (facesAt g v)]
         \<d> |vertices f|
   = ∑v ∈ V ((tri g v) *  \<d> 3
         + (quad g v) * \<d> 4)"
proof -
  assume pl: "inv g"
  assume fin: "final g"
  assume ne: "noExceptionals g (set V)"
  assume "preSeparated g (set V)"  "distinct V" and V_subset: "set V ⊆ set (vertices g)"
  with pl ne fin have
    "∑f ∈ [f∈faces g. ∃v∈set V. f∈set (facesAt g v)] \<d> |vertices f|
   = ∑v ∈ Vf ∈ facesAt g v \<d> |vertices f|"
    by (simp add: preSeparated_disj_Union2)
  also have "!!v. v ∈ set V ==>
    ∑f ∈ facesAt g v \<d> |vertices f|
  = (tri g v) * \<d> 3 + (quad g v) * \<d> 4"
  proof -
    fix v assume v1: "v ∈ set V"
    with V_subset have v: "v ∈ set (vertices g)" by auto

    with ne have d:
      "!!f. f ∈ set (facesAt g v) ==>
      |vertices f| = 3 ∨ |vertices f| = 4"
    proof -
      fix f assume f: "f ∈ set (facesAt g v)"
      then have ff: "f ∈ set (faces g)" by (rule minGraphProps5[OF inv_mgp[OF pl]])
      with ne f v1 pl fin have "|vertices f| ≤ 4"
        by (auto simp add: noExceptionals_def not_exceptional)
      moreover from pl ff have "3 ≤ |vertices f|" by(rule planeN4)
      ultimately show "?thesis f" by arith
    qed

    from d pl v have
      "∑f ∈ facesAt g v \<d> |vertices f|
    = (∑f∈[f ∈ facesAt g v. |vertices f| = 3] \<d> |vertices f| )
    + (∑f∈[f ∈ facesAt g v. |vertices f| = 4] \<d> |vertices f| )"
      apply (rule_tac ListSum_disj_union)
      apply (rule distinct_filter) apply simp
      apply (rule distinct_filter) apply simp
      apply simp
      apply force
      apply force
      done
    also have "… = tri g v * \<d> 3 + quad g v * \<d> 4"
    proof -
      from pl fin v have "!!A.[f ∈ facesAt g v. final f ∧ A f]
        = [f ∈ facesAt g v. A f]"
        by (rule_tac filter_eqI) (auto simp:plane_final_facesAt)
      with fin show ?thesis  by (auto simp add: tri_def quad_def)
    qed
    finally show "∑f ∈ facesAt g v \<d> |vertices f|
   = tri g v * \<d> 3 + quad g v * \<d> 4" .
  qed
  then have "∑v ∈ Vf ∈ facesAt g v \<d> |vertices f| =
         ∑v ∈ V (tri g v * \<d> 3 + quad g v * \<d> 4)"
     by (rule ListSum_eq)
  finally show ?thesis .
qed



lemma preSeparated_subset: (* preSeparated *)
   "V1 ⊆ V2 ==> preSeparated g V2 ==> preSeparated g V1"
proof (simp add:  preSeparated_def separated3_def separated2_def,
  elim conjE, intro allI impI ballI conjI)
  fix v f
  assume a: "v ∈ V1" "V1 ⊆ V2" "f ∈ set (facesAt g v)"
    "|vertices f| ≤ 4"
    "∀v∈V2. ∀f∈set (facesAt g v). |vertices f| ≤ 4 -->
      set (vertices f) ∩ V2 = {v}"
  then show "set (vertices f) ∩ V1 = {v}" by auto
next
  fix v f
  assume a: "v ∈ V1" "V1 ⊆ V2" "f ∈ set (facesAt g v)"
    "∀v∈V2. ∀f∈set (facesAt g v). f • v ∉ V2"
  then have "v ∈ V2" by auto
  with a have "f • v ∉ V2" by auto
  with a show "f • v ∉ V1" by auto
qed

end

lemma deleteAround_empty:

  deleteAround g a [] = []

lemma deleteAroundCons:

  deleteAround g a (p # ps) =
  (if fst p
      ∈ {v. ∃f∈set (facesAt g a).
               |vertices f| = 4 ∧ v ∈ {fa, f • (fa)} ∨
               |vertices f| ≠ 4 ∧ v = fa}
   then deleteAround g a ps else p # deleteAround g a ps)

lemma deleteAround_subset:

  set (deleteAround g a ps) ⊆ set ps

lemma distinct_deleteAround:

  distinct (map fst ps) ==> distinct (map fst (deleteAround g (fst (a, b)) ps))

lemma deleteAround_eq:

  deleteAround g v ps = deleteAround' g v ps

lemma deleteAround_nextVertex:

  f ∈ set (facesAt g a) ==> (fa, b) ∉ set (deleteAround g a ps)

lemma deleteAround_nextVertex_nextVertex:

  [| f ∈ set (facesAt g a); |vertices f| = 4 |]
  ==> (f • (fa), b) ∉ set (deleteAround g a ps)

lemma deleteAround_prevVertex:

  [| minGraphProps g; f ∈ set (facesAt g a) |]
  ==> (f-1a, b) ∉ set (deleteAround g a ps)

lemma deleteAround_separated:

  [| minGraphProps g; final g; |vertices f| ≤ 4; f ∈ set (facesAt g a) |]
  ==> \<V> f ∩ set (map fst (deleteAround g a ps)) ⊆ {a}

lemma

  preSeparated g {}

lemma preSeparated_insert:

  [| minGraphProps g; a ∈ \<V> g; preSeparated g V;
     !!f. f ∈ set (facesAt g a) ==> faV;
     !!f. [| f ∈ set (facesAt g a); |vertices f| ≤ 4 |] ==> \<V> fV ⊆ {a} |]
  ==> preSeparated g (insert a V)

lemma isTable_deleteAround:

  isTable E vs ((a, b) # ps) ==> isTable E vs (deleteAround g a ps)

lemma ListSum_ExcessNotAtRecList:

  isTable E vs ps ==> ExcessNotAtRec ps g = ListSum (ExcessNotAtRecList ps g) E

lemma ExcessNotAtRecList_subset:

  set (ExcessNotAtRecList ps g) ⊆ set (map fst ps)

lemma preSeparated_ExcessNotAtRecList:

  [| minGraphProps g; final g; isTable E (vertices g) ps |]
  ==> preSeparated g (set (ExcessNotAtRecList ps g))

lemma isTable_ExcessTable:

  isTable (ExcessAt g) vs (ExcessTable g vs)

lemma ExcessTable_subset:

  set (map fst (ExcessTable g vs)) ⊆ set vs

lemma distinct_ExcessNotAtRecList:

  distinct (map fst ps) ==> distinct (ExcessNotAtRecList ps g)

lemma distinct_ExcessTable_cont:

  distinct vs ==> distinct (map fst (ExcessTable_cont (ExcessAt g) vs))

lemma ExcessTable_cont_eq:

  ExcessTable_cont E vs = [(v, E v). v : [vvs . 0 < E v]]

lemma ExcessTable_eq:

  ExcessTable = ExcessTable'

lemma distinct_ExcessTable:

  distinct vs ==> distinct (map fst (ExcessTable g vs))

lemma ExcessNotAt_eq:

  [| minGraphProps g; final g |]
  ==> ∃V. ExcessNotAt g None = ListSum V (ExcessAt g) ∧
          preSeparated g (set V) ∧ set V ⊆ \<V> g ∧ distinct V

lemma excess_eq:

  t + q ≤ 6 ==> excessAtType t q 0 + t * \<d> 3 + q * \<d> 4 = \<b> t q

lemma excess_eq1:

  [| Invariants.inv g; final g; tame g; except g v = 0; v ∈ \<V> g |]
  ==> ExcessAt g v + tri g v * \<d> 3 + quad g v * \<d> 4 =
      \<b> (tri g v) (quad g v)

lemma preSeparated_separating:

  [| Invariants.inv g; final g; noExceptionals g (set V);
     preSeparated g (set V) |]
  ==> separating (set V) (λv. set (facesAt g v))

lemma preSeparated_disj_Union2:

  [| Invariants.inv g; final g; noExceptionals g (set V); preSeparated g (set V);
     distinct V; set V ⊆ \<V> g |]
  ==> ∑vV ListSum (facesAt g v) w =
      ListSum [f∈faces g . ∃v∈set V. f ∈ set (facesAt g v)] w

lemma squanderFace_distr2:

  [| Invariants.inv g; final g; noExceptionals g (set V); preSeparated g (set V);
     distinct V; set V ⊆ \<V> g |]
  ==> ∑f∈[f∈faces g . ∃v∈set V. f ∈ set (facesAt g v)] \<d> |vertices f| =
      ∑vV tri g v * \<d> 3 + quad g v * \<d> 4

lemma preSeparated_subset:

  [| V1.0V2.0; preSeparated g V2.0 |] ==> preSeparated g V1.0