#+TITLE: Isabelle-dump

The [[https://isabelle.in.tum.de/][Isabelle proof assistant]] uses lots of mathematical symbols
in its notation, yet still saves its theories as ASCII files,
using lots of escape sequences, e.g. a simple lemma from set
theory (taken from ~HOL/Set.thy~) might be written like this:

#+begin_src
lemma set_eq_iff: "A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
  by (auto intro:set_eqI)
#+end_src

Luckily, unicode contains a lot of symbols. Piped through
~isabelle-dump~, it looks like this:

#+begin_src
lemma set_eq_iff: "A = B ⟷ (∀x. x ∈ A ⟷ x ∈ B)"
   by (auto intro:set_eqI)
#+end_src

* Usage
~isabelle-dump~ takes no arguments for now. Use it like this:

#+begin_src sh
cat /path/to/theory.thy | isabelle-dump | less
#+end_src sh

Since much of isabelle's syntax follows conventions derived from
the ML language family, you can additionally get rudimentary
syntax highlighting by using [[https://github.com/sharkdp/bat][bat]] with its SML highlighter:

#+begin_src sh
cat /path/to/theory.thy | isabelle-dump | bat -l sml
#+end_src

* Limitations
For now, this assumes that each escape sequence stands on its
own, and ignores things like superscript, which are a modifier
(which will be printed as e.g. x⇧2 instead of the more correct x²
– though sub/superscript in unicode [[https://en.wikipedia.org/wiki/Unicode_subscripts_and_superscripts][is a giant mess in general]]).

It also only knows about escape sequences, and has no idea at all
about proofs, functions, or any other bits of syntax.

~isabelle-dump~ was written over some hours in which I also did
other things, so don't be suprised if you manage to make it panic
or otherwise fail for some input – for test purposes the entire
HOL library was piped through it at least once, but there may
still be some edge cases I haven't thought of.

Lastly, it has a dependency closure including over 100 crates,
which may be considered excessive [citation needed] for something
that could also be implemented using only the standard liberay
and nothing else. I mostly wanted to try working with [[https://softdevteam.github.io/grmtools/master/book/quickstart.html][grmtools]] ...