1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
#+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]] ...
|
