Theory Worklist_Subsumption

(* Authors: Lammich, Wimmer *)
section ‹Generic Worklist Algorithm with Subsumption›
theory Worklist_Subsumption
  imports "../Sepref"
begin

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 ⟹ x∈s" 
  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 ‹Search Spaces›
text ‹
  A search space consists of a step relation, a start state, 
  a final state predicate, and a subsumption preorder.
›
locale Search_Space_Defs =
  fixes E :: "'a ⇒ 'a ⇒ bool" ― ‹Step relation›
    and a⇩0 :: 'a                ― ‹Start state› 
    and F :: "'a ⇒ bool"      ― ‹Final states›
    and subsumes :: "'a ⇒ 'a ⇒ bool" (infix ‹≼› 50) ― ‹Subsumption preorder›
begin
  definition reachable where
    "reachable = E⇧*⇧* a⇩0"

  definition "F_reachable ≡ ∃a. reachable a ∧ F a"

end

text ‹The set of reachable states must be finite, 
  subsumption must be a preorder, and be compatible with steps and final states.›
locale Search_Space = Search_Space_Defs +
  assumes finite_reachable: "finite {a. reachable a}"

  assumes refl[intro!, simp]: "a ≼ a"
      and trans[trans]: "a ≼ b ⟹ b ≼ c ⟹ a ≼ c"

  assumes mono: "a ≼ b ⟹ E a a' ⟹ reachable a ⟹ reachable b ⟹ ∃ b'. E b b' ∧ a' ≼ b'"
      and F_mono: "a ≼ a' ⟹ F a ⟹ F a'"
begin

  lemma start_reachable[intro!, simp]:
    "reachable a⇩0"
  unfolding reachable_def by simp

  lemma step_reachable:
    assumes "reachable a" "E a a'"
    shows "reachable a'"
  using assms unfolding reachable_def by simp


  lemma finitely_branching:
    assumes "reachable a"  
    shows "finite (Collect (E a))"
    by (metis assms finite_reachable finite_subset mem_Collect_eq step_reachable subsetI)
    


end

subsection ‹Worklist Algorithm›

term card

context Search_Space_Defs begin
  definition "worklist_var = inv_image (finite_psupset (Collect reachable) <*lex*> measure size) (λ (a, b,c). (a,b))"
  
  definition "worklist_inv_frontier passed wait = 
    (∀ a ∈ passed. ∀ a'. E a a' ⟶ (∃ b' ∈ passed ∪ set_mset wait. a' ≼ b'))"
  
  definition "start_subsumed passed wait = (∃ a ∈ passed ∪ set_mset wait. a⇩0 ≼ a)"

  definition "worklist_inv ≡ λ (passed, wait, brk).
    passed ⊆ Collect reachable ∧
    (brk ⟶ (∃ f. reachable f ∧ F f)) ∧
    (¬ brk ⟶ 
      worklist_inv_frontier passed wait 
    ∧ (∀ a ∈ passed ∪ set_mset wait. ¬ F a) 
    ∧ start_subsumed passed wait
    ∧ set_mset wait ⊆ Collect reachable)
    "

  definition "add_succ_spec wait a ≡ SPEC (λ(wait',brk). 
    if ∃a'. E a a' ∧ F a' then 
      brk
    else set_mset wait' = set_mset wait ∪ {a' . E a a'} ∧ ¬brk
  )"

  definition worklist_algo where
    "worklist_algo = do
      { 
        if F a⇩0 then RETURN True
        else do {
          let passed = {};
          let wait = {#a⇩0#};
          (passed, wait, brk) ← WHILEIT worklist_inv (λ (passed, wait, brk). ¬ brk ∧ wait ≠ {#})
            (λ (passed, wait, brk). do
              { 
                (a, wait) ← take_from_mset wait;
                ASSERT (reachable a);
                if (∃ a' ∈ passed. a ≼ a') then RETURN (passed, wait, brk) else
                do
                  {
                    (wait,brk) ← add_succ_spec wait a;
                    let passed = insert a passed;
                    RETURN (passed, wait, brk)
                  }
              }
            )
            (passed, wait, False);
            RETURN brk
        }
      }
    "

end

subsubsection ‹Correctness Proof›

context Search_Space begin

  lemma wf_worklist_var:
    "wf worklist_var"
  unfolding worklist_var_def by (auto simp: finite_reachable)

  context
  begin
  
  private lemma aux1:
    assumes "∀x∈passed. ¬ a ≼ x"
        and "passed ⊆ Collect reachable"
        and "reachable a"
    shows "
    ((insert a passed, wait', brk'),
     passed, wait, brk)
    ∈ worklist_var"
  proof -
    from assms have "a ∉ passed" by auto
    with assms(2,3) show ?thesis
    by (auto simp: worklist_inv_def worklist_var_def finite_psupset_def)
  qed

  private lemma aux2:
    assumes
      "a' ∈ passed"
      "a ≼ a'"
      "a ∈# wait"
      "worklist_inv_frontier passed wait"
    shows "worklist_inv_frontier passed (wait - {#a#})"
    using assms unfolding worklist_inv_frontier_def 
    using trans 
    apply clarsimp
    by (metis (no_types, lifting) Un_iff count_eq_zero_iff count_single mset_contains_eq mset_un_cases)

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

  private lemma aux3:
    assumes
      "set_mset wait ⊆ Collect reachable"
      "a ∈# wait"
      "set_mset wait' = set_mset (wait - {#a#}) ∪ Collect (E a)"
      "worklist_inv_frontier passed wait"
    shows "worklist_inv_frontier (insert a passed) wait'"
  proof -
    from assms(1,2) have "reachable a"
      by (simp add: subset_iff) 
    with finitely_branching have [simp, intro!]: "finite (Collect (E a))" . 

    from assms(2,3,4) show ?thesis unfolding worklist_inv_frontier_def
      by (metis Un_iff insert_DiffM insert_iff local.refl mem_Collect_eq set_mset_add_mset_insert)
  qed    

  private lemma aux6:
    assumes
      "a ∈# wait"
      "start_subsumed passed wait"
      "set_mset wait' = set_mset (wait - {#a#}) ∪ Collect (E a)"
    shows "start_subsumed (insert a passed) wait'"
    using assms unfolding start_subsumed_def
    by (metis Un_iff insert_DiffM insert_iff set_mset_add_mset_insert)

  lemma aux4:
    assumes "worklist_inv_frontier passed {#}" "reachable x" "start_subsumed passed {#}"
            "passed ⊆ Collect reachable"
    shows "∃ x' ∈ passed. x ≼ x'"
  proof -
    from ‹reachable x› have "E⇧*⇧* a⇩0 x" by (simp add: reachable_def)
    from assms(3) obtain b where "a⇩0 ≼ 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')
      from ‹E a a1› ‹a ≼ b› ‹reachable a› ‹reachable b› obtain b1 where
        "E b b1" "a1 ≼ b1"
      using mono by blast
      then obtain b1' where "E b' b1'" "b1 ≼ b1'" using assms(4) mono step.prems by blast
      with ‹b' ∈ passed› assms(1) obtain b1'' where "b1'' ∈ passed" "b1' ≼ b1''"
      unfolding worklist_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: step_reachable)
      moreover from ‹E b b1› ‹E⇧*⇧* b1 x'› have "E⇧*⇧* b x'" by auto
      ultimately show ?case by auto
    qed
    from this[OF ‹E⇧*⇧* a⇩0 x› ‹a⇩0 ≼ b› refl ‹b ∈ _›] assms(4) ‹b ∈ passed› show ?thesis
    by (auto intro: trans)
  qed

  theorem worklist_algo_correct:
    "worklist_algo ≤ SPEC (λ brk. brk ⟷ F_reachable)"
  proof - 
    note [simp] = size_Diff_submset pred_not_lt_is_zero
    note [dest] = set_mset_mp
    show ?thesis
    unfolding worklist_algo_def add_succ_spec_def F_reachable_def
      apply (refine_vcg wf_worklist_var)
      (* F a⇩0*)
      apply (auto; fail) []
      (* Invar start*)
      apply (auto simp: worklist_inv_def worklist_inv_frontier_def start_subsumed_def; fail)
      (* Precondition for take-from-set *)
      apply (simp; fail)
      (* State is subsumed by passed*)
        (* Assertion *)
        apply (auto simp: worklist_inv_def; fail)
        (*Invariant*)
        apply (auto simp: worklist_inv_def aux2 aux5 
              dest: in_diffD
              split: if_split_asm; fail) []
        (*Variant*)
        apply (auto simp: worklist_inv_def worklist_var_def intro: finite_subset[OF _ finite_reachable]; fail)

      (* Insert successors to wait *)  
        (*Invariant*)
        apply (clarsimp split: if_split_asm) (* Split on F in successors *)
          (* Found final state *)
          apply (clarsimp simp: worklist_inv_def; blast intro: step_reachable; fail)
          (* No final state *)
      apply (auto 
        simp: worklist_inv_def step_reachable aux3 aux6 finitely_branching
        dest: in_diffD; fail)[]
        (*Variant*)
        apply (auto simp: worklist_inv_def aux1; fail)
      (* I ∧ ¬b ⟹ post *)  
      using F_mono apply (fastforce simp: worklist_inv_def dest!: aux4)
      done
  qed  

  lemmas [refine_vcg] = worklist_algo_correct[THEN order_trans]

  end ― ‹Context›

end ― ‹Search Space›


subsection ‹Towards an Implementation›
locale Worklist1_Defs = Search_Space_Defs +
  fixes succs :: "'a ⇒ 'a list"

locale Worklist1 = Worklist1_Defs + Search_Space +
  assumes succs_correct: "reachable a ⟹ set (succs a) = Collect (E a)"
begin

  definition "add_succ1 wait a ≡ nfoldli (succs a) (λ(_,brk). ¬brk) (λa (wait,brk). if F a then RETURN (wait,True) else RETURN (wait + {#a#},False)) (wait, False)"

  lemma add_succ1_ref[refine]: "⟦(wait,wait')∈Id; (a,a')∈b_rel Id reachable⟧ ⟹ add_succ1 wait a ≤ ⇓(Id ×⇩r bool_rel) (add_succ_spec wait' a')"
    apply simp
    unfolding add_succ_spec_def add_succ1_def
    apply (refine_vcg nfoldli_rule[where I = "λl1 _ (wait',brk). if brk then ∃a'. E a a' ∧ F a' else set_mset wait' = set_mset wait ∪ set l1 ∧ set l1 ∩ Collect F = {}"])
    apply (auto; fail)
    using succs_correct[of a] apply (auto; fail)
    using succs_correct[of a] apply (auto; fail)
    apply (auto; fail)
    using succs_correct[of a] apply (auto; fail)
    done

  definition worklist_algo1 where
    "worklist_algo1 = do
      { 
        if F a⇩0 then RETURN True
        else do {
          let passed = {};
          let wait = {#a⇩0#};
          (passed, wait, brk) ← WHILEIT worklist_inv (λ (passed, wait, brk). ¬ brk ∧ wait ≠ {#})
            (λ (passed, wait, brk). do
              { 
                (a, wait) ← take_from_mset wait;
                if (∃ a' ∈ passed. a ≼ a') then RETURN (passed, wait, brk) else
                do
                  {
                    (wait,brk) ← add_succ1 wait a;
                    let passed = insert a passed;
                    RETURN (passed, wait, brk)
                  }
              }
            )
            (passed, wait, False);
            RETURN brk
        }
      }
    "

  lemma worklist_algo1_ref[refine]: "worklist_algo1 ≤ ⇓Id worklist_algo"  
    unfolding worklist_algo1_def worklist_algo_def
    apply (refine_rcg)
    apply refine_dref_type
    unfolding worklist_inv_def
    apply auto
    done

end


end ― ‹Theory›