src/Doc/Isar_Ref/Outer_Syntax.thy
author wenzelm
Fri, 13 Nov 2015 21:31:04 +0100
changeset 61663 63af76397a60
parent 61662 e77def9a63a6
child 62172 7eaeae127955
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61656
cfabbc083977 more uniform jEdit properties;
wenzelm
parents: 61579
diff changeset
     1
(*:maxLineLen=78:*)
cfabbc083977 more uniform jEdit properties;
wenzelm
parents: 61579
diff changeset
     2
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     3
theory Outer_Syntax
42651
e3fdb7c96be5 formal Base theory;
wenzelm
parents: 42596
diff changeset
     4
imports Base Main
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     5
begin
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     6
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
     7
chapter \<open>Outer syntax --- the theory language \label{ch:outer-syntax}\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     8
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
     9
text \<open>
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    10
  The rather generic framework of Isabelle/Isar syntax emerges from three main
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    11
  syntactic categories: \<^emph>\<open>commands\<close> of the top-level Isar engine (covering
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    12
  theory and proof elements), \<^emph>\<open>methods\<close> for general goal refinements
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    13
  (analogous to traditional ``tactics''), and \<^emph>\<open>attributes\<close> for operations on
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    14
  facts (within a certain context). Subsequently we give a reference of basic
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    15
  syntactic entities underlying Isabelle/Isar syntax in a bottom-up manner.
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    16
  Concrete theory and proof language elements will be introduced later on.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    17
61421
e0825405d398 more symbols;
wenzelm
parents: 61252
diff changeset
    18
  \<^medskip>
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    19
  In order to get started with writing well-formed Isabelle/Isar documents,
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    20
  the most important aspect to be noted is the difference of \<^emph>\<open>inner\<close> versus
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    21
  \<^emph>\<open>outer\<close> syntax. Inner syntax is that of Isabelle types and terms of the
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    22
  logic, while outer syntax is that of Isabelle/Isar theory sources
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    23
  (specifications and proofs). As a general rule, inner syntax entities may
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    24
  occur only as \<^emph>\<open>atomic entities\<close> within outer syntax. For example, the
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    25
  string \<^verbatim>\<open>"x + y"\<close> and identifier \<^verbatim>\<open>z\<close> are legal term specifications within a
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    26
  theory, while \<^verbatim>\<open>x + y\<close> without quotes is not.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    27
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    28
  Printed theory documents usually omit quotes to gain readability (this is a
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    29
  matter of {\LaTeX} macro setup, say via \<^verbatim>\<open>\isabellestyle\<close>, see also @{cite
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    30
  "isabelle-system"}). Experienced users of Isabelle/Isar may easily
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    31
  reconstruct the lost technical information, while mere readers need not care
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    32
  about quotes at all.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
    33
\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    34
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    35
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
    36
section \<open>Commands\<close>
50213
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    37
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
    38
text \<open>
50213
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    39
  \begin{matharray}{rcl}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
    40
    @{command_def "print_commands"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
    41
    @{command_def "help"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
50213
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    42
  \end{matharray}
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    43
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
    44
  @{rail \<open>
50213
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    45
    @@{command help} (@{syntax name} * )
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
    46
  \<close>}
50213
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    47
61439
2bf52eec4e8a more symbols;
wenzelm
parents: 61421
diff changeset
    48
  \<^descr> @{command "print_commands"} prints all outer syntax keywords
50213
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    49
  and commands.
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    50
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
    51
  \<^descr> @{command "help"}~\<open>pats\<close> retrieves outer syntax
50213
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    52
  commands according to the specified name patterns.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
    53
\<close>
50213
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    54
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    55
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
    56
subsubsection \<open>Examples\<close>
50213
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    57
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    58
text \<open>
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    59
  Some common diagnostic commands are retrieved like this (according to usual
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    60
  naming conventions):
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    61
\<close>
50213
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    62
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    63
help "print"
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    64
help "find"
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    65
7b73c0509835 refined outer syntax 'help' command;
wenzelm
parents: 48985
diff changeset
    66
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
    67
section \<open>Lexical matters \label{sec:outer-lex}\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    68
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    69
text \<open>
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    70
  The outer lexical syntax consists of three main categories of syntax tokens:
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
    71
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    72
    \<^enum> \<^emph>\<open>major keywords\<close> --- the command names that are available
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    73
    in the present logic session;
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
    74
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    75
    \<^enum> \<^emph>\<open>minor keywords\<close> --- additional literal tokens required
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    76
    by the syntax of commands;
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    77
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    78
    \<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc.
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
    79
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    80
  Major keywords and minor keywords are guaranteed to be disjoint. This helps
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    81
  user-interfaces to determine the overall structure of a theory text, without
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    82
  knowing the full details of command syntax. Internally, there is some
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    83
  additional information about the kind of major keywords, which approximates
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    84
  the command type (theory command, proof command etc.).
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
    85
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    86
  Keywords override named tokens. For example, the presence of a command
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    87
  called \<^verbatim>\<open>term\<close> inhibits the identifier \<^verbatim>\<open>term\<close>, but the string \<^verbatim>\<open>"term"\<close> can
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    88
  be used instead. By convention, the outer syntax always allows quoted
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    89
  strings in addition to identifiers, wherever a named entity is expected.
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
    90
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    91
  When tokenizing a given input sequence, the lexer repeatedly takes the
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    92
  longest prefix of the input that forms a valid token. Spaces, tabs, newlines
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
    93
  and formfeeds between tokens serve as explicit separators.
28776
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
    94
61421
e0825405d398 more symbols;
wenzelm
parents: 61252
diff changeset
    95
  \<^medskip>
e0825405d398 more symbols;
wenzelm
parents: 61252
diff changeset
    96
  The categories for named tokens are defined once and for all as follows.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    97
28776
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
    98
  \begin{center}
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
    99
  \begin{supertabular}{rcl}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   100
    @{syntax_def ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   101
    @{syntax_def longident} & = & \<open>ident(\<close>\<^verbatim>\<open>.\<close>\<open>ident)\<^sup>+\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   102
    @{syntax_def symident} & = & \<open>sym\<^sup>+  |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close> \\
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   103
    @{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   104
    @{syntax_def float} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat}~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>@{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   105
    @{syntax_def var} & = & \<^verbatim>\<open>?\<close>\<open>ident  |\<close>~~\<^verbatim>\<open>?\<close>\<open>ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   106
    @{syntax_def typefree} & = & \<^verbatim>\<open>'\<close>\<open>ident\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   107
    @{syntax_def typevar} & = & \<^verbatim>\<open>?\<close>\<open>typefree  |\<close>~~\<^verbatim>\<open>?\<close>\<open>typefree\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   108
    @{syntax_def string} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   109
    @{syntax_def altstring} & = & \<^verbatim>\<open>`\<close> \<open>\<dots>\<close> \<^verbatim>\<open>`\<close> \\
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   110
    @{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   111
    @{syntax_def verbatim} & = & \<^verbatim>\<open>{*\<close> \<open>\<dots>\<close> \<^verbatim>\<open>*}\<close> \\[1ex]
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   112
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   113
    \<open>letter\<close> & = & \<open>latin  |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>latin\<close>\<^verbatim>\<open>>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>latin latin\<close>\<^verbatim>\<open>>\<close>~~\<open>|  greek  |\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   114
    \<open>subscript\<close> & = & \<^verbatim>\<open>\<^sub>\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   115
    \<open>quasiletter\<close> & = & \<open>letter  |  digit  |\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>'\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   116
    \<open>latin\<close> & = & \<^verbatim>\<open>a\<close>~~\<open>| \<dots> |\<close>~~\<^verbatim>\<open>z\<close>~~\<open>|\<close>~~\<^verbatim>\<open>A\<close>~~\<open>|  \<dots> |\<close>~~\<^verbatim>\<open>Z\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   117
    \<open>digit\<close> & = & \<^verbatim>\<open>0\<close>~~\<open>|  \<dots> |\<close>~~\<^verbatim>\<open>9\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   118
    \<open>sym\<close> & = & \<^verbatim>\<open>!\<close>~~\<open>|\<close>~~\<^verbatim>\<open>#\<close>~~\<open>|\<close>~~\<^verbatim>\<open>$\<close>~~\<open>|\<close>~~\<^verbatim>\<open>%\<close>~~\<open>|\<close>~~\<^verbatim>\<open>&\<close>~~\<open>|\<close>~~\<^verbatim>\<open>*\<close>~~\<open>|\<close>~~\<^verbatim>\<open>+\<close>~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>~~\<open>|\<close>~~\<^verbatim>\<open>/\<close>~~\<open>|\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   119
    & & \<^verbatim>\<open><\<close>~~\<open>|\<close>~~\<^verbatim>\<open>=\<close>~~\<open>|\<close>~~\<^verbatim>\<open>>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>?\<close>~~\<open>|\<close>~~\<^verbatim>\<open>@\<close>~~\<open>|\<close>~~\<^verbatim>\<open>^\<close>~~\<open>|\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>|\<close>~~\<open>|\<close>~~\<^verbatim>\<open>~\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   120
    \<open>greek\<close> & = & \<^verbatim>\<open>\<alpha>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<beta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<gamma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<delta>\<close>~~\<open>|\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   121
          &   & \<^verbatim>\<open>\<epsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<zeta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<eta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<theta>\<close>~~\<open>|\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   122
          &   & \<^verbatim>\<open>\<iota>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<kappa>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<mu>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<nu>\<close>~~\<open>|\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   123
          &   & \<^verbatim>\<open>\<xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<rho>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<sigma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<tau>\<close>~~\<open>|\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   124
          &   & \<^verbatim>\<open>\<upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<chi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<psi>\<close>~~\<open>|\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   125
          &   & \<^verbatim>\<open>\<omega>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Gamma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Delta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Theta>\<close>~~\<open>|\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   126
          &   & \<^verbatim>\<open>\<Lambda>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Sigma>\<close>~~\<open>|\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61494
diff changeset
   127
          &   & \<^verbatim>\<open>\<Upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Psi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Omega>\<close> \\
28775
d25fe9601dbd tuned outer lexical syntax; fixed var/tvar: really need question marks here;
wenzelm
parents: 28774
diff changeset
   128
  \end{supertabular}
28776
e4090e51b8b9 misc tuning;
wenzelm
parents: 28775
diff changeset
   129
  \end{center}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   130
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   131
  A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown, which is
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   132
  internally a pair of base name and index (ML type @{ML_type indexname}).
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   133
  These components are either separated by a dot as in \<open>?x.1\<close> or \<open>?x7.3\<close> or
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   134
  run together as in \<open>?x1\<close>. The latter form is possible if the base name does
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   135
  not end with digits. If the index is 0, it may be dropped altogether: \<open>?x\<close>
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   136
  and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the same unknown, with basename \<open>x\<close> and
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   137
  index 0.
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   138
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   139
  The syntax of @{syntax_ref string} admits any characters, including
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   140
  newlines; ``\<^verbatim>\<open>"\<close>'' (double-quote) and ``\<^verbatim>\<open>\\<close>'' (backslash) need to be
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   141
  escaped by a backslash; arbitrary character codes may be specified as
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   142
  ``\<^verbatim>\<open>\\<close>\<open>ddd\<close>'', with three decimal digits. Alternative strings according to
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   143
  @{syntax_ref altstring} are analogous, using single back-quotes instead.
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   144
58725
9402a7f15ed5 tuned exposition of {* ... *};
wenzelm
parents: 58724
diff changeset
   145
  The body of @{syntax_ref verbatim} may consist of any text not containing
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   146
  ``\<^verbatim>\<open>*}\<close>''; this allows to include quotes without further escapes, but there
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   147
  is no way to escape ``\<^verbatim>\<open>*}\<close>''. Cartouches do not have this limitation.
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28776
diff changeset
   148
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   149
  A @{syntax_ref cartouche} consists of arbitrary text, with properly balanced
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   150
  blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim "\<close>"}''. Note that the rendering
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   151
  of cartouche delimiters is usually like this: ``\<open>\<open> \<dots> \<close>\<close>''.
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 53059
diff changeset
   152
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   153
  Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested, although
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   154
  the user-interface might prevent this. Note that this form indicates source
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   155
  comments only, which are stripped after lexical analysis of the input. The
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   156
  Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are considered as
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   157
  part of the text (see \secref{sec:comments}).
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   158
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   159
  Common mathematical symbols such as \<open>\<forall>\<close> are represented in Isabelle as \<^verbatim>\<open>\<forall>\<close>.
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   160
  There are infinitely many Isabelle symbols like this, although proper
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   161
  presentation is left to front-end tools such as {\LaTeX} or Isabelle/jEdit.
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   162
  A list of predefined Isabelle symbols that work well with these tools is
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   163
  given in \appref{app:symbols}. Note that \<^verbatim>\<open>\<lambda>\<close> does not belong to the
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   164
  \<open>letter\<close> category, since it is already used differently in the Pure term
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   165
  language.
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   166
\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   167
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   168
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   169
section \<open>Common syntax entities\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   170
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   171
text \<open>
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   172
  We now introduce several basic syntactic entities, such as names, terms, and
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   173
  theorem specifications, which are factored out of the actual Isar language
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   174
  elements to be described later.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   175
\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   176
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   177
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   178
subsection \<open>Names\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   179
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   180
text \<open>
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   181
  Entity @{syntax name} usually refers to any name of types, constants,
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   182
  theorems etc.\ that are to be \<^emph>\<open>declared\<close> or \<^emph>\<open>defined\<close> (so qualified
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   183
  identifiers are excluded here). Quoted strings provide an escape for
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   184
  non-identifier names or those ruled out by outer syntax keywords (e.g.\
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   185
  quoted \<^verbatim>\<open>"let"\<close>). Already existing objects are usually referenced by
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   186
  @{syntax nameref}.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   187
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   188
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   189
    @{syntax_def name}: @{syntax ident} | @{syntax symident} |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   190
      @{syntax string} | @{syntax nat}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   191
    ;
60131
wenzelm
parents: 59853
diff changeset
   192
    @{syntax_def par_name}: '(' @{syntax name} ')'
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   193
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   194
    @{syntax_def nameref}: @{syntax name} | @{syntax longident}
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   195
  \<close>}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   196
\<close>
40296
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   197
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   198
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   199
subsection \<open>Numbers\<close>
40296
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   200
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   201
text \<open>
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   202
  The outer lexical syntax (\secref{sec:outer-lex}) admits natural numbers and
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   203
  floating point numbers. These are combined as @{syntax int} and @{syntax
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   204
  real} as follows.
40296
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   205
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   206
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   207
    @{syntax_def int}: @{syntax nat} | '-' @{syntax nat}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   208
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   209
    @{syntax_def real}: @{syntax float} | @{syntax int}
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   210
  \<close>}
40296
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   211
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   212
  Note that there is an overlap with the category @{syntax name}, which also
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   213
  includes @{syntax nat}.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   214
\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   215
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   216
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   217
subsection \<open>Comments \label{sec:comments}\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   218
61579
634cd44bb1d3 symbolic syntax "\<comment> text";
wenzelm
parents: 61503
diff changeset
   219
text \<open>
634cd44bb1d3 symbolic syntax "\<comment> text";
wenzelm
parents: 61503
diff changeset
   220
  Large chunks of plain @{syntax text} are usually given @{syntax verbatim},
634cd44bb1d3 symbolic syntax "\<comment> text";
wenzelm
parents: 61503
diff changeset
   221
  i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>, or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For
634cd44bb1d3 symbolic syntax "\<comment> text";
wenzelm
parents: 61503
diff changeset
   222
  convenience, any of the smaller text units conforming to @{syntax nameref}
634cd44bb1d3 symbolic syntax "\<comment> text";
wenzelm
parents: 61503
diff changeset
   223
  are admitted as well. A marginal @{syntax comment} is of the form
634cd44bb1d3 symbolic syntax "\<comment> text";
wenzelm
parents: 61503
diff changeset
   224
  \<^verbatim>\<open>--\<close>~@{syntax text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur
634cd44bb1d3 symbolic syntax "\<comment> text";
wenzelm
parents: 61503
diff changeset
   225
  within Isabelle/Isar commands.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   226
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   227
  @{rail \<open>
56499
7e0178c84994 allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents: 56451
diff changeset
   228
    @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   229
    ;
61579
634cd44bb1d3 symbolic syntax "\<comment> text";
wenzelm
parents: 61503
diff changeset
   230
    @{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   231
  \<close>}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   232
\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   233
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   234
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   235
subsection \<open>Type classes, sorts and arities\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   236
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   237
text \<open>
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   238
  Classes are specified by plain names. Sorts have a very simple inner syntax,
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   239
  which is either a single class name \<open>c\<close> or a list \<open>{c\<^sub>1, \<dots>, c\<^sub>n}\<close> referring
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   240
  to the intersection of these classes. The syntax of type arities is given
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   241
  directly at the outer level.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   242
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   243
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   244
    @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax nameref} + ','))?
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   245
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   246
    @{syntax_def sort}: @{syntax nameref}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   247
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   248
    @{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   249
  \<close>}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   250
\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   251
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   252
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   253
subsection \<open>Types and terms \label{sec:types-terms}\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   254
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   255
text \<open>
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   256
  The actual inner Isabelle syntax, that of types and terms of the logic, is
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   257
  far too sophisticated in order to be modelled explicitly at the outer theory
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   258
  level. Basically, any such entity has to be quoted to turn it into a single
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   259
  token (the parsing and type-checking is performed internally later). For
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   260
  convenience, a slightly more liberal convention is adopted: quotes may be
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   261
  omitted for any type or term that is already atomic at the outer level. For
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   262
  example, one may just write \<^verbatim>\<open>x\<close> instead of quoted \<^verbatim>\<open>"x"\<close>. Note that
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   263
  symbolic identifiers (e.g.\ \<^verbatim>\<open>++\<close> or \<open>\<forall>\<close> are available as well, provided
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   264
  these have not been superseded by commands or other keywords already (such
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   265
  as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   266
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   267
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   268
    @{syntax_def type}: @{syntax nameref} | @{syntax typefree} |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   269
      @{syntax typevar}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   270
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   271
    @{syntax_def term}: @{syntax nameref} | @{syntax var}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   272
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   273
    @{syntax_def prop}: @{syntax term}
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   274
  \<close>}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   275
59853
4039d8aecda4 more uniform syntax for named instantiations;
wenzelm
parents: 59785
diff changeset
   276
  Positional instantiations are specified as a sequence of terms, or the
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   277
  placeholder ``\<open>_\<close>'' (underscore), which means to skip a position.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   278
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   279
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   280
    @{syntax_def inst}: '_' | @{syntax term}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   281
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   282
    @{syntax_def insts}: (@{syntax inst} *)
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   283
  \<close>}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   284
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   285
  Named instantiations are specified as pairs of assignments \<open>v = t\<close>, which
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   286
  refer to schematic variables in some theorem that is instantiated. Both type
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   287
  and terms instantiations are admitted, and distinguished by the usual syntax
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   288
  of variable names.
59853
4039d8aecda4 more uniform syntax for named instantiations;
wenzelm
parents: 59785
diff changeset
   289
4039d8aecda4 more uniform syntax for named instantiations;
wenzelm
parents: 59785
diff changeset
   290
  @{rail \<open>
4039d8aecda4 more uniform syntax for named instantiations;
wenzelm
parents: 59785
diff changeset
   291
    @{syntax_def named_inst}: variable '=' (type | term)
4039d8aecda4 more uniform syntax for named instantiations;
wenzelm
parents: 59785
diff changeset
   292
    ;
4039d8aecda4 more uniform syntax for named instantiations;
wenzelm
parents: 59785
diff changeset
   293
    @{syntax_def named_insts}: (named_inst @'and' +)
4039d8aecda4 more uniform syntax for named instantiations;
wenzelm
parents: 59785
diff changeset
   294
    ;
4039d8aecda4 more uniform syntax for named instantiations;
wenzelm
parents: 59785
diff changeset
   295
    variable: @{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}
4039d8aecda4 more uniform syntax for named instantiations;
wenzelm
parents: 59785
diff changeset
   296
  \<close>}
4039d8aecda4 more uniform syntax for named instantiations;
wenzelm
parents: 59785
diff changeset
   297
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   298
  Type declarations and definitions usually refer to @{syntax typespec} on the
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   299
  left-hand side. This models basic type constructor application at the outer
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   300
  syntax level. Note that only plain postfix notation is available here, but
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   301
  no infixes.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   302
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   303
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   304
    @{syntax_def typespec}:
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   305
      (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   306
    ;
42705
528a2ba8fa74 tuned some syntax names;
wenzelm
parents: 42651
diff changeset
   307
    @{syntax_def typespec_sorts}:
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   308
      (() | (@{syntax typefree} ('::' @{syntax sort})?) |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   309
        '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   310
  \<close>}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   311
\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   312
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   313
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   314
subsection \<open>Term patterns and declarations \label{sec:term-decls}\<close>
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   315
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   316
text \<open>
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   317
  Wherever explicit propositions (or term fragments) occur in a proof text,
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   318
  casual binding of schematic term variables may be given specified via
61663
wenzelm
parents: 61662
diff changeset
   319
  patterns of the form ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>''. This works both for @{syntax
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   320
  term} and @{syntax prop}.
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   321
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   322
  @{rail \<open>
42705
528a2ba8fa74 tuned some syntax names;
wenzelm
parents: 42651
diff changeset
   323
    @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')'
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   324
    ;
42705
528a2ba8fa74 tuned some syntax names;
wenzelm
parents: 42651
diff changeset
   325
    @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')'
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   326
  \<close>}
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   327
61421
e0825405d398 more symbols;
wenzelm
parents: 61252
diff changeset
   328
  \<^medskip>
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   329
  Declarations of local variables \<open>x :: \<tau>\<close> and logical propositions \<open>a : \<phi>\<close>
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   330
  represent different views on the same principle of introducing a local
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   331
  scope. In practice, one may usually omit the typing of @{syntax vars} (due
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   332
  to type-inference), and the naming of propositions (due to implicit
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   333
  references of current facts). In any case, Isar proof elements usually admit
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   334
  to introduce multiple such items simultaneously.
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   335
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   336
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   337
    @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   338
    ;
42705
528a2ba8fa74 tuned some syntax names;
wenzelm
parents: 42651
diff changeset
   339
    @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
61658
5dce70aecbfc more documentation;
wenzelm
parents: 61656
diff changeset
   340
    ;
5dce70aecbfc more documentation;
wenzelm
parents: 61656
diff changeset
   341
    @{syntax_def props'}: (@{syntax prop} @{syntax prop_pat}? +)
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   342
  \<close>}
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   343
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   344
  The treatment of multiple declarations corresponds to the complementary
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   345
  focus of @{syntax vars} versus @{syntax props}. In ``\<open>x\<^sub>1 \<dots> x\<^sub>n :: \<tau>\<close>'' the
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   346
  typing refers to all variables, while in \<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> the naming refers to
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   347
  all propositions collectively. Isar language elements that refer to @{syntax
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   348
  vars} or @{syntax props} typically admit separate typings or namings via
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   349
  another level of iteration, with explicit @{keyword_ref "and"} separators;
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   350
  e.g.\ see @{command "fix"} and @{command "assume"} in
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   351
  \secref{sec:proof-context}.
59785
4e6ab5831cc0 clarified syntax category "fixes";
wenzelm
parents: 58861
diff changeset
   352
4e6ab5831cc0 clarified syntax category "fixes";
wenzelm
parents: 58861
diff changeset
   353
  @{rail \<open>
4e6ab5831cc0 clarified syntax category "fixes";
wenzelm
parents: 58861
diff changeset
   354
    @{syntax_def "fixes"}:
4e6ab5831cc0 clarified syntax category "fixes";
wenzelm
parents: 58861
diff changeset
   355
      ((@{syntax name} ('::' @{syntax type})? @{syntax mixfix}? | @{syntax vars}) + @'and')
4e6ab5831cc0 clarified syntax category "fixes";
wenzelm
parents: 58861
diff changeset
   356
    ;
4e6ab5831cc0 clarified syntax category "fixes";
wenzelm
parents: 58861
diff changeset
   357
    @{syntax_def "for_fixes"}: (@'for' @{syntax "fixes"})?
4e6ab5831cc0 clarified syntax category "fixes";
wenzelm
parents: 58861
diff changeset
   358
  \<close>}
4e6ab5831cc0 clarified syntax category "fixes";
wenzelm
parents: 58861
diff changeset
   359
4e6ab5831cc0 clarified syntax category "fixes";
wenzelm
parents: 58861
diff changeset
   360
  The category @{syntax "fixes"} is a richer variant of @{syntax vars}: it
4e6ab5831cc0 clarified syntax category "fixes";
wenzelm
parents: 58861
diff changeset
   361
  admits specification of mixfix syntax for the entities that are introduced
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   362
  into the context. An optional suffix ``@{keyword "for"}~\<open>fixes\<close>'' is
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   363
  admitted in many situations to indicate a so-called ``eigen-context'' of a
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   364
  formal element: the result will be exported and thus generalized over the
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   365
  given variables.
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   366
\<close>
28754
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   367
6f2e67a3dfaa moved section "Proof method expressions" to proof chapter;
wenzelm
parents: 28753
diff changeset
   368
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   369
subsection \<open>Attributes and theorems \label{sec:syn-att}\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   370
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   371
text \<open>
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   372
  Attributes have their own ``semi-inner'' syntax, in the sense that input
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   373
  conforming to @{syntax args} below is parsed by the attribute a second time.
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   374
  The attribute argument specifications may be any sequence of atomic entities
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   375
  (identifiers, strings etc.), or properly bracketed argument lists. Below
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   376
  @{syntax atom} refers to any atomic entity, including any @{syntax keyword}
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   377
  conforming to @{syntax symident}.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   378
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   379
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   380
    @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   381
      @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
55045
99056d23e05b cartouche within nested args (attributes, methods, etc.);
wenzelm
parents: 55033
diff changeset
   382
      @{syntax keyword} | @{syntax cartouche}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   383
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   384
    arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']'
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   385
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   386
    @{syntax_def args}: arg *
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   387
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   388
    @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']'
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   389
  \<close>}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   390
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   391
  Theorem specifications come in several flavors: @{syntax axmdecl} and
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   392
  @{syntax thmdecl} usually refer to axioms, assumptions or results of goal
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   393
  statements, while @{syntax thmdef} collects lists of existing theorems.
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   394
  Existing theorems are given by @{syntax thmref} and @{syntax thmrefs}, the
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   395
  former requires an actual singleton result.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   396
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   397
  There are three forms of theorem references:
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   398
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   399
    \<^enum> named facts \<open>a\<close>,
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   400
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   401
    \<^enum> selections from named facts \<open>a(i)\<close> or \<open>a(j - k)\<close>,
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   402
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   403
    \<^enum> literal fact propositions using token syntax @{syntax_ref altstring}
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   404
    \<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close> or @{syntax_ref cartouche}
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   405
    \<open>\<open>\<phi>\<close>\<close> (see also method @{method_ref fact}).
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   406
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   407
  Any kind of theorem specification may include lists of attributes both on
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   408
  the left and right hand sides; attributes are applied to any immediately
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   409
  preceding fact. If names are omitted, the theorems are not stored within the
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   410
  theorem database of the theory or proof context, but any given attributes
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   411
  are applied nonetheless.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   412
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   413
  An extra pair of brackets around attributes (like ``\<open>[[simproc a]]\<close>'')
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   414
  abbreviates a theorem reference involving an internal dummy fact, which will
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   415
  be ignored later on. So only the effect of the attribute on the background
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   416
  context will persist. This form of in-place declarations is particularly
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   417
  useful with commands like @{command "declare"} and @{command "using"}.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   418
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   419
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   420
    @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   421
    ;
60631
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60270
diff changeset
   422
    @{syntax_def thmbind}:
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60270
diff changeset
   423
      @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60270
diff changeset
   424
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   425
    @{syntax_def thmdecl}: thmbind ':'
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   426
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   427
    @{syntax_def thmdef}: thmbind '='
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   428
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   429
    @{syntax_def thmref}:
56499
7e0178c84994 allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents: 56451
diff changeset
   430
      (@{syntax nameref} selection? | @{syntax altstring} | @{syntax cartouche})
7e0178c84994 allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents: 56451
diff changeset
   431
        @{syntax attributes}? |
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   432
      '[' @{syntax attributes} ']'
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   433
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   434
    @{syntax_def thmrefs}: @{syntax thmref} +
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   435
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40296
diff changeset
   436
    selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55045
diff changeset
   437
  \<close>}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58552
diff changeset
   438
\<close>
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   439
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   440
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   441
section \<open>Diagnostic commands\<close>
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   442
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   443
text \<open>
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   444
  \begin{matharray}{rcl}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   445
    @{command_def "print_theory"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   446
    @{command_def "print_definitions"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   447
    @{command_def "print_methods"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   448
    @{command_def "print_attributes"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   449
    @{command_def "print_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   450
    @{command_def "find_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   451
    @{command_def "find_consts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   452
    @{command_def "thm_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   453
    @{command_def "unused_thms"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   454
    @{command_def "print_facts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   455
    @{command_def "print_term_bindings"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   456
  \end{matharray}
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   457
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   458
  @{rail \<open>
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   459
    (@@{command print_theory} |
61252
c165f0472d57 separate command 'print_definitions';
wenzelm
parents: 60674
diff changeset
   460
      @@{command print_definitions} |
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   461
      @@{command print_methods} |
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   462
      @@{command print_attributes} |
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   463
      @@{command print_theorems} |
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   464
      @@{command print_facts}) ('!'?)
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   465
    ;
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   466
    @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   467
    ;
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   468
    thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   469
      'solves' | 'simp' ':' @{syntax term} | @{syntax term})
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   470
    ;
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   471
    @@{command find_consts} (const_criterion*)
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   472
    ;
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   473
    const_criterion: ('-'?)
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   474
      ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   475
    ;
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   476
    @@{command thm_deps} @{syntax thmrefs}
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   477
    ;
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   478
    @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   479
  \<close>}
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   480
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   481
  These commands print certain parts of the theory and proof context. Note
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   482
  that there are some further ones available, such as for the set of rules
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   483
  declared for simplifications.
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   484
61439
2bf52eec4e8a more symbols;
wenzelm
parents: 61421
diff changeset
   485
  \<^descr> @{command "print_theory"} prints the main logical content of the
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   486
  background theory; the ``\<open>!\<close>'' option indicates extra verbosity.
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   487
61439
2bf52eec4e8a more symbols;
wenzelm
parents: 61421
diff changeset
   488
  \<^descr> @{command "print_definitions"} prints dependencies of definitional
61252
c165f0472d57 separate command 'print_definitions';
wenzelm
parents: 60674
diff changeset
   489
  specifications within the background theory, which may be constants
c165f0472d57 separate command 'print_definitions';
wenzelm
parents: 60674
diff changeset
   490
  \secref{sec:consts} or types (\secref{sec:types-pure},
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   491
  \secref{sec:hol-typedef}); the ``\<open>!\<close>'' option indicates extra verbosity.
61252
c165f0472d57 separate command 'print_definitions';
wenzelm
parents: 60674
diff changeset
   492
61439
2bf52eec4e8a more symbols;
wenzelm
parents: 61421
diff changeset
   493
  \<^descr> @{command "print_methods"} prints all proof methods available in the
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   494
  current theory context; the ``\<open>!\<close>'' option indicates extra verbosity.
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   495
61439
2bf52eec4e8a more symbols;
wenzelm
parents: 61421
diff changeset
   496
  \<^descr> @{command "print_attributes"} prints all attributes available in the
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   497
  current theory context; the ``\<open>!\<close>'' option indicates extra verbosity.
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   498
61439
2bf52eec4e8a more symbols;
wenzelm
parents: 61421
diff changeset
   499
  \<^descr> @{command "print_theorems"} prints theorems of the background theory
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   500
  resulting from the last command; the ``\<open>!\<close>'' option indicates extra
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   501
  verbosity.
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   502
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   503
  \<^descr> @{command "print_facts"} prints all local facts of the current context,
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   504
  both named and unnamed ones; the ``\<open>!\<close>'' option indicates extra verbosity.
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   505
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   506
  \<^descr> @{command "print_term_bindings"} prints all term bindings that are present
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   507
  in the context.
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   508
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   509
  \<^descr> @{command "find_theorems"}~\<open>criteria\<close> retrieves facts from the theory or
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   510
  proof context matching all of given search criteria. The criterion \<open>name: p\<close>
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   511
  selects all theorems whose fully qualified name matches pattern \<open>p\<close>, which
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   512
  may contain ``\<open>*\<close>'' wildcards. The criteria \<open>intro\<close>, \<open>elim\<close>, and \<open>dest\<close>
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   513
  select theorems that match the current goal as introduction, elimination or
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   514
  destruction rules, respectively. The criterion \<open>solves\<close> returns all rules
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   515
  that would directly solve the current goal. The criterion \<open>simp: t\<close> selects
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   516
  all rewrite rules whose left-hand side matches the given term. The criterion
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   517
  term \<open>t\<close> selects all theorems that contain the pattern \<open>t\<close> -- as usual,
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   518
  patterns may contain occurrences of the dummy ``\<open>_\<close>'', schematic variables,
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   519
  and type constraints.
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   520
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   521
  Criteria can be preceded by ``\<open>-\<close>'' to select theorems that do \<^emph>\<open>not\<close> match.
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   522
  Note that giving the empty list of criteria yields \<^emph>\<open>all\<close> currently known
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   523
  facts. An optional limit for the number of printed facts may be given; the
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   524
  default is 40. By default, duplicates are removed from the search result.
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   525
  Use \<open>with_dups\<close> to display duplicates.
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   526
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   527
  \<^descr> @{command "find_consts"}~\<open>criteria\<close> prints all constants whose type meets
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   528
  all of the given criteria. The criterion \<open>strict: ty\<close> is met by any type
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   529
  that matches the type pattern \<open>ty\<close>. Patterns may contain both the dummy type
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   530
  ``\<open>_\<close>'' and sort constraints. The criterion \<open>ty\<close> is similar, but it also
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   531
  matches against subtypes. The criterion \<open>name: p\<close> and the prefix ``\<open>-\<close>''
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   532
  function as described for @{command "find_theorems"}.
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   533
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   534
  \<^descr> @{command "thm_deps"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> visualizes dependencies of facts, using
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   535
  Isabelle's graph browser tool (see also @{cite "isabelle-system"}).
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   536
61662
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   537
  \<^descr> @{command "unused_thms"}~\<open>A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n\<close> displays all theorems
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   538
  that are proved in theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close> or their parents but not in \<open>A\<^sub>1 \<dots>
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   539
  A\<^sub>m\<close> or their parents and that are never used. If \<open>n\<close> is \<open>0\<close>, the end of the
e77def9a63a6 tuned whitespace;
wenzelm
parents: 61658
diff changeset
   540
  range of theories defaults to the current theory. If no range is specified,
60674
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   541
  only the unused theorems in the current theory are displayed.
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   542
\<close>
2f66099fb472 clarified sections;
wenzelm
parents: 60631
diff changeset
   543
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   544
end