Theory Syntax
theory Syntax
imports
Complex_Main
"Ids"
begin
section ‹Syntax›
text ‹
We define the syntax of dL terms, formulas and hybrid programs. As in
CADE'15, the syntax allows arbitrarily nested differentials. However,
the semantics of such terms is very surprising (e.g. (x')' is zero in
every state), so we define predicates dfree and dsafe to describe terms
with no differentials and no nested differentials, respectively.
In keeping with the CADE'15 presentation we currently make the simplifying
assumption that all terms are smooth, and thus division and arbitrary
exponentiation are absent from the syntax. Several other standard logical
constructs are implemented as derived forms to reduce the soundness burden.
The types of formulas and programs are parameterized by three finite types
('a, 'b, 'c) used as identifiers for function constants, context constants, and
everything else, respectively. These type variables are distinct because some
substitution operations affect one type variable while leaving the others unchanged.
Because these types will be finite in practice, it is more useful to think of them
as natural numbers that happen to be represented as types (due to HOL's lack of dependent types).
The types of terms and ODE systems follow the same approach, but have only two type
variables because they cannot contain contexts.
›