Theory Examples

theory
  Examples
  imports 
  "Kruskal/Kruskal_Time"
  "BinarySearch"
  "FloydWarshall/FW_Code"
  "Remdups"
  "EdmondsKarp_Maxflow/EdmondsKarp_Time"
begin 

section ‹Remdups›


term remdups_spec    ― ‹The specification for remdups›
term rd_impl1         ― ‹The abstract algorithm in the NREST monad›
thm rd_impl1_correct  ― ‹The correctness theorem›

term remdups_impl    ― ‹The synthesised Imperative/HOL program›


lemma "<$ (remdups_time (length as))> 
          remdups_impl as
        <λr. ∃⇩Ara. da_assn id_assn ra r * ↑ (set as = set ra ∧ distinct ra)>⇩t"
  by(rule remdups_rule)

lemma "remdups_time ∈ Θ(λn. n * ln n)"
  by(fact remdups_time_nln)



section ‹Binary Search›

term binarysearch_SPEC    ― ‹The specification for binary search›
term binarysearch         ― ‹The abstract algorithm in the NREST monad›
thm binarysearch_correct  ― ‹The correctness theorem›

term binarysearch_impl    ― ‹The synthesised Imperative/HOL program›

lemma binary_search_correct: 
  assumes "sorted xs"  "l ≤ r" "r ≤ length xs"
  shows  
    "<array_assn xs p * $(binarysearch_time (r - l))> 
        binarysearch_impl l r x p
     <λra.   array_assn xs p * ↑ (ra ⟷ (∃i≥l. i < r ∧ xs ! i = x))>⇩t"
  using assms binary_search_correct by blast

lemma binary_search_time_ln: "binarysearch_time ∈ Θ(λn. ln (real n))"
  by(fact binary_search_time_ln)


section ‹Floyd Warshall›

term fw_spec              ― ‹The specification for FloydWarshall›
term fw'                  ― ‹The abstract algorithm in the NREST monad›
thm fw'_spec              ― ‹The correctness theorem›

term fw_impl    ― ‹The synthesised Imperative/HOL program›

corollary 
  shows
    "<mtx_curry_assn n M Mi * $(fw_time n)>
        fw_impl n Mi
     <λ Mi'. ∃⇩A M'. mtx_curry_assn n M' Mi'
           * ↑(if (∃ i ≤ n. M' i i < 0) then ¬ cyc_free M n
                else ∀i ≤ n. ∀j ≤ n. M' i j = D M i j n ∧ cyc_free M n)>⇩t"
  by(fact fw_correct)     

lemma "fw_time ∈ Θ(λn. n*n*n)"
  by (fact fw_time_n_cube)



section ‹Kruskal›

definition "kruskal getEdges_impl = Kruskal_intermediate_Impl.kruskal getEdges_impl uf_init uf_cmp uf_union sortEdges'"

lemma "kruskal getedges = Gr"
  unfolding kruskal_def apply(subst Kruskal_intermediate_Impl.kruskal_def) oops


lemma
  fixes connected path and E :: "nat uprod set"
  assumes "Kruskal_intermediate E forest connected path"
    ― ‹If we have a set of edges E for a Graph representation that provides
        predicates for forest, connected and path,...›
    and  "E ≠{}" 
    and getEdges_impl_refines: 
    "(uncurry0 getEdges_impl, uncurry0 (getEdges' weight E (enat (getEdges_time (card E))))) ∈ unit_assn⇧k
                   →⇩a list_assn (nat_assn ×⇩a int_assn ×⇩a nat_assn)"
    ― ‹... and an implementation @{term getEdges_impl}, that gives a list of the edges of the Graph
          in time @{term getEdges_time}, ...  ›
    and getEdges_linear: "getEdges_time ∈ Θ(λn. n)"
    ― ‹... and the time bound @{term getEdges_time} is linear, then we can show ...  ›
  shows 
    ― ‹... that kruskal (using the @{term getEdges_impl} subprogram) calculates
          a minimum spanning forest for the graph and ...  ›
    kruskal_correct:
      "<timeCredit_assn (kruskal_time getEdges_time (card E, Max (Kruskal_intermediate_defs.V E)))>
        kruskal getEdges_impl 
       <λr. ∃⇩Ara. hr_comp (da_assn id_assn) (lst_graph_rel' weight) ra r * ↑ (minWeightBasis.minBasis E forest weight ra)>⇩t"
  and
    ― ‹ ... takes time in O( E * ln E + M + E * ln M ), where cE is the cardinality
          of the set of edges E, and M is the maximal node in the graph. ›
    kruska_time_bound:
      "kruskal_time getEdges_time ∈ Θ⇩2(λ(cE::nat,M::nat). cE * ln cE + M + cE * ln M )"
  subgoal 
    unfolding kruskal_def
    apply(rule Kruskal_final.k_c)
    using assms unfolding Kruskal_final_def Kruskal_final_axioms_def by auto
  subgoal  
    apply(rule kruskal_time_plus_linear) by fact
  done


section ‹Edmonds Karp›

context Network_Impl ― ‹given a Network c s t›
begin

term Edka_Impl.edka5          ― ‹The abstract algorithm in the NREST monad›
thm Edka_Impl.edka5_correct'  ― ‹The correctness theorem›

term edka_imp    ― ‹The synthesised Imperative/HOL program›

theorem edka_imp_correct: 
      assumes VN: "Graph.V c = {0..<N}" and "s < N" and "t < N"
      assumes ABS_PS: "is_adj_map am"
      shows "<$(edka_cost (card V, card E))> 
          edka_imp c s t N am 
        <λfi. ∃⇩Af. is_rflow N f fi * ↑(isMaxFlow f)>⇩t"
  apply (rule edka_imp_correct) by fact+

lemma "edka_cost ∈ Θ⇩2(λ(V::nat,E::nat). (V * E) * (V + E) )"
  by(fact final_running_time)

end


end