Theory TD
section ‹The Top-Down Solver›
text ‹\label{sec:td}›
text‹In this theory we proof the partial correctness of the original TD by establishing its
equivalence with the TD\_plain. Compared to the TD\_plain, it additionally tracks a set of
currently stable unknowns @{term stabl}, and a map @{term infl} collecting for each unknown
@{term x} a list of unknowns influenced by it. This allows for the optimization that skips the
re-evaluation of unknowns which are already stable. It does, however, also require a
destabilization mechanism triggering re-evaluation of all unknowns possibly affected by an unknown
whose value has changed.
›
theory TD
imports Basics Destabilization TD_plain
begin
declare fun_upd_apply[simp del]
subsection‹Definition of the Solver Algorithm›
record ('x,'d) state = "('x,'d) state" +
infl :: "('x, 'x list) fmap"
stabl :: "'x set"
locale TD =
fixes T :: "('x,'d::bot) eqsT"
begin
text‹Apart from passing the additional arguments for the solver state, the @{term iterate} function
contains, compared to the TD\_plain, an additional check to skip iteration of already stable
unknowns. Furthermore, the helper function @{term destabilize} is called whenever the newly
evalauated value of an unknown changed compared to the value tracked in @{term σ}. Lastly, a
dependency is recorded whenever returning from a @{term query} call for unknown @{term x} within
the evaluation of right-hand side of unknown @{term y}.›
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)
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 (d_new, state) = eval x (T x) (state⦇stabl := insert x (stabl state)⦈) in
if mlup (σ state) x = d_new then
(d_new, state⦇called := called state - {x}⦈)
else
let (i, s) = destab x (infl state) (stabl state) in
iterate x (state⦇infl := i, stabl := s, σ := (σ state)(x ↦ d_new)⦈)
else
(mlup (σ state) x, state⦇called := called 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 set × ('x, 'd) map" where
"solve x = (
let (_, state) = iterate x ⦇called = {x}, σ = Map.empty, infl = fmempty, stabl = {}⦈
in (stabl state, σ state))"
definition query_dom where
"query_dom x y state = query_iterate_eval_dom (Inl (x, y, 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 = {}⦈"
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 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="λx y 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]
declare iterate.psimps [simp]
declare eval.psimps [simp]
subsubsection ‹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_new, state1) = eval x (T x) (state⦇stabl := insert x (stabl state)⦈)
⟶ mlup (σ state1) x ≠ xd_new ⟶ (infl2, stabl2) = destab x (infl state1) (stabl state1)
⟶ iterate_dom x (state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ xd_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_new state1 infl2 stabl2 and y g yd state'
rule: query_iterate_eval_pinduct)
case (Query y x state)
then show ?case using query_iterate_eval.domintros(2) by fastforce
next
case (Iterate x state)
then show ?case
using query_iterate_eval.domintros(2)[folded dom_defs, of x
"state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ xd_new)⦈"]
query_iterate_eval.domintros(3)
by auto
next
case (Eval x state)
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 state"
and "(xd, state') = iterate x state"
obtains (Stable) "state' = state⦇called := called state - {x}⦈"
and "mlup (σ state) x = xd"
and "x ∈ stabl state"
| (Fixpoint) state1
where "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}⦈"
and "x ∉ stabl state"
| (Continue) state1 xd_new stabl2 infl2
where "eval_dom x (T x) (state⦇stabl := insert x (stabl state)⦈)"
and "(xd_new, state1) = eval x (T x) (state⦇stabl := insert x (stabl state)⦈)"
and "mlup (σ state1) x ≠ xd_new"
and "(infl2, stabl2) = destab x (infl state1) (stabl state1)"
and "iterate_dom x (state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ xd_new)⦈)"
and "(xd, state') =
iterate x (state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ xd_new)⦈)"
and "x ∉ stabl state"
proof(cases "x ∈ stabl state" rule: case_split[case_names Stable Unstable])
case Stable
then show ?thesis using that(1) assms 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 xd_new state1
where slapp: "eval x (T x) (state⦇stabl := insert x (stabl state)⦈) = (xd_new, state1)"
by (cases "eval x (T x) (state⦇stabl := insert x (stabl state)⦈)") auto
show ?thesis
proof (cases "mlup (σ state1) x = xd_new")
case True
then show ?thesis
using Unstable sldom slapp assms that(2) by auto
next
case False
then obtain infl2 stabl2 where
destab: "destab x (infl state1) (stabl state1) = (infl2, stabl2)"
by (cases "destab x (infl state1) (stabl state1)")
let ?state2 = "(state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ xd_new)⦈)"
have dom: "iterate_dom x ?state2"
and "iterate x state = iterate x ?state2"
and app: "iterate x ?state2 = (xd, state')"
using Unstable False slapp assms(1-2) dom_backwards_pinduct(2) destab
by auto
then show ?thesis using sldom slapp Unstable False destab that(3) by auto
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 "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 "x ∉ called state"
| (Lookup) "mlup (σ state) x = xd"
and "state' = state⦇infl := fminsert (infl state) x y⦈"
and "x ∈ called 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 (Continue state1)
then show ?thesis
using Iterate.IH(2)[OF Continue(7,2)]
Iterate.IH(3)[OF Continue(7,2) _ _ Continue(4) _ Continue(6)]
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)
show ?thesis
using Eval.IH(2)[OF Query(1,3)] Eval.IH(3)[OF Query(1,3) _ Query(5)] by simp
qed fast
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 x state)
show ?case
using Iterate.hyps Iterate.prems(1)
proof(cases rule: iterate_continue_fixpoint_cases)
case (Continue state1 xd_new stabl2 infl2)
then show ?thesis using Iterate.IH Continue by simp+
qed (simp add: Iterate.prems(1))
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 "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"
and "x ∉ called state"
| (Lookup) "mlup (σ state) x = xd"
and "state' = state⦇infl := fminsert (infl state) x y⦈"
and "x ∈ called 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"
by (auto intro: eval_query_answer_cases_basic[OF assms] simp add: 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.›