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 
- sledgehammertactic- Capable of invoking external ATPs to try and figure out proofs
- metistactic: 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)"
 
- Eg: 
- (nat ⇒ nat ⇒ 'a::zero)is like- Zero 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 ⟧means- a,- bare parameters and- A1,- A2are assumptions
- Default associativity of addition is left (unlike coq? where it is right) 
- Variable used in - classhas 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
- methodcommand
 
- 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, - theoremand- lemmahave the same effect.
- hide_const: hide a constant to avoid namespace pollution ??- hide_const f: hides- fcompletely
- 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
- autois 'overeager'
- Functionality of - autoincludes that of- simp
- simpacts on current sub-goal only
- simp_alland- autoacts on all sub-goals
- simp add: nameallows- simpto simplfiy- nameas well
- Example of a case split: - simp split: nat.split
- Like in ssreflect, - by proof-methodis 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 metisallows 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 - rulewith- apply- apply (rule name)
 
- method_setup: for creating custom proof methods- Involves sml ??
 
Default names:
- Definition of a function fisf_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*>*
- oopsis 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> tabfor- ∧
- 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: 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
 
- 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 var- xof type- τand a mixfix annotation- mx
- constrains x ∷ τ: introduce a type constraint- τon local var- x- This is deprecated. Use forinside afixesclause instead.
 
- This is deprecated. Use 
- 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
 
- Convert from abstract to raw type: 
- quotient_type: Generates a new type with- Repand- Absfunctions 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 datatypedeclarations are at least as capable as the 'old datatypes'.
- Theories use datatype_compatto make new datatypes compatible with old datatype machinery
From https://isabelle.in.tum.de/library/Doc/Datatypes/Datatypes.html:
'
datatype_compatcommand 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