Theory Unified_PW

section ‹Unified Passed-Waiting-List›
theory Unified_PW
  imports Refine_Imperative_HOL.Sepref Worklist_Common Worklist_Algorithms_Subsumption_Graphs
begin

hide_const wait

subsection ‹Utilities›

definition take_from_set where
  "take_from_set s = ASSERT (s  {})  SPEC (λ (x, s'). x  s  s' = s - {x})"

lemma take_from_set_correct:
  assumes "s  {}"
  shows "take_from_set s  SPEC (λ (x, s'). x  s  s' = s - {x})"
using assms unfolding take_from_set_def by simp

lemmas [refine_vcg] = take_from_set_correct[THEN order.trans]



definition take_from_mset where
  "take_from_mset s = ASSERT (s  {#})  SPEC (λ (x, s'). x ∈# s  s' = s - {#x#})"

lemma take_from_mset_correct:
  assumes "s  {#}"
  shows "take_from_mset s  SPEC (λ (x, s'). x ∈# s  s' = s - {#x#})"
using assms unfolding take_from_mset_def by simp

lemmas [refine_vcg] = take_from_mset_correct[THEN order.trans]


lemma set_mset_mp: "set_mset m  s  n < count m x  xs"
  by (meson count_greater_zero_iff le_less_trans subsetCE zero_le)

lemma pred_not_lt_is_zero: "(¬ n - Suc 0 < n)  n=0" by auto

subsection ‹Generalized Worklist Algorithm›

context Search_Space_Defs_Empty
begin
  definition "reachable_subsumed S = {x' | x x'. reachable x'  ¬ empty x'  x'  x  x  S}"

  definition
    "pw_var =
      inv_image (
      {(b, b'). b  ¬ b'}
        <*lex*>
      {(passed', passed).
        passed'  {a. reachable a  ¬ empty a}  passed  {a. reachable a  ¬ empty a} 
        reachable_subsumed passed  reachable_subsumed passed'}
        <*lex*>
      measure size
      )
      (λ (a, b, c). (c, a, b))
      "

  definition "pw_inv_frontier passed wait =
    ( a  passed. ( a'  set_mset wait. a  a') 
    ( a'. E a a'  ¬ empty a'  ( b'  passed  set_mset wait. a'  b')))"

  definition "start_subsumed passed wait = (¬ empty a0  ( a  passed  set_mset wait. a0  a))"

  definition "pw_inv  λ (passed, wait, brk).
    (brk  ( f. reachable f  F f)) 
    (¬ brk 
      passed  {a. reachable a  ¬ empty a}
     pw_inv_frontier passed wait
     ( a  passed  set_mset wait. ¬ F a)
     start_subsumed passed wait
     set_mset wait  Collect reachable)
    "

  definition "add_pw_spec passed wait a  SPEC (λ(passed',wait',brk).
    if a'. E a a'  F a' then
      brk
    else
      ¬brk  set_mset wait'  set_mset wait  {a' . E a a'} 
      ( s  set_mset wait.  s'  set_mset wait'. s  s') 
      ( s  {a' . E a a'  ¬ empty a'}.  s'  set_mset wait'  passed. s  s') 
      ( s  passed  {a}.  s'  passed'. s  s') 
      (passed'  passed  {a}  {a' . E a a'  ¬ empty a'} 
      (( x  passed'. ¬ ( x'  passed. x  x'))  wait' ⊆# wait  passed = passed')
      )
  )"

  definition
    "init_pw_spec 
      SPEC (λ (passed, wait).
        if empty a0 then passed = {}  wait ⊆# {#a0#} else passed  {a0}  wait = {#a0#})"

  abbreviation subsumed_elem :: "'a  'a set  bool"
    where "subsumed_elem a M   a'. a'  M  a  a'"

  notation
    subsumed_elem  ((_/ ∈'' _) [51, 51] 50)

    definition "pw_inv_frontier' passed wait =
      ( a. a  passed 
        (a ∈' set_mset wait)
       ( a'. E a a'  ¬ empty a'  (a' ∈' passed  set_mset wait)))"

  lemma pw_inv_frontier_frontier':
    "pw_inv_frontier' passed wait" if
    "pw_inv_frontier passed wait" "passed  Collect reachable"
    using that unfolding pw_inv_frontier'_def pw_inv_frontier_def by (blast intro: trans)

  lemma
    "pw_inv_frontier passed wait" if "pw_inv_frontier' passed wait"
    using that unfolding pw_inv_frontier_def pw_inv_frontier'_def by blast

  definition pw_algo where
    "pw_algo = do
      {
        if F a0 then RETURN (True, {})
        else if empty a0 then RETURN (False, {})
        else do {
          (passed, wait)  init_pw_spec;
          (passed, wait, brk)  WHILEIT pw_inv (λ (passed, wait, brk). ¬ brk  wait  {#})
            (λ (passed, wait, brk). do
              {
                (a, wait)  take_from_mset wait;
                ASSERT (reachable a);
                if empty a then RETURN (passed, wait, brk) else add_pw_spec passed wait a
              }
            )
            (passed, wait, False);
            RETURN (brk, passed)
        }
      }
    "

end

subsubsection ‹Correctness Proof›

instance nat :: preorder ..

context Search_Space_finite begin

  lemma wf_worklist_var_aux:
    "wf {(passed', passed).
      passed'  {a. reachable a  ¬ empty a}  passed  {a. reachable a  ¬ empty a} 
      reachable_subsumed passed  reachable_subsumed passed'}"
  proof (rule finite_acyclic_wf, goal_cases)
    case 1
    have "{(passed', passed).
        passed'  {a. reachable a  ¬ empty a}  passed  {a. reachable a  ¬ empty a} 
        reachable_subsumed passed  reachable_subsumed passed'}
    {(passed', passed).
        passed  {a. reachable a  ¬ empty a}  passed'  {a. reachable a  ¬ empty a}}"
      unfolding reachable_subsumed_def by auto
    moreover have "finite " using finite_reachable using [[simproc add: finite_Collect]] by simp
    ultimately show ?case by (rule finite_subset)
  next
    case 2
    have *: "class.preorder (≤) ((<) :: nat  nat  bool)"
      by (rule preorder_class.axioms)
    show ?case
    proof (rule preorder.acyclicI_order[where f = "λ a. card (reachable_subsumed a)"],
           rule preorder_class.axioms, rule psubset_card_mono)
      fix a
      have "reachable_subsumed a  {a. reachable a  ¬ empty a}"
        unfolding reachable_subsumed_def by blast
      then show "finite (reachable_subsumed a)" using finite_reachable by (rule finite_subset)
    qed auto
  qed

  lemma wf_worklist_var:
    "wf pw_var"
    unfolding pw_var_def
    by (auto 4 3 intro: wf_worklist_var_aux finite_acyclic_wf preorder.acyclicI_order[where f = id]
          preorder_class.axioms)

  context
  begin

  private lemma aux5:
    assumes
      "a'  passed'"
      "a ∈# wait"
      "a  a'"
      "start_subsumed passed wait"
      "spassed. xpassed'. s  x"
      "s∈#wait - {#a#}. Multiset.Bex wait' ((≼) s)"
    shows "start_subsumed passed' wait'"
      using assms unfolding start_subsumed_def apply clarsimp
      by (metis Un_iff insert_DiffM2 local.trans mset_right_cancel_elem)

  private lemma aux11:
    assumes
      "empty a"
      "start_subsumed passed wait"
    shows "start_subsumed passed (wait - {#a#})"
      using assms unfolding start_subsumed_def
      by auto (metis UnI2 diff_single_trivial empty_mono insert_DiffM insert_noteq_member)

  lemma aux3_aux:
    assumes "pw_inv_frontier' passed wait"
      "¬ b ∈' set_mset wait"
      "E b b'"
      "¬ empty b" "¬ empty b'"
      "b ∈' passed"
      "reachable b" "passed  {a. reachable a  ¬ empty a}"
    shows "b' ∈' passed  set_mset wait"
  proof -
    from b ∈' _ obtain b1 where b1: "b  b1" "b1  passed"
      by blast
    with mono[OF this(1) E b b'] passed  _ reachable b ¬ empty b obtain b1' where
      "E b1 b1'" "b'  b1'"
      by auto
    moreover then have "¬ empty b1'"
      using assms(5) empty_mono by blast
    moreover from assms b1 have "¬ b1 ∈' set_mset wait"
      by (blast intro: trans)
    ultimately show ?thesis
      using assms(1) b1
      unfolding pw_inv_frontier'_def
      by (blast intro: trans)
  qed


  private lemma pw_inv_frontier_empty_elem:
    assumes "pw_inv_frontier passed wait" "passed  {a. reachable a  ¬ empty a}" "empty a"
    shows "pw_inv_frontier passed (wait - {#a#})"
    using assms unfolding pw_inv_frontier_def
    by simp
      (smt UnCI UnE diff_single_trivial empty_mono insert_DiffM2 mset_cancel_elem(1)
           subset_Collect_conv)

  private lemma aux3:
    assumes
      "set_mset wait  Collect reachable"
      "a ∈# wait"
      " s  set_mset (wait - {#a#}).  s'  set_mset wait'. s  s'"
      " s  {a'. E a a'  ¬ empty a'}.  s'  passed  set_mset wait'. s  s'"
      " s  passed  {a}.  s'  passed'. s  s'"
      "passed'  passed  {a}  {a' . E a a'  ¬ empty a}"
      "pw_inv_frontier passed wait"
      "passed  {a. reachable a  ¬ empty a}"
    shows "pw_inv_frontier passed' wait'"
  proof -
    from assms(1,2) have "reachable a"
      by (simp add: subset_iff)
    from assms have assms':
      "set_mset wait  Collect reachable"
      "a ∈# wait"
      " s. s ∈' set_mset (wait - {#a#})  s ∈' set_mset wait'"
      " s  {a'. E a a'  ¬ empty a'}. s ∈' passed  set_mset wait'"
      " s. s ∈' passed  {a}  s ∈' passed'"
      "passed'  passed  {a}  {a' . E a a'}"
      "pw_inv_frontier' passed wait"
      "passed  {a. reachable a  ¬ empty a}"
      by (blast intro: trans pw_inv_frontier_frontier')+

    show ?thesis unfolding pw_inv_frontier_def
      apply safe
      unfolding Bex_def
      subgoal for b b'
      proof (goal_cases)
        case A: 1
        from A(1) assms(6) consider "b  passed" | "a = b" | "E a b"
          by auto
        note cases = this
        from cases ¬ b ∈' set_mset wait' assms'(4) reachable a passed  _ have "reachable b"
          by cases (auto intro: reachable_step)
        with A(3,4) have "¬ empty b" by (auto simp: empty_E)
        from cases this reachable b consider "a = b" | "a  b" "b ∈' passed" "reachable b"
          using ¬ b ∈' set_mset wait' assms'(4) by cases (fastforce intro: reachable_step)+
        then consider "b  a" "reachable b" | "¬ b  a" "b ∈' passed" "reachable b"
          using ¬ b ∈' set_mset wait' assms'(4) reachable a by fastforce+
        then show ?case
        proof cases
          case 1
          with A(3,4) have "¬ empty b"
            by (auto simp: empty_E)
          with mono[OF 1(1) E b b' 1(2) reachable a] obtain b1' where
            "E a b1'" "b'  b1'"
            by auto
          with ¬ empty b' have "b1' ∈' passed  set_mset wait'"
            using assms'(4) by (auto dest: empty_mono)
          with b'  _ assms'(5) show ?thesis
            by (auto intro: trans)
        next
          case 2
          with A(3,4) have "¬ empty b"
            by (auto simp: empty_E)
          from 2 ¬ b ∈' set_mset wait' assms'(2,3) have "¬ b ∈' set_mset wait"
            by (metis insert_DiffM2 mset_right_cancel_elem)
          from
            aux3_aux[OF
              assms'(7) this E b b' ¬ empty b ¬ empty b' b ∈' passed reachable b assms'(8)
              ]
          have "b' ∈' passed  set_mset wait" .
          with assms'(2,3,5) show ?thesis
            by auto (metis insert_DiffM insert_noteq_member)
        qed
      qed
      done
  qed

  private lemma aux6:
    assumes
      "a ∈# wait"
      "start_subsumed passed wait"
      " s  set_mset (wait - {#a#})  {a'. E a a'  ¬ empty a'}.  s'  set_mset wait'. s  s'"
    shows "start_subsumed (insert a passed) wait'"
    using assms unfolding start_subsumed_def
    apply clarsimp
    apply (erule disjE)
     apply blast
    subgoal premises prems for x
    proof (cases "a = x")
      case True
      with prems show ?thesis by simp
    next
      case False
      with x ∈# wait have "x  set_mset (wait - {#a#})"
        by (metis insert_DiffM insert_noteq_member prems(1))
      with prems(2,4) _  x show ?thesis
        by (auto dest: trans)
    qed
  done

  lemma empty_E_star:
    "empty x'" if "E** x x'" "reachable x" "empty x"
    using that unfolding reachable_def
    by (induction rule: converse_rtranclp_induct)
       (blast intro: empty_E[unfolded reachable_def] rtranclp.rtrancl_into_rtrancl)+

  lemma aux4:
    assumes "pw_inv_frontier passed {#}" "reachable x" "start_subsumed passed {#}"
            "passed  {a. reachable a  ¬ empty a}" "¬ empty x"
    shows " x'  passed. x  x'"
  proof -
    from reachable x have "E** a0 x" by (simp add: reachable_def)
    have "¬ empty a0" using E** a0 x assms(5) empty_E_star by blast
    with assms(3) obtain b where "a0  b" "b  passed" unfolding start_subsumed_def by auto
    have "x'.  x''. E** b x'  x  x'  x'  x''  x''  passed" if
                     "E** a x"  "a  b"   "b  b'"   "b'  passed"
                     "reachable a" "reachable b" for a b b'
    using that proof (induction arbitrary: b b' rule: converse_rtranclp_induct)
      case base
      then show ?case by auto
    next
      case (step a a1 b b')
      show ?case
      proof (cases "empty a")
        case True
        with step.prems step.hyps have "empty x" by - (rule empty_E_star, auto)
        with step.prems show ?thesis by (auto intro: empty_subsumes)
      next
        case False
        with E a a1 a  b reachable a reachable b obtain b1 where
          "E b b1" "a1  b1"
          using mono by blast
        show ?thesis
        proof (cases "empty b1")
          case True
          with empty_mono a1  b1 have "empty a1" by blast
          with step.prems step.hyps have "empty x" by - (rule empty_E_star, auto simp: reachable_def)
          with step.prems show ?thesis by (auto intro: empty_subsumes)
        next
          case False
          from E b b1 a1  b1 obtain b1' where "E b' b1'" "b1  b1'"
            using ¬ empty a empty_mono assms(4) mono step.prems by blast
          from empty_mono[OF ¬ empty b1 b1  b1'] have "¬ empty b1'"
            by auto
          with E b' b1' b'  passed assms(1) obtain b1'' where "b1''  passed" "b1'  b1''"
            unfolding pw_inv_frontier_def by auto
          with b1  _ have "b1  b1''" using trans by blast
          with step.IH[OF a1  b1 this b1''  passed] reachable a E a a1 reachable b E b b1
          obtain x' x'' where
            "E** b1 x'" "x  x'" "x'  x''" "x''  passed"
            by (auto intro: reachable_step)
          moreover from E b b1 E** b1 x' have "E** b x'" by auto
          ultimately show ?thesis by auto
        qed
      qed
    qed
    from this[OF E** a0 x a0  b refl b  _] assms(4) b  passed show ?thesis
      by (auto intro: trans)
  qed

  lemmas [intro] = reachable_step

  private lemma aux7:
    assumes
      "a ∈# wait"
      "set_mset wait  Collect reachable"
      "set_mset wait'  set_mset (wait - {#a#})  Collect (E a)"
      "x ∈# wait'"
    shows "reachable x"
    using assms by (auto dest: in_diffD)

  private lemma aux8:
    "x  reachable_subsumed S'"  if "x  reachable_subsumed S" "sS. xS'. s  x"
    using that unfolding reachable_subsumed_def by (auto intro: trans)

  private lemma aux9:
    assumes
      "set_mset wait'  set_mset (wait - {#a#})  Collect (E a)"
      "x ∈# wait'" "a'. E a a'  ¬ F a'" "F x"
      "apassed  set_mset wait. ¬ F a"
    shows False
  proof -
    from assms(1,2) have "x  set_mset wait  x  Collect (E a)"
      by (meson UnE in_diffD subsetCE)
    with assms(3,4,5) show ?thesis
      by auto
  qed

  private lemma aux10:
    assumes "apassed'  set_mset wait. ¬ F a" "F x" "x ∈# wait - {#a#}"
    shows "False"
    by (meson UnI2 assms in_diffD)

  lemma aux12:
    "size wait' < size wait" if "wait' ⊆# wait - {#a#}" "a ∈# wait"
    using that
    by (metis
        Diff_eq_empty_iff_mset add_diff_cancel_left' add_mset_add_single add_mset_not_empty
        insert_subset_eq_iff mset_le_add_mset_decr_left1 mset_subset_size subset_mset_def)

  lemma aux13:
    assumes
    "passed  {a. reachable a  ¬ empty a}"
    "passed'  insert a (passed  {a'. E a a'  ¬ empty a'})"
    "¬ empty a"
    "reachable a"
    "spassed. xpassed'. s  x"
    "a''  passed'"
    "xpassed. ¬ a''  x"
    shows
    "passed'  {a. reachable a  ¬ empty a}  reachable_subsumed passed  reachable_subsumed passed'
      passed' = passed  size wait'' < size wait"
  proof -
    have "passed'  {a. reachable a  ¬ empty a}"
      using passed  _ passed'  _ ¬ empty a reachable a by auto
    moreover have "reachable_subsumed passed  reachable_subsumed passed'"
      unfolding reachable_subsumed_def
      using spassed. xpassed'. s  x assms(5-) passed'  {a. reachable a  ¬ empty a}
      by (auto 4 3 intro: trans)
    ultimately show ?thesis
      using passed  _ unfolding pw_var_def by auto
  qed

  method solve_vc =
    rule aux3 aux5 aux7 aux10 aux11 pw_inv_frontier_empty_elem; assumption; fail |
    rule aux3; auto; fail | auto intro: aux9; fail | auto dest: in_diffD; fail

  end ― ‹Context›

end ― ‹Search Space›

theorem (in Search_Space'_finite) pw_algo_correct:
  "pw_algo  SPEC (λ (brk, passed).
    (brk  F_reachable)
   (¬ brk 
      ( a. reachable a  ¬ empty a  ( b  passed. a  b))
     passed  {a. reachable a  ¬ empty a})
    )"
proof -
  note [simp] = size_Diff_submset pred_not_lt_is_zero
  note [dest] = set_mset_mp
  show ?thesis
    unfolding pw_algo_def init_pw_spec_def add_pw_spec_def F_reachable_def
    apply (refine_vcg wf_worklist_var)
      (* F a0*)
             apply (solves auto)
      (* empty a0 *)
            subgoal
              using empty_E_star final_non_empty unfolding reachable_def by auto
            subgoal
              using empty_E_star final_non_empty unfolding reachable_def by auto
            subgoal
              using empty_E_star final_non_empty unfolding reachable_def by auto
            subgoal
              using empty_E_star final_non_empty unfolding reachable_def by auto
            subgoal
              using empty_E_star final_non_empty unfolding reachable_def by auto
      (* Invar start*)
           apply (fastforce simp: pw_inv_def pw_inv_frontier_def start_subsumed_def
                            split: if_split_asm dest: mset_subset_eqD)
      (* Precondition for take-from-set *)
          apply (simp; fail)
      (* State is subsumed by passed*)
      (* Assertion *)
         apply (solves auto simp: pw_inv_def)
      (* Invariant for picking an empty wait list element *)
        subgoal for _ passed wait _ passed' _ _ brk _ a wait'
          by (clarsimp simp: pw_inv_def split: if_split_asm; safe; solve_vc)
      (* Termination for picking an empty wait list element *)
       apply (clarsimp simp: pw_var_def nonempty_has_size; fail)
      (* Invariant for picking a non-empty wait list element *)
      subgoal for _ passed wait _ passed' _ _ brk _ a wait'
        by (clarsimp simp: pw_inv_def split: if_split_asm; safe; solve_vc) (* slow *)
      (* Termination for picking a non-empty wait list element *)
      subgoal for  _ _ _ _ passed _ wait brk _ a wait'
        by (clarsimp simp: pw_inv_def split: if_split_asm; safe)
           (simp_all add: aux12 aux13 pw_var_def)
      (* I ∧ ¬ b ⟶ post *)
      using F_mono by (fastforce simp: pw_inv_def dest!: aux4 dest: final_non_empty)+
qed

lemmas (in Search_Space'_finite) [refine_vcg] = pw_algo_correct[THEN Orderings.order.trans]

end ― ‹End of Theory›