1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Mutual}% |
3 \def\isabellecontext{Mutual}% |
|
4 \isamarkupfalse% |
4 % |
5 % |
5 \isamarkupsubsection{Mutually Inductive Definitions% |
6 \isamarkupsubsection{Mutually Inductive Definitions% |
6 } |
7 } |
|
8 \isamarkuptrue% |
7 % |
9 % |
8 \begin{isamarkuptext}% |
10 \begin{isamarkuptext}% |
9 Just as there are datatypes defined by mutual recursion, there are sets defined |
11 Just as there are datatypes defined by mutual recursion, there are sets defined |
10 by mutual induction. As a trivial example we consider the even and odd |
12 by mutual induction. As a trivial example we consider the even and odd |
11 natural numbers:% |
13 natural numbers:% |
12 \end{isamarkuptext}% |
14 \end{isamarkuptext}% |
|
15 \isamarkuptrue% |
13 \isacommand{consts}\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline |
16 \isacommand{consts}\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline |
14 \ \ \ \ \ \ \ odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline |
17 \ \ \ \ \ \ \ odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline |
15 \isanewline |
18 \isanewline |
|
19 \isamarkupfalse% |
16 \isacommand{inductive}\ even\ odd\isanewline |
20 \isacommand{inductive}\ even\ odd\isanewline |
17 \isakeyword{intros}\isanewline |
21 \isakeyword{intros}\isanewline |
18 zero{\isacharcolon}\ \ {\isachardoublequote}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequote}\isanewline |
22 zero{\isacharcolon}\ \ {\isachardoublequote}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequote}\isanewline |
19 evenI{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline |
23 evenI{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline |
20 oddI{\isacharcolon}\ \ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ odd{\isachardoublequote}% |
24 oddI{\isacharcolon}\ \ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ odd{\isachardoublequote}\isamarkupfalse% |
|
25 % |
21 \begin{isamarkuptext}% |
26 \begin{isamarkuptext}% |
22 \noindent |
27 \noindent |
23 The mutually inductive definition of multiple sets is no different from |
28 The mutually inductive definition of multiple sets is no different from |
24 that of a single set, except for induction: just as for mutually recursive |
29 that of a single set, except for induction: just as for mutually recursive |
25 datatypes, induction needs to involve all the simultaneously defined sets. In |
30 datatypes, induction needs to involve all the simultaneously defined sets. In |
30 \end{isabelle} |
35 \end{isabelle} |
31 |
36 |
32 If we want to prove that all even numbers are divisible by two, we have to |
37 If we want to prove that all even numbers are divisible by two, we have to |
33 generalize the statement as follows:% |
38 generalize the statement as follows:% |
34 \end{isamarkuptext}% |
39 \end{isamarkuptext}% |
35 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}m\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ m{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
40 \isamarkuptrue% |
|
41 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}m\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ m{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
42 % |
36 \begin{isamarkuptxt}% |
43 \begin{isamarkuptxt}% |
37 \noindent |
44 \noindent |
38 The proof is by rule induction. Because of the form of the induction theorem, |
45 The proof is by rule induction. Because of the form of the induction theorem, |
39 it is applied by \isa{rule} rather than \isa{erule} as for ordinary |
46 it is applied by \isa{rule} rather than \isa{erule} as for ordinary |
40 inductive definitions:% |
47 inductive definitions:% |
41 \end{isamarkuptxt}% |
48 \end{isamarkuptxt}% |
42 \isacommand{apply}{\isacharparenleft}rule\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}% |
49 \isamarkuptrue% |
|
50 \isacommand{apply}{\isacharparenleft}rule\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}\isamarkupfalse% |
|
51 % |
43 \begin{isamarkuptxt}% |
52 \begin{isamarkuptxt}% |
44 \begin{isabelle}% |
53 \begin{isabelle}% |
45 \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline |
54 \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline |
46 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ odd{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ Suc\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ n\isanewline |
55 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ odd{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ Suc\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ n\isanewline |
47 \ {\isadigit{3}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% |
56 \ {\isadigit{3}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% |
49 The first two subgoals are proved by simplification and the final one can be |
58 The first two subgoals are proved by simplification and the final one can be |
50 proved in the same manner as in \S\ref{sec:rule-induction} |
59 proved in the same manner as in \S\ref{sec:rule-induction} |
51 where the same subgoal was encountered before. |
60 where the same subgoal was encountered before. |
52 We do not show the proof script.% |
61 We do not show the proof script.% |
53 \end{isamarkuptxt}% |
62 \end{isamarkuptxt}% |
|
63 \isamarkuptrue% |
|
64 \isamarkupfalse% |
|
65 \isamarkupfalse% |
|
66 \isamarkupfalse% |
|
67 \isamarkupfalse% |
|
68 \isamarkupfalse% |
|
69 \isamarkupfalse% |
|
70 \isamarkupfalse% |
|
71 \isamarkupfalse% |
54 \end{isabellebody}% |
72 \end{isabellebody}% |
55 %%% Local Variables: |
73 %%% Local Variables: |
56 %%% mode: latex |
74 %%% mode: latex |
57 %%% TeX-master: "root" |
75 %%% TeX-master: "root" |
58 %%% End: |
76 %%% End: |