Theory Invariants

(*  Author:     Gertrud Bauer, Tobias Nipkow
*)

section‹Invariants of (Plane) Graphs›

theory Invariants
imports FaceDivisionProps
begin

subsection‹Rotation of face into normal form›

definition minVertex :: "face ⇒ vertex" where
"minVertex f ≡ min_list (vertices f)"

(* FIXME define normFace via rotate_min *)
definition normFace :: "face ⇒ vertex list" where
"normFace ≡ λf. verticesFrom f (minVertex f)"

definition normFaces :: "face list ⇒ vertex list list" where
"normFaces fl ≡ map normFace fl"

lemma normFaces_distinct:  "distinct (normFaces fl) ⟹ distinct fl"
apply (induct fl) by (auto simp: normFace_def normFaces_def)


(***********************************************************************)

subsection ‹Minimal (plane) graph properties›

definition minGraphProps' :: "graph ⇒ bool" where
  "minGraphProps' g ≡ ∀f ∈ ℱ g. 2 < |vertices f| ∧ distinct (vertices f)"

definition edges_sym :: "graph ⇒ bool" where
"edges_sym g ≡ ∀ a b. (a,b) ∈ edges g ⟶ (b,a) ∈ edges g"

definition faceListAt_len :: "graph ⇒ bool" where
"faceListAt_len g ≡ (length (faceListAt g) = countVertices g)"

definition facesAt_eq :: "graph ⇒ bool" where
"facesAt_eq g ≡ ∀v ∈ 𝒱 g. set(facesAt g v) = {f. f ∈ ℱ g ∧ v ∈ 𝒱 f}"

definition facesAt_distinct :: "graph ⇒ bool" where
"facesAt_distinct g ≡ ∀v ∈ 𝒱 g. distinct (normFaces (facesAt g  v))"

definition faces_distinct :: "graph ⇒ bool" where
"faces_distinct g ≡ distinct (normFaces (faces g))"

definition faces_subset :: "graph ⇒ bool" where
"faces_subset g ≡ ∀f ∈ ℱ g. 𝒱 f ⊆ 𝒱 g"

definition edges_disj :: "graph ⇒ bool" where
"edges_disj g ≡
 ∀f ∈ ℱ g. ∀f' ∈ ℱ g. f ≠ f' ⟶ ℰ f ∩ ℰ f' = {}"

definition face_face_op :: "graph ⇒ bool" where
"face_face_op g ≡ |faces g| ≠ 2 ⟶
 (∀f∈ℱ g. ∀f'∈ℱ g. f ≠ f' ⟶ ℰ f ≠ (ℰ f')¯)"

definition one_final_but :: "graph ⇒ (vertex × vertex)set ⇒ bool" where
"one_final_but g E ≡
 ∀f ∈ ℱ g. ¬ final f ⟶
   (∀(a,b)∈ℰ f - E. (b,a) : E ∨ (∃f'∈ℱ g. final f' ∧ (b,a) ∈ ℰ f'))"

definition one_final :: "graph ⇒ bool" where
"one_final g ≡ one_final_but g {}"


definition minGraphProps :: "graph ⇒ bool" where
"minGraphProps g ≡ minGraphProps' g ∧ facesAt_eq g ∧ faceListAt_len g ∧ facesAt_distinct g ∧ faces_distinct g ∧ faces_subset g ∧ edges_sym g ∧ edges_disj g ∧ face_face_op g"

definition inv :: "graph ⇒ bool" where
"inv g ≡ minGraphProps g ∧ one_final g ∧ |faces g| ≥ 2"


lemma facesAt_distinctI:
  "(⋀v. v ∈ 𝒱 g ⟹ distinct (normFaces (facesAt g  v))) ⟹ facesAt_distinct g"
 by (simp add: facesAt_distinct_def)

(* minGraphProps' *)
lemma minGraphProps2:
  "minGraphProps g ⟹ f ∈ ℱ g ⟹ 2 < |vertices f|"
by (unfold minGraphProps_def minGraphProps'_def) auto

lemma mgp_vertices3:
  "minGraphProps g ⟹ f ∈ ℱ g ⟹ |vertices f| ≥ 3"
by(auto dest:minGraphProps2)

lemma mgp_vertices_nonempty:
  "minGraphProps g ⟹ f ∈ ℱ g ⟹ vertices f ≠ []"
by(auto dest:minGraphProps2)

lemma minGraphProps3:
  "minGraphProps g ⟹ f ∈ ℱ g ⟹  distinct (vertices f)"
by (unfold minGraphProps_def minGraphProps'_def) auto

(* faceListAt_len *)
lemma minGraphProps4:
  "minGraphProps g ⟹ (length (faceListAt g) = countVertices g)"
by (unfold minGraphProps_def faceListAt_len_def) simp

(* facesAt_eq*)
lemma minGraphProps5:
  "⟦minGraphProps g; v : 𝒱 g; f ∈ set (facesAt g v)⟧ ⟹ f ∈ ℱ g"
by(auto simp: facesAt_def facesAt_eq_def minGraphProps_def minGraphProps'_def
              faceListAt_len_def split:if_split_asm)

lemma minGraphProps6:
  "minGraphProps g ⟹ v : 𝒱 g ⟹ f ∈ set (facesAt g v) ⟹ v ∈ 𝒱 f"
by(auto simp: facesAt_def facesAt_eq_def minGraphProps_def minGraphProps'_def
              faceListAt_len_def split:if_split_asm)

(* faces_subset *)
lemma minGraphProps9:
  "minGraphProps g ⟹ f ∈ ℱ g ⟹ v ∈ 𝒱 f ⟹ v ∈ 𝒱 g"
by (unfold minGraphProps_def faces_subset_def) auto

lemma minGraphProps7:
  "minGraphProps g ⟹ f ∈ ℱ g ⟹ v ∈ 𝒱 f ⟹  f ∈ set (facesAt g v)"
apply(frule (2) minGraphProps9)
by (unfold minGraphProps_def facesAt_eq_def) simp

lemma minGraphProps_facesAt_eq: "minGraphProps g ⟹
  v ∈ 𝒱 g ⟹ set (facesAt g v) = {f ∈ ℱ g. v ∈ 𝒱 f}"
by (simp add: minGraphProps_def facesAt_eq_def)

(* facesAt_distinct *)
lemma mgp_dist_facesAt[simp]:
  "minGraphProps g ⟹ v : 𝒱 g ⟹ distinct (facesAt g v)"
by(auto simp: facesAt_def minGraphProps_def minGraphProps'_def facesAt_distinct_def dest:normFaces_distinct)

lemma minGraphProps8:
  "minGraphProps g ⟹ v : 𝒱 g ⟹ distinct (normFaces (facesAt g v))"
by(auto simp: facesAt_def minGraphProps_def minGraphProps'_def facesAt_distinct_def normFaces_def)

lemma minGraphProps8a:
  "minGraphProps g ⟹ v ∈ 𝒱 g ⟹ distinct (normFaces (faceListAt g ! v))"
apply (frule (1) minGraphProps8[where v=v]) by (simp add: facesAt_def)

lemma minGraphProps8a': "minGraphProps g ⟹
  v < countVertices g ⟹ distinct (normFaces (faceListAt g ! v))"
by (simp add: minGraphProps8a vertices_graph)

lemma minGraphProps9':
  "minGraphProps g ⟹ f ∈ ℱ g ⟹ v ∈ 𝒱 f ⟹ v < countVertices g"
by (simp add: minGraphProps9 in_vertices_graph[symmetric])

lemma minGraphProps10:
  "minGraphProps g ⟹ (a, b) ∈ edges g ⟹ (b, a) ∈ edges g"
apply (unfold minGraphProps_def edges_sym_def)
apply (elim conjE allE impE)
by simp+

(* faces_distinct *)
lemma minGraphProps11:
  "minGraphProps g ⟹ distinct (normFaces (faces g))"
by (unfold minGraphProps_def faces_distinct_def) simp

lemma minGraphProps11':
  "minGraphProps g ⟹ distinct (faces g)"
by(simp add: minGraphProps11 normFaces_distinct)

lemma minGraphProps12:
  "minGraphProps g ⟹ f ∈ ℱ g ⟹ (a,b) ∈ ℰ f ⟹ (b,a) ∉ ℰ f"
apply (subgoal_tac "distinct (vertices f)") apply (simp add: is_nextElem_def)
 apply (case_tac "vertices f = []")
  apply (drule minGraphProps2)
   apply simp
  apply simp
 apply simp
 apply (case_tac "a = last (vertices f) ∧ b = hd (vertices f)")
  apply (case_tac "vertices f") apply simp
  apply (case_tac "list" rule: rev_exhaust)
   apply (drule minGraphProps2) apply simp
   apply simp
  apply (case_tac "ys")
   apply (drule minGraphProps2) apply simp apply simp
  apply (simp del: distinct_append distinct.simps)
  apply (rule conjI)
   apply (rule ccontr) apply (simp del: distinct_append distinct.simps)
   apply (drule is_sublist_distinct_prefix) apply simp
   apply (simp add: is_prefix_def)
  apply simp
 apply (rule conjI)
  apply (simp add: is_sublist_def) apply (elim exE) apply (intro allI) apply (rule ccontr)
  apply (simp del: distinct_append distinct.simps)
  apply (subgoal_tac "asa = as @ [a]") apply simp
  apply (rule dist_at1) apply assumption apply force apply (rule sym) apply simp
 apply (subgoal_tac "is_sublist [a, b] (vertices f)")
  apply (rule impI) apply (rule ccontr)
  apply (simp add: is_sublist_def del: distinct_append distinct.simps)
  apply (subgoal_tac "last (vertices f) = b ∧ hd (vertices f) = a")
   apply (thin_tac "a = hd (vertices f)") apply (thin_tac "b = last (vertices f)") apply (elim conjE)
   apply (elim exE)
   apply (case_tac "as")
    apply (case_tac "bs" rule: rev_exhaust) apply (drule minGraphProps2) apply simp apply simp
    apply simp+
apply (rule minGraphProps3) by simp+

lemma minGraphProps7': "minGraphProps g ⟹
  f ∈ ℱ g ⟹ v ∈ 𝒱 f ⟹  f ∈ set (faceListAt g ! v)"
apply (frule minGraphProps7) apply assumption+
by (simp add: facesAt_def split: if_split_asm)

(* edges_disj *)
lemma mgp_edges_disj:
 "⟦ minGraphProps g; f ≠ f'; f ∈ ℱ g; f' ∈ ℱ g ⟧ ⟹
  uv ∈ ℰ f ⟹ uv ∉ ℰ f'"
by (simp add:minGraphProps_def edges_disj_def) blast

(* one_final *)
lemma one_final_but_antimono:
  "one_final_but g E ⟹ E ⊆ E' ⟹ one_final_but g E'"
apply(unfold one_final_but_def)
apply blast
done

lemma one_final_antimono: "one_final g ⟹ one_final_but g E"
apply(unfold one_final_def one_final_but_def)
apply blast
done

lemma inv_two_faces: "inv g ⟹ |faces g| ≥ 2"
by(simp add:inv_def)

lemma inv_mgp[simp]: "inv g ⟹ minGraphProps g"
by(simp add:inv_def)

lemma makeFaceFinal_id[simp]: "final f ⟹ makeFaceFinal f g = g"
apply(cases g)
apply (simp add:makeFaceFinal_def makeFaceFinalFaceList_def
                setFinal_eq_iff[THEN iffD2])
done

lemma inv_one_finalD':
 "⟦ inv g; f ∈ ℱ g; ¬ final f; (a,b) ∈ ℰ f ⟧ ⟹
  ∃f' ∈ ℱ g. final f' ∧ f' ≠ f ∧ (b,a) ∈ ℰ f'"
apply(unfold inv_def one_final_def one_final_but_def)
apply blast
done

lemmas minGraphProps =
  minGraphProps2 minGraphProps3 minGraphProps4
  minGraphProps5 minGraphProps6 minGraphProps7 minGraphProps8
  minGraphProps9

lemma mgp_no_loop[simp]:
  "minGraphProps g ⟹ f ∈ ℱ g ⟹ v ∈ 𝒱 f ⟹ f ∙ v ≠ v"
apply(frule (1) mgp_vertices3)
apply(frule (1) minGraphProps3)
apply(simp add: distinct_no_loop1)
done

lemma mgp_facesAt_no_loop:
  "minGraphProps g ⟹ v : 𝒱 g ⟹ f ∈ set (facesAt g v) ⟹ f ∙ v ≠ v"
by(blast dest:mgp_no_loop minGraphProps5 minGraphProps6)

lemma edge_pres_faceAt:
 "⟦ minGraphProps g; u : 𝒱 g; f ∈ set(facesAt g u); (u,v) ∈ ℰ f ⟧ ⟹
  f ∈ set(facesAt g v)"
apply(auto simp:edges_face_eq)
apply(rule minGraphProps7, assumption)
 apply(blast intro:minGraphProps)
apply(simp)
done

lemma in_facesAt_nextVertex:
 "minGraphProps g ⟹ v : 𝒱 g ⟹ f ∈ set(facesAt g v) ⟹ f ∈ set(facesAt g (f ∙ v))"
apply(subgoal_tac "(v,f ∙ v) ∈ ℰ f")
 apply(blast intro:edge_pres_faceAt)
by(blast intro: nextVertex_in_edges minGraphProps)


lemma mgp_edge_face_ex:
assumes [intro]: "minGraphProps g" "v : 𝒱 g"
and fv: "f ∈ set(facesAt g v)" and uv: "(u,v) ∈ ℰ f"
shows "∃f' ∈ set(facesAt g v). (v,u) ∈ ℰ f'"
proof -
  from fv have "f ∈ ℱ g" by(blast intro:minGraphProps)
  with uv have "(u,v) ∈ ℰ g" by(auto simp:edges_graph_def)
  hence "(v,u) ∈ ℰ g" by(blast intro:minGraphProps10)
  then obtain f' where f': "f' ∈ ℱ g" and vu: "(v,u) ∈ ℰ f'"
    by(auto simp:edges_graph_def)
  from vu have "v ∈ 𝒱 f'" by(auto simp:edges_face_eq)
  with f' have "f' ∈ set(facesAt g v)" by(blast intro:minGraphProps)
  with vu show ?thesis by blast
qed

lemma nextVertex_in_graph:
  "minGraphProps g ⟹ v : 𝒱 g ⟹ f ∈ set(facesAt g v) ⟹ f ∙ v : 𝒱 g"
by(blast intro: minGraphProps9 minGraphProps5 minGraphProps6 nextVertex_in_face)

lemma mgp_nextVertex_face_ex2:
assumes mgp[intro]: "minGraphProps g" "v : 𝒱 g" and f: "f ∈ set(facesAt g v)"
shows "∃f' ∈ set(facesAt g (f ∙ v)). f' ∙ (f ∙ v) = v"
proof -
  from f have "(v,f ∙ v) ∈ ℰ f"
    by(blast intro: nextVertex_in_edges minGraphProps)
  with in_facesAt_nextVertex[OF mgp f]
    mgp_edge_face_ex[OF mgp(1) nextVertex_in_graph[OF mgp f]]
  obtain f' :: face where "f' ∈ set(facesAt g (f ∙ v))"
    and "(f ∙ v,v) ∈ ℰ f'"
    by(blast)
  thus ?thesis by (auto simp: edges_face_eq)
qed


lemma inv_finals_nonempty: "inv g ⟹ finals g ≠ []"
apply(frule inv_two_faces)
apply(clarsimp simp:filter_empty_conv finals_def)
apply(subgoal_tac "faces g ≠ []")
 prefer 2 apply clarsimp
apply(simp add:neq_Nil_conv)
apply clarify
apply(rename_tac f fs)
apply(case_tac "final f")
 apply simp
apply(frule mgp_vertices_nonempty[OF inv_mgp])
 apply fastforce
apply(clarsimp simp:neq_Nil_conv)
apply(rename_tac v vs)
apply(subgoal_tac "v ∈ 𝒱 f")
 prefer 2 apply simp
apply(drule nextVertex_in_edges)
apply(drule inv_one_finalD')
   prefer 2 apply assumption
  apply simp
 apply assumption
apply(auto)
done


subsection ‹@{const containsDuplicateEdge}›

definition
 containsUnacceptableEdgeSnd' :: "(nat ⇒ nat ⇒ bool) ⇒ nat list ⇒ bool" where
"containsUnacceptableEdgeSnd' N is ≡
 (∃k < |is| - 2. let i0 = is!k; i1 = is!(k+1); i2 = is!(k+2) in
 N i1 i2 ∧ (i0 < i1) ∧ (i1 < i2))"

lemma containsUnacceptableEdgeSnd_eq:
  "containsUnacceptableEdgeSnd N v is = containsUnacceptableEdgeSnd' N (v#is)"
proof (induct "is" arbitrary: v)
  case Nil then show ?case by (simp add: containsUnacceptableEdgeSnd'_def)
next
  case (Cons i "is") then show ?case
    proof (rule_tac iffI)
      assume vors: "containsUnacceptableEdgeSnd N v (i # is)"
      then show "containsUnacceptableEdgeSnd' N (v # i # is)"
        apply (cases "is") apply simp apply simp
        apply (simp split: if_split_asm del: containsUnacceptableEdgeSnd.simps)
         apply (simp add: containsUnacceptableEdgeSnd'_def) apply force
        apply (subgoal_tac "a # list = is") apply (thin_tac "is = a # list") apply (simp add: Cons)
         apply (simp add: containsUnacceptableEdgeSnd'_def) apply (elim exE)
         apply (rule exI) apply (subgoal_tac "Suc k < |is|") apply (rule conjI) apply assumption by auto
    next
      assume vors: "containsUnacceptableEdgeSnd' N (v # i # is)"
      then show "containsUnacceptableEdgeSnd N v (i # is)"
        apply simp apply (cases "is") apply (simp add: containsUnacceptableEdgeSnd'_def)
        apply (simp del:  containsUnacceptableEdgeSnd.simps)
        apply (subgoal_tac "a # list = is") apply (thin_tac "is = a # list")
         apply (simp add: Cons)
         apply (subgoal_tac "is = a # list") apply (thin_tac "a # list = is")
          apply (simp add: containsUnacceptableEdgeSnd'_def)
          apply (elim exE) apply (case_tac "k") apply simp apply simp apply (intro impI exI)
          apply (rule conjI) apply (elim conjE) apply assumption by auto
    qed
qed

lemma containsDuplicateEdge_eq1:
  "containsDuplicateEdge g f v is = containsDuplicateEdge' g f v is"
apply (simp add: containsDuplicateEdge_def)
apply (cases "is") apply (simp add: containsDuplicateEdge'_def)
apply simp
apply (case_tac "list") apply (simp add: containsDuplicateEdge'_def)
apply (simp add: containsUnacceptableEdgeSnd_eq del: containsUnacceptableEdgeSnd.simps)
apply (rule conjI) apply (simp add: containsDuplicateEdge'_def)
apply (rule impI)
apply (case_tac "a < aa")
 by (simp_all add: containsDuplicateEdge'_def containsUnacceptableEdgeSnd'_def)

lemma containsDuplicateEdge_eq:
  "containsDuplicateEdge = containsDuplicateEdge'"
apply (rule ext)+
by (simp add: containsDuplicateEdge_eq1)


declare Nat.diff_is_0_eq' [simp del]


(********************************* replaceFacesAt ****************************)
subsection‹@{const replacefacesAt}›

primrec replacefacesAt2 ::
  "nat list ⇒ face ⇒ face list ⇒ face list list ⇒ face list list" where
"replacefacesAt2 [] f fs F = F" |
"replacefacesAt2 (n#ns) f fs F =
 (if n < |F|
  then replacefacesAt2 ns f fs (F [n:=replace f fs (F!n)])
  else replacefacesAt2 ns f fs F)"


lemma replacefacesAt_eq[THEN eq_reflection]:
  "replacefacesAt ns oldf newfs F =  replacefacesAt2 ns oldf newfs F"
by (induct ns arbitrary: F) (auto simp add: replacefacesAt_def)


lemma replacefacesAt2_notin:
  "i ∉ set is ⟹ (replacefacesAt2 is olfF newFs Fss)!i = Fss!i"
proof (induct "is" arbitrary: Fss)
  case Nil then show ?case by (simp)
next
  case (Cons j js) then show ?case
    by (cases "j < |Fss|") (auto)
qed


lemma replacefacesAt2_in:
  "i ∈ set is ⟹ distinct is ⟹ i < |Fss| ⟹
  (replacefacesAt2 is olfF newFs Fss)!i = replace olfF newFs (Fss !i)"
proof (induct "is" arbitrary: Fss)
  case Nil then show ?case by simp
next
  case (Cons j js)
  then have "j = i ∧ i ∉ set js ∨ i ≠ j ∧ i ∈ set js" by auto
  then show ?case
  proof (elim disjE conjE)
    assume "j = i" "i ∉ set js" with Cons show ?thesis
    by (auto simp add: replacefacesAt2_notin)
  next
    assume "i ∈ set js" "i ≠ j" with Cons show ?thesis by simp
  qed
qed


lemma distinct_replacefacesAt21:
  "i < |Fss| ⟹ i ∈ set is ⟹ distinct is ⟹ distinct (Fss!i) ⟹ distinct newFs ⟹
  set (Fss ! i) ∩ set newFs ⊆ {olfF} ⟹
  distinct ((replacefacesAt2 is olfF newFs Fss)! i)"
proof (induct "is")
  case Nil then show ?case by simp
next
  case (Cons j js)
  then have "j = i ∧ i ∉ set js ∨ i ≠ j ∧ i ∈ set js" by auto
  then show ?case
  proof (elim disjE conjE)
    assume "j = i" "i ∉ set js" with Cons show ?thesis
     by (simp add: replacefacesAt2_notin distinct_replace)
  next
    assume "i ∈ set js" "i ≠ j" with Cons show ?thesis
     by (simp add: replacefacesAt2_in distinct_replace)
  qed
qed

lemma distinct_replacefacesAt22:
  "i < |Fss| ⟹ i ∉ set is ⟹ distinct is ⟹ distinct (Fss!i) ⟹ distinct newFs ⟹
  set (Fss ! i) ∩ set newFs ⊆ {olfF} ⟹
  distinct ((replacefacesAt2 is olfF newFs Fss)! i)"
proof (induct "is")
  case Nil then show ?case by simp
next
  case (Cons j js)
  then have "i ≠ j" by auto
  with Cons show ?case
    by (simp add: replacefacesAt2_notin distinct_replace)
qed

lemma distinct_replacefacesAt2_2:
  "i < |Fss| ⟹ distinct is ⟹ distinct (Fss!i) ⟹ distinct newFs ⟹
  set (Fss ! i) ∩ set newFs ⊆ {olfF} ⟹
  distinct ((replacefacesAt2 is olfF newFs Fss)! i)"
by (cases "i ∈ set is")
   (auto intro: distinct_replacefacesAt21 distinct_replacefacesAt22)

lemma replacefacesAt2_nth1:
  "k ∉ set ns ⟹ (replacefacesAt2 ns oldf newfs F) ! k  =  F ! k"
by (induct ns arbitrary: F) auto

lemma  replacefacesAt2_nth1': "k ∈ set ns ⟹ k < |F| ⟹ distinct ns ⟹
  (replacefacesAt2 ns oldf newfs F) ! k  =  (replace oldf newfs (F!k))"
apply (induct ns arbitrary: F)
 apply auto
 apply (simp add: replacefacesAt2_nth1)+
by (case_tac "a = k") auto


lemma replacefacesAt2_nth2: "k < |F| ⟹
  (replacefacesAt2 [k] oldf newfs F) ! k = replace oldf newfs (F!k)"
by (auto)

lemma replacefacesAt2_length[simp]:
  "|replacefacesAt2 nvs f' f'' vs| = |vs|"
by (induct nvs arbitrary: vs) simp_all

lemma replacefacesAt2_nth: "k ∈  set ns ⟹ k < |F| ⟹ oldf ∉ set newfs  ⟹
  distinct (F!k) ⟹ distinct newfs ⟹ oldf ∈ set (F!k) ⟶ set newfs ∩ set (F!k) ⊆ {oldf} ⟹
  (replacefacesAt2 ns oldf newfs F) ! k  =  (replace  oldf newfs (F!k))"
proof (induct ns arbitrary: F)
  case Nil then show ?case by simp
next
  case (Cons n ns) then show ?case
    apply (simp only: replacefacesAt2.simps)
    apply simp apply (case_tac "n = k")
     apply (simp)
     apply (subgoal_tac "replacefacesAt2 ns oldf newfs (F[k := replace  oldf newfs (F ! k)])  ! k =
    replace oldf newfs ((F[k := replace oldf newfs (F ! k)]) ! k)")
      apply simp
     apply (case_tac "k ∈ set ns")  apply (rule Cons) apply simp+
        apply (rule replace_distinct) apply simp  apply simp
        apply simp
       apply simp
      apply (simp add:distinct_set_replace)
     apply (simp add:  replacefacesAt2_nth1)
    by simp
qed


lemma replacefacesAt_notin:
  "i ∉ set is ⟹ (replacefacesAt is olfF newFs Fss)!i = Fss!i"
by (simp add: replacefacesAt_eq replacefacesAt2_notin)

lemma replacefacesAt_in:
  "i ∈ set is ⟹ distinct is ⟹ i < |Fss| ⟹
  (replacefacesAt is olfF newFs Fss)!i = replace olfF newFs (Fss !i)"
by (simp add: replacefacesAt_eq replacefacesAt2_in)

lemma replacefacesAt_length[simp]: "|replacefacesAt nvs f' [f''] vs| = |vs|"
by (simp add: replacefacesAt_eq)

lemma replacefacesAt_nth2: "k < |F| ⟹
  (replacefacesAt [k] oldf newfs F) ! k = replace oldf newfs (F!k)"
by (simp add: replacefacesAt_eq replacefacesAt2_nth2)

lemma replacefacesAt_nth: "k ∈  set ns ⟹ k < |F| ⟹ oldf ∉ set newfs  ⟹
  distinct (F!k) ⟹ distinct newfs ⟹ oldf ∈ set (F!k) ⟶ set newfs ∩ set (F!k) ⊆ {oldf} ⟹
  (replacefacesAt ns oldf newfs F) ! k  =  (replace  oldf newfs (F!k))"
by (simp add: replacefacesAt_eq replacefacesAt2_nth)

lemma replacefacesAt2_5: "x ∈ set (replacefacesAt2 ns oldf newfs F ! k) ⟹ x ∈ set (F!k) ∨ x ∈ set newfs"
proof (induct ns arbitrary: F)
  case Nil then show ?case by simp
next
  case (Cons n ns)
  then show ?case
    apply(simp add: split: if_split_asm ) apply (frule Cons)
    apply (thin_tac "⋀F. x ∈ set (replacefacesAt2 ns oldf newfs F ! k) ⟹ x ∈ set (F ! k) ∨ x ∈ set newfs")
    apply (case_tac "x ∈ set newfs")  apply simp apply simp
    apply (case_tac "k = n") apply simp apply (frule replace5) apply simp by simp
qed


lemma replacefacesAt_Nil[simp]: "replacefacesAt [] f fs F = F"
by (simp add: replacefacesAt_eq)

lemma replacefacesAt_Cons[simp]:
 "replacefacesAt (n # ns) f fs F =
  (if n < |F| then replacefacesAt ns f fs (F[n := replace f fs (F!n)])
   else replacefacesAt ns f fs F)"
by (simp add: replacefacesAt_eq)

lemmas replacefacesAt_simps = replacefacesAt_Nil replacefacesAt_Cons

lemma len_nth_repAt[simp]:
"⋀xs. i < |xs| ⟹ |replacefacesAt is x [y] xs ! i| = |xs!i|"
by (induct "is") (simp_all add: add:nth_list_update)


subsection‹@{const normFace}›

(************************** min_list & minVertex **********************)

lemma minVertex_in: "vertices f ≠ [] ⟹ minVertex f ∈ 𝒱 f"
by (simp add: minVertex_def)


lemma minVertex_eq_if_vertices_eq:
 "𝒱 f = 𝒱 f' ⟹ minVertex f = minVertex f'"
apply(cases f)
apply(cases f')
apply(rename_tac vs ft vs' ft')
apply(case_tac "vs = []")
 apply(simp add:vertices_face_def minVertex_def)
apply(subgoal_tac "vs' ≠ []")
 prefer 2 apply clarsimp
apply(simp add:vertices_face_def minVertex_def min_list_conv_Min
               insert_absorb del:Min_insert)
done


(************** normFace ***************************)


lemma normFace_replace_in:
 "normFace a ∈ set (normFaces (replace oldF newFs fs)) ⟹
  normFace a ∈ set (normFaces newFs) ∨ normFace a ∈ set (normFaces fs)"
apply (induct fs) apply simp
apply (auto simp add: normFaces_def split:if_split_asm)
done

lemma distinct_replace_norm:
  "distinct (normFaces fs) ⟹  distinct (normFaces newFs) ⟹
   set (normFaces fs) ∩ set (normFaces newFs) ⊆ {} ⟹ distinct (normFaces (replace oldF newFs fs))"
apply (induct fs) apply simp
apply simp
apply (case_tac "a = oldF") apply (simp add: normFaces_def) apply blast
apply (simp add: normFaces_def) apply (rule ccontr)
apply (subgoal_tac "normFace a ∈ set(normFaces (replace oldF newFs fs))")
apply (frule normFace_replace_in)
 by (simp add: normFaces_def)+


lemma distinct_replacefacesAt1_norm:
  "i < |Fss| ⟹ i ∈ set is ⟹ distinct is ⟹ distinct (normFaces (Fss!i)) ⟹ distinct (normFaces newFs) ⟹
  set (normFaces (Fss ! i)) ∩ set (normFaces newFs) ⊆ {} ⟹
  distinct (normFaces ((replacefacesAt is oldF newFs Fss)! i))"
proof (induct "is")
  case Nil then show ?case by simp
next
  case (Cons j js)
  then have "j = i ∧ i ∉ set js ∨ i ≠ j ∧ i ∈ set js" by auto
  then show ?case
  proof (elim disjE conjE)
    assume "j = i" "i ∉ set js" with Cons show ?thesis
     by (simp add: replacefacesAt_notin distinct_replace_norm)
  next
    assume "i ∈ set js" "i ≠ j" with Cons show ?thesis
     by (simp add: replacefacesAt_in distinct_replace_norm)
  qed
qed

lemma distinct_replacefacesAt2_norm:
  "i < |Fss| ⟹ i ∉ set is ⟹ distinct is ⟹ distinct (normFaces (Fss!i)) ⟹ distinct (normFaces newFs) ⟹
  set (normFaces (Fss ! i)) ∩ set (normFaces newFs) ⊆ {} ⟹
  distinct (normFaces ((replacefacesAt is oldF newFs Fss)! i))"
proof (induct "is")
  case Nil then show ?case by simp
next
  case (Cons j js)
  then have "i ≠ j" by auto
  with Cons show ?case
    by (simp add: replacefacesAt_notin distinct_replace_norm)
qed

lemma distinct_replacefacesAt_norm:
  "i < |Fss| ⟹ distinct is ⟹ distinct (normFaces (Fss!i)) ⟹ distinct (normFaces newFs) ⟹
  set (normFaces (Fss ! i)) ∩ set (normFaces newFs) ⊆ {} ⟹
  distinct (normFaces ((replacefacesAt is olfF newFs Fss)! i))"
by (cases "i ∈ set is")
   (auto intro: distinct_replacefacesAt1_norm distinct_replacefacesAt2_norm)


lemma normFace_in_cong:
 "vertices f ≠ [] ⟹ minGraphProps g ⟹ normFace f ∈ set (normFaces (faces g))
  ⟹ ∃ f' ∈ set (faces g). f ≅ f'"
apply (simp add: normFace_def normFaces_def)
apply (erule imageE)
apply(rename_tac f')
apply (rule bexI)
 defer apply assumption
apply (simp add: cong_face_def)
 apply (rule congs_trans) apply (rule verticesFrom_congs)
 apply (rule minVertex_in) apply simp
apply (rule congs_sym) apply (simp add: normFace_def)
apply (rule verticesFrom_congs) apply (rule minVertex_in)
apply (subgoal_tac "2 < | vertices f'|") apply force
by (simp add: minGraphProps2)

lemma normFace_neq:
  "a ∈ 𝒱 f ⟹ a ∉ 𝒱 f' ⟹ vertices f' ≠ [] ⟹ normFace f ≠ normFace f'"
apply (simp add: normFace_def)
apply (subgoal_tac "a ∈ set (verticesFrom f (minVertex f))")
 apply (subgoal_tac "a ∉ set (verticesFrom f' (minVertex f'))") apply force
 apply (subgoal_tac "(vertices f') ≅ (verticesFrom f' (minVertex f'))") apply (simp add: congs_pres_nodes)
 apply (rule verticesFrom_congs) apply (rule minVertex_in) apply simp
apply (subgoal_tac "(vertices f) ≅ (verticesFrom f (minVertex f))") apply (simp add: congs_pres_nodes)
apply (rule verticesFrom_congs) apply (rule minVertex_in) by auto

lemma split_face_f12_f21_neq_norm:
  "pre_split_face oldF ram1 ram2 vs ⟹
  2 < |vertices oldF| ⟹ 2 < |vertices f12| ⟹ 2 < |vertices f21| ⟹
  (f12, f21) = split_face oldF ram1 ram2 vs ⟹ normFace f12 ≠ normFace f21"
proof -
  assume split: "(f12, f21) = split_face oldF ram1 ram2 vs"
  "pre_split_face oldF ram1 ram2 vs"
    and minlen: "2 < |vertices oldF|"  "2 < | vertices f12|"  "2 < | vertices f21|"
  from split have dist_f12: "distinct (vertices f12)" by (rule split_face_distinct1)
  from split have dist_f21: "distinct (vertices f21)" by (rule split_face_distinct2)

  from split dist_f12 dist_f21 minlen show ?thesis
    apply (simp add: split_face_def)
    apply (case_tac "between (vertices oldF) ram2 ram1")
     apply (case_tac "between (vertices oldF) ram1 ram2")
      apply simp apply (subgoal_tac "|vertices oldF| = 2")
       apply simp apply (frule verticesFrom_ram1)
      apply (subgoal_tac "distinct (vertices oldF)") apply (drule verticesFrom_length)
        apply (subgoal_tac "ram1 ∈ 𝒱 oldF") apply assumption apply (simp add: pre_split_face_def) apply simp
       apply (simp add: pre_split_face_def)
      apply (rule normFace_neq)
        apply (subgoal_tac "a ∈ 𝒱 (Face (rev vs @ ram1 # between (vertices oldF) ram1 ram2 @ [ram2]) Nonfinal)")
         apply assumption apply simp apply force  apply simp
    apply (rule not_sym)
    apply (rule normFace_neq)
      apply (subgoal_tac "a ∈ 𝒱 (Face (ram2 # between (vertices oldF) ram2 ram1 @ ram1 # vs) Nonfinal)")
       apply assumption apply simp
     apply (frule verticesFrom_ram1)
     apply (subgoal_tac "distinct (verticesFrom oldF ram1)") apply clarsimp
     apply (rule verticesFrom_distinct)
      by (simp add: pre_split_face_def)+
qed


lemma normFace_in: "f ∈ set fs ⟹ normFace f ∈ set (normFaces fs)"
by (simp add: normFaces_def)



subsection‹Invariants of @{const splitFace}›
(********************************** splitFace & minGraphProps *************************************)

lemma splitFace_holds_minGraphProps':
  "pre_splitFace g' v a f' vs ⟹ minGraphProps' g' ⟹
  minGraphProps' (snd (snd (splitFace g' v a f' vs)))"
apply (simp add: minGraphProps'_def)
apply safe
 apply (simp add: splitFace_def split_def)
 apply (case_tac "f ∈ ℱ g'") apply simp
 apply safe
  apply (simp add: split_face_def) apply safe apply simp apply (drule pre_FaceDiv_between1) apply simp
 apply (frule_tac replace1)
  apply simp_all
 apply (simp add: split_face_def) apply safe apply simp
 apply (drule pre_FaceDiv_between2) apply simp
apply (drule splitFace_split)
apply safe
  apply simp
 apply (subgoal_tac "pre_splitFace g' v a f' vs")
  apply (drule splitFace_distinct2)+ apply simp+
apply (subgoal_tac "pre_splitFace g' v a f' vs")
 apply (drule splitFace_distinct1)+
 by simp+


lemma splitFace_holds_faceListAt_len:
  "pre_splitFace g' v a f' vs ⟹ minGraphProps g' ⟹
   faceListAt_len (snd (snd (splitFace g' v a f' vs)))"
by (simp add: minGraphProps_def faceListAt_len_def splitFace_def split_def)


lemma splitFace_new_f12:
assumes pre: "pre_splitFace g ram1 ram2 oldF newVs"
    and props: "minGraphProps g"
    and spl: "(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs"
shows "f12 ∉ ℱ g"
proof (cases newVs)
  case Nil with pre have "(ram2, ram1) ∉ edges g"
    by (unfold pre_splitFace_def) auto
  moreover from Nil pre
  have "(ram2, ram1) ∈ edges f12"
    apply (rule_tac splitFace_empty_ram2_ram1_in_f12)
     apply (auto simp: Nil[symmetric])
    apply (rule spl)
    done
  ultimately show ?thesis by (auto simp add: edges_graph_def)
next
  case (Cons v vs)
  with pre have "v ∉ 𝒱 g"
    by (auto simp: pre_splitFace_def)
  moreover from Cons spl have "v ∈ 𝒱 f12"
    by (simp add: splitFace_f12_new_vertices)
  moreover note props
  ultimately show ?thesis by (auto dest: minGraphProps)
qed

lemma splitFace_new_f12_norm:
assumes pre: "pre_splitFace g ram1 ram2 oldF newVs"
and props: "minGraphProps g"
and spl: "(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs"
shows "normFace f12 ∉ set (normFaces (faces g))"
proof (cases newVs)
  case Nil with pre have "(ram2, ram1) ∉ edges g"
    by (auto simp: pre_splitFace_def)
  moreover
  from pre spl [symmetric] have dist_f12: "distinct (vertices f12)"
    apply (drule_tac splitFace_distinct2) by simp                  
  moreover
  from Nil pre
  have "(ram2, ram1) ∈ edges f12"
    apply (rule_tac splitFace_empty_ram2_ram1_in_f12)
     apply (auto simp: Nil[symmetric])
    apply (rule spl)
    done
  moreover
  with dist_f12 have "vertices f12 ≠ []"
    apply (simp add: is_nextElem_def) apply (case_tac "vertices f12") apply (simp add: is_sublist_def)
    by simp
  ultimately show ?thesis
    apply (auto simp add: edges_graph_def) apply (frule normFace_in_cong)
      apply (rule props)
     apply assumption
    apply (elim bexE)
    apply (subgoal_tac "(ram2, ram1) ∈ edges f'") apply simp
    apply (subgoal_tac "(vertices f12) ≅ (vertices f')")  apply (frule congs_distinct)
     apply (simp add: cong_face_def is_nextElem_congs_eq)+
    done
next
  case (Cons v vs)
  with pre have "v ∉ 𝒱 g" by (auto simp: pre_splitFace_def)
  moreover from Cons spl have "v ∈ 𝒱 f12"
    by (simp add: splitFace_f12_new_vertices)
  moreover note props
  ultimately show ?thesis
    apply auto
    apply (subgoal_tac "(vertices f12) ≠ []")
     apply (frule normFace_in_cong) apply assumption+ apply (erule bexE)
     apply (subgoal_tac "v ∈ 𝒱 f'") apply (simp add: minGraphProps9)
     apply (simp add: congs_pres_nodes cong_face_def) by auto
qed

lemma splitFace_new_f21:
assumes pre: "pre_splitFace g ram1 ram2 oldF newVs"
and props: "minGraphProps g"
and spl: "(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs"
shows "f21 ∉ ℱ g"
proof (cases newVs)
  case Nil with pre have "(ram1, ram2) ∉ edges g"
    by (auto simp: pre_splitFace_def)
  moreover from Nil pre
  have "(ram1, ram2) ∈ edges f21"
    apply (rule_tac splitFace_empty_ram1_ram2_in_f21)
     apply (auto simp: Nil[symmetric])
    apply (rule spl)
    done
  ultimately show ?thesis by (auto simp add: edges_graph_def)
next
  case (Cons v vs)
  with pre have "v ∉ 𝒱 g" by (auto simp: pre_splitFace_def)
  moreover from Cons spl have "v ∈ 𝒱 f21"
    by (simp add: splitFace_f21_new_vertices)
  moreover note props
  ultimately show ?thesis by (auto dest: minGraphProps)
qed

lemma splitFace_new_f21_norm:
assumes pre: "pre_splitFace g ram1 ram2 oldF newVs"
and props: "minGraphProps g"
and spl: "(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs"
shows "normFace f21 ∉ set (normFaces (faces g))"
proof (cases newVs)
  case Nil with pre have "(ram1, ram2) ∉ edges g"
    by (auto simp: pre_splitFace_def)
  moreover
  from pre spl [symmetric] have dist_f21: "distinct (vertices f21)"
    apply (drule_tac splitFace_distinct1) by simp
  moreover
  from Nil pre
  have "(ram1, ram2) ∈ edges f21"
    apply (rule_tac splitFace_empty_ram1_ram2_in_f21)
     apply (auto simp: Nil[symmetric])
    apply (rule spl)
    done
  moreover
  with dist_f21 have "vertices f21 ≠ []"
    apply (simp add: is_nextElem_def) apply (case_tac "vertices f21") apply (simp add: is_sublist_def)
    by simp
  ultimately show ?thesis apply (auto simp add: edges_graph_def) apply (frule normFace_in_cong)
      apply (rule props)
     apply assumption
    apply (elim bexE)
    apply (subgoal_tac "(ram1, ram2) ∈ edges f'") apply simp
    apply (subgoal_tac "(vertices f21) ≅ (vertices f')")  apply (frule congs_distinct)
     apply (simp add: cong_face_def is_nextElem_congs_eq)+
    done
next
  case (Cons v vs)
  with pre have "v ∉ 𝒱 g" by (auto simp: pre_splitFace_def)
  moreover from Cons spl have "v ∈ 𝒱 f21"
    by (simp add: splitFace_f21_new_vertices)
  moreover note props
  ultimately show ?thesis apply auto
    apply (subgoal_tac "(vertices f21) ≠ []")
     apply (frule normFace_in_cong) apply assumption+ apply (erule bexE)
     apply (subgoal_tac "v ∈ 𝒱 f'") apply (simp add: minGraphProps9)
     apply (simp add: congs_pres_nodes cong_face_def) by auto
qed

lemma splitFace_f21_oldF_neq:
 "pre_splitFace g ram1 ram2 oldF newVs ⟹
  minGraphProps g ⟹
 (f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs ⟹
  oldF ≠ f21"
by (frule splitFace_new_f21) (auto)

lemma splitFace_f12_oldF_neq:
 "pre_splitFace g ram1 ram2 oldF newVs ⟹
  minGraphProps g ⟹
 (f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs ⟹
  oldF ≠ f12"
by (frule splitFace_new_f12) (auto)


lemma splitFace_f12_f21_neq_norm:
 "pre_splitFace g ram1 ram2 oldF vs ⟹ minGraphProps g ⟹
 (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs ⟹
  normFace f12 ≠ normFace f21"
apply (subgoal_tac "minGraphProps' newGraph")
 apply (subgoal_tac "f12 ∈ ℱ newGraph ∧ f21 ∈ ℱ newGraph")
  apply (subgoal_tac "pre_split_face oldF ram1 ram2 vs")
   apply (frule split_face_f12_f21_neq_norm) apply (rule minGraphProps2) apply simp apply(erule pre_splitFace_oldF)
      apply (subgoal_tac "2 < | vertices f12 |") apply assumption apply (force simp: minGraphProps'_def)
     apply (subgoal_tac "2 < | vertices f21 |") apply assumption apply (force simp: minGraphProps'_def)
    apply (simp add: splitFace_def split_def)
   apply simp
  apply force
 apply (simp add: splitFace_def split_def)
 apply (rule disjI2)
 apply (erule replace3[OF pre_splitFace_oldF])
 apply simp
apply (frule splitFace_holds_minGraphProps') apply (simp add: minGraphProps_def minGraphProps'_def)
by (simp add: splitFace_def split_def)


lemma set_faces_splitFace:
"⟦ minGraphProps g; f ∈ ℱ g; pre_splitFace g v1 v2 f vs;
  (f1, f2, g') = splitFace g v1 v2 f vs ⟧
  ⟹ ℱ g' = {f1,f2} ∪ (ℱ g - {f})"
apply(frule minGraphProps11')
apply(blast dest:splitFace_new_f21 splitFace_new_f12
                 splitFace_faces_1 splitFace_delete_oldF)
done


declare minGraphProps8 minGraphProps8a minGraphProps8a' [intro]

lemma splitFace_holds_facesAt_distinct:
assumes pre: "pre_splitFace g v w f [countVertices g..<countVertices g + n]"
    and mgp: "minGraphProps g"
shows "facesAt_distinct (snd (snd (splitFace g v w f [countVertices g..<countVertices g + n])))"
proof -
  define ws where "ws = [countVertices g..<countVertices g + n]"
  define f21 where "f21 = snd (split_face f v w ws)"
  with pre ws_def have dist_f21: "distinct (vertices f21)" by (auto intro: split_face_distinct2)
  define f12 where "f12 = fst (split_face f v w ws)"
  with pre ws_def have dist_f12: "distinct (vertices f12)" by (auto intro: split_face_distinct1)
  define vs1 where "vs1 = between (vertices f) v w"
  define vs2 where "vs2 = between (vertices f) w v"
  define g' where "g' = snd (snd (splitFace g v w f [countVertices g..<countVertices g + n]))"
  from f12_def f21_def ws_def g'_def
  have fdg: "(f12, f21, g') = splitFace g v w f [countVertices g..<countVertices g + n]"
    by (simp add: splitFace_def split_def)
  from pre mgp fdg have new_f12: "f12 ∉ ℱ g"
    apply (rule_tac splitFace_new_f12)  by simp_all
  from pre mgp fdg have new_f21: "f21 ∉ ℱ g"
    apply (rule_tac splitFace_new_f21) by simp_all
  from pre mgp fdg have new_f12_norm: "normFace f12 ∉ set (normFaces (faces g))"
    apply (rule_tac splitFace_new_f12_norm)  by simp_all
  from pre mgp fdg have new_f21_norm: "normFace f21 ∉ set (normFaces (faces g))"
    apply (rule_tac splitFace_new_f21_norm) by simp_all


  have "facesAt_distinct g'"
  proof (rule facesAt_distinctI)
    fix x assume x: "x ∈ 𝒱 g'"
    show "distinct (normFaces (facesAt g' x))"
      proof -
      from mgp pre have a: "v < |faceListAt g|" "w < |faceListAt g|"
        apply (unfold pre_splitFace_def)
        apply (simp_all add: minGraphProps4)
        by (auto intro: minGraphProps9')
      then show ?thesis
      proof (cases "x = w")
        case True
        moreover with pre have "v ≠ w"
          by (unfold pre_splitFace_def) simp
        moreover note a x pre mgp
        ultimately show ?thesis
          apply -
          apply (unfold pre_splitFace_def)
          apply (unfold g'_def splitFace_def facesAt_def)
          apply (simp add: split_def nth_append)
          apply (rule distinct_replace_norm)
            apply (rule distinct_replacefacesAt_norm)
                apply simp
               apply (rule between_distinct)
               apply simp
              apply (rule distinct_replacefacesAt_norm)
                  apply assumption
                 apply (rule between_distinct)
                 apply simp
                apply (rule minGraphProps8a') apply assumption+  apply (simp add: minGraphProps4)
               apply (simp add: normFaces_def)

              apply (subgoal_tac "set (faceListAt g ! w) = {f ∈ ℱ g. w ∈ 𝒱 f}") apply simp
               apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f12} = {}")
                apply (simp add: f12_def ws_def normFaces_def) apply blast
               apply (simp add: new_f12_norm)

              apply (frule minGraphProps_facesAt_eq)
               apply (subgoal_tac "w ∈ 𝒱 g") apply assumption
               apply (rule minGraphProps9) apply assumption apply blast apply simp
              apply (simp add: facesAt_def split: if_split_asm)

             apply (simp add: normFaces_def)

            apply (subgoal_tac "w ∉ set (between (vertices f) v w)")
             apply (simp add: replacefacesAt_notin)
             apply (subgoal_tac "set (faceListAt g ! w) = {f ∈ ℱ g. w ∈ 𝒱 f}")
              apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f21} = {}")
               apply (simp add: f21_def ws_def normFaces_def) apply blast
              apply (simp add: new_f21_norm)

             apply (frule minGraphProps_facesAt_eq)
              apply (subgoal_tac "w ∈ 𝒱 g") apply assumption
              apply (rule minGraphProps9) apply assumption apply blast apply simp
             apply (simp add: facesAt_def minGraphProps4 vertices_graph)
            apply (rule between_not_r2) apply simp
        
           apply (simp add: normFaces_def) apply (rule splitFace_f12_f21_neq_norm)
             apply (rule pre) apply simp
           apply (subgoal_tac "(f12, f21, g') = splitFace g v w f [countVertices g..<countVertices g + n]")
            apply (simp add: f12_def f21_def g'_def ws_def)
           apply (rule fdg)

          apply (subgoal_tac "w ∉ set (between (vertices f) w v)")
           apply (simp add: replacefacesAt_notin)
           apply (subgoal_tac "w ∉ set (between (vertices f) v w)")
            apply (simp add: replacefacesAt_notin)
            apply (subgoal_tac "set (faceListAt g ! w) = {f ∈ ℱ g. w ∈ 𝒱 f}")
             apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f12,normFace f21} = {}")
              apply (simp add: f12_def f21_def ws_def normFaces_def) apply blast
             apply (simp add: new_f21_norm new_f12_norm)
            apply (frule minGraphProps_facesAt_eq)
             apply (subgoal_tac "w ∈ 𝒱 g") apply assumption
             apply (rule minGraphProps9) apply assumption apply blast apply simp
            apply (simp add: facesAt_def minGraphProps4 vertices_graph)
           apply (rule between_not_r2) apply simp
          apply (rule between_not_r1) by simp
      next
        from pre have vw_neq: "v ≠ w"
          by (unfold pre_splitFace_def) simp
        case False then show ?thesis
          proof (cases "x = v")
            case True
              with a x pre mgp vw_neq
              show ?thesis
                apply -
                apply (unfold pre_splitFace_def)
                apply (unfold g'_def splitFace_def facesAt_def)
                apply (simp add: split_def nth_append)
                apply (rule distinct_replace_norm)
                  apply (rule distinct_replacefacesAt_norm)
                      apply simp
                     apply (rule between_distinct)
                     apply simp
                    apply (rule distinct_replacefacesAt_norm)
                        apply assumption
                       apply (rule between_distinct)
                       apply simp
                      apply (rule minGraphProps8a) apply assumption+ apply (simp add: minGraphProps4 vertices_graph)

                     apply (simp add:normFaces_def)

                    apply (subgoal_tac "set (faceListAt g ! v) = {f ∈ ℱ g. v ∈ 𝒱 f}")
                     apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f12} = {}")
                      apply (simp add: f12_def ws_def normFaces_def) apply blast
                     apply (simp add: new_f12_norm)

                    apply (frule minGraphProps_facesAt_eq)
                     apply (subgoal_tac "v ∈ 𝒱 g") apply assumption
                     apply (rule minGraphProps9) apply assumption apply blast apply simp
                    apply (simp add: facesAt_def split: if_split_asm)

                   apply (simp add: normFaces_def)

                  apply (subgoal_tac "v ∉ set (between (vertices f) v w)")
                   apply (simp add: replacefacesAt_notin)
                   apply (subgoal_tac "set (faceListAt g ! v) = {f ∈ ℱ g. v ∈ 𝒱 f}")
                    apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f21} = {}")
                     apply (simp add: f21_def ws_def normFaces_def) apply blast
                    apply (simp add: new_f21_norm)

                   apply (frule minGraphProps_facesAt_eq)
                    apply (subgoal_tac "v ∈ 𝒱 g") apply assumption
                    apply (rule minGraphProps9) apply assumption apply blast apply simp
                   apply (simp add: facesAt_def split: if_split_asm)
                  apply (rule between_not_r1) apply simp
                 apply (simp add: normFaces_def) apply (rule not_sym)
                 apply (rule splitFace_f12_f21_neq_norm) apply (rule pre) apply simp
                 apply (subgoal_tac "(f12, f21, g') = splitFace g v w f [countVertices g..<countVertices g + n]")
                  apply (simp add: f12_def f21_def ws_def g'_def)  apply (rule fdg)

                apply (subgoal_tac "v ∉ set (between (vertices f) w v)")
                 apply (simp add: replacefacesAt_notin)
                 apply (subgoal_tac "v ∉ set (between (vertices f) v w)")
                  apply (simp add: replacefacesAt_notin)
                  apply (subgoal_tac "set (faceListAt g ! v) = {f ∈ ℱ g. v ∈ 𝒱 f}")
                   apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f21,normFace f12} = {}")
                    apply (simp add: f12_def f21_def ws_def normFaces_def) apply blast
                   apply (simp add: new_f21_norm new_f12_norm)
                  apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f21} = {}")
                   apply (simp add: new_f21_norm)
                   apply (frule minGraphProps_facesAt_eq)
                    apply (subgoal_tac "v ∈ 𝒱 g") apply assumption
                    apply (rule minGraphProps9) apply assumption apply blast apply simp
                   apply (simp add: facesAt_def minGraphProps4 vertices_graph)
                  apply (simp add: new_f21_norm)
                 apply (rule between_not_r1) apply simp
                apply (rule between_not_r2) by simp
              next
                assume xw_neq: "x ≠ w"
                case False
                with a x pre mgp vw_neq xw_neq
                show ?thesis
                  apply -
                  apply (unfold pre_splitFace_def g'_def splitFace_def facesAt_def)
                  apply (simp add: split_def nth_append)
                  apply (case_tac "x < |faceListAt g|")
                   apply simp
                   apply (subgoal_tac "x ∈ 𝒱 g")
                    apply (rule distinct_replacefacesAt_norm)
                        apply simp
                       apply (rule between_distinct)
                       apply simp
                      apply (rule distinct_replacefacesAt_norm) apply assumption
                         apply (rule between_distinct)
                         apply simp
                        apply (rule minGraphProps8a) apply assumption apply (simp add: minGraphProps4)

                       apply (simp add: normFaces_def)

                      apply (subgoal_tac "set (faceListAt g ! x) = {f ∈ ℱ g. x ∈ 𝒱 f}")
                       apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f12} = {}")
                        apply (simp add: f12_def ws_def normFaces_def) apply blast
                       apply (simp add: new_f12_norm)

                      apply (frule minGraphProps_facesAt_eq) apply assumption
                      apply (simp add: facesAt_def split: if_split_asm)
                     apply (simp add: normFaces_def)

                    apply (case_tac "x ∉ set (between (vertices f) v w)")
                     apply (simp add: replacefacesAt_notin)
                     apply (subgoal_tac "set (faceListAt g ! x) = {f ∈ ℱ g. x ∈ 𝒱 f}")
                      apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f21} = {}")
                       apply (simp add: f21_def ws_def normFaces_def) apply blast
                      apply (simp add: new_f21_norm)

                     apply (frule minGraphProps_facesAt_eq) apply assumption
                     apply (simp add: facesAt_def split: if_split_asm)
                    apply (simp add: normFaces_def)
                    apply (drule replacefacesAt_nth) apply assumption
                        apply (subgoal_tac "f ∉ set [fst (split_face f v w [countVertices g..<countVertices g + n])]")
                         apply assumption apply simp
                        apply (rule splitFace_f12_oldF_neq)
                          apply (subgoal_tac "pre_splitFace g v w f [countVertices g..<countVertices g + n]")
                           apply assumption apply (simp add: pre) apply assumption+
                        apply (simp add: splitFace_def split_def)
                       apply (rule normFaces_distinct)
                       apply (rule minGraphProps8a) apply assumption apply (simp add: minGraphProps4 vertices_graph)
                      apply (simp add: normFaces_def)
                     apply (rule impI) apply simp
                     apply (subgoal_tac "set (faceListAt g ! x) = {f ∈ ℱ g. x ∈ 𝒱 f}")
                      apply (subgoal_tac "ℱ g ∩ {f12} = {}")
                       apply (simp add: f12_def ws_def)
                      apply (simp add: new_f12)
                     apply (frule minGraphProps_facesAt_eq)
                      apply (subgoal_tac "x ∈ 𝒱 g") apply assumption
                      apply (simp add: minGraphProps4 vertices_graph)
                     apply (simp add:facesAt_def minGraphProps4 vertices_graph)
                    apply (frule replacefacesAt_nth) apply assumption

                        apply (subgoal_tac "f ∉ set [fst (split_face f v w [countVertices g..<countVertices g + n])]")
                         apply assumption apply simp apply (rule splitFace_f12_oldF_neq)
                          apply (subgoal_tac "pre_splitFace g v w f [countVertices g..<countVertices g + n]") apply assumption
                          apply (simp add: pre) apply assumption apply (simp add: splitFace_def split_def)
                       apply (rule normFaces_distinct)
                       apply (rule minGraphProps8a') apply assumption apply (simp add: minGraphProps4)
                      apply simp
                     apply (rule impI) apply simp
                     apply (subgoal_tac "set (faceListAt g ! x) = {f ∈ ℱ g. x ∈ 𝒱 f}")
                      apply (subgoal_tac "ℱ g ∩ {f12} = {}")
                       apply (simp add: f12_def ws_def)
                      apply (simp add: new_f12)
                     apply (frule minGraphProps_facesAt_eq)
                      apply (subgoal_tac "x ∈ 𝒱 g") apply assumption
                      apply (simp add: minGraphProps4 vertices_graph)
                     apply (simp add:facesAt_def minGraphProps4 vertices_graph)
                    apply (simp add: f12_def [symmetric] f21_def [symmetric] ws_def [symmetric])
                    apply (subgoal_tac "normFace f21 ∉ set (normFaces (replace f [f12] (faceListAt g ! x)))")
                     apply (simp add: normFaces_def)
                    apply (rule ccontr) apply simp
                    apply (frule normFace_replace_in)
                    apply (subgoal_tac "normFace f12 ≠ normFace f21")
                     apply (subgoal_tac "normFace f21 ∉ set (normFaces (faceListAt g ! x))")
                      apply (simp add: normFaces_def)
                     apply (rule ccontr) apply simp
                     apply (subgoal_tac "normFace f21 ∉ set (normFaces (facesAt g x))")
                      apply (simp add: facesAt_def)(*
                      apply (subgoal_tac "x ∈ 𝒱 g") apply (simp add: normFaces_def)
                      apply (simp add: minGraphProps4 vertices_graph)*)
                     apply (subgoal_tac "normFace f21 ∉ set (normFaces (faces g))") apply (frule minGraphProps_facesAt_eq)
                       apply (subgoal_tac "x ∈ 𝒱 g") apply assumption apply (simp add: minGraphProps4 vertices_graph)
                      apply (simp add: normFaces_def) apply (rule ccontr)  apply simp
                      apply blast
                     apply (rule new_f21_norm)
                    apply (rule splitFace_f12_f21_neq_norm) apply (rule pre) apply simp apply (rule fdg)
                   apply (simp add: minGraphProps4 vertices_graph)

(* zweite große Implikation *)
                  apply (simp add: normFaces_def)
                  apply (subgoal_tac "(x - |faceListAt g | ) < n") apply simp
                   apply (rule splitFace_f12_f21_neq_norm) apply (rule pre) apply simp
                   apply (simp add: f12_def [symmetric] f21_def [symmetric]  ws_def [symmetric]) apply (simp add: ws_def) apply (rule fdg)
                by (simp add: minGraphProps4)
              qed
            qed
          qed
        qed
  then show ?thesis by (simp add: g'_def)
qed


lemma splitFace_holds_facesAt_eq:
assumes pre_F: "pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n]"
and mgp: "minGraphProps g'"
and g'': "g'' = (snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))"
shows "facesAt_eq g''"
proof -
  have "[0..<countVertices g''] = [0..<countVertices g' + n]"
    apply (simp add: g'') by (simp add: splitFace_def split_def)
  hence vg'': "vertices g'' = [0..<countVertices g' + n]" by (simp add:vertices_graph)

  define ws where "ws = [countVertices g'..<countVertices g' + n]"
  define f21 where "f21 = snd (split_face f' v a ws)"
  define f12 where "f12 = fst (split_face f' v a ws)"
  define vs1 where "vs1 = between (vertices f') v a"
  define vs2 where "vs2 = between (vertices f') a v"
  from ws_def [symmetric] f21_def [symmetric] f12_def [symmetric] g'' have fdg: "(f12, f21, g'') = splitFace g' v a f' ws"
    by (simp add: splitFace_def split_def)
  from pre_F have pre_F': "pre_splitFace g' v a f' ws" apply (unfold pre_splitFace_def ws_def) by force

  from pre_F' mgp fdg have f'_f21: "f' ≠ f21" apply (rule_tac splitFace_f21_oldF_neq) apply assumption by simp+
  from pre_F' mgp fdg have f'_f12: "f' ≠ f12" apply (rule_tac splitFace_f12_oldF_neq) apply assumption by simp+

  from f12_def vs1_def have vert_f12: "vertices f12 = rev ws @ v # vs1 @ [a]" by (simp add: split_face_def)
  from f21_def vs2_def have vert_f21: "vertices f21 = a # vs2 @ v # ws" by (simp add: split_face_def)
  from vs1_def vs2_def pre_F have vertFrom_f': "verticesFrom f' v =
    v # vs1 @ a # vs2" apply simp
    apply (rule_tac verticesFrom_ram1) by (rule pre_splitFace_pre_split_face)
  from vs1_def vs2_def pre_F vertFrom_f' have vert_f': "𝒱 f' =  set vs1 ∪ set vs2 ∪ {a,v}"
    apply (subgoal_tac "(vertices f') ≅ (verticesFrom f' v)") apply (drule congs_pres_nodes)
    apply (simp add: congs_pres_nodes) apply blast
    apply (rule verticesFrom_congs) by (simp only: pre_splitFace_def)
  from pre_F have dist_vertFrom_f': "distinct (verticesFrom f' v)" apply (rule_tac verticesFrom_distinct)
    by (simp only: pre_splitFace_def)+
  then have vs1_vs2_empty: "set vs1 ∩ set vs2 = {}" by (simp add: vertFrom_f')

  from ws_def f21_def f12_def have "faces g'' = (replace f' [f21]  (faces g')) @ [f12]"
    apply (simp add: g'') by (simp add: splitFace_def split_def)

  from mgp have dist_all: "⋀x. x ∈ 𝒱 g' ⟹ distinct (faceListAt g' ! x)"
    apply (rule_tac normFaces_distinct)
    by (simp add: minGraphProps_def facesAt_distinct_def facesAt_def)

  from mgp have fla: "|faceListAt g'| = countVertices g'"
    by (simp add: minGraphProps_def faceListAt_len_def)

  from ws_def [symmetric] f21_def [symmetric] f12_def [symmetric]
    vs1_def [symmetric] vs2_def [symmetric] pre_F mgp vert_f'
show ?thesis
apply (simp add: g'')
apply (unfold splitFace_def facesAt_eq_def facesAt_def)
apply (rule ballI)
apply (simp only: split_def Let_def)
apply (simp only: snd_conv)
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp only: faceListAt.simps vertices_graph.simps split:if_split_asm)
 apply (case_tac "v < |faceListAt g'| ∧ a < | faceListAt g'|")
  apply (simp only: nth_append split: if_split_asm)
   apply (case_tac "va < | faceListAt g' |")
    apply (subgoal_tac "va ∈ 𝒱 g'")
     apply (subgoal_tac "distinct vs1 ∧ distinct vs2 ∧
       v ∉ set vs1 ∧ v ∉ set vs2 ∧ a ∉ set vs1 ∧ a ∉ set vs2 ∧ a ≠ v ∧ v ≠ a ∧ set vs1 ∩ set vs2 = {}" )
      apply (case_tac "a = va")
       apply (simp add:replacefacesAt_nth2 replacefacesAt_notin)
       apply (subgoal_tac "distinct (faceListAt g' ! va)")
        apply (subgoal_tac "distinct (faces g')")
         apply (simp add: replace6)
         apply (case_tac "x = f12") apply (simp add: vert_f12) apply simp
         apply (case_tac "x = f'") apply (simp add: vert_f21) apply(simp)
         apply (case_tac "x = f21") apply (simp add: vert_f21) apply (simp)
         apply (rule conjI)
          apply (rule minGraphProps5) apply assumption apply assumption apply (fastforce simp: facesAt_def)
         apply (rule minGraphProps6) apply assumption apply assumption apply (simp add: facesAt_def)
        apply (rule minGraphProps11') apply simp
       apply (subgoal_tac "distinct (facesAt g' va)") apply (simp add: facesAt_def)
       apply (rule normFaces_distinct) apply (rule minGraphProps8) apply simp apply simp apply simp
      apply (case_tac "v = va")
       apply (simp add:replacefacesAt_nth2 replacefacesAt_notin)
       apply (subgoal_tac "distinct (faceListAt g' ! va)")
        apply (subgoal_tac "distinct (faces g')")
         apply (simp add: replace6)
         apply (case_tac "x = f12") apply (simp add: vert_f12) apply simp
         apply (case_tac "x = f'") apply (simp add: vert_f21) apply simp
         apply (case_tac "x = f21") apply (simp add: vert_f21) apply simp
         apply (rule conjI)
          apply (rule minGraphProps5) apply assumption apply assumption apply (fastforce simp: facesAt_def)
         apply (rule minGraphProps6) apply assumption apply assumption apply(fastforce simp: facesAt_def)
        apply (rule minGraphProps11') apply simp
       apply (subgoal_tac "distinct (facesAt g' va)") apply (simp add: facesAt_def)
       apply (rule normFaces_distinct) apply (rule minGraphProps8) apply simp apply simp apply simp
      apply (case_tac "va ∈ set vs1")
       apply (subgoal_tac "va ∉ set vs2")
        apply (simp add:replacefacesAt_nth2 replacefacesAt_notin replacefacesAt_in)
        apply (subgoal_tac "distinct (faceListAt g' ! va)")
         apply (subgoal_tac "distinct (faces g')")
          apply (simp add: replace6)
          apply (case_tac "x = f12") apply (simp add: vert_f12) apply simp
          apply (case_tac "x = f'") apply (simp add: vert_f21) apply simp
          apply (rule conjI)
           apply (rule disjI2)
           apply (rule minGraphProps5) apply assumption apply assumption apply (fastforce simp: facesAt_def)
          apply (rule minGraphProps6) apply assumption apply assumption apply (fastforce simp: facesAt_def)
         apply (rule minGraphProps11') apply simp
        apply (subgoal_tac "distinct (facesAt g' va)") apply (simp add: facesAt_def)
        apply (rule normFaces_distinct) apply (rule minGraphProps8) apply assumption apply assumption
       apply blast
      apply (case_tac "va ∈ set vs2")
       apply (simp add:replacefacesAt_nth2 replacefacesAt_notin replacefacesAt_in)
       apply (subgoal_tac "distinct (faceListAt g' ! va)")
        apply (subgoal_tac "distinct (faces g')")
         apply (simp add: replace6)
         apply (case_tac "x = f21") apply (simp add: vert_f21) apply simp
         apply (case_tac "x = f'") apply (simp add: vert_f21) apply simp
         apply (rule conjI)
          apply (rule disjI2)
          apply (rule minGraphProps5) apply assumption apply assumption apply (fastforce simp: facesAt_def)
         apply (rule minGraphProps6) apply assumption apply assumption apply (fastforce simp: facesAt_def)
        apply (rule minGraphProps11') apply simp
       apply (subgoal_tac "distinct (facesAt g' va)") apply (simp add: facesAt_def)
       apply (rule normFaces_distinct) apply (rule minGraphProps8) apply assumption apply assumption
    (* case else *)
      apply (simp add:replacefacesAt_nth2 replacefacesAt_notin replacefacesAt_in)
      apply (subgoal_tac "distinct (faceListAt g' ! va)")
       apply (subgoal_tac "distinct (faces g')")
        apply (simp add: replace6)
        apply (case_tac "x = f'")
         apply (subgoal_tac "va ∈ 𝒱 f'") apply simp
         apply (rule minGraphProps6) apply simp apply (simp add: fla)
         apply (simp add: facesAt_def)
        apply simp
        apply (rule conjI)
         apply (rule disjI2) apply (rule disjI2)
         apply (rule minGraphProps5) apply assumption apply assumption apply (fastforce simp: facesAt_def)
        apply (rule minGraphProps6) apply assumption apply assumption apply(fastforce simp: facesAt_def)
       apply (rule minGraphProps11') apply assumption
      apply (subgoal_tac "distinct (facesAt g' va)") apply (simp add: facesAt_def)
      apply (rule normFaces_distinct) apply (rule minGraphProps8) apply assumption apply assumption apply simp
     apply (subgoal_tac "distinct (vertices f12) ∧ distinct (vertices f21)")
      apply (simp add: vert_f12 vert_f21)
      apply (rule vs1_vs2_empty)
     apply (subgoal_tac "pre_split_face f' v a ws")
      apply (simp add: f12_def f21_def split_face_distinct1' split_face_distinct2')
     apply simp
    apply (simp add: vertices_graph fla)
    (* va in ws *)
   apply simp
  apply (subgoal_tac "distinct (faces g')")
   apply (simp add: replace6)
   apply (thin_tac "[countVertices g'..<countVertices g' + n] = ws")
   apply (subgoal_tac "(va - |faceListAt g'| ) < | ws |") apply simp apply (rule conjI) apply blast
    apply (subgoal_tac "va ∈ set ws")
     apply (case_tac "x = f12") apply (simp add: vert_f12) apply (simp add: vert_f21)
    apply (simp add: ws_def fla)
   apply (simp add: ws_def fla)
  apply (rule minGraphProps11') apply assumption
 apply (subgoal_tac "v ∈ 𝒱 g' ∧ a ∈ 𝒱 g'")
  apply (simp only: fla in_vertices_graph)
 apply (subgoal_tac "f' ∈ ℱ g'")
  apply (subgoal_tac "v ∈ 𝒱 f' ∧ a ∈ 𝒱 f'") apply (simp only: minGraphProps9) apply force
  apply (subgoal_tac "pre_split_face f' v a ws") apply (simp only: pre_split_face_def) apply force
  apply (rule pre_splitFace_pre_split_face) apply assumption
 apply (simp only: pre_splitFace_def)

(* Rückrichtung *)
apply (rule subsetI)
apply (case_tac "v < |faceListAt g'| ∧ a < | faceListAt g'|")
 apply (case_tac "va < | faceListAt g' |")
  apply (subgoal_tac "va ∈ 𝒱 g'")
   apply (subgoal_tac "distinct vs1 ∧ distinct vs2 ∧
       v ∉ set vs1 ∧ v ∉ set vs2 ∧ a ∉ set vs1 ∧ a ∉ set vs2 ∧ a ≠ v ∧ v ≠ a ∧ set vs1 ∩ set vs2 = {}" )
    apply (simp del: replacefacesAt_simps add: nth_append)
    apply (case_tac "a = va")
     apply (simp add:replacefacesAt_nth2 replacefacesAt_notin)
     apply (subgoal_tac "distinct (faceListAt g' ! va)")
      apply (subgoal_tac "distinct (faces g')")
       apply (simp add: replace6)
       apply (case_tac "x = f12") apply simp apply (rule disjI1) apply (rule minGraphProps7') apply simp  apply simp apply simp
       apply (case_tac "x = f21") apply simp apply (rule disjI1) apply (rule minGraphProps7') apply simp  apply simp apply simp
       apply simp apply (rule minGraphProps7') apply simp apply simp apply  simp
      apply (rule minGraphProps11') apply simp
     apply (rule normFaces_distinct) apply (rule minGraphProps8a) apply simp apply assumption
    apply simp
    apply (case_tac "v = va")
     apply (simp add:replacefacesAt_nth2 replacefacesAt_notin)
     apply (subgoal_tac "distinct (faceListAt g' ! va)")
      apply (subgoal_tac "distinct (faces g')")
       apply (simp add: replace6)
       apply (case_tac "x = f12") apply simp apply (rule disjI1) apply (rule minGraphProps7') apply simp  apply simp apply simp
       apply (case_tac "x = f21") apply simp apply (rule disjI1) apply (rule minGraphProps7') apply simp  apply simp apply simp
       apply simp apply (rule minGraphProps7') apply simp apply simp apply  simp
      apply (rule minGraphProps11') apply simp apply (rule normFaces_distinct)      apply (rule minGraphProps8a) apply simp apply simp     apply (case_tac "va ∈ set vs1")
     apply (subgoal_tac "va ∉ set vs2")
      apply (simp add:replacefacesAt_nth2 replacefacesAt_notin replacefacesAt_in)
      apply (subgoal_tac "distinct (faceListAt g' ! va)")
       apply (subgoal_tac "distinct (faces g')")
        apply (simp add: replace6)
        apply (case_tac "x = f12") apply simp apply (rule disjI1) apply (rule minGraphProps7') apply simp  apply simp apply simp
        apply (case_tac "x = f'")
         apply (subgoal_tac "f' ≠ f21") apply simp apply (rule splitFace_f21_oldF_neq)
           apply (rule pre_F')
          apply simp
         apply (rule fdg)
        apply (case_tac "x = f21") apply (simp add: vert_f21 fla) apply (thin_tac "[countVertices g'..<countVertices g' + n] = ws")
         apply (simp add: ws_def)
        apply simp apply (rule minGraphProps7') apply simp  apply simp apply simp
       apply (rule minGraphProps11') apply simp
      apply (rule normFaces_distinct) apply (rule minGraphProps8a) apply simp apply simp
     apply blast
    apply (case_tac "va ∈ set vs2")
     apply (simp add:replacefacesAt_nth2 replacefacesAt_notin replacefacesAt_in)
     apply (subgoal_tac "distinct (faceListAt g' ! va)")
      apply (subgoal_tac "distinct (faces g')")
       apply (simp add: replace6)
       apply (case_tac "x = f21") apply simp apply (rule disjI1) apply (rule minGraphProps7') apply simp  apply simp apply simp
       apply (case_tac "x = f'")
        apply (subgoal_tac "f' ≠ f12") apply simp apply (rule splitFace_f12_oldF_neq)
          apply (rule pre_F') apply simp  apply (rule fdg)
       apply (case_tac "x = f12") apply (simp add: vert_f12 fla) apply (thin_tac "[countVertices g'..<countVertices g' + n] = ws")
        apply (simp add: ws_def)
       apply simp apply (rule minGraphProps7') apply simp  apply simp apply simp
      apply (rule minGraphProps11') apply simp apply (rule normFaces_distinct) apply (rule minGraphProps8a) apply simp apply simp
    apply (simp add:replacefacesAt_nth2 replacefacesAt_notin replacefacesAt_in)
    apply (subgoal_tac "distinct (faces g')")
     apply (simp add: replace6)
     apply (rule minGraphProps7') apply simp
      apply (case_tac "x = f21") apply (simp add: vert_f21) apply (thin_tac "[countVertices g'..<countVertices g' + n] = ws")
       apply (simp add: ws_def vertices_graph)
      apply (case_tac "x = f12") apply (simp add: vert_f12) apply (thin_tac "[countVertices g'..<countVertices g' + n] = ws")
       apply (simp add: ws_def vertices_graph)
      apply simp
     apply simp
    apply (rule minGraphProps11') apply simp
   apply (subgoal_tac "distinct (vertices f12) ∧ distinct (vertices f21)")
    apply (simp add: vert_f12 vert_f21)
    apply (rule vs1_vs2_empty)
   apply (subgoal_tac "pre_split_face f' v a ws")
    apply (simp add: f12_def f21_def split_face_distinct1' split_face_distinct2')
   apply (simp add: pre_splitFace_pre_split_face[OF pre_F'])
  apply (simp add: vertices_graph fla)
 apply (simp add: nth_append del:replacefacesAt_simps)
 apply (subgoal_tac "distinct (faces g')")
  apply (simp add: replace6)
  apply (thin_tac "[countVertices g'..<countVertices g' + n] = ws")
  apply (subgoal_tac "(va - |faceListAt g'| ) < |ws|") apply simp
   apply (rule ccontr) apply simp
   apply (case_tac "x = f'") apply simp apply simp
   apply (subgoal_tac "va ∈ 𝒱 g'") apply (simp add: fla vertices_graph)
   apply (rule minGraphProps9) apply simp apply force
   apply (simp add: fla) apply (metis minGraphProps9')
  apply (simp add: ws_def fla)
 apply (rule minGraphProps11') apply simp
apply (subgoal_tac "v ∈ 𝒱 g' ∧ a ∈ 𝒱 g'")
 apply (simp only: fla in_vertices_graph)
apply (subgoal_tac "f' ∈ ℱ g'")
 apply (subgoal_tac "v ∈ 𝒱 f' ∧ a ∈ 𝒱 f'") apply (simp only: minGraphProps9) apply force
by force
qed

lemma splitFace_holds_faces_subset:
assumes pre_F: "pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n]"
and mgp: "minGraphProps g'"
shows "faces_subset (snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))"
proof -
  define g'' where "g'' = (snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))"
  define ws where "ws = [countVertices g'..<countVertices g' + n]"
  define f21 where "f21 = snd (split_face f' v a ws)"
  define f12 where "f12 = fst (split_face f' v a ws)"
  define vs1 where "vs1 = between (vertices f') v a"
  define vs2 where "vs2 = between (vertices f') a v"
  from ws_def [symmetric] f21_def [symmetric] f12_def [symmetric] g''_def
    have fdg: "(f12, f21, g'') = splitFace g' v a f' ws"
      by (simp add: splitFace_def split_def)
  from pre_F have pre_F': "pre_splitFace g' v a f' ws" apply (unfold pre_splitFace_def ws_def) by force

  from f12_def vs1_def have vert_f12: "vertices f12 = rev ws @ v # vs1 @ [a]" by (simp add: split_face_def)
  from f21_def vs2_def have vert_f21: "vertices f21 = a # vs2 @ v # ws" by (simp add: split_face_def)
  from vs1_def vs2_def pre_F have vertFrom_f': "verticesFrom f' v =
    v # vs1 @ a # vs2" apply simp
    apply (rule_tac verticesFrom_ram1) by (rule pre_splitFace_pre_split_face)
  from vs1_def vs2_def pre_F vertFrom_f' have vert_f': "𝒱 f' =  set vs1 ∪ set vs2 ∪ {a,v}"
    apply (subgoal_tac "(vertices f') ≅ (verticesFrom f' v)") apply (drule congs_pres_nodes)
    apply (simp add: congs_pres_nodes) apply blast
    apply (rule verticesFrom_congs) by (simp only: pre_splitFace_def)

  from ws_def f21_def f12_def have faces:"faces g'' = (replace f' [f21]  (faces g')) @ [f12]"
    apply (simp add: g''_def) by (simp add: splitFace_def split_def)

  from ws_def have vertices:"vertices g'' = vertices g' @ ws" by (simp add: g''_def)

  from ws_def [symmetric] f21_def [symmetric] f12_def [symmetric]
    vs1_def [symmetric] vs2_def [symmetric] pre_F mgp  g''_def [symmetric] show ?thesis
    apply (simp add: faces_subset_def) apply (rule ballI)  apply (simp add: faces vertices)
    apply (subgoal_tac "𝒱 f' ⊆ 𝒱 g'")
    apply (case_tac "f = f12") apply (simp add: vert_f12 vert_f') apply force
    apply simp apply (drule replace5)
    apply (case_tac "f = f21") apply (simp add: vert_f21 vert_f') apply force
    apply simp apply (rule subsetI) apply (frule minGraphProps9) apply assumption+ apply simp
    apply (rule subsetI) apply (rule minGraphProps9) by auto
qed


lemma splitFace_holds_edges_sym:
assumes pre_F: "pre_splitFace g' v a f' ws"
and mgp: "minGraphProps g'"
shows "edges_sym (snd (snd (splitFace g' v a f' ws)))"
proof -
  define g'' where "g'' = (snd (snd (splitFace g' v a f' ws)))"
  define f21 where "f21 = snd (split_face f' v a ws)"
  define f12 where "f12 = fst (split_face f' v a ws)"
  define vs1 where "vs1 = between (vertices f') v a"
  define vs2 where "vs2 = between (vertices f') a v"
  from f21_def [symmetric] f12_def [symmetric] g''_def
    have fdg: "(f12, f21, g'') = splitFace g' v a f' ws"
      by (simp add: splitFace_def split_def)
  from pre_F have pre_F': "pre_splitFace g' v a f' ws" apply (unfold pre_splitFace_def) by force

  from f21_def f12_def have faces:"faces g'' = (replace f' [f21]  (faces g')) @ [f12]"
    apply (simp add: g''_def) by (simp add: splitFace_def split_def)

  from f12_def f21_def have split: "(f12, f21) = split_face f' v a ws" by simp

  from pre_F mgp  g''_def [symmetric] split show ?thesis
    apply (simp add: edges_sym_def edges_graph_def f21_def [symmetric] f12_def [symmetric]
    vs1_def [symmetric] vs2_def [symmetric])
    apply (intro allI impI) apply (elim bexE) apply (simp add: faces)
    apply (case_tac "x = f12 ∨ x = f21")
     apply (subgoal_tac "(aa,b) ∈ edges f'  ∨ ((b,aa) ∈ (edges f12 ∪ edges f21) ∧ (aa,b) ∈ (edges f12 ∪ edges f21))") apply simp
      apply (case_tac "(aa, b) ∈ edges f'")
       apply (subgoal_tac "(b,aa) ∈ edges g'")
        apply (simp add: edges_graph_def) apply (elim bexE) apply (rule disjI2) apply (rule bexI)
         apply simp
        apply (subgoal_tac "xa ≠ f'") apply (rule replace4) apply simp apply force
        apply (drule minGraphProps12) apply simp apply simp
        apply (rule ccontr) apply simp
       apply (rule minGraphProps10) apply simp apply (simp add: edges_graph_def)
       apply (rule bexI)  apply (thin_tac "(aa, b) ∈ edges x") apply simp
       apply simp
      apply simp
      apply (case_tac "(b, aa) ∈ edges f12") apply simp apply simp
      apply (case_tac "(b, aa) ∈ edges f21") apply (rule bexI)
        apply simp
       apply (rule replace3) apply simp
       apply simp
      apply simp
     apply (subgoal_tac "
     ((aa,b) ∈ edges f'  ∨ ((b,aa) ∈ (edges f12 ∪ edges f21) ∧ (aa,b) ∈ (edges f12 ∪ edges f21))) = ((aa,b) ∈ edges f12 ∨ (aa,b) ∈ edges f21)") apply force
     apply (rule sym) apply simp
     apply (rule split_face_edges_f12_f21_sym) apply (erule pre_splitFace_oldF)
      apply (subgoal_tac "pre_split_face f' v a ws") apply assumption  apply simp
     apply (rule split)
    apply simp
    apply (subgoal_tac "distinct (faces g')") apply (simp add: replace6)
     apply (case_tac "x = f'") apply simp apply simp
     apply (subgoal_tac "(b,aa) ∈ edges g'")
      apply (simp add: edges_graph_def) apply (elim bexE)
      apply (case_tac "xa = f'")
       apply simp apply (frule split_face_edges_or) apply simp apply simp
       apply (case_tac "(b, aa) ∈ edges f12") apply simp apply simp
       apply (rule bexI) apply (thin_tac "(b, aa) ∈ edges f'")
        apply simp
       apply (rule replace3) apply simp apply simp
      apply (rule disjI2) apply (rule bexI) apply simp
      apply (rule replace4) apply simp
      apply force
     apply (rule minGraphProps10) apply simp
     apply (simp add: edges_graph_def)
     apply (rule bexI)  apply simp apply simp
    apply (rule minGraphProps11') by simp
qed


lemma splitFace_holds_faces_distinct:
assumes pre_F: "pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n]"
and mgp: "minGraphProps g'"
shows "faces_distinct (snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))"
proof -
  define g'' where "g'' = snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n]))"
  define ws where "ws ≡ [countVertices g'..<countVertices g' + n]"
  define f21 where "f21 = snd (split_face f' v a ws)"
  define f12 where "f12 = fst (split_face f' v a ws)"
  define vs1 where "vs1 = between (vertices f') v a"
  define vs2 where "vs2 = between (vertices f') a v"
  from ws_def [symmetric] f21_def [symmetric] f12_def [symmetric] g''_def
  have fdg: "(f12, f21, g'') = splitFace g' v a f' ws"
    by (simp add: splitFace_def split_def)
  from pre_F have pre_F': "pre_splitFace g' v a f' ws" apply (unfold pre_splitFace_def ws_def) by force

  from ws_def f21_def f12_def have faces:"faces g'' = (replace f' [f21]  (faces g')) @ [f12]"
    apply (simp add: g''_def) by (simp add: splitFace_def split_def)
  from f12_def f21_def have split: "(f12, f21) = split_face f' v a ws" by simp

  from ws_def [symmetric] pre_F mgp  g''_def [symmetric] split show ?thesis
    apply (simp add: faces_distinct_def faces)
    apply (subgoal_tac "distinct (normFaces (replace f' [f21] (faces g')))")
     apply (simp add: normFaces_def)
     apply safe
     apply (subgoal_tac "distinct (faces g')") apply (simp add: replace6)
      apply (case_tac "x = f'") apply simp
       apply (subgoal_tac "f' ≠ f21") apply simp
       apply (rule splitFace_f21_oldF_neq)
         apply (rule pre_F') apply simp
       apply (rule fdg)
      apply simp
      apply (case_tac "x = f21") apply simp
       apply (subgoal_tac "normFace f12 ≠ normFace f21") apply simp
       apply (rule splitFace_f12_f21_neq_norm) apply force apply simp
       apply (simp add: fdg) apply (rule fdg)
      apply simp
      apply (subgoal_tac "normFace f12 ∉ set (normFaces (faces g'))")
       apply (simp add: normFaces_def)
      apply (rule splitFace_new_f12_norm) apply (rule pre_F')  apply simp
      apply (rule fdg)
     apply (rule minGraphProps11') apply simp
    apply (rule distinct_replace_norm) apply (rule minGraphProps11) apply simp
     apply (simp add: normFaces_def)
    apply (subgoal_tac "normFace f21 ∉ set (normFaces (faces g'))")
     apply (simp add: normFaces_def)
    apply (rule splitFace_new_f21_norm) apply (rule pre_F')  apply simp
    by (rule fdg)
qed


lemma "help":
shows "xs ≠ [] ⟹ x ∉ set xs ⟹  x ≠ hd xs" and
      "xs ≠ [] ⟹ x ∉ set xs ⟹  x ≠ last xs" and
      "xs ≠ [] ⟹ x ∉ set xs ⟹  hd xs ≠ x" and
      "xs ≠ [] ⟹ x ∉ set xs ⟹  last xs ≠ x"
by(auto)

lemma split_face_edge_disj:
 "⟦ pre_split_face f a b vs; (f⇩1, f⇩2) = split_face f a b vs; |vertices f| ≥ 3;
    vs = [] ⟶ (a,b) ∉ edges f ∧ (b,a) ∉ edges f ⟧
    ⟹ ℰ f⇩1 ∩ ℰ f⇩2 = {}"
apply(frule pre_split_face_p_between[THEN between_inter_empty])
apply(unfold pre_split_face_def)
apply clarify
apply(subgoal_tac "⋀x y. x ∈ set vs ⟹ y ∈ 𝒱 f ⟹ x ≠ y")
 prefer 2 apply blast
apply(subgoal_tac "⋀x y. x ∈ set vs ⟹ y ∈ 𝒱 f ⟹ y ≠ x")
 prefer 2 apply blast
apply(subgoal_tac "a ∉ set vs")
 prefer 2 apply blast
apply(subgoal_tac "b ∉ set vs")
 prefer 2 apply blast
apply(subgoal_tac "distinct(vs @ a # between (vertices f) a b @ [b])")
 prefer 2 apply(simp add:between_not_r1 between_not_r2 between_distinct)
 apply(blast dest:inbetween_inset)
apply(subgoal_tac "distinct(b # between (vertices f) b a @ a # rev vs)")
 prefer 2 apply(simp add:between_not_r1 between_not_r2 between_distinct)
 apply(blast dest:inbetween_inset)
apply(subgoal_tac "vs = [] ⟹ between (vertices f) a b ≠ []")
 prefer 2 apply clarsimp apply(frule (4) is_nextElem_between_empty')apply blast
apply(subgoal_tac "vs = [] ⟹ between (vertices f) b a ≠ []")
 prefer 2 apply clarsimp
apply(frule (3) is_nextElem_between_empty')apply simp apply blast
apply(subgoal_tac "vs ≠ [] ⟹ hd vs ∉ 𝒱 f")
 prefer 2 apply(drule hd_in_set) apply blast
apply(subgoal_tac "vs ≠ [] ⟹ last vs ∉ 𝒱 f")
 prefer 2 apply(drule last_in_set) apply blast
apply(subgoal_tac "⋀u v. between (vertices f) u v ≠ [] ⟹ hd(between (vertices f) u v) ∈ 𝒱 f")
 prefer 2 apply(drule hd_in_set)apply(drule inbetween_inset) apply blast
apply(subgoal_tac "⋀u v. between (vertices f) u v ≠ [] ⟹ last (between (vertices f) u v) ∈ 𝒱 f")
 prefer 2 apply(drule last_in_set) apply(drule inbetween_inset) apply blast
apply(simp add:split_face_def edges_conv_Edges Edges_append Edges_Cons
 last_rev notinset_notinEdge1 notinset_notinEdge2 notinset_notinbetween
 between_not_r1 between_not_r2 "help" Edges_rev_disj disj_sets_disj_Edges
 Int_Un_distrib Int_Un_distrib2)
apply clarify
apply(rule conjI)
 apply clarify
 apply(rule disj_sets_disj_Edges)
 apply simp
 apply(blast dest:inbetween_inset)
apply clarify
apply(rule conjI)
 apply clarify
 apply(rule disj_sets_disj_Edges)
 apply simp
 apply(blast dest:inbetween_inset)
apply clarify
apply(rule conjI)
 apply(rule disj_sets_disj_Edges)
 apply simp
 apply(blast dest:inbetween_inset)
apply(rule disj_sets_disj_Edges)
apply(blast dest:inbetween_inset)
done


lemma splitFace_edge_disj:
assumes mgp: "minGraphProps g" and pre: "pre_splitFace g u v f vs"
and FDG: "(f⇩1,f⇩2,g') = splitFace g u v f vs"
shows "edges_disj g'"
proof -
  from mgp have disj: "edges_disj g" by(simp add:minGraphProps_def)
  have "𝒱 g ∩ set vs = {}" using pre
    by (simp add: pre_splitFace_def)
  hence gvs: "∀f ∈ ℱ g. 𝒱 f ∩ set vs = {}"
    by (clarsimp simp:edges_graph_def edges_face_def)
       (blast dest: minGraphProps9[OF mgp])
  have f: "f ∈ ℱ g" by (rule pre_splitFace_oldF[OF pre])
  note split_face = splitFace_split_face[OF f FDG]
  note pre_split_face = pre_splitFace_pre_split_face[OF pre]
  have "ℰ f⇩1 ∩ ℰ f⇩2 = {}"
    apply(rule split_face_edge_disj[OF pre_split_face split_face mgp_vertices3[OF mgp f]])
    using pre
    apply(simp add:pre_splitFace_def del: pre_splitFace_oldF)
    apply clarify
    by(simp) (* loops if combined *)
  moreover
  { fix f' assume f': "f' ∈ ℱ g" "f' ≠ f"
    have "(ℰ f⇩1 ∪ ℰ f⇩2) ∩ ℰ f' = {}"
    proof cases
      assume vs: "vs = []"
      have "(u,v) ∉ ℰ g ∧ (v,u) ∉ ℰ g" using pre vs
        by(simp add:pre_splitFace_def)
      with split_face_edges_f12_f21_vs[OF pre_split_face[simplified vs] split_face[simplified vs]]
      show ?thesis using f f' disj
        by(simp add:is_duplicateEdge_def edges_graph_def edges_disj_def)
    next
      assume vs: "vs ≠ []"
      have f12: "vs ≠ [] ⟹ ℰ f⇩1 ∪ ℰ f⇩2 ⊆
            ℰ f ∪ UNIV × set vs ∪ set vs × UNIV"
        using split_face_edges_f12_f21[OF pre_split_face split_face]
        by simp (fastforce dest:in_Edges_in_set)
      have "⋀x y. (y,x) ∈ ℰ f' ⟹ x ∉ set vs ∧ y ∉ set vs"
        using f' gvs by(blast dest:in_edges_in_vertices)
      then show ?thesis using f f' f12 disj vs
        by(simp add: edges_graph_def edges_disj_def) blast
    qed }
  ultimately show ?thesis using disj
    by(simp add:edges_disj_def set_faces_splitFace[OF mgp f pre FDG])
      blast
qed

lemma splitFace_edges_disj2:
 "minGraphProps g ⟹ pre_splitFace g u v f vs
 ⟹ edges_disj(snd(snd(splitFace g u v f vs)))"
apply(subgoal_tac "pre_splitFace g u v f vs")
 prefer 2 apply(simp)
by(drule (1) splitFace_edge_disj[where f⇩1 = "fst(splitFace g u v f vs)" and f⇩2 = "fst(snd(splitFace g u v f vs))"], auto)


lemma vertices_conv_Union_edges2:
 "distinct(vertices f) ⟹ 𝒱(f::face) = (⋃(a,b)∈ℰ f. {b})"
apply auto
apply(fast intro: prevVertex_in_edges)
done

lemma splitFace_face_face_op:
assumes mgp: "minGraphProps g" and pre: "pre_splitFace g u v f vs"
and fdg: "(f⇩1,f⇩2,g') = splitFace g u v f vs"
shows "face_face_op g'"
proof -
  have f12: "(f⇩1, f⇩2) = split_face f u v vs"
   and Fg': "ℱ g' = {f⇩1} ∪ set(replace f [f⇩2] (faces g))"
   and g': "g' = snd (snd (splitFace g u v f vs))" using fdg
    by(auto simp add:splitFace_def split_def)
  have f⇩1: "f⇩1= fst(split_face f u v vs)" and f⇩2: "f⇩2 = snd(split_face f u v vs)"
    using f12[symmetric] by simp_all
  note distF = minGraphProps11'[OF mgp]
  note pre_split = pre_splitFace_pre_split_face[OF pre]
  note distf⇩1 = split_face_distinct1[OF f12 pre_split]
  note distf⇩2 = split_face_distinct2[OF f12 pre_split]
  from pre have nf: "¬ final f" and fg: "f ∈ ℱ g" and nuv: "u ≠ v"
    and uinf: "u ∈ 𝒱 f"and vinf: "v ∈ 𝒱 f"
    and distf: "distinct(vertices f)" and new: "𝒱 g ∩ set vs = {}"
    by(unfold pre_splitFace_def, simp)+
  let ?fuv = "between (vertices f) u v" and ?fvu = "between (vertices f) v u"
  have E⇩1: "ℰ f⇩1 = Edges (v # rev vs @ [u]) ∪ Edges (u # ?fuv @ [v])"
    using f⇩1 by(simp add:edges_split_face1[OF pre_split])
  have E⇩2: "ℰ f⇩2 = Edges (u # vs @ [v]) ∪ Edges (v # ?fvu @ [u])"
    using f⇩2 by(simp add:edges_split_face2[OF pre_split])
  have vf⇩1: "vertices f⇩1 = rev vs @ u # ?fuv @ [v]"
    using f⇩1 by(simp add:split_face_def)
  have vf⇩2: "vertices f⇩2 = [v] @ ?fvu @ u # vs"
    using f⇩2 by(simp add:split_face_def)
  have V⇩1: "𝒱 f⇩1 = {u,v} ∪ set(?fuv) ∪ set(vs)" using vf⇩1 by auto
  have V⇩2: "𝒱 f⇩2 = {u,v} ∪ set(?fvu) ∪ set(vs)" using vf⇩2 by auto
  have 2: "(v,u) ∈ ℰ f⇩1 ∧ (u,v) ∈ ℰ f⇩2 ∧ vs = [] ∨
           (∃v ∈ 𝒱 f⇩1 ∩ 𝒱 f⇩2. v ∉ 𝒱 g)"
    using E⇩1 E⇩2 V⇩1 V⇩2 new by(cases vs)(simp_all add:Edges_Cons)
  have "𝒱 f⇩1 ≠ 𝒱 f⇩2"
  proof cases
    assume A: "?fvu = []"
    have "?fuv ≠ []"
    proof
      assume "?fuv = []"
      with A have "ℰ f = {(v,u),(u,v)}"
        using edges_conv_Un_Edges[OF distf uinf vinf nuv]
        by(simp add:Edges_Cons)
      hence "𝒱 f = {u,v}" by(simp add:vertices_conv_Union_edges)
      hence "card(𝒱 f) ≤ 2" by(simp add:card_insert_if)
      thus False
        using mgp_vertices3[OF mgp fg] by(simp add:distinct_card[OF distf])
    qed
    moreover have "set ?fuv ∩ set vs = {}"
      using new minGraphProps9[OF mgp fg inbetween_inset] by blast
    moreover have "{u,v} ∩ set ?fuv = {}"
      using between_not_r1[OF distf] between_not_r2[OF distf] by blast
    ultimately show ?thesis using V⇩1 V⇩2 A by (auto simp:neq_Nil_conv)
  next
    assume "?fvu ≠ []"
    moreover have "{u,v} ∩ set ?fvu = {}"
      using between_not_r1[OF distf] between_not_r2[OF distf] by blast
    moreover have "set ?fuv ∩ set ?fvu = {}"
      by(simp add:pre_between_def between_inter_empty distf uinf vinf nuv)
    moreover have "set ?fvu ∩ set vs = {}"
      using new minGraphProps9[OF mgp fg inbetween_inset] by blast
    ultimately show ?thesis using V⇩1 V⇩2 by (auto simp:neq_Nil_conv)
  qed
  have C12: "ℰ f⇩1 ≠ (ℰ f⇩2)¯"
  proof
    assume A: "ℰ f⇩1 = (ℰ f⇩2)¯"
    show False
    proof -
      have "𝒱 f⇩1 = (⋃(a,b)∈ℰ f⇩1. {a})"
        by(rule vertices_conv_Union_edges)
      also have "… = (⋃(b,a)∈ℰ f⇩2. {a})" by(auto simp:A)
      also have "… = 𝒱 f⇩2"
        by(rule vertices_conv_Union_edges2[OF distf⇩2, symmetric])
      finally show False using ‹𝒱 f⇩1 ≠ 𝒱 f⇩2› by blast
    qed
  qed
  { fix h :: face assume hg: "h ∈ ℱ g"
    have "ℰ h ≠ (ℰ f⇩1)¯ ∧ ℰ h ≠ (ℰ f⇩2)¯" using 2
    proof
      assume "(v,u) ∈ ℰ f⇩1 ∧ (u,v) ∈ ℰ f⇩2 ∧ vs = []"
      moreover hence "(u,v) ∉ ℰ g"
        using pre by(unfold pre_splitFace_def)simp
      moreover hence "(v,u) ∉ ℰ g" by(blast intro:minGraphProps10[OF mgp])
      ultimately show ?thesis using hg by(simp add:edges_graph_def) blast
    next
      assume "∃x ∈ 𝒱 f⇩1 ∩ 𝒱 f⇩2. x ∉ 𝒱 g"
      then obtain x where "x ∈ 𝒱 f⇩1" and "x ∈ 𝒱 f⇩2" and "x ∉ 𝒱 g"
        by blast
      obtain y where "(x,y) ∈ ℰ f⇩1" using ‹x ∈ 𝒱 f⇩1›
        by(auto simp:vertices_conv_Union_edges)
      moreover obtain z where "(x,z) ∈ ℰ f⇩2" using ‹x ∈ 𝒱 f⇩2›
        by(auto simp:vertices_conv_Union_edges)
      moreover have "¬(∃y. (y,x) ∈ ℰ h)"
        using ‹x ∉ 𝒱 g› minGraphProps9[OF mgp hg]
        by(blast dest:in_edges_in_vertices)
      ultimately show ?thesis by blast
    qed
  }
  note Cg12 = this
  show ?thesis
  proof cases
    assume 2: "|faces g| = 2"
    with fg obtain f' where Fg: "ℱ g = {f,f'}"
      by(fastforce simp: eval_nat_numeral length_Suc_conv)
    moreover hence "f ≠ f'" using 2 distinct_card[OF distF] by auto
    ultimately have Fg': "ℱ g' = {f⇩1,f⇩2,f'}"
      using set_faces_splitFace[OF mgp fg pre fdg] by blast
    show ?thesis using Fg' C12 Cg12 Fg
      by(fastforce simp:face_face_op_def)
  next
    assume "|faces g| ≠ 2"
    hence E: "⋀f f'. f∈ℱ g ⟹ f'∈ℱ g ⟹ f ≠ f' ⟹ ℰ f ≠ (ℰ f')¯"
      using mgp by(simp add:minGraphProps_def face_face_op_def)
    thus ?thesis using set_faces_splitFace[OF mgp fg pre fdg] C12 Cg12
      by(fastforce simp:face_face_op_def)
  qed
qed

lemma splitFace_face_face_op2:
 "minGraphProps g ⟹ pre_splitFace g u v f vs
 ⟹ face_face_op(snd(snd(splitFace g u v f vs)))"
apply(subgoal_tac "pre_splitFace g u v f vs")
 prefer 2 apply(simp)
by(drule (1) splitFace_face_face_op[where f⇩1 = "fst(splitFace g u v f vs)" and f⇩2 = "fst(snd(splitFace g u v f vs))"], auto)

lemma splitFace_holds_minGraphProps:
  assumes precond: "pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n]"
  and min: "minGraphProps g'"
  shows "minGraphProps (snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))"
proof -
  from min have "minGraphProps' g'" by (simp add: minGraphProps_def)
  then show ?thesis apply (simp add: minGraphProps_def) apply safe
    apply (rule splitFace_holds_minGraphProps') apply (rule precond) apply assumption
    apply (rule splitFace_holds_facesAt_eq) apply (rule precond) apply (rule min) apply simp
    apply (rule splitFace_holds_faceListAt_len) apply (rule precond) apply (rule min)
    apply (rule splitFace_holds_facesAt_distinct) apply (rule precond) apply (rule min)
    apply (rule splitFace_holds_faces_distinct) apply (rule precond) apply (rule min)
    apply (rule splitFace_holds_faces_subset) apply (rule precond) apply (rule min)
    apply (rule splitFace_holds_edges_sym) apply (rule precond) apply (rule min)
    apply (rule splitFace_edges_disj2) apply (rule min) apply (rule precond)
    apply (rule splitFace_face_face_op2) apply (rule min) apply (rule precond)
    done
qed


subsection‹Invariants of @{const makeFaceFinal}›


lemma MakeFaceFinal_minGraphProps':
  "f ∈ ℱ g ⟹ minGraphProps g ⟹ minGraphProps' (makeFaceFinal f g)"
apply (simp add: minGraphProps_def minGraphProps'_def makeFaceFinal_def)
apply (subgoal_tac "2 < |vertices f| ∧ distinct (vertices f)")
 apply (rule ballI) apply (elim conjE ballE) apply (rule conjI) apply simp apply simp
  apply (simp add: makeFaceFinalFaceList_def) apply (drule replace5) apply (simp add: setFinal_def)
by force

lemma MakeFaceFinal_facesAt_eq:
  "f ∈ ℱ g ⟹ minGraphProps g ⟹ facesAt_eq (makeFaceFinal f g)"
apply (simp add: facesAt_eq_def) apply (rule ballI)
apply (subgoal_tac "v ∈ 𝒱 g")
 apply (rule equalityI)
  apply (rule subsetI)
  apply (simp add: makeFaceFinal_def facesAt_def)
  apply (subgoal_tac "v < | faceListAt g | ")
   apply (simp add: makeFaceFinalFaceList_def)
   apply (subgoal_tac "distinct ((faceListAt g ! v))")
    apply (subgoal_tac "distinct (faces g)")
     apply (simp add: replace6)
     apply (case_tac "x = f")
      apply simp apply (erule (1) minGraphProps6) apply (simp add: facesAt_def) apply blast
     apply simp
     apply (case_tac " f ∈ set (faceListAt g ! v) ∧ x = setFinal f") apply simp
      apply (subgoal_tac "v ∈ 𝒱 f") apply (simp add: setFinal_def)
      apply (erule (1) minGraphProps6) apply (simp add: facesAt_def)
     apply simp
     apply (rule conjI) apply (rule disjI2)
      apply (erule (1) minGraphProps5) apply (fastforce simp: facesAt_def)
     apply (erule (1) minGraphProps6) apply (fastforce simp: facesAt_def)
    apply (rule minGraphProps11') apply simp
   apply (rule normFaces_distinct) apply (rule minGraphProps8a) apply simp apply simp
  apply (simp add: vertices_graph minGraphProps4)
    (* backward *)

 apply (rule subsetI) apply (simp add: makeFaceFinal_def facesAt_def)
 apply (subgoal_tac "v < | faceListAt g | ") apply simp
  apply (subgoal_tac "distinct (faceListAt g ! v)")
   apply (subgoal_tac "distinct (faces g)")
    apply (simp add: makeFaceFinalFaceList_def replace6)
    apply (case_tac "x = setFinal f") apply simp
     apply (rule disjI1) apply (rule minGraphProps7') apply simp apply simp
    apply (simp add: setFinal_def) apply simp
   apply (rule minGraphProps7') apply simp apply simp apply simp
   apply (rule minGraphProps11') apply simp
  apply (rule normFaces_distinct) apply (rule minGraphProps8a) apply simp apply simp
 apply (simp add: vertices_graph minGraphProps4)
   (* Vorbed v in set (vertices g) *)
apply (simp add: makeFaceFinal_def) by (simp add: in_vertices_graph minGraphProps4)

lemma MakeFaceFinal_faceListAt_len:
 "f ∈ ℱ g ⟹ minGraphProps g ⟹ faceListAt_len (makeFaceFinal f g)"
  apply (simp add: faceListAt_len_def makeFaceFinal_def) apply (rule minGraphProps4) by simp

lemma normFaces_makeFaceFinalFaceList: "(normFaces (makeFaceFinalFaceList f fs)) = (normFaces fs)"
  apply (simp add: normFaces_def) apply (simp add: makeFaceFinalFaceList_def)
  apply (induct fs) apply simp apply simp apply (rule impI)
  by (simp add: setFinal_def normFace_def verticesFrom_def minVertex_def)

lemma MakeFaceFinal_facesAt_distinct:
 "f ∈ ℱ g ⟹  minGraphProps g ⟹ facesAt_distinct (makeFaceFinal f g)"
  apply (simp add: facesAt_distinct_def makeFaceFinal_def)
  apply (clarsimp simp: facesAt_def)
  apply (subgoal_tac "v < | (faceListAt g) |") apply (simp add: normFaces_makeFaceFinalFaceList)
  apply (rule minGraphProps8a') apply simp apply simp by (simp add: minGraphProps4)

lemma MakeFaceFinal_faces_subset:
 "f ∈ ℱ g ⟹  minGraphProps g ⟹ faces_subset (makeFaceFinal f g)"
  apply (simp add: faces_subset_def) apply (intro ballI subsetI)
  apply (simp add: makeFaceFinal_def makeFaceFinalFaceList_def)
  apply (drule replace5)
  apply (case_tac "fa ∈ ℱ g") apply simp apply (rule minGraphProps9')
    apply simp apply (thin_tac "f ∈ ℱ g") apply simp+
  apply (rule minGraphProps9') apply simp apply simp by (simp add: setFinal_def)

lemma MakeFaceFinal_edges_sym:
 "f ∈ ℱ g ⟹  minGraphProps g ⟹ edges_sym (makeFaceFinal f g)"
  apply (simp add: edges_sym_def) apply (intro allI impI)
  apply (simp add: makeFaceFinal_def edges_graph_def)
  apply (elim bexE) apply (simp add: makeFaceFinalFaceList_def)
  apply (subgoal_tac "distinct (faces g)")
  apply (case_tac "x ∈ ℱ g")
    apply (subgoal_tac "(a,b) ∈ edges g") apply (frule minGraphProps10) apply assumption
    apply (simp add: edges_graph_def) apply (elim bexE)
    apply (case_tac "xb = f")
      apply (subgoal_tac "(b,a) ∈ edges (setFinal f)")
        apply (rule bexI) apply (rotate_tac -1)  apply assumption
        apply (rule replace3) apply simp apply simp
      apply (subgoal_tac "distinct (vertices f)")
      apply (simp add: edges_setFinal)
      apply (rule minGraphProps3) apply simp apply simp
    apply (rule bexI) apply assumption apply (rule replace4) apply simp apply force
    apply (simp add: edges_graph_def) apply force
  apply (frule replace5) apply simp
  apply (subgoal_tac "(a,b) ∈ edges g")
  apply (frule minGraphProps10) apply assumption apply (simp add: edges_graph_def) apply (elim bexE)
    apply (case_tac "xb = f")
      apply (subgoal_tac "(b, a) ∈ edges (setFinal f)")
        apply (rule bexI) apply (rotate_tac -1) apply assumption
        apply (rule replace3) apply simp apply simp
      apply (subgoal_tac "distinct (vertices f)")
      apply (simp add: edges_setFinal)
      apply (rule minGraphProps3) apply simp apply simp
    apply  (rule bexI) apply simp apply (rule replace4) apply simp apply force
  apply (subgoal_tac "distinct (vertices f)")
  apply (subgoal_tac "(a,b) ∈ edges f")
  apply (simp add: edges_graph_def)   apply force
  apply (simp add: edges_setFinal)
  apply (rule minGraphProps3) apply simp apply simp
  by (rule minGraphProps11')

lemma MakeFaceFinal_faces_distinct:
 "f ∈ ℱ g ⟹  minGraphProps g ⟹ faces_distinct (makeFaceFinal f g)"
  apply (simp add: faces_distinct_def makeFaceFinal_def normFaces_makeFaceFinalFaceList)
  by (rule minGraphProps11)

lemma MakeFaceFinal_edges_disj:
 "f ∈ ℱ g ⟹  minGraphProps g ⟹ edges_disj (makeFaceFinal f g)"
apply(frule minGraphProps11')
apply (clarsimp simp: edges_disj_def makeFaceFinal_def edges_graph_def
                      makeFaceFinalFaceList_def replace6)
apply(case_tac "f = f'")
 apply (fastforce dest:mgp_edges_disj)
apply (fastforce dest:mgp_edges_disj)
done


lemma MakeFaceFinal_face_face_op:
 "f ∈ ℱ g ⟹ minGraphProps g ⟹ face_face_op (makeFaceFinal f g)"
apply(subgoal_tac "face_face_op g")
 prefer 2 apply(simp add:minGraphProps_def)
apply(drule minGraphProps11')
apply(auto simp: face_face_op_def makeFaceFinal_def makeFaceFinalFaceList_def
                 distinct_set_replace)
done


lemma MakeFaceFinal_minGraphProps:
 "f ∈ ℱ g ⟹ minGraphProps g ⟹ minGraphProps (makeFaceFinal f g)"
apply (simp (no_asm) add: minGraphProps_def)
apply (simp add: MakeFaceFinal_minGraphProps' MakeFaceFinal_facesAt_eq
    MakeFaceFinal_faceListAt_len MakeFaceFinal_facesAt_distinct
    MakeFaceFinal_faces_subset MakeFaceFinal_edges_sym
    MakeFaceFinal_edges_disj MakeFaceFinal_faces_distinct
    MakeFaceFinal_face_face_op)
done


subsection‹Invariants of @{const subdivFace'}›

lemma subdivFace'_holds_minGraphProps: "⋀ f v' v n g.
  pre_subdivFace' g f v' v n ovl ⟹ f ∈ ℱ g ⟹
  minGraphProps g ⟹ minGraphProps (subdivFace' g f v n ovl)"
proof (induct ovl)
  case Nil then show ?case by (simp add: MakeFaceFinal_minGraphProps)
next
  case (Cons ov ovl) then show ?case
apply auto
apply (cases "ov")
 apply (simp_all split: if_split_asm)
 apply (rule Cons)
   apply (rule pre_subdivFace'_None)
   apply simp_all
apply (intro conjI)
 apply clarsimp
 apply (rule Cons)
   apply (rule pre_subdivFace'_Some2)
   apply simp_all
apply (clarsimp simp: split_def)
apply (rule Cons)
  apply (rule pre_subdivFace'_Some1)
       apply simp_all
  apply (simp add: minGraphProps_def faces_subset_def)
 apply (rule splitFace_add_f21')
 apply simp_all
apply (rule splitFace_holds_minGraphProps)
 apply simp_all
apply (rule pre_subdivFace'_preFaceDiv)
   apply simp_all
by (simp add: minGraphProps_def faces_subset_def)
qed


(* Invariance of one_final *)

abbreviation (input)
  Edges_if :: "face ⇒ vertex ⇒ vertex ⇒ (vertex × vertex)set" where
  "Edges_if f u v ==
    if u=v then {} else Edges(u # between (vertices f) u v @ [v])"

lemma FaceDivsionGraph_one_final_but:
assumes mgp: "minGraphProps g" and pre: "pre_splitFace g u v f vs"
and fdg: "(f⇩1,f⇩2,g') = splitFace g u v f vs"
and nrv: "r ≠ v"
and ruv: "before (verticesFrom f r) u v" and rf: "r ∈ 𝒱 f"
and 1: "one_final_but g (Edges_if f r u)"
shows "one_final_but g' (Edges(r # between (vertices f⇩2) r v @ [v]))"
proof -
  have f⇩1: "f⇩1= fst(split_face f u v vs)" and f⇩2: "f⇩2 = snd(split_face f u v vs)"
   and F: "ℱ g' = {f⇩1} ∪ set(replace f [f⇩2] (faces g))"
   and g': "g' = snd (snd (splitFace g u v f vs))" using fdg
    by(auto simp add:splitFace_def split_def)
  note pre_split = pre_splitFace_pre_split_face[OF pre]
  from pre have nf: "¬ final f" and fg: "f ∈ ℱ g" and nuv: "u ≠ v"
    and uinf: "u ∈ 𝒱 f"and vinf: "v ∈ 𝒱 f"
    by(unfold pre_splitFace_def, simp)+
  from mgp fg have distf: "distinct(vertices f)" by(rule minGraphProps3)
  note distFg = minGraphProps11'[OF mgp]
  have fvu: "r≠u ⟹ between (vertices f) v u =
                     between (vertices f) v r @ r # between (vertices f) r u"
    using before_between2[OF ruv distf rf] nrv
      split_between[OF distf vinf uinf, of r] by (auto)
  let ?fuv = "between (vertices f) u v" and ?fvu = "between (vertices f) v u"
  let ?fru = "between (vertices f) r u" and ?f⇩2rv = "between (vertices f⇩2) r v"
  have E⇩1: "ℰ f⇩1 = Edges (v # rev vs @ [u]) ∪ Edges (u # ?fuv @ [v])"
    using f⇩1 by(simp add:edges_split_face1[OF pre_split])
  have E⇩2: "ℰ f⇩2 = Edges (u # vs @ [v]) ∪ Edges (v # ?fvu @ [u])"
    using f⇩2 by(simp add:edges_split_face2[OF pre_split])
  have vf⇩2: "vertices f⇩2 = [v] @ ?fvu @ u # vs"
    using f⇩2 by(simp add:split_face_def)
  have vinf⇩2: "v ∈ 𝒱 f⇩2" using vf⇩2 by(simp)
  have rinf⇩2: "r ∈ 𝒱 f⇩2"
  proof cases
    assume "r=u" thus ?thesis by(simp add:vf⇩2)
  next
    assume "r≠u" thus ?thesis by(simp add: vf⇩2 fvu)
  qed
  have distf⇩2: "distinct(vertices f⇩2)"
    by(simp add:f⇩2)(rule split_face_distinct2'[OF pre_split])
  have f⇩2uv: "between (vertices f⇩2) u v = vs"
    using vf⇩2 distf⇩2 by(simp add:between_def split_def)
  have f⇩2ru: "r≠u ⟹ between (vertices f⇩2) r u = between (vertices f) r u"
    using vf⇩2 fvu distf distf⇩2 by(simp add:between_def split_def)
  hence f⇩2rv: "between (vertices f⇩2) r v =
              (if r=u then [] else ?fru @ [u]) @ vs"
  proof cases
    assume "r=u" thus ?thesis by(simp add: f⇩2uv)
  next
    assume nru: "r ≠ u"
    have vinf⇩2: "v ∈ 𝒱 f⇩2" by(simp add: vf⇩2)
    note u_bet_rv = before_between[OF ruv distf rf nru]
    have u_bet_rv⇩2: "u ∈ set (between (vertices f⇩2) r v)"
      using distf⇩2 nru
      apply(simp add:vf⇩2 fvu)
      apply(subst between_def[of _ r v])
      apply(simp add:split_def)
      done
    show ?thesis
      by(simp add:split_between[OF distf⇩2 rinf⇩2 vinf⇩2 u_bet_rv⇩2] f⇩2ru f⇩2uv)
  qed
  have E⇩2rv: "Edges(r # ?f⇩2rv @ [v]) =
         Edges_if f r u ∪ Edges(u # vs @ [v])" (is "?L = ?R")
  proof -
    have "?L = Edges((if r=u then [] else r # ?fru) @ (u # vs @ [v]))"
      by (simp add: f⇩2rv)
    also have "… = ?R" by(auto simp:Edges_Cons Edges_append)
    finally show ?thesis .
  qed
  show ?thesis
  proof (auto del: disjCI simp:one_final_but_def F, goal_cases)
    case prems: (1 a b)
    have ab: "(a,b) ∈ ℰ f⇩1"
      and nab: "(a,b) ∉ Edges (r # ?f⇩2rv @ [v])" by fact+
    have "(a,b) ∈ Edges (v # rev vs @ [u]) ∨
          (a,b) ∈ Edges (u # ?fuv @ [v])" (is "?A ∨ ?B")
      using E⇩1 ab by blast
    thus ?case
    proof
      assume ?A
      hence "(b,a) ∈ Edges (rev(v # rev vs @ [u]))" by (simp del:rev.simps)
      hence "(b,a) ∈ Edges (r # ?f⇩2rv @ [v])" using E⇩2rv by simp
      thus ?case by blast
    next
      assume abfuv: ?B
      have abf: "(a,b) ∈ ℰ f"
        by(rule Edges_between_edges[OF abfuv pre_split])
      have "(∃f'∈set(replace f [f⇩2] (faces g)). final f' ∧ (b,a) ∈ ℰ f')"
      proof cases
        assume "r = u"
        then obtain f' where "f' ∈ ℱ g ∧ final f' ∧ (b, a) ∈ ℰ f'"
          using abf 1 nf fg by(simp add:one_final_but_def)fast
        moreover then have "f' ∈ set (replace f [f⇩2] (faces g))"
          by(clarsimp simp: replace6[OF distFg] nf)
        ultimately show ?thesis by blast
      next
        assume nru: "r ≠ u"
        moreover hence "(a,b) ∉ Edges (r # ?fru @ [u])"
          using abfuv Edges_disj[OF distf rf vinf nru nuv
                        before_between[OF ruv distf rf nru]] by fast
        moreover have "(b,a) ∉ Edges (r # ?fru @ [u])"
        proof
          assume "(b,a) ∈ Edges (r # ?fru @ [u])"
          moreover have "pre_split_face f r u []"
            by(simp add:pre_split_face_def distf rf uinf nru)
          ultimately show False
            using minGraphProps12[OF mgp fg abf]
            by(blast dest:Edges_between_edges)
        qed
        ultimately obtain f' where "f' ∈ ℱ g ∧ final f' ∧ (b, a) ∈ ℰ f'"
          using abf 1 nf fg by(simp add:one_final_but_def)fast
        moreover hence "f' ∈ set (replace f [f⇩2] (faces g))"
          by(clarsimp simp: replace6[OF distFg] nf)
        ultimately show ?thesis by blast
      qed
      thus ?case ..
    qed
  next
    case (2 f' a b)
    have f': "f' ∈ set (replace f [f⇩2] (faces g))"
      and nf': "¬ final f'" and abf': "(a,b) ∈ ℰ f'"
      and nab: "(a,b) ∉ Edges (r # between (vertices f⇩2) r v @ [v])" by fact+
    have "f' = f⇩2 ∨ f' ∈ ℱ g ∧ f' ≠ f"
      using f' by(simp add:replace6[OF distFg]) blast
    hence "(b, a) ∈ Edges (r # between (vertices f⇩2) r v @ [v]) ∨
      (∃f'∈set (replace f [f⇩2] (faces g)). final f' ∧ (b, a) ∈ ℰ f')"
      (is "?A ∨ ?B")
    proof
      assume [simp]: "f' = f⇩2"
      have "(a,b) ∈ Edges (v # between (vertices f⇩2) v r @ [r])"
        using abf' nab Edges_compl[OF distf⇩2 vinf⇩2 rinf⇩2 nrv[symmetric]]
        edges_conv_Un_Edges[OF distf⇩2 rinf⇩2 vinf⇩2 nrv] by auto
      moreover have eq: "between(vertices f⇩2) v r = between (vertices f) v r"
      proof (cases "r=u")
        assume "r=u" thus ?thesis
          by(simp add:vf⇩2)(rule between_front[OF between_not_r2[OF distf]])
      next
        assume "r≠u" thus ?thesis
          by(simp add:vf⇩2 fvu)(rule between_front[OF between_not_r2[OF distf]])
      qed
      ultimately
      have abfvr: "(a,b) ∈ Edges (v # between (vertices f) v r @ [r])"
        by simp
      have abf: "(a,b) ∈ ℰ f"
        apply(rule Edges_between_edges[where vs = "[]", OF abfvr])
        using distf rf vinf nrv by(simp add:pre_split_face_def)
      have "(∃f'∈set(replace f [f⇩2] (faces g)). final f' ∧ (b,a) ∈ ℰ f')"
      proof cases
        assume "r = u"
        then obtain f' where "f' ∈ ℱ g ∧ final f' ∧ (b, a) ∈ ℰ f'"
          using abf 1 nf fg by(simp add:one_final_but_def)fast
        moreover then have "f' ∈ set (replace f [f⇩2] (faces g))"
          by(clarsimp simp: replace6[OF distFg] nf)
        ultimately show ?thesis by blast
      next
        assume nru: "r ≠ u"
        note uvr = rotate_before_vFrom[OF distf rf nru ruv]
        note bet = before_between[OF uvr distf vinf  nrv[symmetric]]
        have "(a,b) ∉ Edges (r # ?fru @ [u])"
          using abfvr Edges_disj[OF distf vinf uinf nrv[symmetric] nru bet]
          by fast
        moreover have "(b,a) ∉ Edges (r # ?fru @ [u])"
        proof
          assume "(b,a) ∈ Edges (r # ?fru @ [u])"
          moreover have "pre_split_face f r u []"
            by(simp add:pre_split_face_def distf rf uinf nru)
          ultimately show False
            using minGraphProps12[OF mgp fg abf]
            by(blast dest:Edges_between_edges)
        qed
        ultimately obtain f' where "f' ∈ ℱ g ∧ final f' ∧ (b, a) ∈ ℰ f'"
          using abf 1 nf fg nru by(simp add:one_final_but_def)fast
        moreover hence "f' ∈ set (replace f [f⇩2] (faces g))"
          by(clarsimp simp: replace6[OF distFg] nf)
        ultimately show ?thesis by blast
      qed
      thus ?thesis ..
    next
      assume  f': "f' ∈ ℱ g ∧ f' ≠ f"
      moreover
      hence "ℰ f' ∩ ℰ f = {}"
        using fg by(blast dest: mgp_edges_disj[OF mgp])
      moreover
      have "Edges_if f r u ⊆ ℰ f"
        using distf rf uinf
        apply(clarsimp simp del:is_nextElem_edges_eq)
        apply(erule Edges_between_edges[where vs = "[]"])
        by(simp add:pre_split_face_def)
      ultimately
      have "(b,a) : Edges_if f r u ∨
            (∃f''∈ℱ g. final f'' ∧ (b,a) ∈ ℰ f'')" (is "?A ∨ ?B")
        using 1 f' nf' abf'
        by(simp add:one_final_but_def split:if_split_asm) blast+
      thus ?thesis (is "?A' ∨ ?B'")
      proof
        assume ?A
        moreover
        have "Edges_if f r u ⊆ Edges (r # between (vertices f⇩2) r v @ [v])"
          using f⇩2rv by (auto simp:Edges_Cons Edges_append)
        ultimately have ?A' by blast
        thus ?thesis ..
      next
        assume ?B
        then obtain f'' where "f''∈ℱ g ∧ final f'' ∧ (b, a) ∈ ℰ f''"
          by blast
        moreover hence "f'' ≠ f" using nf by blast
        ultimately have ?B' by (blast intro:in_set_repl)
        thus ?thesis ..
      qed
    qed
    thus ?case by blast
  qed
qed


lemma one_final_but_makeFaceFinal:
 "⟦ minGraphProps g; one_final_but g E; E ⊆ ℰ f; f ∈ ℱ g; ¬ final f ⟧ ⟹
  one_final (makeFaceFinal f g)"
apply(frule minGraphProps11')
apply(clarsimp simp add:one_final_but_def one_final_def makeFaceFinal_def
         makeFaceFinalFaceList_def replace6)
apply(rename_tac f' a b)
apply(erule disjE)
 apply(simp)
apply(subgoal_tac "(a,b) ∉ E")
 prefer 2 apply (simp add:minGraphProps_def edges_disj_def) apply blast
apply(drule_tac x = f' in bspec)
 apply assumption
apply simp
apply(drule_tac x = "(a,b)" in bspec)
 apply simp
apply(fastforce simp add: replace6)
done


lemma one_final_subdivFace':
  "⋀f v n g.
  pre_subdivFace' g f u v n ovs ⟹ minGraphProps g ⟹ f ∈ ℱ g ⟹
  one_final_but g (Edges_if f u v) ⟹
  one_final(subdivFace' g f v n ovs)"
proof (induct ovs)
  case Nil
  hence "pre_split_face f u v []"
    by(simp add:pre_split_face_def pre_subdivFace'_def)
  hence "Edges(u # between (vertices f) u v @ [v]) ⊆ ℰ f"
    by(auto simp add:Edges_between_edges)
  moreover have "¬ final f" using Nil by(simp add:pre_subdivFace'_def)
  ultimately show ?case using Nil by (simp add: one_final_but_makeFaceFinal)
next
  case (Cons ov ovs)
  note IH = Cons(1) and pre = Cons(2) and mgp = Cons(3) and fg = Cons(4)
  note 1 = Cons(5)
  have nf: "¬ final f" and uf: "u ∈ 𝒱 f" and vf: "v ∈ 𝒱 f"
    using pre by(simp add:pre_subdivFace'_def)+
  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 1])
  next
    case (Some w)
    have uw: "u ≠ w" using pre Some by(clarsimp simp: pre_subdivFace'_def)
    { assume w: "f ∙ v = w" and n: "n = 0"
      from w minGraphProps3[OF mgp fg]
      have vw: "nextElem (vertices f) (hd(vertices f)) v =  w"
        by(simp add:nextVertex_def)
      have 2: "one_final_but g (if u=w then {} else Edges (u # between (vertices f) u w @ [w]))"
          apply (rule one_final_but_antimono[OF 1])
          using uw apply clarsimp
          apply(subgoal_tac "pre_between (vertices f) u v")
           prefer 2
           using pre vf apply(simp add:pre_subdivFace'_def pre_between_def)
          apply(simp add:between_nextElem vw[symmetric])
          apply(fastforce simp add:Edges_Cons Edges_append)
          done
      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)
      have "one_final (subdivFace' g f w 0 ovs)"
        by (simp add: IH[OF pre' mgp fg 2])
    } moreover
    { let ?vs = "[countVertices g..<countVertices g + n]"
      let ?fdg = "splitFace g v w f ?vs"
      let ?Ew = "if u=w then {} else Edges(u # between(vertices (fst(snd ?fdg))) u w @ [w])"
      assume a: "f ∙ v = w ⟶ 0 < n"
      have pre2: "pre_subdivFace' g f u v n (Some w # ovs)"
        using pre Some by simp
      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 _ fg _ fsubg])
            using Some pre apply simp
           using a apply (simp)
           done
      have bet: "before (verticesFrom f u) v w" using pre Some
        by(unfold pre_subdivFace'_def) simp
      have 2: "one_final_but(snd(snd ?fdg)) ?Ew"
        using uw apply simp
        apply(rule FaceDivsionGraph_one_final_but[OF mgp pre_fdg _ uw bet uf 1])
        apply(fastforce intro!:prod_eqI)
        done
      note mgp' = splitFace_holds_minGraphProps[OF pre_fdg mgp]
      have pre2': "pre_subdivFace' (snd (snd ?fdg)) (fst (snd ?fdg)) u w 0 ovs"
        by (rule pre_subdivFace'_Some1[OF pre2 fg _ fsubg HOL.refl HOL.refl])
           (simp add:a)
      note f2inF = splitFace_add_f21'[OF fg]
      have "one_final (subdivFace' (snd (snd ?fdg)) (fst (snd ?fdg)) w 0 ovs)"
        by (simp add: IH[OF pre2' mgp' f2inF 2])
    } ultimately show ?thesis using Some by (simp add: split_def)
  qed
qed


lemma neighbors_edges:
 "minGraphProps g ⟹ a : 𝒱 g ⟹ b ∈ set (neighbors g a) = ((a, b) ∈ edges g)"
apply (rule iffI)
 apply (simp add: neighbors_def) apply clarify apply (frule (1) minGraphProps5)
  apply (simp add: vertices_graph)
 apply (simp add: edges_graph_def) apply (intro bexI)
  prefer 2 apply assumption
 apply(simp add:edges_face_eq)
 apply (erule (2) minGraphProps6)
apply (simp add: neighbors_def) apply (simp add: edges_graph_def) apply (elim bexE)
apply (subgoal_tac "x ∈ set (facesAt g a)") apply (simp add: edges_face_def)
apply (rule minGraphProps7) apply simp+ apply (simp add: edges_face_def)
done


lemma no_self_edges: "minGraphProps' g ⟹ (a, a) ∉ edges g" apply (simp add: minGraphProps'_def)
apply (induct g) apply simp apply (simp add: edges_graph_def) apply auto apply (drule bspec) apply assumption
apply auto apply (simp add: is_nextElem_def) apply safe apply (simp add: is_sublist_def) apply force
apply (case_tac "vertices x") apply simp apply (case_tac "list" rule: rev_exhaust) apply simp by simp

text‹Requires only @{prop"distinct(vertices f)"} and that ‹g›
has no self-loops.›

lemma duplicateEdge_is_duplicateEdge_eq:
"minGraphProps g ⟹ f ∈ ℱ g ⟹ a ∈ 𝒱 f ⟹ b ∈ 𝒱 f ⟹
 duplicateEdge g f a b = is_duplicateEdge g f a b"
apply (subgoal_tac "distinct (vertices f)")
 prefer 2 apply (simp add: minGraphProps3)
apply(subgoal_tac "a : 𝒱 g")
 prefer 2 apply (simp add: minGraphProps9)
apply (simp add: duplicateEdge_def is_duplicateEdge_def neighbors_edges)
apply (rule iffI)
 apply (simp add: minGraphProps10)
 apply (cases "a = b") apply (simp add: no_self_edges minGraphProps_def)
 apply (rule ccontr)
 apply (simp add: directedLength_def)
 apply (case_tac "is_nextElem (vertices f) a b")
  apply (simp add: is_nextElem_between_empty)
 apply (simp add: is_nextElem_between_empty)
apply (cases "a = b") apply (simp add: no_self_edges minGraphProps_def)
apply (rule ccontr)
apply (simp add: directedLength_def)
apply (elim impE)
  apply (cases "between (vertices f) b a")
   apply (simp add: is_nextElem_between_empty' del:is_nextElem_between_empty)
  apply simp
 apply (cases "between (vertices f) a b")
  apply (simp add: is_nextElem_between_empty' del:is_nextElem_between_empty)
 apply simp
apply (simp add: minGraphProps10)
done

lemma incrIndexList_less_eq:
 "incrIndexList ls m nmax ⟹ Suc n < |ls| ⟹ ls!n ≤ ls!Suc n"
apply (subgoal_tac "increasing ls") apply (thin_tac "incrIndexList ls m nmax") apply (rule increasing1) apply simp
apply (subgoal_tac "ls = take n ls @ ls!n # [] @ ls!(Suc n) # drop (Suc (Suc n)) ls") apply assumption
apply simp apply (subgoal_tac "n < | ls|") apply (rotate_tac -1) apply (drule id_take_nth_drop)
apply (subgoal_tac "drop (Suc n) ls = ls ! Suc n # drop (Suc (Suc n)) ls") apply simp apply (drule Cons_nth_drop_Suc)
by auto

lemma incrIndexList_less:
 "incrIndexList ls m nmax ⟹ Suc n < |ls| ⟹ ls!n ≠ ls!Suc n⟹ ls!n < ls!Suc n"
apply (drule  incrIndexList_less_eq) by auto

lemma Seed_holds_minGraphProps': "minGraphProps' (Seed p)"
by (simp  add: graph_def Seed_def minGraphProps'_def)

lemma Seed_holds_facesAt_eq: "facesAt_eq (Seed p)"
by (force simp  add: graph_def Seed_def facesAt_eq_def facesAt_def)

lemma minVertex_zero1: "minVertex (Face [0..<Suc z] Final) = 0"
  apply (induct z) apply (simp add: minVertex_def)
  by (simp add: minVertex_def upt_conv_Cons del: upt_Suc)

lemma minVertex_zero2: "minVertex (Face (rev [0..<Suc z]) Nonfinal) = 0"
  apply (induct z) apply (simp add: minVertex_def)
  by (simp add: minVertex_def min_def)


subsection‹Invariants of @{const Seed}›

lemma Seed_holds_facesAt_distinct: "facesAt_distinct (Seed p)"
apply(simp add: Seed_def graph_def
                facesAt_distinct_def normFaces_def facesAt_def normFace_def)
apply(simp add: eval_nat_numeral minVertex_zero1 minVertex_zero2 verticesFrom_Def
   fst_splitAt_upt snd_splitAt_upt fst_splitAt_rev snd_splitAt_rev del:upt_Suc)
apply(simp add:upt_conv_Cons del:upt_Suc)
apply simp
done

lemma Seed_holds_faces_subset: "faces_subset (Seed p)"
by (simp add: Seed_def graph_def faces_subset_def)

lemma Seed_holds_edges_sym: "edges_sym (Seed p)"
by (simp add: Seed_def graph_def edges_sym_def edges_graph_def)


lemma Seed_holds_edges_disj: "edges_disj (Seed p)"
using is_nextElem_circ[of "[0..<(p+3)]"]
by (fastforce simp add: Seed_def graph_def edges_disj_def edges_graph_def)


lemma Seed_holds_faces_distinct: "faces_distinct (Seed p)"
apply(simp add: Seed_def graph_def
                faces_distinct_def normFaces_def facesAt_def normFace_def)
apply(simp add: eval_nat_numeral minVertex_zero1 minVertex_zero2 verticesFrom_Def
   fst_splitAt_upt snd_splitAt_upt fst_splitAt_rev snd_splitAt_rev del:upt_Suc)
apply(simp add:upt_conv_Cons del:upt_Suc)
apply simp
done

lemma Seed_holds_faceListAt_len: "faceListAt_len (Seed p)"
by (simp add: Seed_def graph_def faceListAt_len_def)

lemma face_face_op_Seed: "face_face_op(Seed p)"
by (simp add: Seed_def graph_def face_face_op_def)

lemma one_final_Seed: "one_final Seed⇘p⇙"
by(clarsimp simp:Seed_def one_final_def one_final_but_def graph_def)

lemma two_face_Seed: "|faces Seed⇘p⇙| ≥ 2"
by(simp add:Seed_def graph_def)

lemma inv_Seed: "inv (Seed p)"
  by (simp add: inv_def minGraphProps_def Seed_holds_minGraphProps'
    Seed_holds_facesAt_eq Seed_holds_facesAt_distinct Seed_holds_faces_subset
    Seed_holds_edges_sym Seed_holds_edges_disj face_face_op_Seed
    Seed_holds_faces_distinct Seed_holds_faceListAt_len
    one_final_Seed two_face_Seed)


lemma pre_subdivFace_indexToVertexList:
assumes mgp: "minGraphProps g" and f: "f ∈ set (nonFinals g)"
  and v: "v ∈ 𝒱 f" and e: "e ∈ set (enumerator i |vertices f| )"
  and containsNot: "¬ containsDuplicateEdge g f v e" and i: "2 < i"
shows "pre_subdivFace g f v (indexToVertexList f v e)"
proof -
  from e i have le: "|e| = i" by (auto intro: enumerator_length2)
  from f have fg: "f ∈ ℱ g" "¬ final f" by (auto simp: nonFinals_def)
  with mgp have le_vf: "2 < |vertices f|"
    by (simp add: minGraphProps_def minGraphProps'_def)
  from fg mgp have dist_f:"distinct (vertices f)"
    by (simp add: minGraphProps_def minGraphProps'_def)
  with le v i e le_vf fg have "pre_subdivFace_face f v (indexToVertexList f v e)"
    by (rule_tac indexToVertexList_pre_subdivFace_face) simp_all
  moreover
  from dist_f v e le_vf have "indexToVertexList f v e = natToVertexList v f e"
    apply (rule_tac indexToVertexList_natToVertexList_eq)
        apply simp
       apply simp
      prefer 2 apply (simp add: enumerator_not_empty)
     by (auto simp:set_enumerator_simps intro:enumerator_bound)
  moreover
  from e le_vf le i have "incrIndexList e i |vertices f|" by simp
  moreover note mgp containsNot i dist_f v le
  ultimately show ?thesis
    apply (simp add: pre_subdivFace_def)
    apply (simp add: invalidVertexList_def)
    apply (simp add: containsDuplicateEdge_eq containsDuplicateEdge'_def)
    apply (rule allI) apply(rename_tac j) apply (rule impI)
    apply (case_tac "natToVertexList v f e ! j") apply simp
    apply simp
    apply (case_tac "natToVertexList v f e ! Suc j") apply simp
    apply simp
    apply (case_tac "j") apply (simp add: natToVertexList_nth_0 natToVertexList_nth_Suc split: if_split_asm)
     apply (drule_tac spec) apply (rotate_tac -1) apply (erule impE)
      apply (subgoal_tac "e ! 0 < e ! Suc 0") apply assumption
      apply (cases "e") apply simp
      apply simp
      apply (drule incrIndexList_help21)
      apply simp
     apply (subgoal_tac "f⇗e ! 0⇖ ∙ v ∈ 𝒱 f")
      apply (subgoal_tac "f⇗e ! Suc 0⇖ ∙ v ∈ 𝒱 f")
       apply (simp add: duplicateEdge_is_duplicateEdge_eq [symmetric] fg)
       apply (rule ccontr)
       apply simp
       apply (cases e) apply simp
       apply simp
       apply (drule incrIndexList_help21) apply clarify apply (drule not_sym) apply (rotate_tac -2) apply simp
      apply (rule nextVertices_in_face) apply simp
     apply (rule nextVertices_in_face) apply simp
    apply simp
    apply (subgoal_tac "natToVertexList v f e ! Suc nat =
        (if e ! nat = e ! Suc nat then None else Some (f⇗e ! Suc nat⇖ ∙ v))")
     apply (simp split: if_split_asm)
     apply (subgoal_tac "natToVertexList v f e ! Suc (Suc nat) =
        (if e ! (Suc nat) = e ! Suc (Suc nat) then None else Some (f⇗e ! Suc (Suc nat)⇖ ∙ v))")
      apply (simp split: if_split_asm)
      apply (drule spec) apply (rotate_tac -1)  apply (erule impE)
       apply (subgoal_tac "e ! nat < e ! Suc nat") apply assumption
       apply (rule incrIndexList_less) apply assumption apply arith
       apply simp
      apply simp
      apply (subgoal_tac "f⇗e ! Suc nat⇖ ∙ v ∈ 𝒱 f")
       apply (subgoal_tac "f⇗e ! Suc (Suc nat)⇖ ∙ v ∈ 𝒱 f")
        apply (simp add: duplicateEdge_is_duplicateEdge_eq [symmetric] fg)
        apply (rule ccontr) apply simp
        apply (rotate_tac -4) apply (erule impE) apply arith
        apply (subgoal_tac "e ! Suc nat < e ! Suc (Suc nat)") apply force
        apply (rule incrIndexList_less) apply assumption apply arith
        apply simp
       apply (rule nextVertices_in_face) apply simp
      apply (rule nextVertices_in_face) apply simp
     apply (rule natToVertexList_nth_Suc) apply simp apply arith
    apply (rule natToVertexList_nth_Suc) apply simp by arith
qed


(* Interlude: increasing properties *)

subsection‹Increasing properties of @{const subdivFace'}›

lemma subdivFace'_incr:
assumes Ptrans: "⋀x y z.  Q x y ⟹ P y z ⟹ P x z"
and mkFin: "⋀f g. f ∈ ℱ g ⟹ ¬ final f ⟹ P g (makeFaceFinal f g)"
and fdg_incr: "⋀g u v f vs.
   pre_splitFace g u v f vs ⟹
   Q g (snd(snd(splitFace g u v f vs)))"
shows
 "⋀f' v n g. pre_subdivFace' g f' v' v n ovl ⟹
  minGraphProps g ⟹  f' ∈ ℱ g ⟹ P g (subdivFace' g f' v n ovl)"
proof (induct ovl)
  case Nil thus ?case by (simp add: pre_subdivFace'_def mkFin)
next
  case (Cons ov ovl) then show ?case
    apply simp
    apply (cases "ov")
     apply (simp)
     apply (rule Cons)
        apply (rule pre_subdivFace'_None)
        apply assumption+
    apply simp
    apply (intro conjI)
     apply rule
     apply simp
     apply (rule Cons)
        apply (rule pre_subdivFace'_Some2)
        apply  assumption+
    apply (rule)
    apply (simp add: split_def)
    apply(rule Ptrans)
    prefer 2
    apply (rule Cons)
       apply (erule (1) pre_subdivFace'_Some1[OF _ _ _ _ HOL.refl HOL.refl])
        apply simp
       apply (simp add: minGraphProps_def faces_subset_def)
      apply (rule splitFace_holds_minGraphProps)
       apply (erule (1) pre_subdivFace'_preFaceDiv)
        apply simp
       apply(simp add: minGraphProps_def faces_subset_def)
      apply assumption
     apply (erule splitFace_add_f21')
    apply(rule fdg_incr)
    apply(erule (1) pre_subdivFace'_preFaceDiv)
     apply simp
    apply(simp add: minGraphProps_def faces_subset_def)
    done
qed

lemma next_plane0_via_subdivFace':
assumes mgp: "minGraphProps g" and gg': "g [next_plane0⇘p⇙]→ g'"
and P: "⋀f v' v n g ovs. minGraphProps g ⟹ pre_subdivFace' g f v' v n ovs ⟹
  f ∈ ℱ g ⟹ P g (subdivFace' g f v n ovs)"
shows "P g g'"
proof -
  from gg'
  obtain f v i "is" e where g': "g' = subdivFace g f is"
    and f: "f ∈ set (nonFinals g)" and v: "v ∈ 𝒱 f"
    and e: "e ∈ set (enumerator i |vertices f| )" and i: "2 < i"
    and containsNot: "¬ containsDuplicateEdge g f v e"
    and is_eq: "is = indexToVertexList f v e"
    by (auto simp: next_plane0_def generatePolygon_def image_def split:if_split_asm)
  from f have fg: "f ∈ ℱ g" by(simp add:nonFinals_def)
  note pre_add = pre_subdivFace_indexToVertexList[OF mgp f v e containsNot i]
  with g' is_eq have g': "g' = subdivFace' g f v 0 (tl is)"
    by (simp  add: subdivFace_subdivFace'_eq)
  from pre_add is_eq have "is ≠ []"
    by (simp add: pre_subdivFace_def pre_subdivFace_face_def)
  with pre_add v is_eq
  have "pre_subdivFace' g f v v 0 (tl is)"
    by(fastforce simp add:neq_Nil_conv elim:pre_subdivFace_pre_subdivFace')
  from P[OF mgp this fg] g' show ?thesis by simp
qed

lemma next_plane0_incr:
assumes Ptrans: "⋀x y z. Q x y ⟹ P y z ⟹ P x z"
and mkFin: "⋀f g. f ∈ ℱ g ⟹ ¬ final f ⟹ P g (makeFaceFinal f g)"
and fdg_incr: "⋀g u v f vs.
   pre_splitFace g u v f vs ⟹
   Q g (snd(snd(splitFace g u v f vs)))"
and mgp: "minGraphProps g" and gg': "g [next_plane0⇘p⇙]→ g'"
shows "P g g'"
apply(rule next_plane0_via_subdivFace'[OF mgp gg'])
apply(rule subdivFace'_incr)
     apply(erule (1) Ptrans)
    apply(erule (1) mkFin)
   apply(erule fdg_incr)
  apply assumption+
done

(* End of interlude *)

subsubsection‹Increasing number of faces›

lemma splitFace_incr_faces:
 "pre_splitFace g u v f vs ⟹
 finals(snd(snd(splitFace g u v f vs))) = finals g ∧
       |nonFinals(snd(snd(splitFace g u v f vs)))| = Suc |nonFinals g|"
apply(unfold pre_splitFace_def)
apply(simp add: splitFace_def split_def finals_def nonFinals_def
      split_face_def filter_replace2 length_filter_replace2)
done


lemma subdivFace'_incr_faces:
 "pre_subdivFace' g f u v n ovs ⟹
  minGraphProps g ⟹  f ∈ ℱ g ⟹
  |finals (subdivFace' g f v n ovs)| = Suc |finals g| ∧
  |nonFinals(subdivFace' g f v n ovs)| ≥ |nonFinals g| - Suc 0"
apply(rule subdivFace'_incr)
prefer 4 apply assumption
prefer 4 apply assumption
prefer 4 apply assumption
prefer 2
apply(simp add: pre_subdivFace'_def len_finals_makeFaceFinal
      len_nonFinals_makeFaceFinal)
prefer 2
apply(erule splitFace_incr_faces)
apply (rule conjI)
 apply simp
apply arith
done


lemma next_plane0_incr_faces:
 "minGraphProps g ⟹ g [next_plane0⇘p⇙]→ g' ⟹
 |finals g'| = |finals g|+1 ∧ |nonFinals g'| ≥ |nonFinals g| - 1"
apply simp
apply(rule next_plane0_incr)
prefer 4 apply assumption
prefer 4 apply assumption
prefer 2
apply(simp add: pre_subdivFace'_def len_finals_makeFaceFinal
      len_nonFinals_makeFaceFinal)
prefer 2
apply(erule splitFace_incr_faces)
apply (rule conjI)
 apply simp
apply arith
done

lemma two_faces_subdivFace':
  "pre_subdivFace' g f u v n ovs ⟹ minGraphProps g ⟹ f ∈ ℱ g ⟹
  |faces g| ≥ 2 ⟹ |faces(subdivFace' g f v n ovs)| ≥ 2"
apply(drule (2) subdivFace'_incr_faces)
using len_faces_sum[of g] len_faces_sum[of "subdivFace' g f v n ovs"] by arith

subsection‹Main invariant theorems›

lemma inv_genPoly:
assumes inv: "inv g" and polygen: "g' ∈ set(generatePolygon i v f g)"
and f: "f ∈ set (nonFinals g)" and i: "2 < i" and v: "v ∈ 𝒱 f"
shows "inv g'"
proof(unfold inv_def)
  have mgp: "minGraphProps g" and 1: "one_final g"
    using inv by(simp add:inv_def)+
  from polygen
  obtain "is" e where g': "g' = subdivFace g f is"
    and e: "e ∈ set (enumerator i |vertices f| )"
    and containsNot: "¬ containsDuplicateEdge g f v e"
    and is_eq: "is = indexToVertexList f v e"
    by (auto simp: generatePolygon_def)
  have f': "f ∈ ℱ g" using f by(simp add:nonFinals_def)
  note pre_add = pre_subdivFace_indexToVertexList[OF mgp f v e containsNot i]
  with g' is_eq have g': "g' = subdivFace' g f v 0 (tl is)"
    by (simp  add: subdivFace_subdivFace'_eq)
  from pre_add is_eq have i_nz: "is ≠ []"
    by (simp add: pre_subdivFace_def pre_subdivFace_face_def)
  with pre_add v i_nz is_eq
  have pre_addSnd: "pre_subdivFace' g f v v 0 (tl is)"
    by(fastforce simp add:neq_Nil_conv elim:pre_subdivFace_pre_subdivFace')
  note 2 = one_final_antimono[OF 1]
  show "minGraphProps g' ∧ one_final g' ∧ |faces g'| ≥ 2"
  proof auto
    show "minGraphProps g'" using g' pre_addSnd f
      apply (simp add:nonFinals_def)
      apply (rule subdivFace'_holds_minGraphProps[OF _ _ mgp])
      by (simp_all add: succs)
  next
    show "one_final g'" using g' 1
      by (simp add: one_final_subdivFace'[OF pre_addSnd mgp f' 2])
  next
    show "|faces g'| ≥ 2" using g'
      by (simp add: two_faces_subdivFace'[OF pre_addSnd mgp f' inv_two_faces[OF inv]])
  qed
qed


lemma inv_inv_next_plane0: "invariant inv next_plane0⇘p⇙"
proof(clarsimp simp:invariant_def)
  fix g g'
  assume  inv: "inv g" and "g' ∈ set (next_plane0⇘p⇙ g)"
  then obtain i v f where "g' ∈ set(generatePolygon i v f g)"
    and "f ∈ set (nonFinals g)" and "2 < i" and "v ∈ 𝒱 f"
    by (auto simp: next_plane0_def split: if_split_asm)
  thus "inv g'" using inv by(blast intro:inv_genPoly)
qed

end