wenzelm@27056
|
1 |
theory Misc
|
wenzelm@27056
|
2 |
imports Main
|
wenzelm@27056
|
3 |
begin
|
wenzelm@27056
|
4 |
|
wenzelm@28779
|
5 |
chapter {* Other commands *}
|
wenzelm@27056
|
6 |
|
wenzelm@27056
|
7 |
section {* Inspecting the context *}
|
wenzelm@27056
|
8 |
|
wenzelm@27056
|
9 |
text {*
|
wenzelm@27056
|
10 |
\begin{matharray}{rcl}
|
wenzelm@28761
|
11 |
@{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
|
wenzelm@28761
|
12 |
@{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28761
|
13 |
@{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28761
|
14 |
@{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28761
|
15 |
@{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28761
|
16 |
@{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
kleing@29831
|
17 |
@{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28761
|
18 |
@{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28761
|
19 |
@{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28761
|
20 |
@{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@27056
|
21 |
\end{matharray}
|
wenzelm@27056
|
22 |
|
wenzelm@27056
|
23 |
\begin{rail}
|
wenzelm@33515
|
24 |
('print\_theory' | 'print\_theorems') ('!'?)
|
wenzelm@27056
|
25 |
;
|
wenzelm@27056
|
26 |
|
kleing@29831
|
27 |
'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
|
wenzelm@27056
|
28 |
;
|
kleing@29831
|
29 |
thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
|
kleing@29830
|
30 |
'solves' | 'simp' ':' term | term)
|
wenzelm@27056
|
31 |
;
|
kleing@29831
|
32 |
'find\_consts' (constcriterion *)
|
kleing@29831
|
33 |
;
|
kleing@29831
|
34 |
constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
|
kleing@29831
|
35 |
;
|
wenzelm@27056
|
36 |
'thm\_deps' thmrefs
|
wenzelm@27056
|
37 |
;
|
wenzelm@27056
|
38 |
\end{rail}
|
wenzelm@27056
|
39 |
|
wenzelm@27056
|
40 |
These commands print certain parts of the theory and proof context.
|
wenzelm@27056
|
41 |
Note that there are some further ones available, such as for the set
|
wenzelm@27056
|
42 |
of rules declared for simplifications.
|
wenzelm@27056
|
43 |
|
wenzelm@28760
|
44 |
\begin{description}
|
wenzelm@27056
|
45 |
|
wenzelm@28760
|
46 |
\item @{command "print_commands"} prints Isabelle's outer theory
|
wenzelm@27056
|
47 |
syntax, including keywords and command.
|
wenzelm@27056
|
48 |
|
wenzelm@28760
|
49 |
\item @{command "print_theory"} prints the main logical content of
|
wenzelm@27056
|
50 |
the theory context; the ``@{text "!"}'' option indicates extra
|
wenzelm@27056
|
51 |
verbosity.
|
wenzelm@27056
|
52 |
|
wenzelm@28760
|
53 |
\item @{command "print_methods"} prints all proof methods
|
wenzelm@27056
|
54 |
available in the current theory context.
|
wenzelm@27056
|
55 |
|
wenzelm@28760
|
56 |
\item @{command "print_attributes"} prints all attributes
|
wenzelm@27056
|
57 |
available in the current theory context.
|
wenzelm@27056
|
58 |
|
wenzelm@33515
|
59 |
\item @{command "print_theorems"} prints theorems resulting from the
|
wenzelm@33515
|
60 |
last command; the ``@{text "!"}'' option indicates extra verbosity.
|
wenzelm@27056
|
61 |
|
wenzelm@28760
|
62 |
\item @{command "find_theorems"}~@{text criteria} retrieves facts
|
wenzelm@27056
|
63 |
from the theory or proof context matching all of given search
|
wenzelm@27056
|
64 |
criteria. The criterion @{text "name: p"} selects all theorems
|
wenzelm@27056
|
65 |
whose fully qualified name matches pattern @{text p}, which may
|
wenzelm@27056
|
66 |
contain ``@{text "*"}'' wildcards. The criteria @{text intro},
|
wenzelm@27056
|
67 |
@{text elim}, and @{text dest} select theorems that match the
|
wenzelm@27056
|
68 |
current goal as introduction, elimination or destruction rules,
|
kleing@29833
|
69 |
respectively. The criterion @{text "solves"} returns all rules
|
kleing@29830
|
70 |
that would directly solve the current goal. The criterion
|
kleing@29830
|
71 |
@{text "simp: t"} selects all rewrite rules whose left-hand side
|
kleing@29830
|
72 |
matches the given term. The criterion term @{text t} selects all
|
kleing@29830
|
73 |
theorems that contain the pattern @{text t} -- as usual, patterns
|
kleing@29830
|
74 |
may contain occurrences of the dummy ``@{text _}'', schematic
|
kleing@29830
|
75 |
variables, and type constraints.
|
wenzelm@27056
|
76 |
|
wenzelm@27056
|
77 |
Criteria can be preceded by ``@{text "-"}'' to select theorems that
|
wenzelm@27056
|
78 |
do \emph{not} match. Note that giving the empty list of criteria
|
wenzelm@27056
|
79 |
yields \emph{all} currently known facts. An optional limit for the
|
wenzelm@27056
|
80 |
number of printed facts may be given; the default is 40. By
|
wenzelm@27056
|
81 |
default, duplicates are removed from the search result. Use
|
wenzelm@27056
|
82 |
@{text with_dups} to display duplicates.
|
kleing@29831
|
83 |
|
kleing@29831
|
84 |
\item @{command "find_consts"}~@{text criteria} prints all constants
|
kleing@29831
|
85 |
whose type meets all of the given criteria. The criterion @{text
|
kleing@29831
|
86 |
"strict: ty"} is met by any type that matches the type pattern
|
kleing@29831
|
87 |
@{text ty}. Patterns may contain both the dummy type ``@{text _}''
|
kleing@29831
|
88 |
and sort constraints. The criterion @{text ty} is similar, but it
|
kleing@29831
|
89 |
also matches against subtypes. The criterion @{text "name: p"} and
|
kleing@29831
|
90 |
the prefix ``@{text "-"}'' function as described for @{command
|
kleing@29831
|
91 |
"find_theorems"}.
|
kleing@29831
|
92 |
|
wenzelm@28760
|
93 |
\item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
|
wenzelm@27056
|
94 |
visualizes dependencies of facts, using Isabelle's graph browser
|
wenzelm@27056
|
95 |
tool (see also \cite{isabelle-sys}).
|
wenzelm@27056
|
96 |
|
wenzelm@28760
|
97 |
\item @{command "print_facts"} prints all local facts of the
|
wenzelm@27056
|
98 |
current context, both named and unnamed ones.
|
wenzelm@27056
|
99 |
|
wenzelm@28760
|
100 |
\item @{command "print_binds"} prints all term abbreviations
|
wenzelm@27056
|
101 |
present in the context.
|
wenzelm@27056
|
102 |
|
wenzelm@28760
|
103 |
\end{description}
|
wenzelm@27056
|
104 |
*}
|
wenzelm@27056
|
105 |
|
wenzelm@27056
|
106 |
|
wenzelm@27056
|
107 |
section {* History commands \label{sec:history} *}
|
wenzelm@27056
|
108 |
|
wenzelm@27056
|
109 |
text {*
|
wenzelm@27056
|
110 |
\begin{matharray}{rcl}
|
wenzelm@28761
|
111 |
@{command_def "undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
|
wenzelm@28761
|
112 |
@{command_def "linear_undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
|
wenzelm@28761
|
113 |
@{command_def "kill"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
|
wenzelm@27056
|
114 |
\end{matharray}
|
wenzelm@27056
|
115 |
|
wenzelm@27056
|
116 |
The Isabelle/Isar top-level maintains a two-stage history, for
|
wenzelm@27056
|
117 |
theory and proof state transformation. Basically, any command can
|
wenzelm@27056
|
118 |
be undone using @{command "undo"}, excluding mere diagnostic
|
wenzelm@27598
|
119 |
elements. Note that a theorem statement with a \emph{finished}
|
wenzelm@27598
|
120 |
proof is treated as a single unit by @{command "undo"}. In
|
wenzelm@27598
|
121 |
contrast, the variant @{command "linear_undo"} admits to step back
|
wenzelm@27598
|
122 |
into the middle of a proof. The @{command "kill"} command aborts
|
wenzelm@27598
|
123 |
the current history node altogether, discontinuing a proof or even
|
wenzelm@27598
|
124 |
the whole theory. This operation is \emph{not} undo-able.
|
wenzelm@27056
|
125 |
|
wenzelm@27056
|
126 |
\begin{warn}
|
wenzelm@27056
|
127 |
History commands should never be used with user interfaces such as
|
wenzelm@27056
|
128 |
Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
|
wenzelm@27056
|
129 |
care of stepping forth and back itself. Interfering by manual
|
wenzelm@27598
|
130 |
@{command "undo"}, @{command "linear_undo"}, or even @{command
|
wenzelm@27598
|
131 |
"kill"} commands would quickly result in utter confusion.
|
wenzelm@27056
|
132 |
\end{warn}
|
wenzelm@27056
|
133 |
*}
|
wenzelm@27056
|
134 |
|
wenzelm@27056
|
135 |
|
wenzelm@27056
|
136 |
section {* System commands *}
|
wenzelm@27056
|
137 |
|
wenzelm@27056
|
138 |
text {*
|
wenzelm@27056
|
139 |
\begin{matharray}{rcl}
|
wenzelm@28761
|
140 |
@{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
|
wenzelm@28761
|
141 |
@{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
|
wenzelm@28761
|
142 |
@{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
|
wenzelm@27056
|
143 |
\end{matharray}
|
wenzelm@27056
|
144 |
|
wenzelm@27056
|
145 |
\begin{rail}
|
wenzelm@27056
|
146 |
('cd' | 'use\_thy' | 'update\_thy') name
|
wenzelm@27056
|
147 |
;
|
wenzelm@27056
|
148 |
\end{rail}
|
wenzelm@27056
|
149 |
|
wenzelm@28760
|
150 |
\begin{description}
|
wenzelm@27056
|
151 |
|
wenzelm@28760
|
152 |
\item @{command "cd"}~@{text path} changes the current directory
|
wenzelm@27056
|
153 |
of the Isabelle process.
|
wenzelm@27056
|
154 |
|
wenzelm@28760
|
155 |
\item @{command "pwd"} prints the current working directory.
|
wenzelm@27056
|
156 |
|
wenzelm@28760
|
157 |
\item @{command "use_thy"}~@{text A} preload theory @{text A}.
|
wenzelm@27056
|
158 |
These system commands are scarcely used when working interactively,
|
wenzelm@27056
|
159 |
since loading of theories is done automatically as required.
|
wenzelm@27056
|
160 |
|
wenzelm@28760
|
161 |
\end{description}
|
wenzelm@27056
|
162 |
*}
|
wenzelm@27056
|
163 |
|
wenzelm@27056
|
164 |
end
|