Theory Static_Semantics

theory Static_Semantics
imports Denotational_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
```