(*
$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 (*>*)