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