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

doc-src/TutorialI/Advanced/advanced.tex

author | nipkow |

Thu Sep 14 17:46:00 2000 +0200 (2000-09-14) | |

changeset 9958 | 67f2920862c7 |

child 9993 | c0f7fb6e538e |

permissions | -rw-r--r-- |

*** empty log message ***

1 \chapter{Advanced Simplification, Recursion, and Induction}

2 \markboth{}{CHAPTER 4: ADVANCED}

4 Although we have already learned a lot about simplification, recursion and

5 induction, there are some advanced proof techniques that we have not covered

6 yet and which are worth knowing about if you intend to beome a serious

7 (human) theorem prover. The three sections of this chapter are almost

8 independent of each other and can be read in any order. Only the notion of

9 \emph{congruence rules}, introduced in the section on simplification, is

10 required for parts of the section on recursion.

12 \input{document/simp.tex}

14 \section{Advanced forms of recursion}

15 \label{sec:advanced-recdef}

16 \index{*recdef|(}

17 \input{../Recdef/document/Nested0.tex}

18 \input{../Recdef/document/Nested1.tex}

19 \input{../Recdef/document/Nested2.tex}

20 \index{*recdef|)}

22 \section{Advanced induction techniques}

23 \label{sec:advanced-ind}

24 \index{induction|(}

25 \input{../Misc/document/AdvancedInd.tex}

26 \index{induction|)}