[isabelle] Isabelle operator precedence



Dear all,

while it is mostly "intuitive" I would like to have a clearer view of 
operator precedence in Isabelle. Attached is what I quickly reverse-
engineered on a train ride on the long weekend. Is it correct? Is there 
already any explicit information on this (beyond using 
Isabelle -> Settings -> Display -> Show Brackets in PG)?

Thanks,

-- 
Holger

Attachment: isabelle-operator-precedence-cheat-sheet.pdf
Description: Adobe PDF document

\documentclass[a4paper]{article}

\usepackage{amssymb}
\usepackage{stmaryrd}

\title{Isabelle operator precedence: experimental cheat sheet}
\author{author}

\begin{document}

\begin{table}[h]
Operator precedence cheat sheet in Isabelle-HOL (quick and dirty ad-hoc reverse-engineered mostly on a train ride, no quality control at all). For discussion at Isabelle users list.
\begin{center}

\begin{tabular}{|l|l|l|}
\hline
Class & Symbol(s) & Weight\\
\hline
\hline function & function application, field dereference (record), nth (list) & \\
\hline type	    & ``set'' type constructor, ``list'' type constructor & \\
\hline function & $\cap$ (set) & \\
\hline function & $\cup$ (set), \# (list), @ (list), + (nat), Suc (nat) & 65 \\
\hline relation & = & \\
\hline relation & $\in$, $<$, $\le$ & 50 \\ 
\hline logic    & $\neg$ & \\ 
\hline logic    & $\wedge$ & 35 \\
\hline logic    & $\vee$ & 30 \\
\hline logic    & $\longrightarrow$, $\leftrightarrow$ & 25 \\
\hline type	    & $\Rightarrow$ & \\
\hline logic    & $\forall$, $\exists$ & \\
\hline term     & if .. then .. else & \\
\hline term     & $\lambda $ & \\
\hline term     & .. $\llparenthesis$ .. := .. $\rrparenthesis$ (record) & \\ 
\hline term     & let .. = .. in .. & \\
\hline metalogic & $\equiv$ & \\
\hline metalogic & $\Longrightarrow$ & \\
\hline metalogic & $\bigwedge$ & \\
\hline

\end{tabular}
\caption{Higher symbols have higher precedence. Weights given where known (grepping Isabelle sources for ``infixr''). Classes are my own interpretation.}
\end{center}
\end{table}

\paragraph{Note on classes:}

\begin{description}
\item[function] if it is a function (type constructors ``set'', ``list'' could also be seen as functions)
\item[relation] if it is a relation
\item[logic] if it is object logic
\item[term] term constructors  
\item[metalogic] if it is meta logic
\end{description}

%\tableofcontents

\end{document}


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.