Theory Static_Semantics

theory "Static_Semantics"
imports
  "Syntax"
  "Denotational_Semantics"
begin
section ‹Static Semantics›

subsection ‹Semantically-defined Static Semantics›
paragraph ‹Auxiliary notions of projection of winning conditions›

text‹upward projection: ‹restrictto X V› is extends X to the states that agree on V with some state in X,
so variables outside V can assume arbitrary values.›
definition restrictto :: "state set ⇒ variable set ⇒ state set"
where
  "restrictto X V = {ν. ∃ω. ω∈X ∧ Vagree ω ν V}"

text‹downward projection: ‹selectlike X ν V› selects state ‹ν› on V in X,
so all variables of V are required to remain constant›
definition selectlike :: "state set ⇒ state ⇒ variable set ⇒ state set"
  where
  "selectlike X ν V = {ω∈X. Vagree ω ν V}"

paragraph ‹Free variables, semantically characterized.›
text‹Free variables of a term›
definition FVT :: "trm ⇒ variable set"
where
  "FVT t = {x. ∃I.∃ν.∃ω. Vagree ν ω (-{x}) ∧ ¬(term_sem I t ν = term_sem I t ω)}"

text‹Free variables of a formula›
definition FVF :: "fml ⇒ variable set"
where
  "FVF φ = {x. ∃I.∃ν.∃ω. Vagree ν ω (-{x}) ∧ ν ∈ fml_sem I φ ∧ ω ∉ fml_sem I φ}"

text‹Free variables of a hybrid game›
definition FVG :: "game ⇒ variable set"
where
  "FVG α = {x. ∃I.∃ν.∃ω.∃X. Vagree ν ω (-{x}) ∧ ν ∈ game_sem I α (restrictto X (-{x})) ∧ ω ∉ game_sem I α (restrictto X (-{x}))}"
  
paragraph ‹Bound variables, semantically characterized.›
text‹Bound variables of a hybrid game›
definition BVG :: "game ⇒ variable set"
where
  "BVG α = {x. ∃I.∃ω.∃X. ω ∈ game_sem I α X ∧ ω ∉ game_sem I α (selectlike X ω {x})}"


subsection ‹Simple Observations›
  
lemma BVG_elem [simp] :"(x∈BVG α) = (∃I ω X. ω ∈ game_sem I α X ∧ ω ∉ game_sem I α (selectlike X ω {x}))"
  unfolding BVG_def by simp

lemma nonBVG_rule: "(⋀I ω X. (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω {x})))
  ⟹ x∉BVG α"
  using BVG_elem by simp

lemma nonBVG_inc_rule: "(⋀I ω X. (ω ∈ game_sem I α X) ⟹ (ω ∈ game_sem I α (selectlike X ω {x})))
  ⟹ x∉BVG α"
  using BVG_elem by simp
  
lemma FVT_finite: "finite(FVT t)"
  using allvars_finite by (metis finite_subset mem_Collect_eq subsetI)
lemma FVF_finite: "finite(FVF e)"
  using allvars_finite by (metis finite_subset mem_Collect_eq subsetI)
lemma FVG_finite: "finite(FVG a)"
  using allvars_finite by (metis finite_subset mem_Collect_eq subsetI)

end