Theory DP_CRelVH

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
  includes lifting_syntax heap_monad_syntax
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)
    App Heap_Monad_Ext.fun_app_lifted"
  unfolding Heap_Monad_Ext.fun_app_lifted_def App_def by transfer_prover

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 *)