Transcript Slide 1

ISABELLE/HOL
CAS- 734 (Presentation -1)
By : Vasudha Kapil
Outline
•
•
•
•
•
Intoduction
Theory Format
HOL
Proof format
Example
ISABELLE/HOL
• Isabelle theorem prover is an interactive proof
assistant.
• It is a Generic Proof Assistant.
• It was developed at University of Cambridge
(Laury Paulson) , TU Munchen (Tobias Nipkow)
and Universt Paris Sud (Makarius Wenzel)
• Isabelle/HOL is specialization of Isabelle for
HOL (Higher Order Logic).
INSTALLATION
• Download system from :
https://www.cl.cam.ac.uk/research/hvg/Isabelle/
• It is currently available for three platforms :
o WINDOWS
o MAC OS X
o LINUX
• Platform specific application bundle includes
sources, documentation and add on components
required.
INTERFACE
• Isabelle jEdit is the interface for current
version of Isabelle/HOL.
• Interactive Development Environment
• Parses and interprets file while it is typed.
• List of mathematical symbols provided.
THEORIES
• General format of theory T in Isabelle/HOL is :
Theory T
Imports B1.......... Bn
Begin
(Declarations, Definitions & Proofs)
end
Brief Review of HOL
• HOL has
o datatypes
o recursive functions
o logical operators (∧, −→, ∀, ∃, . . . )
• HOL = functional programming + logic
Types
Basic Syntax –
τ ::= (τ )
| bool | nat | . . .
| ’a | ’b | . . .
|τ⇒τ
| sets, lists
|. . .
base types
type variables
total functions
type constructors
user-defined types
All terms and formulae should be well typed in Isabelle.
Type Inference and Type Annotation
• Type Inference : Isabelle automatically
computes the type of each variable in a term.
• Type Annotations : In the presence of
overloaded functions type inference is not
always possible. Type constraints are needed
in such cases.
Syntax : f (x::nat)
Terms
• Syntax
term ::=
(term)
|a
| term term
| λx. term
|...
constant or variable (identifier)
function application
function “abstraction”
lots of syntactic sugar
• Terms must be well-typed
• Notation: t :: τ means t is a well-typed term of
type τ .
Formulae
• They are terms of type bool (True & False) and
usual logical connectives.
• Syntax : form ::=
(form) | term = term | ￢form| form ∧ form |
form ∨ form | form −→ form| ∀x. form |
∃x. form
Variables
• Isabelle has three kinds of variables :
o Bound Variables
o Free Variables
o Schematic variables or unknown. Example : ?x
It has ‘?’ as its first character.
Functions
Function definition schemas in Isabelle/HOL
o Non Recursive with definition
 definition name :: “domain” where “fun_def”
Example : definition sq :: “nat => nat” where “sq n= n*n”
o Primitive Recursive with primrec
 primrec name :: “domain” where “fun_def1| fun_def2|......
|fun_defn”
Example : primrec rev :: "'a list =>'a list“ where
"rev [] = []" |
"rev (x # xs) = (rev xs) @ (x # [])"
Functions (continued)
• Well founded recursion with fun
o Syntax : fun f :: “τ”
where
“equations”
o Fun has automatic termination proof.
• Well founded recursion with function.
o Syntax : function f :: “τ”
where
“equations”
....
by pat_completeness auto
Termination by lexicographic_order
o User supplied termination proof.
Proofs
General format:
lemma name : "..."
apply (...)
apply (...)
.
.
.
done
If the lemma is suitable as a simplification rule:
lemma name [simp]: "..."
Automated Methods
• Methods are commands to work on proof
state.
Syntax : apply (method <parameters>)
o assumption : It solves a sub goal if consequent is
contained in set of assumptions.
o auto : Instructs Isabelle to try and prove all subgoals
automatically essentially by simplifying them.
o simp : Same as auto but act on subgoal 1 only.
[simp] : It can be used to make a theorem simplification
rule. Example : prove rev(rev x) = x
lemma rev_rev [simp] : “rev(rev x) = x”
Methods (continued)
o blast : Covers logic, sets, relations
 Doesn’t support equality.
o arith : Covers linear arithmetic.
 Supports int, reals as well
 Doesn’t support complex multiplication (*)
o Induction : apply (induction m) : Tells Isabelle to
start a proof by induction on m.
EXAMPLE
theory addition
imports Main
begin
fun add :: "nat⇒ nat ⇒ nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"
lemma add_ex [simp]: "add m 0 = m"
apply(induction m)
apply(auto)
done
end
Bibliography
• https://www.cl.cam.ac.uk/research/hvg/Isabel
le/documentation.html
• Theorem Proving with Isabelle/HOL : By Tobias
Nipkow.
http://isabelle.in.tum.de/coursematerial/PSV20091/
• Isabelle/HOL : A Proof Assistant for Higher
Order Logic. By- Tobias Nipkow, Lawrence C. Paulson,
Markus Wenzel