(* \$Id: ex.thy,v 1.4 2010/11/29 07:13:36 kleing Exp \$ Author: Martin Strecker *) header {* The Euclidean Algorithm -- Inductively *} (*<*) theory ex imports Main begin (*>*) subsection {* Rules without base case *} text {* Show that the following *} inductive_set evenempty :: "nat set" where Add2Ie: "n \ evenempty \ Suc(Suc n) \ evenempty" text {* defines the empty set: *} lemma evenempty_empty: "evenempty = {}" (*<*) oops (*>*) subsection {* The Euclidean algorithm *} text {* Define inductively the set @{text gcd}, which characterizes the greatest common divisor of two natural numbers: *} (*<*)consts(*>*) gcd :: "(nat \ nat \ nat) set" text {* Here, @{text "(a,b,g) \ gcd"} means that @{text g} is the gcd of @{text a} und @{text b}. The definition should closely follow the Euclidean algorithm. Reminder: The Euclidean algorithm repeatedly subtracts the smaller from the larger number, until one of the numbers is 0. Then, the other number is the gcd. *} text {* Now, compute the gcd of 15 and 10: *} schematic_lemma "(15, 10, ?g) \ gcd" (*<*) oops (*>*) text {* How does your algorithm behave on special cases as the following? *} schematic_lemma "(0, 0, ?g) \ gcd" (*<*) oops (*>*) text {* Show that the gcd is really a divisor (for the proof, you need an appropriate lemma): *} lemma gcd_divides: "(a,b,g) \ gcd \ g dvd a \ g dvd b" (*<*) oops (*>*) text {* Show that the gcd is the greatest common divisor: *} lemma gcd_greatest [rule_format]: "(a,b,g) \ gcd \ 0 < a \ 0 < b \ (\ d. d dvd a \ d dvd b \ d \ g)" (*<*) oops (*>*) text {* Here as well, you will have to prove a suitable lemma. What is the precondition @{text "0 < a \ 0 < b"} good for? So far, we have only shown that @{text gcd} is correct, but your algorithm might not compute a result for all values @{text "a,b"}. Thus, show completeness of the algorithm: *} lemma gcd_defined: "\ a b. \ g. (a, b, g) \ gcd" (*<*) oops (*>*) text {* The following lemma, proved by course-of-value recursion over @{text n}, may be useful. Why does standard induction over natural numbers not work here? *} lemma gcd_defined_aux [rule_format]: "\ a b. (a + b) \ n \ (\ g. (a, b, g) \ gcd)" apply (induct rule: nat_less_induct) apply clarify (*<*) oops (*>*) text {* The idea is to show that @{text gcd} yields a result for all @{text "a, b"} whenever it is known that @{text gcd} yields a result for all @{text "a', b'"} whose sum is smaller than @{text "a + b"}. In order to prove this lemma, make case distinctions corresponding to the different clauses of the algorithm, and show how to reduce computation of @{text gcd} for @{text "a, b"} to computation of @{text gcd} for suitable smaller @{text "a', b'"}. *} (*<*) end (*>*)