Theory Leadsto
section ‹Checking Leads-To Properties›
subsection ‹Abstract Implementation›
theory Leadsto
imports Liveness_Subsumption Unified_PW
begin
context Subsumption_Graph_Pre_Nodes
begin
context
assumes finite_V: "finite {x. V x}"
begin
lemma steps_cycle_mono:
assumes "G'.steps (x # ws @ y # xs @ [y])" "x ≼ x'" "V x" "V x'"
shows "∃ y' xs' ys'. y ≼ y' ∧ G'.steps (x' # xs' @ y' # ys' @ [y'])"
proof -
let ?n = "card {x. V x} + 1"
let ?xs = "y # concat (replicate ?n (xs @ [y]))"
from assms(1) have "G'.steps (x # ws @ [y])" "G'.steps (y # xs @ [y])"
by (auto intro: Graph_Start_Defs.graphI_aggressive2)
with G'.steps_replicate[of "y # xs @ [y]" ?n] have "G'.steps ?xs"
by auto
from steps_mono[OF ‹G'.steps (x # ws @ [y])› ‹x ≼ x'› ‹V x› ‹V x'›] obtain ys where
"G'.steps (x' # ys)" "list_all2 (≼) (ws @ [y]) ys"
by auto
then obtain y' ws' where "G'.steps (x' # ws' @ [y'])" "y ≼ y'"
unfolding list_all2_append1 list_all2_Cons1 by auto
with ‹G'.steps (x # ws @ [y])› have "V y" "V y'"
subgoal
using G'_steps_V_last assms(3) by fastforce
using G'_steps_V_last ‹G'.steps (x' # ws' @ [y'])› assms(4) by fastforce
with steps_mono[OF ‹G'.steps ?xs› ‹y ≼ y'›] obtain ys where ys:
"list_all2 (≼) (concat (replicate ?n (xs @ [y]))) ys" "G'.steps (y' # ys)"
by auto
let ?ys = "filter ((≼) y) ys"
have "length ?ys ≥ ?n"
using list_all2_replicate_elem_filter[OF ys(1), of y]
by auto
have "set ?ys ⊆ set ys"
by auto
also have "… ⊆ {x. V x}"
using ‹G'.steps (y' # _)› ‹V y'› by (auto simp: list_all_iff dest: G'_steps_V_all)
finally have "¬ distinct ?ys"
using distinct_card[of ?ys] ‹_ >= ?n›
by - (rule ccontr; drule distinct_length_le[OF finite_V]; simp)
from not_distinct_decomp[OF this] obtain as y'' bs cs where "?ys = as @ [y''] @ bs @ [y''] @ cs"
by auto
then obtain as' bs' cs' where
"ys = as' @ [y''] @ bs' @ [y''] @ cs'"
apply atomize_elim
apply simp
apply (drule filter_eq_appendD filter_eq_ConsD filter_eq_appendD[OF sym], clarify)+
apply clarsimp
subgoal for as1 as2 bs1 bs2 cs'
by (inst_existentials "as1 @ as2" "bs1 @ bs2") simp
done
from ‹G'.steps (y' # _)› have "G'.steps (y' # as' @ y'' # bs' @ [y''])"
unfolding ‹ys = _› by (force intro: Graph_Start_Defs.graphI_aggressive2)
moreover from ‹?ys = _› have "y ≼ y''"
proof -
from ‹?ys = _› have "y'' ∈ set ?ys" by auto
then show ?thesis by auto
qed
ultimately show ?thesis
using ‹G'.steps (x' # ws' @ [y'])›
by (inst_existentials y'' "ws' @ y' # as'" bs';
fastforce intro: Graph_Start_Defs.graphI_aggressive1
)
qed
lemma reaches_cycle_mono:
assumes "G'.reaches x y" "y →⇧+ y" "x ≼ x'" "V x" "V x'"
shows "∃ y'. y ≼ y' ∧ G'.reaches x' y' ∧ y' →⇧+ y'"
proof -
from assms obtain xs ys where *: "G'.steps (x # xs)" "y = last (x # xs)" "G'.steps (y # ys @ [y])"
apply atomize_elim
including reaches_steps_iff
apply safe
subgoal for xs xs'
by (inst_existentials "tl xs" xs') auto
done
have **: "∃as. G'.steps (x # as @ last list # ys @ [last list])"
if a1: "G'.steps (x # a # list @ ys @ [last list])" "list ≠ []"
for a :: 'a and list :: "'a list"
proof -
from that have "butlast (a # list) @ [last list] = a # list"
by (metis (no_types) append_butlast_last_id last_ConsR list.simps(3))
then show ?thesis
using a1 by (metis (no_types) Cons_eq_appendI append.assoc self_append_conv2)
qed
from * obtain ws where "G'.steps (x # ws @ y # ys @ [y])"
apply atomize_elim
apply (cases xs)
apply (inst_existentials ys)
apply simp
apply rotate_tac
apply (rule G'.steps_append', assumption+, simp+)
apply safe
apply (inst_existentials "[] :: 'a list")
apply (solves ‹auto dest: G'.steps_append›)
apply (drule G'.steps_append)
apply assumption
apply simp
apply simp
by (rule **)
from steps_cycle_mono[OF this ‹x ≼ x'› ‹V x› ‹V x'›] obtain y' xs' ys' where
"y ≼ y'"
"G'.steps (x' # xs' @ y' # ys' @ [y'])"
by safe
then have "G'.steps (x' # xs' @ [y'])" "G'.steps (y' # ys' @ [y'])"
by (force intro: Graph_Start_Defs.graphI_aggressive2)+
with ‹y ≼ y'› show ?thesis
including reaches_steps_iff by force
qed
end
end
locale Leadsto_Search_Space =
A: Search_Space'_finite E a⇩0 _ "(≼)" empty
for E a⇩0 empty and subsumes :: "'a ⇒ 'a ⇒ bool" (infix ‹≼› 50)
+
fixes P Q :: "'a ⇒ bool"
assumes P_mono: "a ≼ a' ⟹ ¬ empty a ⟹ P a ⟹ P a'"
assumes Q_mono: "a ≼ a' ⟹ ¬ empty a ⟹ Q a ⟹ Q a'"
fixes succs_Q :: "'a ⇒ 'a list"
assumes succs_Q_correct: "A.reachable a ⟹ set (succs_Q a) = {y. E a y ∧ Q y ∧ ¬ empty y}"
begin
sublocale A': Search_Space'_finite E a⇩0 "λ _. False" "(≼)" empty
apply standard
apply (rule A.refl A.trans A.mono A.empty_subsumes A.empty_mono A.empty_E; assumption)+
apply assumption
apply blast
apply (rule A.finite_reachable)
done
sublocale B:
Liveness_Search_Space
"λ x y. E x y ∧ Q y ∧ ¬ empty y" a⇩0 "λ _. False" "(≼)" "λ x. A.reachable x ∧ ¬ empty x"
succs_Q
apply standard
apply (rule A.refl A.trans; assumption)+
subgoal for a b a'
by safe (drule A.mono; auto intro: Q_mono dest: A.mono A.empty_mono)
apply blast
apply (solves ‹auto intro: A.finite_reachable›)
subgoal
apply (subst succs_Q_correct)
unfolding Subgraph_Node_Defs.E'_def by auto
done
context
fixes a⇩1 :: 'a
begin
interpretation 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
definition has_cycle where
"has_cycle = B'.dfs"
end
definition leadsto :: "bool nres" where
"leadsto = do {
(r, passed) ← A'.pw_algo;
let P = {x. x ∈ passed ∧ P x ∧ Q x};
(r, _) ←
FOREACH⇩C P (λ(b,_). ¬b) (λv' (_,P). has_cycle v' P) (False,{});
RETURN r
}"
definition
"reaches_cycle a =
(∃ b. (λ x y. E x y ∧ Q y ∧ ¬ empty y)⇧*⇧* a b ∧ (λ x y. E x y ∧ Q y ∧ ¬ empty y)⇧+⇧+ b b)"
definition leadsto_spec where
"leadsto_spec = SPEC (λ r. r ⟷ (∃ a. A.reachable a ∧ ¬ empty a ∧ P a ∧ Q a ∧ reaches_cycle a))"
lemma
"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}"
"∀x ∈ passed. P x ∧ Q x ⟶ ¬ reaches_cycle x"
"A.reachable x" "¬ empty x" "P x" "Q x"
for x passed
proof (rule ccontr, unfold not_not)
assume "reaches_cycle x"
from that obtain x' where "x' ∈ passed" "x ≼ x'"
by auto
with that have "P x'" "Q x'"
by (auto intro: P_mono Q_mono)
with ‹x' ∈ passed› that(3) 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
show ?thesis
unfolding leadsto_def leadsto_spec_def
apply (refine_rcg refine_vcg)
subgoal for _ r passed
apply (refine_vcg
FOREACHc_rule'[where I = "inv {x ∈ passed. P x ∧ Q x}"]
)
subgoal
by (auto intro: finite_subset[OF _ A.finite_reachable])
subgoal
unfolding inv_def B.liveness_compatible_def by auto
subgoal for a⇩1 it σ a passed'
apply clarsimp
subgoal premises prems
proof -
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 ‹inv _ _ _› have
"B'.liveness_compatible passed'" "passed' ⊆ {x. A.reachable x ∧ ¬ empty x}"
unfolding inv_def by auto
from B'.dfs_correct[OF _ this] ‹passed ⊆ _› ‹a⇩1 ∈ _› ‹it ⊆ _› 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 passed'
apply (cases r)
apply simp
subgoal
unfolding inv_def
using ‹passed ⊆ _› ‹a⇩1 ∈ _› ‹it ⊆ _›
apply simp
apply (inst_existentials a⇩1)
by (auto 4 3 simp: reaches_cycle_iff)
subgoal
using ‹inv _ _ _› ‹passed ⊆ _› reaches_cycle_iff unfolding inv_def by blast
done
done
qed
done
subgoal for σ a b
unfolding inv_def by (auto dest!: aux1)
subgoal for it σ a b
unfolding inv_def by auto
done
done
qed
definition leadsto_spec_alt where
"leadsto_spec_alt =
SPEC (λ r.
r ⟷
(∃ a. (λ x y. E x y ∧ ¬ empty y)⇧*⇧* a⇩0 a ∧ ¬ empty a ∧ P a ∧ Q a ∧ reaches_cycle a)
)"
lemma E_reaches_non_empty:
"(λ x y. E x y ∧ ¬ empty y)⇧*⇧* a b" if "a →* b" "A.reachable a" "¬ empty b" for a b
using that
proof induction
case base
then show ?case by blast
next
case (step y z)
from ‹a →* y› ‹A.reachable a› have "A.reachable y"
by - (rule A.reachable_reaches)
have "¬ empty y"
proof (rule ccontr, unfold not_not)
assume "empty y"
from A.empty_E[OF ‹A.reachable y› ‹empty y› ‹E y z›] ‹¬ empty z› show False by blast
qed
with step show ?case
by (auto intro: rtranclp.intros(2))
qed
lemma leadsto_spec_leadsto_spec_alt:
"leadsto_spec ≤ leadsto_spec_alt"
unfolding leadsto_spec_def leadsto_spec_alt_def
by (auto
intro: Subgraph.intro Subgraph.reaches[rotated] E_reaches_non_empty[OF _ A.start_reachable]
simp: A.reachable_def
)
end
end