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