1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/TutorialI/Documents/Documents.thy Mon Oct 01 14:44:00 2001 +0200
1.3 @@ -0,0 +1,7 @@
1.4 +(*<*)
1.5 +theory Documents = Main:
1.6 +(*>*)
1.7 +
1.8 +(*<*)
1.9 +end
1.10 +(*>*)
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/TutorialI/Documents/ROOT.ML Mon Oct 01 14:44:00 2001 +0200
2.3 @@ -0,0 +1,2 @@
2.4 +
2.5 +use_thy "Documents";
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/TutorialI/Documents/document/root.tex Mon Oct 01 14:44:00 2001 +0200
3.3 @@ -0,0 +1,4 @@
3.4 +\documentclass{article}
3.5 +\begin{document}
3.6 +xxx
3.7 +\end{document}
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/TutorialI/Documents/documents.tex Mon Oct 01 14:44:00 2001 +0200
4.3 @@ -0,0 +1,10 @@
4.4 +
4.5 +\chapter{Document preparation}
4.6 +
4.7 +\input{Documents/document/Documents.tex}
4.8 +
4.9 +
4.10 +%%% Local Variables:
4.11 +%%% mode: latex
4.12 +%%% TeX-master: t
4.13 +%%% End:
5.1 --- a/doc-src/TutorialI/IsaMakefile Mon Oct 01 14:42:47 2001 +0200
5.2 +++ b/doc-src/TutorialI/IsaMakefile Mon Oct 01 14:44:00 2001 +0200
5.3 @@ -4,7 +4,9 @@
5.4
5.5 ## targets
5.6
5.7 -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Real-Types HOL-Misc HOL-Protocol styles
5.8 +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef \
5.9 + HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Real-Types HOL-Misc \
5.10 + HOL-Protocol HOL-Documents styles
5.11 images:
5.12 test:
5.13 all: default
5.14 @@ -185,7 +187,15 @@
5.15 $(USEDIR) Protocol
5.16 @rm -f tutorial.dvi
5.17
5.18 +## HOL-Documents
5.19 +
5.20 +HOL-Documents: HOL $(LOG)/HOL-Documents.gz
5.21 +
5.22 +$(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML
5.23 + $(USEDIR) Documents
5.24 + @rm -f tutorial.dvi
5.25 +
5.26 ## clean
5.27
5.28 clean:
5.29 - @rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz Rules/document/*.tex Sets/document/*.tex
5.30 + @rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz $(LOG)/HOL-Documents.gz Rules/document/*.tex Sets/document/*.tex
6.1 --- a/doc-src/TutorialI/Makefile Mon Oct 01 14:42:47 2001 +0200
6.2 +++ b/doc-src/TutorialI/Makefile Mon Oct 01 14:44:00 2001 +0200
6.3 @@ -22,6 +22,7 @@
6.4 Protocol/protocol.tex \
6.5 Rules/rules.tex Sets/sets.tex \
6.6 Types/numerics.tex Types/records.tex Types/types.tex \
6.7 + Documents/documents.tex \
6.8 ../iman.sty ../ttbox.sty ../extra.sty \
6.9 isabelle.sty isabellesym.sty ../pdfsetup.sty
6.10
7.1 --- a/doc-src/TutorialI/tutorial.ind Mon Oct 01 14:42:47 2001 +0200
7.2 +++ b/doc-src/TutorialI/tutorial.ind Mon Oct 01 14:44:00 2001 +0200
7.3 @@ -1,630 +1,630 @@
7.4 \begin{theindex}
7.5
7.6 - \item \ttall, \bold{187}
7.7 - \item \texttt{?}, \bold{187}
7.8 - \item \isasymuniqex, \bold{187}
7.9 - \item \ttuniquex, \bold{187}
7.10 - \item {\texttt {\&}}, \bold{187}
7.11 - \item \verb$~$, \bold{187}
7.12 - \item \verb$~=$, \bold{187}
7.13 - \item \ttor, \bold{187}
7.14 - \item \texttt{[]}, \bold{7}
7.15 - \item \texttt{\#}, \bold{7}
7.16 - \item \texttt{\at}, \bold{8}, 187
7.17 - \item \isasymnotin, \bold{187}
7.18 - \item \verb$~:$, \bold{187}
7.19 - \item \isasymInter, \bold{187}
7.20 - \item \isasymUnion, \bold{187}
7.21 - \item \isasyminverse, \bold{187}
7.22 - \item \verb$^-1$, \bold{187}
7.23 - \item \isactrlsup{\isacharasterisk}, \bold{187}
7.24 - \item \verb$^$\texttt{*}, \bold{187}
7.25 - \item \isasymAnd, \bold{10}, \bold{187}
7.26 - \item \ttAnd, \bold{187}
7.27 - \item \isasymrightleftharpoons, 24
7.28 - \item \isasymrightharpoonup, 24
7.29 - \item \isasymleftharpoondown, 24
7.30 - \item \emph {$\Rightarrow $}, \bold{3}
7.31 - \item \ttlbr, \bold{187}
7.32 - \item \ttrbr, \bold{187}
7.33 - \item \texttt {\%}, \bold{187}
7.34 - \item \texttt {;}, \bold{5}
7.35 - \item \isa {()} (constant), 22
7.36 - \item \isa {+} (tactical), 83
7.37 + \item \ttall, \bold{195}
7.38 + \item \texttt{?}, \bold{195}
7.39 + \item \isasymuniqex, \bold{195}
7.40 + \item \ttuniquex, \bold{195}
7.41 + \item {\texttt {\&}}, \bold{195}
7.42 + \item \verb$~$, \bold{195}
7.43 + \item \verb$~=$, \bold{195}
7.44 + \item \ttor, \bold{195}
7.45 + \item \texttt{[]}, \bold{9}
7.46 + \item \texttt{\#}, \bold{9}
7.47 + \item \texttt{\at}, \bold{10}, 195
7.48 + \item \isasymnotin, \bold{195}
7.49 + \item \verb$~:$, \bold{195}
7.50 + \item \isasymInter, \bold{195}
7.51 + \item \isasymUnion, \bold{195}
7.52 + \item \isasyminverse, \bold{195}
7.53 + \item \verb$^-1$, \bold{195}
7.54 + \item \isactrlsup{\isacharasterisk}, \bold{195}
7.55 + \item \verb$^$\texttt{*}, \bold{195}
7.56 + \item \isasymAnd, \bold{12}, \bold{195}
7.57 + \item \ttAnd, \bold{195}
7.58 + \item \isasymrightleftharpoons, 26
7.59 + \item \isasymrightharpoonup, 26
7.60 + \item \isasymleftharpoondown, 26
7.61 + \item \emph {$\Rightarrow $}, \bold{5}
7.62 + \item \ttlbr, \bold{195}
7.63 + \item \ttrbr, \bold{195}
7.64 + \item \texttt {\%}, \bold{195}
7.65 + \item \texttt {;}, \bold{7}
7.66 + \item \isa {()} (constant), 24
7.67 + \item \isa {+} (tactical), 89
7.68 \item \isa {<*lex*>}, \see{lexicographic product}{1}
7.69 - \item \isa {?} (tactical), 83
7.70 - \item \texttt{|} (tactical), 83
7.71 + \item \isa {?} (tactical), 89
7.72 + \item \texttt{|} (tactical), 89
7.73
7.74 \indexspace
7.75
7.76 - \item \isa {0} (constant), 20, 21, 133
7.77 - \item \isa {1} (symbol), 133
7.78 - \item \isa {2} (symbol), 133
7.79 + \item \isa {0} (constant), 22, 23, 141
7.80 + \item \isa {1} (symbol), 141
7.81 + \item \isa {2} (symbol), 141
7.82
7.83 \indexspace
7.84
7.85 - \item abandoning a proof, \bold{11}
7.86 - \item abandoning a theory, \bold{14}
7.87 - \item \isa {abs} (constant), 135
7.88 - \item \texttt {abs}, \bold{187}
7.89 - \item absolute value, 135
7.90 - \item \isa {add} (modifier), 27
7.91 - \item \isa {add_ac} (theorems), 134
7.92 - \item \isa {add_assoc} (theorem), \bold{134}
7.93 - \item \isa {add_commute} (theorem), \bold{134}
7.94 - \item \isa {add_mult_distrib} (theorem), \bold{133}
7.95 - \item \texttt {ALL}, \bold{187}
7.96 - \item \isa {All} (constant), 93
7.97 - \item \isa {allE} (theorem), \bold{65}
7.98 - \item \isa {allI} (theorem), \bold{64}
7.99 - \item append function, 8--12
7.100 - \item \isacommand {apply} (command), 13
7.101 - \item \isa {arg_cong} (theorem), \bold{80}
7.102 - \item \isa {arith} (method), 21, 131
7.103 + \item abandoning a proof, \bold{13}
7.104 + \item abandoning a theory, \bold{16}
7.105 + \item \isa {abs} (constant), 143
7.106 + \item \texttt {abs}, \bold{195}
7.107 + \item absolute value, 143
7.108 + \item \isa {add} (modifier), 29
7.109 + \item \isa {add_ac} (theorems), 142
7.110 + \item \isa {add_assoc} (theorem), \bold{142}
7.111 + \item \isa {add_commute} (theorem), \bold{142}
7.112 + \item \isa {add_mult_distrib} (theorem), \bold{141}
7.113 + \item \texttt {ALL}, \bold{195}
7.114 + \item \isa {All} (constant), 99
7.115 + \item \isa {allE} (theorem), \bold{71}
7.116 + \item \isa {allI} (theorem), \bold{70}
7.117 + \item append function, 10--14
7.118 + \item \isacommand {apply} (command), 15
7.119 + \item \isa {arg_cong} (theorem), \bold{86}
7.120 + \item \isa {arith} (method), 23, 139
7.121 \item arithmetic operations
7.122 - \subitem for \protect\isa{nat}, 21
7.123 - \item \textsc {ascii} symbols, \bold{187}
7.124 - \item associative-commutative function, 156
7.125 - \item \isa {assumption} (method), 53
7.126 + \subitem for \protect\isa{nat}, 23
7.127 + \item \textsc {ascii} symbols, \bold{195}
7.128 + \item associative-commutative function, 164
7.129 + \item \isa {assumption} (method), 59
7.130 \item assumptions
7.131 - \subitem of subgoal, 10
7.132 - \subitem renaming, 66--67
7.133 - \subitem reusing, 67
7.134 - \item \isa {auto} (method), 35, 76
7.135 - \item \isa {axclass}, 144--150
7.136 - \item axiom of choice, 70
7.137 - \item axiomatic type classes, 144--150
7.138 + \subitem of subgoal, 12
7.139 + \subitem renaming, 72--73
7.140 + \subitem reusing, 73
7.141 + \item \isa {auto} (method), 37, 82
7.142 + \item \isa {axclass}, 152--158
7.143 + \item axiom of choice, 76
7.144 + \item axiomatic type classes, 152--158
7.145
7.146 \indexspace
7.147
7.148 - \item \isacommand {back} (command), 62
7.149 - \item \isa {Ball} (constant), 93
7.150 - \item \isa {ballI} (theorem), \bold{92}
7.151 - \item \isa {best} (method), 76
7.152 - \item \isa {Bex} (constant), 93
7.153 - \item \isa {bexE} (theorem), \bold{92}
7.154 - \item \isa {bexI} (theorem), \bold{92}
7.155 - \item \isa {bij_def} (theorem), \bold{94}
7.156 - \item bijections, 94
7.157 - \item binary trees, 16
7.158 - \item binomial coefficients, 93
7.159 - \item bisimulations, 100
7.160 - \item \isa {blast} (method), 73--74, 76
7.161 - \item \isa {bool} (type), 2, 3
7.162 - \item boolean expressions example, 18--20
7.163 - \item \isa {bspec} (theorem), \bold{92}
7.164 - \item \isacommand{by} (command), 57
7.165 + \item \isacommand {back} (command), 68
7.166 + \item \isa {Ball} (constant), 99
7.167 + \item \isa {ballI} (theorem), \bold{98}
7.168 + \item \isa {best} (method), 82
7.169 + \item \isa {Bex} (constant), 99
7.170 + \item \isa {bexE} (theorem), \bold{98}
7.171 + \item \isa {bexI} (theorem), \bold{98}
7.172 + \item \isa {bij_def} (theorem), \bold{100}
7.173 + \item bijections, 100
7.174 + \item binary trees, 18
7.175 + \item binomial coefficients, 99
7.176 + \item bisimulations, 106
7.177 + \item \isa {blast} (method), 79--80, 82
7.178 + \item \isa {bool} (type), 4, 5
7.179 + \item boolean expressions example, 20--22
7.180 + \item \isa {bspec} (theorem), \bold{98}
7.181 + \item \isacommand{by} (command), 63
7.182
7.183 \indexspace
7.184
7.185 - \item \isa {card} (constant), 93
7.186 - \item \isa {card_Pow} (theorem), \bold{93}
7.187 - \item \isa {card_Un_Int} (theorem), \bold{93}
7.188 - \item cardinality, 93
7.189 - \item \isa {case} (symbol), 30, 31
7.190 - \item \isa {case} expressions, 3, 4, 16
7.191 - \item case distinctions, 17
7.192 - \item case splits, \bold{29}
7.193 - \item \isa {case_tac} (method), 17, 85, 139
7.194 - \item \isa {clarify} (method), 75, 76
7.195 - \item \isa {clarsimp} (method), 75, 76
7.196 - \item \isa {classical} (theorem), \bold{57}
7.197 - \item coinduction, \bold{100}
7.198 - \item \isa {Collect} (constant), 93
7.199 - \item \isa {comp_def} (theorem), \bold{96}
7.200 - \item compiling expressions example, 34--36
7.201 - \item \isa {Compl_iff} (theorem), \bold{90}
7.202 + \item \isa {card} (constant), 99
7.203 + \item \isa {card_Pow} (theorem), \bold{99}
7.204 + \item \isa {card_Un_Int} (theorem), \bold{99}
7.205 + \item cardinality, 99
7.206 + \item \isa {case} (symbol), 32, 33
7.207 + \item \isa {case} expressions, 5, 6, 18
7.208 + \item case distinctions, 19
7.209 + \item case splits, \bold{31}
7.210 + \item \isa {case_tac} (method), 19, 91, 147
7.211 + \item \isa {clarify} (method), 81, 82
7.212 + \item \isa {clarsimp} (method), 81, 82
7.213 + \item \isa {classical} (theorem), \bold{63}
7.214 + \item coinduction, \bold{106}
7.215 + \item \isa {Collect} (constant), 99
7.216 + \item \isa {comp_def} (theorem), \bold{102}
7.217 + \item compiling expressions example, 36--38
7.218 + \item \isa {Compl_iff} (theorem), \bold{96}
7.219 \item complement
7.220 - \subitem of a set, 89
7.221 + \subitem of a set, 95
7.222 \item composition
7.223 - \subitem of functions, \bold{94}
7.224 - \subitem of relations, \bold{96}
7.225 + \subitem of functions, \bold{100}
7.226 + \subitem of relations, \bold{102}
7.227 \item conclusion
7.228 - \subitem of subgoal, 10
7.229 + \subitem of subgoal, 12
7.230 \item conditional expressions, \see{\isa{if} expressions}{1}
7.231 - \item conditional simplification rules, 29
7.232 - \item \isa {cong} (attribute), 156
7.233 - \item congruence rules, \bold{155}
7.234 - \item \isa {conjE} (theorem), \bold{55}
7.235 - \item \isa {conjI} (theorem), \bold{52}
7.236 - \item \isa {Cons} (constant), 7
7.237 - \item \isacommand {constdefs} (command), 23
7.238 - \item \isacommand {consts} (command), 8
7.239 - \item contrapositives, 57
7.240 + \item conditional simplification rules, 31
7.241 + \item \isa {cong} (attribute), 164
7.242 + \item congruence rules, \bold{163}
7.243 + \item \isa {conjE} (theorem), \bold{61}
7.244 + \item \isa {conjI} (theorem), \bold{58}
7.245 + \item \isa {Cons} (constant), 9
7.246 + \item \isacommand {constdefs} (command), 25
7.247 + \item \isacommand {consts} (command), 10
7.248 + \item contrapositives, 63
7.249 \item converse
7.250 - \subitem of a relation, \bold{96}
7.251 - \item \isa {converse_iff} (theorem), \bold{96}
7.252 - \item CTL, 105--110, 171--173
7.253 + \subitem of a relation, \bold{102}
7.254 + \item \isa {converse_iff} (theorem), \bold{102}
7.255 + \item CTL, 111--116, 179--181
7.256
7.257 \indexspace
7.258
7.259 - \item \isacommand {datatype} (command), 7, 36--41
7.260 - \item datatypes, 15--20
7.261 - \subitem and nested recursion, 38, 42
7.262 - \subitem mutually recursive, 36
7.263 - \subitem nested, 160
7.264 - \item \isacommand {defer} (command), 14, 84
7.265 - \item Definitional Approach, 24
7.266 - \item definitions, \bold{23}
7.267 - \subitem unfolding, \bold{28}
7.268 - \item \isacommand {defs} (command), 23
7.269 - \item \isa {del} (modifier), 27
7.270 - \item description operators, 69--71
7.271 + \item \isacommand {datatype} (command), 9, 38--43
7.272 + \item datatypes, 17--22
7.273 + \subitem and nested recursion, 40, 44
7.274 + \subitem mutually recursive, 38
7.275 + \subitem nested, 168
7.276 + \item \isacommand {defer} (command), 16, 90
7.277 + \item Definitional Approach, 26
7.278 + \item definitions, \bold{25}
7.279 + \subitem unfolding, \bold{30}
7.280 + \item \isacommand {defs} (command), 25
7.281 + \item \isa {del} (modifier), 29
7.282 + \item description operators, 75--77
7.283 \item descriptions
7.284 - \subitem definite, 69
7.285 - \subitem indefinite, 70
7.286 - \item \isa {dest} (attribute), 86
7.287 - \item destruction rules, 55
7.288 - \item \isa {diff_mult_distrib} (theorem), \bold{133}
7.289 + \subitem definite, 75
7.290 + \subitem indefinite, 76
7.291 + \item \isa {dest} (attribute), 92
7.292 + \item destruction rules, 61
7.293 + \item \isa {diff_mult_distrib} (theorem), \bold{141}
7.294 \item difference
7.295 - \subitem of sets, \bold{90}
7.296 - \item \isa {disjCI} (theorem), \bold{58}
7.297 - \item \isa {disjE} (theorem), \bold{54}
7.298 - \item \isa {div} (symbol), 21
7.299 - \item divides relation, 68, 79, 85--88, 134
7.300 + \subitem of sets, \bold{96}
7.301 + \item \isa {disjCI} (theorem), \bold{64}
7.302 + \item \isa {disjE} (theorem), \bold{60}
7.303 + \item \isa {div} (symbol), 23
7.304 + \item divides relation, 74, 85, 91--94, 142
7.305 \item division
7.306 - \subitem by negative numbers, 135
7.307 - \subitem by zero, 134
7.308 - \subitem for type \protect\isa{nat}, 133
7.309 + \subitem by negative numbers, 143
7.310 + \subitem by zero, 142
7.311 + \subitem for type \protect\isa{nat}, 141
7.312 \item domain
7.313 - \subitem of a relation, 96
7.314 - \item \isa {Domain_iff} (theorem), \bold{96}
7.315 - \item \isacommand {done} (command), 11
7.316 - \item \isa {drule_tac} (method), 60, 80
7.317 - \item \isa {dvd_add} (theorem), \bold{134}
7.318 - \item \isa {dvd_anti_sym} (theorem), \bold{134}
7.319 - \item \isa {dvd_def} (theorem), \bold{134}
7.320 + \subitem of a relation, 102
7.321 + \item \isa {Domain_iff} (theorem), \bold{102}
7.322 + \item \isacommand {done} (command), 13
7.323 + \item \isa {drule_tac} (method), 66, 86
7.324 + \item \isa {dvd_add} (theorem), \bold{142}
7.325 + \item \isa {dvd_anti_sym} (theorem), \bold{142}
7.326 + \item \isa {dvd_def} (theorem), \bold{142}
7.327
7.328 \indexspace
7.329
7.330 - \item \isa {elim!} (attribute), 115
7.331 - \item elimination rules, 53--54
7.332 - \item \isacommand {end} (command), 12
7.333 - \item \isa {Eps} (constant), 93
7.334 - \item equality, 3
7.335 - \subitem of functions, \bold{93}
7.336 - \subitem of records, 143
7.337 - \subitem of sets, \bold{90}
7.338 - \item \isa {equalityE} (theorem), \bold{90}
7.339 - \item \isa {equalityI} (theorem), \bold{90}
7.340 - \item \isa {erule} (method), 54
7.341 - \item \isa {erule_tac} (method), 60
7.342 - \item Euclid's algorithm, 85--88
7.343 + \item \isa {elim!} (attribute), 121
7.344 + \item elimination rules, 59--60
7.345 + \item \isacommand {end} (command), 14
7.346 + \item \isa {Eps} (constant), 99
7.347 + \item equality, 5
7.348 + \subitem of functions, \bold{99}
7.349 + \subitem of records, 151
7.350 + \subitem of sets, \bold{96}
7.351 + \item \isa {equalityE} (theorem), \bold{96}
7.352 + \item \isa {equalityI} (theorem), \bold{96}
7.353 + \item \isa {erule} (method), 60
7.354 + \item \isa {erule_tac} (method), 66
7.355 + \item Euclid's algorithm, 91--94
7.356 \item even numbers
7.357 - \subitem defining inductively, 111--115
7.358 - \item \texttt {EX}, \bold{187}
7.359 - \item \isa {Ex} (constant), 93
7.360 - \item \isa {exE} (theorem), \bold{66}
7.361 - \item \isa {exI} (theorem), \bold{66}
7.362 - \item \isa {ext} (theorem), \bold{93}
7.363 + \subitem defining inductively, 117--121
7.364 + \item \texttt {EX}, \bold{195}
7.365 + \item \isa {Ex} (constant), 99
7.366 + \item \isa {exE} (theorem), \bold{72}
7.367 + \item \isa {exI} (theorem), \bold{72}
7.368 + \item \isa {ext} (theorem), \bold{99}
7.369 \item extensionality
7.370 - \subitem for functions, \bold{93, 94}
7.371 - \subitem for records, 143
7.372 - \subitem for sets, \bold{90}
7.373 - \item \ttEXU, \bold{187}
7.374 + \subitem for functions, \bold{99, 100}
7.375 + \subitem for records, 151
7.376 + \subitem for sets, \bold{96}
7.377 + \item \ttEXU, \bold{195}
7.378
7.379 \indexspace
7.380
7.381 - \item \isa {False} (constant), 3
7.382 - \item \isa {fast} (method), 76, 108
7.383 - \item Fibonacci function, 44
7.384 - \item \isa {finite} (symbol), 93
7.385 - \item \isa {Finites} (constant), 93
7.386 - \item fixed points, 100
7.387 - \item flags, 3, 4, 31
7.388 - \subitem setting and resetting, 3
7.389 - \item \isa {force} (method), 75, 76
7.390 - \item formulae, 3
7.391 - \item forward proof, 76--82
7.392 - \item \isa {frule} (method), 67
7.393 - \item \isa {frule_tac} (method), 60
7.394 - \item \isa {fst} (constant), 22
7.395 - \item function types, 3
7.396 - \item functions, 93--95
7.397 - \subitem partial, 162
7.398 - \subitem total, 9, 44--50
7.399 - \subitem underdefined, 163
7.400 + \item \isa {False} (constant), 5
7.401 + \item \isa {fast} (method), 82, 114
7.402 + \item Fibonacci function, 46
7.403 + \item \isa {finite} (symbol), 99
7.404 + \item \isa {Finites} (constant), 99
7.405 + \item fixed points, 106
7.406 + \item flags, 5, 6, 33
7.407 + \subitem setting and resetting, 5
7.408 + \item \isa {force} (method), 81, 82
7.409 + \item formulae, 5
7.410 + \item forward proof, 82--88
7.411 + \item \isa {frule} (method), 73
7.412 + \item \isa {frule_tac} (method), 66
7.413 + \item \isa {fst} (constant), 24
7.414 + \item function types, 5
7.415 + \item functions, 99--101
7.416 + \subitem partial, 170
7.417 + \subitem total, 11, 46--52
7.418 + \subitem underdefined, 171
7.419
7.420 \indexspace
7.421
7.422 - \item \isa {gcd} (constant), 77--78, 85--88
7.423 - \item generalizing for induction, 113
7.424 - \item generalizing induction formulae, 32
7.425 - \item Girard, Jean-Yves, \fnote{55}
7.426 - \item Gordon, Mike, 1
7.427 + \item \isa {gcd} (constant), 83--84, 91--94
7.428 + \item generalizing for induction, 119
7.429 + \item generalizing induction formulae, 34
7.430 + \item Girard, Jean-Yves, \fnote{61}
7.431 + \item Gordon, Mike, 3
7.432 \item grammars
7.433 - \subitem defining inductively, 124--129
7.434 - \item ground terms example, 119--124
7.435 + \subitem defining inductively, 130--135
7.436 + \item ground terms example, 125--130
7.437
7.438 \indexspace
7.439
7.440 - \item \isa {hd} (constant), 15, 35
7.441 - \item Hilbert's $\varepsilon$-operator, 70
7.442 - \item HOLCF, 41
7.443 - \item Hopcroft, J. E., 129
7.444 - \item \isa {hypreal} (type), 137
7.445 + \item \isa {hd} (constant), 17, 37
7.446 + \item Hilbert's $\varepsilon$-operator, 76
7.447 + \item HOLCF, 43
7.448 + \item Hopcroft, J. E., 135
7.449 + \item \isa {hypreal} (type), 145
7.450
7.451 \indexspace
7.452
7.453 - \item \isa {Id_def} (theorem), \bold{96}
7.454 - \item \isa {id_def} (theorem), \bold{94}
7.455 - \item identifiers, \bold{4}
7.456 - \subitem qualified, \bold{2}
7.457 - \item identity function, \bold{94}
7.458 - \item identity relation, \bold{96}
7.459 - \item \isa {if} expressions, 3, 4
7.460 - \subitem simplification of, 31
7.461 - \subitem splitting of, 29, 47
7.462 - \item if-and-only-if, 3
7.463 - \item \isa {iff} (attribute), 74, 86, 114
7.464 - \item \isa {iffD1} (theorem), \bold{78}
7.465 - \item \isa {iffD2} (theorem), \bold{78}
7.466 + \item \isa {Id_def} (theorem), \bold{102}
7.467 + \item \isa {id_def} (theorem), \bold{100}
7.468 + \item identifiers, \bold{6}
7.469 + \subitem qualified, \bold{4}
7.470 + \item identity function, \bold{100}
7.471 + \item identity relation, \bold{102}
7.472 + \item \isa {if} expressions, 5, 6
7.473 + \subitem simplification of, 33
7.474 + \subitem splitting of, 31, 49
7.475 + \item if-and-only-if, 5
7.476 + \item \isa {iff} (attribute), 80, 92, 120
7.477 + \item \isa {iffD1} (theorem), \bold{84}
7.478 + \item \isa {iffD2} (theorem), \bold{84}
7.479 \item image
7.480 - \subitem under a function, \bold{95}
7.481 - \subitem under a relation, \bold{96}
7.482 - \item \isa {image_def} (theorem), \bold{95}
7.483 - \item \isa {Image_iff} (theorem), \bold{96}
7.484 - \item \isa {impI} (theorem), \bold{56}
7.485 - \item implication, 56--57
7.486 - \item \isa {ind_cases} (method), 115
7.487 - \item \isa {induct_tac} (method), 10, 17, 50, 170
7.488 - \item induction, 166--173
7.489 - \subitem complete, 168
7.490 - \subitem deriving new schemas, 170
7.491 - \subitem on a term, 167
7.492 - \subitem recursion, 49--50
7.493 - \subitem structural, 17
7.494 - \subitem well-founded, 99
7.495 - \item induction heuristics, 31--33
7.496 - \item \isacommand {inductive} (command), 111
7.497 + \subitem under a function, \bold{101}
7.498 + \subitem under a relation, \bold{102}
7.499 + \item \isa {image_def} (theorem), \bold{101}
7.500 + \item \isa {Image_iff} (theorem), \bold{102}
7.501 + \item \isa {impI} (theorem), \bold{62}
7.502 + \item implication, 62--63
7.503 + \item \isa {ind_cases} (method), 121
7.504 + \item \isa {induct_tac} (method), 12, 19, 52, 178
7.505 + \item induction, 174--181
7.506 + \subitem complete, 176
7.507 + \subitem deriving new schemas, 178
7.508 + \subitem on a term, 175
7.509 + \subitem recursion, 51--52
7.510 + \subitem structural, 19
7.511 + \subitem well-founded, 105
7.512 + \item induction heuristics, 33--35
7.513 + \item \isacommand {inductive} (command), 117
7.514 \item inductive definition
7.515 - \subitem simultaneous, 125
7.516 - \item inductive definitions, 111--129
7.517 - \item \isacommand {inductive\_cases} (command), 115, 123
7.518 - \item infinitely branching trees, 40
7.519 - \item \isacommand{infixr} (annotation), 8
7.520 - \item \isa {inj_on_def} (theorem), \bold{94}
7.521 - \item injections, 94
7.522 - \item \isa {insert} (constant), 91
7.523 - \item \isa {insert} (method), 81--82
7.524 - \item instance, \bold{145}
7.525 - \item \texttt {INT}, \bold{187}
7.526 - \item \texttt {Int}, \bold{187}
7.527 - \item \isa {int} (type), 135
7.528 - \item \isa {INT_iff} (theorem), \bold{92}
7.529 - \item \isa {IntD1} (theorem), \bold{89}
7.530 - \item \isa {IntD2} (theorem), \bold{89}
7.531 - \item integers, 135
7.532 - \item \isa {INTER} (constant), 93
7.533 - \item \texttt {Inter}, \bold{187}
7.534 - \item \isa {Inter_iff} (theorem), \bold{92}
7.535 - \item intersection, 89
7.536 - \subitem indexed, 92
7.537 - \item \isa {IntI} (theorem), \bold{89}
7.538 - \item \isa {intro} (method), 58
7.539 - \item \isa {intro!} (attribute), 112
7.540 - \item \isa {intro_classes} (method), 145
7.541 - \item introduction rules, 52--53
7.542 - \item \isa {inv} (constant), 70
7.543 - \item \isa {inv_image_def} (theorem), \bold{99}
7.544 + \subitem simultaneous, 131
7.545 + \item inductive definitions, 117--135
7.546 + \item \isacommand {inductive\_cases} (command), 121, 129
7.547 + \item infinitely branching trees, 42
7.548 + \item \isacommand{infixr} (annotation), 10
7.549 + \item \isa {inj_on_def} (theorem), \bold{100}
7.550 + \item injections, 100
7.551 + \item \isa {insert} (constant), 97
7.552 + \item \isa {insert} (method), 87--88
7.553 + \item instance, \bold{153}
7.554 + \item \texttt {INT}, \bold{195}
7.555 + \item \texttt {Int}, \bold{195}
7.556 + \item \isa {int} (type), 143
7.557 + \item \isa {INT_iff} (theorem), \bold{98}
7.558 + \item \isa {IntD1} (theorem), \bold{95}
7.559 + \item \isa {IntD2} (theorem), \bold{95}
7.560 + \item integers, 143
7.561 + \item \isa {INTER} (constant), 99
7.562 + \item \texttt {Inter}, \bold{195}
7.563 + \item \isa {Inter_iff} (theorem), \bold{98}
7.564 + \item intersection, 95
7.565 + \subitem indexed, 98
7.566 + \item \isa {IntI} (theorem), \bold{95}
7.567 + \item \isa {intro} (method), 64
7.568 + \item \isa {intro!} (attribute), 118
7.569 + \item \isa {intro_classes} (method), 153
7.570 + \item introduction rules, 58--59
7.571 + \item \isa {inv} (constant), 76
7.572 + \item \isa {inv_image_def} (theorem), \bold{105}
7.573 \item inverse
7.574 - \subitem of a function, \bold{94}
7.575 - \subitem of a relation, \bold{96}
7.576 + \subitem of a function, \bold{100}
7.577 + \subitem of a relation, \bold{102}
7.578 \item inverse image
7.579 - \subitem of a function, 95
7.580 - \subitem of a relation, 98
7.581 - \item \isa {itrev} (constant), 32
7.582 + \subitem of a function, 101
7.583 + \subitem of a relation, 104
7.584 + \item \isa {itrev} (constant), 34
7.585
7.586 \indexspace
7.587
7.588 - \item \isacommand {kill} (command), 14
7.589 + \item \isacommand {kill} (command), 16
7.590
7.591 \indexspace
7.592
7.593 - \item $\lambda$ expressions, 3
7.594 - \item LCF, 41
7.595 - \item \isa {LEAST} (symbol), 21, 69
7.596 - \item least number operator, \see{\protect\isa{LEAST}}{69}
7.597 - \item \isacommand {lemma} (command), 11
7.598 - \item \isacommand {lemmas} (command), 77, 86
7.599 - \item \isa {length} (symbol), 16
7.600 - \item \isa {length_induct}, \bold{170}
7.601 - \item \isa {less_than} (constant), 98
7.602 - \item \isa {less_than_iff} (theorem), \bold{98}
7.603 - \item \isa {let} expressions, 3, 4, 29
7.604 - \item \isa {Let_def} (theorem), 29
7.605 - \item \isa {lex_prod_def} (theorem), \bold{99}
7.606 - \item lexicographic product, \bold{99}, 158
7.607 + \item $\lambda$ expressions, 5
7.608 + \item LCF, 43
7.609 + \item \isa {LEAST} (symbol), 23, 75
7.610 + \item least number operator, \see{\protect\isa{LEAST}}{75}
7.611 + \item \isacommand {lemma} (command), 13
7.612 + \item \isacommand {lemmas} (command), 83, 92
7.613 + \item \isa {length} (symbol), 18
7.614 + \item \isa {length_induct}, \bold{178}
7.615 + \item \isa {less_than} (constant), 104
7.616 + \item \isa {less_than_iff} (theorem), \bold{104}
7.617 + \item \isa {let} expressions, 5, 6, 31
7.618 + \item \isa {Let_def} (theorem), 31
7.619 + \item \isa {lex_prod_def} (theorem), \bold{105}
7.620 + \item lexicographic product, \bold{105}, 166
7.621 \item {\texttt{lfp}}
7.622 - \subitem applications of, \see{CTL}{100}
7.623 - \item linear arithmetic, 20--22, 131
7.624 - \item \isa {List} (theory), 15
7.625 - \item \isa {list} (type), 2, 7, 15
7.626 - \item \isa {list.split} (theorem), 30
7.627 - \item \isa {lists_mono} (theorem), \bold{121}
7.628 - \item Lowe, Gavin, 176--177
7.629 + \subitem applications of, \see{CTL}{106}
7.630 + \item linear arithmetic, 22--24, 139
7.631 + \item \isa {List} (theory), 17
7.632 + \item \isa {list} (type), 4, 9, 17
7.633 + \item \isa {list.split} (theorem), 32
7.634 + \item \isa {lists_mono} (theorem), \bold{127}
7.635 + \item Lowe, Gavin, 184--185
7.636
7.637 \indexspace
7.638
7.639 - \item \isa {Main} (theory), 2
7.640 - \item major premise, \bold{59}
7.641 - \item \isa {max} (constant), 21, 22
7.642 - \item measure functions, 45, 98
7.643 - \item \isa {measure_def} (theorem), \bold{99}
7.644 - \item meta-logic, \bold{64}
7.645 - \item methods, \bold{14}
7.646 - \item \isa {min} (constant), 21, 22
7.647 - \item \isa {mod} (symbol), 21
7.648 - \item \isa {mod_div_equality} (theorem), \bold{133}
7.649 - \item \isa {mod_mult_distrib} (theorem), \bold{133}
7.650 - \item model checking example, 100--110
7.651 - \item \emph{modus ponens}, 51, 56
7.652 - \item \isa {mono_def} (theorem), \bold{100}
7.653 - \item monotone functions, \bold{100}, 123
7.654 - \subitem and inductive definitions, 121--122
7.655 - \item \isa {more} (constant), 140, 141
7.656 - \item \isa {mp} (theorem), \bold{56}
7.657 - \item \isa {mult_ac} (theorems), 134
7.658 - \item multiple inheritance, \bold{149}
7.659 - \item multiset ordering, \bold{99}
7.660 + \item \isa {Main} (theory), 4
7.661 + \item major premise, \bold{65}
7.662 + \item \isa {max} (constant), 23, 24
7.663 + \item measure functions, 47, 104
7.664 + \item \isa {measure_def} (theorem), \bold{105}
7.665 + \item meta-logic, \bold{70}
7.666 + \item methods, \bold{16}
7.667 + \item \isa {min} (constant), 23, 24
7.668 + \item \isa {mod} (symbol), 23
7.669 + \item \isa {mod_div_equality} (theorem), \bold{141}
7.670 + \item \isa {mod_mult_distrib} (theorem), \bold{141}
7.671 + \item model checking example, 106--116
7.672 + \item \emph{modus ponens}, 57, 62
7.673 + \item \isa {mono_def} (theorem), \bold{106}
7.674 + \item monotone functions, \bold{106}, 129
7.675 + \subitem and inductive definitions, 127--128
7.676 + \item \isa {more} (constant), 148, 149
7.677 + \item \isa {mp} (theorem), \bold{62}
7.678 + \item \isa {mult_ac} (theorems), 142
7.679 + \item multiple inheritance, \bold{157}
7.680 + \item multiset ordering, \bold{105}
7.681
7.682 \indexspace
7.683
7.684 - \item \isa {nat} (type), 2, 20, 133--134
7.685 - \item \isa {nat_less_induct} (theorem), 168
7.686 - \item natural deduction, 51--52
7.687 - \item natural numbers, 20, 133--134
7.688 - \item Needham-Schroeder protocol, 175--177
7.689 - \item negation, 57--59
7.690 - \item \isa {Nil} (constant), 7
7.691 - \item \isa {no_asm} (modifier), 27
7.692 - \item \isa {no_asm_simp} (modifier), 27
7.693 - \item \isa {no_asm_use} (modifier), 27
7.694 - \item non-standard reals, 137
7.695 - \item \isa {None} (constant), \bold{22}
7.696 - \item \isa {notE} (theorem), \bold{57}
7.697 - \item \isa {notI} (theorem), \bold{57}
7.698 - \item numbers, 131--137
7.699 - \item numeric literals, 132
7.700 - \subitem for type \protect\isa{nat}, 133
7.701 - \subitem for type \protect\isa{real}, 136
7.702 + \item \isa {nat} (type), 4, 22, 141--142
7.703 + \item \isa {nat_less_induct} (theorem), 176
7.704 + \item natural deduction, 57--58
7.705 + \item natural numbers, 22, 141--142
7.706 + \item Needham-Schroeder protocol, 183--185
7.707 + \item negation, 63--65
7.708 + \item \isa {Nil} (constant), 9
7.709 + \item \isa {no_asm} (modifier), 29
7.710 + \item \isa {no_asm_simp} (modifier), 29
7.711 + \item \isa {no_asm_use} (modifier), 29
7.712 + \item non-standard reals, 145
7.713 + \item \isa {None} (constant), \bold{24}
7.714 + \item \isa {notE} (theorem), \bold{63}
7.715 + \item \isa {notI} (theorem), \bold{63}
7.716 + \item numbers, 139--145
7.717 + \item numeric literals, 140
7.718 + \subitem for type \protect\isa{nat}, 141
7.719 + \subitem for type \protect\isa{real}, 144
7.720
7.721 \indexspace
7.722
7.723 - \item \isa {O} (symbol), 96
7.724 - \item \texttt {o}, \bold{187}
7.725 - \item \isa {o_def} (theorem), \bold{94}
7.726 - \item \isa {OF} (attribute), 79--80
7.727 - \item \isa {of} (attribute), 77, 80
7.728 - \item \isa {only} (modifier), 27
7.729 - \item \isacommand {oops} (command), 11
7.730 - \item \isa {option} (type), \bold{22}
7.731 - \item ordered rewriting, \bold{156}
7.732 - \item overloading, 21, 144--146
7.733 - \subitem and arithmetic, 132
7.734 + \item \isa {O} (symbol), 102
7.735 + \item \texttt {o}, \bold{195}
7.736 + \item \isa {o_def} (theorem), \bold{100}
7.737 + \item \isa {OF} (attribute), 85--86
7.738 + \item \isa {of} (attribute), 83, 86
7.739 + \item \isa {only} (modifier), 29
7.740 + \item \isacommand {oops} (command), 13
7.741 + \item \isa {option} (type), \bold{24}
7.742 + \item ordered rewriting, \bold{164}
7.743 + \item overloading, 23, 152--154
7.744 + \subitem and arithmetic, 140
7.745
7.746 \indexspace
7.747
7.748 - \item pairs and tuples, 22, 137--140
7.749 - \item parent theories, \bold{2}
7.750 + \item pairs and tuples, 24, 145--148
7.751 + \item parent theories, \bold{4}
7.752 \item pattern matching
7.753 - \subitem and \isacommand{recdef}, 45
7.754 + \subitem and \isacommand{recdef}, 47
7.755 \item patterns
7.756 - \subitem higher-order, \bold{157}
7.757 - \item PDL, 102--104
7.758 - \item \isacommand {pr} (command), 14, 84
7.759 - \item \isacommand {prefer} (command), 14, 84
7.760 + \subitem higher-order, \bold{165}
7.761 + \item PDL, 108--110
7.762 + \item \isacommand {pr} (command), 16, 90
7.763 + \item \isacommand {prefer} (command), 16, 90
7.764 \item primitive recursion, \see{recursion, primitive}{1}
7.765 - \item \isacommand {primrec} (command), 8, 16, 36--41
7.766 + \item \isacommand {primrec} (command), 10, 18, 38--43
7.767 \item product type, \see{pairs and tuples}{1}
7.768 - \item Proof General, \bold{5}
7.769 - \item proof state, 10
7.770 + \item Proof General, \bold{7}
7.771 + \item proof state, 12
7.772 \item proofs
7.773 - \subitem abandoning, \bold{11}
7.774 - \subitem examples of failing, 71--73
7.775 + \subitem abandoning, \bold{13}
7.776 + \subitem examples of failing, 77--79
7.777 \item protocols
7.778 - \subitem security, 175--185
7.779 + \subitem security, 183--193
7.780
7.781 \indexspace
7.782
7.783 - \item quantifiers, 3
7.784 - \subitem and inductive definitions, 119--121
7.785 - \subitem existential, 66
7.786 - \subitem for sets, 92
7.787 - \subitem instantiating, 68
7.788 - \subitem universal, 63--66
7.789 + \item quantifiers, 5
7.790 + \subitem and inductive definitions, 125--127
7.791 + \subitem existential, 72
7.792 + \subitem for sets, 98
7.793 + \subitem instantiating, 74
7.794 + \subitem universal, 69--72
7.795
7.796 \indexspace
7.797
7.798 - \item \isa {r_into_rtrancl} (theorem), \bold{96}
7.799 - \item \isa {r_into_trancl} (theorem), \bold{97}
7.800 + \item \isa {r_into_rtrancl} (theorem), \bold{102}
7.801 + \item \isa {r_into_trancl} (theorem), \bold{103}
7.802 \item range
7.803 - \subitem of a function, 95
7.804 - \subitem of a relation, 96
7.805 - \item \isa {range} (symbol), 95
7.806 - \item \isa {Range_iff} (theorem), \bold{96}
7.807 - \item \isa {Real} (theory), 137
7.808 - \item \isa {real} (type), 136--137
7.809 - \item real numbers, 136--137
7.810 - \item \isacommand {recdef} (command), 44--50, 98, 158--166
7.811 - \subitem and numeric literals, 132
7.812 - \item \isa {recdef_cong} (attribute), 162
7.813 - \item \isa {recdef_simp} (attribute), 46
7.814 - \item \isa {recdef_wf} (attribute), 160
7.815 - \item \isacommand {record} (command), 140
7.816 - \item \isa {record_split} (method), 143
7.817 - \item records, 140--144
7.818 - \subitem extensible, 141--142
7.819 + \subitem of a function, 101
7.820 + \subitem of a relation, 102
7.821 + \item \isa {range} (symbol), 101
7.822 + \item \isa {Range_iff} (theorem), \bold{102}
7.823 + \item \isa {Real} (theory), 145
7.824 + \item \isa {real} (type), 144--145
7.825 + \item real numbers, 144--145
7.826 + \item \isacommand {recdef} (command), 46--52, 104, 166--174
7.827 + \subitem and numeric literals, 140
7.828 + \item \isa {recdef_cong} (attribute), 170
7.829 + \item \isa {recdef_simp} (attribute), 48
7.830 + \item \isa {recdef_wf} (attribute), 168
7.831 + \item \isacommand {record} (command), 148
7.832 + \item \isa {record_split} (method), 151
7.833 + \item records, 148--152
7.834 + \subitem extensible, 149--150
7.835 \item recursion
7.836 - \subitem guarded, 163
7.837 - \subitem primitive, 16
7.838 - \subitem well-founded, \bold{159}
7.839 - \item recursion induction, 49--50
7.840 - \item \isacommand {redo} (command), 14
7.841 - \item reflexive and transitive closure, 96--98
7.842 + \subitem guarded, 171
7.843 + \subitem primitive, 18
7.844 + \subitem well-founded, \bold{167}
7.845 + \item recursion induction, 51--52
7.846 + \item \isacommand {redo} (command), 16
7.847 + \item reflexive and transitive closure, 102--104
7.848 \item reflexive transitive closure
7.849 - \subitem defining inductively, 116--119
7.850 - \item relations, 95--98
7.851 - \subitem well-founded, 98--99
7.852 - \item \isa {rename_tac} (method), 66--67
7.853 - \item \isa {rev} (constant), 8--12, 32
7.854 - \item rewrite rules, \bold{25}
7.855 - \subitem permutative, \bold{156}
7.856 - \item rewriting, \bold{25}
7.857 - \item \isa {rotate_tac} (method), 28
7.858 - \item \isa {rtrancl_refl} (theorem), \bold{96}
7.859 - \item \isa {rtrancl_trans} (theorem), \bold{96}
7.860 - \item rule induction, 112--114
7.861 - \item rule inversion, 114--115, 123--124
7.862 - \item \isa {rule_format} (attribute), 167
7.863 - \item \isa {rule_tac} (method), 60
7.864 - \subitem and renaming, 67
7.865 + \subitem defining inductively, 122--125
7.866 + \item relations, 101--104
7.867 + \subitem well-founded, 104--105
7.868 + \item \isa {rename_tac} (method), 72--73
7.869 + \item \isa {rev} (constant), 10--14, 34
7.870 + \item rewrite rules, \bold{27}
7.871 + \subitem permutative, \bold{164}
7.872 + \item rewriting, \bold{27}
7.873 + \item \isa {rotate_tac} (method), 30
7.874 + \item \isa {rtrancl_refl} (theorem), \bold{102}
7.875 + \item \isa {rtrancl_trans} (theorem), \bold{102}
7.876 + \item rule induction, 118--120
7.877 + \item rule inversion, 120--121, 129--130
7.878 + \item \isa {rule_format} (attribute), 175
7.879 + \item \isa {rule_tac} (method), 66
7.880 + \subitem and renaming, 73
7.881
7.882 \indexspace
7.883
7.884 - \item \isa {safe} (method), 75, 76
7.885 - \item safe rules, \bold{74}
7.886 - \item \isa {set} (type), 2, 89
7.887 - \item set comprehensions, 91--92
7.888 - \item \isa {set_ext} (theorem), \bold{90}
7.889 - \item sets, 89--93
7.890 - \subitem finite, 93
7.891 - \subitem notation for finite, \bold{91}
7.892 + \item \isa {safe} (method), 81, 82
7.893 + \item safe rules, \bold{80}
7.894 + \item \isa {set} (type), 4, 95
7.895 + \item set comprehensions, 97--98
7.896 + \item \isa {set_ext} (theorem), \bold{96}
7.897 + \item sets, 95--99
7.898 + \subitem finite, 99
7.899 + \subitem notation for finite, \bold{97}
7.900 \item settings, \see{flags}{1}
7.901 - \item \isa {show_brackets} (flag), 4
7.902 - \item \isa {show_types} (flag), 3, 14
7.903 - \item \isa {simp} (attribute), 9, 26
7.904 - \item \isa {simp} (method), \bold{26}
7.905 - \item \isa {simp} del (attribute), 26
7.906 - \item \isa {simp_all} (method), 26, 35
7.907 - \item simplification, 25--31, 155--158
7.908 - \subitem of \isa{let}-expressions, 29
7.909 - \subitem with definitions, 28
7.910 - \subitem with/of assumptions, 27
7.911 - \item simplification rule, 157--158
7.912 - \item simplification rules, 26
7.913 - \subitem adding and deleting, 27
7.914 - \item \isa {simplified} (attribute), 77, 80
7.915 - \item \isa {size} (constant), 15
7.916 - \item \isa {snd} (constant), 22
7.917 - \item \isa {SOME} (symbol), 70
7.918 - \item \texttt {SOME}, \bold{187}
7.919 - \item \isa {Some} (constant), \bold{22}
7.920 - \item \isa {some_equality} (theorem), \bold{70}
7.921 - \item \isa {someI} (theorem), \bold{70}
7.922 - \item \isa {someI2} (theorem), \bold{70}
7.923 - \item \isa {someI_ex} (theorem), \bold{71}
7.924 - \item sorts, 150
7.925 - \item \isa {spec} (theorem), \bold{64}
7.926 - \item \isa {split} (attribute), 30
7.927 - \item \isa {split} (constant), 137
7.928 - \item \isa {split} (method), 29, 138
7.929 - \item \isa {split} (modifier), 30
7.930 - \item split rule, \bold{30}
7.931 - \item \isa {split_if} (theorem), 30
7.932 - \item \isa {split_if_asm} (theorem), 30
7.933 - \item \isa {ssubst} (theorem), \bold{61}
7.934 + \item \isa {show_brackets} (flag), 6
7.935 + \item \isa {show_types} (flag), 5, 16
7.936 + \item \isa {simp} (attribute), 11, 28
7.937 + \item \isa {simp} (method), \bold{28}
7.938 + \item \isa {simp} del (attribute), 28
7.939 + \item \isa {simp_all} (method), 28, 37
7.940 + \item simplification, 27--33, 163--166
7.941 + \subitem of \isa{let}-expressions, 31
7.942 + \subitem with definitions, 30
7.943 + \subitem with/of assumptions, 29
7.944 + \item simplification rule, 165--166
7.945 + \item simplification rules, 28
7.946 + \subitem adding and deleting, 29
7.947 + \item \isa {simplified} (attribute), 83, 86
7.948 + \item \isa {size} (constant), 17
7.949 + \item \isa {snd} (constant), 24
7.950 + \item \isa {SOME} (symbol), 76
7.951 + \item \texttt {SOME}, \bold{195}
7.952 + \item \isa {Some} (constant), \bold{24}
7.953 + \item \isa {some_equality} (theorem), \bold{76}
7.954 + \item \isa {someI} (theorem), \bold{76}
7.955 + \item \isa {someI2} (theorem), \bold{76}
7.956 + \item \isa {someI_ex} (theorem), \bold{77}
7.957 + \item sorts, 158
7.958 + \item \isa {spec} (theorem), \bold{70}
7.959 + \item \isa {split} (attribute), 32
7.960 + \item \isa {split} (constant), 145
7.961 + \item \isa {split} (method), 31, 146
7.962 + \item \isa {split} (modifier), 32
7.963 + \item split rule, \bold{32}
7.964 + \item \isa {split_if} (theorem), 32
7.965 + \item \isa {split_if_asm} (theorem), 32
7.966 + \item \isa {ssubst} (theorem), \bold{67}
7.967 \item structural induction, \see{induction, structural}{1}
7.968 - \item subclasses, 144, 148
7.969 - \item subgoal numbering, 44
7.970 - \item \isa {subgoal_tac} (method), 82
7.971 - \item subgoals, 10
7.972 - \item subset relation, \bold{90}
7.973 - \item \isa {subsetD} (theorem), \bold{90}
7.974 - \item \isa {subsetI} (theorem), \bold{90}
7.975 - \item \isa {subst} (method), 61
7.976 - \item substitution, 61--63
7.977 - \item \isa {Suc} (constant), 20
7.978 - \item \isa {surj_def} (theorem), \bold{94}
7.979 - \item surjections, 94
7.980 - \item \isa {sym} (theorem), \bold{78}
7.981 - \item syntax, 4, 9
7.982 - \item syntax translations, 24
7.983 + \item subclasses, 152, 156
7.984 + \item subgoal numbering, 46
7.985 + \item \isa {subgoal_tac} (method), 88
7.986 + \item subgoals, 12
7.987 + \item subset relation, \bold{96}
7.988 + \item \isa {subsetD} (theorem), \bold{96}
7.989 + \item \isa {subsetI} (theorem), \bold{96}
7.990 + \item \isa {subst} (method), 67
7.991 + \item substitution, 67--69
7.992 + \item \isa {Suc} (constant), 22
7.993 + \item \isa {surj_def} (theorem), \bold{100}
7.994 + \item surjections, 100
7.995 + \item \isa {sym} (theorem), \bold{84}
7.996 + \item syntax, 6, 11
7.997 + \item syntax translations, 26
7.998
7.999 \indexspace
7.1000
7.1001 - \item tacticals, 83
7.1002 - \item tactics, 10
7.1003 - \item \isacommand {term} (command), 14
7.1004 - \item term rewriting, \bold{25}
7.1005 + \item tacticals, 89
7.1006 + \item tactics, 12
7.1007 + \item \isacommand {term} (command), 16
7.1008 + \item term rewriting, \bold{27}
7.1009 \item termination, \see{functions, total}{1}
7.1010 - \item terms, 3
7.1011 - \item \isa {THE} (symbol), 69
7.1012 - \item \isa {the_equality} (theorem), \bold{69}
7.1013 - \item \isa {THEN} (attribute), \bold{78}, 80, 86
7.1014 - \item \isacommand {theorem} (command), \bold{9}, 11
7.1015 - \item theories, 2
7.1016 - \subitem abandoning, \bold{14}
7.1017 - \item \isacommand {theory} (command), 14
7.1018 - \item theory files, 2
7.1019 - \item \isacommand {thm} (command), 14
7.1020 - \item \isa {tl} (constant), 15
7.1021 - \item \isa {ToyList} example, 7--13
7.1022 - \item \isa {trace_simp} (flag), 31
7.1023 - \item tracing the simplifier, \bold{31}
7.1024 - \item \isa {trancl_trans} (theorem), \bold{97}
7.1025 - \item transition systems, 101
7.1026 - \item \isacommand {translations} (command), 24
7.1027 - \item tries, 41--44
7.1028 - \item \isa {True} (constant), 3
7.1029 + \item terms, 5
7.1030 + \item \isa {THE} (symbol), 75
7.1031 + \item \isa {the_equality} (theorem), \bold{75}
7.1032 + \item \isa {THEN} (attribute), \bold{84}, 86, 92
7.1033 + \item \isacommand {theorem} (command), \bold{11}, 13
7.1034 + \item theories, 4
7.1035 + \subitem abandoning, \bold{16}
7.1036 + \item \isacommand {theory} (command), 16
7.1037 + \item theory files, 4
7.1038 + \item \isacommand {thm} (command), 16
7.1039 + \item \isa {tl} (constant), 17
7.1040 + \item \isa {ToyList} example, 9--15
7.1041 + \item \isa {trace_simp} (flag), 33
7.1042 + \item tracing the simplifier, \bold{33}
7.1043 + \item \isa {trancl_trans} (theorem), \bold{103}
7.1044 + \item transition systems, 107
7.1045 + \item \isacommand {translations} (command), 26
7.1046 + \item tries, 43--46
7.1047 + \item \isa {True} (constant), 5
7.1048 \item tuples, \see{pairs and tuples}{1}
7.1049 - \item \isacommand {typ} (command), 14
7.1050 - \item type constraints, \bold{4}
7.1051 - \item type constructors, 2
7.1052 - \item type inference, \bold{3}
7.1053 - \item type synonyms, 23
7.1054 - \item type variables, 3
7.1055 - \item \isacommand {typedecl} (command), 101, 150
7.1056 - \item \isacommand {typedef} (command), 151--154
7.1057 - \item types, 2--3
7.1058 - \subitem declaring, 150--151
7.1059 - \subitem defining, 151--154
7.1060 - \item \isacommand {types} (command), 23
7.1061 + \item \isacommand {typ} (command), 16
7.1062 + \item type constraints, \bold{6}
7.1063 + \item type constructors, 4
7.1064 + \item type inference, \bold{5}
7.1065 + \item type synonyms, 25
7.1066 + \item type variables, 5
7.1067 + \item \isacommand {typedecl} (command), 107, 158
7.1068 + \item \isacommand {typedef} (command), 159--162
7.1069 + \item types, 4--5
7.1070 + \subitem declaring, 158--159
7.1071 + \subitem defining, 159--162
7.1072 + \item \isacommand {types} (command), 25
7.1073
7.1074 \indexspace
7.1075
7.1076 - \item Ullman, J. D., 129
7.1077 - \item \texttt {UN}, \bold{187}
7.1078 - \item \texttt {Un}, \bold{187}
7.1079 - \item \isa {UN_E} (theorem), \bold{92}
7.1080 - \item \isa {UN_I} (theorem), \bold{92}
7.1081 - \item \isa {UN_iff} (theorem), \bold{92}
7.1082 - \item \isa {Un_subset_iff} (theorem), \bold{90}
7.1083 - \item \isacommand {undo} (command), 14
7.1084 - \item unification, 60--63
7.1085 - \item \isa {UNION} (constant), 93
7.1086 - \item \texttt {Union}, \bold{187}
7.1087 + \item Ullman, J. D., 135
7.1088 + \item \texttt {UN}, \bold{195}
7.1089 + \item \texttt {Un}, \bold{195}
7.1090 + \item \isa {UN_E} (theorem), \bold{98}
7.1091 + \item \isa {UN_I} (theorem), \bold{98}
7.1092 + \item \isa {UN_iff} (theorem), \bold{98}
7.1093 + \item \isa {Un_subset_iff} (theorem), \bold{96}
7.1094 + \item \isacommand {undo} (command), 16
7.1095 + \item unification, 66--69
7.1096 + \item \isa {UNION} (constant), 99
7.1097 + \item \texttt {Union}, \bold{195}
7.1098 \item union
7.1099 - \subitem indexed, 92
7.1100 - \item \isa {Union_iff} (theorem), \bold{92}
7.1101 - \item \isa {unit} (type), 22
7.1102 - \item unknowns, 4, \bold{52}
7.1103 - \item unsafe rules, \bold{74}
7.1104 - \item updating a function, \bold{93}
7.1105 + \subitem indexed, 98
7.1106 + \item \isa {Union_iff} (theorem), \bold{98}
7.1107 + \item \isa {unit} (type), 24
7.1108 + \item unknowns, 6, \bold{58}
7.1109 + \item unsafe rules, \bold{80}
7.1110 + \item updating a function, \bold{99}
7.1111
7.1112 \indexspace
7.1113
7.1114 - \item variables, 4--5
7.1115 - \subitem schematic, 4
7.1116 - \subitem type, 3
7.1117 - \item \isa {vimage_def} (theorem), \bold{95}
7.1118 + \item variables, 6--7
7.1119 + \subitem schematic, 6
7.1120 + \subitem type, 5
7.1121 + \item \isa {vimage_def} (theorem), \bold{101}
7.1122
7.1123 \indexspace
7.1124
7.1125 \item Wenzel, Markus, vii
7.1126 - \item \isa {wf_induct} (theorem), \bold{99}
7.1127 - \item \isa {wf_inv_image} (theorem), \bold{99}
7.1128 - \item \isa {wf_less_than} (theorem), \bold{98}
7.1129 - \item \isa {wf_lex_prod} (theorem), \bold{99}
7.1130 - \item \isa {wf_measure} (theorem), \bold{99}
7.1131 - \item \isa {wf_subset} (theorem), 160
7.1132 - \item \isa {while} (constant), 165
7.1133 - \item \isa {While_Combinator} (theory), 165
7.1134 - \item \isa {while_rule} (theorem), 165
7.1135 + \item \isa {wf_induct} (theorem), \bold{105}
7.1136 + \item \isa {wf_inv_image} (theorem), \bold{105}
7.1137 + \item \isa {wf_less_than} (theorem), \bold{104}
7.1138 + \item \isa {wf_lex_prod} (theorem), \bold{105}
7.1139 + \item \isa {wf_measure} (theorem), \bold{105}
7.1140 + \item \isa {wf_subset} (theorem), 168
7.1141 + \item \isa {while} (constant), 173
7.1142 + \item \isa {While_Combinator} (theory), 173
7.1143 + \item \isa {while_rule} (theorem), 173
7.1144
7.1145 \indexspace
7.1146
7.1147 - \item \isa {zadd_ac} (theorems), 135
7.1148 - \item \isa {zmult_ac} (theorems), 135
7.1149 + \item \isa {zadd_ac} (theorems), 143
7.1150 + \item \isa {zmult_ac} (theorems), 143
7.1151
7.1152 \end{theindex}
8.1 --- a/doc-src/TutorialI/tutorial.tex Mon Oct 01 14:42:47 2001 +0200
8.2 +++ b/doc-src/TutorialI/tutorial.tex Mon Oct 01 14:44:00 2001 +0200
8.3 @@ -54,15 +54,21 @@
8.4
8.5 \cleardoublepage\pagenumbering{arabic}
8.6
8.7 -\input{basics}
8.8 +\part{Basic Techniques} %FIXME rename part to "Basic Concepts" (??)
8.9 +\input{basics} %FIXME mmw: rename section, move it before part I (??)
8.10 \input{fp}
8.11 +\input{Documents/documents}
8.12 +
8.13 +\part{Logic and Sets}
8.14 \input{Rules/rules}
8.15 \input{Sets/sets}\input{CTL/ctl} %these constitute ONE chapter
8.16 \input{Inductive/inductive}
8.17 +
8.18 +\part{Advanced Material}
8.19 \input{Types/types}
8.20 \input{Advanced/advanced}
8.21 -%\chapter{Theory Presentation} Document preparation / Syntax Matters!
8.22 \input{Protocol/protocol}
8.23 +
8.24 %\chapter{Structured Proofs}
8.25 %\label{ch:Isar}
8.26 %\chapter{Case Study: UNIX File-System Security}