Theory Liveness_Subsumption_Map

subsection ‹Implementation on Maps›

theory Liveness_Subsumption_Map
  imports Liveness_Subsumption Worklist_Common
begin

locale Liveness_Search_Space_Key_Defs =
  Liveness_Search_Space_Defs E for E :: "'v ⇒ 'v ⇒ bool" +
  fixes key :: "'v ⇒ 'k"
  fixes subsumes' :: "'v ⇒ 'v ⇒ bool" (infix ‹⊴› 50)
begin

sublocale Search_Space_Key_Defs where empty = undefined and subsumes' = subsumes' .

definition "check_loop_list v ST = (∃ v' ∈ set ST. v' ≼ v)"

definition "insert_map_set v S ≡
  let k = key v; S' = (case S k of Some S ⇒ S | None ⇒ {}) in S(k ↦ (insert v S'))
"

definition "push_map_list v S ≡
  let k = key v; S' = (case S k of Some S ⇒ S | None ⇒ []) in S(k ↦ v # S')
"

definition "check_subsumption_map_set v S ≡
  let k = key v; S' = (case S k of Some S ⇒ S | None ⇒ {}) in (∃ x ∈ S'. v ⊴ x)
"

definition "check_subsumption_map_list v S ≡
  let k = key v; S' = (case S k of Some S ⇒ S | None ⇒ []) in (∃ x ∈ set S'. x ⊴ v)
"

definition "pop_map_list v S ≡
  let k = key v; S' = (case S k of Some S ⇒ tl S | None ⇒ []) in S(k ↦ S')
"

definition dfs_map :: "('k ⇀ 'v set) ⇒ (bool × ('k ⇀ 'v set)) nres" where
  "dfs_map P ≡ do {
    (P,ST,r) ← RECT (λdfs (P,ST,v).
      if check_subsumption_map_list v ST then RETURN (P, ST, True)
      else do {
        if check_subsumption_map_set v P then
          RETURN (P, ST, False)
        else do {
            let ST = push_map_list v ST;
            (P, ST, r) ←
              nfoldli (succs v) (λ(_,_,b). ¬b) (λv' (P,ST,_). dfs (P,ST,v')) (P,ST,False);
            let ST = pop_map_list v ST;
            let P = insert_map_set v P;
            RETURN (P, ST, r)
          }
      }
    ) (P,(Map.empty::('k ⇀ 'v list)),a⇩0);
    RETURN (r, P)
  }"

end (* Search Space Nodes Empty Key Defs *)

locale Liveness_Search_Space_Key =
  Liveness_Search_Space + Liveness_Search_Space_Key_Defs +
  assumes subsumes_key[intro, simp]: "a ⊴ b ⟹ key a = key b"
  assumes V_subsumes': "V a ⟹ a ≼ b ⟷ a ⊴ b"
begin

definition
  "irrefl_trans_on R S ≡ (∀ x ∈ S. ¬ R x x) ∧ (∀ x ∈ S. ∀ y ∈ S. ∀ z ∈ S. R x y ∧ R y z ⟶ R x z)"

definition
  "map_list_rel =
    {(m, xs). ⋃ (set ` ran m) = set xs ∧ (∀ k. ∀ x. m k = Some x ⟶ (∀ v ∈ set x. key v = k))
          ∧ (∃ R. irrefl_trans_on R (set xs)
              ∧ (∀ k. ∀ x. m k = Some x ⟶ sorted_wrt R x) ∧ sorted_wrt R xs)
          ∧ distinct xs
    }"

definition "list_set_hd_rel x ≡ {(l, s). set l = s ∧ distinct l ∧ l ≠ [] ∧ hd l = x}"

lemma empty_map_list_rel:
  "(Map.empty, []) ∈ map_list_rel"
  unfolding map_list_rel_def irrefl_trans_on_def by auto

lemma rel_start[refine]:
  "((P, Map.empty, a⇩0), P', [], a⇩0) ∈ map_set_rel ×⇩r map_list_rel ×⇩r Id" if "(P, P') ∈ map_set_rel"
  using that unfolding map_set_rel_def by (auto intro: empty_map_list_rel)

lemma refine_True:
  "(x1b, x1) ∈ map_set_rel ⟹ (x1c, x1a) ∈ map_list_rel
  ⟹ ((x1b, x1c, True), x1, x1a, True) ∈ map_set_rel ×⇩r map_list_rel ×⇩r Id"
  by simp

lemma check_subsumption_ref[refine]:
  "V x2a ⟹ (x1b, x1) ∈ map_set_rel ⟹ check_subsumption_map_set x2a x1b = (∃x∈x1. x2a ≼ x)"
  unfolding map_set_rel_def list_set_rel_def check_subsumption_map_set_def
  unfolding ran_def by (auto split: option.splits simp: V_subsumes')

lemma check_subsumption'_ref[refine]:
  "set xs ⊆ {x. V x} ⟹ (m, xs) ∈ map_list_rel
  ⟹ check_subsumption_map_list x m = check_loop x xs"
  unfolding map_list_rel_def list_set_rel_def check_subsumption_map_list_def check_loop_def
  unfolding ran_def apply (clarsimp split: option.splits, safe)
  subgoal for R x' xs'
    by (drule sym, drule sym, subst (asm) V_subsumes'[symmetric], auto)
  by (subst (asm) V_subsumes'; force)

lemma not_check_loop_non_elem:
  "x ∉ set xs" if "¬ check_loop_list x xs"
  using that unfolding check_loop_list_def by auto

lemma insert_ref[refine]:
  "(x1b, x1) ∈ map_set_rel ⟹
   (x1c, x1a) ∈ ⟨Id⟩list_set_rel ⟹
   ¬ check_loop_list x2a x1c ⟹
   ((x1b, x2a # x1c, False), x1, insert x2a x1a, False) ∈ map_set_rel ×⇩r list_set_hd_rel x2a ×⇩r Id"
  unfolding list_set_hd_rel_def list_set_rel_def
  by (auto dest: not_check_loop_non_elem simp: br_def)

lemma insert_map_set_ref:
  "(m, S) ∈ map_set_rel ⟹ (insert_map_set x m, insert x S) ∈ map_set_rel"
  unfolding insert_map_set_def insert_def map_set_rel_def
  apply (clarsimp split: option.splits, safe)
  subgoal for x' S'
    unfolding ran_def Let_def by (auto split: option.splits split: if_split_asm)
  subgoal
    unfolding ran_def Let_def by (auto split: if_split_asm)
  subgoal
    unfolding ran_def Let_def
    apply (clarsimp split: option.splits, safe)
     apply (metis option.simps(3))
    by (metis insertCI option.inject)
  subgoal
    unfolding ran_def Let_def by (auto split: option.splits if_split_asm)
  by (auto simp: Let_def split: if_split_asm option.split)

lemma map_list_rel_memD:
  assumes "(m, xs) ∈ map_list_rel" "x ∈ set xs"
  obtains xs' where "x ∈ set xs'" "m (key x) = Some xs'"
  using assms unfolding map_list_rel_def ran_def by (auto 4 3 dest: sym)

lemma map_list_rel_memI:
  "(m, xs) ∈ map_list_rel ⟹ m k = Some xs' ⟹ x' ∈ set xs' ⟹ x' ∈ set xs"
  unfolding map_list_rel_def ran_def by auto

lemma map_list_rel_grouped_by_key:
  "x' ∈ set xs' ⟹ (m, xs) ∈ map_list_rel ⟹ m k = Some xs' ⟹ key x' = k"
  unfolding map_list_rel_def by auto

lemma map_list_rel_not_memI:
  "k ≠ key x ⟹ m k = Some xs' ⟹ (m, xs) ∈ map_list_rel ⟹ x ∉ set xs'"
  unfolding map_list_rel_def by auto

lemma map_list_rel_not_memI2:
  "x ∉ set xs'" if "m a = Some xs'" "(m, xs) ∈ map_list_rel" "x ∉ set xs"
  using that unfolding map_list_rel_def ran_def by auto

lemma push_map_list_ref:
  "x ∉ set xs ⟹ (m, xs) ∈ map_list_rel ⟹ (push_map_list x m, x # xs) ∈ map_list_rel"
  unfolding push_map_list_def
  apply (subst map_list_rel_def)
  apply (clarsimp, safe)
  subgoal for x' xs'
    unfolding ran_def Let_def
    by (auto split: option.split_asm if_split_asm intro: map_list_rel_memI)
  subgoal
    unfolding ran_def Let_def by (auto 4 3 split: option.splits if_splits)
  subgoal for x'
    unfolding ran_def Let_def
    apply (erule map_list_rel_memD, assumption)
    apply (cases "key x = key x'")
    subgoal for xs'
      by auto
    subgoal for xs'
      apply clarsimp
      apply (rule exI[where x = xs'])
       apply safe
      apply (inst_existentials "key x'")
       apply (solves auto)
      apply force
      done
    done
  subgoal for k xs' x'
    unfolding Let_def
    by (auto split: option.split_asm if_split_asm dest: map_list_rel_grouped_by_key)
  subgoal
  proof -
    assume A: "x ∉ set xs" "(m, xs) ∈ map_list_rel"
    then obtain R where *:
      "x ∉ set xs"
      "(⋃ x ∈ ran m. set x) = set xs"
      "∀k x. m k = Some x ⟶ (∀v∈set x. key v = k)"
      "distinct xs"
      "∀k x. m k = Some x ⟶ sorted_wrt R x"
      "sorted_wrt R xs"
      "irrefl_trans_on R (set xs)"
      unfolding map_list_rel_def by auto
    have **: "sorted_wrt (λa b. a = x ∧ b ≠ x ∨ a ≠ x ∧ b ≠ x ∧ R a b) xs" if
      "sorted_wrt R xs" "x ∉ set xs" for xs
      using that by (induction xs) auto

    show ?thesis
      apply (inst_existentials "λ a b. a = x ∧ b ≠ x ∨ a ≠ x ∧ b ≠ x ∧ R a b")
         apply safe
      unfolding Let_def
      subgoal
        using ‹irrefl_trans_on _ _› unfolding irrefl_trans_on_def by blast
      apply (clarsimp split: option.split_asm if_split_asm)
      subgoal
        apply (drule map_list_rel_not_memI, assumption, rule A)
        using *(5) by (auto intro: **)
      using A(1) *(5) by (auto 4 3 intro: * ** A dest: map_list_rel_not_memI2)
  qed
  by (auto simp: map_list_rel_def)

lemma insert_map_set_ref'[refine]:
  "(x1b, x1) ∈ map_set_rel ⟹
   (x1c, x1a) ∈ map_set_rel ⟹
   ¬ check_subsumption' x2a x1c ⟹
   ((x1b, insert_map_set x2a x1c, False), x1, insert x2a x1a, False) ∈ map_set_rel ×⇩r map_set_rel ×⇩r Id"
  by (auto intro: insert_map_set_ref)

lemma map_list_rel_check_subsumption_map_list:
  "set xs ⊆ {x. V x} ⟹ (m, xs) ∈ map_list_rel ⟹ ¬ check_subsumption_map_list x m ⟹ x ∉ set xs"
  unfolding check_subsumption_map_list_def by (auto 4 3 elim!: map_list_rel_memD dest: V_subsumes')

lemma push_map_list_ref'[refine]:
  "set x1a ⊆ {x. V x} ⟹
   (x1b, x1) ∈ map_set_rel ⟹
   (x1c, x1a) ∈ map_list_rel ⟹
   ¬ check_subsumption_map_list x2a x1c ⟹
   ((x1b, push_map_list x2a x1c, False), x1, x2a # x1a, False) ∈ map_set_rel ×⇩r map_list_rel ×⇩r Id"
  by (auto intro: push_map_list_ref dest: map_list_rel_check_subsumption_map_list)

lemma sorted_wrt_tl:
  "sorted_wrt R (tl xs)" if "sorted_wrt R xs"
  using that by (induction xs) auto

lemma irrefl_trans_on_mono:
  "irrefl_trans_on R S" if "irrefl_trans_on R S'" "S ⊆ S'"
  using that unfolding irrefl_trans_on_def by blast

lemma pop_map_list_ref[refine]:
  "(pop_map_list v m, S) ∈ map_list_rel" if "(m, v # S) ∈ map_list_rel"
  using that unfolding map_set_rel_def pop_map_list_def
  apply (clarsimp split: option.splits if_split_asm simp: Let_def, safe)
  subgoal premises prems
    using prems unfolding map_list_rel_def
    by clarsimp (rule map_list_rel_memD[OF prems(1), of v], simp, metis option.simps(3))
  subgoal premises prems0 for xs
    using prems0 unfolding map_list_rel_def
    apply clarsimp
    apply safe
    subgoal premises prems for R x xs'
    proof -
      have *: "x ∈ set S" if "x ∈ set (tl xs)" "m (key v) = Some xs"
      proof -
        from prems have "sorted_wrt R xs"
          by auto
        from ‹m (key v) = _› have "v ∈ set xs"
          using map_list_rel_memD[OF ‹(m, v # S) ∈ map_list_rel›, of v] by auto
        have *: "R v x" if "x ∈ set xs" "v ≠ x" for x
          using that prems by - (drule map_list_rel_memI[OF ‹_ ∈ map_list_rel›], auto)
        have "v ≠ x"
        proof (rule ccontr)
          assume "¬ v ≠ x"
          with that obtain a as bs where
            "xs = a # as @ v # bs"
            unfolding in_set_conv_decomp by (cases xs) auto
          with ‹sorted_wrt R xs› have "a ∈ set xs" "R a v" "a ∈ insert v (set S)"
            using map_list_rel_memI[OF ‹_ ∈ map_list_rel› ‹m _ = _›, of a]
            by auto
          with * ‹irrefl_trans_on _ _› show False
            unfolding irrefl_trans_on_def by auto
        qed
        with that show ?thesis
          by (auto elim: in_set_tlD dest: map_list_rel_memI[OF ‹_ ∈ map_list_rel›])
      qed
      moreover have "x ∈ set S" if "m a = Some xs'" "a ≠ key v" for a :: 'b
        using prems0 prems that by (metis map_list_rel_memI set_ConsD)
      then show ?thesis
        using prems unfolding ran_def by (auto split: if_split_asm intro: *)
    qed
    subgoal premises prems for R x
    proof -
      from map_list_rel_memD[OF ‹_ ∈ map_list_rel›, of x] ‹x ∈ _› obtain xs' where xs':
        "x ∈ set xs'" "m (key x) = Some xs'"
        by auto
      show ?thesis
      proof (cases "key x = key v")
        case True
        with prems xs' have [simp]: "xs' = xs"
          by auto
        from prems have "x ≠ v"
          by auto
        have "x ∈ set (tl xs)"
        proof (rule ccontr)
          assume "x ∉ set (tl xs)"
          with xs' have "hd xs = x"
            by (cases xs) auto
          from prems have "sorted_wrt R xs"
            by auto
          from ‹m (key v) = _› have "v ∈ set xs"
            using map_list_rel_memD[OF ‹(m, v # S) ∈ map_list_rel›, of v] by auto
          have *: "R v x" if "x ∈ set xs" "v ≠ x" for x
            using that prems by - (drule map_list_rel_memI[OF ‹_ ∈ map_list_rel›], auto)
          with ‹x ∈ set xs'› ‹x ≠ v› have "R v x"
            by auto
          from ‹v ∈ set xs› ‹hd xs = x› ‹x ≠ v› have "R x v"
            unfolding in_set_conv_decomp
            apply clarsimp
            using ‹sorted_wrt R xs›
            subgoal for ys
              by (cases ys) auto
            done
          with ‹R v x› ‹irrefl_trans_on _ _› ‹x ∈ set S› show False
            unfolding irrefl_trans_on_def by blast
        qed
        with xs' show ?thesis
          unfolding ‹xs' = _› ran_def by auto
      next
        case False
        with xs' show ?thesis
          unfolding ran_def by auto
      qed
    qed
    subgoal
      by (meson in_set_tlD)
    subgoal for R
      by (blast intro: irrefl_trans_on_mono sorted_wrt_tl)
    done
  done

lemma tl_list_set_ref:
  "(m, S) ∈ map_set_rel ⟹
   (st, ST) ∈ list_set_hd_rel x ⟹
   (tl st, ST - {x}) ∈ ⟨Id⟩list_set_rel"
  unfolding list_set_hd_rel_def list_set_rel_def
  by (auto simp: br_def distinct_hd_tl dest: in_set_tlD in_hd_or_tl_conv)

lemma succs_id_ref:
  "(succs x, succs x) ∈ ⟨Id⟩ list_rel"
  by simp

lemma dfs_map_dfs_refine':
  "dfs_map P ≤ ⇓ (Id ×⇩r map_set_rel) (dfs1 P')" if "(P, P') ∈ map_set_rel"
  using that
  unfolding dfs_map_def dfs1_def
  apply refine_rcg
    using [[goals_limit=1]]
             apply (clarsimp, rule check_subsumption'_ref; assumption)
            apply (clarsimp, rule refine_True; assumption)
          apply (clarsimp, rule check_subsumption_ref; assumption)
          apply (simp; fail)
         apply (clarsimp; rule succs_id_ref; fail)
        apply (clarsimp, rule push_map_list_ref'; assumption)
      by (auto intro: insert_map_set_ref pop_map_list_ref)

lemma dfs_map_dfs_refine:
  "dfs_map P ≤ ⇓ (Id ×⇩r map_set_rel) (dfs P')" if "(P, P') ∈ map_set_rel" "V a⇩0"
proof -
  note dfs_map_dfs_refine'[OF ‹_ ∈ map_set_rel›]
  also note dfs1_dfs_ref[OF ‹V a⇩0›]
  finally show ?thesis .
qed

end (* Liveness Search Space Key *)

end (* Theory *)