theory Kruskal_Refine
imports Kruskal "../../Refine_Heuristics" UnionFind
begin
definition edges_less_eq :: "('a × 'w::{linorder, ordered_comm_monoid_add} × 'a) ⇒ ('a × 'w × 'a) ⇒ bool"
where "edges_less_eq a b ≡ fst(snd a) ≤ fst(snd b)"
context Kruskal_intermediate_time
begin
thm minWeightBasis3_refine
thm minWeightBasis3_aux_def
thm obtain_sorted_carrier_aux_def
term wsorted
definition (in -) "α = (λ(x,y). Upair x y)"
definition (in -) wsorted_wrt_w' where "wsorted_wrt_w' w == sorted_wrt (λx y. w (α x) ≤ w (α y))"
abbreviation "wsorted' ≡ wsorted_wrt_w' weight"
lemma wsorted_mapα[simp]: "wsorted' s ⟹ wsorted (map α s)"
by(auto simp: wsorted_wrt_w'_def sorted_wrt_map)
definition (in -) "obtain_sorted_carrier'_aux c w obst == SPECT (emb (λL. wsorted_wrt_w' w L ∧ distinct (map α L) ∧ α ` set L = c) obst)"
abbreviation "obtain_sorted_carrier' == obtain_sorted_carrier'_aux E weight (getEdges_time + sort_time)"
definition RR :: "(('a × 'a) × 'a uprod) set" where "RR ≡ {( (cx,cy) , a). Upair cx cy = a }"
lemma RR_alt: "RR = br α (λ_. True)"
unfolding RR_def br_def α_def by auto
lemma "obtain_sorted_carrier' ≤ ⇓(list_rel RR) obtain_sorted_carrier"
unfolding obtain_sorted_carrier'_aux_def obtain_sorted_carrier_aux_def
oops
lemma obtain_sorted_carrier'_refine:
"obtain_sorted_carrier' ≤ ⇓ (⟨RR⟩list_rel) obtain_sorted_carrier"
unfolding obtain_sorted_carrier'_aux_def obtain_sorted_carrier_aux_def
apply(rule SPECT_refine)
unfolding RR_alt
subgoal for s apply(rule exI[where x="map α s"])
by(auto simp: map_in_list_rel_conv in_br_conv vcg_simp_rules)
done
abbreviation "empty_forest ≡ {}"
definition kruskal0
where "kruskal0 ≡ do {
l ← obtain_sorted_carrier';
s ← SPECT [empty_forest ↦ enat (empty_forest_time+empty_uf_time)];
spanning_forest ← nfoldli l (λ_. True)
(λ(a,b) T. do {
ASSERT (Upair a b∉T ∧ forest T ∧ Upair a b∈E ∧ T ⊆ E);
i ← SPECT [¬ (a,b) ∈ connected T ↦ enat indep_test_time];
if i then
do {
ASSERT (Upair a b∉T);
SPECT [(insert (Upair a b) T) ↦ enat (insert_time+insert_uf_time)]
}
else
RETURNT T
}) s;
RETURNT spanning_forest
}"
lemma "(xi, x) ∈ RR ⟹ xi = (x1, x2) ⟹ x = Upair x1 x2"
unfolding RR_def by auto
declare RETURNT_refine [simp]
lemma ff: "(sa, sa) ∈ Id" by auto
lemma ffs: "A ≤ B ⟹ A ≤ ⇓ Id B" by auto
lemma kruskal0_refine: "kruskal0 ≤ ⇓Id minWeightBasis3"
unfolding kruskal0_def minWeightBasis3_aux_def
apply(refine_rcg obtain_sorted_carrier'_refine)
apply simp
apply simp
apply (rule ff)
apply simp
subgoal by(auto simp: RR_def augment_forest)
apply(rule ffs)
subgoal by(auto simp: RR_def augment_forest)
subgoal by(auto simp: RR_def augment_forest)
subgoal by(auto simp: RR_def augment_forest)
subgoal by(auto simp: RR_def augment_forest)
subgoal by(auto simp: RR_def augment_forest)
subgoal by(auto simp: RR_def augment_forest)
done
section "kruskal1 - using union find"
definition corresponding_union_find :: "'a per ⇒ 'a uprod set ⇒ bool"
where "corresponding_union_find uf T ≡ (∀a∈V. ∀b∈V.
per_compare uf a b ⟷ ((a,b)∈ connected T ))"
definition "uf_graph_invar uf_T ≡ case uf_T of (uf, T) ⇒
corresponding_union_find uf T ∧
Domain uf = V"
lemma uf_graph_invarE: "uf_graph_invar (uf, T) ⟹ corresponding_union_find uf T"
unfolding uf_graph_invar_def by simp
definition "uf_graph_rel ≡ br snd uf_graph_invar"
lemma uf_graph_relsndD: "((a,b),c) ∈ uf_graph_rel ⟹ b=c"
by(auto simp: uf_graph_rel_def in_br_conv)
lemma uf_graph_relD: "((a,b),c) ∈ uf_graph_rel ⟹ b=c ∧ uf_graph_invar (a,b)"
by(auto simp: uf_graph_rel_def in_br_conv)
definition "initState = do {
initial_union_find ← SPECT [per_init V ↦ enat empty_uf_time];
SPECT [(initial_union_find, empty_forest) ↦ enat empty_forest_time]
}"
definition "addEdge uf a b T = do {
uf ← SPECT [per_union uf a b ↦ enat insert_uf_time];
SPECT [(uf, insert (Upair a b) T)↦enat insert_time]
}"
definition kruskal1
where "kruskal1 ≡ do {
l ← obtain_sorted_carrier';
s ← initState;
(per, spanning_forest) ← nfoldli l (λ_. True)
(λ(a,b) (uf, T). do {
ASSERT (Domain uf = Domain (fst s));
ASSERT (a∈V ∧ b∈V ∧ a ∈ Domain uf ∧ b ∈ Domain uf ∧ a≠b ∧ T⊆E);
i ← SPECT [¬ per_compare uf a b ↦ enat indep_test_time];
if i then
do {
ASSERT (Upair a b∉T);
addEdge uf a b T
}
else
RETURNT (uf,T)
}) s;
RETURNT spanning_forest
}"
lemma corresponding_union_find_empty:
shows "corresponding_union_find (per_init V) empty_forest"
by(auto simp: corresponding_union_find_def connected_same per_init_def)
lemma empty_forest_refine1: "((per_init V, empty_forest), empty_forest)∈uf_graph_rel"
using corresponding_union_find_empty
unfolding uf_graph_rel_def uf_graph_invar_def
by (auto simp: in_br_conv per_init_def)
lemma uf_graph_invar_preserve: "uf_graph_invar (uf, T) ⟹ a∈V ⟹ b∈V ⟹ a≠b ⟹ T⊆E
⟹ uf_graph_invar (per_union uf a b, insert (Upair a b) T)"
by(auto simp add: uf_graph_invar_def corresponding_union_find_def insert_reachable per_union_def)
lemma initloop: "initState ≤ ⇓ uf_graph_rel (SPECT [{} ↦ enat (empty_forest_time+empty_uf_time)])"
unfolding initState_def conc_fun_RES
apply(rule T_specifies_I)
apply (vcg' ‹-› )
apply(rule Sup_upper) apply (auto split: if_splits)
using empty_forest_refine1 by auto
lemma ref: "⋀ xi x si sb x1 x2 x1a x2a x1b x2b.
(xi, x) ∈ Id ×⇩r Id ⟹
(si, sb) ∈ uf_graph_rel ⟹
x = (x1, x2) ⟹
si = (x1b, x2b) ⟹
xi = (x1a, x2a) ⟹
x1a ∈ V ∧ x2a ∈ V ∧ x1a ∈ Domain x1b ∧ x2a ∈ Domain x1b ∧ x1a ≠ x2a ∧ x2b ⊆ E ⟹
addEdge x1b x1a x2a x2b
≤ ⇓ uf_graph_rel (SPECT [insert (Upair x1 x2) sb ↦ enat (insert_time+insert_uf_time)]) "
unfolding addEdge_def conc_fun_RES
apply(rule T_specifies_I)
apply (vcg' ‹-› )
by (auto dest: uf_graph_relD E_inV Eproper uf_graph_invarE
simp: corresponding_union_find_def uf_graph_rel_def in_br_conv uf_graph_invar_preserve
split: if_splits)
theorem kruskal1_refine: "kruskal1 ≤ ⇓Id kruskal0"
unfolding kruskal1_def kruskal0_def Let_def
apply (refine_rcg initloop ref)
apply refine_dref_type
apply simp apply simp apply auto []
apply (auto dest: uf_graph_relD E_inV Eproper uf_graph_invarE
simp: corresponding_union_find_def uf_graph_rel_def in_br_conv uf_graph_invar_preserve)
by (auto simp: uf_graph_invar_def dest: E_inV)
section "kruskal2 - using lists"
abbreviation "lst_graph_P l S ≡ lst_graph_P' weight l S"
lemmas lst_graph_P_def = lst_graph_P'_def
lemma lst_graph_P_distinctD: "lst_graph_P l S ⟹ distinct l"
by(auto simp: lst_graph_P_def dest: distinct_mapI)
abbreviation "lst_graph_rel ≡ lst_graph_rel' weight"
lemmas lst_graph_rel_def = lst_graph_rel'_def
lemma lst_graph_rel_empty[simp]: "([], {}) ∈ lst_graph_rel"
by(simp add: lst_graph_rel_def lst_graph_P_def)
term set_rel
term list_set_rel
abbreviation "edge_rel ≡ br α' (λ(a,w,b). weight (Upair a b) = w)"
abbreviation "edge_rel' ≡ br α'' (λ(a,w,b). weight (Upair a b) = w)"
lemma lst_graph_rel_alt:
"lst_graph_rel = ⟨edge_rel⟩list_set_rel" (is "?L = ?R")
proof
show "?L ⊆ ?R"
unfolding lst_graph_rel_def list_set_rel_def lst_graph_P_def
apply rule apply safe subgoal for a b apply(intro relcompI[where b="map α' a"])
by(auto simp add: list_rel_def in_br_conv list_all2_map2 list_all2_same)
done
next
have D: "⋀x y. (x, y) ∈ ⟨br α' (λ(a, w, b). weight (Upair a b) = w)⟩list_rel
⟹ y = map α' x ∧ (∀(a, w, b)∈set x. weight (Upair a b) = w)"
unfolding list_rel_def apply safe
subgoal for x y
by(auto intro: nth_equalityI[where xs=y and ys="map (λ(a, uu, y). Upair a y) x"]
simp: list_rel_def list_all2_conv_all_nth in_br_conv)
subgoal for x y by(auto simp: list_all2_conv_all_nth in_br_conv in_set_conv_nth)
done
show "?R ⊆ ?L"
unfolding lst_graph_rel_def list_set_rel_def lst_graph_P_def
by (force dest!: D simp: in_br_conv)
qed
abbreviation (in -) getEdges'
:: "('a uprod ⇒ 'w::{linorder, ordered_comm_monoid_add}) ⇒ 'a uprod set ⇒ enat ⇒ ('a × 'w × 'a) list nrest"
where
"getEdges' w c get == SPECT (emb (λL. lst_graph_P' w L c) get)"
abbreviation "getEdges == getEdges' weight E getEdges_time"
abbreviation (in -) obtain_sorted_carrier''_aux
:: "('a uprod ⇒ 'w::{linorder, ordered_comm_monoid_add}) ⇒ 'a uprod set ⇒ enat ⇒ enat ⇒ ('a × 'w × 'a) list nrest" where
"obtain_sorted_carrier''_aux w c get st ≡ do {
(l::('a × 'w × 'a) list) ← getEdges' w c get;
( ((ASSERT (length l = card c))) ⪢
SPECT (emb (λL. sorted_wrt edges_less_eq L ∧ distinct L ∧ set L = set l) st))
}"
abbreviation "obtain_sorted_carrier'' ≡ obtain_sorted_carrier''_aux weight E getEdges_time sort_time "
term "⟨edge_rel⟩list_rel"
lemma "distinct x ⟹ length x = length y ⟹ set x = set y ⟹ distinct y"
using card_distinct distinct_card by fastforce
lemma wsorted'_sorted_wrt_edges_less_eq: "∀x∈set s. case x of (a, wv, b) ⇒ weight (Upair a b) = wv ⟹ sorted_wrt edges_less_eq s
⟹ wsorted' (map α'' s) "
unfolding wsorted_wrt_w'_def sorted_wrt_map edges_less_eq_def
apply(rule sorted_wrt_mono_rel )
by (auto simp add: α_def case_prod_beta)
lemma " distinct s ⟹
set s = set l ⟹
distinct (map f l) ⟹ distinct (map f s)"
by (simp add: distinct_map)
lemma α'_conv: "(((λ(x, y). Upair x y) ∘∘ case_prod) (λa (_, y). (a, y)))
= α'" by auto
lemma "SPECT (emb P1 t1) ⤜ (λl. SPECT (emb (P2 l) t2))
= SPECT (emb P (t1+t2)) " unfolding bindT_def
apply auto unfolding emb'_def apply auto
oops
lemma emb_eq_Some_conv': "⋀T. Some t' = emb' Q T x ⟷ (t'=T x ∧ Q x)"
by (auto simp: emb'_def)
lemma obtain_sorted_carrier''_refine: "obtain_sorted_carrier'' ≤ ⇓ (⟨edge_rel'⟩list_rel) obtain_sorted_carrier'"
unfolding obtain_sorted_carrier'_aux_def
unfolding conc_fun_RES
apply(rule T_specifies_I)
apply(vcg' ‹-› )
apply(rule Sup_upper) apply (auto split: if_splits)
subgoal for l s
apply(rule exI[where x="map α'' s"])
apply (simp add: emb_eq_Some_conv')
apply(auto simp: in_br_conv lst_graph_P_def wsorted'_sorted_wrt_edges_less_eq
α_def α'_conv distinct_map map_in_list_rel_conv)
using image_iff
by fastforce+
subgoal unfolding lst_graph_P_def
using distinct_card by fastforce
done
definition (in -) "initState'_aux c eft eut = do {
initial_union_find ← SPECT [per_init (Kruskal_intermediate_defs.V c) ↦ enat eut];
SPECT [(initial_union_find, []) ↦ enat eft]
}"
abbreviation "initState' == initState'_aux E empty_forest_time empty_uf_time"
definition (in -) "addEdge'_aux uf a w b T iut it = do {
uf ← SPECT [per_union uf a b ↦ enat iut];
T' ← SPECT [ T@[ ( a,w, b) ] ↦enat it];
RETURNT (uf, T')
}"
abbreviation "addEdge' uf a w b T == addEdge'_aux uf a w b T insert_uf_time insert_time"
definition (in -) kruskal2_aux
where "kruskal2_aux w c get st eft eut itt iut it ≡ do {
sl ← obtain_sorted_carrier''_aux w c get st;
s ← initState'_aux c eft eut;
(per, spanning_forest) ← nfoldli sl (λ_. True)
(λ(a,w,b) (uf, T). do {
ASSERT (a ∈ Domain uf ∧ b ∈ Domain uf);
i ← SPECT [¬ per_compare uf a b ↦ itt];
if i then
do {
ASSERT ((a,w,b)∉set T);
addEdge'_aux uf a w b T iut it
}
else
RETURNT (uf,T)
}) s;
RETURNT spanning_forest
}"
abbreviation "kruskal2 == kruskal2_aux weight E getEdges_time sort_time
empty_forest_time empty_uf_time indep_test_time insert_uf_time insert_time "
lemma loop_initial_rel: "((per_init V, []), per_init V, {}) ∈ Id ×⇩r lst_graph_rel"
by simp
lemma loop_initial_refine: "initState'
≤ ⇓ (Id ×⇩r lst_graph_rel) initState"
unfolding initState'_aux_def initState_def
apply(refine_rcg SPECT_refine)
by (auto split: if_splits)
lemma wI: "(λ(a, _, y). Upair a y) ` D = A ⟹ Upair b c ∉ A ⟹ (b, w, c) ∉ D"
by (metis case_prod_conv pair_imageI)
lemma listall2D: " list_all2 P xs y ⟹ (⋀x x'. P x x' ⟶ x' = a x) ⟹ y = map a xs"
by (smt list.rel_eq list.rel_map(1) list_all2_mono)
lemma list_relD: "(x, y) ∈ ⟨br a I⟩list_rel ⟹ y = map a x"
by(auto dest!: listall2D simp: list_rel_def in_br_conv)
lemma list_set_rel_append: "(x,s)∈br a I ⟹ (xs,S)∈⟨br a I⟩list_set_rel ⟹ s∉S
⟹ (xs@[x],insert s S)∈⟨br a I⟩list_set_rel"
unfolding list_set_rel_def
apply(intro relcompI[where b="map a (xs @ [x])"])
apply (auto simp: in_br_conv)
apply parametricity by (auto dest: list_relD simp add: in_br_conv)
theorem kruskal2_refine: "kruskal2 ≤ ⇓lst_graph_rel kruskal1 "
unfolding kruskal1_def kruskal2_aux_def Let_def
apply (refine_rcg obtain_sorted_carrier''_refine loop_initial_refine)
apply simp apply simp
subgoal by (auto simp: in_br_conv)
subgoal by (auto simp: in_br_conv)
apply(rule ffs) subgoal by (auto simp: in_br_conv)
subgoal by (auto simp: in_br_conv )
subgoal unfolding in_br_conv lst_graph_rel_def lst_graph_P_def list_set_rel_def
by (simp add: wI)
subgoal unfolding addEdge'_aux_def addEdge_def
apply refine_rcg
apply refine_dref_type
apply(rule SPECT_refine)
apply (auto split: if_splits simp: in_br_conv lst_graph_rel_alt intro: list_set_rel_append)
unfolding conc_fun_RES
apply(rule T_specifies_I)
apply (vcg' ‹-› )
apply(rule Sup_upper) apply (auto split: if_splits)
by (auto split: if_splits simp: in_br_conv lst_graph_rel_alt intro: list_set_rel_append)
subgoal by (auto simp: in_br_conv )
subgoal by (auto simp: in_br_conv )
done
lemma "single_valued lst_graph_rel"
unfolding lst_graph_rel_alt list_set_rel_def
by(auto intro!: single_valued_relcomp list_rel_sv)
end
end