Up to index of Isabelle/HOL/Tame
theory Plane3Props(* ID: $Id: Plane3Props.thy,v 1.2 2006/01/09 06:56:13 nipkow Exp $ Author: Tobias Nipkow *) header{* All About Finalizing Triangles *} 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 by (simp add:nonFinals_def) 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]" by(simp add:nonFinals_def) also have "… = [h ∈ remove1 f (nonFinals g). triangle h]" by(simp add:nonFins_mkFaceFin) 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) apply(simp add:nat_number) 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(simp add:makeFaceFinal_def) 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" by(simp add:makeTrianglesFinal_def mk3Fin_lem) 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: makeTrianglesFinal_def) 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)" by (simp add:minimalFace_def) 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]" by(fastsimp simp add:neq_Nil_conv) 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) with pre_add v 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 by(simp add:finals_def) have h2g': "h2 ∈ \<F> g'" using h2g fh2 subdivFace_pres_finals[OF _ fnf] g'0 fg by(simp add:finals_def) have h3g': "h3 ∈ \<F> g'" using h3g fh3 subdivFace_pres_finals[OF _ fnf] g'0 fg by(simp add:finals_def) 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 by(simp add:face_face_op_def) 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(simp add:finalGraph_def) 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
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
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