Theory Worklist_Locales

section ‹Preliminaries›

theory Worklist_Locales
  imports Refine_Imperative_HOL.Sepref Collections.HashCode Timed_Automata.Graphs
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 a0 :: 'a                ― ‹Start state›
    and F :: "'a  bool"      ― ‹Final states›
    and subsumes :: "'a  'a  bool" (infix  50) ― ‹Subsumption preorder›
begin

  sublocale Graph_Start_Defs E a0 .

  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" a0 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 a0 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 a0"

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 a0i :: "'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 a0i, uncurry0 (RETURN (PR_CONST a0)))  unit_assnk a A"
  assumes [sepref_fr_rules]: "(Fi,RETURN o PR_CONST F')  Ak a bool_assn"
  assumes [sepref_fr_rules]: "(uncurry Lei,uncurry (RETURN oo PR_CONST (⊴)))  Ak *a Ak a bool_assn"
  assumes [sepref_fr_rules]: "(succsi,RETURN o PR_CONST succs)  Ak a list_assn A"
  assumes [sepref_fr_rules]: "(emptyi,RETURN o PR_CONST empty)  Ak 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 a0 _ _ _ _ _ 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 *)