Theory KBPs.DFS

(*  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  xxs. 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
(*>*)