# Theory PlaneProps

Up to index of Isabelle/HOL/Tame

theory PlaneProps
imports Invariants
begin

```(*  ID:         \$Id: PlaneProps.thy,v 1.2 2006/01/09 06:56:14 nipkow Exp \$
Author:     Gertrud Bauer, Tobias Nipkow
*)

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
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")
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)"
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)
done

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'"
apply(drule next_plane0_finals_subset)
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)
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: 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(rule conjI)
prefer 2 apply blast
apply(frule minGraphProps4)
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|}"
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(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(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}"
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)"
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"
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)"
note pre_split = pre_splitFace_pre_split_face[OF pre_fdg]
have E1: "\<E> ?f1 = Edges (w # rev ?vs @ [v]) ∪ Edges (v # ?fvw @ [w])"
have E2: "\<E> ?f2 = Edges (v # ?vs @ [w]) ∪ Edges (w # ?fwv @ [v])"
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])
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
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
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
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)"
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"
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
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"
hence betuvf2: "between (vertices ?f2) u v = ?vs"
using splitFace_distinct1[OF pre_fdg]
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 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)
qed
have E2: "\<E> ?f2 = Edges (u # ?vs @ [v]) ∪
Edges (v # ?fvu @ [u])"
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`
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"
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
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
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"
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
note pre_fdg = pre_subdivFace'_preFaceDiv[OF pre fg False' VfVg]
note mgp' = splitFace_holds_minGraphProps[OF pre_fdg mgp]
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"
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)
qed
have E2: "\<E> ?f2 = Edges (u # ?vs @ [v]) ∪
Edges (v # ?fvu @ [u])"
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`
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"
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
qed
qed
qed

lemma Seed_max_final_ex:
"∃f∈set (finals (Seed p)). |vertices f| = maxGon p"

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
```

### @{const final}

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)`

### @{const degree}

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```

### Misc

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`

### Increasing final faces

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'`

### Increasing vertices

lemma next_plane0_vertices_subset:

`  [| g' ∈ set (next_plane0p g); minGraphProps g |] ==> \<V> g ⊆ \<V> g'`

### 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|)```

lemma next_plane0_incr_degree:

```  [| g' ∈ set (next_plane0p g); minGraphProps g; v ∈ \<V> g |]
==> degree g v ≤ degree g' v```

### Increasing @{const except}

lemma next_plane0_incr_except:

```  [| g' ∈ set (next_plane0p g); Invariants.inv g; v ∈ \<V> g |]
==> except g v ≤ except g' v```

### Increasing edges

lemma next_plane0_set_edges_subset:

`  [| minGraphProps g; g' ∈ set (next_plane0p g) |] ==> \<E> g ⊆ \<E> g'`

### Increasing final vertices

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```

### Preservation of @{const facesAt} at final vertices

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)|```

### Properties of @{const subdivFace'}

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`