author | wenzelm |
Tue, 28 Aug 2012 18:57:32 +0200 | |
changeset 48985 | 5386df44a037 |
parent 48966 | doc-src/TutorialI/document/advanced0.tex@6e15de7dd871 |
permissions | -rw-r--r-- |
25281
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
1 |
\chapter{Advanced Simplification and Induction} |
9958 | 2 |
|
25281
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
3 |
Although we have already learned a lot about simplification and |
9958 | 4 |
induction, there are some advanced proof techniques that we have not covered |
25281
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
5 |
yet and which are worth learning. The sections of this chapter are |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
6 |
independent of each other and can be read in any order. |
9958 | 7 |
|
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
8 |
\input{simp2.tex} |
9958 | 9 |
|
11216 | 10 |
\section{Advanced Induction Techniques} |
9958 | 11 |
\label{sec:advanced-ind} |
12 |
\index{induction|(} |
|
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
13 |
\input{AdvancedInd.tex} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
14 |
\input{CTLind.tex} |
9958 | 15 |
\index{induction|)} |
25281
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
16 |
|
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
17 |
%\section{Advanced Forms of Recursion} |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
18 |
%\index{recdef@\isacommand {recdef} (command)|(} |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
19 |
|
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
20 |
%This section introduces advanced forms of |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
21 |
%\isacommand{recdef}: how to establish termination by means other than measure |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
22 |
%functions, how to define recursive functions over nested recursive datatypes |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
23 |
%and how to deal with partial functions. |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
24 |
% |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
25 |
%If, after reading this section, you feel that the definition of recursive |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
26 |
%functions is overly complicated by the requirement of |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
27 |
%totality, you should ponder the alternatives. In a logic of partial functions, |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
28 |
%recursive definitions are always accepted. But there are many |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
29 |
%such logics, and no clear winner has emerged. And in all of these logics you |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
30 |
%are (more or less frequently) required to reason about the definedness of |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
31 |
%terms explicitly. Thus one shifts definedness arguments from definition time to |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
32 |
%proof time. In HOL you may have to work hard to define a function, but proofs |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
33 |
%can then proceed unencumbered by worries about undefinedness. |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
34 |
|
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
35 |
%\subsection{Beyond Measure} |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
36 |
%\label{sec:beyond-measure} |
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
37 |
%\input{WFrec.tex} |
25281
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
38 |
% |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
39 |
%\subsection{Recursion Over Nested Datatypes} |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
40 |
%\label{sec:nested-recdef} |
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
41 |
%\input{Nested0.tex} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
42 |
%\input{Nested1.tex} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
43 |
%\input{Nested2.tex} |
25281
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
44 |
% |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
45 |
%\subsection{Partial Functions} |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
46 |
%\index{functions!partial} |
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48522
diff
changeset
|
47 |
%\input{Partial.tex} |
25281
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
48 |
% |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
11494
diff
changeset
|
49 |
%\index{recdef@\isacommand {recdef} (command)|)} |