Theory TD_plain_s

section ‹TD\_plain with simple stable (s)›

theory TD_plain_s
  imports Basics
begin

locale TD_plain_s =
  fixes T :: "'x ⇒ ('x, 'd :: bot) strategy_tree"
begin

function (domintros)
    query :: "'x ⇒ 'x ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map ⇒ 'd × 'x set × ('x, 'd) map" and
  iterate :: "'x ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map ⇒ 'd × 'x set × ('x, 'd) map" and
     eval :: "'x ⇒ ('x, 'd) strategy_tree ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map
             ⇒ 'd × 'x set × ('x, 'd) map" where
  "query x y c s σ = (
    if y ∈ c then
      (mlup σ y, s, σ)
    else
      iterate y (insert y c) s σ)"
| "iterate x c s σ = (
    if x ∉ s then
      let (d_new, s', σ) = eval x (T x) c (insert x s) σ in
      if d_new = mlup σ x then
        (d_new, s', σ)
      else
        iterate x c s (σ(x ↦ d_new))
    else (mlup σ x, s, σ))"
| "eval x t c s σ = (case t of
      Answer d ⇒ (d, s, σ)
    | Query y g ⇒ (let (yd, s, σ) = query x y c s σ in eval x (g yd) c s σ))"
  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 s σ = query_iterate_eval_dom (Inl (x, y, c, s, σ))"
declare query_dom_def [simp]
definition iterate_dom where
  "iterate_dom x c s σ = query_iterate_eval_dom (Inr (Inl (x, c, s, σ)))"
declare iterate_dom_def [simp]
definition eval_dom where
  "eval_dom x t c s σ = query_iterate_eval_dom (Inr (Inr (x, t, c, s, σ)))"
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›

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 s σ. True" and ?R="λx t c s σ. 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 s σ
    ⟹ y ∉ c ⟹ iterate_dom y (insert y c) s σ"
  and "iterate_dom x c s σ
    ⟹ x ∉ s
    ⟹ (eval_dom x (T x) c (insert x s) σ ∧
        (eval x (T x) c (insert x s) σ = (xd_new, s', σ')
          ⟶ mlup σ' x = xd_old ⟶ xd_new ≠ xd_old ⟶
          iterate_dom x c s (σ'(x ↦ xd_new))))"
  and "eval_dom x (Query y g) c s σ
    ⟹ (query_dom x y c s σ ∧ (query x y c s σ = (yd, s', σ') ⟶ eval_dom x (g yd) c s' σ'))"
proof (induction x y c s σ and x c s σ and x "Query y g" c s σ
    arbitrary: and xd_new xd_old s' σ' and y g yd s' σ'
    rule: query_iterate_eval_pinduct)
  case (Query x y c s σ)
  show ?case
  proof (cases "y ∈ s")
    case True
    then show ?thesis using iterate_dom_def query_iterate_eval.domintros(2) by blast
  next
    case False
    then show ?thesis
      using Query.hyps(2) Query.prems query_iterate_eval.domintros(2)[folded dom_defs] by metis
  qed
next
  case (Iterate x c s σ)
  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 x c s σ)
  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 s σ"
    and "iterate x c s σ = (xd, s', σ')"
    and "x ∈ c"
  obtains (Stable) "x ∈ s" "xd = mlup σ x" and "s = s'" and "σ = σ'"
  | (Fixpoint) "eval_dom x (T x) c (insert x s) σ"
    and "eval x (T x) c (insert x s) σ = (xd, s', σ')"
    and "x ∉ s"
    and "mlup σ' x = xd"
  | (Continue) σ1 s1 xd_new
  where "eval_dom x (T x) c (insert x s) σ"
    and "eval x (T x) c (insert x s) σ = (xd_new, s1, σ1)"
    and "x ∉ s"
    and "mlup σ1 x ≠ xd_new"
    and "iterate_dom x c s (σ1(x ↦ xd_new))"
    and "iterate x c s (σ1(x ↦ xd_new)) = (xd, s', σ')"
proof -
  show ?thesis
  proof (cases "x ∈ s")
    case True
    then show ?thesis using Stable assms(1,2) by auto
  next
    case False
    obtain xd_new s1 σ1
      where "eval x (T x) c (insert x s) σ = (xd_new, s1, σ1)"
      by (cases "eval x (T x) c (insert x s) σ")
    then show ?thesis
      using False assms that dom_backwards_pinduct(2) by (cases "mlup σ1 x = xd_new"; simp)
  qed
qed

lemma iterate_fmlookup:
  assumes "iterate_dom x c s σ"
    and "iterate x c s σ = (xd, s', σ')"
    and "x ∈ c"
  shows "mlup σ' x = xd"
  using assms
proof(induction rule: iterate_pinduct)
  case (Iterate x c s σ)
  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 s σ"
    and "query x y c s σ = (yd, s', σ')"
  shows "mlup σ' y = yd"
  using assms iterate_fmlookup dom_backwards_pinduct(1)[of x y c s σ]
  by (auto split: if_splits)

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

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

subsection ‹Partial correctness proofs›

text‹Invariant for induction proof›

definition invariant where
  "invariant s c σ ≡ (∀ξ∈s - c. dep T σ ξ ⊆ s) ∧ (∀ξ∈s - c. eq T ξ σ = mlup σ ξ) ∧ c ⊆ s"

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[of T] by blast
  next
    case 2 then show ?case
      using part_solution_coinciding_sigma_called[where ?T=T] solution_sufficient[where ?T=T]
      by (smt (verit, del_insts))
  next
    case 3 then show ?case by blast
  qed
qed

lemma partial_correctness_ind:
  shows "query_dom x y c s σ
    ⟹ query x y c s σ = (yd, s', σ')
    ⟹ invariant s c σ
    ⟹ invariant s' c σ'
      ∧ s ∪ reach_cap T σ' c y ⊆ s'
      ∧ (∀ξ ∈ s. mlup σ ξ = mlup σ' ξ)"
    and "iterate_dom x c s σ
    ⟹ iterate x c s σ = (xd, s', σ')
    ⟹ x ∈ c
    ⟹ invariant s (c - {x}) σ
    ⟹ invariant s' (c - {x}) σ'
      ∧ x ∈ s'
      ∧ s ∪ (reach_cap T σ' (c - {x}) x) ⊆ s'
      ∧ (∀ξ ∈ s. mlup σ ξ = mlup σ' ξ)"
    and "eval_dom x t c s σ
    ⟹ eval x t c s σ = (xd, s', σ')
    ⟹ invariant s c σ
    ⟹ invariant s' c σ'
      ∧ s ∪ reach_cap_tree T σ' c t ⊆ s'
      ∧ (∀ξ ∈ 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 s σ)
  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(3) by simp
  next
    case Lookup
    then show ?thesis
      using Query.prems(1,2) unfolding invariant_def by auto
  qed
next
  case (Iterate x c s σ)
  show ?case
    using Iterate.IH(1) Iterate.prems(1,2)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis
      using Iterate.prems(3) dep_closed_implies_reach_cap_tree_closed[where ?T=T] invariant_def
      by auto
  next
    case Fixpoint
    note IH = Iterate.IH(2)[OF Fixpoint(3,2), folded eq_def]  invariant_simp[OF Iterate.prems(2,3)]
    then show ?thesis
      using Fixpoint(3,4) 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 (smt (z3) Diff_iff Un_subset_iff insert_Diff insert_iff insert_subset subsetI)
  next
    case (Continue σ1 s1 xd')
    note IH = Iterate.IH(2)[OF Continue(3,2) ] invariant_simp[OF Iterate.prems(2,3)]

    have inv: "invariant s (c - {x}) (σ1(x ↦ xd'))"
      using IH invariant_continue[OF Continue(3) Iterate.prems(3)] by blast

    note ih = Iterate.IH(3)[OF Continue(3) Continue(2)[symmetric] _ _ Continue(4)[symmetric]
        Continue(6) Iterate.prems(2) inv]

    then show ?thesis
      using IH mlup_eq_mupd_set[OF Continue(3), of σ]
      unfolding mlup_def
      by auto
  qed
next
  case (Eval x t c s σ)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (Query y g yd s1 σ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],
        of "(s1, σ1)", simplified]
    have "mlup σ' y = yd" using IH Query(6) ih by auto
    then show ?thesis
      using Query(1) IH ih reach_cap_tree_step[where ?T=T]
        reach_cap_tree_eq[of T σ1 "insert y c" "T y" σ']
       by (simp add: subset_iff)
  next
    case Answer
    then show ?thesis
      using Eval.prems(2) by simp
  qed
qed

corollary partial_correctness:
  assumes "solve_dom x"
    and "solve x = σ"
  shows "part_solution T x σ (reach T σ x)"
proof -
  note it_dom = assms(1)[unfolded solve_dom_def]
  obtain xd s' where it: "iterate x {x} {} Map.empty = (xd, s', σ)"
    using assms(2) unfolding solve_def by (auto split: prod.splits)
  have "part_solution T x σ s' ∧ reach T σ x ⊆ s'"
    using assms(1) partial_correctness_ind(2)[OF it_dom it]
      reach_empty_capped[of T]
    unfolding invariant_def
    by simp
  then show ?thesis by (auto simp add: reach.base reach.step)
qed

end
end