Theory Default_St_Restriction_Refinement

theory Default_St_Restriction_Refinement
  imports Default_St_Reachability "Voblint_Framework.State_Restriction"
begin

unbundle default_st_syntax

section ‹Refinement between executable and abstract split states›

text ‹
  The readback ‹ρ⇘𝒢⇙› maps an executable \<^typ>‹'a default_st›
  to the abstract \<^typ>‹'a abs_state› it represents. It is a homomorphism
  for the local/global projections and for the routed combine, so an executable
  step and its abstract counterpart agree on the represented functions.
›

subsection ‹The represented function of ownership projections›
lemma default_st_to_fun_restrict_local_for [simp]:
  "ρ⇘𝒢⇙ (restrict_local_default_st s) = restrict_local_for 𝒢 (ρ⇘𝒢⇙ s)"
  unfolding restrict_local_for_def
  by (rule ext) simp

lemma default_st_to_fun_restrict_global_for [simp]:
  "ρ⇘𝒢⇙ (restrict_global_default_st s) = restrict_global_for 𝒢 (ρ⇘𝒢⇙ s)"
  unfolding restrict_global_for_def
  by (rule ext) simp

subsection ‹The represented function of joins›

text ‹
  The lifted readback commutes with joins and is monotone. The join law is
  stated for the lifted carrier itself: the generic \<^const>‹map_lift› form
  matches a schematic function and sends the simplifier into higher-order
  search.
›

lemma map_lift_default_st_to_fun_sup [simp]:
  "ρ⇘𝒢⇙ (a ⊔ b :: _ default_st lifted) = ρ⇘𝒢⇙ a ⊔ ρ⇘𝒢⇙ b"
  by (cases a; cases b) simp_all

lemma map_lift_default_st_to_fun_mono:
  assumes "x ≤ (y :: _ default_st lifted)"
  shows "ρ⇘𝒢⇙ x ≤ ρ⇘𝒢⇙ y"
  using assms by (cases x; cases y; simp add: default_st_to_fun_mono)

end