# HG changeset patch
# User paulson
# Date 868010253 -7200
# Node ID 04739732b13e5ffc8c2517f84d30eb2818e597e5
# Parent  f7ac2d1e2051690f43418e26ea7b2be3509e50d4
New comments on how to deal with unproved termination conditions

diff -r f7ac2d1e2051 -r 04739732b13e src/HOL/ex/Primes.ML
--- 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;
diff -r f7ac2d1e2051 -r 04739732b13e src/HOL/ex/Primes.thy
--- 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