https://isabelle.in.tum.de/documentation.html
Comments:
(* .... *)
- Like sml
Launch editor:
isabelle jedit
An example isabelle project: https://github.com/WasmCert/WasmCert-Isabelle/
Has HOL, FOL, ZFC
User plugin location:
~/.isabelle/Isabelle2024/jedit
Structured Isar proofs: https://courses.grainger.illinois.edu/cs576/sp2015/doc/isar-overview.pdf
sledgehammer
tactic- Capable of invoking external ATPs to try and figure out proofs
metis
tactic: for using proof discovered bysledgehammer
??
An example proof: https://github.com/hwayne/lets-prove-leftpad/tree/master/isabelle
type_synonym
: For type aliases- Eg:
type_synonym 'a infmatrix = "nat ⇒ nat ⇒ 'a"
- Eg:
type_synonym mem = "(mem_rep × nat option)"
- Eg:
(nat ⇒ nat ⇒ 'a::zero)
is likeZero a => nat -> nat -> a)
in Haskell- ie,
::
here indicates a type class constraint
- ie,
`~=`: not equal to
Isar: a proof language
- Like ltac in Coq
- 'Intelligible Semi-Automated Reasoning'
- https://isabelle.in.tum.de/dist/Isabelle2024/doc/isar-ref.pdf
∧ a b ⟦ A1; A2 ⟧
meansa
,b
are parameters andA1
,A2
are assumptionsDefault associativity of addition is left (unlike coq? where it is right)
Variable used in
class
has to be'a
??- Can't be just
α
- Can't be just
Eisbach: a collection of tools for defining new proof methods
- https://isabelle.in.tum.de/dist/Isabelle2024/doc/eisbach.pdf
method
command
Matrices (extractable): https://www.isa-afp.org/browser_info/current/AFP/Jordan_Normal_Form/document.pdf
Isabelle Archive of Formal Proofs (Isabelle AFP)
Explicitly open or close a block:
{
and}
- Focus on next block:
next
- Focus on next block:
Inner and outer syntax
typedecl
: declare a type but without its definition- Might be useful for axioms
- Eg:
typedecl 'a set
- https://isabelle.in.tum.de/library/HOL/HOL/Set.html#Set.disjnt|const
axiomatization
- introduce multiple constants along with their axiomatic properties
- Note: best not used unless you really know what you are doing
Inner syntax: the HOL syntax (when using Isabelle/HOL)
- Would be within double quotes
- For a single identifier this quotes aren't necessary
Outer syntax: the theory language
- Eg:
begin
,end
,theory
, etc
- Eg:
Like in Coq,
theorem
andlemma
have the same effect.hide_const
: hide a constant to avoid namespace pollution ??hide_const f
: hidesf
completelyhide_const (open) f
: hidesf
, but it is still accessible likeA.f
- Similarly:
hide_class
,hide_fact
,hide_type
Stuff available from
Main
: https://isabelle.in.tum.de/dist/Isabelle2024/doc/main.pdf
Coq analogues:
Isabelle | Coq |
---|---|
Isar | Ltac |
locale | Section |
Proof methods | Tactics |
==> |
-> (implication) |
=> |
-> (arrow) |
value |
Compute |
sorry |
admit |
oops |
give_up |
x:xs |
x # xs |
Proof methods
auto
is 'overeager'Functionality of
auto
includes that ofsimp
simp
acts on current sub-goal onlysimp_all
andauto
acts on all sub-goalssimp add: name
allowssimp
to simplfiyname
as wellExample of a case split:
simp split: nat.split
Like in ssreflect,
by proof-method
is short forapply proof-method; done
blast
: a complete proof procedure for first order logicmetis
: for using proofs discovered viasledgehammer
- Lemmas given as arguments to
metis
allows Isabelle to independently verify the proof as it doesn't trust third party solvers used bysledgehammer
- Lemmas given as arguments to
fastforce
: ??Backchain (backward reasoning): Use
rule
withapply
apply (rule name)
method_setup
: for creating custom proof methods- Involves sml ??
Default names:
- Definition of a function
f
isf_def
- ζ-reduction possible via using
Let_def
- ζ-reduction possible via using
case_name_unfold
- Eg:
case_prod_unfold
- Eg:
class_name_def
- Eg:
monoid_prod_def
- Eg:
Notations
- Precendence ∈ [0, 1000]
- Higher the value, higher the precedence
- Very low and very high values are reserved for meta-logic
- HOL usually ∈ [10, 100]
- Custom notations could be ∈ [100, 900]
notation
Associate a mixfix notation with a predefined definition.
Example from the isabelle tutorial:
definition xor :: "bool => bool => bool" (infixl "[+]" 60)
where "A [+] B = (A ∧ ¬B) ∨ (¬A ∧ B)"
notation (xsymbols) xor (infixl "±" 60)
where xsymbols
is an optional argument?? called the 'print mode specification' which is used when pretty-printing.
abbreviation
Kind of like a more complex form of notation
.
- Useful to assign an alias for a long expression.
- Will be expanded to its definition before it is ever used
print__abbrevs
: print all abbreviations in the current context
Mixfix notations
- Mixfix notations are defined using underscore though they render as a hyphen in documentation.
class group = monoid +
fixes inverse :: ‹'a ⇒ 'a› (‹(_÷)› [1000] 999)
assumes invl: ‹x÷ ⊗ x = 𝟭›
Isabelle document processor
- % becomes λ
- Session: set of files/theories being used as input for printing output
- Ignore a span of line(s): Put it between
*<*
and*>*
oops
is often made to render as...
via latex macros
—
Markup commands:
- chapter
- section
- subsection
- subsubsection
- paragraph
- subparagraph
- text
- txt
- textraw
—
Anti-quotations
- theory
- thm
- lemma
- prop
- term
- termtype
- typeof
- const
- abbrev
- typ
- type
- class
- text
- goals
- subgoals
- prf
- fullprf
- ML
- MLop
- MLtype
- MLstructure
- MLfunctor
- emph
- bold
- verbatim
- file
- url
- cite
- rail: 'railroad diagrams'
Evaluate a term
Use value
to compute. Like Compute
of Coq.
datatype onat = Zero | Succ onat
fun oadd :: "onat ⇒ onat ⇒ onat" where
"oadd Zero n = n" |
"oadd (Succ m) n = Succ (oadd m n)"
value "oadd Zero (Succ Zero)"
(*
"Succ Zero"
:: "onat"
*)
Jedit stuff
https://isabelle.in.tum.de/dist/doc/jedit.pdf
[|
,|]
to make⟦
,⟧
& tab
, or\<and> tab
for∧
- Type
"
to choose‹ .. ›
- Recently used 'cartouches' will show up first
- Use arrow keys to choose, tab to select
- Indent/unindent a block of lines: Shift-Arrow or Ctrl-Shift-Arrow
- Comment a block of lines:
- C-e C-k: As single line comments
- C-e C-c: As one multiline comment
- Looks like there is no way to toggle without a plugin (TextTools plugin)
- https://www.jedit.org/users-guide/commenting.html
- Undo: C-z
- Redo: C-e C-z
- Select a rectangular text block: Alt-Left click
C-e Up
: superscriptC-e Down
: subscriptC-e Left
: italicC-e Right
: bold- Folding:
- Expand completely:
M-S-Ret
- https://www.jedit.org/users-guide/folding.html
- Expand completely:
Examples of 'cartouches' (ie, the special symbols, I guess):
\<open> |
‹ |
\<one> |
𝟭 |
Other editors:
- vscode:
isabelle vscode
(WIP as of Jan 2025)
Classes
https://isabelle.in.tum.de/doc/classes.pdf
- Like haskell type classes ???
- Locale with exactly one type variable
Record type
Example:
record tg =
tg_mut :: mut
tg_t :: t
Locale
A way of having modularity
Part of the isar proof language
Locales are like
Section
-s in Coq ???- Also,
sublocale
- https://isabelle.in.tum.de/dist/Isabelle2024/doc/locales.pdf
- Also,
Like contexts 'that have been made persistent'
fixes x ∷ τ (mx)
: declare local varx
of typeτ
and a mixfix annotationmx
constrains x ∷ τ
: introduce a type constraintτ
on local varx
- This is deprecated. Use
for
inside afixes
clause instead.
- This is deprecated. Use
assumes
: introduce local assumptionsdefines
: add definition of a previously declared name
Lifting and transfer
https://www21.in.tum.de/%7Ekuncar/documents/huffman-kuncar-cpp2013.pdf
Via Quotient and Lifting packages
setup-lifting
,lift-definition
Coercion functions:
- Convert from abstract to raw type:
Rep
(to an arbitrary element in the equivalence class) - Convert from raw to abstract type:
Abs
- The equivalence relation R may be a partial relation
- Convert from abstract to raw type:
quotient_type
: Generates a new type withRep
andAbs
functions when given a raw type and an equivalence relation- Each element corresponds to an equivalence class in the equivalence relation
quotient_definition
: Create a function on abstract type given function on raw type and the quotient typedescending
,lifting
Bundled declarations (Isar)
bundle
unbundle
include
includes
including
Prove mode and state mode ??
A class instance can be defined in more than one way, apparently.
theory Example
imports Main
begin
class semigroup =
fixes sgop :: ‹'a ⇒ 'a ⇒ 'a› (infixl ‹⊗› 70)
assumes assoc : ‹(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)›
class monoid = semigroup +
fixes unit :: ‹'a› (‹𝟭›)
assumes unitl : ‹unit ⊗ x = x›
and unitr : ‹x ⊗ unit = x›
instantiation prod :: (semigroup, semigroup) semigroup
begin
definition sgop_prod :: "'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b" where
"sgop_prod x y =
(case x of (a1, b1) ⇒
(case y of (a2, b2) ⇒ (a1 ⊗ a2, b1 ⊗ b2)))"
instance proof
fix p q r :: ‹'a::semigroup × 'b::semigroup›
show ‹(p ⊗ q) ⊗ r = p ⊗ (q ⊗ r)›
unfolding sgop_prod_def
unfolding case_prod_unfold
by (simp add: assoc)
qed
end
The instance for pair semigroup could also have been done (outside of prove mode??) like:
instance
apply (standard)
apply (simp add: sgop_prod_def)
apply (simp add: case_prod_unfold)
apply (simp add: assoc)
done
'Old-style datatypes'
- We probably needn't worry about it.
- New
datatype
declarations are at least as capable as the 'old datatypes'. - Theories use
datatype_compat
to make new datatypes compatible with old datatype machinery
From https://isabelle.in.tum.de/library/Doc/Datatypes/Datatypes.html:
'
datatype_compat
command registers new-style datatypes as old-style datatypes and invokes the old-style plugins'
Annotations
Use (nonexhaustive)
annotation to say that a function is not total. For example:
primrec (nonexhaustive) last :: "'a list ⇒ 'a" where
"last (x # xs) = (if xs = [] then x else last xs)"
Code gen
https://isabelle.in.tum.de/doc/codegen.pdf
- Executable specifications can be converted to programs
- Eg: sml, haskell, ocaml, scala
Misc
- Isabelle is named after Gérard Huet's daughter