Theory Liveness_Subsumption
section ‹Checking Always Properties›
subsection ‹Abstract Implementation›
theory Liveness_Subsumption
imports
Refine_Imperative_HOL.Sepref Worklist_Common Worklist_Algorithms_Subsumption_Graphs
begin
context Search_Space_Nodes_Defs
begin
sublocale G: Subgraph_Node_Defs .
no_notation E ("_ → _" [100, 100] 40)
notation G.E' ("_ → _" [100, 100] 40)
no_notation reaches ("_ →* _" [100, 100] 40)
notation G.G'.reaches ("_ →* _" [100, 100] 40)
no_notation reaches1 ("_ →⇧+ _" [100, 100] 40)
notation G.G'.reaches1 ("_ →⇧+ _" [100, 100] 40)
text ‹Plain set membership is also an option.›
definition "check_loop v ST = (∃ v' ∈ set ST. v' ≼ v)"
definition dfs :: "'a set ⇒ (bool × 'a set) nres" where
"dfs P ≡ do {
(P,ST,r) ← RECT (λdfs (P,ST,v).
do {
if check_loop v ST then RETURN (P, ST, True)
else do {
if ∃ v' ∈ P. v ≼ v' then
RETURN (P, ST, False)
else do {
let ST = v # ST;
(P, ST', r) ←
FOREACHcd {v'. v → v'} (λ(_,_,b). ¬b) (λv' (P,ST,_). dfs (P,ST,v')) (P,ST,False);
ASSERT (ST' = ST);
let ST = tl ST';
let P = insert v P;
RETURN (P, ST, r)
}
}
}
) (P,[],a⇩0);
RETURN (r, P)
}"
definition liveness_compatible where "liveness_compatible P ≡
(∀ x x' y. x → y ∧ x' ∈ P ∧ x ≼ x' ⟶ (∃ y' ∈ P. y ≼ y')) ∧
(∀ s' ∈ P. ∀ s. s ≼ s' ∧ V s ⟶
¬ (λ x y. x → y ∧ (∃ x' ∈ P. ∃ y' ∈ P. x ≼ x' ∧ y ≼ y'))⇧+⇧+ s s)
"
definition "dfs_spec ≡
SPEC (λ (r, P).
(r ⟶ (∃ x. a⇩0 →* x ∧ x →⇧+ x))
∧ (¬ r ⟶ ¬ (∃ x. a⇩0 →* x ∧ x →⇧+ x)
∧ liveness_compatible P ∧ P ⊆ {x. V x}
)
)"
end
locale Liveness_Search_Space_pre =
Search_Space_Nodes +
assumes finite_V: "finite {a. V a}"
begin
lemma check_loop_loop: "∃ v' ∈ set ST. v' ≼ v" if "check_loop v ST"
using that unfolding check_loop_def by blast
lemma check_loop_no_loop: "v ∉ set ST" if "¬ check_loop v ST"
using that unfolding check_loop_def by blast
lemma mono:
"a ≼ b ⟹ a → a' ⟹ V b ⟹ ∃ b'. b → b' ∧ a' ≼ b'"
by (auto dest: mono simp: G.E'_def)
context
fixes P :: "'a set" and E1 E2 :: "'a ⇒ 'a ⇒ bool" and v :: 'a
defines [simp]: "E1 ≡ λx y. x → y ∧ (∃x'∈P. x ≼ x') ∧ (∃x∈P. y ≼ x)"
defines [simp]: "E2 ≡ λx y. x → y ∧ (x ≼ v ∨ (∃xa∈P. x ≼ xa)) ∧ (y ≼ v ∨ (∃x∈P. y ≼ x))"
begin
interpretation G: Graph_Defs E1 .
interpretation G': Graph_Defs E2 .
interpretation SG: Subgraph E2 E1 by standard auto
interpretation SG': Subgraph_Start E a⇩0 E1 by standard auto
interpretation SG'': Subgraph_Start E a⇩0 E2 by standard auto
lemma G_subgraph_reaches[intro]:
"G.G'.reaches a b" if "G.reaches a b"
using that by induction auto
lemma G'_subgraph_reaches[intro]:
"G.G'.reaches a b" if "G'.reaches a b"
using that by induction auto
lemma liveness_compatible_extend:
assumes
"V s" "V v" "s ≼ v"
"liveness_compatible P"
"∀va. v → va ⟶ (∃x∈P. va ≼ x)"
"E2⇧+⇧+ s s"
shows False
proof -
include graph_automation_aggressive
have 1: "∃ b' ∈ P. b ≼ b'" if "G.reaches a b" "a ≼ a'" "a' ∈ P" for a a' b
using that by cases auto
have 2: "E1 a b" if "a → b" "a ≼ a'" "a' ∈ P" "V a" for a a' b
using assms(4) that unfolding liveness_compatible_def by auto
from assms(6) have "E2⇧+⇧+ s s"
by auto
have 4: "G.reaches a b" if "G'.reaches a b" "a ≼ a'" "a' ∈ P" "V a" for a a' b
using that
proof induction
case base
then show ?case
by blast
next
case (step b c)
then have "G.reaches a b"
by auto
from ‹V a› ‹G.reaches a b› have "V b"
including subgraph_automation by blast
from ‹G.reaches a b› ‹a ≼ a'› ‹a' ∈ P› obtain b' where "b' ∈ P" "b ≼ b'"
by (fastforce dest: 1)
with ‹E2 b c› ‹V b› have "E1 b c"
by (fastforce intro: 2)
with ‹G.reaches a b› show ?case
by blast
qed
from ‹E2⇧+⇧+ s s› obtain x where "E2 s x" "G'.reaches x s"
by blast
then have "s → x"
by auto
with ‹s ≼ v› ‹V s› ‹V v› obtain x' where "v → x'" "x ≼ x'"
by (auto dest: mono)
with assms(5) obtain x'' where "x ≼ x''" "x'' ∈ P"
by (auto intro: order_trans)
from 4[OF ‹G'.reaches x s› ‹x ≼ x''› ‹x'' ∈ P›] ‹s → x› ‹V s› have "G.reaches x s"
including subgraph_automation by blast
with ‹x ≼ x''› ‹x'' ∈ P› obtain s' where "s ≼ s'" "s' ∈ P"
by (blast dest: 1)
with ‹s → x› ‹x ≼ x''› ‹x'' ∈ P› have "E1 s x"
by auto
with ‹G.reaches x s› have "G.reaches1 s s"
by blast
with assms(4) ‹s' ∈ P› ‹s ≼ s'› ‹V s› show False
unfolding liveness_compatible_def by auto
qed
lemma liveness_compatible_extend':
assumes
"V s" "V v" "s ≼ s'" "s' ∈ P"
"∀va. v → va ⟶ (∃x∈P. va ≼ x)"
"liveness_compatible P"
"E2⇧+⇧+ s s"
shows False
proof -
show ?thesis
proof (cases "G.reaches1 s s")
case True
with assms show ?thesis
unfolding liveness_compatible_def by auto
next
case False
with SG.non_subgraph_cycle_decomp[of s s] assms(7) obtain c d where **:
"G'.reaches s c" "E2 c d" "¬ E1 c d" "G'.reaches d s"
by auto
from ‹E2 c d› ‹¬ E1 c d› have "c ≼ v ∨ d ≼ v"
by auto
with ‹V s› ** obtain v' where "G'.reaches1 v' v'" "v' ≼ v" "V v'"
apply atomize_elim
apply (erule disjE)
subgoal
including graph_automation_aggressive
by (blast intro: rtranclp_trans G.subgraphI)
subgoal
unfolding G'.reaches1_reaches_iff2
by (blast intro: rtranclp_trans intro: G.subgraphI)
done
with assms show ?thesis
by (auto intro: liveness_compatible_extend)
qed
qed
end
lemma liveness_compatible_cycle_start:
assumes
"liveness_compatible P" "a →* x" "x →⇧+ x" "a ≼ s" "s ∈ P"
shows False
proof -
include graph_automation_aggressive
have *: "∃ y ∈ P. x ≼ y" if "G.G'.reaches a x" for x
using that assms unfolding liveness_compatible_def by induction auto
have **:
"(λx y. x → y ∧ (∃x'∈P. x ≼ x') ∧ (∃x∈P. y ≼ x))⇧+⇧+ a' b ⟷ a' →⇧+ b "
if "a →* a'" for a' b
apply standard
subgoal
by (induction rule: tranclp_induct; blast)
subgoal
using ‹a →* a'›
apply - apply (induction rule: tranclp.induct)
subgoal for a' b'
by (auto intro: *)
by (rule tranclp.intros(2), auto intro: *)
done
from assms show ?thesis
unfolding liveness_compatible_def by clarsimp (blast dest: * ** intro: G.subgraphI)
qed
lemma liveness_compatible_inv:
assumes "V v" "liveness_compatible P" "∀va. v → va ⟶ (∃x∈P. va ≼ x)"
shows "liveness_compatible (insert v P)"
using assms
apply (subst liveness_compatible_def)
apply safe
apply clarsimp_all
apply (meson mono order_trans; fail)
apply (subst (asm) liveness_compatible_def, meson; fail)
by (blast intro: liveness_compatible_extend liveness_compatible_extend')+
interpretation subsumption: Subsumption_Graph_Pre_Nodes "(≼)" "(≺)" E V
by standard (drule mono, auto simp: Subgraph_Node_Defs.E'_def)
lemma pre_cycle_cycle:
"(∃ x x'. a⇩0 →* x ∧ x →⇧+ x' ∧ x ≼ x') ⟷ (∃ x. a⇩0 →* x ∧ x →⇧+ x)"
by (meson G.E'_def G.G'.reaches1_reaches_iff1 subsumption.pre_cycle_cycle_reachable finite_V)
lemma reachable_alt:
"V v" if "V a⇩0" "a⇩0 →* v"
using that(2,1) by cases (auto simp: G.E'_def)
lemma dfs_correct:
"dfs P ≤ dfs_spec" if "V a⇩0" "liveness_compatible P" "P ⊆ {x. V x}"
proof -
define rpre where "rpre ≡ λ(P,ST,v).
a⇩0 →* v
∧ V v
∧ P ⊆ {x. V x}
∧ set ST ⊆ {x. a⇩0 →* x}
∧ set ST ⊆ {x. V x}
∧ liveness_compatible P
∧ (∀ s ∈ set ST. s →⇧+ v)
∧ distinct ST
"
define rpost where "rpost ≡ λ(P,ST,v) (P',ST',r).
(r ⟶ (∃ x x'. a⇩0 →* x ∧ x →⇧+ x' ∧ x ≼ x') ∧ ST' = ST) ∧
(¬ r ⟶
P ⊆ P'
∧ P' ⊆ {x. V x}
∧ set ST ⊆ {x. a⇩0 →* x}
∧ ST' = ST
∧ (∀ s ∈ set ST. s →* v)
∧ liveness_compatible P'
∧ (∃ v' ∈ P'. v ≼ v')
∧ distinct ST
)
"
define inv where "inv ≡ λ P ST v (_ :: 'a set) it (P', ST', r).
(r ⟶ (∃ x x'. a⇩0 →* x ∧ x →⇧+ x' ∧ x ≼ x') ∧ ST' = ST) ∧
(¬ r ⟶
P ⊆ P'
∧ P' ⊆ {x. V x}
∧ set ST ⊆ {x. a⇩0 →* x}
∧ ST' = ST
∧ (∀ s ∈ set ST. s →* v)
∧ set ST ⊆ {x. V x}
∧ liveness_compatible P'
∧ (∀ v ∈ {v'. v → v'} - it. (∃ v' ∈ P'. v ≼ v'))
∧ distinct ST
)
"
define Termination :: "(('a set × 'a list × 'a) × 'a set × 'a list × 'a) set" where
"Termination = inv_image (finite_psupset {x. V x}) (λ (a,b,c). set b)"
have rpre_init: "rpre (P, [], a⇩0)"
unfolding rpre_def using ‹V a⇩0› ‹liveness_compatible P› ‹P ⊆ _› by auto
have wf: "wf Termination"
unfolding Termination_def by (blast intro: finite_V)
have successors_finite: "finite {v'. v → v'}" for v
using finite_V unfolding G.E'_def by auto
show ?thesis
unfolding dfs_def dfs_spec_def
apply (refine_rcg refine_vcg)
apply (rule Orderings.order.trans)
apply(rule RECT_rule[where
pre = rpre and
V = Termination and
M = "λx. SPEC (rpost x)"
])
subgoal
unfolding FOREACHcd_def by refine_mono
apply (rule wf; fail)
apply (rule rpre_init; fail)
defer
subgoal
apply refine_vcg
unfolding rpost_def pre_cycle_cycle
including graph_automation
by (auto dest: liveness_compatible_cycle_start)
apply (thin_tac "_ = f")
apply refine_vcg
subgoal for f x a b aa ba
by (subst rpost_def, subst (asm) (2) rpre_def, auto 4 4 dest: check_loop_loop)
subgoal for f x P b ST v
by (subst rpost_def, subst (asm) (2) rpre_def, force)
subgoal for f x P b ST v
apply (refine_vcg
FOREACHcd_rule[where I = "inv P (v # ST) v"]
)
apply clarsimp_all
subgoal
by (auto intro: successors_finite)
subgoal
using ‹V a⇩0›
by (
subst (asm) (2) rpre_def, subst inv_def,
auto dest: check_loop_no_loop
)
subgoal for _ it v' P' ST' c
apply (rule Orderings.order.trans)
apply rprems
subgoal
apply (subst rpre_def, subst (asm) inv_def)
apply clarsimp
subgoal premises prems
proof -
from prems ‹V a⇩0› have "v → v'"
by auto
with prems show ?thesis
by (auto intro: G.E'_V2)
qed
done
subgoal
using ‹V a⇩0› unfolding Termination_def
by (auto simp: finite_psupset_def inv_def intro: G.subgraphI)
subgoal
apply (subst inv_def, subst (asm) inv_def, subst rpost_def)
apply (clarsimp simp: it_step_insert_iff)
by (safe; (intro exI conjI)?; (blast intro: rtranclp_trans))
done
subgoal
by (subst (asm) inv_def, simp)
subgoal for P' ST' c
using ‹V a⇩0› by (subst rpost_def, subst (asm) inv_def, auto)
subgoal
by (subst (asm) inv_def, simp)
subgoal for P' ST'
using ‹V a⇩0›
by (subst rpost_def, subst (asm) inv_def, auto intro: liveness_compatible_inv G.subgraphI)
done
done
qed
end
locale Liveness_Search_Space_Defs =
Search_Space_Nodes_Defs +
fixes succs :: "'a ⇒ 'a list"
begin
definition dfs1 :: "'a set ⇒ (bool × 'a set) nres" where
"dfs1 P ≡ do {
(P,ST,r) ← RECT (λdfs (P,ST,v).
do {
ASSERT (V v ∧ set ST ⊆ {x. V x});
if check_loop v ST then RETURN (P, ST, True)
else do {
if ∃ v' ∈ P. v ≼ v' then
RETURN (P, ST, False)
else do {
let ST = v # ST;
(P, ST', r) ←
nfoldli (succs v) (λ(_,_,b). ¬b) (λv' (P,ST,_). dfs (P,ST,v')) (P,ST,False);
ASSERT (ST' = ST);
let ST = tl ST';
let P = insert v P;
RETURN (P, ST, r)
}
}
}
) (P,[],a⇩0);
RETURN (r, P)
}"
end
locale Liveness_Search_Space =
Liveness_Search_Space_Defs +
Liveness_Search_Space_pre +
assumes succs_correct: "V a ⟹ set (succs a) = {x. a → x}"
assumes finite_V: "finite {a. V a}"
begin
lemma succs_ref[refine]:
"(succs a, succs b) ∈ ⟨Id⟩list_rel" if "(a, b) ∈ Id"
using that by auto
lemma start_ref[refine]:
"((P, [], a⇩0), P, [], a⇩0) ∈ Id ×⇩r br id (λ xs. set xs ⊆ {x. V x}) ×⇩r br id V" if "V a⇩0"
using that by (auto simp: br_def)
lemma refine_aux[refine]:
"((x, x1c, True), x', x1a, True) ∈ Id ×⇩r br id (λxs. set xs ⊆ Collect V) ×⇩r Id"
if "(x1c, x1a) ∈ br id (λxs. set xs ⊆ {x. V x})" "(x, x') ∈ Id"
using that by auto
lemma refine_loop:
"(⋀x x'. (x, x') ∈ Id ×⇩r br id (λxs. set xs ⊆ {x. V x}) ×⇩r br id V ⟹
dfs' x ≤ ⇓ (Id ×⇩r br id (λxs. set xs ⊆ Collect V) ×⇩r bool_rel) (dfsa x')) ⟹
(x, x') ∈ Id ×⇩r br id (λxs. set xs ⊆ {x. V x}) ×⇩r br id V ⟹
x2 = (x1a, x2a) ⟹
x' = (x1, x2) ⟹
x2b = (x1c, x2c) ⟹
x = (x1b, x2b) ⟹
nfoldli (succs x2c) (λ(_, _, b). ¬ b) (λv' (P, ST, _). dfs' (P, ST, v')) (x1b, x2c # x1c, False)
≤ ⇓ (Id ×⇩r br id (λxs. set xs ⊆ {x. V x}) ×⇩r bool_rel)
(FOREACHcd {v'. x2a → v'} (λ(_, _, b). ¬ b)
(λv' (P, ST, _). dfsa (P, ST, v')) (x1, x2a # x1a, False))"
apply (subgoal_tac "(succs x2c, succs x2a) ∈ ⟨br id V⟩list_rel")
unfolding FOREACHcd_def
apply refine_rcg
apply (rule rhs_step_bind_SPEC)
apply (rule succs_correct)
apply (solves ‹auto simp: br_def›)
apply (erule nfoldli_refine)
apply (solves ‹auto simp: br_def›)+
unfolding br_def list_rel_def
by (simp, rule list.rel_refl_strong, auto intro: G.E'_V2 simp: succs_correct)
lemma dfs1_dfs_ref[refine]:
"dfs1 P ≤ ⇓ Id (dfs P)" if "V a⇩0"
using that unfolding dfs1_def dfs_def
apply refine_rcg
apply (solves ‹auto simp: br_def›)+
apply (rule refine_loop; assumption)
by (auto simp: br_def)
end
end