Theory TD_wn_phases
section ‹TD with Widening and Narrowing in Phases›
text‹In this theory, we prove the termination of the TD with widening and narrowing applied in
two phases per iteration on an unknown. This extended TD also dynamically identifies unknowns
at which widening and narrowing is applied. While it terminates for arbitrary equation system
as long as the set of unknowns is finite, it may not necessarily return a partial post-solution.
With a widening operator that is precise and for an equation system where right-hand sides are
monotonic and have monotonic dependencies the returning of a partial post-solution can, however,
be guaranteed. We prove this in the accompanying theory file by showing the phase TD specified
here to be equivalent to the TD extended with the combined warrowing operator.›
theory TD_wn_phases
imports Basics Destabilization TD
begin
datatype phase = Widening | Narrowing
text‹The TD with widening/narrowing phases uses a set @{term point} to dynamically track unknowns
at which widening and narrowing should be applied. @{term point} is tracked as part of the
solver state among the components already used by the vanilla TD:
@{term c} to track already called unknowns, @{term σ} to track the current unknown-to-value
mapping, and @{term stabl} and @{term infl} to track unknowns and their dependencies which need
not be re-iterated because their value is unchanged since their last iteration.›
record ('x,'d) state = "('x,'d) state" +
point :: "'x set"
locale TD_wn_phases =
fixes T :: "('x,'d::order_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, 'd) state ⇒ 'd × ('x, 'd) state" and
iterate :: "'x ⇒ phase ⇒ ('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 Widening (state⦇called := insert x (called state)⦈)
in (xd, state⦇infl := fminsert (infl state) x y⦈))"
| "iterate x phase 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 = if ¬ point⇩x then xd
else if phase = Widening then mlup (σ state) x ∇ xd else mlup (σ state) x Δ xd in
if d = mlup (σ state) x then (
if point⇩x ∧ phase = Widening then (
let d = mlup (σ state) x Δ xd in
if d = mlup (σ state) x then
(d, state⦇called := (called state) - {x}, point := (point state) - {x}⦈)
else (
let (infl, stabl) = destab x (infl state) (stabl state) in
iterate x Narrowing (state⦇infl := infl, stabl := stabl, σ := (σ state)(x ↦ d)⦈)))
else (d, state⦇called := (called state) - {x}, point := (point state) - {x}⦈))
else (
let (infl, stabl) = destab x (infl state) (stabl state) in
iterate x phase (state⦇infl := infl, stabl := stabl, σ := (σ state)(x ↦ d)⦈)))
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 (_, state) = iterate x Widening (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 wn state =
query_iterate_eval_dom (Inr (Inl (x, wn, 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 Widening ⦇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 wn state for x wn 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]
declare iterate.psimps [simp]
declare eval.psimps [simp]
subsection ‹Domain Lemmas›
lemma dom_backwards_pinduct:
shows "query_dom y x state
⟹ x ∉ called state ⟹ iterate_dom x Widening (state⦇called := insert x (called state)⦈)"
and "iterate_dom x wn 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 if wn = Widening then mlup (σ state1) x ∇ xd else mlup (σ state1) x Δ xd)
⟶ (d_new = mlup (σ state1) x ⟶ x ∈ point state ⟶ wn = Widening
⟶ mlup (σ state1) x Δ xd ≠ mlup (σ state1) x
⟶ (infl2, stabl2) = destab x (infl state1) (stabl state1)
⟶ iterate_dom x Narrowing (state1⦇infl := infl2, stabl := stabl2,
σ := (σ state1)(x↦mlup (σ state1) x Δ xd)⦈))
∧ (d_new ≠ mlup (σ state1) x
⟶ (infl2, stabl2) = destab x (infl state1) (stabl state1) ⟶
iterate_dom x wn (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 wn 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
using Query(1) Query(2)[OF Query(3), simplified]
query_iterate_eval.domintros(2)[of x "state⦇called := insert x (called state)⦈" Widening]
by fastforce
next
case (Iterate x wn state)
have eval_dom: "eval_dom x (T x) (state⦇stabl := insert x (stabl state)⦈)"
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 ∈ point state ∧ 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,7), simplified]
query_iterate_eval.domintros(2)[folded dom_defs, of x "state1⦇infl := infl2,
stabl := stabl2, σ := (σ state1)(x ↦ mlup (σ state1) x Δ xd)⦈" Narrowing]
by fastforce
next
case 3
show ?case
using Iterate.hyps(4)[OF Iterate.prems _ 3(1) _ 3(2-4), simplified]
iterate_dom_def query_iterate_eval.domintros(2)[of x "state1⦇infl := infl2,
stabl := stabl2, σ := (σ state1)(x ↦ d_new)⦈" wn]
by fastforce
qed
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_basic[consumes 3]:
assumes "iterate_dom x wn state"
and "(xd, state') = iterate x wn 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 "state' = state1⦇called := (called state1) - {x}, point := (point state1) - {x}⦈"
and "xd = mlup (σ state') x"
| (W_Fixpoint) xd1 state1 infl2 stabl2
where "x ∉ stabl state" and "x ∈ point state" and "wn = Widening"
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 "mlup (σ state1) x ∇ xd1 = mlup (σ state1) x"
and "mlup (σ state1) x Δ xd1 ≠ mlup (σ state1) x"
and "(infl2, stabl2) = destab x (infl state1) (stabl state1)"
and "iterate_dom x Narrowing (state1⦇infl := infl2, stabl := stabl2,
σ := (σ state1)(x↦mlup (σ state1) x Δ xd1)⦈)"
and "(xd, state') = iterate x Narrowing (state1⦇infl := infl2, stabl := stabl2,
σ := (σ state1)(x↦mlup (σ state1) x Δ xd1)⦈)"
| (N_Fixpoint) xd1 state1
where "x ∉ stabl state" and "x ∈ point state"
and "wn = Narrowing ∨ (wn = Widening ∧ mlup (σ state') x ∇ xd1 = mlup (σ state') x)"
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 "xd = mlup (σ state') x"
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
if wn = Widening then mlup (σ state1) x ∇ 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 wn (state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ d_new)⦈)"
and "(xd, state') =
iterate x wn (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 if wn = Widening then mlup (σ state1) x ∇ 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
proof (cases "x ∈ point state")
case True
then show ?thesis
proof (cases wn)
case Widening
obtain infl2 stabl2 where
destab: "destab x (infl state1) (stabl state1) = (infl2, stabl2)"
by (cases "destab x (infl state1) (stabl state1)")
have d_new: "d_new = mlup (σ state1) x ∇ xd1" using d_new Widening True by simp
show ?thesis
proof (cases "mlup (σ state1) x Δ xd1 = mlup (σ state1) x")
case True
then have "iterate x wn state = (mlup (σ state1) x,
state1⦇called := (called state1) - {x}, point := (point state1) - {x}⦈)"
using iterate.psimps[folded dom_defs, OF assms(1)] ‹x ∈ point state› Unstable slapp
Fixpoint d_new Widening True
by force
then have "xd = mlup (σ state1) x" "state' = state1⦇called := (called state1) - {x},
point := (point state1) - {x}⦈"
using assms(2) by auto
moreover have "mlup (σ state1) x ∇ xd1 = mlup (σ state1) x"
using Fixpoint d_new by auto
ultimately show ?thesis
using that(4)[OF Unstable ‹x ∈ point state› _ sldom slapp[symmetric]] True Widening by simp
next
case False
have "mlup (σ state1) x ∇ xd1 = mlup (σ state1) x" using d_new Fixpoint by simp
moreover have "(xd, state') = iterate x Narrowing
(state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x↦mlup (σ state1) x Δ xd1)⦈)"
using iterate.psimps[folded dom_defs, OF assms(1)] Unstable slapp Fixpoint d_new Widening
True destab False assms(2)
by force
moreover have "iterate_dom x Narrowing
(state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x↦mlup (σ state1) x Δ xd1)⦈)"
using Unstable slapp Fixpoint d_new Widening True assms(1) dom_backwards_pinduct(2) destab
False
by simp
ultimately show ?thesis
using that(3)[OF Unstable True Widening sldom slapp[symmetric] _ False destab[symmetric]]
by simp
qed
next
case Narrowing
have "d_new = mlup (σ state1) x Δ xd1" using d_new Narrowing True by simp
moreover have "iterate x wn state = (mlup (σ state1) x, state1⦇called := (called state1) - {x},
point := (point state1) - {x}⦈)"
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 _ sldom] Narrowing Fixpoint
by auto
qed
next
case False
have "iterate x wn state = (mlup (σ state1) x, state1⦇called := (called state1) - {x},
point := (point state1) - {x}⦈)"
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 (infl state1) (stabl state1) = (infl2, stabl2)"
by (cases "destab x (infl state1) (stabl state1)")
then have dom: "iterate_dom x wn
(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(3,5)
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 Widening (state⦇called := insert x (called state)⦈)"
and "(xd, state1) = iterate x Widening (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[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: "query_dom y x state ⟹ (xd, state') = query y x state ⟹ called state' = called state"
"iterate_dom x wn state ⟹ (xd, state') = iterate x wn 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 wn 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.IH(1) Query.prems(1)
proof (cases rule: query_iterate_lookup_cases_basic)
case (Iterate state1)
show ?thesis using Query.IH(2)[OF Iterate(1,3)] Iterate(1,4) by simp
next
case Lookup
then show ?thesis by simp
qed
next
case (Iterate x wn state)
show ?case using Iterate.IH(1) Iterate.prems(1)
proof (cases rule: iterate_continue_fixpoint_cases_basic)
case Stable
then show ?thesis by simp
next
case (Fixpoint state1)
show ?thesis using Iterate.IH(2)[OF _ refl] Fixpoint(1,3-5) by simp
next
case (W_Fixpoint xd1 state1 infl2 stabl2)
show ?thesis
using Iterate.IH(2)[OF _ refl] Iterate.IH(3)[OF _ refl _ refl refl] W_Fixpoint(1-3,5-8,10)
by simp
next
case (N_Fixpoint xd1 state1)
show ?thesis using Iterate.IH(2)[OF _ refl] N_Fixpoint(1,5,8) by simp
next
case (Continue xd1 state1 d_new infl2 stabl2)
show ?thesis
using Iterate.IH(2)[OF _ refl] Iterate.IH(4)[OF _ refl _ refl refl _ refl] Continue(1,3-6,8)
by simp
qed
next
case (Eval x t state)
show ?case using Eval.IH(1) Eval.prems(1)
proof (cases rule: eval_query_answer_cases)
case (Query y g yd state1)
show ?thesis using Eval.IH(2) Eval.IH(3)[OF _ _ refl] Query(1,3,5) by simp
next
case Answer
then show ?thesis by simp
qed
qed
lemma iterate_fmlookup:
assumes "iterate_dom x wn state"
and "(xd, state') = iterate x wn state"
shows "xd = mlup (σ state') x"
using assms
proof(induction rule: iterate_pinduct)
case (Iterate x wn state)
show ?case
using Iterate.hyps Iterate.prems
proof(cases rule: iterate_continue_fixpoint_cases_basic)
case (W_Fixpoint xd1 state1 infl2 stabl2)
show ?thesis
using Iterate.IH(1)[OF _ refl _ refl refl _ _ _ _ refl] W_Fixpoint(1-3,5-8,10)
by simp
next
case (Continue xd1 state1 d_new infl2 stabl2)
show ?thesis using Iterate.IH(2)[OF _ refl _ refl _ _ _ refl] Continue(1,3-6,8) by auto
qed (simp add: Iterate)
qed
corollary query_fmlookup:
assumes "query_dom y x state"
and "(xd, state') = query y x state"
shows "mlup (σ state') x = xd"
proof (cases "x ∈ called state")
case True
then show ?thesis using assms by simp
next
case False
have idom: "iterate_dom x Widening (state⦇called := insert x (called state)⦈)"
using assms(1) dom_backwards_pinduct(1)[OF assms(1) False] by simp
show ?thesis using assms False iterate_fmlookup[OF idom] by (simp split: prod.splits)
qed
lemma iterate_continue_fixpoint_cases[consumes 3]:
assumes "iterate_dom x wn state"
and "(xd, state') = iterate x wn 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 "state' = state1⦇called := (called state1) - {x}, point := (point state1) - {x}⦈"
and "xd = mlup (σ state') x"
| (W_Fixpoint) xd1 state1 infl2 stabl2
where "x ∉ stabl state" and "x ∈ point state" and "wn = Widening"
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 "mlup (σ state1) x ∇ xd1 = mlup (σ state1) x"
and "mlup (σ state1) x Δ xd1 ≠ mlup (σ state1) x"
and "(infl2, stabl2) = destab x (infl state1) (stabl state1)"
and "iterate_dom x Narrowing (state1⦇infl := infl2, stabl := stabl2,
σ := (σ state1)(x↦mlup (σ state1) x Δ xd1)⦈)"
and "(xd, state') = iterate x Narrowing (state1⦇infl := infl2, stabl := stabl2,
σ := (σ state1)(x↦mlup (σ state1) x Δ xd1)⦈)"
and "xd = mlup (σ state') x"
| (N_Fixpoint) xd1 state1
where "x ∉ stabl state" and "x ∈ point state"
and "wn = Narrowing ∨ (wn = Widening ∧ mlup (σ state') x ∇ xd1 = mlup (σ state') x)"
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 "xd = mlup (σ state') x"
and "state' = state1⦇called := (called state1) - {x}, point := (point state1) - {x}⦈"
and "xd = mlup (σ state') 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
if wn = Widening then mlup (σ state1) x ∇ 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 wn (state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ d_new)⦈)"
and "(xd, state') =
iterate x wn (state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ d_new)⦈)"
and "xd = mlup (σ state') x"
apply (rule iterate_continue_fixpoint_cases_basic[OF assms])
using iterate_fmlookup[OF assms]
by blast+
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 Widening (state⦇called := insert x (called state)⦈)"
and "(xd, state1) = iterate x Widening (state⦇called := insert x (called state)⦈)"
and "state' = state1⦇infl := fminsert (infl state1) x y⦈"
and "xd = mlup (σ state') x"
| (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 query_fmlookup[OF assms]
by blast+
end
subsection ‹Termination›
locale TD_wn_phases_term = TD_wn_phases T for
T :: "('x, 'd :: order_bot) eqsT" +
assumes finite_vars: "finite (UNIV :: 'x set)"
fixes widening_chains narrowing_chains :: "('d × 'd) set"
defines widening_chains: "widening_chains ≡ {(x,y). ∃a. x ≠ y ∧ x = y ∇ a}"
and narrowing_chains: "narrowing_chains ≡ {(x,y). ∃a. x ≠ y ∧ x = y Δ a}"
assumes widening_finite: "wf widening_chains"
and narrowing_finite: "wf narrowing_chains"
begin
subsubsection‹Construction of Well-founded Relation for Termination Proof›
type_synonym ('a,'b) query_in = "'a × 'a × ('a, 'b) state"
type_synonym ('a,'b) iterate_in = "'a × phase × ('a, 'b) state"
type_synonym ('a,'b) eval_in = "'a × ('a, 'b) strategy_tree × ('a, 'b) state"
text ‹We define the termination relation as a lexicographic order over 5-tuples. The first
component characterizes that the solver may only descend into finitely many unknowns, the second
describes an order between the three mutual recursive functions, and the third ensures that only
finitely many unknowns are queried in a right-hand side. The fourth component guarantees that an
unknown is not iterated infinitely often without becoming a widening/narrowing point and the
fifth lastly ensures that iteration of a widening/narrowing point terminates based on the
properties of the widening and narrowing operator.›
definition value_relation :: "((phase × 'd) × (phase × 'd)) set" where
"value_relation = {((p2,d2),(p1,d1)). p1 = Widening ∧ p2 = Narrowing}
∪ {((p1,d1),(p2,d2)). p1 = Widening ∧ p2 = Widening ∧ (d1,d2) ∈ widening_chains}
∪ {((p1,d1),(p2,d2)). p1 = Narrowing ∧ p2 = Narrowing ∧ (d1,d2) ∈ narrowing_chains}"
lemma wf_value_relation: "wf value_relation"
proof (intro wfI_min, goal_cases)
case (1 t Q)
define Q⇩N where qn_def: "Q⇩N = {(p,d) ∈ Q. p = Narrowing}"
define Q⇩W where qw_def: "Q⇩W = {(p,d) ∈ Q. p = Widening}"
have "Q = Q⇩N ∪ Q⇩W" unfolding qn_def qw_def using phase.exhaust by blast
define Qd⇩N where qdn_def: "Qd⇩N = {d. (Narrowing,d) ∈ Q}"
define Qd⇩W where qdw_def: "Qd⇩W = {d. (Widening,d) ∈ Q}"
show ?case
proof (cases "Qd⇩N = {}")
case True
then obtain dt where "t = (Widening,dt)"
using 1 qdn_def qdw_def phase.exhaust
by (metis (mono_tags, lifting) ex_in_conv mem_Collect_eq old.prod.exhaust)
then have "dt ∈ Qd⇩W" using qdw_def 1 by auto
then obtain d⇩m⇩i⇩n where d⇩m⇩i⇩n_def: "d⇩m⇩i⇩n ∈ Qd⇩W" "∀d'. (d',d⇩m⇩i⇩n) ∈ widening_chains ⟶ d' ∉ Qd⇩W"
by (metis wfE_min widening_finite)
then have "(Widening,d⇩m⇩i⇩n) ∈ Q" using qdw_def by simp
moreover have "((p',d'),(Widening,d⇩m⇩i⇩n)) ∈ value_relation ⟶ (p',d') ∉ Q" for p' d'
proof (rule ccontr, goal_cases)
case 1
then have "((p', d'), (Widening, d⇩m⇩i⇩n)) ∈ value_relation" "(p', d') ∈ Q" by auto
have "p' = Widening" using ‹(p', d') ∈ Q› True unfolding qdn_def by (cases p') auto
then have "(d',d⇩m⇩i⇩n) ∈ widening_chains"
using ‹((p', d'), (Widening, d⇩m⇩i⇩n)) ∈ value_relation› unfolding value_relation_def by auto
have "d' ∈ Qd⇩W" using qdw_def ‹(p', d') ∈ Q› ‹p' = Widening› by simp
moreover have "d' ∉ Qd⇩W" using d⇩m⇩i⇩n_def ‹(d',d⇩m⇩i⇩n) ∈ widening_chains› by auto
ultimately show ?case by simp
qed
ultimately show ?thesis by auto
next
case False
then obtain d⇩m⇩i⇩n where d⇩m⇩i⇩n_def: "d⇩m⇩i⇩n ∈ Qd⇩N" "∀d'. (d',d⇩m⇩i⇩n) ∈ narrowing_chains ⟶ d' ∉ Qd⇩N"
by (metis ex_in_conv wfE_min narrowing_finite)
then have "(Narrowing,d⇩m⇩i⇩n) ∈ Q" using qdn_def by simp
moreover have "((p',d'),(Narrowing,d⇩m⇩i⇩n)) ∈ value_relation ⟶ (p',d') ∉ Q" for p' d'
proof (rule ccontr, goal_cases)
case 1
then have "((p', d'), (Narrowing, d⇩m⇩i⇩n)) ∈ value_relation" "(p', d') ∈ Q" by auto
then have "p' = Narrowing" "(d',d⇩m⇩i⇩n) ∈ narrowing_chains" unfolding value_relation_def by auto
have "d' ∈ Qd⇩N" using qdn_def ‹(p', d') ∈ Q› ‹p' = Narrowing› by simp
moreover have "d' ∉ Qd⇩N" using d⇩m⇩i⇩n_def ‹(d',d⇩m⇩i⇩n) ∈ narrowing_chains› by auto
ultimately show ?case by simp
qed
ultimately show ?thesis by auto
qed
qed
definition prod_relation :: "((nat × nat × ('x, 'd) strategy_tree × bool × (phase × 'd))
× (nat × nat × ('x, 'd) strategy_tree × bool × (phase × 'd))) set" where
"prod_relation = lex_prod (measure id) (lex_prod (measure id) (lex_prod
strict_subt_relation (lex_prod (measure (λb. if ¬ b then 1 else 0)) value_relation)))"
lemma wf_prod_relation: "wf prod_relation"
unfolding prod_relation_def
using widening_finite wf_rhs_relation wf_value_relation
by auto
definition term_relation :: "((('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in) ×
(('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in)) set"
where
"term_relation = inv_image prod_relation (λst. case st of
Inl (x,y,state) ⇒ (card (UNIV - (called state)), 1, T y, False, (Widening, mlup (σ state) y))
| Inr (Inl (x,wn,state)) ⇒
(card (UNIV - (called state)), 3, T x, x ∈ point state, (wn, mlup (σ state) x))
| Inr (Inr (x,t,state)) ⇒ (card (UNIV - (called state)), 2, t, False, (Widening, mlup (σ state) x)))"
lemma wf_term_relation: "wf term_relation"
unfolding term_relation_def
by (simp add: wf_prod_relation)
subsubsection‹Auxiliary Lemmas›
lemma constant_vals_for_called:
shows "query_dom y x state
⟹ (xd, state') = query y x state
⟹ (∀u ∈ called state. mlup (σ state') u = mlup (σ state) u)"
and "iterate_dom x wn state
⟹ (xd, state') = iterate x wn state
⟹ x ∈ called state
⟹ (∀u ∈ (called state) - {x}. mlup (σ state') u = mlup (σ state) u)"
and "eval_dom x t state
⟹ (xd, state') = eval x t state
⟹ (∀u ∈ called state. mlup (σ state') u = mlup (σ state) u)"
proof(induction y x state and x wn 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.IH(1) Query.prems(1)
proof(cases rule: query_iterate_lookup_cases)
case (Iterate state1)
show ?thesis using Query.IH(2) Iterate(1,3,4) by simp
next
case Lookup
then show ?thesis by simp
qed
next
case (Iterate x wn state)
show ?case using Iterate.IH(1) Iterate.prems(1)
proof (cases rule: iterate_continue_fixpoint_cases)
case Stable
then show ?thesis by auto
next
case (Fixpoint state1)
then show ?thesis using Iterate.IH(2)[OF _ refl] by simp
next
case (W_Fixpoint xd1 state1 infl2 stabl2)
have IH1: "∀u∈called state. mlup (σ state1) u = mlup (σ state) u"
using Iterate.IH(2) W_Fixpoint(1,5) by simp
moreover have IH2:
"∀u∈called state - {x}. mlup (σ state') u = mlup ((σ state1)(x ↦ mlup (σ state1) x Δ xd1)) u"
using Iterate.IH(3)[rotated 11, OF W_Fixpoint(10)] W_Fixpoint(1-3,5-8)
Iterate.prems(2) c_same(3)[OF W_Fixpoint(4,5)]
by simp
moreover have
"∀u∈called state - {x}. mlup ((σ state1)(x ↦ mlup (σ state1) x Δ xd1)) u = mlup (σ state1) u"
by (auto simp add: fun_upd_other mlup_def)
ultimately show ?thesis by auto
next
case (N_Fixpoint xd1 state1)
show ?thesis using Iterate.IH(2) N_Fixpoint(1,5,8) by simp
next
case (Continue xd1 state1 d_new infl2 stabl2)
have IH1: "∀u∈called state. mlup (σ state1) u = mlup (σ state) u"
using Iterate.IH(2) Continue(1,3) by simp
moreover have IH2: "∀u∈called state - {x}. mlup (σ state') u = mlup ((σ state1)(x ↦ d_new)) u"
using Iterate.IH(4)[rotated 8, OF Continue(8)] Continue(1,3-6) Iterate.prems(2)
c_same(3)[OF Continue(2,3)]
by simp
ultimately show ?thesis by (auto simp add: fun_upd_other mlup_def)
qed
next
case (Eval x t state)
show ?case using Eval.IH(1) Eval.prems(1)
proof (cases rule: eval_query_answer_cases)
case (Query y g yd state1)
have IH1: "∀u∈called state. mlup (σ state1) u = mlup (σ state) u"
using Eval.IH(2)[OF Query(1,3)] by simp
have IH2: "∀u∈called state. mlup (σ state') u = mlup (σ state1) u"
using Eval.IH(3)[OF Query(1,3) _ Query(5)] c_same(1)[OF Query(2,3)] by simp
then show ?thesis using IH1 by simp
next
case Answer
then show ?thesis by auto
qed
qed
lemma point_set_subset_c:
shows "query_dom y x state
⟹ (xd, state') = query y x state
⟹ point state ⊆ called state
⟹ point state' ⊆ called state'"
and "iterate_dom x wn state
⟹ (xd, state') = iterate x wn state
⟹ x ∈ called state
⟹ point state - {x} ⊆ called state - {x}
⟹ point state' - {x} ⊆ called state' - {x} ∧ x ∉ point state'"
and "eval_dom x t state
⟹ (xd, state') = eval x t state
⟹ point state ⊆ called state
⟹ point state' ⊆ called state'"
proof(induction y x state and x wn 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.IH(1) Query.prems(1)
proof(cases rule: query_iterate_lookup_cases)
case (Iterate state1)
have IH: "point state' ⊆ (insert x (called state')) - {x}"
using Query.IH(2)[OF Iterate(1,3)] Query.prems(2) Iterate(4) by auto
moreover have "x ∉ point state" using Iterate(1) Query.prems(2) by auto
ultimately show ?thesis by auto
next
case Lookup
then show ?thesis using Query.prems(2) by auto
qed
next
case (Iterate x wn state)
have point_sub_c: "point state ⊆ called state" using Iterate.prems(2,3) by auto
show ?case using Iterate.IH(1) Iterate.prems(1)
proof (cases rule: iterate_continue_fixpoint_cases)
case Stable
then show ?thesis using Iterate.prems(3) by auto
next
case (Fixpoint state1)
show ?thesis
using Iterate.IH(2)[OF _ refl Fixpoint(4)] Fixpoint(1,2,5) point_sub_c by auto
next
case (W_Fixpoint xd1 state1 infl2 stabl2)
have IH1: "point state1 ⊆ called state1"
using Iterate.IH(2)[OF W_Fixpoint(1) _ W_Fixpoint(5)] Iterate.prems(2) point_sub_c by auto
have IH2: "point state' ⊆ called state' - {x}"
using Iterate.IH(3)[OF W_Fixpoint(1) _ W_Fixpoint(5) _ _ W_Fixpoint(6) _ _ W_Fixpoint(7,8) _
W_Fixpoint(10)] W_Fixpoint(2,3) Iterate.prems(2) c_same(3)[OF W_Fixpoint(4,5)] IH1
by auto
then show ?thesis using IH1 c_same(2)[OF W_Fixpoint(9,10)] by auto
next
case (N_Fixpoint xd1 state1)
show ?thesis
using Iterate.IH(2)[OF N_Fixpoint(1) _ N_Fixpoint(5)] N_Fixpoint(8) point_sub_c by auto
next
case (Continue xd1 state1 d_new infl2 stabl2)
have IH1: "point state1 - {x} ⊆ called state1 - {x}"
using Iterate.IH(2)[OF Continue(1) _ Continue(3)] point_sub_c by auto
then show ?thesis
using Iterate.IH(4)[OF Continue(1) _ Continue(3) _ Continue(4-6) _ Continue(8)]
Iterate.prems(2) c_same(3)[OF Continue(2,3)]
by auto
qed
next
case (Eval x t state)
show ?case using Eval.IH(1) Eval.prems(1)
proof (cases rule: eval_query_answer_cases)
case (Query y g yd state1)
have IH1: "point state1 ⊆ called state1" using Eval.IH(2)[OF Query(1,3)] Eval.prems(2) by auto
have IH2: "point state' ⊆ called state'" using Eval.IH(3)[OF Query(1,3) _ Query(5)] IH1(1) by auto
then show ?thesis by simp
next
case Answer
then show ?thesis using Eval.prems(2) by auto
qed
qed
lemma stabl_infl_properties:
shows "query_dom y x state
⟹ (xd, state') = query y x state
⟹ called state ⊆ stabl state
⟹ fset (fmdom (infl state)) ⊆ stabl state
⟹ stabl state ⊆ stabl state' ∧ fset (fmdom (infl state')) ⊆ stabl state'
∧ (∀u. (slookup (infl state') u - slookup (infl state) u) ∩ ((stabl state) - {y}) = {})"
and "iterate_dom x wn state
⟹ (xd, state') = iterate x wn state
⟹ x ∈ called state
⟹ called state - {x} ⊆ stabl state
⟹ fset (fmdom (infl state)) ⊆ stabl state
⟹ insert x (stabl state) ⊆ stabl state' ∧ fset (fmdom (infl state')) ⊆ stabl state'
∧ (∀u. (slookup (infl state') u - slookup (infl state) u) ∩ ((stabl state) - {x}) = {})"
and "eval_dom x t state
⟹ (xd, state') = eval x t state
⟹ called state ⊆ stabl state
⟹ fset (fmdom (infl state)) ⊆ stabl state
⟹ stabl state ⊆ stabl state' ∧ fset (fmdom (infl state')) ⊆ stabl state'
∧ (∀u. (slookup (infl state') u - slookup (infl state) u) ∩ ((stabl state) - {x}) = {})"
proof(induction y x state and x wn 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.IH(1) Query.prems(1)
proof(cases rule: query_iterate_lookup_cases)
case (Iterate state1)
have "insert x (called state) - {x} ⊆ stabl state"
using Iterate(4) Query.prems(2) by (auto split: if_splits)
then have IH: "insert x (stabl state) ⊆ stabl state'"
"fset (fmdom (infl state1)) ⊆ stabl state'"
"∀u. (slookup (infl state1) u - slookup (infl state) u) ∩ ((stabl state) - {x}) = {}"
using Query.IH(2)[OF Iterate(1,3)] Query.prems(3) Iterate(4) by auto
show ?thesis
proof (intro conjI, goal_cases)
case 1
then show ?case using IH(1) Iterate(4) by (auto split: if_splits)
next
case 2
then show ?case using IH(1,2) Iterate(4) fmdom_fmupd unfolding fminsert_def by auto
next
case 3
have IH': "∀u. (slookup (infl state1) u - slookup (infl state) u) ∩ (stabl state) = {}"
using IH(3) Iterate(2,3) by (cases "x ∈ stabl state") auto
then have "(slookup (infl state') u - slookup (infl state) u) ∩ ((stabl state) - {y}) = {}"
for u
using Iterate(4)
by (cases "u = x") (auto simp add: slookup_fminsert_same slookup_fminsert_other)
then show ?case by auto
qed
next
case Lookup
have "(slookup (infl state') u - slookup (infl state) u) ∩ ((stabl state) - {y}) = {}" for u
using Lookup(3)
by (cases "u = x") (auto simp add: slookup_fminsert_same slookup_fminsert_other)
then show ?thesis using Query(4,5) Lookup(1,3) unfolding fminsert_def by auto
qed
next
case (Iterate x wn state)
show ?case using Iterate.IH(1) Iterate.prems(1)
proof (cases rule: iterate_continue_fixpoint_cases)
case Stable
show ?thesis using Iterate.prems(3,4) Stable(1,3) by auto
next
case (Fixpoint state1)
show ?thesis
using Iterate.IH(2)[OF _ refl Fixpoint(4)] Fixpoint(1,5) Iterate.prems(3,4) by auto
next
case (W_Fixpoint xd1 state1 infl2 stabl2)
have IH1: "stabl state ⊆ stabl state1" "fset (fmdom (infl state1)) ⊆ stabl state1"
"∀u. (slookup (infl state1) u - slookup (infl state) u) ∩ (stabl state) = {}"
using Iterate.IH(2)[OF _ refl W_Fixpoint(5)] Iterate.prems(3,4) W_Fixpoint(1) by auto
then have "influenced_by (infl state1) x ∩ (stabl state) = {}"
using TD.new_lookup_to_infl_not_stabl W_Fixpoint(1) Iterate.prems(4)
by meson
then have "stabl state ⊆ stabl2"
using destab_infl_stabl_relation[OF W_Fixpoint(8)] ‹stabl state ⊆ stabl state1› by auto
then have "called state - {x} ⊆ stabl2" using Iterate.prems(3) by blast
moreover have "fset (fmdom infl2) ⊆ stabl2"
by (simp add: IH1(2) destab_preserves_infl_dom_stabl W_Fixpoint(8))
ultimately have
IH2: "insert x stabl2 ⊆ stabl state'" "fset (fmdom (infl state')) ⊆ stabl state'"
"∀u. (slookup (infl state') u - slookup infl2 u) ∩ (stabl2 - {x}) = {}"
using Iterate.IH(3)[OF W_Fixpoint(1) _ W_Fixpoint(5) _ _ W_Fixpoint(6) _ _ W_Fixpoint(7,8) _
W_Fixpoint(10)] W_Fixpoint(2,3) Iterate.prems(2) c_same(3)[OF W_Fixpoint(4,5)] by auto
have "(slookup (infl state') u - slookup (infl state) u) ∩ ((stabl state) - {x}) = {}" for u
proof -
have "slookup infl2 u ⊆ slookup (infl state1) u"
using destab_infl_stabl_relation[OF W_Fixpoint(8)]
by (metis empty_iff empty_set fmlookup_default_drop_set subset_iff)
then show ?thesis using IH2(3) IH1(3) ‹stabl state ⊆ stabl2› by blast
qed
then show ?thesis using IH2 ‹stabl state ⊆ stabl2› by auto
next
case (N_Fixpoint xd1 state1)
show ?thesis
using Iterate.IH(2)[OF N_Fixpoint(1) refl N_Fixpoint(5)] N_Fixpoint(8) Iterate.prems(3,4)
by auto
next
case (Continue xd1 state1 d_new infl2 stabl2)
have IH1: "insert x (stabl state) ⊆ stabl state1" "fset (fmdom (infl state1)) ⊆ stabl state1"
"∀u. (slookup (infl state1) u - slookup (infl state) u)
∩ (insert x (stabl state) - {x}) = {}"
using Iterate.IH(2)[OF Continue(1) _ Continue(3)] Iterate.prems(3,4) by auto
then have "influenced_by (infl state1) x ∩ (stabl state) = {}"
using TD.new_lookup_to_infl_not_stabl Iterate.prems(4) Continue(1) by simp
then have "stabl state ⊆ stabl2"
using ‹insert x (stabl state) ⊆ stabl state1› destab_infl_stabl_relation[OF Continue(6)]
by blast
then have "called state - {x} ⊆ stabl2" using Iterate.prems(3) by blast
moreover have "fset (fmdom infl2) ⊆ stabl2"
by (simp add: IH1(2) destab_preserves_infl_dom_stabl Continue(6))
ultimately have IH2: "insert x stabl2 ⊆ stabl state'"
"fset (fmdom (infl state')) ⊆ stabl state'"
"∀u. (slookup (infl state') u - slookup infl2 u) ∩ (stabl2 - {x}) = {}"
using Iterate.IH(4)[OF Continue(1) _ Continue(3) _ Continue(4,5,6) _ Continue(8)]
Iterate.prems(2) c_same(3)[OF Continue(2,3)]
by auto
have "(slookup (infl state') u - slookup (infl state) u) ∩ ((stabl state) - {x}) = {}" for u
proof -
have "slookup infl2 u ⊆ slookup (infl state1) u"
using destab_infl_stabl_relation[OF Continue(6)]
by (metis empty_iff empty_set fmlookup_default_drop_set subset_iff)
then show ?thesis using IH2(3) IH1(3) ‹stabl state ⊆ stabl2› by blast
qed
then show ?thesis using IH2 ‹stabl state ⊆ stabl2› by auto
qed
next
case (Eval x t state)
show ?case using Eval.IH(1) Eval.prems(1)
proof (cases rule: eval_query_answer_cases)
case (Query y g yd state1)
have IH1: "stabl state ⊆ stabl state1" "fset (fmdom (infl state1)) ⊆ stabl state1"
"∀u. (slookup (infl state1) u - slookup (infl state) u) ∩ ((stabl state) - {x}) = {}"
using Eval.IH(2)[OF Query(1,3)] Eval.prems(2,3) by auto
have "called state ⊆ stabl state1" using IH1(1) Eval.prems(2) by auto
then have IH2: "stabl state1 ⊆ stabl state'" "fset (fmdom (infl state')) ⊆ stabl state'"
"∀u. (slookup (infl state') u - slookup (infl state1) u) ∩ (stabl state1 - {x}) = {}"
using Eval.IH(3)[OF Query(1,3) _ Query(5)] IH1(2,3) c_same(1)[OF Query(2,3)] by auto
then show ?thesis using IH1 ‹stabl state ⊆ stabl state1› by blast
next
case Answer
then show ?thesis using Eval.prems(2,3) by auto
qed
qed
lemma called_with_non_empty_infl_in_point:
shows "query_dom y x state
⟹ (xd, state') = query y x state
⟹ called state ⊆ stabl state
⟹ fset (fmdom (infl state)) ⊆ stabl state
⟹ {u ∈ called state. slookup (infl state) u ≠ {}} ⊆ point state
⟹ {u ∈ called state'. slookup (infl state') u ≠ {}} ⊆ point state'"
and "iterate_dom x phase state
⟹ (xd, state') = iterate x phase state
⟹ x ∈ called state
⟹ called state - {x} ⊆ stabl state
⟹ fset (fmdom (infl state)) ⊆ stabl state
⟹ {u ∈ called state - {x}. slookup (infl state) u ≠ {}} ⊆ point state - {x}
⟹ {u ∈ called state' - {x}. slookup (infl state') u ≠ {}} ⊆ point state' - {x}"
and "eval_dom x t state
⟹ (xd, state') = eval x t state
⟹ called state ⊆ stabl state
⟹ fset (fmdom (infl state)) ⊆ stabl state
⟹ {u ∈ called state. slookup (infl state) u ≠ {}} ⊆ point state
⟹ {u ∈ called state'. slookup (infl state') u ≠ {}} ⊆ point state'"
proof (induction y x state and x phase 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.IH(1) Query.prems(1)
proof (cases rule: query_iterate_lookup_cases)
case (Iterate state1)
have IH: "{u ∈ called state1 - {x}. slookup (infl state1) u ≠ {}} ⊆ point state'"
using Query.IH(2)[OF Iterate(1,3)] Query.prems(2-4) Iterate(4)
by auto
then show ?thesis
using Iterate(1,4) slookup_fminsert_other[of _ x "infl state1" y] c_same(2)[OF Iterate(2,3)]
by force
next
case Lookup
show ?thesis
using Query.prems(2-4) Lookup(3) slookup_fminsert_other[of _ x "infl state" y]
by force
qed
next
case (Iterate x phase state)
show ?case using Iterate.IH(1) Iterate.prems(1)
proof (cases rule: iterate_continue_fixpoint_cases)
case Stable
then show ?thesis using Iterate.prems(5) by auto
next
case (Fixpoint state1)
have "slookup (infl state) x = {}"
using Fixpoint(1) Iterate.prems(4) TD.stabl_infl_empty by fast
then have "{u ∈ called state. slookup (infl state) u ≠ {}} ⊆ point state"
using Iterate.prems(5) by blast
then show ?thesis
using Iterate.IH(2)[OF Fixpoint(1) _ Fixpoint(4)] Fixpoint(5) Iterate.prems(3-4)
by force
next
case (W_Fixpoint xd1 state1 infl2 stabl2)
have "slookup (infl state) x = {}"
using W_Fixpoint(1) Iterate.prems(4) TD.stabl_infl_empty by fast
then have "{u ∈ called state. slookup (infl state) u ≠ {}} ⊆ point state"
using Iterate.prems(5) by blast
then have IH1: "{u ∈ called state1. slookup (infl state1) u ≠ {}} ⊆ point state1"
using Iterate.IH(2)[OF W_Fixpoint(1) _ W_Fixpoint(5)] Iterate.prems(2-4)
by auto
have stabl_infl_props:
"insert x (stabl state) ⊆ stabl state1"
"fset (fmdom (infl state1)) ⊆ stabl state1"
"∀u. (slookup (infl state1) u - slookup (infl state) u)
∩ (insert x (stabl state) - {x}) = {}"
using stabl_infl_properties(3)[OF W_Fixpoint(4,5)] Iterate.prems(3-4)
by auto
have "slookup infl2 u ⊆ slookup (infl state1) u" for u
using destab_infl_stabl_relation[OF W_Fixpoint(8)]
by (metis empty_iff empty_set fmlookup_default_drop_set subsetI)
then have "slookup (infl state1) u ≠ {}" if "slookup infl2 u ≠ {}" for u
using that by (metis subset_empty)
then have "{u ∈ called state1 - {x}. slookup infl2 u ≠ {}} ⊆ point state1 - {x}"
using IH1 Iterate.prems(2) by blast
moreover have "fset (fmdom infl2) ⊆ stabl2"
using destab_preserves_infl_dom_stabl[OF W_Fixpoint(8)] stabl_infl_props(2) by blast
moreover have "called state - {x} ⊆ stabl2"
proof -
have "influenced_by (infl state1) x ∩ stabl state = {}"
using TD.new_lookup_to_infl_not_stabl[of state1 state x]
W_Fixpoint(1) Iterate.prems(4) stabl_infl_props(3)
by blast
then have "stabl state ⊆ stabl2"
using stabl_infl_props(1) destab_infl_stabl_relation[OF W_Fixpoint(8)]
by blast
then show ?thesis using Iterate.prems(3) by auto
qed
ultimately have IH2:
"{u ∈ called state' - {x}. slookup (infl state') u ≠ {}} ⊆ point state' - {x}"
using Iterate.IH(3)[OF W_Fixpoint(1) _ W_Fixpoint(5) _ _ W_Fixpoint(6) _ _ W_Fixpoint(7,8) _
W_Fixpoint(10)] W_Fixpoint(2,3) Iterate.prems(2) c_same(3)[OF W_Fixpoint(4,5)]
by auto
then show ?thesis using IH1 by force
next
case (N_Fixpoint xd1 state1)
have "slookup (infl state) x = {}"
using N_Fixpoint(1) Iterate.prems(4) TD.stabl_infl_empty by fast
then have "{u ∈ called state. slookup (infl state) u ≠ {}} ⊆ point state"
using Iterate.prems(5) by blast
then have "{u ∈ called state'. slookup (infl state') u ≠ {}} ⊆ point state1"
using Iterate.IH(2)[OF N_Fixpoint(1) _ N_Fixpoint(5)] Iterate.prems(3,4) N_Fixpoint(8)
by auto
then show ?thesis using N_Fixpoint(8) Iterate.prems(2) by auto
next
case (Continue xd1 state1 d_new infl2 stabl2)
have "slookup (infl state) x = {}"
using Continue(1) Iterate.prems(4) TD.stabl_infl_empty by fast
then have "{u ∈ called state. slookup (infl state) u ≠ {}} ⊆ point state"
using Iterate.prems(5) by blast
then have IH1: "{u ∈ called state1. slookup (infl state1) u ≠ {}} ⊆ point state1"
using Iterate.IH(2)[OF Continue(1) _ Continue(3)] Iterate.prems(3-5)
by auto
have stabl_infl_props:
"insert x (stabl state) ⊆ stabl state1"
"fset (fmdom (infl state1)) ⊆ stabl state1"
"∀u. (slookup (infl state1) u - slookup (infl state) u)
∩ (insert x (stabl state) - {x}) = {}"
using stabl_infl_properties(3)[OF Continue(2,3)] Iterate.prems(3,4) by auto
have "slookup infl2 u ⊆ slookup (infl state1) u" for u
using destab_infl_stabl_relation[OF Continue(6)]
by (metis empty_iff empty_set fmlookup_default_drop_set subsetI)
then have "slookup (infl state1) u ≠ {}" if "slookup infl2 u ≠ {}" for u
using that by (metis subset_empty)
then have "{u ∈ called state1 - {x}. slookup infl2 u ≠ {}} ⊆ point state1 - {x}"
using IH1 by blast
moreover have "fset (fmdom infl2) ⊆ stabl2"
using destab_preserves_infl_dom_stabl[OF Continue(6)] stabl_infl_props(2) by simp
moreover have "called state - {x} ⊆ stabl2"
proof -
have "influenced_by (infl state1) x ∩ stabl state = {}"
using TD.new_lookup_to_infl_not_stabl[of state1 state x]
Continue(1) Iterate.prems(4) stabl_infl_props(3)
by blast
then have "stabl state ⊆ stabl2"
using stabl_infl_props(1) destab_infl_stabl_relation[OF Continue(6)] by blast
then show ?thesis using Iterate.prems(3) by simp
qed
ultimately have IH2: "{u ∈ called state' - {x}. slookup (infl state') u ≠ {}} ⊆ point state' - {x}"
using Iterate.IH(4)[OF Continue(1) _ Continue(3) _ Continue(4-6) _ Continue(8)]
Iterate.prems(2) c_same(3)[OF Continue(2,3)]
by auto
then show ?thesis using IH1 by force
qed
next
case (Eval x t state)
show ?case using Eval.IH(1) Eval.prems(1)
proof (cases rule: eval_query_answer_cases)
case (Query y g yd state1)
have IH1: "{u ∈ called state1. slookup (infl state1) u ≠ {}} ⊆ point state1"
using Eval.IH(2)[OF Query(1,3)] Eval.prems(2-4)
by auto
note stabl_infl_props = stabl_infl_properties(1)[OF Query(2,3) Eval.prems(2,3)]
then show ?thesis
using IH1 Eval.IH(3)[OF Query(1,3) _ Query(5)] Eval.prems(2) c_same(1)[OF Query(2,3)]
by auto
next
case Answer
then show ?thesis using Eval.prems(2-4) by auto
qed
qed
abbreviation point_invariant where
"point_invariant state ≡
point state ⊆ called state ∧ {u ∈ called state. slookup (infl state) u ≠ {}} ⊆ point state"
lemma well_formed_point_set:
shows "query_dom y x state
⟹ (xd, state') = query y x state
⟹ called state ⊆ stabl state
⟹ fset (fmdom (infl state)) ⊆ stabl state
⟹ point_invariant state
⟹ point_invariant state'"
and "iterate_dom x wn state
⟹ (xd, state') = iterate x wn state
⟹ x ∈ called state
⟹ called state - {x} ⊆ stabl state
⟹ fset (fmdom (infl state)) ⊆ stabl state
⟹ point_invariant (state⦇called := called state - {x}, point := point state - {x}⦈)
⟹ point_invariant (state'⦇called := called state' - {x},
point := point state' - {x}⦈) ∧ x ∉ point state'"
and "eval_dom x t state
⟹ (xd, state') = eval x t state
⟹ called state ⊆ stabl state
⟹ fset (fmdom (infl state)) ⊆ stabl state
⟹ point_invariant state
⟹ point_invariant state'"
proof goal_cases
case 1
show ?case
using point_set_subset_c(1)[OF 1(1-2)] called_with_non_empty_infl_in_point(1)[OF 1(1-4)] 1(5)
by simp
next
case 2
show ?case
using point_set_subset_c(2)[OF 2(1-3)] called_with_non_empty_infl_in_point(2)[OF 2(1-5)] 2(6)
by auto
next
case 3
show ?case
using point_set_subset_c(3)[OF 3(1-2)] called_with_non_empty_infl_in_point(3)[OF 3(1-4)] 3(5)
by simp
qed
subsubsection‹Termination Proof›
text‹In the following, we carry out a conditional termination proof for the three mutual recursive
functions of the solver. The condition demands some well-formedness properties about the solver's
data structures and is defined as follows.›
abbreviation term_cond_aux where
"term_cond_aux state ≡ point state ⊆ called state ∧ called state ⊆ stabl state ∧
fset (fmdom (infl state)) ⊆ stabl state ∧
{u ∈ called state. slookup (infl state) u ≠ {}} ⊆ point state"
abbreviation term_cond where
"term_cond st ≡ (case st of
Inl (y, x, state) ⇒ term_cond_aux state
| Inr (Inl (x, phase, state)) ⇒
x ∈ called state ∧ term_cond_aux (state⦇called := called state - {x}, point := point state - {x}⦈)
| Inr (Inr (x, t, state)) ⇒ term_cond_aux state)"
text‹With the following lemma we prove that a call to any of the three mutually recursive functions
terminates as long as the parameters fulfill the above stated termination condition. As this
condition is fulfilled by the initial solver state we can later derive that the solver
always terminates. The proof is an induction with the well-founded @{term term_relation}
constructed above. To apply the induction hypotheses, it thus needs to be shown, that the
parameters of a recursive function call decrease compared to the parameters of the wrapping
function call and with respect to the @{term term_relation}.›
lemma cond_termination: "query_iterate_eval_dom st" if "term_cond st"
using wf_term_relation that
proof (induction st rule: wf_induct_rule[where ?r = term_relation])
case (less st)
then consider (Query) y x state where "st = Inl (y, x, state)"
| (Iterate) x wn state where "st = Inr (Inl (x, wn, state))"
| (Eval) x t state where "st = Inr (Inr (x, t, state))"
by (auto split: sum.splits)
then show ?case
proof cases
case Query
show ?thesis
proof (cases "x ∈ called state")
case True
then show ?thesis using Query query_iterate_eval.domintros(1) by fast
next
case False
have "point state ⊆ called state" using less.prems Query by simp
have "card (UNIV - (insert x (called state))) < card (UNIV - called state)"
using finite_vars False
by (metis Diff_iff Diff_insert UNIV_I card_Diff1_less finite_Diff)
then have "(Inr (Inl (x, Widening, state⦇called := insert x (called state)⦈)), st) ∈ term_relation"
unfolding term_relation_def prod_relation_def Query
by auto
moreover have "term_cond (Inr (Inl (x, Widening, state⦇called := insert x (called state)⦈)))"
using less.prems Query False by auto
ultimately have "iterate_dom x Widening (state⦇called := insert x (called state)⦈)"
using less.IH by simp
then show ?thesis
using Query False query_iterate_eval.domintros(1) by simp
qed
next
case Iterate
have xcalled: "x ∈ called state" and p_sub_called: "point state ⊆ called state"
using Iterate less(2) by auto
show ?thesis
proof (cases "x ∈ stabl state")
case True
then show ?thesis using Iterate query_iterate_eval.domintros(2) by blast
next
case False
have "(Inr (Inr (x, T x, state⦇stabl := insert x (stabl state)⦈)), st) ∈ term_relation"
using Iterate unfolding term_relation_def prod_relation_def by simp
moreover have "term_cond (Inr (Inr (x, T x, state⦇stabl := insert x (stabl state)⦈)))"
proof -
have "slookup (infl state) x = {}"
using less.prems Iterate TD.stabl_infl_empty[OF False] by auto
then show ?thesis using Iterate less.prems by auto
qed
ultimately have eval_dom: "eval_dom x (T x) (state⦇stabl := insert x (stabl state)⦈)"
using less.IH by auto
then obtain xd state1 where
eval: "(xd, state1) = eval x (T x) (state⦇stabl := insert x (stabl state)⦈)"
by (metis surj_pair)
have stabl_infl_props1: "insert x (stabl state) ⊆ stabl state1"
"fset (fmdom (infl state1)) ⊆ stabl state1"
"∀u. (slookup (infl state1) u - slookup (infl state) u) ∩ (stabl state) = {}"
using stabl_infl_properties(3)[OF eval_dom eval] less.prems Iterate False
by auto
have non_empty_infl_point1: "point state1 ⊆ called state1"
"{u ∈ called state1. slookup (infl state1) u ≠ {}} ⊆ point state1"
proof -
have "slookup (infl state) x = {}"
using False less.prems Iterate TD.stabl_infl_empty by auto
then have "{u ∈ called state. slookup (infl state) u ≠ {}} ⊆ point state"
using less.prems Iterate by auto
then show "point state1 ⊆ called state1"
"{u ∈ called state1. slookup (infl state1) u ≠ {}} ⊆ point state1"
using well_formed_point_set(3)[OF eval_dom eval] less.prems Iterate by auto
qed
obtain infl2 stabl2 where
destab: "(infl2, stabl2) = destab x (infl state1) (stabl state1)"
by (cases "destab x (infl state1) (stabl state1)") simp
have term_cond2: "point state1 ⊆ called state1"
"called state1 - {x} ⊆ stabl2" "fset (fmdom infl2) ⊆ stabl2"
"{u ∈ called state1 - {x}. slookup infl2 u ≠ {}} ⊆ (point state1) - {x}"
proof (goal_cases)
case 1
then show ?case using ‹point state1 ⊆ called state1› by auto
next
case 2
have "influenced_by (infl state1) x ∩ (stabl state) = {}"
using TD.new_lookup_to_infl_not_stabl[of state1 state x] False stabl_infl_props1(3)
less.prems Iterate
by auto
then have "stabl state ⊆ stabl2"
using ‹insert x (stabl state) ⊆ stabl state1› destab_infl_stabl_relation[OF destab]
by blast
then show ?case using Iterate less.prems c_same(3)[OF eval_dom eval] by auto
next
case 3
then show ?case
using destab_preserves_infl_dom_stabl[OF destab] stabl_infl_props1(2)
by simp
next
case 4
have "slookup infl2 u ⊆ slookup (infl state1) u" for u
using destab_infl_stabl_relation[OF destab]
by (metis empty_iff empty_set fmlookup_default_drop_set subsetI)
then show ?case using non_empty_infl_point1 subset_empty by fastforce
qed
show ?thesis
proof (cases "x ∈ point state")
case True
then show ?thesis
proof (cases wn)
case Widening
show ?thesis
proof (cases "mlup (σ state1) x = mlup (σ state1) x ∇ xd")
case True
show ?thesis
proof (cases "mlup (σ state1) x Δ xd = mlup (σ state1) x")
case True
then show ?thesis
using Iterate ‹x ∉ stabl state› ‹x ∈ point state› eval_dom eval
‹mlup (σ state1) x = mlup (σ state1) x ∇ xd› Widening
query_iterate_eval.domintros(2)[of x state wn]
by (cases "eval x (T x) (state⦇stabl := insert x (stabl state)⦈)") auto
next
case False
define st' where st':
"st' :: ('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in ≡
Inr (Inl (x, Narrowing, state1⦇infl := infl2, stabl := stabl2,
σ := (σ state1)(x ↦ mlup (σ state1) x Δ xd)⦈))"
have "iterate_dom x Narrowing (state1⦇infl := infl2, stabl := stabl2,
σ := (σ state1)(x ↦ mlup (σ state1) x Δ xd)⦈)"
proof (cases "x ∈ point state1")
case True
have "insert x ((called state) - {x}) = called state" using less(2) Iterate by auto
then have "(st', st) ∈ term_relation"
using st' Iterate ‹x ∈ point state› Widening True c_same(3)[OF eval_dom eval]
unfolding term_relation_def prod_relation_def value_relation_def
by auto
moreover have "term_cond st'"
using term_cond2 st' xcalled c_same(3)[OF eval_dom eval] by auto
ultimately show ?thesis
using less(1) st' ‹point state1 ⊆ called state1› xcalled by force
next
case False
then have "slookup (infl state1) x = {}"
using non_empty_infl_point1 xcalled c_same(3)[OF eval_dom eval] by auto
then have "influenced_by (infl state1) x = {}"
by (metis influenced_by_aux UN_E all_not_in_conv)
then have "x ∈ stabl2"
using destab_infl_stabl_relation destab stabl_infl_props1(1)
by fastforce
then show ?thesis
using query_iterate_eval.domintros(2)[folded dom_defs, of x] by fastforce
qed
then show ?thesis
using Iterate ‹x ∉ stabl state› ‹x ∈ point state› eval_dom eval
‹mlup (σ state1) x = mlup (σ state1) x ∇ xd›
destab Widening query_iterate_eval.domintros(2)[of x state]
by (cases "eval x (T x) (state⦇stabl := insert x (stabl state)⦈)",
cases "destab x (infl state1) (stabl state1)", cases wn) auto
qed
next
case False
define st' where st':
"st' :: ('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in ≡
Inr (Inl (x, wn, state1⦇infl := infl2, stabl := stabl2,
σ := (σ state1)(x ↦ mlup (σ state1) x ∇ xd)⦈))"
have "iterate_dom x wn (state1⦇infl := infl2, stabl := stabl2,
σ := (σ state1)(x ↦ mlup (σ state1) x ∇ xd)⦈)"
proof (cases "x ∈ point state1")
case True
moreover have "(mlup ((σ state1)(x ↦ mlup (σ state1) x ∇ xd)) x, mlup (σ state) x)
∈ widening_chains"
proof -
have "mlup ((σ state1)(x ↦ mlup (σ state1) x ∇ xd)) x = mlup (σ state1) x ∇ xd"
unfolding mlup_def by (simp add: fun_upd_same)
moreover have "mlup (σ state1) x = mlup (σ state) x"
using constant_vals_for_called(3)[OF eval_dom eval] xcalled by simp
moreover have "mlup (σ state) x ∇ xd ≠ mlup (σ state) x"
using False ‹mlup (σ state1) x = mlup (σ state) x› by simp
ultimately show ?thesis unfolding widening_chains by auto
qed
ultimately have "(st', st) ∈ term_relation"
using st' Iterate ‹x ∈ point state› Widening c_same(3)[OF eval_dom eval]
unfolding term_relation_def prod_relation_def value_relation_def by simp
moreover have "term_cond st'"
using term_cond2 st' xcalled c_same(3)[OF eval_dom eval] by auto
ultimately show ?thesis
using less st' Iterate ‹point state1 ⊆ called state1› xcalled by force
next
case False
then have "slookup (infl state1) x = {}"
using non_empty_infl_point1 ‹x ∈ called state› c_same(3)[OF eval_dom eval] by auto
then have "influenced_by (infl state1) x = {}"
by (metis influenced_by_aux UN_E all_not_in_conv)
then have "x ∈ stabl2"
using destab_infl_stabl_relation destab stabl_infl_props1(1) by fastforce
then show ?thesis
using query_iterate_eval.domintros(2)[folded dom_defs, of x "state1⦇infl := infl2,
stabl := stabl2, σ := (σ state1)(x ↦ mlup (σ state1) x ∇ xd)⦈"]
by simp
qed
then show ?thesis
using Iterate ‹x ∉ stabl state› ‹x ∈ point state› eval_dom eval False destab Widening
query_iterate_eval.domintros(2)[of x state]
by (cases "eval x (T x) (state⦇stabl := insert x (stabl state)⦈)",
cases "destab x (infl state1) (stabl state1)", cases wn) auto
qed
next
case Narrowing
show ?thesis
proof (cases "mlup (σ state1) x = mlup (σ state1) x Δ xd")
case True
then show ?thesis
using Iterate ‹x ∉ stabl state› ‹x ∈ point state› eval_dom eval Narrowing
query_iterate_eval.domintros(2)[of x state]
by (cases "eval x (T x) (state⦇stabl := insert x (stabl state)⦈)") auto
next
case False
define st' where st':
"st' :: ('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in ≡
Inr (Inl (x, wn, state1⦇infl := infl2, stabl := stabl2,
σ := (σ state1)(x ↦ mlup (σ state1) x Δ xd)⦈))"
have "iterate_dom x wn (state1⦇infl := infl2, stabl := stabl2,
σ := (σ state1)(x ↦ mlup (σ state1) x Δ xd)⦈)"
proof (cases "x ∈ point state1")
case True
moreover have "(mlup ((σ state1)(x ↦ mlup (σ state1) x Δ xd)) x, mlup (σ state) x)
∈ narrowing_chains"
proof -
have "mlup ((σ state1)(x ↦ mlup (σ state1) x Δ xd)) x = mlup (σ state1) x Δ xd"
unfolding mlup_def by (simp add: fun_upd_same)
moreover have "mlup (σ state1) x = mlup (σ state) x"
using constant_vals_for_called(3)[OF eval_dom eval] xcalled by simp
moreover have "mlup (σ state) x Δ xd ≠ mlup (σ state) x"
using False ‹mlup (σ state1) x = mlup (σ state) x› by auto
ultimately show ?thesis unfolding narrowing_chains by auto
qed
ultimately have "(st', st) ∈ term_relation"
using Iterate st' Narrowing c_same(3)[OF eval_dom eval]
unfolding term_relation_def prod_relation_def value_relation_def
by simp
moreover have "term_cond st'"
using term_cond2 st' xcalled c_same(3)[OF eval_dom eval] by auto
ultimately show ?thesis
using less st' Iterate ‹point state1 ⊆ called state1› xcalled by force
next
case False
then have "slookup (infl state1) x = {}"
using non_empty_infl_point1 xcalled c_same(3)[OF eval_dom eval] by auto
then have "influenced_by (infl state1) x = {}"
using influenced_by_aux by force
then have "x ∈ stabl2"
using destab_infl_stabl_relation destab stabl_infl_props1(1) by fastforce
then show ?thesis
using query_iterate_eval.domintros(2)[folded dom_defs, of x "state1⦇infl := infl2,
stabl := stabl2, σ := (σ state1)(x ↦ mlup (σ state1) x Δ xd)⦈"]
by simp
qed
then show ?thesis
using Iterate ‹x ∉ stabl state› ‹x ∈ point state› eval_dom eval False destab Narrowing
query_iterate_eval.domintros(2)[of x state]
by (cases "eval x (T x) (state⦇stabl := insert x (stabl state)⦈)",
cases "destab x (infl state1) (stabl state1)", cases wn) auto
qed
qed
next
case False
show ?thesis
proof (cases "mlup (σ state1) x = xd")
case True
then show ?thesis
using Iterate ‹x ∉ stabl state› ‹x ∉ point state› eval_dom eval
query_iterate_eval.domintros(2)[of x state]
by (cases "eval x (T x) (state⦇stabl := insert x (stabl state)⦈)") auto
next
case False
define st' where st': "st' :: ('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in ≡
Inr (Inl (x, wn, state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ xd)⦈))"
have "iterate_dom x wn (state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(x ↦ xd)⦈)"
proof (cases "x ∈ point state1")
case True
then have "(st', st) ∈ term_relation"
using st' Iterate ‹x ∉ point state› c_same(3)[OF eval_dom eval]
unfolding term_relation_def prod_relation_def by simp
moreover have "term_cond st'"
using term_cond2 st' xcalled c_same(3)[OF eval_dom eval] by auto
ultimately show ?thesis
using less st' Iterate ‹point state1 ⊆ called state1› xcalled by force
next
case False
have prems: "point state ⊆ called state" "called state ⊆ insert x (stabl state)"
"fset (fmdom (infl state)) ⊆ stabl state"
"{u ∈ called state - {x}. slookup (infl state) u ≠ {}} ⊆ point state - {x}"
using less.prems Iterate by auto
have "called state ⊆ stabl state1"
using stabl_infl_properties(3)[OF eval_dom eval] prems(2,3) stabl_infl_props1(1)
by blast
have "{u ∈ called state. slookup (infl state) u ≠ {}} ⊆ point state"
proof -
have "slookup (infl state) x = {}"
using ‹x ∉ stabl state› prems(3) TD.stabl_infl_empty by simp
then show ?thesis using prems(4) by auto
qed
then have "{u ∈ called state1. slookup (infl state1) u ≠ {}} ⊆ point state1"
using well_formed_point_set(3)[OF eval_dom eval] prems(1-3) by auto
then have "slookup (infl state1) x = {}"
using False xcalled c_same(3)[OF eval_dom eval] by auto
then have "influenced_by (infl state1) x = {}" using influenced_by_aux by force
then have "stabl state1 = stabl2"
using destab_infl_stabl_relation[OF destab] by simp
then have "x ∈ stabl2" using xcalled ‹called state ⊆ stabl state1› by blast
then show ?thesis using query_iterate_eval.domintros(2) by force
qed
then show ?thesis
using Iterate ‹x ∉ stabl state› ‹x ∉ point state› eval_dom eval False destab
query_iterate_eval.domintros(2)[of x state]
by (cases "eval x (T x) (state⦇stabl := insert x (stabl state)⦈)",
cases "destab x (infl state1) (stabl state1)", cases wn) auto
qed
qed
qed
next
case Eval
show ?thesis
proof (cases t)
case (Answer d)
then show ?thesis using Eval query_iterate_eval.domintros(3) by auto
next
case (Query y g)
have "(Inl (x, y, state), st) ∈ term_relation"
unfolding term_relation_def prod_relation_def Eval by simp
moreover have "term_cond (Inl (x, y, state))" using less.prems Eval by simp
ultimately have query_dom: "query_dom x y state" using less.IH by simp
then obtain d' state' where query: "(d', state') = query x y state"
by (cases "query x y state") auto
have "eval_dom x (g d') state'"
proof -
have "d' = mlup (σ state') y" using query_fmlookup query_dom_def query query_dom by metis
then have "(g d', t) ∈ strict_subt_relation" using Query direct_subt.intros by fastforce
then have "(Inr (Inr (x, g d', state')), st) ∈ term_relation"
using Eval c_same(1)[OF query_dom query] unfolding term_relation_def prod_relation_def
by simp
moreover have "term_cond (Inr (Inr (x, g d', state')))"
proof -
have "stabl state ⊆ stabl state'" "fset (fmdom (infl state')) ⊆ stabl state'"
"(∀u. (slookup (infl state') u - slookup (infl state) u) ∩ (stabl state - {x}) = {})"
using less.prems Eval stabl_infl_properties(1)[OF query_dom query] by auto
moreover have "called state ⊆ stabl state" using less.prems Eval by simp
moreover have "point state' ⊆ called state'"
"{u ∈ called state'. slookup (infl state') u ≠ {}} ⊆ point state'"
using less.prems Eval well_formed_point_set(1)[OF query_dom query]
by auto
ultimately show ?thesis using c_same(1)[OF query_dom query] by auto
qed
ultimately show ?thesis using less.IH unfolding eval_dom_def by auto
qed
then show ?thesis
using Eval Query query_dom query unfolding query_dom_def
by (auto intro: query_iterate_eval.domintros(3)[of _ x state] split: prod.splits)
qed
qed
qed
corollary solve_termination: "solve_dom x"
unfolding solve_dom_def iterate_dom_def by (auto intro: cond_termination)
end
end