summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/TutorialI/Advanced/advanced.tex

changeset 10885 | 90695f46440b |

parent 10654 | 458068404143 |

child 11196 | bb4ede27fcb7 |

1.1 --- a/doc-src/TutorialI/Advanced/advanced.tex Fri Jan 12 16:28:14 2001 +0100 1.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex Fri Jan 12 16:32:01 2001 +0100 1.3 @@ -2,8 +2,7 @@ 1.4 1.5 Although we have already learned a lot about simplification, recursion and 1.6 induction, there are some advanced proof techniques that we have not covered 1.7 -yet and which are worth knowing about if you intend to beome a serious 1.8 -(human) theorem prover. The three sections of this chapter are almost 1.9 +yet and which are worth learning. The three sections of this chapter are almost 1.10 independent of each other and can be read in any order. Only the notion of 1.11 \emph{congruence rules}, introduced in the section on simplification, is 1.12 required for parts of the section on recursion. 1.13 @@ -19,12 +18,12 @@ 1.14 and how to deal with partial functions. 1.15 1.16 If, after reading this section, you feel that the definition of recursive 1.17 -functions is overly and maybe unnecessarily complicated by the requirement of 1.18 +functions is overly complicated by the requirement of 1.19 totality, you should ponder the alternative, a logic of partial functions, 1.20 where recursive definitions are always wellformed. For a start, there are many 1.21 such logics, and no clear winner has emerged. And in all of these logics you 1.22 are (more or less frequently) required to reason about the definedness of 1.23 -terms explicitly. Thus one shifts definedness arguments from definition to 1.24 +terms explicitly. Thus one shifts definedness arguments from definition time to 1.25 proof time. In HOL you may have to work hard to define a function, but proofs 1.26 can then proceed unencumbered by worries about undefinedness. 1.27