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" |
"add (Suc m) n = Suc (add m n)"

lemma add_02: "add m 0 = m"
  apply (induction m)
  apply (auto)
  done

Quotation Marks

  • 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

References