Theory GeneratorProps

(*  Author:  Tobias Nipkow  *)

section "Properties of Tame Graph Enumeration (1)"

theory GeneratorProps
imports Plane1Props Generator TameProps 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  𝒱 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  𝒱 f" "3  n"
shows "faceSquanderLowerBound g'  faceSquanderLowerBound g + 𝖽 n"
proof -
  from genPoly_new_face[OF assms(1) inv_mgp[OF assms(2)] assms(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 assms(5)
    by(rule_tac in_next_plane0I[OF assms(1,3-5)]) simp
  note dist = minGraphProps11'[OF inv_mgp[OF assms(2)]]
  note inv' = invariantE[OF inv_inv_next_plane0, OF g' assms(2)]
  note dist' = minGraphProps11'[OF inv_mgp[OF inv']]
  note subset = next_plane0_finals_subset[OF g']
  have "faceSquanderLowerBound g' 
        faceSquanderLowerBound g + 𝖽 |vertices f|"
  proof(unfold faceSquanderLowerBound_def)
    have "(∑⇘ffinals g𝖽 |vertices f| ) + 𝖽 |vertices f| =
          (fset(finals g). 𝖽 |vertices f| ) + 𝖽 |vertices f|"
      using dist by(simp add:finals_def ListSum_conv_sum)
    also have " = (fset(finals g)  {f}. 𝖽 |vertices f| )"
      using f by simp
    also have "  (fset(finals g'). 𝖽 |vertices f| )"
      using f subset by(fastforce intro!: sum_mono2)
    also have " = (∑⇘ffinals g'𝖽 |vertices f| )"
      using dist' by(simp add:finals_def ListSum_conv_sum)
    finally show "(∑⇘ffinals g𝖽 |vertices f| ) + 𝖽 |vertices f|
           (∑⇘ffinals g'𝖽 |vertices f| )" .
  qed
  with size show ?thesis by blast
qed


definition close :: "graph  vertex  vertex  bool" where
"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 ug: "u : 𝒱 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 ug f]
  note distf = minGraphProps3[OF mgp minGraphProps5[OF mgp ug 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 ug 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 ug 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 ug f] by blast
    thus ?thesis by(auto simp:close_def)
  qed
qed


lemma sep_conv:
assumes mgp: "minGraphProps g" and "V  𝒱 g"
shows "separated g V = (uV.vV. u  v  ¬ close g u v)" (is "?P = ?Q")
proof
  assume sep: ?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
    have "u : 𝒱 g" using u : V V  𝒱 g by blast
    note uf = minGraphProps6[OF mgp u : 𝒱 g 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 sep f uv
          by(simp add:separated_def separated2_def separated3_def)
      next
        assume "v = f  (f  u)"
        moreover hence "v  𝒱 f" using u  𝒱 f by simp
        moreover have "|vertices f|  4" using 4 by arith
        ultimately show False using sep f uv u  𝒱 f
          apply(unfold separated_def separated2_def separated3_def)
(* why does blast get stuck? *)
          apply(subgoal_tac "f  (f  u)  𝒱 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 sep f uv
        by(simp add:separated_def separated2_def separated3_def)
    qed
  qed
next
  assume not_cl: ?Q
  show ?P
  proof(simp add:separated_def, rule conjI)
    show "separated2 g V"
    proof (clarsimp simp:separated2_def)
      fix v f assume a: "v  V" "f  set (facesAt g v)" "f  v  V"
      have "v : 𝒱 g" using a(1) V  𝒱 g by blast
      show False using a not_cl mgp_facesAt_no_loop[OF mgp v : 𝒱 g a(2)]
        by(fastforce simp: close_def split:if_split_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"
      have vg: "v : 𝒱 g" using v : V V  𝒱 g by blast
      note distf = minGraphProps3[OF mgp minGraphProps5[OF mgp vg f]]
      note vf = minGraphProps6[OF mgp vg f]
      { fix u assume "u  𝒱 f" and "u  V"
        have "u = v"
        proof cases
          assume 3: "|vertices f| = 3"
          hence "𝒱 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:if_split_asm)
          }
          moreover
          { assume "u = f  (f  v)"
            hence fu: "f  u = v"
              by(simp add: tri_next3_id[OF 3 distf v  𝒱 f])
            hence "(u,v)   f" using nextVertex_in_edges[OF u  𝒱 f]
              by(simp add:fu)
            then obtain f' where "f'  set(facesAt g v)" "(v,u)    f'"
              using mgp_edge_face_ex[OF mgp vg f] by blast
            hence "u = v" using not_cl u  V v  V 3
              by(force simp:close_def edges_face_eq split:if_split_asm)
          }
          ultimately show "u=v" using u  𝒱 f by blast
        next
          assume 3: "|vertices f|  3"
          hence 4: "|vertices f| = 4"
            using len mgp_vertices3[OF mgp minGraphProps5[OF mgp vg f]] by arith
          hence "𝒱 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:if_split_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:if_split_asm)
          }
          moreover
          { assume "u = f  (f  (f  v))"
            hence fu: "f  u = v"
              by(simp add: quad_next4_id[OF 4 distf v  𝒱 f])
            hence "(u,v)   f" using nextVertex_in_edges[OF u  𝒱 f]
              by(simp add:fu)
            then obtain f' where "f'  set(facesAt g v)" "(v,u)    f'"
              using mgp_edge_face_ex[OF mgp vg f] by blast
            hence "u = v" using not_cl u  V v  V 4
              by(force simp:close_def edges_face_eq split:if_split_asm)
          }
          ultimately show "u=v" using u  𝒱 f by blast
        qed
      }
      thus "𝒱 f  V = {v}" using v  V vf by blast
    qed
  qed
qed

lemma sep_ne: "P  M. separated g (fst ` P)"
by(unfold separated_def separated2_def separated3_def) blast

lemma ExcessNotAtRec_conv_Max:
assumes mgp: "minGraphProps g"
shows "set(map fst ps)  𝒱 g  distinct(map fst ps) 
  ExcessNotAtRec ps g =
  Max{ pP. snd p |P. P  set ps  separated g (fst ` P)}"
  (is "_  _  _ = Max(?M ps)" is "_  _  _ = Max{_ |P. ?S ps P}")
proof(induct ps rule: length_induct)
  case (1 ps0)
  note IH = 1(1) and subset = 1(2) and dist = 1(3)
  show ?case
  proof (cases ps0)
    case Nil thus ?thesis by simp
  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  close g (fst p)"])
      apply(simp add: filter_map o_def)
      done
    have "fst p : 𝒱 g" and "fst ` set ps  𝒱 g"
      using subset Cons by auto
    have sub1: "P Q. P  {x : set ps. Q x}  fst ` P  𝒱 g"
      using subset Cons by auto
    have sub2: "P Q. P  insert p {x : set ps. Q x}  fst ` P  𝒱 g"
      using subset Cons by auto
    have sub3: "P. P  insert p (set ps)  fst ` P  𝒱 g"
      using subset Cons by auto
    have "a. set (map fst (deleteAround g a ps))  𝒱 g"
      using deleteAround_subset[of g _ ps] subset Cons
      by auto
    hence "ExcessNotAtRec ps0 g = max (Max(?M ps)) (Max(?M ?ps) + snd p)"
      using Cons IH subset le dist dist' by (cases p) simp
    also have "Max (?M ?ps) + snd p =
      Max {(pP. snd p) + snd p | P. ?S ?ps P}"
      by (auto simp add:setcompr_eq_image Max_add_commute[symmetric] sep_ne intro!: arg_cong [where f=Max])
    also have "{(pP. snd p) + snd p |P. ?S ?ps P} =
      {sum snd (insert p P) |P. ?S ?ps P}"
      using dist Cons
      apply (auto simp:delAround_def)
      apply(rule_tac x=P in exI)
      apply(fastforce intro!: sum.insert[THEN trans,symmetric] elim: finite_subset)
      apply(rule_tac x=P in exI)
      apply(fastforce intro!: sum.insert[THEN trans] elim: finite_subset)
      done
    also have " = {sum snd P |P.
            P  insert p (set ?ps)  p  P  separated g (fst ` P)}"
      apply(auto simp add:sep_conv[OF mgp] sub1 sub2 delAround_def cong: conj_cong)
      apply(rule_tac x = "insert p P" in exI)
      apply simp
      apply(rule conjI) apply blast
      using image fst (set ps)  𝒱 g fst p : 𝒱 g
      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 " = {sum snd P |P.
            P  insert p (set ps)  p  P  separated g (fst ` P)}"
      using Cons dist
      apply(auto simp add:sep_conv[OF mgp] sub2 sub3 delAround_def cong: conj_cong)
      apply(rule_tac x = "P" in exI)
      apply simp
      apply auto
      done
    also have "max (Max(?M ps)) (Max ) = Max(?M ps  {sum snd P |P.
            P  insert p (set ps)  p  P  separated g (fst ` P)})"
      (is "_ = Max ?U")
    proof -
      have "{sum snd P |P.
            P  insert p (set ps)  p  P  separated g (fst ` P)}  {}"
        apply simp
        apply(rule_tac x="{p}" in exI)
        using fst p : 𝒱 g by(simp add:sep_conv[OF mgp])
      thus ?thesis by(simp add: Max_Un sep_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 o_def)



lemma mono_ExcessTab: "g'  set (next_plane0⇘pg); 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:if_split_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_plane0⇘pg); inv g; u  𝒱 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:if_split_asm)

lemma ExcessTab_vertex:
 "p  set(ExcessTable g (vertices g))  fst p  𝒱 g"
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:if_split_asm)

lemma fst_set_ExcessTable_subset:
 "fst ` set (ExcessTable g (vertices g))  𝒱 g"
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:if_split_asm)

lemma next_plane0_incr_ExcessNotAt:
 "g'  set (next_plane0⇘pg); 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]
  fst_set_ExcessTable_subset)
apply(rule Max_mono)
  prefer 2 apply (simp add: sep_ne)
 prefer 2 apply (simp)
apply auto
apply(rule_tac x=P in exI)
apply auto
apply(subgoal_tac "fst ` P  𝒱 g'")
 prefer 2 apply (blast dest: ExcessTab_vertex)
apply(subgoal_tac "fst ` P  𝒱 g")
 prefer 2 apply (blast dest: ExcessTab_vertex)
apply(simp add:sep_conv)
apply (blast intro:close_antimono ExcessTab_final ExcessTab_vertex)
done
(* close -> in neibhood ?? *)


lemma next_plane0_incr_squander_lb:
 "g'  set (next_plane0⇘pg); 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:if_split_asm)
apply(drule (4) genPoly_incr_facesquander_lb)
apply arith
done

lemma inv_notame:
 "g'  set (next_plane0⇘pg); inv g; notame7 g
   notame7 g'"
apply(simp add:notame_def notame7_def tame11b_def is_tame13a_def tame10ub_def del:disj_not1)
apply(frule inv_mgp)
apply(frule (1) next_plane0_vertices_subset)
apply(erule disjE)
 apply(simp add:vertices_graph)
apply(rule disjI2)
apply(erule disjE)
 apply clarify
 apply(frule (2) next_plane0_incr_degree)
 apply(frule (2) next_plane0_incr_except)
 apply (force split:if_split_asm)
apply(frule (1) next_plane0_incr_squander_lb)
apply(arith)
done


lemma inv_inv_notame:
 "invariant(λg. inv g  notame7 g) next_plane⇘p⇙"
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  notame7 g)"
proof(clarsimp simp add: notame_def notame7_def untame_def tame11b_def is_tame13a_def tame10ub_def
                         linorder_not_le linorder_not_less)
  fix g assume "final g" "inv g" "tame g"
    and cases: "15 < countVertices g 
                (v𝒱 g. (except g v = 0  7 < degree g v) 
                            (0 < except g v  6 < degree g v))
                 squanderTarget  squanderLowerBound g"
                (is "?A  ?B  ?C" is "_  (v𝒱 g. ?B' v)  _")
  from cases show False
  proof(elim disjE)
    assume ?B
    then obtain v where v: "v 𝒱 g" "?B' v" by auto
    show False
    proof cases
      assume "except g v = 0"
      thus False using tame g v by(auto simp: tame_def tame11b_def)
    next
      assume "except g v  0"
      thus False using tame g v
        by(auto simp: except_def filter_empty_conv tame_def tame11b_def
          minGraphProps_facesAt_eq[OF inv_mgp[OF inv g]] split:if_split_asm)
    qed
  next
    assume ?A
    thus False using tame g  by(simp add:tame_def tame10_def)
  next
    assume ?C
    thus False using total_weight_lowerbound[OF inv g final g tame g]
      tame g  by(force simp add:tame_def tame13a_def)
  qed
qed


lemma polysizes_tame:
 " g'  set (generatePolygon n v f g); inv g; f  set(nonFinals g);
   v  𝒱 f; 3  n; n < 4+p; n  set(polysizes p g) 
  notame7 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 notame7_def is_tame13a_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 
   notame7 g'"
by(fastforce simp:generatePolygon_def generatePolygonTame_def enum_enumerator
                 notame_def notame7_def)

declare upt_Suc[simp del] (* FIXME global? *)
lemma excess_notame:
 " inv g; g'  set (next_plane⇘pg); g'  set (next_tame0 p g) 
        notame7 g'"
apply(frule (1) mgp_next_plane0_if_next_plane[OF inv_mgp])
apply(auto simp add:next_tame0_def next_plane_def split:if_split_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))  𝒱(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: " Seed⇘p[next_plane p]→* g; final g; tame g 
  Seed⇘p[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 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_tame: "invariant inv next_tame⇘p⇙"
apply(simp add:next_tame_def)
apply(rule inv_subset[OF inv_inv_next_tame0])
apply auto
done

lemma mgp_TameEnum: "g  TameEnum⇘p minGraphProps g"
by (unfold TameEnumP_def)
   (blast intro: RTranCl_inv[OF inv_inv_next_tame] inv_Seed inv_mgp)


end