\documentclass[namedreferences]{kluwer}
%\usepackage{isabelle,isabellesym}\isabellestyle{it}

\makeatletter
%%
%% Author: Markus Wenzel, TU Muenchen
%% License: GPL (GNU GENERAL PUBLIC LICENSE)
%%
%% macros for Isabelle generated LaTeX output
%%

%%% Simple document preparation (based on theory token language and symbols)

% isabelle environments

\newcommand{\isabellecontext}{UNKNOWN}

\newcommand{\isastyle}{\small\tt\slshape}
\newcommand{\isastyleminor}{\small\tt\slshape}
\newcommand{\isastylescript}{\footnotesize\tt\slshape}
\newcommand{\isastyletext}{\normalsize\rm}
\newcommand{\isastyletxt}{\rm}
\newcommand{\isastylecmt}{\rm}

%symbol markup -- \emph achieves decent spacing via italic corrections
\newcommand{\isamath}[1]{\emph{$#1$}}
\newcommand{\isatext}[1]{\emph{#1}}
\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}

\newdimen\isa@parindent\newdimen\isa@parskip

\newenvironment{isabellebody}{%
\isamarkuptrue\par%
\isa@parindent\parindent\parindent0pt%
\isa@parskip\parskip\parskip0pt%
\isastyle}{\par}

\newenvironment{isabelle}
{\begin{trivlist}\begin{isabellebody}\item\relax}
{\end{isabellebody}\end{trivlist}}

\newcommand{\isa}[1]{\emph{\isastyleminor #1}}

\newcommand{\isaindent}[1]{\hphantom{#1}}
\newcommand{\isanewline}{\mbox{}\\\mbox{}}
\newcommand{\isadigit}[1]{#1}

\chardef\isacharbang=`\!
\chardef\isachardoublequote=`\"
\chardef\isacharhash=`\#
\chardef\isachardollar=`\$
\chardef\isacharpercent=`\%
\chardef\isacharampersand=`\&
\chardef\isacharprime=`\'
\chardef\isacharparenleft=`\(
\chardef\isacharparenright=`\)
\chardef\isacharasterisk=`\*
\chardef\isacharplus=`\+
\chardef\isacharcomma=`\,
\chardef\isacharminus=`\-
\chardef\isachardot=`\.
\chardef\isacharslash=`\/
\chardef\isacharcolon=`\:
\chardef\isacharsemicolon=`\;
\chardef\isacharless=`\<
\chardef\isacharequal=`\=
\chardef\isachargreater=`\>
\chardef\isacharquery=`\?
\chardef\isacharat=`\@
\chardef\isacharbrackleft=`\[
\chardef\isacharbackslash=`\\
\chardef\isacharbrackright=`\]
\chardef\isacharcircum=`\^
\chardef\isacharunderscore=`\_
\chardef\isacharbackquote=`\`
\chardef\isacharbraceleft=`\{
\chardef\isacharbar=`\|
\chardef\isacharbraceright=`\}
\chardef\isachartilde=`\~


% keyword and section markup

\newcommand{\isakeywordcharunderscore}{\_}
\newcommand{\isakeyword}[1]
{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
\newcommand{\isacommand}[1]{\isakeyword{#1}}

\newcommand{\isamarkupheader}[1]{\section{#1}}
\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
\newcommand{\isamarkupsection}[1]{\section{#1}}
\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
\newcommand{\isamarkupsect}[1]{\section{#1}}
\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}

\newif\ifisamarkup
\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
\newcommand{\isaendpar}{\par\medskip}
\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}


% alternative styles

\newcommand{\isabellestyle}{}
\def\isabellestyle#1{\csname isabellestyle#1\endcsname}

\newcommand{\isabellestylett}{%
\renewcommand{\isastyle}{\small\tt}%
\renewcommand{\isastyleminor}{\small\tt}%
\renewcommand{\isastylescript}{\footnotesize\tt}%
}
\newcommand{\isabellestyleit}{%
\renewcommand{\isastyle}{\small\it}%
\renewcommand{\isastyleminor}{\it}%
\renewcommand{\isastylescript}{\footnotesize\it}%
\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
\renewcommand{\isacharbang}{\isamath{!}}%
\renewcommand{\isachardoublequote}{}%
\renewcommand{\isacharhash}{\isamath{\#}}%
\renewcommand{\isachardollar}{\isamath{\$}}%
\renewcommand{\isacharpercent}{\isamath{\%}}%
\renewcommand{\isacharampersand}{\isamath{\&}}%
\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
\renewcommand{\isacharparenleft}{\isamath{(}}%
\renewcommand{\isacharparenright}{\isamath{)}}%
\renewcommand{\isacharasterisk}{\isamath{*}}%
\renewcommand{\isacharplus}{\isamath{+}}%
\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
\renewcommand{\isacharminus}{\isamath{-}}%
\renewcommand{\isachardot}{\isamath{\mathord.}}%
\renewcommand{\isacharslash}{\isamath{/}}%
\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
\renewcommand{\isacharless}{\isamath{<}}%
\renewcommand{\isacharequal}{\isamath{=}}%
\renewcommand{\isachargreater}{\isamath{>}}%
\renewcommand{\isacharat}{\isamath{@}}%
\renewcommand{\isacharbrackleft}{\isamath{[}}%
\renewcommand{\isacharbrackright}{\isamath{]}}%
\renewcommand{\isacharunderscore}{\mbox{-}}%
\renewcommand{\isacharbraceleft}{\isamath{\{}}%
\renewcommand{\isacharbar}{\isamath{\mid}}%
\renewcommand{\isacharbraceright}{\isamath{\}}}%
\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
}

\newcommand{\isabellestylesl}{%
\isabellestyleit%
\renewcommand{\isastyle}{\small\sl}%
\renewcommand{\isastyleminor}{\sl}%
\renewcommand{\isastylescript}{\footnotesize\sl}%
}
 
%%
%% Author: Markus Wenzel, TU Muenchen
%% License: GPL (GNU GENERAL PUBLIC LICENSE)
%%
%% definitions of standard Isabelle symbols
%%

% symbol definitions

\newcommand{\isasymzero}{\isatext{\textzerooldstyle}}  %requires textcomp
\newcommand{\isasymone}{\isatext{\textoneoldstyle}}  %requires textcomp
\newcommand{\isasymtwo}{\isatext{\texttwooldstyle}}  %requires textcomp
\newcommand{\isasymthree}{\isatext{\textthreeoldstyle}}  %requires textcomp
\newcommand{\isasymfour}{\isatext{\textfouroldstyle}}  %requires textcomp
\newcommand{\isasymfive}{\isatext{\textfiveoldstyle}}  %requires textcomp
\newcommand{\isasymsix}{\isatext{\textsixoldstyle}}  %requires textcomp
\newcommand{\isasymseven}{\isatext{\textsevenoldstyle}}  %requires textcomp
\newcommand{\isasymeight}{\isatext{\texteightoldstyle}}  %requires textcomp
\newcommand{\isasymnine}{\isatext{\textnineoldstyle}}  %requires textcomp
\newcommand{\isasymA}{\isamath{\mathcal{A}}}
\newcommand{\isasymB}{\isamath{\mathcal{B}}}
\newcommand{\isasymC}{\isamath{\mathcal{C}}}
\newcommand{\isasymD}{\isamath{\mathcal{D}}}
\newcommand{\isasymE}{\isamath{\mathcal{E}}}
\newcommand{\isasymF}{\isamath{\mathcal{F}}}
\newcommand{\isasymG}{\isamath{\mathcal{G}}}
\newcommand{\isasymH}{\isamath{\mathcal{H}}}
\newcommand{\isasymI}{\isamath{\mathcal{I}}}
\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
\newcommand{\isasymK}{\isamath{\mathcal{K}}}
\newcommand{\isasymL}{\isamath{\mathcal{L}}}
\newcommand{\isasymM}{\isamath{\mathcal{M}}}
\newcommand{\isasymN}{\isamath{\mathcal{N}}}
\newcommand{\isasymO}{\isamath{\mathcal{O}}}
\newcommand{\isasymP}{\isamath{\mathcal{P}}}
\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
\newcommand{\isasymR}{\isamath{\mathcal{R}}}
\newcommand{\isasymS}{\isamath{\mathcal{S}}}
\newcommand{\isasymT}{\isamath{\mathcal{T}}}
\newcommand{\isasymU}{\isamath{\mathcal{U}}}
\newcommand{\isasymV}{\isamath{\mathcal{V}}}
\newcommand{\isasymW}{\isamath{\mathcal{W}}}
\newcommand{\isasymX}{\isamath{\mathcal{X}}}
\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
\newcommand{\isasyma}{\isamath{\mathrm{a}}}
\newcommand{\isasymb}{\isamath{\mathrm{b}}}
\newcommand{\isasymc}{\isamath{\mathrm{c}}}
\newcommand{\isasymd}{\isamath{\mathrm{d}}}
\newcommand{\isasyme}{\isamath{\mathrm{e}}}
\newcommand{\isasymf}{\isamath{\mathrm{f}}}
\newcommand{\isasymg}{\isamath{\mathrm{g}}}
\newcommand{\isasymh}{\isamath{\mathrm{h}}}
\newcommand{\isasymi}{\isamath{\mathrm{i}}}
\newcommand{\isasymj}{\isamath{\mathrm{j}}}
\newcommand{\isasymk}{\isamath{\mathrm{k}}}
\newcommand{\isasyml}{\isamath{\mathrm{l}}}
\newcommand{\isasymm}{\isamath{\mathrm{m}}}
\newcommand{\isasymn}{\isamath{\mathrm{n}}}
\newcommand{\isasymo}{\isamath{\mathrm{o}}}
\newcommand{\isasymp}{\isamath{\mathrm{p}}}
\newcommand{\isasymq}{\isamath{\mathrm{q}}}
\newcommand{\isasymr}{\isamath{\mathrm{r}}}
\newcommand{\isasyms}{\isamath{\mathrm{s}}}
\newcommand{\isasymt}{\isamath{\mathrm{t}}}
\newcommand{\isasymu}{\isamath{\mathrm{u}}}
\newcommand{\isasymv}{\isamath{\mathrm{v}}}
\newcommand{\isasymw}{\isamath{\mathrm{w}}}
\newcommand{\isasymx}{\isamath{\mathrm{x}}}
\newcommand{\isasymy}{\isamath{\mathrm{y}}}
\newcommand{\isasymz}{\isamath{\mathrm{z}}}
\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak
\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak
\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak
\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak
\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak
\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak
\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak
\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak
\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak
\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak
\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak
\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak
\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak
\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak
\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak
\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak
\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak
\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak
\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak
\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak
\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak
\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak
\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak
\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak
\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak
\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak
\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak
\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak
\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak
\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak
\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak
\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak
\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak
\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak
\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak
\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak
\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak
\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak
\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak
\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak
\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak
\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak
\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak
\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak
\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak
\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak
\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak
\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak
\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak
\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak
\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak
\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak
\newcommand{\isasymalpha}{\isamath{\alpha}}
\newcommand{\isasymbeta}{\isamath{\beta}}
\newcommand{\isasymgamma}{\isamath{\gamma}}
\newcommand{\isasymdelta}{\isamath{\delta}}
\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
\newcommand{\isasymzeta}{\isamath{\zeta}}
\newcommand{\isasymeta}{\isamath{\eta}}
\newcommand{\isasymtheta}{\isamath{\vartheta}}
\newcommand{\isasymiota}{\isamath{\iota}}
\newcommand{\isasymkappa}{\isamath{\kappa}}
\newcommand{\isasymlambda}{\isamath{\lambda}}
\newcommand{\isasymmu}{\isamath{\mu}}
\newcommand{\isasymnu}{\isamath{\nu}}
\newcommand{\isasymxi}{\isamath{\xi}}
\newcommand{\isasympi}{\isamath{\pi}}
\newcommand{\isasymrho}{\isamath{\varrho}}
\newcommand{\isasymsigma}{\isamath{\sigma}}
\newcommand{\isasymtau}{\isamath{\tau}}
\newcommand{\isasymupsilon}{\isamath{\upsilon}}
\newcommand{\isasymphi}{\isamath{\varphi}}
\newcommand{\isasymchi}{\isamath{\chi}}
\newcommand{\isasympsi}{\isamath{\psi}}
\newcommand{\isasymomega}{\isamath{\omega}}
\newcommand{\isasymGamma}{\isamath{\Gamma}}
\newcommand{\isasymDelta}{\isamath{\Delta}}
\newcommand{\isasymTheta}{\isamath{\Theta}}
\newcommand{\isasymLambda}{\isamath{\Lambda}}
\newcommand{\isasymXi}{\isamath{\Xi}}
\newcommand{\isasymPi}{\isamath{\Pi}}
\newcommand{\isasymSigma}{\isamath{\Sigma}}
\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
\newcommand{\isasymPhi}{\isamath{\Phi}}
\newcommand{\isasymPsi}{\isamath{\Psi}}
\newcommand{\isasymOmega}{\isamath{\Omega}}
\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
\newcommand{\isasymmapsto}{\isamath{\mapsto}}
\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
\newcommand{\isasymmidarrow}{\isamath{\relbar}}
\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires latexsym
\newcommand{\isasymup}{\isamath{\uparrow}}
\newcommand{\isasymUp}{\isamath{\Uparrow}}
\newcommand{\isasymdown}{\isamath{\downarrow}}
\newcommand{\isasymDown}{\isamath{\Downarrow}}
\newcommand{\isasymupdown}{\isamath{\updownarrow}}
\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
\newcommand{\isasymlangle}{\isamath{\langle}}
\newcommand{\isasymrangle}{\isamath{\rangle}}
\newcommand{\isasymlceil}{\isamath{\lceil}}
\newcommand{\isasymrceil}{\isamath{\rceil}}
\newcommand{\isasymlfloor}{\isamath{\lfloor}}
\newcommand{\isasymrfloor}{\isamath{\rfloor}}
\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel
\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbottom}{\isamath{\bot}}
\newcommand{\isasymtop}{\isamath{\top}}
\newcommand{\isasymand}{\isamath{\wedge}}
\newcommand{\isasymAnd}{\isamath{\bigwedge}}
\newcommand{\isasymor}{\isamath{\vee}}
\newcommand{\isasymOr}{\isamath{\bigvee}}
\newcommand{\isasymforall}{\isamath{\forall\,}}
\newcommand{\isasymexists}{\isamath{\exists\,}}
\newcommand{\isasymbox}{\isamath{\Box}}  %requires latexsym
\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires latexsym
\newcommand{\isasymturnstile}{\isamath{\vdash}}
\newcommand{\isasymTurnstile}{\isamath{\models}}
\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
\newcommand{\isasymstileturn}{\isamath{\dashv}}
\newcommand{\isasymsurd}{\isamath{\surd}}
\newcommand{\isasymle}{\isamath{\le}}
\newcommand{\isasymge}{\isamath{\ge}}
\newcommand{\isasymlless}{\isamath{\ll}}
\newcommand{\isasymggreater}{\isamath{\gg}}
\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb
\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb
\newcommand{\isasymin}{\isamath{\in}}
\newcommand{\isasymnotin}{\isamath{\notin}}
\newcommand{\isasymsubset}{\isamath{\subset}}
\newcommand{\isasymsupset}{\isamath{\supset}}
\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires latexsym
\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
\newcommand{\isasyminter}{\isamath{\cap}}
\newcommand{\isasymInter}{\isamath{\bigcap\,}}
\newcommand{\isasymunion}{\isamath{\cup}}
\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
\newcommand{\isasymsqunion}{\isamath{\sqcup}}
\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
\newcommand{\isasymsqinter}{\isamath{\sqcap}}
\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires stmaryrd
\newcommand{\isasymuplus}{\isamath{\uplus}}
\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
\newcommand{\isasymnoteq}{\isamath{\not=}}
\newcommand{\isasymsim}{\isamath{\sim}}
\newcommand{\isasymdoteq}{\isamath{\doteq}}
\newcommand{\isasymsimeq}{\isamath{\simeq}}
\newcommand{\isasymapprox}{\isamath{\approx}}
\newcommand{\isasymasymp}{\isamath{\asymp}}
\newcommand{\isasymcong}{\isamath{\cong}}
\newcommand{\isasymsmile}{\isamath{\smile}}
\newcommand{\isasymequiv}{\isamath{\equiv}}
\newcommand{\isasymfrown}{\isamath{\frown}}
\newcommand{\isasympropto}{\isamath{\propto}}
\newcommand{\isasymbowtie}{\isamath{\bowtie}}
\newcommand{\isasymprec}{\isamath{\prec}}
\newcommand{\isasymsucc}{\isamath{\succ}}
\newcommand{\isasympreceq}{\isamath{\preceq}}
\newcommand{\isasymsucceq}{\isamath{\succeq}}
\newcommand{\isasymparallel}{\isamath{\parallel}}
\newcommand{\isasymbar}{\isamath{\mid}}
\newcommand{\isasymplusminus}{\isamath{\pm}}
\newcommand{\isasymminusplus}{\isamath{\mp}}
\newcommand{\isasymtimes}{\isamath{\times}}
\newcommand{\isasymdiv}{\isamath{\div}}
\newcommand{\isasymcdot}{\isamath{\cdot}}
\newcommand{\isasymstar}{\isamath{\star}}
\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
\newcommand{\isasymcirc}{\isamath{\circ}}
\newcommand{\isasymdagger}{\isamath{\dagger}}
\newcommand{\isasymddagger}{\isamath{\ddagger}}
\newcommand{\isasymlhd}{\isamath{\lhd}}
\newcommand{\isasymrhd}{\isamath{\rhd}}
\newcommand{\isasymunlhd}{\isamath{\unlhd}}
\newcommand{\isasymunrhd}{\isamath{\unrhd}}
\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
\newcommand{\isasymtriangle}{\isamath{\triangle}}
\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb
\newcommand{\isasymoplus}{\isamath{\oplus}}
\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
\newcommand{\isasymotimes}{\isamath{\otimes}}
\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
\newcommand{\isasymodot}{\isamath{\odot}}
\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
\newcommand{\isasymominus}{\isamath{\ominus}}
\newcommand{\isasymoslash}{\isamath{\oslash}}
\newcommand{\isasymdots}{\isamath{\dots}}
\newcommand{\isasymcdots}{\isamath{\cdots}}
\newcommand{\isasymSum}{\isamath{\sum\,}}
\newcommand{\isasymProd}{\isamath{\prod\,}}
\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
\newcommand{\isasyminfinity}{\isamath{\infty}}
\newcommand{\isasymintegral}{\isamath{\int\,}}
\newcommand{\isasymointegral}{\isamath{\oint\,}}
\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
\newcommand{\isasymaleph}{\isamath{\aleph}}
\newcommand{\isasymemptyset}{\isamath{\emptyset}}
\newcommand{\isasymnabla}{\isamath{\nabla}}
\newcommand{\isasympartial}{\isamath{\partial}}
\newcommand{\isasymRe}{\isamath{\Re}}
\newcommand{\isasymIm}{\isamath{\Im}}
\newcommand{\isasymflat}{\isamath{\flat}}
\newcommand{\isasymnatural}{\isamath{\natural}}
\newcommand{\isasymsharp}{\isamath{\sharp}}
\newcommand{\isasymangle}{\isamath{\angle}}
\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
\newcommand{\isasymhyphen}{\isatext{\rm-}}
\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}}  %requires latin1
\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires latin1
\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}}  %requires latin1
\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires latin1
\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}}  %requires latin1
\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires latin1
\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
\newcommand{\isasymsection}{\isatext{\rm\S}}
\newcommand{\isasymparagraph}{\isatext{\rm\P}}
\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
\newcommand{\isasymeuro}{\isatext{\EUR}}  %requires marvosym
\newcommand{\isasympounds}{\isamath{\pounds}}
\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
\newcommand{\isasymcent}{\isatext{\cent}}  %requires wasysym
\newcommand{\isasymcurrency}{\isatext{\currency}}  %requires wasysym
\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
\newcommand{\isasymamalg}{\isamath{\amalg}}
\newcommand{\isasymmho}{\isamath{\mho}}  %requires latexsym
\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssym
\newcommand{\isasymJoin}{\isamath{\Join}}  %requires latexsym
\newcommand{\isasymwp}{\isamath{\wp}}
\newcommand{\isasymwrong}{\isamath{\wr}}
\newcommand{\isasymstruct}{\isamath{\diamond}}
\newcommand{\isasymacute}{\isatext{\'\relax}}
\newcommand{\isasymindex}{\isatext{\i}}
\newcommand{\isasymdieresis}{\isatext{\"\relax}}
\newcommand{\isasymcedilla}{\isatext{\c\relax}}
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
\newcommand{\isasymspacespace}{\isamath{~~}}
\makeatother
\isabellestyle{it}

\usepackage{url}
\usepackage{alltt}
\usepackage{supertabular}

\raggedbottom

\hyphenation{Isabelle}
\renewcommand{\isadigit}[1]{\isamath{#1}}


\begin{document}

\begin{article}

\begin{opening}

\title{A comparison of Mizar and Isar}
\author{Markus \surname{Wenzel} \email{wenzelm@in.tum.de} \thanks{Research supported by DFG project `Isar' and EU working group `TYPES'}}
\institute{Institut f\"ur Informatik, Technische Universit\"at M\"unchen, Germany}
\author{Freek \surname{Wiedijk} \email{freek@cs.kun.nl} \thanks{Research supported by EU working group `TYPES' and EU network `Calculemus'}}
\institute{Department of Computer Science, University of Nijmegen, the Netherlands}

\begin{abstract}
  The mathematical proof checker Mizar by Andrzej Trybulec uses a proof input
  language that is much more readable than the input languages of most other
  proof assistants.  This system also differs in many other respects from most
  current systems.  John Harrison has shown that one can have a \emph{Mizar
    mode} on top of a tactical prover, allowing one to combine a mathematical
  proof language with other styles of proof checking.  Currently the only
  fully developed Mizar mode in this style is the Isar proof language for the
  Isabelle theorem prover.  In fact the Isar language has become the official
  input language to the Isabelle system, even though many users still use its
  low-level tactical part only.
  
  In this paper we compare Mizar and Isar.  A small example, Euclid's proof of
  the existence of infinitely many primes, is shown in both systems.  We also
  include slightly higher-level views of formal proof sketches.  Moreover a
  list of differences between Mizar and Isar is presented, highlighting the
  strengths of both systems from the perspective of end-users.  Finally, we
  point out some key differences of the internal mechanisms of structured
  proof processing in either system.
\end{abstract}

\keywords{Formalized mathematics, structured proof languages, proof sketches.}

\end{opening}


\section{Introduction}

\subsection{Overview}

We compare two systems for formalizing mathematics in
the computer: the Mizar system by Andrzej Trybulec from Bia{\l}ystok, Poland
\cite{rud:92,try:93,muz:93,wie:99:1}, and the Isar interface by Markus Wenzel
from Munich, Germany \cite{wen:99,wen:02:thesis,wen:02:isar-ref} to the
Isabelle system by Larry Paulson and Tobias Nipkow
\cite{pau:94,nip:pau:wen:02}.  From the perspective of recipients of formal
proof documents, human readers, the proof languages of both systems appear very similar.  The
key differences (concerning the underlying concepts and various technical
issues) become more relevant once that users wish to compose their own
formalizations, or explore the internal principles of structured proof
processing.

The names of the systems can be used on four different levels
(e.g., in the sentence `in Isar the Hahn-Banach theorem is available'
the word `Isar' is used as referring to the Isabelle/HOL library):
\begin{center}
\begin{tabular}{lcl}
the Mizar language &$\qquad$& the Isar language \\
the Mizar system && the Isabelle system \\
&& the Isabelle/HOL logic \\
the Mizar library && the Isabelle/HOL library
\end{tabular}
\end{center}
These four levels are conceptually unrelated:
there could be multiple implementations of the Mizar and Isar
languages, there are many logics for the Isabelle
logical framework, and one could write different libraries for both systems.
However, in practice all four levels are used together, as a whole.
Almost all users of Mizar or Isar are
using the current version of language, system, logic and library.
Therefore, when discussing Mizar and Isar from a user's point of view,
the Mizar and Isar
languages should not be separated from the corresponding systems.
For this same reason we will use the term `Isar system'
to refer to the Isabelle system with the Isar proof language,
and with the Isabelle/HOL logic and library.
(Although the Isar language can be used with all Isabelle logics,
the large majority of Isabelle users work in Isabelle/HOL.)

In this paper we compare the current states of the Mizar
and Isar systems.
Both systems are under active development and probably will
change significantly in the coming years.
This paper should be seen as a snapshot of the current situation.

The intended audiences for this paper are 
those who want to know more about Mizar and Isar
and the people who work on the implementation of Mizar or Isar
or of a similar declarative proof assistant.
We think that systems can benefit from the experiences of other systems.

The aims of this paper are:
\begin{itemize}
\item
\emph{To compare the Mizar and Isar proof languages.}
We demonstrate the similarity between proofs in these two
languages through a simple example from number theory (Sections~\ref{example} and~\ref{sketch}),
but we also show that the
internal principles of processing those proofs are significantly
different in both systems (Section~\ref{internals}).

\item
\emph{To compare the Mizar and
Isar systems from the experience of the end-user.}
We give a high level comparison of the Mizar and Isar
systems from a user's point of view,
by pointing out the relative strengths and weaknesses of
both systems (Section~\ref{differences}).

\item
\emph{To attract more attention to declarative provers.}
The declarative proof style of the Mizar and Isar languages
can draw more people to formal proofs.
The small example that we present in both languages
acts as a gentle introduction to declarative proof.

\end{itemize}

%As an example, we will show Mizar and Isar formalizations of the same proof of
%a simple theorem from number theory (Section~\ref{example}).  We will also
%show how both systems can handle a `formal proof sketch' of these
%formalizations (Section~\ref{sketch}).  Then we discuss the differences of the
%Mizar and Isar systems concerning the end-user view
%(Section~\ref{differences}).  Finally we exhibit key differences of the
%internal mechanisms of structured proof processing (Section~\ref{internals}).


\subsection{Related work}

The concept of human-readable formal proof was pioneered by de Bruijn,
who coined the term
`mathematical vernacular' \cite{bru:87} for a formal language that has
a structure similar to informal mathematical text.
However on the surface de Bruijn's MV language still looks more like
a formal language than like natural language.
%
Recently research into `declarative' proof assistants (as opposed to
the `procedural' proof assistants that have been exercised for
several decades now) has become popular.
Declarative systems not only follow the structure but also the language of
informal mathematics.
Apart from the Mizar and Isar developments, in recent years research
into the declarative proof style has resulted in several
experimental systems.
%that focus on accessible representations of formal proofs themselves.

\medskip The `Mizar mode for HOL' \cite{har:96} provides an alternative
interface for interactive proof composition in HOL (notably HOL Light),
transferring useful ideas from the Mizar proof language into the tactical
setting of HOL.  Harrison introduces separate concrete syntax for structured
proof commands that are translated to special tactics inside, which perform
basic transformations according to natural deduction schemes of raw first
order logic.  Harrison also spends substantial effort on automated reasoning
support, for solving `trivial' situations implicitly (the concrete procedure
may be exchanged by the user).  The Mizar mode also covers a calculational
reasoning style, which refers to a collection of mixed transitivity rules
declared in the context (using $=$/$<$/$\le$ or similar relations).  The
system has been sufficiently developed to conduct some example proofs from
classical analysis, covering a few pages of text.  It has not been applied any
further, though.

\medskip DECLARE \cite{sym:97,sym:98} is a stand-alone prototype system for
`declarative' proof development, which acts like a compiler for formal
documents consisting of theory specifications and structured proof outlines.
The proof language is based on three main principles, namely `first-order
decomposition and enrichment', `second-order schema application', and `appeals
to automation'.  DECLARE has been advertised as `three tactic theorem proving'
\cite{sym:99}.  The system draws from the general experience of the HOL family
(and Harrison's Mizar mode), but renounces established principles like full
reduction to basic logical principles inside.  DECLARE has been successfully
applied by its author in some significant case-studies on Java type-safety and
operational semantics \cite{sym:98}.  In fact, many concepts of DECLARE have
been specifically designed towards such applications of language modeling,
with particular support for inductive definitions and proof schemes.  DECLARE
did not aim at more general applications, and has not been evaluated any
further in practice (the system is not publicly available anyway).

\medskip The `Structured Proof Language' (SPL) \cite{zam:99,zam:99:thesis}
aims at providing another interface for proof construction in mainstream HOL,
drawing from Mizar ideas and the experience with Harrison's Mizar mode.  SPL
has been intended for larger scale applications, just like DECLARE, but is
more careful to stay within the logical foundations of HOL.  All high-level
concepts of SPL are reduced to primitive HOL tactics.  Zammit also spends
significant effort on powerful first-order proof tools in HOL, in order to
support reasoning in large steps.  Another focus is on implicit
simplifications (via rewriting).  The SPL/HOL system has been evaluated by its
author by formalizing some portions of group theory, attempting to achieve the
same level of abstraction seen in the informal proofs of a given textbook.

\medskip `Mizar Light for HOL Light' \cite{wie:01} represents a minimal system
experiment that achieves a readable view on first-order tactical proof
schemes, mainly by exhibiting propositions explicitly in the text instead of
implicitly in goal configurations.  It shows that it is not necessary to
change the notion of proof state of a goal oriented system to be able to
support declarative proofs.

\medskip Systems in the important class of `teaching tools for formal logic'
often provide readable textual representations of proofs as well, although
most seem to prefer graphical views.  Typically, such systems are restricted
to primitive inferences in pure logic, where users may occasionally specify
their own set of rules, but advanced proof procedures are unavailable.

The teaching tool ProveEasy \cite{bur:98} provides an interactive editor for
primitive natural-deduction proof texts presented in a strictly backward
manner.  The underlying structure is oriented towards the well-established
$\lambda$-calculus view of type theory.  Here the main idea is to make the
types of sub-terms (local propositions) visible in the text.

Tutch \cite{abe:01} is a strictly text-oriented proof-checker intended for
teaching constructive logic.  The system deliberately excludes any kind of
user interface, but acts like a batch-mode compiler of proof texts written in
plain ASCII.  Thus students are encouraged to focus on the task of actually
writing proofs, rather than play with fancy point-and-click interfaces.  Proof
steps in Tutch range from primitive natural deduction to more abstract
arrangements of the `assertion level'.  Nevertheless, the system refrains from
arbitrary proof search, but implements an efficient algorithm for structured
proof checking.


\section{Example: there are infinitely many prime numbers}\label{example}

In a talk at the Dutch proof tools day 2002 in Utrecht, Herman Geuvers
presented two slides that were meant to show the difference in style between
informal and formal proofs.  The informal proof on the first slide looked like
this:
\medskip
\begin{quote}
\emph{A romantic proof}
\medskip

\label{romantic}\textsc{Theorem} There are infinitely many primes:\\
for every number $n$ there exists a prime $p> n$ \medskip

\textsc{Proof} [after Euclid]\\
Given $n$. Consider $k=n!+1$, where $n!=1\cdot 2\cdot 3\cdot \ldots\cdot n$.\\
Let $p$ be a prime that divides $k$.\\
For this number $p$ we have $p> n$: otherwise $p\leq n$;\\
but then $p$ divides $n!$,
so $p$ cannot divide $k=n!+1$,\\
contradicting the choice of $p$. QED
\end{quote}

\medskip\noindent
The formal proof on the other slide was a big and unreadable `proof
term' (taken from a Lego formalization by Mark Ruys):
\smallskip
\begin{quote}
\emph{A `real' proof} (\emph{proof-object})
\medskip

%\textsc{Theorem} $\forall n \exists p > n.\, {\rm Prime}(p)$
%\medskip
%
\textsc{Proof-object} [Formalization: Ruys]
\medskip

\begingroup\small
\def\nat{{\rm I\! N}}\def\arr{{\rightarrow}}\def\l{\lambda}\def\qedd{~\rule{3mm}{3mm}}%
$\l n{:}|\nat| .
[\leq=ap2{\_}\nat{\_}\nat{\_}\Omega\ lessEq]
[<=ap2{\_}\nat{\_}\nat{\_}\Omega\ lessE]
[k{=}succ (fac\ n)\\]\ has{\_}prime{\_}factor\ k
({\leq}{\_}elim{\_}2 (fac\ n) (le{\_}one{\_}fac\ n)) (\exists y{:}|\nat|.
(n{<}y\ \&\ y\\{\leq}k\ \&\  prime(y)))
(\l y{:}|\nat| .\l P{:}is{\_}prime{\_}factor\ y\ k.
[D{=}fst(y| k)(prime(y)\\)P] [Q{=}snd(y|k)(prime(y))P]
[H{=}fst(1{<} y)({\Pi u{:}|\nat|}.(1{<}u)\arr(u{<} y)\arr (u\\\!\not| y))Q]
ExIntro(|\nat|)\ y\ (\l v{:}|\nat|.(n{<}v\ \&\ v{\leq}k\ \&\ prime(v))
(pair(n{<}y\ \&\ y\\{\leq}\ k\ (prime(y)) (pair(n{<}y)\ (y {\leq} k)
({<}{\_}intro\ y\ n\ (\l F{:}
y{\leq}n.{<}{\_}irrefl\ 1\ (\\extenRel\_\nat\_\nat\ {<}\ 1\
(Eq{\_}refl\_\nat\ 1) y\ 1\ (divides{\_}lemma{\_}3\ y\ (fac\ n)\ (\\fac{\_}divides\ y\ n
({\leq}{\_}intro{\_}2\ y\ ({<}{\_}succ{\_}intro\ 1\ y\ H))F) D) H) \bot))
(\\divides{\_}lemma{\_}1\ y\ k\ D\ (y{\leq}k\ 
(Id\ (y{\leq}k))\ (\l G{:}Eq\_\nat\ k\ 0. 
Succ{\_}not{\_}zero\ (\\fac\ n)G\ (y {\leq}k))))\ Q))
(\exists y{:}|\nat|.(n{<}y\ \&\ prime(y))\ 
(\l y{:}|\nat|.{}\l H{:}n{<}y\ \&\ y{\leq}k\\\ \&\ 
prime(y).ExIntro(|\nat|)\ y
(\l w{:}|\nat|. (n{<}w\ \&\
prime(w)) (pair(n{<}y)\ (\\prime(y))\ (fst(n{<}y)\ (y{\leq}k) (fst(n{<}y\ \&\
y{\leq}k) (prime(y))\ H))(snd(n{<}y\\\ \&\ \ y{\leq}k)\ (prime(y))H))))))))$
\endgroup
\end{quote}

\medskip\noindent
But a formal proof does not need to look like this!  In a
Mizar-style proof language the formal proof of this theorem will be quite
similar to the `informal' version from Herman's first slide.  Subsequently we
will use this example (the infinity of the set of prime numbers) as the proof
for which we will show both Mizar and Isar versions.



\subsection{Mizar version of the formalization}\label{example-mizar}

Here is the final part of a Mizar formalization of the `romantic proof'.  The
full Mizar formalization is 44 lines long.  It builds on the Mizar
Mathematical Library (\url{http://mizar.org/JFM/}), which is part of the Mizar
system.  Here we have used Mizar version 6.1.10.

\begin{verbatim}
reserve n,p for Nat;
\end{verbatim}

\begin{verbatim}
theorem Euclid: ex p st p is prime & p > n
proof
 set k = n! + 1;
 n! > 0 by NEWTON:23;
 then n! >= 0 + 1 by NAT_1:38;
 then k >= 1 + 1 by REAL_1:55;
 then consider p such that
A1: p is prime & p divides k by INT_2:48;
A2: p <> 0 & p > 1 by A1,INT_2:def 5;
 take p;
 thus p is prime by A1;
 assume p <= n;
 then p divides n! by A2,NAT_LAT:16;
 then p divides 1 by A1,NAT_1:57;
 hence contradiction by A2,NAT_1:54;
end;
\end{verbatim}

\begin{verbatim}
theorem {p: p is prime} is infinite
 from Unbounded(Euclid);
\end{verbatim}
Note that the proof of the first theorem has to contain low level `algebraic
facts' like \verb|n!| \verb|>=| \verb|0| \verb|+| \verb|1|, \verb|k| \verb|>=|
\verb|1| \verb|+| \verb|1|, \verb|p| \verb|<>| \verb|0| and \verb|p| \verb|>|
\verb|1|.  Apart from the part of the text that is shown, the Mizar
formalization contains an `\verb|environ|' header and a proof of the following
rule scheme:
\smallskip
\begin{quote}
\begin{verbatim}
scheme Unbounded {P[Nat]}: {n: P[n]} is infinite
 provided for m ex n st P[n] & n > m;
\end{verbatim}
\end{quote}
\smallskip
It is proved from a similar theorem from the Mizar library.

\smallskip

The Mizar system is not interactive.  One runs the main executable \verb|mizf|
like a batch-mode compiler and it inserts the error messages, if any, as
comments inside the original Mizar source text.


\subsection{Isar version of the formalization}\label{example-isar}

Here is the final part of an Isar formalization of the `romantic proof' again.
The full Isar formalization is 95 lines long.  It includes the theory
\textit{Main} from the standard Isabelle/HOL library
(\url{http://isabelle.in.tum.de/library/HOL/}), as well as the theory
\textit{Factorization} by Thomas Rasmussen (from the Isabelle examples).  Here
we use Isabelle2002.

\medskip
\begin{isabellebody}\normalsize
\isamarkupfalse%
\isacommand{theorem}\ Euclid{\isacharcolon}\ {\isachardoublequote}{\isasymexists}p\ {\isasymin}\ prime{\isachardot}\ n\ {\isacharless}\ p{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{proof}\ {\isacharminus}\isanewline
\ \ \isamarkupfalse%
\isacommand{let}\ {\isacharquery}k\ {\isacharequal}\ {\isachardoublequote}n{\isacharbang}\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\isanewline
\ \ \isamarkupfalse%
\isacommand{obtain}\ p\ \isakeyword{where}\ prime{\isacharcolon}\ {\isachardoublequote}p\ {\isasymin}\ prime{\isachardoublequote}\ \isakeyword{and}\ dvd{\isacharcolon}\ {\isachardoublequote}p\ dvd\ {\isacharquery}k{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{using}\ prime{\isacharunderscore}factor{\isacharunderscore}exists\ \isamarkupfalse%
\isacommand{by}\ auto\isanewline
\ \ \isamarkupfalse%
\isacommand{have}\ {\isachardoublequote}n\ {\isacharless}\ p{\isachardoublequote}\isanewline
\ \ \isamarkupfalse%
\isacommand{proof}\ {\isacharminus}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ p\ {\isasymle}\ n{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{proof}\isanewline
\ \ \ \ \ \ \isamarkupfalse%
\isacommand{assume}\ {\isachardoublequote}p\ {\isasymle}\ n{\isachardoublequote}\isanewline
\ \ \ \ \ \ \isamarkupfalse%
\isacommand{with}\ prime{\isacharunderscore}g{\isacharunderscore}zero\ \isamarkupfalse%
\isacommand{have}\ {\isachardoublequote}p\ dvd\ n{\isacharbang}{\isachardoublequote}\ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}rule\ dvd{\isacharunderscore}factorial{\isacharparenright}\isanewline
\ \ \ \ \ \ \isamarkupfalse%
\isacommand{with}\ dvd\ \isamarkupfalse%
\isacommand{have}\ {\isachardoublequote}p\ dvd\ {\isacharquery}k\ {\isacharminus}\ n{\isacharbang}{\isachardoublequote}\ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}rule\ dvd{\isacharunderscore}diff{\isacharparenright}\isanewline
\ \ \ \ \ \ \isamarkupfalse%
\isacommand{then}\ \isamarkupfalse%
\isacommand{have}\ {\isachardoublequote}p\ dvd\ {\isadigit{1}}{\isachardoublequote}\ \isamarkupfalse%
\isacommand{by}\ simp\isanewline
\ \ \ \ \ \ \isamarkupfalse%
\isacommand{with}\ prime\ \isamarkupfalse%
\isacommand{show}\ False\ \isamarkupfalse%
\isacommand{using}\ prime{\isacharunderscore}nd{\isacharunderscore}one\ \isamarkupfalse%
\isacommand{by}\ auto\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{qed}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{then}\ \isamarkupfalse%
\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
\isacommand{by}\ simp\isanewline
\ \ \isamarkupfalse%
\isacommand{qed}\isanewline
\ \ \isamarkupfalse%
\isacommand{from}\ this\ \isakeyword{and}\ prime\ \isamarkupfalse%
\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
\isacommand{{\isachardot}{\isachardot}}\isanewline
\isamarkupfalse%
\isacommand{qed}
\end{isabellebody}
\bigskip

\begin{isabellebody}\normalsize
\isamarkupfalse%
\isacommand{corollary}\ {\isachardoublequote}{\isasymnot}\ finite\ prime{\isachardoublequote}\isanewline
\ \ \isamarkupfalse%
\isacommand{using}\ Euclid\ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}fastsimp\ dest{\isacharbang}{\isacharcolon}\ finite{\isacharunderscore}nat{\isacharunderscore}set{\isacharunderscore}is{\isacharunderscore}bounded\ simp{\isacharcolon}\ le{\isacharunderscore}def{\isacharparenright}$\!\!\!$
\end{isabellebody}

\medskip\noindent Note that the Isabelle library does not know the $>$
relation.  Therefore, instead of writing $p > n$ one has to write $n < p$.
Also the relationship between $<$ and $\le$ is not hard-wired into the system,
making an extra level of \textbf{proof} {\dots} \textbf{qed} in the proof of
$n < p$ necessary here.  The \textit{fastsimp} method that is used in the
proof of the final corollary is not one of the three most commonly used ones:
\textit{simp}, \textit{blast} and \textit{auto}.  The corollary may also have
been proved with a three step Isar proof that only uses the \textit{auto}
method.

Apart from the part of the text that is shown here, the Isar formalization
contains the definition of the factorial function and the following five
lemmas (including hints for automated tools):

\medskip
\begin{quote}
\begin{isabellebody}\normalsize
\isamarkupfalse%
\isacommand{lemma}\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isadigit{0}}\ {\isacharless}\ n{\isacharbang}{\isachardoublequote}
\end{isabellebody}
\medskip

\begin{isabellebody}\normalsize
\isamarkupfalse%
\isacommand{lemma}\ dvd{\isacharunderscore}prod\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ dvd\ prod\ {\isacharparenleft}n\ {\isacharhash}\ ns{\isacharparenright}{\isachardoublequote}
\end{isabellebody}
\medskip

\begin{isabellebody}\normalsize
\isamarkupfalse%
\isacommand{lemma}\ prime{\isacharunderscore}factor{\isacharunderscore}exists{\isacharcolon}\ {\isachardoublequote}{\isadigit{1}}\ {\isacharless}\ n\ {\isasymLongrightarrow}\ {\isasymexists}p\ {\isasymin}\ prime{\isachardot}\ p\ dvd\ n{\isachardoublequote}
\end{isabellebody}
\medskip

\begin{isabellebody}\normalsize
\isamarkupfalse%
\isacommand{lemma}\ dvd{\isacharunderscore}factorial{\isacharcolon}\ {\isachardoublequote}{\isadigit{0}}\ {\isacharless}\ m\ {\isasymLongrightarrow}\ m\ {\isasymle}\ n\ {\isasymLongrightarrow}\ m\ dvd\ n{\isacharbang}{\isachardoublequote}
\end{isabellebody}
\medskip

\begin{isabellebody}\normalsize
\isamarkupfalse%
\isacommand{lemma}\ finite{\isacharunderscore}nat{\isacharunderscore}set{\isacharunderscore}is{\isacharunderscore}bounded{\isacharcolon}\isanewline
\ \ {\isachardoublequote}finite\ M\ {\isasymLongrightarrow}\ {\isasymexists}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m\ {\isasymin}\ M{\isachardot}\ m\ {\isasymle}\ n{\isachardoublequote}
\end{isabellebody}
\end{quote}
%

\medskip\noindent
Isar is an interactive system.  The preferred interface to Isar is Proof
General \cite{asp:00}, which is the `proof assistant mode' for the (X)Emacs
editor.  When editing an Isar formalization, at each point in the text the
interface shows relevant bits of the proof state.


\subsection{Relating the two languages}

The Mizar and Isar languages use different keywords for similar notions.  Here
is a rough translation table that relates major language elements.

\begin{center}
\begin{supertabular}{rcl}
\emph{Mizar} && \emph{Isar} \\[0.5ex]

\verb|let| && \textbf{fix} \\[-0.5ex]
\verb|assume| && \textbf{assume} \\[-0.5ex]
\verb|set| && \textbf{let} \\[-0.5ex]
\verb|set| && \textbf{def} \\[-0.5ex]
\verb|consider| {\dots} \verb|such that| && \textbf{obtain} {\dots} \textbf{where} \\[-0.5ex]
%\verb|given| {\dots} \verb|such that| && \textbf{obtain} {\dots} \textbf{where} {\dots} \textbf{using} \textit{prems} \\[-0.5ex]
\verb|take| && \emph{no equivalent} \\[-0.5ex]
\verb|per| \verb|cases| {\dots} && \textbf{proof} {\dots} \textbf{qed} \\[-0.5ex]
\verb|suppose| && \textbf{next assume} \\[-0.5ex]
\emph{no keyword} && \textbf{have} \\[-0.5ex]
\verb|thus| && \textbf{show} \\[-0.5ex]
\verb|hence| && \textbf{then show} \\[-0.5ex]
\verb|thesis| && \textit{?thesis} \\[-0.5ex]
\verb|proof| {\dots} \verb|end| && \textbf{proof} {\dots} \textbf{qed} \\[-0.5ex]
\verb|@proof| {\dots} \verb|end| && \textbf{sorry} \\[-0.5ex]
\verb|now| {\dots} \verb|end| && \textbf{\{} {\dots} \textbf{\}} \\[-0.5ex]
\verb|then| && \textbf{then} \\[-0.5ex]
\verb|then| {\dots} \verb|by| && \textbf{with} \\[-0.5ex]
\verb|by| &$\quad$& \textbf{from} \\[-0.5ex]
\verb|by| &$\quad$& \textbf{using} \\[-0.5ex]
\verb|;| && \textbf{.} \\[-0.5ex]
\verb|;| && \textbf{..} \\[-0.5ex]
\verb|;| && \textbf{by} \emph{auto} \\[-0.5ex]
\verb|from| {\dots}\verb|;| && \textbf{by} (\emph{rule} {\dots}) \\[-0.5ex]
\end{supertabular}
\end{center}

\noindent
Note that the mapping between language elements is not exact.  For instance
the distinction between \verb|by| and \verb|from| (the first is first
order while the second is higher order) is not reflected in the Isar
equivalent.

Also note that in the translation of Mizar's `\verb|by| {\dots} \verb|;|' to
Isar's `\verb|using| {\dots} \verb|by| \emph{auto}', we have actually
separated `\verb|by|' and `\verb|;|'.  However in Mizar these two parts are
not considered to have separate meanings (in fact `\verb|;|' is just a
syntactic terminator).

\medskip Despite the similarities between the two languages, we observe some
stylistic differences, stemming from different philosophies of language
design.  The Isar proof language is \emph{compositional}, it emerges in
\emph{bottom-up} fashion from only a few basic primitives following pure
principles of natural deduction --- according to the existing Isabelle
framework \cite{pau:89}.  In contrast, Mizar does not particularly try to
reduce everything to a few primitive language elements.

Without going into details, just consider the following examples:
\begin{enumerate}
  
\item Mizar's \verb|let| {\dots} \verb|such| \verb|that| is almost
  equivalent to a combination of \verb|let| and \verb|assume|, but not
  exactly.  In the first case one is not allowed to follow the step by a
  \verb|then|, while in the second case one is.  According to Isar's
  philosophy, the first really should be an abbreviation of the second,
  providing a more uniform language view \cite[\S5.3]{wen:02:thesis}.
  
\item Mizar has built-in automated justification of \verb|by|, while Isar uses
  explicit references to particular proof methods such as the automated
  \textit{simp}, \textit{blast}, \textit{auto}, or single-step \textit{rule}
  applications.  Therefore the combination `\textbf{by}~\textit{auto}' becomes a
  canonical automated justification, while `\textbf{by}~(\textit{rule}~\dots)'
  corresponds to rule scheme applications, which are treated separately in
  Mizar.

\end{enumerate}

\noindent Also note that the above table merely covers the `logical'
parts of the two languages.  Both Mizar and Isar also support a notion of
`algebraic reasoning', using chains of equalities (and inequalities in Isar).
See also \cite{bau:wen:01} for further discussion of this particular aspect of
structured proofs.


\section{A higher-level view: formal proof sketches}\label{sketch}

Formal proof sketches address the issue of presenting formal texts in a more
abstract manner, and support top-down development.

In this section we present
proof skeletons in the formal languages of Mizar and Isar
that are as close as possible to the informal natural language
proof on page \pageref{romantic}.
Also, in this section
we show the full files including the headers, instead of only showing
the final theorem.


\subsection{Mizar version of a formal proof sketch}

The Mizar system is able to continue to check a text after it finds the first
error.  A Mizar text that contains only justification errors, which can be
eliminated by adding more text, is in \cite{wie:02} called a \emph{formal proof
  sketch}.  Here is a formal proof sketch that corresponds to the Mizar
formalization in Section~\ref{example-mizar}.  It is the full text of the
formal proof sketch, including the `\verb|environ|' header.

\begin{quote}
\begin{verbatim}
environ
 vocabulary FINSET_1, FILTER_0, QC_LANG1, ARYTM_3;
 notation INT_2, FINSET_1, ARYTM, NAT_1, NAT_LAT;
 constructors NAT_1, NAT_LAT;
 clusters ARYTM, NAT_1;
 requirements SUBSET, ARYTM;
\end{verbatim}

\begin{verbatim}
begin
 reserve n,p for Nat;
\end{verbatim}

\begin{flushleft}
\verb|theorem ex p st p is prime & p > n|\\
\verb|proof|\\
\verb| set k = n! + 1;|\\
\verb| consider p such that|\\
\strut\llap{\texttt{*4} $\to\qquad$}\verb|  p is prime & p divides k;|\\
\verb| take p;|\\
\strut\llap{\texttt{*4} $\to\qquad$}\verb| thus p is prime;|\\
\verb| assume p <= n;|\\
\strut\llap{\texttt{*4} $\to\qquad$}\verb| p divides n!;|\\
\strut\llap{\texttt{*4} $\to\qquad$}\verb| p divides 1;|\\
\strut\llap{\texttt{*1} $\to\qquad$}\verb| thus contradiction;|\\
\verb|end;|
\end{flushleft}

\begin{flushleft}
\strut\llap{\texttt{*4} $\to\qquad$}\verb|theorem {p: p is prime} is infinite;|
\end{flushleft}
\end{quote}
%
Mizar gives six justification errors for this text.  These have been indicated
by arrows in the left margin.  The numbers in front of the arrows are the
error codes.  The explanation of error \verb|*1| is `\verb|It| \verb|is|
\verb|not| \verb|true|' and the explanation of error \verb|*4| is `\verb|This|
\verb|inference| \verb|is| \verb|not| \verb|accepted|'.  Those two errors are
the two justification errors of the Mizar system.


\subsection{Isar version of a formal proof sketch}

The Isar system stops checking after the first error that it finds.  However,
one can skip justification errors by inserting the `fake proof'
\textbf{sorry}.  Therefore, the Isar system also can be used to write and
check formal proof sketches.  Here is a formal proof sketch that corresponds
to the Isar formalization in Section~\ref{example-isar}.  The \textbf{sorry}
elements are pretty-printed as `$\langle\mathit{proof}\rangle$'.  This is the
full text of the formal proof sketch, including the `\textbf{theory} {\dots}
\textbf{end}' brackets.

\medskip
\begin{quote}
\begin{isabellebody}\normalsize
\isacommand{theory}\ Sketch\ {\isacharequal}\ Main\ {\isacharplus}\ Factorization{\isacharcolon}
\end{isabellebody}
\medskip

\begin{isabellebody}\normalsize
\isamarkupfalse%
\isacommand{consts}\ fact\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isacharbang}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
\isamarkupfalse%
\isacommand{primrec}\isanewline
\ \ {\isachardoublequote}{\isadigit{0}}{\isacharbang}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}{\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbang}\ {\isacharequal}\ n{\isacharbang}\ {\isacharasterisk}\ Suc\ n{\isachardoublequote}
\end{isabellebody}
\medskip

\begin{isabellebody}\normalsize
\isamarkupfalse%
\isacommand{theorem}\ {\isachardoublequote}{\isasymexists}p\ {\isasymin}\ prime{\isachardot}\ n\ {\isacharless}\ p{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{proof}\ {\isacharminus}\isanewline
\ \ \isamarkupfalse%
\isacommand{let}\ {\isacharquery}k\ {\isacharequal}\ {\isachardoublequote}n{\isacharbang}\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\isanewline
\ \ \isamarkupfalse%
\isacommand{obtain}\ p\ \isakeyword{where}\ {\isachardoublequote}p\ {\isasymin}\ prime{\isachardoublequote}\ \isakeyword{and}\ {\isachardoublequote}p\ dvd\ {\isacharquery}k{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
$\;\langle\mathit{proof}\rangle$\isanewline
\ \ \isamarkupfalse%
\isacommand{have}\ {\isachardoublequote}n\ {\isacharless}\ p{\isachardoublequote}\isanewline
\ \ \isamarkupfalse%
\isacommand{proof}\ {\isacharminus}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ p\ {\isasymle}\ n{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{proof}\isanewline
\ \ \ \ \ \ \isamarkupfalse%
\isacommand{assume}\ {\isachardoublequote}p\ {\isasymle}\ n{\isachardoublequote}\isanewline
\ \ \ \ \ \ \isamarkupfalse%
\isacommand{then}\ \isacommand{have}\ {\isachardoublequote}p\ dvd\ n{\isacharbang}{\isachardoublequote}\ \isamarkupfalse%
$\;\langle\mathit{proof}\rangle$\isanewline
\ \ \ \ \ \ \isamarkupfalse%
\isacommand{then}\ \isacommand{have}\ {\isachardoublequote}p\ dvd\ {\isadigit{1}}{\isachardoublequote}\ \isamarkupfalse%
$\;\langle\mathit{proof}\rangle$\isanewline
\ \ \ \ \ \ \isamarkupfalse%
\isacommand{then}\ \isacommand{show}\ False\ \isamarkupfalse%
$\;\langle\mathit{proof}\rangle$\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{qed}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{then}\ \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
$\;\langle\mathit{proof}\rangle$\isanewline
\ \ \isamarkupfalse%
\isacommand{qed}\isanewline
\ \ \isamarkupfalse%
\isacommand{then}\ \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
$\;\langle\mathit{proof}\rangle$\isanewline
\isamarkupfalse%
\isacommand{qed}
\end{isabellebody}
\medskip

\begin{isabellebody}\normalsize
\isamarkupfalse%
\isacommand{corollary}\ {\isachardoublequote}{\isasymnot}\ finite\ prime{\isachardoublequote}\ $\;\langle\mathit{proof}\rangle$
\end{isabellebody}
\medskip

\begin{isabellebody}\normalsize
\isamarkupfalse%
\isacommand{end}
\end{isabellebody}
\end{quote}


\section{The user experience: eighteen differences}\label{differences}

We will now list eighteen differences between the Mizar and Isar systems.  For
each of these differences we will state which system (in our opinion) is the
more attractive one.  In nine cases it will turn out to be the Mizar system,
and in nine cases it will turn out to be the Isar system.  But of course not
all differences are of the same importance.

\subsection{Better documentation: Isar}

The Isar system has much better documentation than the Mizar system.

For Mizar there are introductory texts, like \cite{muz:93}, but they are too
brief to be of real use, and they generally describe old versions of the
system.

The Isabelle/Isar documentation is clear and thorough.  There is a tutorial
for Isabelle/HOL \cite{nip:pau:wen:02} and there are reference manuals for
Isabelle \cite{pau:02:ref}, Isar \cite{wen:02:isar-ref} and for further logics
of the system, notably FOL and ZF \cite{pau:02:zf}.  All of these are
distributed with Isabelle (\url{http://isabelle.in.tum.de/dist/}).  The
tutorial for Isabelle/HOL is also available as a printed book from Springer.
Finally there is Wenzel's PhD thesis \cite{wen:02:thesis} that describes the
development of Isar in detail, including many practical proof patterns, as
well as some reference applications.  A dedicated Isabelle/Isar tutorial for
beginners is still missing.


\subsection{Available on more platforms: Isar}

The Isar system is available on more different kinds of platforms than the
Mizar system.

The Mizar system is written in Borland Delphi Pascal and has been ported to
Free Pascal.  Those compilers cannot generate code for many machines.
Therefore, the Mizar system is only available on Intel systems (both Windows
and Linux).  Some old DOS legacy is still visible, e.g.\ the limitation of
Mizar article names to 8 characters.  The binaries of the Mizar system
can be freely downloaded on the Internet.  The source of the Mizar system is
only available to members of the Association of Mizar Users.

The Isar system is written in standard ML.  The Isabelle2002 system can be run
on all major Unix platforms, including Intel, Sun and Apple.  The binaries and
source of the Isabelle system can be freely downloaded on the Internet.


\subsection{More users: Mizar}

The Mizar language has more serious users than the Isar language.

It is easy to determine who are the serious Mizar users.  Those are exactly
the people who have contributed an `article' to the Mizar Mathematical
Library.  In the Mizar community these are called `Mizar authors'.  A Mizar
article is a significant piece of Mizar text.  To write a Mizar article one
needs to understand the Mizar language thoroughly:
even authors who are not active anymore can still be considered to be
Mizar experts.
Currently there are more than 120 Mizar authors.

The Isar proof language is now the official input language of the Isabelle
system.  However, most Isabelle users only use the `improper commands'
\textbf{apply} and \textbf{done} of the Isar language, effectively writing an
`old style' tactic proof encapsulated in a thin Isar wrapping.  Presently only
few people write `new style' Isar proofs, although some substantial
applications are distributed with Isabelle2002, such as the Hahn-Banach
Theorem for real vector spaces \cite{bau:wen:00}.


\subsection{Bigger mathematical library: Mizar}

The Mizar system has a bigger library than the Isabelle/Isar system.

It is difficult to measure the size of a formal library in an objective way.
However, even from the small example from Section~\ref{example} it is clear
that the Mizar system has more background theory available than the Isabelle
system, as far as classical mathematics is concerned.

For the Mizar proof above, only one lemma needed to be proved, while for the
Isar proof five lemmas were needed.  Also the Mizar library already has the
definition of the factorial function, while the Isabelle library
does not have it as a standard function.  Finally, for the example the Mizar
library was sufficient, while the Isar library needed to be supplemented by a
theory about factorization.

The size of the Mizar library is about 50 megabytes, while that of Isabelle is
about 10 megabytes (including the sources of the system and the example
theories).


\subsection{Better library lookup: Isar}

The Isar system has better support for finding theorems in the library than
the Mizar system.

The main difficulty when writing mathematical formalizations is finding the
relevant theorems in the library.  For the Mizar system most people use the
\verb|grep| program for this.  There are more specific tools, like Grzegorz
Bancerek's MML Query (\url{http://megrez.mizar.org/mmlquery/}), but they are not easy to
understand and they are not integrated into the official Mizar system.

The Isabelle/Isar system, being interactive, provides a `live' view of the
current theory context.  Its
\textbf{thms}{\isacharunderscore}\textbf{containing} command finds theorems in
the library: for example,
\textbf{thms}{\isacharunderscore}\textbf{containing}~$x < y$~~$x \le y$
retrieves all facts involving the $<$ and $\le$ relations. This is a much more
structured way to look for theorems than the \verb|grep| program.


\subsection{Shorter formalizations: Mizar}

The Mizar language gives slightly shorter formalizations than the Isar language.
(This is the least objective of the choices in this list.)

Basically the Mizar and Isar languages are very similar and will lead to
proofs that have similar length.  However, when looking at the examples from
Sections~\ref{example} and \ref{sketch}, the Mizar proofs seem a bit more
terse.  For instance the Isar justification `\textbf{using}
\emph{prime{\isacharunderscore}factor{\isacharunderscore}exists} \textbf{by}
\emph{auto}' is longer than the Mizar justification `\verb|by|
\verb|INT_2:48;|'.  Also the Isar formalization from
Section~\ref{example-isar} has more than twice as many lines as the Mizar
formalization.

There are two effects causing a difference in size between Mizar and Isar
formalizations.  These two effects counteract each other.  In the Mizar
library much more has been proved already, leading to shorter Mizar
formalizations.  But the standard Isabelle/Isar proof methods are more
powerful than Mizar justifications (see \ref{tactics} below) leading to
shorter Isar formalizations.


\subsection{Simpler proof state: Mizar}

The Mizar system has a much simpler proof state than the Isar system.

The Isar system divides the proof state in a `static' and a `dynamic' context,
and it also contains a set of `using this' facts to move information from the
static to the dynamic world.  However, in the way that the Isar proof state is
used, the static and dynamic contexts are duplicates of each other.  To prove
a subgoal one has to build a copy of the corresponding part of the dynamic
context in the static context.  Then when giving the \textbf{show} command the
system verifies whether both contexts are compatible.  If this turns out not to
be the case, then the user gets an error message and has to search for himself
which of the preceding \textbf{assume} lines caused the incompatibility.  The
duplication of contexts does not give fundamental advantages concerning basic
goal refinement steps, but provides a slightly more `declarative' view.

In Mizar there is only a single context, which is closer to the traditional
goal-oriented concept of stepwise problem refinement.


\subsection{Simpler module system: Isar}

The Isabelle/Isar system has a much simpler module system than the Mizar
system.

In the Mizar system one has to give an `\verb|environ|' header that specifies
the articles from the library that are going to be used.  For each of the
various notions that an article exports (notation, definitions, theorems,
etc.), the \verb|environ| contains a separate import list.  Generally those
lists contain more or less the same articles.  Also, the Mizar \verb|environ|
refers to \emph{two} kinds of modules, the articles and the vocabularies.
Both use different name spaces.  In practice it turns out to be difficult to
get a Mizar \verb|environ| right.

In the Isar system one just gives a single list of theories to be imported.
Also the import of theories is transitive.  This gives a much simpler module
system.


\subsection{More powerful justifications: Isar}\label{tactics}

The Isar system has more powerful justifications than the Mizar system.

In Mizar there are only two justification methods: the \verb|by|
justification and the \verb|from| justification.  Both methods have been
hard-wired into the system, and have intentionally been kept simple.
Therefore they can be checked in a fast way and have a relatively clear
semantics.

In Isar there are many justification methods, and a user can add justification
methods of his own to the system.  The most common ones are \emph{rule},
\emph{simp}, \emph{blast}, \emph{auto} and \emph{arith}.  These proof tools
are generally more powerful than the Mizar justification methods.  This
explains why the `algebraic facts' (\verb|n!| \verb|>=| \verb|1|, \verb|k|
\verb|>=| \verb|2|, \verb|p| \verb|<>| \verb|0|, \verb|p| \verb|>| \verb|1|)
from the Mizar proof do not need to be stated explicitly in the Isar proof.


\subsection{Simpler justifications: Mizar}

Mizar justifications are easier to work with than the Isar justifications.

The Mizar justifications only use \verb|by| (light-weight automated reasoning)
or \verb|from| (single rule scheme application).  That means that if a certain
justification does not work, then there is nothing to be done on the
justification level.  This actually makes writing proofs easier, since one
focuses on the steps in the proof and not on internal details.

In Isar there are two ways to write proofs: the old way of `unstructured
scripts' and the new way of `structured texts'.  The old way consists of
applying tactics to the goal, using sequences of the \textbf{apply} command
followed by the \textbf{done} command.  The new way consists of writing
Mizar-style proofs.  But in fact when writing proofs in the new way, one still
generally discovers the justifications in the old way, before turning the
(local) tactic proof that one discovered into a single \textbf{by}
justification.  In development one still uses the \textbf{apply} command,
although this does not show in the final proof text.  This means a lot of
experimentation with various tactics and their parameters, focusing on the
machinery of the justifications and not on the mathematics of the proof.
Because of the diversity of Isar justifications, users are tempted to spend
considerable effort into tweaking the final text!


\subsection{Easier to work with incomplete text: Mizar}

Mizar can deal better with incomplete text than the Isar system.

The Mizar system will keep checking a text no matter what errors it encounters
(as long as the `\verb|environ|' header is correct, but that is a different
matter).  It will recover from syntax errors, type errors, missing
definitions, justification errors.  This means that if one is in the middle of
a complicated proof (even one that is not syntactically correct yet),
one can switch to a different part of the file \emph{after} that complicated
proof, and continue to do useful work there.

For instance, consider the following fragment of a Mizar text, in which the
proof of the scheme has not yet been finished:
\smallskip
\begin{quote}
\begin{verbatim}
scheme Unbounded {P[Nat]}: {n: P[n]} is infinite
 provided
A1: for m ex n st P[n] & n > m
proof
::> *214
 now let m;
::>*214
  consider n' such that
A2: P[n'] & n' > m by A1;
  take n';
::>       *215,215
\end{verbatim}
\end{quote}
\begin{quote}
\begin{verbatim}
theorem Euclid: ex p st p is prime & p > n
::>   *70
proof
 set k = n! + 1;
 n! > 0 by NEWTON:23;
\end{verbatim}
\vspace{-\smallskipamount}
\emph{etcetera}
\end{quote}
\begin{quote}
\begin{verbatim}
::> 70: Something remains to be proved
::> 214: "end" missing
::> 215: No pairing "end" for this word
\end{verbatim}
\end{quote}
\smallskip
All errors in this example are
related to the fact that the scheme \texttt{Unbounded} is not finished.
The remaining text is checked as expected.

The Isar system cannot do anything like this.  One can skip missing
justifications with the \textbf{sorry} command.  For all other errors, one
needs to change the text (for instance by putting it in comment brackets) to
make it correct, before being able to work on text after the error.  This is
less convenient than the way Mizar treats errors.  Here we experience a
disadvantage of Isar's incremental approach vs.\ Mizar's batch-mode.


\subsection{More feedback from the system: Isar}

The Isar system gives more feedback to the user than the Mizar system.

The Mizar system will only give natural numbers to the user: error codes and
the positions in the file to which these codes apply.  For instance, the
errors in the formal proof sketch from Section \ref{sketch} correspond to the
18 natural numbers:
\begin{center}
\begin{supertabular}{ccc}
16 & 26 & \ 4 \\
18 & 16 & \ 4 \\
20 & 13 & \ 4 \\
21 & 12 & \ 4 \\
22 & 19 & \ 1 \\
25 & 35 & \ 4 \\
\end{supertabular}
\end{center}
(The meaning of these is: line numbers, offsets into the line, and error
codes.)  In practice it is often not very convenient just to be told codes,
because with more specific information the errors would be easier to
understand.  In particular it would be good to know what the \verb|thesis| is
at specific points in the text (in other systems called the `goal').

The Isar system is a full-fledged interactive tactic-based prover.  It is able
to print a large amount of information at any point in the text, including the
goal that has to be proved.  For instance, just before the `\textbf{with}
\textit{prime} \textbf{show} \textit{False}' line in the example of
Section~\ref{example-isar}, the proof state of the Isar system looks like
this: \smallskip
\begin{quote}\small
\begin{verbatim}
proof (state): step 19
\end{verbatim}
\end{quote}
\begin{quote}
\begin{flushleft}
\verb|fixed variables: n, p = p|\\
\verb|prems:|\\
\verb|  p |$\in$\verb| prime|\\
\verb|  p dvd n! + 1|\\
\verb|  p |$\le$\verb| n|
\end{flushleft}
\end{quote}
\begin{quote}
\begin{verbatim}
this:
  p dvd 1
\end{verbatim}
\end{quote}
\begin{quote}
\begin{flushleft}
\verb|goal (have, 1 subgoal):|\\
$\neg$\verb| p |$\le$\verb| n|\\
\verb| 1. p |$\le$\verb| n |$\Longrightarrow$\verb| False|
\end{flushleft}
\end{quote}


\subsection{Logically more general: Isar}

The Isar language can represent proofs of many different logics, unlike the
Mizar language which only can represent proofs of classical
first order predicate logic.

The proof steps of the Mizar language are the natural deduction steps of first
order predicate logic, including built-in classical principles.

Isabelle is a \emph{logical framework} where the logic can be chosen by the
user.  The Isar language works on the generic level of the meta-logic, and is
compatible with common object-logics (e.g.\ HOL, HOLCF, FOL, ZF).  For
instance, the \textbf{obtain} element (which corresponds to Mizar's
\verb|consider|) directly refers to Isabelle's meta-logic, bypassing any
particular notion of existential quantifier in the object-logic.


\subsection{More mathematical type system: Mizar}

The Mizar type system is much richer and much more mathematical than the type
system that Isar inherits from Isabelle.

Mizar has structure types, dependent types, various kinds of sub-typing and
type modifiers called \emph{attributes}.  Mizar uses the types for automatic
deduction and for overloading of predicates and operators.

Isar uses the HOL type system.  In particular it does not have dependent
types.  Dependent types are very important to be able to model mathematical
practice in a natural way, but prevent conveniences like Hindley-Milner
type inference.


\subsection{Simpler type system: Isar}

Isar types are easier than Mizar types.

The Mizar type system is difficult to use.  Regularly one needs `clusters' or
`redefinitions' in the environment to get the typing of expressions right.
Finding these clusters and redefinitions in the Mizar library takes a
significant amount of time.

The Isabelle types are much simpler than the Mizar types, and rarely cause
problems for the user.  Occasionally Isabelle's type inference can lead to
confusion when the inferred types turn out to be more general than has been
anticipated by the user.


\subsection{Better support for mathematical symbols: Isar}

Isar offers the use of mathematical symbols while Mizar does not.

Until recently Mizar articles contained symbols from the high ASCII part of
the DOS character set.  These symbols have been eliminated from the Mizar
library and currently Mizar articles only use standard ASCII characters.

Isar formalizations contain many mathematical symbols.  Using the Emacs +
Proof General combination these can be displayed on screen by the X-Symbol
package (\url{http://x-symbol.sourceforge.net/}).  In the final pretty-printed
document, these symbols are printed using the {\LaTeX} typesetting system.  In
the Isar files symbols are represented using special escape sequences.  For
instance the statement of the theorem from Section~\ref{example} is
represented in the ASCII file as:

\begin{quote}
\begin{verbatim}
theorem Euclid: "\<exists>p \<in> prime. n < p"
\end{verbatim}
\end{quote}


\subsection{Less meaningless typographic noise: Mizar}

Mizar texts contain less mathematically meaningless symbols than Isar texts.

In Isar formalizations there are some low-level `noise' characters that do not
mean anything mathematically.  There are quotes (\verb|"|) around formulas
(they are not shown in the pretty-printed version of Isar but are seen in the
input and need to be typed), there are question marks (\emph{?}) for term
bindings, there are minuses ($-$) and dots (\textbf{.} and \textbf{..}).


\subsection{More natural language-like: Mizar}

Mizar texts resemble natural language more than Isar texts.

In Mizar both the proof steps and the formulas use English keywords.  In Isar
the formulas are written with symbols.  This causes Mizar texts to be closer
to mathematical English.  For instance, in Mizar one might write:
\smallskip
\begin{quote}
\verb|assume that for n being natural number such that| \dots
\end{quote}
\smallskip\noindent
while in Isar this would look more symbolic:
\medskip
\begin{quote}
\begin{isabellebody}\normalsize
\isamarkupfalse%
\isakeyword{assume}\ {\isachardoublequote}{\isasymforall}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ \dots
\end{isabellebody}
\end{quote}
\smallskip\noindent The ratio of verbal expressions versus formulas is a
matter of taste.  Traditional mathematics used to be mostly verbal for several
hundred years, even for expressions like `$a = b + c$'.


\section{Internal mechanisms: key differences of proof processing}\label{internals}

We shall now take a closer look at the internal machinery of both systems, in
order to gain some understanding of the basic principles underlying structured
proof processing encountered here.  Mizar and Isar differ considerably inside,
despite the similar high-level view of final proof texts shown to the
recipients.

Roughly speaking, Mizar is based on \emph{procedural transformations} of a
pending proof problem, with primitive elements stemming from classical
first-order logic.  In contrast, the most fundamental Isar operations are
\emph{applicative refinements} of pending problems according to the built-in
principle of higher-order resolution (and unification) of the Isabelle/Pure
framework.

Subsequently, the fact $(\exists x.\, \forall y.\, P\, x\, y) \longrightarrow
(\forall v.\, \exists u.\, P\, u\, v)$ shall serve as an example.  This is
sufficiently characteristic for quantifier reasoning, since both introductions
and eliminations of $\forall$ and $\exists$ are involved.


\subsection{Mizar}\label{sec:internals-mizar}

Technically, a Mizar proof consists of a claim at the head (theorem or local
statement etc.), together with a body consisting of several transformations of
the remaining problem.
Within the body, the special proposition
\verb,thesis, is updated dynamically to reflect the pending goal; at the same
time a context of local variables and facts is being built up.  In the example
below we indicate the course of value of \texttt{thesis}.

\begin{flushleft}
\verb|theorem (ex x st for y holds P[x,y]) implies|\\
\verb|  (for v holds ex u st P[u,v])|\\
\verb|proof|\\
\verb| assume ex x st for y holds P[x,y];|\\
\verb|  :: |thesis = \verb|for v holds ex u st P[u,v]|\\
\verb| then consider x such that A: for y holds P[x,y];|\\
\verb|  :: |thesis unchanged\\
\verb| let v;|\\
\verb|  :: |thesis = \verb|ex u st P[u,v]|\\
\verb| take x;|\\
\verb|  :: |thesis = \verb|P[x,v]|\\
\verb| thus P[x,v] by A;|\\
\verb|  :: |thesis = empty conjunction\\
\verb|end;|
\end{flushleft}

\noindent
(The combination \texttt{assume} \texttt{ex} \texttt{x} \texttt{st} {\dots} \texttt{then} \texttt{consider} \texttt{x} \texttt{such} \texttt{that} {\dots} can be
abbreviated as \texttt{given} \texttt{x} \texttt{such} \texttt{that} {\dots}
but for clarity we have not done this.)
Mizar proof body elements may be understood as standard transformations
according to well-known principles of natural deduction.  This simplified
model of Mizar's approach to structured proof processing has been elaborated
further in \cite{wie:00:2}.  Nevertheless, Mizar's built-in procedure actually
admits slightly more involved transformations, based on a theory of so-called
`semantic correlates', which provides a certain algebraic view on top of
classical first-order logic.

For example, $\alpha$-conversion of bound variables works as expected (above
we have sticked to the original names $x$, $y$, $u$, $v$ nevertheless).
Moreover, conjunctions may be considered as split, both in assumptions and
conclusions (so \verb|assume| \verb|A| \verb|&| \verb|B| is the same as \verb|assume| \verb|A| followed by
\verb|assume| \verb|B|, which is the same as \verb|assume| \verb|A| \verb|and| \verb|B|).  Further
equivalences allow to swap a final \verb|thus| \verb|not| \verb|A| with the combination \verb|assume| \verb|A| {\dots} \verb|thus| \verb|contradiction|.

Unfortunately, Mizar's semantic correlates do not cover commutativity, so the
order of basic transformations in the above proof is essentially dictated by
that of the initial statement.  The arrangement in the body may not just swap
assumptions or skip unused ones.  In practice, one would often wish to change
the order that local facts emerge, arriving at a mostly linear chain that
reflects the course of reasoning in the body, rather than the original goal
statement.  Failing to do so, one typically requires additional labels and
references, which are apt to spoil the structure of Mizar texts.


\subsection{Isar}\label{sec:internals-isar}

In Isar a proven fact consists of a claim at the head (similar to Mizar),
followed by a \emph{proof} according to Isar's formal syntax.  In general this
consists of an initial \textbf{proof} step (with optional \emph{method}
specification), followed by a sequence of body \emph{statements}, followed by
a terminal \textbf{qed} step (again with optional \emph{method}).  Isar's
\textbf{by} (with one or two $method$ arguments) merely abbreviates a proof
with an empty body.

The initial and terminal methods are the only places where arbitrary
operational transformations of the pending problem may take place, say an
initial induction followed by a terminal method to solve any remaining
sub-problems automatically.  Within the body text, the only way to affect the
pending goal configuration is via explicit \textbf{show} statements.  This
format is again illustrated by our example of quantifier reasoning.

\medskip
\begin{isabellebody}\normalsize
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}v{\isachardot}\ {\isasymexists}u{\isachardot}\ P\ u\ v{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{proof}\isanewline
\ \ \ \ %
\isamarkupcmt{rule \isa{{\isachardoublequote}{\isacharparenleft}{\isasymAnd}v{\isachardot}\ {\isasymexists}u{\isachardot}\ P\ u\ v{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}v{\isachardot}\ {\isasymexists}u{\isachardot}\ P\ u\ v{\isacharparenright}{\isachardoublequote}}%
}
\isanewline
\ \ \isamarkupfalse%
\isacommand{fix}\ v\isanewline
\ \ \isamarkupfalse%
\isacommand{assume}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\isanewline
\ \ \isamarkupfalse%
\isacommand{then}\ \isamarkupfalse%
\isacommand{obtain}\ u\ \isakeyword{where}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ P\ u\ y{\isachardoublequote}\ \isamarkupfalse%
\isacommand{{\isachardot}{\isachardot}}\isanewline
\ \ \ \ %
\isamarkupcmt{rule \isa{{\isachardoublequote}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}u{\isachardot}\ {\isacharparenleft}{\isasymforall}y{\isachardot}\ P\ u\ y{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequote}}%
}
\isanewline
\ \ \isamarkupfalse%
\isacommand{then}\ \isamarkupfalse%
\isacommand{have}\ {\isachardoublequote}P\ u\ v{\isachardoublequote}\ \isamarkupfalse%
\isacommand{{\isachardot}{\isachardot}}\isanewline
\ \ \ \ %
\isamarkupcmt{rule \isa{{\isachardoublequote}{\isacharparenleft}{\isasymforall}y{\isachardot}\ P\ u\ y{\isacharparenright}\ {\isasymLongrightarrow}\ P\ u\ v{\isachardoublequote}}%
}
\isanewline
\ \ \isamarkupfalse%
\isacommand{then}\ \isamarkupfalse%
\isacommand{show}\ {\isachardoublequote}{\isasymexists}u{\isachardot}\ P\ u\ v{\isachardoublequote}\ \isamarkupfalse%
\isacommand{{\isachardot}{\isachardot}}\isanewline
\ \ \ \ %
\isamarkupcmt{rule \isa{{\isachardoublequote}P\ u\ v\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymexists}u{\isachardot}\ P\ u\ v{\isacharparenright}{\isachardoublequote}}%
}
\isanewline
\ \ \ \ %
\isamarkupcmt{composition \isa{{\isachardoublequote}{\isasymAnd}v{\isachardot}\ {\isacharparenleft}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymexists}u{\isachardot}\ P\ u\ v{\isacharparenright}{\isachardoublequote}}%
}
\isanewline
\isamarkupfalse%
\isacommand{qed}\isamarkupfalse%
\end{isabellebody}

\medskip\noindent
The notation used for rule statements is that of the Isabelle/Pure
framework \cite{pau:89}: $\bigwedge$ and $\Longrightarrow$ refer to meta-level
universal quantification and implication, respectively.  Both goal states and
inference rules are represented as `Hereditary Harrop Formulae' built from
these connectives; the general form may be specified inductively as $H =
\bigwedge x_1 \dots x_m.\, H_1 \Longrightarrow \dots H_n \Longrightarrow A$,
for atomic propositions $A$.  This is a natural generalization of Horn clauses
$A_1 \Longrightarrow \dots A_n \Longrightarrow A$.  The internal Isabelle
machinery uses a generalization of Prolog-style backwards resolution as the
most basic reasoning principle.

The implicit rule applications indicated in the above example are easily
recognized as instances of $\forall$ introduction, $\exists$ elimination,
$\forall$ elimination, and $\exists$ introduction, respectively.  The final
composition step fits the result of the \textbf{show} into the enclosing goal;
the local context of \textbf{fix}-\textbf{assume} has already been discharged
in the obvious manner.

The key idea underlying the Isar interpretation process is to provide a
structured discipline to drive standard inferences of the underlying
Isabelle/Pure framework (arbitrary automated proof tools may enter the scene
much later).  As it happens, the Isabelle kernel is able to record the
resulting course of internal inferences as \emph{proof-objects} in canonical
$\lambda$-term representation \cite{ber:00}.  For our proof this looks as
follows:

\medskip
\begin{isabellebody}\normalsize\def\isacharquery{}
\ \ \isactrlbold {\isasymlambda}H{\isacharcolon}\ {\isasymexists}x{\isachardot}\ {\isasymforall}xa{\isachardot}\ {\isacharquery}P\ x\ xa{\isachardot}\isanewline
\isaindent{\ \ \ }allI\ {\isasymcdot}\ TYPE{\isacharparenleft}{\isacharquery}{\isacharprime}b{\isacharparenright}\ {\isasymcdot}\ {\isacharparenleft}{\isasymlambda}v{\isachardot}\ {\isasymexists}x{\isachardot}\ {\isacharquery}P\ x\ v{\isacharparenright}\ {\isasymbullet}\isanewline
\isaindent{\ \ \ \ }{\isacharparenleft}\isactrlbold {\isasymlambda}v{\isachardot}\ exE\ {\isasymcdot}\ TYPE{\isacharparenleft}{\isacharquery}{\isacharprime}a{\isacharparenright}\ {\isasymcdot}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ {\isasymforall}xa{\isachardot}\ {\isacharquery}P\ x\ xa{\isacharparenright}\ {\isasymcdot}\ {\isasymexists}x{\isachardot}\ {\isacharquery}P\ x\ v\ {\isasymbullet}\ H\ {\isasymbullet}\isanewline
\isaindent{\ \ \ \ {\isacharparenleft}\isactrlbold {\isasymlambda}v{\isachardot}\ \ }{\isacharparenleft}\isactrlbold {\isasymlambda}u\ H{\isacharcolon}\ {\isasymforall}x{\isachardot}\ {\isacharquery}P\ u\ x{\isachardot}\isanewline
\isaindent{\ \ \ \ {\isacharparenleft}\isactrlbold {\isasymlambda}v{\isachardot}\ \ {\isacharparenleft}\ }exI\ {\isasymcdot}\ TYPE{\isacharparenleft}{\isacharquery}{\isacharprime}a{\isacharparenright}\ {\isasymcdot}\ {\isacharparenleft}{\isasymlambda}u{\isachardot}\ {\isacharquery}P\ u\ v{\isacharparenright}\ {\isasymcdot}\ u\ {\isasymbullet}\isanewline
\isaindent{\ \ \ \ {\isacharparenleft}\isactrlbold {\isasymlambda}v{\isachardot}\ \ {\isacharparenleft}\ \ }{\isacharparenleft}allE\ {\isasymcdot}\ TYPE{\isacharparenleft}{\isacharquery}{\isacharprime}b{\isacharparenright}\ {\isasymcdot}\ {\isacharquery}P\ u\ {\isasymcdot}\ v\ {\isasymcdot}\ {\isacharquery}P\ u\ v\ {\isasymbullet}\ H\ {\isasymbullet}\ {\isacharparenleft}\isactrlbold {\isasymlambda}H{\isacharcolon}\ {\isacharquery}P\ u\ v{\isachardot}\ H{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}%
\end{isabellebody}

\medskip\noindent
Thus Isabelle/Isar is able to cover both human-readable and
foundationally clean representations of formal proofs.  Observe how the latter
has lost much `redundant' structure of the original text (due to internal
$\beta$-normalization.

\medskip Similar to Mizar, Isar proof processing involves a number of
liberalities in the arrangement of proof body elements, but is biased towards
the generic concepts of the Isabelle/Pure framework rather than classical
principles.  These proof text equivalences directly correspond to basic facts
of the meta-logic, including $\alpha$-conversion of parameters $(\bigwedge
x.\, P\, x) \equiv (\bigwedge y.\, P\, y)$, permutation of parameters
$(\bigwedge x\,y.\, P\,x\,y) \equiv (\bigwedge y\,x.\, P\,x\,y)$ and
assumptions $(A \Longrightarrow B \Longrightarrow C) \equiv (B \Longrightarrow
A \Longrightarrow C)$, commutation of parameters and assumptions $(A
\Longrightarrow (\bigwedge x.\, B\, x)) \equiv (\bigwedge x.\, A
\Longrightarrow B\, x)$.  Moreover, the composition phase of fitting the
result of \textbf{fix}-\textbf{assume}-\textbf{show} back into a goal admits
projection of the context, i.e.\ the body may have omitted unused assumptions.
Sub-goals may usually be solved in any order, too.

In practice, Isar proof texts require much less labeling of intermediate facts
than Mizar.

\medskip Generally speaking, the proof composition scheme of Isar is somewhat
more `generic' and `declarative' than Mizar.  On the other hand, Isar is
reluctant to let the user operate directly on pending problems, resulting in
slower progress of consecutive transformations.  Here Isar typically requires
additional local statements (with separate sub-proofs).  This has only been
avoided in the above example, since we have used $\Longrightarrow$ of the
meta-logic at the outermost level (conforming to common Isabelle practice);
using $\longrightarrow$ of the object-logic would have demanded an additional
\textbf{assume}-\textbf{show} layer in the beginning, to accommodate
implication introduction.


\section{Conclusion}

We have compared the proof languages of the Mizar and Isar systems, listing
various properties of those systems, and showing their relative strong points.
By presenting a small but realistic mathematical example in both systems side
by side, we hope to have escaped the common delusions of artificial `benchmark
problems'.  Our formalizations of Euclid's proof of the existence of
infinitely many primes is intended to represent quite typical applications of
either proof system.

The system evaluation shows that both Mizar and Isar provide a solid
environment for formalized mathematics.  Despite the rather different
background and design philosophies, the end user experience is quite similar
in general.  Recall that only the differences have been pointed out
explicitly.

Mizar provides proven technology for formalizing classical mathematics, with a
huge body of `articles' being collected over the last 10 to 20 years.  Isar
takes the existing Isabelle framework as a starting point to achieve a generic
environment for human-readable proof documents, where classical mathematics is
just one potential application domain.

Certainly, both systems have their inherent advantages and disadvantages.
Speaking in terms of the system itself, the best choice for users is probably
a matter of taste.  In reality, the availability of existing background theory
and proof tools is probably more important.

\medskip Concerning future work, it would be interesting to study how much of
the advantages of Mizar can be added to Isar, and vice versa.  The present
paper may serve as a guideline for any such efforts towards better acceptance
of formalized mathematics in broader circles, by providing convincing computer
assistance.

%\bibliographystyle{klunamed}
%\bibliography{bib}

\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Abel et~al.}{2001}]{abe:01}
Abel, A., B.-Y.~E. Chang, and F. Pfenning: 2001, `Human-Readable
  Machine-Verifiable Proofs for Teaching Constructive Logic'.
\newblock IJCAR Workshop on Proof Transformations, Proof Presentations and
  Complexity of Proofs (PTP-01),
  \url{http://www.tcs.informatik.uni-muenchen.de/~abel/ptp01.ps.gz}.

\bibitem[\protect\citeauthoryear{Aspinall}{2000}]{asp:00}
Aspinall, D.: 2000, `Proof {G}eneral: A Generic Tool for Proof Development'.
\newblock In: {\em European Joint Conferences on Theory and Practice of
  Software (ETAPS)}.

\bibitem[\protect\citeauthoryear{Bauer and Wenzel}{2000}]{bau:wen:00}
Bauer, G. and M. Wenzel: 2000, `Computer-Assisted Mathematics at Work --- The
  {H}ahn-{B}anach Theorem in {I}sabelle/{I}sar'.
\newblock In: T. Coquand, P. Dybjer, B. Nordstr\"om, and J. Smith (eds.): {\em
  Types for Proofs and Programs: TYPES'99}, Vol. 1956 of {\em LNCS}.

\bibitem[\protect\citeauthoryear{Bauer and Wenzel}{2001}]{bau:wen:01}
Bauer, G. and M. Wenzel: 2001, `Calculational reasoning revisited --- an
  {Isabelle/Isar} experience'.
\newblock In: R.~J. Boulton and P.~B. Jackson (eds.): {\em Theorem Proving in
  Higher Order Logics: {TPHOLs} 2001}, Vol. 2152 of {\em LNCS}.

\bibitem[\protect\citeauthoryear{Berghofer and Nipkow}{2000}]{ber:00}
Berghofer, S. and T. Nipkow: 2000, `Proof terms for simply typed higher order
  logic'.
\newblock In: J. Harrison and M. Aagaard (eds.): {\em Theorem Proving in Higher
  Order Logics: {TPHOLs} 2000}, Vol. 1869 of {\em LNCS}.

\bibitem[\protect\citeauthoryear{Burstall}{1998}]{bur:98}
Burstall, R.: 1998, `Teaching people to write Proofs: a Tool'.
\newblock In: {\em CafeOBJ Symposium, Numazu, Japan}.

\bibitem[\protect\citeauthoryear{de~Bruijn}{1987}]{bru:87}
de~Bruijn, N.: 1987, `{The Mathematical Vernacular, a language for mathematics
  with typed sets}'.
\newblock In: P. Dybjer et~al. (eds.): {\em Proceedings of the Workshop on
  Programming Languages}. Marstrand, Sweden.

\bibitem[\protect\citeauthoryear{Harrison}{1996}]{har:96}
Harrison, J.: 1996, `{A Mizar Mode for HOL}'.
\newblock In: {\em Proceedings of the 9th International Conference on Theorem
  Proving in Higher Order Logics, TPHOLs '96}, Vol. 1125 of {\em LNCS}.
  Springer.

\bibitem[\protect\citeauthoryear{Muzalewski}{1993}]{muz:93}
Muzalewski, M.: 1993, {\em An Outline of PC Mizar}.
\newblock Brussels: Fondation Philippe le Hodey.
\newblock \url{http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz}.

\bibitem[\protect\citeauthoryear{Nipkow et~al.}{2002}]{nip:pau:wen:02}
Nipkow, T., L. Paulson, and M. Wenzel: 2002, {\em Isabelle/HOL --- A Proof
  Assistant for Higher-Order Logic}, Vol. 2283 of {\em LNCS}.
\newblock Springer.

\bibitem[\protect\citeauthoryear{Paulson}{1994}]{pau:94}
Paulson, L.: 1994, {\em Isabelle: a generic theorem prover}, Vol. 828 of {\em
  LNCS}.
\newblock Springer.

\bibitem[\protect\citeauthoryear{Paulson}{2002a}]{pau:02:ref}
Paulson, L.: 2002a, `The Isabelle Reference Manual'.
\newblock \url{http://isabelle.in.tum.de/doc/ref.pdf}.

\bibitem[\protect\citeauthoryear{Paulson}{1989}]{pau:89}
Paulson, L.~C.: 1989, `The foundation of a generic Theorem Prover'.
\newblock {\em Journal of Automated Reasoning} {\bf 5}(3).

\bibitem[\protect\citeauthoryear{Paulson}{2002b}]{pau:02:zf}
Paulson, L.~C.: 2002b, `{Isabelle}'s Logics: {FOL} and {ZF}'.
\newblock \url{http://isabelle.in.tum.de/doc/logics-ZF.pdf}.

\bibitem[\protect\citeauthoryear{Rudnicki}{1992}]{rud:92}
Rudnicki, P.: 1992, `An Overview of the {MIZAR} Project'.
\newblock In: {\em 1992 Workshop on Types for Proofs and Programs}. Bastad.

\bibitem[\protect\citeauthoryear{Syme}{1997}]{sym:97}
Syme, D.: 1997, `{DECLARE}: A Prototype Declarative Proof System for Higher
  Order Logic'.
\newblock Technical Report 416, University of Cambridge Computer Laboratory.

\bibitem[\protect\citeauthoryear{Syme}{1998}]{sym:98}
Syme, D.: 1998, `Declarative Theorem Proving for Operational Semantics'.
\newblock Ph.D. thesis, University of Cambridge.

\bibitem[\protect\citeauthoryear{Syme}{1999}]{sym:99}
Syme, D.: 1999, `{Three Tactic Theorem Proving}'.
\newblock In: {\em Theorem Proving in Higher Order Logics, TPHOLs '99, Nice,
  France}, Vol. 1690 of {\em LNCS}. Springer.

\bibitem[\protect\citeauthoryear{Trybulec}{1993}]{try:93}
Trybulec, A.: 1993, `Some Features of the {Mizar} Language'.
\newblock Presented at a workshop in Turin, Italy.

\bibitem[\protect\citeauthoryear{Wenzel}{1999}]{wen:99}
Wenzel, M.: 1999, `{Isar} --- a Generic Interpretative Approach to Readable
  Formal Proof Documents'.
\newblock In: Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery
  (eds.): {\em Theorem Proving in Higher Order Logics: {TPHOLs} '99}, Vol. 1690
  of {\em LNCS}.

\bibitem[\protect\citeauthoryear{Wenzel}{2002a}]{wen:02:thesis}
Wenzel, M.: 2002a, `{Isabelle/Isar --- a versatile environment for
  human-readable formal proof documents}'.
\newblock Ph.D. thesis, {Institut f\"ur Informatik, Technische Universit\"at
  M\"unchen}.
\newblock
  \url{http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html}.

\bibitem[\protect\citeauthoryear{Wenzel}{2002b}]{wen:02:isar-ref}
Wenzel, M.: 2002b, {\em The Isabelle/Isar Reference Manual}.
\newblock TU M{\"u}nchen.
\newblock \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}.

\bibitem[\protect\citeauthoryear{Wiedijk}{1999}]{wie:99:1}
Wiedijk, F.: 1999, `{Mizar: An Impression}'.
\newblock \url{http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz}.

\bibitem[\protect\citeauthoryear{Wiedijk}{2000}]{wie:00:2}
Wiedijk, F.: 2000, `The Mathematical Vernacular'.
\newblock \url{http://www.cs.kun.nl/~freek/notes/mv.ps.gz}.

\bibitem[\protect\citeauthoryear{Wiedijk}{2001}]{wie:01}
Wiedijk, F.: 2001, `Mizar Light for {HOL} Light'.
\newblock In: R.~J. Boulton and P.~B. Jackson (eds.): {\em Theorem Proving in
  Higher Order Logics: {TPHOLs} 2001}, Vol. 2152 of {\em LNCS}.

\bibitem[\protect\citeauthoryear{Wiedijk}{2002}]{wie:02}
Wiedijk, F.: 2002, `{Formal proof sketches}'.
\newblock \url{http://www.cs.kun.nl/~freek/notes/sketches.ps.gz}.

\bibitem[\protect\citeauthoryear{Zammit}{1999a}]{zam:99}
Zammit, V.: 1999a, `{On the Implementation of an Extensible Declarative Proof
  Language}'.
\newblock In: {\em Theorem Proving in Higher Order Logics, TPHOLs '99, Nice,
  France}, Vol. 1690 of {\em LNCS}. Springer.

\bibitem[\protect\citeauthoryear{Zammit}{1999b}]{zam:99:thesis}
Zammit, V.: 1999b, `On the Readability of Machine Checkable Formal Proofs'.
\newblock Ph.D. thesis, University of Kent.

\end{thebibliography}

\end{article}

\end{document}