*Subject*: [isabelle] Follow-up [Re: Isabelle operator precedence]*From*: Holger Blasum <hbl at sysgo.com>*Date*: Mon, 12 Nov 2012 23:05:15 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20121105142302.GA10786@laptop-hbl.localdomain>*References*: <20121105142302.GA10786@laptop-hbl.localdomain>*User-agent*: Mutt/1.5.21 (2010-09-15)

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**

\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}

**Follow-Ups**:**Re: [isabelle] Follow-up [Re: Isabelle operator precedence]***From:*Makarius

**References**:**[isabelle] Isabelle operator precedence***From:*Holger Blasum

- Previous by Date: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails
- Next by Date: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions
- Previous by Thread: Re: [isabelle] Isabelle operator precedence
- Next by Thread: Re: [isabelle] Follow-up [Re: Isabelle operator precedence]
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list