IJCAR 2004 — Tutorial 4
λ →
∀=Isa
belle
βα
Introduction to the Isabelle Proof Assistant
Clemens Ballarin Gerwin Klein
IJCAR 2004, Tutorial T4 – p.1
Tutorial Schedule
I Session II Basics
I Session III Specification ToolsI Readable Proofs
I Session IIII More on Readable ProofsI Modules
I Session IVI ApplicationsI Q & A session with Larry Paulson
IJCAR 2004, Tutorial T4 – p.2
Session I
Basics
IJCAR 2004, Tutorial T4 – p.3
System Architecture
User can access all layers!
Proof General — User interface
HOL, ZF — Object-logics
Isabelle — Generic, interactive theorem prover
Standard ML — Logic implemented as ADT
IJCAR 2004, Tutorial T4 – p.4
Documentation
Available from http://isabelle.in.tum.de
I Learning IsabelleI Tutorial on Isabelle/HOL (LNCS 2283)I Tutorial on IsarI Tutorial on Locales
I Reference ManualsI Isabelle/Isar Reference ManualI Isabelle Reference ManualI Isabelle System Manual
I Reference Manuals for Object-Logics
IJCAR 2004, Tutorial T4 – p.5
Isabelle’s Meta-Logic
I Intuitionistic fragment of Church’s theory of simpletypes.
I With type variables.
I Can be used to formalise your own object-logic.
I Normally, use rich infrastructure of the object-logicsHOL and ZF.
I This presentation assumes HOL.
IJCAR 2004, Tutorial T4 – p.6
Types
IJCAR 2004, Tutorial T4 – p.7
Syntax
Syntax:
τ ::= (τ)
| ’a | ’b | . . . type variables| τ ⇒ τ total functions| bool | nat | . . . HOL base types| τ × τ HOL pairs (ascii: *)| τ list HOL lists| . . . user-defined types
Parentheses: T1 ⇒ T2 ⇒ T3 ≡ T1 ⇒ (T2 ⇒ T3)
IJCAR 2004, Tutorial T4 – p.8
Introducing new Types: typedecl
typedecl name
Introduces new “opaque” type name without definition.
Example:
typedecl addr — An abstract type of addresses.
IJCAR 2004, Tutorial T4 – p.9
Terms
IJCAR 2004, Tutorial T4 – p.10
Syntax
Syntax: (curried version)
term ::= (term)
| a constant or variable (identifier)| term term function application| λx. term function “abstraction”| . . . lots of syntactic sugar
Examples: f (g x) y h (λx. f (g x))
Parentheses: f a1 a2 a3 ≡ ((f a1) a2) a3
IJCAR 2004, Tutorial T4 – p.11
Schematic variables
Three kinds of variables:I bound: ∀ x. x = xI free: x = xI schematic: ?x = ?x (“unknown”)
I Logically: free = schematic
I Operationally:I free variables are fixedI schematic variables are instantiated by
substitutions and unification
IJCAR 2004, Tutorial T4 – p.12
Theorems
IJCAR 2004, Tutorial T4 – p.13
Connectives of the Meta-Logic
Implication =⇒ (==>)For separating premises and conclusion of theorems.
Equality ≡ (==)For definitions.
Universal quantifier∧
(!!)For parameters in goals.
Do not use inside object-logic formulae.
IJCAR 2004, Tutorial T4 – p.14
Notation
[[ A1; . . . ; An ]] =⇒ B
abbreviates
A1 =⇒ . . . =⇒ An =⇒ B
; ≈ “and”
IJCAR 2004, Tutorial T4 – p.15
Introducing New Theorems
I As axioms.I Through definitions.
I Through proofs.
! Axioms should mainly be used whenspecifying object-logics.
!
IJCAR 2004, Tutorial T4 – p.16
Definition (non-recursive)
Declaration:
constssq :: nat ⇒ nat
Definition:
defssq_def: sq n ≡ n*n
Declaration + definition:
constdefssq :: nat ⇒ natsq n ≡ n*n
IJCAR 2004, Tutorial T4 – p.17
Proofs
General schema:
lemma name: <goal>apply <method>apply <method>...done
I Sequential application of methods until all subgoalsare solved.
IJCAR 2004, Tutorial T4 – p.18
The proof state
1.∧
x1 . . . xp. [[ A1; . . . ; An ]] =⇒ B2.
∧y1 . . . y q. [[ C1; . . . ; Cn ]] =⇒ D
x1 . . . xp ParametersA1 . . . An Local assumptionsB Actual (sub)goal
IJCAR 2004, Tutorial T4 – p.19
Isabelle Theories
IJCAR 2004, Tutorial T4 – p.20
Theory = Source file
Syntax:
theory MyTh = ImpTh1 + . . .+ ImpThn:
(declarations, definitions, theorems, proofs, ...)∗
end
I MyTh: name of theory. Must live in file MyTh.thy
I ImpThi: name of imported theories. Import transitive.
Unless you need something special:
theory MyTh = Main:
IJCAR 2004, Tutorial T4 – p.21
X-Symbols
Input of funny symbols in Proof General
I via menu (“X-Symbol”)
I via ascii encoding (similar to LATEX): \<and>, \<or>,. . .
I via abbreviation: /\, \/, -->, . . .
x-symbol ∀ ∃ λ ¬ ∧ ∨ −→ ⇒
ascii (1) \<forall> \<exists> \<lambda> \<not> /\ \/ --> =>
ascii (2) ALL EX % ˜ & |
(1) is converted to x-symbol, (2) stays ascii.
IJCAR 2004, Tutorial T4 – p.22
Demo: Isabelle theories
IJCAR 2004, Tutorial T4 – p.23
Natural Deduction
IJCAR 2004, Tutorial T4 – p.24
Rules
A BA ∧ B
conjIA ∧ B [[A;B]] =⇒ C
CconjE
AA ∨ B
BA ∨ B
disjI1/2 A ∨ B A =⇒ C B =⇒ CC
disjE
A =⇒ BA −→ B
impI A −→ B A B =⇒ CC
impE
IJCAR 2004, Tutorial T4 – p.25
Proof by assumption
apply assumptionproves
1. [[ B1; . . . ; Bm ]] =⇒ C
by unifying C with one of the Bi (backtracking!)
IJCAR 2004, Tutorial T4 – p.26
How to prove it by natural deduction
I Intro rules decompose formulae to the right of =⇒.
apply(rule <intro-rule>)
Applying rule [[ A1; . . . ; An ]] =⇒ A to subgoal C:I Unify A and CI Replace C with n new subgoals A1 . . . An
I Elim rules decompose formulae on the left of =⇒.
apply(erule <elim-rule>)
Like rule but alsoI unifies first premise of rule with an assumptionI eliminates that assumption
IJCAR 2004, Tutorial T4 – p.27
Demo: natural deduction
IJCAR 2004, Tutorial T4 – p.28
Safe and unsafe rules
Safe rules preserve provabilityconjI, impI, conjE, disjE,notI, iffI, refl, ccontr, classical
Unsafe rules can turn provable goal into unprovable goaldisjI1, disjI2, impE,iffD1, iffD2, notE
Apply safe rules before unsafe ones
IJCAR 2004, Tutorial T4 – p.29
Predicate Logic: ∀ and ∃
IJCAR 2004, Tutorial T4 – p.30
Scope
I Scope of parameters: whole subgoal
I Scope of ∀ , ∃ , . . . : ends with ; or =⇒
∧x y. [[ ∀ y. P y −→ Q z y; Q x y ]] =⇒ ∃ x. Q x y
means∧
x y. [[ (∀ y1. P y1 −→ Q z y1); Q x y ]] =⇒ (∃ x1. Q x1 y)
IJCAR 2004, Tutorial T4 – p.31
Natural deduction for quantifiers
∧x. P x
∀ x. P x allI ∀ x. P x P ?x =⇒ RR allE
P ?x∃ x. P x
exI∃ x. P x
∧x. P x =⇒ RR
exE
I allI and exE introduce new parameters (∧
x).
I allE and exI introduce new unknowns (?x).
IJCAR 2004, Tutorial T4 – p.32
Instantiating rules
apply(rule_tac x = "term" in rule)
Like rule, but ?x in rule is instantiated by term beforeapplication.
Similar: erule_tac
! x is in rule, not in the goal !
IJCAR 2004, Tutorial T4 – p.33
Safe and unsafe rules
Safe allI, exE
Unsafe allE, exI
Create parameters first, unknowns later
IJCAR 2004, Tutorial T4 – p.34
Forward proofs: frule and drule
apply(frule rulename)
Forward rule: A1 =⇒ ASubgoal: 1. [[ B1; . . . ; Bn ]] =⇒ C
Unifies: one Bi with A1
New subgoal: 1. [[ B1; . . . ; Bn; A ]] =⇒ C
apply(drule rulename)
Like frule but also deletes Bi
IJCAR 2004, Tutorial T4 – p.35
Demo: quantifier proofs
IJCAR 2004, Tutorial T4 – p.36
Practical Session I
In the cool morningA man simplifies, a goal
A theorem is born.
— Don Syme
IJCAR 2004, Tutorial T4 – p.37
Session II
HOL = Functional programming + Logic
IJCAR 2004, Tutorial T4 – p.38
Proof by Term Rewriting
IJCAR 2004, Tutorial T4 – p.39
Term rewriting means . . .
Using equations l = r from left to right
as long as possible
Terminology: equation ; rewrite rule
IJCAR 2004, Tutorial T4 – p.40
Example
Example:
Equation: 0 + n = n
Term: a + (0 + (b + c))
Result: a + (b + c)
Rewrite rules can be conditional: [[P1 . . . Pn]] =⇒ l = r
is usedI like l = r, butI P1, . . . , Pn must be proved by rewriting first.
IJCAR 2004, Tutorial T4 – p.41
Simplification in Isabelle
Goal: 1. [[ P1; . . . ; Pm ]] =⇒ C
apply(simp add: eq1 . . . eqn)
Simplify P1 . . . Pm and C using
I lemmas with attribute simp
I additional lemmas eq1 . . . eqn
I assumptions P1 . . . Pm
Variations:I (simp . . . del: . . . ) removes simp-lemmas
I add and del are optional
IJCAR 2004, Tutorial T4 – p.42
Termination
Simplification may not terminate.Isabelle uses simp-rules (almost) blindly from left to right.
Example: f(x) = g(x), g(x) = f(x)
[[P1 . . . Pn]] =⇒ l = r
is suitable as a simp-rule onlyif l is “bigger” than r and each Pi
n < m =⇒ (n < Suc m) = True YESSuc n < m =⇒ (n < m) = True NO
IJCAR 2004, Tutorial T4 – p.43
How to ignore assumptions
Assumptions sometimes cause problems, e.g.nontermination. How to exclude them from simp:
apply(simp (no_asm_simp) . . . )Simplify only conclusion
apply(simp (no_asm_use) . . . )Simplify but do not use assumptions
apply(simp (no_asm) . . . )Ignore assumptions completely
IJCAR 2004, Tutorial T4 – p.44
Tracing
Set trace mode on/off in Proof General:
Isabelle/Isar → Settings → Trace simplifier
Output in separate buffer:
Proof-General → Buffers → Trace
IJCAR 2004, Tutorial T4 – p.45
auto
I auto acts on all subgoals
I simp acts only on subgoal 1
I auto applies simp and more
IJCAR 2004, Tutorial T4 – p.46
Demo: simp
IJCAR 2004, Tutorial T4 – p.47
Type definitions in Isabelle/HOL
Keywords:
I typedecl: pure declaration (session 1)
I types: abbreviationI datatype: recursive datatype
IJCAR 2004, Tutorial T4 – p.48
types
types name = τ
Introduces an abbreviation name for type τ
Examples:
typesname = string(’a,’b)foo = "’a list × ’b list"
Type abbreviations are expanded after parsingNot present in internal representation and Isabelle output
IJCAR 2004, Tutorial T4 – p.49
datatype
datatype ’a list = Nil | Cons ’a "’a list"
Properties:
I Types: Nil :: ’a listCons :: ’a ⇒ ’a list ⇒ ’a list
I Distinctness: Nil 6= Cons x xsI Injectivity: (Cons x xs = Cons y ys) = (x = y ∧ xs = ys)
IJCAR 2004, Tutorial T4 – p.50
case
Every datatype introduces a case construct, e.g.
(case xs of Nil ⇒ . . . | Cons y ys ⇒ ... y ... ys ...)
I one case per constructor
I no nested patterns (Cons x (Cons y zs))
I but nested cases
apply(case_tac xs) ⇒ one subgoal for each constructor
xs = Nil =⇒ . . .
xs = Cons a list =⇒ . . .
IJCAR 2004, Tutorial T4 – p.51
Function definition schemas in Isabelle/HOL
I Non-recursive with constdefs (session 1)No problem
I Primitive-recursive with primrecTerminating by construction
I Well-founded recursion with recdefUser must (help to) prove termination
IJCAR 2004, Tutorial T4 – p.52
primrec
consts app :: "’a list ⇒ ’a list ⇒ ’a list"primrec"app Nil ys = ys""app (Cons x xs) ys = Cons x (app xs ys)"
I Each recursive call structurally smaller than lhs.
I Equations used automatically in simplifier
IJCAR 2004, Tutorial T4 – p.53
Structural induction
P xs holds for all lists xs ifI P NilI and for arbitrary x and xs, P xs implies P (Cons x xs)
Induction theorem list.induct:[[P Nil;
∧a list. P list =⇒ P (Cons a list)]]
=⇒ P listI General proof method for induction: (induct x)
I x must be a free variable in the first subgoal.I The type of x must be a datatype.
IJCAR 2004, Tutorial T4 – p.54
Induction heuristics
Theorems about recursive functions proved by induction
consts itrev :: ’a list ⇒ ’a list ⇒ ’a listprimrec
itrev [] ys = ysitrev (x#xs) ys = itrev xs (x#ys)
lemma itrev xs [] = rev xs
IJCAR 2004, Tutorial T4 – p.55
Demo: proof attempt
IJCAR 2004, Tutorial T4 – p.56
Generalisation
Replace constants by variables
lemma itrev xs ys = rev xs @ ys
Quantify free variables by ∀(except the induction variable)
lemma ∀ ys. itrev xs ys = rev xs @ ys
IJCAR 2004, Tutorial T4 – p.57
Function definition schemas in Isabelle/HOL
I Non-recursive with constdefs (session 1)No problem
I Primitive-recursive with primrecTerminating by construction
I Well-founded recursion with recdefUser must (help to) prove termination
IJCAR 2004, Tutorial T4 – p.58
recdef — examples
consts sep :: "’a × ’a list ⇒ ’a list"recdef sep "measure (λ(a, xs). size xs)"
"sep (a, x # y # zs) = x # a # sep (a, y # zs)""sep (a, xs) = xs"
consts ack :: "nat × nat ⇒ nat"recdef ack "measure (λm. m) <*lex*> measure (λn. n)"
"ack (0, n) = Suc n""ack (Suc m, 0) = ack (m, 1)""ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"
IJCAR 2004, Tutorial T4 – p.59
recdef
I The definiton:I one parameterI free pattern matching, order of rules importantI termination relation
(measure sufficient for most cases)
I Termination relation:I must decrease for each recursive callI must be well founded
I Generates own induction principle.
IJCAR 2004, Tutorial T4 – p.60
Demo: recdef and induction
IJCAR 2004, Tutorial T4 – p.61
Sets
IJCAR 2004, Tutorial T4 – p.62
Notation
Type ’a set : sets over type ’a
I {}, {e1,. . . ,en}, {x. P x}I e ∈ A, A ⊆ BI A ∪ B, A ∩ B, A - B, - AI
⋃x∈A B x,
⋂x∈A B x
I {i..j}
I insert :: ’a ⇒ ’a set ⇒ ’a setI f ‘ A ≡ {y. ∃ x∈A. y = f x}I . . .
IJCAR 2004, Tutorial T4 – p.63
Inductively defined sets: even numbers
Informally:
I 0 is evenI If n is even, so is n + 2
I These are the only even numbers
In Isabelle/HOL:
consts Ev :: nat set — The set of all even numbersinductive Evintros
0 ∈ Evn ∈ Ev =⇒ n + 2 ∈ Ev
IJCAR 2004, Tutorial T4 – p.64
Rule induction for Ev
To prove
n ∈ Ev =⇒ P n
by rule induction on n ∈ Ev we must prove
I P 0I P n =⇒ P(n+2)
Rule Ev.induct:
[[ n ∈ Ev; P 0;∧
n. P n =⇒ P(n+2) ]] =⇒ P n
An elimination rule
IJCAR 2004, Tutorial T4 – p.65
Demo: inductively defined sets
IJCAR 2004, Tutorial T4 – p.66
Isar
A Language for StructuredProofs
IJCAR 2004, Tutorial T4 – p.67
Apply scripts
I unreadableI hard to maintainI do not scale
No structure!
IJCAR 2004, Tutorial T4 – p.68
A typical Isar proof
proof
assume formula0
have formula1 by simp...have formulan by blastshow formulan+1 by . . .
qed
proves formula0 =⇒ formulan+1
IJCAR 2004, Tutorial T4 – p.69
Isar core syntax
proof = proof [method] statement∗ qed
| by method
method = (simp . . . ) | (blast . . . ) | (rule . . . ) | . . .
statement = fix variables (∧
)| assume proposition (=⇒)| [from name+] (have | show) proposition proof| next (separates subgoals)
proposition = [name:] formula
IJCAR 2004, Tutorial T4 – p.70
Demo: propositional logic
IJCAR 2004, Tutorial T4 – p.71
Elimination rules / forward reasoning
I Elim rules are triggered by facts fed into a proof:from ~a have formula proof
I from ~a have formula proof (rule rule)
~a must prove the first n premises of rule
in the right orderthe others are left as new subgoals
I proof alone abbreviates proof ruleI rule: tries elim rules first
(if there are incoming facts ~a!)
IJCAR 2004, Tutorial T4 – p.72
Practical Session II
Theorem proving andsanity; Oh, my! What a
delicate balance.
— Victor Carreno
IJCAR 2004, Tutorial T4 – p.73
Session III
More about Isar
IJCAR 2004, Tutorial T4 – p.74
Overview
I AbbreviationsI Predicate Logic
I Accumulating facts
I Reasoning with chains of equations
I Locales: the module system
IJCAR 2004, Tutorial T4 – p.75
Abbreviations
this = the previous proposition proved or assumedthen = from this
with ~a = from ~a this
?thesis = the last enclosing show formula
IJCAR 2004, Tutorial T4 – p.76
Mixing proof styles
from . . .have . . .
apply - make incoming facts assumptionsapply( . . . )...apply( . . . )done
IJCAR 2004, Tutorial T4 – p.77
Demo: Abbreviations
IJCAR 2004, Tutorial T4 – p.78
Predicate Calculus
IJCAR 2004, Tutorial T4 – p.79
fix
Syntax:
fix variables
Introduces new arbitrary but fixed variables(∼ parameters)
IJCAR 2004, Tutorial T4 – p.80
obtain
Syntax:
obtain variables where proposition proof
Introduces new variables together with property
IJCAR 2004, Tutorial T4 – p.81
Demo: predicate calculus
IJCAR 2004, Tutorial T4 – p.82
moreover/ultimately
have formula1 . . .moreover
have formula2 . . .moreover...moreover
have formulan . . .ultimately
show . . .— pipes facts formula1 . . . formulan into the proofproof . . .
IJCAR 2004, Tutorial T4 – p.83
Demo: moreover/ultimately
IJCAR 2004, Tutorial T4 – p.84
General case distinctions
show formula
proof -have P1 ∨ P2 ∨ P3 . . .moreover
{ assume P1 . . . have ?thesis . . . }moreover
{ assume P2 . . . have ?thesis . . . }moreover
{ assume P3 . . . have ?thesis . . . }ultimately show ?thesis by blast
qed
IJCAR 2004, Tutorial T4 – p.85
Chains of equations
I Keywords also and finally.
I . . . : predefined schematic term variable,refers to the right hand side of the last expression.
I Uses transitivity rule.
IJCAR 2004, Tutorial T4 – p.86
also/finally
have "t0 = t1" . . .also t0 = t1
have " . . . = t2" . . .also t0 = t2
......
also t0 = tn-1have " . . . = tn" . . .finally show . . .— pipes fact t0 = tn into the proofproof
...IJCAR 2004, Tutorial T4 – p.87
More about also
I Works for all combinations of =, ≤ and <.I Uses rules declared as [trans].I To view all combinations in Proof General:
Isabelle/Isar → Show me → Transitivity rules
IJCAR 2004, Tutorial T4 – p.88
Demo: also/finally
IJCAR 2004, Tutorial T4 – p.89
Locales
Isabelle’s Module System
IJCAR 2004, Tutorial T4 – p.90
Isar is based on contexts
theorem∧
x. A =⇒ Cproof -
fix xassume Ass: A... x and Ass are visiblefrom Ass show C . . . inside this context
qed
IJCAR 2004, Tutorial T4 – p.91
Beyond Isar contexts
Locales are extended contextsI Locales are namedI Fixed variables may have syntax
I It is possible to add and export theorems
I Locale expression: combine and modify locales
IJCAR 2004, Tutorial T4 – p.92
Context elements
Locales consist of context elements.
fixes Parameter, with syntaxassumes Assumptiondefines Definitionnotes Record a theorem
IJCAR 2004, Tutorial T4 – p.93
Declaring locales
locale loc =loc1 + Importfixes . . . Context elementsassumes . . .
Declares named locale loc.
IJCAR 2004, Tutorial T4 – p.94
Declaring locales
Theorems may be stated relative to a named locale.
lemma (in loc) P [simp]: propositionproof
I Adds theorem P to context loc.I Theorem P is in the simpset in context loc.
I Exported theorem loc.P visible in the entire theory.
IJCAR 2004, Tutorial T4 – p.95
Demo: locales 1
IJCAR 2004, Tutorial T4 – p.96
Parameters must be consistent!
I Parameters in fixes are distinct.I Free variables in assumes and defines occur in
preceding fixes.
I Defined parameters must neither occur in precedingassumes nor defines.
IJCAR 2004, Tutorial T4 – p.97
Locale expressions
Locale name: nRename: e q1 . . . qn
Change names of parameters in e.Merge: e1 + e2
Context elements of e1, then e2.
I Syntax is lost after rename (currently).
IJCAR 2004, Tutorial T4 – p.98
Demo: locales 2
IJCAR 2004, Tutorial T4 – p.99
Normal form of locale expressions
Locale expressions are converted to flattened lists oflocale names.I With full parameter lists
I Duplicates removed
Allows for multiple inheritance!
IJCAR 2004, Tutorial T4 – p.100
Instantiation
Move from abstract to concrete.
instantiate label : loc
I From chained fact loc t1 . . . tn instantiate locale loc.I Imports all theorems of loc into current context.
I Instantiates the parameters with t 1 . . . tn.I Interprets attributes of theorems.I Prefixes theorem names with label
I Currently only works inside Isar contexts.
IJCAR 2004, Tutorial T4 – p.101
Demo: locales 3
IJCAR 2004, Tutorial T4 – p.102
Practical Session III
The sun spills darknessA dog howls after midnight
Goals remain unsolved.
— Chris Owens
IJCAR 2004, Tutorial T4 – p.103
Session IV
Case Studies
IJCAR 2004, Tutorial T4 – p.104
Case Study
Compiling Expressions
IJCAR 2004, Tutorial T4 – p.105
The Task
I develop a compiler
I from expressions
I to a stack machineI and show its correctness
I expressions built fromI variablesI constantsI binary operations
IJCAR 2004, Tutorial T4 – p.106
Expressions — Syntax
Syntax for
I binary operations
I expressions
Design decision:
I no syntax for variables and values
Instead:I expressions generic in variable names,
I nat for values.
IJCAR 2004, Tutorial T4 – p.107
Expressions — Data Type
I Binary operations
datatype binop = Plus | Minus | Mult
I Expressions
datatype ’v expr = Const nat| Var ’v| Binop binop "’v expr" "’v expr"
I ’v = variable names
IJCAR 2004, Tutorial T4 – p.108
Expressions — Semantics
I Sematics for binary operations:
consts semop :: "binop ⇒ nat ⇒ nat ⇒ nat" (" [[_]]")primrec " [[Plus]] = (λx y. x + y)"
" [[Minus]] = (λx y. x - y)"" [[Mult ]] = (λx y. x * y)"
I Sematics for expressions:
consts value :: "’v expr ⇒ (’v ⇒ nat) ⇒ nat"primrec
"value (Const v) E = v""value (Var a) E = E a""value (Binop f e1 e2) E = [[f ]] (value e1 E) (value e2 E)"
IJCAR 2004, Tutorial T4 – p.109
Stack Machine — Syntax
Machine with 3 instructions:I push constant value onto stack
I load contents of register onto stack
I apply binary operator to top of stack
Simplification: register names = variable names
datatype ’v instr = Push nat| Load ’v| Apply binop
IJCAR 2004, Tutorial T4 – p.110
Stack Machine — Execution
Modelled by a function taking
I list of instructions (program)
I store (register names to values)
I list of values (stack)
ReturnsI new stack
IJCAR 2004, Tutorial T4 – p.111
exec
consts exec :: "’v instr list ⇒ (’v ⇒ nat) ⇒ nat list ⇒ nat list"primrec
"exec [] s vs = vs""exec (i#is) s vs = (case i of
Push v ⇒ exec is s (v # vs)| Load a ⇒ exec is s (s a # vs)| Apply f ⇒ let v 1 = hd vs; v2 = hd (tl vs); ts = tl (tl vs) in
exec is s ( [[f ]] v 1 v2 # ts))"
I hd and tl are head and tail of lists
IJCAR 2004, Tutorial T4 – p.112
The Compiler
Compilation easy:
I Constants ⇒ PushI Variables ⇒ LoadI Binop ⇒ Apply
consts comp :: "’v expr ⇒ ’v instr list"primrec
"comp (Const v) = [Push v]""comp (Var a) = [Load a]""comp (Binop f e1 e2) = (comp e2) @ (comp e1) @ [Apply f]"
IJCAR 2004, Tutorial T4 – p.113
Correctness
Executing compiled program yields value of expression
theorem "exec (comp e) s [] = [value e s]"
Proof?
IJCAR 2004, Tutorial T4 – p.114
Demo: correctness proof
IJCAR 2004, Tutorial T4 – p.115
Case Study
Commutative Algebra
IJCAR 2004, Tutorial T4 – p.116
Abstract Mathematics
I Concerns classes of objects specified by axioms, notconcrete objects like the integers or reals.
I Objects are typically structures: (G, ·, 1, -1)I Groups, rings, lattices, topological spaces
I Concepts are frequently combined and extended.
I Instances may be concrete or abstract.
IJCAR 2004, Tutorial T4 – p.117
Formalisation
I Structures are not theories of proof tools.
I Structures must be first-class values.I Syntax should reflect context:
I If G is a group, then (x · y)-1 = y-1 · x-1 refersimplicitly to G.
I Inheritance of syntax and theorems should beautomatic.
IJCAR 2004, Tutorial T4 – p.118
Support for Abstraction
I Locales: portable contexts.
I ı (\<index>) arguments in syntax declarations.
I Extensible records (in HOL).
I Locale instantiation.
IJCAR 2004, Tutorial T4 – p.119
Index Arguments in Syntax Declarations
I One function argument may be \<index>.
I Works also for infix operators and binders:x ⊗G y
⊕Ri ∈ {0..n}. f i
I Good for denoting record fields.
I Can declare default by (structure).
I Yields a concise syntax for G while allowingreferences to other groups.
I Letter subscripts for \<index> only available incurrent development version of Isabelle.
IJCAR 2004, Tutorial T4 – p.120
Records
I Are used to represent structures.
I Fields are functions and can have special syntax.
I Records can be extended with additional fields.
record ’a monoid =carrier :: "’a set"mult :: "[’a, ’a] ⇒ ’a" (infixl "⊗ı" 70)one :: ’a ("1ı")
IJCAR 2004, Tutorial T4 – p.121
A Locale for Monoids
locale monoid = struct G +assumes m_closed [intro, simp]:
"[[ x ∈ carrier G; y ∈ carrier G ]] =⇒ x ⊗ y ∈ carrier G"and m_assoc:"[[ x ∈ carrier G; y ∈ carrier G; z ∈ carrier G ]]
=⇒ (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)"and one_closed [intro, simp]: "1 ∈ carrier G"and l_one [simp]: "x ∈ carrier G =⇒ 1 ⊗ x = x"and r_one [simp]: "x ∈ carrier G =⇒ x ⊗ 1 = x"
IJCAR 2004, Tutorial T4 – p.122
A Locale for Groups
A group is a monoid whose elements have inverses.
locale group = monoid +assumes inv_ex:"x ∈ carrier G =⇒ ∃ y ∈ carrier G. y ⊗ x = 1 ∧ x ⊗ y = 1"
I Reasoning in locale group makes implicit theassumption that G is a group.
I Inverse operation is derived, not part of the record.
IJCAR 2004, Tutorial T4 – p.123
Hierarchy of Structures
record ’a ring = "’a monoid" +zero :: ’a ("0ı")add :: "[’a, ’a] ⇒ ’a" (infixl "⊕ı" 65)
record (’a, ’b) module = "’b ring" +smult :: "[’a, ’b] ⇒ ’b" (infixl "�ı" 70)
record (’a, ’p) up_ring = "(’a, ’p) module" +monom :: "[’a, nat] ⇒ ’p"coeff :: "[’p, nat] ⇒ ’a"
IJCAR 2004, Tutorial T4 – p.124
Hierarchy of Specifications
monoid G
group G comm_monoid G
comm_group G
abelian_monoid G
abelian_group G
cring R
ring_hom_cring R S domain R module R M
R
R
M
R S
IJCAR 2004, Tutorial T4 – p.125
Polynomials
Functor UP that maps ring structures to polynomialstructures.
constdefs (structure R)UP :: "(’a, ’m) ring_scheme ⇒ (’a, nat ⇒ ’a) up_ring""UP R ≡ (| carrier = up R,mult = (λp∈up R. λq∈up R. λn.
⊕i ∈ {..n}. p i ⊗ q (n-i)),
one = (λi. if i=0 then 1 else 0),zero = (λi. 0),add = (λp∈up R. λq∈up R. λi. p i ⊕ q i),smult = (λa∈carrier R. λp∈up R. λi. a ⊗ p i),monom = (λa∈carrier R. λn i. if i=n then a else 0),coeff = (λp∈up R. λn. p n) |)"
IJCAR 2004, Tutorial T4 – p.126
Locales for Polynomials
I Make the polynomial ring a locale parameter
locale UP = struct R + struct P +defines P_def: "P ≡ UP R"
I Add information about base ring
UP R Pcring R
UP_cring R Pdomain R
UP_domain R P
ring_hom_cring R S
UP_univ_prop R S P
IJCAR 2004, Tutorial T4 – p.127
Properties of UP
Polynomials over a ring form a ring.theorem (in UP_cring) UP_cring: "cring P"
Polynomials over an integral domain form a domain.
theorem (in UP_domain) UP_domain: "domain P"
IJCAR 2004, Tutorial T4 – p.128
The Universal Property
R S
UP R
ϕ
Φ, unique for ΦX = s
I Existence of Φ:
eval R S phi s ≡ λp ∈ carrier (UP R).⊕
i ∈ {..deg R p}. phi (coeff (UP R) p i) ⊗ s (^) i
Show that eval R S phi is a homomorphism.
IJCAR 2004, Tutorial T4 – p.129
The Universal Property
R S
UP R
ϕ
Φ, unique for ΦX = s
I Uniqueness of Φ:
Show that two homomorphisms Φ,Ψ : UP R → S withΦX = ΨX = s are identical.
IJCAR 2004, Tutorial T4 – p.130
Demo: uniqueness
IJCAR 2004, Tutorial T4 – p.131
Questions answered by Larry Paulson
Hah! A proof of FalseYour axioms are bogusGo back to square one.
— Larry Paulson
IJCAR 2004, Tutorial T4 – p.132