Theory Strategy_Program_Fold

theory Strategy_Program_Fold
  imports Strategy_Tree_Program
begin

section ‹Folding a right-hand side from contribution programs›

text ‹
  An equation's right-hand side is assembled from a list of contributions ---
  one per incoming contribution, such as an intra predecessor, a call return, or
  a routed activation hook --- joined into one answer. Each contribution is a
  ∗‹program›, not a finished tree: the fold sequences them with ‹⤜›, joining
  each answer into a running accumulator, and the result is again a program.
  Nothing is compiled here. A generator compiles once, at the end, where the
  solver takes over.

  That is why the characterizations below can speak one vocabulary on both
  sides. ‹traverse_program›, ‹sides_of_program› and ‹dep_program› ask a
  contribution the same questions they ask the fold, and each hypothesis
  ‹∀p ∈ set ps. sp_wf p› is what makes asking them of a program well posed at
  all: an arbitrary program may ignore or duplicate its continuation, and then
  what it publishes would depend on what follows it.

  The fold never emits a \<^const>‹Side› itself: a fold of Side-free
  contributions stays Side-free, which is what lets a generator publish once,
  after the whole fold, instead of once per contribution --- several updates to
  one key during a single right-hand-side evaluation otherwise change what the
  vendored solver's per-origin update rule widens against.

  What a caller varies is ∗‹how much of each answer accumulates›. The fold
  therefore takes a projection ‹prj› into the accumulator and an embedding
  ‹emb› back out. At the identity pair the whole answer accumulates. A D/G
  instance instead projects the local half into the accumulator and embeds the
  result as ‹DG d bot›; the global half of a contribution simply does not reach
  the node's answer, and a contribution that has one to share must publish
  it itself through \<^const>‹Side›. Nothing here makes that happen.

  The two parameters are used as a projection and a final embedding, but the
  fold assumes no inverse or homomorphism law relating them. Order preservation
  is required only where it is actually used, by the environment-monotonicity
  results; the publication and dependency characterizations hold for arbitrary
  ‹prj› and ‹emb›.
›

subsection ‹Join-folds over a list›

text ‹
  ‹⨆x←xs. f x› joins ‹f x› over the list ‹xs›; the empty join is
  \<^const>‹bot›. It is built like HOL's \<^const>‹sum_list›: ‹join_list› is the
  list fold of the commutative monoid ‹(⊔, ⊥)›, and the binder maps
  before it folds.
›

context bounded_semilattice_sup_bot
begin

sublocale join_list: comm_monoid_list sup bot
  defines join_list = join_list.F ..

end

open_bundle join_list_syntax
begin

syntax
  "_join_list" :: "pttrn ⇒ 'a list ⇒ 'b ⇒ 'b"
    (‹(‹indent=3 notation=‹binder ⨆››⨆_←_. _)› [0, 51, 10] 10)
syntax_consts
  "_join_list" == join_list
translations
  "⨆x←xs. b" == "CONST join_list (CONST map (λx. b) xs)"

end

text ‹
  Every characterization below states the fold as a list join over
  already-computed values, so its consumers keep needing the same handful of
  facts about that: the seed of a right fold can be moved out, a bound against
  the join is a bound against every element, one element is below the join,
  only the element set matters, a pointwise bound lifts, two lists that agree
  elementwise agree, and an all-\<^const>‹bot› join is \<^const>‹bot›.

  They are collected here, ahead of the fold they serve, rather than restated
  per generator. ‹foldr_sup_seed_swap› is the one with content --- it needs
  only ‹semilattice_sup› --- and ‹foldr_join_list› and ‹foldr_join_seed_out›
  read a right fold with a \<^const>‹bot› or an arbitrary seed as a list join.
›

lemma foldr_sup_seed_swap:
  fixes h :: "'a ⇒ 'b::semilattice_sup"
  shows "foldr (λt acc'. h t ⊔ acc') ts (acc ⊔ x) = x ⊔ foldr (λt acc'. h t ⊔ acc') ts acc"
  by (induction ts arbitrary: acc) (simp_all add: sup_assoc sup_commute sup_left_commute)

lemma foldr_join_list:
  fixes h :: "'a ⇒ 'b::bounded_semilattice_sup_bot"
  shows "foldr (λt acc'. h t ⊔ acc') ts bot = (⨆t←ts. h t)"
  by (induction ts) simp_all

lemma foldr_join_seed_out:
  fixes h :: "'a ⇒ 'b::bounded_semilattice_sup_bot"
  shows "foldr (λt acc'. h t ⊔ acc') ts a = a ⊔ (⨆t←ts. h t)"
  using foldr_sup_seed_swap[of h ts bot a] by (simp add: foldr_join_list)

lemma foldr_sup_le_iff [simp]:
  fixes h :: "'a ⇒ 'b::bounded_semilattice_sup_bot"
  shows "(⨆t←xs. h t) ≤ y ⟷ (∀x ∈ set xs. h x ≤ y)"
  by (induction xs) auto

lemma foldr_sup_member_le [intro]:
  fixes h :: "'a ⇒ 'b::bounded_semilattice_sup_bot"
  assumes "x ∈ set xs"
  shows "h x ≤ (⨆t←xs. h t)"
  using assms by (induction xs) (auto intro: le_supI2)

lemma foldr_sup_mono:
  fixes f g :: "'a ⇒ 'b::bounded_semilattice_sup_bot"
  assumes "⋀x. x ∈ set xs ⟹ f x ≤ g x"
  shows "(⨆t←xs. f t) ≤ (⨆t←xs. g t)"
  using assms by (auto intro: order_trans[OF _ foldr_sup_member_le])

lemma foldr_sup_set_cong:
  fixes h :: "'a ⇒ 'b::bounded_semilattice_sup_bot"
  assumes eq: "set xs = set ys"
  shows "(⨆t←xs. h t) = (⨆t←ys. h t)"
  by (rule order_antisym) (auto simp: eq)

text ‹Two lists whose elements agree under their respective observations have
  the same join. This is what lets a correspondence proof relate two
  generators' contribution lists elementwise instead of reasoning about the
  folds themselves.›

lemma foldr_sup_list_all2_cong:
  fixes f :: "'a ⇒ 'c::bounded_semilattice_sup_bot"
  assumes "list_all2 (λx y. f x = g y) xs ys"
  shows "(⨆x←xs. f x) = (⨆y←ys. g y)"
  using assms by (induction rule: list_all2_induct) simp_all

text ‹The two ways such a correspondence is built and consumed: establishing
  it between two maps over one list, and reading it as an equality of unions.
  Neither mentions a fold, a tree, or a graph.›

lemma list_all2_map_diag:
  "(⋀x. x ∈ set xs ⟹ P (f x) (g x)) ⟹ list_all2 P (map f xs) (map g xs)"
  by (induction xs) simp_all

lemma list_all2_Union_eq:
  assumes "list_all2 (λa b. f a = g b) xs ys"
  shows "(⋃x∈set xs. f x) = (⋃y∈set ys. g y)"
  using assms by (induction rule: list_all2_induct) auto

lemma foldr_sup_bot_of_all_bot:
  fixes L :: "'a list" and h :: "'a ⇒ 'b::bounded_semilattice_sup_bot"
  assumes "⋀x. x ∈ set L ⟹ h x = bot"
  shows "(⨆x←L. h x) = bot"
  using assms by (induction L) simp_all

subsection ‹Folding contributions into one right-hand side›

text ‹Several contribution programs, one right-hand side: run each in list order, join its
  answer into the accumulator, and answer with the accumulator.  ‹prj› and ‹emb› keep the
  fold generic in which part of an answer accumulates -- that is what later lets the D/G
  layer join the local half while the global half travels as a side effect.›

fun fold_rhs_program_projected ::
  "('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ 'b::semilattice_sup
   ⇒ ('k, 'g, 'a, 'a) strategy_program list
   ⇒ ('k, 'g, 'a, 'a) strategy_program"
where
  "fold_rhs_program_projected prj emb acc [] = sp_return (emb acc)"
| "fold_rhs_program_projected prj emb acc (p # ps) =
     do {
       res ← p;
       fold_rhs_program_projected prj emb (acc ⊔ prj res) ps
     }"

text ‹The accumulator read declaratively off a valuation, rather than run.
  Every answer characterization below is stated through it.›

fun fold_acc_projected ::
  "('a::bounded_semilattice_sup_bot ⇒ 'b::semilattice_sup) ⇒ 'b
   ⇒ ('k + 'g ⇒ 'a) ⇒ ('k, 'g, 'a, 'a) strategy_program list ⇒ 'b"
where
  "fold_acc_projected prj acc σ [] = acc"
| "fold_acc_projected prj acc σ (p # ps) =
     fold_acc_projected prj (acc ⊔ prj (traverse_program p σ)) σ ps"

subsection ‹Declarative characterizations›

text ‹
  Contributions are traversed in list order: each answer joins the running
  accumulator before the next program runs. The publication and dependency
  characterizations forget that order, the underlying operation being
  commutative --- a set union for \<^const>‹dep_aux›, a join seeded at ‹bot› for
  \<^const>‹sides_of_rhs› --- and neither sees ‹prj› or ‹emb› at all: what a fold
  publishes and reads is its contributions' business, not its accumulator's.
  That is also why both are independent of the accumulator it starts from.
›

theorem traverse_fold_rhs_program_projected_char:
  assumes "∀p ∈ set ps. sp_wf p"
  shows "traverse_program (fold_rhs_program_projected prj emb acc ps) σ
     = emb (fold_acc_projected prj acc σ ps)"
  using assms
  by (induction ps arbitrary: acc)
     (simp_all add: sp_compile_def sp_compile_with_bind traverse_rhs_sp_wf)

theorem sides_of_program_fold_rhs_program_projected_char:
  fixes ps :: "('x, 'g, 'd::bounded_semilattice_sup_bot, 'd) strategy_program list"
  assumes "∀p ∈ set ps. sp_wf p"
  shows "sides_of_program (fold_rhs_program_projected prj emb acc ps) σ z
     = (⨆p←ps. sides_of_program p σ z)"
  using assms
  by (induction ps arbitrary: acc)
     (auto simp add: sp_compile_def sp_compile_with_bind sides_of_rhs_sp_wf traverse_rhs_sp_wf)

theorem dep_program_fold_rhs_program_projected_char:
  assumes "∀p ∈ set ps. sp_wf p"
  shows "dep_program σ (fold_rhs_program_projected prj emb acc ps)
     = (⋃p∈set ps. dep_program σ p)"
  using assms
  by (induction ps arbitrary: acc)
     (auto simp add: sp_compile_def sp_compile_with_bind dep_aux_sp_wf traverse_rhs_sp_wf)

lemma fold_acc_projected_as_foldr:
  fixes prj :: "'a::bounded_semilattice_sup_bot ⇒ 'b::bounded_semilattice_sup_bot"
  shows "fold_acc_projected prj acc σ ps
           = acc ⊔ (⨆p←ps. prj (traverse_program p σ))"
  by (induction ps arbitrary: acc) (simp_all add: sup_assoc)

lemma fold_acc_projected_acc_mono:
  fixes prj :: "'a::bounded_semilattice_sup_bot ⇒ 'b::bounded_semilattice_sup_bot"
  assumes "acc1 ≤ acc2"
  shows "fold_acc_projected prj acc1 σ ts ≤ fold_acc_projected prj acc2 σ ts"
  using assms by (simp add: fold_acc_projected_as_foldr le_supI1)

text ‹
  Monotonicity in the ∗‹environment› rather than the accumulator. This is
  where ‹prj› and ‹emb› stop being arbitrary: a fold inherits its
  contributions' monotonicity only if the two also preserve order. Publications
  and dependencies need no such hypothesis, since neither passes through them.
›

lemma fold_acc_projected_env_mono:
  fixes prj :: "'a::bounded_semilattice_sup_bot ⇒ 'b::bounded_semilattice_sup_bot"
  assumes prj_mono: "mono prj"
    and progs_mono: "⋀p. p ∈ set ps ⟹ traverse_program p σ1 ≤ traverse_program p σ2"
  shows "fold_acc_projected prj acc σ1 ps ≤ fold_acc_projected prj acc σ2 ps"
  unfolding fold_acc_projected_as_foldr
  by (rule sup_mono[OF order_refl])
     (rule foldr_sup_mono, rule monoD[OF prj_mono, OF progs_mono])

lemma traverse_fold_rhs_program_projected_mono:
  fixes prj :: "'a::bounded_semilattice_sup_bot ⇒ 'b::bounded_semilattice_sup_bot"
  assumes wf: "∀p ∈ set ps. sp_wf p"
    and prj_mono: "mono prj"
    and emb_mono: "mono emb"
    and progs_mono: "⋀p. p ∈ set ps ⟹ traverse_program p σ1 ≤ traverse_program p σ2"
  shows "traverse_program (fold_rhs_program_projected prj emb acc ps) σ1
       ≤ traverse_program (fold_rhs_program_projected prj emb acc ps) σ2"
  unfolding traverse_fold_rhs_program_projected_char[OF wf]
  by (rule monoD[OF emb_mono])
     (rule fold_acc_projected_env_mono[OF prj_mono progs_mono])

lemma sides_of_program_fold_rhs_program_projected_mono:
  fixes ps :: "('x, 'g, 'd::bounded_semilattice_sup_bot, 'd) strategy_program list"
  assumes wf: "∀p ∈ set ps. sp_wf p"
    and progs_mono: "⋀p. p ∈ set ps ⟹ sides_of_program p σ1 ≤ sides_of_program p σ2"
  shows "sides_of_program (fold_rhs_program_projected prj emb acc ps) σ1
       ≤ sides_of_program (fold_rhs_program_projected prj emb acc ps) σ2"
  unfolding le_fun_def sides_of_program_fold_rhs_program_projected_char[OF wf]
  using progs_mono
  by (fastforce simp: le_fun_def
        intro: order_trans[OF _ foldr_sup_member_le])

lemma sides_of_program_fold_rhs_program_projected_acc_indep:
  fixes ps :: "('x, 'g, 'd::bounded_semilattice_sup_bot, 'd) strategy_program list"
  assumes wf: "∀p ∈ set ps. sp_wf p"
  shows "sides_of_program (fold_rhs_program_projected prj emb acc1 ps) σ
       = sides_of_program (fold_rhs_program_projected prj emb acc2 ps) σ"
  by (simp add: fun_eq_iff sides_of_program_fold_rhs_program_projected_char[OF wf])

lemma dep_program_fold_rhs_program_projected_acc_indep:
  assumes wf: "∀p ∈ set ps. sp_wf p"
  shows "dep_program σ (fold_rhs_program_projected prj emb acc1 ps)
     = dep_program σ (fold_rhs_program_projected prj emb acc2 ps)"
  by (simp add: dep_program_fold_rhs_program_projected_char[OF wf])

subsection ‹Accumulating the whole answer›

text ‹The identity instance: nothing is projected away, so the accumulator has
  the answer type and every contribution joins into the node's answer whole.›

lemma sp_wf_fold_rhs_program_projected [intro]:
  "∀p ∈ set ps. sp_wf p ⟹ sp_wf (fold_rhs_program_projected prj emb acc ps)"
  by (induction ps arbitrary: acc) auto

definition fold_rhs_program ::
  "'a::semilattice_sup
   ⇒ ('k, 'g, 'a, 'a) strategy_program list
   ⇒ ('k, 'g, 'a, 'a) strategy_program"
where
  "fold_rhs_program acc ps = fold_rhs_program_projected id id acc ps"

lemma sp_wf_fold_rhs_program [intro]:
  "∀p ∈ set ps. sp_wf p ⟹ sp_wf (fold_rhs_program acc ps)"
  unfolding fold_rhs_program_def by (rule sp_wf_fold_rhs_program_projected)

lemma fold_rhs_program_simps [simp, code]:
  "fold_rhs_program acc [] = sp_return acc"
  "fold_rhs_program acc (p # ps) =
     do { res ← p; fold_rhs_program (acc ⊔ res) ps }"
  by (simp_all add: fold_rhs_program_def)

text ‹The answer as a right fold. \<^const>‹fold_rhs_program› threads the
  accumulator in evaluation order, which is a left fold;
  proofs about a node's contributions are usually already phrased as a right
  fold, and \<^const>‹traverse_rhs› only ever joins, so the two agree.›

theorem traverse_fold_rhs_program_char_foldr:
  assumes "∀p ∈ set ps. sp_wf p"
  shows "traverse_program (fold_rhs_program acc ps) σ
     = foldr (λp acc'. traverse_program p σ ⊔ acc') ps acc"
  using assms
  by (induction ps arbitrary: acc)
     (simp_all add: sp_compile_def sp_compile_with_bind foldr_sup_seed_swap
        traverse_rhs_sp_wf)

theorem sides_of_program_fold_rhs_program_char:
  fixes ps :: "('x,'g,'d::bounded_semilattice_sup_bot,'d) strategy_program list"
  assumes wf: "∀p ∈ set ps. sp_wf p"
  shows "sides_of_program (fold_rhs_program acc ps) σ z
     = (⨆p←ps. sides_of_program p σ z)"
  unfolding fold_rhs_program_def
  by (rule sides_of_program_fold_rhs_program_projected_char[OF wf])

theorem dep_program_fold_rhs_program_char:
  assumes wf: "∀p ∈ set ps. sp_wf p"
  shows "dep_program σ (fold_rhs_program acc ps) = (⋃p∈set ps. dep_program σ p)"
  unfolding fold_rhs_program_def
  by (rule dep_program_fold_rhs_program_projected_char[OF wf])


subsection ‹Dependency-property preservation›

text ‹
  A fold of programs whose query set is (respectively environment-independent,
  monotone in the environment) is itself environment-independent (monotone) --
  the list-level analogue of \<^const>‹env_indep_deps›/\<^const>‹mono_tree_deps›'s
  own single-tree closure facts, and what lets a generator's whole-node
  dependency obligation reduce to a per-hook one.

  Both read straight off ‹dep_program_fold_rhs_program_projected_char›: a fold's
  dependencies are the union of its contributions', so whatever closure
  property each contribution has, the union inherits.
›

lemma env_indep_deps_fold_rhs_program_projected:
  assumes wf: "∀p ∈ set ps. sp_wf p"
    and "⋀p. p ∈ set ps ⟹ env_indep_deps (sp_compile p)"
  shows "env_indep_deps (sp_compile (fold_rhs_program_projected prj emb acc ps))"
  using assms
  unfolding env_indep_deps_def
  by (auto simp add: dep_program_fold_rhs_program_projected_char[OF wf]; blast)

lemma mono_tree_deps_fold_rhs_program_projected:
  assumes wf: "∀p ∈ set ps. sp_wf p"
    and "⋀p. p ∈ set ps ⟹ mono_tree_deps (sp_compile p)"
  shows "mono_tree_deps (sp_compile (fold_rhs_program_projected prj emb acc ps))"
  using assms
  unfolding mono_tree_deps_def
  by (fastforce simp: dep_program_fold_rhs_program_projected_char[OF wf])

end