# Theory Invariants

Up to index of Isabelle/HOL/Tame

theory Invariants
imports FaceDivisionProps
begin

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

header{* Invariants of (Plane) Graphs *}

theory Invariants
imports FaceDivisionProps
begin

subsection{* Rotation of face into normal form *}

constdefs minVertex :: "face => vertex"
"minVertex f ≡ minList (vertices f)"

(* FIXME define normFace via rotate_min *)
constdefs normFace :: "face => vertex list"
"normFace ≡ λf. verticesFrom f (minVertex f)"

constdefs normFaces :: "face list => vertex list list"
"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 *}

constdefs minGraphProps' :: "graph => bool"
"minGraphProps' g ≡ ∀f ∈ \<F> g. 2 < |vertices f| ∧ distinct (vertices f)"

constdefs edges_sym:: "graph => bool"
"edges_sym g ≡ ∀ a b. (a,b) ∈ edges g --> (b,a) ∈ edges g"

constdefs faceListAt_len:: "graph => bool"
"faceListAt_len g ≡ (length (faceListAt g) = countVertices g)"

constdefs facesAt_eq:: "graph => bool"
"facesAt_eq g ≡ ∀v ∈ \<V> g. set(facesAt g v) = {f. f ∈ \<F> g ∧ v ∈ \<V> f}"

constdefs facesAt_distinct:: "graph => bool"
"facesAt_distinct g ≡ ∀v ∈ \<V> g. distinct (normFaces (facesAt g  v))"

constdefs faces_distinct:: "graph => bool"
"faces_distinct g ≡ distinct (normFaces (faces g))"

constdefs faces_subset:: "graph => bool"
"faces_subset g ≡ ∀f ∈ \<F> g. \<V> f ⊆ \<V> g"

constdefs edges_disj :: "graph => bool"
"edges_disj g ≡
∀f ∈ \<F> g. ∀f' ∈ \<F> g. f ≠ f' --> \<E> f ∩ \<E> f' = {}"

constdefs
face_face_op:: "graph => bool"
"face_face_op g ≡ |faces g| ≠ 2 -->
(∀f∈\<F> g. ∀f'∈\<F> g. f ≠ f' --> \<E> f ≠ (\<E> f')¯)"

constdefs
one_final_but :: "graph => (vertex × vertex)set => bool"
"one_final_but g E ≡
∀f ∈ \<F> g. ¬ final f -->
(∀(a,b)∈\<E> f - E. (b,a) : E ∨ (∃f'∈\<F> g. final f' ∧ (b,a) ∈ \<E> f'))"

one_final :: "graph => bool"
"one_final g ≡ one_final_but g {}"

constdefs
minGraphProps :: "graph => bool"
"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"

inv :: "graph => bool"
"inv g ≡ minGraphProps g ∧ one_final g ∧ |faces g| ≥ 2"

lemma facesAt_distinctI:
"(!!v. v ∈ \<V> g ==> distinct (normFaces (facesAt g  v))) ==> facesAt_distinct g"

(* minGraphProps' *)
lemma minGraphProps2: "minGraphProps g ==>
f ∈ \<F> g ==> 2 < |vertices f|"
by (unfold minGraphProps_def minGraphProps'_def) auto

lemma mgp_vertices3:
"minGraphProps g ==> f ∈ \<F> g ==> |vertices f| ≥ 3"
by(auto dest:minGraphProps2)

lemma mgp_vertices_nonempty:
"minGraphProps g ==> f ∈ \<F> g ==> vertices f ≠ []"
by(auto dest:minGraphProps2)

lemma minGraphProps3: "minGraphProps g ==>
f ∈ \<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; f ∈ set (facesAt g v)|] ==> f ∈ \<F> g"
by(auto simp: facesAt_def facesAt_eq_def minGraphProps_def minGraphProps'_def
faceListAt_len_def split:split_if_asm)

lemma minGraphProps6:
"minGraphProps g ==> f ∈ set (facesAt g v) ==> v ∈ \<V> f"
by(auto simp: facesAt_def facesAt_eq_def minGraphProps_def minGraphProps'_def
faceListAt_len_def split:split_if_asm)

(* faces_subset *)
lemma minGraphProps9: "minGraphProps g ==>
f ∈ \<F> g ==> v ∈ \<V> f ==> v ∈ \<V> g"
by (unfold minGraphProps_def faces_subset_def) auto

lemma minGraphProps7: "minGraphProps g ==>
f ∈ \<F> g ==> v ∈ \<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 ∈ \<V> g ==> set (facesAt g v) = {f ∈ \<F> g. v ∈ \<V> f}"

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

lemma minGraphProps8: "minGraphProps 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 ∈ \<V> g ==> distinct (normFaces (faceListAt g ! v))"
apply (frule minGraphProps8[where v=v]) by (simp add: facesAt_def)

lemma minGraphProps8a': "minGraphProps g ==>
v < countVertices g ==> distinct (normFaces (faceListAt g ! v))"

lemma minGraphProps9': "minGraphProps g ==>
f ∈ \<F> g ==> v ∈ \<V> f ==> v < countVertices g"

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

lemma face_eq_if_normFace_eq:
"[| minGraphProps g; f ∈ \<F> g; f' ∈ \<F> g; normFace f = normFace f' |]
==> f = f'"
apply(drule minGraphProps11)
apply(blast dest:inj_onD)
done

lemma minGraphProps12:
"minGraphProps g ==> f ∈ \<F> g ==> (a,b) ∈ \<E> f ==> (b,a) ∉ \<E> 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 ∈ \<F> g ==> v ∈ \<V> f ==>  f ∈ set (faceListAt g ! v)"
apply (frule minGraphProps7) apply assumption+
by (simp add: facesAt_def split: split_if_asm)

(* edges_disj *)
lemma mgp_edges_disj:
"[| minGraphProps g; f ≠ f'; f ∈ \<F> g; f' ∈ \<F> g |] ==>
uv ∈ \<E> f ==> uv ∉ \<E> f'"

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

lemma inv_mgp[simp]: "inv g ==> minGraphProps g"

lemma makeFaceFinal_id[simp]: "final f ==> makeFaceFinal f g = g"
apply(induct g)
setFinal_eq_iff[THEN iffD2])
done

lemma inv_one_finalD':
"[| inv g; f ∈ \<F> g; ¬ final f; (a,b) ∈ \<E> f |] ==>
∃f' ∈ \<F> g. final f' ∧ f' ≠ f ∧ (b,a) ∈ \<E> 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

lemmas minGraphProps_simps = minGraphProps4

lemma mgp_no_loop[simp]:
"minGraphProps g ==> f ∈ \<F> g ==> v ∈ \<V> f ==> f • v ≠ v"
apply(frule (1) mgp_vertices3)
apply(frule (1) minGraphProps3)
done

lemma mgp_facesAt_no_loop:
"minGraphProps g ==> f ∈ set (facesAt g v) ==> f • v ≠ v"
by(blast dest:mgp_no_loop minGraphProps5 minGraphProps6)

lemma edge_pres_faceAt:
"[| minGraphProps g; f ∈ set(facesAt g u); (u,v) ∈ \<E> 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 ==> f ∈ set(facesAt g v) ==> f ∈ set(facesAt g (f • v))"
apply(subgoal_tac "(v,f • v) ∈ \<E> f")
apply(blast intro:edge_pres_faceAt)
by(blast intro: nextVertex_in_edges minGraphProps)

lemma mgp_edge_face_ex:
assumes [intro]: "minGraphProps g"
and fv: "f ∈ set(facesAt g v)" and uv: "(u,v) ∈ \<E> f"
shows "∃f' ∈ set(facesAt g v). (v,u) ∈ \<E> f'"
proof -
from fv have "f ∈ \<F> g" by(blast intro:minGraphProps)
with uv have "(u,v) ∈ \<E> g" by(auto simp:edges_graph_def)
hence "(v,u) ∈ \<E> g" by(blast intro:minGraphProps10)
then obtain f' where f': "f' ∈ \<F> g" and vu: "(v,u) ∈ \<E> f'"
by(auto simp:edges_graph_def)
from vu have "v ∈ \<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 mgp_nextVertex_face_ex2:
assumes mgp[intro]: "minGraphProps 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) ∈ \<E> f"
by(blast intro: nextVertex_in_edges minGraphProps)
with in_facesAt_nextVertex[OF mgp f]
obtain f' where "f' ∈ set(facesAt g (f • v))"
and "(f • v,v) ∈ \<E> f'"
by(blast dest: mgp_edge_face_ex[OF mgp])
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 clarify
apply(rename_tac f fs)
apply(case_tac "final f")
apply simp
apply(frule mgp_vertices_nonempty[OF inv_mgp])
apply fastsimp
apply(clarsimp simp:neq_Nil_conv)
apply(rename_tac v vs)
apply(subgoal_tac "v ∈ \<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} *}

constdefs containsUnacceptableEdgeSnd' :: "(nat => nat => bool) => nat list => bool"
"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: "!! v. containsUnacceptableEdgeSnd N v is = containsUnacceptableEdgeSnd' N (v#is)"
proof (induct "is")
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: split_if_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 (subgoal_tac "is = a # list") apply (thin_tac "a # list = is")
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 (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")

lemma containsDuplicateEdge_eq: "containsDuplicateEdge = containsDuplicateEdge'"
apply (rule ext)+

declare Nat.diff_is_0_eq' [simp del]

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

consts replacefacesAt2 :: "nat list => face => face list => face list list => face list list"
primrec "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]:
"!!F. replacefacesAt ns oldf newfs F =  replacefacesAt2 ns oldf newfs F"
apply (induct ns)

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

lemma replacefacesAt2_in:
"!!Fss i. i ∈ set is ==> distinct is ==> i < |Fss| ==>
(replacefacesAt2 is olfF newFs Fss)!i = replace 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
next
assume "i ∈ set js" "i ≠ j" with Cons show ?thesis by simp
qed
qed

lemma distinct_replacefacesAt21:
"!!i. 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
next
assume "i ∈ set js" "i ≠ j" with Cons show ?thesis
qed
qed

lemma distinct_replacefacesAt22:
"!!i. 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
qed

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

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

lemma replacefacesAt2_nth1: "!!F. k ∉ set ns ==>
(replacefacesAt2 ns oldf newfs F) ! k  =  F ! k"
apply (induct ns) by auto

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

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

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

lemma replacefacesAt2_replacefacesAt2_nth1:
"!!F. k < | F | ==> k ∉ set ns ==> distinct ms ==>
replacefacesAt2 ms oldf' newfs' (replacefacesAt2 ns oldf newfs F)  ! k  =
replacefacesAt2 ms oldf' newfs' F ! k"
proof (induct ms)
case Nil then show ?case by (simp add: replacefacesAt2_nth1)
next
case (Cons m ms) then show ?case
apply (case_tac "m = k") apply (simp) apply safe
apply (simp) apply (rule impI) apply safe
apply (case_tac "k ∈ set ms")  apply (simp add: replacefacesAt2_nth1')
qed

lemma replacefacesAt2_nth: "!!F. 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)
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 add:  replacefacesAt2_nth1) by simp
qed

lemma replacefacesAt_notin:
"!!Fss. i ∉ set is ==> (replacefacesAt is olfF newFs Fss)!i = Fss!i"

lemma replacefacesAt_in:
"!!Fss i. i ∈ set is ==> distinct is ==> i < |Fss| ==>
(replacefacesAt is olfF newFs Fss)!i = replace olfF newFs (Fss !i)"

lemma distinct_replacefacesAt1:
"!!i. i < |Fss| ==> i ∈ set is ==> distinct is ==> distinct (Fss!i) ==> distinct newFs ==>
set (Fss ! i) ∩ set newFs ⊆ {olfF} ==>
distinct ((replacefacesAt is olfF newFs Fss)! i)"

lemma distinct_replacefacesAt2:
"!!i. i < |Fss| ==> i ∉ set is ==> distinct is ==> distinct (Fss!i) ==> distinct newFs ==>
set (Fss ! i) ∩ set newFs ⊆ {olfF} ==>
distinct ((replacefacesAt is olfF newFs Fss)! i)"

lemma distinct_replacefacesAt:
"!!i. i < |Fss| ==> distinct is ==> distinct (Fss!i) ==> distinct newFs ==>
set (Fss ! i) ∩ set newFs ⊆ {olfF} ==>
distinct ((replacefacesAt is olfF newFs Fss)! i)"

lemma replacefacesAt_length[simp]: "|replacefacesAt nvs f' [f''] vs| = |vs|"

lemma replacefacesAt_nth1: "k ∉ set ns ==>
(replacefacesAt ns oldf newfs F) ! k  =  F ! k"

lemma  replacefacesAt_nth1': "k ∈ set ns ==> k < |F| ==> distinct ns ==>
(replacefacesAt ns oldf newfs F) ! k  =  (replace oldf newfs (F!k))"

lemma replacefacesAt_nth2: "k < |F| ==>
(replacefacesAt [k] oldf newfs F) ! k = replace oldf newfs (F!k)"

lemma replacefacesAt_replacefacesAt_nth1:
"k < | F | ==> k ∉ set ns ==> distinct ms ==>
replacefacesAt ms oldf' newfs' (replacefacesAt ns oldf newfs F)  ! k  =
replacefacesAt ms oldf' newfs' F ! k"

lemma replacefacesAt_nth: "!!F. 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))"

lemma replacefacesAt2_5: "!! F. x ∈ set (replacefacesAt2 ns oldf newfs F ! k) ==> x ∈ set (F!k) ∨ x ∈ set newfs"
proof (induct ns)
case Nil then show ?case by simp
next
case (Cons n ns)
then show ?case apply(simp add: split: split_if_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 replacefacesAt5: "!! F. x ∈ set (replacefacesAt ns oldf newfs F ! k) ==> x ∈ set (F!k) ∨ x ∈ set newfs"

lemma replacefacesAt_delete_oldF: "oldF ∉ set newfs ==> distinct (F!k) ==> k ∈ set ns ==> distinct newfs ==>
oldF ∈ set (F ! k) --> set newfs ∩ set (F ! k) ⊆ {oldF} ==> k < |F| ==>
oldF ∉ set (replacefacesAt ns oldF newfs F ! k)"
apply (frule replacefacesAt_nth) apply (simp_all)

lemma replacefacesAt_Nil[simp]: "replacefacesAt [] f fs F = F"

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

lemmas replacefacesAt_simps = replacefacesAt_Nil replacefacesAt_Cons

lemma len_nth_repAt[simp]:
"!!xs. i < |xs| ==> |replacefacesAt is x [y] xs ! i| = |xs!i|"

subsection{*@{const normFace}*}

(************************** minList & minVertex **********************)

lemma minVertex_in: "vertices f ≠ [] ==> minVertex f ∈ \<V> f"

lemma minVertex_eq_if_vertices_eq:
"\<V> f = \<V> f' ==> minVertex f = minVertex f'"
apply(induct f)
apply(induct f')
apply(rename_tac vs ft vs' ft')
apply(case_tac "vs = []")
apply(subgoal_tac "vs' ≠ []")
prefer 2 apply clarsimp
insert_absorb del:Min_insert)
done

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

lemma normFace_eq_if_edges_eq:
"[| distinct(vertices f); distinct(vertices f'); \<E> f = \<E> f' |]
==> normFace f = normFace f'"
apply(subgoal_tac "vertices f ≅ vertices f'")
prefer 2
apply(rule cong_if_is_nextElem_eq)
apply assumption+
apply(subgoal_tac "\<V> f = \<V> f'")
apply(frule minVertex_eq_if_vertices_eq)
apply(cases "vertices f = []")
apply(cases "vertices f' = []")
apply(simp)
apply(subgoal_tac "minVertex f' ∈ \<V> f'")
prefer 2 apply(erule minVertex_in)
apply(subgoal_tac "minVertex f ∈ \<V> f")
prefer 2 apply(erule minVertex_in)
apply(erule (2) verticesFrom_eq_if_vertices_cong)
apply simp
done

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 (simp add: normFaces_def split:split_if_asm) by auto

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 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. 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
next
assume "i ∈ set js" "i ≠ j" with Cons show ?thesis
qed
qed

lemma distinct_replacefacesAt2_norm:
"!!i. 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
qed

lemma distinct_replacefacesAt_norm:
"!!i. 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))"
apply  (cases "i ∈ set is")
by (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 (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

lemma normFace_neq: "a ∈ \<V> f ==> a ∉ \<V> f' ==> vertices f' ≠ [] ==> normFace f ≠ normFace f'"
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 (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 ∈ \<V> oldF") apply assumption apply (simp add: pre_split_face_def) apply simp

apply (rule normFace_neq)
apply (subgoal_tac "a ∈ \<V> (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 ∈ \<V> (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)"

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 safe
apply (case_tac "f ∈ \<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:
"pre_splitFace g ram1 ram2 oldF newVs ==>
minGraphProps g ==>
(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs ==>
f12 ∉ \<F> g"
proof -
assume props: "minGraphProps g"
assume pre: "pre_splitFace g ram1 ram2 oldF newVs"
assume spl: "(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs"
show ?thesis
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)
by (auto simp: Nil[symmetric])
ultimately show ?thesis by (auto simp add: edges_graph_def)
next
case (Cons v vs)
with pre have "v ∉ \<V> g"
apply (unfold pre_splitFace_def) by auto
moreover from Cons spl have "v ∈ \<V> f12"
moreover note props
ultimately show ?thesis by (auto dest: minGraphProps)
qed
qed

lemma splitFace_new_f12_norm:
"pre_splitFace g ram1 ram2 oldF newVs ==>
minGraphProps g ==>
(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs ==>
normFace f12 ∉ set (normFaces (faces g))"
proof -
assume props: "minGraphProps g"
assume pre: "pre_splitFace g ram1 ram2 oldF newVs"
assume spl: "(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs"
show ?thesis
proof (cases newVs)
case Nil with pre have "(ram2, ram1) ∉ edges g"
by (unfold pre_splitFace_def) auto
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)
by (auto simp: Nil[symmetric])
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 assumption+ apply (elim bexE)
apply (subgoal_tac "(ram2, ram1) ∈ edges f'") apply simp
apply (subgoal_tac "(vertices f12) ≅ (vertices f')")  apply (frule congs_distinct)
next
case (Cons v vs)
with pre have "v ∉ \<V> g"
apply (unfold pre_splitFace_def) by auto
moreover from Cons spl have "v ∈ \<V> f12"
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 ∈ \<V> f'") apply (simp add: minGraphProps9)
apply (simp add: congs_pres_nodes cong_face_def) by auto
qed
qed

lemma splitFace_new_f21:
"pre_splitFace g ram1 ram2 oldF newVs ==>
minGraphProps g ==>
(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs ==>
f21 ∉ \<F> g"
proof -
assume props: "minGraphProps g"
assume pre: "pre_splitFace g ram1 ram2 oldF newVs"
assume spl: "(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs"
show ?thesis
proof (cases newVs)
case Nil with pre have "(ram1, ram2) ∉ edges g"
by (unfold pre_splitFace_def) auto
moreover from Nil pre
have "(ram1, ram2) ∈ edges f21"
apply (rule_tac splitFace_empty_ram1_ram2_in_f21)
by (auto simp: Nil[symmetric])
ultimately show ?thesis by (auto simp add: edges_graph_def)
next
case (Cons v vs)
with pre have "v ∉ \<V> g"
apply (unfold pre_splitFace_def) by auto
moreover from Cons spl have "v ∈ \<V> f21"
moreover note props
ultimately show ?thesis by (auto dest: minGraphProps)
qed
qed

lemma splitFace_new_f21_norm:
"pre_splitFace g ram1 ram2 oldF newVs ==>
minGraphProps g ==>
(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs ==>
normFace f21 ∉ set (normFaces (faces g))"
proof -
assume props: "minGraphProps g"
assume pre: "pre_splitFace g ram1 ram2 oldF newVs"
assume spl: "(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs"
show ?thesis
proof (cases newVs)
case Nil with pre have "(ram1, ram2) ∉ edges g"
by (unfold pre_splitFace_def) auto
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)
by (auto simp: Nil[symmetric])
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 assumption+ apply (elim bexE)
apply (subgoal_tac "(ram1, ram2) ∈ edges f'") apply simp
apply (subgoal_tac "(vertices f21) ≅ (vertices f')")  apply (frule congs_distinct)
next
case (Cons v vs)
with pre have "v ∉ \<V> g"
apply (unfold pre_splitFace_def) by auto
moreover from Cons spl have "v ∈ \<V> f21"
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 ∈ \<V> f'") apply (simp add: minGraphProps9)
apply (simp add: congs_pres_nodes cong_face_def) by auto
qed
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"
apply (frule splitFace_new_f21)
by (auto)

lemma splitFace_f21_oldF_neq_norm:
"pre_splitFace g ram1 ram2 oldF newVs ==>
minGraphProps g ==>
(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs ==>
normFace oldF ≠ normFace f21"
apply (frule splitFace_new_f21_norm) apply simp  apply simp
apply (subgoal_tac "normFace oldF ∈ set (normFaces (faces g))") apply force
apply (rule normFace_in) by (simp)

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"
apply (frule splitFace_new_f12)
by(auto)

lemma splitFace_f12_oldF_neq_norm:
"pre_splitFace g ram1 ram2 oldF newVs ==>
minGraphProps g ==>
(f12, f21, newGraph) = splitFace g ram1 ram2 oldF newVs ==>
normFace oldF ≠ normFace f12"
apply (frule splitFace_new_f12_norm) apply simp apply simp
apply (subgoal_tac "normFace oldF ∈ set (normFaces (faces g))") apply force
apply (rule normFace_in) by (simp)

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 ∈ \<F> newGraph ∧ f21 ∈ \<F> 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
apply force
apply (rule disjI2)
apply (erule replace3[OF pre_splitFace_oldF])
apply simp
apply (frule splitFace_holds_minGraphProps') apply (simp add: minGraphProps_def minGraphProps'_def)

lemma set_faces_splitFace:
"[| minGraphProps g; f ∈ \<F> g; pre_splitFace g v1 v2 f vs;
(f1, f2, g') = splitFace g v1 v2 f vs |]
==> \<F> g' = {f1,f2} ∪ (\<F> 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:
"pre_splitFace g v w f [countVertices g..<countVertices g + n] ==>
minGraphProps g ==>
facesAt_distinct (snd (snd (splitFace g v w f [countVertices g..<countVertices g + n])))"
proof -
assume pre: "pre_splitFace g v w f [countVertices g..<countVertices g + n]"
and mgp: "minGraphProps g"
def ws ≡  "[countVertices g..<countVertices g + n]"
def f21 ≡ "snd (split_face f v w ws)"
with pre ws_def have dist_f21: "distinct (vertices f21)" by (auto intro: split_face_distinct2)
def f12 ≡ "fst (split_face f v w ws)"
with pre ws_def have dist_f12: "distinct (vertices f12)" by (auto intro: split_face_distinct1)
def vs1 ≡ "between (vertices f) v w"
def vs2 ≡ "between (vertices f) w v"
def 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]"
from pre mgp fdg have new_f12: "f12 ∉ \<F> g"
apply (rule_tac splitFace_new_f12)  by simp_all
from pre mgp fdg have new_f21: "f21 ∉ \<F> 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 ∈ \<V> g'"
show "distinct (normFaces (facesAt g' x))"
proof -
from mgp pre have a: "v < |faceListAt g|" "w < |faceListAt g|"
apply (unfold pre_splitFace_def)
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 (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 (subgoal_tac "set (faceListAt g ! w) = {f ∈ \<F> g. w ∈ \<V> f}") apply simp
apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f12} = {}")
apply (simp add: f12_def ws_def normFaces_def) apply blast

apply (frule minGraphProps_facesAt_eq)
apply (subgoal_tac "w ∈ \<V> g") apply assumption
apply (rule minGraphProps9) apply assumption apply blast apply simp
apply (simp add: facesAt_def split: split_if_asm)

apply (subgoal_tac "w ∉ set (between (vertices f) v w)")
apply (subgoal_tac "set (faceListAt g ! w) = {f ∈ \<F> g. w ∈ \<V> f}")
apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f21} = {}")
apply (simp add: f21_def ws_def normFaces_def) apply blast

apply (frule minGraphProps_facesAt_eq)
apply (subgoal_tac "w ∈ \<V> 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 (subgoal_tac "w ∉ set (between (vertices f) v w)")
apply (subgoal_tac "set (faceListAt g ! w) = {f ∈ \<F> g. w ∈ \<V> 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 (frule minGraphProps_facesAt_eq)
apply (subgoal_tac "w ∈ \<V> 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 (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 (subgoal_tac "set (faceListAt g ! v) = {f ∈ \<F> g. v ∈ \<V> f}")
apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f12} = {}")
apply (simp add: f12_def ws_def normFaces_def) apply blast

apply (frule minGraphProps_facesAt_eq)
apply (subgoal_tac "v ∈ \<V> g") apply assumption
apply (rule minGraphProps9) apply assumption apply blast apply simp
apply (simp add: facesAt_def split: split_if_asm)

apply (subgoal_tac "v ∉ set (between (vertices f) v w)")
apply (subgoal_tac "set (faceListAt g ! v) = {f ∈ \<F> g. v ∈ \<V> f}")
apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f21} = {}")
apply (simp add: f21_def ws_def normFaces_def) apply blast

apply (frule minGraphProps_facesAt_eq)
apply (subgoal_tac "v ∈ \<V> g") apply assumption
apply (rule minGraphProps9) apply assumption apply blast apply simp
apply (simp add: facesAt_def split: split_if_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 (subgoal_tac "v ∉ set (between (vertices f) v w)")
apply (subgoal_tac "set (faceListAt g ! v) = {f ∈ \<F> g. v ∈ \<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 (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f21} = {}")
apply (frule minGraphProps_facesAt_eq)
apply (subgoal_tac "v ∈ \<V> g") apply assumption
apply (rule minGraphProps9) apply assumption apply blast apply simp
apply (simp add: facesAt_def minGraphProps4 vertices_graph)
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 (case_tac "x < |faceListAt g|")
apply simp
apply (subgoal_tac "x ∈ \<V> 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 (subgoal_tac "set (faceListAt g ! x) = {f ∈ \<F> g. x ∈ \<V> f}")
apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f12} = {}")
apply (simp add: f12_def ws_def normFaces_def) apply blast

apply (frule minGraphProps_facesAt_eq) apply assumption
apply (simp add: facesAt_def split: split_if_asm)

apply (case_tac "x ∉ set (between (vertices f) v w)")
apply (subgoal_tac "set (faceListAt g ! x) = {f ∈ \<F> g. x ∈ \<V> f}")
apply (subgoal_tac "set (normFaces (faces g)) ∩ {normFace f21} = {}")
apply (simp add: f21_def ws_def normFaces_def) apply blast

apply (frule minGraphProps_facesAt_eq) apply assumption
apply (simp add: facesAt_def split: split_if_asm)
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 force
apply (rule normFaces_distinct)
apply (rule minGraphProps8a) apply assumption apply (simp add: minGraphProps4 vertices_graph)
apply (rule impI) apply simp
apply (subgoal_tac "set (faceListAt g ! x) = {f ∈ \<F> g. x ∈ \<V> f}")
apply (subgoal_tac "\<F> g ∩ {f12} = {}")
apply (simp add: f12_def ws_def) apply blast
apply (frule minGraphProps_facesAt_eq)
apply (subgoal_tac "x ∈ \<V> g") apply assumption
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 force
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 ∈ \<F> g. x ∈ \<V> f}")
apply (subgoal_tac "\<F> g ∩ {f12} = {}")
apply (simp add: f12_def ws_def) apply blast
apply (frule minGraphProps_facesAt_eq)
apply (subgoal_tac "x ∈ \<V> g") apply assumption
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 (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 (rule ccontr) apply simp
apply (subgoal_tac "normFace f21 ∉ set (normFaces (facesAt g x))")
apply (subgoal_tac "x ∈ \<V> g") apply (simp add: normFaces_def)
apply (subgoal_tac "normFace f21 ∉ set (normFaces (faces g))") apply (frule minGraphProps_facesAt_eq)
apply (subgoal_tac "x ∈ \<V> 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)

(* zweite große Implikation *)
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)
apply (simp add: minGraphProps4) by arith
qed
qed
qed
qed
then show ?thesis by (simp add: g'_def)
qed

lemma splitFace_holds_facesAt_eq:
"pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n] ==>
minGraphProps g'  ==>
g'' = (snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n]))) ==>
facesAt_eq g''"
proof -
assume 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])))"
have "[0..<countVertices g''] = [0..<countVertices g' + n]"
hence vg'': "vertices g'' = [0..<countVertices g' + n]" by (simp add:vertices_graph)

def ws ≡  "[countVertices g'..<countVertices g' + n]"
def f21 ≡  "snd (split_face f' v a ws)"
def f12 ≡ "fst (split_face f' v a ws)"
def vs1 ≡ "between (vertices f') v a"
def 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"
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': "\<V> 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]"

from mgp have dist_all: "!!x. x ∈ \<V> 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'"

from ws_def [symmetric] f21_def [symmetric] f12_def [symmetric]
vs1_def [symmetric] vs2_def [symmetric] pre_F mgp vert_f' show ?thesis
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.simps split:split_if_asm)
apply (case_tac "v < |faceListAt g'| ∧ a < | faceListAt g'|")
apply (simp only: nth_append split: split_if_asm)
apply (case_tac "va < | faceListAt g' |")
apply (subgoal_tac "va ∈ \<V> 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 (subgoal_tac "distinct (faceListAt g' ! va)")
apply (subgoal_tac "distinct (faces g')")
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 simp apply (fastsimp simp: facesAt_def)
apply (rule minGraphProps6) apply simp 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 (case_tac "v = va")
apply (subgoal_tac "distinct (faceListAt g' ! va)")
apply (subgoal_tac "distinct (faces g')")
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 simp apply (fastsimp simp: facesAt_def)
apply (rule minGraphProps6) apply simp apply (fastsimp 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 (case_tac "va ∈ set vs1")
apply (subgoal_tac "va ∉ set vs2")
apply (subgoal_tac "distinct (faceListAt g' ! va)")
apply (subgoal_tac "distinct (faces g')")
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 simp apply (fastsimp simp: facesAt_def)
apply (rule minGraphProps6) apply simp apply (fastsimp 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 blast
apply (case_tac "va ∈ set vs2")
apply (subgoal_tac "distinct (faceListAt g' ! va)")
apply (subgoal_tac "distinct (faces g')")
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 simp apply (fastsimp simp: facesAt_def)
apply (rule minGraphProps6) apply simp apply (fastsimp 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
(* case else *)
apply (subgoal_tac "distinct (faceListAt g' ! va)")
apply (subgoal_tac "distinct (faces g')")
apply (case_tac "x = f'")
apply (subgoal_tac "va ∈ \<V> f'") apply simp apply (rule minGraphProps6) apply simp
apply (rule conjI)
apply (rule disjI2) apply (rule disjI2)
apply (rule minGraphProps5) apply simp apply (fastsimp simp: facesAt_def)
apply (rule minGraphProps6) apply simp apply(fastsimp 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 (subgoal_tac "distinct (vertices f12) ∧ distinct (vertices 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
(* va in ws *)
apply simp
apply (subgoal_tac "distinct (faces g')")
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 arith
apply (rule minGraphProps11') apply simp
apply (subgoal_tac "v ∈ \<V> g' ∧ a ∈ \<V> g'")
apply (simp only: fla in_vertices_graph)
apply (subgoal_tac "f' ∈ \<F> g'")
apply (subgoal_tac "v ∈ \<V> f' ∧ a ∈ \<V> 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)
apply simp

(* Rückrichtung *)
apply (rule subsetI)
apply (case_tac "v < |faceListAt g'| ∧ a < | faceListAt g'|")
apply (case_tac "va < | faceListAt g' |")
apply (subgoal_tac "va ∈ \<V> 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 (subgoal_tac "distinct (faceListAt g' ! va)")
apply (subgoal_tac "distinct (faces g')")
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 "v = va")
apply (subgoal_tac "distinct (faceListAt g' ! va)")
apply (subgoal_tac "distinct (faces g')")
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 (subgoal_tac "distinct (faceListAt g' ! va)")
apply (subgoal_tac "distinct (faces g')")
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 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 (subgoal_tac "distinct (faceListAt g' ! va)")
apply (subgoal_tac "distinct (faces g')")
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 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 (subgoal_tac "distinct (faces g')")
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 (case_tac "x = f12") apply (simp add: vert_f12) apply (thin_tac "[countVertices g'..<countVertices g' + n] ≡ ws")
apply simp apply simp apply (rule minGraphProps11') apply simp
apply (subgoal_tac "distinct (vertices f12) ∧ distinct (vertices 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 (subgoal_tac "distinct (faces g')")
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 ∈ \<V> g'") apply (simp add: fla vertices_graph)
apply (rule minGraphProps9) apply simp apply force apply simp
apply (simp add: ws_def fla) apply arith
apply (rule minGraphProps11') apply simp
apply (subgoal_tac "v ∈ \<V> g' ∧ a ∈ \<V> g'")
apply (simp only: fla in_vertices_graph)
apply (subgoal_tac "f' ∈ \<F> g'")
apply (subgoal_tac "v ∈ \<V> f' ∧ a ∈ \<V> 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
by (simp only: pre_splitFace_def)
qed

lemma splitFace_holds_faces_subset:
"pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n] ==>
minGraphProps g' ==>
faces_subset (snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))"
proof -
assume pre_F: "pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n]"
and mgp: "minGraphProps g'"
def g'' ≡  "(snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))"
def ws ≡  "[countVertices g'..<countVertices g' + n]"
def f21 ≡  "snd (split_face f' v a ws)"
def f12 ≡ "fst (split_face f' v a ws)"
def vs1 ≡ "between (vertices f') v a"
def 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"
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': "\<V> 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]"

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 "\<V> f' ⊆ \<V> 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:
"pre_splitFace g' v a f' ws ==>
minGraphProps g' ==>
edges_sym (snd (snd (splitFace g' v a f' ws)))"
proof -
assume pre_F: "pre_splitFace g' v a f' ws"
and mgp: "minGraphProps g'"
def g'' ≡  "(snd (snd (splitFace g' v a f' ws)))"
def f21 ≡  "snd (split_face f' v a ws)"
def f12 ≡ "fst (split_face f' v a ws)"
def vs1 ≡ "between (vertices f') v a"
def 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"
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]"

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:
"pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n] ==>
minGraphProps g' ==>
faces_distinct (snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))"
proof -
assume pre_F: "pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n]"
and mgp: "minGraphProps g'"
def g'' ≡  "(snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))"
def ws ≡  "[countVertices g'..<countVertices g' + n]"
def f21 ≡  "snd (split_face f' v a ws)"
def f12 ≡ "fst (split_face f' v a ws)"
def vs1 ≡ "between (vertices f') v a"
def 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"
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]"
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 (subgoal_tac "distinct (normFaces (replace f' [f21] (faces g')))")
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 (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 (subgoal_tac "normFace f21 ∉ set (normFaces (faces g'))")
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; (f1, f2) = split_face f a b vs; |vertices f| ≥ 3;
vs = [] --> (a,b) ∉ edges f ∧ (b,a) ∉ edges f |]
==> \<E> f1 ∩ \<E> f2 = {}"
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 ∈ \<V> f ==> x ≠ y")
prefer 2 apply blast
apply(subgoal_tac "!!x y. x ∈ set vs ==> y ∈ \<V> 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 ∉ \<V> f")
prefer 2 apply(drule hd_in_set) apply blast
apply(subgoal_tac "vs ≠ [] ==> last vs ∉ \<V> 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) ∈ \<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) ∈ \<V> f")
prefer 2 apply(drule last_in_set) apply(drule inbetween_inset) apply blast
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: "(f1,f2,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 "\<V> g ∩ set vs = {}" using pre
hence gvs: "∀f ∈ \<F> g. \<V> f ∩ set vs = {}"
by (clarsimp simp:edges_graph_def edges_face_def)
(blast dest: minGraphProps9[OF mgp])
have f: "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 "\<E> f1 ∩ \<E> f2 = {}"
apply(rule split_face_edge_disj[OF pre_split_face split_face mgp_vertices3[OF mgp f]])
using pre
apply clarify
by(simp) (* loops if combined *)
moreover
{ fix f' assume f': "f' ∈ \<F> g" "f' ≠ f"
have "(\<E> f1 ∪ \<E> f2) ∩ \<E> f' = {}"
proof cases
assume vs: "vs = []"
have "(u,v) ∉ \<E> g ∧ (v,u) ∉ \<E> g" using pre vs
with split_face_edges_f12_f21_vs[OF pre_split_face[simplified vs] split_face[simplified vs]]
show ?thesis using f f' disj
next
assume vs: "vs ≠ []"
have f12: "vs ≠ [] ==> \<E> f1 ∪ \<E> f2 ⊆
\<E> f ∪ UNIV × set vs ∪ set vs × UNIV"
using split_face_edges_f12_f21[OF pre_split_face split_face]
by simp (fastsimp dest:in_Edges_in_set)
have "!!x y. (y,x) ∈ \<E> 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
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 f1 = "fst(splitFace g u v f vs)" and f2 = "fst(snd(splitFace g u v f vs))"], auto)

lemma vertices_conv_Union_edges2:
"distinct(vertices f) ==> \<V>(f::face) = (\<Union>(a,b)∈\<E> 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: "(f1,f2,g') = splitFace g u v f vs"
shows "face_face_op g'"
proof -
have f12: "(f1, f2) = split_face f u v vs"
and Fg': "\<F> g' = {f1} ∪ set(replace f [f2] (faces g))"
and g': "g' = snd (snd (splitFace g u v f vs))" using fdg
have f1: "f1= fst(split_face f u v vs)" and f2: "f2 = 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 distf1 = split_face_distinct1[OF f12 pre_split]
note distf2 = split_face_distinct2[OF f12 pre_split]
from pre have nf: "¬ final f" and fg: "f ∈ \<F> g" and nuv: "u ≠ v"
and uinf: "u ∈ \<V> f"and vinf: "v ∈ \<V> f"
and distf: "distinct(vertices f)" and new: "\<V> g ∩ set vs = {}"
by(unfold pre_splitFace_def, simp)+
let ?fuv = "between (vertices f) u v" and ?fvu = "between (vertices f) v u"
have E1: "\<E> f1 = Edges (v # rev vs @ [u]) ∪ Edges (u # ?fuv @ [v])"
have E2: "\<E> f2 = Edges (u # vs @ [v]) ∪ Edges (v # ?fvu @ [u])"
have vf1: "vertices f1 = rev vs @ u # ?fuv @ [v]"
have vf2: "vertices f2 = [v] @ ?fvu @ u # vs"
have V1: "\<V> f1 = {u,v} ∪ set(?fuv) ∪ set(vs)" using vf1 by auto
have V2: "\<V> f2 = {u,v} ∪ set(?fvu) ∪ set(vs)" using vf2 by auto
have 2: "(v,u) ∈ \<E> f1 ∧ (u,v) ∈ \<E> f2 ∧ vs = [] ∨
(∃v ∈ \<V> f1 ∩ \<V> f2. v ∉ \<V> g)"
using E1 E2 V1 V2 new by(cases vs)(simp_all add:Edges_Cons)
have "\<V> f1 ≠ \<V> f2"
proof cases
assume A: "?fvu = []"
have "?fuv ≠ []"
proof
assume "?fuv = []"
with A have "\<E> f = {(v,u),(u,v)}"
using edges_conv_Un_Edges[OF distf uinf vinf nuv]
hence "\<V> f = {u,v}" by(simp add:vertices_conv_Union_edges)
hence "card(\<V> 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 V1 V2 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 V1 V2 by (auto simp:neq_Nil_conv)
qed
have C12: "\<E> f1 ≠ (\<E> f2)¯"
proof
assume A: "\<E> f1 = (\<E> f2)¯"
show False
proof -
have "\<V> f1 = (\<Union>(a,b)∈\<E> f1. {a})"
by(rule vertices_conv_Union_edges)
also have "… = (\<Union>(b,a)∈\<E> f2. {a})" by(auto simp:A)
also have "… = \<V> f2"
by(rule vertices_conv_Union_edges2[OF distf2, symmetric])
finally show False using `\<V> f1 ≠ \<V> f2` by blast
qed
qed
{ fix h :: face assume hg: "h ∈ \<F> g"
have "\<E> h ≠ (\<E> f1)¯ ∧ \<E> h ≠ (\<E> f2)¯" using 2
proof
assume "(v,u) ∈ \<E> f1 ∧ (u,v) ∈ \<E> f2 ∧ vs = []"
moreover hence "(u,v) ∉ \<E> g"
using pre by(unfold pre_splitFace_def)simp
moreover hence "(v,u) ∉ \<E> g" by(blast intro:minGraphProps10[OF mgp])
ultimately show ?thesis using hg by(simp add:edges_graph_def) blast
next
assume "∃x ∈ \<V> f1 ∩ \<V> f2. x ∉ \<V> g"
then obtain x where "x ∈ \<V> f1" and "x ∈ \<V> f2" and "x ∉ \<V> g"
by blast
obtain y where "(x,y) ∈ \<E> f1" using `x ∈ \<V> f1`
by(auto simp:vertices_conv_Union_edges)
moreover obtain z where "(x,z) ∈ \<E> f2" using `x ∈ \<V> f2`
by(auto simp:vertices_conv_Union_edges)
moreover have "¬(EX y. (y,x) ∈ \<E> h)"
using `x ∉ \<V> 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: "\<F> g = {f,f'}"
by(fastsimp simp: nat_number length_Suc_conv)
moreover hence "f ≠ f'" using 2 distinct_card[OF distF] by auto
ultimately have Fg': "\<F> g' = {f1,f2,f'}"
using set_faces_splitFace[OF mgp fg pre fdg] by blast
show ?thesis using Fg' C12 Cg12 Fg
by(fastsimp simp:face_face_op_def)
next
assume "|faces g| ≠ 2"
hence E: "!!f f'. f∈\<F> g ==> f'∈\<F> g ==> f ≠ f' ==> \<E> f ≠ (\<E> f')¯"
thus ?thesis using set_faces_splitFace[OF mgp fg pre fdg] C12 Cg12
by(fastsimp 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 f1 = "fst(splitFace g u v f vs)" and f2 = "fst(snd(splitFace g u v f vs))"], auto)

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

subsection{* Invariants of @{const makeFaceFinal} *}

lemma MakeFaceFinal_minGraphProps':
"f ∈ \<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
by force

lemma MakeFaceFinal_facesAt_eq:
"f ∈ \<F> g ==> minGraphProps g ==> facesAt_eq (makeFaceFinal f g)"
apply (simp add: facesAt_eq_def) apply (rule ballI)
apply (subgoal_tac "v ∈ \<V> g")
apply (rule equalityI) apply (rule subsetI)
apply (subgoal_tac "v < | faceListAt g | ")
apply (subgoal_tac "distinct ((faceListAt g ! v))")
apply (subgoal_tac "distinct (faces g)")
apply (case_tac "x = f") apply simp apply (erule minGraphProps6)
apply (simp add: facesAt_def) apply force apply simp
apply (case_tac " f ∈ set (faceListAt g ! v) ∧ x = setFinal f") apply simp
apply (subgoal_tac "v ∈ \<V> f") apply (simp add: setFinal_def)
apply (erule minGraphProps6) apply (simp add: facesAt_def) apply simp
apply (rule conjI) apply (rule disjI2)
apply (erule minGraphProps5) apply (fastsimp simp: facesAt_def)
apply (erule minGraphProps6) apply (fastsimp simp: facesAt_def)
apply (rule minGraphProps11') apply simp
apply (rule normFaces_distinct) apply (rule minGraphProps8a) apply simp apply simp
(* 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 (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
(* Vorbed v in set (vertices g) *)

lemma MakeFaceFinal_faceListAt_len:
"f ∈ \<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 (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 ∈ \<F> g ==>  minGraphProps g ==> facesAt_distinct (makeFaceFinal f g)"
apply (rule allI) apply (rule impI)
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 ∈ \<F> g ==>  minGraphProps g ==> faces_subset (makeFaceFinal f g)"
apply (simp add: faces_subset_def) apply (intro ballI subsetI)
apply (drule replace5)
apply (case_tac "fa ∈ \<F> g") apply simp apply (rule minGraphProps9')
apply simp apply (thin_tac "f ∈ \<F> g") apply simp+
apply (rule minGraphProps9') apply simp apply simp by (simp add: setFinal_def)

lemma MakeFaceFinal_edges_sym:
"f ∈ \<F> g ==>  minGraphProps g ==> edges_sym (makeFaceFinal f g)"
apply (simp add: edges_sym_def) apply (intro allI impI)
apply (elim bexE) apply (simp add: makeFaceFinalFaceList_def)
apply (subgoal_tac "distinct (faces g)")
apply (case_tac "x ∈ \<F> 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 (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 (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 (rule minGraphProps3) apply simp apply simp
by (rule minGraphProps11')

lemma MakeFaceFinal_faces_distinct:
"f ∈ \<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 ∈ \<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 (fastsimp dest:mgp_edges_disj)
apply (fastsimp dest:mgp_edges_disj)
done

lemma MakeFaceFinal_face_face_op:
"f ∈ \<F> g ==> minGraphProps g ==> face_face_op (makeFaceFinal f g)"
apply(subgoal_tac "face_face_op g")
apply(drule minGraphProps11')
apply(auto simp: face_face_op_def makeFaceFinal_def makeFaceFinalFaceList_def
distinct_set_replace)
done

lemma MakeFaceFinal_minGraphProps:
"f ∈ \<F> g ==> minGraphProps g ==> minGraphProps (makeFaceFinal f g)"
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 ∈ \<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: split_if_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_all
apply (rule splitFace_holds_minGraphProps)
apply simp_all
apply (rule pre_subdivFace'_preFaceDiv)
apply simp_all
qed

(* Invariance of one_final *)

syntax Edges_if :: "face => vertex => vertex => (vertex × vertex)set"
translations
"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: "(f1,f2,g') = splitFace g u v f vs"
and nrv: "r ≠ v"
and ruv: "before (verticesFrom f r) u v" and rf: "r ∈ \<V> f"
and 1: "one_final_but g (Edges_if f r u)"
shows "one_final_but g' (Edges(r # between (vertices f2) r v @ [v]))"
proof -
have f1: "f1= fst(split_face f u v vs)" and f2: "f2 = snd(split_face f u v vs)"
and F: "\<F> g' = {f1} ∪ set(replace f [f2] (faces g))"
and g': "g' = snd (snd (splitFace g u v f vs))" using fdg
note pre_split = pre_splitFace_pre_split_face[OF pre]
from pre have nf: "¬ final f" and fg: "f ∈ \<F> g" and nuv: "u ≠ v"
and uinf: "u ∈ \<V> f"and vinf: "v ∈ \<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 ?f2rv = "between (vertices f2) r v"
have E1: "\<E> f1 = Edges (v # rev vs @ [u]) ∪ Edges (u # ?fuv @ [v])"
have E2: "\<E> f2 = Edges (u # vs @ [v]) ∪ Edges (v # ?fvu @ [u])"
have vf2: "vertices f2 = [v] @ ?fvu @ u # vs"
have vinf2: "v ∈ \<V> f2" using vf2 by(simp)
have rinf2: "r ∈ \<V> f2"
proof cases
assume "r=u" thus ?thesis by(simp add:vf2)
next
assume "r≠u" thus ?thesis by(simp add: vf2 fvu)
qed
have distf2: "distinct(vertices f2)"
have f2uv: "between (vertices f2) u v = vs"
using vf2 distf2 by(simp add:between_def split_def)
have f2ru: "r≠u ==> between (vertices f2) r u = between (vertices f) r u"
using vf2 fvu distf distf2 by(simp add:between_def split_def)
hence f2rv: "between (vertices f2) r v =
(if r=u then [] else ?fru @ [u]) @ vs"
proof cases
assume "r=u" thus ?thesis by(simp add: f2uv)
next
assume nru: "r ≠ u"
have vinf2: "v ∈ \<V> f2" by(simp add: vf2)
note u_bet_rv = before_between[OF ruv distf rf nru]
have u_bet_rv2: "u ∈ set (between (vertices f2) r v)"
using distf2 nru
apply(subst between_def[of _ r v])
done
show ?thesis
by(simp add:split_between[OF distf2 rinf2 vinf2 u_bet_rv2] f2ru f2uv)
qed
have E2rv: "Edges(r # ?f2rv @ [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]))"
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)
case (goal1 a b)
have ab: "(a,b) ∈ \<E> f1"
and nab: "(a,b) ∉ Edges (r # ?f2rv @ [v])" .
have "(a,b) ∈ Edges (v # rev vs @ [u]) ∨
(a,b) ∈ Edges (u # ?fuv @ [v])" (is "?A ∨ ?B")
using E1 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 # ?f2rv @ [v])" using E2rv by simp
thus ?case by blast
next
assume abfuv: ?B
have abf: "(a,b) ∈ \<E> f"
by(rule Edges_between_edges[OF abfuv pre_split])
have "(∃f'∈set(replace f [f2] (faces g)). final f' ∧ (b,a) ∈ \<E> f')"
proof cases
assume "r = u"
then obtain f' where "f' ∈ \<F> g ∧ final f' ∧ (b, a) ∈ \<E> f'"
using abf 1 nf fg by(simp add:one_final_but_def)fast
moreover then have "f' ∈ set (replace f [f2] (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' ∈ \<F> g ∧ final f' ∧ (b, a) ∈ \<E> f'"
using abf 1 nf fg by(simp add:one_final_but_def)fast
moreover hence "f' ∈ set (replace f [f2] (faces g))"
by(clarsimp simp: replace6[OF distFg] nf)
ultimately show ?thesis by blast
qed
thus ?case ..
qed
next
case (goal2  f' a b)
have f': "f' ∈ set (replace f [f2] (faces g))"
and nf': "¬ final f'" and abf': "(a,b) ∈ \<E> f'"
and nab: "(a,b) ∉ Edges (r # between (vertices f2) r v @ [v])" .
have "f' = f2 ∨ f' ∈ \<F> g ∧ f' ≠ f"
using f' by(simp add:replace6[OF distFg]) blast
hence "(b, a) ∈ Edges (r # between (vertices f2) r v @ [v]) ∨
(∃f'∈set (replace f [f2] (faces g)). final f' ∧ (b, a) ∈ \<E> f')"
(is "?A ∨ ?B")
proof
assume [simp]: "f' = f2"
have "(a,b) ∈ Edges (v # between (vertices f2) v r @ [r])"
using abf' nab Edges_compl[OF distf2 vinf2 rinf2 nrv[symmetric]]
edges_conv_Un_Edges[OF distf2 rinf2 vinf2 nrv] by auto
moreover have eq: "between(vertices f2) v r = between (vertices f) v r"
proof (cases "r=u")
assume "r=u" thus ?thesis
next
assume "r≠u" thus ?thesis
by(simp add:vf2 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) ∈ \<E> 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 [f2] (faces g)). final f' ∧ (b,a) ∈ \<E> f')"
proof cases
assume "r = u"
then obtain f' where "f' ∈ \<F> g ∧ final f' ∧ (b, a) ∈ \<E> f'"
using abf 1 nf fg by(simp add:one_final_but_def)fast
moreover then have "f' ∈ set (replace f [f2] (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' ∈ \<F> g ∧ final f' ∧ (b, a) ∈ \<E> f'"
using abf 1 nf fg nru by(simp add:one_final_but_def)fast
moreover hence "f' ∈ set (replace f [f2] (faces g))"
by(clarsimp simp: replace6[OF distFg] nf)
ultimately show ?thesis by blast
qed
thus ?thesis ..
next
assume  f': "f' ∈ \<F> g ∧ f' ≠ f"
moreover
hence "\<E> f' ∩ \<E> f = {}"
using fg by(blast dest: mgp_edges_disj[OF mgp])
moreover
have "Edges_if f r u ⊆ \<E> f"
using distf rf uinf
apply(clarsimp simp del:is_nextElem_edges_eq)
apply(erule Edges_between_edges[where vs = "[]"])
ultimately
have "(b,a) : Edges_if f r u ∨
(∃f''∈\<F> g. final f'' ∧ (b,a) ∈ \<E> f'')" (is "?A ∨ ?B")
using 1 f' nf' abf'
thus ?thesis (is "?A' ∨ ?B'")
proof
assume ?A
moreover
have "Edges_if f r u ⊆ Edges (r # between (vertices f2) r v @ [v])"
using f2rv by (auto simp:Edges_Cons Edges_append)
ultimately have ?A' by blast
thus ?thesis ..
next
assume ?B
then obtain f'' where "f''∈\<F> g ∧ final f'' ∧ (b, a) ∈ \<E> 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 ⊆ \<E> f; f ∈ \<F> g; ¬ final f |] ==>
one_final (makeFaceFinal f g)"
apply(frule minGraphProps11')
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
done

lemma one_final_subdivFace':
"!!f v n g.
pre_subdivFace' g f u v n ovs ==> minGraphProps g ==> f ∈ \<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 []"
hence "Edges(u # between (vertices f) u v @ [v]) ⊆ \<E> f"
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 ∈ \<V> f" and vf: "v ∈ \<V> f"
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"
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)
done
have pre': "pre_subdivFace' g f u w 0 ovs"
using pre Some n by (simp (depth_limit:5) 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: "\<V> f ⊆ \<V> g"
using mgp fg by(simp add: minGraphProps_def faces_subset_def)
have pre_fdg: "pre_splitFace g v w f ?vs"
apply (rule pre_subdivFace'_preFaceDiv[OF _ 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(fastsimp 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])
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 ==> b ∈ set (neighbors g a) = ((a, b) ∈ edges g)"
apply(cases "a ∈ \<V> g")
apply (rule iffI)
apply (simp add: neighbors_def)  apply clarify apply (frule minGraphProps5)
apply (simp add: edges_graph_def) apply (intro bexI)
prefer 2 apply assumption
apply (erule (1) minGraphProps6)
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)
apply(auto simp: neighbors_def image_def edges_graph_def)
apply(blast dest:in_edges_in_vertices  minGraphProps6 minGraphProps9)
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 @{text g}
has no self-loops. *}

lemma duplicateEdge_is_duplicateEdge_eq:
"minGraphProps g ==> f ∈ \<F> g ==> a ∈ \<V> f ==> b ∈ \<V> 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 (simp add: duplicateEdge_def is_duplicateEdge_def neighbors_edges)
apply (rule iffI)
apply (cases "a = b") apply (simp add: no_self_edges minGraphProps_def)
apply (rule ccontr)
apply (case_tac "is_nextElem (vertices f) a b")
apply (cases "a = b") apply (simp add: no_self_edges minGraphProps_def)
apply (rule ccontr)
apply (elim impE)
apply (cases "between (vertices f) b a")
apply simp
apply (cases "between (vertices f) a b")
apply simp
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 drop_Suc_conv_tl) 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..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..z]) Nonfinal) = 0"
apply (induct z) apply (simp add: minVertex_def)

subsection{* Invariants of @{const Seed} *}

lemma Seed_holds_facesAt_distinct: "facesAt_distinct (Seed p)"
facesAt_distinct_def normFaces_def facesAt_def normFace_def)
apply(simp add: nat_number minVertex_zero1 minVertex_zero2 verticesFrom_Def
fst_splitAt_upt snd_splitAt_upt fst_splitAt_rev snd_splitAt_rev 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]"]
apply (fastsimp simp add: Seed_def graph_def edges_disj_def edges_graph_def)
done

lemma Seed_holds_faces_distinct: "faces_distinct (Seed p)"
faces_distinct_def normFaces_def facesAt_def normFace_def)
apply(simp add: nat_number minVertex_zero1 minVertex_zero2 verticesFrom_Def
fst_splitAt_upt snd_splitAt_upt fst_splitAt_rev snd_splitAt_rev 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 Seedp"
by(clarsimp simp:Seed_def one_final_def one_final_but_def graph_def)

lemma two_face_Seed: "|faces Seedp| ≥ 2"

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 ∈ \<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 ∈ \<F> g" "¬ final f" by (auto simp: nonFinals_def)
with mgp have le_vf: "2 < |vertices f|"
from fg mgp have dist_f:"distinct (vertices f)"
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 (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: split_if_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 "fe ! 0 • v ∈ \<V> f")
apply (subgoal_tac "fe ! Suc 0 • v ∈ \<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 fe ! Suc nat • v)")
apply (simp split: split_if_asm)
apply (subgoal_tac "natToVertexList v f e ! Suc (Suc nat) =
(if e ! (Suc nat) = e ! Suc (Suc nat) then None else Some fe ! Suc (Suc nat) • v)")
apply (simp split: split_if_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 "fe ! Suc nat • v ∈ \<V> f")
apply (subgoal_tac "fe ! Suc (Suc nat) • v ∈ \<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 ∈ \<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' ∈ \<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(rule Ptrans)
prefer 2
apply (rule Cons)
apply (erule (1) pre_subdivFace'_Some1[OF _ _ _ _ HOL.refl HOL.refl])
apply simp
apply (rule splitFace_holds_minGraphProps)
apply (erule (1) pre_subdivFace'_preFaceDiv)
apply simp
apply assumption
apply(rule fdg_incr)
apply(erule (1) pre_subdivFace'_preFaceDiv)
apply simp
done
qed

lemma next_plane0_via_subdivFace':
assumes mgp: "minGraphProps g" and gg': "g [next_plane0p]-> g'"
and P: "!!f v' v n g ovs. minGraphProps g ==> pre_subdivFace' g f v' v n ovs ==>
f ∈ \<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 ∈ \<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:split_if_asm)
from f have fg: "f ∈ \<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)"
from pre_add is_eq have "is ≠ []"
have "pre_subdivFace' g f v v 0 (tl is)"
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 ∈ \<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_plane0p]-> 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 ∈ \<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
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_plane0p]-> 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
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 ∈ \<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 ∈ \<V> f"
shows "inv g'"
proof(unfold inv_def)
have mgp: "minGraphProps g" and 1: "one_final g"
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 ∈ \<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)"
from pre_add is_eq have i_nz: "is ≠ []"
have pre_addSnd: "pre_subdivFace' g f v v 0 (tl is)"
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 (rule subdivFace'_holds_minGraphProps[OF _ _ mgp])
next
show "one_final g'" using g' 1
next
show "|faces g'| ≥ 2" using g'
qed
qed

lemma inv_inv_next_plane0: "invariant inv next_plane0p"
proof(clarsimp simp:invariant_def)
fix g g'
assume  inv: "inv g" and "g' ∈ set (next_plane0p g)"
then obtain i v f where "g' ∈ set(generatePolygon i v f g)"
and "f ∈ set (nonFinals g)" and "2 < i" and "v ∈ \<V> f"
by (auto simp: next_plane0_def split: split_if_asm)
thus "inv g'" using inv by(blast intro:inv_genPoly)
qed

end
```

### Rotation of face into normal form

lemma normFaces_distinct:

`  distinct (normFaces fl) ==> distinct fl`

### Minimal (plane) graph properties

lemma facesAt_distinctI:

`  (!!v. v ∈ \<V> g ==> distinct (normFaces (facesAt g v))) ==> facesAt_distinct g`

lemma minGraphProps2:

`  [| minGraphProps g; f ∈ \<F> g |] ==> 2 < |vertices f|`

lemma mgp_vertices3:

`  [| minGraphProps g; f ∈ \<F> g |] ==> 3 ≤ |vertices f|`

lemma mgp_vertices_nonempty:

`  [| minGraphProps g; f ∈ \<F> g |] ==> vertices f ≠ []`

lemma minGraphProps3:

`  [| minGraphProps g; f ∈ \<F> g |] ==> distinct (vertices f)`

lemma minGraphProps4:

`  minGraphProps g ==> |faceListAt g| = countVertices g`

lemma minGraphProps5:

`  [| minGraphProps g; f ∈ set (facesAt g v) |] ==> f ∈ \<F> g`

lemma minGraphProps6:

`  [| minGraphProps g; f ∈ set (facesAt g v) |] ==> v ∈ \<V> f`

lemma minGraphProps9:

`  [| minGraphProps g; f ∈ \<F> g; v ∈ \<V> f |] ==> v ∈ \<V> g`

lemma minGraphProps7:

`  [| minGraphProps g; f ∈ \<F> g; v ∈ \<V> f |] ==> f ∈ set (facesAt g v)`

lemma minGraphProps_facesAt_eq:

```  [| minGraphProps g; v ∈ \<V> g |]
==> set (facesAt g v) = {f : \<F> g. v ∈ \<V> f}```

lemma mgp_dist_facesAt:

`  minGraphProps g ==> distinct (facesAt g v)`

lemma minGraphProps8:

`  minGraphProps g ==> distinct (normFaces (facesAt g v))`

lemma minGraphProps8a:

`  [| minGraphProps g; v ∈ \<V> g |] ==> distinct (normFaces (faceListAt g ! v))`

lemma minGraphProps8a':

```  [| minGraphProps g; v < countVertices g |]
==> distinct (normFaces (faceListAt g ! v))```

lemma minGraphProps9':

`  [| minGraphProps g; f ∈ \<F> g; v ∈ \<V> f |] ==> v < countVertices g`

lemma minGraphProps10:

`  [| minGraphProps g; (a, b) ∈ \<E> g |] ==> (b, a) ∈ \<E> g`

lemma minGraphProps11:

`  minGraphProps g ==> distinct (normFaces (faces g))`

lemma minGraphProps11':

`  minGraphProps g ==> distinct (faces g)`

lemma face_eq_if_normFace_eq:

```  [| minGraphProps g; f ∈ \<F> g; f' ∈ \<F> g; normFace f = normFace f' |]
==> f = f'```

lemma minGraphProps12:

`  [| minGraphProps g; f ∈ \<F> g; (a, b) ∈ \<E> f |] ==> (b, a) ∉ \<E> f`

lemma minGraphProps7':

`  [| minGraphProps g; f ∈ \<F> g; v ∈ \<V> f |] ==> f ∈ set (faceListAt g ! v)`

lemma mgp_edges_disj:

```  [| minGraphProps g; f ≠ f'; f ∈ \<F> g; f' ∈ \<F> g; uv ∈ \<E> f |]
==> uv ∉ \<E> f'```

lemma one_final_but_antimono:

`  [| one_final_but g E; E ⊆ E' |] ==> one_final_but g E'`

lemma one_final_antimono:

`  one_final g ==> one_final_but g E`

lemma inv_two_faces:

`  Invariants.inv g ==> 2 ≤ |faces g|`

lemma inv_mgp:

`  Invariants.inv g ==> minGraphProps g`

lemma makeFaceFinal_id:

`  final f ==> makeFaceFinal f g = g`

lemma inv_one_finalD':

```  [| Invariants.inv g; f ∈ \<F> g; ¬ final f; (a, b) ∈ \<E> f |]
==> ∃f'∈\<F> g. final f' ∧ f' ≠ f ∧ (b, a) ∈ \<E> f'```

lemmas minGraphProps:

`  [| minGraphProps g; f ∈ \<F> g |] ==> 2 < |vertices f|`
`  [| minGraphProps g; f ∈ \<F> g |] ==> distinct (vertices f)`
`  minGraphProps g ==> |faceListAt g| = countVertices g`
`  [| minGraphProps g; f ∈ set (facesAt g v) |] ==> f ∈ \<F> g`
`  [| minGraphProps g; f ∈ set (facesAt g v) |] ==> v ∈ \<V> f`
`  [| minGraphProps g; f ∈ \<F> g; v ∈ \<V> f |] ==> f ∈ set (facesAt g v)`
`  minGraphProps g ==> distinct (normFaces (facesAt g v))`
`  [| minGraphProps g; f ∈ \<F> g; v ∈ \<V> f |] ==> v ∈ \<V> g`

lemmas minGraphProps:

`  [| minGraphProps g; f ∈ \<F> g |] ==> 2 < |vertices f|`
`  [| minGraphProps g; f ∈ \<F> g |] ==> distinct (vertices f)`
`  minGraphProps g ==> |faceListAt g| = countVertices g`
`  [| minGraphProps g; f ∈ set (facesAt g v) |] ==> f ∈ \<F> g`
`  [| minGraphProps g; f ∈ set (facesAt g v) |] ==> v ∈ \<V> f`
`  [| minGraphProps g; f ∈ \<F> g; v ∈ \<V> f |] ==> f ∈ set (facesAt g v)`
`  minGraphProps g ==> distinct (normFaces (facesAt g v))`
`  [| minGraphProps g; f ∈ \<F> g; v ∈ \<V> f |] ==> v ∈ \<V> g`

lemmas minGraphProps_simps:

`  minGraphProps g ==> |faceListAt g| = countVertices g`

lemmas minGraphProps_simps:

`  minGraphProps g ==> |faceListAt g| = countVertices g`

lemma mgp_no_loop:

`  [| minGraphProps g; f ∈ \<F> g; v ∈ \<V> f |] ==> f • v ≠ v`

lemma mgp_facesAt_no_loop:

`  [| minGraphProps g; f ∈ set (facesAt g v) |] ==> f • v ≠ v`

lemma edge_pres_faceAt:

```  [| minGraphProps g; f ∈ set (facesAt g u); (u, v) ∈ \<E> f |]
==> f ∈ set (facesAt g v)```

lemma in_facesAt_nextVertex:

`  [| minGraphProps g; f ∈ set (facesAt g v) |] ==> f ∈ set (facesAt g (f • v))`

lemma mgp_edge_face_ex:

```  [| minGraphProps g; f ∈ set (facesAt g v); (u, v) ∈ \<E> f |]
==> ∃f'∈set (facesAt g v). (v, u) ∈ \<E> f'```

lemma mgp_nextVertex_face_ex2:

```  [| minGraphProps g; f ∈ set (facesAt g v) |]
==> ∃f'∈set (facesAt g (f • v)). f' • (f • v) = v```

lemma inv_finals_nonempty:

`  Invariants.inv g ==> finals g ≠ []`

### @{const containsDuplicateEdge}

lemma containsUnacceptableEdgeSnd_eq:

`  containsUnacceptableEdgeSnd N v is = containsUnacceptableEdgeSnd' N (v # is)`

lemma containsDuplicateEdge_eq1:

`  containsDuplicateEdge g f v is = containsDuplicateEdge' g f v is`

lemma containsDuplicateEdge_eq:

`  containsDuplicateEdge = containsDuplicateEdge'`

### @{const replacefacesAt}

lemma replacefacesAt_eq:

`  replacefacesAt ns1 oldf1 newfs1 F1 == replacefacesAt2 ns1 oldf1 newfs1 F1`

lemma replacefacesAt2_notin:

`  i ∉ set is ==> replacefacesAt2 is olfF newFs Fss ! i = Fss ! i`

lemma replacefacesAt2_in:

```  [| i ∈ set is; distinct is; i < |Fss| |]
==> replacefacesAt2 is olfF newFs Fss ! i = replace olfF newFs (Fss ! i)```

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

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

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

lemma replacefacesAt2_length:

`  |replacefacesAt2 nvs f' [f''] vs| = |vs|`

lemma replacefacesAt2_nth1:

`  k ∉ set ns ==> replacefacesAt2 ns oldf newfs F ! k = F ! k`

lemma replacefacesAt2_nth1':

```  [| k ∈ set ns; k < |F|; distinct ns |]
==> replacefacesAt2 ns oldf newfs F ! k = replace oldf newfs (F ! k)```

lemma replacefacesAt2_nth2:

`  k < |F| ==> replacefacesAt2 [k] oldf newfs F ! k = replace oldf newfs (F ! k)`

lemma replacefacesAt2_length:

`  |replacefacesAt2 nvs f' f'' vs| = |vs|`

lemma replacefacesAt2_replacefacesAt2_nth1:

```  [| k < |F|; k ∉ set ns; distinct ms |]
==> replacefacesAt2 ms oldf' newfs' (replacefacesAt2 ns oldf newfs F) ! k =
replacefacesAt2 ms oldf' newfs' F ! k```

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

lemma replacefacesAt_notin:

`  i ∉ set is ==> replacefacesAt is olfF newFs Fss ! i = Fss ! i`

lemma replacefacesAt_in:

```  [| i ∈ set is; distinct is; i < |Fss| |]
==> replacefacesAt is olfF newFs Fss ! i = replace olfF newFs (Fss ! i)```

lemma distinct_replacefacesAt1:

```  [| i < |Fss|; i ∈ set is; distinct is; distinct (Fss ! i); distinct newFs;
set (Fss ! i) ∩ set newFs ⊆ {olfF} |]
==> distinct (replacefacesAt is olfF newFs Fss ! i)```

lemma distinct_replacefacesAt2:

```  [| i < |Fss|; i ∉ set is; distinct is; distinct (Fss ! i); distinct newFs;
set (Fss ! i) ∩ set newFs ⊆ {olfF} |]
==> distinct (replacefacesAt is olfF newFs Fss ! i)```

lemma distinct_replacefacesAt:

```  [| i < |Fss|; distinct is; distinct (Fss ! i); distinct newFs;
set (Fss ! i) ∩ set newFs ⊆ {olfF} |]
==> distinct (replacefacesAt is olfF newFs Fss ! i)```

lemma replacefacesAt_length:

`  |replacefacesAt nvs f' [f''] vs| = |vs|`

lemma replacefacesAt_nth1:

`  k ∉ set ns ==> replacefacesAt ns oldf newfs F ! k = F ! k`

lemma replacefacesAt_nth1':

```  [| k ∈ set ns; k < |F|; distinct ns |]
==> replacefacesAt ns oldf newfs F ! k = replace oldf newfs (F ! k)```

lemma replacefacesAt_nth2:

`  k < |F| ==> replacefacesAt [k] oldf newfs F ! k = replace oldf newfs (F ! k)`

lemma replacefacesAt_replacefacesAt_nth1:

```  [| k < |F|; k ∉ set ns; distinct ms |]
==> replacefacesAt ms oldf' newfs' (replacefacesAt ns oldf newfs F) ! k =
replacefacesAt ms oldf' newfs' F ! k```

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

lemma replacefacesAt2_5:

```  x ∈ set (replacefacesAt2 ns oldf newfs F ! k)
==> x ∈ set (F ! k) ∨ x ∈ set newfs```

lemma replacefacesAt5:

`  x ∈ set (replacefacesAt ns oldf newfs F ! k) ==> x ∈ set (F ! k) ∨ x ∈ set newfs`

lemma replacefacesAt_delete_oldF:

```  [| oldF ∉ set newfs; distinct (F ! k); k ∈ set ns; distinct newfs;
oldF ∈ set (F ! k) --> set newfs ∩ set (F ! k) ⊆ {oldF}; k < |F| |]
==> oldF ∉ set (replacefacesAt ns oldF newfs F ! k)```

lemma replacefacesAt_Nil:

`  replacefacesAt [] f fs F = F`

lemma replacefacesAt_Cons:

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

lemmas replacefacesAt_simps:

`  replacefacesAt [] f fs F = F`
```  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)```

lemmas replacefacesAt_simps:

`  replacefacesAt [] f fs F = F`
```  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)```

lemma len_nth_repAt:

`  i < |xs| ==> |replacefacesAt is x [y] xs ! i| = |xs ! i|`

### @{const normFace}

lemma minVertex_in:

`  vertices f ≠ [] ==> minVertex f ∈ \<V> f`

lemma minVertex_eq_if_vertices_eq:

`  \<V> f = \<V> f' ==> minVertex f = minVertex f'`

lemma normFace_eq_if_edges_eq:

```  [| distinct (vertices f); distinct (vertices f'); \<E> f = \<E> f' |]
==> normFace f = normFace f'```

lemma normFace_replace_in:

```  normFace a ∈ set (normFaces (replace oldF newFs fs))
==> normFace a ∈ set (normFaces newFs) ∨ normFace a ∈ set (normFaces fs)```

lemma distinct_replace_norm:

```  [| distinct (normFaces fs); distinct (normFaces newFs);
set (normFaces fs) ∩ set (normFaces newFs) ⊆ {} |]
==> distinct (normFaces (replace oldF newFs fs))```

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

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

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

lemma normFace_in_cong:

```  [| vertices f ≠ []; minGraphProps g; normFace f ∈ set (normFaces (faces g)) |]
==> ∃f'∈\<F> g. f ≅ f'```

lemma normFace_neq:

`  [| a ∈ \<V> f; a ∉ \<V> f'; vertices f' ≠ [] |] ==> normFace f ≠ normFace f'`

lemma split_face_f12_f21_neq_norm:

```  [| pre_split_face oldF ram1.0 ram2.0 vs; 2 < |vertices oldF|;
2 < |vertices f12.0|; 2 < |vertices f21.0|;
(f12.0, f21.0) = split_face oldF ram1.0 ram2.0 vs |]
==> normFace f12.0 ≠ normFace f21.0```

lemma normFace_in:

`  f ∈ set fs ==> normFace f ∈ set (normFaces fs)`

### Invariants of @{const splitFace}

lemma splitFace_holds_minGraphProps':

```  [| pre_splitFace g' v a f' vs; minGraphProps' g' |]
==> minGraphProps' (snd (snd (splitFace g' v a f' vs)))```

lemma splitFace_holds_faceListAt_len:

```  [| pre_splitFace g' v a f' vs; minGraphProps g' |]
==> faceListAt_len (snd (snd (splitFace g' v a f' vs)))```

lemma splitFace_new_f12:

```  [| pre_splitFace g ram1.0 ram2.0 oldF newVs; minGraphProps g;
(f12.0, f21.0, newGraph) = splitFace g ram1.0 ram2.0 oldF newVs |]
==> f12.0 ∉ \<F> g```

lemma splitFace_new_f12_norm:

```  [| pre_splitFace g ram1.0 ram2.0 oldF newVs; minGraphProps g;
(f12.0, f21.0, newGraph) = splitFace g ram1.0 ram2.0 oldF newVs |]
==> normFace f12.0 ∉ set (normFaces (faces g))```

lemma splitFace_new_f21:

```  [| pre_splitFace g ram1.0 ram2.0 oldF newVs; minGraphProps g;
(f12.0, f21.0, newGraph) = splitFace g ram1.0 ram2.0 oldF newVs |]
==> f21.0 ∉ \<F> g```

lemma splitFace_new_f21_norm:

```  [| pre_splitFace g ram1.0 ram2.0 oldF newVs; minGraphProps g;
(f12.0, f21.0, newGraph) = splitFace g ram1.0 ram2.0 oldF newVs |]
==> normFace f21.0 ∉ set (normFaces (faces g))```

lemma splitFace_f21_oldF_neq:

```  [| pre_splitFace g ram1.0 ram2.0 oldF newVs; minGraphProps g;
(f12.0, f21.0, newGraph) = splitFace g ram1.0 ram2.0 oldF newVs |]
==> oldF ≠ f21.0```

lemma splitFace_f21_oldF_neq_norm:

```  [| pre_splitFace g ram1.0 ram2.0 oldF newVs; minGraphProps g;
(f12.0, f21.0, newGraph) = splitFace g ram1.0 ram2.0 oldF newVs |]
==> normFace oldF ≠ normFace f21.0```

lemma splitFace_f12_oldF_neq:

```  [| pre_splitFace g ram1.0 ram2.0 oldF newVs; minGraphProps g;
(f12.0, f21.0, newGraph) = splitFace g ram1.0 ram2.0 oldF newVs |]
==> oldF ≠ f12.0```

lemma splitFace_f12_oldF_neq_norm:

```  [| pre_splitFace g ram1.0 ram2.0 oldF newVs; minGraphProps g;
(f12.0, f21.0, newGraph) = splitFace g ram1.0 ram2.0 oldF newVs |]
==> normFace oldF ≠ normFace f12.0```

lemma splitFace_f12_f21_neq_norm:

```  [| pre_splitFace g ram1.0 ram2.0 oldF vs; minGraphProps g;
(f12.0, f21.0, newGraph) = splitFace g ram1.0 ram2.0 oldF vs |]
==> normFace f12.0 ≠ normFace f21.0```

lemma set_faces_splitFace:

```  [| minGraphProps g; f ∈ \<F> g; pre_splitFace g v1.0 v2.0 f vs;
(f1.0, f2.0, g') = splitFace g v1.0 v2.0 f vs |]
==> \<F> g' = {f1.0, f2.0} ∪ (\<F> g - {f})```

lemma splitFace_holds_facesAt_distinct:

```  [| pre_splitFace g v w f [countVertices g..<countVertices g + n];
minGraphProps g |]
==> facesAt_distinct
(snd (snd (splitFace g v w f [countVertices g..<countVertices g + n])))```

lemma splitFace_holds_facesAt_eq:

```  [| pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n];
minGraphProps g';
g'' =
snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])) |]
==> facesAt_eq g''```

lemma splitFace_holds_faces_subset:

```  [| pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n];
minGraphProps g' |]
==> faces_subset
(snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))```

lemma splitFace_holds_edges_sym:

```  [| pre_splitFace g' v a f' ws; minGraphProps g' |]
==> edges_sym (snd (snd (splitFace g' v a f' ws)))```

lemma splitFace_holds_faces_distinct:

```  [| pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n];
minGraphProps g' |]
==> faces_distinct
(snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))```

lemma help(1):

`  [| xs ≠ []; x ∉ set xs |] ==> x ≠ hd xs`

and help(2):

`  [| xs ≠ []; x ∉ set xs |] ==> x ≠ last xs`

and help(3):

`  [| xs ≠ []; x ∉ set xs |] ==> hd xs ≠ x`

and help(4):

`  [| xs ≠ []; x ∉ set xs |] ==> last xs ≠ x`

lemma split_face_edge_disj:

```  [| pre_split_face f a b vs; (f1, f2) = split_face f a b vs; 3 ≤ |vertices f|;
vs = [] --> (a, b) ∉ \<E> f ∧ (b, a) ∉ \<E> f |]
==> \<E> f1 ∩ \<E> f2 = {}```

lemma splitFace_edge_disj:

```  [| minGraphProps g; pre_splitFace g u v f vs;
(f1, f2, g') = splitFace g u v f vs |]
==> edges_disj g'```

lemma splitFace_edges_disj2:

```  [| minGraphProps g; pre_splitFace g u v f vs |]
==> edges_disj (snd (snd (splitFace g u v f vs)))```

lemma vertices_conv_Union_edges2:

`  distinct (vertices f) ==> \<V> f = (UN (a, b):\<E> f. {b})`

lemma splitFace_face_face_op:

```  [| minGraphProps g; pre_splitFace g u v f vs;
(f1, f2, g') = splitFace g u v f vs |]
==> face_face_op g'```

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

lemma splitFace_holds_minGraphProps:

```  [| pre_splitFace g' v a f' [countVertices g'..<countVertices g' + n];
minGraphProps g' |]
==> minGraphProps
(snd (snd (splitFace g' v a f' [countVertices g'..<countVertices g' + n])))```

### Invariants of @{const makeFaceFinal}

lemma MakeFaceFinal_minGraphProps':

`  [| f ∈ \<F> g; minGraphProps g |] ==> minGraphProps' (makeFaceFinal f g)`

lemma MakeFaceFinal_facesAt_eq:

`  [| f ∈ \<F> g; minGraphProps g |] ==> facesAt_eq (makeFaceFinal f g)`

lemma MakeFaceFinal_faceListAt_len:

`  [| f ∈ \<F> g; minGraphProps g |] ==> faceListAt_len (makeFaceFinal f g)`

lemma normFaces_makeFaceFinalFaceList:

`  normFaces (makeFaceFinalFaceList f fs) = normFaces fs`

lemma MakeFaceFinal_facesAt_distinct:

`  [| f ∈ \<F> g; minGraphProps g |] ==> facesAt_distinct (makeFaceFinal f g)`

lemma MakeFaceFinal_faces_subset:

`  [| f ∈ \<F> g; minGraphProps g |] ==> faces_subset (makeFaceFinal f g)`

lemma MakeFaceFinal_edges_sym:

`  [| f ∈ \<F> g; minGraphProps g |] ==> edges_sym (makeFaceFinal f g)`

lemma MakeFaceFinal_faces_distinct:

`  [| f ∈ \<F> g; minGraphProps g |] ==> faces_distinct (makeFaceFinal f g)`

lemma MakeFaceFinal_edges_disj:

`  [| f ∈ \<F> g; minGraphProps g |] ==> edges_disj (makeFaceFinal f g)`

lemma MakeFaceFinal_face_face_op:

`  [| f ∈ \<F> g; minGraphProps g |] ==> face_face_op (makeFaceFinal f g)`

lemma MakeFaceFinal_minGraphProps:

`  [| f ∈ \<F> g; minGraphProps g |] ==> minGraphProps (makeFaceFinal f g)`

### Invariants of @{const subdivFace'}

lemma subdivFace'_holds_minGraphProps:

```  [| pre_subdivFace' g f v' v n ovl; f ∈ \<F> g; minGraphProps g |]
==> minGraphProps (subdivFace' g f v n ovl)```

lemma FaceDivsionGraph_one_final_but:

```  [| minGraphProps g; pre_splitFace g u v f vs;
(f1, f2, g') = splitFace g u v f vs; r ≠ v; before (verticesFrom f r) u v;
r ∈ \<V> f;
one_final_but g
(if r = u then {} else Edges (r # between (vertices f) r u @ [u])) |]
==> one_final_but g' (Edges (r # between (vertices f2) r v @ [v]))```

lemma one_final_but_makeFaceFinal:

```  [| minGraphProps g; one_final_but g E; E ⊆ \<E> f; f ∈ \<F> g; ¬ final f |]
==> one_final (makeFaceFinal f g)```

lemma one_final_subdivFace':

```  [| pre_subdivFace' g f u v n ovs; minGraphProps g; f ∈ \<F> g;
one_final_but g
(if u = v then {} else Edges (u # between (vertices f) u v @ [v])) |]
==> one_final (subdivFace' g f v n ovs)```

lemma neighbors_edges:

`  minGraphProps g ==> (b ∈ set (neighbors g a)) = ((a, b) ∈ \<E> g)`

lemma no_self_edges:

`  minGraphProps' g ==> (a, a) ∉ \<E> g`

lemma duplicateEdge_is_duplicateEdge_eq:

```  [| minGraphProps g; f ∈ \<F> g; a ∈ \<V> f; b ∈ \<V> f |]
==> duplicateEdge g f a b = is_duplicateEdge g f a b```

lemma incrIndexList_less_eq:

`  [| incrIndexList ls m nmax; Suc n < |ls| |] ==> ls ! n ≤ ls ! Suc n`

lemma incrIndexList_less:

```  [| incrIndexList ls m nmax; Suc n < |ls|; ls ! n ≠ ls ! Suc n |]
==> ls ! n < ls ! Suc n```

lemma Seed_holds_minGraphProps':

`  minGraphProps' Seedp`

lemma Seed_holds_facesAt_eq:

`  facesAt_eq Seedp`

lemma minVertex_zero1:

`  minVertex (Face [0..z] Final) = 0`

lemma minVertex_zero2:

`  minVertex (Face (rev [0..z]) Nonfinal) = 0`

### Invariants of @{const Seed}

lemma Seed_holds_facesAt_distinct:

`  facesAt_distinct Seedp`

lemma Seed_holds_faces_subset:

`  faces_subset Seedp`

lemma Seed_holds_edges_sym:

`  edges_sym Seedp`

lemma Seed_holds_edges_disj:

`  edges_disj Seedp`

lemma Seed_holds_faces_distinct:

`  faces_distinct Seedp`

lemma Seed_holds_faceListAt_len:

`  faceListAt_len Seedp`

lemma face_face_op_Seed:

`  face_face_op Seedp`

lemma one_final_Seed:

`  one_final Seedp`

lemma two_face_Seed:

`  2 ≤ |faces Seedp|`

lemma inv_Seed:

`  Invariants.inv Seedp`

lemma pre_subdivFace_indexToVertexList:

```  [| minGraphProps g; f ∈ set (nonFinals g); v ∈ \<V> f;
e ∈ set (enumerator i |vertices f|); ¬ containsDuplicateEdge g f v e;
2 < i |]
==> pre_subdivFace g f v (indexToVertexList f v e)```

### Increasing properties of @{const subdivFace'}

lemma subdivFace'_incr:

```  [| !!x y z. [| Q x y; P y z |] ==> P x z;
!!f g. [| f ∈ \<F> g; ¬ final f |] ==> P g (makeFaceFinal f g);
!!g u v f vs.
pre_splitFace g u v f vs ==> Q g (snd (snd (splitFace g u v f vs)));
pre_subdivFace' g f' v' v n ovl; minGraphProps g; f' ∈ \<F> g |]
==> P g (subdivFace' g f' v n ovl)```

lemma next_plane0_via_subdivFace':

```  [| minGraphProps g; g' ∈ set (next_plane0p g);
!!f v' v n g ovs.
[| minGraphProps g; pre_subdivFace' g f v' v n ovs; f ∈ \<F> g |]
==> P g (subdivFace' g f v n ovs) |]
==> P g g'```

lemma next_plane0_incr:

```  [| !!x y z. [| Q x y; P y z |] ==> P x z;
!!f g. [| f ∈ \<F> g; ¬ final f |] ==> P g (makeFaceFinal f g);
!!g u v f vs.
pre_splitFace g u v f vs ==> Q g (snd (snd (splitFace g u v f vs)));
minGraphProps g; g' ∈ set (next_plane0p g) |]
==> P g g'```

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

lemma subdivFace'_incr_faces:

```  [| pre_subdivFace' g f u v n ovs; minGraphProps g; f ∈ \<F> g |]
==> |finals (subdivFace' g f v n ovs)| = Suc |finals g| ∧
|nonFinals g| - Suc 0 ≤ |nonFinals (subdivFace' g f v n ovs)|```

lemma next_plane0_incr_faces:

```  [| minGraphProps g; g' ∈ set (next_plane0p g) |]
==> |finals g'| = |finals g| + 1 ∧ |nonFinals g| - 1 ≤ |nonFinals g'|```

lemma two_faces_subdivFace':

```  [| pre_subdivFace' g f u v n ovs; minGraphProps g; f ∈ \<F> g; 2 ≤ |faces g| |]
==> 2 ≤ |faces (subdivFace' g f v n ovs)|```

### Main invariant theorems

lemma inv_genPoly:

```  [| Invariants.inv g; g' ∈ set (generatePolygon i v f g); f ∈ set (nonFinals g);
2 < i; v ∈ \<V> f |]
==> Invariants.inv g'```

lemma inv_inv_next_plane0:

`  invariant Invariants.inv next_plane0p`