Theory TD.Basics_side

theory Basics_side
  imports Main "HOL-Library.Finite_Map"
begin

unbundle lattice_syntax


subsection ‹Auxiliary Lemmas for Default Maps›

text‹The solver maintains a solver state to implement optimizations based on self-observation.
  Among the data structures for the solver state are maps that return a default value for
  non-existing keys. In the following, we define some helper functions and lemmas for these.›

definition fmlookup_default where
  "fmlookup_default m d x = (case fmlookup m x of Some v ⇒ v | None ⇒ d)"

abbreviation slookup where
  "slookup infl x ≡ set (fmlookup_default infl [] x)"

definition mlup where
  "mlup σ x ≡ case σ x of Some v ⇒ v | None ⇒ ⊥"

definition fminsert where
  "fminsert infl x y = fmupd x (y # (fmlookup_default infl [] x)) infl"

lemma set_fmlookup_default_cases:
  assumes "y ∈ slookup infl x"
  obtains (1) xs where "fmlookup infl x = Some xs" and "y ∈ set xs"
  using assms that unfolding fmlookup_default_def
  by (cases "fmlookup infl x"; auto)

lemma notin_fmlookup_default_cases:
  assumes "y ∉ slookup infl x"
  obtains (1) xs where "fmlookup infl x = Some xs" and "y ∉ set xs"
  | (2) "fmlookup infl x = None"
  using assms that unfolding fmlookup_default_def
  by (cases "fmlookup infl x"; auto)

lemma slookup_helper[simp]:
  assumes "fmlookup m x = Some ys"
    and "y ∈ set ys"
  shows "y ∈ slookup m x"
  using assms(1,2) notin_fmlookup_default_cases by force

lemma lookup_implies_mlup:
  assumes "σ x = σ' x'"
  shows "mlup σ x = mlup σ' x'"
  using assms
  unfolding mlup_def fmlookup_default_def
  by auto

lemma fmlookup_fminsert:
  assumes "fmlookup_default infl [] x = xs"
  shows "fmlookup (fminsert infl x y) x = Some (y # xs)"
proof(cases "fmlookup infl x")
  case None
  then show ?thesis using assms unfolding fmlookup_default_def fminsert_def by auto
next
  case (Some a)
  then show ?thesis using assms unfolding fmlookup_default_def fminsert_def by auto
qed

lemma fmlookup_fminsert':
  obtains xs ys
  where "fmlookup (fminsert infl x y) x = Some xs"
    and "fmlookup_default infl [] x = ys" and "xs = y # ys"
  using that fmlookup_fminsert
  by fastforce

lemma fmlookup_default_drop_set:
  "fmlookup_default (fmdrop_set A m) [] x = (if x ∉ A then fmlookup_default m [] x else [])"
  by (simp add: fmlookup_default_def)

lemma mlup_eq_mupd_set:
  assumes "x ∉ s"
    and "∀y∈s. mlup σ y = mlup σ' y"
  shows "∀y∈s. mlup σ y = mlup (σ'(x ↦ xd)) y"
  using assms
  by (simp add: mlup_def)

lemma slookup_fminsert_other: "z ≠ x ⟹ slookup (fminsert infl1 x y) z = slookup infl1 z"
  unfolding fminsert_def fmlookup_default_def by auto

lemma slookup_fminsert_same: "slookup (fminsert infl1 x y) x = slookup infl1 x ∪ {y}"
  unfolding fminsert_def fmlookup_default_def by auto

lemma slookup_fminsert: "slookup (fminsert infl x y) z =
  (if x = z then slookup infl x ∪ {y} else slookup infl z)"
  unfolding fminsert_def fmlookup_default_def by auto


subsection ‹Definitions for Strategy Trees with Side Effects›

datatype ('x,'g,'d) strategy_tree = Answer 'd |
  QueryL 'x "'d ⇒ ('x,'g,'d) strategy_tree" |
  QueryG 'g "'d ⇒ ('x,'g,'d) strategy_tree" |
  Side 'g 'd "('x,'g,'d) strategy_tree"

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

primrec dep_aux :: "('x + 'g ⇒ 'd) ⇒ ('x,'g,'d::bot) strategy_tree ⇒ ('x + 'g) set" where
  "dep_aux σ (Answer d) = {}"
| "dep_aux σ (QueryL y g) = insert (Inl y) (dep_aux σ (g (σ (Inl y))))"
| "dep_aux σ (QueryG y g) = insert (Inr y) (dep_aux σ (g (σ (Inr y))))"
| "dep_aux σ (Side y d t) = dep_aux σ t"

definition dep ::
    "('x,'g,'d::order_bot) eqsT ⇒ ('x + 'g ⇒ 'd) ⇒ 'x ⇒ ('x + 'g) set" where
  "dep T sigma x = dep_aux sigma (T x)"

lemma dep_aux_eq:
  assumes "∀y ∈ dep_aux sigma t. sigma y = sigma' y"
  shows "dep_aux sigma t = dep_aux sigma' t"
  using assms
  by (induction t rule: strategy_tree.induct; simp add: dep_aux_def)

lemma dep_eq:
  assumes "∀y ∈ dep T sigma x. sigma y = sigma' y"
  shows "dep T sigma x = dep T sigma' x"
  using assms unfolding dep_def by (rule dep_aux_eq)

definition dep⇩L ::
    "('x,'g,'d::order_bot) eqsT ⇒ ('x + 'g ⇒ 'd) ⇒ 'x ⇒ 'x set" where
  "dep⇩L T sigma x = {l. Inl l ∈ dep T sigma x}"

definition dep_aux⇩L ::
    "('x + 'g ⇒ 'd) ⇒ ('x,'g,'d::order_bot) strategy_tree ⇒ 'x set" where
  "dep_aux⇩L sigma t = {l. Inl l ∈ dep_aux sigma t}"

abbreviation trans_dep⇩L_rel :: "('x,'g,'d::order_bot) eqsT ⇒ ('x + 'g ⇒ 'd) ⇒ ('x × 'x) set" where
  "trans_dep⇩L_rel T sigma ≡ {(u, d). d ∈ dep⇩L T sigma u}⇧+"
abbreviation trans_dep⇩L :: "('x,'g,'d::order_bot) eqsT ⇒ ('x + 'g ⇒ 'd) ⇒ 'x ⇒ 'x set" where
  "trans_dep⇩L T sigma x ≡ {u. (x,u) ∈ trans_dep⇩L_rel T sigma}"

lemma trans_dep⇩L_step:
  "y ∈ dep⇩L T sigma x ⟹ insert y (trans_dep⇩L T sigma y) ⊆ trans_dep⇩L T sigma x"
proof
  fix u
  assume A: "y ∈ dep⇩L T sigma x" "u ∈ insert y (trans_dep⇩L T sigma y)"
  show "u ∈ trans_dep⇩L T sigma x"
    apply (cases "u = y")
    subgoal using A(1) by blast
    subgoal
    proof goal_cases
      case 1
      then have "u ∈ trans_dep⇩L T sigma y" using A(2) by simp
      moreover have "y ∈ trans_dep⇩L T sigma x" using A(1) by blast
      ultimately show ?case by simp
    qed
    done
qed


subsection ‹Subtrees of Strategy Trees›

inductive_set subt_aux ::
    "('x + 'g ⇒ 'd::bot) ⇒ ('x, 'g, 'd) strategy_tree ⇒ ('x, 'g, 'd) strategy_tree set"
    for σ t where
  base: "t ∈ subt_aux σ t"
| step_QueryL: "t' ∈ subt_aux σ t ⟹ t' = QueryL y g ⟹ (g (σ (Inl y))) ∈ subt_aux σ t"
| step_QueryG: "t' ∈ subt_aux σ t ⟹ t' = QueryG y g ⟹ (g (σ (Inr y))) ∈ subt_aux σ t"
| step_Side: "t' ∈ subt_aux σ t ⟹ t' = Side y d t'' ⟹ t'' ∈ subt_aux σ t"

definition subt :: "('x,'g,'d) eqsT ⇒ ('x + 'g ⇒ 'd::bot) ⇒ 'x ⇒
  ('x, 'g, 'd) strategy_tree set" where
  "subt T sigma x = subt_aux sigma (T x)"

lemma subt_of_answer_singleton:
  shows "subt_aux sigma (Answer d) = {Answer d}"
proof (intro set_eqI iffI, goal_cases)
  case (1 x)
  then show ?case by (induction rule: subt_aux.induct; simp)
next
  case (2 x)
  then show ?case by (simp add: subt_aux.base)
qed

lemma subt_transitive:
  assumes "t' ∈ subt_aux sigma t"
  shows "subt_aux sigma t' ⊆ subt_aux sigma t"
proof
  fix τ
  assume "τ ∈ subt_aux sigma t'"
  then show "τ ∈ subt_aux sigma t"
    using assms
    by (induction rule: subt_aux.induct; simp add: subt_aux.step_QueryL subt_aux.step_QueryG
        subt_aux.step_Side)
qed

lemma subt_unfold_QueryL:
  "subt_aux sigma (QueryL x f) = insert (QueryL x f) (subt_aux sigma (f (sigma (Inl x))))"
proof(intro set_eqI iffI, goal_cases)
  case (1 τ)
  then show ?case
    using subt_aux.simps
    by (induction rule: subt_aux.induct; fast)
next
  case (2 τ)
  then show ?case
  proof (elim insertE, goal_cases)
    case 1
    then show ?case
      using subt_aux.base
      by simp
  next
    case 2
    then show ?case
      using subt_transitive[of "f (sigma (Inl x))" sigma "QueryL x f"] subt_aux.base
        subt_aux.step_QueryL
      by fast
  qed
qed

lemma subt_unfold_QueryG:
  "subt_aux sigma (QueryG x f) = insert (QueryG x f) (subt_aux sigma (f (sigma (Inr x))))"
proof(intro set_eqI iffI, goal_cases)
  case (1 τ)
  then show ?case
    using subt_aux.simps
    by (induction rule: subt_aux.induct; fast)
next
  case (2 τ)
  then show ?case
  proof (elim insertE, goal_cases)
    case 1
    then show ?case
      using subt_aux.base
      by simp
  next
    case 2
    then show ?case
      using subt_transitive[of "f (sigma (Inr x))" sigma "QueryG x f"] subt_aux.base
        subt_aux.step_QueryG
      by fast
  qed
qed

lemma subt_unfold_Side:
  shows "subt_aux sigma (Side x d t) = insert (Side x d t) (subt_aux sigma t)"
proof(intro set_eqI iffI, goal_cases)
  case (1 τ)
  then show ?case
    using subt_aux.simps
    apply (induction rule: subt_aux.induct) apply blast apply fast apply blast by fast
next
  case (2 τ)
  then show ?case
  proof (elim insertE, goal_cases)
    case 1
    then show ?case
      using subt_aux.base
      by simp
  next
    case 2
    then show ?case
      using subt_transitive[of t sigma "Side x d t"] subt_aux.base subt_aux.step_Side
      by fast
  qed
qed

lemma subt_unfold_Answer[simp]:
  shows "subt_aux sigma (Answer d) = {Answer d}"
  using subt_of_answer_singleton by blast

lemma subt_unfold:
    "subt_aux sigma t =
      (case t of Answer d ⇒ {Answer d}
      | QueryL x f ⇒ insert (QueryL x f) (subt_aux sigma (f (sigma (Inl x))))
      | QueryG x f ⇒ insert (QueryG x f) (subt_aux sigma (f (sigma (Inr x))))
      | Side x d t ⇒ insert (Side x d t) (subt_aux sigma t))"
  using subt_unfold_Answer subt_unfold_QueryL subt_unfold_QueryG subt_unfold_Side
  by (cases t) fastforce+

lemma subt_implies_dep_locale:
  assumes "QueryL y g ∈ subt_aux σ t"
  shows "Inl y ∈ dep_aux σ t"
  using assms
  by (induction t) (auto simp add: subt_unfold)

lemma subt_implies_dep_globale:
  assumes "QueryG y g ∈ subt_aux σ t"
  shows "Inr y ∈ dep_aux σ t"
  using assms
  by (induction t) (auto simp add: subt_unfold)


subsection ‹Definitions to Describe Correctness›

primrec sides_of_rhs ::
    "('x,'g,'d::bounded_semilattice_sup_bot) strategy_tree ⇒ ('x + 'g ⇒ 'd) ⇒ ('x + 'g ⇒ 'd)"
    where
  "sides_of_rhs (Answer d) sigma = (λ_. ⊥)"
| "sides_of_rhs (QueryL y g) sigma = sides_of_rhs (g (sigma (Inl y))) sigma"
| "sides_of_rhs (QueryG y g) sigma = sides_of_rhs (g (sigma (Inr y))) sigma"
| "sides_of_rhs (Side y d t) sigma = (let m = sides_of_rhs t sigma in m(Inr y := m (Inr y) ⊔ d))"

primrec traverse_rhs :: "('x,'g,'d::bot) strategy_tree ⇒ ('x + 'g ⇒ 'd) ⇒ 'd" where
  "traverse_rhs (Answer d) _ = d" |
  "traverse_rhs (QueryL x f) σ = traverse_rhs (f (σ (Inl x))) σ" |
  "traverse_rhs (QueryG x f) σ = traverse_rhs (f (σ (Inr x))) σ" |
  "traverse_rhs (Side x d t) σ = traverse_rhs t σ"

abbreviation eq :: "('x,'g,'d::bot) eqsT ⇒ 'x ⇒ ('x + 'g ⇒ 'd) ⇒ 'd" where
  "eq T x sigma ≡ traverse_rhs (T x) sigma"

text‹For a partial solution, values in @term{σ} need to subsume the right-hand side evaluation of
     the corresponding unknown as well as the side effects to it. For @term{σ} to be a valid
     partial solution for set X, it also needs to be closed. We define the closedness property
     separately.›

abbreviation eq_equal_sides_subsumed ::
  "('x,'g,'d::bounded_semilattice_sup_bot) eqsT ⇒ ('x + 'g ⇒ 'd) ⇒ 'x set ⇒ bool"
  where
  "eq_equal_sides_subsumed T sigma vars ≡ (∀x ∈ vars.
    eq T x sigma = sigma (Inl x) ∧ sides_of_rhs (T x) sigma ≤ sigma)"

abbreviation part_solution ::
  "('x,'g,'d::bounded_semilattice_sup_bot) eqsT ⇒ 'x ⇒ ('x + 'g ⇒ 'd) ⇒ 'x set ⇒ bool"
  where
  "part_solution T x sigma vars ≡
    x ∈ vars ∧ (∀u ∈ vars.
    dep⇩L T sigma u ⊆ vars ∧
    eq T u sigma = sigma (Inl u) ∧
    sides_of_rhs (T u) sigma ≤ sigma)"

lemma part_solution_implies_trans_dep_subsumed:
  "part_solution T x σl varsl ⟹ trans_dep⇩L T σl x ⊆ varsl"
proof (intro subsetI, goal_cases)
  case (1 z)
  have "x ∈ varsl" "∀u ∈ varsl. dep⇩L T σl u ⊆ varsl" using 1(1) by auto
  have "(x, z) ∈ trans_dep⇩L_rel T σl" using 1(2) by blast
  then show ?case
    using ‹x ∈ varsl› ‹∀u ∈ varsl. dep⇩L T σl u ⊆ varsl›
    by (induction rule: trancl.induct) auto
qed

abbreviation part_post_solution ::
    "('x,'g,'d::bounded_semilattice_sup_bot) eqsT ⇒ 'x ⇒ ('x + 'g ⇒ 'd) ⇒ 'x set ⇒ bool" where
  "part_post_solution T x sigma vars ≡
    x ∈ vars ∧ (∀u ∈ vars.
    dep⇩L T sigma u ⊆ vars ∧
    eq T u sigma ≤ sigma (Inl u) ∧
    sides_of_rhs (T u) sigma ≤ sigma)"

text ‹One name per conjunct of @{term part_post_solution}, so a proof can cite the obligation it
  uses instead of unfolding the abbreviation.›

lemma part_post_solution_query:
  "part_post_solution T x σ vars ⟹ x ∈ vars"
  by blast

lemma part_post_solution_closed:
  "part_post_solution T x σ vars ⟹ u ∈ vars ⟹ dep⇩L T σ u ⊆ vars"
  by blast

lemma part_post_solution_local_bound:
  "part_post_solution T x σ vars ⟹ u ∈ vars ⟹ eq T u σ ≤ σ (Inl u)"
  by blast

lemma part_post_solution_side_bound:
  "part_post_solution T x σ vars ⟹ u ∈ vars ⟹ sides_of_rhs (T u) σ ≤ σ"
  by blast

lemma part_post_solutionI:
  assumes "x ∈ vars"
    and "⋀u. u ∈ vars ⟹ dep⇩L T σ u ⊆ vars"
    and "⋀u. u ∈ vars ⟹ eq T u σ ≤ σ (Inl u)"
    and "⋀u. u ∈ vars ⟹ sides_of_rhs (T u) σ ≤ σ"
  shows "part_post_solution T x σ vars"
  using assms by blast

lemma part_post_solution_implies_trans_dep_subsumed:
  "part_post_solution T x σl varsl ⟹ trans_dep⇩L T σl x ⊆ varsl"
proof (intro subsetI, goal_cases)
  case (1 z)
  have "x ∈ varsl" "∀u ∈ varsl. dep⇩L T σl u ⊆ varsl" using 1(1) by auto
  have "(x, z) ∈ trans_dep⇩L_rel T σl" using 1(2) by blast
  then show ?case
    using ‹x ∈ varsl› ‹∀u ∈ varsl. dep⇩L T σl u ⊆ varsl›
    by (induction rule: trancl.induct) auto
qed

lemma subsumes_se_eq:
  assumes "∀u ∈ dep_aux sigma t. sigma u = sigma' u"
    and "∀u. sigma (Inr u) ≤ sigma' (Inr u)"
    and "sides_of_rhs t sigma ≤ sigma"
  shows "sides_of_rhs t sigma' ≤ sigma'"
  using assms(3,1)
  apply (induction t)
  using assms(2)
  apply (auto simp add: dep_aux_def Let_def le_fun_def fun_upd_def split: if_splits)
  using order.trans
  by metis

lemma solution_sufficient_t:
  assumes "∀y ∈ dep_aux σ t. σ y = σ' y"
  shows "traverse_rhs t σ = traverse_rhs t σ'"
proof -
  obtain xd where xd_def: "traverse_rhs t σ = xd" by simp
  have "traverse_rhs t' σ' = xd"
    if "t' ∈ subt_aux σ t" and "traverse_rhs t' σ = xd" for t'
    using that
  proof(induction t' rule: strategy_tree.induct)
    case (Answer d)
    then show ?case by simp
  next
    case (QueryL y g)
    define t'' where [simp]: "t'' = g (σ (Inl y))"
    have "traverse_rhs t'' σ' = xd"
      using subt_aux.step_QueryL[of "QueryL y g"] QueryL.prems QueryL.IH
      unfolding subt_def by fastforce
    then show ?case
      using subt_implies_dep_locale[where ?t=t, folded subt_def dep_def] QueryL.prems(1) assms(1)
      by simp
  next
    case (QueryG y g)
    define t'' where [simp]: "t'' = g (σ (Inr y))"
    have "traverse_rhs t'' σ' = xd"
      using subt_aux.step_QueryG[of "QueryG y g"] QueryG.prems QueryG.IH
      unfolding subt_def by fastforce
    then show ?case
      using subt_implies_dep_globale[where ?t=t, folded subt_def dep_def] QueryG.prems(1) assms(1)
      by simp
  next
    case (Side y d t)
    show ?case by (metis Side.IH Side.prems(1,2) traverse_rhs.simps(4) subt_aux.step_Side)
  qed
  then show ?thesis
    using assms subt_aux.base xd_def
    unfolding subt_def by fastforce
qed

lemma solution_sufficient:
  assumes "∀y ∈ dep T σ x. σ y = σ' y"
  shows "eq T x σ = eq T x σ'"
  using assms solution_sufficient_t
  unfolding dep_def
  by auto

corollary eq_mupd_no_dep:
  assumes "x ∉ dep T σ y"
  shows "eq T y σ = eq T y (σ (x := xd))"
  apply (rule solution_sufficient[of T])
  using assms
  by (metis fun_upd_other)


subsection ‹Subtrees for Specific Prefixes›

fun subt_for_prefix ::
  "('x,'g,'d::bot) strategy_tree ⇒ (('x + 'g) + ('g × 'd)) list ⇒ ('x + 'g ⇒ 'd) ⇒
   ('x,'g,'d) strategy_tree option" where
  "subt_for_prefix t [] _ = Some t"
| "subt_for_prefix (Answer _) (p#pre) _ = None"
| "subt_for_prefix (QueryL y g) (p#pre) sigma =
    (if Inl (Inl y) = p then subt_for_prefix (g (sigma (Inl y))) pre sigma else None)"
| "subt_for_prefix (QueryG y g) (p#pre) sigma =
    (if Inl (Inr y) = p then subt_for_prefix (g (sigma (Inr y))) pre sigma else None)"
| "subt_for_prefix (Side y d t) (p#pre) sigma =
    (if Inr (y, d) = p then subt_for_prefix t pre sigma else None)"

lemma subt_for_prefix_same:
  assumes "∀u ∈ {u. Inl u ∈ set pre}. sigma u = sigma' u"
  shows "subt_for_prefix t pre sigma = subt_for_prefix t pre sigma'"
  using assms by (induction t pre sigma rule: subt_for_prefix.induct) auto

lemma subt_for_prefix_transitive:
  assumes "subt_for_prefix t1 pre1 sigma = Some t2"
    and "subt_for_prefix t2 pre2 sigma = Some t3"
  shows "subt_for_prefix t1 (pre1 @ pre2) sigma = Some t3"
  using assms
proof (induction pre1 arbitrary: t1)
  case Nil
  then have "t1 = t2" by simp
  then show ?case using Nil(2) by simp
next
  case (Cons p pre1)
  show ?case
  proof (cases t1)
    case (Answer x1)
    then show ?thesis using Cons.prems(1) by force
  next
    case (QueryL y g)
    have "Inl (Inl y) = p" "subt_for_prefix (g (sigma (Inl y))) pre1 sigma = Some t2"
      using Cons(2) QueryL by (auto split: if_splits)
    then have "subt_for_prefix (g (sigma (Inl y))) (pre1 @ pre2) sigma = Some t3"
      using Cons(1,3) by auto
    then show ?thesis using QueryL ‹Inl (Inl y) = p› by auto
  next
    case (QueryG y g)
    then have "Inl (Inr y) = p" "subt_for_prefix (g (sigma (Inr y))) pre1 sigma = Some t2"
      using Cons(2) by (auto split: if_splits)
    then have "subt_for_prefix (g (sigma (Inr y))) (pre1 @ pre2) sigma = Some t3"
      using Cons(1,3) by auto
    then show ?thesis using QueryG ‹Inl (Inr y) = p› by simp
  next
    case (Side y d t)
    then have "Inr (y, d) = p" "subt_for_prefix t pre1 sigma = Some t2"
      using Cons(2) by (auto split: if_splits)
    then have "subt_for_prefix t (pre1 @ pre2) sigma = Some t3"
      using Cons(1,3) by auto
    then show ?thesis using Side ‹Inr (y, d) = p› by simp
  qed
qed

lemma subt_for_prefix_subset_dep:
  "subt_for_prefix t pre sigma = Some t' ⟹ {r. Inl r ∈ set pre} ⊆ dep_aux sigma t"
proof (induction t pre sigma arbitrary: t' rule: subt_for_prefix.induct)
  case (1 t sigma)
  then show ?case by simp
next
  case (2 d p pre sigma)
  then show ?case by simp
next
  case (3 y g p pre sigma)
  have "Inl (Inl y) = p" "subt_for_prefix (g (sigma (Inl y))) pre sigma = Some t'"
    using 3(2) by (simp split: if_splits)+
  then have IH: "{r. Inl r ∈ set pre} ⊆ dep_aux sigma (g (sigma (Inl y)))"
    using 3(1) by simp
  then show ?case using ‹Inl (Inl y) = p› 3(2) by (auto simp add: dep_aux⇩L_def dep_aux_def)
next
  case (4 y g p pre sigma)
  have "Inl (Inr y) = p" "subt_for_prefix (g (sigma (Inr y))) pre sigma = Some t'"
    using 4(2) by (auto split: if_splits)
  then have IH: "{r. Inl r ∈ set pre} ⊆ dep_aux sigma (g (sigma (Inr y)))"
    using 4(1) by simp
  then show ?case using ‹Inl (Inr y) = p› 4(2) by (auto simp add: dep_aux⇩L_def dep_aux_def)
next
  case (5 y d t'' p pre sigma)
  have "Inr (y, d) = p" "subt_for_prefix t'' pre sigma = Some t'"
    using 5(2) by (auto split: if_splits)
  then have IH: "{r. Inl r ∈ set pre} ⊆ dep_aux sigma t''"
    using 5(1) by simp
  then show ?case using ‹Inr (y, d) = p› 5(2) by (auto simp add: dep_aux⇩L_def dep_aux_def)
qed

lemma subt_for_prefix_Answer_eq_traverse:
  "subt_for_prefix t pre sigma = Some (Answer d) ⟹ traverse_rhs t sigma = d"
  by (induction t pre sigma rule: subt_for_prefix.induct) (auto split: if_splits)

lemma subt_for_prefix_Answer_subsumes:
  "subt_for_prefix t pre sigma = Some (Answer d) ⟹
   ∀(u, ud) ∈ {s. Inr s ∈ set pre}. ud ≤ sigma (Inr u) ⟹ sides_of_rhs t sigma ≤ sigma"
  apply (induction t pre sigma rule: subt_for_prefix.induct)
  by (auto simp add: Let_def le_fun_def fun_upd_def split: if_splits)

lemma sides_of_rhs_helper:
  "subt_for_prefix t pre sigma = Some (Side y d t') ⟹ d ≤ (sides_of_rhs t sigma) (Inr y)"
proof (induction t pre sigma rule: subt_for_prefix.induct)
  case (5 y2 d2 t2 p pre sigma)
  have "Inr (y2, d2) = p" "subt_for_prefix t2 pre sigma = Some (Side y d t')"
    using 5 by (auto split: if_splits)
  then have IH: "d ≤ sides_of_rhs t2 sigma (Inr y)" using 5(1) by simp
  then show ?case
    apply (cases "y2 = y")
    using order.trans[OF _ sup_ge1[of "sides_of_rhs t2 sigma (Inr y)" d2]]
    by (auto simp add: Let_def fun_upd_same fun_upd_other)
qed (auto simp add: Let_def fun_upd_same split: if_splits)


subsection ‹Definition for Monotonicity›

definition is_mono_eq :: "('x,'g,'d::order_bot) eqsT ⇒ bool" where
  "is_mono_eq T ≡ (∀x σ⇩1 σ⇩2. σ⇩1 ≤ σ⇩2 ⟶ eq T x σ⇩1 ≤ eq T x σ⇩2)"

definition mono_sides :: "('x,'g,'d::bounded_semilattice_sup_bot) eqsT ⇒ bool" where
  "mono_sides T ≡ (∀x σ⇩1 σ⇩2. σ⇩1 ≤ σ⇩2 ⟶ sides_of_rhs (T x) σ⇩1 ≤ sides_of_rhs (T x) σ⇩2)"

definition mono_deps :: "('x,'g,'d::order_bot) eqsT ⇒ bool" where
  "mono_deps T ≡ (∀x σ⇩1 σ⇩2. σ⇩1 ≤ σ⇩2 ⟶ dep T σ⇩1 x ⊆ dep T σ⇩2 x)"


subsection ‹Definition for Least Partial Post Solution›

abbreviation least_part_post_solution ::
    "('x,'g,'d::bounded_semilattice_sup_bot) eqsT ⇒ 'x ⇒ ('x + 'g ⇒ 'd) ⇒ 'x set ⇒ bool" where
  "least_part_post_solution T x sigma vars ≡ part_post_solution T x sigma vars ∧
    (∀sigma' vars'. part_post_solution T x sigma' vars' ⟶ sigma ≤ sigma' ∧ vars ⊆ vars')"


subsection ‹Partial Post Solutions per Unknown›

text ‹A valuation covers a right-hand side at @{term u} when it bounds both the local answer and
  every side contribution of the same traversal. @{term part_post_solution} is this obligation
  at every covered unknown together with dependency closure, so an argument about one
  right-hand side can discharge its part locally.›

definition tree_covered_at ::
  "('x,'g,'d::bounded_semilattice_sup_bot) strategy_tree ⇒ ('x + 'g ⇒ 'd) ⇒ 'x ⇒ bool"
where
  "tree_covered_at t σ u ≡ traverse_rhs t σ ≤ σ (Inl u) ∧ sides_of_rhs t σ ≤ σ"

lemma tree_covered_at_local [dest]:
  "tree_covered_at t σ u ⟹ traverse_rhs t σ ≤ σ (Inl u)"
  unfolding tree_covered_at_def by simp

lemma tree_covered_at_sides [dest]:
  "tree_covered_at t σ u ⟹ sides_of_rhs t σ ≤ σ"
  unfolding tree_covered_at_def by simp

lemma tree_covered_atI [intro]:
  "traverse_rhs t σ ≤ σ (Inl u) ⟹ sides_of_rhs t σ ≤ σ ⟹ tree_covered_at t σ u"
  unfolding tree_covered_at_def by simp

lemma part_post_solution_iff_tree_covered_at:
  "part_post_solution T x σ vars ⟷
     x ∈ vars ∧ (∀u ∈ vars. dep⇩L T σ u ⊆ vars ∧ tree_covered_at (T u) σ u)"
  unfolding tree_covered_at_def by auto

lemma part_post_solution_imp_tree_covered_at:
  assumes "part_post_solution T x σ vars" and "u ∈ vars"
  shows "tree_covered_at (T u) σ u"
  using assms part_post_solution_iff_tree_covered_at by blast

text ‹@{term post_bounded} drops the dependency closure: an argument about the solved values
  needs only the bounds at the unknowns it reasons about, so it may restrict to any subset that
  still contains the root.›

definition post_bounded ::
  "('x,'g,'d::bounded_semilattice_sup_bot) eqsT ⇒ 'x ⇒ ('x + 'g ⇒ 'd) ⇒ 'x set ⇒ bool"
where
  "post_bounded T x σ vars ⟷ x ∈ vars ∧ (∀u ∈ vars. tree_covered_at (T u) σ u)"

lemma post_boundedD [dest]:
  "post_bounded T x σ vars ⟹ u ∈ vars ⟹ tree_covered_at (T u) σ u"
  unfolding post_bounded_def by blast

lemma post_bounded_of_part_post_solution:
  "part_post_solution T x σ vars ⟹ post_bounded T x σ vars"
  unfolding post_bounded_def part_post_solution_iff_tree_covered_at by blast

lemma post_bounded_subset:
  "post_bounded T x σ vars ⟹ x ∈ V ⟹ V ⊆ vars ⟹ post_bounded T x σ V"
  unfolding post_bounded_def by blast

text ‹@{term part_post_solution} reads a system only through local answers, side contributions
  and dependencies, so two systems agreeing on all three are post-solved by the same
  valuations.›

lemma part_post_solution_cong:
  assumes traverse: "⋀u. traverse_rhs (T u) σ = traverse_rhs (T' u) σ"
    and deps: "⋀u. dep_aux σ (T u) = dep_aux σ (T' u)"
    and sides: "⋀u. sides_of_rhs (T u) σ = sides_of_rhs (T' u) σ"
  shows "part_post_solution T x σ vars ⟷ part_post_solution T' x σ vars"
  unfolding part_post_solution_iff_tree_covered_at tree_covered_at_def dep⇩L_def dep_def
  by (simp add: traverse deps sides)


subsection ‹Dependency Monotonicity per Right-Hand Side›

text ‹@{term mono_deps} asks, for the whole system, that queried unknowns only grow with the
  valuation. @{term mono_tree_deps} is the same property for one right-hand side, and
  @{term env_indep_deps} the stronger one that holds for a right-hand side whose query
  skeleton does not depend on the valuation at all.›

definition env_indep_deps :: "('x, 'g, 'd::bot) strategy_tree ⇒ bool" where
  "env_indep_deps t ⟷ (∀σ1 σ2. dep_aux σ1 t = dep_aux σ2 t)"

lemma env_indep_depsI [intro]:
  "(⋀σ1 σ2. dep_aux σ1 t = dep_aux σ2 t) ⟹ env_indep_deps t"
  unfolding env_indep_deps_def by simp

text ‹Not a ‹[dest]› rule: both valuations are unconstrained by the premise, so ‹auto› would
  instantiate them arbitrarily.›

lemma env_indep_depsD:
  "env_indep_deps t ⟹ dep_aux σ1 t = dep_aux σ2 t"
  unfolding env_indep_deps_def by blast

definition mono_tree_deps :: "('x, 'g, 'd::{order,bot}) strategy_tree ⇒ bool" where
  "mono_tree_deps t ⟷ (∀σ1 σ2. σ1 ≤ σ2 ⟶ dep_aux σ1 t ⊆ dep_aux σ2 t)"

lemma mono_tree_depsI [intro]:
  "(⋀σ1 σ2. σ1 ≤ σ2 ⟹ dep_aux σ1 t ⊆ dep_aux σ2 t) ⟹ mono_tree_deps t"
  unfolding mono_tree_deps_def by blast

lemma mono_tree_depsD [dest]:
  assumes "mono_tree_deps t" and "σ1 ≤ σ2"
  shows "dep_aux σ1 t ⊆ dep_aux σ2 t"
  using assms unfolding mono_tree_deps_def by blast

lemma env_indep_deps_imp_mono_tree_deps [intro]:
  "env_indep_deps t ⟹ mono_tree_deps t"
  unfolding env_indep_deps_def mono_tree_deps_def by blast

lemma mono_deps_of_mono_tree_deps:
  "(⋀x. mono_tree_deps (T x)) ⟹ mono_deps T"
  unfolding mono_deps_def mono_tree_deps_def dep_def by blast

end ―‹end of theory Basics_side›