Theory PlaneProps

(*  Author:  Gertrud Bauer, Tobias Nipkow  *)

section "Further Plane Graph Properties"

theory PlaneProps
imports Invariants
begin

subsection ‹@{const final}›

lemma plane_final_facesAt:
assumes "inv g" "final g" "v : 𝒱 g" "f ∈ set (facesAt g v)" shows "final f"
proof -
  from assms(1,3,4) have "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 ∈ 𝒱 g ⟧ ⟹ finalVertex g v"
by (auto simp add: finalVertex_def nonFinals_def filter_empty_conv plane_final_facesAt)


lemma setFinal_notin_finals:
 "⟦ 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 ∈ ℱ 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 : 𝒱 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 : 𝒱 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 v])
  then show ?thesis by (simp add: filter_simp exceptionalVertex_def except_def)
qed

lemma not_exceptional:
  "inv g ⟹ final g ⟹ 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 ∈ 𝒱 f" "3 ≤ n" "n < 4+p"
shows "g' ∈ set (next_plane0⇘p⇙ g)"
proof -
  from assms have
    "∃n∈{3..<4 + p}. g' ∈ set (generatePolygon n v f g)"
    by auto
  with assms have 
    "∃v∈𝒱 f. ∃n∈{3..<4 + p}. g' ∈ set (generatePolygon n v f g)"
    by auto
  with assms have
    "∃f∈set (nonFinals g). ∃v∈𝒱 f. ∃n∈{3..<4 + p}. g' ∈ set (generatePolygon n v f g)"
    by auto
  moreover have "¬ final g" using assms(2)
    by (auto simp: nonFinals_def finalGraph_def filter_empty_conv)
  ultimately show ?thesis
    by (simp add: next_plane0_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 ∈ 𝒱 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 ∈ ℱ 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:if_split_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 ∈ ℱ g; final 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 ⟧ ⟹ 𝒱 g ⊆ 𝒱 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 ∈ 𝒱 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 ∈ 𝒱 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 : 𝒱 g›]]
  have "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 : 𝒱 g'›]]
  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∈ ℱ g. v ∈ 𝒱 f ∧ final f ∧ 5 ≤ |vertices f|}"
    by(simp add: minGraphProps_facesAt_eq[OF mgp assms(3)])
  also have "… = {f ∈ set(finals g) . v ∈ 𝒱 f ∧ 5 ≤ |vertices f|}"
    by(auto simp:finals_def)
  also have "card … ≤ card{f ∈ set(finals g'). 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∈ ℱ g' . 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 ∈ 𝒱 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_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›

(*
This should really be proved via the (unproven) invariant
v : f ⟹ ((g,v).f).(f.v) = v
*)

declare  atLeastLessThan_iff[iff]

lemma next_plane0_incr_finV:
 "⟦g' ∈ set (next_plane0⇘p⇙ g); minGraphProps g ⟧
  ⟹ ∀v ∈ 𝒱 g. v ∈ 𝒱 g' ∧
        ((∀f∈ℱ g. v ∈ 𝒱 f ⟶ final f) ⟶
         (∀f∈ℱ g'. v ∈ 𝒱 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 ∈ 𝒱 g; finalVertex g u ⟧
  ⟹ finalVertex g' u"
apply(frule (1) invariantE[OF inv_inv_next_plane0])
apply(subgoal_tac "u ∈ 𝒱 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 ∈ 𝒱 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 ∈ 𝒱 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 ∈ 𝒱 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 : 𝒱 g›]]
  have "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 : 𝒱 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 ∈ ℱ g ⟹
  subdivFace' g f v n ovs = makeFaceFinal f g ∨
  (∀f' ∈ ℱ (subdivFace' g f v n ovs) - (ℱ g - {f}).
   ∃e ∈ ℰ f'. 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 ∈ 𝒱 f" and vf: "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⇩₁ = "fst ?fdg" and ?f⇩₂ = "fst(snd ?fdg)" and ?g' = "snd(snd ?fdg)"
      let ?g'' = "subdivFace' ?g' ?f⇩₂ 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: "𝒱 f ⊆ 𝒱 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 ∈ 𝒱 f" by(unfold pre_splitFace_def)simp+
      have f⇩₁: "?f⇩₁= fst(split_face f v w ?vs)"
        and f⇩₂: "?f⇩₂ = 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⇩₁: "ℰ ?f⇩₁ = Edges (w # rev ?vs @ [v]) ∪ Edges (v # ?fvw @ [w])"
        using f⇩₁ by(simp add:edges_split_face1[OF pre_split])
      have E⇩₂: "ℰ ?f⇩₂ = 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⇩₂ 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 ∈ ℰ ?f⇩₁. e ∉ ℰ g"
      proof cases
        assume "rev ?vs = []"
        hence "(w,v) ∈ ℰ ?f⇩₁ ∧ (w,v) ∉ ℰ g" using pre_fdg E⇩₁
          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) ∈ ℰ ?f⇩₁" using E⇩₁ by (auto simp:Edges_Cons)
        moreover have "(w,x) ∉ ℰ g"
        proof -
          have "x ∈ set(rev ?vs)" using rvs by simp
          hence "x ≥ countVertices g" by simp
          hence "x ∉ 𝒱 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 ∈ ℰ ?f⇩₂. e ∉ ℰ g"
      proof cases
        assume "?vs = []"
        hence "(v,w) ∈ ℰ ?f⇩₂ ∧ (v,w) ∉ ℰ g" using pre_fdg E⇩₂
          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) ∈ ℰ ?f⇩₂" using E⇩₂ by (auto simp:Edges_Cons)
        moreover have "(v,x) ∉ ℰ g"
        proof -
          have "x ∈ set ?vs" using vs by simp
          hence "x ≥ countVertices g" by simp
          hence "x ∉ 𝒱 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⇩₁,?f⇩₂,?g') = splitFace g v w f ?vs" by auto
      hence Fg': "ℱ ?g' = {?f⇩₁,?f⇩₂} ∪ (ℱ g - {f})"
        using set_faces_splitFace[OF mgp fg pre_fdg] by blast
      have "∀f' ∈ ℱ ?g'' - (ℱ g - {f}). ∃e ∈ ℰ f'. e ∉ ℰ g"
      proof (clarify)
        fix f' assume f'g'': "f' ∈ ℱ ?g''" and f'ng: "f' ∉ ℱ g - {f}"
        from IH[OF pre' mgp' f2inF]
        show "∃e ∈ ℰ f'. e ∉ ℰ g"
        proof
          assume "?g'' = makeFaceFinal ?f⇩₂ ?g'"
          hence "f' = setFinal ?f⇩₂ ∨ f' = ?f⇩₁" (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' ∈ ℱ ?g'' - (ℱ ?g' - {?f⇩₂}).
                     ∃e ∈ ℰ f'. e ∉ ℰ ?g'"
          show ?thesis
          proof cases
            assume "f' ∈ {?f⇩₁,?f⇩₂}"
            thus ?thesis using 1 2 by blast
          next
            assume "f' ∉ {?f⇩₁,?f⇩₂}"
            hence "∃e∈ℰ f'. 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 ∈ ℱ g ⟹
  subdivFace' g f v n ovs = makeFaceFinal f g ∨
  (∀f' ∈ ℱ (subdivFace' g f v n ovs) - (ℱ g - {f}). ℰ f' ≠ ℰ 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 ∈ 𝒱 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

(* FIXME move condition to pre_addfacesnd? *)
lemma final_subdivFace': "⋀f u n g. minGraphProps g ⟹
  pre_subdivFace' g f r u n ovs ⟹ 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) ∈ ℰ 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 ∈ 𝒱 f" and "u ∈ 𝒱 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 ∈ 𝒱 f› ‹u ∈ 𝒱 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⇩₂ = "fst(snd ?fdg)"
      let ?fvu = "between (vertices f) v u"
      have False': "f ∙ u = v ⟶ n ≠ 0" using False by auto
      have VfVg: "𝒱 f ⊆ 𝒱 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 ∈ 𝒱 f" and disj: "𝒱 f ∩ set ?vs = {}"
        by(unfold pre_splitFace_def)simp+
      hence vvs: "v ∉ set ?vs" by auto
      have vf⇩₂: "vertices ?f⇩₂ = [v] @ ?fvu @ u # ?vs"
        by(simp add:split_face_def splitFace_def split_def)
      hence betuvf⇩₂: "between (vertices ?f⇩₂) u v = ?vs"
        using splitFace_distinct1[OF pre_fdg]
        by(simp add: between_back)
      have betrvf⇩₂: "r ≠ u ⟹ between (vertices ?f⇩₂) 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 ∈ 𝒱 f› ‹r ∈ 𝒱 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 ∈ 𝒱 f› ‹u ∈ 𝒱 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⇩₂ ‹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 ∈ 𝒱 f" and disj: "𝒱 f ∩ set ?vs = {}"
        by(unfold pre_splitFace_def, simp)+
      have fr: "?f⇩₂⇗^-1⇖ ∙ r = f⇗^-1⇖ ∙ r"
      proof -
        note pre_split = pre_splitFace_pre_split_face[OF pre_fdg]
        have rinf⇩₂: "r ∈ 𝒱 ?f⇩₂"
        proof cases
          assume "r = u" thus ?thesis by(simp add:vf⇩₂)
        next
          assume "r ≠ u"
          hence "r ∈ set ?fvu" using distf ‹v : 𝒱 f› ‹r≠v› ‹r : 𝒱 f› ruv
            by(blast intro: before_between rotate_before_vFrom)
          thus ?thesis by(simp add:vf⇩₂)
        qed
        have E⇩₂: "ℰ ?f⇩₂ = Edges (u # ?vs @ [v]) ∪
                             Edges (v # ?fvu @ [u])"
          by(simp add:splitFace_def split_def
            edges_split_face2[OF pre_split])
        moreover have "(?f⇩₂⇗^-1⇖ ∙ r, r) ∈ ℰ ?f⇩₂"
          by(blast intro: prevVertex_in_edges rinf⇩₂
            splitFace_distinct1[OF pre_fdg])
        moreover have "(?f⇩₂⇗^-1⇖ ∙ r, r) ∉ Edges (u # ?vs @ [v])"
        proof -
          have "r ∉ set ?vs" using ‹r : 𝒱 f› disj by blast
          thus ?thesis using ‹r ≠ v›
            by(simp add:Edges_Cons Edges_append notinset_notinEdge2) arith
        qed
        ultimately have "(?f⇩₂⇗^-1⇖ ∙ r, r) ∈ Edges (v # ?fvu @ [u])" by blast
        hence "(?f⇩₂⇗^-1⇖ ∙ r, r) ∈ ℰ f" using pre_split_face_symI[OF pre_split]
          by(blast intro: Edges_between_edges)
        hence eq: "f ∙ (?f⇩₂⇗^-1⇖ ∙ r) = r" and inf: "?f⇩₂⇗^-1⇖ ∙ r ∈ 𝒱 f"
          by(simp add:edges_face_eq)+
        have "?f⇩₂⇗^-1⇖ ∙ r = f⇗^-1⇖ ∙ (f ∙ (?f⇩₂⇗^-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⇩₂ 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⇩₂ v 0 ovs)) - set(finals ?g')"
        and ff: "(?f⇩₂⇗^-1⇖ ∙ r, r) ∈ ℰ f'"
        "|vertices f'| = |ovs| + |between (vertices ?f⇩₂) 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⇩₂ betrvf⇩₂)
      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