Theory Leadsto_Map
subsection ‹Implementation on Maps›
theory Leadsto_Map
imports Leadsto Unified_PW_Hashing Liveness_Subsumption_Map Heap_Hash_Map Next_Key
begin
definition map_to_set :: "('b ⇀ 'a set) ⇒ 'a set" where
"map_to_set m = (⋃ (ran m))"
hide_const wait
definition
"map_list_set_rel =
{(ml, ms). dom ml = dom ms
∧ (∀ k ∈ dom ms. set (the (ml k)) = the (ms k) ∧ distinct (the (ml k)))
∧ finite (dom ml)
}"
context Worklist_Map2_Defs
begin
definition
"add_pw'_map3 passed wait a ≡
nfoldli (succs a) (λ(_, _, brk). ¬brk)
(λa (passed, wait, _).
do {
RETURN (
if empty a then
(passed, wait, False)
else if F' a then (passed, wait, True)
else
let k = key a; passed' = (case passed k of Some passed' ⇒ passed' | None ⇒ [])
in
if ∃ x ∈ set passed'. a ⊴ x then
(passed, wait, False)
else
(passed(k ↦ (a # passed')), a # wait, False)
)
}
)
(passed,wait,False)"
definition
"pw_map_inv3 ≡ λ (passed, wait, brk).
∃ passed'. (passed, passed') ∈ map_list_set_rel ∧ pw_map_inv (passed', wait, brk)
"
definition pw_algo_map3 where
"pw_algo_map3 = do
{
if F a⇩0 then RETURN (True, Map.empty)
else if empty a⇩0 then RETURN (False, Map.empty)
else do {
(passed, wait) ← RETURN ([key a⇩0 ↦ [a⇩0]], [a⇩0]);
(passed, wait, brk) ← WHILEIT pw_map_inv3 (λ (passed, wait, brk). ¬ brk ∧ wait ≠ [])
(λ (passed, wait, brk). do
{
(a, wait) ← take_from_list wait;
ASSERT (reachable a);
if empty a then RETURN (passed, wait, brk) else add_pw'_map3 passed wait a
}
)
(passed, wait, False);
RETURN (brk, passed)
}
}
"
end
lemma map_list_set_rel_empty[refine, simp, intro]:
"(Map.empty, Map.empty) ∈ map_list_set_rel"
unfolding map_list_set_rel_def by auto
lemma map_list_set_rel_single:
"(ml(key a⇩0 ↦ [a⇩0]), ms(key a⇩0 ↦ {a⇩0})) ∈ map_list_set_rel" if "(ml, ms) ∈ map_list_set_rel"
using that unfolding map_list_set_rel_def by auto
context Worklist_Map2
begin
lemma refine_start[refine]:
"(([key a⇩0 ↦ [a⇩0]], [a⇩0]), [key a⇩0 ↦ {a⇩0}], [a⇩0]) ∈ map_list_set_rel ×⇩r Id"
by (simp add: map_list_set_rel_single)
lemma pw_map_inv_ref:
"pw_map_inv (x1, x2, x3) ⟹ (x1a, x1) ∈ map_list_set_rel ⟹ pw_map_inv3 (x1a, x2, x3)"
unfolding pw_map_inv3_def by auto
lemma refine_aux[refine]:
"(x1, x) ∈ map_list_set_rel ⟹ ((x1, x2, False), x, x2, False) ∈ map_list_set_rel ×⇩r Id ×⇩r Id"
by simp
lemma map_list_set_relD:
"ms k = Some (set xs)" if "(ml, ms) ∈ map_list_set_rel" "ml k = Some xs"
using that unfolding map_list_set_rel_def
by clarsimp (metis (mono_tags, lifting) domD domI option.sel)
lemma map_list_set_rel_distinct:
"distinct xs" if "(ml, ms) ∈ map_list_set_rel" "ml k = Some xs"
using that unfolding map_list_set_rel_def by clarsimp (metis domI option.sel)
lemma map_list_set_rel_NoneD1[dest, intro]:
"ms k = None" if "(ml, ms) ∈ map_list_set_rel" "ml k = None"
using that unfolding map_list_set_rel_def by auto
lemma map_list_set_rel_NoneD2[dest, intro]:
"ml k = None" if "(ml, ms) ∈ map_list_set_rel" "ms k = None"
using that unfolding map_list_set_rel_def by auto
lemma map_list_set_rel_insert:
"(ml, ms) ∈ map_list_set_rel ⟹
ml (key a) = Some xs ⟹
ms (key a) = Some (set xs) ⟹
a ∉ set xs ⟹
(ml(key a ↦ a # xs), ms(key a ↦ insert a (set xs))) ∈ map_list_set_rel"
apply (frule map_list_set_rel_distinct) unfolding map_list_set_rel_def by auto
lemma add_pw'_map3_ref:
"add_pw'_map3 ml xs a ≤ ⇓ (map_list_set_rel ×⇩r Id) (add_pw'_map2 ms xs a)"
if "(ml, ms) ∈ map_list_set_rel" "¬ empty a"
using that unfolding add_pw'_map3_def add_pw'_map2_def
apply refine_rcg
apply refine_dref_type
apply (simp; fail)
apply (simp; fail)
apply (simp; fail)
apply (clarsimp simp: Let_def)
apply safe
subgoal
by (auto dest: map_list_set_relD[OF _ sym])
subgoal
by (simp split: option.split_asm)
(metis (mono_tags, lifting)
map_list_set_relD map_list_set_rel_NoneD1 option.collapse option.sel option.simps(3)
)
subgoal premises prems for a ms x2a ml x2c
proof (cases "ml (key a)")
case None
with ‹(ml, ms) ∈ map_list_set_rel› have "ms (key a) = None"
by auto
with None ‹(ml, ms) ∈ map_list_set_rel› show ?thesis
by (auto intro: map_list_set_rel_single)
next
case (Some xs)
from map_list_set_relD[OF ‹(ml, ms) ∈ map_list_set_rel› ‹ml _ = _›] have
"ms (key a) = Some (set xs)"
by auto
moreover from prems have "a ∉ set xs"
by (metis Some empty_subsumes' local.eq_refl)
ultimately show ?thesis
using Some ‹(ml, ms) ∈ map_list_set_rel› by (auto intro: map_list_set_rel_insert)
qed
done
lemma pw_algo_map3_ref[refine]:
"pw_algo_map3 ≤ ⇓ (Id ×⇩r map_list_set_rel) pw_algo_map2"
unfolding pw_algo_map3_def pw_algo_map2_def
apply refine_rcg
apply refine_dref_type
apply (simp; fail)+
apply (clarsimp, rule refine_aux; assumption)
by (auto intro: add_pw'_map3_ref pw_map_inv_ref)
lemma pw_algo_map2_ref':
"pw_algo_map2 ≤ ⇓ (bool_rel ×⇩r map_set_rel) pw_algo"
proof -
note pw_algo_map2_ref
also note pw_algo_map_ref
also note pw_algo_unified_ref
finally show ?thesis .
qed
lemma pw_algo_map3_ref'[refine]:
"pw_algo_map3 ≤ ⇓ (bool_rel ×⇩r (map_list_set_rel O map_set_rel)) pw_algo"
proof -
have [simp]:
"((bool_rel ×⇩r map_list_set_rel) O (bool_rel ×⇩r map_set_rel))
= (bool_rel ×⇩r (map_list_set_rel O map_set_rel))"
unfolding relcomp_def prod_rel_def by auto
note pw_algo_map3_ref
also note pw_algo_map2_ref'
finally show ?thesis
by (simp add: conc_fun_chain)
qed
end
lemma (in Worklist_Map2_finite) map_set_rel_finite_domI[intro]:
"finite (dom m)" if "(m, S) ∈ map_set_rel"
using that unfolding map_set_rel_def by auto
lemma (in Worklist_Map2_finite) map_set_rel_finiteI:
"finite S" if "(m, S) ∈ map_set_rel"
using that unfolding map_set_rel_def
apply clarsimp
apply (rule finite_Union)
apply (solves ‹auto intro: map_dom_ran_finite›)+
apply (solves ‹auto simp: ran_def›)
done
lemma (in Worklist_Map2_finite) map_set_rel_finite_ranI[intro]:
"finite S'" if "(m, S) ∈ map_set_rel" "S' ∈ ran m"
using that unfolding map_set_rel_def ran_def by auto
locale Leadsto_Search_Space_Key =
A: Worklist_Map2 _ _ _ _ _ _ _ succs1 +
Leadsto_Search_Space for succs1
begin
sublocale A': Worklist_Map2_finite a⇩0 "λ _. False" "(≼)" empty "(⊴)" E key succs1 "λ _. False"
by (standard; blast intro!: A.succs_correct)
interpretation B:
Liveness_Search_Space_Key
"λ x y. E x y ∧ Q y ∧ ¬ empty y" a⇩0 "λ _. False" "(≼)" "λ x. A.reachable x ∧ ¬ empty x"
succs_Q key
by standard (auto intro!: A.empty_subsumes')
context
fixes a⇩1 :: 'a
begin
interpretation B':
Liveness_Search_Space_Key_Defs
a⇩1 "λ _. False" "(≼)" "λ x. A.reachable x ∧ ¬ empty x"
succs_Q "λ x y. E x y ∧ Q y ∧ ¬ empty y" key .
definition has_cycle_map where
"has_cycle_map = B'.dfs_map"
context
assumes "A.reachable a⇩1"
begin
interpretation B':
Liveness_Search_Space_Key
"λ x y. E x y ∧ Q y ∧ ¬ empty y" a⇩1 "λ _. False" "(≼)" "λ x. A.reachable x ∧ ¬ empty x"
succs_Q key
by standard
lemmas has_cycle_map_ref[refine] = B'.dfs_map_dfs_refine[folded has_cycle_map_def has_cycle_def]
end
end
definition outer_inv where
"outer_inv passed done todo ≡ λ (r, passed').
(r ⟶ (∃ a. A.reachable a ∧ ¬ empty a ∧ P a ∧ Q a ∧ reaches_cycle a))
∧ (¬ r ⟶
(∀ a ∈ ⋃ done. P a ∧ Q a ⟶ ¬ reaches_cycle a)
∧ B.liveness_compatible passed'
∧ passed' ⊆ {x. A.reachable x ∧ ¬ empty x}
)
"
definition inner_inv where
"inner_inv passed done todo ≡ λ (r, passed').
(r ⟶ (∃ a. A.reachable a ∧ ¬ empty a ∧ P a ∧ Q a ∧ reaches_cycle a))
∧ (¬ r ⟶
(∀ a ∈ done. P a ∧ Q a ⟶ ¬ reaches_cycle a)
∧ B.liveness_compatible passed'
∧ passed' ⊆ {x. A.reachable x ∧ ¬ empty x}
)
"
definition leadsto' :: "bool nres" where
"leadsto' = do {
(r, passed) ← A'.pw_algo_map2;
let passed = ran passed;
(r, _) ← FOREACHcdi (outer_inv passed) passed (λ(b,_). ¬b)
(λ passed' (_,acc).
FOREACHcdi (inner_inv acc) passed' (λ(b,_). ¬b)
(λv' (_,passed).
do {
ASSERT(A.reachable v' ∧ ¬ empty v');
if P v' ∧ Q v' then has_cycle v' passed else RETURN (False, passed)
}
)
(False, acc)
)
(False, {});
RETURN r
}"
lemma leadsto'_correct:
"leadsto' ≤ leadsto_spec"
proof -
define inv where
"inv ≡ λ passed it (r, passed').
(r ⟶ (∃ a. A.reachable a ∧ ¬ empty a ∧ P a ∧ Q a ∧ reaches_cycle a))
∧ (¬ r ⟶
(∀ a ∈ passed - it. ¬ reaches_cycle a)
∧ B.liveness_compatible passed'
∧ passed' ⊆ {x. A.reachable x ∧ ¬ empty x}
)
"
have [simp, intro]:
"¬ A'.F_reachable"
unfolding A'.F_reachable_def by simp
have B_reaches_empty:
"¬ empty b" if "¬ empty a" "B.reaches a b" for a b
using that(2,1)by induction auto
interpret Subgraph_Start E a⇩0 "λ a x. E a x ∧ Q x ∧ ¬ empty x"
by standard auto
have B_A_reaches:
"A.reaches a b" if "B.reaches a b" for a b
using that by (rule reaches)
have reaches_iff: "B.reaches a x ⟷ B.G.G'.reaches a x"
if "A.reachable a" "¬ empty a" for a x
unfolding reaches_cycle_def
apply standard
using that
apply (rotate_tac 3)
apply (induction rule: rtranclp.induct)
apply blast
apply (rule rtranclp.rtrancl_into_rtrancl)
apply assumption
apply (subst B.G.E'_def)
subgoal for a b c
by (auto dest: B_reaches_empty)
subgoal
by (rule B.G.reaches)
done
have reaches1_iff: "B.reaches1 a x ⟷ B.G.G'.reaches1 a x"
if "A.reachable a" "¬ empty a" for a x
unfolding reaches_cycle_def
apply standard
subgoal
using that
apply (rotate_tac 3)
apply (induction rule: tranclp.induct)
apply (solves ‹rule tranclp.intros(1), auto simp: B.G.E'_def›)
apply (
rule tranclp.intros(2);
auto 4 3 simp: B.G.E'_def dest:B_reaches_empty tranclp_into_rtranclp
)
done
subgoal
by (rule B.G.reaches1)
done
have reaches_cycle_iff: "reaches_cycle a ⟷ (∃x. B.G.G'.reaches a x ∧ B.G.G'.reaches1 x x)"
if "A.reachable a" "¬ empty a" for a
unfolding reaches_cycle_def
apply (subst reaches_iff[OF that])
using reaches1_iff B.G.G'_reaches_V that by blast
have aux1:
"¬ reaches_cycle x"
if
"∀a. A.reachable a ∧ ¬ empty a ⟶ (∃x∈passed. a ≼ x)"
"passed ⊆ {a. A.reachable a ∧ ¬ empty a}"
"∀ y ∈ ran passed'. ∀ x ∈ y. P x ∧ Q x ⟶ ¬ reaches_cycle x"
"A.reachable x" "¬ empty x" "P x" "Q x"
"(passed', passed) ∈ A'.map_set_rel"
for x passed passed'
proof (rule ccontr, unfold not_not)
assume "reaches_cycle x"
from that obtain x' where x':"x' ∈ passed" "x ≼ x'"
by auto
with ‹(_, _) ∈ _› obtain y where y: "y ∈ ran passed'" "x' ∈ y"
unfolding A'.map_set_rel_def by auto
from x' that have "P x'" "Q x'"
by (auto intro: P_mono Q_mono)
with ‹x' ∈ passed› that(3) y have "¬ reaches_cycle x'"
by auto
have "A.reachable x'" "¬ empty x'"
using ‹x' ∈ passed› that(2) A.empty_mono ‹x ≼ x'› that(5) by auto
note reaches_cycle_iff' = reaches_cycle_iff[OF this] reaches_iff[OF this] reaches1_iff[OF this]
from ‹reaches_cycle x› obtain y where "B.reaches x y" "B.reaches1 y y"
unfolding reaches_cycle_def by atomize_elim
interpret
Subsumption_Graph_Pre_Nodes
"(≼)" A.subsumes_strictly "λ x y. E x y ∧ Q y ∧ ¬ empty y"
"λ x. A.reachable x ∧ ¬ empty x"
by standard (rule B.mono[simplified]; assumption)
from ‹B.reaches x y› ‹x ≼ x'› ‹B.reaches1 y y› reaches_cycle_mono[OF B.finite_V] obtain y' where
"y ≼ y'" "B.G.G'.reaches x' y'" "B.G.G'.reaches1 y' y'"
apply atomize_elim
apply (subst (asm) reaches_iff[rotated 2])
defer
defer
apply (subst (asm) reaches1_iff)
defer
defer
using ‹A.reachable x› ‹¬ empty x› ‹A.reachable x'› ‹¬ empty x'› ‹B.reaches1 y y›
by (auto simp: B.reaches1_reaches_iff2 dest!: B.G.G'_reaches_V)
with ‹A.reachable x'› ‹¬ empty x'› have "reaches_cycle x'"
unfolding reaches_cycle_iff'
by auto
with ‹¬ reaches_cycle x'› show False ..
qed
note [refine_vcg] = A'.pw_algo_map2_correct[THEN order.trans]
show ?thesis
unfolding leadsto'_def leadsto_spec_def
apply (refine_rcg refine_vcg)
subgoal
by (auto intro: map_dom_ran_finite)
subgoal
unfolding outer_inv_def B.liveness_compatible_def by simp
subgoal
by auto
subgoal for x a b S1 S2 todo σ aa passed
unfolding inner_inv_def outer_inv_def by simp
subgoal
unfolding inner_inv_def outer_inv_def A'.map_set_rel_def by auto
subgoal
unfolding inner_inv_def outer_inv_def A'.map_set_rel_def by auto
subgoal for _ _ b S1 S2 xa σ aa passed S1' S2' a⇩1 σ' ab passed'
unfolding outer_inv_def
apply clarsimp
subgoal premises prems for p
proof -
from prems have "a⇩1 ∈ p"
unfolding A'.map_set_rel_def by auto
with ‹passed ⊆ _› ‹p ⊆ _› have "A.reachable a⇩1"
by auto
interpret B':
Liveness_Search_Space
"λ x y. E x y ∧ Q y ∧ ¬ empty y" a⇩1 "λ _. False" "(≼)"
"λ x. A.reachable x ∧ ¬ empty x" succs_Q
by standard
from ‹inner_inv _ _ _ _› have
"B'.liveness_compatible passed'" "passed' ⊆ {x. A.reachable x ∧ ¬ empty x}"
unfolding inner_inv_def by auto
from B'.dfs_correct[OF _ this] ‹passed ⊆ _› ‹a⇩1 ∈ _› ‹p ⊆ _› have
"B'.dfs passed' ≤ B'.dfs_spec"
by auto
then show ?thesis
unfolding has_cycle_def
apply (rule order.trans)
unfolding B'.dfs_spec_def
apply clarsimp
subgoal for r passed1
apply (cases r)
apply simp
subgoal
unfolding inner_inv_def
using ‹passed ⊆ _› ‹a⇩1 ∈ _› ‹p ⊆ _›
apply simp
apply (inst_existentials a⇩1)
by (auto 4 3 simp: reaches_cycle_iff intro: prems)
subgoal
using ‹inner_inv _ _ _ _› ‹passed ⊆ _› ‹a⇩1 ∈ _› ‹p ⊆ _› reaches_cycle_iff
unfolding inner_inv_def by auto
done
done
qed
done
subgoal for x a b S1 S2 xa σ aa ba S1a S2a xb σ' ab bb
unfolding inner_inv_def by auto
subgoal for x a b S1 S2 xa σ aa ba S1a S2a σ'
unfolding inner_inv_def outer_inv_def by auto
subgoal for x a b S1 S2 xa σ aa ba σ'
unfolding inner_inv_def outer_inv_def by auto
subgoal for x a b S1 S2 σ aa ba
unfolding outer_inv_def by auto
subgoal for x a b σ aa ba
unfolding outer_inv_def by (auto dest!: aux1)
done
qed
lemma init_ref[refine]:
"((False, Map.empty), False, {}) ∈ bool_rel ×⇩r A'.map_set_rel"
unfolding A'.map_set_rel_def by auto
lemma has_cycle_map_ref'[refine]:
assumes "(P1, P1') ∈ A'.map_set_rel" "(a, a') ∈ Id" "A.reachable a" "¬ empty a"
shows "has_cycle_map a P1 ≤ ⇓ (bool_rel ×⇩r A'.map_set_rel) (has_cycle a' P1')"
using has_cycle_map_ref assms by auto
definition leadsto_map3' :: "bool nres" where
"leadsto_map3' = do {
(r, passed) ← A'.pw_algo_map2;
let passed = ran passed;
(r, _) ← FOREACHcd passed (λ(b,_). ¬b)
(λ passed' (_,acc).
do {
passed' ← SPEC (λl. set l = passed');
nfoldli passed' (λ(b,_). ¬b)
(λv' (_,passed).
if P v' ∧ Q v' then has_cycle_map v' passed else RETURN (False, passed)
)
(False, acc)
}
)
(False, Map.empty);
RETURN r
}"
definition "pw_algo_map2_copy = A'.pw_algo_map2"
lemma [refine]:
"A'.pw_algo_map2 ≤
⇓ (br id (λ (_, m). finite (dom m) ∧ (∀ k S. m k = Some S ⟶ finite S))) pw_algo_map2_copy"
proof -
have [refine]:
"(x, x') ∈ Id ⟹
x' = (x1, x2) ⟹
x = (x1a, x2a) ⟹
A'.pw_map_inv (x1, x2, False)
⟹ ((x1a, x2a, False), x1, x2, False) ∈
(br id (λ m. finite (dom m) ∧ (∀ k S. m k = Some S ⟶ finite S))) ×⇩r Id ×⇩r Id"
for x x' x1 x2 x1a x2a
by (auto simp: br_def A'.pw_map_inv_def A'.map_set_rel_def)
show ?thesis
unfolding pw_algo_map2_copy_def
unfolding A'.pw_algo_map2_def
apply refine_rcg
apply refine_dref_type
prefer 5
apply assumption
apply (assumption | solves ‹simp add: br_def› | solves ‹auto simp: br_def›)+
subgoal
apply (clarsimp simp: br_def)
subgoal premises prems
using ‹finite _› ‹∀k S. _ ⟶ finite _›
unfolding A'.add_pw'_map2_def
apply refine_rcg
apply refine_dref_type
apply (auto simp: Let_def split!: option.split)
done
done
by (simp add: br_def)
qed
lemma leadsto_map3'_ref[refine]:
"leadsto_map3' ≤ ⇓ Id leadsto'"
unfolding leadsto_map3'_def leadsto'_def
apply (subst (2) pw_algo_map2_copy_def[symmetric])
apply (subst (2) FOREACHcdi_def)
apply (subst (2) FOREACHcd_def)
apply refine_rcg
apply refine_dref_type
by (auto simp: br_def intro: map_dom_ran_finite)
definition leadsto_map3 :: "bool nres" where
"leadsto_map3 = do {
(r, passed) ← A'.pw_algo_map3;
let passed = ran passed;
(r, _) ← FOREACHcd passed (λ(b,_). ¬b)
(λ passed' (_,acc).
nfoldli passed' (λ(b,_). ¬b)
(λv' (_,passed).
if P v' ∧ Q v' then has_cycle_map v' passed else RETURN (False, passed)
)
(False, acc)
)
(False, Map.empty);
RETURN r
}"
lemma start_ref:
"((False, Map.empty), False, Map.empty) ∈ Id ×⇩r map_list_set_rel"
by simp
lemma map_list_set_rel_ran_set_rel:
"(ran ml, ran ms) ∈ ⟨br set (λ_. True)⟩set_rel" if "(ml, ms) ∈ map_list_set_rel"
using that unfolding map_list_set_rel_def set_rel_def
apply safe
subgoal for x
by (auto simp: ran_def dom_def in_br_conv dest: A.map_list_set_relD[OF that])
subgoal premises prems for x'
proof -
from prems(4) obtain a where "ms a = Some x'"
unfolding ran_def by clarsimp
with prems(1) obtain m' where
"ml a = Some (m' a)"
by (fastforce simp: dom_def ran_def)
with prems(2) ‹ms a = _› show ?thesis
by (fastforce simp: in_br_conv dom_def ran_def)
qed
done
lemma Id_list_rel_ref:
"(x'a, x'a) ∈ ⟨Id⟩list_rel"
by simp
lemma map_list_set_rel_finite_ran:
"finite (ran ml)" if "(ml, ms) ∈ map_list_set_rel"
using that unfolding map_list_set_rel_def by (auto intro: map_dom_ran_finite)
lemma leadsto_map3_ref[refine]:
"leadsto_map3 ≤ ⇓ Id leadsto'"
unfolding leadsto_map3_def leadsto'_def
apply (subst (2) FOREACHcdi_def)
apply (subst (2) FOREACHcd_def)
apply (refine_rcg map_list_set_rel_ran_set_rel map_list_set_rel_finite_ran)
prefer 4
apply (rule rhs_step_bind_SPEC)
apply (clarsimp simp: br_def; rule HOL.refl; fail)
apply (refine_rcg Id_list_rel_ref; simp; fail)
by auto
definition leadsto_map4 :: "bool nres" where
"leadsto_map4 = do {
(r, passed) ← A'.pw_algo_map3;
ASSERT (finite (dom passed));
passed ← ran_of_map passed;
(r, _) ← nfoldli passed (λ(b,_). ¬b)
(λ passed' (_,acc).
nfoldli passed' (λ(b,_). ¬b)
(λv' (_,passed).
if P v' ∧ Q v' then has_cycle_map v' passed else RETURN (False, passed)
)
(False, acc)
)
(False, Map.empty);
RETURN r
}"
lemma ran_of_map_ref:
"ran_of_map m ≤ SPEC (λc. (c, ran m') ∈ br set (λ _. True))" if "finite (dom m)" "(m, m') ∈ Id"
using ran_of_map_correct[OF that(1)] that(2) unfolding br_def by (simp add: pw_le_iff)
lemma aux_ref:
"(xa, x'a) ∈ Id ⟹
x'a = (x1b, x2b) ⟹ xa = (x1c, x2c) ⟹ (x1c, x1b) ∈ bool_rel"
by simp
definition "foo = A'.pw_algo_map3"
lemma [refine]:
"A'.pw_algo_map3 ≤ ⇓ (br id (λ (_, m). finite (dom m))) foo"
proof -
have [refine]:
"(x, x') ∈ Id ⟹
x' = (x1, x2) ⟹
x = (x1a, x2a) ⟹
A'.pw_map_inv3 (x1, x2, False)
⟹ ((x1a, x2a, False), x1, x2, False) ∈ (br id (λ m. finite (dom m))) ×⇩r Id ×⇩r Id"
for x x' x1 x2 x1a x2a
by (auto simp: br_def A'.pw_map_inv3_def map_list_set_rel_def)
show ?thesis
unfolding foo_def
unfolding A'.pw_algo_map3_def
apply refine_rcg
apply refine_dref_type
prefer 5
apply assumption
apply (assumption | solves ‹simp add: br_def› | solves ‹auto simp: br_def›)+
subgoal
apply (clarsimp simp: br_def)
subgoal premises prems
using ‹finite _›
unfolding A'.add_pw'_map3_def
apply refine_rcg
apply refine_dref_type
apply (auto simp: Let_def)
done
done
by (simp add: br_def)
qed
lemma leadsto_map4_ref[refine]:
"leadsto_map4 ≤ ⇓ Id leadsto_map3"
unfolding leadsto_map4_def leadsto_map3_def FOREACHcd_def
apply (subst (2) foo_def[symmetric])
apply (refine_rcg ran_of_map_ref)
apply refine_dref_type
apply (simp add: br_def; fail)
apply (simp add: br_def; fail)
apply (rule rhs_step_bind_SPEC)
by (auto simp: br_def)
definition leadsto_map4' :: "bool nres" where
"leadsto_map4' = do {
(r, passed) ← A'.pw_algo_map2;
ASSERT (finite (dom passed));
passed ← ran_of_map passed;
(r, _) ← nfoldli passed (λ(b,_). ¬b)
(λ passed' (_,acc).
do {
passed' ← SPEC (λl. set l = passed');
nfoldli passed' (λ(b,_). ¬b)
(λv' (_,passed).
if P v' ∧ Q v' then has_cycle_map v' passed else RETURN (False, passed)
)
(False, acc)
}
)
(False, Map.empty);
RETURN r
}"
lemma leadsto_map4'_ref:
"leadsto_map4' ≤ ⇓ Id leadsto_map3'"
unfolding leadsto_map4'_def leadsto_map3'_def FOREACHcd_def
apply (subst (2) pw_algo_map2_copy_def[symmetric])
apply (refine_rcg ran_of_map_ref)
apply refine_dref_type
apply (simp add: br_def; fail)
apply (simp add: br_def; fail)
apply (rule rhs_step_bind_SPEC)
by (auto simp: br_def)
lemma leadsto_map4'_correct:
"leadsto_map4' ≤ leadsto_spec_alt"
proof -
note leadsto_map4'_ref
also note leadsto_map3'_ref
also note leadsto'_correct
also note leadsto_spec_leadsto_spec_alt
finally show ?thesis .
qed
end
end