Isabelle

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
https://isabelle.in.tum.de/doc/tutorial.pdf
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 by sledgehammer ??
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)"
(nat ⇒ nat ⇒ 'a::zero) is like Zero a => nat -> nat -> a) in Haskell
- ie, :: here indicates a type class constraint
`~=`: 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 ⟧ means a, b are parameters and A1, A2 are assumptions
Default associativity of addition is left (unlike coq? where it is right)
Variable used in class has to be 'a ??
- 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
- http://cl-informatik.uibk.ac.at/software/ceta/
- https://isabelle.in.tum.de/library/HOL/HOL-Matrix_LP/Matrix.html
Isabelle Archive of Formal Proofs (Isabelle AFP)
Explicitly open or close a block: { and }
- Focus on next block: next
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
Like in Coq, theorem and lemma have the same effect.
hide_const: hide a constant to avoid namespace pollution ??
- hide_const f: hides f completely
- hide_const (open) f: hides f, but it is still accessible like A.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 of simp
simp acts on current sub-goal only
simp_all and auto acts on all sub-goals
simp add: name allows simp to simplfiy name as well
Example of a case split: simp split: nat.split
Like in ssreflect, by proof-method is short for apply proof-method; done
blast: a complete proof procedure for first order logic
metis: for using proofs discovered via sledgehammer
- Lemmas given as arguments to metis allows Isabelle to independently verify the proof as it doesn't trust third party solvers used by sledgehammer
fastforce: ??
Backchain (backward reasoning): Use rule with apply
- apply (rule name)
method_setup: for creating custom proof methods
- Involves sml ??

Default names:

Definition of a function f is f_def
- ζ-reduction possible via using Let_def
case_name_unfold
- Eg: case_prod_unfold
class_name_def
- Eg: monoid_prod_def

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.
- https://stackoverflow.com/questions/65757547/isabelle-too-many-precedences-in-mixfix-annotation

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
text_raw

—

Anti-quotations

theory
thm
lemma
prop
term
term_type
typeof
const
abbrev
typ
type
class
text
goals
subgoals
prf
full_prf
ML
ML_op
ML_type
ML_structure
ML_functor
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
- https://community.jedit.org/?q=node/view/4439
C-e Up: superscript
C-e Down: subscript
C-e Left: italic
C-e Right: bold
Folding:
- Expand completely: M-S-Ret
- https://www.jedit.org/users-guide/folding.html

Examples of 'cartouches' (ie, the special symbols, I guess):

`\<open>`	`‹`
`\<one>`	`𝟭`

Other editors:

vscode: isabelle vscode (WIP as of Jan 2025)
- https://github.com/seL4/isabelle/blob/master/src/Tools/VSCode/extension/README.md

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
Like contexts 'that have been made persistent'
fixes x ∷ τ (mx): declare local var x of type τ and a mixfix annotation mx
constrains x ∷ τ: introduce a type constraint τ on local var x
- This is deprecated. Use for inside a fixes clause instead.
assumes: introduce local assumptions
defines: 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
quotient_type: Generates a new type with Rep and Abs 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 type
descending, 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:

https://isabelle.in.tum.de/library/HOL/HOL/List.html

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