99 \<^medskip> |
99 \<^medskip> |
100 The categories for named tokens are defined once and for all as follows. |
100 The categories for named tokens are defined once and for all as follows. |
101 |
101 |
102 \begin{center} |
102 \begin{center} |
103 \begin{supertabular}{rcl} |
103 \begin{supertabular}{rcl} |
104 @{syntax_def ident} & = & @{text "letter (subscript\<^sup>? quasiletter)\<^sup>*"} \\ |
104 @{syntax_def ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\ |
105 @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\ |
105 @{syntax_def longident} & = & \<open>ident(\<close>@{verbatim "."}\<open>ident)\<^sup>+\<close> \\ |
106 @{syntax_def symident} & = & @{text "sym\<^sup>+ | "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text ident}@{verbatim ">"} \\ |
106 @{syntax_def symident} & = & \<open>sym\<^sup>+ | \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>ident\<close>@{verbatim ">"} \\ |
107 @{syntax_def nat} & = & @{text "digit\<^sup>+"} \\ |
107 @{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\ |
108 @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ |
108 @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}\<open> | \<close>@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ |
109 @{syntax_def var} & = & @{verbatim "?"}@{text "ident | "}@{verbatim "?"}@{text ident}@{verbatim "."}@{text nat} \\ |
109 @{syntax_def var} & = & @{verbatim "?"}\<open>ident | \<close>@{verbatim "?"}\<open>ident\<close>@{verbatim "."}\<open>nat\<close> \\ |
110 @{syntax_def typefree} & = & @{verbatim "'"}@{text ident} \\ |
110 @{syntax_def typefree} & = & @{verbatim "'"}\<open>ident\<close> \\ |
111 @{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree | "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\ |
111 @{syntax_def typevar} & = & @{verbatim "?"}\<open>typefree | \<close>@{verbatim "?"}\<open>typefree\<close>@{verbatim "."}\<open>nat\<close> \\ |
112 @{syntax_def string} & = & @{verbatim \<open>"\<close>} @{text "\<dots>"} @{verbatim \<open>"\<close>} \\ |
112 @{syntax_def string} & = & @{verbatim \<open>"\<close>} \<open>\<dots>\<close> @{verbatim \<open>"\<close>} \\ |
113 @{syntax_def altstring} & = & @{verbatim "`"} @{text "\<dots>"} @{verbatim "`"} \\ |
113 @{syntax_def altstring} & = & @{verbatim "`"} \<open>\<dots>\<close> @{verbatim "`"} \\ |
114 @{syntax_def cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\ |
114 @{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\ |
115 @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*}"} \\[1ex] |
115 @{syntax_def verbatim} & = & @{verbatim "{*"} \<open>\<dots>\<close> @{verbatim "*}"} \\[1ex] |
116 |
116 |
117 @{text letter} & = & @{text "latin | "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text " | "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text " | greek |"} \\ |
117 \<open>letter\<close> & = & \<open>latin | \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin\<close>@{verbatim ">"}\<open> | \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin latin\<close>@{verbatim ">"}\<open> | greek |\<close> \\ |
118 @{text subscript} & = & @{verbatim "\<^sub>"} \\ |
118 \<open>subscript\<close> & = & @{verbatim "\<^sub>"} \\ |
119 @{text quasiletter} & = & @{text "letter | digit | "}@{verbatim "_"}@{text " | "}@{verbatim "'"} \\ |
119 \<open>quasiletter\<close> & = & \<open>letter | digit | \<close>@{verbatim "_"}\<open> | \<close>@{verbatim "'"} \\ |
120 @{text latin} & = & @{verbatim a}@{text " | \<dots> | "}@{verbatim z}@{text " | "}@{verbatim A}@{text " | \<dots> | "}@{verbatim Z} \\ |
120 \<open>latin\<close> & = & @{verbatim a}\<open> | \<dots> | \<close>@{verbatim z}\<open> | \<close>@{verbatim A}\<open> | \<dots> | \<close>@{verbatim Z} \\ |
121 @{text digit} & = & @{verbatim "0"}@{text " | \<dots> | "}@{verbatim "9"} \\ |
121 \<open>digit\<close> & = & @{verbatim "0"}\<open> | \<dots> | \<close>@{verbatim "9"} \\ |
122 @{text sym} & = & @{verbatim "!"}@{text " | "}@{verbatim "#"}@{text " | "}@{verbatim "$"}@{text " | "}@{verbatim "%"}@{text " | "}@{verbatim "&"}@{text " | "}@{verbatim "*"}@{text " | "}@{verbatim "+"}@{text " | "}@{verbatim "-"}@{text " | "}@{verbatim "/"}@{text " |"} \\ |
122 \<open>sym\<close> & = & @{verbatim "!"}\<open> | \<close>@{verbatim "#"}\<open> | \<close>@{verbatim "$"}\<open> | \<close>@{verbatim "%"}\<open> | \<close>@{verbatim "&"}\<open> | \<close>@{verbatim "*"}\<open> | \<close>@{verbatim "+"}\<open> | \<close>@{verbatim "-"}\<open> | \<close>@{verbatim "/"}\<open> |\<close> \\ |
123 & & @{verbatim "<"}@{text " | "}@{verbatim "="}@{text " | "}@{verbatim ">"}@{text " | "}@{verbatim "?"}@{text " | "}@{verbatim "@"}@{text " | "}@{verbatim "^"}@{text " | "}@{verbatim "_"}@{text " | "}@{verbatim "|"}@{text " | "}@{verbatim "~"} \\ |
123 & & @{verbatim "<"}\<open> | \<close>@{verbatim "="}\<open> | \<close>@{verbatim ">"}\<open> | \<close>@{verbatim "?"}\<open> | \<close>@{verbatim "@"}\<open> | \<close>@{verbatim "^"}\<open> | \<close>@{verbatim "_"}\<open> | \<close>@{verbatim "|"}\<open> | \<close>@{verbatim "~"} \\ |
124 @{text greek} & = & @{verbatim "\<alpha>"}@{text " | "}@{verbatim "\<beta>"}@{text " | "}@{verbatim "\<gamma>"}@{text " | "}@{verbatim "\<delta>"}@{text " |"} \\ |
124 \<open>greek\<close> & = & @{verbatim "\<alpha>"}\<open> | \<close>@{verbatim "\<beta>"}\<open> | \<close>@{verbatim "\<gamma>"}\<open> | \<close>@{verbatim "\<delta>"}\<open> |\<close> \\ |
125 & & @{verbatim "\<epsilon>"}@{text " | "}@{verbatim "\<zeta>"}@{text " | "}@{verbatim "\<eta>"}@{text " | "}@{verbatim "\<theta>"}@{text " |"} \\ |
125 & & @{verbatim "\<epsilon>"}\<open> | \<close>@{verbatim "\<zeta>"}\<open> | \<close>@{verbatim "\<eta>"}\<open> | \<close>@{verbatim "\<theta>"}\<open> |\<close> \\ |
126 & & @{verbatim "\<iota>"}@{text " | "}@{verbatim "\<kappa>"}@{text " | "}@{verbatim "\<mu>"}@{text " | "}@{verbatim "\<nu>"}@{text " |"} \\ |
126 & & @{verbatim "\<iota>"}\<open> | \<close>@{verbatim "\<kappa>"}\<open> | \<close>@{verbatim "\<mu>"}\<open> | \<close>@{verbatim "\<nu>"}\<open> |\<close> \\ |
127 & & @{verbatim "\<xi>"}@{text " | "}@{verbatim "\<pi>"}@{text " | "}@{verbatim "\<rho>"}@{text " | "}@{verbatim "\<sigma>"}@{text " | "}@{verbatim "\<tau>"}@{text " |"} \\ |
127 & & @{verbatim "\<xi>"}\<open> | \<close>@{verbatim "\<pi>"}\<open> | \<close>@{verbatim "\<rho>"}\<open> | \<close>@{verbatim "\<sigma>"}\<open> | \<close>@{verbatim "\<tau>"}\<open> |\<close> \\ |
128 & & @{verbatim "\<upsilon>"}@{text " | "}@{verbatim "\<phi>"}@{text " | "}@{verbatim "\<chi>"}@{text " | "}@{verbatim "\<psi>"}@{text " |"} \\ |
128 & & @{verbatim "\<upsilon>"}\<open> | \<close>@{verbatim "\<phi>"}\<open> | \<close>@{verbatim "\<chi>"}\<open> | \<close>@{verbatim "\<psi>"}\<open> |\<close> \\ |
129 & & @{verbatim "\<omega>"}@{text " | "}@{verbatim "\<Gamma>"}@{text " | "}@{verbatim "\<Delta>"}@{text " | "}@{verbatim "\<Theta>"}@{text " |"} \\ |
129 & & @{verbatim "\<omega>"}\<open> | \<close>@{verbatim "\<Gamma>"}\<open> | \<close>@{verbatim "\<Delta>"}\<open> | \<close>@{verbatim "\<Theta>"}\<open> |\<close> \\ |
130 & & @{verbatim "\<Lambda>"}@{text " | "}@{verbatim "\<Xi>"}@{text " | "}@{verbatim "\<Pi>"}@{text " | "}@{verbatim "\<Sigma>"}@{text " |"} \\ |
130 & & @{verbatim "\<Lambda>"}\<open> | \<close>@{verbatim "\<Xi>"}\<open> | \<close>@{verbatim "\<Pi>"}\<open> | \<close>@{verbatim "\<Sigma>"}\<open> |\<close> \\ |
131 & & @{verbatim "\<Upsilon>"}@{text " | "}@{verbatim "\<Phi>"}@{text " | "}@{verbatim "\<Psi>"}@{text " | "}@{verbatim "\<Omega>"} \\ |
131 & & @{verbatim "\<Upsilon>"}\<open> | \<close>@{verbatim "\<Phi>"}\<open> | \<close>@{verbatim "\<Psi>"}\<open> | \<close>@{verbatim "\<Omega>"} \\ |
132 \end{supertabular} |
132 \end{supertabular} |
133 \end{center} |
133 \end{center} |
134 |
134 |
135 A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown, |
135 A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown, |
136 which is internally a pair of base name and index (ML type @{ML_type |
136 which is internally a pair of base name and index (ML type @{ML_type |
137 indexname}). These components are either separated by a dot as in |
137 indexname}). These components are either separated by a dot as in |
138 @{text "?x.1"} or @{text "?x7.3"} or run together as in @{text |
138 \<open>?x.1\<close> or \<open>?x7.3\<close> or run together as in \<open>?x1\<close>. The latter form is possible if the base name does not end |
139 "?x1"}. The latter form is possible if the base name does not end |
|
140 with digits. If the index is 0, it may be dropped altogether: |
139 with digits. If the index is 0, it may be dropped altogether: |
141 @{text "?x"} and @{text "?x0"} and @{text "?x.0"} all refer to the |
140 \<open>?x\<close> and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the |
142 same unknown, with basename @{text "x"} and index 0. |
141 same unknown, with basename \<open>x\<close> and index 0. |
143 |
142 |
144 The syntax of @{syntax_ref string} admits any characters, including |
143 The syntax of @{syntax_ref string} admits any characters, including |
145 newlines; ``@{verbatim \<open>"\<close>}'' (double-quote) and ``@{verbatim \<open>\\<close>}'' |
144 newlines; ``@{verbatim \<open>"\<close>}'' (double-quote) and ``@{verbatim \<open>\\<close>}'' |
146 (backslash) need to be escaped by a backslash; arbitrary |
145 (backslash) need to be escaped by a backslash; arbitrary |
147 character codes may be specified as ``@{verbatim \<open>\\<close>}@{text ddd}'', |
146 character codes may be specified as ``@{verbatim \<open>\\<close>}\<open>ddd\<close>'', |
148 with three decimal digits. Alternative strings according to |
147 with three decimal digits. Alternative strings according to |
149 @{syntax_ref altstring} are analogous, using single back-quotes |
148 @{syntax_ref altstring} are analogous, using single back-quotes |
150 instead. |
149 instead. |
151 |
150 |
152 The body of @{syntax_ref verbatim} may consist of any text not containing |
151 The body of @{syntax_ref verbatim} may consist of any text not containing |
153 ``@{verbatim "*}"}''; this allows to include quotes without further |
152 ``@{verbatim "*}"}''; this allows to include quotes without further |
154 escapes, but there is no way to escape ``@{verbatim "*}"}''. Cartouches |
153 escapes, but there is no way to escape ``@{verbatim "*}"}''. Cartouches |
155 do not have this limitation. |
154 do not have this limitation. |
156 |
155 |
157 A @{syntax_ref cartouche} consists of arbitrary text, with properly |
156 A @{syntax_ref cartouche} consists of arbitrary text, with properly |
158 balanced blocks of ``@{verbatim "\<open>"}~@{text "\<dots>"}~@{verbatim |
157 balanced blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim |
159 "\<close>"}''. Note that the rendering of cartouche delimiters is |
158 "\<close>"}''. Note that the rendering of cartouche delimiters is |
160 usually like this: ``@{text "\<open> \<dots> \<close>"}''. |
159 usually like this: ``\<open>\<open> \<dots> \<close>\<close>''. |
161 |
160 |
162 Source comments take the form @{verbatim "(*"}~@{text |
161 Source comments take the form @{verbatim "(*"}~\<open>\<dots>\<close>~@{verbatim "*)"} and may be nested, although the user-interface |
163 "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface |
|
164 might prevent this. Note that this form indicates source comments |
162 might prevent this. Note that this form indicates source comments |
165 only, which are stripped after lexical analysis of the input. The |
163 only, which are stripped after lexical analysis of the input. The |
166 Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are |
164 Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are |
167 considered as part of the text (see \secref{sec:comments}). |
165 considered as part of the text (see \secref{sec:comments}). |
168 |
166 |
169 Common mathematical symbols such as @{text \<forall>} are represented in |
167 Common mathematical symbols such as \<open>\<forall>\<close> are represented in |
170 Isabelle as @{verbatim \<forall>}. There are infinitely many Isabelle |
168 Isabelle as @{verbatim \<forall>}. There are infinitely many Isabelle |
171 symbols like this, although proper presentation is left to front-end |
169 symbols like this, although proper presentation is left to front-end |
172 tools such as {\LaTeX} or Isabelle/jEdit. A list of |
170 tools such as {\LaTeX} or Isabelle/jEdit. A list of |
173 predefined Isabelle symbols that work well with these tools is given |
171 predefined Isabelle symbols that work well with these tools is given |
174 in \appref{app:symbols}. Note that @{verbatim "\<lambda>"} does not belong |
172 in \appref{app:symbols}. Note that @{verbatim "\<lambda>"} does not belong |
175 to the @{text letter} category, since it is already used differently |
173 to the \<open>letter\<close> category, since it is already used differently |
176 in the Pure term language.\<close> |
174 in the Pure term language.\<close> |
177 |
175 |
178 |
176 |
179 section \<open>Common syntax entities\<close> |
177 section \<open>Common syntax entities\<close> |
180 |
178 |
404 and @{syntax thmrefs}, the former requires an actual singleton |
401 and @{syntax thmrefs}, the former requires an actual singleton |
405 result. |
402 result. |
406 |
403 |
407 There are three forms of theorem references: |
404 There are three forms of theorem references: |
408 |
405 |
409 \<^enum> named facts @{text "a"}, |
406 \<^enum> named facts \<open>a\<close>, |
410 |
407 |
411 \<^enum> selections from named facts @{text "a(i)"} or @{text "a(j - k)"}, |
408 \<^enum> selections from named facts \<open>a(i)\<close> or \<open>a(j - k)\<close>, |
412 |
409 |
413 \<^enum> literal fact propositions using token syntax @{syntax_ref altstring} |
410 \<^enum> literal fact propositions using token syntax @{syntax_ref altstring} |
414 @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} or @{syntax_ref cartouche} |
411 @{verbatim "`"}\<open>\<phi>\<close>@{verbatim "`"} or @{syntax_ref cartouche} |
415 @{text "\<open>\<phi>\<close>"} (see also method @{method_ref fact}). |
412 \<open>\<open>\<phi>\<close>\<close> (see also method @{method_ref fact}). |
416 |
413 |
417 |
414 |
418 Any kind of theorem specification may include lists of attributes |
415 Any kind of theorem specification may include lists of attributes |
419 both on the left and right hand sides; attributes are applied to any |
416 both on the left and right hand sides; attributes are applied to any |
420 immediately preceding fact. If names are omitted, the theorems are |
417 immediately preceding fact. If names are omitted, the theorems are |
421 not stored within the theorem database of the theory or proof |
418 not stored within the theorem database of the theory or proof |
422 context, but any given attributes are applied nonetheless. |
419 context, but any given attributes are applied nonetheless. |
423 |
420 |
424 An extra pair of brackets around attributes (like ``@{text |
421 An extra pair of brackets around attributes (like ``\<open>[[simproc a]]\<close>'') abbreviates a theorem reference involving an |
425 "[[simproc a]]"}'') abbreviates a theorem reference involving an |
|
426 internal dummy fact, which will be ignored later on. So only the |
422 internal dummy fact, which will be ignored later on. So only the |
427 effect of the attribute on the background context will persist. |
423 effect of the attribute on the background context will persist. |
428 This form of in-place declarations is particularly useful with |
424 This form of in-place declarations is particularly useful with |
429 commands like @{command "declare"} and @{command "using"}. |
425 commands like @{command "declare"} and @{command "using"}. |
430 |
426 |
452 |
448 |
453 section \<open>Diagnostic commands\<close> |
449 section \<open>Diagnostic commands\<close> |
454 |
450 |
455 text \<open> |
451 text \<open> |
456 \begin{matharray}{rcl} |
452 \begin{matharray}{rcl} |
457 @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
453 @{command_def "print_theory"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
458 @{command_def "print_definitions"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
454 @{command_def "print_definitions"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
459 @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
455 @{command_def "print_methods"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
460 @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
456 @{command_def "print_attributes"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
461 @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
457 @{command_def "print_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
462 @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
458 @{command_def "find_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
463 @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
459 @{command_def "find_consts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
464 @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
460 @{command_def "thm_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
465 @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
461 @{command_def "unused_thms"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
466 @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
462 @{command_def "print_facts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
467 @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
463 @{command_def "print_term_bindings"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
468 \end{matharray} |
464 \end{matharray} |
469 |
465 |
470 @{rail \<open> |
466 @{rail \<open> |
471 (@@{command print_theory} | |
467 (@@{command print_theory} | |
472 @@{command print_definitions} | |
468 @@{command print_definitions} | |
493 These commands print certain parts of the theory and proof context. |
489 These commands print certain parts of the theory and proof context. |
494 Note that there are some further ones available, such as for the set |
490 Note that there are some further ones available, such as for the set |
495 of rules declared for simplifications. |
491 of rules declared for simplifications. |
496 |
492 |
497 \<^descr> @{command "print_theory"} prints the main logical content of the |
493 \<^descr> @{command "print_theory"} prints the main logical content of the |
498 background theory; the ``@{text "!"}'' option indicates extra verbosity. |
494 background theory; the ``\<open>!\<close>'' option indicates extra verbosity. |
499 |
495 |
500 \<^descr> @{command "print_definitions"} prints dependencies of definitional |
496 \<^descr> @{command "print_definitions"} prints dependencies of definitional |
501 specifications within the background theory, which may be constants |
497 specifications within the background theory, which may be constants |
502 \secref{sec:consts} or types (\secref{sec:types-pure}, |
498 \secref{sec:consts} or types (\secref{sec:types-pure}, |
503 \secref{sec:hol-typedef}); the ``@{text "!"}'' option indicates extra |
499 \secref{sec:hol-typedef}); the ``\<open>!\<close>'' option indicates extra |
504 verbosity. |
500 verbosity. |
505 |
501 |
506 \<^descr> @{command "print_methods"} prints all proof methods available in the |
502 \<^descr> @{command "print_methods"} prints all proof methods available in the |
507 current theory context; the ``@{text "!"}'' option indicates extra |
503 current theory context; the ``\<open>!\<close>'' option indicates extra |
508 verbosity. |
504 verbosity. |
509 |
505 |
510 \<^descr> @{command "print_attributes"} prints all attributes available in the |
506 \<^descr> @{command "print_attributes"} prints all attributes available in the |
511 current theory context; the ``@{text "!"}'' option indicates extra |
507 current theory context; the ``\<open>!\<close>'' option indicates extra |
512 verbosity. |
508 verbosity. |
513 |
509 |
514 \<^descr> @{command "print_theorems"} prints theorems of the background theory |
510 \<^descr> @{command "print_theorems"} prints theorems of the background theory |
515 resulting from the last command; the ``@{text "!"}'' option indicates |
511 resulting from the last command; the ``\<open>!\<close>'' option indicates |
516 extra verbosity. |
512 extra verbosity. |
517 |
513 |
518 \<^descr> @{command "print_facts"} prints all local facts of the current |
514 \<^descr> @{command "print_facts"} prints all local facts of the current |
519 context, both named and unnamed ones; the ``@{text "!"}'' option indicates |
515 context, both named and unnamed ones; the ``\<open>!\<close>'' option indicates |
520 extra verbosity. |
516 extra verbosity. |
521 |
517 |
522 \<^descr> @{command "print_term_bindings"} prints all term bindings that |
518 \<^descr> @{command "print_term_bindings"} prints all term bindings that |
523 are present in the context. |
519 are present in the context. |
524 |
520 |
525 \<^descr> @{command "find_theorems"}~@{text criteria} retrieves facts |
521 \<^descr> @{command "find_theorems"}~\<open>criteria\<close> retrieves facts |
526 from the theory or proof context matching all of given search |
522 from the theory or proof context matching all of given search |
527 criteria. The criterion @{text "name: p"} selects all theorems |
523 criteria. The criterion \<open>name: p\<close> selects all theorems |
528 whose fully qualified name matches pattern @{text p}, which may |
524 whose fully qualified name matches pattern \<open>p\<close>, which may |
529 contain ``@{text "*"}'' wildcards. The criteria @{text intro}, |
525 contain ``\<open>*\<close>'' wildcards. The criteria \<open>intro\<close>, |
530 @{text elim}, and @{text dest} select theorems that match the |
526 \<open>elim\<close>, and \<open>dest\<close> select theorems that match the |
531 current goal as introduction, elimination or destruction rules, |
527 current goal as introduction, elimination or destruction rules, |
532 respectively. The criterion @{text "solves"} returns all rules |
528 respectively. The criterion \<open>solves\<close> returns all rules |
533 that would directly solve the current goal. The criterion |
529 that would directly solve the current goal. The criterion |
534 @{text "simp: t"} selects all rewrite rules whose left-hand side |
530 \<open>simp: t\<close> selects all rewrite rules whose left-hand side |
535 matches the given term. The criterion term @{text t} selects all |
531 matches the given term. The criterion term \<open>t\<close> selects all |
536 theorems that contain the pattern @{text t} -- as usual, patterns |
532 theorems that contain the pattern \<open>t\<close> -- as usual, patterns |
537 may contain occurrences of the dummy ``@{text _}'', schematic |
533 may contain occurrences of the dummy ``\<open>_\<close>'', schematic |
538 variables, and type constraints. |
534 variables, and type constraints. |
539 |
535 |
540 Criteria can be preceded by ``@{text "-"}'' to select theorems that |
536 Criteria can be preceded by ``\<open>-\<close>'' to select theorems that |
541 do \<^emph>\<open>not\<close> match. Note that giving the empty list of criteria |
537 do \<^emph>\<open>not\<close> match. Note that giving the empty list of criteria |
542 yields \<^emph>\<open>all\<close> currently known facts. An optional limit for the |
538 yields \<^emph>\<open>all\<close> currently known facts. An optional limit for the |
543 number of printed facts may be given; the default is 40. By |
539 number of printed facts may be given; the default is 40. By |
544 default, duplicates are removed from the search result. Use |
540 default, duplicates are removed from the search result. Use |
545 @{text with_dups} to display duplicates. |
541 \<open>with_dups\<close> to display duplicates. |
546 |
542 |
547 \<^descr> @{command "find_consts"}~@{text criteria} prints all constants |
543 \<^descr> @{command "find_consts"}~\<open>criteria\<close> prints all constants |
548 whose type meets all of the given criteria. The criterion @{text |
544 whose type meets all of the given criteria. The criterion \<open>strict: ty\<close> is met by any type that matches the type pattern |
549 "strict: ty"} is met by any type that matches the type pattern |
545 \<open>ty\<close>. Patterns may contain both the dummy type ``\<open>_\<close>'' |
550 @{text ty}. Patterns may contain both the dummy type ``@{text _}'' |
546 and sort constraints. The criterion \<open>ty\<close> is similar, but it |
551 and sort constraints. The criterion @{text ty} is similar, but it |
547 also matches against subtypes. The criterion \<open>name: p\<close> and |
552 also matches against subtypes. The criterion @{text "name: p"} and |
548 the prefix ``\<open>-\<close>'' function as described for @{command |
553 the prefix ``@{text "-"}'' function as described for @{command |
|
554 "find_theorems"}. |
549 "find_theorems"}. |
555 |
550 |
556 \<^descr> @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} |
551 \<^descr> @{command "thm_deps"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> |
557 visualizes dependencies of facts, using Isabelle's graph browser |
552 visualizes dependencies of facts, using Isabelle's graph browser |
558 tool (see also @{cite "isabelle-system"}). |
553 tool (see also @{cite "isabelle-system"}). |
559 |
554 |
560 \<^descr> @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"} |
555 \<^descr> @{command "unused_thms"}~\<open>A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n\<close> |
561 displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"} |
556 displays all theorems that are proved in theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close> |
562 or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and |
557 or their parents but not in \<open>A\<^sub>1 \<dots> A\<^sub>m\<close> or their parents and |
563 that are never used. |
558 that are never used. |
564 If @{text n} is @{text 0}, the end of the range of theories |
559 If \<open>n\<close> is \<open>0\<close>, the end of the range of theories |
565 defaults to the current theory. If no range is specified, |
560 defaults to the current theory. If no range is specified, |
566 only the unused theorems in the current theory are displayed. |
561 only the unused theorems in the current theory are displayed. |
567 \<close> |
562 \<close> |
568 |
563 |
569 end |
564 end |