header "Further Plane Graph Properties"
theory PlaneProps
imports Invariants
begin
subsection {* @{const final} *}
lemma plane_final_facesAt:
assumes "inv g" "final g" "v : \<V> g" "f ∈ set (facesAt g v)" shows "final f"
proof -
from assms(1,3,4) have "f ∈ \<F> g" by(blast intro: minGraphProps inv_mgp)
with assms(2) 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(fastforce 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" and v: "v : \<V> g"
shows "degree g v = tri g v + quad g v + except g v"
proof -
have dist: "distinct(facesAt g v)" using pl v 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] v 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 fastforce
apply (subst card_Un_disjoint)
apply simp
apply simp
apply fastforce
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 fin v] cong:conj_cong)
finally show ?thesis .
qed
lemma plane_fin_exceptionalVertex_def:
assumes pl: "inv g" and fin: "final g" and v: "v : \<V> g"
shows "exceptionalVertex g v =
( | [f \<leftarrow> 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 v])
then show ?thesis by (simp add: filter_simp exceptionalVertex_def except_def)
qed
lemma not_exceptional:
"inv g ==> final g ==> v : \<V> g ==> f ∈ set (facesAt g v) ==>
¬ exceptionalVertex g v ==> |vertices f| ≤ 4"
by (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_plane0⇘p⇙ g)"
proof -
have "¬ final g" using assms(2)
by(auto simp: nonFinals_def finalGraph_def filter_empty_conv)
thus ?thesis using assms by(auto simp:next_plane0_def Bex_def)
qed
lemma next_plane0_nonfinals: "g [next_plane0⇘p⇙]-> g' ==> nonFinals g ≠ []"
by(auto simp:next_plane0_def finalGraph_def)
lemma next_plane0_ex:
assumes a: "g [next_plane0⇘p⇙]-> g'"
shows "∃f∈ set(nonFinals g). ∃v ∈ \<V> f. ∃i ∈ set([3..<Suc(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_plane0⇘p⇙]-> 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_plane0⇘p⇙]-> 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_plane0⇘p⇙ g) ==>
set (finals g) ⊆ set (finals g')"
by (auto simp add: next_plane0_finals_incr)
lemma next_plane0_final_mono:
"[| g' ∈ set (next_plane0⇘p⇙ 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_plane0⇘p⇙ 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_plane0⇘p⇙ g); minGraphProps g |]
==> |faceListAt g| ≤ |faceListAt g'| &
(∀v < |faceListAt g|. |faceListAt g ! v| ≤ |faceListAt g' ! v| )"
(is "_ ==> _ ==> ?Q g g'")
apply(rule next_plane0_incr[where Q = ?Q])
prefer 4 apply assumption
prefer 4 apply assumption
apply(rule conjI) apply fastforce
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_plane0⇘p⇙ 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(frule minGraphProps4)
apply(simp add:vertices_graph)
done
subsection{* Increasing @{const except} *}
lemma next_plane0_incr_except:
assumes "g' ∈ set (next_plane0⇘p⇙ 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 assms(1,2)]
note mgp = inv_mgp[OF assms(2)] and mgp' = inv_mgp[OF inv']
note dist = distinct_filter[OF mgp_dist_facesAt[OF mgp `v : \<V> g`]]
have "v ∈ \<V> g'"
using assms(3) next_plane0_vertices_subset[OF assms(1) mgp] by blast
note dist' = distinct_filter[OF mgp_dist_facesAt[OF mgp' `v : \<V> g'`]]
have "|[f\<leftarrow>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 assms(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 assms(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 \<leftarrow> 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_plane0⇘p⇙]-> 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 *}
declare atLeastLessThan_iff[iff]
lemma next_plane0_incr_finV:
"[|g' ∈ set (next_plane0⇘p⇙ 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))" (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 fast
apply(clarsimp simp:makeFaceFinal_def vertices_graph makeFaceFinalFaceList_def)
apply(drule replace5)
apply(erule disjE)apply blast
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 atLeastLessThan_def)
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_plane0⇘p⇙ 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_plane0⇘p⇙ 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_plane0⇘p⇙ 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 assms(1,2)]
note mgp = inv_mgp[OF assms(2)] and mgp' = inv_mgp[OF inv']
note dist = distinct_filter[OF mgp_dist_facesAt[OF mgp `v : \<V> g`]]
have "v ∈ \<V> g'"
using assms(3) next_plane0_vertices_subset[OF assms(1) mgp] by blast
note dist' = distinct_filter[OF mgp_dist_facesAt[OF mgp' `v : \<V> g'`]]
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 assms])
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 using [[simp_depth_limit = 5]] by (simp 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 ?f⇣1 = "fst ?fdg" and ?f⇣2 = "fst(snd ?fdg)" and ?g' = "snd(snd ?fdg)"
let ?g'' = "subdivFace' ?g' ?f⇣2 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 f⇣1: "?f⇣1= fst(split_face f v w ?vs)"
and f⇣2: "?f⇣2 = 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 E⇣1: "\<E> ?f⇣1 = Edges (w # rev ?vs @ [v]) ∪ Edges (v # ?fvw @ [w])"
using f⇣1 by(simp add:edges_split_face1[OF pre_split])
have E⇣2: "\<E> ?f⇣2 = 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' ?f⇣2 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> ?f⇣1. e ∉ \<E> g"
proof cases
assume "rev ?vs = []"
hence "(w,v) ∈ \<E> ?f⇣1 ∧ (w,v) ∉ \<E> g" using pre_fdg E⇣1
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> ?f⇣1" using E⇣1 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> ?f⇣2. e ∉ \<E> g"
proof cases
assume "?vs = []"
hence "(v,w) ∈ \<E> ?f⇣2 ∧ (v,w) ∉ \<E> g" using pre_fdg E⇣2
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> ?f⇣2" using E⇣2 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: "(?f⇣1,?f⇣2,?g') = splitFace g v w f ?vs" by auto
hence Fg': "\<F> ?g' = {?f⇣1,?f⇣2} ∪ (\<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 ?f⇣2 ?g'"
hence "f' = setFinal ?f⇣2 ∨ f' = ?f⇣1" (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' - {?f⇣2}).
∃e ∈ \<E> f'. e ∉ \<E> ?g'"
show ?thesis
proof cases
assume "f' ∈ {?f⇣1,?f⇣2}"
thus ?thesis using 1 2 by blast
next
assume "f' ∉ {?f⇣1,?f⇣2}"
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 (fastforce dest: last_in_set
simp: between_def verticesFrom_Def split_def
last_append butlast_append fst_splitAt_last)
done
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)
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 using [[simp_depth_limit = 5]] by (simp 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 ?f⇣2 = "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 vf⇣2: "vertices ?f⇣2 = [v] @ ?fvu @ u # ?vs"
by(simp add:split_face_def splitFace_def split_def)
hence betuvf⇣2: "between (vertices ?f⇣2) u v = ?vs"
using splitFace_distinct1[OF pre_fdg]
by(simp add: between_back)
have betrvf⇣2: "r ≠ u ==> between (vertices ?f⇣2) 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 vf⇣2 `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: "?f⇣2⇗-1⇖ • r = f⇗-1⇖ • r"
proof -
note pre_split = pre_splitFace_pre_split_face[OF pre_fdg]
have rinf⇣2: "r ∈ \<V> ?f⇣2"
proof cases
assume "r = u" thus ?thesis by(simp add:vf⇣2)
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:vf⇣2)
qed
have E⇣2: "\<E> ?f⇣2 = Edges (u # ?vs @ [v]) ∪
Edges (v # ?fvu @ [u])"
by(simp add:splitFace_def split_def
edges_split_face2[OF pre_split])
moreover have "(?f⇣2⇗-1⇖ • r, r) ∈ \<E> ?f⇣2"
by(blast intro: prevVertex_in_edges rinf⇣2
splitFace_distinct1[OF pre_fdg])
moreover have "(?f⇣2⇗-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 "(?f⇣2⇗-1⇖ • r, r) ∈ Edges (v # ?fvu @ [u])" by blast
hence "(?f⇣2⇗-1⇖ • r, r) ∈ \<E> f" using pre_split_face_symI[OF pre_split]
by(blast intro: Edges_between_edges)
hence eq: "f • (?f⇣2⇗-1⇖ • r) = r" and inf: "?f⇣2⇗-1⇖ • r ∈ \<V> f"
by(simp add:edges_face_eq)+
have "?f⇣2⇗-1⇖ • r = f⇗-1⇖ • (f • (?f⇣2⇗-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 ?f⇣2 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' :: face where
f: "f' ∈ set(finals(subdivFace' ?g' ?f⇣2 v 0 ovs)) - set(finals ?g')"
and ff: "(?f⇣2⇗-1⇖ • r, r) ∈ \<E> f'"
"|vertices f'| = |ovs| + |between (vertices ?f⇣2) 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:betuvf⇣2 betrvf⇣2)
qed
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: "Seed⇘p⇙ [next_plane0⇘p⇙]->* 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: "f∈set (finals g)" and "|vertices f| = maxGon p"
by auto
moreover from succs(1) f have "f∈set (finals g')" by (rule next_plane0_finals_incr)
ultimately show ?case by auto
qed
end