Theory Strategy_Tree_Program

theory Strategy_Tree_Program
  imports "TD.Basics_side" "HOL-Library.Monad_Syntax"
begin

section ‹A typed frontend over the homogeneous vendor tree›

text ‹
  ‹strategy_tree› fixes query results and terminal answers to the same
  carrier ‹'d› and therefore does not support a polymorphic bind.
  ‹strategy_program› supplies a continuation-based typed interface: a
  program may produce any result type ‹'a› while its generated vendor tree
  continues to use ‹'d› for solver values and contributions.
  ‹sp_compile_with› encodes the final result into ‹'d› and produces the vendor
  tree consumed by the solver.
›

type_synonym ('x,'g,'d,'a) strategy_program =
  "('a ⇒ ('x,'g,'d) strategy_tree) ⇒ ('x,'g,'d) strategy_tree"

definition sp_return :: "'a ⇒ ('x,'g,'d,'a) strategy_program" where
  "sp_return a k = k a"

definition sp_bind ::
  "('x,'g,'d,'a) strategy_program
   ⇒ ('a ⇒ ('x,'g,'d,'b) strategy_program)
   ⇒ ('x,'g,'d,'b) strategy_program" where
  "sp_bind m f k = m (λv. f v k)"

definition sp_read_local :: "'x ⇒ ('x,'g,'d,'d) strategy_program" where
  "sp_read_local x k = QueryL x k"

definition sp_read_global :: "'g ⇒ ('x,'g,'d,'d) strategy_program" where
  "sp_read_global g k = QueryG g k"

definition sp_publish :: "'g ⇒ 'd ⇒ ('x,'g,'d,unit) strategy_program" where
  "sp_publish g d k = Side g d (k ())"

text ‹
  ‹sp_read_at› reads an unknown in the solver's combined address space
  \<^typ>‹'x + 'g›, dispatching \<^const>‹Inl› to ‹sp_read_local› and \<^const>‹Inr› to
  ‹sp_read_global› instead of fixing the constructor at the call site.
›

fun sp_read_at :: "'x + 'g ⇒ ('x,'g,'d,'d) strategy_program" where
  "sp_read_at (Inl x) = sp_read_local x"
| "sp_read_at (Inr g) = sp_read_global g"

adhoc_overloading Monad_Syntax.bind == sp_bind

text ‹
  ‹sp_read_local›/‹sp_read_global›/‹sp_publish› build a program one effect at a time.
  ‹sp_lift_tree› instead embeds an already-built vendor tree -- the shape a
  backend combinator produces by folding several contribution trees into one
  -- as the program that runs it and continues, by recursing over the tree's
  own constructors directly: an ‹Answer› becomes a pure result, a
  ‹QueryL›/‹QueryG› becomes a read continuing into the lifted subtree, a
  ‹Side› becomes a published contribution continuing into the lifted
  subtree. Defined directly against the constructors, its primitive-recursion
  equations are already the normal form needed by proofs about vendor trees.
›

primrec sp_lift_tree :: "('x,'g,'d) strategy_tree ⇒ ('x,'g,'d,'d) strategy_program" where
  "sp_lift_tree (Answer d)   k = k d"
| "sp_lift_tree (QueryL x f) k = QueryL x (λd. sp_lift_tree (f d) k)"
| "sp_lift_tree (QueryG g f) k = QueryG g (λd. sp_lift_tree (f d) k)"
| "sp_lift_tree (Side g d t) k = Side g d (sp_lift_tree t k)"

lemma traverse_rhs_sp_lift_tree [simp]:
  "traverse_rhs (sp_lift_tree t k) σ = traverse_rhs (k (traverse_rhs t σ)) σ"
  by (induction t arbitrary: k) (auto intro: rangeI)

lemma dep_aux_sp_lift_tree [simp]:
  "dep_aux σ (sp_lift_tree t k) = dep_aux σ t ∪ dep_aux σ (k (traverse_rhs t σ))"
  by (induction t arbitrary: k) (auto intro: rangeI)

lemma sides_of_rhs_sp_lift_tree [simp]:
  fixes t :: "('x, 'g, 'd::bounded_semilattice_sup_bot) strategy_tree"
  shows "sides_of_rhs (sp_lift_tree t k) σ
         = sides_of_rhs t σ ⊔ sides_of_rhs (k (traverse_rhs t σ)) σ"
  by (induction t arbitrary: k) (auto simp: Let_def sup_fun_def fun_upd_def ac_simps intro: rangeI)

text ‹
  ‹traverse_rhs_sp_lift_tree_mono›: environment-monotonicity of the answer
  \<^const>‹sp_lift_tree› produces, not of its dependency set -- if ‹t› is
  monotone in the environment, every continuation ‹k v› is monotone in the
  environment, and ‹k› is monotone in the value it receives, then
  ‹sp_lift_tree t k› is monotone in the environment.
›

lemma traverse_rhs_sp_lift_tree_mono:
  fixes t :: "('x, 'g, 'd::{order,bot}) strategy_tree"
  assumes t_mono:
    "⋀σ1 σ2. σ1 ≤ σ2 ⟹ traverse_rhs t σ1 ≤ traverse_rhs t σ2"
  assumes k_mono_env:
    "⋀v σ1 σ2. σ1 ≤ σ2 ⟹ traverse_rhs (k v) σ1 ≤ traverse_rhs (k v) σ2"
  assumes k_mono_val:
    "⋀σ v1 v2. v1 ≤ v2 ⟹ traverse_rhs (k v1) σ ≤ traverse_rhs (k v2) σ"
  assumes le: "σ1 ≤ σ2"
  shows "traverse_rhs (sp_lift_tree t k) σ1 ≤ traverse_rhs (sp_lift_tree t k) σ2"
proof -
  have "traverse_rhs (k (traverse_rhs t σ1)) σ1
      ≤ traverse_rhs (k (traverse_rhs t σ1)) σ2"
    by (rule k_mono_env[OF le])
  also have "…
      ≤ traverse_rhs (k (traverse_rhs t σ2)) σ2"
    by (rule k_mono_val[OF t_mono[OF le]])
  finally show ?thesis
    by simp
qed

text ‹
  \<^const>‹mono_tree_deps› gives the generally applicable composition rule: the
  continuation may query more unknowns as its received value grows.
  \<^const>‹env_indep_deps› is also preserved, under the stronger condition that
  the continuation's dependency set is independent of both its argument and
  the environment.
›

text ‹
  ‹sp_compile› only accepts a program whose answer is already ‹'d›.
  ‹sp_compile_with encode› generalizes that to any ‹'a›, packing the final
  answer through ‹encode›; ‹sp_compile› is its ‹id› specialization.
›

definition sp_compile_with ::
  "('a ⇒ 'd) ⇒ ('x,'g,'d,'a) strategy_program ⇒ ('x,'g,'d) strategy_tree" where
  "sp_compile_with encode p = p (Answer o encode)"

definition sp_compile :: "('x,'g,'d,'d) strategy_program ⇒ ('x,'g,'d) strategy_tree" where
  "sp_compile p = sp_compile_with id p"

subsection ‹Compiling programs to vendor trees›

text ‹One rewrite per program constructor, each ‹simp›, so compiling a concrete program is
  normalization rather than proof: the simplifier builds the tree from the program's own
  syntax, and a transfer written against the program layer never has to name a tree
  constructor.›
lemma sp_compile_with_bind_read_local [simp]:
  "sp_compile_with encode ((sp_read_local x) ⤜ f) = QueryL x (λd. sp_compile_with encode (f d))"
  by (simp add: sp_compile_with_def sp_bind_def sp_read_local_def)

lemma sp_compile_with_bind_read_global [simp]:
  "sp_compile_with encode ((sp_read_global g) ⤜ f) = QueryG g (λd. sp_compile_with encode (f d))"
  by (simp add: sp_compile_with_def sp_bind_def sp_read_global_def)

lemma sp_compile_with_bind_publish [simp]:
  "sp_compile_with encode ((sp_publish g d) ⤜ f) = Side g d (sp_compile_with encode (f ()))"
  by (simp add: sp_compile_with_def sp_bind_def sp_publish_def)

lemma sp_compile_with_return [simp]:
  "sp_compile_with encode (sp_return a) = Answer (encode a)"
  by (simp add: sp_compile_with_def sp_return_def)

lemma sp_compile_with_read_local [simp]:
  "sp_compile_with encode (sp_read_local x) = QueryL x (Answer o encode)"
  by (simp add: sp_compile_with_def sp_read_local_def)

lemma sp_compile_with_read_global [simp]:
  "sp_compile_with encode (sp_read_global g) = QueryG g (Answer o encode)"
  by (simp add: sp_compile_with_def sp_read_global_def)

lemma sp_compile_with_publish [simp]:
  "sp_compile_with encode (sp_publish g d) = Side g d (Answer (encode ()))"
  by (simp add: sp_compile_with_def sp_publish_def)

lemma sp_compile_with_bind_read_at [simp]:
  "sp_compile_with encode ((sp_read_at src) ⤜ f) =
     (case src of Inl x ⇒ QueryL x (λd. sp_compile_with encode (f d))
                | Inr g ⇒ QueryG g (λd. sp_compile_with encode (f d)))"
  by (cases src) simp_all

lemma sp_compile_with_read_at [simp]:
  "sp_compile_with encode (sp_read_at src) =
     (case src of Inl x ⇒ QueryL x (Answer o encode) | Inr g ⇒ QueryG g (Answer o encode))"
  by (cases src) simp_all

lemma sp_compile_sp_lift_tree [simp]: "sp_compile (sp_lift_tree t) = t"
  by (induction t) (simp_all add: sp_compile_def sp_compile_with_def)

subsection ‹Programs that run their continuation once›

text ‹
  A \<^typ>‹('x,'g,'d,'a) strategy_program› is any function from a continuation to a
  tree, so nothing stops one from ignoring its continuation, or from using it
  twice. Such a program has no semantics the tree vocabulary can describe: what
  it publishes and what it reads would depend on the continuation it is handed.

  ‹sp_wf p› names the programs that do not do this. It says ‹p› commutes with
  grafting: continuing into ‹k› and then grafting ‹h› onto every leaf of the
  result is the same as continuing into ‹k› already grafted. A program that
  dropped its continuation would lose ‹h› on the left and keep it on the
  right; one that used it twice would duplicate the grafting. Everything the
  generator builds runs its continuation once, and this is the condition under
  which asking a program what it publishes is a well-posed question at all.

  Stating it this way rather than as ‹p = sp_lift_tree (sp_compile p)› is what
  lets it apply to a transfer, whose answer type is the analysis' own ‹'dl›
  rather than the solver's ‹'d›: there is no tree whose leaves carry a ‹'dl›,
  so a transfer has no compilation to be recoverable from, but it commutes with
  grafting all the same. For a program that does answer ‹'d› the two agree, which
  is ‹sp_wfD›.
›

lemma sp_lift_tree_sp_lift_tree:
  "sp_lift_tree (sp_lift_tree t g) k = sp_lift_tree t (λv. sp_lift_tree (g v) k)"
  by (induction t) simp_all

definition sp_wf :: "('x,'g,'d,'a) strategy_program ⇒ bool" where
  "sp_wf p ⟷ (∀k h. p (λv. sp_lift_tree (k v) h) = sp_lift_tree (p k) h)"

lemma sp_wfI:
  "(⋀k h. p (λv. sp_lift_tree (k v) h) = sp_lift_tree (p k) h) ⟹ sp_wf p"
  by (simp add: sp_wf_def)

lemma sp_wf_graft:
  "sp_wf p ⟹ p (λv. sp_lift_tree (k v) h) = sp_lift_tree (p k) h"
  by (simp add: sp_wf_def)

text ‹
  The homogeneous reading: a program answering the solver's own value type is
  recoverable from the tree it compiles to. This is the form every consumer
  below uses, and ‹sp_compile› only accepts such a program in the first place.
›

lemma sp_wfD:
  assumes "sp_wf p"
  shows "p k = sp_lift_tree (sp_compile p) k"
  using sp_wf_graft[OF assms, where k = Answer and h = k]
  by (simp add: sp_compile_def sp_compile_with_def)

text ‹Closure under the constructors a generator actually builds with, so a
  well-formedness side condition discharges by ‹simp› at the use site instead
  of being threaded through as a hypothesis.›

lemma sp_wf_lift_tree [intro, simp]: "sp_wf (sp_lift_tree t)"
  by (simp add: sp_wf_def sp_lift_tree_sp_lift_tree)

lemma sp_wf_return [intro, simp]: "sp_wf (sp_return a)"
  by (simp add: sp_wf_def sp_return_def)

lemma sp_wf_read_local [intro, simp]: "sp_wf (sp_read_local x)"
  by (simp add: sp_wf_def sp_read_local_def)

lemma sp_wf_read_global [intro, simp]: "sp_wf (sp_read_global g)"
  by (simp add: sp_wf_def sp_read_global_def)

lemma sp_wf_publish [intro, simp]: "sp_wf (sp_publish g d)"
  by (simp add: sp_wf_def sp_publish_def)

lemma sp_wf_read_at [intro, simp]: "sp_wf (sp_read_at src)"
  by (cases src) simp_all

lemma sp_wf_bind [intro]:
  assumes "sp_wf p" and "⋀v. sp_wf (f v)"
  shows "sp_wf (p ⤜ f)"
proof (rule sp_wfI)
  fix k h
  have "(p ⤜ f) (λv. sp_lift_tree (k v) h) = p (λv. sp_lift_tree (f v k) h)"
    by (simp add: sp_bind_def sp_wf_graft[OF assms(2)])
  also have "… = sp_lift_tree (p (λv. f v k)) h"
    by (rule sp_wf_graft[OF assms(1)])
  finally show "(p ⤜ f) (λv. sp_lift_tree (k v) h) = sp_lift_tree ((p ⤜ f) k) h"
    by (simp add: sp_bind_def)
qed

text ‹
  Post-composing a program's answer with an encoding, so a transfer answering
  ‹'dl› becomes a contribution answering the packed ‹('dl,'dg) dg_state› the
  generator folds. It is \<^const>‹sp_compile_with›'s program-level counterpart:
  compiling it is compiling through the same encoding.
›

definition sp_map ::
  "('a ⇒ 'b) ⇒ ('x,'g,'d,'a) strategy_program ⇒ ('x,'g,'d,'b) strategy_program"
where
  "sp_map e p = (λk. p (λv. k (e v)))"

lemma sp_map_apply [simp]: "sp_map e p k = p (λv. k (e v))"
  by (simp add: sp_map_def)

lemma sp_compile_with_sp_map [simp]:
  "sp_compile_with e' (sp_map e p) = sp_compile_with (e' ∘ e) p"
  by (simp add: sp_map_def sp_compile_with_def comp_def)

lemma sp_compile_sp_map [simp]: "sp_compile (sp_map e p) = sp_compile_with e p"
  by (simp add: sp_compile_def sp_compile_with_def comp_def)

lemma sp_wf_map [intro, simp]: "sp_wf p ⟹ sp_wf (sp_map e p)"
  by (simp add: sp_wf_def)

text ‹
  What a well-formed program answers, publishes and reads, asked of the program
  rather than of a tree. Each is the tree vocabulary applied to its compilation,
  so the three carry over unchanged --- and the point of stating them is that a
  characterization of a combinator can now speak one vocabulary on both sides,
  instead of a program on the left and its contributions' trees on the right.
›

abbreviation traverse_program ::
  "('x,'g,'d::bot,'d) strategy_program ⇒ ('x + 'g ⇒ 'd) ⇒ 'd"
  where "traverse_program p σ ≡ traverse_rhs (sp_compile p) σ"

abbreviation sides_of_program ::
  "('x,'g,'d::bounded_semilattice_sup_bot,'d) strategy_program
   ⇒ ('x + 'g ⇒ 'd) ⇒ 'x + 'g ⇒ 'd"
  where "sides_of_program p σ ≡ sides_of_rhs (sp_compile p) σ"

abbreviation dep_program ::
  "('x + 'g ⇒ 'd::bot) ⇒ ('x,'g,'d,'d) strategy_program ⇒ ('x + 'g) set"
  where "dep_program σ p ≡ dep_aux σ (sp_compile p)"

text ‹Running a well-formed program under any continuation: its own effects
  happen, then the continuation runs on the value it answered.

  Left bare. Their left-hand sides are ‹f (p k) σ› with both ‹p› and ‹k›
  schematic, which is not a higher-order pattern: as ‹simp› rules they match any
  application under one of the three observers and spawn an ‹sp_wf› subgoal for
  it --- including their own right-hand sides, where ‹sides_of_program p σ›
  unfolds to ‹sides_of_rhs (sp_compile p) σ› and matches at ‹?p := sp_compile›.
  Nothing loops while ‹sp_wf sp_compile› is unprovable by the simpset, but that is
  an accident to rely on, so each use cites the rule.›

lemma traverse_rhs_sp_wf:
  assumes "sp_wf p"
  shows "traverse_rhs (p k) σ = traverse_rhs (k (traverse_program p σ)) σ"
  by (subst sp_wfD[OF assms]) simp

lemma dep_aux_sp_wf:
  assumes "sp_wf p"
  shows "dep_aux σ (p k) = dep_program σ p ∪ dep_aux σ (k (traverse_program p σ))"
  by (subst sp_wfD[OF assms]) simp

lemma sides_of_rhs_sp_wf:
  fixes p :: "('x,'g,'d::bounded_semilattice_sup_bot,'d) strategy_program"
  assumes "sp_wf p"
  shows "sides_of_rhs (p k) σ
           = sides_of_program p σ ⊔ sides_of_rhs (k (traverse_program p σ)) σ"
  by (subst sp_wfD[OF assms]) simp

text ‹The three together: what a proof that has just exposed ‹p k› under an
  observer needs, cited as one name.›

lemmas sp_wf_observes = traverse_rhs_sp_wf sides_of_rhs_sp_wf dep_aux_sp_wf

text ‹
  The ‹id›-specialized counterparts of the ‹sp_compile_with_*› equations above,
  stated directly against ‹sp_compile› so a proof reasoning about compiled
  programs does not have to unfold ‹sp_compile_def› at every step.
›

lemma sp_compile_bind_read_local [simp]:
  "sp_compile ((sp_read_local x) ⤜ f) = QueryL x (λd. sp_compile (f d))"
  by (simp add: sp_compile_def)

lemma sp_compile_bind_read_global [simp]:
  "sp_compile ((sp_read_global g) ⤜ f) = QueryG g (λd. sp_compile (f d))"
  by (simp add: sp_compile_def)

lemma sp_compile_bind_publish [simp]:
  "sp_compile ((sp_publish g d) ⤜ f) = Side g d (sp_compile (f ()))"
  by (simp add: sp_compile_def)

lemma sp_compile_return [simp]: "sp_compile (sp_return a) = Answer a"
  by (simp add: sp_compile_def)

lemma sp_compile_read_local [simp]: "sp_compile (sp_read_local x) = QueryL x Answer"
  by (simp add: sp_compile_def)

lemma sp_compile_read_global [simp]: "sp_compile (sp_read_global g) = QueryG g Answer"
  by (simp add: sp_compile_def)

lemma sp_compile_bind_read_at [simp]:
  "sp_compile ((sp_read_at src) ⤜ f) =
     (case src of Inl x ⇒ QueryL x (λd. sp_compile (f d))
                | Inr g ⇒ QueryG g (λd. sp_compile (f d)))"
  by (cases src) simp_all

lemma sp_compile_read_at [simp]:
  "sp_compile (sp_read_at src) =
     (case src of Inl x ⇒ QueryL x Answer | Inr g ⇒ QueryG g Answer)"
  by (cases src) simp_all

text ‹
  Left bare rather than ‹[simp]›: using this equation on arbitrary binds
  exposes ‹m› as a raw CPS function application. The specialized equations
  above preserve the program abstraction and give the simplifier the
  vendor-tree constructors it needs.
›

lemma sp_compile_bind: "sp_compile (m ⤜ f) = m (λx. sp_compile (f x))"
  by (simp add: sp_compile_def sp_compile_with_def sp_bind_def)

lemma sp_compile_with_bind: "sp_compile_with encode (m ⤜ f) = m (λx. sp_compile_with encode (f x))"
  by (simp add: sp_compile_with_def sp_bind_def)

subsection ‹Monad laws›

text ‹The three laws, so a caller may rewrite a program before compiling it and know the
  tree is unchanged.  All three hold by function extensionality alone -- a program is a
  continuation transformer, and ‹⤜› is composition -- so no tree-level reasoning is
  involved.›
lemma sp_bind_sp_return_left [simp]: "(sp_return a) ⤜ f = f a"
  by (rule ext) (simp add: sp_bind_def sp_return_def)

lemma sp_bind_sp_return_right [simp]: "m ⤜ sp_return = m"
  by (rule ext) (simp add: sp_bind_def sp_return_def)

lemma sp_bind_assoc:
  fixes m :: "('x, 'g, 'd, 'a) strategy_program"
    and f :: "'a ⇒ ('x, 'g, 'd, 'b) strategy_program"
    and g :: "'b ⇒ ('x, 'g, 'd, 'c) strategy_program"
  shows "(m ⤜ f) ⤜ g = m ⤜ (λx. f x ⤜ g)"
  by (rule ext) (simp add: sp_bind_def)

end