Up to index of Isabelle/HOL/Tame

theory ScorePropsimports 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, f^{2}• a]" in bspec) apply (fastsimp simp:image_def) apply (simp) apply(drule_tac x = "[f • a, f^{2}• 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 separated_{2}_def separated_{3}_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 separated_{2}_def separated_{3}_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 separated_{2}_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 separated_{3}_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 separated_{3}_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 ∈ V}∑_{f ∈ 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 ∈ V}∑_{f ∈ 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 ∈ V}∑_{f ∈ 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 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

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 ∈ {f • a, f • (f • a)} ∨ |vertices f| ≠ 4 ∧ v = f • a} 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) ==> (f • a, b) ∉ set (deleteAround g a ps)

lemma deleteAround_nextVertex_nextVertex:

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

lemma deleteAround_prevVertex:

[| minGraphProps g; f ∈ set (facesAt g a) |] ==> (f^{-1}• a, 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) ==> f • a ∉ V; !!f. [| f ∈ set (facesAt g a); |vertices f| ≤ 4 |] ==> \<V> f ∩ V ⊆ {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 : [v∈vs . 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 |] ==> ∑_{v∈V}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| = ∑_{v∈V}tri g v * \<d> 3 + quad g v * \<d> 4

lemma preSeparated_subset:

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