Theory Dijkstra_Impl_Adet
section ‹Implementation of Dijkstra's-Algorithm using Automatic Determinization›
theory Dijkstra_Impl_Adet
imports
Dijkstra
GraphSpec
HashGraphImpl
Collections.Refine_Dflt_ICF
"HOL-Library.Code_Target_Numeral"
begin
subsection ‹Setup›
subsubsection ‹Infinity›
definition infty_rel_internal_def:
"infty_rel R ≡ {(Num a, Num a')| a a'. (a,a')∈R} ∪ {(Infty,Infty)}"
lemma infty_rel_def[refine_rel_defs]:
"⟨R⟩infty_rel = {(Num a, Num a')| a a'. (a,a')∈R} ∪ {(Infty,Infty)}"
unfolding infty_rel_internal_def relAPP_def by simp
lemma infty_relI:
"(Infty,Infty)∈⟨R⟩infty_rel"
"(a,a')∈R ⟹ (Num a, Num a')∈⟨R⟩infty_rel"
unfolding infty_rel_def by auto
lemma infty_relE:
assumes "(x,x')∈⟨R⟩infty_rel"
obtains "x=Infty" and "x'=Infty"
| a a' where "x=Num a" and "x'=Num a'" and "(a,a')∈R"
using assms
unfolding infty_rel_def
by auto
lemma infty_rel_simps[simp]:
"(Infty,x')∈⟨R⟩infty_rel ⟷ x'=Infty"
"(x,Infty)∈⟨R⟩infty_rel ⟷ x=Infty"
"(Num a, Num a')∈⟨R⟩infty_rel ⟷ (a,a')∈R"
unfolding infty_rel_def by auto
lemma infty_rel_sv[relator_props]:
"single_valued R ⟹ single_valued (⟨R⟩infty_rel)"
unfolding infty_rel_def
by (auto intro: single_valuedI dest: single_valuedD)
lemma infty_rel_id[simp, relator_props]: "⟨Id⟩infty_rel = Id"
apply rule
apply (auto elim: infty_relE) []
apply safe
apply (case_tac b) by auto
consts i_infty :: "interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of infty_rel i_infty]
lemma autoref_infty[param,autoref_rules]:
"(Infty,Infty)∈⟨R⟩infty_rel"
"(Num,Num)∈R→⟨R⟩infty_rel"
"(case_infty,case_infty)∈Rr→(R→Rr)→⟨R⟩infty_rel→Rr"
"(rec_infty,rec_infty)∈Rr→(R→Rr)→⟨R⟩infty_rel→Rr"
unfolding infty_rel_def
by (auto dest: fun_relD)
definition [simp]: "is_Infty x ≡ case x of Infty ⇒ True | _ ⇒ False"
context begin interpretation autoref_syn .
lemma pat_is_Infty[autoref_op_pat]:
"x=Infty ≡ (OP is_Infty :::⇩i ⟨I⟩⇩ii_infty →⇩i i_bool)$x"
"Infty=x ≡ (OP is_Infty :::⇩i ⟨I⟩⇩ii_infty →⇩i i_bool)$x"
by (auto intro!: eq_reflection split: infty.splits)
end
lemma autoref_is_Infty[autoref_rules]:
"(is_Infty, is_Infty)∈⟨R⟩infty_rel → bool_rel"
by (auto split: infty.splits)
definition "infty_eq eq v1 v2 ≡
case (v1,v2) of
(Infty,Infty) ⇒ True
| (Num a1, Num a2) ⇒ eq a1 a2
| _ ⇒ False"
lemma infty_eq_autoref[autoref_rules (overloaded)]:
"⟦ GEN_OP eq (=) (R→R→bool_rel) ⟧
⟹ (infty_eq eq,(=))∈⟨R⟩infty_rel→⟨R⟩infty_rel→bool_rel"
unfolding infty_eq_def[abs_def]
by (auto split: infty.splits dest: fun_relD elim!: infty_relE)
lemma infty_eq_expand[autoref_struct_expand]: "(=) = infty_eq (=)"
by (auto intro!: ext simp: infty_eq_def split: infty.splits)
context begin interpretation autoref_syn .
lemma infty_val_autoref[autoref_rules]:
"⟦SIDE_PRECOND (x≠Infty); (xi,x)∈⟨R⟩infty_rel⟧
⟹ (val xi,(OP val ::: ⟨R⟩infty_rel → R) $ x)∈R"
apply (cases x)
apply (auto elim: infty_relE)
done
end
definition infty_plus where
"infty_plus pl a b ≡ case (a,b) of (Num a, Num b) ⇒ Num (pl a b) | _ ⇒ Infty "
lemma infty_plus_param[param]:
"(infty_plus,infty_plus) ∈ (R→R→R) → ⟨R⟩infty_rel → ⟨R⟩infty_rel → ⟨R⟩infty_rel"
unfolding infty_plus_def[abs_def]
by parametricity
lemma infty_plus_eq_plus: "infty_plus (+) = (+)"
unfolding infty_plus_def[abs_def]
by (auto intro!: ext split: infty.split)
lemma infty_plus_autoref[autoref_rules]:
"GEN_OP pl (+) (R→R→R)
⟹ (infty_plus pl,(+)) ∈ ⟨R⟩infty_rel → ⟨R⟩infty_rel → ⟨R⟩infty_rel"
apply (fold infty_plus_eq_plus)
apply simp
apply parametricity
done
subsubsection ‹Graph›
consts i_graph :: "interface ⇒ interface ⇒ interface"
definition graph_more_rel_internal_def:
"graph_more_rel Rm Rv Rw ≡ { (g,g').
(graph.nodes g, graph.nodes g')∈⟨Rv⟩set_rel
∧ (graph.edges g, graph.edges g')∈⟨⟨Rv,⟨Rw,Rv⟩prod_rel⟩prod_rel⟩set_rel
∧ (graph.more g, graph.more g')∈Rm}"
lemma graph_more_rel_def[refine_rel_defs]:
"⟨Rm,Rv,Rw⟩graph_more_rel ≡ { (g,g').
(graph.nodes g, graph.nodes g')∈⟨Rv⟩set_rel
∧ (graph.edges g, graph.edges g')∈⟨⟨Rv,⟨Rw,Rv⟩prod_rel⟩prod_rel⟩set_rel
∧ (graph.more g, graph.more g')∈Rm}"
unfolding relAPP_def graph_more_rel_internal_def by simp
abbreviation "graph_rel ≡ ⟨unit_rel⟩graph_more_rel"
lemmas graph_rel_def = graph_more_rel_def[where Rm=unit_rel, simplified]
lemma graph_rel_id[simp]: "⟨Id,Id⟩graph_rel = Id"
unfolding graph_rel_def by auto
lemma graph_more_rel_sv[relator_props]:
"⟦single_valued Rm; single_valued Rv; single_valued Rw⟧
⟹ single_valued (⟨Rm,Rv,Rw⟩graph_more_rel)"
unfolding graph_more_rel_def
apply (rule single_valuedI, clarsimp)
apply (rule graph.equality)
apply (erule (1) single_valuedD[rotated], tagged_solver)+
done
lemma [autoref_itype]:
"graph.nodes ::⇩i ⟨Iv,Iw⟩⇩ii_graph →⇩i ⟨Iv⟩⇩ii_set"
by simp_all
thm is_map_to_sorted_list_def
definition "nodes_to_list g ≡ it_to_sorted_list (λ_ _. True) (graph.nodes g)"
lemma nodes_to_list_itype[autoref_itype]: "nodes_to_list ::⇩i ⟨Iv,Iw⟩⇩ii_graph →⇩i ⟨⟨Iv⟩⇩ii_list⟩⇩ii_nres" by simp
lemma nodes_to_list_pat[autoref_op_pat]: "it_to_sorted_list (λ_ _. True) (graph.nodes g) ≡ nodes_to_list g"
unfolding nodes_to_list_def by simp
definition "succ_to_list g v ≡ it_to_sorted_list (λ_ _. True) (Graph.succ g v)"
lemma succ_to_list_itype[autoref_itype]:
"succ_to_list ::⇩i ⟨Iv,Iw⟩⇩ii_graph →⇩i Iv →⇩i ⟨⟨⟨Iw,Iv⟩⇩ii_prod⟩⇩ii_list⟩⇩ii_nres" by simp
lemma succ_to_list_pat[autoref_op_pat]: "it_to_sorted_list (λ_ _. True) (Graph.succ g v) ≡ succ_to_list g v"
unfolding succ_to_list_def by simp
context graph begin
definition rel_def_internal: "rel Rv Rw ≡ br α invar O ⟨Rv,Rw⟩graph_rel"
lemma rel_def: "⟨Rv,Rw⟩rel ≡ br α invar O ⟨Rv,Rw⟩graph_rel"
unfolding relAPP_def rel_def_internal by simp
lemma rel_id[simp]: "⟨Id,Id⟩rel = br α invar" by (simp add: rel_def)
lemma rel_sv[relator_props]:
"⟦single_valued Rv; single_valued Rw⟧ ⟹ single_valued (⟨Rv,Rw⟩rel)"
unfolding rel_def
by tagged_solver
lemmas [autoref_rel_intf] = REL_INTFI[of rel i_graph]
end
lemma (in graph_nodes_it) autoref_nodes_it[autoref_rules]:
assumes ID: "PREFER_id Rv"
shows "(λs. RETURN (it_to_list nodes_it s),nodes_to_list) ∈ ⟨Rv,Rw⟩rel → ⟨⟨Rv⟩list_rel⟩nres_rel"
unfolding nodes_to_list_def[abs_def]
proof (intro fun_relI nres_relI)
fix s s'
from ID have [simp]: "Rv = Id" by simp
assume "(s,s')∈⟨Rv,Rw⟩rel"
hence INV: "invar s" and [simp]: "nodes s' = nodes (α s)" unfolding rel_def
by (auto simp add: br_def graph_rel_def)
obtain l where
[simp]: "distinct l" "nodes (α s) = set l" "it_to_list nodes_it s = l"
unfolding it_to_list_def
by (metis nodes_it_correct[OF INV, unfolded set_iterator_def set_iterator_genord_def]
foldli_snoc_id self_append_conv2)
show "RETURN (it_to_list nodes_it s)
≤ ⇓ (⟨Rv⟩list_rel) (it_to_sorted_list (λ_ _. True) (nodes s'))"
by (simp add: it_to_sorted_list_def)
qed
lemma (in graph_succ_it) autoref_succ_it[autoref_rules]:
assumes ID: "PREFER_id Rv" "PREFER_id Rw"
shows "(λs v. RETURN (it_to_list (λs. succ_it s v) s),succ_to_list)
∈ ⟨Rv,Rw⟩rel → Rv → ⟨⟨⟨Rw,Rv⟩prod_rel⟩list_rel⟩nres_rel"
unfolding succ_to_list_def[abs_def]
proof (intro fun_relI nres_relI)
fix s s' v v'
from ID have [simp]: "Rv = Id" "Rw=Id" by simp_all
assume "(v,v')∈Rv" hence [simp]: "v'=v" by simp
assume "(s,s')∈⟨Rv,Rw⟩rel"
hence INV: "invar s" and [simp]: "Graph.succ s' = Graph.succ (α s)" unfolding rel_def
by (auto simp add: br_def graph_rel_def succ_def)
obtain l where
[simp]: "distinct l" "succ (α s) v = set l" "it_to_list (λs. succ_it s v) s = l"
unfolding it_to_list_def
by (metis succ_it_correct[OF INV, unfolded set_iterator_def set_iterator_genord_def]
foldli_snoc_id self_append_conv2)
show "RETURN (it_to_list (λs. succ_it s v) s)
≤ ⇓ (⟨⟨Rw,Rv⟩prod_rel⟩list_rel) (it_to_sorted_list (λ_ _. True) (succ s' v'))"
by (simp add: it_to_sorted_list_def)
qed
subsection ‹Refinement›
locale dijkstraC =
g: StdGraph g_ops +
mr: StdMap mr_ops +
qw: StdUprio qw_ops
for g_ops :: "('V,'W::weight,'G,'moreg) graph_ops_scheme"
and mr_ops :: "('V, (('V,'W) path × 'W), 'mr,'more_mr) map_ops_scheme"
and qw_ops :: "('V ,'W infty,'qw,'more_qw) uprio_ops_scheme"
begin
end
locale dijkstraC_fixg = dijkstraC g_ops mr_ops qw_ops +
Dijkstra ga v0
for g_ops :: "('V,'W::weight,'G,'moreg) graph_ops_scheme"
and mr_ops :: "('V, (('V,'W) path × 'W), 'mr,'more_mr) map_ops_scheme"
and qw_ops :: "('V ,'W infty,'qw,'more_qw) uprio_ops_scheme"
and ga::"('V,'W) graph" and "v0"::'V and g :: 'G+
assumes ga_trans: "(g,ga)∈br g.α g.invar"
begin
abbreviation "v_rel ≡ Id :: ('V×'V) set"
abbreviation "w_rel ≡ Id :: ('W×'W) set"
definition i_node :: interface where "i_node ≡ undefined"
definition i_weight :: interface where "i_weight ≡ undefined"
lemmas [autoref_rel_intf] = REL_INTFI[of v_rel i_node]
lemmas [autoref_rel_intf] = REL_INTFI[of w_rel i_weight]
lemma weight_plus_autoref[autoref_rules]:
"(0,0) ∈ w_rel"
"((+),(+)) ∈ w_rel → w_rel → w_rel"
"((+),(+)) ∈ ⟨w_rel⟩infty_rel → ⟨w_rel⟩infty_rel → ⟨w_rel⟩infty_rel"
"((<),(<)) ∈ ⟨w_rel⟩infty_rel → ⟨w_rel⟩infty_rel → bool_rel"
by simp_all
lemma [autoref_rules]: "(g,ga)∈⟨v_rel,w_rel⟩g.rel" using ga_trans
by (simp add: g.rel_def)
lemma [autoref_rules]: "(v0,v0)∈v_rel" by simp
term mpath_weight'
lemma [autoref_rules]:
"(mpath_weight',mpath_weight')
∈ ⟨⟨v_rel×⇩rw_rel×⇩rv_rel⟩list_rel×⇩rw_rel⟩option_rel → ⟨w_rel⟩infty_rel"
"(mpath', mpath')
∈ ⟨⟨v_rel×⇩rw_rel×⇩rv_rel⟩list_rel×⇩rw_rel⟩option_rel
→ ⟨⟨v_rel×⇩rw_rel×⇩rv_rel⟩list_rel⟩option_rel"
by auto
term mdinit
lemmas [autoref_tyrel] =
ty_REL[where R=v_rel]
ty_REL[where R=w_rel]
ty_REL[where R="⟨w_rel⟩infty_rel"]
ty_REL[where R="⟨v_rel,⟨w_rel⟩infty_rel⟩qw.rel"]
ty_REL[where R="⟨v_rel,⟨v_rel×⇩rw_rel×⇩rv_rel⟩list_rel×⇩rw_rel⟩mr.rel"]
ty_REL[where R="⟨v_rel×⇩rw_rel×⇩rv_rel⟩list_rel"]
lemmas [autoref_op_pat] = uprio_pats[where 'e = 'V and 'a = "'W infty"]
schematic_goal cdijkstra_refines_aux:
shows "(?c::?'c,
mdijkstra
) ∈ ?R"
apply (simp only: mdijkstra_def mdinit_def mpop_min_def[abs_def] mupdate_def)
using [[goals_limit = 1]]
apply (fold op_map_empty_def[where 'a="'V" and 'b = "('V×'W×'V) list × 'W"])
apply (fold op_uprio_empty_def[where 'a="'V" and 'b = "'W infty"])
using [[autoref_trace_failed_id]]
apply (autoref_monadic (plain,trace))
done
end
context dijkstraC
begin
concrete_definition cdijkstra for g ?v0.0
uses dijkstraC_fixg.cdijkstra_refines_aux
[of g_ops mr_ops qw_ops]
term cdijkstra
end
context dijkstraC_fixg
begin
term cdijkstra
term mdijkstra
lemma cdijkstra_refines:
"RETURN (cdijkstra g v0) ≤ ⇓(build_rel mr.α mr.invar) mdijkstra"
apply (rule cdijkstra.refine[THEN nres_relD, simplified])
apply unfold_locales
done
theorem cdijkstra_correct:
shows
"weighted_graph.is_shortest_path_map ga v0 (αr (mr.α (cdijkstra g v0)))"
(is ?G1)
and "mr.invar (cdijkstra g v0)" (is ?G2)
and "res_invarm (mr.α (cdijkstra g v0))" (is ?G3)
proof -
note cdijkstra_refines
also note mdijkstra_refines
finally have Z: "RETURN (cdijkstra g v0) ≤
⇓(build_rel (αr ∘ mr.α) (λm. mr.invar m ∧ res_invarm (mr.α m)))
dijkstra'"
apply (subst (asm) conc_fun_chain)
apply (simp only: br_chain)
done
also note dijkstra'_refines[simplified]
also note dijkstra_correct
finally show ?G1 ?G2 ?G3
by (auto elim: RETURN_ref_SPECD simp: refine_rel_defs)
qed
end
theorem (in dijkstraC) cdijkstra_correct:
assumes INV: "g.invar g"
assumes V0: "v0 ∈ nodes (g.α g)"
assumes nonneg_weights: "⋀v w v'. (v,w,v')∈edges (g.α g) ⟹ 0≤w"
shows
"weighted_graph.is_shortest_path_map (g.α g) v0
(Dijkstra.αr (mr.α (cdijkstra g v0)))" (is ?G1)
and "Dijkstra.res_invarm (mr.α (cdijkstra g v0))" (is ?G2)
proof -
interpret hlgv: valid_graph "g.α g" using g.valid INV .
interpret dc: dijkstraC_fixg g_ops mr_ops qw_ops "g.α g" v0
apply unfold_locales
apply (simp_all
add: hlg.finite INV V0 hlg_ops_def nonneg_weights refine_rel_defs)
done
from dc.cdijkstra_correct show ?G1 ?G2 by auto
qed
text ‹
Example instantiation with HashSet.based graph,
red-black-tree based result map, and finger-tree based priority queue.
›
setup Locale_Code.open_block
interpretation hrf: dijkstraC hlg_ops rm_ops aluprioi_ops
by unfold_locales
setup Locale_Code.close_block
definition "hrf_dijkstra ≡ hrf.cdijkstra"
lemmas hrf_dijkstra_correct = hrf.cdijkstra_correct[folded hrf_dijkstra_def]
export_code hrf_dijkstra checking SML
export_code hrf_dijkstra in OCaml
export_code hrf_dijkstra in Haskell
export_code hrf_dijkstra checking Scala
definition hrfn_dijkstra :: "(nat,nat) hlg ⇒ _"
where "hrfn_dijkstra ≡ hrf_dijkstra"
export_code hrfn_dijkstra checking SML
lemmas hrfn_dijkstra_correct =
hrf_dijkstra_correct[where ?'a = nat and ?'b = nat, folded hrfn_dijkstra_def]
end