Theory Liveness_Subsumption

(* Authors: Simon Wimmer, Peter Lammich *)

section ‹Checking Always Properties›

subsection ‹Abstract Implementation›

theory Liveness_Subsumption
  imports
    Refine_Imperative_HOL.Sepref Worklist_Common Worklist_Algorithms_Subsumption_Graphs
begin

context Search_Space_Nodes_Defs
begin

sublocale G: Subgraph_Node_Defs .

no_notation E (‹_  _› [100, 100] 40)
notation G.E' (‹_  _› [100, 100] 40)
no_notation reaches (‹_ →* _› [100, 100] 40)
notation G.G'.reaches (‹_ →* _› [100, 100] 40)
no_notation reaches1 (‹_ + _› [100, 100] 40)
notation G.G'.reaches1 (‹_ + _› [100, 100] 40)

text ‹Plain set membership is also an option.›
definition "check_loop v ST = ( v'  set ST. v'  v)"

definition dfs :: "'a set  (bool × 'a set) nres" where
  "dfs P  do {
    (P,ST,r)  RECT (λdfs (P,ST,v).
      do {
        if check_loop v ST then RETURN (P, ST, True)
        else do {
          if  v'  P. v  v' then
            RETURN (P, ST, False)
          else do {
              let ST = v # ST;
              (P, ST', r) 
                FOREACHcd {v'. v  v'} (λ(_,_,b). ¬b) (λv' (P,ST,_). dfs (P,ST,v')) (P,ST,False);
              ASSERT (ST' = ST);
              let ST = tl ST';
              let P = insert v P;
              RETURN (P, ST, r)
            }
        }
      }
    ) (P,[],a0);
    RETURN (r, P)
  }"

definition liveness_compatible where "liveness_compatible P 
    ( x x' y. x  y  x'  P  x  x'  ( y'  P. y  y')) 
    ( s'  P.  s. s  s'  V s 
      ¬ (λ x y. x  y  ( x'  P.  y'  P. x  x'  y  y'))++ s s)
    "

definition "dfs_spec 
  SPEC (λ (r, P).
    (r  ( x. a0 →* x  x + x))
   (¬ r  ¬ ( x. a0 →* x  x + x)
       liveness_compatible P  P  {x. V x}
    )
  )"

end (* Search Space Defs *)

locale Liveness_Search_Space_pre =
  Search_Space_Nodes +
  assumes finite_V: "finite {a. V a}"
begin

lemma check_loop_loop: " v'  set ST. v'  v" if "check_loop v ST"
  using that unfolding check_loop_def by blast

lemma check_loop_no_loop: "v  set ST" if "¬ check_loop v ST"
  using that unfolding check_loop_def by blast

lemma mono:
  "a  b  a  a'  V b   b'. b  b'  a'  b'"
  by (auto dest: mono simp: G.E'_def)

context
  fixes P :: "'a set" and E1 E2 :: "'a  'a  bool" and v :: 'a
  defines [simp]: "E1  λx y. x  y  (x'P. x  x')  (xP. y  x)"
  defines [simp]: "E2  λx y. x  y  (x  v  (xaP. x  xa))  (y  v  (xP. y  x))"
begin

interpretation G:  Graph_Defs E1  .
interpretation G': Graph_Defs E2 .
interpretation SG: Subgraph E2 E1 by standard auto
interpretation SG': Subgraph_Start E a0 E1 by standard auto
interpretation SG'': Subgraph_Start E a0 E2 by standard auto

lemma G_subgraph_reaches[intro]:
  "G.G'.reaches a b" if "G.reaches a b"
  using that by induction auto

lemma G'_subgraph_reaches[intro]:
  "G.G'.reaches a b" if "G'.reaches a b"
  using that by induction auto

lemma liveness_compatible_extend:
  assumes
    "V s" "V v" "s  v"
    "liveness_compatible P"
    "va. v  va  (xP. va  x)"
    "E2++ s s"
  shows False
proof -
  include graph_automation_aggressive
  have 1: " b'  P. b  b'" if "G.reaches a b" "a  a'" "a'  P" for a a' b
    using that by cases auto
  have 2: "E1 a b" if "a  b" "a  a'" "a'  P" "V a" for a a' b
    using assms(4) that unfolding liveness_compatible_def by auto
  from assms(6) have "E2++ s s"
    by auto
  have 4: "G.reaches a b" if "G'.reaches a b" "a  a'" "a'  P" "V a" for a a' b
    using that
  proof induction
    case base
    then show ?case
      by blast
  next
    case (step b c)
    then have "G.reaches a b"
      by auto
    from V a G.reaches a b have "V b"
      including subgraph_automation by blast
    from G.reaches a b a  a' a'  P obtain b' where "b'  P" "b  b'"
      by (fastforce dest: 1)
    with E2 b c V b have "E1 b c"
      by (fastforce intro: 2)
    with G.reaches a b show ?case
      by blast
  qed
  from E2++ s s obtain x where "E2 s x" "G'.reaches x s"
    by blast
  then have "s  x"
    by auto
  with s  v V s V v obtain x' where "v  x'" "x  x'"
    by (auto dest: mono)
  with assms(5) obtain x'' where "x  x''" "x''  P"
    by (auto intro: order_trans)
  from 4[OF G'.reaches x s x  x'' x''  P] s  x V s have "G.reaches x s"
    including subgraph_automation by blast
  with x  x'' x''  P obtain s' where "s  s'" "s'  P"
    by (blast dest: 1)
  with s  x x  x'' x''  P have "E1 s x"
    by auto
  with G.reaches x s have "G.reaches1 s s"
    by blast
  with assms(4) s'  P s  s' V s show False
    unfolding liveness_compatible_def by auto
qed

lemma liveness_compatible_extend':
  assumes
    "V s" "V v" "s  s'" "s'  P"
    "va. v  va  (xP. va  x)"
    "liveness_compatible P"
    "E2++ s s"
  shows False
proof -
  show ?thesis
  proof (cases "G.reaches1 s s")
    case True
    with assms show ?thesis
      unfolding liveness_compatible_def by auto
  next
    case False
    with SG.non_subgraph_cycle_decomp[of s s] assms(7) obtain c d where **:
      "G'.reaches s c" "E2 c d" "¬ E1 c d" "G'.reaches d s"
      by auto
    from E2 c d ¬ E1 c d have "c  v  d  v"
      by auto
    with V s ** obtain v' where "G'.reaches1 v' v'" "v'  v" "V v'"
      apply atomize_elim
      apply (erule disjE)
      subgoal
        including graph_automation_aggressive
        by (blast intro: rtranclp_trans G.subgraphI)
      subgoal
        unfolding G'.reaches1_reaches_iff2
        by (blast intro: rtranclp_trans intro: G.subgraphI)
      done
    with assms show ?thesis
      by (auto intro: liveness_compatible_extend)
  qed
qed

end (* Edge sets restricted to passed set *)

lemma liveness_compatible_cycle_start:
  assumes
    "liveness_compatible P" "a →* x" "x + x" "a  s" "s  P"
  shows False
proof -
  include graph_automation_aggressive
  have *: " y  P. x  y" if "G.G'.reaches a x" for x
    using that assms unfolding liveness_compatible_def by induction auto
  have **:
    "(λx y. x  y  (x'P. x  x')  (xP. y  x))++ a' b  a' + b "
    if "a →* a'" for a' b
    apply standard
    subgoal
      by (induction rule: tranclp_induct; blast)
    subgoal
      using a →* a'
      apply - apply (induction rule: tranclp.induct)
      subgoal for a' b'
        by (auto intro: *)
      by (rule tranclp.intros(2), auto intro: *)
    done
  from assms show ?thesis
    unfolding liveness_compatible_def by clarsimp (blast dest: * ** intro: G.subgraphI)
qed

lemma liveness_compatible_inv:
  assumes "V v" "liveness_compatible P" "va. v  va  (xP. va  x)"
  shows "liveness_compatible (insert v P)"
  using assms
  apply (subst liveness_compatible_def)
  apply safe
     apply clarsimp_all
     apply (meson mono order_trans; fail)
    apply (subst (asm) liveness_compatible_def, meson; fail)
  by (blast intro: liveness_compatible_extend liveness_compatible_extend')+

interpretation subsumption: Subsumption_Graph_Pre_Nodes "(≼)" "(≺)" E V
  by standard (drule mono, auto simp: Subgraph_Node_Defs.E'_def)

lemma pre_cycle_cycle:
  "( x x'. a0 →* x  x + x'  x  x')  ( x. a0 →* x  x + x)"
  by (meson G.E'_def G.G'.reaches1_reaches_iff1 subsumption.pre_cycle_cycle_reachable finite_V)

lemma reachable_alt:
  "V v" if "V a0" "a0 →* v"
  using that(2,1) by cases (auto simp: G.E'_def)

lemma dfs_correct:
  "dfs P  dfs_spec" if "V a0" "liveness_compatible P" "P  {x. V x}"
proof -

  define rpre where "rpre  λ(P,ST,v).
        a0 →* v
       V v
       P  {x. V x}
       set ST  {x. a0 →* x}
       set ST  {x. V x}
       liveness_compatible P
       ( s  set ST. s + v)
       distinct ST
    "

  define rpost where "rpost  λ(P,ST,v) (P',ST',r).
    (r  ( x x'. a0 →* x  x + x'  x  x')  ST' = ST) 
    (¬ r 
      P  P'
       P'  {x. V x}
       set ST  {x. a0 →* x}
       ST' = ST
       ( s  set ST. s →* v)
       liveness_compatible P'
       ( v'  P'. v  v')
       distinct ST
      )
      "

  define inv where "inv  λ P ST v (_ :: 'a set) it (P', ST', r).
    (r  ( x x'. a0 →* x  x + x'  x  x')  ST' = ST) 
    (¬ r 
        P  P'
       P'  {x. V x}
       set ST  {x. a0 →* x}
       ST' = ST
       ( s  set ST. s →* v)
       set ST  {x. V x}
       liveness_compatible P'
       ( v  {v'. v  v'} - it. ( v'  P'. v  v'))
       distinct ST
    )
  "

  define Termination :: "(('a set × 'a list × 'a) × 'a set × 'a list × 'a) set" where
    "Termination = inv_image (finite_psupset {x. V x}) (λ (a,b,c). set b)"

  have rpre_init: "rpre (P, [], a0)"
    unfolding rpre_def using V a0 liveness_compatible P P  _ by auto

  have wf: "wf Termination"
    unfolding Termination_def by (blast intro: finite_V)

  have successors_finite: "finite {v'. v  v'}" for v
    using finite_V unfolding G.E'_def by auto

  show ?thesis
    unfolding dfs_def dfs_spec_def
    apply (refine_rcg refine_vcg)
    apply (rule Orderings.order.trans)
     apply(rule RECT_rule[where
          pre = rpre and
          V = Termination and
          M = "λx. SPEC (rpost x)"
          ])

      (* Trimono *)
      subgoal
        unfolding FOREACHcd_def by refine_mono

      (* Termination *)
       apply (rule wf; fail)

      (* Precondition holds initially *)
      apply (rule rpre_init; fail)

     defer

    (* The postcondition establishes the specification *)
    subgoal
      apply refine_vcg
      unfolding rpost_def pre_cycle_cycle
      including graph_automation
      by (auto dest: liveness_compatible_cycle_start)

    apply (thin_tac "_ = f")

    (* Pre ⟶ Post *)
    apply refine_vcg

    (*
    (* Assertion *)
    subgoal for f x a b aa ba
      unfolding rpre_def by auto

    (* Assertion *)
    subgoal for f x a b aa ba
      unfolding rpre_def by auto
    *)

    (* Cycle found *)
    subgoal for f x a b aa ba
      by (subst rpost_def, subst (asm) (2) rpre_def, auto 4 4 dest: check_loop_loop)

    (* Subsumption *)
    subgoal for f x P b ST v
      by (subst rpost_def, subst (asm) (2) rpre_def, force)

    (* Foreach *)
    subgoal for f x P b ST v

      apply (refine_vcg
          FOREACHcd_rule[where I = "inv P (v # ST) v"]
          )
         apply clarsimp_all
        (*
      (* Finitely Branching *)
      subgoal
        thm succs_correct
        apply (auto intro: successors_finite simp: rpre_def rpost_def succs_correct)
          apply (subst succs_correct)
          oops
*)

      (* Finitely Branching *)
      subgoal
        by (auto intro: successors_finite)

      (* Pre ⟶ Invariant *)
      subgoal
        using V a0
        by (
          subst (asm) (2) rpre_def, subst inv_def,
          auto dest: check_loop_no_loop
        )

      (* Invariant *)
      subgoal for _ it v' P' ST' c
        apply (rule Orderings.order.trans)
         apply rprems

        (* Inv ⟶ Pre *)
        subgoal
          apply (subst rpre_def, subst (asm) inv_def)
          apply clarsimp
          subgoal premises prems
          proof -
            from prems V a0 have "v  v'"
              by auto
            with prems show ?thesis
              by (auto intro: G.E'_V2)
          qed
          done

        (* Termination *)
        subgoal
          using V a0 unfolding Termination_def
          by (auto simp: finite_psupset_def inv_def intro: G.subgraphI)

        (* Post ⟶ Inv *)
        subgoal
          apply (subst inv_def, subst (asm) inv_def, subst rpost_def)
          apply (clarsimp simp: it_step_insert_iff)
          by (safe; (intro exI conjI)?; (blast intro: rtranclp_trans))

        done

      (* Cycle ⟶ Assertion *)
      subgoal
        by (subst (asm) inv_def, simp)

      (* Cycle ⟶ Post *)
      subgoal for P' ST' c
        using V a0 by (subst rpost_def, subst (asm) inv_def, auto)

      (* No cycle ⟶ Assertion *)
      subgoal
        by (subst (asm) inv_def, simp)

      (* No cycle ⟶ Post *)
      subgoal for P' ST'
        using V a0
        by (subst rpost_def, subst (asm) inv_def, auto intro: liveness_compatible_inv G.subgraphI)

      done
    done
qed

end (* Search Space Finite Strict *)

locale Liveness_Search_Space_Defs =
  Search_Space_Nodes_Defs +
  fixes succs :: "'a  'a list"
begin

definition dfs1 :: "'a set  (bool × 'a set) nres" where
  "dfs1 P  do {
    (P,ST,r)  RECT (λdfs (P,ST,v).
      do {
        ASSERT (V v  set ST  {x. V x});
        if check_loop v ST then RETURN (P, ST, True)
        else do {
          if  v'  P. v  v' then
            RETURN (P, ST, False)
          else do {
              let ST = v # ST;
              (P, ST', r) 
                nfoldli (succs v) (λ(_,_,b). ¬b) (λv' (P,ST,_). dfs (P,ST,v')) (P,ST,False);
              ASSERT (ST' = ST);
              let ST = tl ST';
              let P = insert v P;
              RETURN (P, ST, r)
            }
        }
      }
    ) (P,[],a0);
    RETURN (r, P)
  }"

end (* Liveness Search Space Defs *)

locale Liveness_Search_Space =
  Liveness_Search_Space_Defs +
  Liveness_Search_Space_pre +
  assumes succs_correct: "V a  set (succs a) = {x. a  x}"
  assumes finite_V: "finite {a. V a}"
begin

― ‹The following complications only arise because we add the assertion in this refinement step.›
lemma succs_ref[refine]:
  "(succs a, succs b)  Idlist_rel" if "(a, b)  Id"
  using that by auto

lemma start_ref[refine]:
  "((P, [], a0), P, [], a0)  Id ×r br id (λ xs. set xs  {x. V x}) ×r br id V" if "V a0"
  using that by (auto simp: br_def)

lemma refine_aux[refine]:
  "((x, x1c, True), x', x1a, True)  Id ×r br id (λxs. set xs  Collect V) ×r Id"
  if "(x1c, x1a)  br id (λxs. set xs  {x. V x})" "(x, x')  Id"
  using that by auto

lemma refine_loop:
  "(x x'. (x, x')  Id ×r br id (λxs. set xs  {x. V x}) ×r br id V 
            dfs' x   (Id ×r br id (λxs. set xs  Collect V) ×r bool_rel) (dfsa x')) 
   (x, x')  Id ×r br id (λxs. set xs  {x. V x}) ×r br id V 
   x2 = (x1a, x2a) 
   x' = (x1, x2) 
   x2b = (x1c, x2c) 
   x = (x1b, x2b) 
   nfoldli (succs x2c) (λ(_, _, b). ¬ b) (λv' (P, ST, _). dfs' (P, ST, v')) (x1b, x2c # x1c, False)
     (Id ×r br id (λxs. set xs  {x. V x}) ×r bool_rel)
       (FOREACHcd {v'. x2a  v'} (λ(_, _, b). ¬ b)
          (λv' (P, ST, _). dfsa (P, ST, v')) (x1, x2a # x1a, False))"
  apply (subgoal_tac "(succs x2c, succs x2a)  br id Vlist_rel")

  unfolding FOREACHcd_def
   apply refine_rcg
   apply (rule rhs_step_bind_SPEC)
    apply (rule succs_correct)
    apply (solves auto simp: br_def)
   apply (erule nfoldli_refine)
     apply (solves auto simp: br_def)+
  unfolding br_def list_rel_def
  by (simp, rule list.rel_refl_strong, auto intro: G.E'_V2 simp: succs_correct)

lemma dfs1_dfs_ref[refine]:
  "dfs1 P   Id (dfs P)" if "V a0"
  using that unfolding dfs1_def dfs_def
  apply refine_rcg
            apply (solves auto simp: br_def)+
     apply (rule refine_loop; assumption)
  by (auto simp: br_def)

end (* Liveness Search Space *)

end (* Theory *)