|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{a{\isadigit{5}}}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsubsection{The Euclidean Algorithm -- Inductively% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \isamarkupsubsubsection{Rules without Base Case% |
|
11 } |
|
12 \isamarkuptrue% |
|
13 % |
|
14 \begin{isamarkuptext}% |
|
15 Show that the following% |
|
16 \end{isamarkuptext}% |
|
17 \isamarkuptrue% |
|
18 \isacommand{consts}\ evenempty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline |
|
19 \isamarkupfalse% |
|
20 \isacommand{inductive}\ evenempty\isanewline |
|
21 \ \ \isakeyword{intros}\isanewline |
|
22 \ \ Add{\isadigit{2}}Ie{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ evenempty\ {\isasymLongrightarrow}\ Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ evenempty{\isachardoublequote}\isamarkupfalse% |
|
23 % |
|
24 \begin{isamarkuptext}% |
|
25 defines the empty set:% |
|
26 \end{isamarkuptext}% |
|
27 \isamarkuptrue% |
|
28 \isacommand{lemma}\ evenempty{\isacharunderscore}empty{\isacharcolon}\ {\isachardoublequote}evenempty\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse% |
|
29 \isamarkupfalse% |
|
30 % |
|
31 \isamarkupsubsubsection{The Euclidean Algorithm% |
|
32 } |
|
33 \isamarkuptrue% |
|
34 % |
|
35 \begin{isamarkuptext}% |
|
36 Define inductively the set \isa{gcd}, which characterizes |
|
37 the greatest common divisor of two natural numbers:% |
|
38 \end{isamarkuptext}% |
|
39 \isamarkuptrue% |
|
40 \ \ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat{\isacharparenright}\ set{\isachardoublequote}\isamarkupfalse% |
|
41 % |
|
42 \begin{isamarkuptext}% |
|
43 Here, \isa{{\isacharparenleft}a{\isacharcomma}b{\isacharcomma}g{\isacharparenright}\ {\isasymin}\ gcd} means that \isa{g} is the gcd |
|
44 of \isa{a} und \isa{b}. The definition should closely follow the |
|
45 Euclidean algorithm. |
|
46 |
|
47 Reminder: The Euclidean algorithm repeatedly subtracts the smaller |
|
48 from the larger number, until one of the numbers is 0. Then, the other |
|
49 number is the gcd.% |
|
50 \end{isamarkuptext}% |
|
51 \isamarkuptrue% |
|
52 % |
|
53 \begin{isamarkuptext}% |
|
54 Now, compute the gcd of 15 and 10:% |
|
55 \end{isamarkuptext}% |
|
56 \isamarkuptrue% |
|
57 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}g{\isacharparenright}\ \ {\isasymin}\ gcd{\isachardoublequote}\isamarkupfalse% |
|
58 \isamarkupfalse% |
|
59 % |
|
60 \begin{isamarkuptext}% |
|
61 How does your algorithm behave on special cases as the following?% |
|
62 \end{isamarkuptext}% |
|
63 \isamarkuptrue% |
|
64 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isacharquery}g{\isacharparenright}\ \ {\isasymin}\ gcd{\isachardoublequote}\isamarkupfalse% |
|
65 \isamarkupfalse% |
|
66 % |
|
67 \begin{isamarkuptext}% |
|
68 Show that the gcd is really a divisor (for the proof, you need an appropriate lemma):% |
|
69 \end{isamarkuptext}% |
|
70 \isamarkuptrue% |
|
71 \isacommand{lemma}\ gcd{\isacharunderscore}divides{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}a{\isacharcomma}b{\isacharcomma}g{\isacharparenright}\ {\isasymin}\ gcd\ {\isasymLongrightarrow}\ g\ dvd\ a\ {\isasymand}\ g\ dvd\ b{\isachardoublequote}\isamarkupfalse% |
|
72 \isamarkupfalse% |
|
73 % |
|
74 \begin{isamarkuptext}% |
|
75 Show that the gcd is the greatest common divisor:% |
|
76 \end{isamarkuptext}% |
|
77 \isamarkuptrue% |
|
78 \isacommand{lemma}\ gcd{\isacharunderscore}greatest\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}a{\isacharcomma}b{\isacharcomma}g{\isacharparenright}\ {\isasymin}\ gcd\ {\isasymLongrightarrow}\isanewline |
|
79 \ \ {\isadigit{0}}\ {\isacharless}\ a\ {\isasymor}\ {\isadigit{0}}\ {\isacharless}\ b\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}\ d{\isachardot}\ d\ dvd\ a\ {\isasymlongrightarrow}\ d\ dvd\ b\ {\isasymlongrightarrow}\ d\ {\isasymle}\ g{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
80 \isamarkupfalse% |
|
81 % |
|
82 \begin{isamarkuptext}% |
|
83 Here as well, you will have to prove a suitable lemma. What is |
|
84 the precondition \isa{{\isadigit{0}}\ {\isacharless}\ a\ {\isasymor}\ {\isadigit{0}}\ {\isacharless}\ b} good for? |
|
85 |
|
86 So far, we have only shown that \isa{gcd} is correct, but your |
|
87 algorithm might not compute a result for all values \isa{a{\isacharcomma}b}. Thus, show completeness of the algorithm:% |
|
88 \end{isamarkuptext}% |
|
89 \isamarkuptrue% |
|
90 \isacommand{lemma}\ gcd{\isacharunderscore}defined{\isacharcolon}\ {\isachardoublequote}{\isasymforall}\ a\ b{\isachardot}\ {\isasymexists}\ g{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharcomma}\ g{\isacharparenright}\ {\isasymin}\ gcd{\isachardoublequote}\isamarkupfalse% |
|
91 \isamarkupfalse% |
|
92 % |
|
93 \begin{isamarkuptext}% |
|
94 The following lemma, proved by course-of-value recursion over |
|
95 \isa{n}, may be useful. Why does standard induction over natural |
|
96 numbers not work here?% |
|
97 \end{isamarkuptext}% |
|
98 \isamarkuptrue% |
|
99 \isacommand{lemma}\ gcd{\isacharunderscore}defined{\isacharunderscore}aux\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \isanewline |
|
100 \ \ {\isachardoublequote}{\isasymforall}\ a\ b{\isachardot}\ {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isasymle}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ g{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharcomma}\ g{\isacharparenright}\ {\isasymin}\ gcd{\isacharparenright}{\isachardoublequote}\isanewline |
|
101 \isamarkupfalse% |
|
102 \isacommand{apply}\ {\isacharparenleft}induct\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}\isanewline |
|
103 \isamarkupfalse% |
|
104 \isacommand{apply}\ clarify\isanewline |
|
105 \isamarkupfalse% |
|
106 \isamarkupfalse% |
|
107 % |
|
108 \begin{isamarkuptext}% |
|
109 The idea is to show that \isa{gcd} yields a result for all |
|
110 \isa{a{\isacharcomma}\ b} whenever it is known that \isa{gcd} yields a result |
|
111 for all \isa{a{\isacharprime}{\isacharcomma}\ b{\isacharprime}} whose sum is smaller than \isa{a\ {\isacharplus}\ b}. |
|
112 |
|
113 In order to prove this lemma, make case distinctions corresponding to |
|
114 the different clauses of the algorithm, and show how to reduce |
|
115 computation of \isa{gcd} for \isa{a{\isacharcomma}\ b} to computation of \isa{gcd} for suitable smaller \isa{a{\isacharprime}{\isacharcomma}\ b{\isacharprime}}.% |
|
116 \end{isamarkuptext}% |
|
117 \isamarkuptrue% |
|
118 \isanewline |
|
119 \isamarkupfalse% |
|
120 \end{isabellebody}% |
|
121 %%% Local Variables: |
|
122 %%% mode: latex |
|
123 %%% TeX-master: "root" |
|
124 %%% End: |