wenzelm@27056
|
1 |
theory Misc
|
wenzelm@43522
|
2 |
imports Base 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>"} \\
|
berghofe@41872
|
19 |
@{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28761
|
20 |
@{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28761
|
21 |
@{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@27056
|
22 |
\end{matharray}
|
wenzelm@27056
|
23 |
|
wenzelm@43467
|
24 |
@{rail "
|
wenzelm@43467
|
25 |
(@@{command print_theory} | @@{command print_theorems}) ('!'?)
|
wenzelm@27056
|
26 |
;
|
wenzelm@27056
|
27 |
|
wenzelm@43467
|
28 |
@@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \\ (thmcriterion * )
|
wenzelm@27056
|
29 |
;
|
wenzelm@43467
|
30 |
thmcriterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
|
wenzelm@43467
|
31 |
'solves' | 'simp' ':' @{syntax term} | @{syntax term})
|
wenzelm@27056
|
32 |
;
|
wenzelm@43467
|
33 |
@@{command find_consts} (constcriterion * )
|
kleing@29831
|
34 |
;
|
wenzelm@43467
|
35 |
constcriterion: ('-'?)
|
wenzelm@43467
|
36 |
('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
|
kleing@29831
|
37 |
;
|
wenzelm@43467
|
38 |
@@{command thm_deps} @{syntax thmrefs}
|
wenzelm@27056
|
39 |
;
|
wenzelm@43467
|
40 |
@@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
|
wenzelm@43467
|
41 |
"}
|
wenzelm@27056
|
42 |
|
wenzelm@27056
|
43 |
These commands print certain parts of the theory and proof context.
|
wenzelm@27056
|
44 |
Note that there are some further ones available, such as for the set
|
wenzelm@27056
|
45 |
of rules declared for simplifications.
|
wenzelm@27056
|
46 |
|
wenzelm@28760
|
47 |
\begin{description}
|
wenzelm@27056
|
48 |
|
wenzelm@28760
|
49 |
\item @{command "print_commands"} prints Isabelle's outer theory
|
wenzelm@27056
|
50 |
syntax, including keywords and command.
|
wenzelm@27056
|
51 |
|
wenzelm@28760
|
52 |
\item @{command "print_theory"} prints the main logical content of
|
wenzelm@27056
|
53 |
the theory context; the ``@{text "!"}'' option indicates extra
|
wenzelm@27056
|
54 |
verbosity.
|
wenzelm@27056
|
55 |
|
wenzelm@28760
|
56 |
\item @{command "print_methods"} prints all proof methods
|
wenzelm@27056
|
57 |
available in the current theory context.
|
wenzelm@27056
|
58 |
|
wenzelm@28760
|
59 |
\item @{command "print_attributes"} prints all attributes
|
wenzelm@27056
|
60 |
available in the current theory context.
|
wenzelm@27056
|
61 |
|
wenzelm@33515
|
62 |
\item @{command "print_theorems"} prints theorems resulting from the
|
wenzelm@33515
|
63 |
last command; the ``@{text "!"}'' option indicates extra verbosity.
|
wenzelm@27056
|
64 |
|
wenzelm@28760
|
65 |
\item @{command "find_theorems"}~@{text criteria} retrieves facts
|
wenzelm@27056
|
66 |
from the theory or proof context matching all of given search
|
wenzelm@27056
|
67 |
criteria. The criterion @{text "name: p"} selects all theorems
|
wenzelm@27056
|
68 |
whose fully qualified name matches pattern @{text p}, which may
|
wenzelm@27056
|
69 |
contain ``@{text "*"}'' wildcards. The criteria @{text intro},
|
wenzelm@27056
|
70 |
@{text elim}, and @{text dest} select theorems that match the
|
wenzelm@27056
|
71 |
current goal as introduction, elimination or destruction rules,
|
kleing@29833
|
72 |
respectively. The criterion @{text "solves"} returns all rules
|
kleing@29830
|
73 |
that would directly solve the current goal. The criterion
|
kleing@29830
|
74 |
@{text "simp: t"} selects all rewrite rules whose left-hand side
|
kleing@29830
|
75 |
matches the given term. The criterion term @{text t} selects all
|
kleing@29830
|
76 |
theorems that contain the pattern @{text t} -- as usual, patterns
|
kleing@29830
|
77 |
may contain occurrences of the dummy ``@{text _}'', schematic
|
kleing@29830
|
78 |
variables, and type constraints.
|
wenzelm@27056
|
79 |
|
wenzelm@27056
|
80 |
Criteria can be preceded by ``@{text "-"}'' to select theorems that
|
wenzelm@27056
|
81 |
do \emph{not} match. Note that giving the empty list of criteria
|
wenzelm@27056
|
82 |
yields \emph{all} currently known facts. An optional limit for the
|
wenzelm@27056
|
83 |
number of printed facts may be given; the default is 40. By
|
wenzelm@27056
|
84 |
default, duplicates are removed from the search result. Use
|
wenzelm@27056
|
85 |
@{text with_dups} to display duplicates.
|
kleing@29831
|
86 |
|
kleing@29831
|
87 |
\item @{command "find_consts"}~@{text criteria} prints all constants
|
kleing@29831
|
88 |
whose type meets all of the given criteria. The criterion @{text
|
kleing@29831
|
89 |
"strict: ty"} is met by any type that matches the type pattern
|
kleing@29831
|
90 |
@{text ty}. Patterns may contain both the dummy type ``@{text _}''
|
kleing@29831
|
91 |
and sort constraints. The criterion @{text ty} is similar, but it
|
kleing@29831
|
92 |
also matches against subtypes. The criterion @{text "name: p"} and
|
kleing@29831
|
93 |
the prefix ``@{text "-"}'' function as described for @{command
|
kleing@29831
|
94 |
"find_theorems"}.
|
kleing@29831
|
95 |
|
wenzelm@28760
|
96 |
\item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
|
wenzelm@27056
|
97 |
visualizes dependencies of facts, using Isabelle's graph browser
|
wenzelm@27056
|
98 |
tool (see also \cite{isabelle-sys}).
|
berghofe@41872
|
99 |
|
berghofe@41872
|
100 |
\item @{command "unused_thms"}~@{text "A\<^isub>1 \<dots> A\<^isub>m - B\<^isub>1 \<dots> B\<^isub>n"}
|
berghofe@41872
|
101 |
displays all unused theorems in theories @{text "B\<^isub>1 \<dots> B\<^isub>n"}
|
berghofe@41872
|
102 |
or their parents, but not in @{text "A\<^isub>1 \<dots> A\<^isub>m"} or their parents.
|
berghofe@41872
|
103 |
If @{text n} is @{text 0}, the end of the range of theories
|
berghofe@41872
|
104 |
defaults to the current theory. If no range is specified,
|
berghofe@41872
|
105 |
only the unused theorems in the current theory are displayed.
|
wenzelm@27056
|
106 |
|
wenzelm@28760
|
107 |
\item @{command "print_facts"} prints all local facts of the
|
wenzelm@27056
|
108 |
current context, both named and unnamed ones.
|
wenzelm@27056
|
109 |
|
wenzelm@28760
|
110 |
\item @{command "print_binds"} prints all term abbreviations
|
wenzelm@27056
|
111 |
present in the context.
|
wenzelm@27056
|
112 |
|
wenzelm@28760
|
113 |
\end{description}
|
wenzelm@27056
|
114 |
*}
|
wenzelm@27056
|
115 |
|
wenzelm@27056
|
116 |
|
wenzelm@27056
|
117 |
section {* System commands *}
|
wenzelm@27056
|
118 |
|
wenzelm@27056
|
119 |
text {*
|
wenzelm@27056
|
120 |
\begin{matharray}{rcl}
|
wenzelm@28761
|
121 |
@{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
|
wenzelm@28761
|
122 |
@{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
|
wenzelm@28761
|
123 |
@{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
|
wenzelm@27056
|
124 |
\end{matharray}
|
wenzelm@27056
|
125 |
|
wenzelm@43467
|
126 |
@{rail "
|
wenzelm@43467
|
127 |
(@@{command cd} | @@{command use_thy}) @{syntax name}
|
wenzelm@43467
|
128 |
"}
|
wenzelm@27056
|
129 |
|
wenzelm@28760
|
130 |
\begin{description}
|
wenzelm@27056
|
131 |
|
wenzelm@28760
|
132 |
\item @{command "cd"}~@{text path} changes the current directory
|
wenzelm@27056
|
133 |
of the Isabelle process.
|
wenzelm@27056
|
134 |
|
wenzelm@28760
|
135 |
\item @{command "pwd"} prints the current working directory.
|
wenzelm@27056
|
136 |
|
wenzelm@28760
|
137 |
\item @{command "use_thy"}~@{text A} preload theory @{text A}.
|
wenzelm@27056
|
138 |
These system commands are scarcely used when working interactively,
|
wenzelm@27056
|
139 |
since loading of theories is done automatically as required.
|
wenzelm@27056
|
140 |
|
wenzelm@28760
|
141 |
\end{description}
|
wenzelm@40275
|
142 |
|
wenzelm@40275
|
143 |
%FIXME proper place (!?)
|
wenzelm@40275
|
144 |
Isabelle file specification may contain path variables (e.g.\
|
wenzelm@40275
|
145 |
@{verbatim "$ISABELLE_HOME"}) that are expanded accordingly. Note
|
wenzelm@48538
|
146 |
that @{verbatim "~"} abbreviates @{verbatim "$USER_HOME"}, and
|
wenzelm@48538
|
147 |
@{verbatim "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}. The
|
wenzelm@48538
|
148 |
general syntax for path specifications follows POSIX conventions.
|
wenzelm@27056
|
149 |
*}
|
wenzelm@27056
|
150 |
|
wenzelm@27056
|
151 |
end
|