Theory TD_plain

section ‹The plain Top-Down Solver›
text ‹\label{sec:td_plain}›

text‹TD\_plain is a simplified version of the original TD which only keeps track of already called
  unknowns to avoid infinite descend in case of recursive dependencies. In contrast to the TD, it
  does, however, not track stable unknowns and the dependencies between unknowns. Instead, it
  re-iterates every unknown when queried again.
›

theory TD_plain
  imports Basics
begin

locale TD_plain = Solver D T
  for D :: "'d :: bot"
    and T :: "'x ⇒ ('x, 'd) strategy_tree"
begin

subsection ‹Definition of the Solver Algorithm›

text ‹The recursively descending solver algorithm is defined with three mutual recursive functions.
  Initially, the function @{term iterate} is called from the top-level @{term solve} function for
  the requested unknown. @{term iterate} keeps evaluating the right-hand side by calling the
  function @{term eval} and updates the value mapping @{term σ} until the value stabilizes. The
  function @{term eval} walks through a strategy tree and chooses the path based on the result for
  queried unknowns. These queries are delegated to the third mutual recursive function @{term query}
  which checks that the unknown is not already being evaluated and iterates it otherwise. The
  function keyword is used for the definition, since, without further assumptions, the solver may
  not terminate.›

function (domintros)
    query :: "'x ⇒ 'x ⇒ 'x set ⇒ ('x, 'd) map ⇒ 'd × ('x, 'd) map" and
  iterate :: "'x ⇒ 'x set ⇒ ('x, 'd) map ⇒ 'd × ('x, 'd) map" and
     eval :: "'x ⇒ ('x, 'd) strategy_tree ⇒ 'x set ⇒ ('x, 'd) map ⇒ 'd × ('x, 'd) map" where
  "query x y c σ = (
    if y ∈ c then
      (mlup σ y, σ)
    else
      iterate y (insert y c) σ)"
| "iterate x c σ = (
    let (d_new, σ) = eval x (T x) c σ in
    if d_new = mlup σ x then
      (d_new, σ)
    else
      iterate x c (σ(x ↦ d_new)))"
| "eval x t c σ = (case t of
      Answer d ⇒ (d, σ)
    | Query y g ⇒ (let (yd, σ) = query x y c σ in eval x (g yd) c σ))"
  by pat_completeness auto

definition solve :: "'x ⇒ ('x, 'd) map" where
  "solve x = (let (_, σ) = iterate x {x} Map.empty in σ)"

definition query_dom where
  "query_dom x y c σ = query_iterate_eval_dom (Inl (x, y, c, σ))"
declare query_dom_def [simp]
definition iterate_dom where
  "iterate_dom x c σ = query_iterate_eval_dom (Inr (Inl (x, c, σ)))"
declare iterate_dom_def [simp]
definition eval_dom where
  "eval_dom x t c σ = query_iterate_eval_dom (Inr (Inr (x, t, c, σ)))"
declare eval_dom_def [simp]

definition solve_dom where
  "solve_dom x = iterate_dom x {x} Map.empty"

lemmas dom_defs = query_dom_def iterate_dom_def eval_dom_def


subsection ‹Refinement of Auto-Generated Rules›

text ‹The auto-generated \texttt{pinduct} rule contains a redundant assumption. This lemma removes
  this redundant assumption for easier instantiation and assigns each case a comprehensible name.›

lemmas query_iterate_eval_pinduct[consumes 1, case_names Query Iterate Eval]
  = query_iterate_eval.pinduct(1)[
      folded query_dom_def iterate_dom_def eval_dom_def,
      of x y c σ for x y c σ
    ]
    query_iterate_eval.pinduct(2)[
      folded query_dom_def iterate_dom_def eval_dom_def,
      of x c σ for x c σ
    ]
    query_iterate_eval.pinduct(3)[
      folded query_dom_def iterate_dom_def eval_dom_def,
      of x t c σ for x t c σ
    ]

lemmas iterate_pinduct[consumes 1, case_names Iterate]
  = query_iterate_eval_pinduct(2)[where ?P="λx y c σ. True" and ?R="λx t c σ. True",
    simplified (no_asm_use), folded query_dom_def iterate_dom_def eval_dom_def]

declare query.psimps [simp]
declare iterate.psimps [simp]
declare eval.psimps [simp]

subsection ‹Domain Lemmas›

lemma dom_backwards_pinduct:
  shows "query_dom x y c σ
    ⟹ y ∉ c ⟹ iterate_dom y (insert y c) σ"
  and "iterate_dom x c σ
    ⟹ (eval_dom x (T x) c σ ∧
        (eval x (T x) c σ = (xd_new, σ')
          ⟶ mlup σ' x = xd_old ⟶ xd_new ≠ xd_old ⟶
          iterate_dom x c (σ'(x ↦ xd_new))))"
  and "eval_dom x (Query y g) c σ
    ⟹ (query_dom x y c σ ∧ (query x y c σ = (yd, σ') ⟶ eval_dom x (g yd) c σ'))"
proof (induction x y c σ and x c σ and x "Query y g" c σ
    arbitrary: and xd_new xd_old σ' and y g yd σ'
    rule: query_iterate_eval_pinduct)
  case (Query x c σ)
  then show ?case
    using query_iterate_eval.domintros(2) by fastforce
next
  case (Iterate x c σ)
  then show ?case
    using query_iterate_eval.domintros(2,3)[folded eval_dom_def iterate_dom_def query_dom_def]
    by metis
next
  case (Eval c σ)
  then show ?case
    using query_iterate_eval.domintros(1,3) by simp
qed

subsection ‹Case Rules›

lemma iterate_continue_fixpoint_cases[consumes 3]:
  assumes "iterate_dom x c σ"
    and "iterate x c σ = (xd, σ')"
    and "x ∈ c"
  obtains (Fixpoint) "eval_dom x (T x) c σ"
    and "eval x (T x) c σ = (xd, σ')"
    and "mlup σ' x = xd"
  | (Continue) σ1 xd_new
  where "eval_dom x (T x) c σ"
    and "eval x (T x) c σ = (xd_new, σ1)"
    and "mlup σ1 x ≠ xd_new"
    and "iterate_dom x c (σ1(x ↦ xd_new))"
    and "iterate x c (σ1(x ↦ xd_new)) = (xd, σ')"
proof -
 obtain xd_new σ1
    where "eval x (T x) c σ = (xd_new, σ1)"
    by (cases "eval x (T x) c σ")
  then show ?thesis
    using assms that dom_backwards_pinduct(2)
    by (cases "mlup σ1 x = xd_new"; simp)
qed

lemma iterate_fmlookup:
  assumes "iterate_dom x c σ"
    and "iterate x c σ = (xd, σ')"
    and "x ∈ c"
  shows "mlup σ' x = xd"
  using assms
proof(induction rule: iterate_pinduct)
  case (Iterate x c σ)
  show ?case
    using Iterate.hyps Iterate.prems
  proof (cases rule: iterate_continue_fixpoint_cases)
    case (Continue σ1 xd_new)
    then show ?thesis
      using Iterate.prems(2) Iterate.IH
      by fastforce
  qed simp
qed

corollary query_fmlookup:
  assumes "query_dom x y c σ"
    and "query x y c σ = (yd, σ')"
  shows "mlup σ' y = yd"
  using assms iterate_fmlookup dom_backwards_pinduct(1)[of x y c σ]
  by (auto split: if_splits)

lemma query_iterate_lookup_cases [consumes 2]:
  assumes "query_dom x y c σ"
    and "query x y c σ = (yd, σ')"
  obtains (Iterate)
        "iterate_dom y (insert y c) σ"
    and "iterate y (insert y c) σ = (yd, σ')"
    and "mlup σ' y = yd"
    and "y ∉ c"
  | (Lookup) "mlup σ y = yd"
    and "σ = σ'"
    and "y ∈ c"
  using assms that dom_backwards_pinduct(1) query_fmlookup[of x y c σ yd σ']
  by (cases "y ∈ c"; auto)

lemma eval_query_answer_cases [consumes 2]:
  assumes "eval_dom x t c σ"
    and "eval x t c σ = (d, σ')"
  obtains (Query) y g yd σ1
  where "t = Query y g"
    and "query_dom x y c σ"
    and "query x y c σ = (yd, σ1)"
    and "eval_dom x (g yd) c σ1"
    and "eval x (g yd) c σ1 = (d, σ')"
    and "mlup σ1 y = yd"
  | (Answer) "t = Answer d"
    and "σ = σ'"
  using assms dom_backwards_pinduct(3) that query_fmlookup
  by (cases t; auto split: prod.splits)

subsection ‹Predicate for Valid Input States›

text‹We define a predicate for valid input solver states. @{term c} is the set of called unknowns,
  i.e., the unknowns currently being evaluated and @{term σ} is an unknown-to-value mapping. Both
  are data structures maintained by the solver. In contrast, the parameter @{term s} describing a
  set of unknowns, for which a partial solution has already been computed or which are currently
  being evaluated, is introduced for the proof. Although it is similar to the set @{term stabl}
  maintained by the original TD, it is only an under-approximation of it.
  A valid solver state is one, where @{term σ} is a partial solution for all truly stable unknowns,
  i.e., unknowns in @{term "s - c"}, and where these truly stable unknowns only depend on unknowns
  which are also truly stable or currently being evaluated.
  A substantial part of the partial correctness proof is to show that this property about the
  solver's state is preserved during a solver's run.›

definition invariant where
  "invariant s c σ ≡ (∀ξ∈s - c. dep σ ξ ⊆ s) ∧ part_solution σ (s - c)"

lemma invariant_simp:
  assumes "x ∈ c"
    and "invariant s (c - {x}) σ"
  shows "invariant (insert x s) c σ"
  using assms
proof -
  have "c - {x} ⊆ s ≡ c ⊆ insert x s"
    using assms(1)
    by (simp add: subset_insert_iff)
  moreover have "s - (c - {x}) ⊇ insert x s - c"
    using assms(1)
    by auto
  ultimately show ?thesis
    using assms(2)
    unfolding invariant_def
    by fastforce
qed

lemma invariant_continue:
  assumes "x ∉ s"
    and "invariant s c σ"
    and "∀y∈s. mlup σ y = mlup σ1 y"
  shows "invariant s c (σ1(x ↦ xd))"
proof -
  show ?thesis
  using assms mlup_eq_mupd_set[OF assms(1,3)] unfolding invariant_def
  proof(intro conjI, goal_cases)
    case 1 then show ?case using dep_eq by blast
  next
    case 2 then show ?case using part_solution_coinciding_sigma_called
      by (metis DiffD1 solution_sufficient subsetD)
  qed
qed

subsection ‹Partial Correctness Proofs›

lemma x_not_stable:
  assumes "eq x σ ≠ mlup σ x"
    and "part_solution σ s"
  shows "x ∉ s"
  using assms by auto

text‹With the following lemma we establish, that whenever the solver is called for an unknown
  in @{term s} and where the solver state and @{term s} fulfill the invariant, the output value
  mapping is unchanged compared to the input value mapping.›

lemma already_solution:
  shows "query_dom x y c σ
    ⟹ query x y c σ = (yd, σ')
    ⟹ y ∈ s
    ⟹ invariant s c σ
    ⟹ σ = σ'"
    and "iterate_dom x c σ
    ⟹ iterate x c σ = (xd, σ')
    ⟹ x ∈ c
    ⟹ x ∈ s
    ⟹ invariant s (c - {x}) σ
    ⟹ σ = σ'"
    and "eval_dom x t c σ
    ⟹ eval x t c σ = (xd, σ')
    ⟹ dep_aux σ t ⊆ s
    ⟹ invariant s c σ
    ⟹ traverse_rhs t σ' = xd ∧ σ = σ'"
proof(induction arbitrary: yd s σ' and xd s σ' and xd s σ' rule: query_iterate_eval_pinduct)
  case (Query x y c σ)
  show ?case using Query.IH(1) Query.prems Query.IH(2)
    by (cases rule: query_iterate_lookup_cases; simp)
next
  case (Iterate x c σ)
  show ?case using Iterate.IH(1) Iterate.prems(1,2)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Fixpoint
    then show ?thesis
      using Iterate.prems(3,4) Iterate.IH(2)[of _ _ "insert x s"]
        invariant_simp[OF Iterate.prems(2,4)]
      unfolding dep_def invariant_def by auto
  next
    case (Continue σ1 xd')
    show ?thesis
    proof(rule ccontr)
      have IH: "eq x σ1 = xd' ∧ σ = σ1"
        using Iterate.prems(2-4) Iterate.IH(2)[OF Continue(2), of s]
          invariant_simp[OF Iterate.prems(2,4)] unfolding dep_def invariant_def by auto
      then show False
        using Iterate.prems(2-4) Continue(3) unfolding invariant_def by simp
    qed
  qed
next
  case (Eval x t c σ)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (Query y g yd σ1)
    then show ?thesis using Eval.prems(1-3) Eval.IH(1) Eval.IH(2)[OF Query(1,3)]
        Eval.IH(3)[OF Query(1) Query(3)[symmetric] _ Query(5)]
      by auto
  qed simp
qed

text‹Furthermore, we show that whenever the solver is called with a valid solver state, the valid
  solver state invariant also holds for its output state and the set of stable unknowns increases by
  the set @{term [source = true] reach_cap} of the current unknown.›

lemma partial_correctness_ind:
  shows "query_dom x y c σ
    ⟹ query x y c σ = (yd, σ')
    ⟹ invariant s c σ
    ⟹ invariant (s ∪ reach_cap σ' c y) c σ'
      ∧ (∀ξ ∈ s. mlup σ ξ = mlup σ' ξ)"
    and "iterate_dom x c σ
    ⟹ iterate x c σ = (xd, σ')
    ⟹ x ∈ c
    ⟹ invariant s (c - {x}) σ
    ⟹ invariant (s ∪ (reach_cap σ' (c - {x}) x)) (c - {x}) σ'
      ∧ (∀ξ ∈ s. mlup σ ξ = mlup σ' ξ)"
    and "eval_dom x t c σ
    ⟹ eval x t c σ = (xd, σ')
    ⟹ invariant s c σ
    ⟹ invariant (s ∪ reach_cap_tree σ' c t) c σ'
      ∧ (∀ξ ∈ s. mlup σ ξ = mlup σ' ξ)
      ∧ traverse_rhs t σ' = xd"
proof(induction arbitrary: yd s σ' and xd s σ' and xd s σ' rule: query_iterate_eval_pinduct)
  case (Query x y c σ)
  show ?case
    using Query.IH(1) Query.prems(1)
  proof (cases rule: query_iterate_lookup_cases)
    case Iterate
    note IH = Query.IH(2)[simplified, OF Iterate(4,2) Query.prems(2)]
    then show ?thesis
      using Iterate(4) by simp
  next
    case Lookup
    then show ?thesis
      using Query.prems(2) unfolding invariant_def by auto
  qed
next
  case (Iterate x c σ)
  show ?case
    using Iterate.IH(1) Iterate.prems(1,2)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Fixpoint
    note IH = Iterate.IH(2)[OF Fixpoint(2) invariant_simp[OF Iterate.prems(2,3)], folded eq_def]
    then show ?thesis
      using Fixpoint(3) Iterate.prems(2) reach_cap_tree_simp2[of x "c - {x}"]
        dep_subset_reach_cap_tree[of σ' "T x", folded dep_def]
      unfolding invariant_def
      by (auto simp add: insert_absorb)
  next
    case (Continue σ1 xd')
    note IH = Iterate.IH(2)[OF Continue(2) invariant_simp[OF Iterate.prems(2,3)]]

    have "part_solution σ1 (s - (c - {x}))"
      using part_solution_coinciding_sigma_called[of s "c - {x}" σ σ1] IH Iterate.prems(3)
      unfolding invariant_def
      by simp
    then have x_not_stable: "x ∉ s"
      using x_not_stable[of x σ1 s] IH Continue(3)
      by auto
    then have inv: "invariant s (c - {x}) (σ1(x ↦ xd'))"
      using IH invariant_continue[OF x_not_stable Iterate.prems(3)] by blast

    note ih = Iterate.IH(3)[OF Continue(2)[symmetric] _ Continue(3)[symmetric] Continue(5)
        Iterate.prems(2) inv, simplified]
    then show ?thesis
      using IH mlup_eq_mupd_set[OF x_not_stable, of σ]
      unfolding mlup_def
      by auto
  qed
next
  case (Eval x t c σ)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (Query y g yd σ1)
    note IH = Eval.IH(2)[OF Query(1,3) Eval.prems(2)]
    note ih = Eval.IH(3)[OF Query(1) Query(3)[symmetric] _ Query(5) conjunct1[OF IH], simplified]
    show ?thesis
      using Query IH ih reach_cap_tree_step reach_cap_tree_eq[of σ1 "insert y c" "T y" σ']
      by (auto simp add: Un_assoc)
  next
    case Answer
    then show ?thesis
      using Eval.prems(2) by simp
  qed
qed

text‹Since the initial solver state fulfills the valid solver state predicate, we can conclude from
  the above lemma, that the solve function returns a partial solution for the queried unknown
  @{term x} and all unknowns on which it transitively depends.›

corollary partial_correctness:
  assumes "solve_dom x"
    and "solve x = σ"
  shows "part_solution σ (reach σ x)"
proof -
  obtain xd where "iterate x {x} Map.empty = (xd, σ)"
    using assms(2) unfolding solve_def by (auto split: prod.splits)
  then show ?thesis
  using assms(1) partial_correctness_ind(2)[of x "{x}" Map.empty xd σ "{}"] reach_empty_capped
  unfolding solve_dom_def invariant_def by simp
qed


subsection ‹Termination of TD\_plain for Stable Unknowns›

text‹In the equivalence proof of the TD and the TD\_plain, we need to show that when the TD
  trivially terminates because the queried unknown is already stable and its value is only looked
  up, the evaluation of this unknown @{term x} with TD\_plain also terminates. For this, we exploit
  that the set of stable unknowns is always finite during a terminating solver's run and provide the
  following lemma:›

lemma td1_terminates_for_stabl:
  assumes "x ∈ s"
    and "invariant s (c - {x}) σ"
    and "mlup σ x = xd"
    and "finite s"
    and "x ∈ c"
  shows "iterate_dom x c σ" and "iterate x c σ = (xd, σ)"
proof(goal_cases)
  have "reach_cap σ (c - {x}) x ⊆ s"
    using assms(1,2) dep_closed_implies_reach_cap_tree_closed unfolding invariant_def by simp
  from finite_subset[OF this] have "finite (reach_cap σ (c - {x}) x - (c - {x}))"
    using assms(4) by simp+
  then have goal: "iterate_dom x c σ ∧ iterate x c σ = (xd, σ)" using assms(1-3,5)
  proof(induction "reach_cap σ (c - {x}) x - (c - {x})"
      arbitrary: x c xd rule: finite_psubset_induct)
    case psubset
    have "eval_dom x t c σ ∧ (traverse_rhs t σ, σ) = eval x t c σ" if "t ∈ subt σ x" for t
      using that
    proof(induction t)
      case (Answer _)
      then show ?case
        using query_iterate_eval.domintros(3)[folded query_dom_def iterate_dom_def eval_dom_def]
        by fastforce
    next
      case (Query y g)
      have "reach_cap_tree σ (insert x (c - {x})) (T x) ⊆ s"
        using dep_closed_implies_reach_cap_tree_closed[OF psubset.prems(1), of c σ]
          psubset.prems(2)[unfolded invariant_def]
        by auto
      then have y_stable: "y ∈ s"
        using dep_subset_reach_cap_tree subt_implies_dep[OF Query(2)[unfolded subt_def]]
        by blast
      show ?case
      proof(cases "y ∈ c" rule: case_split[case_names called not_called])
        case called
        then have dom: "query_dom x y c σ"
          using query_iterate_eval.domintros(1)[folded query_dom_def] by auto
        moreover have query_val: "(mlup σ y, σ) = query x y c σ"
          using called already_solution(1) partial_correctness_ind(1)
          by (metis query.psimps query_iterate_eval.domintros(1))
        ultimately have "eval_dom x (Query y g) c σ"
          using Query.IH[of "g (mlup σ y)"]
            query_iterate_eval.domintros(3)[folded dom_defs, of "Query y g" x c σ] Query.prems
            subt_aux.step subt_def
          by fastforce
        have "g (mlup σ y) ∈ subt_aux σ (T x)"
          using Query.prems subt_aux.step subt_def by blast
        then have "eval_dom x (g (mlup σ y)) c σ"
            and "(traverse_rhs (g (mlup σ y)) σ, σ) = eval x (g (mlup σ y)) c σ"
          using Query.IH unfolding subt_def by auto
        then show ?thesis
          using ‹eval_dom x (Query y g) c σ› query_val
          by (auto split: strategy_tree.split prod.split)
      next
        case not_called
        then obtain yd where lupy: "mlup σ y = yd" and eqy: "eq y σ = yd"
          using y_stable psubset.prems(2) unfolding invariant_def by auto
        have ih: "eval_dom x (g (mlup σ y)) c σ"
            and "(traverse_rhs (g (mlup σ y)) σ, σ) = eval x (g (mlup σ y)) c σ"
          using Query.IH[of "g (mlup σ y)"] Query.prems subt_aux.step subt_def by auto
        moreover have "reach_cap σ c y ⊆ reach_cap σ (c - {x}) x"
          using not_called psubset.prems(4) reach_cap_tree_step[of σ y yd c g, OF lupy]
            reach_cap_tree_subset_subt[of "Query y g" σ "T x" c, folded subt_def, OF Query.prems]
          by (simp add: insert_absorb subset_insertI2)
        then have f_def: "reach_cap σ c y - c ⊂ reach_cap σ (c - {x}) x - (c - {x})"
          using psubset.prems(4)
          by blast
        have "invariant s (c - {y}) σ"
          using psubset.prems(2) not_called psubset.prems(1) invariant_simp
          by (metis Diff_empty Diff_insert0 insert_absorb)
        then have IH: "iterate_dom y (insert y c) σ ∧ iterate y (insert y c) σ = (yd, σ)"
          using f_def y_stable not_called lupy psubset.hyps(2)[of y "c - {y}" yd] psubset.hyps(2)
          by (metis Diff_idemp Diff_insert_absorb insertCI )
        then have "query_dom x y c σ ∧ (mlup σ y, σ) = query x y c σ"
          using not_called lupy query_iterate_eval.domintros(1)[folded dom_defs, of y c σ]
          by simp
        ultimately show ?thesis
          using query_iterate_eval.domintros(3)[folded dom_defs, of "Query y g" x c σ] by fastforce
      qed
    qed
    note IH = this[of "T x", folded eq_def, OF subt_aux.base[of "T x" σ, folded subt_def]]
    moreover have "eq x σ = mlup σ x" using psubset.prems(1,2) unfolding invariant_def by auto
    moreover have "iterate_dom x c σ"
      using query_iterate_eval.domintros(2)[folded dom_defs, of x c σ] IH ‹eq x σ = mlup σ x›
      by (metis Pair_inject)
    ultimately show ?case
      using iterate.psimps[folded dom_defs, of x c σ] psubset.prems(3)
      by (cases "eval x (T x) c σ") auto
  qed
  case 1 show ?case using goal ..
  case 2 show ?case using goal ..
qed


subsection ‹Program Refinement for Code Generation›

text‹For code generation, we define a refined version of the solver function using the
partial\_function keyword with the option attribute.›

datatype ('a,'b) state = Q "'a × 'a × 'a set × ('a, 'b) map"
  | I "'a × 'a set × ('a, 'b) map"  | E "'a × ('a,'b) strategy_tree × 'a set × ('a, 'b) map"

partial_function (option)
  solve_rec_c :: "('x, 'd) state ⇒ ('d × ('x, 'd) map) option"
 where
  "solve_rec_c s = (case s of Q (x, y, c, σ) ⇒
      if y ∈ c then
        Some (mlup σ y, σ)
      else
        solve_rec_c (I (y, (insert y c), σ))
    | I (x, c, σ) ⇒
      Option.bind (solve_rec_c (E (x, (T x), c, σ))) (λ(d_new, σ).
      if d_new = mlup σ x then
        Some (d_new, σ)
      else
        solve_rec_c (I (x, c, (σ(x ↦ d_new)))))
    | E (x, t, c, σ) ⇒
      (case t of
        Answer d ⇒ Some (d, σ)
      | Query y g ⇒ Option.bind (solve_rec_c (Q (x, y, c, σ)))
        (λ(yd, σ). solve_rec_c (E (x, (g yd), c, σ)))))"

declare solve_rec_c.simps[simp,code]

definition solve_rec_c_dom where "solve_rec_c_dom p ≡ ∃σ. solve_rec_c p = Some σ"

definition solve_c :: "'x ⇒ (('x, 'd) map) option" where
  "solve_c x = Option.bind (solve_rec_c (I (x, {x}, Map.empty))) (λ(_, σ). Some σ)"

definition solve_c_dom :: "'x ⇒ bool" where "solve_c_dom x ≡ ∃σ. solve_c x = Some σ"


text‹We proof the equivalence between the refined solver function for code generation and the
initial version used for the partial correctness proof.›

lemma query_iterate_eval_solve_rec_c_equiv:
  shows "query_dom x y c σ ⟹ solve_rec_c_dom (Q (x,y,c,σ))
    ∧ query x y c σ = the (solve_rec_c (Q (x,y,c,σ)))"
  and "iterate_dom x c σ ⟹ solve_rec_c_dom (I (x,c,σ))
    ∧ iterate x c σ = the (solve_rec_c (I (x,c,σ)))"
  and "eval_dom x t c σ ⟹ solve_rec_c_dom (E (x,t,c,σ))
    ∧ eval x t c σ = the (solve_rec_c (E (x,t,c,σ)))"
proof (induction x y c σ and x c σ and x t c σ rule: query_iterate_eval_pinduct)
  case (Query x y c σ)
  show ?case
  proof (cases "y ∈ c")
    case True
    then have "solve_rec_c (Q (x, y, c, σ)) = Some (mlup σ y, σ)" by simp
    moreover have "query x y c σ = (mlup σ y, σ)"
      using query.psimps[folded dom_defs] Query(1) True by force
    ultimately show ?thesis unfolding solve_rec_c_dom_def by auto
  next
    case False
    then have "query x y c σ = iterate y (insert y c) σ"
      using Query.IH(1) query.pelims[folded dom_defs] by fastforce
    then have "query x y c σ = the (solve_rec_c (Q (x, y, c, σ)))"
      using Query False False by simp
    moreover have "solve_rec_c_dom (Q (x, y, c, σ))"
      using Query(2) False unfolding solve_rec_c_dom_def by simp
    ultimately show ?thesis using Query unfolding solve_rec_c_dom_def by auto
  qed
next
  case (Iterate x c σ)
  obtain d1 σ1 where eval: "eval x (T x) c σ = (d1, σ1)"
    and "solve_rec_c (E (x, T x, c, σ)) = Some (d1, σ1)" using Iterate(2) solve_rec_c_dom_def by force
  show ?case
  proof (cases "d1 = mlup σ1 x")
    case True
    have "iterate x c σ = (d1, σ1)"
      using eval iterate.psimps[folded dom_defs, OF Iterate(1)] True by simp
    then show ?thesis
      using solve_rec_c_dom_def dom_defs iterate.psimps Iterate by fastforce
  next
    case False
    then have "solve_rec_c_dom (I (x, c, σ1(x ↦ d1)))"
        and "iterate x c (σ1(x ↦ d1)) = the (solve_rec_c (I (x, c, σ1(x ↦ d1))))"
      using Iterate(3)[OF eval[symmetric] _ False] by blast+
    moreover have "iterate x c σ = iterate x c (σ1(x ↦ d1))"
      using eval iterate.psimps[folded dom_defs, OF Iterate(1)] False by simp
    moreover have "solve_rec_c (I (x, c, σ1(x ↦ d1))) = solve_rec_c (I (x, c, σ))"
      using False eval Iterate(2) solve_rec_c_dom_def by auto
    ultimately show ?thesis unfolding solve_rec_c_dom_def by auto
  qed
next
  case (Eval x t c σ)
  show ?case
  proof (cases t)
    case (Answer d)
    then have "eval x t c σ = (d, σ)"
      using eval.psimps query_iterate_eval.domintros(3) dom_defs(3)
      by fastforce
    then show ?thesis using Eval Answer unfolding solve_rec_c_dom_def by simp
  next
    case (Query y g)
    then obtain d1 σ1 where "solve_rec_c (Q (x, y, c, σ)) = Some (d1, σ1)"
        and "query x y c σ = (d1, σ1)"
      using Query Eval(2) unfolding solve_rec_c_dom_def by auto
    then have "solve_rec_c_dom (E (x, t, c, σ))"
        "eval x (g d1) c σ1 = the (solve_rec_c (E (x, t, c, σ)))"
      using Eval(3) Query unfolding solve_rec_c_dom_def by auto
    moreover have "eval x t c σ = eval x (g d1) c σ1"
      using Eval.IH(1) Query eval.psimps eval_dom_def
        ‹query x y c σ = (d1, σ1)›
      by fastforce
    ultimately show ?thesis by simp
  qed
qed

lemma solve_rec_c_query_iterate_eval_equiv:
  shows "solve_rec_c s = Some r ⟹ (case s of
        Q (x,y,c,σ) ⇒ query_dom x y c σ ∧ query x y c σ = r
      | I (x,c,σ) ⇒ iterate_dom x c σ ∧ iterate x c σ = r
      | E (x,t,c,σ) ⇒ eval_dom x t c σ ∧ eval x t c σ = r)"
proof (induction arbitrary: s r rule: solve_rec_c.fixp_induct)
  case 1
  then show ?case using option_admissible by fast
next
  case 2
  then show ?case by simp
next
  case (3 S)
  show ?case
  proof (cases s)
    case (Q a)
    obtain x y c σ where "a = (x, y, c, σ)" using prod_cases4 by blast
    have "query_dom x y c σ ∧ query x y c σ = r"
    proof (cases "y ∈ c")
      case True
      then have "Some (mlup σ y, σ) = Some r" using 3(2) Q ‹a = (x, y, c, σ)› by simp
      then show ?thesis
        by (metis query.psimps query_dom_def
            query_iterate_eval.domintros(1) True option.inject)
    next
      case False
      then have "S (I (y, insert y c, σ)) = Some r"
        using 3(2) Q ‹a = (x, y, c, σ)› by auto
      then have "iterate_dom y (insert y c) σ ∧ iterate y (insert y c) σ = r"
        using 3(1) unfolding iterate_dom_def by fastforce
      then show ?thesis using False
        by (simp add: query_iterate_eval.domintros(1))
    qed
    then show ?thesis using Q ‹a = (x, y, c, σ)› unfolding query_dom_def by simp
  next
    case (I a)
    obtain x c σ where "a = (x, c, σ)" using prod_cases3 by blast
    then have IH1: "Option.bind (S (E (x, T x, c, σ)))
       (λ(d_new, σ).
         if d_new = mlup σ x then Some (d_new, σ)
         else S (I (x, c, σ(x ↦ d_new)))) = Some r"
      using 3(2) I by simp
    then obtain d_new σ1 where eval_some: "S (E (x, T x, c, σ)) = Some (d_new, σ1)"
      using 3(2) I
      by (cases "S (E (x, T x, c, σ))") auto
    then have eval: "eval_dom x (T x) c σ ∧ eval x (T x) c σ = (d_new, σ1)"
      using 3(1) unfolding eval_dom_def by force
    have "iterate_dom x c σ ∧ iterate x c σ = r"
    proof (cases "d_new = mlup σ1 x")
      case True
      then show ?thesis
        using eval IH1 dom_defs(2) dom_defs(3) iterate.psimps
          query_iterate_eval.domintros(2) eval_some
        by fastforce
    next
      case False
      then have "S (I (x, c, σ1(x ↦ d_new))) = Some r" using IH1 eval_some by simp
      then have "iterate_dom x c (σ1(x ↦ d_new))
          ∧ iterate x c (σ1(x ↦ d_new)) = r"
        using 3(1) unfolding iterate_dom_def by fastforce
      then show ?thesis using eval False
        by (smt (verit, best) Pair_inject dom_defs(2) dom_defs(3)
            iterate.psimps query_iterate_eval.domintros(2) case_prod_conv)
    qed
    then show ?thesis using I ‹a = (x, c, σ)› unfolding iterate_dom_def by simp
  next
    case (E a)
    obtain x t c σ where "a = (x, t, c, σ)" using prod_cases4 by blast
    then have "s = E (x, t, c, σ)" using E by auto
    have "eval_dom x t c σ ∧ eval x t c σ = r"
    proof (cases t)
      case (Answer d)
      then have "eval_dom x t c σ" unfolding eval_dom_def
        using query_iterate_eval.domintros(3) by fastforce
      moreover have "eval x t c σ = (d, σ)"
        by (smt (verit, del_insts) Answer eval_query_answer_cases calculation
            strategy_tree.distinct(1) strategy_tree.simps(1) surj_pair)
      moreover have "(d, σ) = r" using 3(2) ‹s = E (x, t, c, σ)› Answer by simp
      ultimately show ?thesis by simp
    next
      case (Query y g)
      then have A: "Option.bind (S (Q (x, y, c, σ))) (λ(yd, σ). S (E (x, g yd, c, σ)))
        = Some r" using ‹s = E (x, t, c, σ)› 3(2) by simp
      then obtain yd σ1 where S1: "S (Q (x, y, c, σ)) = Some (yd, σ1)"
          and S2: "S (E (x, g yd, c, σ1)) = Some r"
        by (cases "S (Q (x, y, c, σ))") auto
      then have "query_dom x y c σ ∧ query x y c σ = (yd, σ1)"
          and "eval_dom x (g yd) c σ1 ∧ eval x (g yd) c σ1 = r"
        using 3(1)[OF S1] 3(1)[OF S2] unfolding dom_defs by force+
      then show ?thesis
        using query_iterate_eval.domintros(3)[folded dom_defs, of t x c σ] Query
        by fastforce
    qed
    then show ?thesis using E ‹a = (x, t, c, σ)› unfolding eval_dom_def by simp
  qed
qed

theorem term_equivalence: "solve_dom x ⟷ solve_c_dom x"
  using query_iterate_eval_solve_rec_c_equiv(2)[of x "{x}" "λx. None"]
    solve_rec_c_query_iterate_eval_equiv[of "I (x, {x}, λx. None)"]
  unfolding solve_dom_def solve_c_dom_def solve_rec_c_dom_def solve_c_def
  by (cases "solve_rec_c (I (x, {x}, λx. None))") force+

theorem value_equivalence:
  "solve_dom x ⟹ ∃σ. solve_c x = Some σ ∧ solve x = σ"
proof goal_cases
  case 1
  then obtain r where "solve_rec_c (I (x, {x}, λx. None)) = Some r
    ∧ iterate x {x} (λx. None) = r"
    using query_iterate_eval_solve_rec_c_equiv(2)
    unfolding solve_rec_c_dom_def solve_dom_def
    by fastforce
  then show ?case unfolding solve_def solve_c_def by (auto split: prod.split)
qed

text‹Then, we can define the code equation for @{term solve} based on the refined solver program
  @{term solve_c}.›

lemma solve_code_equation [code]:
  "solve x = (case solve_c x of Some r ⇒ r
  | None ⇒ Code.abort (String.implode ''Input not in domain'') (λ_. solve x))"
proof (cases "solve_dom x")
  case True
  then show ?thesis unfolding solve_def solve_c_def
    by (metis solve_def solve_c_def option.simps(5) value_equivalence)
next
  case False
  then have "solve_c x = None" using solve_c_dom_def term_equivalence by auto
  then show ?thesis by auto
qed

end

text‹To setup the code generation for the solver locale we use a dedicated rewrite definition.›

global_interpretation TD_plain_Interp: TD_plain D T for D T
  defines TD_plain_Interp_solve = TD_plain_Interp.solve
  done

end