(* Title: Presburger-Automata/DFS.thy Author: Toshiaki Nishihara and Yasuhiko Minamide Author: Stefan Berghofer and Alex Krauss, TU Muenchen, 2008-2009 Author: Peter Gammie (data refinement futz), 2010 *) (*<*) 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})" (* Yuck, something to do with Skolems broke. *) 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 (* by (auto simp add: reachable_def ins_eq set_of_def cong: conj_cong) *) 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 (* context DFS *) (*>*) 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 (*>*)