Theory PlaneProps

(*  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