Theory TD_warrow
section ‹Warrowing TD›
text‹In this theory, we first prove the partial correctness of the warrowing TD and later, with
additional assumptions, its equivalence with the TD with widening and narrowing in phases. The
warrowing TD extends the vanilla TD by dynamically tracking potential warrowing points.
The warrowing operator is applied at warrowing points in function @{term iterate} to
accelerate fixpoint iteration. Compared to the vanilla TD, the warrowing TD is no longer
guaranteed to return partial solutions. Instead, computed assignments are only partial
post-solutions to the given system of equations.›
theory TD_warrow
imports Basics TD_wn_phases
begin
text‹We first use a locale to specify the context for the definitions. Later, extensions of this
locale are used to specify further assumptions for the proofs.›
locale TD_warrow_defs =
fixes T :: "('x,'d::order_bot) eqsT"
fixes widening :: "'d ⇒ 'd ⇒ 'd" (infixl "∇" 65)
and narrowing :: "'d ⇒ 'd ⇒ 'd" (infixl "Δ" 70)
begin
subsection ‹The Warrowing Operator›
text‹The warrowing is defined as a dynamic operator that dispatches to widening or narrowing based
on the current relation of the old value @{term a} and the new value @{term b}. For non-monotonic
equation systems, the warrowing solver may switch between widening and narrowing phases multiple
times before reaching a fixpoint---or even never terminate.›
definition warrowing :: "'d ⇒ 'd ⇒ 'd" (infixl "∇Δ" 65)
where "warrowing a b = (if b ≤ a then a Δ b else a ∇ b)"
subsection‹Definition of the Solver Algorithm›
text‹As the TD with widening/narrowing phases, TD with warrowing uses a set @{term point} to
dynamically track unknowns at which to apply warrowing. In case a transitive self-dependence of
an unknown is detected in function @{term query}, the solver marks the unknown as point.
The warrowing operator is applied all unknowns in points in the function @{term iterate}.›
function (domintros)
query :: "'x ⇒ 'x ⇒ ('x,'d) state ⇒ 'd × ('x,'d) state" and
iterate :: "'x ⇒ ('x,'d) state ⇒ 'd × ('x,'d) state" and
eval :: "'x ⇒ ('x,'d) strategy_tree ⇒ ('x,'d) state ⇒ 'd × ('x,'d) state" where
"query y x state = (
let (xd, state) =
if x ∈ called state then
(mlup (σ state) x, state ⦇point := insert x (point state)⦈)
else
iterate x (state ⦇called := insert x (called state)⦈)
in (xd, state ⦇infl := fminsert (infl state) x y⦈))"
| "iterate x state = (
if x ∉ stabl state then
let point⇩x = x ∈ point state in
let (xd, state) = eval x (T x) (state ⦇stabl := insert x (stabl state)⦈) in
let d_new = if ¬ point⇩x then xd else mlup (σ state) x ∇Δ xd in
if d_new = mlup (σ state) x then
(d_new, state ⦇called := called state - {x}, point := (point state) - {x}⦈)
else
let (infl', stabl') = destab x (infl state) (stabl state) in
iterate x (state ⦇infl := infl', stabl := stabl', σ := (σ state)(x ↦ d_new)⦈)
else
(mlup (σ state) x, state ⦇called := called state - {x}, point := (point state) - {x}⦈))"
| "eval x t state = (case t of
Answer d ⇒ (d, state)
| Query y g ⇒ (let (yd, state) = query x y state in eval x (g yd) state))"
by pat_completeness auto
definition solve :: "'x ⇒ ('x, 'd) map × 'x set" where
"solve x = (
let state = ⦇called = {}, σ = Map.empty, infl = fmempty, stabl = {}, point = {}⦈ in
let (d, state) = iterate x (state ⦇ called := insert x (called state) ⦈) in
(σ state, stabl state))"
definition query_dom where
"query_dom y x state = query_iterate_eval_dom (Inl (y, x, state))"
declare query_dom_def [simp]
definition iterate_dom where
"iterate_dom x state = query_iterate_eval_dom (Inr (Inl (x, state)))"
declare iterate_dom_def [simp]
definition eval_dom where
"eval_dom x t state = query_iterate_eval_dom (Inr (Inr (x, t, state)))"
declare eval_dom_def [simp]
definition solve_dom where
"solve_dom x =
iterate_dom x ⦇called = {x}, σ = Map.empty, infl = fmempty, stabl = {}, point = {}⦈"
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 y x state for y x state
]
query_iterate_eval.pinduct(2)[
folded query_dom_def iterate_dom_def eval_dom_def,
of x state for x state
]
query_iterate_eval.pinduct(3)[
folded query_dom_def iterate_dom_def eval_dom_def,
of x t state for x t state
]
lemmas iterate_pinduct[consumes 1, case_names Iterate]
= query_iterate_eval_pinduct(2)[where ?P="λy x state. True"
and ?R="λx t state. True", simplified (no_asm_use),
folded query_dom_def iterate_dom_def eval_dom_def]
declare query.psimps[simp] iterate.psimps[simp] eval.psimps[simp]
subsection ‹Domain Lemmas›
lemma dom_backwards_pinduct:
shows "query_dom y x state
⟹ x ∉ (called state) ⟹ iterate_dom x (state ⦇called := insert x (called state)⦈)"
and "iterate_dom x state
⟹ x ∉ (stabl state) ⟹ (eval_dom x (T x) (state ⦇stabl := insert x (stabl state)⦈) ∧
((xd, state1) = eval x (T x) (state ⦇stabl := insert x (stabl state)⦈)
⟶ d_new = (if x ∉ (point state) then xd else mlup (σ state1) x ∇Δ xd)
⟶ mlup (σ state1) x ≠ d_new
⟶ (infl2, stabl2) = destab x (infl state1) (stabl state1) ⟶
iterate_dom x (state1 ⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ d_new)⦈)))"
and "eval_dom x (Query y g) state
⟹ (query_dom x y state ∧
((yd, state') = query x y state ⟶
eval_dom x (g yd) state'))"
proof (induction y x state and x state and x "Query y g" state
arbitrary: and xd state1 d_new infl2 stabl2 and y g yd state'
rule: query_iterate_eval_pinduct)
case (Query y x state)
show ?case
apply (rule query_iterate_eval.domintros(2)[folded dom_defs])
using Query.hyps(2) Query.prems by auto
next
case (Iterate x state)
show ?case apply (intro impI conjI)
subgoal
apply (rule query_iterate_eval.domintros(3)[folded dom_defs])
using Iterate.hyps(2)[OF Iterate.prems] by fastforce+
subgoal
apply (rule query_iterate_eval.domintros(2)[folded dom_defs])
using Iterate.hyps(3)[OF Iterate.prems, folded dom_defs] by (fastforce split: prod.splits)+
done
next
case (Eval x state)
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 state"
and "(xd, state') = iterate x state"
obtains (Stable) "x ∈ (stabl state)"
and "xd = mlup (σ state) x"
and "state' = state ⦇called := called state - {x}, point := (point state) - {x}⦈"
| (Fixpoint) state1
where "x ∉ (stabl state)" and "x ∉ (point state)"
and "eval_dom x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
and "(xd, state1) = eval x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
and "mlup (σ state') x = xd"
and "state' = state1 ⦇called := called state1 - {x}, point := (point state1) - {x}⦈"
| (WN_Fixpoint) xd1 state1
where "x ∉ (stabl state)" and "x ∈ (point state)"
and "eval_dom x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
and "(xd1, state1) = eval x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
and "xd = mlup (σ state') x ∇Δ xd1"
and "mlup (σ state') x = xd"
and "state' = state1 ⦇called := called state1 - {x}, point := (point state1) - {x}⦈"
| (Continue) xd1 state1 d_new infl2 stabl2
where "x ∉ (stabl state)"
and "eval_dom x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
and "(xd1, state1) = eval x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
and "d_new = (if x ∉ (point state) then xd1 else mlup (σ state1) x ∇Δ xd1)"
and "d_new ≠ mlup (σ state1) x"
and "(infl2, stabl2) = destab x (infl state1) (stabl state1)"
and "iterate_dom x (state1 ⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ d_new)⦈)"
and "(xd, state') =
iterate x (state1 ⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ d_new)⦈)"
proof(cases "x ∈ (stabl state)" 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) (state ⦇stabl := insert x (stabl state)⦈)"
using assms(1) dom_backwards_pinduct(2)
by simp
then obtain xd1 state1
where slapp: "eval x (T x) (state ⦇stabl := insert x (stabl state)⦈) = (xd1, state1)"
by (cases "eval x (T x) (state ⦇stabl := insert x (stabl state)⦈)") auto
then obtain d_new
where d_new: "d_new = (if x ∉ (point state) then xd1 else mlup (σ state1) x ∇Δ xd1)"
by blast
show ?thesis
proof (cases "mlup (σ state1) x = d_new" rule: case_split[case_names Fixpoint Continue])
case Fixpoint
then show ?thesis
using Unstable sldom slapp d_new assms that(2,3)
by (cases "x ∈ point state") auto
next
case Continue
obtain infl2 stabl2 where destab: "destab x (infl state1) (stabl state1) = (infl2, stabl2)"
by (cases "destab x (infl state1) (stabl state1)")
then have dom:
"iterate_dom x (state1 ⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ d_new)⦈)"
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(4)
by (cases "x ∈ (point state)") (auto simp add: Let_def)
qed
qed
lemma query_iterate_lookup_cases_basic[consumes 2]:
assumes "query_dom y x state"
and "(xd, state') = query y x state"
obtains (Iterate) state1
where "x ∉ (called state)"
and "iterate_dom x (state ⦇called := insert x (called state)⦈)"
and "(xd, state1) = iterate x (state ⦇called := insert x (called state)⦈)"
and "state' = state1 ⦇infl := fminsert (infl state1) x y⦈"
| (Lookup) "x ∈ (called state)"
and "xd = mlup (σ state) x"
and "state' = state ⦇infl := fminsert (infl state) x y, point := insert x (point state)⦈"
using assms that dom_backwards_pinduct(1)
by (cases "x ∈ (called state)") (auto split!: prod.splits)
lemma eval_query_answer_cases_basic[consumes 2]:
assumes "eval_dom x t state"
and "(xd, state') = eval x t state"
obtains (Query) y g yd state1
where "t = Query y g"
and "query_dom x y state"
and "(yd, state1) = query x y state"
and "eval_dom x (g yd) state1"
and "(xd, state') = eval x (g yd) state1"
| (Answer) "t = Answer xd"
and "state' = state"
using assms dom_backwards_pinduct(3) that
by (cases t; auto split: prod.splits)
lemma c_same:
shows
"query_dom y x state ⟹ (xd, state') = query y x state ⟹ called state' = called state"
"iterate_dom x state ⟹ (xd, state') = iterate x state ⟹ called state' = called state - {x}"
"eval_dom x t state ⟹ (xd, state') = eval x t state ⟹ called state' = called state"
proof (induction y x state and x state and x t state
arbitrary: xd state' and xd state' and xd state'
rule: query_iterate_eval_pinduct)
case (Query x y state)
show ?case using Query(1,3)
proof (cases rule: query_iterate_lookup_cases_basic)
case (Iterate state1)
then show ?thesis using Query(2)[of xd state1] by simp
next
case Lookup
then show ?thesis by fastforce
qed
next
case (Iterate x state)
show ?case using Iterate(1,4)
proof (cases rule: iterate_continue_fixpoint_cases)
case Stable
then show ?thesis by simp
next
case Fixpoint
then show ?thesis using Iterate.IH(2) by simp
next
case (WN_Fixpoint xd1 state1)
then show ?thesis using Iterate.IH(2) by simp
next
case (Continue xd1 state1 d_new infl2 stabl2)
then show ?thesis
using Iterate.IH(2)[OF Continue(1) _ Continue(3)]
Iterate.IH(3)[OF Continue(1) _ Continue(3) _ Continue(4,5) _ Continue(6),
simplified, OF Continue(8)]
by simp
qed
next
case (Eval x t state)
show ?case using Eval(1, 4)
proof (cases rule: eval_query_answer_cases_basic)
case (Query y g yd state1)
then show ?thesis
using Eval.IH(2)[OF Query(1,3)] Eval.IH(3)[OF Query(1,3) _ Query(5), simplified] by simp
qed simp
qed
lemma iterate_fmlookup:
assumes "iterate_dom x state"
and "(xd, state') = iterate x state"
shows "mlup (σ state') x = xd"
using assms
proof(induction rule: iterate_pinduct)
case Iterate
show ?case
using Iterate.hyps Iterate.prems
proof(cases rule: iterate_continue_fixpoint_cases)
case Continue
then show ?thesis
using Iterate.IH(1) c_same(3)[OF Continue(2,3)] Iterate(3) by fastforce
qed simp+
qed
corollary query_fmlookup:
assumes "query_dom y x state"
and "(xd, state') = query y x state"
shows "mlup (σ state') x = xd"
using assms iterate_fmlookup dom_backwards_pinduct(1)[of y x state]
by (auto split: prod.splits if_splits)
lemma query_iterate_lookup_cases[consumes 2]:
assumes "query_dom y x state"
and "(xd, state') = query y x state"
obtains (Iterate) state1
where "x ∉ (called state)"
and "iterate_dom x (state ⦇called := insert x (called state)⦈)"
and "(xd, state1) = iterate x (state ⦇called := insert x (called state)⦈)"
and "state' = state1 ⦇infl := fminsert (infl state1) x y⦈"
and "mlup (σ state') x = xd"
| (Lookup) "x ∈ (called state)"
and "xd = mlup (σ state) x"
and "state' = state ⦇infl := fminsert (infl state) x y, point := insert x (point state)⦈"
apply (rule query_iterate_lookup_cases_basic[OF assms])
using iterate_fmlookup[of x "state⦇called := insert x (called state)⦈"]
by (simp_all split: if_splits del: dom_defs)
lemma eval_query_answer_cases[consumes 2]:
assumes "eval_dom x t state"
and "(xd, state') = eval x t state"
obtains (Query) y g yd state1
where "t = Query y g"
and "query_dom x y state"
and "(yd, state1) = query x y state"
and "eval_dom x (g yd) state1"
and "(xd, state') = eval x (g yd) state1"
and "mlup (σ state1) y = yd"
| (Answer) "t = Answer xd"
and "state' = state"
apply (rule eval_query_answer_cases_basic[OF assms])
by (auto simp: query_fmlookup[of x _ state])
subsection ‹Program Refinement for Code Generation›
text‹To derive executable code for the TD, we do a program refinement and define an
equivalent solve function based on partial\_function with options that can be used for the code
generation.›