Isabelle/HOL Syntax

This is one of the most important sections of the Wiki. Here you'll find the basic reserved words used in Isabelle/HOL, how should they be called, in which context, their meaning and hopefully some example code. If you're uploading/updating content, please try to adapt to the schema used for all the words to improve readability.

theory name

• Is how you begin all your .THY files.

• Params
  • name: arbitrary name that you want to give to your theory.

• Example

theory MyTheory

imports package

• Indicates what external modules (i.g. theories, packages) to import. Since Isabelle/HOL doesn't actually know a lot about functions and complex data types, you need to import them. If you create some handy theory and put it in a THY file (or just happen to have a file with a bunch of handy functions) and now you would like to use that to proof some other stuff, you can import it using this statement. Since most of the time, you need to work with some common data structures such as lists, there are already modules that come with Isabelle/HOL that deal with it. The most common one is the Main package. That comes with the structures and functions that are used the most when using Isabelle/HOL.

• Params
  • package: the name of the package/theory/module that you want to import. Works pretty much like importing stuff in other programming languages like Python, Java, C, etc…

• Exampe

theory Bar
imports Main
begin
...
end

begin … end

• Denotes the beginning and ending of Isabelle/HOL code. Should be present in all THY files right after the definition of imports.

• Params
  • none

• Example

theory Foo
imports Main
begin
...
end

definition name :: “domain” where “fun_def”

• most simple way to define non-recursive functions. Doesn't require to input a termination.

• Params
  • name: can be an arbitrary string that identifies the function.
  • domain: specifies the datatypes expected by the function
  • fun_def: is the actual definition of the function.

• Example

definition swap :: "('a * 'b) => ('b * 'a)"
where
"swap pair = (snd pair, fst pair)"

primrec name :: “domain” where “fun_def_1 | fun_def_2 | … | fun_def_n”

• defines primitive recursive functions over datatypes.

• Params
  • name: can be an arbitrary string that identifies the function.
  • domain: specifies the datatypes expected by the function
  • fun_def_i: are the actual definitions of the function. There can be several of them (like for Fibonacci or Ackermann) They have to be separated by a vertical bar '|'.

• Example

primrec listSwap :: "('a * 'b) list => ('b * 'a) list"
where
"listSwap [] = []" |
"listSwap(x#xs) = (swap(x))#(listSwap(xs))"

value “some_val”

• Useful for checking function definitions and call them with some dummy data and test if it does what it's supposed to.

• Params
  • some_val: statement that yields a value (including functions)

• Example

value "(1 # 2 # 3 # [])"
(*Assume you have a function definition called myMap :: "('a => 'b) => ('a list) => ('b list)"*)
value "myMap ((op +)1) ((1::nat) # 3 # [])"

Cons firstElem listTale

• Append firstElem to the front of the list listTale. This function often appears abbreviated with the infix operator #.

• Params
  • firstElem: element to be appended to the list
  • listTale: the list where firstElem is going to be appended

• Example

value "Cons 0 (Cons 1 (Cons 2 (Cons 3 Nil)))"
(*Equivalent expression using the abbreviations*)
value "0 # 1 # 2 # 3 # []"

Syntax definition of the term with its parameters parameters

• Short description

• Params
  • param_1: description of param1
  • param_2: description of param 2

• Example

put some simple example code here. 
Hopefully an example that isn't already in the documentation so we can have more examples.