1 theory Misc |
|
2 imports Base Main |
|
3 begin |
|
4 |
|
5 chapter {* Other commands *} |
|
6 |
|
7 section {* Inspecting the context *} |
|
8 |
|
9 text {* |
|
10 \begin{matharray}{rcl} |
|
11 @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
|
12 @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
13 @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
14 @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
15 @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
16 @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
17 @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
18 @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
19 @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
20 @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
21 @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
22 \end{matharray} |
|
23 |
|
24 @{rail " |
|
25 (@@{command print_theory} | @@{command print_theorems}) ('!'?) |
|
26 ; |
|
27 |
|
28 @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \\ (thmcriterion * ) |
|
29 ; |
|
30 thmcriterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' | |
|
31 'solves' | 'simp' ':' @{syntax term} | @{syntax term}) |
|
32 ; |
|
33 @@{command find_consts} (constcriterion * ) |
|
34 ; |
|
35 constcriterion: ('-'?) |
|
36 ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type}) |
|
37 ; |
|
38 @@{command thm_deps} @{syntax thmrefs} |
|
39 ; |
|
40 @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))? |
|
41 "} |
|
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 |
|
47 \begin{description} |
|
48 |
|
49 \item @{command "print_commands"} prints Isabelle's outer theory |
|
50 syntax, including keywords and command. |
|
51 |
|
52 \item @{command "print_theory"} prints the main logical content of |
|
53 the theory context; the ``@{text "!"}'' option indicates extra |
|
54 verbosity. |
|
55 |
|
56 \item @{command "print_methods"} prints all proof methods |
|
57 available in the current theory context. |
|
58 |
|
59 \item @{command "print_attributes"} prints all attributes |
|
60 available in the current theory context. |
|
61 |
|
62 \item @{command "print_theorems"} prints theorems resulting from the |
|
63 last command; the ``@{text "!"}'' option indicates extra verbosity. |
|
64 |
|
65 \item @{command "find_theorems"}~@{text criteria} retrieves facts |
|
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, |
|
72 respectively. The criterion @{text "solves"} returns all rules |
|
73 that would directly solve the current goal. The criterion |
|
74 @{text "simp: t"} selects all rewrite rules whose left-hand side |
|
75 matches the given term. The criterion term @{text t} selects all |
|
76 theorems that contain the pattern @{text t} -- as usual, patterns |
|
77 may contain occurrences of the dummy ``@{text _}'', schematic |
|
78 variables, and type constraints. |
|
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. |
|
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 |
|
96 \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} |
|
97 visualizes dependencies of facts, using Isabelle's graph browser |
|
98 tool (see also \cite{isabelle-sys}). |
|
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. |
|
106 |
|
107 \item @{command "print_facts"} prints all local facts of the |
|
108 current context, both named and unnamed ones. |
|
109 |
|
110 \item @{command "print_binds"} prints all term abbreviations |
|
111 present in the context. |
|
112 |
|
113 \end{description} |
|
114 *} |
|
115 |
|
116 |
|
117 section {* System commands *} |
|
118 |
|
119 text {* |
|
120 \begin{matharray}{rcl} |
|
121 @{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
|
122 @{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
|
123 @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
|
124 \end{matharray} |
|
125 |
|
126 @{rail " |
|
127 (@@{command cd} | @@{command use_thy}) @{syntax name} |
|
128 "} |
|
129 |
|
130 \begin{description} |
|
131 |
|
132 \item @{command "cd"}~@{text path} changes the current directory |
|
133 of the Isabelle process. |
|
134 |
|
135 \item @{command "pwd"} prints the current working directory. |
|
136 |
|
137 \item @{command "use_thy"}~@{text A} preload theory @{text A}. |
|
138 These system commands are scarcely used when working interactively, |
|
139 since loading of theories is done automatically as required. |
|
140 |
|
141 \end{description} |
|
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 "$USER_HOME"}, and |
|
147 @{verbatim "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}. The |
|
148 general syntax for path specifications follows POSIX conventions. |
|
149 *} |
|
150 |
|
151 end |
|