Theory KBPs.DFS
theory DFS
imports Main
begin
subsection‹Generic DFS›
text‹
\label{sec:dfs}
We use a generic DFS to construct the transitions and action function
of the implementation of the JKBP. This theory is largely due to
Stefan Berghofer and Alex Krauss
\<^citep>‹"DBLP:conf/tphol/BerghoferR09"›. All proofs are elided as the
fine details of how we explore the state space are inessential to the
synthesis algorithm.
The DFS itself is defined in the standard tail-recursive way:
›
partial_function (tailrec) gen_dfs where
"gen_dfs succs ins memb S wl = (case wl of
[] ⇒ S
| (x # xs) ⇒
if memb x S then gen_dfs succs ins memb S xs
else gen_dfs succs ins memb (ins x S) (succs x @ xs))"
lemma gen_dfs_simps[code, simp]:
"gen_dfs succs ins memb S [] = S"
"gen_dfs succs ins memb S (x # xs) =
(if memb x S then gen_dfs succs ins memb S xs
else gen_dfs succs ins memb (ins x S) (succs x @ xs))"
by (simp_all add: gen_dfs.simps)
text_raw‹
\begin{figure}
\begin{isabellebody}%
›
locale DFS =
fixes succs :: "'a ⇒ 'a list"
and isNode :: "'a ⇒ bool"
and invariant :: "'b ⇒ bool"
and ins :: "'a ⇒ 'b ⇒ 'b"
and memb :: "'a ⇒ 'b ⇒ bool"
and empt :: 'b
and nodeAbs :: "'a ⇒ 'c"
assumes ins_eq: "⋀x y S. ⟦ isNode x; isNode y; invariant S; ¬ memb y S ⟧
⟹ memb x (ins y S)
⟷ ((nodeAbs x = nodeAbs y) ∨ memb x S)"
and succs: "⋀x y. ⟦ isNode x; isNode y; nodeAbs x = nodeAbs y ⟧
⟹ nodeAbs ` set (succs x) = nodeAbs ` set (succs y)"
and empt: "⋀x. isNode x ⟹ ¬ memb x empt"
and succs_isNode: "⋀x. isNode x ⟹ list_all isNode (succs x)"
and empt_invariant: "invariant empt"
and ins_invariant: "⋀x S. ⟦ isNode x; invariant S; ¬ memb x S ⟧
⟹ invariant (ins x S)"
and graph_finite: "finite (nodeAbs ` { x . isNode x})"
text_raw‹
\end{isabellebody}%
\begin{isamarkuptext}%
\caption{The ‹DFS› locale.}
\label{fig:kbps-theory-dfs-locale}
\end{isamarkuptext}%
\end{figure}
›
text‹
The proofs are carried out in the locale of
Figure~\ref{fig:kbps-theory-dfs-locale}, which details our
requirements on the parameters for the DFS to behave as one would
expect. Intuitively we are traversing a graph defined by @{term
"succs"} from some initial work list @{term "wl"}, constructing an
object of type @{typ "'b"} as we go. The function @{term "ins"}
integrates the current node into this construction. The predicate
@{term "isNode"} is invariant over the set of states reachable from
the initial work list, and is respected by @{term "empt"} and @{term
"ins"}. We can also supply an invariant for the constructed object
(@{term "invariant"}). Inside the locale, @{term "dfs"} abbreviates
@{term "gen_dfs"} partially applied to the fixed parameters.
To support our data refinement
(\S\ref{sec:kbps-automata-synthesis-alg}) we also require that the
representation of nodes be adequate via the abstraction function
@{term "nodeAbs"}, which the transition relation @{term "succs"} and
visited predicate @{term "memb"} must respect. To ensure termination
it must be the case that there are only a finite number of states,
though there might be an infinity of representations.
We characterise the DFS traversal using the reflexive
transitive closure operator:
›
definition (in DFS) reachable :: "'a set ⇒ 'a set" where
"reachable xs ≡ {(x, y). y ∈ set (succs x)}⇧* `` xs"
context DFS
begin
definition
"succss xs ≡ ⋃x∈xs. set (succs x)"
definition
"set_of S ≡ {x. isNode x ∧ memb x S}"
abbreviation
"dfs ≡ gen_dfs succs ins memb"
definition rel where
"rel = inv_image finite_psubset (λS. nodeAbs ` {n. isNode n ∧ ¬ memb n S})"
lemma nodeAbs_subset_grot:
"⟦invariant S; isNode x; list_all isNode xs; ¬memb x S⟧
⟹ nodeAbs ` {n . isNode n ∧ ¬ memb n (ins x S)}
⊂ nodeAbs ` {n . isNode n ∧ ¬ memb n S}"
apply rule
apply (auto simp add: ins_eq cong: conj_cong)
apply (subgoal_tac "nodeAbs x ∈ nodeAbs ` {n. isNode n ∧ ¬ memb n S}")
apply (subgoal_tac "nodeAbs x ∉ nodeAbs ` {n. isNode n ∧ nodeAbs n ≠ nodeAbs x ∧ ¬ memb n S}")
apply blast
apply rule
apply (erule imageE) back
apply auto[1]
apply auto[1]
done
lemma psubsetI2: "⟦ A ⊆ B; x ∈ A; x ∉ B⟧ ⟹ A ⊂ B"
by (unfold less_le) blast
lemma dfs_induct[consumes 2, case_names base step]:
assumes S: "invariant S"
and xs: "list_all isNode xs"
and I1: "⋀S. invariant S ⟹ P S []"
and I2: "⋀S x xs. invariant S ⟹ isNode x ⟹ list_all isNode xs ⟹
(memb x S ⟹ P S xs) ⟹ (¬ memb x S ⟹ P (ins x S) (succs x @ xs)) ⟹ P S (x # xs)"
shows "P S xs" using I1 I2 S xs
apply induction_schema
apply atomize_elim
apply (case_tac xs, simp+)
apply atomize_elim
apply (rule conjI)
apply (rule ins_invariant, assumption+)
apply (rule succs_isNode, assumption)
apply (relation "rel <*lex*> measure length")
apply (simp add: wf_lex_prod rel_def)
apply simp
apply simp
apply (rule disjI1)
apply (simp add: rel_def finite_psubset_def)
apply (rule conjI)
apply (erule (3) nodeAbs_subset_grot)
apply (rule finite_subset[OF _ graph_finite])
apply auto
done
lemma visit_subset_dfs: "invariant S ⟹ list_all isNode xs ⟹
isNode y ⟹ memb y S ⟹ memb y (dfs S xs)"
by (induct S xs rule: dfs_induct) (simp_all add: ins_eq)
lemma next_subset_dfs: "invariant S ⟹ list_all isNode xs ⟹
x ∈ set xs ⟹ memb x (dfs S xs)"
proof (induct S xs rule: dfs_induct)
case (step S y xs)
then show ?case
by (auto simp add: visit_subset_dfs ins_eq ins_invariant succs_isNode)
qed simp
lemma succss_closed_dfs':
"invariant ys ⟹ list_all isNode xs ⟹
nodeAbs ` succss (set_of ys) ⊆ nodeAbs ` (set xs ∪ set_of ys) ⟹ nodeAbs ` succss (set_of (dfs ys xs)) ⊆ nodeAbs ` set_of (dfs ys xs)"
proof(induct ys xs rule: dfs_induct)
case (base S) thus ?case by simp
next
case (step S x xs) thus ?case
apply (auto simp add: succss_def set_of_def cong: conj_cong)
apply (subgoal_tac "nodeAbs xa ∈ nodeAbs ` (⋃x∈{x. isNode x ∧ memb x (dfs S xs)}. set (succs x))")
apply blast
apply blast
apply (subgoal_tac "nodeAbs ` (⋃x∈{xa. isNode xa ∧ memb xa (ins x S)}. set (succs x)) ⊆ nodeAbs ` (set (succs x) ∪ set xs ∪ {xa. isNode xa ∧ memb xa (ins x S)})")
apply blast
apply (auto simp add: ins_eq succss_def set_of_def cong: conj_cong)
apply (subgoal_tac "∃xc'. xc' ∈ set (succs x) ∧ nodeAbs xc' = nodeAbs xc")
apply clarsimp
apply (rule_tac x=xc' in image_eqI)
apply simp
apply simp
apply (cut_tac x=xd and y=x in succs)
apply simp_all
apply (subgoal_tac "nodeAbs xc ∈ nodeAbs ` set (succs x)")
apply auto[1]
apply auto[1]
apply (subgoal_tac "nodeAbs ` set (succs xd) ⊆ nodeAbs ` (⋃x∈{x. isNode x ∧ memb x S}. set (succs x))")
defer
apply auto[1]
apply (subgoal_tac "nodeAbs xc ∈ nodeAbs ` set (succs xd)")
defer
apply auto[1]
apply (subgoal_tac "nodeAbs xc ∈ insert (nodeAbs x) (nodeAbs ` (set xs ∪ {x. isNode x ∧ memb x S}))")
defer
apply (erule rev_subsetD)
apply (erule subset_trans)
apply blast
apply auto
done
qed
lemma succss_closed_dfs: "list_all isNode xs ⟹
nodeAbs ` succss (set_of (dfs empt xs)) ⊆ nodeAbs ` set_of (dfs empt xs)"
apply (rule succss_closed_dfs')
apply (rule empt_invariant)
apply assumption
apply (simp add: succss_def)
apply (rule subsetI)
apply clarsimp
unfolding set_of_def
using empt
apply clarsimp
done
definition
"succsr ≡ {(x, y). y ∈ set (succs x)}"
theorem succsr_isNode:
assumes xy: "(x, y) ∈ succsr⇧*"
shows "isNode x ⟹ isNode y" using xy
proof induct
case (step y z)
then have "isNode y" by simp
then have "list_all isNode (succs y)"
by (rule succs_isNode)
with step show ?case
by (simp add: succsr_def list_all_iff)
qed
lemma succss_closed:
assumes inc: "nodeAbs ` succss X ⊆ nodeAbs ` X"
and X: "X ⊆ { x . isNode x }"
shows "nodeAbs ` reachable X = nodeAbs ` X"
proof
show "nodeAbs ` X ⊆ nodeAbs ` reachable X"
unfolding reachable_def by auto
next
show "nodeAbs ` reachable X ⊆ nodeAbs ` X"
proof(unfold reachable_def, auto)
fix x y
assume y: "y ∈ X"
assume "(y, x) ∈ {(x, y). y ∈ set (succs x)}⇧*"
thus "nodeAbs x ∈ nodeAbs ` X" using y
proof induct
case base thus ?case by simp
next
case (step r s)
from X step have "isNode r"
using succsr_isNode[where x=y and y=r]
unfolding succsr_def by fastforce
with inc step show ?case
apply clarsimp
apply (subgoal_tac "isNode x")
apply (cut_tac x=r and y=x in succs)
apply auto
apply (subgoal_tac "nodeAbs s ∈ nodeAbs ` set (succs x)")
using X
apply (auto simp: succss_def)
done
qed
qed
qed
lemma dfs_isNode:
assumes S: "invariant S"
and xs: "list_all isNode xs"
shows "set_of (dfs S xs) ⊆ {x . isNode x}"
using assms
by (induct S xs rule: dfs_induct) (auto simp: set_of_def)
lemma reachable_closed_dfs:
assumes xs: "list_all isNode xs"
shows "nodeAbs ` reachable (set xs) ⊆ nodeAbs ` set_of (dfs empt xs)"
proof -
from xs have "reachable (set xs) ⊆ reachable (set_of (dfs empt xs))"
apply (unfold reachable_def)
apply (rule Image_mono)
apply (auto simp add: set_of_def next_subset_dfs empt_invariant list_all_iff)
done
hence "nodeAbs ` reachable (set xs) ⊆ nodeAbs ` reachable (set_of (dfs empt xs))"
by auto
also from succss_closed_dfs[OF xs] have "… = nodeAbs ` set_of (dfs empt xs)"
apply (rule succss_closed)
apply (rule dfs_isNode[OF empt_invariant xs])
done
finally show ?thesis .
qed
lemma reachable_succs: "reachable (set (succs x)) ⊆ reachable {x}"
by (auto simp add: reachable_def intro: converse_rtrancl_into_rtrancl)
lemma dfs_subset_reachable_visit_nodes:
"invariant ys ⟹ list_all isNode xs ⟹
nodeAbs ` set_of (dfs ys xs) ⊆ nodeAbs ` (reachable (set xs) ∪ set_of ys)"
proof(induct ys xs rule: dfs_induct)
case (step S x xs)
show ?case
proof (cases "memb x S")
case True
with step show ?thesis by (auto simp add: reachable_def)
next
case False
have "reachable (set (succs x)) ⊆ reachable {x}"
by (rule reachable_succs)
then have "reachable (set (succs x @ xs)) ⊆ reachable (set (x # xs))"
by (auto simp add: reachable_def)
then show ?thesis using step
apply (auto simp add: reachable_def set_of_def cong: conj_cong)
apply (subgoal_tac "nodeAbs xa ∈ nodeAbs `
({(x, y). y ∈ set (succs x)}⇧* `` set xs ∪
{x. isNode x ∧ memb x S})")
apply auto[1]
apply auto[1]
apply (subgoal_tac "nodeAbs xa ∈ nodeAbs `
({(x, y). y ∈ set (succs x)}⇧* `` (set (succs x) ∪ set xs) ∪
{xa. isNode xa ∧ memb xa (ins x S)})")
defer
apply auto[1]
apply auto[1]
apply (rule_tac x=xb in image_eqI)
apply auto[1]
apply auto[1]
apply (auto iff: ins_eq)
done
qed
qed (simp add: reachable_def)
theorem dfs_imp_reachable:
assumes y: "isNode y"
and xs: "list_all isNode xs"
and m: "memb y (dfs empt xs)"
shows "∃y'. nodeAbs y' = nodeAbs y ∧ y' ∈ reachable (set xs)"
proof -
from m dfs_subset_reachable_visit_nodes [OF empt_invariant xs] y
obtain y'
where "nodeAbs y' = nodeAbs y"
and "y' ∈ reachable (set xs)"
by (auto simp add: empt set_of_def)
thus ?thesis by blast
qed
text‹
We make use of two results about the traversal. Firstly, that some
representation of each reachable node has been incorporated into the
final construction:
›
theorem (in DFS) reachable_imp_dfs:
assumes y: "isNode y"
and xs: "list_all isNode xs"
and m: "y ∈ reachable (set xs)"
shows "∃y'. nodeAbs y' = nodeAbs y ∧ memb y' (dfs empt xs)"
using y m reachable_closed_dfs[OF xs]
apply (auto simp add: set_of_def)
apply (drule subsetD[where c="nodeAbs y"])
apply simp
apply auto
done
theorem dfs_invariant' [consumes 2, case_names base step]:
assumes S: "invariant S"
and xs: "list_all isNode xs"
and H: "I S"
and I: "⋀S x. ¬ memb x S ⟹ isNode x ⟹ invariant S ⟹ I S ⟹ I (ins x S)"
shows "I (dfs S xs)"
proof -
from S xs H
have "I (dfs S xs) ∧ invariant (dfs S xs)"
proof (induct S xs rule: dfs_induct)
case (step S x xs)
show ?case
proof (cases "memb x S")
case False
then show ?thesis
apply simp
apply (rule step)
apply assumption
apply (rule I)
apply assumption
apply (rule step)+
done
qed (simp add: step)
qed simp
then show ?thesis ..
qed
end
text‹
Secondly, that if an invariant holds on the initial object then it
holds on the final one:
›
theorem (in DFS) dfs_invariant:
assumes "invariant S"
assumes "list_all isNode xs"
shows "invariant (dfs S xs)"
using assms
by (induct S xs rule: dfs_induct) auto
text‹
\FloatBarrier
›
end