Isabelle-CAS-Integration

Developed from the dissertations of Thomas Hickman and Christian Pardillo Laursen.

Steps for installation

• Install Isabelle 2022-1.

• Add the Ordinary_Differential_Equations entry to your Isabelle ROOTS - follow these instructions.

• Download and activate the Wolfram Engine. WolframScript is installed with it, and is called from bash.

OR

• Install SageMath and optionally FriCAS.

• Add the file config.sml configures the path of the file sage-integration/ConvertToIsabelle.py. An example of this file is found in config-example.sml.

• Finally, launch Isabelle/jEdit with the ODE heap image: isabelle jedit -d $PATH_TO_AFP/thys -l Ordinary_Differential_Equations,

Usage

Examples can be found in the two test sets: Keymaera_tests.thy and TestSet.thy.

Contents:

Arithmetic Expressions for integration with CAS

• Arith_Expr.ML: We introduce the AExp type, intended to represent arithmetic expressions generically in order to provide an intermediate representation that can be easily converted from and to Isabellle and CAS.

• Subst_ODE.ML: Mapping between ODEs as substitutions and AExps.

• Tupled_ODE.ML: Mapping between ODEs as tuples and AExps.

CAS integrations

• Sage integration: ConvertToSage.ML implements desolve, taking an AExp SODE and returning a tuple (solution, domain).
• Wolfram integration: see README