1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/TutorialI/tutorial.ind Fri Jul 13 11:31:05 2001 +0200
1.3 @@ -0,0 +1,676 @@
1.4 +\begin{theindex}
1.5 +
1.6 + \item \emph {$\forall \tmspace +\thinmuskip {.1667em}$}, \bold{3},
1.7 + \bold{189}
1.8 + \item \ttall, \bold{189}
1.9 + \item \emph {$\exists \tmspace +\thinmuskip {.1667em}$}, \bold{3},
1.10 + \bold{189}
1.11 + \item \texttt{?}, \hyperpage{5}, \bold{189}
1.12 + \item \emph {$\varepsilon $}, \bold{189}
1.13 + \item \isasymuniqex, \bold{3}, \bold{189}
1.14 + \item \ttuniquex, \bold{189}
1.15 + \item \emph {$\wedge $}, \bold{3}, \bold{189}
1.16 + \item {\texttt {\&}}, \bold{189}
1.17 + \item \texttt {=}, \bold{3}
1.18 + \item \emph {$\DOTSB \relbar \joinrel \rightarrow $}, \bold{3},
1.19 + \bold{189}
1.20 + \item \texttt {-->}, \bold{189}
1.21 + \item \emph {$\neg $}, \bold{3}, \bold{189}
1.22 + \item \verb$~$, \bold{189}
1.23 + \item \emph {$\not =$}, \bold{189}
1.24 + \item \verb$~=$, \bold{189}
1.25 + \item \emph {$\vee $}, \bold{3}, \bold{189}
1.26 + \item \ttor, \bold{189}
1.27 + \item \emph {$\circ $}, \bold{189}
1.28 + \item \emph {$\mid $}\nobreakspace {}\emph {$\mid $}, \bold{189}
1.29 + \item \texttt {*}, \bold{20, 21}, \bold{189}
1.30 + \item \texttt {+}, \bold{20, 21}
1.31 + \item \texttt {-}, \bold{20, 21}
1.32 + \item \emph {$\le $}, \bold{20, 21}, \bold{189}
1.33 + \item \texttt {<=}, \bold{189}
1.34 + \item \texttt {<}, \bold{20, 21}
1.35 + \item \texttt{[]}, \bold{7}
1.36 + \item \texttt{\#}, \bold{7}
1.37 + \item \texttt{\at}, \bold{8}, \hyperpage{189}
1.38 + \item \emph {$\in $}, \bold{189}
1.39 + \item \texttt {:}, \bold{189}
1.40 + \item \isasymnotin, \bold{189}
1.41 + \item \verb$~:$, \bold{189}
1.42 + \item \emph {$\subseteq $}, \bold{189}
1.43 + \item \emph {$\subset $}, \bold{189}
1.44 + \item \emph {$\cap $}, \bold{189}
1.45 + \item \emph {$\cup $}, \bold{189}
1.46 + \item \isasymInter, \bold{189}
1.47 + \item \isasymUnion, \bold{189}
1.48 + \item \isasyminverse, \bold{189}
1.49 + \item \verb$^-1$, \bold{189}
1.50 + \item \isactrlsup{\isacharasterisk}, \bold{189}
1.51 + \item \verb$^$\texttt{*}, \bold{189}
1.52 + \item \isasymAnd, \bold{10}, \bold{189}
1.53 + \item \ttAnd, \bold{189}
1.54 + \item \emph {$\equiv $}, \bold{23}, \bold{189}
1.55 + \item \texttt {==}, \bold{189}
1.56 + \item \emph {$\rightleftharpoons $}, \bold{23}, \bold{189}
1.57 + \item \emph {$\rightharpoonup $}, \bold{23}, \bold{189}
1.58 + \item \emph {$\leftharpoondown $}, \bold{23}, \bold{189}
1.59 + \item \emph {$\Rightarrow $}, \bold{3}, \bold{189}
1.60 + \item \texttt {=>}, \bold{189}
1.61 + \item \texttt {<=}, \bold{189}
1.62 + \item \emph {$\DOTSB \Relbar \joinrel \Rightarrow $}, \bold{189}
1.63 + \item \texttt {==>}, \bold{189}
1.64 + \item \emph {$\mathopen {[\mkern -3mu[}$}, \bold{10}, \bold{189}
1.65 + \item \ttlbr, \bold{189}
1.66 + \item \emph {$\mathclose {]\mkern -3mu]}$}, \bold{10}, \bold{189}
1.67 + \item \ttrbr, \bold{189}
1.68 + \item \emph {$\lambda $}, \bold{3}, \bold{189}
1.69 + \item \texttt {\%}, \bold{189}
1.70 + \item \texttt {,}, \bold{29}
1.71 + \item \texttt {;}, \bold{5}
1.72 + \item \emph {$\times $}, \bold{21}, \bold{189}
1.73 + \item \texttt {'a}, \bold{3}
1.74 + \item \texttt {()}, \bold{22}
1.75 + \item \texttt {::}, \bold{4}
1.76 + \item \isa {+} (tactical), \hyperpage{83}
1.77 + \item \isa {<*lex*>}, \see{lexicographic product}{1}
1.78 + \item \isa {?} (tactical), \hyperpage{83}
1.79 + \item \texttt{|} (tactical), \hyperpage{83}
1.80 +
1.81 + \indexspace
1.82 +
1.83 + \item \isa {0}, \bold{20}
1.84 + \item \texttt {0}, \bold{21}
1.85 +
1.86 + \indexspace
1.87 +
1.88 + \item abandon proof, \bold{11}
1.89 + \item abandon theory, \bold{14}
1.90 + \item \texttt {abs}, \bold{189}
1.91 + \item \isa {abs_mult} (theorem), \bold{135}
1.92 + \item \isa {add_2_eq_Suc} (theorem), \bold{133}
1.93 + \item \isa {add_2_eq_Suc'} (theorem), \bold{133}
1.94 + \item \isa {add_assoc} (theorem), \bold{134}
1.95 + \item \isa {add_commute} (theorem), \bold{134}
1.96 + \item \isa {add_left_commute} (theorem), \bold{134}
1.97 + \item \isa {add_mult_distrib} (theorem), \bold{133}
1.98 + \item \texttt {ALL}, \bold{189}
1.99 + \item \isa {All} (constant), \hyperpage{93}
1.100 + \item \isa {allE} (theorem), \bold{65}
1.101 + \item \isa {allI} (theorem), \bold{64}
1.102 + \item \isa {analz_Crypt_if} (theorem), \bold{186}
1.103 + \item \isa {analz_idem} (theorem), \bold{180}
1.104 + \item \isa {analz_mono} (theorem), \bold{180}
1.105 + \item \isa {analz_synth} (theorem), \bold{180}
1.106 + \item \isa {append_take_drop_id} (theorem), \bold{127}
1.107 + \item apply, \bold{13}
1.108 + \item \isa {arg_cong} (theorem), \bold{80}
1.109 + \item \isa {arith}, \bold{21}
1.110 + \item arithmetic, \hyperpage{20--21}, \hyperpage{31}
1.111 + \item \textsc {ascii} symbols, \bold{189}
1.112 + \item associative-commutative function, \hyperpage{158}
1.113 + \item \isa {assumption} (method), \hyperpage{53}
1.114 + \item assumptions
1.115 + \subitem renaming, \hyperpage{66--67}
1.116 + \subitem reusing, \hyperpage{67}
1.117 + \item \isa {auto}, \hyperpage{36}
1.118 + \item \isa {auto} (method), \hyperpage{76}
1.119 + \item \isa {axclass}, \hyperpage{144--150}
1.120 + \item axiom of choice, \hyperpage{70}
1.121 + \item axiomatic type class, \hyperpage{144--150}
1.122 +
1.123 + \indexspace
1.124 +
1.125 + \item \isacommand {back} (command), \hyperpage{62}
1.126 + \item \isa {Ball} (constant), \hyperpage{93}
1.127 + \item \isa {ballI} (theorem), \bold{92}
1.128 + \item \isa {best} (method), \hyperpage{75, 76}
1.129 + \item \isa {Bex} (constant), \hyperpage{93}
1.130 + \item \isa {bexE} (theorem), \bold{92}
1.131 + \item \isa {bexI} (theorem), \bold{92}
1.132 + \item \isa {bij_def} (theorem), \bold{94}
1.133 + \item bijections, \hyperpage{94}
1.134 + \item binomial coefficients, \hyperpage{93}
1.135 + \item bisimulation, \bold{100}
1.136 + \item \isa {blast} (method), \hyperpage{72--75}
1.137 + \item \isa {bool}, \hyperpage{2}, \bold{3}
1.138 + \item \isa {bspec} (theorem), \bold{92}
1.139 + \item \isacommand{by} (command), \hyperpage{57}
1.140 +
1.141 + \indexspace
1.142 +
1.143 + \item \isa {card} (constant), \hyperpage{93}
1.144 + \item \isa {card_Pow} (theorem), \bold{93}
1.145 + \item \isa {card_Un_Int} (theorem), \bold{93}
1.146 + \item cardinality, \hyperpage{93}
1.147 + \item \isa {case}, \bold{3}, \hyperpage{4}, \bold{16},
1.148 + \hyperpage{30, 31}
1.149 + \item case distinction, \bold{17}
1.150 + \item case splits, \bold{29}
1.151 + \item \isa {case_tac}, \bold{17}
1.152 + \item \isa {case_tac} (method), \hyperpage{85}
1.153 + \item \isa {clarify} (method), \hyperpage{74}, \hyperpage{76}
1.154 + \item \isa {clarsimp} (method), \hyperpage{75, 76}
1.155 + \item \isa {classical} (theorem), \bold{57}
1.156 + \item closure
1.157 + \subitem reflexive and transitive, \hyperpage{96--98}
1.158 + \item \isa {coinduct} (theorem), \bold{100}
1.159 + \item coinduction, \bold{100}
1.160 + \item \isa {Collect} (constant), \hyperpage{93}
1.161 + \item \isa {Collect_mem_eq} (theorem), \bold{91}
1.162 + \item \isa {comp_def} (theorem), \bold{96}
1.163 + \item \isa {comp_mono} (theorem), \bold{96}
1.164 + \item \isa {Compl_iff} (theorem), \bold{90}
1.165 + \item \isa {Compl_partition} (theorem), \bold{90}
1.166 + \item \isa {Compl_Un} (theorem), \bold{90}
1.167 + \item complement
1.168 + \subitem of a set, \hyperpage{89}
1.169 + \item composition
1.170 + \subitem of functions, \bold{94}
1.171 + \subitem of relations, \bold{96}
1.172 + \item congruence rules, \bold{157}
1.173 + \item \isa {conjE} (theorem), \bold{55}
1.174 + \item \isa {conjI} (theorem), \bold{52}
1.175 + \item \isa {Cons}, \bold{7}
1.176 + \item \isa {constdefs}, \bold{23}
1.177 + \item \isa {contrapos_nn} (theorem), \bold{57}
1.178 + \item \isa {contrapos_np} (theorem), \bold{57}
1.179 + \item \isa {contrapos_pn} (theorem), \bold{57}
1.180 + \item \isa {contrapos_pp} (theorem), \bold{57}
1.181 + \item contrapositives, \hyperpage{57}
1.182 + \item converse
1.183 + \subitem of a relation, \bold{96}
1.184 + \item \isa {converse_comp} (theorem), \bold{96}
1.185 + \item \isa {converse_iff} (theorem), \bold{96}
1.186 + \item CTL, \hyperpage{100--110}
1.187 +
1.188 + \indexspace
1.189 +
1.190 + \item \isa {datatype}, \hyperpage{7}, \hyperpage{36--42}
1.191 + \item \isa {defer}, \bold{14}
1.192 + \item \isacommand {defer} (command), \hyperpage{84}
1.193 + \item definition, \bold{23}
1.194 + \subitem unfolding, \bold{28}
1.195 + \item \isa {defs}, \bold{23}
1.196 + \item descriptions
1.197 + \subitem definite, \hyperpage{69}
1.198 + \subitem indefinite, \hyperpage{70}
1.199 + \item \isa {dest} (attribute), \hyperpage{86}
1.200 + \item destruction rules, \hyperpage{55}
1.201 + \item \isa {Diff_disjoint} (theorem), \bold{90}
1.202 + \item \isa {diff_mult_distrib} (theorem), \bold{133}
1.203 + \item difference
1.204 + \subitem of sets, \bold{90}
1.205 + \item \isa {disjCI} (theorem), \bold{58}
1.206 + \item \isa {disjE} (theorem), \bold{54}
1.207 + \item \isa {div}, \bold{20}
1.208 + \item \isa {div_le_mono} (theorem), \bold{133}
1.209 + \item \isa {div_mult1_eq} (theorem), \bold{133}
1.210 + \item \isa {div_mult2_eq} (theorem), \bold{133}
1.211 + \item \isa {div_mult_mult1} (theorem), \bold{133}
1.212 + \item divides relation, \bold{68}, \hyperpage{78}, \hyperpage{85--87}
1.213 + \item \isa {DIVISION_BY_ZERO_DIV} (theorem), \bold{134}
1.214 + \item \isa {DIVISION_BY_ZERO_MOD} (theorem), \bold{134}
1.215 + \item domain
1.216 + \subitem of a relation, \hyperpage{96}
1.217 + \item \isa {Domain_iff} (theorem), \bold{96}
1.218 + \item done, \bold{11}
1.219 + \item \isa {drule_tac} (method), \hyperpage{60}, \hyperpage{80}
1.220 + \item \isa {dvd_add} (theorem), \bold{79}, \bold{134}
1.221 + \item \isa {dvd_anti_sym} (theorem), \bold{134}
1.222 + \item \isa {dvd_def} (theorem), \bold{68}, \bold{78}, \bold{134}
1.223 + \item \isa {dvd_mod} (theorem), \bold{87}
1.224 + \item \isa {dvd_mod_imp_dvd} (theorem), \bold{86}
1.225 + \item \isa {dvd_refl} (theorem), \bold{79}
1.226 + \item \isa {dvd_trans} (theorem), \bold{87}
1.227 +
1.228 + \indexspace
1.229 +
1.230 + \item \isa {elim!} (attribute), \hyperpage{115}
1.231 + \item elimination rules, \hyperpage{53--54}
1.232 + \item \isa {Eps} (constant), \hyperpage{93}
1.233 + \item equality
1.234 + \subitem of functions, \bold{93}
1.235 + \subitem of sets, \bold{90}
1.236 + \item \isa {equalityE} (theorem), \bold{90}
1.237 + \item \isa {equalityI} (theorem), \bold{90}
1.238 + \item \isa {erule}, \hyperpage{54}
1.239 + \item \isa {erule_tac} (method), \hyperpage{60}
1.240 + \item Euclid's algorithm, \hyperpage{85--87}
1.241 + \item even numbers
1.242 + \subitem defining inductively, \hyperpage{111--115}
1.243 + \item \isa {even.cases} (theorem), \bold{114}
1.244 + \item \isa {even.induct} (theorem), \bold{112}
1.245 + \item \isa {even.step} (theorem), \bold{112}
1.246 + \item \isa {even.zero} (theorem), \bold{112}
1.247 + \item \texttt {EX}, \bold{189}
1.248 + \item \isa {Ex} (constant), \hyperpage{93}
1.249 + \item \isa {exE} (theorem), \bold{66}
1.250 + \item \isa {exI} (theorem), \bold{66}
1.251 + \item \isa {expand_fun_eq} (theorem), \bold{94}
1.252 + \item \isa {ext} (theorem), \bold{93}
1.253 + \item extensionality
1.254 + \subitem for functions, \bold{93, 94}
1.255 + \subitem for sets, \bold{90}
1.256 + \item \ttEXU, \bold{189}
1.257 +
1.258 + \indexspace
1.259 +
1.260 + \item \isa {False}, \bold{3}
1.261 + \item \isa {fast} (method), \hyperpage{75, 76}
1.262 + \item \isa {finite} (symbol), \hyperpage{93}
1.263 + \item \isa {Finites} (constant), \hyperpage{93}
1.264 + \item fixed points, \hyperpage{100}
1.265 + \item flag, \hyperpage{3, 4}, \hyperpage{31}
1.266 + \subitem (re)setting, \bold{3}
1.267 + \item \isa {force} (method), \hyperpage{75, 76}
1.268 + \item formula, \bold{3}
1.269 + \item forward proof, \hyperpage{76--82}
1.270 + \item \isa {frule} (method), \hyperpage{67}
1.271 + \item \isa {frule_tac} (method), \hyperpage{60}
1.272 + \item \isa {fst}, \bold{21}
1.273 + \item \isa {fun_upd_apply} (theorem), \bold{94}
1.274 + \item \isa {fun_upd_upd} (theorem), \bold{94}
1.275 + \item functions, \hyperpage{93--95}
1.276 +
1.277 + \indexspace
1.278 +
1.279 + \item \isa {gcd} (constant), \hyperpage{76--78}, \hyperpage{85--87}
1.280 + \item \isa {gcd_mult_distrib2} (theorem), \bold{77}
1.281 + \item generalizing for induction, \hyperpage{113}
1.282 + \item \isa {gfp_unfold} (theorem), \bold{100}
1.283 + \item Girard, Jean-Yves, \fnote{55}
1.284 + \item ground terms example, \hyperpage{119--124}
1.285 + \item \isa {gterm_Apply_elim} (theorem), \bold{123}
1.286 +
1.287 + \indexspace
1.288 +
1.289 + \item \isa {hd}, \bold{15}
1.290 + \item higher-order pattern, \bold{159}
1.291 + \item Hilbert's $\varepsilon$-operator, \hyperpage{69--71}
1.292 +
1.293 + \indexspace
1.294 +
1.295 + \item \isa {Id_def} (theorem), \bold{96}
1.296 + \item \isa {id_def} (theorem), \bold{94}
1.297 + \item identifier, \bold{4}
1.298 + \subitem qualified, \bold{2}
1.299 + \item identity function, \bold{94}
1.300 + \item identity relation, \bold{96}
1.301 + \item \isa {if}, \bold{3}, \hyperpage{4}
1.302 + \item \isa {iff} (attribute), \hyperpage{73, 74}, \hyperpage{86},
1.303 + \hyperpage{114}
1.304 + \item \isa {iffD1} (theorem), \bold{78}
1.305 + \item \isa {iffD2} (theorem), \bold{78}
1.306 + \item image
1.307 + \subitem under a function, \bold{95}
1.308 + \subitem under a relation, \bold{96}
1.309 + \item \isa {image_compose} (theorem), \bold{95}
1.310 + \item \isa {image_def} (theorem), \bold{95}
1.311 + \item \isa {Image_iff} (theorem), \bold{96}
1.312 + \item \isa {image_Int} (theorem), \bold{95}
1.313 + \item \isa {image_Un} (theorem), \bold{95}
1.314 + \item \isa {impI} (theorem), \bold{56}
1.315 + \item implication, \hyperpage{56--57}
1.316 + \item \isa {induct_tac}, \hyperpage{10}, \hyperpage{17},
1.317 + \hyperpage{50}, \hyperpage{172}
1.318 + \item induction, \hyperpage{168--175}
1.319 + \subitem recursion, \hyperpage{49--50}
1.320 + \subitem structural, \bold{17}
1.321 + \subitem well-founded, \hyperpage{99}
1.322 + \item \isacommand {inductive} (command), \hyperpage{111}
1.323 + \item inductive definition, \hyperpage{111--129}
1.324 + \subitem simultaneous, \hyperpage{125}
1.325 + \item \isacommand {inductive\_cases} (command), \hyperpage{115},
1.326 + \hyperpage{123}
1.327 + \item \isa {infixr}, \bold{8}
1.328 + \item \isa {inj_on_def} (theorem), \bold{94}
1.329 + \item injections, \hyperpage{94}
1.330 + \item inner syntax, \bold{9}
1.331 + \item \isa {insert} (constant), \hyperpage{91}
1.332 + \item \isa {insert} (method), \hyperpage{80--82}
1.333 + \item \isa {insert_is_Un} (theorem), \bold{91}
1.334 + \item instance, \bold{145}
1.335 + \item \texttt {INT}, \bold{189}
1.336 + \item \texttt {Int}, \bold{189}
1.337 + \item \isa {INT_iff} (theorem), \bold{92}
1.338 + \item \isa {IntD1} (theorem), \bold{89}
1.339 + \item \isa {IntD2} (theorem), \bold{89}
1.340 + \item \isa {INTER} (constant), \hyperpage{93}
1.341 + \item \texttt {Inter}, \bold{189}
1.342 + \item \isa {Inter_iff} (theorem), \bold{92}
1.343 + \item intersection, \hyperpage{89}
1.344 + \subitem indexed, \hyperpage{92}
1.345 + \item \isa {IntI} (theorem), \bold{89}
1.346 + \item \isa {intro} (method), \hyperpage{58}
1.347 + \item \isa {intro!} (attribute), \hyperpage{112}
1.348 + \item introduction rules, \hyperpage{52--53}
1.349 + \item \isa {inv} (constant), \hyperpage{70}
1.350 + \item \isa {inv_def} (theorem), \bold{70}
1.351 + \item \isa {inv_f_f} (theorem), \bold{94}
1.352 + \item \isa {inv_image_def} (theorem), \bold{99}
1.353 + \item \isa {inv_inv_eq} (theorem), \bold{94}
1.354 + \item inverse
1.355 + \subitem of a function, \bold{94}
1.356 + \subitem of a relation, \bold{96}
1.357 + \item inverse image
1.358 + \subitem of a function, \hyperpage{95}
1.359 + \subitem of a relation, \hyperpage{98}
1.360 +
1.361 + \indexspace
1.362 +
1.363 + \item \isa {kill}, \bold{14}
1.364 +
1.365 + \indexspace
1.366 +
1.367 + \item \isa {le_less_trans} (theorem), \bold{171}
1.368 + \item \isa {LEAST}, \bold{20}
1.369 + \item least number operator, \hyperpage{69}
1.370 + \item lemma, \hyperpage{11}
1.371 + \item \isa {lemma}, \bold{11}
1.372 + \item \isacommand {lemmas} (command), \hyperpage{77}, \hyperpage{86}
1.373 + \item \isa {length}, \bold{15}
1.374 + \item \isa {length_induct}, \bold{172}
1.375 + \item \isa {less_than} (constant), \hyperpage{98}
1.376 + \item \isa {less_than_iff} (theorem), \bold{98}
1.377 + \item \isa {let}, \bold{3}, \hyperpage{4}, \hyperpage{29}
1.378 + \item \isa {lex_prod_def} (theorem), \bold{99}
1.379 + \item lexicographic product, \bold{99}, \hyperpage{160}
1.380 + \item {\texttt{lfp}}
1.381 + \subitem applications of, \see{CTL}{100}
1.382 + \item \isa {lfp_induct} (theorem), \bold{100}
1.383 + \item \isa {lfp_unfold} (theorem), \bold{100}
1.384 + \item linear arithmetic, \bold{21}
1.385 + \item \isa {list}, \hyperpage{2}, \bold{7}, \bold{15}
1.386 + \item \isa {lists_Int_eq} (theorem), \bold{123}
1.387 + \item \isa {lists_mono} (theorem), \bold{121}
1.388 +
1.389 + \indexspace
1.390 +
1.391 + \item \isa {Main}, \bold{2}
1.392 + \item major premise, \bold{59}
1.393 + \item \isa {max}, \bold{20, 21}
1.394 + \item measure function, \bold{45}, \bold{98}
1.395 + \item \isa {measure_def} (theorem), \bold{99}
1.396 + \item \isa {mem_Collect_eq} (theorem), \bold{91}
1.397 + \item meta-logic, \bold{64}
1.398 + \item method, \bold{14}
1.399 + \item \isa {min}, \bold{20, 21}
1.400 + \item \isa {mod}, \bold{20}
1.401 + \item \isa {mod_div_equality} (theorem), \bold{81}, \bold{133}
1.402 + \item \isa {mod_if} (theorem), \bold{133}
1.403 + \item \isa {mod_mult1_eq} (theorem), \bold{133}
1.404 + \item \isa {mod_mult2_eq} (theorem), \bold{133}
1.405 + \item \isa {mod_mult_distrib} (theorem), \bold{133}
1.406 + \item \isa {mod_Suc} (theorem), \bold{80}
1.407 + \item \emph{modus ponens}, \hyperpage{51}, \hyperpage{56}
1.408 + \item \isa {mono_def} (theorem), \bold{100}
1.409 + \item \isa {mono_Int} (theorem), \bold{123}
1.410 + \item \isa {monoD} (theorem), \bold{100}
1.411 + \item \isa {monoI} (theorem), \bold{100}
1.412 + \item monotone functions, \bold{100}, \hyperpage{123}
1.413 + \subitem and inductive definitions, \hyperpage{121--122}
1.414 + \item \isa {mp} (theorem), \bold{56}
1.415 + \item \isa {mult_commute} (theorem), \bold{61}
1.416 + \item \isa {mult_le_mono} (theorem), \bold{133}
1.417 + \item \isa {mult_le_mono1} (theorem), \bold{80}
1.418 + \item \isa {mult_less_mono1} (theorem), \bold{133}
1.419 + \item multiset ordering, \bold{99}
1.420 +
1.421 + \indexspace
1.422 +
1.423 + \item \isa {n_subsets} (theorem), \bold{93}
1.424 + \item \isa {nat}, \hyperpage{2}, \bold{20}
1.425 + \item \isa {nat_diff_split} (theorem), \bold{134}
1.426 + \item natural deduction, \hyperpage{51--52}
1.427 + \item \isa {neg_mod_bound} (theorem), \bold{135}
1.428 + \item \isa {neg_mod_sign} (theorem), \bold{135}
1.429 + \item negation, \hyperpage{57--59}
1.430 + \item \isa {Nil}, \bold{7}
1.431 + \item \isa {no_asm}, \bold{27}
1.432 + \item \isa {no_asm_simp}, \bold{27}
1.433 + \item \isa {no_asm_use}, \bold{28}
1.434 + \item \isa {None}, \bold{22}
1.435 + \item \isa {notE} (theorem), \bold{57}
1.436 + \item \isa {notI} (theorem), \bold{57}
1.437 + \item \isa {numeral_0_eq_0} (theorem), \bold{133}
1.438 + \item \isa {numeral_1_eq_1} (theorem), \bold{133}
1.439 +
1.440 + \indexspace
1.441 +
1.442 + \item \isa {O} (symbol), \hyperpage{96}
1.443 + \item \texttt {o}, \bold{189}
1.444 + \item \isa {o_assoc} (theorem), \bold{94}
1.445 + \item \isa {o_def} (theorem), \bold{94}
1.446 + \item \isa {OF} (attribute), \hyperpage{78--79}
1.447 + \item \isa {of} (attribute), \hyperpage{77}, \hyperpage{79}
1.448 + \item \isa {oops}, \bold{11}
1.449 + \item \isa {option}, \bold{22}
1.450 + \item \isa {order_antisym} (theorem), \bold{69}
1.451 + \item ordered rewriting, \bold{158}
1.452 + \item outer syntax, \bold{9}
1.453 + \item overloading, \hyperpage{144--146}
1.454 +
1.455 + \indexspace
1.456 +
1.457 + \item pair, \bold{21}, \hyperpage{137--140}
1.458 + \item parent theory, \bold{2}
1.459 + \item partial function, \hyperpage{164}
1.460 + \item pattern, higher-order, \bold{159}
1.461 + \item PDL, \hyperpage{102--105}
1.462 + \item permutative rewrite rule, \bold{158}
1.463 + \item \isa {pos_mod_bound} (theorem), \bold{135}
1.464 + \item \isa {pos_mod_sign} (theorem), \bold{135}
1.465 + \item \isa {pr}, \bold{14}
1.466 + \item \isacommand {pr} (command), \hyperpage{83}
1.467 + \item \isa {prefer}, \bold{14}
1.468 + \item \isacommand {prefer} (command), \hyperpage{84}
1.469 + \item primitive recursion, \bold{16}
1.470 + \item \isa {primrec}, \hyperpage{8}, \bold{16}, \hyperpage{36--42}
1.471 + \item product type, \see{pair}{1}
1.472 + \item proof
1.473 + \subitem abandon, \bold{11}
1.474 + \item Proof General, \bold{5}
1.475 + \item proofs
1.476 + \subitem examples of failing, \hyperpage{71--72}
1.477 +
1.478 + \indexspace
1.479 +
1.480 + \item quantifiers
1.481 + \subitem and inductive definitions, \hyperpage{119--121}
1.482 + \subitem existential, \hyperpage{66}
1.483 + \subitem for sets, \hyperpage{92}
1.484 + \subitem instantiating, \hyperpage{68}
1.485 + \subitem universal, \hyperpage{63--66}
1.486 +
1.487 + \indexspace
1.488 +
1.489 + \item \isa {r_into_rtrancl} (theorem), \bold{96}
1.490 + \item \isa {r_into_trancl} (theorem), \bold{97}
1.491 + \item \isa {R_O_Id} (theorem), \bold{96}
1.492 + \item range
1.493 + \subitem of a function, \hyperpage{95}
1.494 + \subitem of a relation, \hyperpage{96}
1.495 + \item \isa {range} (symbol), \hyperpage{95}
1.496 + \item \isa {Range_iff} (theorem), \bold{96}
1.497 + \item \isa {real_add_divide_distrib} (theorem), \bold{136}
1.498 + \item \isa {real_dense} (theorem), \bold{136}
1.499 + \item \isa {real_divide_divide1_eq} (theorem), \bold{136}
1.500 + \item \isa {real_divide_divide2_eq} (theorem), \bold{136}
1.501 + \item \isa {real_divide_minus_eq} (theorem), \bold{136}
1.502 + \item \isa {real_minus_divide_eq} (theorem), \bold{136}
1.503 + \item \isa {real_times_divide1_eq} (theorem), \bold{136}
1.504 + \item \isa {real_times_divide2_eq} (theorem), \bold{136}
1.505 + \item \isa {realpow_abs} (theorem), \bold{136}
1.506 + \item \isa {recdef}, \hyperpage{45--50}, \hyperpage{160--168}
1.507 + \item \isacommand {recdef} (command), \hyperpage{98}
1.508 + \item \isa {recdef_cong}, \bold{164}
1.509 + \item \isa {recdef_simp}, \bold{47}
1.510 + \item \isa {recdef_wf}, \bold{162}
1.511 + \item recursion
1.512 + \subitem well-founded, \bold{161}
1.513 + \item recursion induction, \hyperpage{49--50}
1.514 + \item \isa {redo}, \bold{14}
1.515 + \item relations, \hyperpage{95--98}
1.516 + \subitem well-founded, \hyperpage{98--99}
1.517 + \item \isa {relprime_dvd_mult} (theorem), \bold{78}
1.518 + \item \isa {rename_tac} (method), \hyperpage{66--67}
1.519 + \item \isa {rev}, \bold{8}
1.520 + \item rewrite rule, \bold{26}
1.521 + \subitem permutative, \bold{158}
1.522 + \item rewriting, \bold{26}
1.523 + \subitem ordered, \bold{158}
1.524 + \item \isa {rotate_tac}, \bold{28}
1.525 + \item \isa {rtrancl_idemp} (theorem), \bold{97}
1.526 + \item \isa {rtrancl_induct} (theorem), \bold{97}
1.527 + \item \isa {rtrancl_refl} (theorem), \bold{96}
1.528 + \item \isa {rtrancl_trans} (theorem), \bold{96}
1.529 + \item \isa {rtrancl_unfold} (theorem), \bold{96}
1.530 + \item rule induction, \hyperpage{112--114}
1.531 + \item rule inversion, \hyperpage{114--115}, \hyperpage{123--124}
1.532 + \item \isa {rule_tac} (method), \hyperpage{60}
1.533 + \subitem and renaming, \hyperpage{67}
1.534 +
1.535 + \indexspace
1.536 +
1.537 + \item \isa {safe} (method), \hyperpage{75, 76}
1.538 + \item safe rules, \bold{73}
1.539 + \item schematic variable, \bold{4}
1.540 + \item \isa {set}, \hyperpage{2}
1.541 + \item {\textit {set}} (type), \hyperpage{89}
1.542 + \item set comprehensions, \hyperpage{91--92}
1.543 + \item \isa {set_ext} (theorem), \bold{90}
1.544 + \item sets, \hyperpage{89--93}
1.545 + \subitem finite, \hyperpage{93}
1.546 + \subitem notation for finite, \bold{91}
1.547 + \item \isa {show_brackets}, \bold{4}
1.548 + \item \isa {show_types}, \bold{3}
1.549 + \item \texttt {show_types}, \hyperpage{14}
1.550 + \item \isa {simp} (attribute), \bold{9}, \hyperpage{26}
1.551 + \item \isa {simp} (method), \bold{26}
1.552 + \item \isa {simp_all}, \hyperpage{26}, \hyperpage{36}
1.553 + \item simplification, \hyperpage{25--32}, \hyperpage{157--160}
1.554 + \subitem of let-expressions, \hyperpage{29}
1.555 + \subitem ordered, \bold{158}
1.556 + \subitem with definitions, \hyperpage{28}
1.557 + \subitem with/of assumptions, \hyperpage{27}
1.558 + \item simplification rule, \bold{26}, \hyperpage{159--160}
1.559 + \item \isa {simplified} (attribute), \hyperpage{77}, \hyperpage{79}
1.560 + \item simplifier, \bold{25}
1.561 + \item \isa {size}, \bold{15}
1.562 + \item \isa {snd}, \bold{21}
1.563 + \item \isa {SOME} (symbol), \hyperpage{69}
1.564 + \item \texttt {SOME}, \bold{189}
1.565 + \item \isa {Some}, \bold{22}
1.566 + \item \isa {some_equality} (theorem), \bold{69}
1.567 + \item \isa {someI} (theorem), \bold{70}, \bold{75}
1.568 + \item \isa {someI2} (theorem), \bold{70}
1.569 + \item \isa {someI_ex} (theorem, \bold){71}
1.570 + \item sort, \bold{150}
1.571 + \item \isa {spec} (theorem), \bold{64}
1.572 + \item \isa {split} (constant), \bold{137}
1.573 + \item \isa {split} (method, attr.), \hyperpage{29--31}
1.574 + \item split rule, \bold{30}
1.575 + \item \isa {split_if}, \bold{30}
1.576 + \item \isa {ssubst} (theorem), \bold{61}
1.577 + \item structural induction, \bold{17}
1.578 + \item \isa {subgoal_tac} (method), \hyperpage{81, 82}
1.579 + \item subset relation, \bold{90}
1.580 + \item \isa {subsetD} (theorem), \bold{90}
1.581 + \item \isa {subsetI} (theorem), \bold{90}
1.582 + \item \isa {subst} (method), \hyperpage{61}
1.583 + \item substitution, \hyperpage{61--63}
1.584 + \item \isa {Suc}, \bold{20}
1.585 + \item \isa {Suc_leI} (theorem), \bold{171}
1.586 + \item \isa {Suc_Suc_cases} (theorem), \bold{115}
1.587 + \item \isa {surj_def} (theorem), \bold{94}
1.588 + \item \isa {surj_f_inv_f} (theorem), \bold{94}
1.589 + \item surjections, \hyperpage{94}
1.590 + \item \isa {sym} (theorem), \bold{77}
1.591 + \item syntax translation, \bold{23}
1.592 +
1.593 + \indexspace
1.594 +
1.595 + \item tactic, \bold{10}
1.596 + \item tacticals, \hyperpage{82--83}
1.597 + \item term, \bold{3}
1.598 + \item \isa {term}, \bold{14}
1.599 + \item term rewriting, \bold{26}
1.600 + \item termination, \see{total function}{1}
1.601 + \item \isa {THEN} (attribute), \bold{77}, \hyperpage{79},
1.602 + \hyperpage{86}
1.603 + \item theorem, \hyperpage{11}
1.604 + \item \isa {theorem}, \bold{9}, \hyperpage{11}
1.605 + \item theory, \bold{2}
1.606 + \subitem abandon, \bold{14}
1.607 + \item theory file, \bold{2}
1.608 + \item \isa {thm}, \bold{14}
1.609 + \item \isa {tl}, \bold{15}
1.610 + \item total function, \hyperpage{9}
1.611 + \item \isa {trace_simp}, \bold{31}
1.612 + \item tracing the simplifier, \bold{31}
1.613 + \item \isa {trancl_converse} (theorem), \bold{97}
1.614 + \item \isa {trancl_trans} (theorem), \bold{97}
1.615 + \item \isa {translations}, \bold{23}
1.616 + \item \isa {True}, \bold{3}
1.617 + \item tuple, \see{pair}{1}
1.618 + \item \isa {typ}, \bold{14}
1.619 + \item type, \bold{2}
1.620 + \item type constraint, \bold{4}
1.621 + \item type declaration, \bold{150}
1.622 + \item type definition, \bold{151}
1.623 + \item type inference, \bold{3}
1.624 + \item type synonym, \bold{22}
1.625 + \item type variable, \bold{3}
1.626 + \item \isa {typedecl}, \bold{151}
1.627 + \item \isa {typedef}, \bold{151}
1.628 + \item \isa {types}, \bold{22}
1.629 +
1.630 + \indexspace
1.631 +
1.632 + \item \texttt {UN}, \bold{189}
1.633 + \item \texttt {Un}, \bold{189}
1.634 + \item \isa {UN_E} (theorem), \bold{92}
1.635 + \item \isa {UN_I} (theorem), \bold{92}
1.636 + \item \isa {UN_iff} (theorem), \bold{92}
1.637 + \item \isa {Un_subset_iff} (theorem), \bold{90}
1.638 + \item underdefined function, \hyperpage{165}
1.639 + \item \isa {undo}, \bold{14}
1.640 + \item \isa {unfold}, \bold{28}
1.641 + \item unification, \hyperpage{60--63}
1.642 + \item \isa {UNION} (constant), \hyperpage{93}
1.643 + \item \texttt {Union}, \bold{189}
1.644 + \item union
1.645 + \subitem indexed, \hyperpage{92}
1.646 + \item \isa {Union_iff} (theorem), \bold{92}
1.647 + \item \isa {unit}, \bold{22}
1.648 + \item unknown, \bold{4}
1.649 + \item unknowns, \bold{52}
1.650 + \item unsafe rules, \bold{73}
1.651 + \item updating a function, \bold{93}
1.652 +
1.653 + \indexspace
1.654 +
1.655 + \item variable, \bold{4}
1.656 + \subitem schematic, \bold{4}
1.657 + \subitem type, \bold{3}
1.658 + \item \isa {vimage_Compl} (theorem), \bold{95}
1.659 + \item \isa {vimage_def} (theorem), \bold{95}
1.660 +
1.661 + \indexspace
1.662 +
1.663 + \item \isa {wf_induct} (theorem), \bold{99}
1.664 + \item \isa {wf_inv_image} (theorem), \bold{99}
1.665 + \item \isa {wf_less_than} (theorem), \bold{98}
1.666 + \item \isa {wf_lex_prod} (theorem), \bold{99}
1.667 + \item \isa {wf_measure} (theorem), \bold{99}
1.668 + \item \isa {while}, \bold{167}
1.669 +
1.670 + \indexspace
1.671 +
1.672 + \item \isa {zdiv_zadd1_eq} (theorem), \bold{135}
1.673 + \item \isa {zdiv_zmult1_eq} (theorem), \bold{135}
1.674 + \item \isa {zdiv_zmult2_eq} (theorem), \bold{135}
1.675 + \item \isa {zmod_zadd1_eq} (theorem), \bold{135}
1.676 + \item \isa {zmod_zmult1_eq} (theorem), \bold{135}
1.677 + \item \isa {zmod_zmult2_eq} (theorem), \bold{135}
1.678 +
1.679 +\end{theindex}