author  wenzelm 
Sun, 18 Aug 2013 13:25:31 +0200  
changeset 53059  f4811f3628dc 
parent 53015  a1119cf551e8 
child 55033  8e8243975860 
permissions  rwrr 
27037  1 
theory Outer_Syntax 
42651  2 
imports Base Main 
27037  3 
begin 
4 

47114
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46282
diff
changeset

5 
chapter {* Outer syntax  the theory language \label{ch:outersyntax} *} 
27037  6 

7 
text {* 

8 
The rather generic framework of Isabelle/Isar syntax emerges from 

9 
three main syntactic categories: \emph{commands} of the toplevel 

10 
Isar engine (covering theory and proof elements), \emph{methods} for 

11 
general goal refinements (analogous to traditional ``tactics''), and 

12 
\emph{attributes} for operations on facts (within a certain 

13 
context). Subsequently we give a reference of basic syntactic 

14 
entities underlying Isabelle/Isar syntax in a bottomup manner. 

15 
Concrete theory and proof language elements will be introduced later 

16 
on. 

17 

18 
\medskip In order to get started with writing wellformed 

19 
Isabelle/Isar documents, the most important aspect to be noted is 

20 
the difference of \emph{inner} versus \emph{outer} syntax. Inner 

21 
syntax is that of Isabelle types and terms of the logic, while outer 

22 
syntax is that of Isabelle/Isar theory sources (specifications and 

23 
proofs). As a general rule, inner syntax entities may occur only as 

24 
\emph{atomic entities} within outer syntax. For example, the string 

25 
@{verbatim "\"x + y\""} and identifier @{verbatim z} are legal term 

26 
specifications within a theory, while @{verbatim "x + y"} without 

27 
quotes is not. 

28 

29 
Printed theory documents usually omit quotes to gain readability 

30 
(this is a matter of {\LaTeX} macro setup, say via @{verbatim 

31 
"\\isabellestyle"}, see also \cite{isabellesys}). Experienced 

32 
users of Isabelle/Isar may easily reconstruct the lost technical 

33 
information, while mere readers need not care about quotes at all. 

34 

35 
\medskip Isabelle/Isar input may contain any number of input 

36 
termination characters ``@{verbatim ";"}'' (semicolon) to separate 

37 
commands explicitly. This is particularly useful in interactive 

38 
shell sessions to make clear where the current command is intended 

39 
to end. Otherwise, the interpreter loop will continue to issue a 

40 
secondary prompt ``@{verbatim "#"}'' until an endofcommand is 

41 
clearly recognized from the input syntax, e.g.\ encounter of the 

42 
next command keyword. 

43 

51058  44 
More advanced interfaces such as Isabelle/jEdit \cite{Wenzel:2012} 
45 
and Proof~General \cite{proofgeneral} do not require explicit 

51062  46 
semicolons: command spans are determined by inspecting the content 
47 
of the editor buffer. In the printed presentation of Isabelle/Isar 

48 
documents semicolons are omitted altogether for readability. 

27037  49 

50 
\begin{warn} 

51 
Proof~General requires certain syntax classification tables in 

52 
order to achieve properly synchronized interaction with the 

53 
Isabelle/Isar process. These tables need to be consistent with 

54 
the Isabelle version and particular logic image to be used in a 

55 
running session (common objectlogics may well change the outer 

56 
syntax). The standard setup should work correctly with any of the 

57 
``official'' logic images derived from Isabelle/HOL (including 

58 
HOLCF etc.). Users of alternative logics may need to tell 

59 
Proof~General explicitly, e.g.\ by giving an option @{verbatim "k ZF"} 

60 
(in conjunction with @{verbatim "l ZF"}, to specify the default 

61 
logic image). Note that option @{verbatim "L"} does both 

62 
of this at the same time. 

63 
\end{warn} 

64 
*} 

65 

66 

50213  67 
section {* Commands *} 
68 

69 
text {* 

70 
\begin{matharray}{rcl} 

71 
@{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ 

72 
@{command_def "help"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ 

73 
\end{matharray} 

74 

75 
@{rail " 

76 
@@{command help} (@{syntax name} * ) 

77 
"} 

78 

79 
\begin{description} 

80 

81 
\item @{command "print_commands"} prints all outer syntax keywords 

82 
and commands. 

83 

84 
\item @{command "help"}~@{text "pats"} retrieves outer syntax 

85 
commands according to the specified name patterns. 

86 

87 
\end{description} 

88 
*} 

89 

90 

91 
subsubsection {* Examples *} 

92 

93 
text {* Some common diagnostic commands are retrieved like this 

94 
(according to usual naming conventions): *} 

95 

96 
help "print" 

97 
help "find" 

98 

99 

28774  100 
section {* Lexical matters \label{sec:outerlex} *} 
27037  101 

28775
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

102 
text {* The outer lexical syntax consists of three main categories of 
28776  103 
syntax tokens: 
28775
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

104 

d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

105 
\begin{enumerate} 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

106 

d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

107 
\item \emph{major keywords}  the command names that are available 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

108 
in the present logic session; 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

109 

d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

110 
\item \emph{minor keywords}  additional literal tokens required 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

111 
by the syntax of commands; 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

112 

28776  113 
\item \emph{named tokens}  various categories of identifiers etc. 
27037  114 

28775
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

115 
\end{enumerate} 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

116 

28776  117 
Major keywords and minor keywords are guaranteed to be disjoint. 
28775
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

118 
This helps userinterfaces to determine the overall structure of a 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

119 
theory text, without knowing the full details of command syntax. 
28776  120 
Internally, there is some additional information about the kind of 
121 
major keywords, which approximates the command type (theory command, 

122 
proof command etc.). 

28775
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

123 

d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

124 
Keywords override named tokens. For example, the presence of a 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

125 
command called @{verbatim term} inhibits the identifier @{verbatim 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

126 
term}, but the string @{verbatim "\"term\""} can be used instead. 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

127 
By convention, the outer syntax always allows quoted strings in 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

128 
addition to identifiers, wherever a named entity is expected. 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

129 

28776  130 
When tokenizing a given input sequence, the lexer repeatedly takes 
131 
the longest prefix of the input that forms a valid token. Spaces, 

132 
tabs, newlines and formfeeds between tokens serve as explicit 

133 
separators. 

134 

28775
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

135 
\medskip The categories for named tokens are defined once and for 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

136 
all as follows. 
27037  137 

28776  138 
\begin{center} 
28775
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

139 
\begin{supertabular}{rcl} 
53059  140 
@{syntax_def ident} & = & @{text "letter (subscript\<^sup>? quasiletter)\<^sup>*"} \\ 
28775
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

141 
@{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

142 
@{syntax_def symident} & = & @{text "sym\<^sup>+  "}@{verbatim "\\"}@{verbatim "<"}@{text ident}@{verbatim ">"} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

143 
@{syntax_def nat} & = & @{text "digit\<^sup>+"} \\ 
40290
47f572aff50a
support for floatingpoint tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
35841
diff
changeset

144 
@{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  "}@{verbatim ""}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ 
28775
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

145 
@{syntax_def var} & = & @{verbatim "?"}@{text "ident  "}@{verbatim "?"}@{text ident}@{verbatim "."}@{text nat} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

146 
@{syntax_def typefree} & = & @{verbatim "'"}@{text ident} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

147 
@{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree  "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

148 
@{syntax_def string} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

149 
@{syntax_def altstring} & = & @{verbatim "`"} @{text "\<dots>"} @{verbatim "`"} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

150 
@{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*"}@{verbatim "}"} \\[1ex] 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

151 

d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

152 
@{text letter} & = & @{text "latin  "}@{verbatim "\\"}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  "}@{verbatim "\\"}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  greek "} \\ 
53059  153 
@{text subscript} & = & @{verbatim "\<^sub>"} \\ 
28775
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

154 
@{text quasiletter} & = & @{text "letter  digit  "}@{verbatim "_"}@{text "  "}@{verbatim "'"} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

155 
@{text latin} & = & @{verbatim a}@{text "  \<dots>  "}@{verbatim z}@{text "  "}@{verbatim A}@{text "  \<dots>  "}@{verbatim Z} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

156 
@{text digit} & = & @{verbatim "0"}@{text "  \<dots>  "}@{verbatim "9"} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

157 
@{text sym} & = & @{verbatim "!"}@{text "  "}@{verbatim "#"}@{text "  "}@{verbatim "$"}@{text "  "}@{verbatim "%"}@{text "  "}@{verbatim "&"}@{text "  "}@{verbatim "*"}@{text "  "}@{verbatim "+"}@{text "  "}@{verbatim ""}@{text "  "}@{verbatim "/"}@{text " "} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

158 
& & @{verbatim "<"}@{text "  "}@{verbatim "="}@{text "  "}@{verbatim ">"}@{text "  "}@{verbatim "?"}@{text "  "}@{verbatim "@"}@{text "  "}@{verbatim "^"}@{text "  "}@{verbatim "_"}@{text "  "}@{verbatim ""}@{text "  "}@{verbatim "~"} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

159 
@{text greek} & = & @{verbatim "\<alpha>"}@{text "  "}@{verbatim "\<beta>"}@{text "  "}@{verbatim "\<gamma>"}@{text "  "}@{verbatim "\<delta>"}@{text " "} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

160 
& & @{verbatim "\<epsilon>"}@{text "  "}@{verbatim "\<zeta>"}@{text "  "}@{verbatim "\<eta>"}@{text "  "}@{verbatim "\<theta>"}@{text " "} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

161 
& & @{verbatim "\<iota>"}@{text "  "}@{verbatim "\<kappa>"}@{text "  "}@{verbatim "\<mu>"}@{text "  "}@{verbatim "\<nu>"}@{text " "} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

162 
& & @{verbatim "\<xi>"}@{text "  "}@{verbatim "\<pi>"}@{text "  "}@{verbatim "\<rho>"}@{text "  "}@{verbatim "\<sigma>"}@{text "  "}@{verbatim "\<tau>"}@{text " "} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

163 
& & @{verbatim "\<upsilon>"}@{text "  "}@{verbatim "\<phi>"}@{text "  "}@{verbatim "\<chi>"}@{text "  "}@{verbatim "\<psi>"}@{text " "} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

164 
& & @{verbatim "\<omega>"}@{text "  "}@{verbatim "\<Gamma>"}@{text "  "}@{verbatim "\<Delta>"}@{text "  "}@{verbatim "\<Theta>"}@{text " "} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

165 
& & @{verbatim "\<Lambda>"}@{text "  "}@{verbatim "\<Xi>"}@{text "  "}@{verbatim "\<Pi>"}@{text "  "}@{verbatim "\<Sigma>"}@{text " "} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

166 
& & @{verbatim "\<Upsilon>"}@{text "  "}@{verbatim "\<Phi>"}@{text "  "}@{verbatim "\<Psi>"}@{text "  "}@{verbatim "\<Omega>"} \\ 
d25fe9601dbd
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents:
28774
diff
changeset

167 
\end{supertabular} 
28776  168 
\end{center} 
27037  169 

28778  170 
A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown, 
171 
which is internally a pair of base name and index (ML type @{ML_type 

172 
indexname}). These components are either separated by a dot as in 

173 
@{text "?x.1"} or @{text "?x7.3"} or run together as in @{text 

174 
"?x1"}. The latter form is possible if the base name does not end 

175 
with digits. If the index is 0, it may be dropped altogether: 

176 
@{text "?x"} and @{text "?x0"} and @{text "?x.0"} all refer to the 

177 
same unknown, with basename @{text "x"} and index 0. 

178 

179 
The syntax of @{syntax_ref string} admits any characters, including 

27037  180 
newlines; ``@{verbatim "\""}'' (doublequote) and ``@{verbatim 
181 
"\\"}'' (backslash) need to be escaped by a backslash; arbitrary 

182 
character codes may be specified as ``@{verbatim "\\"}@{text ddd}'', 

183 
with three decimal digits. Alternative strings according to 

28778  184 
@{syntax_ref altstring} are analogous, using single backquotes 
185 
instead. 

186 

187 
The body of @{syntax_ref verbatim} may consist of any text not 

27037  188 
containing ``@{verbatim "*"}@{verbatim "}"}''; this allows 
28778  189 
convenient inclusion of quotes without further escapes. There is no 
190 
way to escape ``@{verbatim "*"}@{verbatim "}"}''. If the quoted 

191 
text is {\LaTeX} source, one may usually add some blank or comment 

192 
to avoid the critical character sequence. 

193 

194 
Source comments take the form @{verbatim "(*"}~@{text 

195 
"\<dots>"}~@{verbatim "*)"} and may be nested, although the userinterface 

196 
might prevent this. Note that this form indicates source comments 

197 
only, which are stripped after lexical analysis of the input. The 

198 
Isar syntax also provides proper \emph{document comments} that are 

199 
considered as part of the text (see \secref{sec:comments}). 

27037  200 

201 
Common mathematical symbols such as @{text \<forall>} are represented in 

202 
Isabelle as @{verbatim \<forall>}. There are infinitely many Isabelle 

203 
symbols like this, although proper presentation is left to frontend 

47822
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks XSymbol mode of 3.x;
wenzelm
parents:
47114
diff
changeset

204 
tools such as {\LaTeX}, Proof~General, or Isabelle/jEdit. A list of 
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks XSymbol mode of 3.x;
wenzelm
parents:
47114
diff
changeset

205 
predefined Isabelle symbols that work well with these tools is given 
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks XSymbol mode of 3.x;
wenzelm
parents:
47114
diff
changeset

206 
in \appref{app:symbols}. Note that @{verbatim "\<lambda>"} does not belong 
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks XSymbol mode of 3.x;
wenzelm
parents:
47114
diff
changeset

207 
to the @{text letter} category, since it is already used differently 
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks XSymbol mode of 3.x;
wenzelm
parents:
47114
diff
changeset

208 
in the Pure term language. *} 
27037  209 

210 

211 
section {* Common syntax entities *} 

212 

213 
text {* 

214 
We now introduce several basic syntactic entities, such as names, 

215 
terms, and theorem specifications, which are factored out of the 

216 
actual Isar language elements to be described later. 

217 
*} 

218 

219 

220 
subsection {* Names *} 

221 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

222 
text {* Entity @{syntax name} usually refers to any name of types, 
27037  223 
constants, theorems etc.\ that are to be \emph{declared} or 
224 
\emph{defined} (so qualified identifiers are excluded here). Quoted 

225 
strings provide an escape for nonidentifier names or those ruled 

226 
out by outer syntax keywords (e.g.\ quoted @{verbatim "\"let\""}). 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

227 
Already existing objects are usually referenced by @{syntax 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

228 
nameref}. 
27037  229 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

230 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

231 
@{syntax_def name}: @{syntax ident}  @{syntax symident}  
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

232 
@{syntax string}  @{syntax nat} 
27037  233 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

234 
@{syntax_def parname}: '(' @{syntax name} ')' 
27037  235 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

236 
@{syntax_def nameref}: @{syntax name}  @{syntax longident} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

237 
"} 
40296  238 
*} 
239 

240 

241 
subsection {* Numbers *} 

242 

243 
text {* The outer lexical syntax (\secref{sec:outerlex}) admits 

244 
natural numbers and floating point numbers. These are combined as 

245 
@{syntax int} and @{syntax real} as follows. 

246 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

247 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

248 
@{syntax_def int}: @{syntax nat}  '' @{syntax nat} 
27037  249 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

250 
@{syntax_def real}: @{syntax float}  @{syntax int} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

251 
"} 
40296  252 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

253 
Note that there is an overlap with the category @{syntax name}, 
40296  254 
which also includes @{syntax nat}. 
27037  255 
*} 
256 

257 

258 
subsection {* Comments \label{sec:comments} *} 

259 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

260 
text {* Large chunks of plain @{syntax text} are usually given 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

261 
@{syntax verbatim}, i.e.\ enclosed in @{verbatim "{"}@{verbatim 
27037  262 
"*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}. For convenience, 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

263 
any of the smaller text units conforming to @{syntax nameref} are 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

264 
admitted as well. A marginal @{syntax comment} is of the form 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

265 
@{verbatim ""}~@{syntax text}. Any number of these may occur 
27037  266 
within Isabelle/Isar commands. 
267 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

268 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

269 
@{syntax_def text}: @{syntax verbatim}  @{syntax nameref} 
27037  270 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

271 
@{syntax_def comment}: '' @{syntax text} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

272 
"} 
27037  273 
*} 
274 

275 

276 
subsection {* Type classes, sorts and arities *} 

277 

278 
text {* 

279 
Classes are specified by plain names. Sorts have a very simple 

280 
inner syntax, which is either a single class name @{text c} or a 

281 
list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the 

282 
intersection of these classes. The syntax of type arities is given 

283 
directly at the outer level. 

284 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

285 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

286 
@{syntax_def classdecl}: @{syntax name} (('<'  '\<subseteq>') (@{syntax nameref} + ','))? 
27037  287 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

288 
@{syntax_def sort}: @{syntax nameref} 
27037  289 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

290 
@{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

291 
"} 
27037  292 
*} 
293 

294 

295 
subsection {* Types and terms \label{sec:typesterms} *} 

296 

297 
text {* 

298 
The actual inner Isabelle syntax, that of types and terms of the 

299 
logic, is far too sophisticated in order to be modelled explicitly 

300 
at the outer theory level. Basically, any such entity has to be 

301 
quoted to turn it into a single token (the parsing and typechecking 

302 
is performed internally later). For convenience, a slightly more 

303 
liberal convention is adopted: quotes may be omitted for any type or 

304 
term that is already atomic at the outer level. For example, one 

305 
may just write @{verbatim x} instead of quoted @{verbatim "\"x\""}. 

306 
Note that symbolic identifiers (e.g.\ @{verbatim "++"} or @{text 

307 
"\<forall>"} are available as well, provided these have not been superseded 

308 
by commands or other keywords already (such as @{verbatim "="} or 

309 
@{verbatim "+"}). 

310 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

311 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

312 
@{syntax_def type}: @{syntax nameref}  @{syntax typefree}  
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

313 
@{syntax typevar} 
27037  314 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

315 
@{syntax_def term}: @{syntax nameref}  @{syntax var} 
27037  316 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

317 
@{syntax_def prop}: @{syntax term} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

318 
"} 
27037  319 

320 
Positional instantiations are indicated by giving a sequence of 

321 
terms, or the placeholder ``@{text _}'' (underscore), which means to 

322 
skip a position. 

323 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

324 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

325 
@{syntax_def inst}: '_'  @{syntax term} 
27037  326 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

327 
@{syntax_def insts}: (@{syntax inst} *) 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

328 
"} 
27037  329 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

330 
Type declarations and definitions usually refer to @{syntax 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

331 
typespec} on the lefthand side. This models basic type constructor 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

332 
application at the outer syntax level. Note that only plain postfix 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

333 
notation is available here, but no infixes. 
27037  334 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

335 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

336 
@{syntax_def typespec}: 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

337 
(()  @{syntax typefree}  '(' ( @{syntax typefree} + ',' ) ')') @{syntax name} 
27037  338 
; 
42705  339 
@{syntax_def typespec_sorts}: 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

340 
(()  (@{syntax typefree} ('::' @{syntax sort})?)  
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

341 
'(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

342 
"} 
27037  343 
*} 
344 

345 

28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

346 
subsection {* Term patterns and declarations \label{sec:termdecls} *} 
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

347 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

348 
text {* Wherever explicit propositions (or term fragments) occur in a 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

349 
proof text, casual binding of schematic term variables may be given 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

350 
specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}''. 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

351 
This works both for @{syntax term} and @{syntax prop}. 
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

352 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

353 
@{rail " 
42705  354 
@{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')' 
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

355 
; 
42705  356 
@{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')' 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

357 
"} 
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

358 

6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

359 
\medskip Declarations of local variables @{text "x :: \<tau>"} and 
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

360 
logical propositions @{text "a : \<phi>"} represent different views on 
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

361 
the same principle of introducing a local scope. In practice, one 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

362 
may usually omit the typing of @{syntax vars} (due to 
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

363 
typeinference), and the naming of propositions (due to implicit 
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

364 
references of current facts). In any case, Isar proof elements 
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

365 
usually admit to introduce multiple such items simultaneously. 
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

366 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

367 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

368 
@{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})? 
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

369 
; 
42705  370 
@{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +) 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

371 
"} 
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

372 

6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

373 
The treatment of multiple declarations corresponds to the 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

374 
complementary focus of @{syntax vars} versus @{syntax props}. In 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

375 
``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}'' the typing refers to all variables, while 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

376 
in @{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} the naming refers to all propositions 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

377 
collectively. Isar language elements that refer to @{syntax vars} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

378 
or @{syntax props} typically admit separate typings or namings via 
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

379 
another level of iteration, with explicit @{keyword_ref "and"} 
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

380 
separators; e.g.\ see @{command "fix"} and @{command "assume"} in 
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

381 
\secref{sec:proofcontext}. 
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

382 
*} 
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

383 

6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

384 

27037  385 
subsection {* Attributes and theorems \label{sec:synatt} *} 
386 

28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

387 
text {* Attributes have their own ``semiinner'' syntax, in the sense 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

388 
that input conforming to @{syntax args} below is parsed by the 
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

389 
attribute a second time. The attribute argument specifications may 
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

390 
be any sequence of atomic entities (identifiers, strings etc.), or 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

391 
properly bracketed argument lists. Below @{syntax atom} refers to 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

392 
any atomic entity, including any @{syntax keyword} conforming to 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

393 
@{syntax symident}. 
27037  394 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

395 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

396 
@{syntax_def atom}: @{syntax nameref}  @{syntax typefree}  
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

397 
@{syntax typevar}  @{syntax var}  @{syntax nat}  @{syntax float}  
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

398 
@{syntax keyword} 
27037  399 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

400 
arg: @{syntax atom}  '(' @{syntax args} ')'  '[' @{syntax args} ']' 
27037  401 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

402 
@{syntax_def args}: arg * 
27037  403 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

404 
@{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']' 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

405 
"} 
27037  406 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

407 
Theorem specifications come in several flavors: @{syntax axmdecl} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

408 
and @{syntax thmdecl} usually refer to axioms, assumptions or 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

409 
results of goal statements, while @{syntax thmdef} collects lists of 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

410 
existing theorems. Existing theorems are given by @{syntax thmref} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

411 
and @{syntax thmrefs}, the former requires an actual singleton 
27037  412 
result. 
413 

414 
There are three forms of theorem references: 

415 
\begin{enumerate} 

416 

417 
\item named facts @{text "a"}, 

418 

419 
\item selections from named facts @{text "a(i)"} or @{text "a(j  k)"}, 

420 

421 
\item literal fact propositions using @{syntax_ref altstring} syntax 

422 
@{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method 

28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
28753
diff
changeset

423 
@{method_ref fact}). 
27037  424 

425 
\end{enumerate} 

426 

427 
Any kind of theorem specification may include lists of attributes 

428 
both on the left and right hand sides; attributes are applied to any 

429 
immediately preceding fact. If names are omitted, the theorems are 

430 
not stored within the theorem database of the theory or proof 

431 
context, but any given attributes are applied nonetheless. 

432 

433 
An extra pair of brackets around attributes (like ``@{text 

434 
"[[simproc a]]"}'') abbreviates a theorem reference involving an 

435 
internal dummy fact, which will be ignored later on. So only the 

436 
effect of the attribute on the background context will persist. 

437 
This form of inplace declarations is particularly useful with 

438 
commands like @{command "declare"} and @{command "using"}. 

439 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

440 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

441 
@{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':' 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

442 
; 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

443 
@{syntax_def thmdecl}: thmbind ':' 
27037  444 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

445 
@{syntax_def thmdef}: thmbind '=' 
27037  446 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

447 
@{syntax_def thmref}: 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

448 
(@{syntax nameref} selection?  @{syntax altstring}) @{syntax attributes}?  
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

449 
'[' @{syntax attributes} ']' 
27037  450 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

451 
@{syntax_def thmrefs}: @{syntax thmref} + 
27037  452 
; 
453 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

454 
thmbind: @{syntax name} @{syntax attributes}  @{syntax name}  @{syntax attributes} 
27037  455 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

456 
selection: '(' ((@{syntax nat}  @{syntax nat} '' @{syntax nat}?) + ',') ')' 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40296
diff
changeset

457 
"} 
27037  458 
*} 
459 

460 
end 