Theory ScoreProps
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
lemma [iff]: "separated g {}"
by (simp add: separated_def separated⇩2_def separated⇩3_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 separated⇩2_def separated⇩3_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 separated⇩2_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 separated⇩3_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 g⇙ E 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)"
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
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 ← [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)
∧ 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"
with 7 show ?thesis by (simp add: simps)
next
assume q: "q = 1"
with 7 show ?thesis by (simp add: simps)
next
assume q: "q = 2"
with 7 show ?thesis by (simp add: simps)
next
assume q: "q = 3"
with 7 show ?thesis by (simp add: simps)
next
assume q: "q = 4"
with 7 show ?thesis by (simp add: simps)
next
assume q: "q = 5"
with 7 show ?thesis by (simp add: simps)
next
assume q: "q = 6"
with 7 show ?thesis by (simp add: simps)
next
assume q: "q = 7"
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 ⟹
(∑v∈V. ∑f∈(F v). (w f::nat)) = (∑f∈(⋃v∈V. 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: "(∑v∈V. ∑f∈(F v). w f) = (∑f∈(⋃v∈V. 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) ∩ (⋃v∈V. 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: "∀f∈P. |vertices f| ≤ 4"
shows "separating (set V) (λv. set (facesAt g v) ∩ P)"
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: separated_def separated⇩3_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 ∈ [f←faces 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 [f←faces 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)} =
(⋃v∈set V. set (facesAt g v) ∩ Collect P)" using V_subset
by (blast intro:minGraphProps inv_mgp)
moreover from v have "(∑v∈set V. ListSum (filter P (facesAt g v)) w) = (∑v∈set 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 ∈ [f←faces 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 ∈ [f←faces 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 ∈ [f←faces g. ∃v∈set V. f∈set (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:
"V1 ⊆ V2 ⟹ separated g V2 ⟹ separated g V1"
proof (simp add: separated_def separated⇩3_def separated⇩2_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