# Theory Syntax

theory Syntax
imports Identifiers
```theory "Syntax"
imports
Complex_Main
"Identifiers"
begin
section ‹Syntax›

text ‹
Defines the syntax of Differential Game Logic as inductively defined data types.
🌐‹https://doi.org/10.1145/2817824› 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15›
›

subsection ‹Terms›

text ‹Numeric literals›
type_synonym lit = real

text ‹the set of all real variables›
abbreviation allidents:: "ident set"
where "allidents ≡ {x | x. True}"

text ‹Variables and differential variables›

datatype variable =
RVar ident
| DVar ident

datatype trm =
Var variable
| Number lit
| Const ident
| Func ident trm
| Plus trm trm
| Times trm trm
| Differential trm

subsection ‹Formulas and Hybrid Games›

datatype fml =
Pred ident trm
| Geq trm trm
| Not fml                 ("!")
| And fml fml             (infixr "&&" 8)
| Exists variable fml
| Diamond game fml        ("(⟨ _ ⟩ _)" 20)
and game =
Game ident
| Assign variable trm     (infixr ":=" 20)
| Test fml                ("?")
| Choice game game        (infixr "∪∪" 10)
| Compose game game       (infixr ";;" 8)
| Loop game               ("_**")
| Dual game               ("_^d")
| ODE ident trm

paragraph ‹Derived operators›
definition Neg ::"trm ⇒ trm"
where "Neg θ = Times (Number (-1)) θ"

definition Minus ::"trm ⇒ trm ⇒ trm"
where "Minus θ η = Plus θ (Neg η)"

definition Or :: "fml ⇒ fml ⇒ fml" (infixr "||" 7)
where "Or P Q = Not (And (Not P) (Not Q))"

definition Implies :: "fml ⇒ fml ⇒ fml" (infixr "→" 10)
where "Implies P Q = Or Q (Not P)"

definition Equiv :: "fml ⇒ fml ⇒ fml" (infixr "↔" 10)
where "Equiv P Q = Or (And P Q) (And (Not P) (Not Q))"

definition Forall :: "variable ⇒ fml ⇒ fml"
where "Forall x P = Not (Exists x (Not P))"

definition Equals :: "trm ⇒ trm ⇒ fml"
where "Equals θ θ' = ((Geq θ θ') && (Geq θ' θ))"

definition Greater :: "trm ⇒ trm ⇒ fml"
where "Greater θ θ' = ((Geq θ θ') && (Not (Geq θ' θ)))"

text ‹Justification: determinacy theorem justifies this equivalent syntactic abbreviation for box modalities from diamond modalities
Theorem 3.1 🌐‹https://doi.org/10.1145/2817824››
definition Box :: "game ⇒ fml ⇒ fml" ("([[_]]_)" 20)
where "Box α P = Not (Diamond α (Not P))"

definition TT ::"fml"
where "TT = Geq (Number 0) (Number 0)"

definition FF ::"fml"
where "FF = Geq (Number 0) (Number 1)"

definition Skip ::"game"
where "Skip = Test TT"

text ‹Inference: premises, then conclusion›
type_synonym inference = "fml list * fml"

type_synonym sequent = "fml list * fml list"
text ‹Rule: premises, then conclusion›
type_synonym rule = "sequent list * sequent"

subsection ‹Structural Induction›

text ‹Induction principles for hybrid games owing to their mutually recursive definition with formulas ›

lemma game_induct [case_names Game Assign ODE Test Choice Compose Loop Dual]:
"(⋀a. P (Game a))
⟹ (⋀x θ. P (Assign x θ))
⟹ (⋀x θ. P (ODE x θ))
⟹ (⋀φ. P (? φ))
⟹ (⋀α β. P α ⟹ P β ⟹ P (α ∪∪ β))
⟹ (⋀α β. P α ⟹ P β ⟹ P (α ;; β))
⟹ (⋀α. P α ⟹ P (α**))
⟹ (⋀α. P α ⟹ P (α^d))
⟹ P α"
by(induction rule: game.induct) (auto)

lemma fml_induct [case_names Pred Geq Not And Exists Diamond]:
"(⋀x θ. P (Pred x θ))
⟹ (⋀θ η. P (Geq θ η))
⟹ (⋀φ. P φ ⟹ P (Not φ))
⟹ (⋀φ ψ. P φ ⟹ P ψ ⟹ P (And φ ψ))
⟹ (⋀x φ. P φ ⟹ P (Exists x φ))
⟹ (⋀α φ. P φ ⟹ P (Diamond α φ))
⟹ P φ"
by (induction rule: fml.induct) (auto)

text ‹the set of all variables›
abbreviation allvars:: "variable set"
where "allvars ≡ {x::variable. True}"

end
```