Theory Strategy_Tree_Pair

theory Strategy_Tree_Pair
  imports Strategy_Tree_Side_Buffering
begin

section ‹A right-hand side as a pair›

text ‹
  A side-effecting right-hand side is often presented as a function from a valuation to a
  pair: the contributions it publishes, a partial map from unknowns to values, and its own
  value. A strategy tree evaluates to the same pair. The second component is
  \<^const>‹traverse_rhs›; the first is \<^const>‹sides_of_rhs› restricted to the keys
  \<^const>‹side_path› visits, so a key that receives only ‹⊥› stays in the domain and
  a key that receives nothing does not. Both components come from the existing evaluators.
›

definition rhs_sides ::
  "('x,'g,'d::bounded_semilattice_sup_bot) strategy_tree ⇒ ('x + 'g ⇒ 'd) ⇒ 'x + 'g ⇀ 'd"
where
  "rhs_sides t σ = (Some ∘ sides_of_rhs t σ) |` (Inr ` set (side_path σ t))"

definition rhs_pair ::
  "('x,'g,'d::bounded_semilattice_sup_bot) strategy_tree ⇒ ('x + 'g ⇒ 'd)
     ⇒ ('x + 'g ⇀ 'd) × 'd"
where
  "rhs_pair t σ = (rhs_sides t σ, traverse_rhs t σ)"

subsection ‹The partial map loses nothing›

text ‹Off the visited keys \<^const>‹sides_of_rhs› is ‹⊥›, so reading the map back with \<^const>‹mlup› recovers it.›

lemma sides_of_rhs_Inl [simp]: "sides_of_rhs t σ (Inl u) = ⊥"
  by (induction t) (simp_all add: Let_def)

lemma sides_of_rhs_off_path:
  "g ∉ set (side_path σ t) ⟹ sides_of_rhs t σ (Inr g) = ⊥"
  by (induction t) (auto simp: Let_def)

lemma rhs_sides_apply:
  "rhs_sides t σ z =
     (if z ∈ Inr ` set (side_path σ t) then Some (sides_of_rhs t σ z) else None)"
  by (simp add: rhs_sides_def restrict_map_def)

lemma dom_rhs_sides: "dom (rhs_sides t σ) = Inr ` set (side_path σ t)"
  by (auto simp: dom_def rhs_sides_apply)

text ‹Side effects only reach global unknowns; a local unknown is never in the domain.›

lemma rhs_sides_Inl [simp]: "rhs_sides t σ (Inl u) = None"
  by (auto simp: rhs_sides_apply)

lemma mlup_rhs_sides: "mlup (rhs_sides t σ) = sides_of_rhs t σ"
proof
  fix z
  show "mlup (rhs_sides t σ) z = sides_of_rhs t σ z"
    by (cases z) (auto simp: mlup_def rhs_sides_apply sides_of_rhs_off_path image_iff)
qed

text ‹
  Several side effects to one unknown appear once in the domain, with the join of their values,
  in the order of the traversal.
›

lemma rhs_sides_Side:
  "rhs_sides (Side g d t) σ = (rhs_sides t σ)(Inr g ↦ mlup (rhs_sides t σ) (Inr g) ⊔ d)"
  by (rule ext) (auto simp: mlup_rhs_sides rhs_sides_apply Let_def)

lemma rhs_pair_two_sides:
  "rhs_pair (Side g a (Side g b (Answer d))) σ = ([Inr g ↦ b ⊔ a], d)"
  unfolding rhs_pair_def by (auto simp: rhs_sides_apply Let_def intro!: ext)

subsection ‹The certificate in pair form›

text ‹A side map is below a valuation exactly when every contribution it publishes is below its target.›

lemma sides_of_rhs_le_iff_rhs_sides:
  "sides_of_rhs t σ ≤ σ ⟷ (∀z d. rhs_sides t σ z = Some d ⟶ d ≤ σ z)"
proof
  assume "sides_of_rhs t σ ≤ σ"
  then show "∀z d. rhs_sides t σ z = Some d ⟶ d ≤ σ z"
    by (auto simp: rhs_sides_apply le_fun_def)
next
  assume bound: "∀z d. rhs_sides t σ z = Some d ⟶ d ≤ σ z"
  show "sides_of_rhs t σ ≤ σ"
  proof (rule le_funI)
    fix z
    show "sides_of_rhs t σ z ≤ σ z"
    proof (cases "z ∈ Inr ` set (side_path σ t)")
      case True
      then show ?thesis
        using bound by (simp add: rhs_sides_apply)
    next
      case False
      then have "sides_of_rhs t σ z = ⊥"
        by (cases z) (auto simp: sides_of_rhs_off_path image_iff)
      then show ?thesis
        by simp
    qed
  qed
qed

text ‹
  \<^const>‹part_post_solution› with its local and side bounds stated on the pair: the
  value is below the unknown, and every published contribution is below its target. The
  bounds constrain the side-effect targets although they are global unknowns outside
  ‹vars›, and say nothing about unknowns outside ‹vars› that the solve never reached.
›

theorem part_post_solution_iff_rhs_pair:
  "part_post_solution T x σ vars ⟷
     x ∈ vars ∧ (∀u ∈ vars. dep⇩L T σ u ⊆ vars ∧
       (case rhs_pair (T u) σ of (ρ, d) ⇒
          d ≤ σ (Inl u) ∧ (∀z d'. ρ z = Some d' ⟶ d' ≤ σ z)))"
  unfolding rhs_pair_def by (simp add: sides_of_rhs_le_iff_rhs_sides)

end