author | wenzelm |
Wed, 06 May 2015 23:28:09 +0200 | |
changeset 60270 | a147272b16f9 |
parent 59917 | 9830c944670f |
child 60665 | 61be352b1f79 |
permissions | -rw-r--r-- |
27056 | 1 |
theory Misc |
42651 | 2 |
imports Base Main |
27056 | 3 |
begin |
4 |
||
58618 | 5 |
chapter \<open>Other commands\<close> |
27056 | 6 |
|
58618 | 7 |
section \<open>Inspecting the context\<close> |
27056 | 8 |
|
58618 | 9 |
text \<open> |
27056 | 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>"} \\ |
57415
e721124f1b1e
command 'print_term_bindings' supersedes 'print_binds';
wenzelm
parents:
56582
diff
changeset
|
20 |
@{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
27056 | 21 |
\end{matharray} |
22 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
23 |
@{rail \<open> |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
24 |
(@@{command print_theory} | |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
25 |
@@{command print_methods} | |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
26 |
@@{command print_attributes} | |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
27 |
@@{command print_theorems} | |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
28 |
@@{command print_facts}) ('!'?) |
27056 | 29 |
; |
55029
61a6bf7d4b02
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents:
55011
diff
changeset
|
30 |
@@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thmcriterion * ) |
27056 | 31 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41624
diff
changeset
|
32 |
thmcriterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' | |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41624
diff
changeset
|
33 |
'solves' | 'simp' ':' @{syntax term} | @{syntax term}) |
27056 | 34 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41624
diff
changeset
|
35 |
@@{command find_consts} (constcriterion * ) |
29894 | 36 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41624
diff
changeset
|
37 |
constcriterion: ('-'?) |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41624
diff
changeset
|
38 |
('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type}) |
27056 | 39 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41624
diff
changeset
|
40 |
@@{command thm_deps} @{syntax thmrefs} |
41624 | 41 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41624
diff
changeset
|
42 |
@@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))? |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
43 |
\<close>} |
27056 | 44 |
|
45 |
These commands print certain parts of the theory and proof context. |
|
46 |
Note that there are some further ones available, such as for the set |
|
47 |
of rules declared for simplifications. |
|
48 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
49 |
\begin{description} |
27056 | 50 |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
51 |
\item @{command "print_theory"} prints the main logical content of the |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
52 |
background theory; the ``@{text "!"}'' option indicates extra verbosity. |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
53 |
|
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
54 |
\item @{command "print_methods"} prints all proof methods available in the |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
55 |
current theory context; the ``@{text "!"}'' option indicates extra |
27056 | 56 |
verbosity. |
57 |
||
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
58 |
\item @{command "print_attributes"} prints all attributes available in the |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
59 |
current theory context; the ``@{text "!"}'' option indicates extra |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
60 |
verbosity. |
27056 | 61 |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
62 |
\item @{command "print_theorems"} prints theorems of the background theory |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
63 |
resulting from the last command; the ``@{text "!"}'' option indicates |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
64 |
extra verbosity. |
27056 | 65 |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
66 |
\item @{command "print_facts"} prints all local facts of the current |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
67 |
context, both named and unnamed ones; the ``@{text "!"}'' option indicates |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
58618
diff
changeset
|
68 |
extra verbosity. |
56158
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
55112
diff
changeset
|
69 |
|
57415
e721124f1b1e
command 'print_term_bindings' supersedes 'print_binds';
wenzelm
parents:
56582
diff
changeset
|
70 |
\item @{command "print_term_bindings"} prints all term bindings that |
e721124f1b1e
command 'print_term_bindings' supersedes 'print_binds';
wenzelm
parents:
56582
diff
changeset
|
71 |
are present in the context. |
56158
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
55112
diff
changeset
|
72 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
73 |
\item @{command "find_theorems"}~@{text criteria} retrieves facts |
27056 | 74 |
from the theory or proof context matching all of given search |
75 |
criteria. The criterion @{text "name: p"} selects all theorems |
|
76 |
whose fully qualified name matches pattern @{text p}, which may |
|
77 |
contain ``@{text "*"}'' wildcards. The criteria @{text intro}, |
|
78 |
@{text elim}, and @{text dest} select theorems that match the |
|
79 |
current goal as introduction, elimination or destruction rules, |
|
29896 | 80 |
respectively. The criterion @{text "solves"} returns all rules |
29893
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28779
diff
changeset
|
81 |
that would directly solve the current goal. The criterion |
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28779
diff
changeset
|
82 |
@{text "simp: t"} selects all rewrite rules whose left-hand side |
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28779
diff
changeset
|
83 |
matches the given term. The criterion term @{text t} selects all |
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28779
diff
changeset
|
84 |
theorems that contain the pattern @{text t} -- as usual, patterns |
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28779
diff
changeset
|
85 |
may contain occurrences of the dummy ``@{text _}'', schematic |
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28779
diff
changeset
|
86 |
variables, and type constraints. |
27056 | 87 |
|
88 |
Criteria can be preceded by ``@{text "-"}'' to select theorems that |
|
89 |
do \emph{not} match. Note that giving the empty list of criteria |
|
90 |
yields \emph{all} currently known facts. An optional limit for the |
|
91 |
number of printed facts may be given; the default is 40. By |
|
92 |
default, duplicates are removed from the search result. Use |
|
93 |
@{text with_dups} to display duplicates. |
|
29894 | 94 |
|
95 |
\item @{command "find_consts"}~@{text criteria} prints all constants |
|
96 |
whose type meets all of the given criteria. The criterion @{text |
|
97 |
"strict: ty"} is met by any type that matches the type pattern |
|
98 |
@{text ty}. Patterns may contain both the dummy type ``@{text _}'' |
|
99 |
and sort constraints. The criterion @{text ty} is similar, but it |
|
100 |
also matches against subtypes. The criterion @{text "name: p"} and |
|
101 |
the prefix ``@{text "-"}'' function as described for @{command |
|
102 |
"find_theorems"}. |
|
103 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
104 |
\item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} |
27056 | 105 |
visualizes dependencies of facts, using Isabelle's graph browser |
60270 | 106 |
tool (see also @{cite "isabelle-system"}). |
41624 | 107 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50213
diff
changeset
|
108 |
\item @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"} |
55011 | 109 |
displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"} |
110 |
or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and |
|
111 |
that are never used. |
|
41624 | 112 |
If @{text n} is @{text 0}, the end of the range of theories |
113 |
defaults to the current theory. If no range is specified, |
|
114 |
only the unused theorems in the current theory are displayed. |
|
27056 | 115 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
116 |
\end{description} |
58618 | 117 |
\<close> |
27056 | 118 |
|
119 |
end |