pmisabelle.sty

% Poor man's Isabelle markup
% Author: Christoph Lange <math.semantic.web@gmail.com>
% https://github.com/clange/latex
\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{pmisabelle}[2013/10/03]
\RequirePackage{amsmath}% for align environments
% Documentation
%
% The following sample lemma does everything the hard way.  It is recommended to use this package with unicode-chars.sty (to be able to copy/paste mathematical Unicode symbols from Isabelle/jEdit or ProofGeneral).
%
% LaTeX:
% \begin{pmi}
%   \pmikw*{lemma}\pminl
%   \quad\pmikw{fixes} \pmiid*{valid}::\text{``}\pmiid*{'Inputs} \Rightarrow \pmiid*{bool}\text{''}\pminl
%   \quad\pmikw{and} R::\pmitm*{(\pmiid*{'Inputs} \times \pmiid*{'Outcomes})\ set\text{''}}\pminl
%   \quad\pmikw{shows}\ \pmitm{(\forall \pmiid*{inp}\ldotp\pmiid{valid} \pmiid*{inp} \longrightarrow (\exists \pmiid*{out}\ldotp(\pmiid*{inp}, \pmiid*{out}) \in R))\pminl
%   \qquad\longleftrightarrow \pmiid{Domain} R \supseteq \{ \pmiid*{inp}\ldotp\pmiid{valid} \pmiid*{inp}\}}\pminl
%   \quad\pmikw{by} \pmiid*{blast}\pmill
% \end{pmi}
%
% Isabelle:
% lemma
%   fixes valid::"'Inputs ⇒ bool"
%     and R::"('Inputs × 'Outcomes) set"
%   shows "(∀ inp . valid inp ⟶ (∃ out . (inp, out) ∈ R)) ⟷ Domain R ⊇ { inp . valid inp }"
%   by blast
%
% If you want automated keyword highlighting and feel like experimenting, you can use lstsemantic.sty and, instead of \begin{pmi}...\end{pmi} wrap your Isabelle listing into \begin{lstlisting}[language=Isabelle]...\end{lstlisting}.  For the inner language you would then have to manually go into math mode by using $...$.

% the environment in which all of the following commands should be used
\newenvironment{pmi}{%
  \setlength{\jot}{0pt}% no additional vertical spacing
  \start@align\tw@\st@rredtrue\m@ne&% same environment as align*
}{%         
  \endalign
}
% a new line
\newcommand*{\pminl}{&\\ &}
% last line
\newcommand*{\pmill}{&}
% type restriction colon when not everything is in math mode (e.g. when using this with listings.sty and lstsemantic.sty)
\newcommand*{\pmity}{{}::{}}
% The following commands normally have a space appended, unless you use the starred variant.
% keyword of the Isabelle/Isar language
\newcommand*{\pmikwstar}[1]{\mathbf{#1}}
\newcommand*{\pmikwnostar}[1]{\pmikwstar{#1}\ }
\newcommand\pmikw{\@ifstar\pmikwstar\pmikwnostar}
% identifier
\newcommand*{\pmiidstar}[1]{\mathit{#1}}
\newcommand*{\pmiidnostar}[1]{\pmiidstar{#1}\ }
\newcommand\pmiid{\@ifstar\pmiidstar\pmiidnostar}
% term in "…"
\newcommand*{\pmitmstar}[1]{\text{``}#1\text{''}}
\newcommand*{\pmitmnostar}[1]{\pmitmstar{#1}\ }
\newcommand\pmitm{\@ifstar\pmitmstar\pmitmnostar}