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.

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

Name		Name	Last commit message	Last commit date
Latest commit History 28 Commits
sage-integration		sage-integration
verification		verification
wolfram-integration		wolfram-integration
.gitignore		.gitignore
Keymaera_tests.thy		Keymaera_tests.thy
ODE_Solve_Keyword.thy		ODE_Solve_Keyword.thy
README.md		README.md
TestSet.thy		TestSet.thy
TestSet_2.thy		TestSet_2.thy
config-example.sml		config-example.sml
generate_keymaera_examples.py		generate_keymaera_examples.py
manually_solved_cases.thy		manually_solved_cases.thy
proved_case_10_and_11.thy		proved_case_10_and_11.thy