Theory Greedy_Step_Spec

theory Greedy_Step_Spec
  imports
    "../Algorithms/Greedy_Submodular_Construct"
begin

text ‹
  Step-specification interface for greedy-style algorithms.

  The main construction locale is ‹Greedy_Setup›. The following locale is an
  intentionally thin named view of this setup, using the name ‹select› for an
  oracle that chooses a maximum-marginal-gain element from every finite
  non-empty candidate set. This keeps later corollaries independent of the
  concrete choice-based oracle used for the basic greedy construction.
›

locale Greedy_Step_Oracle =
  Greedy_Setup V f k select
  for V :: "'a set"
    and f :: "'a set ⇒ real"
    and k :: nat
    and select :: "'a set ⇒ 'a set ⇒ 'a"
begin

end

end