tools-only Isabelle/HOL Syntax Reference
Quick reference for Isabelle/HOL syntax when modeling functional programs.
Basic Types
nat -- Natural numbers (0, 1, 2, ...)
int -- Integers
bool -- Booleans (True, False)
'a -- Type variable (polymorphic)
'a list -- List of 'a elements
'a option -- Optional value (None | Some x)
'a set -- Set of 'a elements
'a ⇒ 'b -- Function type (a to b)
'a × 'b -- Product type (pairs)
Data Types
datatype 'a tree = Leaf | Node "'a" "'a tree" "'a tree"
datatype 'a option = None | Some 'a
datatype ('a, 'b) either = Left 'a | Right 'b
Function Definitions
Simple Functions
fun factorial :: "nat ⇒ nat" where
"factorial 0 = 1" |
"factorial (Suc n) = Suc n * factorial n"
Pattern Matching
fun length :: "'a list ⇒ nat" where
"length [] = 0" |
"length (x # xs) = 1 + length xs"
Non-Primitive Recursion
function gcd :: "nat ⇒ nat ⇒ nat" where
"gcd m n = (if n = 0 then m else gcd n (m mod n))"
by pat_completeness auto
termination by (relation "measure snd") auto
Definitions (Non-Recursive)
definition compose :: "('b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'c)" where
"compose f g = (λx. f (g x))"
List Operations
[] -- Empty list
x # xs -- Cons (prepend x to xs)
xs @ ys -- Append
hd xs -- Head (first element)
tl xs -- Tail (rest of list)
length xs -- Length
map f xs -- Map function over list
filter p xs -- Filter elements satisfying predicate
fold f acc xs -- Left fold
foldr f xs acc -- Right fold
rev xs -- Reverse
set xs -- Convert list to set
mset xs -- Convert list to multiset
Common Predicates
sorted xs -- List is sorted
distinct xs -- No duplicates
x ∈ set xs -- Element membership
mset xs = mset ys -- Permutation (multiset equality)
∀x ∈ set xs. P x -- All elements satisfy P
∃x ∈ set xs. P x -- Some element satisfies P
Logical Operators
¬ P -- Negation (not P)
P ∧ Q -- Conjunction (and)
P ∨ Q -- Disjunction (or)
P ⟹ Q -- Implication
P ⟷ Q -- Bi-implication (iff)
∀x. P x -- Universal quantification
∃x. P x -- Existential quantification
Set Operations
{} -- Empty set
{x, y, z} -- Finite set
x ∈ A -- Membership
A ⊆ B -- Subset
A ∪ B -- Union
A ∩ B -- Intersection
A - B -- Difference
{x. P x} -- Set comprehension
Option Type
None -- No value
Some x -- Value x
case opt of None ⇒ ... | Some x ⇒ ...
Lambda Expressions
λx. x + 1 -- Lambda (anonymous function)
λx y. x + y -- Multi-argument lambda
Case Expressions
case xs of
[] ⇒ 0 |
(x # xs) ⇒ x + sum xs
case tree of
Leaf ⇒ 0 |
Node v l r ⇒ 1 + size l + size r
Let Bindings
let x = expr1 in expr2
let x = expr1; y = expr2 in expr3
Common Lemma Patterns
Induction
lemma "P xs"
proof (induction xs)
case Nil
show ?case ...
next
case (Cons x xs)
show ?case ...
qed
Case Analysis
lemma "P x"
proof (cases x)
case None
show ?thesis ...
next
case (Some y)
show ?thesis ...
qed
Structural Properties
lemma length_append: "length (xs @ ys) = length xs + length ys"
lemma map_compose: "map f (map g xs) = map (f ∘ g) xs"
lemma filter_filter: "filter p (filter q xs) = filter (λx. p x ∧ q x) xs"
Type Classes
'a::ord -- Ordered type (has ≤, <)
'a::linorder -- Linear order (total order)
'a::zero -- Has zero element
'a::one -- Has one element
'a::plus -- Has addition
'a::times -- Has multiplication
Useful Functions
min x y -- Minimum
max x y -- Maximum
abs x -- Absolute value
x div y -- Integer division
x mod y -- Modulo
x ^ n -- Exponentiation
sum_list xs -- Sum of list elements
prod_list xs -- Product of list elements
zip xs ys -- Zip two lists
take n xs -- First n elements
drop n xs -- Drop first n elements