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