Theory TD_plain_s_warrow

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

theory TD_plain_s_warrow
  imports Basics
begin

locale TD_plain_s_warrow =
  fixes T :: "'x ⇒ ('x, 'd :: bounded_lattice_bot) strategy_tree"

  fixes widening :: "'d ⇒ 'd ⇒ 'd" (infixl "∇" 65)
    and narrowing :: "'d ⇒ 'd ⇒ 'd" (infixl "Δ" 70)
  assumes widening_ge: "a ⊔ b ≤ a ∇ b"
    and narrowing_in: "a ⊓ b ≤ a Δ b ∧ a Δ b ≤ a"
begin

definition warrowing :: "'d ⇒ 'd ⇒ 'd" (infixl "∇Δ" 65)
  where "warrowing a b = (if b ≤ a then a Δ b else a ∇ b)"

function (domintros)
  query ::
      "'x ⇒ 'x ⇒ 'x set ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map ⇒ 'd × 'x set × 'x set × ('x, 'd) map" and
  iterate ::
      "'x ⇒ 'x set ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map ⇒ 'd × 'x set × 'x set × ('x, 'd) map" and
  eval ::
      "'x ⇒ ('x, 'd) strategy_tree ⇒ 'x set ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map
      ⇒ 'd × 'x set × 'x set × ('x, 'd) map" where
  "query x y c s p σ = (
    if y ∈ c then
      (mlup σ y, s, insert y p, σ)
    else
      iterate y (insert y c) s p σ)"
| "iterate x c s p σ = (
    if x ∉ s then
      let (d_new, s', p', σ) = eval x (T x) c (insert x s) p σ in
      let d_new' = if x ∉ p then d_new else mlup σ x ∇Δ d_new in
      if d_new' = mlup σ x then
        (mlup σ x, s', Set.remove x p', σ)
      else
        iterate x c s p' (σ(x ↦ d_new'))
    else (mlup σ x, s, p, σ))"
| "eval x t c s p σ = (case t of
      Answer d ⇒ (d, s, p, σ)
    | Query y g ⇒ (let (yd, s, p, σ) = query x y c s p σ in eval x (g yd) c s p σ))"
  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 p σ = query_iterate_eval_dom (Inl (x, y, c, s, p, σ))"
declare query_dom_def [simp]
definition iterate_dom where
  "iterate_dom x c s p σ = query_iterate_eval_dom (Inr (Inl (x, c, s, p, σ)))"
declare iterate_dom_def [simp]
definition eval_dom where
  "eval_dom x t c s p σ = query_iterate_eval_dom (Inr (Inr (x, t, c, s, p, σ)))"
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 p σ. True" and ?R="λx t c s p σ. 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 p σ
    ⟹ y ∉ c ⟹ iterate_dom y (insert y c) s p σ"
  and "iterate_dom x c s p σ
    ⟹ x ∉ s
    ⟹ (eval_dom x (T x) c (insert x s) p σ ∧
        (eval x (T x) c (insert x s) p σ = (xd_new, s', p', σ')
          ⟶ mlup σ' x = xd_old ⟶ (if x ∉ p then xd_new else xd_old ∇Δ xd_new) = xd_new'
          ⟶ xd_new' ≠ xd_old ⟶ iterate_dom x c s p' (σ'(x ↦ xd_new'))))"
  and "eval_dom x (Query y g) c s p σ
    ⟹ (query_dom x y c s p σ ∧ (query x y c s p σ = (yd, s', p', σ')
          ⟶ eval_dom x (g yd) c s' p' σ'))"
proof (induction x y c s p σ and x c s p σ and x "Query y g" c s p σ
    arbitrary: and xd_new xd_new' xd_old s' p' σ' and y g yd s' p' σ'
    rule: query_iterate_eval_pinduct)
  case (Query x y c s p σ)
  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 p σ)
  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 p σ)
  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 p σ"
    and "iterate x c s p σ = (xd, s', p', σ')"
    and "x ∈ c"
  obtains (Stable) "x ∈ s"
    and "xd = mlup σ x"
    and "s = s'"
    and "σ = σ'"
    and "p = p'"
  | (Fixpoint) xd1 p1
    where "eval_dom x (T x) c (insert x s) p σ"
    and "eval x (T x) c (insert x s) p σ = (xd1, s', p1, σ')"
    and "x ∉ s"
    and "x ∉ p"
    and "xd1 = mlup σ' x"
    and "p' = Set.remove x p1"
  | (Fixpoint_W) xd1 p1
    where "eval_dom x (T x) c (insert x s) p σ"
    and "eval x (T x) c (insert x s) p σ = (xd1, s', p1, σ')"
    and "x ∉ s"
    and "x ∈ p"
    and "mlup σ' x ∇Δ xd1 = mlup σ' x"
    and "p' = Set.remove x p1"
  | (Continue) xd1 s1 p1 σ1
    where "eval_dom x (T x) c (insert x s) p σ"
    and "eval x (T x) c (insert x s) p σ = (xd1, s1, p1, σ1)"
    and "x ∉ s"
    and "x ∉ p"
    and "xd1 ≠ mlup σ1 x"
    and "iterate_dom x c s p1 (σ1(x ↦ xd1))"
    and "iterate x c s p1 (σ1(x ↦ xd1)) = (xd, s', p', σ')"
  | (Continue_W) xd1 s1 p1 σ1 xdw
    where "eval_dom x (T x) c (insert x s) p σ"
    and "eval x (T x) c (insert x s) p σ = (xd1, s1, p1, σ1)"
    and "x ∉ s"
    and "x ∈ p"
    and "xdw = mlup σ1 x ∇Δ xd1"
    and "xdw ≠ mlup σ1 x"
    and "iterate_dom x c s p1 (σ1(x ↦ xdw))"
    and "iterate x c s p1 (σ1(x ↦ xdw)) = (xd, s', p', σ')"
proof -
  show ?thesis
  proof (cases "x ∈ s")
    case True
    then show ?thesis using Stable assms(1,2) by auto
  next
    case False
    obtain xd1 s1 p1 σ1
      where ev: "eval x (T x) c (insert x s) p σ = (xd1, s1, p1, σ1)"
      by (cases "eval x (T x) c (insert x s) p σ")
    then show ?thesis
    proof (cases "x ∈ p")
      case True
      then show ?thesis
      proof (cases "mlup σ1 x ∇Δ xd1 = mlup σ1 x")
        case True
        then show ?thesis
          using assms dom_backwards_pinduct(2)[OF assms(1)] that(3) ev ‹x ∉ s› ‹x ∈ p›
          by simp
      next
        case False
        then show ?thesis using assms dom_backwards_pinduct(2)[OF assms(1)] ev True that(5) ‹x ∉ s›
          by fastforce
      qed
    next
      case False
      then show ?thesis
      proof (cases "xd1 = mlup σ1 x")
        case True
        then show ?thesis using assms dom_backwards_pinduct(2) that(2) ev ‹x ∉ s› False by auto
      next
        case False
        then show ?thesis using assms dom_backwards_pinduct(2) ev ‹x ∉ s› ‹x ∉ p› that(4) by simp
      qed
    qed
  qed
qed

lemma iterate_fmlookup:
  assumes "iterate_dom x c s p σ"
    and "iterate x c s p σ = (xd, s', p', σ')"
    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 Iterate
    by (cases rule: iterate_continue_fixpoint_cases) fastforce+
qed

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

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

lemma eval_query_answer_cases [consumes 2]:
  assumes "eval_dom x t c s p σ"
    and "eval x t c s p σ = (d, s', p', σ')"
  obtains (Query) y g yd s1 p1 σ1
  where "t = Query y g"
    and "query_dom x y c s p σ"
    and "query x y c s p σ = (yd, s1, p1, σ1)"
    and "eval_dom x (g yd) c s1 p1 σ1"
    and "eval x (g yd) c s1 p1 σ1 = (d, s', p', σ')"
    and "mlup σ1 y = yd"
  | (Answer) "t = Answer d"
    and "σ = σ'"
    and "s = s'"
    and "p = p'"
  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 σ ≡ (∀u∈s - c. dep T σ u ⊆ s) ∧ (∀u∈s - c. eq T u σ ≤ mlup σ u) ∧ 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 auto
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 solution_sufficient[of T] by (metis DiffD1 subsetD)
  next
    case 3 then show ?case by blast
  qed
qed

lemma partial_correctness_ind:
  shows "query_dom x y c s p σ
    ⟹ query x y c s p σ = (yd, s', p', σ')
    ⟹ invariant s c σ
    ⟹ invariant s' c σ'
      ∧ s ∪ reach_cap T σ' c y ⊆ s'
      ∧ (∀ξ ∈ s. mlup σ ξ = mlup σ' ξ)"
    and "iterate_dom x c s p σ
    ⟹ iterate x c s p σ = (xd, s', p', σ')
    ⟹ 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 p σ
    ⟹ eval x t c s p σ = (xd, s', p', σ')
    ⟹ invariant s c σ
    ⟹ invariant s' c σ'
      ∧ s ∪ reach_cap_tree T σ' c t ⊆ s'
      ∧ (∀ξ ∈ s. mlup σ ξ = mlup σ' ξ)
      ∧ traverse_rhs t σ' = xd
      ∧ dep_aux σ' t ⊆ s'"
proof(induction arbitrary: yd s' p' σ' and xd s' p' σ' and xd s' p' σ'
    rule: query_iterate_eval_pinduct)
  case (Query x c s p σ)
  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 p σ)
  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 xd1 p1)
    note IH = Iterate.IH(2)[OF Fixpoint(3,2) invariant_simp[OF Iterate.prems(2,3)], folded eq_def]
    then have "invariant s' (c - {x}) σ'"
      using Fixpoint(5)
      unfolding invariant_def dep_def
      using Diff_iff order_refl singletonD by auto
    then show ?thesis
      using IH dep_closed_implies_reach_cap_tree_closed[where ?T=T]
      unfolding invariant_def
      by auto
  next
    case (Fixpoint_W xd1 p1)
    note IH = Iterate.IH(2)[OF Fixpoint_W(3,2) invariant_simp[OF Iterate.prems(2,3)], folded eq_def]
    moreover have "xd1 ≤ mlup σ' x"
    proof (rule ccontr, goal_cases)
      case 1
      then have "mlup σ' x ∇ xd1 = mlup σ' x" using Fixpoint_W(5) unfolding warrowing_def by auto
      then have "xd1 ≤ mlup σ' x" using widening_ge by (metis le_supE)
      then show ?case using 1 by simp
    qed
    ultimately show ?thesis
      using Fixpoint_W(3,4,5) 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 xd1 s1 p1 σ1)
    note IH = Iterate.IH(2)[OF Continue(3,2) invariant_simp[OF Iterate.prems(2,3)]]

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

    note ih = Iterate.IH(3)[OF Continue(3) Continue(2)[symmetric] _ _ _ _ Continue(5,7)
        Iterate.prems(2) inv]

    then show ?thesis
      using IH mlup_eq_mupd_set[OF Continue(3), of σ] Continue(4)
      unfolding mlup_def
      by auto
  next
    case (Continue_W xd1 s1 p1 σ1 xdw)
    note IH = Iterate.IH(2)[OF Continue_W(3,2) ] invariant_simp[OF Iterate.prems(2,3)]

    have xd1_nle_lup: "xd1 ≠ mlup σ1 x"
    proof (cases "xd1 ≤ mlup σ1 x")
      case True
      then have "xdw = mlup σ1 x Δ xd1" using Continue_W(5) unfolding warrowing_def by simp
      moreover have "mlup σ1 x ⊓ xd1 = xd1" using inf_absorb2[OF True] by blast
      ultimately have "xd1 ≤ xdw ∧ xdw ≤ mlup σ1 x" using narrowing_in[of "mlup σ1 x" xd1] by auto
      then show ?thesis using Continue_W(6) by force
    next
      case False
      then have "xdw = mlup σ1 x ∇ xd1" using Continue_W(5) unfolding warrowing_def by simp
      then show ?thesis using Continue_W(6) False by auto
    qed

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

    have ih: "invariant s' (c - {x}) σ' ∧ x ∈ s' ∧ s ∪ insert x (if x ∈ c - {x} then {}
      else reach_cap_tree T σ' (insert x (c - {x})) (T x)) ⊆ s'
      ∧ (∀ξ∈s. mlup (σ1(x ↦ xdw)) ξ = mlup σ' ξ)"
      using Iterate.IH(3) Continue_W(8)  Iterate.prems(2) inv xd1_nle_lup Continue_W(2-6)
      by force

    then show ?thesis
      using IH mlup_eq_mupd_set[OF Continue_W(3), of σ]
      unfolding mlup_def
      by auto
  qed
next
  case (Eval x t c s p σ)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (Query y g yd s1 p1 σ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, p1, σ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_post_solution T x σ (reach T σ x)"
proof -
  obtain xd p' s' where it: "iterate x {x} {} {} Map.empty = (xd, s', p', σ)"
    using assms(2) unfolding solve_def by (auto split: prod.splits)
  have "(∀u∈s'. dep T σ u ⊆ s') ∧ (∀u∈s'. eq T u σ ≤ mlup σ u) ∧ reach T σ x ⊆ s'"
    using partial_correctness_ind(2)[OF assms(1)[unfolded solve_dom_def] it]
      reach_empty_capped[where ?T=T]
    unfolding invariant_def
    by simp
  then show ?thesis using reach.step reach.base by fast
qed

end
end