# Theory DP_CRelVH

theory DP_CRelVH
imports State_Heap
```subsection ‹Parametricity of the Heap Monad›

theory DP_CRelVH
imports State_Heap
begin

locale dp_heap =
state_dp_consistency: dp_consistency lookup_st update_st P dp + heap_mem_defs Q lookup update
for P Q :: "heap ⇒ bool" and dp :: "'k ⇒ 'v" and lookup :: "'k ⇒ 'v option Heap"
and lookup_st update update_st +
assumes
rel_state_lookup: "rel_fun (=) (rel_state (=)) lookup_st lookup"
and
rel_state_update: "rel_fun (=) (rel_fun (=) (rel_state (=))) update_st update"
begin

context
begin

definition "crel_vs R v f ≡
∀heap. P heap ∧ Q heap ∧ state_dp_consistency.cmem heap ⟶
(case execute f heap of
None ⇒ False |
Some (v', heap') ⇒ P heap' ∧ Q heap' ∧ R v v' ∧ state_dp_consistency.cmem heap'
)
"

abbreviation rel_fun_lifted :: "('a ⇒ 'c ⇒ bool) ⇒ ('b ⇒ 'd ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ ('c ==H⟹ 'd) ⇒ bool" (infixr "===>⇩T" 55) where
"rel_fun_lifted R R' ≡ R ===> crel_vs R'"

definition consistentDP :: "('k ⇒ 'v Heap) ⇒ bool" where
"consistentDP ≡ ((=) ===> crel_vs (=)) dp"

lemma consistentDP_intro:
assumes "⋀param. Transfer.Rel (crel_vs (=)) (dp param) (dp⇩T param)"
shows "consistentDP dp⇩T"
using assms unfolding consistentDP_def Rel_def by blast

lemma crel_vs_execute_None:
False if "crel_vs R a b" "execute b heap = None" "P heap" "Q heap" "state_dp_consistency.cmem heap"
using that unfolding crel_vs_def by auto

lemma crel_vs_execute_Some:
assumes "crel_vs R a b" "P heap" "Q heap" "state_dp_consistency.cmem heap"
obtains x heap' where "execute b heap = Some (x, heap')" "P heap'" "Q heap'"
using assms unfolding crel_vs_def by (cases "execute b heap") auto

lemma crel_vs_executeD:
assumes "crel_vs R a b" "P heap" "Q heap" "state_dp_consistency.cmem heap"
obtains x heap' where
"execute b heap = Some (x, heap')" "P heap'" "Q heap'" "state_dp_consistency.cmem heap'" "R a x"
using assms unfolding crel_vs_def by (cases "execute b heap") auto

lemma crel_vs_success:
assumes "crel_vs R a b" "P heap" "Q heap" "state_dp_consistency.cmem heap"
shows "success b heap"
using assms unfolding success_def by (auto elim: crel_vs_executeD)

lemma crel_vsI: "crel_vs R a b" if "(state_dp_consistency.crel_vs R OO rel_state (=)) a b"
using that by (auto 4 3 elim: state_dp_consistency.crel_vs_elim rel_state_elim simp: crel_vs_def)

lemma transfer'_return[transfer_rule]:
"(R ===> crel_vs R) Wrap return"
proof -
have "(R ===> (state_dp_consistency.crel_vs R OO rel_state (=))) Wrap return"
by (rule rel_fun_comp1 state_dp_consistency.return_transfer transfer_return)+ auto
then show ?thesis
by (blast intro: rel_fun_mono crel_vsI)
qed

lemma crel_vs_return:
"Transfer.Rel (crel_vs R) (Wrap x) (return y)" if "Transfer.Rel R x y"
using that unfolding Rel_def by (rule transfer'_return[unfolded rel_fun_def, rule_format])

lemma crel_vs_return_ext:
"⟦Transfer.Rel R x y⟧ ⟹ Transfer.Rel (crel_vs R) x (Heap_Monad.return y)"
by (fact crel_vs_return[unfolded Wrap_def])
term 0 (**)

lemma bind_transfer[transfer_rule]:
"(crel_vs R0 ===> (R0 ===> crel_vs R1) ===> crel_vs R1) (λv f. f v) (⤜)"
unfolding rel_fun_def bind_def
by safe (subst crel_vs_def, auto 4 4 elim: crel_vs_execute_Some elim!: crel_vs_executeD)

lemma crel_vs_update:
"crel_vs (=) () (update param (dp param))"
by (rule
crel_vsI relcomppI state_dp_consistency.crel_vs_update
rel_state_update[unfolded rel_fun_def, rule_format] HOL.refl
)+

lemma crel_vs_lookup:
"crel_vs
(λ v v'. case v' of None ⇒ True | Some v' ⇒ v = v' ∧ v = dp param) (dp param) (lookup param)"
by (rule
crel_vsI relcomppI state_dp_consistency.crel_vs_lookup
rel_state_lookup[unfolded rel_fun_def, rule_format] HOL.refl
)+

lemma crel_vs_eq_eq_onp:
"crel_vs (eq_onp (λ x. x = v)) v s" if "crel_vs (=) v s"
using that unfolding crel_vs_def by (auto split: option.split simp: eq_onp_def)

lemma crel_vs_bind_eq:
"⟦crel_vs (=) v s; crel_vs R (f v) (sf v)⟧ ⟹ crel_vs R (f v) (s ⤜ sf)"
by (erule bind_transfer[unfolded rel_fun_def, rule_format, OF crel_vs_eq_eq_onp])
(auto simp: eq_onp_def)

lemma crel_vs_checkmem:
"Transfer.Rel (crel_vs R) (dp param) (checkmem param s)" if "is_equality R" "Transfer.Rel (crel_vs R) (dp param) s"
unfolding checkmem_def Rel_def that(1)[unfolded is_equality_def]
by (rule bind_transfer[unfolded rel_fun_def, rule_format, OF crel_vs_lookup])
(auto 4 3 split: option.split_asm intro: crel_vs_bind_eq crel_vs_update crel_vs_return[unfolded Wrap_def Rel_def] that(2)[unfolded Rel_def that(1)[unfolded is_equality_def]])

lemma crel_vs_checkmem_tupled:
assumes "v = dp param"
shows "⟦is_equality R; Transfer.Rel (crel_vs R) v s⟧
⟹ Transfer.Rel (crel_vs R) v (checkmem param s)"
unfolding assms by (fact crel_vs_checkmem)

lemma transfer_fun_app_lifted[transfer_rule]:
"(crel_vs (R0 ===> crel_vs R1) ===> crel_vs R0 ===> crel_vs R1)

lemma crel_vs_fun_app:
"⟦Transfer.Rel (crel_vs R0) x x⇩T; Transfer.Rel (crel_vs (R0 ===>⇩T R1)) f f⇩T⟧ ⟹ Transfer.Rel (crel_vs R1) (App f x) (f⇩T . x⇩T)"
unfolding Rel_def using transfer_fun_app_lifted[THEN rel_funD, THEN rel_funD] .

end (* Lifting Syntax *)

end (* Dynamic Programming Problem *)

locale dp_consistency_heap = heap_correct +
fixes dp :: "'a ⇒ 'b"
begin

interpretation state_mem_correct: mem_correct lookup' update' P
by (rule mem_correct_heap)

interpretation state_dp_consistency: dp_consistency lookup' update' P dp ..

lemma dp_heap: "dp_heap P P lookup lookup' update update'"
by (standard; rule transfer_lookup transfer_update)

sublocale dp_heap P P dp lookup lookup' update update'
by (rule dp_heap)

notation rel_fun_lifted (infixr "===>⇩T" 55)
end

locale heap_correct_empty = heap_correct +
fixes empty
assumes empty_correct: "map_of_heap empty ⊆⇩m Map.empty" and P_empty: "P empty"

locale dp_consistency_heap_empty =
dp_consistency_heap + heap_correct_empty
begin

lemma cmem_empty:
"state_dp_consistency.cmem empty"
using empty_correct
unfolding state_dp_consistency.cmem_def
unfolding map_of_heap_def
unfolding state_dp_consistency.map_of_def
unfolding lookup'_def
unfolding map_le_def
by auto

corollary memoization_correct:
"dp x = v" "state_dp_consistency.cmem m" if
"consistentDP dp⇩T" "Heap_Monad.execute (dp⇩T x) empty = Some (v, m)"
using that unfolding consistentDP_def
by (auto dest!: rel_funD[where x = x] elim!: crel_vs_executeD intro: P_empty cmem_empty)

lemma memoized_success:
"success (dp⇩T x) empty" if "consistentDP dp⇩T"
using that cmem_empty P_empty
by (auto dest!: rel_funD intro: crel_vs_success simp: consistentDP_def)

lemma memoized:
"dp x = fst (the (Heap_Monad.execute (dp⇩T x) empty))" if "consistentDP dp⇩T"
using surjective_pairing memoization_correct(1)[OF that]
memoized_success[OF that, unfolded success_def]
by (cases "execute (dp⇩T x) empty"; auto)

lemma cmem_result:
"state_dp_consistency.cmem (snd (the (Heap_Monad.execute (dp⇩T x) empty)))" if "consistentDP dp⇩T"
using surjective_pairing memoization_correct(2)[OF that(1)]
memoized_success[OF that, unfolded success_def]
by (cases "execute (dp⇩T x) empty"; auto)

end

end (* Theory *)
```