Theory TD_wn_wo_opt
section ‹TD with Widening/Narrowing Phases per Unknown›
theory TD_wn_wo_opt
imports Basics TD_wn_post_wo_opt
begin
locale TD_wn_wo_opt =
fixes T :: "('x, 'd :: bounded_lattice_bot) eqsT"
fixes widening :: "'d ⇒ 'd ⇒ 'd" (infixl "∇" 65)
and narrowing :: "'d ⇒ 'd ⇒ 'd" (infixl "Δ" 70)
begin
subsection ‹Definitions›
function (domintros)
query :: "'x ⇒ 'x ⇒ 'x set ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map
⇒ 'd × ('x, 'x list) fmap × 'x set × 'x set × ('x, 'd) map" and
iterate :: "'x ⇒ 'x set ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map ⇒ phase
⇒ 'd × ('x, 'x list) fmap × 'x set × 'x set × ('x, 'd) map" and
eval :: "'x ⇒ ('x, 'd) strategy_tree ⇒ 'x set ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'x set
⇒ ('x, 'd) map ⇒ 'd × ('x, 'x list) fmap × 'x set × 'x set × ('x, 'd) map"
where
"query y x c infl stabl p σ = (
let (xd, infl, stabl, p, σ) =
if x ∈ c then
(mlup σ x, infl, stabl, insert x p, σ)
else
iterate x (insert x c) infl stabl p σ Widening
in (xd, fminsert infl x y, stabl, p, σ))"
| "iterate x c infl stabl p σ wn = (
if x ∉ stabl then (
let (xd, infl, stabl, p', σ) = eval x (T x) c infl (insert x stabl) p σ in
let d_new = if x ∉ p then xd else if wn = Widening then mlup σ x ∇ xd else mlup σ x Δ xd in
if mlup σ x = d_new then (
if x ∈ p ∧ wn = Widening then (
let (infl, stabl) = destab x infl stabl in
iterate x c infl stabl p' σ Narrowing)
else (mlup σ x, infl, stabl, Set.remove x p', σ))
else (
let (infl, stabl) = destab x infl stabl in
iterate x c infl stabl p' (σ(x ↦ d_new)) wn))
else
(mlup σ x, infl, stabl, Set.remove x p, σ))"
| "eval x t c infl stabl p σ = (case t of
Answer d ⇒ (d, infl, stabl, p, σ)
| Query y g ⇒ (
let (yd, infl, stabl, p, σ) = query x y c infl stabl p σ in
eval x (g yd) c infl stabl p σ))"
by pat_completeness auto
definition solve :: "'x ⇒ 'x set × ('x, 'd) map" where
"solve x = (let (_, _, stabl, _, σ) = iterate x {x} fmempty {} {} Map.empty Widening in (stabl, σ))"
definition query_dom where
"query_dom y x c infl stabl p σ = query_iterate_eval_dom (Inl (y, x, c, infl, stabl, p, σ))"
declare query_dom_def [simp]
definition iterate_dom where
"iterate_dom x c infl stabl p σ wn = query_iterate_eval_dom (Inr (Inl (x, c, infl, stabl, p, σ, wn)))"
declare iterate_dom_def [simp]
definition eval_dom where
"eval_dom x t c infl stabl p σ = query_iterate_eval_dom (Inr (Inr (x, t, c, infl, stabl, p, σ)))"
declare eval_dom_def [simp]
definition solve_dom where
"solve_dom x = iterate_dom x {x} fmempty {} {} Map.empty Widening"
lemmas dom_defs = query_dom_def iterate_dom_def eval_dom_def
subsubsection ‹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 y x c infl stabl p σ for y x c infl stabl p σ
]
query_iterate_eval.pinduct(2)[
folded query_dom_def iterate_dom_def eval_dom_def,
of x c infl stabl p σ wn for x c infl stabl p σ wn
]
query_iterate_eval.pinduct(3)[
folded query_dom_def iterate_dom_def eval_dom_def,
of x t c infl stabl p σ for x t c infl stabl p σ
]
declare query.psimps [simp]
declare iterate.psimps [simp]
declare eval.psimps [simp]
subsubsection ‹Domain lemmas›
lemma dom_backwards_pinduct:
shows "query_dom y x c infl stabl p σ
⟹ x ∉ c ⟹ iterate_dom x (insert x c) infl stabl p σ Widening"
and "iterate_dom x c infl stabl p σ wn
⟹ x ∉ stabl ⟹ (eval_dom x (T x) c infl (insert x stabl) p σ ∧
((xd, infl1, stabl1, p1, σ1) = eval x (T x) c infl (insert x stabl) p σ
⟶ d_new = (if x ∉ p then xd else if wn = Widening then mlup σ1 x ∇ xd else mlup σ1 x Δ xd)
⟶ (mlup σ1 x = d_new ⟶ x ∈ p ⟶ wn = Widening ⟶ (infl2, stabl2) = destab x infl1 stabl1
⟶ iterate_dom x c infl2 stabl2 p1 σ1 Narrowing)
∧ (mlup σ1 x ≠ d_new ⟶ (infl2, stabl2) = destab x infl1 stabl1 ⟶
iterate_dom x c infl2 stabl2 p1 (σ1(x ↦ d_new)) wn)))"
and "eval_dom x (Query y g) c infl stabl p σ
⟹ (query_dom x y c infl stabl p σ ∧
((yd, infl', stabl', p', σ') = query x y c infl stabl p σ ⟶
eval_dom x (g yd) c infl' stabl' p' σ'))"
proof (induction y x c infl stabl p σ and x c infl stabl p σ wn
and x "Query y g" c infl stabl p σ
arbitrary: and xd infl1 stabl1 p1 σ1 d_new infl2 stabl2 and y g yd infl' stabl' p' σ'
rule: query_iterate_eval_pinduct)
case (Query y x c infl stabl p σ)
then show ?case using query_iterate_eval.domintros(2) by (auto, presburger)
next
case (Iterate x c infl stabl p σ wn)
have eval_dom: "eval_dom x (T x) c infl (insert x stabl) p σ"
using Iterate.hyps(2) Iterate.prems query_iterate_eval.domintros(3) by force
show ?case
proof (intro impI conjI, goal_cases)
case 1
then show ?case using eval_dom by force
next
case 2
have B: "x ∈ p ∧ wn = Widening" using 2(4,5) by simp
show ?case
using Iterate.hyps(3)[OF Iterate.prems 2(1) _ _ _ _ 2(2,3) B 2(6), simplified]
query_iterate_eval.domintros(2)[folded dom_defs, of x stabl2 c infl2 p1 σ1 Narrowing]
by fastforce
next
case 3
show ?case
using Iterate.hyps(4)[OF Iterate.prems 3(1) _ _ _ _ 3(2-4), of _ _ _ _ infl2, simplified]
iterate_dom_def query_iterate_eval.domintros(2)[of x stabl2 c infl2 p1 "σ1(x ↦ d_new)" wn]
by presburger
qed
next
case (Eval x c infl stabl p σ)
then show ?case using query_iterate_eval.domintros(1,3) by simp
qed
subsubsection ‹Case rules›
lemma iterate_continue_fixpoint_cases[consumes 3]:
assumes "iterate_dom x c infl stabl p σ wn"
and "(xd, infl', stabl', p', σ') = iterate x c infl stabl p σ wn"
and "x ∈ c"
obtains (Stable) "x ∈ stabl"
and "xd = mlup σ x"
and "infl' = infl"
and "stabl' = stabl"
and "p' = Set.remove x p"
and "σ' = σ"
| (Fixpoint) p1
where "x ∉ stabl" and "x ∉ p"
and "eval_dom x (T x) c infl (insert x stabl) p σ"
and "(xd, infl', stabl', p1, σ') = eval x (T x) c infl (insert x stabl) p σ"
and "mlup σ' x = xd"
and "p' = Set.remove x p1"
| (W_Fixpoint) xd1 infl1 stabl1 p1 σ1 infl2 stabl2
where "x ∉ stabl" and "x ∈ p" and "wn = Widening"
and "eval_dom x (T x) c infl (insert x stabl) p σ"
and "(xd1, infl1, stabl1, p1, σ1) = eval x (T x) c infl (insert x stabl) p σ"
and "mlup σ1 x = mlup σ1 x ∇ xd1"
and "(infl2, stabl2) = destab x infl1 stabl1"
and "iterate_dom x c infl2 stabl2 p1 σ1 Narrowing"
and "(xd, infl', stabl', p', σ') = iterate x c infl2 stabl2 p1 σ1 Narrowing"
| (N_Fixpoint) xd1 p1
where "x ∉ stabl" and "x ∈ p" and "wn = Narrowing"
and "eval_dom x (T x) c infl (insert x stabl) p σ"
and "(xd1, infl', stabl', p1, σ') = eval x (T x) c infl (insert x stabl) p σ"
and "xd = mlup σ' x Δ xd1"
and "mlup σ' x = xd"
and "p' = Set.remove x p1"
| (Continue) xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2
where "x ∉ stabl"
and "eval_dom x (T x) c infl (insert x stabl) p σ"
and "(xd1, infl1, stabl1, p1, σ1) = eval x (T x) c infl (insert x stabl) p σ"
and "d_new = (if x ∉ p then xd1 else if wn = Widening then mlup σ1 x ∇ xd1 else mlup σ1 x Δ xd1)"
and "mlup σ1 x ≠ d_new"
and "(infl2, stabl2) = destab x infl1 stabl1"
and "iterate_dom x c infl2 stabl2 p1 (σ1(x ↦ d_new)) wn"
and "(xd, infl', stabl', p', σ') = iterate x c infl2 stabl2 p1 (σ1(x ↦ d_new)) wn"
proof(cases "x ∈ stabl" rule: case_split[case_names Stable Unstable])
case Stable
then show ?thesis using that(1) assms(1,2) by auto
next
case Unstable
then have sldom: "eval_dom x (T x) c infl (insert x stabl) p σ"
using assms(1) dom_backwards_pinduct(2)
by simp
then obtain xd1 infl1 stabl1 p1 σ1
where slapp: "eval x (T x) c infl (insert x stabl) p σ = (xd1, infl1, stabl1, p1, σ1)"
by (cases "eval x (T x) c infl (insert x stabl) p σ") auto
then obtain d_new where d_new:
"d_new = (if x ∉ p then xd1 else if wn = Widening then mlup σ1 x ∇ xd1 else mlup σ1 x Δ xd1)"
by blast
show ?thesis
proof (cases "mlup σ1 x = d_new" rule: case_split[case_names Fixpoint Continue])
case Fixpoint
then show ?thesis
proof (cases "x ∈ p")
case True
then show ?thesis
proof (cases wn)
case Widening
obtain infl2 stabl2 where destab: "destab x infl1 stabl1 = (infl2, stabl2)"
by (cases "destab x infl1 stabl1")
have "d_new = mlup σ1 x ∇ xd1" using d_new Widening True by simp
moreover have "iterate x c infl stabl p σ wn = iterate x c infl2 stabl2 p1 σ1 Narrowing"
using assms iterate.psimps[folded dom_defs, OF assms(1)] Unstable slapp Fixpoint d_new Widening
True destab
by force
moreover have "iterate_dom x c infl2 stabl2 p1 σ1 Narrowing"
using Unstable slapp Fixpoint d_new Widening True assms(1) dom_backwards_pinduct(2) destab
by presburger
ultimately show ?thesis
using assms(2) Fixpoint that(3)[OF Unstable True Widening sldom slapp[symmetric]] destab by simp
next
case Narrowing
have "d_new = mlup σ1 x Δ xd1" using d_new Narrowing True by simp
moreover have "iterate x c infl stabl p σ wn = (mlup σ1 x, infl1, stabl1,
Set.remove x p1, σ1)"
using assms iterate.psimps[folded dom_defs, OF assms(1)] Unstable slapp Fixpoint d_new Narrowing
True
by fastforce
ultimately show ?thesis
using Unstable sldom slapp d_new assms that(4)[OF Unstable True Narrowing sldom _] Fixpoint
by auto
qed
next
case False
have "iterate x c infl stabl p σ wn = (mlup σ1 x, infl1, stabl1, Set.remove x p1, σ1)"
using assms iterate.psimps[folded dom_defs, OF assms(1)] Unstable slapp Fixpoint d_new False
by simp
then show ?thesis
using Unstable sldom slapp d_new assms that(2)[OF Unstable False sldom] False Fixpoint
by auto
qed
next
case Continue
obtain infl2 stabl2 where destab: "destab x infl1 stabl1 = (infl2, stabl2)"
by (cases "destab x infl1 stabl1")
then have dom: "iterate_dom x c infl2 stabl2 p1 (σ1(x ↦ d_new)) wn"
using Unstable Continue slapp d_new assms(1) dom_backwards_pinduct(2) by auto
then show ?thesis
using Unstable Continue sldom slapp d_new assms destab that(3,5)
by (cases "x ∈ p") (auto simp add: Let_def)
qed
qed
lemma query_iterate_lookup_cases[consumes 2]:
assumes "query_dom y x c infl stabl p σ"
and "(xd, infl', stabl', p', σ') = query y x c infl stabl p σ"
obtains (Iterate) infl1
where "x ∉ c"
and "iterate_dom x (insert x c) infl stabl p σ Widening"
and "(xd, infl1, stabl', p', σ') = iterate x (insert x c) infl stabl p σ Widening"
and "infl' = fminsert infl1 x y"
| (Lookup) "x ∈ c"
and "xd = mlup σ x"
and "infl' = fminsert infl x y"
and "stabl' = stabl"
and "p' = insert x p"
and "σ' = σ"
using assms that dom_backwards_pinduct(1)
by (cases "x ∈ c"; auto split: prod.splits)
lemma eval_query_answer_cases[consumes 2]:
assumes "eval_dom x t c infl stabl p σ"
and "(xd, infl', stabl', p', σ') = eval x t c infl stabl p σ"
obtains (Query) y g yd infl1 stabl1 p1 σ1
where "t = Query y g"
and "query_dom x y c infl stabl p σ"
and "(yd, infl1, stabl1, p1, σ1) = query x y c infl stabl p σ"
and "eval_dom x (g yd) c infl1 stabl1 p1 σ1"
and "(xd, infl', stabl', p', σ') = eval x (g yd) c infl1 stabl1 p1 σ1"
| (Answer) "t = Answer xd"
and "infl' = infl"
and "stabl' = stabl"
and "p' = p"
and "σ' = σ"
using assms dom_backwards_pinduct(3) that
by (cases t; auto split: prod.splits)
subsection ‹Equivalence Proofs›
text‹In this section, we prove the equivalence of the TD with w/n and the annotated TD with w/n and
explicit tracking of post unknowns. This is then used to prove the correctness of the TD with w/n.›
interpretation TD_post: TD_wn_post_wo_opt T "(∇)" "(Δ)"
done
context
assumes widening_ge: "a ⊔ b ≤ a ∇ b"
and widening_bounded: "b ≤ a ⟹ a ∇ b = a"
and narrowing_ge: "a ⊓ b ≤ a Δ b"
and narrowing_le: "a Δ b ≤ a"
begin
lemma equiv_post_solver_aux_1:
shows "query_dom y x c infl stabl p σ
⟹ (xd, infl', stabl', p', σ') = query y x c infl stabl p σ
⟹ c⇩w ∪ c⇩n = c
⟹ ∃pinfl' post'. TD_post.query_dom y x c⇩w c⇩n infl stabl p σ pinfl post
∧ (xd, infl', stabl', p', σ', pinfl', post')
= TD_post.query y x c⇩w c⇩n infl stabl p σ pinfl post"
and "iterate_dom x c infl stabl p σ wn
⟹ (xd, infl', stabl', p', σ') = iterate x c infl stabl p σ wn
⟹ x ∈ c
⟹ c⇩w ∪ c⇩n = c
⟹ ∃pinfl' post'. TD_post.iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post
∧ (xd, infl', stabl', p', σ', pinfl', post')
= TD_post.iterate x c⇩w c⇩n infl stabl p σ wn pinfl post"
and "eval_dom x t c infl stabl p σ
⟹ (xd, infl', stabl', p', σ') = eval x t c infl stabl p σ
⟹ c⇩w ∪ c⇩n = c
⟹ ∃pinfl' post'. TD_post.eval_dom x t c⇩w c⇩n infl stabl p σ pinfl post
∧ (xd, infl', stabl', p', σ', pinfl', post')
= TD_post.eval x t c⇩w c⇩n infl stabl p σ pinfl post"
proof (induction y x c infl stabl p σ and x c infl stabl p σ wn and x t c infl stabl p σ
arbitrary: xd infl' stabl' p' σ' c⇩w c⇩n post pinfl and xd infl' stabl' p' σ' c⇩w c⇩n post pinfl
and xd infl' stabl' p' σ' c⇩w c⇩n post pinfl rule: query_iterate_eval_pinduct)
case (Query y x c infl stabl p σ)
show ?case using Query.IH(1) Query.prems(1)
proof(cases rule: query_iterate_lookup_cases)
case (Iterate infl1)
obtain c1⇩w c1⇩n where
c1_defs: "(c1⇩w, c1⇩n) = (if x ∈ post then (c⇩w, insert x c⇩n) else (insert x c⇩w, c⇩n))"
by fastforce
have "c1⇩w ∪ c1⇩n = insert x c"
using Iterate(1) Query.prems c1_defs by (auto split: if_splits)
then obtain pinfl1 post' where it_dom: "TD_post.iterate_dom x c1⇩w c1⇩n infl stabl p σ Widening pinfl post"
and it_val: "(xd, infl1, stabl', p', σ', pinfl1, post')
= TD_post.iterate x c1⇩w c1⇩n infl stabl p σ Widening pinfl post"
using Query.IH(2)[OF Iterate(1,3), of c1⇩w c1⇩n] by blast
have q_dom: "TD_post.query_dom y x c⇩w c⇩n infl stabl p σ pinfl post"
using TD_post.query_iterate_eval.domintros(1)[of x post c⇩w c⇩n] c1_defs Iterate(1) it_dom
by (auto split: if_splits)
then have "(xd, fminsert infl1 x y, stabl', p', σ', fminsert pinfl1 x y, post')
= TD_post.query y x c⇩w c⇩n infl stabl p σ pinfl post"
using TD_post.query.psimps Iterate(1) Query.prems(2) c1_defs it_val
by (auto split: prod.splits)
then show ?thesis using q_dom Iterate(4) by blast
next
case Lookup
then show ?thesis
using Query.prems(2) TD_post.query_iterate_eval.domintros(1)[of x post c⇩w c⇩n] by auto
qed
next
case (Iterate x c infl stabl p σ wn)
show ?case using Iterate.IH(1) Iterate.prems(1,2)
proof (cases rule: iterate_continue_fixpoint_cases)
case Stable
then show ?thesis using TD_post.query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n] by simp
next
case (Fixpoint p1)
obtain pinfl' post' where e_dom:
"TD_post.eval_dom x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
and e_val: "(xd, infl', stabl', p1, σ', pinfl', post')
= TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
using Iterate(2)[OF Fixpoint(1,4) Iterate.prems(3)] by blast
then have i_dom: "TD_post.iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post"
using TD_post.query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post]
Fixpoint(1,2,5)
by (cases "TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
then have i_val: "(mlup σ' x, infl', stabl', Set.remove x p1, σ', pinfl', post')
= TD_post.iterate x c⇩w c⇩n infl stabl p σ wn pinfl post"
using Fixpoint(1,2,5) TD_post.iterate.psimps[folded TD_post.dom_defs, OF i_dom] e_val
by (cases "TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
then show ?thesis using Fixpoint(5,6) i_val i_dom by blast
next
case (W_Fixpoint xd1 infl1 stabl1 p1 σ1 infl2 stabl2)
obtain pinfl1 post1 where e_dom:
"TD_post.eval_dom x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
and e_val: "(xd1, infl1, stabl1, p1, σ1, pinfl1, post1)
= TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
using Iterate(2)[OF W_Fixpoint(1,5) Iterate.prems(3)] by blast
have "Set.remove x c⇩w ∪ insert x c⇩n = c"
using Iterate.prems(2-3) by fastforce
then obtain pinfl' post' where i2_dom:
"TD_post.iterate_dom x (Set.remove x c⇩w) (insert x c⇩n) infl2 stabl2 p1 σ1 Narrowing pinfl1 post1"
and i2_val: "(xd, infl', stabl', p', σ', pinfl', post') =
TD_post.iterate x (Set.remove x c⇩w) (insert x c⇩n) infl2 stabl2 p1 σ1 Narrowing pinfl1 post1"
using Iterate.IH(3)[OF W_Fixpoint(1,5) _ _ _ _ _ W_Fixpoint(6) _ W_Fixpoint(7) _
W_Fixpoint(9), of _ _ _ _ "Set.remove x c⇩w" "insert x c⇩n" pinfl1 post1] Iterate.prems(2,3)
W_Fixpoint by presburger
have i_dom: "TD_post.iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post"
using TD_post.query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post wn]
e_dom e_val i2_dom W_Fixpoint(1-3,6,7)
by (cases "TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
cases "destab x infl1 stabl1") simp
then show ?thesis
using TD_post.iterate.psimps[folded TD_post.dom_defs, OF i_dom] W_Fixpoint(1-3,6,7) e_val i2_val
by (cases "TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
cases "destab x infl1 stabl1") fastforce
next
case (N_Fixpoint xd1 p1)
obtain pinfl1 post1 where e_dom:
"TD_post.eval_dom x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
and e_val: "(xd1, infl', stabl', p1, σ', pinfl1, post1)
= TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
using Iterate(2)[OF N_Fixpoint(1,5) Iterate.prems(3)] by blast
then have i_dom: "TD_post.iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post"
using TD_post.query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post]
N_Fixpoint(1-3,6,7)
by (cases "TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
then have i_val: "(mlup σ' x, infl', stabl', Set.remove x p1, σ', pinfl1, post1)
= TD_post.iterate x c⇩w c⇩n infl stabl p σ wn pinfl post"
using N_Fixpoint(1-3,6,7) e_val
by (cases "TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
then show ?thesis using i_dom N_Fixpoint(7,8) by blast
next
case (Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2)
obtain pinfl1 post1 where e_dom:
"TD_post.eval_dom x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
and e_val: "(xd1, infl1, stabl1, p1, σ1, pinfl1, post1)
= TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
using Iterate(2)[OF Continue(1,3) Iterate.prems(3)] by blast
obtain pinfl2 post2 where destab_post:
"(pinfl2, post2) = TD_post.destab_post x post pinfl1 post1 stabl2"
by (cases "TD_post.destab_post x post pinfl1 post1 stabl2") fastforce
obtain pinfl' post' where i2_dom:
"TD_post.iterate_dom x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ d_new)) wn pinfl2 post2"
and i2_val: "(xd, infl', stabl', p', σ', pinfl', post') =
TD_post.iterate x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ d_new)) wn pinfl2 post2"
using Iterate.IH(4) Continue Iterate.prems(2-3) by presburger
have i_dom: "TD_post.iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post"
using TD_post.query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post wn]
e_dom e_val i2_dom Continue(1-2,4-6) destab_post
by (cases "TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
cases "destab x infl1 stabl1", cases "TD_post.destab_post x post pinfl1 post1
stabl2") (auto split: if_splits)
then show ?thesis
using TD_post.iterate.psimps[folded TD_post.dom_defs, OF i_dom] Continue(1-2,4-6) e_val
i2_val destab_post by (cases "TD_post.eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl
(insert x post)", cases "destab x infl1 stabl1", cases "TD_post.destab_post x post
pinfl1 post1 stabl2") (fastforce split: if_splits)
qed
next
case (Eval x t c infl stabl p σ)
show ?case using Eval.IH(1)Eval.prems(1)
proof (cases rule: eval_query_answer_cases)
case (Query y g yd infl1 stabl1 p1 σ1)
obtain pinfl1 post1 where Q: "TD_post.query_dom x y c⇩w c⇩n infl stabl p σ pinfl post ∧
(yd, infl1, stabl1, p1, σ1, pinfl1, post1)
= TD_post.query x y c⇩w c⇩n infl stabl p σ pinfl post"
using Eval(2)[OF Query(1,3) Eval.prems(2)] by blast
obtain pinfl' post' where E: "TD_post.eval_dom x (g yd) c⇩w c⇩n infl1 stabl1 p1 σ1 pinfl1 post1 ∧
(xd, infl', stabl', p', σ', pinfl', post')
= TD_post.eval x (g yd) c⇩w c⇩n infl1 stabl1 p1 σ1 pinfl1 post1"
using Eval(3)[OF Query(1,3) _ _ _ _ Query(5) Eval.prems(2)] by metis
have "TD_post.eval_dom x t c⇩w c⇩n infl stabl p σ pinfl post"
using Q E TD_post.query_iterate_eval.domintros(3)[of t x c⇩w c⇩n] Query(1)
by (cases "TD_post.query x y c⇩w c⇩n infl stabl p σ pinfl post") fastforce
then show ?thesis using TD_post.eval.psimps[folded TD_post.dom_defs] Query(1) Q E
by (cases "TD_post.query x y c⇩w c⇩n infl stabl p σ pinfl post") fastforce
next
case Answer
then show ?thesis using TD_post.query_iterate_eval.domintros(3) by fastforce
qed
qed
corollary TD_wn_TD_wn_post_equivalence:
assumes "solve_dom x"
and "solve x = (stabl, σ)"
shows "TD_post.solve_dom x ∧ TD_post.solve x = (stabl, σ)"
proof -
obtain xd infl p where "(xd, infl, stabl, p, σ) = iterate x {x} fmempty {} {} (λx. None) Widening"
using assms(2) unfolding solve_def by (auto split: prod.splits)
then obtain pinfl post where "TD_post.iterate_dom x {x} {} fmempty {} {} (λx. None) Widening fmempty {}"
"(xd, infl, stabl, p, σ, pinfl, post) = TD_post.iterate x {x} {} fmempty {} {} (λx. None) Widening fmempty {}"
using equiv_post_solver_aux_1(2)[where c⇩w = "{x}" and c⇩n ="{}"] assms(1)
unfolding solve_dom_def by blast
then show ?thesis unfolding TD_post.solve_dom_def TD_post.solve_def by (auto split: prod.splits)
qed
lemma equiv_post_solver_aux_2:
shows "TD_post.query_dom y x c⇩w c⇩n infl stabl p σ pinfl post
⟹ (xd, infl', stabl', p', σ', pinfl', post') =
TD_post.query y x c⇩w c⇩n infl stabl p σ pinfl post
⟹ query_dom y x (c⇩w ∪ c⇩n) infl stabl p σ
∧ (xd, infl', stabl', p', σ') = query y x (c⇩w ∪ c⇩n) infl stabl p σ"
and "TD_post.iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post
⟹ (xd, infl', stabl', p', σ', pinfl', post') =
TD_post.iterate x c⇩w c⇩n infl stabl p σ wn pinfl post
⟹ x ∈ c⇩w ∪ c⇩n
⟹ iterate_dom x (c⇩w ∪ c⇩n) infl stabl p σ wn
∧ (xd, infl', stabl', p', σ') = iterate x (c⇩w ∪ c⇩n) infl stabl p σ wn"
and "TD_post.eval_dom x t c⇩w c⇩n infl stabl p σ pinfl post
⟹ (xd, infl', stabl', p', σ', pinfl', post') = TD_post.eval x t c⇩w c⇩n infl stabl p σ pinfl post
⟹ eval_dom x t (c⇩w ∪ c⇩n) infl stabl p σ
∧ (xd, infl', stabl', p', σ') = eval x t (c⇩w ∪ c⇩n) infl stabl p σ"
proof(induction y x c⇩w c⇩n infl stabl p σ pinfl post and x c⇩w c⇩n infl stabl p σ wn pinfl post
and y t c⇩w c⇩n infl stabl p σ pinfl post arbitrary: xd infl' stabl' p' σ' pinfl' post'
and xd infl' stabl' p' σ' pinfl' post' and xd infl' stabl' p' σ' pinfl' post'
rule: TD_post.query_iterate_eval_pinduct)
case (Query y x c⇩w c⇩n infl stabl p σ pinfl post)
show ?case using Query.IH(1) Query.prems(1)
proof(cases rule: TD_post.query_iterate_lookup_cases)
case (Iterate infl1 pinfl1 c1⇩w c1⇩n)
have IH: "iterate_dom x (c1⇩w ∪ c1⇩n) infl stabl p σ Widening"
"(xd, infl1, stabl', p', σ') = iterate x (c1⇩w ∪ c1⇩n) infl stabl p σ Widening"
using Query.IH(2) Iterate(1,3,4) by (auto split: if_splits)
then have "query_dom y x (c⇩w ∪ c⇩n) infl stabl p σ"
using query_iterate_eval.domintros(1)[of x "c⇩w ∪ c⇩n"] Iterate(1,4) by (auto split: if_splits)
then show ?thesis
using query.psimps[folded dom_defs] Iterate(1,4) IH(2) Iterate(5)
by (auto split: prod.splits if_splits)
next
case Lookup
then show ?thesis using query_iterate_eval.domintros(1)[of x "c⇩w ∪ c⇩n"] by auto
qed
next
case (Iterate x c⇩w c⇩n infl stabl p σ wn pinfl post)
show ?case using Iterate.IH(1) Iterate.prems(1,2)
proof(cases rule: TD_post.iterate_continue_fixpoint_cases)
case Stable
then show ?thesis using query_iterate_eval.domintros(2)[of x stabl] by fastforce
next
case (Fixpoint p1)
have IH1: "eval_dom x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ"
"(xd, infl', stabl', p1, σ') = eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ"
using Iterate.IH(2)[OF Fixpoint(1,4)] by auto
have "iterate_dom x (c⇩w ∪ c⇩n) infl stabl p σ wn"
using Fixpoint(1,2,5) IH1 query_iterate_eval.domintros(2)[of x stabl "c⇩w ∪ c⇩n" infl p σ wn]
by (cases "eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ") auto
then show ?thesis
using iterate.psimps[of x "c⇩w ∪ c⇩n" infl stabl p σ wn] IH1 Fixpoint(1,2,5,6)
by (cases "eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ") simp
next
case (W_Fixpoint xd1 infl1 stabl1 p1 σ1 infl2 stabl2 pinfl1 post1)
have IH1: "eval_dom x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ"
"(xd1, infl1, stabl1, p1, σ1) = eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ"
using Iterate.IH(2)[OF W_Fixpoint(1,5)] by auto
have "Set.remove x c⇩w ∪ insert x c⇩n = c⇩w ∪ c⇩n" using Iterate.prems(2) by auto
then have IH2: "iterate_dom x (c⇩w ∪ c⇩n) infl2 stabl2 p1 σ1 Narrowing"
"(xd, infl', stabl', p', σ') = iterate x (c⇩w ∪ c⇩n) infl2 stabl2 p1 σ1 Narrowing"
using Iterate.IH(3) W_Fixpoint(1-3,5-7,9) Iterate.prems(2) by auto
have "iterate_dom x (c⇩w ∪ c⇩n) infl stabl p σ wn"
using W_Fixpoint(1-3,6,7) IH1 IH2(1) Iterate.prems(2) query_iterate_eval.domintros(2)[of x
stabl "c⇩w ∪ c⇩n" infl p σ] by (cases "eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ",
cases "destab x infl1 stabl1", cases wn) auto
then show ?thesis using iterate.psimps[folded dom_defs] W_Fixpoint(1,2,3,6,7) IH1(2) IH2(2)
by (cases "eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ", cases
"destab x infl1 stabl1") simp
next
case (N_Fixpoint xd1 p1)
have IH1: "eval_dom x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ"
"(xd1, infl', stabl', p1, σ') = eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ"
using Iterate.IH(2)[OF N_Fixpoint(1,5)] by auto
have "iterate_dom x (c⇩w ∪ c⇩n) infl stabl p σ wn"
using N_Fixpoint(1-3,6-7) IH1 query_iterate_eval.domintros(2)[of x stabl "c⇩w ∪ c⇩n" infl p σ]
by (cases "eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ") auto
then show ?thesis
using iterate.psimps[of x "c⇩w ∪ c⇩n" infl stabl p σ wn] IH1 N_Fixpoint(1-3,6-8)
by (cases "eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ") simp
next
case (Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2 pinfl1 post1 pinfl2 post2)
have IH1: "eval_dom x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ"
"(xd1, infl1, stabl1, p1, σ1) = eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ"
using Iterate.IH(2)[OF Continue(1,3)] by auto
have IH2: "iterate_dom x (c⇩w ∪ c⇩n) infl2 stabl2 p1 (σ1(x ↦ d_new)) wn"
"(xd, infl', stabl', p', σ') = iterate x (c⇩w ∪ c⇩n) infl2 stabl2 p1 (σ1(x ↦ d_new)) wn"
using Iterate.IH(4) Continue(1-3,4-7,9) Iterate.prems(2) by auto
have "iterate_dom x (c⇩w ∪ c⇩n) infl stabl p σ wn"
using Continue(1-3,4-7) IH1 IH2(1) query_iterate_eval.domintros(2)[of x stabl "c⇩w ∪ c⇩n" infl
p σ] by (cases "eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ", cases
"destab x infl1 stabl1", cases "TD_post.destab_post x post pinfl1 post1 stabl2",
cases wn) (auto split: if_splits)
then show ?thesis using iterate.psimps[folded dom_defs] Continue(1,2,4-6) IH1(2) IH2(2)
by (cases "eval x (T x) (c⇩w ∪ c⇩n) infl (insert x stabl) p σ", cases
"destab x infl1 stabl1") auto
qed
next
case (Eval x t c⇩w c⇩n infl stabl p σ pinfl post)
show ?case using Eval.IH(1) Eval.prems(1)
proof(cases rule: TD_post.eval_query_answer_cases)
case (Query y g yd infl1 stabl1 p1 σ1 pinfl1 post1)
have IH1: "query_dom x y (c⇩w ∪ c⇩n) infl stabl p σ"
"(yd, infl1, stabl1, p1, σ1) = query x y (c⇩w ∪ c⇩n) infl stabl p σ"
using Eval.IH(2)[OF Query(1,3)] by auto
have IH2: "eval_dom x (g yd) (c⇩w ∪ c⇩n) infl1 stabl1 p1 σ1"
"(xd, infl', stabl', p', σ') = eval x (g yd) (c⇩w ∪ c⇩n) infl1 stabl1 p1 σ1"
using Eval.IH(3)[OF Query(1,3) _ _ _ _ _ _ Query(5)] by auto
have "eval_dom x t (c⇩w ∪ c⇩n) infl stabl p σ"
using query_iterate_eval.domintros(3)[of t x "c⇩w ∪ c⇩n" infl stabl p σ] Query(1) IH1 IH2(1)
by (smt (z3) Pair_inject query_dom_def eval_dom_def strategy_tree.inject(2))
then show ?thesis
using eval.psimps[folded dom_defs] Query(1) IH1(2) IH2(2) by (auto split: prod.splits)
next
case Answer
then show ?thesis using query_iterate_eval.domintros(3)[of t] by simp
qed
qed
corollary TD_wn_post_TD_wn_equivalence:
assumes "TD_post.solve_dom x"
and "TD_post.solve x = (stabl, σ)"
shows "solve_dom x ∧ solve x = (stabl, σ)"
proof -
obtain xd infl p pinfl post where "(xd, infl, stabl, p, σ, pinfl, post) =
TD_post.iterate x {x} {} fmempty {} {} (λx. None) Widening fmempty {}"
using assms(2) unfolding TD_post.solve_def by (auto split: prod.splits)
then have "iterate_dom x {x} fmempty {} {} (λx. None) Widening"
"(xd, infl, stabl, p, σ) = iterate x {x} fmempty {} {} (λx. None) Widening"
using equiv_post_solver_aux_2(2)[where c⇩w = "{x}" and c⇩n ="{}"] assms(1)
unfolding TD_post.solve_dom_def by auto
then show ?thesis unfolding solve_dom_def solve_def by (auto split: prod.splits)
qed
subsection ‹Partial Correctness›
theorem partial_correctness:
assumes "is_mono_eq T"
and "mono_deps T"
and "solve_dom x"
and "solve x = (stabl, σ)"
shows "part_post_solution T x σ stabl"
proof -
have "TD_post.solve_dom x" "TD_post.solve x = (stabl, σ)"
using TD_wn_TD_wn_post_equivalence[OF assms(3,4)] by auto
then show ?thesis
using TD_post.partial_correctness widening_ge widening_bounded narrowing_ge narrowing_le
assms(1,2)
by auto
qed
subsection ‹Termination›
context
assumes widening_finite: "wf {(x,y). ∃a. x ≠ y ∧ x = y ∇ a}"
and narrowing_finite: "wf {(x,y). ∃a. x ≠ y ∧ x = y Δ a}"
and finite_vars: "finite (UNIV :: 'x set)"
begin
theorem solve_termination: "solve_dom x"
proof -
have "TD_post.solve_dom x"
using TD_post.solve_termination widening_finite narrowing_finite finite_vars by auto
moreover obtain σ stabl where "TD_post.solve x = (stabl, σ)" by fastforce
ultimately show ?thesis using TD_wn_post_TD_wn_equivalence by blast
qed
end
end
end
end