# Isabelle/HOL

## Overview

• Isabelle is a generic proof assistant
• HOL = Higher-Order Logic = Functional Programming + Logic
• Isabelle’s interface is based on the jEdit editor
• In textual form most symbols are displayed as \<name>
• \<Rightarrow> is rendered as $$\Rightarrow$$
• File extension is *.thy

## Basics

• Each file is a theory
• A theory is a collection of definitions, functions and proofs
• Similar to modules in other languages
theory T
imports T_1 ... T_n
begin
definitions, theorems and proofs here...
end
• Theory name must be equal to the file name

### Syntax

datatype bool = True | False

fun conj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
"conj True True = True" |
"conj _ _ = False"

datatype nat = 0 | Suc nat

fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
"add 0 n = n" |
done
• Everything HOL-specific (terms and types) must be enclosed in " ... "