Isabelle/HOL Support Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== 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.

===== Keywords =====

==== theory ====
theory //name//

  * Is how you begin all your .THY files.

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

  * **Example**
<code>
theory MyTheory
</code>

==== imports ====
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**
<code>
theory Bar
imports Main
begin
...
end
</code>

==== 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**
<code>
theory Foo
imports Main
begin
...
end
</code>

==== definition ====
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**
<code>
definition swap :: "('a * 'b) => ('b * 'a)"
where
"swap pair = (snd pair, fst pair)"
</code>

==== primrec ====
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**
<code>
primrec listSwap :: "('a * 'b) list => ('b * 'a) list"
where
"listSwap [] = []" |
"listSwap(x#xs) = (swap(x))#(listSwap(xs))"
</code>

==== value ====
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**
<code>
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 # [])"
</code>

===== Symbols from Libraries =====

==== Cons ====
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**
<code>
value "Cons 0 (Cons 1 (Cons 2 (Cons 3 Nil)))"
(*Equivalent expression using the abbreviations*)
value "0 # 1 # 2 # 3 # []"
</code>

===== Template =====

==== TERM ====
Syntax definition of the term with its parameters //parameters//

  * Short description

  * **Params**
    * //param_1//: description of param1
    * //param_2//: description of param 2

  * **Example**
<code>
put some simple example code here. 
Hopefully an example that isn't already in the documentation so we can have more examples.
</code>
Isabelle/HOL Support Wiki

User Tools

Site Tools

Page Tools
