--- a/src/HOL/ex/Primes.ML Fri Jul 04 11:56:49 1997 +0200
+++ b/src/HOL/ex/Primes.ML Fri Jul 04 11:57:33 1997 +0200
@@ -16,11 +16,14 @@
(** Greatest Common Divisor **)
(************************************************)
-(* Euclid's Algorithm *)
+(*** Euclid's Algorithm ***)
+(** Prove the termination condition and remove it from the recursion equations
+ and induction rule **)
+
Tfl.tgoalw thy [] gcd.rules;
-by (simp_tac (!simpset addsimps [mod_less_divisor,zero_less_eq]) 1);
+by (simp_tac (!simpset addsimps [mod_less_divisor, zero_less_eq]) 1);
val tc = result();
val gcd_eq = tc RS hd gcd.rules;
--- a/src/HOL/ex/Primes.thy Fri Jul 04 11:56:49 1997 +0200
+++ b/src/HOL/ex/Primes.thy Fri Jul 04 11:57:33 1997 +0200
@@ -4,6 +4,11 @@
Copyright 1996 University of Cambridge
The Greatest Common Divisor and Euclid's algorithm
+
+The "simpset" clause in the recdef declaration is omitted on purpose:
+ in order to demonstrate the treatment of definitions that have
+ unproved termination conditions. Restoring the clause lets
+ Isabelle prove those conditions.
*)
Primes = Divides + WF_Rel +
@@ -13,7 +18,8 @@
coprime :: [nat,nat]=>bool
prime :: nat set
-recdef gcd "measure ((%(x,y).y) ::nat*nat=>nat)"
+recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
+(* simpset "!simpset addsimps [mod_less_divisor, zero_less_eq]" *)
"gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
defs