Theory BMSSP_Bucketed_Runtime
theory BMSSP_Bucketed_Runtime
imports BMSSP_Top_Level_Bounds BMSSP_Bucketed_Cost_Bridge
begin
section ‹Non-Conditional Bucketed Running-Time Bound›
text ‹
The capstone of 🗏‹BMSSP_Bucketed_Cost_Bridge.thy› is conditional: it
assumes a cost function already bounded by the refined graph-time expression
with the bucketed costs in the Insert and BatchPrepend slots. This theory
discharges that assumption against an actual costed BMSSP run, producing a
hypothesis-free ‹O(m * log⇧2⇧/⇧3 n)› bound that carries the bucketed
operation costs.
The key structural fact making this possible is that the local-budget
amortised theorem
‹direct_insert_costed_bmssp_amortized_bound_from_local_budgets_with_invariants›
is parametric in the level geometry ‹M_of›/‹cap› and in the per-operation
costs ‹t›/‹h› \emph{independently}. We therefore keep the level geometry at
the paper's schedule exponents ‹p = log⇧1⇧/⇧3›, ‹q = log⇧2⇧/⇧3› (so the
recursion tree, pivot growth, and pull blocks are unchanged), while charging
Insert at the bucketed budget ‹9 + q› and BatchPrepend at ‹2 + p›. Because
the FindPivots pivot set ‹find_pivots_pivots_capped› depends only on the
geometry, not on the costs, the same emptiness argument that makes the existing
headline total applies here verbatim, so the bound is total in ‹N›.
Throughout, ‹D› is a fixed outdegree bound and the running graph is the locale
graph of @{locale strict_tie_breaking_digraph}.
›
subsection ‹A One-Third-Scale Envelope for the BatchPrepend Cost›
text ‹
The BatchPrepend cost ‹2 + p› here grows like ‹p = log⇧1⇧/⇧3› (the schedule
parameter), not a constant. This envelope, the one-third analogue of the
two-thirds envelope in the cost bridge, shows it stays within a constant
multiple of ‹log⇧1⇧/⇧3› --- exactly the ‹H_bound› the recurrence solver needs.
›
lemma const_plus_one_third_param_le_one_third_factor:
"eventually
(λn. real (c + sssp_log_one_third_param n) ≤
real (c + 2) * sssp_log_factor_one_third n) at_top"
using eventually_one_le_sssp_log_factor_one_third
proof eventually_elim
case (elim n)
have one_le: "1 ≤ sssp_log_factor_one_third n"
using elim .
have param_le:
"real (sssp_log_one_third_param n) ≤ sssp_log_factor_one_third n + 1"
proof -
have nonneg: "0 ≤ sssp_log_factor_one_third n"
using one_le by linarith
have "real (nat ⌈sssp_log_factor_one_third n⌉) =
of_int ⌈sssp_log_factor_one_third n⌉"
using of_nat_int_ceiling[OF nonneg] .
moreover have "of_int ⌈sssp_log_factor_one_third n⌉ ≤
sssp_log_factor_one_third n + 1"
using ceiling_correct[of "sssp_log_factor_one_third n"] by linarith
ultimately show ?thesis
unfolding sssp_log_one_third_param_def by simp
qed
have c_le: "real c ≤ real c * sssp_log_factor_one_third n"
proof -
have "real c * 1 ≤ real c * sssp_log_factor_one_third n"
by (rule mult_left_mono[OF one_le]) simp
then show ?thesis by simp
qed
have "real (c + sssp_log_one_third_param n) =
real c + real (sssp_log_one_third_param n)"
by simp
also have "… ≤ real c + (sssp_log_factor_one_third n + 1)"
using param_le by linarith
also have "… ≤ real c * sssp_log_factor_one_third n +
2 * sssp_log_factor_one_third n"
using c_le one_le by linarith
also have "… = real (c + 2) * sssp_log_factor_one_third n"
by (simp add: algebra_simps)
finally show ?case .
qed
text ‹
An affine version used for the vertex factor ‹A = a * p + b›: it is dominated
by ‹(2 a + b)› times the one-third log factor, hence ‹O(log⇧1⇧/⇧3)›.
›
lemma affine_one_third_param_le_one_third_factor:
"eventually
(λn. real (a * sssp_log_one_third_param n + b) ≤
real (2 * a + b) * sssp_log_factor_one_third n) at_top"
using eventually_one_le_sssp_log_factor_one_third
proof eventually_elim
case (elim n)
have one_le: "1 ≤ sssp_log_factor_one_third n"
using elim .
have nonneg: "0 ≤ sssp_log_factor_one_third n"
using one_le by linarith
let ?L = "sssp_log_factor_one_third n"
have param_le:
"real (sssp_log_one_third_param n) ≤ ?L + 1"
proof -
have "real (nat ⌈?L⌉) = of_int ⌈?L⌉"
using of_nat_int_ceiling[OF nonneg] .
moreover have "of_int ⌈?L⌉ ≤ ?L + 1"
using ceiling_correct[of ?L] by linarith
ultimately show ?thesis
unfolding sssp_log_one_third_param_def by simp
qed
have "real (a * sssp_log_one_third_param n + b) =
real a * real (sssp_log_one_third_param n) + real b"
by simp
also have "… ≤ real a * (?L + 1) + real b"
using param_le by (intro add_mono mult_left_mono) simp_all
also have "… = real a * ?L + (real a + real b)"
by (simp add: algebra_simps)
also have "… ≤ real a * ?L + (real a + real b) * ?L"
proof -
have "(real a + real b) * 1 ≤ (real a + real b) * ?L"
by (rule mult_left_mono[OF one_le]) simp
then show ?thesis by simp
qed
also have "… = real (2 * a + b) * ?L"
by (simp add: algebra_simps)
finally show ?case .
qed
context strict_tie_breaking_digraph
begin
subsection ‹A Decoupled Amortised Bound: Geometry Exponent vs.\ Operation Cost›
text ‹
This is the existing level-cap amortised theorem with one generalisation: the
level geometry uses an exponent ‹tg› that is decoupled from the per-Insert
cost ‹t›. In the original theorem the two coincide (‹M_of = bmssp_level_cap k
t›); here ‹M_of = bmssp_level_cap k tg›, while ‹t› remains the cost charged at
each direct insert. The proof is the original one: the local-budget amortised
lemma is parametric in ‹M_of›, ‹cap›, ‹t›, ‹h›, ‹A›, ‹R›, ‹k›, so the only
coupling needed is @{prop "M_of i ≤ cap"} for ‹i ≤ l›, which still holds by
monotonicity of @{const bmssp_level_cap} in the level.
›
theorem finite_initial_label_decoupled_amortized:
assumes all_reachable: "⋀v. v ∈ V ⟹ reachable s v"
and degree: "edge_outdegree_le Δ"
and degree_factor: "Δ ≤ A"
and R_pos: "0 < R"
and insert_factor: "t ≤ A * k"
and insert_scaled_factor: "t ≤ A_insert * k"
and seen_scaled_factor: "k * Δ + A_insert ≤ 2 * A"
and source_factor: "Suc h ≤ 2 * A"
and k_pos: "0 < k"
and run:
"direct_insert_costed_bmssp Δ (bmssp_level_cap k tg) t h k
(bmssp_level_cap k tg l) l
finite_initial_label {s} Infinity d' Infinity U c"
shows "sssp_correct d' ∧
c ≤ bmssp_refined_graph_time_bound (λ_. A) (λ_. R) (λ_. h)
(λ_. l) (λ_. t) (λ_. edge_count) vertex_count"
proof
show "sssp_correct d'"
by (rule finite_initial_label_direct_insert_costed_top_level_correct
[OF all_reachable run])
next
have pre: "bmssp_pre_full finite_initial_label {s} Infinity"
using all_reachable finite_initial_label_source_complete
by (rule top_bmssp_pre_full)
have sound: "sound_label finite_initial_label"
using finite_initial_label_sound[OF all_reachable] .
have S_reaches: "⋀x. x ∈ {s} ⟹ reachable s x"
using all_reachable source_in_V by blast
have below: "⋀x. x ∈ {s} ⟹
below_bound (finite_initial_label x) Infinity"
by simp
have top_cap: "k * card {s} ≤ bmssp_level_cap k tg l"
proof -
have one_le: "1 ≤ bmssp_level_width tg l"
unfolding bmssp_level_width_def by simp
have "k * 1 ≤ k * bmssp_level_width tg l"
by (rule mult_left_mono[OF one_le]) simp
then show ?thesis
unfolding bmssp_level_cap_def by simp
qed
have top_anti: "tree_antichain {s}"
by simp
have amortized:
"c ≤ bmssp_amortized_cost_bound (2 * A) R h t l (2 * l + 1)
Infinity U"
proof (rule direct_insert_costed_bmssp_amortized_bound_from_local_budgets_with_invariants
[where A = "2 * A" and R = R,
OF _ R_pos source_factor k_pos _ _ run sound pre S_reaches below
top_cap top_anti])
show "Δ ≤ 2 * A"
using degree_factor by simp
next
fix i
assume "i ≤ l"
then show "bmssp_level_cap k tg i ≤ bmssp_level_cap k tg l"
by (rule bmssp_level_cap_mono)
next
fix l' d S B D c_insert d' a betas bs B' Us U_loop c_loop
child_costs U
assume D_def:
"D = label_partition_view
(find_pivots_label_capped k (bmssp_level_cap k tg l) d S B)
(find_pivots_pivots_capped k (bmssp_level_cap k tg l) d S B)"
and insert:
"partition_initial_insert_cost_bound c_insert t
(find_pivots_pivots_capped k (bmssp_level_cap k tg l) d S B)"
and loop:
"direct_insert_costed_partition_loop_state Δ (bmssp_level_cap k tg) t h k
(bmssp_level_cap k tg l) l'
(find_pivots_label_capped k (bmssp_level_cap k tg l) d S B)
(find_pivots_pivots_capped k (bmssp_level_cap k tg l) d S B) B d' D
a betas bs B' Us U_loop c_loop child_costs"
and complete:
"complete_on d'
{v ∈ bound_tree S B'.
find_pivots_label_capped k (bmssp_level_cap k tg l) d S B v =
dist s v}"
and U_def:
"U = U_loop ∪
{v ∈ bound_tree S B'.
find_pivots_label_capped k (bmssp_level_cap k tg l) d S B v =
dist s v}"
and sound_s: "sound_label d"
and pre_s: "bmssp_pre_full d S B"
and reaches_s: "⋀x. x ∈ S ⟹ reachable s x"
and below_s: "⋀x. x ∈ S ⟹ below_bound (d x) B"
and S_k_cap: "k * card S ≤ bmssp_level_cap k tg l"
and anti: "tree_antichain S"
have seen_success:
"B' = B ⟹
card (find_pivots_seen_capped k (bmssp_level_cap k tg l) d S B)
≤ card U"
by (rule direct_insert_costed_step_seen_success
[OF loop U_def sound_s pre_s reaches_s below_s])
show "fp_iter_capped_scan_cost k (bmssp_level_cap k tg l) d S S B +
c_insert ≤ 2 * A * card U"
by (rule direct_insert_costed_capped_step_scan_insert_budget_from_scaled_seen_or_threshold
[OF degree degree_factor insert_factor insert_scaled_factor
seen_scaled_factor insert loop U_def sound_s pre_s reaches_s
S_k_cap anti k_pos seen_success])
qed
have post_full:
"bmssp_post_full finite_initial_label {s} Infinity d' Infinity U"
by (rule direct_insert_costed_bmssp_correct[OF run sound pre S_reaches])
have post: "bmssp_post finite_initial_label {s} Infinity d' Infinity U"
using bmssp_post_full_imp_post[OF post_full] .
have U_V: "U = V"
using post bound_tree_source_infinity[OF all_reachable]
unfolding bmssp_post_def by auto
have graph_bound:
"bmssp_amortized_cost_bound (2 * A) R h t l (2 * l + 1) Infinity U
≤ bmssp_refined_graph_time_bound (λ_. A) (λ_. R) (λ_. h)
(λ_. l) (λ_. t) (λ_. edge_count) vertex_count"
proof -
have U_card: "card U = vertex_count"
unfolding U_V vertex_count_def by simp
have out_le: "card (outgoing_edges U) ≤ edge_count"
by (rule edge_count_outgoing_bound)
have range_le: "card (outgoing_edges_range U 0 Infinity) ≤ edge_count"
by (rule card_outgoing_edges_range_le_edge_count)
have out_term:
"(R + l * h) * card (outgoing_edges U) ≤
(R + l * h) * edge_count"
using out_le by simp
have range_term:
"t * card (outgoing_edges_range U 0 Infinity) ≤ t * edge_count"
using range_le by simp
show ?thesis
unfolding bmssp_amortized_cost_bound_def bmssp_refined_graph_time_bound_def
using U_card out_term range_term by (simp add: algebra_simps; linarith)
qed
show "c ≤ bmssp_refined_graph_time_bound (λ_. A) (λ_. R) (λ_. h)
(λ_. l) (λ_. t) (λ_. edge_count) vertex_count"
using amortized graph_bound by linarith
qed
subsection ‹A Costed Run With Decoupled Geometry and Bucketed Costs›
text ‹
‹bmssp_bucketed_run D N› is a top-level costed run whose level geometry uses
the schedule exponents ‹p, q› but whose Insert cost is the bucketed budget
‹9 + q› and whose BatchPrepend cost is ‹2 + p›.
›
definition bmssp_bucketed_run ::
"nat ⇒ nat ⇒ ('a ⇒ real) ⇒ 'a set ⇒ nat ⇒ bool" where
"bmssp_bucketed_run D N d' U c ⟷
(let p = sssp_log_one_third_param N;
q = sssp_log_two_thirds_param N
in exact_concrete_bmssp D (bmssp_level_cap p q) (9 + q) (2 + p) p
(bmssp_level_cap p q p) p
finite_initial_label {s} Infinity d' Infinity U c)"
definition bmssp_bucketed_cost :: "nat ⇒ nat ⇒ nat ⇒ bool" where
"bmssp_bucketed_cost D N c ⟷ (∃d' U. bmssp_bucketed_run D N d' U c)"
definition bmssp_bucketed_time :: "nat ⇒ nat ⇒ nat" where
"bmssp_bucketed_time D N = (LEAST c. bmssp_bucketed_cost D N c)"
subsection ‹Totality of the Bucketed Cost›
text ‹
The same FindPivots-emptiness argument as the existing headline, with the
bucketed costs in the cost slots. Since
‹exact_concrete_bmssp_Suc_exists_if_pivots_empty_same_bound› is
parametric in the costs, the substitution is immediate.
›
lemma bmssp_bucketed_cost_exists_if_top_pivots_empty:
assumes pivots_empty:
"find_pivots_pivots_capped (sssp_log_one_third_param N)
(bmssp_level_cap (sssp_log_one_third_param N)
(sssp_log_two_thirds_param N) (sssp_log_one_third_param N))
finite_initial_label {s} Infinity = {}"
shows "∃c. bmssp_bucketed_cost D N c"
proof -
let ?p = "sssp_log_one_third_param N"
let ?q = "sssp_log_two_thirds_param N"
have p_eq: "?p = Suc (?p - 1)"
using sssp_log_one_third_param_pos[of N] by simp
have source_subset: "{s} ⊆ V"
using source_in_V by simp
have run:
"∃d' U c.
exact_concrete_bmssp D (bmssp_level_cap ?p ?q) (9 + ?q) (2 + ?p) ?p
(bmssp_level_cap ?p ?q ?p) (Suc (?p - 1))
finite_initial_label {s} Infinity d' Infinity U c"
by (rule exact_concrete_bmssp_Suc_exists_if_pivots_empty_same_bound
[OF source_subset _ pivots_empty]) simp
then obtain d' U c where
"exact_concrete_bmssp D (bmssp_level_cap ?p ?q) (9 + ?q) (2 + ?p) ?p
(bmssp_level_cap ?p ?q ?p) (Suc (?p - 1))
finite_initial_label {s} Infinity d' Infinity U c"
by blast
then have root_run:
"exact_concrete_bmssp D (bmssp_level_cap ?p ?q) (9 + ?q) (2 + ?p) ?p
(bmssp_level_cap ?p ?q ?p) ?p
finite_initial_label {s} Infinity d' Infinity U c"
using p_eq by simp
have "bmssp_bucketed_run D N d' U c"
unfolding bmssp_bucketed_run_def
using root_run by (simp add: Let_def)
then have "bmssp_bucketed_cost D N c"
unfolding bmssp_bucketed_cost_def by blast
then show ?thesis
by blast
qed
lemma eventually_bmssp_bucketed_cost:
"eventually (λN. ∃c. bmssp_bucketed_cost D N c) at_top"
using eventually_top_level_pivots_empty[of finite_initial_label Infinity]
proof eventually_elim
case (elim N)
show ?case
by (rule bmssp_bucketed_cost_exists_if_top_pivots_empty[OF elim])
qed
lemma bmssp_bucketed_time_witness:
assumes "bmssp_bucketed_cost D N c"
shows "bmssp_bucketed_cost D N (bmssp_bucketed_time D N)"
unfolding bmssp_bucketed_time_def
by (rule LeastI_ex) (use assms in blast)
subsection ‹Cost Bound for a Bucketed Run›
text ‹
A bucketed run refines a direct-insert run with the same (decoupled) geometry
and costs, to which the decoupled amortised theorem applies. Choosing
‹A = Suc D * p + 9› makes the local-budget side conditions hold for \emph{all}
‹N› (the binding constraint ‹9 + q ≤ A * p› follows from ‹q ≤ p⇧2› and
‹9 ≤ 9 * p›), and ‹A› still grows only like ‹log⇧1⇧/⇧3›.
›
lemma bmssp_bucketed_run_refined_bound:
assumes all_reachable: "⋀v. v ∈ V ⟹ reachable s v"
and degree: "edge_outdegree_le D"
and run: "bmssp_bucketed_run D N d' U c"
shows "c ≤ bmssp_refined_graph_time_bound
(λ_. Suc D * sssp_log_one_third_param N + 9)
(λ_. sssp_log_two_thirds_param N)
(λ_. 2 + sssp_log_one_third_param N)
(λ_. sssp_log_one_third_param N)
(λ_. 9 + sssp_log_two_thirds_param N)
(λ_. edge_count) vertex_count"
proof -
let ?p = "sssp_log_one_third_param N"
let ?q = "sssp_log_two_thirds_param N"
let ?A = "Suc D * ?p + 9"
have direct:
"direct_insert_costed_bmssp D (bmssp_level_cap ?p ?q) (9 + ?q) (2 + ?p) ?p
(bmssp_level_cap ?p ?q ?p) ?p
finite_initial_label {s} Infinity d' Infinity U c"
by (rule exact_concrete_bmssp_refines_direct_insert
[OF run[unfolded bmssp_bucketed_run_def Let_def]])
have p_pos: "0 < ?p" by simp
have p_ge1: "1 ≤ ?p" using p_pos by linarith
have q_le_sq: "?q ≤ ?p * ?p"
by (rule sssp_log_two_thirds_param_le_one_third_square)
have degree_factor: "D ≤ ?A"
proof -
have "D ≤ Suc D * ?p"
using p_pos by (cases ?p) simp_all
then show ?thesis by simp
qed
have insert_factor: "9 + ?q ≤ ?A * ?p"
proof -
have "9 + ?q ≤ 9 * ?p + ?p * ?p"
using q_le_sq p_ge1 by (simp add: algebra_simps; linarith)
also have "… ≤ 9 * ?p + Suc D * ?p * ?p"
by simp
also have "… = ?A * ?p"
by (simp add: algebra_simps)
finally show ?thesis .
qed
have insert_scaled_factor: "9 + ?q ≤ ?A * ?p"
by (rule insert_factor)
have seen_scaled_factor: "?p * D + ?A ≤ 2 * ?A"
proof -
have "?p * D ≤ Suc D * ?p"
by (simp add: algebra_simps)
also have "… ≤ ?A"
by simp
finally have "?p * D ≤ ?A" .
then show ?thesis by simp
qed
have source_factor: "Suc (2 + ?p) ≤ 2 * ?A"
proof -
have "2 * ?A = 2 * Suc D * ?p + 18"
by (simp add: algebra_simps)
moreover have "2 * ?p ≤ 2 * Suc D * ?p"
by (simp add: algebra_simps)
ultimately have "2 * ?p + 18 ≤ 2 * ?A"
by linarith
moreover have "Suc (2 + ?p) ≤ 2 * ?p + 18"
by simp
ultimately show ?thesis by linarith
qed
have R_pos: "0 < ?q"
by (rule sssp_log_two_thirds_param_pos)
have "sssp_correct d' ∧
c ≤ bmssp_refined_graph_time_bound
(λ_. ?A) (λ_. ?q) (λ_. 2 + ?p)
(λ_. ?p) (λ_. 9 + ?q) (λ_. edge_count) vertex_count"
by (rule finite_initial_label_decoupled_amortized
[OF all_reachable degree degree_factor R_pos insert_factor
insert_scaled_factor seen_scaled_factor source_factor p_pos direct])
then show ?thesis
by blast
qed
subsection ‹The Non-Conditional Bucketed Running-Time Bound›
text ‹
Assembling the pieces. Totality of the bucketed cost (via the
FindPivots-emptiness argument) discharges the existence premise; the cost
bound discharges the recurrence premise; and the schedule envelopes for the
five cost parameters discharge the component bounds. Nothing is left
conditional: the bucketed BMSSP running time is ‹O(m * log⇧2⇧/⇧3 n)›.
›
theorem bmssp_bucketed_time_bigo_sssp_time_target:
fixes m :: "nat ⇒ nat"
and Cn Cm :: real
assumes all_reachable: "⋀v. v ∈ V ⟹ reachable s v"
and degree: "edge_outdegree_le D"
and Cn_pos: "0 < Cn"
and Cm_pos: "0 < Cm"
and vc_dom: "eventually (λn. real vertex_count ≤ Cn * real (m n)) at_top"
and ec_dom: "eventually (λn. real edge_count ≤ Cm * real (m n)) at_top"
shows "(λn. real (bmssp_bucketed_time D n)) ∈ O(λn. sssp_time_target m n)"
proof (rule bmssp_refined_cost_bound_bigo_sssp_time_target_from_component_bounds_slack)
show "0 < Cn" by (rule Cn_pos)
show "0 < Cm" by (rule Cm_pos)
show "eventually (λn. real ((λ_. vertex_count) n) ≤ Cn * real (m n)) at_top"
using vc_dom by simp
show "eventually (λn. real ((λ_. edge_count) n) ≤ Cm * real (m n)) at_top"
using ec_dom by simp
show "eventually
(λn. real (Suc D * sssp_log_one_third_param n + 9) ≤
real (2 * Suc D + 9) * sssp_log_factor_one_third n) at_top"
using affine_one_third_param_le_one_third_factor[of "Suc D" 9] by simp
show "eventually
(λn. real (sssp_log_one_third_param n) ≤ 2 * sssp_log_factor_one_third n)
at_top"
using const_plus_one_third_param_le_one_third_factor[of 0] by simp
show "eventually
(λn. real (sssp_log_two_thirds_param n) ≤ 2 * sssp_log_factor n) at_top"
using const_plus_two_thirds_param_le_two_thirds_factor[of 0] by simp
show "eventually
(λn. real (9 + sssp_log_two_thirds_param n) ≤ 11 * sssp_log_factor n)
at_top"
using const_plus_two_thirds_param_le_two_thirds_factor[of 9] by simp
show "eventually
(λn. real (2 + sssp_log_one_third_param n) ≤
4 * sssp_log_factor_one_third n) at_top"
using const_plus_one_third_param_le_one_third_factor[of 2] by simp
have cost_ev: "eventually
(λn. bmssp_bucketed_time D n ≤
bmssp_refined_graph_time_bound
(λ_. Suc D * sssp_log_one_third_param n + 9)
(λ_. sssp_log_two_thirds_param n)
(λ_. 2 + sssp_log_one_third_param n)
(λ_. sssp_log_one_third_param n)
(λ_. 9 + sssp_log_two_thirds_param n)
(λ_. edge_count) vertex_count) at_top"
proof (rule eventually_mono[OF eventually_bmssp_bucketed_cost])
fix n :: nat
assume "∃c. bmssp_bucketed_cost D n c"
then obtain c where c: "bmssp_bucketed_cost D n c"
by blast
have cost: "bmssp_bucketed_cost D n (bmssp_bucketed_time D n)"
by (rule bmssp_bucketed_time_witness[OF c])
then obtain d' U where run:
"bmssp_bucketed_run D n d' U (bmssp_bucketed_time D n)"
unfolding bmssp_bucketed_cost_def by blast
show "bmssp_bucketed_time D n ≤
bmssp_refined_graph_time_bound
(λ_. Suc D * sssp_log_one_third_param n + 9)
(λ_. sssp_log_two_thirds_param n)
(λ_. 2 + sssp_log_one_third_param n)
(λ_. sssp_log_one_third_param n)
(λ_. 9 + sssp_log_two_thirds_param n)
(λ_. edge_count) vertex_count"
by (rule bmssp_bucketed_run_refined_bound[OF all_reachable degree run])
qed
show "eventually
(λn. bmssp_bucketed_time D n ≤
bmssp_refined_graph_time_bound
(λ_. Suc D * sssp_log_one_third_param n + 9)
(λ_. sssp_log_two_thirds_param n)
(λ_. 2 + sssp_log_one_third_param n)
(λ_. sssp_log_one_third_param n)
(λ_. 9 + sssp_log_two_thirds_param n)
(λ_. (λ_. edge_count) n) ((λ_. vertex_count) n)) at_top"
using cost_ev by simp
qed auto
text ‹
The sparse-graph specialisation, fully closed: for the bounded-outdegree
locale graph with at least one edge, the bucketed BMSSP running time is
‹O(m * (ln n) powr (2/3))›, where the Insert and BatchPrepend costs charged
inside the recurrence are the actual bucketed budgets, not free parameters.
›
theorem bmssp_bucketed_runtime_bigo_target:
assumes all_reachable: "⋀v. v ∈ V ⟹ reachable s v"
and degree: "edge_outdegree_le D"
and edge_count_pos: "0 < edge_count"
shows "(λn. real (bmssp_bucketed_time D n)) ∈
O(λn. real edge_count * (ln (real n + 2)) powr (2 / 3))"
proof -
have vertex_le: "vertex_count ≤ 2 * edge_count"
by (rule vertex_count_le_twice_edge_count_if_all_reachable
[OF all_reachable edge_count_pos])
have "(λn. real (bmssp_bucketed_time D n)) ∈
O(λn. sssp_time_target (λ_. edge_count) n)"
proof (rule bmssp_bucketed_time_bigo_sssp_time_target [OF all_reachable degree])
show "0 < (2::real)" by simp
show "0 < (1::real)" by simp
show "eventually (λn. real vertex_count ≤ 2 * real edge_count) at_top"
using vertex_le by simp
show "eventually (λn. real edge_count ≤ 1 * real edge_count) at_top"
by simp
qed
then show ?thesis
unfolding sssp_time_target_def sssp_log_factor_def by simp
qed
end
end