Theory TD_plain_widen

section ‹TD\_plain with Widening›


theory TD_plain_widen
  imports Basics
begin

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

  fixes widening :: "'d ⇒ 'd ⇒ 'd" (infixl "∇" 65)
  assumes widening_ge: "a ⊔ b ≤ a ∇ b"
    and widening_bounded: "b ≤ a ⟹ a ∇ b = a"
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 called point σ = (
    if y ∈ called then
      (mlup σ y, insert y point, σ)
    else
      iterate y (insert y called) point σ)"
| "iterate x called point σ = (
    let (d_new, point', σ) = eval x (T x) called point σ in
    let d_new' = if x ∉ point then d_new else mlup σ x ∇ d_new in
    if d_new' ≤ mlup σ x then
      (mlup σ x, Set.remove x point', σ)
    else
      iterate x called point' (σ(x ↦ d_new')))"
| "eval x t c point σ = (case t of
      Answer d ⇒ (d, point, σ)
    | Query y g ⇒ (let (yd, point, σ) = query x y c point σ in eval x (g yd) c point σ))"
  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 p σ = query_iterate_eval_dom (Inl (x, y, c, p, σ))"
declare query_dom_def [simp]
definition iterate_dom where
  "iterate_dom x c p σ = query_iterate_eval_dom (Inr (Inl (x, c, p, σ)))"
declare iterate_dom_def [simp]
definition eval_dom where
  "eval_dom x t c p σ = query_iterate_eval_dom (Inr (Inr (x, t, c, 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›

text ‹The auto-generated \texttt{pinduct} rule contains a redundant assumption. This lemma removes
this redundant assumption such that the rule is easier to instantiate and gives comprehensible
names to the cases.›

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 p σ for x y c p σ
    ]
    query_iterate_eval.pinduct(2)[
      folded query_dom_def iterate_dom_def eval_dom_def,
      of x c p σ for x c p σ
    ]
    query_iterate_eval.pinduct(3)[
      folded query_dom_def iterate_dom_def eval_dom_def,
      of x t c p σ for x t c p σ
    ]

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

(* add simps to simp set *)
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 p σ
    ⟹ y ∉ c ⟹ iterate_dom y (insert y c) p σ"
  and "iterate_dom x c p σ
    ⟹ (eval_dom x (T x) c p σ ∧
        (eval x (T x) c p σ = (xd_new, 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 p' (σ'(x ↦ xd_new'))))"
  and "eval_dom x (Query y g) c p σ
    ⟹ (query_dom x y c p σ ∧ (query x y c p σ = (yd, p', σ') ⟶ eval_dom x (g yd) c p' σ'))"
proof (induction x y c p σ and x c p σ and x "Query y g" c p σ
    arbitrary: and xd_new xd_new' xd_old p' σ' and y g yd p' σ'
    rule: query_iterate_eval_pinduct)
  case (Query x y c p σ)
  then show ?case
    using query_iterate_eval.domintros(2)[of y "insert y c" p σ, folded dom_defs] by presburger
next
  case (Iterate x c p σ)
  then show ?case
    using query_iterate_eval.domintros(2)[folded dom_defs]
      query_iterate_eval.domintros(3)[folded dom_defs] by metis
next
  case (Eval c 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 p σ"
    and "iterate x c p σ = (xd, p', σ')"
    and "x ∈ c"
  obtains (Fixpoint) xd1 p1
    where "eval_dom x (T x) c p σ"
    and "eval x (T x) c p σ = (xd1, p1, σ')"
    and "x ∉ p"
    and "xd1 ≤ mlup σ' x"
    and "p' = Set.remove x p1"
  | (Fixpoint_W) xd1 p1
    where "eval_dom x (T x) c p σ"
    and "eval x (T x) c p σ = (xd1, p1, σ')"
    and "x ∈ p"
    and "mlup σ' x ∇ xd1 ≤ mlup σ' x"
    and "p' = Set.remove x p1"
  | (Continue) xd1 p1 σ1
    where "eval_dom x (T x) c p σ"
    and "eval x (T x) c p σ = (xd1, p1, σ1)"
    and "x ∉ p"
    and "¬ xd1 ≤ mlup σ1 x"
    and "iterate_dom x c p1 (σ1(x ↦ xd1))"
    and "iterate x c p1 (σ1(x ↦ xd1)) = (xd, p', σ')"
  | (Continue_W) xd1 p1 σ1 xdw
      where "eval_dom x (T x) c p σ"
      and "eval x (T x) c p σ = (xd1, p1, σ1)"
      and "x ∈ p"
      and "xdw = mlup σ1 x ∇ xd1"
      and "¬ xdw ≤ mlup σ1 x"
      and "iterate_dom x c p1 (σ1(x ↦ xdw))"
      and "iterate x c p1 (σ1(x ↦ xdw)) = (xd, p', σ')"
proof -
  obtain xd1 p1 σ1 xd2 where ev: "eval x (T x) c p σ = (xd1, p1, σ1)"
    and w: "xd2 = (if x ∉ p then xd1 else mlup σ1 x ∇ xd1)"
   by (cases "eval x (T x) c p σ", simp)
  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) that(2) ev ‹x ∈ p› by simp
    next
      case False
      then show ?thesis using assms dom_backwards_pinduct(2) ev True that(4) by simp
    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(1) ev False by auto
    next
      case False
      then show ?thesis using assms dom_backwards_pinduct(2) that(1) ev ‹x ∉ p› that(3) by simp
    qed
  qed
qed

lemma iterate_fmlookup:
  assumes "iterate_dom x c p σ"
    and "iterate x c p σ = (xd, p', σ')"
    and "x ∈ c"
  shows "mlup σ' x = xd"
  using assms
proof(induction rule: iterate_pinduct)
  case (Iterate x c p σ)
  show ?case
    using Iterate.hyps Iterate.prems
  proof (cases rule: iterate_continue_fixpoint_cases)
    case (Fixpoint xd1 p1)
    then show ?thesis using Iterate.hyps Iterate.prems(1) by auto
  next
    case (Fixpoint_W xd1 p1)
    then show ?thesis using Iterate.hyps Iterate.prems(1) by auto
  next
    case (Continue xd1 p1 σ1)
    then show ?thesis using Iterate.IH Iterate.prems(2) by force
  next
    case (Continue_W xd1 p1 σ1 xdw)
    then show ?thesis using Iterate.IH Iterate.prems(2) by force
  qed
qed

corollary query_fmlookup:
  assumes "query_dom x y c p σ"
    and "query x y c p σ = (yd, p', σ')"
  shows "mlup σ' y = yd"
  using assms iterate_fmlookup dom_backwards_pinduct(1) query.psimps[folded dom_defs, OF assms(1)]
  by (metis insertCI prod.inject)

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

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


subsection ‹Partial correctness proofs›

abbreviation part_post_solution where
  "part_post_solution σ vars ≡ (∀x ∈ vars. eq T x σ ≤ mlup σ x)"

text‹Invariant for induction proof›

definition invariant where
  "invariant s c σ ≡ (∀ξ∈s - c. dep T σ ξ ⊆ s) ∧ part_post_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[of T] by blast
  next
    case 2 then show ?case
      using part_solution_coinciding_sigma_called[where ?T=T] solution_sufficient[of T]
      by (metis DiffD1 subsetD)
  qed
qed

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

    have x_not_stable: "x ∉ s"
    proof
      assume assm: "x ∈ s"
      have "∀y∈dep T σ x. mlup σ y = mlup σ1 y"
        using Iterate.prems(3) assm IH
        unfolding invariant_def by blast
      then have "xd1 ≤ mlup σ x"
        using solution_sufficient Iterate.prems(3) assm IH
        unfolding invariant_def
        by (metis Diff_iff eq_def insertCI)
      then show False using IH Continue by force
    qed

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

    have ih: "invariant (s ∪ insert x (if x ∈ c - {x} then {}
      else reach_cap_tree T σ' (insert x (c - {x})) (T x))) (c - {x}) σ'
      ∧ (∀ξ∈s. mlup (σ1(x ↦ xd1)) ξ = mlup σ' ξ)"
      using Iterate.IH(3) Iterate.prems(2) inv Continue(2-4,6) by force
    then show ?thesis
      using IH mlup_eq_mupd_set[OF x_not_stable, of σ]
      unfolding mlup_def
      by auto
  next
    case (Fixpoint_W xd1 p1)
    note IH = Iterate.IH(2)[OF Fixpoint_W(2) invariant_simp[OF Iterate.prems(2,3)], folded eq_def]
    moreover have "xd1 ≤ mlup σ' x" using Fixpoint_W(4) widening_ge
      by (meson le_sup_iff order.trans)
    ultimately show ?thesis
      using Iterate.prems(2) reach_cap_tree_simp2[of x "c - {x}" T]
        dep_subset_reach_cap_tree[of σ' "T x" T, folded dep_def] widening_ge
      unfolding invariant_def
      by (auto simp add: insert_absorb)
  next
    case (Continue_W xd1 p1 σ1 xdw)
    note IH = Iterate.IH(2)[OF Continue_W(2) invariant_simp[OF Iterate.prems(2,3)]]

    have xd1_nle_lup: "¬ xd1 ≤ mlup σ1 x" using Continue_W(4,5) widening_bounded by force

    have x_not_stable: "x ∉ s"
    proof
      assume assm: "x ∈ s"
      have "∀y∈dep T σ x. mlup σ y = mlup σ1 y"
        using Iterate.prems(3) assm IH
        unfolding invariant_def by blast
      then have "eq T x σ = eq T x σ1" using solution_sufficient by simp
      then have "xd1 ≤ mlup σ1 x"
        using IH Iterate.prems(3) assm eq_def unfolding invariant_def by auto
      then show False using xd1_nle_lup by simp
    qed

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

    have ih: "invariant (s ∪ insert x (if x ∈ c - {x} then {}
      else reach_cap_tree T σ' (insert x (c - {x})) (T x))) (c - {x}) σ'
      ∧ (∀ξ∈s. mlup (σ1(x ↦ xdw)) ξ = mlup σ' ξ)"
      using Iterate.IH(3) Continue_W(2-5,7) Iterate.prems(2) inv'
      by force
    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 p σ)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (Query y g yd 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], simplified]
    show ?thesis
      using Query IH ih reach_cap_tree_step[where ?T=T]
        reach_cap_tree_eq[of T σ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

corollary partial_correctness:
  assumes "solve_dom x"
    and "solve x = σ"
  shows "part_post_solution σ (reach T σ x)"
proof -
  obtain xd p where "iterate x {x} {} Map.empty = (xd, p, σ)"
    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] reach_empty_capped[of T]
    unfolding solve_dom_def invariant_def by auto
qed


end
end