Isabelle in Livebook

Mix.install([
  # Outside this repository: {:kino_isabelle, "~> 0.1.0-alpha.1"}
  {:kino_isabelle, path: Path.expand("..", __DIR__)}
])

Introduction

This notebook shows the Isabelle theory smart cell of kino_isabelle. It needs a local Isabelle installation: isabelle on PATH, or ISABELLE_TOOL set to the executable. Tested with Isabelle2025-2.

An Isabelle cell has an editor for theory text and a toolbar. Nothing is checked while you type: Isabelle runs when you press Check or evaluate the cell. The first check starts an Isabelle server and the HOL session, which takes a few seconds; later checks reuse them. Both are stopped with the runtime.

A first theory

The cell below generates the theory header from its toolbar: theory Basics, importing Main. Evaluating it binds the result to the variable in Assign to, here basics. Press Check, then move the cursor through the text. The panel under the editor shows the output of the command under the cursor: on value it is "55" :: "nat", on thm the proved statement.

Symbols are stored as \<Rightarrow> and displayed as ⇒. To enter one, type \Rightarrow, \<Righ or an abbreviation such as =>, and pick the symbol from the completion list.

{:ok, basics} =
  KinoIsabelle.check(
    ~S"""
    section \<open>Sums of natural numbers\<close>

    fun sum_to :: "nat \<Rightarrow> nat" where
      "sum_to 0 = 0"
    | "sum_to (Suc n) = Suc n + sum_to n"

    value "sum_to 10"

    lemma sum_to_closed: "2 * sum_to n = n * (n + 1)"
      by (induction n) auto

    thm sum_to_closed
    """,
    session: "HOL",
    theory: "Basics",
    imports: ["Main"]
  )

basics

Errors and counterexamples

This cell imports Basics, the theory of the cell above. All cells of a runtime write their theories to one directory, so a cell can import any theory that was checked before. Check the cell above first.

sum_to_bound is false. With the cursor on nitpick, the panel shows the counterexample Nitpick found. The proof after it fails: the error is underlined and shown in the panel when the cursor is on by. An error does not stop Isabelle; sum_to_mono is still checked.

{:ok, mistakes} =
  KinoIsabelle.check(
    ~S"""
    lemma sum_to_bound: "sum_to n \<le> n"
      nitpick
      by (induction n) auto

    lemma sum_to_mono: "m \<le> n \<Longrightarrow> sum_to m \<le> sum_to n"
      by (induction n) (auto simp: le_Suc_eq)
    """,
    session: "HOL",
    theory: "Mistakes",
    imports: ["Basics"]
  )

mistakes

A complete theory

With Header set to in text, the cell holds a complete theory, from theory … imports … begin to end. The theory name is taken from the text.

{:ok, lists} =
  KinoIsabelle.check(
    ~S"""
    theory Lists
      imports Main
    begin

    fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
      "itrev [] ys = ys"
    | "itrev (x # xs) ys = itrev xs (x # ys)"

    lemma itrev_rev: "itrev xs ys = rev xs @ ys"
      by (induction xs arbitrary: ys) auto

    lemma "\<forall>xs. itrev xs [] = rev xs"
      by (simp add: itrev_rev)

    end
    """,
    session: "HOL",
    header_mode: :manual
  )

lists

Results in Elixir

Evaluating an Isabelle cell returns a KinoIsabelle.Result, rendered as tabs: a summary, all messages grouped by command, the errors only, and Isabelle's raw answer. The cells above bound theirs to basics, mistakes and lists:

{basics.status, mistakes.status, lists.status}

KinoIsabelle.check/2 does the same from Elixir code:

{:ok, result} =
  KinoIsabelle.check(
    ~S"""
    lemma "rev (rev xs) = xs" by simp
    lemma "rev xs = xs" by simp
    """,
    theory: "From_Elixir"
  )

result.status

Each message has a kind (:error, :warning or :writeln), its text, and its range in the checked text as from and to, counted in UTF-16 code units like the editor does.

for message <- result.messages, message.kind == :error, do: message.text

result