Theory Routed_Context_Unit

theory Routed_Context_Unit
  imports Routed_Context
begin

section ‹The monovariant context as a routed-context instance›

text ‹
  Every other \<^locale>‹routed_context› instance (call-string, entry-state)
  routes to a non-trivial context. This theory checks the routed-context abstraction
  also admits the degenerate case a context-insensitive analysis needs: exactly one
  context, chosen the same way at every call, carrying no history and no dependence on
  the abstract state. ‹route_unit› is that routing function; nothing else
  about \<^locale>‹routed_context› changes.

  The context-insensitive analysis is the routed analysis registered at this routing
  function, exactly as the call-string and entry-state analyses are registered at
  theirs; nothing here is a second analysis. What this theory adds is the collapse at
  the end: at the unit context the activation-indexed collecting semantics is
  \<^const>‹node_collect›.
›

subsection ‹Unit routing›

text ‹
  ‹route_unit› ignores every argument and always chooses the sole context ‹()›: no
  call-site history, no dependence on the caller's abstract state, no sentinel encoding.
  ‹enterc_unit› is its trace-semantic counterpart; its graph
  ‹context_policy_of_fun enterc_unit› instantiates
  \<^locale>‹routed_context›'s ‹adm› parameter. The two are definitionally
  the same constant function, so ‹routing_adequate›'s routing agreement holds
  independently of any call edge, solved state, or concrete store.
›

definition route_unit :: "pp ⇒ unit ⇒ 'D ⇒ call_action ⇒ unit" where
  [simp]: "route_unit u ctx d ca = ()"

definition enterc_unit :: "cfg_node ⇒ unit ⇒ store ⇒ unit" where
  [simp]: "enterc_unit u ctx s = ()"

text ‹
  The unit context never filters a trace: every valid activation trace carries the one context
  \<^term>‹()›, so \<^const>‹activation_collect›'s context conjunct holds for every trace
  reaching ‹v› and the two collectors coincide. Domain-generic: no domain-specific fact is
  used, so every \<^typ>‹unit›-context routed producer (Sign, Interval, ...) cites this one
  lemma rather than re-deriving it.
›

lemma activation_collect_unit_eq_node_collect:
  "𝒜⇘𝒢,context_policy_of_fun enterc_unit,(),g,S⇙ v () = 𝒞⇘𝒢,g,S⇙ v"
  unfolding activation_collect_of_fun node_collect_def by simp

end