1 theory Misc |
|
2 imports Base Main |
|
3 begin |
|
4 |
|
5 chapter \<open>Other commands\<close> |
|
6 |
|
7 section \<open>Inspecting the context\<close> |
|
8 |
|
9 text \<open> |
|
10 \begin{matharray}{rcl} |
|
11 @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
12 @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
13 @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
14 @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
15 @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
16 @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
17 @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
18 @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
19 @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
20 @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
21 \end{matharray} |
|
22 |
|
23 @{rail \<open> |
|
24 (@@{command print_theory} | |
|
25 @@{command print_methods} | |
|
26 @@{command print_attributes} | |
|
27 @@{command print_theorems} | |
|
28 @@{command print_facts}) ('!'?) |
|
29 ; |
|
30 @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*) |
|
31 ; |
|
32 thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' | |
|
33 'solves' | 'simp' ':' @{syntax term} | @{syntax term}) |
|
34 ; |
|
35 @@{command find_consts} (const_criterion*) |
|
36 ; |
|
37 const_criterion: ('-'?) |
|
38 ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type}) |
|
39 ; |
|
40 @@{command thm_deps} @{syntax thmrefs} |
|
41 ; |
|
42 @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))? |
|
43 \<close>} |
|
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 |
|
49 \begin{description} |
|
50 |
|
51 \item @{command "print_theory"} prints the main logical content of the |
|
52 background theory; the ``@{text "!"}'' option indicates extra verbosity. |
|
53 |
|
54 \item @{command "print_methods"} prints all proof methods available in the |
|
55 current theory context; the ``@{text "!"}'' option indicates extra |
|
56 verbosity. |
|
57 |
|
58 \item @{command "print_attributes"} prints all attributes available in the |
|
59 current theory context; the ``@{text "!"}'' option indicates extra |
|
60 verbosity. |
|
61 |
|
62 \item @{command "print_theorems"} prints theorems of the background theory |
|
63 resulting from the last command; the ``@{text "!"}'' option indicates |
|
64 extra verbosity. |
|
65 |
|
66 \item @{command "print_facts"} prints all local facts of the current |
|
67 context, both named and unnamed ones; the ``@{text "!"}'' option indicates |
|
68 extra verbosity. |
|
69 |
|
70 \item @{command "print_term_bindings"} prints all term bindings that |
|
71 are present in the context. |
|
72 |
|
73 \item @{command "find_theorems"}~@{text criteria} retrieves facts |
|
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, |
|
80 respectively. The criterion @{text "solves"} returns all rules |
|
81 that would directly solve the current goal. The criterion |
|
82 @{text "simp: t"} selects all rewrite rules whose left-hand side |
|
83 matches the given term. The criterion term @{text t} selects all |
|
84 theorems that contain the pattern @{text t} -- as usual, patterns |
|
85 may contain occurrences of the dummy ``@{text _}'', schematic |
|
86 variables, and type constraints. |
|
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. |
|
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 |
|
104 \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} |
|
105 visualizes dependencies of facts, using Isabelle's graph browser |
|
106 tool (see also @{cite "isabelle-system"}). |
|
107 |
|
108 \item @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"} |
|
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. |
|
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. |
|
115 |
|
116 \end{description} |
|
117 \<close> |
|
118 |
|
119 end |
|