Theory TD_plain
section ‹The plain Top-Down Solver›
text ‹\label{sec:td_plain}›
text‹TD\_plain is a simplified version of the original TD which only keeps track of already called
unknowns to avoid infinite descend in case of recursive dependencies. In contrast to the TD, it
does, however, not track stable unknowns and the dependencies between unknowns. Instead, it
re-iterates every unknown when queried again.
›
theory TD_plain
imports Basics
begin
subsection ‹Definition of the Solver Algorithm›
record ('x,'d) state =
called :: "'x set"
σ :: "('x,'d) map"
locale TD_plain =
fixes T :: "('x,'d::bot) eqsT"
begin
text ‹The recursively descending solver algorithm is defined with three mutual recursive functions.
Initially, the function @{term iterate} is called from the top-level @{term solve} function for
the requested unknown. @{term iterate} keeps evaluating the right-hand side by calling the
function @{term eval} and updates the value mapping @{term σ} until the value stabilizes. The
function @{term eval} walks through a strategy tree and chooses the path based on the result for
queried unknowns. These queries are delegated to the third mutual recursive function @{term query}
which checks that the unknown is not already being evaluated and iterates it otherwise. The
function keyword is used for the definition, since, without further assumptions, the solver may
not terminate.›
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 = (
if x ∈ called state then
(mlup (σ state) x, state)
else
iterate x (state⦇called := insert x (called state)⦈))"
| "iterate x state = (
let (d_new, state) = eval x (T x) state in
if mlup (σ state) x = d_new then
(d_new, state⦇called := called state - {x}⦈)
else
iterate x (state⦇σ := (σ state)(x ↦ d_new)⦈))"
| "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" where
"solve x = (let (_, state) = iterate x ⦇called = {x}, σ = Map.empty⦈ in σ 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⦈"
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 for easier instantiation and assigns each case a comprehensible name.›
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
⟹ (eval_dom x (T x) state ∧
((xd_new, state') = eval x (T x) state
⟶ mlup (σ state') x ≠ xd_new ⟶
iterate_dom x (state'⦇σ := (σ state')(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 state' and y g yd state'
rule: query_iterate_eval_pinduct)
case (Query T x state)
then show ?case
using query_iterate_eval.domintros(2) by fastforce
next
case (Iterate T x state)
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 T 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 (Fixpoint) state1
where "eval_dom x (T x) state"
and "(xd, state1) = eval x (T x) state"
and "mlup (σ state') x = xd"
and "state' = state1⦇called := called state1 - {x}⦈"
| (Continue) state1 xd_new
where "eval_dom x (T x) state"
and "(xd_new, state1) = eval x (T x) state"
and "mlup (σ state1) x ≠ xd_new"
and "iterate_dom x (state1⦇σ := (σ state1)(x ↦ xd_new)⦈)"
and "(xd, state') = iterate x (state1⦇σ := (σ state1)(x ↦ xd_new)⦈)"
proof -
obtain xd_new state1
where "eval x (T x) state = (xd_new, state1)"
by (cases "eval x (T x) state")
then show ?thesis
using assms that dom_backwards_pinduct(2)[OF assms(1)]
by (cases "mlup (σ state1) x = xd_new") fastforce+
qed
lemma query_iterate_lookup_cases_basic [consumes 2]:
assumes "query_dom y x state"
and "(xd, state') = query y x state"
obtains (Iterate)
"iterate_dom x (state⦇called := insert x (called state)⦈)"
and "(xd, state') = iterate x (state⦇called := insert x (called state)⦈)"
and "x ∉ called state"
| (Lookup) "mlup (σ state) x = xd"
and "state' = state"
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 y x state)
show ?case using Query(1,3)
proof (cases rule: query_iterate_lookup_cases_basic)
case Iterate
then show ?thesis using Query(2)[of xd state'] 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 Fixpoint
then show ?thesis using Iterate.IH(2) by simp
next
case (Continue state1)
then show ?thesis
using Iterate.IH(2)[OF Continue(2)] Iterate.IH(3)[OF Continue(2) _ _ Continue(5)]
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)
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 assms(1)]
by (auto simp del: iterate.psimps split: if_splits)
lemma query_iterate_lookup_cases [consumes 2]:
assumes "query_dom y x state"
and "(xd, state') = query y x state"
obtains (Iterate)
"iterate_dom x (state⦇called := insert x (called state)⦈)"
and "(xd, state') = iterate x (state⦇called := insert x (called state)⦈)"
and "mlup (σ state') x = xd"
and "x ∉ called state"
| (Lookup) "mlup (σ state) x = xd"
and "state' = state"
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‹For code generation, we define a refined version of the solver function using the
partial\_function keyword with the option attribute.›