(*  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}

  use a generic DFS to construct the transitions and action function
  the implementation of the JKBP. This theory is largely due to
  Berghofer and Alex Krauss
 🚫‹"DBLP:conf/tphol/BerghoferR09"›. All proofs are elided as the
  details of how we explore the state space are inessential to the
  algorithm.

  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 [simp, code]:
  "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‹

  proofs are carried out in the locale of
 ~\ref{fig:kbps-theory-dfs-locale}, which details our
  on the parameters for the DFS to behave as one would
 . Intuitively we are traversing a graph defined by @{term
 succs"} from some initial work list @{term "wl"}, constructing an
  of type @{typ "'b"} as we go. The function @{term "ins"}
  the current node into this construction. The predicate
 {term "isNode"} is invariant over the set of states reachable from
  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.

  support our data refinement
 \S\ref{sec:kbps-automata-synthesis-alg}) we also require that the
  of nodes be adequate via the abstraction function
 {term "nodeAbs"}, which the transition relation @{term "succs"} and
  predicate @{term "memb"} must respect. To ensure termination
  must be the case that there are only a finite number of states,
  there might be an infinity of representations.

  characterise the DFS traversal using the reflexive
  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)}<sup>*</sup> `` 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‹

  make use of two results about the traversal. Firstly, that some
  of each reachable node has been incorporated into the
  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‹

 , that if an invariant holds on the initial object then it
  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
(*>*)