Theory Syntax

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