Theory State_Restriction

theory State_Restriction
  imports "Voblint_VIMP.VIMP_Globals" "Voblint_Domain.Nonrelational_State"
    "Voblint_Domain.Reachability_Lift"
begin

section ‹Local/global restriction of abstract states›

text ‹
  A variable classifier selects one half of an abstract state and replaces the
  other with \<^const>‹bot›. Both restrictions specialize the generic
  \<^const>‹combine_env› selector. Their join recovers the original state;
  they preserve joins, are idempotent, and annihilate each other.
›

definition restrict_local_for ::
  "(vname => bool) => 'a::bounded_semilattice_sup_bot abs_state => 'a abs_state" where
  "restrict_local_for 𝒢 sigma = combine_env 𝒢 sigma bot"

definition restrict_global_for ::
  "(vname => bool) => 'a::bounded_semilattice_sup_bot abs_state => 'a abs_state" where
  "restrict_global_for 𝒢 sigma = combine_env 𝒢 bot sigma"

lemma restrict_local_for_join [simp]:
  "restrict_local_for 𝒢 (A ⊔ B) = restrict_local_for 𝒢 A ⊔ restrict_local_for 𝒢 B"
  unfolding restrict_local_for_def sup_fun_def by (rule ext) simp

lemma restrict_global_for_join [simp]:
  "restrict_global_for 𝒢 (A ⊔ B) = restrict_global_for 𝒢 A ⊔ restrict_global_for 𝒢 B"
  unfolding restrict_global_for_def sup_fun_def by (rule ext) simp

lemma restrict_local_for_idem [simp]:
  "restrict_local_for 𝒢 (restrict_local_for 𝒢 A) = restrict_local_for 𝒢 A"
  unfolding restrict_local_for_def by (rule ext) simp

lemma restrict_global_for_idem [simp]:
  "restrict_global_for 𝒢 (restrict_global_for 𝒢 A) = restrict_global_for 𝒢 A"
  unfolding restrict_global_for_def by (rule ext) simp

lemma map_lift_restrict_global_for_idem [simp]:
  fixes x :: "'a::bounded_semilattice_sup_bot abs_state lifted"
  shows "map_lift (restrict_global_for 𝒢) (map_lift (restrict_global_for 𝒢) x)
           = map_lift (restrict_global_for 𝒢) x"
  unfolding map_lift_comp o_def by simp

lemma restrict_local_for_restrict_global_for_bot [simp]:
  "restrict_local_for 𝒢 (restrict_global_for 𝒢 A) = bot"
  unfolding restrict_local_for_def restrict_global_for_def by (rule ext) simp

lemma restrict_global_for_restrict_local_for_bot [simp]:
  "restrict_global_for 𝒢 (restrict_local_for 𝒢 A) = bot"
  unfolding restrict_local_for_def restrict_global_for_def by (rule ext) simp

lemma restrict_local_for_global_join [simp]:
  "restrict_local_for 𝒢 d ⊔ restrict_global_for 𝒢 d = d"
  unfolding restrict_local_for_def restrict_global_for_def sup_fun_def
  by (rule ext) simp

lemma restrict_global_for_local_join [simp]:
  "restrict_global_for 𝒢 d ⊔ restrict_local_for 𝒢 d = d"
  unfolding restrict_local_for_def restrict_global_for_def sup_fun_def
  by (rule ext) simp

text ‹
  The selector equals the join of its disjoint local and global projections.
  This bridge lets state proofs use the restriction algebra without unfolding
  \<^const>‹combine_env›.
›

lemma combine_env_for_eq_restrictions:
  "combine_env 𝒢 sc se =
     restrict_local_for 𝒢 sc ⊔ restrict_global_for 𝒢 se"
  unfolding combine_env_def restrict_local_for_def restrict_global_for_def
    sup_fun_def
  by (rule ext) simp

subsection ‹Lifted restrictions›

text ‹The lifted rules transport the same join homomorphisms to reachable states.›

lemma map_lift_restrict_local_for_join [simp]:
  "map_lift (restrict_local_for 𝒢) (a ⊔ b)
     = map_lift (restrict_local_for 𝒢) a ⊔ map_lift (restrict_local_for 𝒢) b"
  by (rule map_lift_sup) simp

lemma map_lift_restrict_global_for_join [simp]:
  "map_lift (restrict_global_for 𝒢) (a ⊔ b)
     = map_lift (restrict_global_for 𝒢) a ⊔ map_lift (restrict_global_for 𝒢) b"
  by (rule map_lift_sup) simp

subsection ‹Splitting and rejoining›

text ‹Routing a state's two halves back through \<^const>‹combine_env› recovers it
  exactly: each half is already bottom outside the names it owns.›

lemma combine_env_restrict_id [simp]:
  "combine_env 𝒢 (restrict_local_for 𝒢 sigma) (restrict_global_for 𝒢 sigma) = sigma"
  by (simp add: combine_env_for_eq_restrictions)

subsection ‹Reading one selected name›

text ‹The two pointwise equations, so a proof about a single variable never has
  to unfold \<^const>‹combine_env›. The nesting law is what lets a combine step
  read a returned value straight out of the callee exit: every call site owns
  ‹ret_var› as its own compiler-internal name and never a user-declared global
  (‹reserved_ret_var›), so routing it through \<^const>‹combine_env› a second
  time would change nothing.›

lemma combine_env_local_eq [simp]:
  "¬ 𝒢 x ⟹ combine_env 𝒢 sc se x = sc x"
  by (simp add: combine_env_def)

lemma combine_env_global_eq [simp]:
  "𝒢 x ⟹ combine_env 𝒢 sc se x = se x"
  by (simp add: combine_env_def)

lemma combine_env_combine_env_left [simp]:
  "combine_env 𝒢 (combine_env 𝒢 dc g) (combine_env 𝒢 de g) = combine_env 𝒢 dc g"
  by (auto simp: combine_env_def)

end