105
|
1 |
\begin{theindex}
|
|
2 |
|
|
3 |
\item $\Forall$, \bold{5}, 7
|
|
4 |
\item $\Imp$, \bold{5}
|
|
5 |
\item $\To$, \bold{1}, \bold{3}
|
|
6 |
\item $\equiv$, \bold{5}
|
|
7 |
|
|
8 |
\indexspace
|
|
9 |
|
|
10 |
\item {\tt allI}, 35
|
|
11 |
\item arities
|
|
12 |
\subitem declaring, 3, \bold{46}
|
|
13 |
\item {\tt asm_simp_tac}, 55
|
|
14 |
\item associativity of addition, 54
|
|
15 |
\item {\tt assume_tac}, \bold{27}, 29, 30, 35, 43, 44
|
|
16 |
\item assumptions, 6
|
|
17 |
|
|
18 |
\indexspace
|
|
19 |
|
|
20 |
\item {\tt ba}, \bold{28}
|
|
21 |
\item {\tt back}, 54, 57
|
|
22 |
\item backtracking, 57
|
|
23 |
\item {\tt bd}, \bold{28}
|
|
24 |
\item {\tt be}, \bold{28}
|
|
25 |
\item {\tt br}, \bold{28}
|
|
26 |
\item {\tt by}, \bold{28}
|
|
27 |
|
|
28 |
\indexspace
|
|
29 |
|
|
30 |
\item {\tt choplev}, 34, 35, 59
|
|
31 |
\item classes, \bold{3}
|
|
32 |
\subitem built-in, \bold{23}
|
|
33 |
\item classical reasoning package, 36
|
|
34 |
\item classical sets, \bold{36}
|
|
35 |
\item {\tt conjunct1}, 25
|
|
36 |
\item constants
|
|
37 |
\subitem declaring, \bold{45}
|
|
38 |
|
|
39 |
\indexspace
|
|
40 |
|
|
41 |
\item definitions, \bold{5}
|
|
42 |
\subitem reasoning about, \bold{40}
|
|
43 |
\item {\tt DEPTH_FIRST}, 59
|
|
44 |
\item destruct-resolution, \bold{20}
|
|
45 |
\item destruction rules, \bold{20}
|
|
46 |
\item {\tt disjE}, 29
|
|
47 |
\item {\tt dres_inst_tac}, \bold{52}
|
|
48 |
\item {\tt dresolve_tac}, \bold{28}, 30, 33, 36
|
|
49 |
|
|
50 |
\indexspace
|
|
51 |
|
|
52 |
\item eigenvariables, \see{parameters}{7}
|
|
53 |
\item elim-resolution, \bold{18}
|
|
54 |
\item equality
|
|
55 |
\subitem meta-level, \bold{5}
|
|
56 |
\item {\tt eres_inst_tac}, \bold{52}
|
|
57 |
\item {\tt eresolve_tac}, \bold{27}, 30, 36, 43, 44
|
|
58 |
\item examples
|
|
59 |
\subitem of deriving rules, 38
|
|
60 |
\subitem of induction, 52, 53
|
|
61 |
\subitem of rewriting, 54
|
|
62 |
\subitem of tacticals, 35
|
|
63 |
\subitem of theories, 45--51, 56
|
|
64 |
\subitem propositional, 16, 28, 30
|
|
65 |
\subitem with quantifiers, 17, 31, 33, 35
|
|
66 |
\item {\tt exE}, 35
|
|
67 |
|
|
68 |
\indexspace
|
|
69 |
|
|
70 |
\item {\tt FalseE}, 42
|
|
71 |
\item {\tt fast_tac}, 36, 37
|
|
72 |
\item flex-flex equations, \bold{5}, 23, \bold{26}
|
|
73 |
\item {\tt flexflex_rule}, 26
|
|
74 |
\item {\tt FOL}, 56
|
|
75 |
\item {\tt FOL.thy}, 28
|
|
76 |
\item folding, \bold{40}
|
|
77 |
|
|
78 |
\indexspace
|
|
79 |
|
|
80 |
\item {\tt goal}, \bold{28}, 38, 39, 41--43
|
|
81 |
\item {\tt goalw}, 42, 43
|
|
82 |
|
|
83 |
\indexspace
|
|
84 |
|
|
85 |
\item {\tt has_fewer_prems}, 59
|
|
86 |
|
|
87 |
\indexspace
|
|
88 |
|
|
89 |
\item identifiers, \bold{22}
|
|
90 |
\item imitation, \bold{10}
|
|
91 |
\item {\tt impI}, 29, 41
|
|
92 |
\item implication
|
|
93 |
\subitem meta-level, \bold{5}
|
|
94 |
\item infix operators, \bold{47}
|
|
95 |
\item instantiation
|
|
96 |
\subitem explicit, \bold{52}
|
|
97 |
\item Isabelle
|
|
98 |
\subitem definitions in, 40
|
|
99 |
\subitem formalizing rules, \bold{5}
|
|
100 |
\subitem formalizing syntax, \bold{1}
|
|
101 |
\subitem getting started, 22
|
|
102 |
\subitem object-logics supported, i
|
|
103 |
\subitem overview, i
|
|
104 |
\subitem proof construction in, \bold{9}
|
|
105 |
\subitem release history, i
|
|
106 |
\subitem syntax of, 23
|
|
107 |
|
|
108 |
\indexspace
|
|
109 |
|
|
110 |
\item LCF, i, 14, 24
|
|
111 |
\item level, \bold{29}
|
|
112 |
\item lifting, \bold{13}
|
|
113 |
\subitem over assumptions, \bold{13}
|
|
114 |
\subitem over parameters, \bold{13}
|
|
115 |
\item {\tt logic}, 23
|
|
116 |
|
|
117 |
\indexspace
|
|
118 |
|
|
119 |
\item main goal, \bold{14}
|
|
120 |
\item major premise, \bold{19}
|
|
121 |
\item {\tt Match}, 39
|
|
122 |
\item meta-formulae
|
|
123 |
\subitem syntax, \bold{23}
|
|
124 |
\item meta-logic, \bold{5}
|
|
125 |
\item mixfix operators, \bold{47}
|
|
126 |
\item ML, i, 22, 25
|
|
127 |
\item {\tt mp}, 25
|
|
128 |
|
|
129 |
\indexspace
|
|
130 |
|
|
131 |
\item {\tt Nat}, \bold{51}
|
|
132 |
\item {\tt Nat.thy}, 53
|
|
133 |
\item {\tt not_def}, 41
|
|
134 |
\item {\tt notE}, \bold{43}, 53
|
|
135 |
\item {\tt notI}, \bold{41}, 53
|
|
136 |
|
|
137 |
\indexspace
|
|
138 |
|
|
139 |
\item {\tt ORELSE}, 35
|
|
140 |
\item overloading, \bold{4}, 48
|
|
141 |
|
|
142 |
\indexspace
|
|
143 |
|
|
144 |
\item parameters, \bold{7}, 31
|
|
145 |
\item printing commands, \bold{25}
|
|
146 |
\item projection, \bold{10}
|
|
147 |
\item {\tt Prolog}, 56
|
|
148 |
\item Prolog interpreter, \bold{55}
|
|
149 |
\item proof
|
|
150 |
\subitem backward, \bold{14}
|
|
151 |
\subitem by assumption, \bold{15}
|
|
152 |
\subitem by induction, 52
|
|
153 |
\subitem commands for, \bold{28}
|
|
154 |
\subitem forward, 20
|
|
155 |
\item proof state, \bold{14}
|
|
156 |
\item {\tt PROP}, 24
|
|
157 |
\item {\tt prop}, 23, 24
|
|
158 |
\item {\tt prth}, \bold{25}
|
|
159 |
\item {\tt prthq}, \bold{25}, 26
|
|
160 |
\item {\tt prths}, \bold{25}
|
|
161 |
\item {\tt Pure}, \bold{44}
|
|
162 |
|
|
163 |
\indexspace
|
|
164 |
|
|
165 |
\item quantifiers
|
|
166 |
\subitem meta-level, \bold{5}
|
|
167 |
\subitem reasoning about, 31
|
|
168 |
|
|
169 |
\indexspace
|
|
170 |
|
|
171 |
\item {\tt read_instantiate}, 27
|
|
172 |
\item refinement, \bold{15}
|
|
173 |
\subitem with instantiation, \bold{52}
|
|
174 |
\item {\tt refl}, 27
|
|
175 |
\item {\tt REPEAT}, 30, 35, 57, 59
|
|
176 |
\item {\tt res_inst_tac}, \bold{52}, 54, 55
|
|
177 |
\item reserved words, \bold{22}
|
|
178 |
\item resolution, \bold{11}
|
|
179 |
\subitem in backward proof, 14
|
|
180 |
\item {\tt resolve_tac}, \bold{27}, 29, 43, 53
|
|
181 |
\item {\tt result}, \bold{28}, 29, 38, 39, 44
|
|
182 |
\item {\tt rewrite_goals_tac}, 41, 42
|
|
183 |
\item {\tt rewrite_rule}, 42, 43
|
|
184 |
\item rewriting
|
|
185 |
\subitem meta-level, 40, \bold{40}
|
|
186 |
\subitem object-level, 54
|
|
187 |
\item {\tt RL}, 27
|
|
188 |
\item {\tt RLN}, 27
|
|
189 |
\item {\tt RS}, \bold{25}, 27, 43
|
|
190 |
\item {\tt RSN}, \bold{25}, 27
|
|
191 |
\item rules
|
|
192 |
\subitem declaring, \bold{45}
|
|
193 |
\subitem derived, 12, \bold{20}, 38, 40
|
|
194 |
\subitem propositional, \bold{6}
|
|
195 |
\subitem quantifier, \bold{7}
|
|
196 |
|
|
197 |
\indexspace
|
|
198 |
|
|
199 |
\item search
|
|
200 |
\subitem depth-first, 58
|
|
201 |
\item signatures, \bold{8}
|
|
202 |
\item {\tt simp_tac}, 55
|
|
203 |
\item simplification set, \bold{54}
|
|
204 |
\item sorts, \bold{4}
|
|
205 |
\item {\tt spec}, 26, 33, 35
|
|
206 |
\item {\tt standard}, \bold{25}
|
|
207 |
\item subgoals, \bold{14}
|
|
208 |
\item substitution, \bold{7}
|
|
209 |
\item {\tt Suc_inject}, 53
|
|
210 |
\item {\tt Suc_neq_0}, 53
|
|
211 |
|
|
212 |
\indexspace
|
|
213 |
|
|
214 |
\item tacticals, \bold{14}, \bold{17}, 35
|
|
215 |
\item Tactics, \bold{14}
|
|
216 |
\item tactics, \bold{17}
|
|
217 |
\subitem basic, \bold{27}
|
|
218 |
\item terms
|
|
219 |
\subitem syntax, \bold{23}
|
|
220 |
\item theorems
|
|
221 |
\subitem basic operations on, \bold{24}
|
|
222 |
\item theories, \bold{8}
|
|
223 |
\subitem defining, 44--52
|
|
224 |
\item {\tt thm}, 24
|
|
225 |
\item {\tt topthm}, 39
|
|
226 |
\item {$Trueprop$}, 6, 7, 9, 23
|
|
227 |
\item type constructors
|
|
228 |
\subitem declaring, \bold{46}
|
|
229 |
\item types, 1
|
|
230 |
\subitem higher, \bold{4}
|
|
231 |
\subitem polymorphic, \bold{3}
|
|
232 |
\subitem simple, \bold{1}
|
|
233 |
\subitem syntax, \bold{23}
|
|
234 |
|
|
235 |
\indexspace
|
|
236 |
|
|
237 |
\item {\tt undo}, \bold{28}
|
|
238 |
\item unfolding, \bold{40}
|
|
239 |
\item unification
|
|
240 |
\subitem higher-order, \bold{10}, 53
|
|
241 |
\item unknowns, \bold{9}, 31
|
|
242 |
\subitem of function type, \bold{11}, 26
|
|
243 |
\item {\tt use_thy}, \bold{44, 45}
|
|
244 |
|
|
245 |
\indexspace
|
|
246 |
|
|
247 |
\item variables
|
|
248 |
\subitem bound, 7
|
|
249 |
\subitem schematic, \see{unknowns}{9}
|
|
250 |
|
|
251 |
\end{theindex}
|