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