- 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
\<Rightarrow> is rendered as \(\Rightarrow\)
- File extension is
- Each file is a theory
- A theory is a collection of definitions, functions and proofs
- Similar to modules in other languages
imports T_1 ... T_n
definitions, theorems and proofs here...
- Theory name must be equal to the file name
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" |
"add (Suc m) n = Suc (add m n)"
lemma add_02: "add m 0 = m"
apply (induction m)
- We need to distinguish between meta-level and HOL-level
- Everything HOL-specific (terms and types) must be enclosed in
" ... "
- Quotation marks around a single identifier can be omitted