Theory GeneratorProps

(*  ID:         $Id: GeneratorProps.thy,v 1.4 2006/01/13 19:18:53 nipkow Exp $
    Author:     Tobias Nipkow
*)

header "Properties of Tame Graph Enumeration (1)"

theory GeneratorProps
imports Plane3Props LowerBound
begin

lemma genPolyTame_spec:
 "generatePolygonTame n v f g = [g' ∈ generatePolygon n v f g . ¬ notame g']"
by(simp add:generatePolygonTame_def generatePolygon_def enum_enumerator)

lemma genPolyTame_subset_genPoly:
 "g' ∈ set(generatePolygonTame i v f g) ==>
  g' ∈ set(generatePolygon i v f g)"
by(auto simp add:generatePolygon_def generatePolygonTame_def enum_enumerator)


lemma next_tame0_subset_plane:
 "set(next_tame0 p g) ⊆ set(next_plane p g)"
by(auto simp add:next_tame0_def next_plane_def polysizes_def
           elim!:genPolyTame_subset_genPoly simp del:upt_Suc)


lemma genPoly_new_face:
 "[|g' ∈ set (generatePolygon n v f g); minGraphProps g; f ∈ set (nonFinals g);
   v ∈ \<V> f; n ≥ 3 |] ==>
  ∃f ∈ set(finals g') - set(finals g). |vertices f| = n"
apply(auto simp add:generatePolygon_def image_def)
apply(rename_tac "is")
apply(frule enumerator_length2)
 apply arith
apply(frule (4) pre_subdivFace_indexToVertexList)
 apply(arith)
apply(subgoal_tac "indexToVertexList f v is ≠ []")
 prefer 2 apply(subst length_0_conv[symmetric]) apply simp
apply(simp add: subdivFace_subdivFace'_eq)
apply(clarsimp simp:neq_Nil_conv)
apply(rename_tac "ovs")
apply(subgoal_tac "|indexToVertexList f v is| = |ovs| + 1")
 prefer 2 apply(simp)
apply(drule (1) pre_subdivFace_pre_subdivFace')
apply(drule (1) final_subdivFace')
  apply(simp add:nonFinals_def)
 apply(simp add:pre_subdivFace'_def)
apply (simp (no_asm_use))
apply(simp)
apply blast
done


(* Could prove = instead of >=, but who needs it? *)
lemma genPoly_incr_facesquander_lb:
assumes "g' ∈ set (generatePolygon n v f g)" "inv g"
        "f ∈ set(nonFinals g)" "v ∈ \<V> f" "3 ≤ n"
shows "faceSquanderLowerBound g' ≥ faceSquanderLowerBound g + \<d> n"
proof -
  from genPoly_new_face[OF prems(1) inv_mgp[OF prems(2)] prems(3-5)] obtain f
    where f: "f ∈ set (finals g') - set(finals g)"
    and size: "|vertices f| = n" by auto
  have g': "g' ∈ set(next_plane0 (n - 3) g)" using prems(5)
    by(rule_tac in_next_plane0I[OF prems(1,3-5)]) simp
  note dist = minGraphProps11'[OF inv_mgp[OF prems(2)]]
  note inv' = invariantE[OF inv_inv_next_plane0, OF g' prems(2)]
  note dist' = minGraphProps11'[OF inv_mgp[OF inv']]
  note subset = next_plane0_finals_subset[OF g']
  have "faceSquanderLowerBound g' ≥
        faceSquanderLowerBound g + \<d> |vertices f|"
  proof(unfold faceSquanderLowerBound_def)
    have "(∑f∈finals g \<d> |vertices f| ) + \<d> |vertices f| =
          (∑f∈set(finals g). \<d> |vertices f| ) + \<d> |vertices f|"
      using dist by(simp add:finals_def ListSum_conv_setsum)
    also have "… = (∑f∈set(finals g) ∪ {f}. \<d> |vertices f| )"
      using f by simp
    also have "… ≤ (∑f∈set(finals g'). \<d> |vertices f| )"
      using f subset by(fastsimp intro!: setsum_mono3)
    also have "… = (∑f∈finals g' \<d> |vertices f| )"
      using dist' by(simp add:finals_def ListSum_conv_setsum)
    finally show "(∑f∈finals g \<d> |vertices f| ) + \<d> |vertices f|
          ≤ ∑f∈finals g' \<d> |vertices f|" .
  qed
  with size show ?thesis by blast
qed


lemma ExcessTable_empty:
 "∀x ∈ \<V> g. ¬ finalVertex g x ==> ExcessTable g (vertices g) = []"
by(simp add:ExcessTable_def filter_empty_conv ExcessAt_def)


constdefs
 close :: "graph => vertex => vertex => bool"
"close g u v ≡
 ∃f ∈ set(facesAt g u). if |vertices f| = 4 then v = f • u ∨ v = f • (f • u)
                        else v = f • u"

(* FIXME This should be the def of delAround *)
lemma delAround_def: "deleteAround g u ps = [p ∈ ps. ¬ close g u (fst p)]"
by (induct ps) (auto simp: deleteAroundCons close_def)


lemma close_sym: assumes mgp: "minGraphProps g" and cl: "close g u v"
shows "close g v u"
proof -
  obtain f where f: "f ∈ set(facesAt g u)" and
    if: "if |vertices f| = 4 then v = f • u ∨ v = f • (f • u) else v = f • u"
    using cl by (unfold close_def) blast
  note uf = minGraphProps6[OF mgp f]
  note distf = minGraphProps3[OF mgp minGraphProps5[OF mgp f]]
  show ?thesis
  proof cases
    assume 4: "|vertices f| = 4"
    hence "v = f • u ∨ v = f • (f • u)" using if by simp
    thus ?thesis
    proof
      assume "v = f • u"
      then obtain f' where "f' ∈ set(facesAt g v)" "f' • v = u"
        using mgp_nextVertex_face_ex2[OF mgp f] by blast
      thus ?thesis by(auto simp:close_def)
    next
      assume v: "v = f • (f • u)"
      hence "f • (f • v) = u" using quad_next4_id[OF 4 distf uf] by simp
      moreover have "f ∈ set(facesAt g v)" using v uf
        by(simp add: minGraphProps7[OF mgp minGraphProps5[OF mgp f]])
      ultimately show ?thesis using 4 by(auto simp:close_def)
    qed
  next
    assume "|vertices f| ≠ 4"
    hence "v = f • u" using if by simp
    then obtain f' where "f' ∈ set(facesAt g v)" "f' • v = u"
      using mgp_nextVertex_face_ex2[OF mgp f] by blast
    thus ?thesis by(auto simp:close_def)
  qed
qed


lemma preSep_conv:
assumes mgp: "minGraphProps g"
shows "preSeparated g V = (∀u∈V.∀v∈V. u ≠ v --> ¬ close g u v)" (is "?P = ?Q")
proof
  assume preSep: ?P
  show ?Q
  proof(clarify)
    fix u v assume uv: "u ∈ V" "v ∈ V" "u ≠ v" and cl: "close g u v"
    from cl obtain f where f: "f ∈ set(facesAt g u)" and
      if: "if |vertices f| = 4 then (v = f • u) ∨ (v = f • (f • u))
                               else (v = f • u)"
      by (unfold close_def) blast
    note uf = minGraphProps6[OF mgp f]
    show False
    proof cases
      assume 4: "|vertices f| = 4"
      hence "v = f • u ∨ v = f • (f • u)" using if by simp
      thus False
      proof
        assume "v = f • u"
        thus False using preSep f uv
          by(simp add:preSeparated_def separated2_def separated3_def)
      next
        assume "v = f • (f • u)"
        moreover hence "v ∈ \<V> f" using `u ∈ \<V> f` by simp
        moreover have "|vertices f| ≤ 4" using 4 by arith
        ultimately show False using preSep f uv `u ∈ \<V> f`
          apply(unfold preSeparated_def separated2_def separated3_def)
(* why does blast get stuck? *)
          apply(subgoal_tac "f • (f • u) ∈ \<V> f ∩ V")
          prefer 2 apply blast
          by simp
      qed
    next
      assume 4: "|vertices f| ≠ 4"
      hence "v = f • u" using if by simp
      thus False using preSep f uv
        by(simp add:preSeparated_def separated2_def separated3_def)
    qed
  qed
next
  assume not_cl: ?Q
  show ?P
  proof(simp add:preSeparated_def, rule conjI)
    show "separated2 g V"
    proof (clarsimp simp:separated2_def)
      fix v f assume "v ∈ V" and f: "f ∈ set (facesAt g v)" and "f • v ∈ V"
      thus False using not_cl mgp_facesAt_no_loop[OF mgp f]
        by(fastsimp simp: close_def split:split_if_asm)
    qed
    show "separated3 g V"
    proof (clarsimp simp:separated3_def)
      fix v f
      assume "v ∈ V" and f: "f ∈ set (facesAt g v)" and len: "|vertices f| ≤ 4"
      note distf = minGraphProps3[OF mgp minGraphProps5[OF mgp f]]
      note vf = minGraphProps6[OF mgp f]
      { fix u assume "u ∈ \<V> f" and "u ∈ V"
        have "u = v"
        proof cases
          assume 3: "|vertices f| = 3"
          hence "\<V> f = {v, f • v, f • (f • v)}"
            using vertices_triangle[OF _ vf distf] by simp
          moreover
          { assume "u = f • v"
            hence "u = v"
              using not_cl f `u ∈ V` `v ∈ V` 3
              by(force simp:close_def split:split_if_asm)
          }
          moreover
          { assume "u = f • (f • v)"
            hence fu: "f • u = v"
              by(simp add: tri_next3_id[OF 3 distf `v ∈ \<V> f`])
            hence "(u,v) ∈ \<E> f" using nextVertex_in_edges[OF `u ∈ \<V> f`]
              by(simp add:fu)
            then obtain f' where "f' ∈ set(facesAt g v)" "(v,u) ∈  \<E> f'"
              using mgp_edge_face_ex[OF mgp f] by blast
            hence "u = v" using not_cl `u ∈ V` `v ∈ V` 3
              by(force simp:close_def edges_face_eq split:split_if_asm)
          }
          ultimately show "u=v" using `u ∈ \<V> f` by blast
        next
          assume 3: "|vertices f| ≠ 3"
          hence 4: "|vertices f| = 4"
            using len mgp_vertices3[OF mgp minGraphProps5[OF mgp f]] by arith
          hence "\<V> f = {v, f • v, f • (f • v), f • (f • (f • v))}"
            using vertices_quad[OF _ vf distf] by simp
          moreover
          { assume "u = f • v"
            hence "u = v"
              using not_cl f `u ∈ V` `v ∈ V` 4
              by(force simp:close_def split:split_if_asm)
          }
          moreover
          { assume "u = f • (f • v)"
            hence "u = v"
              using not_cl f `u ∈ V` `v ∈ V` 4
              by(force simp:close_def split:split_if_asm)
          }
          moreover
          { assume "u = f • (f • (f • v))"
            hence fu: "f • u = v"
              by(simp add: quad_next4_id[OF 4 distf `v ∈ \<V> f`])
            hence "(u,v) ∈ \<E> f" using nextVertex_in_edges[OF `u ∈ \<V> f`]
              by(simp add:fu)
            then obtain f' where "f' ∈ set(facesAt g v)" "(v,u) ∈  \<E> f'"
              using mgp_edge_face_ex[OF mgp f] by blast
            hence "u = v" using not_cl `u ∈ V` `v ∈ V` 4
              by(force simp:close_def edges_face_eq split:split_if_asm)
          }
          ultimately show "u=v" using `u ∈ \<V> f` by blast
        qed
      }
      thus "\<V> f ∩ V = {v}" using `v ∈ V` vf by blast
    qed
  qed
qed


lemma fin_aux: "finite B ==> finite{f A|A. A ⊆ B ∧ P A}"
apply(rule finite_subset[where B = "f ` Pow B"])
 apply blast
apply simp
done

lemma preSep_ne: "∃P ⊆ M. preSeparated g (fst ` P)"
by(unfold preSeparated_def separated2_def separated3_def) blast

lemma ExcessNotAtRec_conv_Max:
assumes mgp: "minGraphProps g"
shows "distinct(map fst ps) ==> ExcessNotAtRec ps g =
  Max{ ∑p∈P. snd p |P. P ⊆ set ps ∧ preSeparated g (fst ` P)}"
  (concl is "_ = Max(?M ps)" is "_ = Max{_ |P. ?S ps P}")
proof(induct ps rule: length_induct)
  case (1 ps0)
  note IH = 1(1) and dist = 1(2)
  show ?case
  proof (cases ps0)
    case Nil thus ?thesis by(simp add:Max_def)
  next
    case (Cons p ps)
    let ?ps = "deleteAround g (fst p) ps"
    have le: "|?ps| ≤ |ps|" by(simp add:delAround_def)
    have dist': "distinct(map fst ?ps)" using dist Cons
      apply (clarsimp simp:delAround_def)
      apply(drule distinct_filter[where P = "Not o close g (fst p)"])
      apply(simp add: filter_map o_def)
      done
    have "ExcessNotAtRec ps0 g = max (Max(?M ps)) (snd p + Max(?M ?ps))"
      using Cons IH le dist dist' by(simp)
    also have "snd p + Max(?M ?ps) =
      (Max{snd p + (∑p∈P. snd p) |P. ?S ?ps P})"
      by(auto simp add:add_Max_commute fin_aux preSep_ne intro!:arg_cong[where f=Max])
    also have "{snd p + (∑p∈P. snd p) |P. ?S ?ps P} =
      {setsum snd (insert p P) |P. ?S ?ps P}"
      using dist Cons
      apply (auto simp:delAround_def)
      apply(rule_tac x=P in exI)
      apply(fastsimp intro!: setsum_insert[THEN trans,symmetric] elim: finite_subset)
      apply(rule_tac x=P in exI)
      apply(fastsimp intro!: setsum_insert[THEN trans] elim: finite_subset)
      done
    also have "… = {setsum snd P |P.
            P ⊆ insert p (set ?ps) ∧ p ∈ P ∧ preSeparated g (fst ` P)}"
      apply(auto simp add:preSep_conv[OF mgp] delAround_def)
      apply(rule_tac x = "insert p P" in exI)
      apply simp
      apply(rule conjI) apply blast
      apply (blast intro:close_sym[OF mgp])
      apply(rule_tac x = "P-{p}" in exI)
      apply (simp add:insert_absorb)
      apply blast
      done
    also have "… = {setsum snd P |P.
            P ⊆ insert p (set ps) ∧ p ∈ P ∧ preSeparated g (fst ` P)}"
      using Cons dist
      apply(auto simp add:preSep_conv[OF mgp] delAround_def)
      apply(rule_tac x = "P" in exI)
      apply simp
      apply auto
      done
    also have "max (Max(?M ps)) (Max …) = Max(?M ps ∪ {setsum snd P |P.
            P ⊆ insert p (set ps) ∧ p ∈ P ∧ preSeparated g (fst ` P)})"
      (is "_ = Max ?U")
    proof -
      have "{setsum snd P |P.
            P ⊆ insert p (set ps) ∧ p ∈ P ∧ preSeparated g (fst ` P)} ≠ {}"
        apply simp
        apply(rule_tac x="{p}" in exI)
        by(simp add:preSep_conv[OF mgp])
      thus ?thesis by(simp add: Max_Un fin_aux preSep_ne)
    qed
    also have "?U = ?M ps0" using Cons by simp blast
    finally show ?thesis .
  qed
qed


lemma dist_ExcessTab: "distinct (map fst (ExcessTable g (vertices g)))"
by(simp add:ExcessTable_def vertices_graph map_compose[symmetric] o_def)



lemma mono_ExcessTab: "[|g' ∈ set (next_plane0p g); inv g |] ==>
  set(ExcessTable g (vertices g)) ⊆ set(ExcessTable g' (vertices g'))"
apply(clarsimp simp:ExcessTable_def image_def)
apply(rule conjI)
 apply(blast dest:next_plane0_vertices_subset inv_mgp)
apply (clarsimp simp:ExcessAt_def split:split_if_asm)
apply(frule (3) next_plane0_finalVertex_mono)
apply(simp add: next_plane0_len_filter_eq tri_def quad_def except_def)
done


lemma close_antimono:
 "[|g' ∈ set (next_plane0p g); inv g; u ∈ \<V> g; finalVertex g u |] ==>
  close g' u v ==> close g u v"
by(simp add:close_def next_plane0_finalVertex_facesAt_eq)

lemma ExcessTab_final:
 "p ∈ set(ExcessTable g (vertices g)) ==> finalVertex g (fst p)"
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:split_if_asm)

lemma ExcessTab_vertex:
 "p ∈ set(ExcessTable g (vertices g)) ==> fst p ∈ \<V> g"
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:split_if_asm)

lemma next_plane0_incr_ExcessNotAt:
 "[|g' ∈ set (next_plane0p g); inv g |] ==>
  ExcessNotAt g None ≤ ExcessNotAt g' None"
apply(frule (1) invariantE[OF inv_inv_next_plane0])
apply(frule (1) mono_ExcessTab)
apply(simp add: ExcessNotAt_def ExcessNotAtRec_conv_Max[OF _ dist_ExcessTab])
apply(rule Max_mono)
  prefer 2 apply (simp add: preSep_ne)
 prefer 2 apply (simp add: fin_aux)
apply auto
apply(rule_tac x=P in exI)
apply auto
apply(simp add:preSep_conv)
apply (blast intro:close_antimono ExcessTab_final ExcessTab_vertex)
done
(* close -> in neibhood ?? *)


lemma next_plane0_incr_squander_lb:
 "[|g' ∈ set (next_plane0p g); inv g |] ==>
  squanderLowerBound g ≤ squanderLowerBound g'"
apply(simp add:squanderLowerBound_def)
apply(frule (1) next_plane0_incr_ExcessNotAt)
apply(clarsimp simp add:next_plane0_def split:split_if_asm)
apply(drule (4) genPoly_incr_facesquander_lb)
apply arith
done

lemma inv_notame:
 "[|g' ∈ set (next_plane0p g); inv g; notame g|]
  ==> notame g'"
apply(simp add:notame_def tame45_def is_tame7_def del:disj_not1)
apply(erule disjE)
 apply(rule disjI1)
 apply(clarify)
 apply(frule inv_mgp)
 apply(frule (2) next_plane0_incr_degree)
 apply(frule (2) next_plane0_incr_except)
 apply(frule (1) next_plane0_vertices_subset)
 apply(case_tac "except g' v = 0")
  apply(rule bexI) prefer 2 apply fast
  apply simp
 apply(rule bexI) prefer 2 apply fast
 apply (simp split:split_if_asm)
apply(frule (1) next_plane0_incr_squander_lb)
apply(arith)
done


lemma inv_inv_notame:
 "invariant(λg. inv g ∧ notame g) next_planep"
apply(simp add:invariant_def)
apply(blast intro: inv_notame mgp_next_plane0_if_next_plane[OF inv_mgp]
       invariantE[OF inv_inv_next_plane])
done


lemma untame_notame:
 "untame (λg. inv g ∧ notame g)"
proof(clarsimp simp add: notame_def untame_def tame45_def is_tame7_def
                         linorder_not_le linorder_not_less)
  fix g assume "final g" "inv g" "tame g"
    and cases: "(∃v∈\<V> g. (except g v = 0 --> 6 < degree g v) ∧
                            (0 < except g v --> 5 < degree g v))
                ∨ squanderTarget ≤ squanderLowerBound g"
                (is "?A ∨ ?B" is "(∃v∈\<V> g. ?C v) ∨ _")
  from cases show False
  proof
    assume ?A
    then obtain v where v: "v ∈\<V> g" "?C v" by auto
    show False
    proof cases
      assume "except g v = 0"
      thus False using `tame g` v by(auto simp: tame_def tame45_def)
    next
      assume "except g v ≠ 0"
      thus False using `tame g` v
        by(auto simp: except_def filter_empty_conv tame_def tame45_def
          minGraphProps_facesAt_eq[OF inv_mgp[OF `inv g`]] split:split_if_asm)
    qed
  next
    assume ?B
    thus False using total_weight_lowerbound[OF `inv g` `final g` `tame g`]
      `tame g`  by(force simp add:tame_def tame7_def)
  qed
qed


lemma polysizes_tame:
 "[| g' ∈ set (generatePolygon n v f g); inv g; f ∈ set(nonFinals g);
   v ∈ \<V> f; 3 ≤ n; n < 4+p; n ∉ set(polysizes p g) |]
 ==> notame g'"
apply(frule (4) in_next_plane0I)
apply(frule (4) genPoly_incr_facesquander_lb)
apply(frule (1) next_plane0_incr_ExcessNotAt)
apply(simp add: notame_def is_tame7_def faceSquanderLowerBound_def
           polysizes_def squanderLowerBound_def)
done

lemma genPolyTame_notame:
 "[| g' ∈ set (generatePolygon n v f g); g' ∉ set (generatePolygonTame n v f g);
    inv g; 3 ≤ n |]
  ==> notame g'"
by(fastsimp simp:generatePolygon_def generatePolygonTame_def enum_enumerator
                 notame_def)


declare upt_Suc[simp del] (* FIXME global? *)
lemma excess_notame:
 "[| inv g; g' ∈ set (next_planep g); g' ∉ set (next_tame0 p g) |]
       ==> notame g'"
apply(frule (1) mgp_next_plane0_if_next_plane[OF inv_mgp])
apply(auto simp add:next_tame0_def next_plane_def split:split_if_asm)
apply(rename_tac n)
apply(case_tac "n ∈ set(polysizes p g)")
 apply(drule bspec) apply assumption
 apply(simp add:genPolyTame_notame)
apply(subgoal_tac "minimalFace (nonFinals g) ∈ set(nonFinals g)")
 prefer 2 apply(simp add:minimalFace_def)
apply(subgoal_tac "minimalVertex g (minimalFace (nonFinals g)) ∈ \<V>(minimalFace (nonFinals g))")
 apply(blast intro:polysizes_tame)
apply(simp add:minimalVertex_def)
apply(rule minimal_in_set)
apply(erule mgp_vertices_nonempty[OF inv_mgp])
apply(simp add:nonFinals_def)
done
declare upt_Suc[simp]

lemma next_tame0_comp: "[| Seedp [next_plane p]->* g; final g; tame g |]
 ==> Seedp [next_tame0 p]->* g"
apply(rule filterout_untame_succs[OF inv_inv_next_plane inv_inv_notame
  untame_notame])
    apply(blast intro:excess_notame)
   apply assumption
  apply(rule inv_Seed)
 apply assumption
apply assumption
done

lemma next_tame1_comp:
 "[| tame g; final g; Seedp [next_tame0 p]->* g |]
 ==> Seedp [next_tame1p]->* g"
apply (unfold next_tame1_def)
apply(rule make3Fin_complete)
    apply(blast intro: inv_subset[OF inv_inv_next_plane next_tame0_subset_plane])
   apply(rule next_tame0_subset_plane)
  apply assumption+
done

lemma inv_inv_next_tame0: "invariant inv (next_tame0 p)"
by(rule inv_subset[OF inv_inv_next_plane next_tame0_subset_plane])


lemma inv_inv_next_tame1: "invariant inv next_tame1p"
apply(simp add:next_tame1_def)
apply(rule inv_comp_map[OF inv_inv_next_tame0])
by(blast intro:RTranCl_inv[OF inv_inv_next_plane] mk3Fin_in_RTranCl)

lemma inv_inv_next_tame: "invariant inv next_tamep"
apply(simp add:next_tame_def)
apply(rule inv_subset[OF inv_inv_next_tame1])
apply auto
done

lemma mgp_TameEnum: "g ∈ TameEnump ==> minGraphProps g"
by (unfold TameEnumP_def)
   (blast intro: RTranCl_inv[OF inv_inv_next_tame] inv_Seed inv_mgp)


end