29 |
29 |
30 \index{sets|(}% |
30 \index{sets|(}% |
31 HOL's set theory should not be confused with traditional, untyped set |
31 HOL's set theory should not be confused with traditional, untyped set |
32 theory, in which everything is a set. Our sets are typed. In a given set, |
32 theory, in which everything is a set. Our sets are typed. In a given set, |
33 all elements have the same type, say~$\tau$, and the set itself has type |
33 all elements have the same type, say~$\tau$, and the set itself has type |
34 \isa{$\tau$~set}. |
34 $\tau$~\tydx{set}. |
35 |
35 |
36 We begin with \bfindex{intersection}, \bfindex{union} and |
36 We begin with \textbf{intersection}, \textbf{union} and |
37 \bfindex{complement}. In addition to the |
37 \textbf{complement}. In addition to the |
38 \bfindex{membership relation}, there is a symbol for its negation. These |
38 \textbf{membership relation}, there is a symbol for its negation. These |
39 points can be seen below. |
39 points can be seen below. |
40 |
40 |
41 Here are the natural deduction rules for intersection. Note the |
41 Here are the natural deduction rules for \rmindex{intersection}. Note |
42 resemblance to those for conjunction. |
42 the resemblance to those for conjunction. |
43 \begin{isabelle} |
43 \begin{isabelle} |
44 \isasymlbrakk c\ \isasymin\ A;\ c\ \isasymin\ B\isasymrbrakk\ |
44 \isasymlbrakk c\ \isasymin\ A;\ c\ \isasymin\ B\isasymrbrakk\ |
45 \isasymLongrightarrow\ c\ \isasymin\ A\ \isasyminter\ B% |
45 \isasymLongrightarrow\ c\ \isasymin\ A\ \isasyminter\ B% |
46 \rulename{IntI}\isanewline |
46 \rulename{IntI}\isanewline |
47 c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ A |
47 c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ A |
48 \rulename{IntD1}\isanewline |
48 \rulename{IntD1}\isanewline |
49 c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ B |
49 c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ B |
50 \rulename{IntD2} |
50 \rulename{IntD2} |
51 \end{isabelle} |
51 \end{isabelle} |
52 |
52 |
53 Here are two of the many installed theorems concerning set complement. |
53 Here are two of the many installed theorems concerning set |
|
54 complement.\index{complement!of a set}% |
54 Note that it is denoted by a minus sign. |
55 Note that it is denoted by a minus sign. |
55 \begin{isabelle} |
56 \begin{isabelle} |
56 (c\ \isasymin\ -\ A)\ =\ (c\ \isasymnotin\ A) |
57 (c\ \isasymin\ -\ A)\ =\ (c\ \isasymnotin\ A) |
57 \rulename{Compl_iff}\isanewline |
58 \rulename{Compl_iff}\isanewline |
58 -\ (A\ \isasymunion\ B)\ =\ -\ A\ \isasyminter\ -\ B |
59 -\ (A\ \isasymunion\ B)\ =\ -\ A\ \isasyminter\ -\ B |
124 \begin{isabelle} |
125 \begin{isabelle} |
125 ({\isasymAnd}x.\ (x\ {\isasymin}\ A)\ =\ (x\ {\isasymin}\ B))\ |
126 ({\isasymAnd}x.\ (x\ {\isasymin}\ A)\ =\ (x\ {\isasymin}\ B))\ |
126 {\isasymLongrightarrow}\ A\ =\ B |
127 {\isasymLongrightarrow}\ A\ =\ B |
127 \rulename{set_ext} |
128 \rulename{set_ext} |
128 \end{isabelle} |
129 \end{isabelle} |
129 Extensionality is often expressed as |
130 Extensionality can be expressed as |
130 $A=B\iff A\subseteq B\conj B\subseteq A$. |
131 $A=B\iff (A\subseteq B)\conj (B\subseteq A)$. |
131 The following rules express both |
132 The following rules express both |
132 directions of this equivalence. Proving a set equation using |
133 directions of this equivalence. Proving a set equation using |
133 \isa{equalityI} allows the two inclusions to be proved independently. |
134 \isa{equalityI} allows the two inclusions to be proved independently. |
134 \begin{isabelle} |
135 \begin{isabelle} |
135 \isasymlbrakk A\ \isasymsubseteq\ B;\ B\ \isasymsubseteq\ |
136 \isasymlbrakk A\ \isasymsubseteq\ B;\ B\ \isasymsubseteq\ |
143 \end{isabelle} |
144 \end{isabelle} |
144 |
145 |
145 |
146 |
146 \subsection{Finite Set Notation} |
147 \subsection{Finite Set Notation} |
147 |
148 |
148 \indexbold{sets!notation for finite}\index{*insert (constant)} |
149 \indexbold{sets!notation for finite} |
149 Finite sets are expressed using the constant \isa{insert}, which is |
150 Finite sets are expressed using the constant \cdx{insert}, which is |
150 a form of union: |
151 a form of union: |
151 \begin{isabelle} |
152 \begin{isabelle} |
152 insert\ a\ A\ =\ \isacharbraceleft a\isacharbraceright\ \isasymunion\ A |
153 insert\ a\ A\ =\ \isacharbraceleft a\isacharbraceright\ \isasymunion\ A |
153 \rulename{insert_is_Un} |
154 \rulename{insert_is_Un} |
154 \end{isabelle} |
155 \end{isabelle} |
230 \isanewline |
231 \isanewline |
231 \ \ \ \ \ \ \ \ \isacharbraceleft z.\ \isasymexists p\ q.\ z\ =\ p*q\ |
232 \ \ \ \ \ \ \ \ \isacharbraceleft z.\ \isasymexists p\ q.\ z\ =\ p*q\ |
232 \isasymand\ p{\isasymin}prime\ \isasymand\ |
233 \isasymand\ p{\isasymin}prime\ \isasymand\ |
233 q{\isasymin}prime\isacharbraceright" |
234 q{\isasymin}prime\isacharbraceright" |
234 \end{isabelle} |
235 \end{isabelle} |
235 The proof is trivial because the left and right hand side |
236 The left and right hand sides |
236 of the expression are synonymous. The syntax appearing on the |
237 of this equation are identical. The syntax used in the |
237 left-hand side abbreviates the right-hand side: in this case, all numbers |
238 left-hand side abbreviates the right-hand side: in this case, all numbers |
238 that are the product of two primes. The syntax provides a neat |
239 that are the product of two primes. The syntax provides a neat |
239 way of expressing any set given by an expression built up from variables |
240 way of expressing any set given by an expression built up from variables |
240 under specific constraints. The drawback is that it hides the true form of |
241 under specific constraints. The drawback is that it hides the true form of |
241 the expression, with its existential quantifiers. |
242 the expression, with its existential quantifiers. |
368 Unions, intersections and so forth are not simply replaced by their |
369 Unions, intersections and so forth are not simply replaced by their |
369 definitions. Instead, membership tests are simplified. For example, $x\in |
370 definitions. Instead, membership tests are simplified. For example, $x\in |
370 A\cup B$ is replaced by $x\in A\vee x\in B$. |
371 A\cup B$ is replaced by $x\in A\vee x\in B$. |
371 |
372 |
372 The internal form of a comprehension involves the constant |
373 The internal form of a comprehension involves the constant |
373 \isa{Collect},\index{*Collect (constant)} |
374 \cdx{Collect}, |
374 which occasionally appears when a goal or theorem |
375 which occasionally appears when a goal or theorem |
375 is displayed. For example, \isa{Collect\ P} is the same term as |
376 is displayed. For example, \isa{Collect\ P} is the same term as |
376 \isa{\isacharbraceleft x.\ P\ x\isacharbraceright}. The same thing can |
377 \isa{\isacharbraceleft x.\ P\ x\isacharbraceright}. The same thing can |
377 happen with quantifiers: \hbox{\isa{All\ P}}\index{*All (constant)} |
378 happen with quantifiers: \hbox{\isa{All\ P}}\index{*All (constant)} |
378 is |
379 is |
381 also \isa{Ball\ A\ P}\index{*Ball (constant)} is |
382 also \isa{Ball\ A\ P}\index{*Ball (constant)} is |
382 \isa{{\isasymforall}z\isasymin A.\ P\ x} and |
383 \isa{{\isasymforall}z\isasymin A.\ P\ x} and |
383 \isa{Bex\ A\ P}\index{*Bex (constant)} is |
384 \isa{Bex\ A\ P}\index{*Bex (constant)} is |
384 \isa{\isasymexists z\isasymin A.\ P\ x}. For indexed unions and |
385 \isa{\isasymexists z\isasymin A.\ P\ x}. For indexed unions and |
385 intersections, you may see the constants |
386 intersections, you may see the constants |
386 \isa{UNION}\index{*UNION (constant)} and |
387 \cdx{UNION} and \cdx{INTER}\@. |
387 \isa{INTER}\index{*INTER (constant)}\@. |
388 The internal constant for $\varepsilon x.P(x)$ is~\cdx{Eps}. |
388 The internal constant for $\varepsilon x.P(x)$ is |
|
389 \isa{Eps}\index{*Eps (constant)}. |
|
390 |
|
391 |
389 |
392 We have only scratched the surface of Isabelle/HOL's set theory. |
390 We have only scratched the surface of Isabelle/HOL's set theory. |
393 One primitive not mentioned here is the powerset operator |
391 Hundreds of theorems are proved in theory \isa{Set} and its |
394 {\isa{Pow}}. Hundreds of theorems are proved in theory \isa{Set} and its |
|
395 descendants. |
392 descendants. |
396 |
393 |
397 |
394 |
398 \subsection{Finiteness and Cardinality} |
395 \subsection{Finiteness and Cardinality} |
399 |
396 |
400 \index{sets!finite}% |
397 \index{sets!finite}% |
401 The predicate \isa{finite} holds of all finite sets. Isabelle/HOL includes |
398 The predicate \sdx{finite} holds of all finite sets. Isabelle/HOL |
402 many familiar theorems about finiteness and cardinality |
399 includes many familiar theorems about finiteness and cardinality |
403 (\isa{card}). For example, we have theorems concerning the cardinalities |
400 (\cdx{card}). For example, we have theorems concerning the |
404 of unions, intersections and the powerset:\index{cardinality} |
401 cardinalities of unions, intersections and the |
|
402 powerset:\index{cardinality} |
405 % |
403 % |
406 \begin{isabelle} |
404 \begin{isabelle} |
407 {\isasymlbrakk}finite\ A;\ finite\ B\isasymrbrakk\isanewline |
405 {\isasymlbrakk}finite\ A;\ finite\ B\isasymrbrakk\isanewline |
408 \isasymLongrightarrow\ card\ A\ \isacharplus\ card\ B\ =\ card\ (A\ \isasymunion\ B)\ \isacharplus\ card\ (A\ \isasyminter\ B) |
406 \isasymLongrightarrow\ card\ A\ \isacharplus\ card\ B\ =\ card\ (A\ \isasymunion\ B)\ \isacharplus\ card\ (A\ \isasyminter\ B) |
409 \rulename{card_Un_Int}% |
407 \rulename{card_Un_Int}% |
424 $k$-element subsets of~$A$ is \index{binomial coefficients} |
422 $k$-element subsets of~$A$ is \index{binomial coefficients} |
425 $\binom{n}{k}$. |
423 $\binom{n}{k}$. |
426 |
424 |
427 \begin{warn} |
425 \begin{warn} |
428 The term \isa{finite\ A} is defined via a syntax translation as an |
426 The term \isa{finite\ A} is defined via a syntax translation as an |
429 abbreviation for \isa{A \isasymin Finites}, where the constant \isa{Finites} |
427 abbreviation for \isa{A \isasymin Finites}, where the constant |
430 denotes the set of all finite sets of a given type. There is no constant |
428 \cdx{Finites} denotes the set of all finite sets of a given type. There |
431 \isa{finite}. |
429 is no constant \isa{finite}. |
432 \end{warn} |
430 \end{warn} |
433 \index{sets|)} |
431 \index{sets|)} |
434 |
432 |
435 |
433 |
436 \section{Functions} |
434 \section{Functions} |
452 \begin{isabelle} |
450 \begin{isabelle} |
453 ({\isasymAnd}x.\ f\ x\ =\ g\ x)\ {\isasymLongrightarrow}\ f\ =\ g |
451 ({\isasymAnd}x.\ f\ x\ =\ g\ x)\ {\isasymLongrightarrow}\ f\ =\ g |
454 \rulename{ext} |
452 \rulename{ext} |
455 \end{isabelle} |
453 \end{isabelle} |
456 |
454 |
457 \indexbold{function updates}% |
455 \indexbold{updating a function}% |
458 Function \textbf{update} is useful for modelling machine states. It has |
456 Function \textbf{update} is useful for modelling machine states. It has |
459 the obvious definition and many useful facts are proved about |
457 the obvious definition and many useful facts are proved about |
460 it. In particular, the following equation is installed as a simplification |
458 it. In particular, the following equation is installed as a simplification |
461 rule: |
459 rule: |
462 \begin{isabelle} |
460 \begin{isabelle} |
558 \begin{isabelle} |
556 \begin{isabelle} |
559 (f\ =\ g)\ =\ ({\isasymforall}x.\ f\ x\ =\ g\ x) |
557 (f\ =\ g)\ =\ ({\isasymforall}x.\ f\ x\ =\ g\ x) |
560 \rulename{expand_fun_eq} |
558 \rulename{expand_fun_eq} |
561 \end{isabelle} |
559 \end{isabelle} |
562 % |
560 % |
563 This is just a restatement of extensionality. Our lemma states |
561 This is just a restatement of |
564 that an injection can be cancelled from the left |
562 extensionality.\indexbold{extensionality!for functions} |
565 side of function composition: |
563 Our lemma |
|
564 states that an injection can be cancelled from the left side of |
|
565 function composition: |
566 \begin{isabelle} |
566 \begin{isabelle} |
567 \isacommand{lemma}\ "inj\ f\ \isasymLongrightarrow\ (f\ o\ g\ =\ f\ o\ h)\ =\ (g\ =\ h)"\isanewline |
567 \isacommand{lemma}\ "inj\ f\ \isasymLongrightarrow\ (f\ o\ g\ =\ f\ o\ h)\ =\ (g\ =\ h)"\isanewline |
568 \isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def)\isanewline |
568 \isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def)\isanewline |
569 \isacommand{apply}\ auto\isanewline |
569 \isacommand{apply}\ auto\isanewline |
570 \isacommand{done} |
570 \isacommand{done} |
616 \isacommand{lemma}\ "f\ `\ \isacharbraceleft(x,y){.}\ P\ x\ y\isacharbraceright\ =\ \isacharbraceleft f(x,y)\ \isacharbar\ x\ y.\ P\ x\ |
616 \isacommand{lemma}\ "f\ `\ \isacharbraceleft(x,y){.}\ P\ x\ y\isacharbraceright\ =\ \isacharbraceleft f(x,y)\ \isacharbar\ x\ y.\ P\ x\ |
617 y\isacharbraceright" |
617 y\isacharbraceright" |
618 \end{isabelle} |
618 \end{isabelle} |
619 |
619 |
620 \medskip |
620 \medskip |
621 A function's \textbf{range} is the set of values that the function can |
621 \index{range!of a function}% |
|
622 A function's \textbf{range} is the set of values that the function can |
622 take on. It is, in fact, the image of the universal set under |
623 take on. It is, in fact, the image of the universal set under |
623 that function. There is no constant {\isa{range}}. Instead, {\isa{range}} |
624 that function. There is no constant \isa{range}. Instead, |
624 abbreviates an application of image to {\isa{UNIV}}: |
625 \sdx{range} abbreviates an application of image to \isa{UNIV}: |
625 \begin{isabelle} |
626 \begin{isabelle} |
626 \ \ \ \ \ range\ f\ |
627 \ \ \ \ \ range\ f\ |
627 {\isasymrightleftharpoons}\ f`UNIV |
628 {\isasymrightleftharpoons}\ f`UNIV |
628 \end{isabelle} |
629 \end{isabelle} |
629 % |
630 % |
663 Id\ \isasymequiv\ \isacharbraceleft p.\ \isasymexists x.\ p\ =\ (x,x){\isacharbraceright}% |
664 Id\ \isasymequiv\ \isacharbraceleft p.\ \isasymexists x.\ p\ =\ (x,x){\isacharbraceright}% |
664 \rulename{Id_def} |
665 \rulename{Id_def} |
665 \end{isabelle} |
666 \end{isabelle} |
666 |
667 |
667 \indexbold{composition!of relations}% |
668 \indexbold{composition!of relations}% |
668 \textbf{Composition} of relations (the infix \isa{O}) is also available: |
669 \textbf{Composition} of relations (the infix \sdx{O}) is also |
|
670 available: |
669 \begin{isabelle} |
671 \begin{isabelle} |
670 r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright |
672 r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright |
671 \rulename{comp_def} |
673 \rulename{comp_def} |
672 \end{isabelle} |
674 \end{isabelle} |
673 % |
675 % |
713 A.\ (x,b)\ \isasymin\ r) |
715 A.\ (x,b)\ \isasymin\ r) |
714 \rulename{Image_iff} |
716 \rulename{Image_iff} |
715 \end{isabelle} |
717 \end{isabelle} |
716 It satisfies many similar laws. |
718 It satisfies many similar laws. |
717 |
719 |
718 %Image under relations, like image under functions, distributes over unions: |
720 \index{domain!of a relation}% |
719 %\begin{isabelle} |
721 \index{range!of a relation}% |
720 %r\ ``\ |
722 The \textbf{domain} and \textbf{range} of a relation are defined in the |
721 %({\isasymUnion}x\isasyminA.\ |
|
722 %B\ |
|
723 %x)\ =\ |
|
724 %({\isasymUnion}x\isasyminA.\ |
|
725 %r\ ``\ B\ |
|
726 %x) |
|
727 %\rulename{Image_UN} |
|
728 %\end{isabelle} |
|
729 |
|
730 |
|
731 The \bfindex{domain} and \bfindex{range} of a relation are defined in the |
|
732 standard way: |
723 standard way: |
733 \begin{isabelle} |
724 \begin{isabelle} |
734 (a\ \isasymin\ Domain\ r)\ =\ (\isasymexists y.\ (a,y)\ \isasymin\ |
725 (a\ \isasymin\ Domain\ r)\ =\ (\isasymexists y.\ (a,y)\ \isasymin\ |
735 r) |
726 r) |
736 \rulename{Domain_iff}% |
727 \rulename{Domain_iff}% |
741 \isasymin\ r) |
732 \isasymin\ r) |
742 \rulename{Range_iff} |
733 \rulename{Range_iff} |
743 \end{isabelle} |
734 \end{isabelle} |
744 |
735 |
745 Iterated composition of a relation is available. The notation overloads |
736 Iterated composition of a relation is available. The notation overloads |
746 that of exponentiation: |
737 that of exponentiation. Two simplification rules are installed: |
747 \begin{isabelle} |
738 \begin{isabelle} |
748 R\ \isacharcircum\ \isadigit{0}\ =\ Id\isanewline |
739 R\ \isacharcircum\ \isadigit{0}\ =\ Id\isanewline |
749 R\ \isacharcircum\ Suc\ n\ =\ R\ O\ R\isacharcircum n |
740 R\ \isacharcircum\ Suc\ n\ =\ R\ O\ R\isacharcircum n |
750 \rulename{relpow.simps} |
|
751 \end{isabelle} |
741 \end{isabelle} |
752 |
742 |
753 \subsection{The Reflexive and Transitive Closure} |
743 \subsection{The Reflexive and Transitive Closure} |
754 |
744 |
755 \index{closure!reflexive and transitive|(}% |
745 \index{closure!reflexive and transitive|(}% |
808 \rulename{trancl_converse} |
798 \rulename{trancl_converse} |
809 \end{isabelle} |
799 \end{isabelle} |
810 |
800 |
811 \subsection{A Sample Proof} |
801 \subsection{A Sample Proof} |
812 |
802 |
813 The reflexive transitive closure also commutes with the converse. |
803 The reflexive transitive closure also commutes with the converse |
814 Let us examine the proof. Each direction of the equivalence is |
804 operator. Let us examine the proof. Each direction of the equivalence |
815 proved separately. The two proofs are almost identical. Here |
805 is proved separately. The two proofs are almost identical. Here |
816 is the first one: |
806 is the first one: |
817 \begin{isabelle} |
807 \begin{isabelle} |
818 \isacommand{lemma}\ rtrancl_converseD:\ "(x,y)\ \isasymin \ |
808 \isacommand{lemma}\ rtrancl_converseD:\ "(x,y)\ \isasymin \ |
819 (r\isasyminverse)\isactrlsup *\ \isasymLongrightarrow \ (y,x)\ \isasymin |
809 (r\isasyminverse)\isactrlsup *\ \isasymLongrightarrow \ (y,x)\ \isasymin |
820 \ r\isactrlsup *"\isanewline |
810 \ r\isactrlsup *"\isanewline |
854 \isacommand{by}\ (auto\ intro:\ rtrancl_converseI\ dest:\ |
844 \isacommand{by}\ (auto\ intro:\ rtrancl_converseI\ dest:\ |
855 rtrancl_converseD) |
845 rtrancl_converseD) |
856 \end{isabelle} |
846 \end{isabelle} |
857 |
847 |
858 \begin{warn} |
848 \begin{warn} |
859 Note that \isa{blast} cannot prove this theorem. Here is a subgoal that |
849 This trivial proof requires \isa{auto} rather than \isa{blast} because |
860 arises internally after the rules \isa{equalityI} and \isa{subsetI} have |
850 of a subtle issue involving ordered pairs. Here is a subgoal that |
861 been applied: |
851 arises internally after the rules |
|
852 \isa{equalityI} and \isa{subsetI} have been applied: |
862 \begin{isabelle} |
853 \begin{isabelle} |
863 \ 1.\ \isasymAnd x.\ x\ \isasymin \ (r\isasyminverse )\isactrlsup *\ \isasymLongrightarrow \ x\ \isasymin \ (r\isactrlsup |
854 \ 1.\ \isasymAnd x.\ x\ \isasymin \ (r\isasyminverse )\isactrlsup *\ \isasymLongrightarrow \ x\ \isasymin \ (r\isactrlsup |
864 *)\isasyminverse |
855 *)\isasyminverse |
865 %ignore subgoal 2 |
856 %ignore subgoal 2 |
866 %\ 2.\ \isasymAnd x.\ x\ \isasymin \ (r\isactrlsup *)\isasyminverse \ |
857 %\ 2.\ \isasymAnd x.\ x\ \isasymin \ (r\isactrlsup *)\isasyminverse \ |
867 %\isasymLongrightarrow \ x\ \isasymin \ (r\isasyminverse )\isactrlsup * |
858 %\isasymLongrightarrow \ x\ \isasymin \ (r\isasyminverse )\isactrlsup * |
868 \end{isabelle} |
859 \end{isabelle} |
869 \par\noindent |
860 \par\noindent |
870 We cannot use \isa{rtrancl_converseD}\@. It refers to |
861 We cannot apply \isa{rtrancl_converseD}\@. It refers to |
871 ordered pairs, while \isa{x} is a variable of product type. |
862 ordered pairs, while \isa{x} is a variable of product type. |
872 The \isa{simp} and \isa{blast} methods can do nothing, so let us try |
863 The \isa{simp} and \isa{blast} methods can do nothing, so let us try |
873 \isa{clarify}: |
864 \isa{clarify}: |
874 \begin{isabelle} |
865 \begin{isabelle} |
875 \ 1.\ \isasymAnd a\ b.\ (a,b)\ \isasymin \ (r\isasyminverse )\isactrlsup *\ \isasymLongrightarrow \ (b,a)\ \isasymin \ r\isactrlsup |
866 \ 1.\ \isasymAnd a\ b.\ (a,b)\ \isasymin \ (r\isasyminverse )\isactrlsup *\ \isasymLongrightarrow \ (b,a)\ \isasymin \ r\isactrlsup |
886 \section{Well-Founded Relations and Induction} |
877 \section{Well-Founded Relations and Induction} |
887 \label{sec:Well-founded} |
878 \label{sec:Well-founded} |
888 |
879 |
889 \index{relations!well-founded|(}% |
880 \index{relations!well-founded|(}% |
890 A well-founded relation captures the notion of a terminating process. |
881 A well-founded relation captures the notion of a terminating process. |
891 Each \isacommand{recdef}\index{recdef@\isacommand{recdef}} |
882 Each \commdx{recdef} |
892 declaration must specify a well-founded relation that |
883 declaration must specify a well-founded relation that |
893 justifies the termination of the desired recursive function. Most of the |
884 justifies the termination of the desired recursive function. Most of the |
894 forms of induction found in mathematics are merely special cases of |
885 forms of induction found in mathematics are merely special cases of |
895 induction over a well-founded relation. |
886 induction over a well-founded relation. |
896 |
887 |
912 returned by |
903 returned by |
913 \isacommand{recdef} is good enough for most purposes. We use an explicit |
904 \isacommand{recdef} is good enough for most purposes. We use an explicit |
914 well-founded induction only in \S\ref{sec:CTL-revisited}. |
905 well-founded induction only in \S\ref{sec:CTL-revisited}. |
915 \end{warn} |
906 \end{warn} |
916 |
907 |
917 Isabelle/HOL declares \isa{less_than} as a relation object, |
908 Isabelle/HOL declares \cdx{less_than} as a relation object, |
918 that is, a set of pairs of natural numbers. Two theorems tell us that this |
909 that is, a set of pairs of natural numbers. Two theorems tell us that this |
919 relation behaves as expected and that it is well-founded: |
910 relation behaves as expected and that it is well-founded: |
920 \begin{isabelle} |
911 \begin{isabelle} |
921 ((x,y)\ \isasymin\ less_than)\ =\ (x\ <\ y) |
912 ((x,y)\ \isasymin\ less_than)\ =\ (x\ <\ y) |
922 \rulename{less_than_iff}\isanewline |
913 \rulename{less_than_iff}\isanewline |
948 \rulename{measure_def}\isanewline |
939 \rulename{measure_def}\isanewline |
949 wf\ (measure\ f) |
940 wf\ (measure\ f) |
950 \rulename{wf_measure} |
941 \rulename{wf_measure} |
951 \end{isabelle} |
942 \end{isabelle} |
952 |
943 |
953 Of the other constructions, the most important is the \textbf{lexicographic |
944 Of the other constructions, the most important is the |
954 product} of two relations. It expresses the standard dictionary |
945 \bfindex{lexicographic product} of two relations. It expresses the |
955 ordering over pairs. We write \isa{ra\ <*lex*>\ rb}, where \isa{ra} |
946 standard dictionary ordering over pairs. We write \isa{ra\ <*lex*>\ |
956 and \isa{rb} are the two operands. The lexicographic product satisfies the |
947 rb}, where \isa{ra} and \isa{rb} are the two operands. The |
957 usual definition and it preserves well-foundedness: |
948 lexicographic product satisfies the usual definition and it preserves |
|
949 well-foundedness: |
958 \begin{isabelle} |
950 \begin{isabelle} |
959 ra\ <*lex*>\ rb\ \isasymequiv \isanewline |
951 ra\ <*lex*>\ rb\ \isasymequiv \isanewline |
960 \ \ \isacharbraceleft ((a,b),(a',b')).\ (a,a')\ \isasymin \ ra\ |
952 \ \ \isacharbraceleft ((a,b),(a',b')).\ (a,a')\ \isasymin \ ra\ |
961 \isasymor\isanewline |
953 \isasymor\isanewline |
962 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \,a=a'\ \isasymand \ (b,b')\ |
954 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \,a=a'\ \isasymand \ (b,b')\ |
974 The \bfindex{multiset ordering}, useful for hard termination proofs, is |
966 The \bfindex{multiset ordering}, useful for hard termination proofs, is |
975 available in the Library. Baader and Nipkow \cite[\S2.5]{Baader-Nipkow} |
967 available in the Library. Baader and Nipkow \cite[\S2.5]{Baader-Nipkow} |
976 discuss it. |
968 discuss it. |
977 |
969 |
978 \medskip |
970 \medskip |
979 Induction comes in many forms, including traditional mathematical |
971 Induction\index{induction!well-founded|(} |
980 induction, structural induction on lists and induction on size. All are |
972 comes in many forms, |
981 instances of the following rule, for a suitable well-founded |
973 including traditional mathematical induction, structural induction on |
982 relation~$\prec$: |
974 lists and induction on size. All are instances of the following rule, |
|
975 for a suitable well-founded relation~$\prec$: |
983 \[ \infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}} \] |
976 \[ \infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}} \] |
984 To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for |
977 To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for |
985 arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$. |
978 arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$. |
986 Intuitively, the well-foundedness of $\prec$ ensures that the chains of |
979 Intuitively, the well-foundedness of $\prec$ ensures that the chains of |
987 reasoning are finite. |
980 reasoning are finite. |
999 |
992 |
1000 Many familiar induction principles are instances of this rule. |
993 Many familiar induction principles are instances of this rule. |
1001 For example, the predecessor relation on the natural numbers |
994 For example, the predecessor relation on the natural numbers |
1002 is well-founded; induction over it is mathematical induction. |
995 is well-founded; induction over it is mathematical induction. |
1003 The ``tail of'' relation on lists is well-founded; induction over |
996 The ``tail of'' relation on lists is well-founded; induction over |
1004 it is structural induction. |
997 it is structural induction.% |
|
998 \index{induction!well-founded|)}% |
1005 \index{relations!well-founded|)} |
999 \index{relations!well-founded|)} |
1006 |
1000 |
1007 |
1001 |
1008 \section{Fixed Point Operators} |
1002 \section{Fixed Point Operators} |
1009 |
1003 |