[isabelle] Follow-up [Re: Isabelle operator precedence]



Dear all, 

attached is an attempt to follow-up on last week's discussion (thanks!). I
think it is good enough for myself at the moment, however in case 
sth like this would make it into user documentation note that there 
are still some gaps e.g. concerning precedence values e.g. of "set"/"list"
type constructors or the application of user-defined functions.

Best,

-- 
Holger

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

\documentclass[a4paper]{article}
\usepackage[margin=1in]{geometry}
\usepackage{hyperref}

\usepackage{amssymb}
\usepackage{stmaryrd}

\title{}
\author{}

\begin{document}

\begin{table}[h]
{\em Operator precedence cheat sheet for Isabelle/HOL} (quick and dirty, little quality control, version 2012-Nov-12). Follow-up of the discussion at the Isabelle mailing list in November 2012, \url{https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/msg00020.html}.  Entries without a fixed precedence are still rough guesstimates (that may need further correction).
\begin{center}

\begin{tabular}{|l|r|p{6cm}|}
\hline
Class & Precedence & Symbols and the minimum precedence of symbols that may be contained in non-terminals \\
\hline
\hline function &      & application of user-defined function, field dereference (record) \\
\hline function &  900 & (900 $\llparenthesis$ 0 $\rrparenthesis$ (record update)) \\ 
\hline function &  100 & (100 nth (list) 101) \\ 
\hline type	    &      & ``set'' type constructor, ``list'' type constructor \\
\hline function &   70 & (70 $\cap$ (set) 71), (70 * (nat) 71) \\
\hline function &   65 & (65 $\cup$ (set) 66), (65 + (nat) 66), (65 $-$ (nat) 66), (66 \# (list) 65), (66 @ (list) 65) \\
\hline relation &   50 & (50 = 51), (50 $\in$ 51), (51 $<$ 51), (51 $\le$ 51) \\ 
\hline logic    &   40 & ($\neg$ 40) \\ 
\hline logic    &   35 & (36 $\wedge$ 35) \\
\hline logic    &   30 & (31 $\vee$ 30) \\
\hline logic    &   25 & (26 $\longrightarrow$ 25), (26 $\leftrightarrow$ 25) \\
\hline logic    &   10 & ($\forall$ 0 .\ 10), ($\exists$ 0 .\ 10), (if 0 then 0 else 10), (case 0 of 10), (let 0 in 10) \\
\hline type	    &    3 & (4 :: 0)  \\
\hline logic    &    3 & ($\lambda $ 0 .\ 3) \\
\hline metalogic &   2 & (3 $\equiv$ 2) \\
\hline metalogic &   1 & (2 $\Longrightarrow$ 1) \\
\hline type	    &    0 & (1 $\Rightarrow$ 0) \\
\hline metalogic &   0 & ($\bigwedge$ 0 .\ 0) \\
\hline

\end{tabular}
\caption{Higher symbols have higher precedence. Precedences given where known to me, by use of the Isabelle command ``print\_syntax'' - you can issue this command for example anywhere in an empty theory or an existing theory. ``print\_syntax'' also shows precedence for a lot of symbols not given in the table for brevity (say, exponentiation of natural numbers). Following the convention of the output of ``print\_syntax'', associativity of binary operators is determined by that a non-terminal in the right-hand side production rule of a grammar only may be expanded by non-terminals with the same or higher precedence. Hence, for example addition on the natural numbers is left-associative, as its production still allows expansion to the left of the ``+'' operator. Conversely, for example list concatenation is right-associative. ``$<$'' is not associative at all (no expansion allowed either way). See also the post by Holger Gast for a more detailed explanation (\url{https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/msg00032.html}). 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[metalogic] if it is meta logic
\end{description}

\end{document}


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