Theory Pairing_Heap_LLVM.Map_Fun_Rel

theory Map_Fun_Rel
  imports More_Sepref.WB_More_Refinement
begin

subsection ‹Refinement from function to lists›

text ‹Throughout our formalization, we often use functions at the most abstract level, that we refine to
lists assuming a known domain.

One thing to remark is that I have changed my mind on how to do things. Before we refined things
directly and kept the domain implicit. Nowadays, I make the domain explicit -- even if this means
that we have to duplicate the information of the domain through all the components of our state.
›
paragraph ‹Definition›

definition map_fun_rel :: ‹(nat × 'key) set ⇒ ('b × 'a) set ⇒ ('b list × ('key ⇒ 'a)) set› where
  map_fun_rel_def_internal:
    ‹map_fun_rel D R = {(m, f). ∀(i, j)∈D. i < length m ∧ (m ! i, f j) ∈ R}›

lemma map_fun_rel_def:
  ‹⟨R⟩map_fun_rel D = {(m, f). ∀(i, j)∈D. i < length m ∧ (m ! i, f j) ∈ R}›
  unfolding relAPP_def map_fun_rel_def_internal by auto


lemma map_fun_rel_nth:
  ‹(xs,ys)∈⟨R⟩map_fun_rel D ⟹ (i,j)∈D ⟹ (xs ! i , ys j) ∈ R›
  unfolding map_fun_rel_def by auto
(*TODO is that really useful here?*)



paragraph ‹In combination with lists›

definition length_ll_f where
  ‹length_ll_f W L = length (W L)›

lemma map_fun_rel_length:
  ‹(xs,ys)∈⟨⟨R⟩list_rel⟩map_fun_rel D ⟹ (i,j)∈D ⟹ (length_ll xs i, length_ll_f ys j) ∈ nat_rel›
  unfolding map_fun_rel_def by (auto simp: length_ll_def length_ll_f_def
    dest!: bspec list_rel_imp_same_length)

(*TODO is this used or is only the definition unfolded*)
definition append_update :: ‹('a ⇒ 'b list) ⇒ 'a ⇒ 'b ⇒ 'a ⇒ 'b list› where
  ‹append_update W L a = W(L:= W (L) @ [a])›

end