(* ID: $Id: PlaneProps.thy,v 1.2 2006/01/09 06:56:14 nipkow Exp $ Author: Gertrud Bauer, Tobias Nipkow *) header "Further Plane Graph Poroperties" theory PlaneProps imports Invariants begin subsection {* @{const final} *} lemma plane_final_facesAt: "[| inv g; final g; f ∈ set (facesAt g v) |] ==> final f" proof - assume g: "inv g" and fin:"final g" and "f ∈ set (facesAt g v)" with g have "f ∈ \<F> g" by(blast intro: minGraphProps inv_mgp) with fin show ?thesis by (rule finalGraph_face) qed lemma finalVertexI: "[| inv g; final g; v ∈ \<V> g |] ==> finalVertex g v" by (auto simp add: finalVertex_def nonFinals_def filter_empty_conv plane_final_facesAt) lemma setFinal_notin_finals: "[| f ∈ \<F> g; ¬ final f; minGraphProps g |] ==> setFinal f ∉ set (finals g)" apply(drule minGraphProps11) apply(cases f) apply(fastsimp simp:finals_def setFinal_def normFaces_def normFace_def verticesFrom_def minVertex_def inj_on_def distinct_map split:facetype.splits) done subsection {* @{const degree} *} lemma planeN4: "inv g ==> f ∈ \<F> g ==> 3 ≤ |vertices f|" apply(subgoal_tac "2 < | vertices f |") apply arith apply(drule inv_mgp) apply (erule (1) minGraphProps2) done lemma degree_eq: assumes pl: "inv g" and fin: "final g" shows "degree g v = tri g v + quad g v + except g v" proof - have dist: "distinct(facesAt g v)" using pl by simp have 3: "∀f ∈ set(facesAt g v). |vertices f| = 3 ∨ |vertices f| = 4 ∨ |vertices f| ≥ 5" proof fix f assume f: "f ∈ set (facesAt g v)" hence "|vertices f| ≥ 3" using minGraphProps5[OF inv_mgp[OF pl] f] planeN4[OF pl] by blast thus "|vertices f| = 3 ∨ |vertices f| = 4 ∨ |vertices f| ≥ 5" by arith qed have "degree g v = |facesAt g v|" by(simp add:degree_def) also have "… = card(set(facesAt g v))" by (simp add:distinct_card[OF dist]) also have "set(facesAt g v) = {f ∈ set(facesAt g v). |vertices f| = 3} ∪ {f ∈ set(facesAt g v). |vertices f| = 4} ∪ {f ∈ set(facesAt g v). |vertices f| ≥ 5}" (is "_ = ?T ∪ ?Q ∪ ?E") using 3 by blast also have "card(?T ∪ ?Q ∪ ?E) = card ?T + card ?Q + card ?E" apply (subst card_Un_disjoint) apply simp apply simp apply fastsimp apply (subst card_Un_disjoint) apply simp apply simp apply fastsimp apply simp done also have "… = tri g v + quad g v + except g v" using fin by(simp add:tri_def quad_def except_def distinct_card[symmetric] distinct_filter[OF dist] plane_final_facesAt[OF pl] cong:conj_cong) finally show ?thesis . qed lemma plane_fin_exceptionalVertex_def: assumes pl: "inv g" and fin: "final g" shows "exceptionalVertex g v = ( | [f ∈ facesAt g v . 5 ≤ |vertices f| ] | ≠ 0)" proof - have "!!f. f ∈ set (facesAt g v) ==> final f" by(rule plane_final_facesAt[OF pl fin]) then show ?thesis by (simp add: filter_simp exceptionalVertex_def except_def) qed lemma not_exceptional: "inv g ==> final g ==> f ∈ set (facesAt g v) ==> ¬ exceptionalVertex g v ==> |vertices f| ≤ 4" by (frule C0) (auto simp add: plane_fin_exceptionalVertex_def except_def filter_empty_conv) subsection {* Misc *} lemma in_next_plane0I: assumes "g' ∈ set (generatePolygon n v f g)" "f ∈ set (nonFinals g)" "v ∈ \<V> f" "3 ≤ n" "n < 4+p" shows "g' ∈ set (next_plane0p g)" proof - have "¬ final g" using prems(2) by(auto simp: nonFinals_def finalGraph_def filter_empty_conv) thus ?thesis using prems by(auto simp:next_plane0_def) qed lemma next_plane0_nonfinals: "g [next_plane0p]-> g' ==> nonFinals g ≠ []" by(auto simp:next_plane0_def finalGraph_def) lemma next_plane0_ex: assumes a: "g [next_plane0p]-> g'" shows "∃f∈ set(nonFinals g). ∃v ∈ \<V> f. ∃i ∈ set([3..maxGon p]). g' ∈ set (generatePolygon i v f g)" proof - from a have "¬ final g" by (auto simp add: next_plane0_def) with a show ?thesis by (auto simp add: next_plane0_def nonFinals_def) qed lemma step_outside2: "inv g ==> g [next_plane0p]-> g' ==> ¬ final g' ==> |faces g'| ≠ 2" apply(frule inv_two_faces) apply(frule inv_finals_nonempty) apply(drule inv_mgp) apply(insert len_faces_sum[of g] len_faces_sum[of g']) apply(subgoal_tac "|nonFinals g| ≠ 0") prefer 2 apply(drule next_plane0_nonfinals) apply simp apply(subgoal_tac "|nonFinals g'| ≠ 0") prefer 2 apply(simp add:finalGraph_def) apply(drule (1) next_plane0_incr_faces) apply(case_tac "|faces g| = 2") prefer 2 apply arith apply(subgoal_tac "|finals g| ≠ 0") apply arith apply simp done subsection{* Increasing final faces *} lemma set_finals_splitFace[simp]: "[| f ∈ \<F> g; ¬ final f |] ==> set(finals(snd(snd(splitFace g u v f vs)))) = set(finals g)" apply(auto simp add:splitFace_def split_def finals_def split_face_def) apply(drule replace5) apply(clarsimp) apply(erule replace4) apply clarsimp done lemma next_plane0_finals_incr: "g [next_plane0p]-> g' ==> f ∈ set(finals g) ==> f ∈ set(finals g')" apply(auto simp:next_plane0_def generatePolygon_def split:split_if_asm) apply(erule subdivFace_pres_finals) apply (simp add:nonFinals_def) done lemma next_plane0_finals_subset: "g' ∈ set (next_plane0p g) ==> set (finals g) ⊆ set (finals g')" by (auto simp add: next_plane0_finals_incr) lemma next_plane0_final_mono: "[| g' ∈ set (next_plane0p g); f ∈ \<F> g; final f |] ==> f ∈ \<F> g'" apply(drule next_plane0_finals_subset) apply(simp add:finals_def) apply blast done subsection{* Increasing vertices *} lemma next_plane0_vertices_subset: "[| g' ∈ set (next_plane0p g); minGraphProps g |] ==> \<V> g ⊆ \<V> g'" apply(rule next_plane0_incr) apply(erule (1) subset_trans) apply(simp add: vertices_makeFaceFinal) defer apply assumption+ apply (auto simp: splitFace_def split_def vertices_graph) done subsection{* Increasing vertex degrees *} lemma next_plane0_incr_faceListAt: "[| g' ∈ set (next_plane0p g); minGraphProps g |] ==> |faceListAt g| ≤ |faceListAt g'| & (∀v < |faceListAt g|. |faceListAt g ! v| ≤ |faceListAt g' ! v| )" (concl is "?Q g g'") apply(rule next_plane0_incr[where Q = ?Q]) prefer 4 apply assumption prefer 4 apply assumption apply(rule conjI) apply fastsimp apply(clarsimp) apply(erule allE, erule impE, assumption) apply(erule_tac x = v in allE, erule impE) apply force apply force apply(simp add: makeFaceFinal_def makeFaceFinalFaceList_def) apply (simp add: splitFace_def split_def nth_append nth_list_update) done lemma next_plane0_incr_degree: "[| g' ∈ set (next_plane0p g); minGraphProps g; v ∈ \<V> g |] ==> degree g v ≤ degree g' v" apply(frule (1) next_plane0_incr_faceListAt) apply(frule (1) next_plane0_vertices_subset) apply(simp add:degree_def facesAt_def) apply(rule conjI) prefer 2 apply blast apply(frule minGraphProps4) apply(simp add:vertices_graph) done subsection{* Increasing @{const except} *} lemma next_plane0_incr_except: assumes "g' ∈ set (next_plane0p g)" "inv g" "v ∈ \<V> g" shows "except g v ≤ except g' v" proof (unfold except_def) note inv' = invariantE[OF inv_inv_next_plane0, OF prems(1,2)] note mgp = inv_mgp[OF prems(2)] and mgp' = inv_mgp[OF inv'] note dist = distinct_filter[OF mgp_dist_facesAt[OF mgp]] note dist' = distinct_filter[OF mgp_dist_facesAt[OF mgp']] have "v ∈ \<V> g'" using prems(3) next_plane0_vertices_subset[OF prems(1) mgp] by blast have "|[f∈facesAt g v . final f ∧ 5 ≤ |vertices f| ]| = card{f∈ set(facesAt g v) . final f ∧ 5 ≤ |vertices f|}" (is "?L = card ?M") using distinct_card[OF dist] by simp also have "?M = {f∈ \<F> g. v ∈ \<V> f ∧ final f ∧ 5 ≤ |vertices f|}" by(simp add: minGraphProps_facesAt_eq[OF mgp prems(3)]) also have "… = {f ∈ set(finals g) . v ∈ \<V> f ∧ 5 ≤ |vertices f|}" by(auto simp:finals_def) also have "card … ≤ card{f ∈ set(finals g'). v ∈ \<V> f ∧ 5 ≤ |vertices f|}" (is "_ ≤ card ?M") apply(rule card_mono) apply simp using next_plane0_finals_subset[OF prems(1)] by blast also have "?M = {f∈ \<F> g' . v ∈ \<V> f ∧ final f ∧ 5 ≤ |vertices f|}" by(auto simp:finals_def) also have "… = {f ∈ set(facesAt g' v) . final f ∧ 5 ≤ |vertices f|}" by(simp add: minGraphProps_facesAt_eq[OF mgp' `v ∈ \<V> g'`]) also have "card … = |[f∈facesAt g' v . final f ∧ 5 ≤ |vertices f| ]|" (is "_ = ?R") using distinct_card[OF dist'] by simp finally show "?L ≤ ?R" . qed subsection{* Increasing edges *} lemma next_plane0_set_edges_subset: "[| minGraphProps g; g [next_plane0p]-> g' |] ==> edges g ⊆ edges g'" apply(rule next_plane0_incr) apply(erule (1) subset_trans) apply(simp add: edges_makeFaceFinal) apply(erule snd_snd_splitFace_edges_incr) apply assumption+ done subsection{* Increasing final vertices *} (* This should really be proved via the (unproven) invariant v : f ==> ((g,v).f).(f.v) = v *) lemma next_plane0_incr_finV: "[|g' ∈ set (next_plane0p g); minGraphProps g |] ==> ∀v ∈ \<V> g. v ∈ \<V> g' ∧ ((∀f∈\<F> g. v ∈ \<V> f --> final f) --> (∀f∈\<F> g'. v ∈ \<V> f --> f ∈ \<F> g))" (concl is "?Q g g'") apply(rule next_plane0_incr[where Q = ?Q and g=g and g'=g']) prefer 4 apply assumption prefer 4 apply assumption apply blast apply(clarsimp simp:makeFaceFinal_def vertices_graph makeFaceFinalFaceList_def) apply(drule replace5) apply(erule disjE)apply blast apply simp apply(simp add:setFinal_def) apply(unfold pre_splitFace_def) apply(clarsimp simp:splitFace_def split_def vertices_graph) apply(rule conjI) apply(clarsimp simp:split_face_def vertices_graph) apply(blast dest:inbetween_inset) apply(clarsimp) apply(erule disjE[OF replace5]) apply blast apply(clarsimp simp:split_face_def vertices_graph) apply(blast dest:inbetween_inset) done lemma next_plane0_finalVertex_mono: "[|g' ∈ set (next_plane0p g); inv g; u ∈ \<V> g; finalVertex g u |] ==> finalVertex g' u" apply(frule (1) invariantE[OF inv_inv_next_plane0]) apply(subgoal_tac "u ∈ \<V> g'") prefer 2 apply(blast dest:next_plane0_vertices_subset inv_mgp) apply(clarsimp simp:finalVertex_def minGraphProps_facesAt_eq[OF inv_mgp]) apply(blast dest:next_plane0_incr_finV inv_mgp) done subsection{* Preservation of @{const facesAt} at final vertices *} lemma next_plane0_finalVertex_facesAt_eq: "[|g' ∈ set (next_plane0p g); inv g; v ∈ \<V> g; finalVertex g v |] ==> set(facesAt g' v) = set(facesAt g v)" apply(frule (1) invariantE[OF inv_inv_next_plane0]) apply(subgoal_tac "v ∈ \<V> g'") prefer 2 apply(blast dest:next_plane0_vertices_subset inv_mgp) apply(clarsimp simp:finalVertex_def minGraphProps_facesAt_eq[OF inv_mgp]) by(blast dest:next_plane0_incr_finV next_plane0_final_mono inv_mgp) lemma next_plane0_len_filter_eq: assumes "g' ∈ set (next_plane0p g)" "inv g" "v ∈ \<V> g" "finalVertex g v" shows "|filter P (facesAt g' v)| = |filter P (facesAt g v)|" proof - note inv' = invariantE[OF inv_inv_next_plane0, OF prems(1,2)] note mgp = inv_mgp[OF prems(2)] and mgp' = inv_mgp[OF inv'] note dist = distinct_filter[OF mgp_dist_facesAt[OF mgp]] note dist' = distinct_filter[OF mgp_dist_facesAt[OF mgp']] have "v ∈ \<V> g'" using prems(3) next_plane0_vertices_subset[OF prems(1) mgp] by blast have "|filter P (facesAt g' v)| = card{f ∈ set(facesAt g' v) . P f}" using distinct_card[OF dist'] by simp also have "… = card{f ∈ set(facesAt g v) . P f}" by(simp add: next_plane0_finalVertex_facesAt_eq[OF prems]) also have "… = |filter P (facesAt g v)|" using distinct_card[OF dist] by simp finally show ?thesis . qed subsection{* Properties of @{const subdivFace'} *} lemma new_edge_subdivFace': "!!f v n g. pre_subdivFace' g f u v n ovs ==> minGraphProps g ==> f ∈ \<F> g ==> subdivFace' g f v n ovs = makeFaceFinal f g ∨ (∀f' ∈ \<F> (subdivFace' g f v n ovs) - (\<F> g - {f}). ∃e ∈ \<E> f'. e ∉ \<E> g)" proof (induct ovs) case Nil thus ?case by simp next case (Cons ov ovs) note IH = Cons(1) and pre = Cons(2) and mgp = Cons(3) and fg = Cons(4) have uf: "u ∈ \<V> f" and vf: "v ∈ \<V> f" and distf: "distinct (vertices f)" using pre by(simp add:pre_subdivFace'_def)+ note distFg = minGraphProps11'[OF mgp] show ?case proof (cases ov) case None have pre': "pre_subdivFace' g f u v (Suc n) ovs" using None pre by (simp add: pre_subdivFace'_None) show ?thesis using None by (simp add: IH[OF pre' mgp fg]) next case (Some w) note pre = pre[simplified Some] have uvw: "before (verticesFrom f u) v w" using pre by(simp add:pre_subdivFace'_def) have uw: "u ≠ w" using pre by(clarsimp simp: pre_subdivFace'_def) { assume w: "f • v = w" and n: "n = 0" have pre': "pre_subdivFace' g f u w 0 ovs" using pre Some n by (simp (depth_limit:5) add: pre_subdivFace'_Some2) note IH[OF pre' mgp fg] } moreover { let ?vs = "[countVertices g..<countVertices g + n]" let ?fdg = "splitFace g v w f ?vs" let ?f1 = "fst ?fdg" and ?f2 = "fst(snd ?fdg)" and ?g' = "snd(snd ?fdg)" let ?g'' = "subdivFace' ?g' ?f2 w 0 ovs" let ?fvw = "between(vertices f) v w" and ?fwv = "between(vertices f) w v" assume a: "f • v = w --> 0 < n" have fsubg: "\<V> f ⊆ \<V> g" using mgp fg by(simp add: minGraphProps_def faces_subset_def) have pre_fdg: "pre_splitFace g v w f ?vs" apply (rule pre_subdivFace'_preFaceDiv[OF pre fg _ fsubg]) using a by simp hence "v ≠ w" and "w ∈ \<V> f" by(unfold pre_splitFace_def)simp+ have f1: "?f1= fst(split_face f v w ?vs)" and f2: "?f2 = snd(split_face f v w ?vs)" by(auto simp add:splitFace_def split_def) note pre_split = pre_splitFace_pre_split_face[OF pre_fdg] have E1: "\<E> ?f1 = Edges (w # rev ?vs @ [v]) ∪ Edges (v # ?fvw @ [w])" using f1 by(simp add:edges_split_face1[OF pre_split]) have E2: "\<E> ?f2 = Edges (v # ?vs @ [w]) ∪ Edges (w # ?fwv @ [v])" by(simp add:splitFace_def split_def edges_split_face2[OF pre_split]) note mgp' = splitFace_holds_minGraphProps[OF pre_fdg mgp] note distFg' = minGraphProps11'[OF mgp'] have pre': "pre_subdivFace' ?g' ?f2 u w 0 ovs" by (rule pre_subdivFace'_Some1[OF pre fg _ fsubg HOL.refl HOL.refl]) (simp add:a) note f2inF = splitFace_add_f21'[OF fg] have 1: "∃e ∈ \<E> ?f1. e ∉ \<E> g" proof cases assume "rev ?vs = []" hence "(w,v) ∈ \<E> ?f1 ∧ (w,v) ∉ \<E> g" using pre_fdg E1 by(unfold pre_splitFace_def) (auto simp:Edges_Cons) thus ?thesis by blast next assume "rev ?vs ≠ []" then obtain x xs where rvs: "rev ?vs = x#xs" by(auto simp only:neq_Nil_conv) hence "(w,x) ∈ \<E> ?f1" using E1 by (auto simp:Edges_Cons) moreover have "(w,x) ∉ \<E> g" proof - have "x ∈ set(rev ?vs)" using rvs by simp hence "x ≥ countVertices g" by simp hence "x ∉ \<V> g" by(induct g) (simp add:vertices_graph_def) thus ?thesis by (auto simp:edges_graph_def) (blast dest: in_edges_in_vertices minGraphProps9[OF mgp]) qed ultimately show ?thesis by blast qed have 2: "∃e ∈ \<E> ?f2. e ∉ \<E> g" proof cases assume "?vs = []" hence "(v,w) ∈ \<E> ?f2 ∧ (v,w) ∉ \<E> g" using pre_fdg E2 by(unfold pre_splitFace_def) (auto simp:Edges_Cons) thus ?thesis by blast next assume "?vs ≠ []" then obtain x xs where vs: "?vs = x#xs" by(auto simp only:neq_Nil_conv) hence "(v,x) ∈ \<E> ?f2" using E2 by (auto simp:Edges_Cons) moreover have "(v,x) ∉ \<E> g" proof - have "x ∈ set ?vs" using vs by simp hence "x ≥ countVertices g" by simp hence "x ∉ \<V> g" by(induct g) (simp add:vertices_graph_def) thus ?thesis by (auto simp:edges_graph_def) (blast dest: in_edges_in_vertices minGraphProps9[OF mgp]) qed ultimately show ?thesis by blast qed have fdg: "(?f1,?f2,?g') = splitFace g v w f ?vs" by auto hence Fg': "\<F> ?g' = {?f1,?f2} ∪ (\<F> g - {f})" using set_faces_splitFace[OF mgp fg pre_fdg] by blast have "∀f' ∈ \<F> ?g'' - (\<F> g - {f}). ∃e ∈ \<E> f'. e ∉ \<E> g" proof (clarify) fix f' assume f'g'': "f' ∈ \<F> ?g''" and f'ng: "f' ∉ \<F> g - {f}" from IH[OF pre' mgp' f2inF] show "∃e ∈ \<E> f'. e ∉ \<E> g" proof assume "?g'' = makeFaceFinal ?f2 ?g'" hence "f' = setFinal ?f2 ∨ f' = ?f1" (is "?A ∨ ?B") using f'g'' Fg' f'ng by(auto simp:makeFaceFinal_def makeFaceFinalFaceList_def distinct_set_replace[OF distFg']) thus ?thesis proof assume ?A thus ?thesis using 2 by(simp) next assume ?B thus ?thesis using 1 by blast qed next assume A: "∀f' ∈ \<F> ?g'' - (\<F> ?g' - {?f2}). ∃e ∈ \<E> f'. e ∉ \<E> ?g'" show ?thesis proof cases assume "f' ∈ {?f1,?f2}" thus ?thesis using 1 2 by blast next assume "f' ∉ {?f1,?f2}" hence "∃e∈\<E> f'. e ∉ \<E> ?g'" using A f'g'' f'ng Fg' by simp with splitFace_edges_incr[OF pre_fdg fdg] show ?thesis by blast qed qed qed } ultimately show ?thesis using Some by(auto simp: split_def) qed qed lemma dist_edges_subdivFace': "pre_subdivFace' g f u v n ovs ==> minGraphProps g ==> f ∈ \<F> g ==> subdivFace' g f v n ovs = makeFaceFinal f g ∨ (∀f' ∈ \<F> (subdivFace' g f v n ovs) - (\<F> g - {f}). \<E> f' ≠ \<E> f)" apply(drule (2) new_edge_subdivFace') apply(erule disjE) apply blast apply(rule disjI2) apply(clarify) apply(drule bspec) apply fast apply(simp add:edges_graph_def) by(blast) lemma between_last: "[| distinct(vertices f); u ∈ \<V> f |] ==> between (vertices f) u (last (verticesFrom f u)) = butlast(tl(verticesFrom f u))" apply(drule split_list) apply (fastsimp dest: last_in_set simp: between_def verticesFrom_Def split_def last_append butlast_append fst_splitAt_last) done (* FIXME replaces subdivFace'_final_base below *) (* FIXME move condition to pre_addfacesnd? *) lemma final_subdivFace': "!!f u n g. minGraphProps g ==> pre_subdivFace' g f r u n ovs ==> f ∈ \<F> g ==> (ovs = [] --> n=0 ∧ u = last(verticesFrom f r)) ==> ∃f' ∈ set(finals(subdivFace' g f u n ovs)) - set(finals g). (f-1 • r,r) ∈ \<E> f' ∧ |vertices f'| = n + |ovs| + (if r=u then 1 else |between (vertices f) r u| + 2)" proof (induct ovs) case Nil show ?case (is "∃f' ∈ ?F. ?P f'") proof show "?P (setFinal f)" (is "?A ∧ ?B") proof show "?A" using Nil by(simp add:pre_subdivFace'_def prevVertex_in_edges del:is_nextElem_edges_eq) show "?B" using Nil mgp_vertices3[OF Nil(1,3)] by(simp add: setFinal_def between_last pre_subdivFace'_def) arith qed next show "setFinal f ∈ ?F" using Nil by(simp add:pre_subdivFace'_def setFinal_notin_finals minGraphProps11') qed next case (Cons ov ovs) note IH = Cons(1) and mgp = Cons(2) and pre = Cons(3) and fg = Cons(4) and mt = Cons(5) have "r ∈ \<V> f" and "u ∈ \<V> f" and distf: "distinct (vertices f)" using pre by(simp add:pre_subdivFace'_def)+ show ?case proof (cases ov) case None have pre': "pre_subdivFace' g f r u (Suc n) ovs" using None pre by (simp add: pre_subdivFace'_None) have "ovs ≠ []" using pre None by (auto simp: pre_subdivFace'_def) thus ?thesis using None IH[OF mgp pre' fg] by simp next case (Some v) note pre = pre[simplified Some] have ruv: "before (verticesFrom f r) u v" and "r ≠ v" using pre by(simp add:pre_subdivFace'_def)+ show ?thesis proof (cases "f • u = v ∧ n = 0") case True have pre': "pre_subdivFace' g f r v 0 ovs" using pre True by (simp (depth_limit:5) add: pre_subdivFace'_Some2) have mt: "ovs = [] --> 0 = 0 ∧ v = last (verticesFrom f r)" using pre by(clarsimp simp:pre_subdivFace'_def) show ?thesis using Some True IH[OF mgp pre' fg mt] `r ≠ v` by(auto simp: between_next_empty[OF distf] unroll_between_next2[OF distf `r ∈ \<V> f` `u ∈ \<V> f`]) next case False let ?vs = "[countVertices g..<countVertices g + n]" let ?fdg = "splitFace g u v f ?vs" let ?g' = "snd(snd ?fdg)" and ?f2 = "fst(snd ?fdg)" let ?fvu = "between (vertices f) v u" have False': "f • u = v --> n ≠ 0" using False by auto have VfVg: "\<V> f ⊆ \<V> g" using mgp fg by (simp add: minGraphProps_def faces_subset_def) note pre_fdg = pre_subdivFace'_preFaceDiv[OF pre fg False' VfVg] hence "u ≠ v" and "v ∈ \<V> f" and disj: "\<V> f ∩ set ?vs = {}" by(unfold pre_splitFace_def)simp+ hence vvs: "v ∉ set ?vs" by auto have vf2: "vertices ?f2 = [v] @ ?fvu @ u # ?vs" by(simp add:split_face_def splitFace_def split_def) hence betuvf2: "between (vertices ?f2) u v = ?vs" using splitFace_distinct1[OF pre_fdg] by(simp add: between_back) have betrvf2: "r ≠ u ==> between (vertices ?f2) r v = between (vertices f) r u @ [u] @ ?vs" proof - assume "r≠u" have r: "r ∈ set (between (vertices f) v u)" using `r≠u` `r≠v` `u≠v` `v ∈ \<V> f` `r ∈ \<V> f` distf ruv by(blast intro:rotate_before_vFrom before_between) have "between (vertices f) v u = between (vertices f) v r @ [r] @ between (vertices f) r u" using split_between[OF distf `v ∈ \<V> f` `u ∈ \<V> f` r] `r≠v` by simp moreover hence "v ∉ set (between (vertices f) r u)" using between_not_r1[OF distf, of v u] by simp ultimately show ?thesis using vf2 `r≠v` `u≠v` vvs by (simp add: between_back between_not_r2[OF distf]) qed note mgp' = splitFace_holds_minGraphProps[OF pre_fdg mgp] note f2g = splitFace_add_f21'[OF fg] note pre' = pre_subdivFace'_Some1[OF pre fg False' VfVg HOL.refl HOL.refl] from pre_fdg have "v ∈ \<V> f" and disj: "\<V> f ∩ set ?vs = {}" by(unfold pre_splitFace_def, simp)+ have fr: "?f2-1 • r = f-1 • r" proof - note pre_split = pre_splitFace_pre_split_face[OF pre_fdg] have rinf2: "r ∈ \<V> ?f2" proof cases assume "r = u" thus ?thesis by(simp add:vf2) next assume "r ≠ u" hence "r ∈ set ?fvu" using distf `v : \<V> f` `r≠v` `r : \<V> f` ruv by(blast intro: before_between rotate_before_vFrom) thus ?thesis by(simp add:vf2) qed have E2: "\<E> ?f2 = Edges (u # ?vs @ [v]) ∪ Edges (v # ?fvu @ [u])" by(simp add:splitFace_def split_def edges_split_face2[OF pre_split]) moreover have "(?f2-1 • r, r) ∈ \<E> ?f2" by(blast intro: prevVertex_in_edges rinf2 splitFace_distinct1[OF pre_fdg]) moreover have "(?f2-1 • r, r) ∉ Edges (u # ?vs @ [v])" proof - have "r ∉ set ?vs" using `r : \<V> f` disj by blast thus ?thesis using `r ≠ v` by(simp add:Edges_Cons Edges_append notinset_notinEdge2) arith qed ultimately have "(?f2-1 • r, r) ∈ Edges (v # ?fvu @ [u])" by blast hence "(?f2-1 • r, r) ∈ \<E> f" using pre_split_face_symI[OF pre_split] by(blast intro: Edges_between_edges) hence eq: "f • (?f2-1 • r) = r" and inf: "?f2-1 • r ∈ \<V> f" by(simp add:edges_face_eq)+ have "?f2-1 • r = f-1 • (f • (?f2-1 • r))" using prevVertex_nextVertex[OF distf inf] by simp also have "… = f-1 • r" using eq by simp finally show ?thesis . qed hence mt: "ovs = [] --> 0 = 0 ∧ v = last (verticesFrom ?f2 r)" using pre' pre by(auto simp:pre_subdivFace'_def splitFace_def split_def last_vFrom) from IH[OF mgp' pre' f2g mt] `r ≠ v` obtain f' where f: "f' ∈ set(finals(subdivFace' ?g' ?f2 v 0 ovs)) - set(finals ?g')" and ff: "(?f2-1 • r, r) ∈ \<E> f'" "|vertices f'| = |ovs| + |between (vertices ?f2) r v| + 2" by simp blast show ?thesis (is "∃f' ∈ ?F. ?P f'") proof show "f' ∈ ?F" using f pre Some fg by(simp add:False split_def pre_subdivFace'_def) show "?P f'" using ff fr by(clarsimp simp:betuvf2 betrvf2) qed qed qed qed lemma subdivFace'_final_base: "!!f u n g. minGraphProps g ==> pre_subdivFace' g f r u n ovs ==> f ∈ \<F> g ==> ∃f' ∈ \<F> (subdivFace' g f u n ovs). final f' ∧ (f-1 • r,r) ∈ \<E> f'" proof (induct ovs) case Nil show ?case (is "∃f' ∈ ?F. ?P f'") proof show "?P (setFinal f)" using Nil by(simp add:pre_subdivFace'_def prevVertex_in_edges del:is_nextElem_edges_eq) next show "setFinal f ∈ ?F" using Nil by (simp add: makeFaceFinal_def makeFaceFinalFaceList_def replace3) qed next case (Cons ov ovs) show ?case proof (cases ov) case None thus ?thesis using Cons by(fastsimp simp:pre_subdivFace'_None) next case (Some v) show ?thesis proof (cases "f • u = v ∧ n = 0") case True with Cons Some show ?thesis by(fastsimp intro:pre_subdivFace'_Some2) next case False note IH = Cons(1) and mgp = Cons(2) and pre = Cons(3) and fg = Cons(4) note pre = pre[simplified Some] have ruv: "before (verticesFrom f r) u v" and "v ≠ r" and distf: "distinct (vertices f)" and "r ∈ \<V> f" using pre by(simp add:pre_subdivFace'_def)+ let ?vs = "[countVertices g..<countVertices g + n]" let ?fdg = "splitFace g u v f ?vs" let ?g' = "snd(snd ?fdg)" and ?f2 = "fst(snd ?fdg)" have False': "f • u = v --> n ≠ 0" using False by auto have VfVg: "\<V> f ⊆ \<V> g" using mgp fg by (simp add: minGraphProps_def faces_subset_def) note pre_fdg = pre_subdivFace'_preFaceDiv[OF pre fg False' VfVg] note mgp' = splitFace_holds_minGraphProps[OF pre_fdg mgp] note f2g = splitFace_add_f21'[OF fg] note pre' = pre_subdivFace'_Some1[OF pre fg False' VfVg HOL.refl HOL.refl] from pre_fdg have "v ∈ \<V> f" and disj: "\<V> f ∩ set ?vs = {}" by(unfold pre_splitFace_def, simp)+ from IH[OF mgp' pre' f2g] obtain f' where "f' ∈ \<F> (subdivFace' ?g' ?f2 v 0 ovs)" and "final f'" and "(?f2-1 • r, r) ∈ \<E> f'" by blast moreover have "?f2-1 • r = f-1 • r" proof - let ?fvu = "between (vertices f) v u" note pre_split = pre_splitFace_pre_split_face[OF pre_fdg] have vf2: "vertices ?f2 = [v] @ ?fvu @ u # ?vs" by(simp add:split_face_def splitFace_def split_def) have rinf2: "r ∈ \<V> ?f2" proof cases assume "r = u" thus ?thesis by(simp add:vf2) next assume "r ≠ u" hence "r ∈ set ?fvu" using distf `v : \<V> f` `v≠r` `r : \<V> f` ruv by(blast intro: before_between rotate_before_vFrom) thus ?thesis by(simp add:vf2) qed have E2: "\<E> ?f2 = Edges (u # ?vs @ [v]) ∪ Edges (v # ?fvu @ [u])" by(simp add:splitFace_def split_def edges_split_face2[OF pre_split]) moreover have "(?f2-1 • r, r) ∈ \<E> ?f2" by(blast intro: prevVertex_in_edges rinf2 splitFace_distinct1[OF pre_fdg]) moreover have "(?f2-1 • r, r) ∉ Edges (u # ?vs @ [v])" proof - have "r ∉ set ?vs" using `r : \<V> f` disj by blast thus ?thesis using `v ≠ r` by(simp add:Edges_Cons Edges_append notinset_notinEdge2) arith qed ultimately have "(?f2-1 • r, r) ∈ Edges (v # ?fvu @ [u])" by blast hence "(?f2-1 • r, r) ∈ \<E> f" using pre_split_face_symI[OF pre_split] by(blast intro: Edges_between_edges) hence eq: "f • (?f2-1 • r) = r" and inf: "?f2-1 • r ∈ \<V> f" by(simp add:edges_face_eq)+ have "?f2-1 • r = f-1 • (f • (?f2-1 • r))" using prevVertex_nextVertex[OF distf inf] by simp also have "… = f-1 • r" using eq by simp finally show ?thesis . qed ultimately show ?thesis using Cons Some by(simp add:False split_def) blast qed qed qed lemma Seed_max_final_ex: "∃f∈set (finals (Seed p)). |vertices f| = maxGon p" by (simp add: Seed_def graph_max_final_ex) lemma max_face_ex: assumes a: "Seedp [next_plane0p]->* g" shows "∃f ∈ set (finals g). |vertices f| = maxGon p" using a proof (induct rule: RTranCl_induct) case refl then show ?case using Seed_max_final_ex by simp next case (succs g g') then obtain f where "f∈set (finals g)" and "|vertices f| = maxGon p" by auto moreover have "f∈set (finals g')" by (rule next_plane0_finals_incr) ultimately show ?case by auto qed end
lemma plane_final_facesAt:
[| Invariants.inv g; final g; f ∈ set (facesAt g v) |] ==> final f
lemma finalVertexI:
[| Invariants.inv g; final g; v ∈ \<V> g |] ==> finalVertex g v
lemma setFinal_notin_finals:
[| f ∈ \<F> g; ¬ final f; minGraphProps g |] ==> setFinal f ∉ set (finals g)
lemma planeN4:
[| Invariants.inv g; f ∈ \<F> g |] ==> 3 ≤ |vertices f|
lemma degree_eq:
[| Invariants.inv g; final g |] ==> degree g v = tri g v + quad g v + except g v
lemma plane_fin_exceptionalVertex_def:
[| Invariants.inv g; final g |] ==> exceptionalVertex g v = (|[f∈facesAt g v . 5 ≤ |vertices f|]| ≠ 0)
lemma not_exceptional:
[| Invariants.inv g; final g; f ∈ set (facesAt g v); ¬ exceptionalVertex g v |] ==> |vertices f| ≤ 4
lemma in_next_plane0I:
[| g' ∈ set (generatePolygon n v f g); f ∈ set (nonFinals g); v ∈ \<V> f; 3 ≤ n; n < 4 + p |] ==> g' ∈ set (next_plane0p g)
lemma next_plane0_nonfinals:
g' ∈ set (next_plane0p g) ==> nonFinals g ≠ []
lemma next_plane0_ex:
g' ∈ set (next_plane0p g) ==> ∃f∈set (nonFinals g). ∃v∈\<V> f. ∃i∈set [3..maxGon p]. g' ∈ set (generatePolygon i v f g)
lemma step_outside2:
[| Invariants.inv g; g' ∈ set (next_plane0p g); ¬ final g' |] ==> |faces g'| ≠ 2
lemma set_finals_splitFace:
[| f ∈ \<F> g; ¬ final f |] ==> set (finals (snd (snd (splitFace g u v f vs)))) = set (finals g)
lemma next_plane0_finals_incr:
[| g' ∈ set (next_plane0p g); f ∈ set (finals g) |] ==> f ∈ set (finals g')
lemma next_plane0_finals_subset:
g' ∈ set (next_plane0p g) ==> set (finals g) ⊆ set (finals g')
lemma next_plane0_final_mono:
[| g' ∈ set (next_plane0p g); f ∈ \<F> g; final f |] ==> f ∈ \<F> g'
lemma next_plane0_vertices_subset:
[| g' ∈ set (next_plane0p g); minGraphProps g |] ==> \<V> g ⊆ \<V> g'
lemma next_plane0_incr_faceListAt:
[| g' ∈ set (next_plane0p g); minGraphProps g |] ==> |faceListAt g| ≤ |faceListAt g'| ∧ (∀v<|faceListAt g|. |faceListAt g ! v| ≤ |faceListAt g' ! v|)
lemma next_plane0_incr_degree:
[| g' ∈ set (next_plane0p g); minGraphProps g; v ∈ \<V> g |] ==> degree g v ≤ degree g' v
lemma next_plane0_incr_except:
[| g' ∈ set (next_plane0p g); Invariants.inv g; v ∈ \<V> g |] ==> except g v ≤ except g' v
lemma next_plane0_set_edges_subset:
[| minGraphProps g; g' ∈ set (next_plane0p g) |] ==> \<E> g ⊆ \<E> g'
lemma next_plane0_incr_finV:
[| g' ∈ set (next_plane0p g); minGraphProps g |] ==> ∀v∈\<V> g. v ∈ \<V> g' ∧ ((∀f∈\<F> g. v ∈ \<V> f --> final f) --> (∀f∈\<F> g'. v ∈ \<V> f --> f ∈ \<F> g))
lemma next_plane0_finalVertex_mono:
[| g' ∈ set (next_plane0p g); Invariants.inv g; u ∈ \<V> g; finalVertex g u |] ==> finalVertex g' u
lemma next_plane0_finalVertex_facesAt_eq:
[| g' ∈ set (next_plane0p g); Invariants.inv g; v ∈ \<V> g; finalVertex g v |] ==> set (facesAt g' v) = set (facesAt g v)
lemma next_plane0_len_filter_eq:
[| g' ∈ set (next_plane0p g); Invariants.inv g; v ∈ \<V> g; finalVertex g v |] ==> |filter P (facesAt g' v)| = |filter P (facesAt g v)|
lemma new_edge_subdivFace':
[| pre_subdivFace' g f u v n ovs; minGraphProps g; f ∈ \<F> g |] ==> subdivFace' g f v n ovs = makeFaceFinal f g ∨ (∀f'∈\<F> (subdivFace' g f v n ovs) - (\<F> g - {f}). ∃e∈\<E> f'. e ∉ \<E> g)
lemma dist_edges_subdivFace':
[| pre_subdivFace' g f u v n ovs; minGraphProps g; f ∈ \<F> g |] ==> subdivFace' g f v n ovs = makeFaceFinal f g ∨ (∀f'∈\<F> (subdivFace' g f v n ovs) - (\<F> g - {f}). \<E> f' ≠ \<E> f)
lemma between_last:
[| distinct (vertices f); u ∈ \<V> f |] ==> between (vertices f) u (last (verticesFrom f u)) = butlast (tl (verticesFrom f u))
lemma final_subdivFace':
[| minGraphProps g; pre_subdivFace' g f r u n ovs; f ∈ \<F> g; ovs = [] --> n = 0 ∧ u = last (verticesFrom f r) |] ==> ∃f'∈set (finals (subdivFace' g f u n ovs)) - set (finals g). (f-1 • r, r) ∈ \<E> f' ∧ |vertices f'| = n + |ovs| + (if r = u then 1 else |between (vertices f) r u| + 2)
lemma subdivFace'_final_base:
[| minGraphProps g; pre_subdivFace' g f r u n ovs; f ∈ \<F> g |] ==> ∃f'∈\<F> (subdivFace' g f u n ovs). final f' ∧ (f-1 • r, r) ∈ \<E> f'
lemma Seed_max_final_ex:
∃f∈set (finals Seedp). |vertices f| = maxGon p
lemma max_face_ex:
Seedp [next_plane0p]->* g ==> ∃f∈set (finals g). |vertices f| = maxGon p