# Theory Plane3Props

Up to index of Isabelle/HOL/Tame

theory Plane3Props
imports Plane1Props Generator TameProps
begin

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

theory Plane3Props
imports Plane1Props Generator TameProps
begin

subsection{* Correctness *}

lemma decomp_nonFinal3:
assumes mgp: "minGraphProps g"
and ffs: "f#fs = [f ∈ faces g. ¬ final f ∧ triangle f]"
shows "f = minimalFace(nonFinals g) &
fs = [f ∈ faces(makeFaceFinal (minimalFace(nonFinals g)) g).
¬ final f ∧ triangle f]" (is "?A & ?B")
proof -
have 3: "∀f ∈ \<F> g. 3 ≤ |vertices f|"
using minGraphProps2[OF mgp] by fastsimp
have ffs': "f#fs = [f ∈ nonFinals g. triangle f]" using ffs
from Cons_eq_filterD[OF ffs'] obtain us vs where
[simp]: "nonFinals g = us @ f # vs" "triangle f"
"fs = [f∈vs . triangle f]" and us: "∀u∈set us. ¬ triangle u"
by blast
have "∀u ∈ set(nonFinals g). u ∈ \<F> g" by(simp add:nonFinals_def)
hence usg: "∀u∈set us. u ∈ \<F> g"
and vsg: "∀u∈set vs. u ∈ \<F> g" by simp+
let ?m = "size o vertices"
have us3: "∀u∈set us. |vertices u| > 3"
proof
fix f' assume "f' ∈ set us"
thus "|vertices f'| > 3"
using bspec[OF us, of f'] bspec[OF 3, of f'] bspec[OF usg, of f']
by simp
qed
have A: ?A
proof -
have "minimal ?m (us @ f # vs) = minimal ?m (f # vs)"
using us3 by(simp add: minimal_append2)
also have "… = f" using 3 vsg
by (rule_tac minimal_Cons1) simp
finally show ?A by(simp add: minimalFace_def)
qed
moreover have ?B (is "?l = ?r")
proof -
have "?r = [h ∈ faces (makeFaceFinal f g) . ¬ final h ∧ triangle h]"
using A by simp
also have "… = [h ∈ nonFinals (makeFaceFinal f g). triangle h]"
also have "… = [h ∈ remove1 f (nonFinals g). triangle h]"
also have "… = [h ∈ vs. triangle h]"
proof -
have "f ∉ set us" using us by auto
thus ?thesis using us by(simp add:remove1_append)
qed
finally show ?B by simp
qed
ultimately show ?thesis ..
qed

lemma noDupEdge3:
"[| minGraphProps g; f ∈ \<F> g; triangle f; v ∈ \<V> f |]
==> ¬ containsDuplicateEdge g f v [0..<3]"
apply(frule (1) minGraphProps3)
apply(drule length3D)
apply auto
apply(simp add: containsDuplicateEdge_eq containsDuplicateEdge'_def
nat_number nextVertices_def nextVertex_def
duplicateEdge_is_duplicateEdge_eq is_duplicateEdge_def is_nextElem_def)
apply(simp add:is_sublist_rec[where 'a = nat])
apply(simp add: containsDuplicateEdge_eq containsDuplicateEdge'_def
nat_number nextVertices_def nextVertex_def
duplicateEdge_is_duplicateEdge_eq is_duplicateEdge_def is_nextElem_def)
apply(simp add: containsDuplicateEdge_eq containsDuplicateEdge'_def
nat_number nextVertices_def nextVertex_def
duplicateEdge_is_duplicateEdge_eq is_duplicateEdge_def is_nextElem_def)
apply(simp add:is_sublist_rec[where 'a = nat])
done

lemma indexToVs3:
"[| triangle f; distinct(vertices f); v ∈ \<V> f |]
==> indexToVertexList f v [0..<3] = [Some v, Some(f • v), Some(f • (f • v))]"
apply(auto dest!: length3D)
apply(auto simp:indexToVertexList_def nat_number
nextVertices_def nextVertex_def)
done

lemma upt3_in_enumerator: "[0..<3] ∈ set (enumerator 3 3)"
apply(simp only:enumerator_def incrIndexList_def enumBase_def)
done

lemma mkFaceFin3_in_succs1:
assumes mgp: "minGraphProps g"
and ffs: "f#fs = [f ∈ faces g. ¬ final f ∧ triangle f]"
shows "Graph (makeFaceFinalFaceList f (faces g)) (countVertices g)
(map (makeFaceFinalFaceList f) (faceListAt g)) (heights g)
∈ set (next_planep g)" (is "?g' ∈ _")
proof -
have "¬ final g" using Cons_eq_filterD[OF ffs]
by(auto simp: finalGraph_def nonFinals_def)
moreover have "?g' ∈ set (generatePolygon 3 (minimalVertex g f) f g)"
proof -
have [simp]: "|vertices f| = 3" and fg: "f ∈ \<F> g"
using Cons_eq_filterD[OF ffs] by auto
have "vertices f ≠ []" by (auto simp:length_0_conv[symmetric])
hence min: "minimalVertex g f ∈ \<V> f"  by(simp add:minimalVertex_def)
note upt3_in_enumerator noDupEdge3[OF mgp fg _ min]
moreover have
"?g' = subdivFace g f (indexToVertexList f (minimalVertex g f) [0..<3])"
using min minGraphProps3[OF mgp fg]
by(simp add:indexToVs3 makeFaceFinal_def subdivFace_def)
ultimately show ?thesis
by (fastsimp simp:generatePolygon_def image_def del:enumerator_equiv)
qed
moreover have "f = minimalFace (nonFinals g)"
using decomp_nonFinal3[OF mgp ffs] by simp
ultimately show ?thesis by(auto simp add:next_plane_def finalGraph_def)
qed

lemma mkFaceFin3_in_rtrancl:
"minGraphProps g ==> f#fs = [f ∈ faces g . ¬ final f ∧ triangle f] ==>
g [next_planep]->* makeFaceFinal f g"
apply(rule RTranCl.succs[OF _ RTranCl.refl])
apply(erule (1) mkFaceFin3_in_succs1)
done

lemma mk3Fin_lem:
"!!g. minGraphProps g ==> fs = [f ∈ faces g. ¬ final f ∧ triangle f] ==>
g [next_planep]->* foldl (%g f. makeFaceFinal f g) g fs"
proof(induct fs)
case Nil show ?case by (simp add:RTranCl.refl)
next
case (Cons f fs)
let ?g = "makeFaceFinal f g"
note mkFaceFin3_in_rtrancl[OF Cons(2-3)] moreover
have "?g [next_planep]->* foldl (%g f. makeFaceFinal f g) ?g fs"
using Cons_eq_filterD[OF Cons(3)] Cons(2)
by(rule_tac Cons(1)[OF MakeFaceFinal_minGraphProps])
(auto simp: makeFaceFinal_def makeFaceFinalFaceList_def pre_subdivFace'_def)
ultimately show ?case by(rule_tac RTranCl_compose) auto
qed

lemma mk3Fin_in_RTranCl:
"inv g ==> g [next_planep]->* makeTrianglesFinal g"

subsection "Completeness"

constdefs
"in2finals g a b ≡
∃f ∈ set(finals g). ∃f' ∈ set(finals g). (a,b) ∈ \<E> f ∧ (b,a) ∈ \<E> f'"

untame2 :: "graph => bool"
"untame2 g ≡ ∃a b c. is_cycle g [a,b,c] ∧ distinct[a,b,c] ∧
(∀f ∈ \<F> g. \<E> f ≠ {(c,a), (a,b), (b,c)} ∧
\<E> f ≠ {(a,c), (c,b), (b,a)}) ∧
in2finals g a b"

lemma untame2: "untame(untame2)"
apply(auto simp:untame_def untame2_def tame_def tame2_def Edges_Cons)
apply(erule allE,erule allE,erule allE,erule impE,assumption)
apply(bestsimp dest!:edges_conv_Edges_if_cong simp: Edges_Cons)
done

lemma mk3Fin_id: "final g ==> makeTrianglesFinal g = g"
apply(subgoal_tac "[f∈faces g . ¬ final f ∧ triangle f] = []")
apply(simp add: finalGraph_def nonFinals_def filter_empty_conv)
done

lemma inv_untame2:
"invariant (λg. inv g ∧ untame2 g) next_planep"
proof (clarsimp simp:invariant_def invariantE[OF inv_inv_next_plane])
fix g g' assume g': "g [next_planep]-> g'"
and inv: "inv g" and un: "untame2 g"
note mgp' = inv_mgp[OF invariantE[OF inv_inv_next_plane, OF g' inv]]
show "untame2 g'" using un
proof(clarsimp simp:untame2_def)
fix a b c
assume 3: "is_cycle g [a,b,c]" and abc: "a ≠ b" "a ≠ c" "b ≠ c"
and untame: "∀f∈ \<F> g.
\<E> f ≠ {(c, a), (a, b), (b, c)} ∧
\<E> f ≠ {(a, c), (c, b), (b, a)}" (is "?P g a b c")
and in2: "in2finals g a b"
from in2 obtain f1 f2 :: face
where f1: "f1 ∈ \<F> g ∧ final f1 ∧ (a,b) ∈ \<E> f1"
and   f2: "f2 ∈ \<F> g ∧ final f2 ∧ (b,a) ∈ \<E> f2"
by(auto simp:finals_def in2finals_def)+
note mgp = inv_mgp[OF inv]
note g'1 = mgp_next_plane0_if_next_plane[OF mgp g']
have f1': "f1 ∈ \<F> g'" and f2': "f2 ∈ \<F> g'"
using next_plane0_finals_incr[OF g'1] f1 f2 by(auto simp:finals_def)
have "is_cycle g' [a,b,c]"
using 3 next_plane0_set_edges_subset[OF mgp g'1]
by(auto simp:is_cycle_def edges_graph_def
neighbors_edges[OF mgp] neighbors_edges[OF mgp'])
moreover have "?P g' a b c"
proof (rule ccontr, auto)
fix f assume fg: "f ∈ \<F> g'" and Ef: "\<E> f = {(c,a), (a,b), (b,c)}"
moreover have "f ≠ f1" using untame f1 Ef by blast
ultimately show False
using f1 f1' by(blast dest: mgp_edges_disj[OF mgp'])
next
fix f assume fg: "f ∈ \<F> g'" and Ef: "\<E> f = {(a,c), (c,b), (b,a)}"
moreover have "f ≠ f2" using untame f2 Ef by blast
ultimately show False
using f2 f2' by(blast dest: mgp_edges_disj[OF mgp'])
qed
moreover have "in2finals g' a b" using in2 next_plane0_finals_subset[OF g'1]
by(auto simp:in2finals_def)
ultimately
show "∃a b c. is_cycle g' [a,b,c] ∧ a≠b ∧ a≠c ∧ b≠c ∧ ?P g' a b c ∧ in2finals g' a b"
using abc by blast
qed
qed

lemma mk3Fin_id2:
assumes mgp: "minGraphProps g" and nf: "nonFinals g ≠ []"
and n3: "¬ triangle(minimalFace(nonFinals g))"
shows "makeTrianglesFinal g = g"
proof -
have "∀f∈set (nonFinals g). 3 ≤ |vertices f|"
using mgp_vertices3[OF mgp] by(simp add:nonFinals_def)
with n3 have "∀f ∈ set(nonFinals g). ¬ triangle f"
by(rule_tac minimal_neq_lowerbound[OF nf])
(auto simp:minimalFace_def o_def)
hence "∀f ∈ set(faces g). final f ∨ ¬ triangle f"
by(auto simp:nonFinals_def)
thus ?thesis  by(simp add:makeTrianglesFinal_def)
qed

lemma mk3Fin_mkFaceFin:
assumes mgp: "minGraphProps g" and nf: "nonFinals g ≠ []"
and 3: "triangle(minimalFace(nonFinals g))"
shows "makeTrianglesFinal (makeFaceFinal (minimalFace (nonFinals g)) g) =
makeTrianglesFinal g"
proof -
let ?f = "minimalFace (nonFinals g)"
from nf 3 have "minimalFace(nonFinals g) ∈ set(nonFinals g)"
with 3 have "[f ∈ faces g. ¬ final f ∧ triangle f] ≠ []"
by (auto simp: filter_empty_conv nonFinals_def)
then obtain f fs where ffs: "f#fs = [f ∈ faces g. ¬ final f ∧ triangle f]"
with decomp_nonFinal3[OF mgp ffs]
have "[f ∈ faces g. ¬ final f ∧ triangle f] =
?f # [f ∈ faces(makeFaceFinal ?f g). ¬ final f ∧ triangle f]" by(simp)
thus ?thesis by(simp add:makeTrianglesFinal_def)
qed

lemma next_plane_mk3Fin_alternatives:
assumes inv: "inv g" and 2: "|faces g| ≠ 2" and 1: "g [next_planep]-> g'"
shows "untame2 g' ∨ makeTrianglesFinal g = g ∨
makeTrianglesFinal g' = makeTrianglesFinal g"
proof -
note mgp = inv_mgp[OF inv]
note mgp' = inv_mgp[OF invariantE[OF inv_inv_next_plane, OF 1 inv]]
have nf: "nonFinals g ≠ []" using 1 by(auto simp:next_plane_def)
note gg' = mgp_next_plane0_if_next_plane[OF mgp 1]
show ?thesis
proof (cases "triangle(minimalFace(nonFinals g))")
case True
let ?f = "minimalFace(nonFinals g)"
have f: "?f ∈ set(nonFinals g)" using nf by (simp add:minimalFace_def)
hence fg: "?f ∈ \<F> g" by(simp add:nonFinals_def)
from f have fnf: "¬ final ?f" by(simp add:nonFinals_def)
note distf = minGraphProps3[OF mgp fg]
def a ≡ "minimalVertex g ?f"
from mgp_vertices_nonempty[OF mgp fg]
have v: "a ∈ set(vertices ?f)" by (simp add:a_def minimalVertex_def)
from 1 obtain i e
where g'0: "g' = subdivFace g ?f (indexToVertexList ?f a e)"
and e: "e ∈ set (enumerator i |vertices ?f| )" and i: "2 < i"
and containsNot: "¬ containsDuplicateEdge g ?f a e"
by (auto simp: a_def next_plane_def generatePolygon_def image_def
split:split_if_asm)
note pre_add = pre_subdivFace_indexToVertexList[OF mgp f v e containsNot i]
with g'0 have g': "g' = subdivFace' g ?f a 0 (tl(indexToVertexList ?f a e))"
by (simp  add: subdivFace_subdivFace'_eq)
from pre_add have "indexToVertexList ?f a e ≠ []"
by (simp add: pre_subdivFace_def pre_subdivFace_face_def)
have pre: "pre_subdivFace' g ?f a a 0 (tl(indexToVertexList ?f a e))"
by(fastsimp simp add:neq_Nil_conv elim:pre_subdivFace_pre_subdivFace')
have "g' = makeFaceFinal ?f g ∨
(∀f' ∈ \<F> g' - (\<F> g - {?f}). \<E> f' ≠ \<E> ?f)" (is "?A ∨ ?B")
by(simp only:g')(rule dist_edges_subdivFace'[OF pre mgp fg])
thus ?thesis
proof
assume ?A
hence "makeTrianglesFinal g' = makeTrianglesFinal g"
by(simp add:mk3Fin_mkFaceFin[OF mgp nf True])
thus ?thesis by blast
next
assume B: ?B
obtain b c where fabs: "vertices ?f = [a,b,c] ∨ vertices ?f = [c,a,b] ∨
vertices ?f = [b,c,a]"
using v True by(fastsimp simp: nat_number length_Suc_conv)
hence Ef: "\<E> ?f = {(a,b), (b,c), (c,a)}"
by(fastsimp simp: edges_conv_Edges[OF distf] Edges_Cons)
hence "{(a,b), (b,c), (c,a)} ⊆ \<E> g'"
using fg next_plane0_set_edges_subset[OF mgp gg']
by(unfold edges_graph_def) blast
hence 3: "is_cycle g' [c,a,b]"
by(auto simp: is_cycle_def neighbors_edges[OF mgp'])
have abc: "distinct[a,b,c]" using distf fabs by auto
obtain f' where f': "f' ∈ \<F> g ∧ final f' ∧ (a,c) ∈ \<E> f'"
using Ef inv_one_finalD'[OF inv fg fnf]
by blast
hence f'g': "f' ∈ \<F> g'"
using f' next_plane0_finals_subset[OF gg'] by (simp add:finals_def)blast
have "?f-1 • a = c" using fabs abc by(auto simp:prevVertex_def)
then obtain f'' where f'': "f'' ∈ \<F> g' ∧ final f'' ∧ (c,a)∈ \<E> f''"
using g' subdivFace'_final_base[OF mgp pre fg] by simp blast
{ fix ff assume ffg': "ff ∈ \<F> g'"
assume "\<E> ff = {(b,c), (c,a), (a,b)} ∨
\<E> ff = {(c,b), (b,a), (a,c)}" (is "?ab ∨ ?ba")
hence False
proof
assume Eff: ?ab
have "ff ∉ \<F> g - {?f}"
proof
assume "ff ∈ \<F> g - {?f}"
hence ffg: "ff ∈ \<F> g" and neq: "ff ≠ ?f" by auto
note distff = minGraphProps3[OF mgp ffg]
have "ff = ?f" using Ef Eff
by(blast intro: face_eq_if_normFace_eq[OF mgp ffg fg]
normFace_eq_if_edges_eq[OF distff distf])
with neq show False by fast
qed
with B ffg' have "\<E> ff ≠ \<E> ?f" by blast
with Eff Ef show False by blast
next
assume Eff: ?ba
obtain h1 :: face where h1g: "h1 ∈ \<F> g" and fh1: "final h1"
and ach1: "(a,c) : \<E> h1"
using inv_one_finalD'[OF inv fg fnf] Ef by blast
obtain h2 :: face where h2g: "h2 ∈ \<F> g" and fh2: "final h2"
and cbh2: "(c,b) : \<E> h2"
using inv_one_finalD'[OF inv fg fnf] Ef by blast
obtain h3 :: face where h3g: "h3 ∈ \<F> g" and fh3: "final h3"
and bah3: "(b,a) : \<E> h3"
using inv_one_finalD'[OF inv fg fnf] Ef by blast
have h1g': "h1 ∈ \<F> g'"
using h1g fh1 subdivFace_pres_finals[OF _ fnf] g'0 fg
have h2g': "h2 ∈ \<F> g'"
using h2g fh2 subdivFace_pres_finals[OF _ fnf] g'0 fg
have h3g': "h3 ∈ \<F> g'"
using h3g fh3 subdivFace_pres_finals[OF _ fnf] g'0 fg
note mgp' = inv_mgp[OF inv_inv_next_plane0[THEN invariantE, OF gg' inv]]
note disth1 = minGraphProps3[OF mgp h1g]
have "¬(h1 = h2 ∧ h1 = h3 ∧ h2 = h3)"
proof
assume [simp]: "h1 = h2 ∧ h1 = h3 ∧ h2 = h3"
have "face_face_op g" using mgp by(simp add:minGraphProps_def)
moreover have "h1 ≠ ?f" using fnf fh1 by auto
ultimately have "\<E> h1 ≠ (\<E> ?f)¯" using 2 h1g fg
moreover have "\<E> h1 = {(c,b),(b,a),(a,c)}"
using abc ach1 cbh2 bah3
by(rule_tac triangle_if_3circular[OF _ disth1])auto
ultimately show False using Ef by fastsimp
qed
hence "¬(h1 = ff ∧ h2 = ff ∧ h3 = ff)" by blast
thus False using Eff
mgp_edges_disj[OF mgp' _ h1g' ffg' ach1]
mgp_edges_disj[OF mgp' _ h2g' ffg' cbh2]
mgp_edges_disj[OF mgp' _ h3g' ffg' bah3]
by blast
qed }
with 3 abc f' f'g' f'' have "untame2 g'"
by(simp add: untame2_def in2finals_def finals_def) blast
thus ?thesis by blast
qed
next
case False
thus ?thesis by(simp add:mk3Fin_id2[OF mgp nf])
qed
qed

theorem make3Fin_complete:
"[| invariant inv (succ p);
!!g. inv g ==> set (succ p g) ⊆ set (next_plane p g);
tame g; final g; Seedp [succ p]->* g |] ==>
Seedp [map makeTrianglesFinal o succ p]->* g"
apply(rule comp_map_tame_pres[OF _ _ untame2])
apply assumption
apply(rule inv_subset[OF inv_untame2[where p=p]])
apply blast
apply(erule mk3Fin_id)
apply(rule inv_RTranCl_subset[OF inv_untame2[where p=p]])
apply(rule mk3Fin_in_RTranCl)
apply blast
defer
apply assumption
apply(rule inv_Seed)
apply assumption
apply assumption
apply(rule next_plane_mk3Fin_alternatives)
apply(rule invariantE[OF inv_inv_next_plane])
apply blast
apply assumption
apply(rule step_outside2)
apply assumption
apply(rule mgp_next_plane0_if_next_plane[OF inv_mgp])
apply assumption
apply blast
apply(rule next_plane0_nonfinals)
apply(rule mgp_next_plane0_if_next_plane[OF inv_mgp])
apply(rule invariantE[OF inv_inv_next_plane])
apply blast
apply assumption
apply (blast dest:invariantE)
apply (blast dest:invariantE)
done

end
```

### Correctness

lemma decomp_nonFinal3:

```  [| minGraphProps g; f # fs = [f∈faces g . ¬ final f ∧ triangle f] |]
==> f = minimalFace (nonFinals g) ∧
fs =
[f∈faces (makeFaceFinal (minimalFace (nonFinals g)) g) .
¬ final f ∧ triangle f]```

lemma noDupEdge3:

```  [| minGraphProps g; f ∈ \<F> g; triangle f; v ∈ \<V> f |]
==> ¬ containsDuplicateEdge g f v [0..<3]```

lemma indexToVs3:

```  [| triangle f; distinct (vertices f); v ∈ \<V> f |]
==> indexToVertexList f v [0..<3] = [Some v, Some (f • v), Some (f • (f • v))]```

lemma upt3_in_enumerator:

`  [0..<3] ∈ set (enumerator 3 3)`

lemma mkFaceFin3_in_succs1:

```  [| minGraphProps g; f # fs = [f∈faces g . ¬ final f ∧ triangle f] |]
==> Graph (makeFaceFinalFaceList f (faces g)) (countVertices g)
(map (makeFaceFinalFaceList f) (faceListAt g)) (heights g)
∈ set (next_planep g)```

lemma mkFaceFin3_in_rtrancl:

```  [| minGraphProps g; f # fs = [f∈faces g . ¬ final f ∧ triangle f] |]
==> g [next_planep]->* makeFaceFinal f g```

lemma mk3Fin_lem:

```  [| minGraphProps g; fs = [f∈faces g . ¬ final f ∧ triangle f] |]
==> g [next_planep]->* foldl (λg f. makeFaceFinal f g) g fs```

lemma mk3Fin_in_RTranCl:

`  Invariants.inv g ==> g [next_planep]->* makeTrianglesFinal g`

### Completeness

lemma untame2:

`  untame untame2`

lemma mk3Fin_id:

`  final g ==> makeTrianglesFinal g = g`

lemma inv_untame2:

`  invariant (λg. Invariants.inv g ∧ untame2 g) next_planep`

lemma mk3Fin_id2:

```  [| minGraphProps g; nonFinals g ≠ [];
|vertices (minimalFace (nonFinals g))| ≠ 3 |]
==> makeTrianglesFinal g = g```

lemma mk3Fin_mkFaceFin:

```  [| minGraphProps g; nonFinals g ≠ []; triangle (minimalFace (nonFinals g)) |]
==> makeTrianglesFinal (makeFaceFinal (minimalFace (nonFinals g)) g) =
makeTrianglesFinal g```

lemma next_plane_mk3Fin_alternatives:

```  [| Invariants.inv g; |faces g| ≠ 2; g' ∈ set (next_planep g) |]
==> untame2 g' ∨
makeTrianglesFinal g = g ∨ makeTrianglesFinal g' = makeTrianglesFinal g```

theorem make3Fin_complete:

```  [| invariant Invariants.inv (succ p);
!!g. Invariants.inv g ==> set (succ p g) ⊆ set (next_planep g); tame g;
final g; Seedp [succ p]->* g |]
==> Seedp [map makeTrianglesFinal o succ p]->* g```