Theory Kruskal_Time

theory Kruskal_Time
  imports MaxNode_Impl
    Union_Find_Time
begin





locale Kruskal_final = Kruskal_intermediate  E forest connected path weight 
  for E :: "nat uprod set" and forest connected path
      and weight :: "nat uprod ⇒ int"
    + fixes getEdges getEdges_time getEdges_impl
  assumes E: "E ≠{}"
    and getEdges_Spec: "getEdges ≤ ⇓ Id (getEdges' weight E (enat (getEdges_time (card E))))"
    and getEdges_impl_refines: 
          "(uncurry0 getEdges_impl, uncurry0 getEdges) ∈ unit_assn⇧k
                   →⇩a list_assn (nat_assn ×⇩a int_assn ×⇩a nat_assn)" 
begin
 
sublocale  Kruskal_intermediate_Impl E forest connected path weight getEdges getEdges_impl
      "getEdges_time (card E)" "sortEdges'_time (card E)" "uf_init_time (Suc (Max V))"
      "uf_cmp_time (Suc (Max V))" "uf_union_time (Suc (Max V))"
      is_uf uf_init uf_init_time uf_cmp uf_cmp_time uf_union uf_union_time
      sortEdges' sortEdges'_time
  apply(unfold_locales)
        apply (fact E)
       apply(fact getEdges_Spec)
      apply(fact getEdges_impl_refines)
  by auto 


thm kruskal_correct_forest
 

term minBasis_time
thm minBasis_time_def

definition (in -) "kruskal_time gt  ≡ λ(cE, M). gt cE + sortEdges'_time cE + (12 + uf_init_time (Suc M)) + cE * (uf_cmp_time (Suc M) + (23 + uf_union_time (Suc M)))"
definition (in -) "kruskal_time'  ≡ λ(cE, M). sortEdges'_time cE + (12 + uf_init_time (M + 1)) + cE * (uf_cmp_time (M + 1) + (23 + uf_union_time (M + 1)))"

term minBasis_time

lemma mBT: "minBasis_time = kruskal_time getEdges_time (card E, Max V)"
  unfolding minBasis_time_def kruskal_time_def by simp


lemma k_c: "<timeCredit_assn (kruskal_time getEdges_time (card E, Max V))> kruskal <λr. ∃⇩Ara. hr_comp (da_assn id_assn) lst_graph_rel ra r * ↑ (MST ra)>⇩t"
  unfolding mBT[symmetric] using kruskal_correct_forest by simp

thm sortEdges'_time_bound uf_init_bound uf_cmp_time_bound uf_union_time_bound

lemma uf_init_bound[asym_bound]: "uf_init_time ∈ Θ(λn. n)" 
  unfolding uf_init_time_def by auto2

lemma (in -) kruskal_time'_bound:
  shows "kruskal_time'  ∈ Θ⇩2(λ(E::nat,M::nat). E * ln E + M + E * ln M )"
  unfolding kruskal_time'_def
  by (auto2)

lemma (in -) kruskal_time_split: "kruskal_time gt  = (λ(cE,M). gt cE) +  kruskal_time'"
  apply(rule ext) apply (simp add: kruskal_time'_def kruskal_time_def) by auto

lemma (in -) polylog00: "polylog 0 0 m = 1" unfolding polylog_def by simp

lemma (in -) kruskal_time_plus_linear:
  assumes "gt ∈ Θ(λn. n)"
  shows "kruskal_time gt ∈ Θ⇩2(λ(E::nat,M::nat). E * ln E + M + E * ln M )" (is "_ ∈ ?T")
proof -
  have A: "(λx. real (gt (fst x))) ∈ Θ⇩2 (λ(n::nat, m::nat). real n)"
    using mult_Theta_bivariate1[unfolded polylog2_def polylog_def, of gt 1 0 ]
    apply auto using assms by simp

  have split: "⋀x. gt (fst x) + kruskal_time' x = kruskal_time gt x"
    unfolding kruskal_time'_def kruskal_time_def by auto

  have r: "(λx. real (gt (fst x) + kruskal_time' x)) ∈ Θ⇩2 ((λx. case x of (n, m) ⇒ real n) + (λx. case x of (E, M) ⇒ real E * ln (real E) + real M + real E * ln (real M)))"
    apply(rule bigtheta_add[OF _ _ A kruskal_time'_bound ])
    subgoal apply(auto simp: eventually_nonneg_def eventually_sequentially)
       
      using eventually_prod_same by force  
    subgoal apply(auto simp: eventually_nonneg_def eventually_sequentially)
      apply(subst eventually_prod_same) apply auto apply(rule exI[where x="λx. x≥1"])
      by simp
    done

  { fix x y :: nat and c
    assume t: "y≥1 " " x≥1 " " 1 ≤ c * ln (real x)" "c>0"
    then have t': "real y + real x * ln (real y) ≥ 0"  
      by simp  
    from t have "real x ≤ c * real x * ln (real x)" by auto
    also have "… ≤ c * (real x * ln (real x) + real y + real x * ln (real y)) " 
      using t' t by auto 
    finally
    have "real x ≤ c * (real x * ln (real x) + real y + real x * ln (real y)) " .
  } note blub = this



  have 2: "?T = Θ⇩2 ((λx. case x of (n, m) ⇒ real n) + (λx. case x of (E, M) ⇒ real E * ln (real E) + real M + real E * ln (real M)))"
    apply(subst plus_absorb1')
    subgoal apply(rule landau_o.smallI) apply(subst eventually_prod_same) 
      subgoal for c apply(rule exI[where x="λx::nat. real x ≤ c * ¦real x * ln (real x)¦ ∧ x≥1"])
        apply safe subgoal apply(simp add: eventually_sequentially) apply (rule exI[where x="max (max 1 (nat (ceiling (exp (1/c))))) (nat (ceiling (1/c)))"])
          apply auto  
          by (metis exp_gt_zero exp_le_cancel_iff exp_ln less_le_trans mult.commute pos_divide_le_eq)    
          apply auto  apply(rule blub) by auto       
        done
    by simp

  show ?thesis 
    unfolding split[symmetric] 2
    using r .
qed 

end


end