ThomasHickman/Isabelle-CAS-Integration

A project to integrate the functionality of Computer Algebra Systems into Isabelle

Isabelle-CAS-Integration

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

Steps for installation

• Install Isabelle 2020. Earlier versions are not supported.

• 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 theory loading, to avoid recompiling. This can be done with the command isabelle jedit -d ~/AFP/thys -l Ordinary_Differential_Equations, replacing the path to the AFP with wherever it is downloaded.

Usage

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