New comments on how to deal with unproved termination conditions
authorpaulson
Fri Jul 04 11:57:33 1997 +0200 (1997-07-04)
changeset 349504739732b13e
parent 3494 f7ac2d1e2051
child 3496 32e7edc609fd
New comments on how to deal with unproved termination conditions
src/HOL/ex/Primes.ML
src/HOL/ex/Primes.thy
     1.1 --- a/src/HOL/ex/Primes.ML	Fri Jul 04 11:56:49 1997 +0200
     1.2 +++ b/src/HOL/ex/Primes.ML	Fri Jul 04 11:57:33 1997 +0200
     1.3 @@ -16,11 +16,14 @@
     1.4  (** Greatest Common Divisor                    **)
     1.5  (************************************************)
     1.6  
     1.7 -(* Euclid's Algorithm *)
     1.8 +(*** Euclid's Algorithm ***)
     1.9  
    1.10  
    1.11 +(** Prove the termination condition and remove it from the recursion equations
    1.12 +    and induction rule **)
    1.13 +
    1.14  Tfl.tgoalw thy [] gcd.rules;
    1.15 -by (simp_tac (!simpset addsimps [mod_less_divisor,zero_less_eq]) 1);
    1.16 +by (simp_tac (!simpset addsimps [mod_less_divisor, zero_less_eq]) 1);
    1.17  val tc = result();
    1.18  
    1.19  val gcd_eq = tc RS hd gcd.rules;
     2.1 --- a/src/HOL/ex/Primes.thy	Fri Jul 04 11:56:49 1997 +0200
     2.2 +++ b/src/HOL/ex/Primes.thy	Fri Jul 04 11:57:33 1997 +0200
     2.3 @@ -4,6 +4,11 @@
     2.4      Copyright   1996  University of Cambridge
     2.5  
     2.6  The Greatest Common Divisor and Euclid's algorithm
     2.7 +
     2.8 +The "simpset" clause in the recdef declaration is omitted on purpose:
     2.9 +	in order to demonstrate the treatment of definitions that have
    2.10 +	unproved termination conditions.  Restoring the clause lets
    2.11 +	Isabelle prove those conditions.
    2.12  *)
    2.13  
    2.14  Primes = Divides + WF_Rel +
    2.15 @@ -13,7 +18,8 @@
    2.16    coprime :: [nat,nat]=>bool
    2.17    prime   :: nat set
    2.18    
    2.19 -recdef gcd "measure ((%(x,y).y) ::nat*nat=>nat)"
    2.20 +recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
    2.21 +(*  simpset "!simpset addsimps [mod_less_divisor, zero_less_eq]" *)
    2.22      "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
    2.23  
    2.24  defs