How to successfully Isabelle

from-users guides
,
1

Documenting how I got anything working from the Concrete Semantics book and other tutorials, as they aren’t particularly clear on how to get working code.

1 Like
2

First of all, to set up Isabelle on Linux, download the archive from here, unpack it to a location like /path/to/, then edit your .bashrc like this:

export PATH=/path/to/Isabelle2023/bin/:$PATH
export ISABELLE_HOME=/path/to/Isabelle2023

After reloading the shell, you should be able to run isabelle jedit file_name.thy.

To see all available special symbols, run less $ISABELLE_HOME/etc/symbols.

3

ImpTutorial.thy (1.5 KB)

Done up to the exercises before boolean expressions. Highlights:

  • \<Rightarrow> for function definitions
  • \<^sub> for subscripts
4

ImpTutorial.thy (1.8 KB)

Version with the Times expr added, and removed the old asimp_const code.

5

ImpTutorial.thy (2.2 KB)

Initial version with bval, negation is \<not> and conjunction is \<and>.

6

ImpTutorial.thy (3.0 KB)

boolean expressions up to exercises.

7

ImpTutorial.thy (4.3 KB)

com datatype and the inductive big_step definition.

8

ImpTutorial.thy (4.4 KB)

Evaluation. You need to put quotes " around the values expression.