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