Theory ScoreProps

(*  Author:     Gertrud Bauer, Tobias Nipkow
*)

section ‹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)"
by (fastforce simp: nextV2 deleteAround_def)

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


definition deleteAround' :: "graph  vertex  (vertex × nat) list 
    (vertex × nat) list" where
  "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: if_split_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  a : 𝒱 g  f  set (facesAt g a) 
  (f-1  a, b)  set (deleteAround g a ps)"
proof -
  assume a: "minGraphProps g" "a : 𝒱 g" "f  set (facesAt g a)"
  have "(f-1  a, a)   f" using a
    by(blast intro:prevVertex_in_edges minGraphProps)
  then obtain f' :: face where f': "f'  set(facesAt g a)"
    and e: "(a, f-1  a)   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:
assumes mgp: "minGraphProps g" and fin: "final g" and ag: "a : 𝒱 g" and 4: "|vertices f|  4"
and f: "f  set(facesAt g a)"
shows "𝒱 f  set [fst p. p  deleteAround g a ps]  {a}" (is "?A")
proof -
  note MGP = mgp ag f
  have af: "a  𝒱 f" using MGP by(blast intro:minGraphProps)
  have "2 < |vertices f|" using MGP 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  𝒱 f"
        "b  set (map fst (deleteAround g a ps))" by auto
      from MGP have d: "distinct (vertices f)"
        by(blast intro:minGraphProps)
      with af 3 have "𝒱 f = {a, f  a, f  (f  a)}"
          by (rule_tac vertices_triangle)
      also from d af 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 have "b  set (map fst (deleteAround g a ps))"
      using deleteAround_nextVertex deleteAround_prevVertex by auto
      then show False by contradiction (rule b1)
    qed
  next
    assume 4: "|vertices f| = 4"
    show "?A"
    proof (rule ccontr)
      assume "¬ ?A"
      then obtain b where b1: "b  a" "b  𝒱 f"
        "b  set (map fst (deleteAround g a ps))" by auto
      from MGP have d: "distinct (vertices f)" by(blast intro:minGraphProps)
      with af 4 have "𝒱 f = {a, f  a, f  (f  a), f  (f  (f  a))}"
        by (rule_tac vertices_quad)
      also from d af 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 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 (rule b1)
    qed
  qed
qed
(*
deleteAround g y loescht nextVertex f a,
nextVertex f (nextVertex f a),
prevVertex f a wird mit nachbarflaeche geloescht.
*)

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

lemma separated_insert:
assumes mgp: "minGraphProps g" and a: "a  𝒱 g"
  and Vg: "V  𝒱 g"
  and ps: "separated g V"
  and s2: "(f. f  set (facesAt g a)  f  a  V)"
  and s3: "(f. f  set (facesAt g a) 
      |vertices f|  4  𝒱 f  V  {a})"
  shows "separated g (insert a V)"
proof (simp add: separated_def separated2_def separated3_def,
 intro conjI ballI impI)
  fix f assume f: "f  set (facesAt g a)"
  then show "f  a  a" by (rule mgp_facesAt_no_loop[OF mgp a])
  from f show "f  a  V" by (rule s2)
next
  fix f v assume v: "f  set (facesAt g v)" and vV: "v  V"
  have "v : 𝒱 g" using vV Vg by blast
  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 : 𝒱 g v] by blast
    have "f'  a  V" using v vV by simp
    with f' s2 show False by blast
  qed
  from ps v vV show "f  v  V"
    by (simp add: separated_def separated2_def)
next
  fix f assume f:  "f  set (facesAt g a)" "|vertices f|  4"
  then have "𝒱 f  V  {a}" by (rule s3)
  moreover from mgp a f have "a  𝒱 f" by(blast intro:minGraphProps)
  ultimately show "𝒱 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: "𝒱 f  V = {v}"
    by (simp add: separated_def separated3_def)
  have "v : 𝒱 g" using a Vg by blast
  show  "𝒱 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  𝒱 f"
    proof
      assume a2: "a  𝒱 f"
      with mgp a v : 𝒱 g have "f   g" by(blast intro:minGraphProps)
      with mgp a2 have "f  set (facesAt g a)" by(blast intro:minGraphProps)
      with a have "𝒱 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 "𝒱 f  insert a V = {v}" by blast
  qed
qed


function ExcessNotAtRecList :: "(vertex, nat) table  graph  vertex list" where
  "ExcessNotAtRecList [] = (λg. [])"
  | "ExcessNotAtRecList ((x, y) # ps) = (λg.
      let l1 = ExcessNotAtRecList ps g;
      l2 = ExcessNotAtRecList (deleteAround g x ps) g in
      if ExcessNotAtRec ps g
        y + ExcessNotAtRec (deleteAround g x ps) g
      then x # l2 else l1)"
by pat_completeness auto
termination by (relation "measure size")
  (auto simp add: 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 gE p)" (is "?T ps  ?P ps")
proof (induct ps rule: ExcessNotAtRecList.induct)
  case 1 show ?case by simp
next
  case (2 a b ps)
  from 2 have prem: "?T ((a,b)#ps)" by blast
  then have E: "b = E a" by (simp add: isTable_eq)
  from 2 have hyp1: "?T (deleteAround g a ps) 
   ?P (deleteAround g a ps)" by blast
  from 2 have hyp2:  "?T ps  ?P ps" by blast
  have H1: "?P (deleteAround g a ps)"
    by (rule hyp1, rule isTable_deleteAround) (rule prem)
  have H2: "?P ps" by (rule hyp2, rule isTable_Cons, rule prem)
  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: if_split_asm)
  next
    assume "¬ ExcessNotAtRec ps g
        b + ExcessNotAtRec (deleteAround g a ps) g"
    with H2 E show ?thesis
      by (simp add: max_def split: if_split_asm)
  qed
qed

lemma ExcessNotAtRecList_subset:
  "set (ExcessNotAtRecList ps g)  set [fst p. p  ps]" (is "?P ps")
proof (induct ps rule: ExcessNotAtRecList.induct)
  case 1 show ?case by simp
next
  case (2 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 separated_ExcessNotAtRecList:
 "minGraphProps g  final g  isTable E (vertices g) ps 
  separated g (set (ExcessNotAtRecList ps g))"
proof -
  assume fin: "final g" and mgp: "minGraphProps g"
  show
   "isTable E (vertices g) ps  separated g (set (ExcessNotAtRecList ps g))"
   (is "?T ps  ?P ps")
  proof (induct rule: ExcessNotAtRec.induct)
    case 1 show ?case by simp
  next
    case (2 a b ps)
    from 2 have prem: "?T ((a,b)#ps)" by blast
    then have E: "b = E a" by (simp add: isTable_eq)
    have "a :𝒱 g" using prem by(auto simp: isTable_def)
    from 2 have hyp1: "?T (deleteAround g a ps) 
      ?P (deleteAround g a ps)" by blast
    from 2 have hyp2:  "?T ps  ?P ps" by blast
    have H1: "?P (deleteAround g a ps)"
      by (rule hyp1, rule isTable_deleteAround) (rule prem)
    have H2: "?P ps" by (rule hyp2, rule isTable_Cons) (rule prem)

    show "?P ((a,b)#ps)"
    proof cases
      assume c: "ExcessNotAtRec ps g
         b + ExcessNotAtRec (deleteAround g a ps) g"
      have "separated g
       (insert a (set (ExcessNotAtRecList (deleteAround g a ps) g)))"
      proof (rule separated_insert[OF mgp])
        from prem show "a  set (vertices g)" by (auto simp add: isTable_def)

        show "set (ExcessNotAtRecList (deleteAround g a ps) g)  𝒱 g"
        proof-
          have "set (ExcessNotAtRecList (deleteAround g a ps) g) 
                set (map fst (deleteAround g a ps))"
            by(rule ExcessNotAtRecList_subset[simplified concat_map_singleton])
          also have "  set (map fst ps)"
            using deleteAround_subset by fastforce
          finally show ?thesis using prem by(auto simp: isTable_def)
        qed
        from H1
        show pS: "separated g
            (set (ExcessNotAtRecList (deleteAround g a ps) g))"
          by simp

        fix f assume f: "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: if_split_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"
        from this f have "set (vertices f)
           set [fst p. p  deleteAround g a ps]  {a}"
          by (rule deleteAround_separated[OF mgp fin a : 𝒱 g])
        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)
  case 1 show ?case by simp
next
  case (2 a b ps)
  from 2 have prem: "?T ((a,b)#ps)" by blast
  then have a: "a  set (map fst ps)" by simp
  from 2 have hyp1: "?T (deleteAround g a ps) 
    ?P (deleteAround g a ps)" by blast
  from 2 have hyp2:  "?T ps  ?P ps" by blast
  from 2 have "?T ps" by simp
  then have H1: "?P (deleteAround g a ps)"
   by (rule_tac hyp1) (rule distinct_deleteAround [simplified])
  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)" by simp
    with a show False by contradiction
  qed
  with H1 H2 show "?P ((a,b)#ps)"
    by ( simp add: ExcessNotAtRecList_subset)
qed

(* alternative definition *)
primrec ExcessTable_cont ::
  "(vertex  nat)  vertex list  (vertex × nat) list"
where
  "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)"

definition ExcessTable' :: "graph  vertex list  (vertex × nat) list" where
  "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  [vvs . 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  VExcessAt g v)
    separated 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 "separated g (set ?V)"
    by(rule separated_ExcessNotAtRecList[OF mgp fin t])

  have "set (ExcessNotAtRecList ?ps g)  set (map fst ?ps)"
    by (rule ExcessNotAtRecList_subset[simplified concat_map_singleton])
  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[simplified concat_map_singleton])
qed

lemma excess_eq:
  assumes 7: "t + q  7"
  shows "excessAtType t q 0 + t * 𝖽 3 + q * 𝖽 4 = 𝖻 t q"
proof -
  note simps = excessAtType_def squanderVertex_def squanderFace_def
    nat_minus_add_max squanderTarget_def
  from 7 have "q=0  q=1  q=2  q=3  q=4  q=5  q=6  q=7" by arith
  then show ?thesis
  proof (elim disjE)
    assume q: "q = 0" (* 16 subgoals *)
    with 7 show ?thesis by (simp add: simps)
  next
    assume q: "q = 1" (* 29 subgoals *)
    with 7 show ?thesis by (simp add: simps)
  next
    assume q: "q = 2" (* 16 subgoals *)
    with 7 show ?thesis by (simp add: simps)
  next
    assume q: "q = 3" (* 16 subgoals *)
    with 7 show ?thesis by (simp add: simps)
  next
    assume q: "q = 4" (* 6 subgoals *)
    with 7 show ?thesis by (simp add: simps)
  next
    assume q: "q = 5" (* 1 subgoal *)
    with 7 show ?thesis by (simp add: simps)
  next
    assume q: "q = 6" (* 1 subgoal *)
    with 7 show ?thesis by (simp add: simps)
  next
    assume q: "q = 7" (* 1 subgoal *)
    with 7 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) * 𝖽 3 + (quad g v) * 𝖽  4
   = 𝖻 (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 ‹separating›

definition separating :: "'a set  ('a  'b set)  bool" where
  "separating V F  
   (v1  V. v2  V. v1  v2   F v1  F v2 = {})"


lemma separating_insert1: 
  "separating (insert a V) F  separating V F"
  by (simp add: separating_def)

lemma separating_insert2:
  "separating (insert a V) F  a  V   v  V  
  F a  F v = {}"
  by (auto simp add: separating_def)

lemma sum_disj_Union: 
 "finite V  
  (f. finite (F f))  
  separating V F  
  (vV. f(F v). (w f::nat)) = (f(vV. F v). w f)"
proof (induct  rule: finite_induct)
  case empty then show ?case by simp
next
  case (insert a V) 
  then have s: "separating (insert a V) F" by simp
  then have "separating V F" by (rule_tac separating_insert1)
  with insert
  have IH: "(vV. f(F v). w f) = (f(vV. F v). w f)" 
    by simp

  moreover have fin: "finite V" "a  V" "f. finite (F f)" by fact+

  moreover from s have "v. a  V  v  V  F a  F v = {}"
   by (simp add: separating_insert2)
  with fin have "(F a)  (vV. F v) = {}" by auto 

  ultimately show ?case by (simp add: sum.union_disjoint)
qed

lemma separated_separating:
assumes Vg: "set V  𝒱 g"
and pS: "separated g (set V)"
and noex: "fP. |vertices f|  4"
shows "separating (set V) (λv. set (facesAt g v)  P)"
proof -
  from pS have i: "vset V. fset (facesAt g v).
    |vertices f|  4  set (vertices f)  set V = {v}"
    by (simp add: separated_def separated3_def)
  show "separating (set V) (λv. set (facesAt g v)  P)"
  proof (simp add: separating_def, intro ballI impI)
    fix v1 v2 assume v: "v1  set V" "v2  set V" "v1  v2"
    hence "v1 : 𝒱 g" using Vg by blast
    show "(set (facesAt g v1)  P)  (set (facesAt g v2)  P) = {}" (is "?P")
    proof (rule ccontr)
      assume "¬ ?P"
      then obtain f where f1: "f  set (facesAt g v1)"
        and f2: "f  set (facesAt g v2)" and "f : P" by auto
      with noex have l: "|vertices f|  4" by blast
      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 (rule v)
    qed
  qed
qed

lemma ListSum_V_F_eq_ListSum_F:
assumes pl: "inv g"
and pS: "separated g (set V)" and dist: "distinct V"
and V_subset: "set V  set (vertices g)"
and noex: "f  Collect P. |vertices f|  4"
shows "(∑⇘v  V⇙ ∑⇘f  filter P (facesAt g v)(w::face  nat) f)
       = (∑⇘f  [ffaces g . v  set V. f  set (facesAt g v)  Collect P]w f)"
proof -
  have s: "separating (set V) (λv. set (facesAt g v)  Collect P)"
    by (rule separated_separating[OF V_subset pS noex])
  moreover note dist
  moreover from pl V_subset
  have "v. v  set V  distinct (facesAt g v)"
    by(blast intro:mgp_dist_facesAt[OF inv_mgp])
  hence v: "v. v  set V  distinct (filter P (facesAt g v))"
    by simp
  moreover
  have "distinct [ffaces g . v  set V. f  set (facesAt g v)  Collect P]"
    by (intro distinct_filter minGraphProps11'[OF inv_mgp[OF pl]])
  moreover from pl have "{x. x   g  (v  set V. x  set (facesAt g v)  P x)} =
      (vset V. set (facesAt g v)  Collect P)" using V_subset
    by (blast intro:minGraphProps inv_mgp)
  moreover from v have "(vset V. ListSum (filter P (facesAt g v)) w) = (vset V. sum w (set(facesAt g v)  Collect P))"
    by (auto simp add: ListSum_conv_sum Int_def)
  ultimately show ?thesis
    by (simp add: ListSum_conv_sum sum_disj_Union)
qed

lemma separated_disj_Union2:
assumes pl: "inv g" and fin: "final g" and ne: "noExceptionals g (set V)"
and pS: "separated g (set V)" and dist: "distinct V"
and V_subset: "set V  set (vertices g)"
shows "(∑⇘v  V⇙ ∑⇘f  facesAt g v(w::face  nat) f)
       = (∑⇘f  [ffaces g . v  set V. f  set (facesAt g v)]w f)"
proof -
  let ?P = "λf. |vertices f|  4"
  have "v  set V. f  set (facesAt g v). |vertices f|  4"
    using V_subset ne
    by (auto simp: noExceptionals_def
      intro: minGraphProps5[OF inv_mgp[OF pl]] not_exceptional[OF pl fin])
  thus ?thesis
    using ListSum_V_F_eq_ListSum_F[where P = ?P, OF pl pS dist V_subset]
    by (simp add: Int_def cong: conj_cong)
qed

lemma squanderFace_distr2: "inv g  final g  noExceptionals g (set V) 
  separated g (set V)  distinct V  set V  set (vertices g) 
     (∑⇘f  [ffaces g. v  set V. f  set (facesAt g v)]𝖽 |vertices f| )
   = (∑⇘v  V((tri g v) * 𝖽 3
         + (quad g v) * 𝖽 4))"
proof -
  assume pl: "inv g"
  assume fin: "final g"
  assume ne: "noExceptionals g (set V)"
  assume "separated g (set V)"  "distinct V" and V_subset: "set V  set (vertices g)"
  with pl ne fin have
    "(∑⇘f  [ffaces g. vset V. fset (facesAt g v)]𝖽 |vertices f| )
   = (∑⇘v  V⇙ ∑⇘f  facesAt g v𝖽 |vertices f| )"
    by (simp add: separated_disj_Union2)
  also have "v. v  set V 
    (∑⇘f  facesAt g v𝖽 |vertices f| )
  = (tri g v) * 𝖽 3 + (quad g v) * 𝖽 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] v])
      with ne f v1 pl fin v 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𝖽 |vertices f| )
    = (∑⇘f[f  facesAt g v. |vertices f| = 3]𝖽 |vertices f| )
    + (∑⇘f[f  facesAt g v. |vertices f| = 4]𝖽 |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 * 𝖽 3 + quad g v * 𝖽 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𝖽 |vertices f| ) = tri g v * 𝖽 3 + quad g v * 𝖽 4" .
  qed
  then have "(∑⇘v  V⇙ ∑⇘f  facesAt g v𝖽 |vertices f| ) =
         (∑⇘v  V(tri g v * 𝖽 3 + quad g v * 𝖽 4))"
     by (rule ListSum_eq)
  finally show ?thesis .
qed



lemma separated_subset: (* separated *)
   "V1  V2  separated g V2  separated g V1"
proof (simp add:  separated_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"
    "vV2. fset (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)"
    "vV2. fset (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