Theory Worklist_Locales

section ‹Preliminaries›

theory Worklist_Locales
  imports Refine_Imperative_HOL.Sepref Collections.HashCode Probabilistic_Timed_Automata.Graphs
  "HOL-ex.Sketch_and_Explore"
begin

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⇩₀ :: 'a                ― ‹Start state›
    and F :: "'a ⇒ bool"      ― ‹Final states›
    and subsumes :: "'a ⇒ 'a ⇒ bool" (infix "≼" 50) ― ‹Subsumption preorder›
begin

  sublocale Graph_Start_Defs E a⇩₀ .

  definition subsumes_strictly (infix "≺" 50) where
    "subsumes_strictly x y = (x ≼ y ∧ ¬ y ≼ x)"

  no_notation fun_rel_syn (infixr "→" 60)

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

end

locale Search_Space_Nodes_Defs = Search_Space_Defs +
  fixes V :: "'a ⇒ bool"

locale Search_Space_Defs_Empty = Search_Space_Defs +
  fixes empty :: "'a ⇒ bool"

locale Search_Space_Nodes_Empty_Defs = Search_Space_Nodes_Defs + Search_Space_Defs_Empty

locale Search_Space_Nodes = Search_Space_Nodes_Defs +
  assumes refl[intro!, simp]: "a ≼ a"
      and trans[trans]: "a ≼ b ⟹ b ≼ c ⟹ a ≼ c"

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

  sublocale preorder "(≼)" "(≺)"
    by standard (auto simp: subsumes_strictly_def intro: trans)

end (* Search Space Nodes *)

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_Nodes_Empty = Search_Space_Nodes_Empty_Defs +
  assumes refl[intro!, simp]: "a ≼ a"
      and trans[trans]: "a ≼ b ⟹ b ≼ c ⟹ a ≼ c"

  assumes mono:
      "a ≼ b ⟹ E a a' ⟹ V a ⟹ V b ⟹ ¬ empty a ⟹ ∃ b'. V b' ∧ E b b' ∧ a' ≼ b'"
      and empty_subsumes: "empty a ⟹ a ≼ a'"
      and empty_mono: "¬ empty a ⟹ a ≼ b ⟹ ¬ empty b"
      and empty_E: "V x ⟹ empty x ⟹ E x x' ⟹ empty x'"
      and F_mono: "a ≼ a' ⟹ F a ⟹ F a'"
begin

  sublocale preorder "(≼)" "(≺)"
    by standard (auto simp: subsumes_strictly_def intro: trans)

  sublocale search_space:
    Search_Space_Nodes "λ x y. E x y ∧ ¬ empty y" a⇩₀ F "(≼)" "λ v. V v ∧ ¬ empty v"
    apply standard
       apply blast
      apply (blast intro: trans)
     apply (drule mono; blast dest: empty_mono)
    apply (blast intro: F_mono)
    done

end (* Search Space Nodes *)

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_Empty +
  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 ⟹ ¬ empty a ⟹ ∃ b'. E b b' ∧ a' ≼ b'"
      and empty_subsumes: "empty a ⟹ a ≼ a'"
      and empty_mono: "¬ empty a ⟹ a ≼ b ⟹ ¬ empty b"
      and empty_E: "reachable x ⟹ empty x ⟹ E x x' ⟹ empty x'"
      and F_mono: "a ≼ a' ⟹ F a ⟹ F a'"
begin

  sublocale preorder "(≼)" "(≺)"
    by standard (auto simp: subsumes_strictly_def intro: trans)

  sublocale Search_Space_Nodes_Empty E a⇩₀ F "(≼)" reachable empty
    including graph_automation
    by standard
      (auto intro: trans empty_subsumes dest: empty_mono empty_E F_mono, auto 4 4 dest: mono)

end (* Search Space *)

locale Search_Space_finite = Search_Space +
  assumes finite_reachable: "finite {a. reachable a ∧ ¬ empty a}"

locale Search_Space_finite_strict = Search_Space +
  assumes finite_reachable: "finite {a. reachable a}"

sublocale Search_Space_finite_strict ⊆ Search_Space_finite
  by standard (auto simp: finite_reachable)

locale Search_Space' = Search_Space +
  assumes final_non_empty: "F a ⟹ ¬ empty a"

locale Search_Space'_finite = Search_Space' + Search_Space_finite

locale Search_Space''_Defs = Search_Space_Defs_Empty +
  fixes subsumes' :: "'a ⇒ 'a ⇒ bool" (infix "⊴" 50) ― ‹Subsumption preorder›

locale Search_Space''_pre = Search_Space''_Defs +
  assumes empty_subsumes': "¬ empty a ⟹ a ≼ b ⟷ a ⊴ b"

locale Search_Space''_start = Search_Space''_pre +
  assumes start_non_empty [simp]: "¬ empty a⇩₀"

locale Search_Space'' = Search_Space''_pre + Search_Space'

locale Search_Space''_finite = Search_Space'' + Search_Space_finite

sublocale Search_Space''_finite ⊆ Search_Space'_finite ..

locale Search_Space''_finite_strict = Search_Space'' + Search_Space_finite_strict

locale Search_Space_Key_Defs =
  Search_Space''_Defs E for E :: "'v ⇒ 'v ⇒ bool" +
  fixes key :: "'v ⇒ 'k"

locale Search_Space_Key =
  Search_Space_Key_Defs + Search_Space'' +
  assumes subsumes_key[intro, simp]: "a ⊴ b ⟹ key a = key b"

locale Worklist0_Defs = Search_Space_Defs +
  fixes succs :: "'a ⇒ 'a list"

locale Worklist0 = Worklist0_Defs + Search_Space +
  assumes succs_correct: "reachable a ⟹ set (succs a) = Collect (E a)"

locale Worklist1_Defs = Worklist0_Defs + Search_Space_Defs_Empty

locale Worklist1 = Worklist1_Defs + Worklist0

locale Worklist2_Defs = Worklist1_Defs + Search_Space''_Defs

locale Worklist2 = Worklist2_Defs + Worklist1 + Search_Space''_pre + Search_Space

locale Worklist3_Defs = Worklist2_Defs +
  fixes F' :: "'a ⇒ bool"

locale Worklist3 = Worklist3_Defs + Worklist2 +
  assumes F_split: "F a ⟷ ¬ empty a ∧ F' a"

locale Worklist4 = Worklist3 + Search_Space''

locale Worklist_Map_Defs = Search_Space_Key_Defs + Worklist2_Defs

locale Worklist_Map =
  Worklist_Map_Defs + Search_Space_Key + Worklist2

locale Worklist_Map2_Defs = Worklist_Map_Defs + Worklist3_Defs

locale Worklist_Map2 = Worklist_Map2_Defs + Worklist_Map + Worklist3

locale Worklist_Map2_finite = Worklist_Map2 + Search_Space_finite

sublocale Worklist_Map2_finite ⊆ Search_Space''_finite ..

locale Worklist4_Impl_Defs = Worklist3_Defs +
  fixes A :: "'a ⇒ 'ai ⇒ assn"
  fixes succsi :: "'ai ⇒ 'ai list Heap"
  fixes a⇩₀i :: "'ai Heap"
  fixes Fi :: "'ai ⇒ bool Heap"
  fixes Lei :: "'ai ⇒ 'ai ⇒ bool Heap"
  fixes emptyi :: "'ai ⇒ bool Heap"

locale Worklist4_Impl = Worklist4_Impl_Defs + Worklist4 +
  ― ‹This is the easy variant: Operations cannot depend on additional heap.›
  assumes [sepref_fr_rules]: "(uncurry0 a⇩₀i, uncurry0 (RETURN (PR_CONST a⇩₀))) ∈ unit_assn⇧^k →⇩_a A"
  assumes [sepref_fr_rules]: "(Fi,RETURN o PR_CONST F') ∈ A⇧^k →⇩_a bool_assn"
  assumes [sepref_fr_rules]: "(uncurry Lei,uncurry (RETURN oo PR_CONST (⊴))) ∈ A⇧^k *⇩_a A⇧^k →⇩_a bool_assn"
  assumes [sepref_fr_rules]: "(succsi,RETURN o PR_CONST succs) ∈ A⇧^k →⇩_a list_assn A"
  assumes [sepref_fr_rules]: "(emptyi,RETURN o PR_CONST empty) ∈ A⇧^k →⇩_a bool_assn"

locale Worklist4_Impl_finite_strict = Worklist4_Impl + Search_Space_finite_strict

sublocale Worklist4_Impl_finite_strict ⊆ Search_Space''_finite_strict ..

locale Worklist_Map2_Impl_Defs =
  Worklist4_Impl_Defs _ _ _ _ _ _ _ _ A + Worklist_Map2_Defs a⇩₀ _ _ _ _ _ key
  for A :: "'a ⇒ 'ai :: {heap} ⇒ _" and key :: "'a ⇒ 'k" +
  fixes keyi :: "'ai ⇒ 'ki :: {hashable, heap} Heap"
  fixes copyi :: "'ai ⇒ 'ai Heap"
  fixes tracei :: "string ⇒ 'ai ⇒ unit Heap"

end (* Theory *)